English
For hm, every measurable f integrable with μ is a.e. equal to its condExp integrated against condExpKernel.
Русский
Для hm любая интегрируемая f удовлетворяет a.e. равенству condExp μ f равно интегралу по condExpKernel.
LaTeX
$$$\\text{ae}_{m} (f) = \\int f(y) d condExpKernel(μ,m) $ a.e.$$
Lean4
/-- The conditional expectation of `f` with respect to a σ-algebra `m` is
(`μ.trim hm`)-almost everywhere equal to the integral `∫ y, f y ∂(condExpKernel μ m ω)`. -/
theorem condExp_ae_eq_trim_integral_condExpKernel [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F]
(hm : m ≤ mΩ) (hf_int : Integrable f μ) : μ[f|m] =ᵐ[μ.trim hm] fun ω ↦ ∫ y, f y ∂condExpKernel μ m ω :=
by
refine (condExp_congr_ae_trim hm hf_int.1.ae_eq_mk).trans ?_
refine (condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable hm hf_int.1.stronglyMeasurable_mk ?_).trans ?_
· rwa [integrable_congr hf_int.1.ae_eq_mk.symm]
filter_upwards [aestronglyMeasurable_trim_condExpKernel hm hf_int.1] with ω hω
rw [integral_congr_ae hω]
