English
Let a, b be nonnegative. If p, q are Hölder conjugates with p > 1 (equivalently 1/p + 1/q = 1), then a b ≤ a^p/p + b^q/q.
Русский
Пусть a, b ≥ 0. Если p и q являются сопряжёнными по Холдера и p > 1 (то есть 1/p + 1/q = 1), то a b ≤ a^p/p + b^q/q.
LaTeX
$$$a b \le \dfrac{a^{p}}{p} + \dfrac{b^{q}}{q}$, где $a,b \ge 0$ и $p,q>1$ с $\tfrac{1}{p}+\tfrac{1}{q}=1$.$$
Lean4
/-- **Young's inequality**, `ℝ≥0` version. We use `{p q : ℝ≥0}` in order to avoid constructing
witnesses of `0 ≤ p` and `0 ≤ q` for the denominators. -/
theorem young_inequality (a b : ℝ≥0) {p q : ℝ≥0} (hpq : p.HolderConjugate q) :
a * b ≤ a ^ (p : ℝ) / p + b ^ (q : ℝ) / q :=
Real.young_inequality_of_nonneg a.coe_nonneg b.coe_nonneg hpq.coe
