feat(Probability/Kernel): disintegration of finite kernels

[RemyDegenne]

Let κ : kernel α (β × Ω) be a finite kernel, where Ω is a standard Borel space. Then if α is countable or β has a countably generated σ-algebra (for example if it is standard Borel), there exists a kernel (α × β) Ω, called conditional kernel and denoted by kernel.condKernel κ such that κ = kernel.fst κ ⊗ₖ kernel.condKernel κ. We also define a conditional kernel for a measure ρ : Measure (β × Ω), where Ω is a standard Borel space. This is a kernel β Ω denoted by ρ.condKernel such that ρ = ρ.fst ⊗ₘ ρ.condKernel.

In order to obtain a disintegration for any standard Borel space Ω, we use that these spaces embed measurably into ℝ: it then suffices to define a suitable kernel for Ω = ℝ.

For κ : kernel α (β × ℝ), the construction of the conditional kernel proceeds as follows:

• Build a measurable function f : (α × β) → ℚ → ℝ such that for all measurable sets s and all q : ℚ, ∫ x in s, f (a, x) q ∂(kernel.fst κ a) = (κ a (s ×ˢ Iic (q : ℝ))).toReal. We restrict to Q here to be able to prove the measurability.
• Extend that function to (α × β) → StieltjesFunction. See the file MeasurableStieltjes.lean.
• Finally obtain from the measurable Stieltjes function a measure on ℝ for each element of α × β in a measurable way: we have obtained a kernel (α × β) ℝ. See the file CDFKernel.lean for that step.

The first step (building the measurable function on ℚ) is done differently depending on whether α is countable or not.

• If α is countable, we can provide for each a : α a function f : β → ℚ → ℝ and proceed as above to obtain a kernel β ℝ. Since α is countable, measurability is not an issue and we can put those together into a kernel (α × β) ℝ. The construction of that f is done in the CondCDF.lean file.
• If α is not countable, we can't proceed separately for each a : α and have to build a function f : α × β → ℚ → ℝ which is measurable on the product. We are able to do so if β has a countably generated σ-algebra (this is the case in particular for standard Borel spaces). See the files Density.lean and KernelCDFReal.lean.

We define a class CountableOrCountablyGenerated α β which encodes the property (Countable α ∧ MeasurableSingletonClass α) ∨ CountablyGenerated β. The conditional kernel is defined under that assumption.

Properties of integrals involving kernel.condKernel are collated in the file Integral.lean. The conditional kernel is unique (almost everywhere w.r.t. kernel.fst κ): this is proved in the file Unique.lean.

---

[sgouezel]

When alpha is countable, can you explain why you need MeasurableSingletonClass? Otherwise, I would expect that everything is constant on the atoms of the partition generated by the sigma-algebra, and the quotient space is countable, so the general case should be reducable to the MeasurableSingletonClass case. I'm absolutely not saying that it should be implemented in this way with a quotient, rather that with this heuristics I don't see mathematically why MeasurableSingletonClass should be relevant.

[RemyDegenne]

The non-mathematical reason I added that hypothesis is that I used measurable_from_prod_countable (in the file Probability.Kernel.Disintegration.Basic). It asked for that typeclass and I added it without thinking about it.

[RemyDegenne]

I don't see how I could remove the MeasurableSingletonClass assumption without adding another assumption somewhere. To conclude that everything is constant on the atoms, I would need the codomain to have measurable singletons? Otherwise the function could take several values in a non-singleton atom, as long as all those values belong to some atom of the codomain?

Also the existence of a partition of atoms would mean that the measurable space is countably generated, but I think that's not necessarily the case even if the space is countable.

[sgouezel]

I don't see how I could remove the MeasurableSingletonClass assumption without adding another assumption somewhere. To conclude that everything is constant on the atoms, I would need the codomain to have measurable singletons? Otherwise the function could take several values in a non-singleton atom, as long as all those values belong to some atom of the codomain?

I would think that everything is done taking preimages of measurable sets under measurable maps. Such preimages should be constant over atoms, right? (Warning: I haven't looked at the code, so I might be completely wrong)

Also the existence of a partition of atoms would mean that the measurable space is countably generated, but I think that's not necessarily the case even if the space is countable.

I don't see the problem here. Define the atom of x as the intersection of all measurable sets that contain x. For any y not in the atom, one can take a measurable set containing x but not y, so the atom is in fact a countable intersection (of such sets over all y not belonging to the atom), and it belongs to the sigma-algebra. Then any measurable set is the (countable) union of the atoms it contains. But again, I don't think one should go through this argument for the construction, rather see where MeasurableSingletonClass is used and if one can remove it locally. If you want, I can have a look in the next days.

[RemyDegenne]

@sgouezel All prerequisites are now merged (thanks for the reviews!), and this is the final disintegration PR. I did not resolve your question about the MeasurableSetSingleton hypothesis: if you have time to have a look at the construction and see if you can remove that hypothesis, that would be great!

[sgouezel]

I've just pushed a commit removing MeasurableSetSingleton, following the sketch above. Can you tell me if you're happy with the modification? If so, I'll review the rest of the PR.

[RemyDegenne]

Thanks for the help! Your code looks good. I saw a place where I think I can refactor my code to improve its clarity, so I'm turning that PR back to awaiting-author for now and will come back to you when it's again ready for review.

[sgouezel]

I'm confused by github here. I got an email saying that you had realized that the refactor wasn't worth it, and that the PR was ready for review, but I can't see your message on github and the PR is still awaiting author. Can you confirm that I did not dream this message, and that the PR is indeed ready for review?

[RemyDegenne]

The PR is not ready for review. I wrote that message too fast, changed my mind once again about the refactor and then deleted the message. I forgot that github also sends an email. The refactor is in progress. Sorry for the confusion!

[RemyDegenne]

The refactor is done and this is ready for review. The PR is big, but if I dismantle the old disintegration file I have to have all the replacements in the PR (which means I can't PR the files about integrals and uniqueness later).

[mathlib-bors[bot]]

:v: RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

Thanks for all the reviews and for your help on the disintegration PRs. No worries about the review time: I don't expect a quick review for a 1000 lines PR :) I agree that the assumptions in the Unique file don't feel right. I won't work on that myself for now (at least not for the next days), so feel free to have a look.

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style