English
For a finite s, f ∈ ℝ≥0∞, and p>1 with Hölder conjugate q, ∑ f_i^p and ∑ g_i^q bound ∑ f_i g_i by Hölder inequality.
Русский
Для конечного s, f_i≥0, p>1, q сопряжённый к p: ∑ f_i g_i ≤ (∑ f_i^p)^{1/p} (∑ g_i^q)^{1/q}.
LaTeX
$$$\sum_{i\in s} f_i \cdot g_i \le \left(\sum_{i\in s} f_i^p\right)^{1/p} \left(\sum_{i\in s} g_i^q\right)^{1/q}$$$
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 (hp : 1 ≤ p) :
(∑ i ∈ s, f i) ^ p ≤ (card 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 [ENNReal.mul_rpow_of_nonneg _ _ hpq.nonneg, ← ENNReal.rpow_mul, hp₁, hq, coe_one, one_mul, one_rpow,
rpow_one, Pi.one_apply, sum_const, Nat.smul_one_eq_cast] using
ENNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg
