mathlib3 documentation

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 #

Main statements #

@[irreducible]
noncomputable def probability_theory.cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} [measurable_space β] (Y : α Ω) (X : α β) (μ : measure_theory.measure α) [measure_theory.is_finite_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
theorem probability_theory.measurable_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hs : measurable_set s) :
measurable (λ (a : α), ((probability_theory.cond_distrib Y X μ) (X a)) s)
theorem measure_theory.ae_strongly_measurable.integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf : measure_theory.ae_strongly_measurable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.ae_strongly_measurable (λ (a : α), (y : Ω), f (X a, y) (probability_theory.cond_distrib Y X μ) (X a)) μ
theorem probability_theory.integrable_to_real_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hX : ae_measurable X μ) (hs : measurable_set s) :
theorem measure_theory.integrable.cond_distrib_ae_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
theorem measure_theory.integrable.cond_distrib_ae {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
∀ᵐ (a : α) μ, measure_theory.integrable (λ (ω : Ω), f (X a, ω)) ((probability_theory.cond_distrib Y X μ) (X a))
theorem measure_theory.integrable.integral_norm_cond_distrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
theorem measure_theory.integrable.integral_norm_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (a : α), (y : Ω), f (X a, y) (probability_theory.cond_distrib Y X μ) (X a)) μ
theorem measure_theory.integrable.norm_integral_cond_distrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
theorem measure_theory.integrable.norm_integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (a : α), (y : Ω), f (X a, y) (probability_theory.cond_distrib Y X μ) (X a)) μ
theorem measure_theory.integrable.integral_cond_distrib_map {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
theorem measure_theory.integrable.integral_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : ae_measurable X μ) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.integrable (λ (a : α), (y : Ω), f (X a, y) (probability_theory.cond_distrib Y X μ) (X a)) μ
theorem probability_theory.set_lintegral_preimage_cond_distrib {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} {t : set β} (hX : measurable X) (hY : ae_measurable Y μ) (hs : measurable_set s) (ht : measurable_set t) :
∫⁻ (a : α) in X ⁻¹' t, ((probability_theory.cond_distrib Y X μ) (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} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hX : measurable X) (hY : ae_measurable Y μ) (hs : measurable_set s) {t : set α} (ht : measurable_set t) :
∫⁻ (a : α) in t, ((probability_theory.cond_distrib Y X μ) (X a)) s μ = μ (t Y ⁻¹' s)
theorem probability_theory.cond_distrib_ae_eq_condexp {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {s : set Ω} (hX : measurable X) (hY : measurable Y) (hs : measurable_set s) :
(λ (a : α), (((probability_theory.cond_distrib Y X μ) (X a)) s).to_real) =ᵐ[μ] measure_theory.condexp (measurable_space.comap X mβ) μ ((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} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : measurable X) (hY : ae_measurable Y μ) (hf_int : measure_theory.integrable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
measure_theory.condexp (measurable_space.comap X mβ) μ (λ (a : α), f (X a, Y a)) =ᵐ[μ] λ (a : α), (y : Ω), f (X a, y) (probability_theory.cond_distrib Y X μ) (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} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : measurable X) (hY : ae_measurable Y μ) (hf : measure_theory.ae_strongly_measurable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) (hf_int : measure_theory.integrable (λ (a : α), f (X a, Y a)) μ) :
measure_theory.condexp (measurable_space.comap X mβ) μ (λ (a : α), f (X a, Y a)) =ᵐ[μ] λ (a : α), (y : Ω), f (X a, y) (probability_theory.cond_distrib Y X μ) (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} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} {f : β × Ω F} [normed_space F] [complete_space F] (hX : measurable X) (hY : ae_measurable Y μ) (hf : measure_theory.strongly_measurable f) (hf_int : measure_theory.integrable (λ (a : α), f (X a, Y a)) μ) :
measure_theory.condexp (measurable_space.comap X mβ) μ (λ (a : α), f (X a, Y a)) =ᵐ[μ] λ (a : α), (y : Ω), f (X a, y) (probability_theory.cond_distrib Y X μ) (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} [topological_space Ω] [measurable_space Ω] [polish_space Ω] [borel_space Ω] [nonempty Ω] [normed_add_comm_group F] {mα : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {X : α β} {Y : α Ω} {mβ : measurable_space β} [normed_space F] [complete_space F] (hX : measurable X) (hY : ae_measurable Y μ) {f : Ω F} (hf : measure_theory.strongly_measurable f) (hf_int : measure_theory.integrable (λ (a : α), f (Y a)) μ) :
measure_theory.condexp (measurable_space.comap X mβ) μ (λ (a : α), f (Y a)) =ᵐ[μ] λ (a : α), (y : Ω), f y (probability_theory.cond_distrib Y X μ) (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 Ω} [topological_space F] (hX : measurable X) {f : Ω F} (hf : measure_theory.ae_strongly_measurable 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} [normed_add_comm_group F] {mβ : measurable_space β} {Ω : Type u_1} {mΩ : measurable_space Ω} {X : Ω β} {μ : measure_theory.measure Ω} (hX : measurable X) {f : Ω F} (hf_int : measure_theory.integrable f μ) :
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 Ω} [topological_space F] {X : Ω β} {μ : measure_theory.measure Ω} (hX : measurable X) {f : Ω F} :
theorem probability_theory.integrable_comp_snd_map_prod_mk_iff {β : Type u_2} {F : Type u_4} [normed_add_comm_group F] {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 ω, ω)) μ) measure_theory.integrable f μ