Theorems · Theorem · measure theory

ENNReal.lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add

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

Defined in

Mathlib.MeasureTheory.Integral.MeanInequalities

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpace