Set-integral disintegration for a measure followed by a kernel

Proved

MarkovChainCLT.setIntegral_measure_comp_kernel

by Zehao Jin · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

disintegrationintegrationkernelmeasure-theory

Let $\mu$ be a $\sigma$ -finite measure and let $\eta$ be an $s$ -finite transition kernel. If $f$ is integrable on a measurable set $s$ under the composed measure $\mu\eta$ , then its set integral disintegrates as

\int_s f(z)\,(\mu\eta)(dz)=\int \left(\int_s f(y)\,\eta(x,dy)\right)\mu(dx).

This is the measure-level specialization of the kernel composition integral theorem used to disintegrate finite-prefix trajectory measures.

Preamble

import Mathlib.Probability.Kernel.Composition.IntegralCompProd

open MeasureTheory ProbabilityTheory

Formal statement

theorem MarkovChainCLT.setIntegral_measure_comp_kernel
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (mu : Measure A) [SFinite mu]
    (eta : Kernel A B) [IsSFiniteKernel eta]
    {f : B → ℝ} {s : Set B}
    (hs : MeasurableSet s) (hf : IntegrableOn f s (eta ∘ₘ mu)) :
    ∫ z in s, f z ∂(eta ∘ₘ mu) = ∫ x, ∫ y in s, f y ∂eta x ∂mu := by sorry

Source

Mathlib, Probability.Kernel.Composition.IntegralCompProd, theorem ProbabilityTheory.Kernel.setIntegral_comp; the measure-kernel specialization is the standard Fubini/disintegration formula for composed kernels.

View graph