T_univ — Mathlib

English

In the finite universe case, T μ p f univ x equals the iterated integral formula with all coordinates included.

Русский

В случае конечного множества координат, T μ p f на всем множестве координат равен явному выражению через двойной интеграл по всем координатам.

LaTeX

$$$T μ p f \\, univ \\, x = \\int^{-}_{x} f(x)^{1 - (|ι| - 1) p} \\prod_{i} (\\int^{-} t\, f(update x i t) ∂μ_i)^p ∂(.pi μ)$$$

Lean4

@[simp]
theorem T_univ [Fintype ι] [∀ i, SigmaFinite (μ i)] (f : (∀ i, A i) → ℝ≥0∞) (x : ∀ i, A i) :
    T μ p f univ x =
      ∫⁻ (x : ∀ i, A i), (f x ^ (1 - (#ι - 1 : ℝ) * p) * ∏ i : ι, (∫⁻ t : A i, f (update x i t) ∂(μ i)) ^ p) ∂(.pi μ) :=
  by simp [T, lmarginal_singleton]

Похожие утверждения