English
Let R be a linearly ordered semiring with a strictly ordered ring structure. If a and b are nonnegative, then for every natural n we have (a + b)^n ≤ 2^(n-1) (a^n + b^n).
Русский
Пусть R — линейно упорядоченное полуг ring с строго упорядоченной структурой. Если a ≥ 0 и b ≥ 0, то для любого натурального n выполняется (a + b)^n ≤ 2^(n-1) (a^n + b^n).
LaTeX
$$$(a+b)^n \le 2^{n-1} \bigl(a^n + b^n\bigr)$$$
Lean4
theorem add_pow_le (ha : 0 ≤ a) (hb : 0 ≤ b) : ∀ n, (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)
| 0 => by simp
| 1 => by simp
| n + 2 => by
rw [pow_succ]
calc
_ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
_ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _), add_add_add_comm,
add_comm (_ * a)]
_ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) :=
(mul_le_mul_of_nonneg_left (add_le_add_left ?_ _) <| pow_nonneg (zero_le_two (α := R)) _)
_ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl
· obtain hab | hba := le_total a b
· exact mul_add_mul_le_mul_add_mul (pow_le_pow_left₀ ha hab _) hab
· exact mul_add_mul_le_mul_add_mul' (pow_le_pow_left₀ hb hba _) hba
