# mathlib3documentation

measure_theory.function.conditional_expectation.basic

# Conditional expectation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We build the conditional expectation of an integrable function f with value in a Banach space with respect to a measure μ (defined on a measurable space structure m0) and a measurable space structure m with hm : m ≤ m0 (a sub-sigma-algebra). This is an m-strongly measurable function μ[f|hm] which is integrable and verifies ∫ x in s, μ[f|hm] x ∂μ = ∫ x in s, f x ∂μ for all m-measurable sets s. It is unique as an element of L¹.

The construction is done in four steps:

• Define the conditional expectation of an L² function, as an element of L². This is the orthogonal projection on the subspace of almost everywhere m-measurable functions.
• Show that the conditional expectation of the indicator of a measurable set with finite measure is integrable and define a map set α → (E →L[ℝ] (α →₁[μ] E)) which to a set associates a linear map. That linear map sends x ∈ E to the conditional expectation of the indicator of the set with value x.
• Extend that map to condexp_L1_clm : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the file measure_theory/integral/set_to_L1).
• Define the conditional expectation of a function f : α → E, which is an integrable function α → E equal to 0 if f is not integrable, and equal to an m-measurable representative of condexp_L1_clm applied to [f], the equivalence class of f in L¹.

The first step is done in measure_theory.function.conditional_expectation.condexp_L2, the two next steps in measure_theory.function.conditional_expectation.condexp_L1 and the final step is performed in this file.

## Main results #

The conditional expectation and its properties

• condexp (m : measurable_space α) (μ : measure α) (f : α → E): conditional expectation of f with respect to m.
• integrable_condexp : condexp is integrable.
• strongly_measurable_condexp : condexp is m-strongly-measurable.
• set_integral_condexp (hf : integrable f μ) (hs : measurable_set[m] s) : if m ≤ m0 (the σ-algebra over which the measure is defined), then the conditional expectation verifies ∫ x in s, condexp m μ f x ∂μ = ∫ x in s, f x ∂μ for any m-measurable set s.

While condexp is function-valued, we also define condexp_L1 with value in L1 and a continuous linear map condexp_L1_clm from L1 to L1. condexp should be used in most cases.

Uniqueness of the conditional expectation

• ae_eq_condexp_of_forall_set_integral_eq: an a.e. m-measurable function which verifies the equality of integrals is a.e. equal to condexp.

## Notations #

For a measure μ defined on a measurable space structure m0, another measurable space structure m with hm : m ≤ m0 (a sub-σ-algebra) and a function f, we define the notation

• μ[f|m] = condexp m μ f.

## Tags #

conditional expectation, conditional expected value

@[irreducible]
noncomputable def measure_theory.condexp {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] (m : measurable_space α) {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α F') :
α F'

Conditional expectation of a function. It is defined as 0 if any one of the following conditions is true:

• m is not a sub-σ-algebra of m0,
• μ is not σ-finite with respect to m,
• f is not integrable.
Equations
theorem measure_theory.condexp_of_not_le {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hm_not : ¬m m0) :
= 0
theorem measure_theory.condexp_of_not_sigma_finite {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hm : m m0) (hμm_not : ¬) :
= 0
theorem measure_theory.condexp_of_sigma_finite {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.condexp_of_strongly_measurable {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] {f : α F'} (hfi : μ) :
= f
theorem measure_theory.condexp_const {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (c : F')  :
(λ (x : α), c) = λ (_x : α), c
theorem measure_theory.condexp_ae_eq_condexp_L1 {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] (f : α F') :
=ᵐ[μ] f)
theorem measure_theory.condexp_ae_eq_condexp_L1_clm {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hf : μ) :
theorem measure_theory.condexp_undef {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hf : ¬) :
= 0
@[simp]
theorem measure_theory.condexp_zero {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} :
= 0
theorem measure_theory.strongly_measurable_condexp {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} :
theorem measure_theory.condexp_congr_ae {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α F'} (h : f =ᵐ[μ] g) :
=ᵐ[μ]
theorem measure_theory.condexp_of_ae_strongly_measurable' {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] {f : α F'} (hf : μ) (hfi : μ) :
=ᵐ[μ] f
theorem measure_theory.integrable_condexp {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} :
theorem measure_theory.set_integral_condexp {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} {s : set α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hf : μ) (hs : measurable_set s) :
(x : α) in s, x μ = (x : α) in s, f x μ

The integral of the conditional expectation μ[f|hm] over an m-measurable set is equal to the integral of f on that set.

theorem measure_theory.integral_condexp {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] (hf : μ) :
(x : α), x μ = (x : α), f x μ
theorem measure_theory.ae_eq_condexp_of_forall_set_integral_eq {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] {f g : α F'} (hf : μ) (hg_int_finite : (s : set α), μ s < ) (hg_eq : (s : set α), μ s < (x : α) in s, g x μ = (x : α) in s, f x μ) (hgm : μ) :
g =ᵐ[μ]

Uniqueness of the conditional expectation If a function is a.e. m-measurable, verifies an integrability condition and has same integral as f on all m-measurable sets, then it is a.e. equal to μ[f|hm].

theorem measure_theory.condexp_bot' {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m0 : measurable_space α} {μ : measure_theory.measure α} [hμ : μ.ae.ne_bot] (f : α F') :
= λ (_x : α), ((μ set.univ).to_real)⁻¹ (x : α), f x μ
theorem measure_theory.condexp_bot_ae_eq {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m0 : measurable_space α} {μ : measure_theory.measure α} (f : α F') :
=ᵐ[μ] λ (_x : α), ((μ set.univ).to_real)⁻¹ (x : α), f x μ
theorem measure_theory.condexp_bot {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m0 : measurable_space α} {μ : measure_theory.measure α} (f : α F') :
= λ (_x : α), (x : α), f x μ
theorem measure_theory.condexp_add {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α F'} (hf : μ) (hg : μ) :
(f + g) =ᵐ[μ] +
theorem measure_theory.condexp_finset_sum {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} {s : finset ι} {f : ι α F'} (hf : (i : ι), i s μ) :
(s.sum (λ (i : ι), f i)) =ᵐ[μ] s.sum (λ (i : ι), (f i))
theorem measure_theory.condexp_smul {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_4} [is_R_or_C 𝕜] [ F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (c : 𝕜) (f : α F') :
(c f) =ᵐ[μ] c
theorem measure_theory.condexp_neg {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : α F') :
(-f) =ᵐ[μ] -
theorem measure_theory.condexp_sub {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α F'} (hf : μ) (hg : μ) :
(f - g) =ᵐ[μ] -
theorem measure_theory.condexp_condexp_of_le {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {f : α F'} {m₁ m₂ m0 : measurable_space α} {μ : measure_theory.measure α} (hm₁₂ : m₁ m₂) (hm₂ : m₂ m0) [measure_theory.sigma_finite (μ.trim hm₂)] :
f) =ᵐ[μ] f
theorem measure_theory.condexp_mono {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} [ E] [ E] {f g : α E} (hf : μ) (hg : μ) (hfg : f ≤ᵐ[μ] g) :
theorem measure_theory.condexp_nonneg {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} [ E] [ E] {f : α E} (hf : 0 ≤ᵐ[μ] f) :
theorem measure_theory.condexp_nonpos {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} [ E] [ E] {f : α E} (hf : f ≤ᵐ[μ] 0) :
theorem measure_theory.tendsto_condexp_L1_of_dominated_convergence {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] {fs : α F'} {f : α F'} (bound_fs : α ) (hfs_meas : (n : ), ) (h_int_bound_fs : measure_theory.integrable bound_fs μ) (hfs_bound : (n : ), ∀ᵐ (x : α) μ, fs n x bound_fs x) (hfs : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), fs n x) filter.at_top (nhds (f x))) :
filter.tendsto (λ (n : ), (fs n)) filter.at_top (nhds f))

Lebesgue dominated convergence theorem: sufficient conditions under which almost everywhere convergence of a sequence of functions implies the convergence of their image by condexp_L1.

theorem measure_theory.tendsto_condexp_unique {α : Type u_1} {F' : Type u_3} [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (fs gs : α F') (f g : α F') (hfs_int : (n : ), μ) (hgs_int : (n : ), μ) (hfs : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), fs n x) filter.at_top (nhds (f x))) (hgs : ∀ᵐ (x : α) μ, filter.tendsto (λ (n : ), gs n x) filter.at_top (nhds (g x))) (bound_fs : α ) (h_int_bound_fs : measure_theory.integrable bound_fs μ) (bound_gs : α ) (h_int_bound_gs : measure_theory.integrable bound_gs μ) (hfs_bound : (n : ), ∀ᵐ (x : α) μ, fs n x bound_fs x) (hgs_bound : (n : ), ∀ᵐ (x : α) μ, gs n x bound_gs x) (hfg : (n : ), (fs n) =ᵐ[μ] (gs n)) :
=ᵐ[μ]

If two sequences of functions have a.e. equal conditional expectations at each step, converge and verify dominated convergence hypotheses, then the conditional expectations of their limits are a.e. equal.