add_rpow_le_two_rpow_mul_rpow_add_rpow

English

For p ∈ ℝ with p ≥ 0 and a,b ∈ ENNReal, (a+b)^p ≤ 2^p (a^p + b^p).

Русский

Для p ∈ ℝ, p ≥ 0 и a,b ∈ ℝ≥0∞: (a+b)^p ≤ 2^p (a^p + b^p).

LaTeX

$$$$ (a + b)^p \le 2^p \\left(a^p + b^p \\right). $$$$

Lean4

theorem add_rpow_le_two_rpow_mul_rpow_add_rpow {p : ℝ} (a b : ℝ≥0∞) (hp : 0 ≤ p) :
    (a + b) ^ p ≤ 2 ^ p * (a ^ p + b ^ p) :=
  calc
    (a + b) ^ p ≤ (2 * max a b) ^ p := by rw [two_mul]; gcongr <;> simp
    _ = 2 ^ p * (max a b) ^ p := (mul_rpow_of_nonneg _ _ hp)
    _ = 2 ^ p * max (a ^ p) (b ^ p) := by rw [max_rpow hp]
    _ ≤ 2 ^ p * (a ^ p + b ^ p) := by gcongr; apply max_le_add_of_nonneg <;> simp

Похожие утверждения