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 μ] μ[f|m]

theorem MeasureTheory.eLpNorm_one_condExp_le_eLpNorm {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (f : α → ℝ) : eLpNorm μ[f|m] 1 μ ≤ eLpNorm f 1 μ

theorem MeasureTheory.integral_abs_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (f : α → ℝ) : ∫ (x : α), |μ[f|m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

theorem MeasureTheory.setIntegral_abs_condExp_le {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ℝ) : ∫ (x : α) in s, |μ[f|m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

theorem MeasureTheory.ae_bdd_condExp_of_ae_bdd {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {R : NNReal} {f : α → ℝ} (hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R) : ∀ᵐ (x : α) ∂μ, |μ[f|m] 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 α} {μ : 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 μ) : μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]

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 : StronglyMeasurable f) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

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) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

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 μ) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

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 μ) : μ[f * g|m] =ᶠ[ae μ] μ[f|m] * g

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 μ) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

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 μ) : μ[f * g|m] =ᶠ[ae μ] μ[f|m] * g

Pull-out property of the conditional expectation.