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': twoLpfunctions 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 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas E' 𝕜 m p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑f s μ)
(hf_zero : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, ⇑f x ∂μ = 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 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E' p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑f s μ)
(hf_zero : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, ⇑f x ∂μ = 0)
(hf_meas : measure_theory.ae_strongly_measurable' m ⇑f μ) :
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 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp E' p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑f s μ)
(hg_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑g s μ)
(hfg : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, ⇑f x ∂μ = ∫ (x : α) in s, ⇑g x ∂μ)
(hf_meas : measure_theory.ae_strongly_measurable' m ⇑f μ)
(hg_meas : measure_theory.ae_strongly_measurable' m ⇑g μ) :
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 α}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
{f g : α → F'}
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on f s μ)
(hg_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on g s μ)
(hfg_eq : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ)
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hgm : measure_theory.ae_strongly_measurable' m 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 : α → ℝ}
(hf : measure_theory.strongly_measurable f)
(hfi : measure_theory.integrable_on f s μ)
(hg : measure_theory.strongly_measurable g)
(hgi : measure_theory.integrable_on g s μ)
(hgf : ∀ (t : set α), measurable_set t → ⇑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
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 : α → ℝ}
(hf : measure_theory.strongly_measurable f)
(hfi : measure_theory.integrable_on f s μ)
(hg : measure_theory.strongly_measurable g)
(hgi : measure_theory.integrable_on g s μ)
(hgf : ∀ (t : set α), measurable_set t → ⇑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
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.