hasSum_orthogonalProjection — Mathlib

English

The representation map provides that x is the sum of b.repr x i times b_i.

Русский

Преобразование представления даёт, что x есть сумма (repr x)_i · b_i.

LaTeX

$$$ HasSum (\\lambda i, (b.repr x)_i · b_i) x $$$

Lean4

protected theorem hasSum_orthogonalProjection {U : Submodule 𝕜 E} [CompleteSpace U] (b : HilbertBasis ι 𝕜 U) (x : E) :
    HasSum (fun i => ⟪(b i : E), x⟫ • b i) (U.orthogonalProjection x) := by
  simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
    b.hasSum_repr (U.orthogonalProjection x)

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