English
Variant of the previous lemma with strengthened conditions; equality holds a.e. under measurable X,Y.
Русский
Вариант предыдущего леммы при усиленных условиях; a.e. равенство сохраняется для измеримых X,Y.
LaTeX
$$$\\text{condDistrib}(X,Y,μ)(Y(a))\,s =^a.e_{μ}\\; (\\text{condExpKernel}(μ,(mγ.comap Y)).map X)(a,s)$$$
Lean4
theorem condExp_ae_eq_integral_condExpKernel' [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F]
(hf_int : Integrable f μ) : μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ y, f y ∂condExpKernel μ m ω :=
by
rcases isEmpty_or_nonempty Ω with h | h
· have : μ = 0 := Measure.eq_zero_of_isEmpty μ
simpa [this] using trivial
have hX : @Measurable Ω Ω mΩ (m ⊓ mΩ) id := measurable_id.mono le_rfl (inf_le_right : m ⊓ mΩ ≤ mΩ)
simp_rw [condExpKernel_apply_eq_condDistrib]
have h := condExp_ae_eq_integral_condDistrib_id hX hf_int
simpa only [MeasurableSpace.comap_id, id_eq] using h
