English
For measurable X,Y and s measurable, the a.e. equality holds between condDistrib X Y μ (Y a) s and (condExpKernel μ (mγ.comap Y)).map X a s.
Русский
Для измеримых X,Y и s измеримого, выполняется a.e. равенство между condDistrib X Y μ (Y a) s и (condExpKernel μ (mγ.comap Y)).map X a s.
LaTeX
$$$\\text{condDistrib}(X,Y,μ)(Y(a))\,s =^a.e_{μ}\\; (\\text{condExpKernel}(μ,(mγ^{-1} Y)).map X)(a,s)$$$
Lean4
theorem condDistrib_apply_ae_eq_condExpKernel_map {β γ : Type*} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
[StandardBorelSpace β] [Nonempty β] {X : Ω → β} {Y : Ω → γ} (hX : Measurable X) (hY : Measurable Y) {s : Set β}
(hs : MeasurableSet s) :
(fun a ↦ condDistrib X Y μ (Y a) s) =ᵐ[μ] fun a ↦ (condExpKernel μ (mγ.comap Y)).map X a s :=
by
simp_rw [Kernel.map_apply' _ hX _ hs]
filter_upwards [condDistrib_ae_eq_condExp hY hX (μ := μ) hs,
condExpKernel_ae_eq_condExp hY.comap_le (μ := μ) (hX hs)] with a ha₁ ha₂
rw [← measureReal_eq_measureReal_iff, ha₁, ha₂]
