English
If a net of lp(E,p)-valued elements F_i is eventually bounded by C in norm and converges pointwise to f, then the partial sums over a finite set s satisfy a bound ∑_{i∈s} ‖f_i‖^p ≤ C^p.
Русский
Если сеть значений lp(E,p) ограничена по норме ≤ C и сходится по точкам к f, то частичные суммы по конечному множеству s удовлетворяют неравенству ∑ ‖f_i‖^p ≤ C^p.
LaTeX
$$$\\exists (hp: p ≠ ∞)\\; (hCF: \\forall^∗ k, \\|F_k\\| ≤ C) \\Rightarrow \\forall f,\\; \\forall s,\\; \\sum_{i∈s} \\|f_i\\|^p ≤ C^p.$$$
Lean4
theorem sum_rpow_le_of_tendsto (hp : p ≠ ∞) {C : ℝ} {F : ι → lp E p} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C) {f : ∀ a, E a}
(hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) (s : Finset α) : ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal :=
by
have hp' : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp' hp
let G : (∀ a, E a) → ℝ := fun f => ∑ a ∈ s, ‖f a‖ ^ p.toReal
have hG : Continuous G := by
refine continuous_finset_sum s ?_
intro a _
have : Continuous fun f : ∀ a, E a => f a := continuous_apply a
exact this.norm.rpow_const fun _ => Or.inr hp''.le
refine le_of_tendsto (hG.continuousAt.tendsto.comp hf) ?_
refine hCF.mono ?_
intro k hCFk
refine (lp.sum_rpow_le_norm_rpow hp'' (F k) s).trans ?_
gcongr
