# Documentation

Mathlib.Probability.Kernel.CondDistrib

# 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 : ] → { x // }

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.

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 : αΩ} [] :
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, ω)) MeasureTheory.Integrable fun a => ∫ (ω : Ω), f (a, ω)↑() 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.integrable_toReal_condDistrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [] [] [] [] [] {mα : } {μ : } {X : αβ} {Y : αΩ} {mβ : } {s : Set Ω} (hX : ) (hs : ) :
MeasureTheory.Integrable fun a => ENNReal.toReal (↑(↑() (X a)) s)
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 : ) :
∀ᵐ (b : β) ∂, MeasureTheory.Integrable fun ω => f (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 : ) :
∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable fun ω => f (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 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 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 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 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 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 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 => ENNReal.toReal (↑(↑() (X a)) s)) =ᶠ[] 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.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.snd) (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.snd
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.snd) (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.snd)
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)