mathlib documentation

measure_theory.function.conditional_expectation.real

Conditional expectation of real-valued functions #

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

Main results #

theorem measure_theory.integral_abs_condexp_le {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : α → ) :
(x : α), |measure_theory.condexp m μ f x| μ (x : α), |f x| μ
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 : α → ) :
(x : α) in s, |measure_theory.condexp m μ f x| μ (x : α) in s, |f x| μ
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) :
∀ᵐ (x : α) ∂μ, |measure_theory.condexp m μ 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) :

Given a integrable function g, the conditional expectations of g with respect to a sequence of sub-σ-algebras is uniformly integrable.

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) :
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) :

Pull-out property of the conditional expectation.

Pull-out property of the conditional expectation.