English
Let s and t be measurable subsets. Then for μ-almost every ω in μ restricted to s, the kernel condExpKernel μ (generateFrom {s}) evaluated at ω and t equals μ[t|s].
Русский
Пусть s и t — измеримые множества. Тогда для μ-почти всех ω в ограничении μ на s верно: condExpKernel μ (generateFrom {s}) ω t = μ[t|s].
LaTeX
$$$\mu\restriction s\{ \omega \mid \condExpKernel \mu (\mathrm{generateFrom}\{s\}) \omega t \neq \mu[t|s] \} = 0$$$
Lean4
theorem condExpKernel_singleton_ae_eq_cond [StandardBorelSpace Ω] (hs : MeasurableSet s) (ht : MeasurableSet t) :
∀ᵐ ω ∂μ.restrict s, condExpKernel μ (generateFrom { s }) ω t = μ[t|s] :=
by
have : (fun ω ↦ (condExpKernel μ (generateFrom { s }) ω).real t) =ᵐ[μ.restrict s] μ⟦t|generateFrom { s }⟧ :=
ae_restrict_le <| condExpKernel_ae_eq_condExp (generateFrom_singleton_le hs) ht
filter_upwards [condExp_set_generateFrom_singleton hs ht, this] with ω hω₁ hω₂
rwa [hω₁, measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂
