rpow_add_rpow_le_add — Mathlib

English

Let a, b be nonnegative real numbers and p ≥ 1. Then (a^p + b^p)^(1/p) ≤ a + b.

Русский

Пусть a, b ≥ 0 и p ≥ 1. Тогда (a^p + b^p)^(1/p) ≤ a + b.

LaTeX

$$$\forall a,b \ge 0,\ \forall p \ge 1:\ (a^p + b^p)^{\frac{1}{p}} \le a + b$$$

Lean4

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

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