mathlib documentation

measure_theory.function.conditional_expectation

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'.congr {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f g : α → β} (hf : measure_theory.ae_strongly_measurable' m f μ) (hfg : f =ᵐ[μ] g) :
theorem measure_theory.ae_strongly_measurable'.const_smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {m m0 : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {f : α → β} [has_scalar 𝕜 β] [has_continuous_const_smul 𝕜 β] (c : 𝕜) (hf : measure_theory.ae_strongly_measurable' m f μ) :
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 𝕜] [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
theorem measure_theory.ae_strongly_measurable'.continuous_comp {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [topological_space β] {γ : Type u_3} [topological_space γ] {f : α → β} {g : β → γ} (hg : continuous g) (hf : measure_theory.ae_strongly_measurable' m f μ) :
theorem measure_theory.ae_strongly_measurable'.ae_strongly_measurable'_of_measurable_space_le_on {α : Type u_1} {E : Type u_2} {m m₂ m0 : measurable_space α} {μ : measure_theory.measure α} [topological_space E] [has_zero E] (hm : m m0) {s : set α} {f : α → E} (hs_m : measurable_set s) (hs : ∀ (t : set α), measurable_set (s t)measurable_set (s t)) (hf : measure_theory.ae_strongly_measurable' m f μ) (hf_zero : f =ᵐ[μ.restrict s] 0) :

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_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_iff_ae_strongly_measurable' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ennreal} [is_R_or_C 𝕜] [normed_group F] [normed_space 𝕜 F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : (measure_theory.Lp F p μ)} :
theorem measure_theory.Lp_meas.ae_strongly_measurable' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ennreal} [is_R_or_C 𝕜] [normed_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_self {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ennreal} [is_R_or_C 𝕜] [normed_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_subgroup_coe {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : (measure_theory.Lp_meas_subgroup F m p μ)} :
theorem measure_theory.Lp_meas_coe {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} {p : ennreal} [is_R_or_C 𝕜] [normed_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_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 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).

theorem measure_theory.mem_ℒp_trim_of_mem_Lp_meas_subgroup {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp F p μ)) (hf_meas : f measure_theory.Lp_meas_subgroup F m p μ) :

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_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_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_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_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_trim_to_Lp_meas_subgroup_ae_eq {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (measure_theory.Lp F p (μ.trim hm))) :
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_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_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_group F] [normed_space 𝕜 F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (c : 𝕜) (f : (measure_theory.Lp_meas F 𝕜 m p μ)) :
theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_norm_map {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [hp : fact (1 p)] (hm : m m0) (f : (measure_theory.Lp_meas_subgroup F m p μ)) :

Lp_meas_subgroup_to_Lp_trim preserves the norm.

theorem measure_theory.isometry_Lp_meas_subgroup_to_Lp_trim {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [hp : fact (1 p)] (hm : m m0) :
noncomputable def measure_theory.Lp_meas_subgroup_to_Lp_trim_iso {α : Type u_1} (F : Type u_6) (p : ennreal) [normed_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_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_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]
def measure_theory.Lp_meas_subgroup.complete_space {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [hm : fact (m m0)] [complete_space F] [hp : fact (1 p)] :
@[protected, 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_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.is_complete_ae_strongly_measurable' {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [hp : fact (1 p)] [complete_space F] (hm : m m0) :
theorem measure_theory.is_closed_ae_strongly_measurable' {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [hp : fact (1 p)] [complete_space F] (hm : m m0) :
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_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 ) :
∃ (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.

theorem measure_theory.Lp_meas_to_Lp_trim_lie_symm_indicator {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_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.

theorem measure_theory.Lp_meas_to_Lp_trim_lie_symm_to_Lp {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [one_le_p : fact (1 p)] [normed_space F] (hm : m m0) (f : α → F) (hf : measure_theory.mem_ℒp f p (μ.trim hm)) :
theorem measure_theory.Lp.induction_strongly_measurable_aux {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [fact (1 p)] [normed_space F] (hm : m m0) (hp_ne_top : p ) (P : (measure_theory.Lp F p μ) → Prop) (h_ind : ∀ (c : F) {s : set α} (hs : measurable_set s) (hμs : μ s < ), P (measure_theory.Lp.simple_func.indicator_const p _ _ c)) (h_add : ∀ ⦃f g : α → F⦄ (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ), measure_theory.ae_strongly_measurable' m f μmeasure_theory.ae_strongly_measurable' m g μdisjoint (function.support f) (function.support g)P (measure_theory.mem_ℒp.to_Lp f hf)P (measure_theory.mem_ℒp.to_Lp g hg)P (measure_theory.mem_ℒp.to_Lp f hf + measure_theory.mem_ℒp.to_Lp g hg)) (h_closed : is_closed {f : (measure_theory.Lp_meas F m p μ) | P f}) (f : (measure_theory.Lp F p μ)) :

Auxiliary lemma for Lp.induction_strongly_measurable.

theorem measure_theory.Lp.induction_strongly_measurable {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [fact (1 p)] [normed_space F] (hm : m m0) (hp_ne_top : p ) (P : (measure_theory.Lp F p μ) → Prop) (h_ind : ∀ (c : F) {s : set α} (hs : measurable_set s) (hμs : μ s < ), P (measure_theory.Lp.simple_func.indicator_const p _ _ c)) (h_add : ∀ ⦃f g : α → F⦄ (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ), measure_theory.strongly_measurable fmeasure_theory.strongly_measurable gdisjoint (function.support f) (function.support g)P (measure_theory.mem_ℒp.to_Lp f hf)P (measure_theory.mem_ℒp.to_Lp g hg)P (measure_theory.mem_ℒp.to_Lp f hf + measure_theory.mem_ℒp.to_Lp g hg)) (h_closed : is_closed {f : (measure_theory.Lp_meas F m p μ) | P f}) (f : (measure_theory.Lp F p μ)) :

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_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 fmeasure_theory.strongly_measurable gP fP gP (f + g)) (h_closed : is_closed {f : (measure_theory.Lp_meas F m p μ) | P f}) (h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] gmeasure_theory.mem_ℒp f p μP fP 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 𝕜] [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 𝕜] [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 𝕜] [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_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 𝕜] [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.ae_strongly_measurable'_condexp_L2 {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [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.integrable_on_condexp_L2_of_measure_ne_top {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [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 𝕜] [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 𝕜] [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.snorm_condexp_L2_le {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [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 𝕜] [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.inner_condexp_L2_left_eq_right {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f g : (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 𝕜] [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.inner_condexp_L2_eq_inner_fun {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f g : (measure_theory.Lp E 2 μ)) (hg : measure_theory.ae_strongly_measurable' m g μ) :
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 𝕜] [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 𝕜] [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 𝕜] [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 𝕜'] [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 𝕜] [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 𝕜] [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 𝕜] [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 𝕜] [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_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.ae_strongly_measurable'_condexp_ind_smul {α : Type u_1} {G : Type u_8} [normed_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.condexp_ind_smul_add {α : Type u_1} {G : Type u_8} [normed_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_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_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_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_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 ) :
theorem measure_theory.lintegral_nnnorm_condexp_ind_smul_le {α : Type u_1} {G : Type u_8} [normed_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) [measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.integrable_condexp_ind_smul {α : Type u_1} {G : Type u_8} [normed_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) :

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

theorem measure_theory.condexp_ind_smul_empty {α : Type u_1} {G : Type u_8} [normed_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} [normed_space G] {hm : m m0} {x : G} :
theorem measure_theory.set_integral_condexp_ind_smul {α : Type u_1} {G' : Type u_9} [normed_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

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_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_ae_eq_condexp_ind_smul {α : Type u_1} {G : Type u_8} [normed_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_add {α : Type u_1} {G : Type u_8} [normed_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_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_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_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_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_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_measurable_set_of_measure_ne_top {α : Type u_1} {G : Type u_8} [normed_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_of_measure_eq_top {α : Type u_1} {G : Type u_8} [normed_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_of_not_measurable_set {α : Type u_1} {G : Type u_8} [normed_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) (x : G) :
theorem measure_theory.condexp_ind_L1_add {α : Type u_1} {G : Type u_8} [normed_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (x y : G) :
theorem measure_theory.condexp_ind_L1_smul {α : Type u_1} {G : Type u_8} [normed_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_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.norm_condexp_ind_L1_le {α : Type u_1} {G : Type u_8} [normed_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (x : G) :
theorem measure_theory.continuous_condexp_ind_L1 {α : Type u_1} {G : Type u_8} [normed_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.condexp_ind_L1_disjoint_union {α : Type u_1} {G : Type u_8} [normed_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_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_ae_eq_condexp_ind_smul {α : Type u_1} {G : Type u_8} [normed_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.ae_strongly_measurable'_condexp_ind {α : Type u_1} {G : Type u_8} [normed_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) :
@[simp]
theorem measure_theory.condexp_ind_empty {α : Type u_1} {G : Type u_8} [normed_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.condexp_ind_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_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.norm_condexp_ind_apply_le {α : Type u_1} {G : Type u_8} [normed_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (x : G) :
theorem measure_theory.norm_condexp_ind_le {α : Type u_1} {G : Type u_8} [normed_group G] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} [normed_space G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.condexp_ind_disjoint_union_apply {α : Type u_1} {G : Type u_8} [normed_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_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_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_of_measurable {α : Type u_1} {G : Type u_8} [normed_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 : G) :
noncomputable def measure_theory.condexp_L1_clm {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] :

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_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.condexp_L1_clm_indicator_const_Lp {α : Type u_1} {F' : Type u_7} [normed_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 α} (hs : measurable_set s) (hμs : μ s ) (x : F') :
theorem measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top {α : Type u_1} {F' : Type u_7} [normed_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_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_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
theorem measure_theory.condexp_L1_undef {α : Type u_1} {F' : Type u_7} [normed_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'} (hf : ¬measure_theory.integrable f μ) :
theorem measure_theory.condexp_L1_zero {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.condexp_L1_congr_ae {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → F'} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (h : f =ᵐ[μ] g) :
theorem measure_theory.integrable_condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_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') :
theorem measure_theory.set_integral_condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_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_add {α : Type u_1} {F' : Type u_7} [normed_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 : measure_theory.integrable g μ) :
theorem measure_theory.condexp_L1_neg {α : Type u_1} {F' : Type u_7} [normed_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') :
theorem measure_theory.condexp_L1_smul {α : Type u_1} {F' : Type u_7} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_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') :
theorem measure_theory.condexp_L1_sub {α : Type u_1} {F' : Type u_7} [normed_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 : measure_theory.integrable g μ) :

Conditional expectation of a function #

noncomputable def measure_theory.condexp {α : Type u_1} {F' : Type u_7} [normed_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. Its value is 0 if the function is not integrable, if the σ-algebra is not a sub-σ-algebra or if the measure is not σ-finite on that σ-algebra.

Equations
theorem measure_theory.condexp_of_not_le {α : Type u_1} {F' : Type u_7} [normed_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_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_of_strongly_measurable {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space 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 : measure_theory.strongly_measurable f) (hfi : measure_theory.integrable f μ) :
theorem measure_theory.condexp_const {α : Type u_1} {F' : Type u_7} [normed_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_ae_eq_condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] (f : α → F') :
theorem measure_theory.condexp_undef {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} (hf : ¬measure_theory.integrable f μ) :
@[simp]
theorem measure_theory.condexp_zero {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} :
theorem measure_theory.condexp_congr_ae {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space 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_7} [normed_group F'] [normed_space 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 : measure_theory.ae_strongly_measurable' m f μ) (hfi : measure_theory.integrable f μ) :
theorem measure_theory.integrable_condexp {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space 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_7} [normed_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_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_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_add {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → F'} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
theorem measure_theory.condexp_smul {α : Type u_1} {F' : Type u_7} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_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_neg {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : α → F') :
theorem measure_theory.condexp_sub {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → F'} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
theorem measure_theory.condexp_condexp_of_le {α : Type u_1} {F' : Type u_7} [normed_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.condexp_ae_eq_restrict_zero {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} {s : set α} (hs : measurable_set s) (hf : f =ᵐ[μ.restrict s] 0) :
theorem measure_theory.condexp_indicator_aux {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} {s : set α} (hs : measurable_set s) (hf : f =ᵐ[μ.restrict s] 0) :

Auxiliary lemma for condexp_indicator.

theorem measure_theory.condexp_indicator {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} {s : set α} (hf_int : measure_theory.integrable f μ) (hs : measurable_set s) :

The conditional expectation of the indicator of a function over an m-measurable set with respect to the σ-algebra m is a.e. equal to the indicator of the conditional expectation.

theorem measure_theory.condexp_restrict_ae_eq_restrict {α : Type u_1} {F' : Type u_7} [normed_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)] (hs_m : measurable_set s) (hf_int : measure_theory.integrable f μ) :
theorem measure_theory.condexp_ae_eq_restrict_of_measurable_space_eq_on {α : Type u_1} {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space F'] {f : α → F'} {s : set α} {m m₂ m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (hm₂ : m₂ m0) [measure_theory.sigma_finite (μ.trim hm)] [measure_theory.sigma_finite (μ.trim hm₂)] (hs_m : measurable_set s) (hs : ∀ (t : set α), measurable_set (s t) measurable_set (s t)) :

If the restriction to a m-measurable set s of a σ-algebra m is equal to the restriction to s of another σ-algebra m₂ (hypothesis hs), then μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂].