Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-28 08:12 82481e30

View on Github →

feat(analysis/normed_space/inner_product): existence of orthonormal basis (#5734) Define orthonormal sets (indexed) of vectors in an inner product space E. Show that a finite-dimensional inner product space has an orthonormal basis. Co-authored by: Busiso Chisala

Estimated changes

Modified docs/undergrad.yaml

Modified src/algebra/group_power/basic.lean

added theorem eq_of_pow_two_eq_pow_two

Modified src/analysis/normed_space/inner_product.lean

added theorem exists_is_orthonormal_basis

added theorem exists_is_orthonormal_dense_span

added theorem exists_maximal_orthonormal

added theorem exists_subset_is_orthonormal_basis

added theorem exists_subset_is_orthonormal_dense_span

added theorem finsupp.inner_sum

added theorem finsupp.sum_inner

added theorem inner_self_eq_norm_sq_to_K

added def is_basis.equiv_fun_euclidean

added theorem is_basis_of_orthonormal_of_card_eq_findim

added theorem maximal_orthonormal_iff_dense_span

added theorem maximal_orthonormal_iff_is_basis_of_finite_dimensional

added theorem maximal_orthonormal_iff_orthogonal_complement_eq_bot

added theorem orthonormal.inner_finsupp_eq_zero

added theorem orthonormal.inner_left_finsupp

added theorem orthonormal.inner_right_finsupp

added theorem orthonormal.linear_independent

added theorem orthonormal.ne_zero

added def orthonormal

added theorem orthonormal_Union_of_directed

added theorem orthonormal_empty

added theorem orthonormal_iff_ite

added theorem orthonormal_sUnion_of_directed

added theorem orthonormal_subtype_iff_ite

added theorem submodule.coe_inner

added theorem submodule.inf_orthogonal_eq_bot

Modified src/data/complex/is_R_or_C.lean

added theorem norm_smul_inv_norm

Modified src/data/finsupp/basic.lean

modified theorem finsupp.prod_ite_eq'

modified theorem finsupp.prod_ite_eq

added theorem finsupp.sum_ite_self_eq'

added theorem finsupp.sum_ite_self_eq