Theorems · Theorem · measure theory

NNReal.lintegral_mul_le_Lp_mul_Lq

∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  p.HolderConjugate q →
    ∀ {f g : α → NNReal},
      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

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpace