# Regular conditional probability distribution #

We define the regular conditional probability distribution of Y : α → Ω given X : α → β, where Ω is a standard Borel space. This is a kernel β Ω such that for almost all a, condDistrib evaluated at X a and a measurable set s is equal to the conditional expectation μ⟦Y ⁻¹' s | mβ.comap X⟧ evaluated at a.

μ⟦Y ⁻¹' s | mβ.comap X⟧ maps a measurable set s to a function α → ℝ≥0∞, and for all s that map is unique up to a μ-null set. For all a, the map from sets to ℝ≥0∞ that we obtain that way verifies some of the properties of a measure, but in general the fact that the μ-null set depends on s can prevent us from finding versions of the conditional expectation that combine into a true measure. The standard Borel space assumption on Ω allows us to do so.

The case Y = X = id is developed in more detail in Probability/Kernel/Condexp.lean: here X is understood as a map from Ω with a sub-σ-algebra m to Ω with its default σ-algebra and the conditional distribution defines a kernel associated with the conditional expectation with respect to m.

## Main definitions #

• condDistrib Y X μ: regular conditional probability distribution of Y : α → Ω given X : α → β, where Ω is a standard Borel space.

## Main statements #

• condDistrib_ae_eq_condexp: for almost all a, condDistrib evaluated at X a and a measurable set s is equal to the conditional expectation μ⟦Y ⁻¹' s | mβ.comap X⟧ a.
• condexp_prod_ae_eq_integral_condDistrib: the conditional expectation μ[(fun a => f (X a, Y a)) | X; mβ] is almost everywhere equal to the integral ∫ y, f (X a, y) ∂(condDistrib Y X μ (X a)).
@[irreducible]
noncomputable def ProbabilityTheory.condDistrib {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [] [] :
{x : } → [inst : ] → (αΩ)(αβ)(μ : ) → [inst_1 : ] → ()

Regular conditional probability distribution: kernel associated with the conditional expectation of Y given X. For almost all a, condDistrib Y X μ evaluated at X a and a measurable set s is equal to the conditional expectation μ⟦Y ⁻¹' s | mβ.comap X⟧ a. It also satisfies the equality μ[(fun a => f (X a, Y a)) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂(condDistrib Y X μ (X a)) for all integrable functions f.

Equations
Instances For
theorem ProbabilityTheory.condDistrib_def {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [] [] :
∀ {x : } [inst : ] (Y : αΩ) (X : αβ) (μ : ) [inst_1 : ], = MeasureTheory.Measure.condKernel (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)
instance ProbabilityTheory.instIsMarkovKernelCondDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} [] :
Equations
• =
theorem ProbabilityTheory.condDistrib_apply_of_ne_zero {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } (hY : ) (x : β) (hX : {x} 0) (s : Set Ω) :
(() x) s = ( {x})⁻¹ * (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ) ({x} ×ˢ s)

If the singleton {x} has non-zero mass for μ.map X, then for all s : Set Ω, condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s) .

theorem ProbabilityTheory.measurable_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {s : Set Ω} (hs : ) :
Measurable fun (a : α) => (() (X a)) s
theorem MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} (hY : ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
(∀ᵐ (a : β) ∂, MeasureTheory.Integrable (fun (ω : Ω) => f (a, ω)) (() a)) MeasureTheory.Integrable (fun (a : β) => ∫ (ω : Ω), f (a, ω)() a) MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)
theorem MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] (hY : ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y)() x)
theorem MeasureTheory.AEStronglyMeasurable.integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] (hX : ) (hY : ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.AEStronglyMeasurable (fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)) μ
theorem ProbabilityTheory.aestronglyMeasurable'_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] (hX : ) (hY : ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.AEStronglyMeasurable' () (fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)) μ
theorem ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } (hX : ) (hY : ) (κ : ()) (hκ : MeasureTheory.Measure.map (fun (x : α) => (X x, Y x)) μ = ) :
∀ᵐ (x : β) ∂, κ x = () x

condDistrib is a.e. uniquely defined as the kernel satisfying the defining property of condKernel.

theorem ProbabilityTheory.integrable_toReal_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {s : Set Ω} (hX : ) (hs : ) :
MeasureTheory.Integrable (fun (a : α) => ((() (X a)) s).toReal) μ
theorem MeasureTheory.Integrable.condDistrib_ae_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
∀ᵐ (b : β) ∂, MeasureTheory.Integrable (fun (ω : Ω) => f (b, ω)) (() b)
theorem MeasureTheory.Integrable.condDistrib_ae {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} (hX : ) (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (ω : Ω) => f (X a, ω)) (() (X a))
theorem MeasureTheory.Integrable.integral_norm_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.Integrable (fun (x : β) => ∫ (y : Ω), f (x, y)() x)
theorem MeasureTheory.Integrable.integral_norm_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} (hX : ) (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.Integrable (fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)) μ
theorem MeasureTheory.Integrable.norm_integral_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.Integrable (fun (x : β) => ∫ (y : Ω), f (x, y)() x)
theorem MeasureTheory.Integrable.norm_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] (hX : ) (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.Integrable (fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)) μ
theorem MeasureTheory.Integrable.integral_condDistrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.Integrable (fun (x : β) => ∫ (y : Ω), f (x, y)() x)
theorem MeasureTheory.Integrable.integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] (hX : ) (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
MeasureTheory.Integrable (fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)) μ
theorem ProbabilityTheory.set_lintegral_preimage_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {s : Set Ω} {t : Set β} (hX : ) (hY : ) (hs : ) (ht : ) :
∫⁻ (a : α) in X ⁻¹' t, (() (X a)) sμ = μ (X ⁻¹' t Y ⁻¹' s)
theorem ProbabilityTheory.set_lintegral_condDistrib_of_measurableSet {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {s : Set Ω} (hX : ) (hY : ) (hs : ) {t : Set α} (ht : ) :
∫⁻ (a : α) in t, (() (X a)) sμ = μ (t Y ⁻¹' s)
theorem ProbabilityTheory.condDistrib_ae_eq_condexp {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {s : Set Ω} (hX : ) (hY : ) (hs : ) :
(fun (a : α) => ((() (X a)) s).toReal) =ᶠ[] MeasureTheory.condexp () μ (Set.indicator (Y ⁻¹' s) fun (ω : α) => 1)

For almost every a : α, the condDistrib Y X μ kernel applied to X a and a measurable set s is equal to the conditional expectation of the indicator of Y ⁻¹' s.

theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib' {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] [] (hX : ) (hY : ) (hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) :
(MeasureTheory.condexp () μ fun (a : α) => f (X a, Y a)) =ᶠ[] fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)

The conditional expectation of a function f of the product (X, Y) is almost everywhere equal to the integral of y ↦ f(X, y) against the condDistrib kernel.

theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] [] (hX : ) (hY : ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)) (hf_int : MeasureTheory.Integrable (fun (a : α) => f (X a, Y a)) μ) :
(MeasureTheory.condexp () μ fun (a : α) => f (X a, Y a)) =ᶠ[] fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)

The conditional expectation of a function f of the product (X, Y) is almost everywhere equal to the integral of y ↦ f(X, y) against the condDistrib kernel.

theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {f : β × ΩF} [] [] (hX : ) (hY : ) (hf : ) (hf_int : MeasureTheory.Integrable (fun (a : α) => f (X a, Y a)) μ) :
(MeasureTheory.condexp () μ fun (a : α) => f (X a, Y a)) =ᶠ[] fun (a : α) => ∫ (y : Ω), f (X a, y)() (X a)

The conditional expectation of a function f of the product (X, Y) is almost everywhere equal to the integral of y ↦ f(X, y) against the condDistrib kernel.

theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } [] [] (hX : ) (hY : ) {f : ΩF} (hf : ) (hf_int : MeasureTheory.Integrable (fun (a : α) => f (Y a)) μ) :
(MeasureTheory.condexp () μ fun (a : α) => f (Y a)) =ᶠ[] fun (a : α) => ∫ (y : Ω), f y() (X a)
theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib' {α : Type u_1} {β : Type u_2} {mα : } {μ : } {X : αβ} {mβ : } {Ω : Type u_5} [] [] [] [] {Y : αΩ} (hX : ) (hY_int : ) :
=ᶠ[] fun (a : α) => ∫ (y : Ω), y() (X a)

The conditional expectation of Y given X is almost everywhere equal to the integral ∫ y, y ∂(condDistrib Y X μ (X a)).

theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_mk {β : Type u_2} {mβ : } {Ω : Type u_5} {F : Type u_6} {mΩ : } (X : Ωβ) {μ : } [] {f : ΩF} (hf : ) :
MeasureTheory.AEStronglyMeasurable (fun (x : β × Ω) => f x.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
theorem MeasureTheory.Integrable.comp_snd_map_prod_mk {β : Type u_2} {F : Type u_4} {mβ : } {Ω : Type u_5} {mΩ : } (X : Ωβ) {μ : } {f : ΩF} (hf_int : ) :
MeasureTheory.Integrable (fun (x : β × Ω) => f x.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
theorem ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prod_mk_iff {β : Type u_2} {mβ : } {Ω : Type u_5} {F : Type u_6} :
∀ {x : } [inst : ] {X : Ωβ} {μ : }, ∀ {f : ΩF}, MeasureTheory.AEStronglyMeasurable (fun (x : β × Ω) => f x.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
theorem ProbabilityTheory.integrable_comp_snd_map_prod_mk_iff {β : Type u_2} {F : Type u_4} {mβ : } {Ω : Type u_5} :
∀ {x : } {X : Ωβ} {μ : }, ∀ {f : ΩF}, MeasureTheory.Integrable (fun (x : β × Ω) => f x.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib_id {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [] [] {mβ : } [] [] {X : Ωβ} {μ : } (hX : ) {f : ΩF} (hf_int : ) :
=ᶠ[] fun (a : Ω) => ∫ (y : Ω), f y() (X a)