memℓp_gen_iff — Mathlib

English

For p with positive real part, membership in ℓ^p is equivalent to summability of the p-th power of norms: Memℓp f p ↔ Summable ∥f(i)∥^p.toReal.

Русский

Для p с положительной вещественной частью принадлежность к ℓ^p эквивалентна суммируемости по нормам в степени p: Memℓp f p ⇔ Summable ∥f(i)∥^p.toReal.

LaTeX

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

Lean4

theorem memℓp_gen_iff (hp : 0 < p.toReal) {f : ∀ i, E i} : Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal :=
  by
  rw [ENNReal.toReal_pos_iff] at hp
  dsimp [Memℓp]
  rw [if_neg hp.1.ne', if_neg hp.2.ne]

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