lintegral_prod — Mathlib

English

If κ and η are s-finite, then the lintegral over their product kernel equals the iterated lintegral: ∫ g d(κ ×ₖ η) a = ∫ b ∫ c g(b,c) dη a ∂κ a.

Русский

Если κ и η s-конечны, то линтегральная формула для их произведения равна итеративному линтигранту.

LaTeX

$$$$\\int^{-} c \\; g c \\; \\partial(κ ×ₖ η) a = \\int^{-} b \\int^{-} c \\; g(b,c) \\; \\partial η a \\; \\partial κ a.$$$$

Lean4

theorem lintegral_prod (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (a : α)
    {g : β × γ → ℝ≥0∞} (hg : Measurable g) : ∫⁻ c, g c ∂(κ ×ₖ η) a = ∫⁻ b, ∫⁻ c, g (b, c) ∂η a ∂κ a :=
  by
  simp_rw [prod, lintegral_comp _ _ _ hg, copy_apply]
  rw [lintegral_dirac' _ (by fun_prop)]
  simp_rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]

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