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 ofY : α → ΩgivenX : α → β, whereΩis a standard Borel space.
Main statements #
cond_distrib_ae_eq_condexp: for almost alla,cond_distribevaluated atX aand a measurable setsis 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}
[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
- probability_theory.cond_distrib Y X μ = (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ).cond_kernel
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}
[topological_space Ω]
[measurable_space Ω]
[polish_space Ω]
[borel_space Ω]
[nonempty Ω]
{mα : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
{X : α → β}
{Y : α → Ω}
[measurable_space β] :
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.ae_integrable_cond_distrib_map_iff
{α : 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 : measure_theory.ae_strongly_measurable f (measure_theory.measure.map (λ (a : α), (X a, Y a)) μ)) :
(∀ᵐ (a : β) ∂measure_theory.measure.map X μ, measure_theory.integrable (λ (ω : Ω), f (a, ω)) (⇑(probability_theory.cond_distrib Y X μ) a)) ∧ measure_theory.integrable (λ (a : β), ∫ (ω : Ω), ‖f (a, ω)‖ ∂⇑(probability_theory.cond_distrib Y X μ) a) (measure_theory.measure.map X μ) ↔ measure_theory.integrable f (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}
[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 (λ (x : β), ∫ (y : Ω), f (x, y) ∂⇑(probability_theory.cond_distrib Y X μ) x) (measure_theory.measure.map X μ)
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.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' (measurable_space.comap X mβ) (λ (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) :
measure_theory.integrable (λ (a : α), (⇑(⇑(probability_theory.cond_distrib Y X μ) (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}
[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)) μ)) :
∀ᵐ (b : β) ∂measure_theory.measure.map X μ, measure_theory.integrable (λ (ω : Ω), f (b, ω)) (⇑(probability_theory.cond_distrib Y X μ) b)
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)) μ)) :
measure_theory.integrable (λ (x : β), ∫ (y : Ω), ‖f (x, y)‖ ∂⇑(probability_theory.cond_distrib Y X μ) x) (measure_theory.measure.map X μ)
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)) μ)) :
measure_theory.integrable (λ (x : β), ‖∫ (y : Ω), f (x, y) ∂⇑(probability_theory.cond_distrib Y X μ) x‖) (measure_theory.measure.map X μ)
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)) μ)) :
measure_theory.integrable (λ (x : β), ∫ (y : Ω), f (x, y) ∂⇑(probability_theory.cond_distrib Y X μ) x) (measure_theory.measure.map X μ)
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) :
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) :
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)
theorem
probability_theory.condexp_ae_eq_integral_cond_distrib'
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
{X : α → β}
{mβ : measurable_space β}
{Ω : Type u_3}
[normed_add_comm_group Ω]
[normed_space ℝ Ω]
[complete_space Ω]
[measurable_space Ω]
[borel_space Ω]
[topological_space.second_countable_topology Ω]
{Y : α → Ω}
(hX : measurable X)
(hY_int : measure_theory.integrable Y μ) :
measure_theory.condexp (measurable_space.comap X mβ) μ Y =ᵐ[μ] λ (a : α), ∫ (y : Ω), 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} :
measure_theory.ae_strongly_measurable (λ (x : β × Ω), f x.snd) (measure_theory.measure.map (λ (ω : Ω), (X ω, ω)) μ) ↔ measure_theory.ae_strongly_measurable 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 μ
theorem
probability_theory.condexp_ae_eq_integral_cond_distrib_id
{β : 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 β}
[normed_space ℝ F]
[complete_space F]
{X : Ω → β}
{μ : measure_theory.measure Ω}
[measure_theory.is_finite_measure μ]
(hX : measurable X)
{f : Ω → F}
(hf_int : measure_theory.integrable f μ) :
measure_theory.condexp (measurable_space.comap X mβ) μ f =ᵐ[μ] λ (a : Ω), ∫ (y : Ω), f y ∂⇑(probability_theory.cond_distrib id X μ) (X a)