# 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 : } {μ : } [] [] [] [] [] (hm : m m0) (f : (MeasureTheory.lpMeas E' 𝕜 m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (f) s μ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0
@[deprecated MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero]
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 : } {m0 : } {μ : } [] [] [] [] [] (hm : m m0) (f : (MeasureTheory.lpMeas E' 𝕜 m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (f) s μ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) :
f =ᵐ[μ] 0

Alias of MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero.

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 : } {μ : } [] [] [] [] [] (hm : m m0) (f : (MeasureTheory.Lp E' p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (f) s μ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) (hf_meas : ) :
f =ᵐ[μ] 0
@[deprecated MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero']
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 : } {m0 : } {μ : } [] [] [] [] [] (hm : m m0) (f : (MeasureTheory.Lp E' p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (f) s μ) (hf_zero : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = 0) (hf_meas : ) :
f =ᵐ[μ] 0

Alias of MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero'.

theorem MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m : } {m0 : } {μ : } [] [] [] [] [] (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 α), μ s < MeasureTheory.IntegrableOn (f) s μ) (hg_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (g) s μ) (hfg : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) (hf_meas : ) (hg_meas : ) :
f =ᵐ[μ] g

Uniqueness of the conditional expectation

@[deprecated MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq']
theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ENNReal} {m : } {m0 : } {μ : } [] [] [] [] [] (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 α), μ s < MeasureTheory.IntegrableOn (f) s μ) (hg_int_finite : ∀ (s : Set α), μ s < MeasureTheory.IntegrableOn (g) s μ) (hfg : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) (hf_meas : ) (hg_meas : ) :
f =ᵐ[μ] g

Alias of MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq'.

Uniqueness of the conditional expectation

theorem MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' {α : Type u_1} {F' : Type u_3} {m : } {m0 : } {μ : } [] [] [] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {g : αF'} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_eq : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) (hfm : ) (hgm : ) :
f =ᵐ[μ] g
@[deprecated MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite']
theorem MeasureTheory.ae_eq_of_forall_set_integral_eq_of_sigmaFinite' {α : Type u_1} {F' : Type u_3} {m : } {m0 : } {μ : } [] [] [] (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] {f : αF'} {g : αF'} (hf_int_finite : ∀ (s : Set α), μ s < ) (hg_int_finite : ∀ (s : Set α), μ s < ) (hfg_eq : ∀ (s : Set α), μ s < ∫ (x : α) in s, f xμ = ∫ (x : α) in s, g xμ) (hfm : ) (hgm : ) :
f =ᵐ[μ] g

Alias of MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'.

theorem MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) {f : α} {g : α} (hf : ) (hfi : ) (hg : ) (hgi : ) (hgf : ∀ (t : Set α), μ t < ∫ (x : α) in t, g xμ = ∫ (x : α) in t, f xμ) (hs : ) (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 : } {m0 : } {μ : } {s : Set α} (hm : m m0) {f : α} {g : α} (hf : ) (hfi : ) (hg : ) (hgi : ) (hgf : ∀ (t : Set α), μ t < ∫ (x : α) in t, g xμ = ∫ (x : α) in t, f xμ) (hs : ) (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.