Disintegration Theorem

We formalize mixture and disintegraion of measures. This entry is a formalization of Chapter 14.D of the book by Baccelli et.al. The main result is the disintegration theorem: let $(X,\Sigma_X)$ be a measurable space, $(Y,\Sigma_Y)$ be a standard Borel space, $\nu$ be a $\sigma$-finite measure on $X \times Y$, and $\nu_X$ be the marginal measure on $X$ defined by $\nu_X(A) = \nu(A\times Y)$. Assume that $\nu_X$ is $\sigma$-finite, then there exists a probability kernel $\kappa$ from $X$ to $Y$ such that \[ \nu(A\times B) = \int_A \kappa_x (B) \nu_X(\mathrm{d}x), \: A\in\Sigma_X, B\in\Sigma_Y.\] Such a probability kernel is unique $\nu_X$-almost everywhere.