sum_rpow_le_norm_rpow — Mathlib

English

For hp > 0, and a finite Finset s, the p-th power sum over s is bounded by the p-th power of the norm: ∑ i∈s ‖f i‖^{p.toReal} ≤ ‖f‖^{p.toReal}.

Русский

При hp > 0 и конечном Finset s сумма по i∈s ‖f_i‖^{p.toReal} ≤ ‖f‖^{p.toReal}.

LaTeX

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

Lean4

theorem sum_rpow_le_norm_rpow (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :
    ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal :=
  by
  rw [lp.norm_rpow_eq_tsum hp f]
  have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _
  refine Summable.sum_le_tsum _ (fun i _ => this i) ?_
  exact (lp.memℓp f).summable hp

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