lintegral_parallelComp — Mathlib

English

If κ and η are s-finite, then for ac = (a,c) and a measurable g on β×δ, the lintegral with respect to (κ ∥ₖ η) ac equals the iterated lintegral over κ and η.

Русский

Если κ и η — s-ограниченные, то линегральный интеграл по (κ ∥ₖ η)ac равен вложенному по κ и η интегралу по β и δ.

LaTeX

$$$$\\int^{-} g \\; d(κ ∥ₖ η) ac = \\int^{-} b \\int^{-} d \\, g(b,d) \\; dη ac.2 \\; dκ ac.1.$$$$

Lean4

theorem lintegral_parallelComp [IsSFiniteKernel κ] [IsSFiniteKernel η] (ac : α × γ) {g : β × δ → ℝ≥0∞}
    (hg : Measurable g) : ∫⁻ bd, g bd ∂(κ ∥ₖ η) ac = ∫⁻ b, ∫⁻ d, g (b, d) ∂η ac.2 ∂κ ac.1 := by
  rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]

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