English
For NNReal a,b and p ≤ q with p>0, the rpow bound compares the q-mean and p-mean.
Русский
Для NNReal: сравнение q- и p-неравенств.
LaTeX
$$$(a^q + b^q)^{1/q} \le (a^p + b^p)^{1/p}$$$
Lean4
theorem rpow_add_rpow_le {p q : ℝ} (a b : ℝ≥0) (hp_pos : 0 < p) (hpq : p ≤ q) :
(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p) :=
by
have h_rpow : ∀ a : ℝ≥0, a ^ q = (a ^ p) ^ (q / p) := fun a => by
rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm, one_mul]
have h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p :=
by
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
rwa [one_le_div hp_pos]
rw [h_rpow a, h_rpow b, one_div p, NNReal.le_rpow_inv_iff hp_pos, ← NNReal.rpow_mul, mul_comm, mul_one_div]
rwa [one_div_div] at h_rpow_add_rpow_le_add
