Conditional measures / disintegration

Stream: Is there code for X?

[Lua Viana Reis]

I see there is docs#MeasureTheory.Measure.condKernel, but does it easily imply in the existence of conditional measures as generally as written in Bogachev below? If not, is this theorem desirable for mathlib if I'm willing to write it and contribute? (this is the most general statement of the "Rokhlin disintegration" that I know).

image.png

[Lua Viana Reis]

ChatGPT transcription for accessibility:

10.4.5. Theorem.
(i) Suppose that the $\sigma$-algebra $\mathcal{A}$ is countably generated and that $\mu$ has a compact approximating class in $\mathcal{A}$. Then, for every sub-$\sigma$-algebra $\mathcal{B} \subset \mathcal{A}$, there exists a regular conditional measure $\mu^{\mathcal{B}}$ on $\mathcal{A}$.

(ii) More generally, let $\mathcal{A}_0$ be a sub-$\sigma$-algebra in the $\sigma$-algebra $\mathcal{A}$ such that there exists a countable algebra $\mathcal{U}$ generating $\mathcal{A}_0$. Assume, additionally, that there is a compact class $\mathcal{K}$ such that for every $A \in \mathcal{U}$ and $\varepsilon > 0$, there exist $K_\varepsilon \in \mathcal{K}$ and $A_\varepsilon \in \mathcal{A}$ with $A_\varepsilon \subset K_\varepsilon \subset A$ and $|\mu|(A \setminus A_\varepsilon) < \varepsilon$. Then, for every sub-$\sigma$-algebra $\mathcal{B} \subset \mathcal{A}$, there exists a regular conditional measure $\mu^{\mathcal{B}}_{\mathcal{A}_0}$ on $\mathcal{A}_0$ (a probability if $\mu$ is nonnegative).

In addition, for every $\mathcal{A}_0$-measurable $\mu$-integrable function $f$, one has:

$$\int_X f\,d\mu = \int_X \left( \int_X f(y)\,\mu^{\mathcal{B}}_{\mathcal{A}_0}(dy,x) \right) |\mu|(dx).$$