Theorems · Theorem · real analysis

ENNReal.young_inequality_eq_iff

∀ (a b : ENNReal) {p q : ℝ},
  p.HolderConjugate q →
    (a * b = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q ↔ a = ⊤ ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = ⊤ ∨ a ^ p = b ^ q)

Young's inequality equality condition, ℝ≥0∞ version with real conjugate exponents.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

0 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound