English
A special form of Hölder-type inequality for ENNReal that bounds a product of Lp-powers with derivatives of the integrals.
Русский
Особая форма неравенства Хольдера для ENNReal, ограничивающая произведение степеней и производных интегралов.
LaTeX
$$$\\text{For real } p,q: p.HolderConjugate q \\Rightarrow ∫ f g ≤ ∫ f^p ∫ g^q$$$
Lean4
/-- Hölder's inequality for functions `α → ℝ≥0`. The integral of the product of two functions
is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
exponents. -/
theorem lintegral_mul_le_Lp_mul_Lq {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ≥0} (hf : AEMeasurable f μ)
(hg : AEMeasurable g μ) :
(∫⁻ a, (f * g) a ∂μ) ≤ (∫⁻ a, (f a : ℝ≥0∞) ^ p ∂μ) ^ (1 / p) * (∫⁻ a, (g a : ℝ≥0∞) ^ q ∂μ) ^ (1 / q) :=
by
simp_rw [Pi.mul_apply, ENNReal.coe_mul]
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.coe_nnreal_ennreal hg.coe_nnreal_ennreal
