English
The grid-lines operator T acts on nonnegative functions on a finite product of measure spaces; it partially integrates over coordinates in a subset and then applies a product of powers to the remaining integrals. This is a central construction in iterative Sobolev-type inequalities.
Русский
Опертор «сеточные линии» T действует на неотрицательные функции на конечном произведении мерных пространств; частично интегрирует по некоторым координатам и затем применяет произведение степеней к оставшимся интегралам. Это ключевое построение в итеративных неравенствах типа Соболева.
LaTeX
$$$T(p,f,s) := \\int_{s}^{-} f^{1 - (|s|) p} \\prod_{i \in s} \\left( \\int_{i}^{-} f \\right)^{p} d\\mu$$$
Lean4
/-- 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`. -/
def T (p : ℝ) (f : (∀ i, A i) → ℝ≥0∞) (s : Finset ι) : (∀ i, A i) → ℝ≥0∞ :=
∫⋯∫⁻_s, f ^ (1 - (s.card - 1 : ℝ) * p) * ∏ i ∈ s, (∫⋯∫⁻_{ i }, f ∂μ) ^ p ∂μ
