Theorems · Definition · functional analysis

MeasureTheory.GridLines.T

{ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : (i : ι) → MeasurableSpace (A i)] →
      ((i : ι) → MeasureTheory.Measure (A i)) →
        [DecidableEq ι] → ℝ → (((i : ι) → A i) → ENNReal) → Finset ι → ((i : ι) → A i) → ENNReal

The "grid-lines operation" (not a standard name) which is central in the inductive proof of the Sobolev inequality. For a finite dependent product Π i : ι, A i of sigma-finite measure spaces, a finite set s of indices from ι, and a (later assumed nonnegative) real number p, this operation acts on a function f from Π i, A i into the extended nonnegative reals. The operation is to partially integrate, in the s co-ordinates, the function whose value at x : Π i, A i is obtained by multiplying a certain power of f with the product, for each co-ordinate i in s, of a certain power of the integral of f along the "grid line" in the i direction through x. We are most interested in this operation when the set s is the universe in ι, but as a proxy for "induction on dimension" we define it for a general set s of co-ordinates: the s-grid-lines operation on a function f which is constant along the co-ordinates in sᶜ is morally (that is, up to type-theoretic nonsense) the same thing as the universe-grid-lines operation on the associated function on the "lower-dimensional" space Π i : s, A i.

Defined in

Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceDecidableEq