Source indexedtheorem · leanprover/lean4:v4.32.0

ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm

Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:79 to 91

Source documentation

Hölder's inequality for functions α → ℝ≥0∞, using exponents in ℝ≥0∞

Exact Lean statement

theorem lintegral_mul_le_eLpNorm_mul_eLqNorm {p q : ℝ≥0∞} (hpq : p.HolderConjugate q)
    {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    ∫⁻ (a : α), (f * g) a ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem lintegral_mul_le_eLpNorm_mul_eLqNorm {p q : ℝ≥0∞} (hpq : p.HolderConjugate q)    {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :    ∫⁻ (a : α), (f * g) a ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by  by_cases! pq_top : p = ∞ ∨ q = ∞  · wlog hp : p = ∞    · have hq := pq_top.resolve_left hp      simpa only [mul_comm] using this hpq.symm hg hf (Or.inl hq) hq    apply le_of_le_of_eq <| lintegral_mono_ae ((ae_le_essSup f).mono (fun a ha ↦ mul_left_mono ha))    simp [eLpNorm, eLpNorm', eLpNormEssSup, hp, hpq.conj_eq, lintegral_const_mul'' _ hg]  have hp : p ≠ 0 := HolderConjugate.ne_zero p q  have hq : q ≠ 0 := HolderConjugate.ne_zero q p  convert ENNReal.lintegral_mul_le_Lp_mul_Lq μ (hpq.toReal_of_ne_top pq_top.1 pq_top.2) hf hg  all_goals simp [eLpNorm, eLpNorm', pq_top, hp, hq]