English
In the same setting, the inequality (a + b)^n ≤ 2^(n-1) (a^n + b^n) holds whenever n is even and a, b ≥ 0.
Русский
В той же постановке неравенство (a + b)^n ≤ 2^(n-1) (a^n + b^n) выполняется, когда n чётно и a, b ≥ 0.
LaTeX
$$$(a+b)^n \le 2^{n-1} \bigl(a^n + b^n\bigr) \quad \text{если } n \text{ чётно } a,b \ge 0$$$
Lean4
protected theorem add_pow_le (hn : Even n) : (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n) :=
by
obtain ⟨n, rfl⟩ := hn
rw [← two_mul, pow_mul]
calc
_ ≤ (2 * (a ^ 2 + b ^ 2)) ^ n := pow_le_pow_left₀ (sq_nonneg _) add_sq_le _
_ = 2 ^ n * (a ^ 2 + b ^ 2) ^ n := by -- TODO: Should be `Nat.cast_commute`
rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
_ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) :=
(mul_le_mul_of_nonneg_left (add_pow_le (sq_nonneg _) (sq_nonneg _) _) <| pow_nonneg (zero_le_two (α := R)) _)
_ = _ := by
simp only [← mul_assoc, ← pow_add, ← pow_mul]
cases n
· rfl
· simp [Nat.two_mul]
