Uniqueness of the Lebesgue conditional expectation
theorem
MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite'
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
{f g : α → ENNReal}
(hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ)
(hfm : AEStronglyMeasurable f μ)
(hgm : AEStronglyMeasurable g μ)
: