rpow_add_le_add_rpow — Mathlib

English

For p ≥ 0 and p ≤ 1, (a + b)^p ≤ a^p + b^p for ENNReal a,b.

Русский

Для p в [0,1] и ENNReal a,b выполняется (a + b)^p ≤ a^p + b^p.

LaTeX

$$$\forall a,b\in ENNReal,\ 0 \le p \le 1:\ (a + b)^p ≤ a^p + b^p$$$

Lean4

theorem rpow_add_le_add_rpow {p : ℝ} (a b : ℝ≥0∞) (hp : 0 ≤ p) (hp1 : p ≤ 1) : (a + b) ^ p ≤ a ^ p + b ^ p :=
  by
  rcases hp.eq_or_lt with (rfl | hp_pos)
  · simp
  have h := rpow_add_rpow_le a b hp_pos hp1
  rw [one_div_one, one_div] at h
  repeat' rw [ENNReal.rpow_one] at h
  exact (ENNReal.le_rpow_inv_iff hp_pos).mp h

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