Abstract
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.