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

### License

BSD License

### Topics

- Mathematics/Measure and integration
- Mathematics/Probability theory

### Session Disintegration

- Lemmas_Disintegration
- Disintegration

### Depends on

- S-Finite Measure Monad on Quasi-Borel Spaces
- Standard Borel Spaces

## Cite

×

Disintegration-AFP

    @article{Disintegration-AFP,
      author  = {Michikazu Hirata},
      title   = {Disintegration Theorem},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Disintegration.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest