mathlib documentation

measure_theory.function.conditional_expectation

Conditional expectation #

We build the conditional expectation of a 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-measurable function μ[f|hm] which is integrable and verifies ∫ x in s, μ[f|hm] x ∂μ = ∫ x in s, f x ∂μ for any m-measurable sets s. It is unique as an element of .

The construction is done in four steps:

Main results #

The conditional expectation and its properties

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

Notations #

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

Implementation notes #

Most of the results in this file are valid for a second countable, borel, real normed space F. However, some lemmas also use 𝕜 : is_R_or_C:

Tags #

conditional expectation, conditional expected value

def measure_theory.ae_measurable' {α : Type u_1} {β : Type u_2} [measurable_space β] (m : measurable_space α) {m0 : measurable_space α} (f : α → β) (μ : measure_theory.measure α) :
Prop

A function f verifies ae_measurable' m f μ if it is μ-a.e. equal to an m-measurable function. This is similar to ae_measurable, but the measurable_space structures used for the measurability statement and for the measure are different.

Equations
theorem measure_theory.ae_measurable'.congr {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] {f g : α → β} (hf : measure_theory.ae_measurable' m f μ) (hfg : f =ᵐ[μ] g) :
theorem measure_theory.ae_measurable'.add {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] {f g : α → β} [has_add β] [has_measurable_add₂ β] (hf : measure_theory.ae_measurable' m f μ) (hg : measure_theory.ae_measurable' m g μ) :
theorem measure_theory.ae_measurable'.neg {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] [has_neg β] [has_measurable_neg β] {f : α → β} (hfm : measure_theory.ae_measurable' m f μ) :
theorem measure_theory.ae_measurable'.sub {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] [has_sub β] [has_measurable_sub₂ β] {f g : α → β} (hfm : measure_theory.ae_measurable' m f μ) (hgm : measure_theory.ae_measurable' m g μ) :
theorem measure_theory.ae_measurable'.const_smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] [measurable_space 𝕜] {f : α → β} [has_scalar 𝕜 β] [has_measurable_smul 𝕜 β] (c : 𝕜) (hf : measure_theory.ae_measurable' m f μ) :
theorem measure_theory.ae_measurable'.const_inner {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] [measurable_space 𝕜] [is_R_or_C 𝕜] [borel_space 𝕜] [inner_product_space 𝕜 β] [topological_space.second_countable_topology β] [opens_measurable_space β] {f : α → β} (hfm : measure_theory.ae_measurable' m f μ) (c : β) :
measure_theory.ae_measurable' m (λ (x : α), inner c (f x)) μ
def measure_theory.ae_measurable'.mk {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] (f : α → β) (hfm : measure_theory.ae_measurable' m f μ) :
α → β

A m-measurable function almost everywhere equal to f.

Equations
theorem measure_theory.ae_measurable'.measurable_mk {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] {f : α → β} (hfm : measure_theory.ae_measurable' m f μ) :
theorem measure_theory.ae_measurable'.ae_eq_mk {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] {f : α → β} (hfm : measure_theory.ae_measurable' m f μ) :
theorem measure_theory.ae_measurable'.measurable_comp {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [measurable_space β] {γ : Type u_3} [measurable_space γ] {f : α → β} {g : β → γ} (hg : measurable g) (hf : measure_theory.ae_measurable' m f μ) :
theorem measure_theory.ae_measurable'_of_ae_measurable'_trim {α : Type u_1} {β : Type u_2} {m m0 m0' : measurable_space α} [measurable_space β] (hm0 : m0 m0') {μ : measure_theory.measure α} {f : α → β} (hf : measure_theory.ae_measurable' m f (μ.trim hm0)) :
theorem measure_theory.measurable.ae_measurable' {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} [measurable_space β] {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) :

The subset Lp_meas of Lp functions a.e. measurable with respect to a sub-sigma-algebra #

Lp_meas_subgroup F m p μ is the subspace of Lp F p μ containing functions f verifying ae_measurable' m f μ, i.e. functions which are μ-a.e. equal to an m-measurable function.

Equations

Lp_meas F 𝕜 m p μ is the subspace of Lp F p μ containing functions f verifying ae_measurable' m f μ, i.e. functions which are μ-a.e. equal to an m-measurable function.

Equations
theorem measure_theory.mem_Lp_meas_self {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m0 : measurable_space α} (μ : measure_theory.measure α) (f : (measure_theory.Lp F p μ)) :
f measure_theory.Lp_meas F 𝕜 m0 p μ
theorem measure_theory.Lp_meas_coe {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : (measure_theory.Lp_meas F 𝕜 m p μ)} :
theorem measure_theory.mem_Lp_meas_indicator_const_Lp {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} (hm : m m0) {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (hμs : μ s ) {c : F} :

The subspace Lp_meas is complete. #

We define an isometric between Lp_meas_subgroup and the Lp space corresponding to the measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of Lp_meas_subgroup (and Lp_meas).

If f belongs to Lp_meas_subgroup F m p μ, then the measurable function it is almost everywhere equal to (given by ae_measurable.mk) belongs to ℒp for the measure μ.trim hm.

If f belongs to Lp for the measure μ.trim hm, then it belongs to the subgroup Lp_meas_subgroup F m p μ.

Map from Lp_meas_subgroup to Lp F p (μ.trim hm).

Equations
def measure_theory.Lp_meas_to_Lp_trim {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) (p : ℝ≥0∞) [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} (μ : measure_theory.measure α) (hm : m m0) (f : (measure_theory.Lp_meas F 𝕜 m p μ)) :

Map from Lp_meas to Lp F p (μ.trim hm).

Equations

Map from Lp F p (μ.trim hm) to Lp_meas_subgroup, inverse of Lp_meas_subgroup_to_Lp_trim.

Equations
def measure_theory.Lp_trim_to_Lp_meas {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) (p : ℝ≥0∞) [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} (μ : measure_theory.measure α) (hm : m m0) (f : (measure_theory.Lp F p (μ.trim hm))) :

Map from Lp F p (μ.trim hm) to Lp_meas, inverse of Lp_meas_to_Lp_trim.

Equations
theorem measure_theory.Lp_meas_to_Lp_trim_ae_eq {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp_meas F 𝕜 m p μ)) :
theorem measure_theory.Lp_trim_to_Lp_meas_ae_eq {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp F p (μ.trim hm))) :

Lp_trim_to_Lp_meas_subgroup is a right inverse of Lp_meas_subgroup_to_Lp_trim.

Lp_trim_to_Lp_meas_subgroup is a left inverse of Lp_meas_subgroup_to_Lp_trim.

theorem measure_theory.Lp_meas_to_Lp_trim_smul {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (c : 𝕜) (f : (measure_theory.Lp_meas F 𝕜 m p μ)) :

Lp_meas_subgroup_to_Lp_trim preserves the norm.

def measure_theory.Lp_meas_to_Lp_trim_lie {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) (p : ℝ≥0∞) [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} (μ : measure_theory.measure α) [hp : fact (1 p)] (hm : m m0) :

Lp_meas and Lp F p (μ.trim hm) are isometric, with a linear equivalence.

Equations
@[instance]
def measure_theory.Lp_meas.complete_space {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} [hm : fact (m m0)] [complete_space F] [hp : fact (1 p)] :
theorem measure_theory.Lp_meas.ae_fin_strongly_measurable' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [opens_measurable_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp_meas F 𝕜 m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) :
∃ (g : α → F), measure_theory.fin_strongly_measurable g (μ.trim hm) f =ᵐ[μ] g

We do not get ae_fin_strongly_measurable f (μ.trim hm), since we don't have f =ᵐ[μ.trim hm] Lp_meas_to_Lp_trim F 𝕜 p μ hm f but only the weaker f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f.

Uniqueness of the conditional expectation #

theorem measure_theory.Lp_meas.ae_eq_zero_of_forall_set_integral_eq_zero {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] (hm : m m0) (f : (measure_theory.Lp_meas E' 𝕜 m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) :
f =ᵐ[μ] 0
theorem measure_theory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero' {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] (hm : m m0) (f : (measure_theory.Lp E' p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hf_zero : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = 0) (hf_meas : measure_theory.ae_measurable' m f μ) :
f =ᵐ[μ] 0
theorem measure_theory.Lp.ae_eq_of_forall_set_integral_eq' {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} {p : ℝ≥0∞} [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] (hm : m m0) (f g : (measure_theory.Lp E' p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hg_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on g s μ) (hfg : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = (x : α) in s, g x μ) (hf_meas : measure_theory.ae_measurable' m f μ) (hg_meas : measure_theory.ae_measurable' m g μ) :

Uniqueness of the conditional expectation

theorem measure_theory.ae_eq_of_forall_set_integral_eq_of_sigma_finite' {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] {f g : α → F'} (hf_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on f s μ) (hg_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on g s μ) (hfg_eq : ∀ (s : set α), measurable_set sμ s < (x : α) in s, f x μ = (x : α) in s, g x μ) (hfm : measure_theory.ae_measurable' m f μ) (hgm : measure_theory.ae_measurable' m g μ) :
f =ᵐ[μ] g
theorem measure_theory.integral_norm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) {f g : α → } (hf : measurable f) (hfi : measure_theory.integrable_on f s μ) (hg : measurable g) (hgi : measure_theory.integrable_on g s μ) (hgf : ∀ (t : set α), measurable_set tμ t < (x : α) in t, g x μ = (x : α) in t, f x μ) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, g x μ (x : α) in s, f x μ

Let m be a sub-σ-algebra of m0, f a m0-measurable function and g a m-measurable function, such that their integrals coincide on m-measurable sets with finite measure. Then ∫ x in s, ∥g x∥ ∂μ ≤ ∫ x in s, ∥f x∥ ∂μ on all m-measurable sets with finite measure.

theorem measure_theory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) {f g : α → } (hf : measurable f) (hfi : measure_theory.integrable_on f s μ) (hg : measurable g) (hgi : measure_theory.integrable_on g s μ) (hgf : ∀ (t : set α), measurable_set tμ t < (x : α) in t, g x μ = (x : α) in t, f x μ) (hs : measurable_set s) (hμs : μ s ) :
∫⁻ (x : α) in s, g x∥₊ μ ∫⁻ (x : α) in s, f x∥₊ μ

Let m be a sub-σ-algebra of m0, f a m0-measurable function and g a m-measurable function, such that their integrals coincide on m-measurable sets with finite measure. Then ∫⁻ x in s, ∥g x∥₊ ∂μ ≤ ∫⁻ x in s, ∥f x∥₊ ∂μ on all m-measurable sets with finite measure.

Conditional expectation in L2 #

We define a conditional expectation in L2: it is the orthogonal projection on the subspace Lp_meas.

def measure_theory.condexp_L2 {α : Type u_1} {E : Type u_4} (𝕜 : Type u_11) [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) :

Conditional expectation of a function in L2 with respect to a sigma-algebra

Equations
theorem measure_theory.integral_condexp_L2_eq_of_fin_meas_real {α : Type u_1} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} (f : (measure_theory.Lp 𝕜 2 μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ((measure_theory.condexp_L2 𝕜 hm) f) x μ = (x : α) in s, f x μ
theorem measure_theory.lintegral_nnnorm_condexp_L2_le {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (f : (measure_theory.Lp 2 μ)) :
theorem measure_theory.condexp_L2_ae_eq_zero_of_ae_eq_zero {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} (hs : measurable_set s) (hμs : μ s ) {f : (measure_theory.Lp 2 μ)} (hf : f =ᵐ[μ.restrict s] 0) :
theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le_real {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (ht : measurable_set t) (hμt : μ t ) :
theorem measure_theory.condexp_L2_const_inner {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E] [measurable_space E] [borel_space E] [topological_space.second_countable_topology E] [complete_space E] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp E 2 μ)) (c : E) :
((measure_theory.condexp_L2 𝕜 hm) (measure_theory.mem_ℒp.to_Lp (λ (a : α), inner c (f a)) _)) =ᵐ[μ] λ (a : α), inner c (((measure_theory.condexp_L2 𝕜 hm) f) a)

condexp_L2 commutes with taking inner products with constants. See the lemma condexp_L2_comp_continuous_linear_map for a more general result about commuting with continuous linear maps.

theorem measure_theory.integral_condexp_L2_eq {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [is_scalar_tower 𝕜 E'] (hm : m m0) (f : (measure_theory.Lp E' 2 μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ((measure_theory.condexp_L2 𝕜 hm) f) x μ = (x : α) in s, f x μ

condexp_L2 verifies the equality of integrals defining the conditional expectation.

theorem measure_theory.condexp_L2_comp_continuous_linear_map {α : Type u_1} {E' : Type u_5} (𝕜 : Type u_11) [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {E'' : Type u_12} (𝕜' : Type u_13) [is_R_or_C 𝕜'] [measurable_space 𝕜'] [borel_space 𝕜'] [measurable_space E''] [inner_product_space 𝕜' E''] [borel_space E''] [topological_space.second_countable_topology E''] [complete_space E''] [normed_space E''] [is_scalar_tower 𝕜 E'] [is_scalar_tower 𝕜' E''] (hm : m m0) (T : E' →L[] E'') (f : (measure_theory.Lp E' 2 μ)) :
theorem measure_theory.condexp_L2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_5} (𝕜 : Type u_11) [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [is_scalar_tower 𝕜 E'] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') :
theorem measure_theory.set_lintegral_nnnorm_condexp_L2_indicator_le {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [is_scalar_tower 𝕜 E'] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') {t : set α} (ht : measurable_set t) (hμt : μ t ) :
theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E'] [topological_space.second_countable_topology E'] [complete_space E'] [normed_space E'] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [is_scalar_tower 𝕜 E'] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') [measure_theory.sigma_finite (μ.trim hm)] :

If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set with finite measure is integrable.

def measure_theory.condexp_ind_smul {α : Type u_1} {G : Type u_8} [normed_group G] [measurable_space G] [borel_space G] [topological_space.second_countable_topology G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) :

Conditional expectation of the indicator of a measurable set with finite measure, in L2.

Equations
theorem measure_theory.condexp_ind_smul_add {α : Type u_1} {G : Type u_8} [normed_group G] [measurable_space G] [borel_space G] [topological_space.second_countable_topology G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (x y : G) :
theorem measure_theory.condexp_ind_smul_smul {α : Type u_1} {G : Type u_8} [normed_group G] [measurable_space G] [borel_space G] [topological_space.second_countable_topology G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (c : ) (x : G) :
theorem measure_theory.condexp_ind_smul_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [normed_space F] [smul_comm_class 𝕜 F] (hs : measurable_set s) (hμs : μ s ) (c : 𝕜) (x : F) :
theorem measure_theory.set_lintegral_nnnorm_condexp_ind_smul_le {α : Type u_1} {G : Type u_8} [normed_group G] [measurable_space G] [borel_space G] [topological_space.second_countable_topology G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) {t : set α} (ht : measurable_set t) (hμt : μ t ) :

If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set with finite measure is integrable.

theorem measure_theory.set_integral_condexp_ind_smul {α : Type u_1} {G' : Type u_9} [normed_group G'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology G'] [normed_space G'] [complete_space G'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} {hm : m m0} (hs : measurable_set s) (ht : measurable_set t) (hμs : μ s ) (hμt : μ t ) (x : G') :
(a : α) in s, (measure_theory.condexp_ind_smul hm ht hμt x) a μ = (μ (t s)).to_real x

Conditional expectation of an indicator as a condinuous linear map. #

The goal of this section is to build condexp_ind (hm : m ≤ m0) (μ : measure α) (s : set s) : G →L[ℝ] α →₁[μ] G, which takes x : G to the conditional expectation of the indicator of the set s with value x, seen as an element of α →₁[μ] G.

def measure_theory.condexp_ind_L1_fin {α : Type u_1} {G : Type u_8} [normed_group G] [measurable_space G] [borel_space G] [topological_space.second_countable_topology G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :

Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.

Equations
theorem measure_theory.condexp_ind_L1_fin_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [normed_space F] [smul_comm_class 𝕜 F] (hs : measurable_set s) (hμs : μ s ) (c : 𝕜) (x : F) :

Conditional expectation of the indicator of a set, as a function in L1. Its value for sets which are not both measurable and of finite measure is not used: we set it to 0.

Equations
theorem measure_theory.condexp_ind_L1_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [normed_space F] [smul_comm_class 𝕜 F] (c : 𝕜) (x : F) :
theorem measure_theory.condexp_ind_L1_disjoint_union {α : Type u_1} {G : Type u_8} [normed_group G] [measurable_space G] [borel_space G] [topological_space.second_countable_topology G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (ht : measurable_set t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :

Conditional expectation of the indicator of a set, as a linear map from G to L1.

Equations
theorem measure_theory.condexp_ind_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F] [normed_space 𝕜 F] [measurable_space F] [borel_space F] [topological_space.second_countable_topology F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [normed_space F] [smul_comm_class 𝕜 F] (c : 𝕜) (x : F) :
theorem measure_theory.condexp_ind_disjoint_union_apply {α : Type u_1} {G : Type u_8} [normed_group G] [measurable_space G] [borel_space G] [topological_space.second_countable_topology G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (ht : measurable_set t) (hμs : μ s ) (hμt : μ t ) (hst : s t = ) (x : G) :
theorem measure_theory.set_integral_condexp_ind {α : Type u_1} {G' : Type u_9} [normed_group G'] [measurable_space G'] [borel_space G'] [topological_space.second_countable_topology G'] [normed_space G'] [complete_space G'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (ht : measurable_set t) (hμs : μ s ) (hμt : μ t ) (x : G') :
(a : α) in s, ((measure_theory.condexp_ind hm μ t) x) a μ = (μ (t s)).to_real x

Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.

Equations
theorem measure_theory.condexp_L1_clm_smul {α : Type u_1} {F' : Type u_7} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F'] [normed_space 𝕜 F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] [is_scalar_tower 𝕜 F'] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : 𝕜) (f : (measure_theory.Lp F' 1 μ)) :
theorem measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {s : set α} (f : (measure_theory.Lp F' 1 μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ((measure_theory.condexp_L1_clm hm μ) f) x μ = (x : α) in s, f x μ

Auxiliary lemma used in the proof of set_integral_condexp_L1_clm.

theorem measure_theory.set_integral_condexp_L1_clm {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {s : set α} (f : (measure_theory.Lp F' 1 μ)) (hs : measurable_set s) :
(x : α) in s, ((measure_theory.condexp_L1_clm hm μ) f) x μ = (x : α) in s, f x μ

The integral of the conditional expectation condexp_L1_clm over an m-measurable set is equal to the integral of f on that set. See also set_integral_condexp, the similar statement for condexp.

def measure_theory.condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] (f : α → F') :

Conditional expectation of a function, in L1. Its value is 0 if the function is not integrable. The function-valued condexp should be used instead in most cases.

Equations
theorem measure_theory.set_integral_condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} {s : set α} (hf : measure_theory.integrable f μ) (hs : measurable_set s) :
(x : α) in s, (measure_theory.condexp_L1 hm μ f) x μ = (x : α) in s, f x μ

The integral of the conditional expectation condexp_L1 over an m-measurable set is equal to the integral of f on that set. See also set_integral_condexp, the similar statement for condexp.

theorem measure_theory.condexp_L1_smul {α : Type u_1} {F' : Type u_7} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F'] [normed_space 𝕜 F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] [is_scalar_tower 𝕜 F'] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : 𝕜) (f : α → F') :

Conditional expectation of a function #

def measure_theory.condexp {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] (f : α → F') :
α → F'

Conditional expectation of a function. Its value is 0 if the function is not integrable.

Equations
theorem measure_theory.condexp_of_measurable {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hf : measurable f) (hfi : measure_theory.integrable f μ) :
μ[f|hm] = f
theorem measure_theory.condexp_const {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : F') [measure_theory.is_finite_measure μ] :
μ[λ (x : α), c|hm] = λ (_x : α), c
theorem measure_theory.condexp_undef {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hf : ¬measure_theory.integrable f μ) :
μ[f|hm] =ᵐ[μ] 0
@[simp]
theorem measure_theory.set_integral_condexp {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} {s : set α} (hf : measure_theory.integrable f μ) (hs : measurable_set s) :
(x : α) in s, μ[f|hm] 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_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hf : measure_theory.integrable f μ) :
(x : α), μ[f|hm] x μ = (x : α), f x μ
theorem measure_theory.ae_eq_condexp_of_forall_set_integral_eq {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] {f g : α → F'} (hf : measure_theory.integrable f μ) (hg_int_finite : ∀ (s : set α), measurable_set sμ s < measure_theory.integrable_on g s μ) (hg_eq : ∀ (s : set α), measurable_set sμ s < (x : α) in s, g x μ = (x : α) in s, f x μ) (hgm : measure_theory.ae_measurable' m g μ) :
g =ᵐ[μ][f|hm])

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_add {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f g : α → F'} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
μ[f + g|hm] =ᵐ[μ] μ[f|hm] +[g|hm])
theorem measure_theory.condexp_smul {α : Type u_1} {F' : Type u_7} {𝕜 : Type u_11} [is_R_or_C 𝕜] [measurable_space 𝕜] [normed_group F'] [normed_space 𝕜 F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} [borel_space 𝕜] [is_scalar_tower 𝕜 F'] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : 𝕜) (f : α → F') :
μ[c f|hm] =ᵐ[μ] c [f|hm])
theorem measure_theory.condexp_neg {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : α → F') :
μ[-f|hm] =ᵐ[μ] -[f|hm])
theorem measure_theory.condexp_sub {α : Type u_1} {F' : Type u_7} [normed_group F'] [measurable_space F'] [borel_space F'] [topological_space.second_countable_topology F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f g : α → F'} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
μ[f - g|hm] =ᵐ[μ] μ[f|hm] -[g|hm])