# mathlib3documentation

measure_theory.function.conditional_expectation.unique

# Uniqueness of the conditional expectation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 measure_theory.function.conditional_expectation.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 [sigma_finite (μ.trim hm)].

## Uniqueness of the conditional expectation #

theorem measure_theory.Lp_meas.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E' : Type u_2} {𝕜 : Type u_4} {p : ennreal} {m m0 : measurable_space α} {μ : measure_theory.measure α} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ E'] (hm : m m0) (f : m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : (s : set α), μ s < ) (hf_zero : (s : set α), μ s < (x : α) in s, f x μ = 0) :
f =ᵐ[μ] 0
theorem measure_theory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ennreal} {m m0 : measurable_space α} {μ : measure_theory.measure α} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ E'] (hm : m m0) (f : p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : (s : set α), μ s < ) (hf_zero : (s : set α), μ s < (x : α) in s, f x μ = 0) (hf_meas : μ) :
f =ᵐ[μ] 0
theorem measure_theory.Lp.ae_eq_of_forall_set_integral_eq' {α : Type u_1} {E' : Type u_2} (𝕜 : Type u_4) {p : ennreal} {m m0 : measurable_space α} {μ : measure_theory.measure α} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ E'] (hm : m m0) (f g : p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : (s : set α), μ s < ) (hg_int_finite : (s : set α), μ s < ) (hfg : (s : set α), μ s < (x : α) in s, f x μ = (x : α) in s, g x μ) (hf_meas : μ) (hg_meas : μ) :

Uniqueness of the conditional expectation

theorem measure_theory.ae_eq_of_forall_set_integral_eq_of_sigma_finite' {α : Type u_1} {F' : Type u_3} {m m0 : measurable_space α} {μ : measure_theory.measure α} [ F'] [complete_space F'] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] {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
theorem measure_theory.integral_norm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) {f g : α } (hfi : μ) (hgi : μ) (hgf : (t : set α), μ t < (x : α) in t, g x μ = (x : α) in t, f x μ) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, g x μ (x : α) in s, f x μ

Let m be a sub-σ-algebra of m0, f a m0-measurable function and g a 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 measure_theory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) {f g : α } (hfi : μ) (hgi : μ) (hgf : (t : set α), μ t < (x : α) in t, g x μ = (x : α) in t, f x μ) (hs : measurable_set s) (hμs : μ s ) :
∫⁻ (x : α) in s, g x‖₊ μ ∫⁻ (x : α) in s, f x‖₊ μ

Let m be a sub-σ-algebra of m0, f a m0-measurable function and g a 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.