Theorems · Theorem · real analysis

ENNReal.rpow_sum_le_const_mul_sum_rpow

∀ {ι : Type u} (s : Finset ι) (f : ι → ENNReal) {p : ℝ},
  1 ≤ p → (∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p

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 ℝ≥0∞-valued functions.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

0 results in Mathlib

Foundations

Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound