English
If the series ∑ ‖f(i)‖^p.toReal is summable, then f ∈ ℓ^p.
Русский
Если сумма ∑_i ‖f(i)‖^p.toReal сходится, то f принадлежит ℓ^p.
LaTeX
$$$$ \mathrm{Summable}\;\|f(i)\|^{p^{toReal}} \Rightarrow \mathrm{Mem}_{\ell^p}(f,p). $$$$
Lean4
theorem memℓp_gen {f : ∀ i, E i} (hf : Summable fun i => ‖f i‖ ^ p.toReal) : Memℓp f p :=
by
rcases p.trichotomy with (rfl | rfl | hp)
· apply memℓp_zero
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
exact (Set.Finite.of_summable_const (by simp) H).subset (Set.subset_univ _)
· apply memℓp_infty
have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
simpa using ((Set.Finite.of_summable_const (by simp) H).image fun i => ‖f i‖).bddAbove
exact (memℓp_gen_iff hp).2 hf
