English
If hm ≤ m0 and there are appropriate integrability conditions and equalities of integrals on all sets, then g equals μ[f|m] almost everywhere.
Русский
При условиях интегрируемости и равенстве интегралов на всех m-измеримых множествах, g равен μ[f|m] почти наверняка.
LaTeX
$$$$g =_{\\text{ae}} μ[f|m] \\quad\\text{given the set-integral equalities.}$$$$
Lean4
/-- **Uniqueness of the conditional expectation**
If a function is a.e. `m`-measurable, verifies an integrability condition and has same integral
as `f` on all `m`-measurable sets, then it is a.e. equal to `μ[f|hm]`. -/
theorem ae_eq_condExp_of_forall_setIntegral_eq (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] {f g : α → E}
(hf : Integrable f μ) (hg_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn g s μ)
(hg_eq : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, g x ∂μ = ∫ x in s, f x ∂μ)
(hgm : AEStronglyMeasurable[m] g μ) : g =ᵐ[μ] μ[f|m] :=
by
refine
ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm hg_int_finite (fun s _ _ => integrable_condExp.integrableOn)
(fun s hs hμs => ?_) hgm (StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_condExp)
rw [hg_eq s hs hμs, setIntegral_condExp hm hf hs]
