hasSum_inner_mul_inner — Mathlib

English

For a subspace U, the orthogonal projection of x is the sum of inner products with basis vectors times those vectors.

Русский

Проекция на ортогональное дополнение даёт соответствующий суммовый разложение по базису.

LaTeX

$$$ U.orthogonalProjection x = \\sum_i ⟪x, b_i⟫ · b_i $$$

Lean4

protected theorem hasSum_inner_mul_inner (b : HilbertBasis ι 𝕜 E) (x y : E) :
    HasSum (fun i => ⟪x, b i⟫ * ⟪b i, y⟫) ⟪x, y⟫ :=
  by
  convert (b.hasSum_repr y).mapL (innerSL 𝕜 x) using 1
  ext i
  rw [innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm]

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