young_inequality — Mathlib

English

General Young's inequality for arbitrary real a,b with Holder conjugate p,q: a b ≤ |a|^p/p + |b|^q/q.

Русский

Общая версия Young: a b ≤ |a|^p/p + |b|^q/q.

LaTeX

$$$a b \\le |a|^p/p + |b|^q/q$$$

Lean4

/-- **Young's inequality**, a version for arbitrary real numbers. -/
theorem young_inequality (a b : ℝ) {p q : ℝ} (hpq : p.HolderConjugate q) : a * b ≤ |a| ^ p / p + |b| ^ q / q :=
  calc
    a * b ≤ |a * b| := le_abs_self (a * b)
    _ = |a| * |b| := (abs_mul a b)
    _ ≤ |a| ^ p / p + |b| ^ q / q := Real.young_inequality_of_nonneg (abs_nonneg a) (abs_nonneg b) hpq

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