young_inequality_of_nonneg — Mathlib

English

Young's inequality for nonnegative a,b with Holder conjugate p,q: ab ≤ a^p/p + b^q/q.

Русский

Неотрицательные a,b и сопряженные p,q: ab ≤ a^p/p + b^q/q.

LaTeX

$$$a b \\le \\frac{a^p}{p} + \\frac{b^q}{q}$$$

Lean4

/-- **Young's inequality**, a version for nonnegative real numbers. -/
theorem young_inequality_of_nonneg {a b p q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hpq : p.HolderConjugate q) :
    a * b ≤ a ^ p / p + b ^ q / q := by
  simpa [← rpow_mul, ha, hb, hpq.ne_zero, hpq.symm.ne_zero, _root_.div_eq_inv_mul] using
    geom_mean_le_arith_mean2_weighted hpq.inv_nonneg hpq.symm.inv_nonneg (rpow_nonneg ha p) (rpow_nonneg hb q)
      hpq.inv_add_inv_eq_one

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