Equivalence of definitions of probability kernels

Stream: Is there code for X?

[Fred Rajasekaran]

Does anyone know if someone has proved the equivalence between the two following definitions of probability kernels? The first is the more standard definition currently in mathlib and also given on the Wikipedia page. The second is that a kernel is a measurable map

$$\kappa : X \to \mathcal{P}(\mathcal{Y})$$

(using the notation from the Wikipedia page), where P(Y) is the space of all probability measures on Y equipped with the cylinder sigma algebra generated by the projections

$$\pi_B : \mathcal{P}(\mathcal{Y}) \to [0,1], \qquad B \in \mathcal{B}$$

that sends

$$\pi_{B}(\mu) = \mu(B),$$

with [0,1] equipped with the standard Borel sigma algebra (a reference for this definition is for example Kallenberg's probability book, Chapter 3). I'm happy to formalize it myself, but would be easier if it's done already (I couldn't find it when I looked in mathlib, though maybe I missed it)

[Aaron Liu]

I though mathlib used the second definition

[Aaron Liu]

docs#ProbabilityTheory.Kernel

[Etienne Marion]

Indeed Mathlib's definition is the second, and you get the first with ProbabilityTheory.Kernel.measurable_coe.

[Etienne Marion]

The general equivalence is MeasureTheory.Measure.measurable_measure.

[Fred Rajasekaran]

Thanks! and yea sorry messed up in my head which was the one in mathlib :sweat_smile: