mathlib documentation

measure_theory.function.conditional_expectation.basic

Conditional expectation #

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 .

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-σ-algebra) and a function f, we define the notation

Implementation notes #

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

Tags #

conditional expectation, conditional expected value

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

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

Equations
theorem measure_theory.ae_strongly_measurable'.const_inner {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_2} {β : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group β] [inner_product_space 𝕜 β] {f : α β} (hfm : measure_theory.ae_strongly_measurable' m f μ) (c : β) :
noncomputable def measure_theory.ae_strongly_measurable'.mk {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [topological_space β] (f : α β) (hfm : measure_theory.ae_strongly_measurable' m f μ) :
α β

An m-strongly measurable function almost everywhere equal to f.

Equations

If the restriction to a set s of a σ-algebra m is included in the restriction to s of another σ-algebra m₂ (hypothesis hs), the set s is m measurable and a function f almost everywhere supported on s is m-ae-strongly-measurable, then f is also m₂-ae-strongly-measurable.

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_strongly_measurable' m f μ, i.e. functions which are μ-a.e. equal to an m-strongly measurable function.

Equations
Instances for measure_theory.Lp_meas_subgroup
def measure_theory.Lp_meas {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] (m : measurable_space α) [measurable_space α] (p : ennreal) (μ : measure_theory.measure α) :

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

Equations
Instances for measure_theory.Lp_meas
theorem measure_theory.mem_Lp_meas_self {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 isometry_equiv 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 μ.

noncomputable def measure_theory.Lp_meas_subgroup_to_Lp_trim {α : Type u_1} (F : Type u_6) (p : ennreal) [normed_add_comm_group F] {m m0 : measurable_space α} (μ : measure_theory.measure α) (hm : m m0) (f : (measure_theory.Lp_meas_subgroup F m p μ)) :

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

Equations
noncomputable def measure_theory.Lp_meas_to_Lp_trim {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) (p : ennreal) [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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
noncomputable def measure_theory.Lp_trim_to_Lp_meas_subgroup {α : Type u_1} (F : Type u_6) (p : ennreal) [normed_add_comm_group F] {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_subgroup, inverse of Lp_meas_subgroup_to_Lp_trim.

Equations
noncomputable def measure_theory.Lp_trim_to_Lp_meas {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) (p : ennreal) [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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.

noncomputable def measure_theory.Lp_meas_subgroup_to_Lp_trim_iso {α : Type u_1} (F : Type u_6) (p : ennreal) [normed_add_comm_group F] {m m0 : measurable_space α} (μ : measure_theory.measure α) [hp : fact (1 p)] (hm : m m0) :

Lp_meas_subgroup and Lp F p (μ.trim hm) are isometric.

Equations
noncomputable def measure_theory.Lp_meas_subgroup_to_Lp_meas_iso {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) (p : ennreal) [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {m m0 : measurable_space α} (μ : measure_theory.measure α) [hp : fact (1 p)] :

Lp_meas_subgroup and Lp_meas are isometric.

Equations
noncomputable def measure_theory.Lp_meas_to_Lp_trim_lie {α : Type u_1} (F : Type u_6) (𝕜 : Type u_11) (p : ennreal) [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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
@[protected, instance]
@[protected, nolint, instance]
def measure_theory.Lp_meas.complete_space {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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 ) :

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.

theorem measure_theory.Lp_meas_to_Lp_trim_lie_symm_indicator {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_add_comm_group F] {m m0 : measurable_space α} [one_le_p : fact (1 p)] [normed_space F] {hm : m m0} {s : set α} {μ : measure_theory.measure α} (hs : measurable_set s) (hμs : (μ.trim hm) s ) (c : F) :

When applying the inverse of Lp_meas_to_Lp_trim_lie (which takes a function in the Lp space of the sub-sigma algebra and returns its version in the larger Lp space) to an indicator of the sub-sigma-algebra, we obtain an indicator in the Lp space of the larger sigma-algebra.

Auxiliary lemma for Lp.induction_strongly_measurable.

To prove something for an Lp function a.e. strongly measurable with respect to a sub-σ-algebra m in a normed space, it suffices to show that

  • the property holds for (multiples of) characteristic functions which are measurable w.r.t. m;
  • is closed under addition;
  • the set of functions in Lp strongly measurable w.r.t. m for which the property holds is closed.
theorem measure_theory.mem_ℒp.induction_strongly_measurable {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_add_comm_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [fact (1 p)] [normed_space F] (hm : m m0) (hp_ne_top : p ) (P : F) Prop) (h_ind : (c : F) ⦃s : set α⦄, measurable_set s μ s < P (s.indicator (λ (_x : α), c))) (h_add : ⦃f g : α F⦄, disjoint (function.support f) (function.support g) measure_theory.mem_ℒp f p μ measure_theory.mem_ℒp g p μ measure_theory.strongly_measurable f measure_theory.strongly_measurable g P f P g P (f + g)) (h_closed : is_closed {f : (measure_theory.Lp_meas F m p μ) | P f}) (h_ae : ⦃f g : α F⦄, f =ᵐ[μ] g measure_theory.mem_ℒp f p μ P f P g) ⦃f : α F⦄ (hf : measure_theory.mem_ℒp f p μ) (hfm : measure_theory.ae_strongly_measurable' m f μ) :
P f

To prove something for an arbitrary mem_ℒp function a.e. strongly measurable with respect to a sub-σ-algebra m in a normed space, it suffices to show that

  • the property holds for (multiples of) characteristic functions which are measurable w.r.t. m;
  • is closed under addition;
  • the set of functions in the Lᵖ space strongly measurable w.r.t. m for which the property holds is closed.
  • the property is closed under the almost-everywhere equal relation.

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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (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_strongly_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 : ennreal} [is_R_or_C 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (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_strongly_measurable' m f μ) (hg_meas : measure_theory.ae_strongly_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_add_comm_group 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_strongly_measurable' m f μ) (hgm : measure_theory.ae_strongly_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 : measure_theory.strongly_measurable f) (hfi : measure_theory.integrable_on f s μ) (hg : measure_theory.strongly_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 : measure_theory.strongly_measurable f) (hfi : measure_theory.integrable_on f s μ) (hg : measure_theory.strongly_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.

noncomputable def measure_theory.condexp_L2 {α : Type u_1} {E : Type u_4} (𝕜 : Type u_11) [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {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.integrable_on_condexp_L2_of_measure_ne_top {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hμs : μ s ) (f : (measure_theory.Lp E 2 μ)) :
theorem measure_theory.norm_condexp_L2_le_one {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) :
theorem measure_theory.norm_condexp_L2_le {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp E 2 μ)) :
theorem measure_theory.norm_condexp_L2_coe_le {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp E 2 μ)) :
theorem measure_theory.condexp_L2_indicator_of_measurable {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (c : E) :
theorem measure_theory.integral_condexp_L2_eq_of_fin_meas_real {α : Type u_1} {𝕜 : Type u_11} [is_R_or_C 𝕜] {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 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp E 2 μ)) (c : E) :

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 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (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 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {E'' : Type u_12} (𝕜' : Type u_13) [is_R_or_C 𝕜'] [normed_add_comm_group E''] [inner_product_space 𝕜' E''] [complete_space E''] [normed_space 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 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (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 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (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 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') [measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.integrable_condexp_L2_indicator {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group E'] [inner_product_space 𝕜 E'] [complete_space E'] [normed_space E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : E') :

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

noncomputable def measure_theory.condexp_ind_smul {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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_add_comm_group 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_add_comm_group 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 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {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.condexp_ind_smul_ae_eq_smul {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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) :
theorem measure_theory.set_lintegral_nnnorm_condexp_ind_smul_le {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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_L2_indicator {α : Type u_1} {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 ) :
theorem measure_theory.set_integral_condexp_ind_smul {α : Type u_1} {G' : Type u_9} [normed_add_comm_group 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
theorem measure_theory.condexp_ind_smul_nonneg {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} {E : Type u_2} [normed_lattice_add_comm_group E] [normed_space E] [ordered_smul E] [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : E) (hx : 0 x) :

Conditional expectation of an indicator as a continuous 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.

noncomputable def measure_theory.condexp_ind_L1_fin {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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_add {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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 y : G) :
theorem measure_theory.condexp_ind_L1_fin_smul {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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 ) (c : ) (x : G) :
theorem measure_theory.condexp_ind_L1_fin_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {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) :
theorem measure_theory.norm_condexp_ind_L1_fin_le {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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) :
theorem measure_theory.condexp_ind_L1_fin_disjoint_union {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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) :
noncomputable def measure_theory.condexp_ind_L1 {α : Type u_1} {G : Type u_8} [normed_add_comm_group G] [normed_space G] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) (s : set α) [measure_theory.sigma_finite (μ.trim hm)] (x : G) :

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_of_measure_eq_top {α : Type u_1} {G : Type u_8} [normed_add_comm_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hμs : μ s = ) (x : G) :
theorem measure_theory.condexp_ind_L1_smul {α : Type u_1} {G : Type u_8} [normed_add_comm_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : ) (x : G) :
theorem measure_theory.condexp_ind_L1_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {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_add_comm_group 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) :
noncomputable def measure_theory.condexp_ind {α : Type u_1} {G : Type u_8} [normed_add_comm_group G] [normed_space G] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] (s : set α) :

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 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {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_add_comm_group 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.condexp_ind_disjoint_union {α : Type u_1} {G : Type u_8} [normed_add_comm_group 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 = ) :
theorem measure_theory.set_integral_condexp_ind {α : Type u_1} {G' : Type u_9} [normed_add_comm_group 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
theorem measure_theory.condexp_ind_nonneg {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {E : Type u_2} [normed_lattice_add_comm_group E] [normed_space E] [ordered_smul E] (hs : measurable_set s) (hμs : μ s ) (x : E) (hx : 0 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 𝕜] [normed_add_comm_group F'] [normed_space 𝕜 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.Lp F' 1 μ)) :
theorem measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top {α : Type u_1} {F' : Type u_7} [normed_add_comm_group 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_add_comm_group 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.

noncomputable def measure_theory.condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_add_comm_group 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
@[simp]
theorem measure_theory.condexp_L1_measure_zero {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {f : α F'} (hm : m m0) :
theorem measure_theory.set_integral_condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_add_comm_group 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 𝕜] [normed_add_comm_group F'] [normed_space 𝕜 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 : α F') :

Conditional expectation of a function #

@[irreducible]
noncomputable def measure_theory.condexp {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space 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_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hm_not : ¬m m0) :
theorem measure_theory.condexp_of_not_sigma_finite {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α F'} (hm : m m0) (hμm_not : ¬measure_theory.sigma_finite (μ.trim hm)) :
theorem measure_theory.condexp_const {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (c : F') [measure_theory.is_finite_measure μ] :
measure_theory.condexp m μ (λ (x : α), c) = λ (_x : α), c
theorem measure_theory.condexp_congr_ae {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α F'} (h : f =ᵐ[μ] g) :
theorem measure_theory.set_integral_condexp {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space 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 : measure_theory.integrable f μ) (hs : measurable_set s) :
(x : α) in s, measure_theory.condexp m μ f 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_add_comm_group F'] [normed_space 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 : measure_theory.integrable f μ) :
(x : α), measure_theory.condexp m μ f x μ = (x : α), f x μ
theorem measure_theory.ae_eq_condexp_of_forall_set_integral_eq {α : Type u_1} {F' : Type u_7} [normed_add_comm_group 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_strongly_measurable' m 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_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m0 : measurable_space α} {μ : measure_theory.measure α} [hμ : μ.ae.ne_bot] (f : α F') :
measure_theory.condexp μ f = λ (_x : α), ((μ set.univ).to_real)⁻¹ (x : α), f x μ
theorem measure_theory.condexp_bot_ae_eq {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m0 : measurable_space α} {μ : measure_theory.measure α} (f : α F') :
measure_theory.condexp μ f =ᵐ[μ] λ (_x : α), ((μ set.univ).to_real)⁻¹ (x : α), f x μ
theorem measure_theory.condexp_bot {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m0 : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_probability_measure μ] (f : α F') :
measure_theory.condexp μ f = λ (_x : α), (x : α), f x μ
theorem measure_theory.condexp_finset_sum {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {ι : Type u_2} {s : finset ι} {f : ι α F'} (hf : (i : ι), i s measure_theory.integrable (f i) μ) :
measure_theory.condexp m μ (s.sum (λ (i : ι), f i)) =ᵐ[μ] s.sum (λ (i : ι), measure_theory.condexp m μ (f i))
theorem measure_theory.condexp_smul {α : Type u_1} {F' : Type u_7} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_add_comm_group F'] [normed_space 𝕜 F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (c : 𝕜) (f : α F') :
theorem measure_theory.condexp_condexp_of_le {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space 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₂)] :
theorem measure_theory.tendsto_condexp_L1_of_dominated_convergence {α : Type u_1} {F' : Type u_7} [normed_add_comm_group F'] [normed_space 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 : ), measure_theory.ae_strongly_measurable (fs 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))) :

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_7} [normed_add_comm_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (fs gs : α F') (f g : α F') (hfs_int : (n : ), measure_theory.integrable (fs n) μ) (hgs_int : (n : ), measure_theory.integrable (gs 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 : ), measure_theory.condexp m μ (fs n) =ᵐ[μ] measure_theory.condexp m μ (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.