rpow_sum_le_const_mul_sum_rpow — Mathlib

English

For p ≥ 1 and real-valued f on a finite set, (∑ |f|)^p ≤ (#s)^{p-1} ∑ |f|^p.

Русский

Для p ≥ 1 и функции f на конечном множестве, (Σ|f|)^p ≤ |s|^{p-1} Σ|f|^p.

LaTeX

$$$\left(\sum_{i\in s} |f_i|\right)^p \le |s|^{p-1} \sum_{i\in s} |f_i|^p$$$

Lean4

/-- For `1 ≤ p`, the `p`-th power of the sum of `f i` is bounded above by a constant times the
sum of the `p`-th powers of `f i`. Version for sums over finite sets, with `ℝ`-valued functions. -/
theorem rpow_sum_le_const_mul_sum_rpow (hp : 1 ≤ p) : (∑ i ∈ s, |f i|) ^ p ≤ (#s : ℝ) ^ (p - 1) * ∑ i ∈ s, |f i| ^ p :=
  by
  have := NNReal.coe_le_coe.2 (NNReal.rpow_sum_le_const_mul_sum_rpow s (fun i => ⟨_, abs_nonneg (f i)⟩) hp)
  push_cast at this
  exact this

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