Theorems · Theorem · functional analysis

MeasureTheory.lintegral_prod_lintegral_pow_le

∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {p : ℝ},
  (↑(Fintype.card ι)).HolderConjugate p →
    ∀ {f : ((a : ι) → A a) → ENNReal},
      Measurable f →
        ∫⁻ (x : (i : ι) → A i),
            ∏ i,
              (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^
                (1 / (↑(Fintype.card ι) - 1)) ∂MeasureTheory.Measure.pi μ ≤
          (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ p

Special case of the grid-lines lemma lintegral_mul_prod_lintegral_pow_le, taking the extremal exponent p = (#ι - 1)⁻¹.

Defined in

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEqFintypeMeasureTheory.SigmaFinite