theorem MeasureTheory.toReal_ae_eq_indicator_condExp_of_forall_setLIntegral_eq {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] (hm : m ≤ m0) {g : α → ENNReal} {s : Set α} (hs₀ : MeasurableSet s) (hgm : AEStronglyMeasurable g μ) (hg_int_finite : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫⁻ (a : α) in t, g a ∂μ ≠ ⊤) (hg_eq : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫⁻ (a : α) in t, g a ∂μ = μ (s ∩ t)) : (fun (a : α) => (g a).toReal) =ᶠ[ae μ] μ[s.indicator 1 | m]

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 MeasureTheory.toReal_ae_eq_indicator_condExp_iff_forall_meas_inter_eq {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] {g : α → ENNReal} {s : Set α} : (fun (a : α) => (g a).toReal) =ᶠ[ae μ] μ[s.indicator 1 | m] ↔ ∀ (t : Set α), MeasurableSet t → μ (s ∩ t) = ∫⁻ (a : α) in t, g a ∂μ