structure RegularConditionalDistribution {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace S] (μ_rcd : Ω → MeasureTheory.Measure S) (X : Ω → S) (𝒢 : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) : Prop

Regular conditional distribution (textbook form). A family of measures μ_rcd : Ω → Measure S is a regular conditional distribution for X given the sub-σ-algebra 𝒢 under P if: (1) for every measurable A ⊆ S, the map ω ↦ μ_rcd ω A is a version of P(X ∈ A | 𝒢), and (2) for P-a.e. ω, the map A ↦ μ_rcd ω A is a probability measure.

• ae_eq_condexp {A : Set S} : MeasurableSet A → (fun (ω : Ω) => ((μ_rcd ω) A).toReal) =ᵐ[P] P[(X ⁻¹' A).indicator fun (ω : Ω) => 1 | 𝒢]
• ae_isProbabilityMeasure : ∀ᵐ (ω : Ω) ∂P, MeasureTheory.IsProbabilityMeasure (μ_rcd ω)

structure ProbabilityTheory.IsRegularConditionalDistribution {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace Ω] (κ : Kernel β Ω) (Y : α → Ω) (X : α → β) (μ : MeasureTheory.Measure α) : Prop

Regular conditional distribution (kernel form). A Markov kernel κ : Kernel β Ω is a regular conditional distribution of Y : α → Ω given X : α → β under μ if for every measurable s ⊆ Ω, the function a ↦ κ (X a) s is a version of the conditional probability μ(Y ∈ s | σ(X)).

• isMarkovKernel : IsMarkovKernel κ
• ae_eq_condExp {s : Set Ω} : MeasurableSet s → (fun (a : α) => (κ (X a)).real s) =ᵐ[μ] μ[(Y ⁻¹' s).indicator fun (ω : α) => 1 | MeasurableSpace.comap X mβ]

theorem ProbabilityTheory.condDistrib_isRegularConditionalDistribution {α : 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) : IsRegularConditionalDistribution (condDistrib Y X μ) Y X μ

When Ω is a standard Borel space, Mathlib's condDistrib Y X μ is a regular conditional distribution of Y given X under μ. This packages condDistrib_ae_eq_condExp together with the Markov-kernel property.