English
For a ≠ b, the Gram-Schmidt vectors at indices a and b are orthogonal: ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0.
Русский
Для a ≠ b векторы GramSchmidt 𝕜 f на позициях a и b ортогональны: ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0.
LaTeX
$$$ \langle \mathrm{gramSchmidt}_{\mathbb{K}}(f)(a), \mathrm{gramSchmidt}_{\mathbb{K}}(f)(b) \rangle = 0 \quad (a \neq b) $$$
Lean4
/-- **Gram-Schmidt Orthogonalisation**:
`gramSchmidt` produces an orthogonal system of vectors. -/
theorem gramSchmidt_orthogonal (f : ι → E) {a b : ι} (h₀ : a ≠ b) : ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0 :=
by
suffices ∀ a b : ι, a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0
by
rcases h₀.lt_or_gt with ha | hb
· exact this _ _ ha
· rw [inner_eq_zero_symm]
exact this _ _ hb
clear h₀ a b
intro a b h₀
revert a
apply wellFounded_lt.induction b
intro b ih a h₀
simp only [gramSchmidt_def 𝕜 f b, inner_sub_right, inner_sum, starProjection_singleton, inner_smul_right]
rw [Finset.sum_eq_single_of_mem a (Finset.mem_Iio.mpr h₀)]
· by_cases h : gramSchmidt 𝕜 f a = 0
· simp only [h, inner_zero_left, zero_div, zero_mul, sub_zero]
· rw [RCLike.ofReal_pow, ← inner_self_eq_norm_sq_to_K, div_mul_cancel₀, sub_self]
rwa [inner_self_ne_zero]
intro i hi hia
simp only [mul_eq_zero, div_eq_zero_iff]
right
rcases hia.lt_or_gt with hia₁ | hia₂
· rw [inner_eq_zero_symm]
exact ih a h₀ i hia₁
· exact ih i (mem_Iio.1 hi) a hia₂
