young_inequality — Mathlib

English

Let a, b be nonnegative extended nonnegative reals. If p,q are Hölder conjugates, then a b ≤ a^p / ENNReal.ofReal(p) + b^q / ENNReal.ofReal(q).

Русский

Пусть a, w ≥ 0 бесконечно-выпуклые числа; если p,q сопряжённые по Холдера, то a b ≤ a^p / ENNReal.ofReal(p) + b^q / ENNReal.ofReal(q).

LaTeX

$$$a b \le \dfrac{a^{p}}{\mathrm{ENNReal}.ofReal(p)} + \dfrac{b^{q}}{\mathrm{ENNReal}.ofReal(q)}$$$

Lean4

/-- **Young's inequality**, `ℝ≥0∞` version with real conjugate exponents. -/
theorem young_inequality (a b : ℝ≥0∞) {p q : ℝ} (hpq : p.HolderConjugate q) :
    a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q :=
  by
  by_cases h : a = ⊤ ∨ b = ⊤
  · refine le_trans le_top (le_of_eq ?_)
    repeat rw [div_eq_mul_inv]
    rcases h with h | h <;> rw [h] <;> simp [hpq.pos, hpq.symm.pos]
  push_neg at h
  rw [← coe_toNNReal h.left, ← coe_toNNReal h.right, ← coe_mul, ← coe_rpow_of_nonneg _ hpq.nonneg, ←
    coe_rpow_of_nonneg _ hpq.symm.nonneg, ENNReal.ofReal, ENNReal.ofReal, ←
    @coe_div (Real.toNNReal p) _ (by simp [hpq.pos]), ← @coe_div (Real.toNNReal q) _ (by simp [hpq.symm.pos]), ←
    coe_add, coe_le_coe]
  exact NNReal.young_inequality_real a.toNNReal b.toNNReal hpq

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