English
If 0 ≤ x and 0 ≤ y and n ≠ 0, then x^n + y^n ≤ (x + y)^n.
Русский
Если 0 ≤ x, 0 ≤ y и n ≠ 0, то x^n + y^n ≤ (x + y)^n.
LaTeX
$$$\forall x,y\in \mathbb{R},\ 0\le x,\ 0\le y,\ n\in \mathbb{N},\ n \neq 0 \Rightarrow x^n + y^n \le (x+y)^n.$$$
Lean4
theorem pow_add_pow_le (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n :=
by
rcases Nat.exists_eq_add_one_of_ne_zero hn with ⟨k, rfl⟩
induction k with
| zero => simp only [zero_add, pow_one, le_refl]
| succ k ih =>
let n := k.succ
have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
have h2 := add_nonneg hx hy
calc
x ^ (n + 1) + y ^ (n + 1) ≤ x * x ^ n + y * y ^ n + (x * y ^ n + y * x ^ n) :=
by
rw [pow_succ' _ n, pow_succ' _ n]
exact le_add_of_nonneg_right h1
_ = (x + y) * (x ^ n + y ^ n) := by
rw [add_mul, mul_add, mul_add, add_comm (y * x ^ n), ← add_assoc, ← add_assoc,
add_assoc (x * x ^ n) (x * y ^ n), add_comm (x * y ^ n) (y * y ^ n), ← add_assoc]
_ ≤ (x + y) ^ (n + 1) := by
rw [pow_succ' _ n]
exact mul_le_mul_of_nonneg_left (ih (Nat.succ_ne_zero k)) h2
