norm_le_of_forall_le — Mathlib

English

If every partial sum ∑ i∈s ‖f i‖^p.toReal ≤ C^p.toReal for all Finsets s, then ‖f‖ ≤ C.

Русский

Если каждая частичная сумма ∑ i∈s ‖f_i‖^p ≤ C^p для всех Finset s, то ‖f‖ ≤ C.

LaTeX

$$$$ \forall s, \sum_{i\in s} \|f_i\|^{p^{\mathrm{toReal}}} \le C^{p^{\mathrm{toReal}}} \Rightarrow \|f\| \le C. $$$$

Lean4

theorem norm_le_of_forall_le {f : lp E ∞} {C : ℝ} (hC : 0 ≤ C) (hCf : ∀ i, ‖f i‖ ≤ C) : ‖f‖ ≤ C :=
  by
  cases isEmpty_or_nonempty α
  · simpa [eq_zero' f] using hC
  · exact norm_le_of_forall_le' C hCf

Похожие утверждения