Randomization Lemma

Stream: Is there code for X?

[Anthony Vandikas]

Does mathlib contain a formalization of any of the "Randomization Lemmas" found in this paper (section 10)?

The simplest version of this is: every probability measure on a standard borel space is equal to the pushforward of some function on the uniform measure on [0, 1].

[Rémy Degenne]

It's not in Mathlib yet but we have it for Markov kernels in a PR: #30112
It's not quite in the generality of the paper you linked, but if I remember correctly that paper uses the result for Markov kernels on the path to getting randomization for s-finite kernels.