Theorems · Theorem · measure theory

ENNReal.lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow

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

Defined in

Mathlib.MeasureTheory.Integral.MeanInequalities

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace