rpow_sum_le_const_mul_sum_rpow_of_nonneg

English

If p ≥ 1 and f_i ≥ 0, then (∑_{i∈s} f_i)^p ≤ |s|^{p-1} ∑_{i∈s} f_i^p for a finite index set s.

Русский

Пусть p ≥ 1 и f_i ≥ 0. Тогда (∑_{i∈s} f_i)^p ≤ |s|^{p-1} ∑_{i∈s} f_i^p для конечного множества индексов s.

LaTeX

$$$(\sum_{i \in s} f_i)^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 nonnegative `ℝ`-valued
functions. -/
theorem rpow_sum_le_const_mul_sum_rpow_of_nonneg (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) :
    (∑ i ∈ s, f i) ^ p ≤ (#s : ℝ) ^ (p - 1) * ∑ i ∈ s, f i ^ p := by
  convert rpow_sum_le_const_mul_sum_rpow s f hp using 2 <;> apply sum_congr rfl <;> intro i hi <;>
    simp only [abs_of_nonneg, hf i hi]

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