English
For ENNReal with two elements z1,z2 and p ≥ 1, (z1^p + z2^p) ≤ (z1 + z2)^p under appropriate normalization.
Русский
Для двух элементов z1,z2 ∈ ℝ≥0∞ и p ≥ 1 выполняется (z1^p + z2^p) ≤ (z1 + z2)^p при надлежащей нормализации.
LaTeX
$$$\forall z_1,z_2:\, (z_1^p + z_2^p) ≤ (z_1+z_2)^p \text{ для } p ≥ 1$$$
Lean4
/-- Unweighted mean inequality, version for two elements of `ℝ≥0∞` and real exponents. -/
theorem rpow_add_le_mul_rpow_add_rpow (z₁ z₂ : ℝ≥0∞) {p : ℝ} (hp : 1 ≤ p) :
(z₁ + z₂) ^ p ≤ (2 : ℝ≥0∞) ^ (p - 1) * (z₁ ^ p + z₂ ^ p) :=
by
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (ENNReal.add_halves 1) hp using 1
· simp [← mul_assoc, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]
· simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero ofNat_ne_top,
ENNReal.div_eq_inv_mul, rpow_one, mul_one]
ring
