norm_le_of_forall_sum_le — Mathlib

English

Generalization with ENNReal p: if ∀ s, ∑ i∈s ‖f i‖^{p.toReal} ≤ (C)^{p.toReal}, then ‖f‖ ≤ C.

Русский

Обобщение для ENNReal: если для всех Finset s верно ∑ i∈s ‖f_i‖^{p.toReal} ≤ C^{p.toReal}, тогда ‖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_sum_le (hp : 0 < p.toReal) {C : ℝ} (hC : 0 ≤ C) {f : lp E p}
    (hf : ∀ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal) : ‖f‖ ≤ C :=
  norm_le_of_tsum_le hp hC (((lp.memℓp f).summable hp).tsum_le_of_sum_le hf)

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