mathlib3 documentation

measure_theory.function.conditional_expectation.real

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 #

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

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.

Pull-out property of the conditional expectation.

Pull-out property of the conditional expectation.