Theorems · Theorem · functional analysis

MeasureTheory.GridLines.T_univ

∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] {p : ℝ} [inst_2 : Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  (f : ((i : ι) → A i) → ENNReal) (x : (i : ι) → A i),
  MeasureTheory.GridLines.T μ p f Finset.univ x =
    ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑(Fintype.card ι) - 1) * p) *
        ∏ i, (∫⁻ (t : A i), f (Function.update x i t) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ

Defined in

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEqFintypeMeasureTheory.SigmaFinite