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 : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [hμm : MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ hm)] {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.SignedMeasure.rnDeriv (MeasureTheory.VectorMeasure.trim (MeasureTheory.Measure.withDensityᵥ μ f) hm) (MeasureTheory.Measure.trim μ hm) =ᶠ[MeasureTheory.Measure.ae μ] 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.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| ∂μ

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) =ᶠ[MeasureTheory.Measure.ae μ] ↑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) =ᶠ[MeasureTheory.Measure.ae μ] 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) =ᶠ[MeasureTheory.Measure.ae μ] 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) =ᶠ[MeasureTheory.Measure.ae μ] 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) =ᶠ[MeasureTheory.Measure.ae μ] f * MeasureTheory.condexp m μ g

Pull-out property of the conditional expectation.