condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable

English

If f is strongly measurable and integrable, then almost everywhere on μ.trim hm, condExp and the integral over condExpKernelμ m reproduce f almost everywhere.

Русский

Если f сильно измерима и интегрируема, то почти всюду на μ.trim hm condExp и интеграл по condExpKernel μ m восстанавливают f почти наверняка.

LaTeX

$$$\\text{StronglyMeasurable}(f) \\Rightarrow \\text{ae}_{μ.trim hm}(f)\\Rightarrow \\text{ae}_{μ.trim hm}(f = \\int f d condExpKernel)$$$

Lean4

/-- Auxiliary lemma for `condExp_ae_eq_trim_integral_condExpKernel`. -/
theorem condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable [NormedAddCommGroup F] {f : Ω → F}
    [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ) (hf : StronglyMeasurable f) (hf_int : Integrable f μ) :
    μ[f|m] =ᵐ[μ.trim hm] fun ω ↦ ∫ y, f y ∂condExpKernel μ m ω :=
  by
  refine StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm ?_ ?_ ?_
  · exact stronglyMeasurable_condExp
  · exact hf.integral_condExpKernel
  · exact condExp_ae_eq_integral_condExpKernel hm hf_int

Похожие утверждения