English
For NNReal a,b and p≥0, (a^p + b^p)^{1/p} ≤ a+b.
Русский
Для a,b≥0 и p≥0: (a^p+b^p)^{1/p} ≤ a+b.
LaTeX
$$$(a^p + b^p)^{1/p} \le a + b$$$
Lean4
theorem add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0) (hp1 : 1 ≤ p) : a ^ p + b ^ p ≤ (a + b) ^ p :=
by
have hp_pos : 0 < p := by positivity
by_cases h_zero : a + b = 0
· simp [add_eq_zero.mp h_zero, hp_pos.ne']
have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero] at h_zero
have h_add : a / (a + b) + b / (a + b) = 1 := by rw [← add_div, div_self h_zero]
have h := add_rpow_le_one_of_add_le_one (a / (a + b)) (b / (a + b)) h_add.le hp1
rw [div_rpow a (a + b), div_rpow b (a + b)] at h
have hab_0 : (a + b) ^ p ≠ 0 := by simp [h_nonzero]
have hab_0' : 0 < (a + b) ^ p := zero_lt_iff.mpr hab_0
have h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p := by
nth_rw 4 [← mul_one ((a + b) ^ p)]; gcongr
rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a ^ p), mul_comm (b ^ p), ← mul_assoc, ← mul_assoc,
mul_inv_cancel₀ hab_0, one_mul, one_mul] at h_mul
