English
For measurable s, the a.e. equality of the ω-realisation of condExpKernel on s with condExp is obtained after restricting to the infimum m ⊓ mΩ.
Русский
Для измеримого s a.e. равенство condExpKernel(ω).real s и condExp(mΩ ∧ m)(μ, s.indicator) достигается после ограничения до infimum m ⊓ mΩ.
LaTeX
$$$(condExpKernel_{\\mu,m})_{\\omega}.real(s) =^a.e_{μ} μ⟦s|m\\land mΩ\\ ба⟧$$$
Lean4
theorem condExpKernel_ae_eq_condExp' {s : Set Ω} (hs : MeasurableSet s) :
(fun ω ↦ (condExpKernel μ m ω).real s) =ᵐ[μ] μ⟦s|m ⊓ mΩ⟧ :=
by
rcases isEmpty_or_nonempty Ω with h | h
· have : μ = 0 := Measure.eq_zero_of_isEmpty μ
simpa [this] using trivial
have h := condDistrib_ae_eq_condExp (μ := μ) (measurable_id'' (inf_le_right : m ⊓ mΩ ≤ mΩ)) measurable_id hs
simp only [id_eq, MeasurableSpace.comap_id, preimage_id_eq] at h
simp_rw [condExpKernel_apply_eq_condDistrib]
exact h
