rpow_add_le_add_rpow — Mathlib

English

If a, b ≥ 0 and 0 ≤ 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 \le p \le 1:\ (a + b)^p \le a^p + b^p$$$

Lean4

theorem rpow_add_le_add_rpow {p : ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hp : 0 ≤ p) (hp1 : p ≤ 1) :
    (a + b) ^ p ≤ a ^ p + b ^ p := by
  lift a to NNReal using ha
  lift b to NNReal using hb
  exact_mod_cast NNReal.rpow_add_le_add_rpow a b hp hp1

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