Commit 2022-02-19 18:23 e88badbf

View on Github →

feat(analysis/inner_product_space/pi_L2): Orthonormal basis (#12060) Added the structure orthonormal_basis and basic associated API Renamed the previous definition orthonormal_basis in analysis/inner_product_space/projection to std_orthonormal_basis

Estimated changes

Modified src/analysis/inner_product_space/orientation.lean

Modified src/analysis/inner_product_space/pi_L2.lean

deleted theorem basis.coe_isometry_euclidean_of_orthonormal

deleted theorem basis.coe_isometry_euclidean_of_orthonormal_symm

added theorem basis.coe_to_orthonormal_basis

added theorem basis.coe_to_orthonormal_basis_repr

added theorem basis.coe_to_orthonormal_basis_repr_symm

deleted def basis.isometry_euclidean_of_orthonormal

added theorem basis.to_basis_to_orthonormal_basis

added def basis.to_orthonormal_basis

added theorem euclidean_space.inner_single_left

added theorem euclidean_space.inner_single_right

added def euclidean_space.single

added theorem euclidean_space.single_apply

added structure orthonormal_basis

Modified src/analysis/inner_product_space/projection.lean

deleted theorem coe_orthonormal_basis

added theorem coe_std_orthonormal_basis

deleted def fin_orthonormal_basis

deleted theorem fin_orthonormal_basis_orthonormal

added def fin_std_orthonormal_basis

added theorem fin_std_orthonormal_basis_orthonormal

deleted def orthonormal_basis

deleted theorem orthonormal_basis_orthonormal

added def std_orthonormal_basis

added theorem std_orthonormal_basis_orthonormal

Modified src/analysis/inner_product_space/spectrum.lean

Modified src/linear_algebra/basis.lean

added theorem basis.of_equiv_fun_equiv_fun