Uniqueness of the conditional expectation

Two Lp functions f, g which are almost everywhere strongly measurable with respect to a σ-algebra m and verify ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ for all m-measurable sets s are equal almost everywhere. This proves the uniqueness of the conditional expectation, which is not yet defined in this file but is introduced in Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic.

Main statements

• Lp.ae_eq_of_forall_setIntegral_eq': two Lp functions verifying the equality of integrals defining the conditional expectation are equal.
• ae_eq_of_forall_setIntegral_eq_of_sigma_finite': two functions verifying the equality of integrals defining the conditional expectation are equal almost everywhere. Requires [SigmaFinite (μ.trim hm)].

Uniqueness of the conditional expectation

theorem MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero {α : Type u_1} {E' : Type u_2} {𝕜 : Type u_4} {p : ENNReal} {m m0 : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace Real E'] (hm : LE.le m m0) (f : Subtype fun (x : Subtype fun (x : AEEqFun α E' μ) => Membership.mem (Lp E' p μ) x) => Membership.mem (lpMeas E' 𝕜 m p μ) x) (hp_ne_zero : Ne p 0) (hp_ne_top : Ne p Top.top) (hf_int_finite : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → IntegrableOn f.val.val.cast s μ) (hf_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → Eq (integral (μ.restrict s) fun (x : α) => f.val.val.cast x) 0) : (ae μ).EventuallyEq f.val.val.cast 0

theorem MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m m0 : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace Real E'] (hm : LE.le m m0) (f : Subtype fun (x : AEEqFun α E' μ) => Membership.mem (Lp E' p μ) x) (hp_ne_zero : Ne p 0) (hp_ne_top : Ne p Top.top) (hf_int_finite : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → IntegrableOn f.val.cast s μ) (hf_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → Eq (integral (μ.restrict s) fun (x : α) => f.val.cast x) 0) (hf_meas : AEStronglyMeasurable f.val.cast μ) : (ae μ).EventuallyEq f.val.cast 0

theorem MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m m0 : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace Real E'] (hm : LE.le m m0) (f g : Subtype fun (x : AEEqFun α E' μ) => Membership.mem (Lp E' p μ) x) (hp_ne_zero : Ne p 0) (hp_ne_top : Ne p Top.top) (hf_int_finite : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → IntegrableOn f.val.cast s μ) (hg_int_finite : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → IntegrableOn g.val.cast s μ) (hfg : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → Eq (integral (μ.restrict s) fun (x : α) => f.val.cast x) (integral (μ.restrict s) fun (x : α) => g.val.cast x)) (hf_meas : AEStronglyMeasurable f.val.cast μ) (hg_meas : AEStronglyMeasurable g.val.cast μ) : (ae μ).EventuallyEq f.val.cast g.val.cast

Uniqueness of the conditional expectation

theorem MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' {α : Type u_1} {F' : Type u_3} {m m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup F'] [NormedSpace Real F'] [CompleteSpace F'] (hm : LE.le m m0) [SigmaFinite (μ.trim hm)] {f g : α → F'} (hf_int_finite : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → IntegrableOn f s μ) (hg_int_finite : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → IntegrableOn g s μ) (hfg_eq : ∀ (s : Set α), MeasurableSet s → LT.lt (DFunLike.coe μ s) Top.top → Eq (integral (μ.restrict s) fun (x : α) => f x) (integral (μ.restrict s) fun (x : α) => g x)) (hfm : AEStronglyMeasurable f μ) (hgm : AEStronglyMeasurable g μ) : (ae μ).EventuallyEq f g

theorem MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : LE.le m m0) {f g : α → Real} (hf : StronglyMeasurable f) (hfi : IntegrableOn f s μ) (hg : StronglyMeasurable g) (hgi : IntegrableOn g s μ) (hgf : ∀ (t : Set α), MeasurableSet t → LT.lt (DFunLike.coe μ t) Top.top → Eq (integral (μ.restrict t) fun (x : α) => g x) (integral (μ.restrict t) fun (x : α) => f x)) (hs : MeasurableSet s) (hμs : Ne (DFunLike.coe μ s) Top.top) : LE.le (integral (μ.restrict s) fun (x : α) => Norm.norm (g x)) (integral (μ.restrict s) fun (x : α) => Norm.norm (f x))

Let m be a sub-σ-algebra of m0, f an m0-measurable function and g an m-measurable function, such that their integrals coincide on m-measurable sets with finite measure. Then ∫ x in s, ‖g x‖ ∂μ ≤ ∫ x in s, ‖f x‖ ∂μ on all m-measurable sets with finite measure.

theorem MeasureTheory.lintegral_enorm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : LE.le m m0) {f g : α → Real} (hf : StronglyMeasurable f) (hfi : IntegrableOn f s μ) (hg : StronglyMeasurable g) (hgi : IntegrableOn g s μ) (hgf : ∀ (t : Set α), MeasurableSet t → LT.lt (DFunLike.coe μ t) Top.top → Eq (integral (μ.restrict t) fun (x : α) => g x) (integral (μ.restrict t) fun (x : α) => f x)) (hs : MeasurableSet s) (hμs : Ne (DFunLike.coe μ s) Top.top) : LE.le (lintegral (μ.restrict s) fun (x : α) => ENorm.enorm (g x)) (lintegral (μ.restrict s) fun (x : α) => ENorm.enorm (f x))

Let m be a sub-σ-algebra of m0, f an m0-measurable function and g an m-measurable function, such that their integrals coincide on m-measurable sets with finite measure. Then ∫⁻ x in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ x in s, ‖f x‖ₑ ∂μ on all m-measurable sets with finite measure.

@[deprecated MeasureTheory.lintegral_enorm_le_of_forall_fin_meas_integral_eq (since := "2025-01-21")]

theorem MeasureTheory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : LE.le m m0) {f g : α → Real} (hf : StronglyMeasurable f) (hfi : IntegrableOn f s μ) (hg : StronglyMeasurable g) (hgi : IntegrableOn g s μ) (hgf : ∀ (t : Set α), MeasurableSet t → LT.lt (DFunLike.coe μ t) Top.top → Eq (integral (μ.restrict t) fun (x : α) => g x) (integral (μ.restrict t) fun (x : α) => f x)) (hs : MeasurableSet s) (hμs : Ne (DFunLike.coe μ s) Top.top) : LE.le (lintegral (μ.restrict s) fun (x : α) => ENorm.enorm (g x)) (lintegral (μ.restrict s) fun (x : α) => ENorm.enorm (f x))

Alias of MeasureTheory.lintegral_enorm_le_of_forall_fin_meas_integral_eq.

---

Let m be a sub-σ-algebra of m0, f an m0-measurable function and g an m-measurable function, such that their integrals coincide on m-measurable sets with finite measure. Then ∫⁻ x in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ x in s, ‖f x‖ₑ ∂μ on all m-measurable sets with finite measure.