English
For NNReal z1,z2 and p≥0 with a+b=2, a^p+b^p ≤ (a+b)^p; a standard two-term bound.
Русский
Два элемента: a^p+b^p ≤ (a+b)^p для p≥0.
LaTeX
$$$a^p + b^p \le (a+b)^p$$$
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
rcases eq_or_lt_of_le hp with (rfl | h'p)
· simp only [rpow_one, sub_self, rpow_zero, one_mul]; rfl
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (add_halves 1) hp using 1
· simp only [one_div, inv_mul_cancel_left₀, Ne, two_ne_zero, not_false_iff]
· have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
simp only [mul_rpow, rpow_sub' A, div_eq_inv_mul, rpow_one, mul_one]
ring
