Documentation

Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Conditional expectation of real-valued functions #

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

Main results #

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) =ᶠ[μ.ae] MeasureTheory.condexp m μ f
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_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) :
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) :

Pull-out property of the conditional expectation.

Pull-out property of the conditional expectation.