English
If F_i are lp(E,p) elements that converge to f in the lp topology, finite-sum bounds hold in the limit: the sum of p-th powers of coordinates is bounded by the limit bound C^p.
Русский
Если F_i сходятся к f в lp топологии, предел суммы по координатам удовлетворяет ограничению: сумма по i ∈ s ‖f_i‖^p ≤ C^p.
LaTeX
$$$\\text{If } F_i \\to f \\text{ in lp topology, then } \\sum_{i∈s} \\|f_i\\|^p \\le C^p.$$$
Lean4
/-- "Semicontinuity of the `lp` norm": If all sufficiently large elements of a sequence in `lp E p`
have `lp` norm `≤ C`, then the pointwise limit, if it exists, also has `lp` norm `≤ C`. -/
theorem norm_le_of_tendsto {C : ℝ} {F : ι → lp E p} (hCF : ∀ᶠ k in l, ‖F k‖ ≤ C) {f : lp E p}
(hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) : ‖f‖ ≤ C :=
by
obtain ⟨i, hi⟩ := hCF.exists
have hC : 0 ≤ C := (norm_nonneg _).trans hi
rcases eq_top_or_lt_top p with (rfl | hp)
· apply norm_le_of_forall_le hC
exact norm_apply_le_of_tendsto hCF hf
· have : 0 < p := zero_lt_one.trans_le _i.elim
have hp' : 0 < p.toReal := ENNReal.toReal_pos this.ne' hp.ne
apply norm_le_of_forall_sum_le hp' hC
exact sum_rpow_le_of_tendsto hp.ne hCF hf
