Composition of measure and kernel

Stream: Is there code for X?

[Kin Yau James Wong]

Hello, I am aware that the composition of Markov kernels already exists in mathlib. The composition of a measure and a Markov kernel would be a special case of this composition, where we interpret the measure as a kernel from a singleton to some other measurable space. Does such an implementation already exist in mathlib?

[Rémy Degenne]

It exists in Mathlib, but mostly without API: this is MeasureTheory.Measure.bind

[Yaël Dillies]

Thanks Rémy!

[Rémy Degenne]

With @Lorenzo Luccioli we added API for it in our project about divergences between measures here: https://github.com/RemyDegenne/testing-lower-bounds/blob/master/TestingLowerBounds/MeasureCompProd.lean

[Rémy Degenne]

That code will make its way to mathlib, but it's not there yet.

[Rémy Degenne]

Feel free to copy anything you could need for your own project

[Yaël Dillies]

Is it just this one file we should copy or do you have more stuff elsewhere?

[Rémy Degenne]

That file imports other files from our project. You'll need to look around and pick what you need, sorry.

[Yaël Dillies]

Ah okay, will try doing that and complain if it's too painful :smile: