Conditional expectation of real-valued functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves some results regarding the conditional expectation of real-valued functions.
Main results #
measure_theory.rn_deriv_ae_eq_condexp: the conditional expectationμ[f | m]is equal to the Radon-Nikodym derivative offμrestricted onmwith respect toμrestricted onm.measure_theory.integrable.uniform_integrable_condexp: the conditional expectation of a function form a uniformly integrable class.measure_theory.condexp_strongly_measurable_mul: the pull-out property of the conditional expectation.
theorem
measure_theory.rn_deriv_ae_eq_condexp
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[hμm : measure_theory.sigma_finite (μ.trim hm)]
{f : α → ℝ}
(hf : measure_theory.integrable f μ) :
measure_theory.signed_measure.rn_deriv ((μ.with_densityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] measure_theory.condexp m μ f
theorem
measure_theory.snorm_one_condexp_le_snorm
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(f : α → ℝ) :
measure_theory.snorm (measure_theory.condexp m μ f) 1 μ ≤ measure_theory.snorm f 1 μ
theorem
measure_theory.integral_abs_condexp_le
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(f : α → ℝ) :
theorem
measure_theory.set_integral_abs_condexp_le
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(f : α → ℝ) :
theorem
measure_theory.ae_bdd_condexp_of_ae_bdd
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{R : nnreal}
{f : α → ℝ}
(hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R) :
If the real valued function f is bounded almost everywhere by R, then so is its conditional
expectation.
theorem
measure_theory.integrable.uniform_integrable_condexp
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{ι : Type u_2}
[measure_theory.is_finite_measure μ]
{g : α → ℝ}
(hint : measure_theory.integrable g μ)
{ℱ : ι → measurable_space α}
(hℱ : ∀ (i : ι), ℱ i ≤ m0) :
measure_theory.uniform_integrable (λ (i : ι), measure_theory.condexp (ℱ i) μ g) 1 μ
Given a integrable function g, the conditional expectations of g with respect to
a sequence of sub-σ-algebras is uniformly integrable.
theorem
measure_theory.condexp_strongly_measurable_simple_func_mul
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : measure_theory.simple_func α ℝ)
{g : α → ℝ}
(hg : measure_theory.integrable g μ) :
measure_theory.condexp m μ (⇑f * g) =ᵐ[μ] ⇑f * measure_theory.condexp m μ g
Auxiliary lemma for condexp_measurable_mul.
theorem
measure_theory.condexp_strongly_measurable_mul_of_bound
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.is_finite_measure μ]
{f g : α → ℝ}
(hf : measure_theory.strongly_measurable f)
(hg : measure_theory.integrable g μ)
(c : ℝ)
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :
measure_theory.condexp m μ (f * g) =ᵐ[μ] f * measure_theory.condexp m μ g
theorem
measure_theory.condexp_strongly_measurable_mul_of_bound₀
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.is_finite_measure μ]
{f g : α → ℝ}
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hg : measure_theory.integrable g μ)
(c : ℝ)
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :
measure_theory.condexp m μ (f * g) =ᵐ[μ] f * measure_theory.condexp m μ g
theorem
measure_theory.condexp_strongly_measurable_mul
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ}
(hf : measure_theory.strongly_measurable f)
(hfg : measure_theory.integrable (f * g) μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp m μ (f * g) =ᵐ[μ] f * measure_theory.condexp m μ g
Pull-out property of the conditional expectation.
theorem
measure_theory.condexp_strongly_measurable_mul₀
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → ℝ}
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hfg : measure_theory.integrable (f * g) μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp m μ (f * g) =ᵐ[μ] f * measure_theory.condexp m μ g
Pull-out property of the conditional expectation.