English
If gramSchmidtNormed i = 0, then the inner product with any j-th basis vector is zero.
Русский
Если gramSchmidtNormed i = 0, то скалярное произведение с любым вектором базиса равно 0.
LaTeX
$$$$ \langle \mathrm{gramSchmidtOrthonormalBasis}(h,f)_i, f_j \rangle = 0 \\text{whenever } \mathrm{gramSchmidtNormed}_{\mathbb{K}} f(i) = 0.$$$$
Lean4
theorem inner_gramSchmidtOrthonormalBasis_eq_zero {f : ι → E} {i : ι} (hi : gramSchmidtNormed 𝕜 f i = 0) (j : ι) :
⟪gramSchmidtOrthonormalBasis h f i, f j⟫ = 0 :=
by
rw [← mem_orthogonal_singleton_iff_inner_right]
suffices span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ gramSchmidtOrthonormalBasis h f i
by
apply this
rw [span_gramSchmidtNormed]
exact mem_span_gramSchmidt 𝕜 f le_rfl
rw [isOrtho_span]
rintro u ⟨k, _, rfl⟩ v (rfl : v = _)
by_cases hk : gramSchmidtNormed 𝕜 f k = 0
· rw [hk, inner_zero_left]
rw [← gramSchmidtOrthonormalBasis_apply h hk]
have : k ≠ i := by
rintro rfl
exact hk hi
exact (gramSchmidtOrthonormalBasis h f).orthonormal.2 this
