theorem ProbabilityTheory.exists_regularConditionalDistribution {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} (hX : Measurable X) (hY : Measurable Y) : ∃ (κ : Kernel β Ω), IsRegularConditionalDistribution κ Y X μ

Existence of regular conditional probabilities. When Ω is a standard Borel space (a "nice" space), for any finite measure μ and measurable maps X : α → β, Y : α → Ω, there exists a Markov kernel κ : Kernel β Ω that is a regular conditional distribution of Y given X.