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': twoLpfunctions 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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[RCLike 𝕜]
[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
@[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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[RCLike 𝕜]
[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
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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[RCLike 𝕜]
[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
@[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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[RCLike 𝕜]
[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
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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[RCLike 𝕜]
[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
@[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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[RCLike 𝕜]
[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
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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
(hm : m ≤ m0)
[MeasureTheory.SigmaFinite (μ.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 μ)
:
@[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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
[CompleteSpace F']
(hm : m ≤ m0)
[MeasureTheory.SigmaFinite (μ.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 μ)
:
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 : 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 ≠ ⊤)
:
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 ≠ ⊤)
:
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.