gramSchmidtNormed_orthonormal — Mathlib

English

A variant asserting the same vanishing inner products for the primed basis representation.

Русский

Вариант утверждает ту же нулевую проективность скалярного произведения для представления с пометкой 'прикрепления'.

LaTeX

$$$$\langle (\mathrm{gramSchmidtOrthonormalBasis}(h,f))_j, f_i \rangle = 0 \quad \text{for } i

Lean4

/-- **Gram-Schmidt Orthonormalization**:
`gramSchmidtNormed` applied to a linearly independent set of vectors produces an orthornormal
system of vectors. -/
theorem gramSchmidtNormed_orthonormal {f : ι → E} (h₀ : LinearIndependent 𝕜 f) :
    Orthonormal 𝕜 (gramSchmidtNormed 𝕜 f) := by
  unfold Orthonormal
  constructor
  · simp only [gramSchmidtNormed_unit_length, h₀, imp_true_iff]
  · intro i j hij
    simp only [gramSchmidtNormed, inner_smul_left, inner_smul_right, RCLike.conj_inv, RCLike.conj_ofReal, mul_eq_zero,
      inv_eq_zero, RCLike.ofReal_eq_zero, norm_eq_zero]
    repeat' right
    exact gramSchmidt_orthogonal 𝕜 f hij

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