English
Let a, b ≥ 0 and p, q ∈ R be Hölder conjugates. Then a b ≤ a^p / Real.toNNReal(p) + b^q / Real.toNNReal(q).
Русский
Пусть a, b ≥ 0 и p, q ∈ R являются сопряжёнными по Холдера. Тогда a b ≤ a^p / Real.toNNReal(p) + b^q / Real.toNNReal(q).
LaTeX
$$$a b \le \dfrac{a^{p}}{\operatorname{Real.toNNReal}(p)} + \dfrac{b^{q}}{\operatorname{Real.toNNReal}(q)}$, при $a,b \ge 0$ и $p,q$ — сопряжённые по Холдера.$$
Lean4
/-- **Young's inequality**, `ℝ≥0` version with real conjugate exponents. -/
theorem young_inequality_real (a b : ℝ≥0) {p q : ℝ} (hpq : p.HolderConjugate q) :
a * b ≤ a ^ p / Real.toNNReal p + b ^ q / Real.toNNReal q := by
simpa [Real.coe_toNNReal, hpq.nonneg, hpq.symm.nonneg] using young_inequality a b hpq.toNNReal
