English
If a bounded sequence in lp(E,p) converges pointwise, its limit f lies in lp(E,p).
Русский
Если ограниченная последовательность в lp(E,p) сходится по точкам к f, то предел f ∈ lp(E,p).
LaTeX
$$$\\text{If } hF: \\text{Bornology.IsBounded}(\\mathrm{Range}(F)) \\text{ and } F_i \\to f\\text{ pointwise, then } f ∈ \\ell^p(E).$$$
Lean4
/-- If `f` is the pointwise limit of a bounded sequence in `lp E p`, then `f` is in `lp E p`. -/
theorem memℓp_of_tendsto {F : ι → lp E p} (hF : Bornology.IsBounded (Set.range F)) {f : ∀ a, E a}
(hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) : Memℓp f p :=
by
obtain ⟨C, hCF⟩ : ∃ C, ∀ k, ‖F k‖ ≤ C := hF.exists_norm_le.imp fun _ ↦ Set.forall_mem_range.1
rcases eq_top_or_lt_top p with (rfl | hp)
· apply memℓp_infty
use C
rintro _ ⟨a, rfl⟩
exact norm_apply_le_of_tendsto (Eventually.of_forall hCF) hf a
· apply memℓp_gen'
exact sum_rpow_le_of_tendsto hp.ne (Eventually.of_forall hCF) hf
