Commit 2023-05-30 07:01 56e41333

View on Github →

feat: port Analysis.InnerProductSpace.GramSchmidtOrtho (#4473)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

added theorem coe_gramSchmidtBasis

added theorem gramSchmidtNormed_unit_length'

added theorem gramSchmidtNormed_unit_length

added theorem gramSchmidtNormed_unit_length_coe

added theorem gramSchmidtOrthonormalBasis_apply

added theorem gramSchmidtOrthonormalBasis_apply_of_orthogonal

added theorem gramSchmidtOrthonormalBasis_det

added theorem gramSchmidtOrthonormalBasis_inv_blockTriangular

added theorem gramSchmidtOrthonormalBasis_inv_triangular'

added theorem gramSchmidtOrthonormalBasis_inv_triangular

added theorem gramSchmidt_def''

added theorem gramSchmidt_def'

added theorem gramSchmidt_def

added theorem gramSchmidt_inv_triangular

added theorem gramSchmidt_linearIndependent

added theorem gramSchmidt_mem_span

added theorem gramSchmidt_ne_zero

added theorem gramSchmidt_ne_zero_coe

added theorem gramSchmidt_of_orthogonal

added theorem gramSchmidt_orthogonal

added theorem gramSchmidt_orthonormal'

added theorem gramSchmidt_orthonormal

added theorem gramSchmidt_pairwise_orthogonal

added theorem gramSchmidt_triangular

added theorem gramSchmidt_zero

added theorem inner_gramSchmidtOrthonormalBasis_eq_zero

added theorem mem_span_gramSchmidt

added theorem span_gramSchmidt

added theorem span_gramSchmidtNormed

added theorem span_gramSchmidtNormed_range

added theorem span_gramSchmidt_Iic

added theorem span_gramSchmidt_Iio