Theorems · Theorem · functional analysis

MeasureTheory.lintegral_mul_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 : ℝ},
  0 ≤ p →
    (↑(Fintype.card ι) - 1) * p ≤ 1 →
      ∀ {f : ((i : ι) → A i) → ENNReal},
        Measurable f →
          ∫⁻ (x : (i : ι) → A i),
              f x ^ (1 - (↑(Fintype.card ι) - 1) * p) *
                ∏ i, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ ≤
            (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ (1 + p)

The "grid-lines lemma" (not a standard name), stated with a general parameter p as the exponent. Compare with lintegral_prod_lintegral_pow_le. For any finite dependent product Π i : ι, A i of sigma-finite measure spaces, for any nonnegative real number p such that (#ι - 1) * p ≤ 1, for any function f from Π i, A i into the extended nonnegative reals, we consider an associated "grid-lines quantity", the integral of an associated function from Π i, A i into the extended nonnegative reals. The value of this function at x : Π i, A i is obtained by multiplying a certain power of f with the product, for each co-ordinate i, of a certain power of the integral of f along the "grid line" in the i direction through x. This lemma bounds the Lebesgue integral of the grid-lines quantity by a power of the Lebesgue integral of f.

Defined in

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEqFintypeMeasureTheory.SigmaFinite