# mathlib3documentation

probability.kernel.cond_distrib

# Regular conditional probability distribution #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, cond_distrib 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 to Ω with its default σ-algebra and the conditional distribution defines a kernel associated with the conditional expectation with respect to m.

## Main definitions #

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

## Main statements #

• cond_distrib_ae_eq_condexp: for almost all a, cond_distrib 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_cond_distrib: the conditional expectation μ[(λ a, f (X a, Y a)) | X ; mβ] is almost everywhere equal to the integral ∫ y, f (X a, y) ∂(cond_distrib Y X μ (X a)).
@[irreducible]
noncomputable def probability_theory.cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} (Y : α Ω) (X : α β) (μ : measure_theory.measure α)  :

Regular conditional probability distribution: kernel associated with the conditional expectation of Y given X. For almost all a, cond_distrib 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 μ[(λ a, f (X a, Y a)) | mβ.comap X] =ᵐ[μ] λ a, ∫ y, f (X a, y) ∂(cond_distrib Y X μ (X a)) for all integrable functions f.

Equations
Instances for probability_theory.cond_distrib
@[protected, instance]
def probability_theory.cond_distrib.is_markov_kernel {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω}  :
theorem probability_theory.measurable_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hs : measurable_set s) :
measurable (λ (a : α), ( (X a)) s)
theorem measure_theory.ae_strongly_measurable.ae_integrable_cond_distrib_map_iff {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : μ) (hY : μ) (hf : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
(∀ᵐ (a : β) , measure_theory.integrable (λ (ω : Ω), f (a, ω)) ( a)) measure_theory.integrable (λ (a : β), (ω : Ω), f (a, ω) a) (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)
theorem measure_theory.ae_strongly_measurable.integral_cond_distrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : μ) (hY : μ) (hf : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.ae_strongly_measurable (λ (x : β), (y : Ω), f (x, y) x)
theorem measure_theory.ae_strongly_measurable.integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : μ) (hY : μ) (hf : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.ae_strongly_measurable (λ (a : α), (y : Ω), f (X a, y) (X a)) μ
theorem probability_theory.ae_strongly_measurable'_integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : μ) (hY : μ) (hf : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
(λ (a : α), (y : Ω), f (X a, y) (X a)) μ
theorem probability_theory.integrable_to_real_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hX : μ) (hs : measurable_set s) :
measure_theory.integrable (λ (a : α), (( (X a)) s).to_real) μ
theorem measure_theory.integrable.cond_distrib_ae_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
∀ᵐ (b : β) , measure_theory.integrable (λ (ω : Ω), f (b, ω)) ( b)
theorem measure_theory.integrable.cond_distrib_ae {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
∀ᵐ (a : α) μ, measure_theory.integrable (λ (ω : Ω), f (X a, ω)) ( (X a))
theorem measure_theory.integrable.integral_norm_cond_distrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (x : β), (y : Ω), f (x, y) x)
theorem measure_theory.integrable.integral_norm_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (a : α), (y : Ω), f (X a, y) (X a)) μ
theorem measure_theory.integrable.norm_integral_cond_distrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (x : β), (y : Ω), f (x, y) x)
theorem measure_theory.integrable.norm_integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (a : α), (y : Ω), f (X a, y) (X a)) μ
theorem measure_theory.integrable.integral_cond_distrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (x : β), (y : Ω), f (x, y) x)
theorem measure_theory.integrable.integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : μ) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (a : α), (y : Ω), f (X a, y) (X a)) μ
theorem probability_theory.set_lintegral_preimage_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} {t : set β} (hX : measurable X) (hY : μ) (hs : measurable_set s) (ht : measurable_set t) :
∫⁻ (a : α) in X ⁻¹' t, ( (X a)) s μ = μ (X ⁻¹' t Y ⁻¹' s)
theorem probability_theory.set_lintegral_cond_distrib_of_measurable_set {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hX : measurable X) (hY : μ) (hs : measurable_set s) {t : set α} (ht : measurable_set t) :
∫⁻ (a : α) in t, ( (X a)) s μ = μ (t Y ⁻¹' s)
theorem probability_theory.cond_distrib_ae_eq_condexp {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hX : measurable X) (hY : measurable Y) (hs : measurable_set s) :
(λ (a : α), (( (X a)) s).to_real) =ᵐ[μ] ((Y ⁻¹' s).indicator (λ (ω : α), 1))

For almost every a : α, the cond_distrib 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 probability_theory.condexp_prod_ae_eq_integral_cond_distrib' {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : measurable X) (hY : μ) (hf_int : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
(λ (a : α), f (X a, Y a)) =ᵐ[μ] λ (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 cond_distrib kernel.

theorem probability_theory.condexp_prod_ae_eq_integral_cond_distrib₀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : measurable X) (hY : μ) (hf : (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) (hf_int : measure_theory.integrable (λ (a : α), f (X a, Y a)) μ) :
(λ (a : α), f (X a, Y a)) =ᵐ[μ] λ (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 cond_distrib kernel.

theorem probability_theory.condexp_prod_ae_eq_integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [ F] (hX : measurable X) (hY : μ) (hf_int : measure_theory.integrable (λ (a : α), f (X a, Y a)) μ) :
(λ (a : α), f (X a, Y a)) =ᵐ[μ] λ (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 cond_distrib kernel.

theorem probability_theory.condexp_ae_eq_integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {Y : α Ω} {mβ : measurable_space β} [ F] (hX : measurable X) (hY : μ) {f : Ω F} (hf_int : measure_theory.integrable (λ (a : α), f (Y a)) μ) :
(λ (a : α), f (Y a)) =ᵐ[μ] λ (a : α), (y : Ω), f y (X a)
theorem probability_theory.condexp_ae_eq_integral_cond_distrib' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {μ : measure_theory.measure α} {X : α β} {mβ : measurable_space β} {Ω : Type u_3} [ Ω] [borel_space Ω] {Y : α Ω} (hX : measurable X) (hY_int : μ) :
Y =ᵐ[μ] λ (a : α), (y : Ω), y (X a)

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

theorem measure_theory.ae_strongly_measurable.comp_snd_map_prod_mk {β : Type u_2} {mβ : measurable_space β} {Ω : Type u_1} {F : Type u_3} {mΩ : measurable_space Ω} {X : Ω β} {μ : measure_theory.measure Ω} (hX : measurable X) {f : Ω F}  :
measure_theory.ae_strongly_measurable (λ (x : β × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (X ω, ω)) μ)
theorem measure_theory.integrable.comp_snd_map_prod_mk {β : Type u_2} {F : Type u_4} {mβ : measurable_space β} {Ω : Type u_1} {mΩ : measurable_space Ω} {X : Ω β} {μ : measure_theory.measure Ω} (hX : measurable X) {f : Ω F} (hf_int : μ) :
measure_theory.integrable (λ (x : β × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (X ω, ω)) μ)
theorem probability_theory.ae_strongly_measurable_comp_snd_map_prod_mk_iff {β : Type u_2} {mβ : measurable_space β} {Ω : Type u_1} {F : Type u_3} {mΩ : measurable_space Ω} {X : Ω β} {μ : measure_theory.measure Ω} (hX : measurable X) {f : Ω F} :
measure_theory.ae_strongly_measurable (λ (x : β × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (X ω, ω)) μ)
theorem probability_theory.integrable_comp_snd_map_prod_mk_iff {β : Type u_2} {F : Type u_4} {mβ : measurable_space β} {Ω : Type u_1} {mΩ : measurable_space Ω} {X : Ω β} {μ : measure_theory.measure Ω} (hX : measurable X) {f : Ω F} :
measure_theory.integrable (λ (x : β × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (X ω, ω)) μ)
theorem probability_theory.condexp_ae_eq_integral_cond_distrib_id {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [polish_space Ω] [borel_space Ω] [nonempty Ω] {mβ : measurable_space β} [ F] {X : Ω β} {μ : measure_theory.measure Ω} (hX : measurable X) {f : Ω F} (hf_int : μ) :
f =ᵐ[μ] λ (a : Ω), (y : Ω), f y (X a)