English
Given nonzero gramSchmidtNormed components, the basis vector equals the corresponding Gram–Schmidt vector.
Русский
При не нулевых компонентах gramSchmidtNormed основание базиса совпадает с соответствующим вектором Gram-Schmidt.
LaTeX
$$$$ \mathrm{gramSchmidtOrthonormalBasis}(h,f)_i = \mathrm{gramSchmidtNormed}_{\mathbb{K}} f(i) \quad (\text{when } \mathrm{gramSchmidtNormed}_{\mathbb{K}} f(i) \neq 0). $$$$
Lean4
/-- **Gram-Schmidt Orthonormalization**:
`gramSchmidtNormed` produces an orthornormal system of vectors after removing the vectors which
become zero in the process. -/
theorem gramSchmidtNormed_orthonormal' (f : ι → E) :
Orthonormal 𝕜 fun i : {i | gramSchmidtNormed 𝕜 f i ≠ 0} => gramSchmidtNormed 𝕜 f i :=
by
refine ⟨fun i => gramSchmidtNormed_unit_length' i.prop, ?_⟩
rintro i j (hij : ¬_)
rw [Subtype.ext_iff] at hij
simp [gramSchmidtNormed, inner_smul_left, inner_smul_right, gramSchmidt_orthogonal 𝕜 f hij]
