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 ofY : α → ΩgivenX : α → β, whereΩis a standard Borel space.
Main statements #
condDistrib_ae_eq_condexp: for almost alla,condDistribevaluated atX aand a measurable setsis 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
:
{x : MeasurableSpace α} →
[inst : MeasurableSpace β] →
(α → Ω) →
(α → β) →
(μ : MeasureTheory.Measure α) → [inst_1 : MeasureTheory.IsFiniteMeasure μ] → ↥(ProbabilityTheory.kernel β Ω)
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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
:
∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] (Y : α → Ω) (X : α → β) (μ : MeasureTheory.Measure α)
[inst_1 : MeasureTheory.IsFiniteMeasure μ],
ProbabilityTheory.condDistrib Y X μ = MeasureTheory.Measure.condKernel (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)
instance
ProbabilityTheory.instIsMarkovKernelCondDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
[MeasurableSpace β]
:
Equations
- (_ : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.condDistrib Y X μ)) = (_ : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.condDistrib Y X μ))
theorem
ProbabilityTheory.condDistrib_apply_of_ne_zero
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
[MeasurableSingletonClass β]
(hY : Measurable Y)
(x : β)
(hX : ↑↑(MeasureTheory.Measure.map X μ) {x} ≠ 0)
(s : Set Ω)
:
↑↑((ProbabilityTheory.condDistrib Y X μ) x) s = (↑↑(MeasureTheory.Measure.map X μ) {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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hs : MeasurableSet s)
:
Measurable fun (a : α) => ↑↑((ProbabilityTheory.condDistrib Y X μ) (X a)) s
theorem
MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
((∀ᵐ (a : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable fun (ω : Ω) => f (a, ω)) ∧ MeasureTheory.Integrable fun (a : β) => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(ProbabilityTheory.condDistrib Y X μ) a) ↔ MeasureTheory.Integrable f
theorem
MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
MeasureTheory.AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x)
(MeasureTheory.Measure.map X μ)
theorem
MeasureTheory.AEStronglyMeasurable.integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
MeasureTheory.AEStronglyMeasurable (fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
theorem
ProbabilityTheory.aestronglyMeasurable'_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
MeasureTheory.AEStronglyMeasurable' (MeasurableSpace.comap X mβ)
(fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
theorem
ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
(hX : Measurable X)
(hY : Measurable Y)
(κ : ↥(ProbabilityTheory.kernel β Ω))
[ProbabilityTheory.IsFiniteKernel κ]
(hκ : MeasureTheory.Measure.map (fun (x : α) => (X x, Y x)) μ = MeasureTheory.Measure.compProd (MeasureTheory.Measure.map X μ) κ)
:
∀ᵐ (x : β) ∂MeasureTheory.Measure.map X μ, κ x = (ProbabilityTheory.condDistrib Y 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : AEMeasurable X)
(hs : MeasurableSet s)
:
MeasureTheory.Integrable fun (a : α) => ENNReal.toReal (↑↑((ProbabilityTheory.condDistrib Y X μ) (X a)) s)
theorem
MeasureTheory.Integrable.condDistrib_ae_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
∀ᵐ (b : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable fun (ω : Ω) => f (b, ω)
theorem
MeasureTheory.Integrable.condDistrib_ae
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
∀ᵐ (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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun (x : β) => ∫ (y : Ω), ‖f (x, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) x
theorem
MeasureTheory.Integrable.integral_norm_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun (a : α) => ∫ (y : Ω), ‖f (X a, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
theorem
MeasureTheory.Integrable.norm_integral_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun (x : β) => ‖∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x‖
theorem
MeasureTheory.Integrable.norm_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun (a : α) => ‖∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)‖
theorem
MeasureTheory.Integrable.integral_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun (x : β) => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x
theorem
MeasureTheory.Integrable.integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
theorem
ProbabilityTheory.set_lintegral_preimage_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
{t : Set β}
(hX : Measurable X)
(hY : AEMeasurable Y)
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.set_lintegral_condDistrib_of_measurableSet
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : Measurable X)
(hY : AEMeasurable Y)
(hs : MeasurableSet s)
{t : Set α}
(ht : MeasurableSet t)
:
∫⁻ (a : α) in t, ↑↑((ProbabilityTheory.condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (t ∩ Y ⁻¹' s)
theorem
ProbabilityTheory.condDistrib_ae_eq_condexp
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : Measurable X)
(hY : Measurable Y)
(hs : MeasurableSet s)
:
(fun (a : α) => ENNReal.toReal (↑↑((ProbabilityTheory.condDistrib Y X μ) (X a)) s)) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ (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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun (a : α) => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib 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 condDistrib kernel.
theorem
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
(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 (MeasurableSpace.comap X mβ) μ fun (a : α) => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib 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 condDistrib kernel.
theorem
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_int : MeasureTheory.Integrable fun (a : α) => f (X a, Y a))
:
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun (a : α) => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib 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 condDistrib kernel.
theorem
ProbabilityTheory.condexp_ae_eq_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
{f : Ω → F}
(hf : MeasureTheory.StronglyMeasurable f)
(hf_int : MeasureTheory.Integrable fun (a : α) => f (Y a))
:
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun (a : α) => f (Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
theorem
ProbabilityTheory.condexp_ae_eq_integral_condDistrib'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
[NormedAddCommGroup Ω]
[NormedSpace ℝ Ω]
[CompleteSpace Ω]
[MeasurableSpace Ω]
[BorelSpace Ω]
[SecondCountableTopology Ω]
{Y : α → Ω}
(hX : Measurable X)
(hY_int : MeasureTheory.Integrable Y)
:
MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ Y =ᶠ[MeasureTheory.Measure.ae μ] fun (a : α) =>
∫ (y : Ω), y ∂(ProbabilityTheory.condDistrib Y X μ) (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β : MeasurableSpace β}
{Ω : Type u_5}
{F : Type u_6}
{mΩ : MeasurableSpace Ω}
(X : Ω → β)
{μ : MeasureTheory.Measure Ω}
[TopologicalSpace F]
{f : Ω → F}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
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}
[NormedAddCommGroup F]
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{mΩ : MeasurableSpace Ω}
(X : Ω → β)
{μ : MeasureTheory.Measure Ω}
{f : Ω → F}
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun (x : β × Ω) => f x.2
theorem
ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prod_mk_iff
{β : Type u_2}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{F : Type u_6}
:
∀ {x : MeasurableSpace Ω} [inst : TopologicalSpace F] {X : Ω → β} {μ : MeasureTheory.Measure Ω},
Measurable X →
∀ {f : Ω → F},
MeasureTheory.AEStronglyMeasurable (fun (x : β × Ω) => f x.2)
(MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, ω)) μ) ↔ MeasureTheory.AEStronglyMeasurable f μ
theorem
ProbabilityTheory.integrable_comp_snd_map_prod_mk_iff
{β : Type u_2}
{F : Type u_4}
[NormedAddCommGroup F]
{mβ : MeasurableSpace β}
{Ω : Type u_5}
:
∀ {x : MeasurableSpace Ω} {X : Ω → β} {μ : MeasureTheory.Measure Ω},
Measurable X → ∀ {f : Ω → F}, (MeasureTheory.Integrable fun (x : β × Ω) => f x.2) ↔ MeasureTheory.Integrable f
theorem
ProbabilityTheory.condexp_ae_eq_integral_condDistrib_id
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mβ : MeasurableSpace β}
[NormedSpace ℝ F]
[CompleteSpace F]
{X : Ω → β}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : Measurable X)
{f : Ω → F}
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ f =ᶠ[MeasureTheory.Measure.ae μ] fun (a : Ω) =>
∫ (y : Ω), f y ∂(ProbabilityTheory.condDistrib id X μ) (X a)