The diagonal coefficient of the Gram-Schmidt process #
Mathlib's InnerProductSpace.gramSchmidt_triangular records that, in the basis b it is fed,
gramSchmidt 𝕜 b i has no component along b j for i < j. This file supplies the diagonal
companion: the component along b i itself is 1, because the Gram-Schmidt step subtracts from
b i only vectors spanned by the earlier basis vectors. Together the two say that the matrix of
the Gram-Schmidt process is lower unitriangular.
Main results #
Module.Basis.repr_gramSchmidt_self_eq_one— the Gram-Schmidt process leaves the coefficient of a basis vector along itself equal to1.
@[simp]
theorem
Module.Basis.repr_gramSchmidt_self_eq_one
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{ι : Type u_3}
[LinearOrder ι]
[LocallyFiniteOrderBot ι]
[WellFoundedLT ι]
(b : Basis ι 𝕜 E)
(i : ι)
:
The Gram-Schmidt process does not change the coefficient of a basis vector along itself:
gramSchmidt 𝕜 b i differs from b i by a combination of the strictly earlier gramSchmidt
vectors, each of which has no component along b i.