gramSchmidtOrthonormalBasis_inv_triangular

English

In a triangular arrangement, the inner product between the j-th orthonormal basis vector and the i-th original vector vanishes for i < j.

Русский

В треугольной схеме внутреннее произведение между j-м вектором ортонормированного базиса и i-м исходным вектором равно 0 при i < j.

LaTeX

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

Lean4

theorem gramSchmidtOrthonormalBasis_inv_triangular {i j : ι} (hij : i < j) :
    ⟪gramSchmidtOrthonormalBasis h f j, f i⟫ = 0 :=
  by
  by_cases hi : gramSchmidtNormed 𝕜 f j = 0
  · rw [inner_gramSchmidtOrthonormalBasis_eq_zero h hi]
  ·
    simp [gramSchmidtOrthonormalBasis_apply h hi, gramSchmidtNormed, inner_smul_left,
      gramSchmidt_inv_triangular 𝕜 f hij]

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