Theorems · Theorem · measure theory

ENNReal.lintegral_prod_norm_pow_le

∀ {α : Type u_2} {ι : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι)
  {f : ι → α → ENNReal},
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

A version of Hölder with multiple arguments

Defined in

Mathlib.MeasureTheory.Integral.MeanInequalities

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace