# mathlib3documentation

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 #

• measure_theory.rn_deriv_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.
• 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 : μ) :
(μ.trim hm) =ᵐ[μ]
theorem measure_theory.snorm_one_condexp_le_snorm {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : α ) :
μ μ
theorem measure_theory.integral_abs_condexp_le {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : α ) :
(x : α), | 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, | 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 : α) μ, | 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} {g : α } (hint : μ) {ℱ : ι } (hℱ : (i : ι), ℱ i m0) :
measure_theory.uniform_integrable (λ (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 : ) {g : α } (hg : μ) :
(f * g) =ᵐ[μ] f *

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) {f g : α } (hg : μ) (c : ) (hf_bound : ∀ᵐ (x : α) μ, f x c) :
(f * g) =ᵐ[μ] f *
theorem measure_theory.condexp_strongly_measurable_mul_of_bound₀ {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f g : α } (hf : μ) (hg : μ) (c : ) (hf_bound : ∀ᵐ (x : α) μ, f x c) :
(f * g) =ᵐ[μ] f *
theorem measure_theory.condexp_strongly_measurable_mul {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α } (hfg : μ) (hg : μ) :
(f * g) =ᵐ[μ] f *

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 : μ) (hfg : μ) (hg : μ) :
(f * g) =ᵐ[μ] f *

Pull-out property of the conditional expectation.