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 offμrestricted onmwith respect toμrestricted onm.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 μ)
:
@[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 μ)
:
Alias of MeasureTheory.rnDeriv_ae_eq_condExp.
@[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 : α → ℝ)
:
Alias of MeasureTheory.setIntegral_abs_condExp_le.
@[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)
:
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.
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 : ι) => μ[g|ℱ i]) 1 μ
Given an integrable function g, the conditional expectations of g with respect to
a sequence of sub-σ-algebras is uniformly integrable.
theorem
MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : SimpleFunc α ℝ)
{g : α → ℝ}
(hg : Integrable g μ)
:
Auxiliary lemma for condExp_mul_of_stronglyMeasurable_left.
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)
:
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 μ)
:
Pull-out property of the conditional expectation.
theorem
MeasureTheory.condExp_mul_of_stronglyMeasurable_right
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → ℝ}
(hg : StronglyMeasurable g)
(hfg : Integrable (f * g) μ)
(hf : Integrable f μ)
:
Pull-out property of the conditional expectation.
theorem
MeasureTheory.condExp_mul_of_aestronglyMeasurable_left
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → ℝ}
(hf : AEStronglyMeasurable f μ)
(hfg : Integrable (f * g) μ)
(hg : Integrable g μ)
:
Pull-out property of the conditional expectation.
theorem
MeasureTheory.condExp_mul_of_aestronglyMeasurable_right
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → ℝ}
(hg : AEStronglyMeasurable g μ)
(hfg : Integrable (f * g) μ)
(hf : Integrable f μ)
:
Pull-out property of the conditional expectation.