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_stronglyMeasurable_mul: the pull-out property of the conditional expectation.
theorem
MeasureTheory.rnDeriv_ae_eq_condexp
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{hm : m ≤ m0}
[hμm : MeasureTheory.SigmaFinite (μ.trim hm)]
{f : α → ℝ}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] MeasureTheory.condexp m μ f
theorem
MeasureTheory.snorm_one_condexp_le_snorm
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(f : α → ℝ)
:
MeasureTheory.snorm (MeasureTheory.condexp m μ f) 1 μ ≤ MeasureTheory.snorm f 1 μ
theorem
MeasureTheory.integral_abs_condexp_le
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(f : α → ℝ)
:
∫ (x : α), |MeasureTheory.condexp m μ f x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
theorem
MeasureTheory.setIntegral_abs_condexp_le
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(f : α → ℝ)
:
∫ (x : α) in s, |MeasureTheory.condexp m μ f x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
@[deprecated MeasureTheory.setIntegral_abs_condexp_le]
theorem
MeasureTheory.set_integral_abs_condexp_le
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(f : α → ℝ)
:
∫ (x : α) in s, |MeasureTheory.condexp m μ f x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
Alias of MeasureTheory.setIntegral_abs_condexp_le.
theorem
MeasureTheory.ae_bdd_condexp_of_ae_bdd
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{R : NNReal}
{f : α → ℝ}
(hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R)
:
∀ᵐ (x : α) ∂μ, |MeasureTheory.condexp m μ f x| ≤ ↑R
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 α}
{μ : MeasureTheory.Measure α}
{ι : Type u_2}
[MeasureTheory.IsFiniteMeasure μ]
{g : α → ℝ}
(hint : MeasureTheory.Integrable g μ)
{ℱ : ι → MeasurableSpace α}
(hℱ : ∀ (i : ι), ℱ i ≤ m0)
:
MeasureTheory.UniformIntegrable (fun (i : ι) => MeasureTheory.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.
theorem
MeasureTheory.condexp_stronglyMeasurable_simpleFunc_mul
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : MeasureTheory.SimpleFunc α ℝ)
{g : α → ℝ}
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.condexp m μ (↑f * g) =ᵐ[μ] ↑f * MeasureTheory.condexp m μ g
Auxiliary lemma for condexp_stronglyMeasurable_mul.
theorem
MeasureTheory.condexp_stronglyMeasurable_mul_of_bound
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
{f : α → ℝ}
{g : α → ℝ}
(hf : MeasureTheory.StronglyMeasurable f)
(hg : MeasureTheory.Integrable g μ)
(c : ℝ)
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c)
:
MeasureTheory.condexp m μ (f * g) =ᵐ[μ] f * MeasureTheory.condexp m μ g
theorem
MeasureTheory.condexp_stronglyMeasurable_mul_of_bound₀
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
{f : α → ℝ}
{g : α → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
(hg : MeasureTheory.Integrable g μ)
(c : ℝ)
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c)
:
MeasureTheory.condexp m μ (f * g) =ᵐ[μ] f * MeasureTheory.condexp m μ g
theorem
MeasureTheory.condexp_stronglyMeasurable_mul
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{g : α → ℝ}
(hf : MeasureTheory.StronglyMeasurable f)
(hfg : MeasureTheory.Integrable (f * g) μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.condexp m μ (f * g) =ᵐ[μ] f * MeasureTheory.condexp m μ g
Pull-out property of the conditional expectation.
theorem
MeasureTheory.condexp_stronglyMeasurable_mul₀
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{g : α → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
(hfg : MeasureTheory.Integrable (f * g) μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.condexp m μ (f * g) =ᵐ[μ] f * MeasureTheory.condexp m μ g
Pull-out property of the conditional expectation.