Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 19:11 5b774133

View on Github →

refactor(analysis/inner_product_space/pi_L2): change std_orthonormal_basis to type orthonormal_basis (#12253)

Estimated changes

Modified src/analysis/inner_product_space/orientation.lean

Modified src/analysis/inner_product_space/pi_L2.lean

added theorem coe_std_orthonormal_basis

added theorem direct_sum.is_internal.collected_orthonormal_basis_mem

added def direct_sum.is_internal.sigma_orthonormal_basis_index_equiv

added def direct_sum.is_internal.subordinate_orthonormal_basis

added def direct_sum.is_internal.subordinate_orthonormal_basis_index

added theorem direct_sum.is_internal.subordinate_orthonormal_basis_subordinate

added theorem euclidean_space.pi_Lp_congr_left_single

added theorem exists_orthonormal_basis

added def fin_std_orthonormal_basis

deleted def linear_isometry_equiv.from_orthogonal_span_singleton

deleted def linear_isometry_equiv.of_inner_product_space

added theorem orthonormal.exists_orthonormal_basis_extension

added theorem orthonormal_basis.coe_of_repr

added def orthonormal_basis.from_orthogonal_span_singleton

added def orthonormal_basis.reindex

added def orthonormal_basis_index

added def std_orthonormal_basis

Modified src/analysis/inner_product_space/projection.lean

deleted theorem coe_std_orthonormal_basis

deleted def direct_sum.is_internal.sigma_orthonormal_basis_index_equiv

deleted def direct_sum.is_internal.subordinate_orthonormal_basis

deleted def direct_sum.is_internal.subordinate_orthonormal_basis_index

deleted theorem direct_sum.is_internal.subordinate_orthonormal_basis_orthonormal

deleted theorem direct_sum.is_internal.subordinate_orthonormal_basis_subordinate

deleted theorem exists_subset_is_orthonormal_basis

deleted def fin_std_orthonormal_basis

deleted theorem fin_std_orthonormal_basis_orthonormal

deleted def orthonormal_basis_index

deleted def std_orthonormal_basis

deleted theorem std_orthonormal_basis_orthonormal

Modified src/analysis/inner_product_space/spectrum.lean

deleted theorem inner_product_space.is_self_adjoint.diagonalization_basis_symm_apply

deleted theorem inner_product_space.is_self_adjoint.eigenvector_basis_orthonormal

Modified src/analysis/normed_space/pi_Lp.lean

added def linear_isometry_equiv.pi_Lp_congr_left

added theorem linear_isometry_equiv.pi_Lp_congr_left_apply

added theorem linear_isometry_equiv.pi_Lp_congr_left_single

added theorem linear_isometry_equiv.pi_Lp_congr_left_symm

Modified src/geometry/manifold/instances/sphere.lean

Modified src/linear_algebra/finite_dimensional.lean

added theorem linear_independent.finite

Modified src/linear_algebra/matrix/spectrum.lean