English
For finite index set s, nonnegative function f on s, and p≥1, (sum f)^p ≤ |s|^{p-1} sum f^p.
Русский
Для конечного множества s, неотрицательной функции f на s и p≥1 верно (∑ 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 \quad (p\ge 1)$$$
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 `ℝ≥0`-valued functions.
-/
theorem rpow_sum_le_const_mul_sum_rpow (f : ι → ℝ≥0) {p : ℝ} (hp : 1 ≤ p) :
(∑ i ∈ s, f i) ^ p ≤ (#s : ℝ≥0) ^ (p - 1) * ∑ i ∈ s, f i ^ p :=
by
rcases eq_or_lt_of_le hp with hp | hp
· simp [← hp]
let q : ℝ := p / (p - 1)
have hpq : p.HolderConjugate q := .conjExponent hp
have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
have hq : 1 / q * p = p - 1 := by
rw [← hpq.div_conj_eq_sub_one]
ring
simpa only [NNReal.mul_rpow, ← NNReal.rpow_mul, hp₁, hq, one_mul, one_rpow, rpow_one, Pi.one_apply, sum_const,
Nat.smul_one_eq_cast] using NNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg
