English
For measurable X, Y, s measurable, the a.e. equality between the kernel-valued map (condDistrib Y X μ)(X a) restricted to s and the conditional expectation conditioned on X of the indicator of Y⁻¹ s holds almost everywhere.
Русский
Для измеримых X, Y и s частично, существует почти полное равенство между condDistrib и условным экспонентом индикатора Y⁻¹ s.
LaTeX
$$$\\bigl( (a \\mapsto (\\operatorname{condDistrib}(Y,X,μ)(X a)).\\mathrm{real}(s)) \\bigr) =^{}_{μ} μ\\llbracket Y^{-1} s \\mid mβ.\\!\\!\\!\\!\\! \\_{\mathsf{comap} X} \\rrbracket.$$$
Lean4
/-- 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 condDistrib_ae_eq_condExp (hX : Measurable X) (hY : Measurable Y) (hs : MeasurableSet s) :
(fun a => (condDistrib Y X μ (X a)).real s) =ᵐ[μ] μ⟦Y ⁻¹' s|mβ.comap X⟧ :=
by
refine ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le ?_ ?_ ?_ ?_
· exact (integrable_const _).indicator (hY hs)
· exact fun t _ _ => (integrable_toReal_condDistrib hX.aemeasurable hs).integrableOn
· intro t ht _
simp_rw [measureReal_def]
rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
(Eventually.of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
integral_indicator_const _ (hY hs), measureReal_restrict_apply (hY hs), smul_eq_mul, mul_one, inter_comm,
setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht, measureReal_def]
· exact (measurable_condDistrib hs).ennreal_toReal.aestronglyMeasurable
