gramSchmidt_inv_triangular — Mathlib

English

If i < j, then ⟪gramSchmidt 𝕜 v j, v i⟫ = 0, i.e., the GramSchmidt vector at j is orthogonal to v_i for i < j.

Русский

Если i < j, то ⟪gramSchmidt 𝕜 v j, v i⟫ = 0, то есть вектор GramSchmidt с индексом j ортогонален v_i для i < j.

LaTeX

$$$ \langle \mathrm{gramSchmidt}_{\mathbb{K}}(v)(j), v(i) \rangle = 0 \quad \text{если } i < j$$$

Lean4

theorem gramSchmidt_inv_triangular (v : ι → E) {i j : ι} (hij : i < j) : ⟪gramSchmidt 𝕜 v j, v i⟫ = 0 :=
  by
  rw [gramSchmidt_def'' 𝕜 v]
  simp only [inner_add_right, inner_sum, inner_smul_right]
  set b : ι → E := gramSchmidt 𝕜 v
  convert zero_add (0 : 𝕜)
  · exact gramSchmidt_orthogonal 𝕜 v hij.ne'
  apply Finset.sum_eq_zero
  rintro k hki'
  have hki : k < i := by simpa using hki'
  have : ⟪b j, b k⟫ = 0 := gramSchmidt_orthogonal 𝕜 v (hki.trans hij).ne'
  simp [this]

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