Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 02:46 a2323660

View on Github →

feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an orthogonal_family (#10208) In a finite-dimensional inner product space of E, there exists an orthonormal basis subordinate to a given direct sum decomposition into an orthogonal_family of subspaces E.

Estimated changes

Modified src/algebra/direct_sum/module.lean

added theorem direct_sum.submodule_is_internal.collected_basis_coe

added theorem direct_sum.submodule_is_internal.collected_basis_mem

Modified src/analysis/inner_product_space/basic.lean

added theorem direct_sum.submodule_is_internal.collected_basis_orthonormal

added theorem orthogonal_family.orthonormal_sigma_orthonormal

Modified src/analysis/inner_product_space/projection.lean

modified theorem coe_orthonormal_basis

added def direct_sum.submodule_is_internal.sigma_orthonormal_basis_index_equiv

added def direct_sum.submodule_is_internal.subordinate_orthonormal_basis

added def direct_sum.submodule_is_internal.subordinate_orthonormal_basis_index

added theorem direct_sum.submodule_is_internal.subordinate_orthonormal_basis_orthonormal

added theorem direct_sum.submodule_is_internal.subordinate_orthonormal_basis_subordinate

modified def fin_orthonormal_basis

modified theorem fin_orthonormal_basis_orthonormal

modified def orthonormal_basis

modified def orthonormal_basis_index

modified theorem orthonormal_basis_orthonormal

Modified src/data/finsupp/to_dfinsupp.lean

added theorem sigma_finsupp_equiv_dfinsupp_single