English
A form of Hölder for products: the integral of a product is bounded by the product of the p-norms and q-norms of the factors.
Русский
Неравенство Хольдера для произведения: интеграл произведения ограничен произведением норм p и q факторов.
LaTeX
$$$\\forall p,q\\; (hpq: p.HolderConjugate q), \\; f,g:X→ℝ_{≥0}^{∞}, AEMeasurable f μ, AEMeasurable g μ \\Rightarrow ∫ f g ≤ (∫ f^{p})^{1/p} (∫ g^{q})^{1/q}$$$
Lean4
theorem lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ≥0∞}
(hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) :
(∫⁻ a, f a * g a ^ (p - 1) ∂μ) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ p ∂μ) ^ (1 / q) :=
by
refine le_trans (ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf (hg.pow_const _)) ?_
by_cases hf_zero_rpow : (∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) = 0
· rw [hf_zero_rpow, zero_mul]
exact zero_le _
have hf_top_rpow : (∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) ≠ ⊤ :=
by
by_contra h
refine hf_top ?_
have hp_not_neg : ¬p < 0 := by simp [hpq.nonneg]
simpa [hpq.pos, hp_not_neg] using h
refine (ENNReal.mul_le_mul_left hf_zero_rpow hf_top_rpow).mpr (le_of_eq ?_)
congr
ext1 a
rw [← ENNReal.rpow_mul, hpq.sub_one_mul_conj]
