gramSchmidtOrthonormalBasis_apply_of_orthogonal

English

If the vectors are pairwise orthogonal and the i-th vector is nonzero, then gramSchmidtOrthonormalBasis h f i equals a scaled version of f i by its norm inverse.

Русский

Если векторы попарно ортогональны и i-й вектор не нулевой, то старая позиция i совпадает с нормированной копией f i.

LaTeX

$$$$ \mathrm{gramSchmidtOrthonormalBasis}(h,f)_i = \|f_i\|^{-1} f_i \quad \text{when } \langle f_i, f_j \rangle = 0 \ (i\neq j) \text{ and } f_i \neq 0. $$$$

Lean4

theorem gramSchmidtOrthonormalBasis_apply_of_orthogonal {f : ι → E} (hf : Pairwise fun i j => ⟪f i, f j⟫ = 0) {i : ι}
    (hi : f i ≠ 0) : gramSchmidtOrthonormalBasis h f i = (‖f i‖⁻¹ : 𝕜) • f i :=
  by
  have H : gramSchmidtNormed 𝕜 f i = (‖f i‖⁻¹ : 𝕜) • f i := by rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]
  rw [gramSchmidtOrthonormalBasis_apply h, H]
  simpa [H] using hi

Похожие утверждения