English
If vectors are pairwise orthogonal and the i-th vector is nonzero, then the i-th basis vector equals a normalized version of that vector.
Русский
Если векторы попарно ортогональны и i-й вектор ненулевой, то i-й вектор базиса равен нормализации этого вектора.
LaTeX
$$$$ \text{If } \langle f_i, f_j \rangle = 0 \ (i\neq j) \text{ and } f_i \neq 0, \quad \mathrm{gramSchmidtOrthonormalBasis}(h,f)_i = \frac{1}{\|f_i\|} f_i. $$$$
Lean4
theorem span_gramSchmidtNormed (f : ι → E) (s : Set ι) :
span 𝕜 (gramSchmidtNormed 𝕜 f '' s) = span 𝕜 (gramSchmidt 𝕜 f '' s) :=
by
refine
span_eq_span (Set.image_subset_iff.2 fun i hi => smul_mem _ _ <| subset_span <| mem_image_of_mem _ hi)
(Set.image_subset_iff.2 fun i hi => span_mono (image_mono <| singleton_subset_set_iff.2 hi) ?_)
simp only [coe_singleton, Set.image_singleton]
by_cases h : gramSchmidt 𝕜 f i = 0
· simp [h]
· refine mem_span_singleton.2 ⟨‖gramSchmidt 𝕜 f i‖, smul_inv_smul₀ ?_ _⟩
exact mod_cast norm_ne_zero_iff.2 h
