lintegral_parallelComp_symm — Mathlib

English

For symmetric iterated integration, the lintegral over (κ ∥ η) ac equals the iterated lintegral with order swapped.

Русский

Для симметричного порядка интегрирования линегральный интеграл по (κ ∥ η)ac равен интегралу с поменянным порядком.

LaTeX

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

Lean4

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

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