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_set_integral_eq': two Lp functions verifying the equality of integrals defining the conditional expectation are equal.
• ae_eq_of_forall_set_integral_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_set_integral_eq_zero {α : Type u_1} {E' : Type u_2} {𝕜 : Type u_4} {p : ENNReal} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] (hm : m ≤ m0) (f : ↥(MeasureTheory.lpMeas E' 𝕜 m p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑↑f) s) (hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0) : ↑↑↑f =ᶠ[MeasureTheory.Measure.ae μ] 0

theorem MeasureTheory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E' p)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s) (hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0) (hf_meas : MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ) : ↑↑f =ᶠ[MeasureTheory.Measure.ae μ] 0

theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [IsROrC 𝕜] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedSpace ℝ E'] (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E' p)) (g : ↥(MeasureTheory.Lp E' p)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s) (hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑g) s) (hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ) (hf_meas : MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ) (hg_meas : MeasureTheory.AEStronglyMeasurable' m (↑↑g) μ) : ↑↑f =ᶠ[MeasureTheory.Measure.ae μ] ↑↑g

Uniqueness of the conditional expectation

theorem MeasureTheory.ae_eq_of_forall_set_integral_eq_of_sigmaFinite' {α : Type u_1} {F' : Type u_3} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [CompleteSpace F'] (hm : m ≤ m0) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] {f : α → F'} {g : α → F'} (hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn f s) (hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn g s) (hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ) (hfm : MeasureTheory.AEStronglyMeasurable' m f μ) (hgm : MeasureTheory.AEStronglyMeasurable' m g μ) : f =ᶠ[MeasureTheory.Measure.ae μ] g

theorem MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) {f : α → ℝ} {g : α → ℝ} (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.IntegrableOn f s) (hg : MeasureTheory.StronglyMeasurable g) (hgi : MeasureTheory.IntegrableOn g s) (hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) : ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖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_nnnorm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) {f : α → ℝ} {g : α → ℝ} (hf : MeasureTheory.StronglyMeasurable f) (hfi : MeasureTheory.IntegrableOn f s) (hg : MeasureTheory.StronglyMeasurable g) (hgi : MeasureTheory.IntegrableOn g s) (hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ) (hs : MeasurableSet s) (hμs : ↑↑μ s ≠ ⊤) : ∫⁻ (x : α) in s, ↑‖g x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖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.