Conditional expectation of real-valued functions #

This file proves some results regarding the conditional expectation of real-valued functions.

Main results #

MeasureTheory.rnDeriv_ae_eq_condExp: the conditional expectation μ[f | m] is equal to the Radon-Nikodym derivative of fμ restricted on m with respect to μ restricted on m.
MeasureTheory.Integrable.uniformIntegrable_condExp: the conditional expectation of a function form a uniformly integrable class.
MeasureTheory.condExp_mul_of_stronglyMeasurable_left: the pull-out property of the conditional expectation.

theorem MeasureTheory.rnDeriv_ae_eq_condExp {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [hμm : SigmaFinite (μ.trim hm)] {f : α → ℝ} (hf : Integrable f μ) :

SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᶠ[ae μ] condExp m μ f

source

@[deprecated MeasureTheory.rnDeriv_ae_eq_condExp (since := "2025-01-21")]

theorem MeasureTheory.rnDeriv_ae_eq_condexp {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [hμm : SigmaFinite (μ.trim hm)] {f : α → ℝ} (hf : Integrable f μ) :

SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᶠ[ae μ] condExp m μ f

Alias of MeasureTheory.rnDeriv_ae_eq_condExp.

source

theorem MeasureTheory.eLpNorm_one_condExp_le_eLpNorm {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (f : α → ℝ) :

eLpNorm (condExp m μ f) 1 μ ≤ eLpNorm f 1 μ

source

@[deprecated MeasureTheory.eLpNorm_one_condExp_le_eLpNorm (since := "2025-01-21")]

theorem MeasureTheory.eLpNorm_one_condexp_le_eLpNorm {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (f : α → ℝ) :

eLpNorm (condExp m μ f) 1 μ ≤ eLpNorm f 1 μ

Alias of MeasureTheory.eLpNorm_one_condExp_le_eLpNorm.

source

theorem MeasureTheory.integral_abs_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (f : α → ℝ) :

∫ (x : α), |condExp m μ f x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

source

@[deprecated MeasureTheory.integral_abs_condExp_le (since := "2025-01-21")]

theorem MeasureTheory.integral_abs_condexp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (f : α → ℝ) :

∫ (x : α), |condExp m μ f x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Alias of MeasureTheory.integral_abs_condExp_le.

source

theorem MeasureTheory.setIntegral_abs_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ℝ) :

∫ (x : α) in s, |condExp m μ f x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

source

@[deprecated MeasureTheory.setIntegral_abs_condExp_le (since := "2025-01-21")]

theorem MeasureTheory.setIntegral_abs_condexp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ℝ) :

∫ (x : α) in s, |condExp m μ f x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Alias of MeasureTheory.setIntegral_abs_condExp_le.

source

theorem MeasureTheory.ae_bdd_condExp_of_ae_bdd {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {R : NNReal} {f : α → ℝ} (hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R) :

∀ᵐ (x : α) ∂μ, |condExp m μ f x| ≤ ↑R

If the real valued function f is bounded almost everywhere by R, then so is its conditional expectation.

source

@[deprecated MeasureTheory.ae_bdd_condExp_of_ae_bdd (since := "2025-01-21")]

theorem MeasureTheory.ae_bdd_condexp_of_ae_bdd {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {R : NNReal} {f : α → ℝ} (hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R) :

∀ᵐ (x : α) ∂μ, |condExp m μ f x| ≤ ↑R

Alias of MeasureTheory.ae_bdd_condExp_of_ae_bdd.

If the real valued function f is bounded almost everywhere by R, then so is its conditional expectation.

source

theorem MeasureTheory.Integrable.uniformIntegrable_condExp {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ι : Type u_2} [IsFiniteMeasure μ] {g : α → ℝ} (hint : Integrable g μ) {ℱ : ι → MeasurableSpace α} (hℱ : ∀ (i : ι), ℱ i ≤ m0) :

UniformIntegrable (fun (i : ι) => condExp (ℱ i) μ g) 1 μ

Given an integrable function g, the conditional expectations of g with respect to a sequence of sub-σ-algebras is uniformly integrable.

source

@[deprecated MeasureTheory.Integrable.uniformIntegrable_condExp (since := "2025-01-21")]

theorem MeasureTheory.Integrable.uniformIntegrable_condexp {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {ι : Type u_2} [IsFiniteMeasure μ] {g : α → ℝ} (hint : Integrable g μ) {ℱ : ι → MeasurableSpace α} (hℱ : ∀ (i : ι), ℱ i ≤ m0) :

UniformIntegrable (fun (i : ι) => condExp (ℱ i) μ g) 1 μ

Alias of MeasureTheory.Integrable.uniformIntegrable_condExp.

Given an integrable function g, the conditional expectations of g with respect to a sequence of sub-σ-algebras is uniformly integrable.

source

theorem MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f : SimpleFunc α ℝ) {g : α → ℝ} (hg : Integrable g μ) :

condExp m μ (⇑f * g) =ᶠ[ae μ] ⇑f * condExp m μ g

Auxiliary lemma for condExp_mul_of_stronglyMeasurable_left.

source

@[deprecated MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul (since := "2025-01-21")]

theorem MeasureTheory.condexp_stronglyMeasurable_simpleFunc_mul {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (f : SimpleFunc α ℝ) {g : α → ℝ} (hg : Integrable g μ) :

condExp m μ (⇑f * g) =ᶠ[ae μ] ⇑f * condExp m μ g

Alias of MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul.

Auxiliary lemma for condExp_mul_of_stronglyMeasurable_left.

source

theorem MeasureTheory.condExp_stronglyMeasurable_mul_of_bound {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ} (hf : StronglyMeasurable f) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :

condExp m μ (f * g) =ᶠ[ae μ] f * condExp m μ g

source

@[deprecated MeasureTheory.condExp_stronglyMeasurable_mul_of_bound (since := "2025-01-21")]

theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ} (hf : StronglyMeasurable f) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :

condExp m μ (f * g) =ᶠ[ae μ] f * condExp m μ g

Alias of MeasureTheory.condExp_stronglyMeasurable_mul_of_bound.

source

theorem MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ} (hf : AEStronglyMeasurable f μ) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :

condExp m μ (f * g) =ᶠ[ae μ] f * condExp m μ g

source

@[deprecated MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀ (since := "2025-01-21")]

theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound₀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ} (hf : AEStronglyMeasurable f μ) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :

condExp m μ (f * g) =ᶠ[ae μ] f * condExp m μ g

Alias of MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀.

source

theorem MeasureTheory.condExp_mul_of_stronglyMeasurable_left {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {f g : α → ℝ} (hf : StronglyMeasurable f) (hfg : Integrable (f * g) μ) (hg : Integrable g μ) :

condExp m μ (f * g) =ᶠ[ae μ] f * condExp m μ g