summable_of_lp — Mathlib

English

If V is an orthogonal family of subspaces, then for any f ∈ lp G 2 the sum ∑ i V_i(f(i)) converges in E.

Русский

Если V образует ортогональную семью подпредприятий, то для любого f ∈ lp G 2 сумма ∑ i V_i(f(i)) сходится в E.

LaTeX

$$$ \\text{Summable}\\big(i \\to V_i(f(i))\\big)$$$

Lean4

protected theorem summable_of_lp (f : lp G 2) : Summable fun i => V i (f i) :=
  by
  rw [hV.summable_iff_norm_sq_summable]
  convert (lp.memℓp f).summable _
  · norm_cast
  · norm_num

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