Randomized inverses of maps of a uniform variable #
Disintegration supplies a randomized inverse even when a map has fibers of positive measure. This is the extra randomness needed to handle atoms in Sklar's theorem.
theorem
ProbabilityTheory.exists_randomized_inverse
{B : Type u_1}
[MeasurableSpace B]
[StandardBorelSpace B]
[Nonempty B]
(q : ↑unitInterval → B)
(hq : Measurable q)
:
∃ (g : B → ↑unitInterval → ↑unitInterval),
Measurable (Function.uncurry g) ∧ MeasureTheory.Measure.map (Function.uncurry g)
((MeasureTheory.Measure.map q MeasureTheory.volume).prod MeasureTheory.volume) = MeasureTheory.volume ∧ ∀ᵐ (p : B × ↑unitInterval) ∂(MeasureTheory.Measure.map q MeasureTheory.volume).prod MeasureTheory.volume, q (g p.1 p.2) = p.1
A measurable map of a uniform variable has a randomized inverse that recovers the uniform law and inverts the map almost everywhere.