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_stronglyMeasurable_mul: the pull-out property of the conditional expectation.
theorem MeasureTheory.rnDeriv_ae_eq_condexp {α : Type u_1} {m : } {m0 : } {μ : } {hm : m m0} [hμm : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α} (hf : ) :
MeasureTheory.SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᶠ[μ.ae]
theorem MeasureTheory.snorm_one_condexp_le_snorm {α : Type u_1} {m : } {m0 : } {μ : } (f : α) :
theorem MeasureTheory.integral_abs_condexp_le {α : Type u_1} {m : } {m0 : } {μ : } (f : α) :
∫ (x : α), ||μ ∫ (x : α), |f x|μ
theorem MeasureTheory.setIntegral_abs_condexp_le {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hs : ) (f : α) :
∫ (x : α) in s, ||μ ∫ (x : α) in s, |f x|μ
@[deprecated MeasureTheory.setIntegral_abs_condexp_le]
theorem MeasureTheory.set_integral_abs_condexp_le {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hs : ) (f : α) :
∫ (x : α) in s, ||μ ∫ (x : α) in s, |f x|μ

Alias of MeasureTheory.setIntegral_abs_condexp_le.

theorem MeasureTheory.ae_bdd_condexp_of_ae_bdd {α : Type u_1} {m : } {m0 : } {μ : } {R : NNReal} {f : α} (hbdd : ∀ᵐ (x : α) ∂μ, |f x| R) :
∀ᵐ (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 : } {μ : } {ι : Type u_2} {g : α} (hint : ) {ℱ : ι} (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 : } {m0 : } {μ : } (hm : m m0) (f : ) {g : α} (hg : ) :
MeasureTheory.condexp m μ (f * g) =ᶠ[μ.ae] f *

Auxiliary lemma for condexp_stronglyMeasurable_mul.

theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) {f : α} {g : α} (hf : ) (hg : ) (c : ) (hf_bound : ∀ᵐ (x : α) ∂μ, f x c) :
MeasureTheory.condexp m μ (f * g) =ᶠ[μ.ae] f *
theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound₀ {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) {f : α} {g : α} (hf : ) (hg : ) (c : ) (hf_bound : ∀ᵐ (x : α) ∂μ, f x c) :
MeasureTheory.condexp m μ (f * g) =ᶠ[μ.ae] f *
theorem MeasureTheory.condexp_stronglyMeasurable_mul {α : Type u_1} {m : } {m0 : } {μ : } {f : α} {g : α} (hf : ) (hfg : MeasureTheory.Integrable (f * g) μ) (hg : ) :
MeasureTheory.condexp m μ (f * g) =ᶠ[μ.ae] f *

Pull-out property of the conditional expectation.

theorem MeasureTheory.condexp_stronglyMeasurable_mul₀ {α : Type u_1} {m : } {m0 : } {μ : } {f : α} {g : α} (hf : ) (hfg : MeasureTheory.Integrable (f * g) μ) (hg : ) :
MeasureTheory.condexp m μ (f * g) =ᶠ[μ.ae] f *

Pull-out property of the conditional expectation.