add_rpow_le_rpow_add — Mathlib

English

For nonnegative real numbers a,b and p≥1, the same convexity inequality holds in Real as in NNReal; lifting preserves inequality.

Русский

Для неотрицательных действительных a,b и p≥1 верно то же неравенство, что и в NNReal; переход между ними сохраняет неравенство.

LaTeX

$$Для вещественных a,b≥0, p≥1: a^p + b^p ≤ (a+b)^p$$

Lean4

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

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