English
If the input family is pairwise orthogonal, Gram-Schmidt leaves the input vectors unchanged.
Русский
Если входная система векторов попарно ортогональна, то Gram-Schmidt оставляет их без изменений.
LaTeX
$$$$\text{If } \langle f_i, f_j \rangle = 0 \ (i\neq j), \quad \mathrm{gramSchmidt}_{\mathbb{K}} f = f.$$$$
Lean4
/-- If given an orthogonal set of vectors, `gramSchmidt` fixes its input. -/
theorem gramSchmidt_of_orthogonal {f : ι → E} (hf : Pairwise (⟪f ·, f ·⟫ = 0)) : gramSchmidt 𝕜 f = f :=
by
ext i
rw [gramSchmidt_def]
trans f i - 0
· congr
apply Finset.sum_eq_zero
intro j hj
rw [Submodule.starProjection_apply, Submodule.coe_eq_zero]
suffices span 𝕜 (f '' Set.Iic j) ⟂ 𝕜 ∙ f i
by
apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
rw [mem_orthogonal_singleton_iff_inner_left, ← mem_orthogonal_singleton_iff_inner_right]
exact this (gramSchmidt_mem_span 𝕜 f (le_refl j))
rw [isOrtho_span]
rintro u ⟨k, hk, rfl⟩ v (rfl : v = f i)
apply hf
exact (lt_of_le_of_lt hk (Finset.mem_Iio.mp hj)).ne
· simp
