English
If the input vectors are linearly independent, then the Gram-Schmidt output is a linearly independent family.
Русский
Если входные векторы линейно независимы, то выход Gram-Schmidt образует линейно независимую систему.
LaTeX
$$$$\text{If } f \text{ is LI, then } \mathrm{gramSchmidt}_{\mathbb{K}} f \text{ is LI}. $$$$
Lean4
/-- `gramSchmidt` produces a triangular matrix of vectors when given a basis. -/
theorem gramSchmidt_triangular {i j : ι} (hij : i < j) (b : Basis ι 𝕜 E) : b.repr (gramSchmidt 𝕜 b i) j = 0 :=
by
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (gramSchmidt 𝕜 b '' Set.Iio j) :=
subset_span ((Set.mem_image _ _ _).2 ⟨i, hij, rfl⟩)
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (b '' Set.Iio j) := by rwa [← span_gramSchmidt_Iio 𝕜 b j]
have : ↑(b.repr (gramSchmidt 𝕜 b i)).support ⊆ Set.Iio j := Basis.repr_support_subset_of_mem_span b (Set.Iio j) this
exact (Finsupp.mem_supported' _ _).1 ((Finsupp.mem_supported 𝕜 _).2 this) j Set.notMem_Iio_self
