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 be a measurable space, be a standard Borel space, be a -finite measure on ,
and be the marginal measure on defined by .
Assume that is -finite, then there exists a probability kernel
from to such that
Such a probability kernel is unique -almost everywhere.