English
If there exists a real C such that for every finite subset s of indices the partial sums ∑_{i∈s} ‖f(i)‖^p.toReal ≤ C, then Memℓp f p.
Русский
Если существует число C такое, что для каждого конечного подмножества s индексного множества частичные суммы ≤ C, то f ∈ ℓ^p.
LaTeX
$$$$ \forall s \in \mathrm{Finset}(\alpha), \sum_{i\in s} \|f(i)\|^{p^{toReal}} \le C \Rightarrow \mathrm{Mem}_{\ell^p}(f,p). $$$$
Lean4
theorem memℓp_gen' {C : ℝ} {f : ∀ i, E i} (hf : ∀ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C) : Memℓp f p :=
by
apply memℓp_gen
use ⨆ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal
apply hasSum_of_isLUB_of_nonneg
· intro b
exact Real.rpow_nonneg (norm_nonneg _) _
apply isLUB_ciSup
use C
rintro - ⟨s, rfl⟩
exact hf s
