Disintegration theorem for a probability measure (source code)

= Disintegration theorem for a probability measure
{title2=$\mu=\int\mu_y\,d(\pi_*\mu)(y)$}

For a <probability measure> on a standard Borel space and a measurable map $\pi$ to another standard Borel space, there is an almost-everywhere unique <measurable probability kernel> $y\mapsto\mu_y$ supported on $\pi^{-1}\{y\}$. It integrates to $\mu$, and $\int f\,d\mu_{\pi(x)}$ realizes <conditional expectation> given $\pi$. These measures are the <conditional measures of a factor>.