Conditional Expectation via Conditional Distribution Kernels #
This file establishes the connection between conditional expectations and regular conditional probability distributions (kernels).
Main results #
condExp_indicator_eq_integral_condDistrib: Conditional expectation of an indicator function can be expressed as integration against the conditional distribution kernel.
Representation lemma: Conditional expectation via conditional distribution #
theorem
condExp_indicator_eq_integral_condDistrib
{Ω : Type u_1}
{Γ : Type u_2}
{E : Type u_3}
[MeasurableSpace Ω]
[MeasurableSpace Γ]
[MeasurableSpace E]
[StandardBorelSpace Ω]
[StandardBorelSpace Γ]
[StandardBorelSpace E]
[Nonempty Ω]
[Nonempty Γ]
[Nonempty E]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(ζ : Ω → Γ)
(hζ : Measurable ζ)
(ξ : Ω → E)
(hξ : Measurable ξ)
(B : Set E)
(hB : MeasurableSet B)
:
μ[(ξ ⁻¹' B).indicator fun (x : Ω) => 1|MeasurableSpace.comap ζ inferInstance] =ᵐ[μ] fun (ω : Ω) =>
∫ (e : E), B.indicator (fun (x : E) => 1) e ∂(ProbabilityTheory.condDistrib ξ ζ μ) (ζ ω)
Conditional expectation of a bounded measurable function composed with a random variable can be expressed as integration against the conditional distribution kernel.
This is the key link between conditional expectation (a measure-theoretic notion) and conditional distribution (a kernel-theoretic notion).