rpow_add_rpow_le — Mathlib

English

Let a, b ≥ 0 and 0 < p ≤ q. Then (a^q + b^q)^(1/q) ≤ (a^p + b^p)^(1/p).

Русский

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

LaTeX

$$$\forall a,b \ge 0,\ \forall p,q>0:\ p\le q \Rightarrow (a^q + b^q)^{1/q} \le (a^p + b^p)^{1/p}$$$

Lean4

theorem rpow_add_rpow_le {p q : ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hp_pos : 0 < p) (hpq : p ≤ q) :
    (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p) :=
  by
  lift a to NNReal using ha
  lift b to NNReal using hb
  exact_mod_cast NNReal.rpow_add_rpow_le a b hp_pos hpq

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