Theorems · Theorem · measure theory

ENNReal.lintegral_mul_le_Lp_mul_Lq

∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → ENNReal},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

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.

Defined in

Mathlib.MeasureTheory.Integral.MeanInequalities

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasurableSpace