summable — Mathlib

English

If hp > 0, then Memℓp f p implies the series ∑ ‖f(i)‖^p.toReal is summable.

Русский

Пусть hp>0; тогда Memℓp f p влечёт суммируемость ряда ∑ ‖f(i)‖^p.toReal.

LaTeX

$$$$ \text{hp} > 0 \Rightarrow \mathrm{Mem}_{\ell^p}(f,p) \Rightarrow \mathrm{Summable}\;\|f(i)\|^{p^{toReal}}. $$$$

Lean4

theorem summable (hp : 0 < p.toReal) {f : ∀ i, E i} (hf : Memℓp f p) : Summable fun i => ‖f i‖ ^ p.toReal :=
  (memℓp_gen_iff hp).1 hf

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