English
For a,b ≥ 0 and p > 0 with p ≤ 1, then (a + b)^p ≤ a^p + b^p.
Русский
Пусть a,b ≥ 0 и 0 < p ≤ 1. Тогда (a + b)^p ≤ a^p + b^p.
LaTeX
$$$\forall a,b \ge 0,\ 0 < p,\ p \le 1:\ (a + b)^p ≤ a^p + b^p$$$
Lean4
theorem rpow_add_rpow_le {p q : ℝ} (a b : ℝ≥0∞) (hp_pos : 0 < p) (hpq : p ≤ q) :
(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p) :=
by
have h_rpow : ∀ a : ℝ≥0∞, a ^ q = (a ^ p) ^ (q / p) := fun a => by
rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']
have h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p :=
by
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
rwa [one_le_div hp_pos]
rw [h_rpow a, h_rpow b, one_div p, ENNReal.le_rpow_inv_iff hp_pos, ← ENNReal.rpow_mul, mul_comm, mul_one_div]
rwa [one_div_div] at h_rpow_add_rpow_le_add
