# mathlibdocumentation

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 `L¹`.

The construction is done in four steps:

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

## Main results #

The conditional expectation and its properties

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

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

Uniqueness of the conditional expectation

• `Lp.ae_eq_of_forall_set_integral_eq'`: two `Lp` functions verifying the equality of integrals defining the conditional expectation are equal.
• `ae_eq_of_forall_set_integral_eq_of_sigma_finite'`: two functions verifying the equality of integrals defining the conditional expectation are equal almost everywhere. Requires `[sigma_finite (μ.trim hm)]`.
• `ae_eq_condexp_of_forall_set_integral_eq`: an a.e. `m`-measurable function which verifies the equality of integrals is a.e. equal to `condexp`.

## Notations #

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

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

## 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`:

• `condexp_L2` is defined only for an `inner_product_space` for now, and we use `𝕜` for its field.
• results about scalar multiplication are stated not only for `ℝ` but also for `𝕜` if we happen to have `normed_space 𝕜 F`.

## Tags #

conditional expectation, conditional expected value

def measure_theory.ae_strongly_measurable' {α : Type u_1} {β : Type u_2} (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
• = ∃ (g : α → β),
theorem measure_theory.ae_strongly_measurable'.congr {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} (hf : μ) (hfg : f =ᵐ[μ] g) :
theorem measure_theory.ae_strongly_measurable'.add {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} [has_add β] (hf : μ) (hg : μ) :
μ
theorem measure_theory.ae_strongly_measurable'.neg {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [add_group β] {f : α → β} (hfm : μ) :
theorem measure_theory.ae_strongly_measurable'.sub {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} [add_group β] {f g : α → β} (hfm : μ) (hgm : μ) :
μ
theorem measure_theory.ae_strongly_measurable'.const_smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} [ β] (c : 𝕜) (hf : μ) :
μ
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 𝕜] [ β] {f : α → β} (hfm : μ) (c : β) :
(λ (x : α), (f x)) μ
noncomputable def measure_theory.ae_strongly_measurable'.mk {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : α → β) (hfm : μ) :
α → β

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

Equations
theorem measure_theory.ae_strongly_measurable'.strongly_measurable_mk {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} (hfm : μ) :
theorem measure_theory.ae_strongly_measurable'.ae_eq_mk {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β} (hfm : μ) :
theorem measure_theory.ae_strongly_measurable'.continuous_comp {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} {γ : Type u_3} {f : α → β} {g : β → γ} (hg : continuous g) (hf : μ) :
μ
theorem measure_theory.ae_strongly_measurable'_of_ae_strongly_measurable'_trim {α : Type u_1} {β : Type u_2} {m m0 m0' : measurable_space α} (hm0 : m0 m0') {μ : measure_theory.measure α} {f : α → β} (hf : (μ.trim hm0)) :
theorem measure_theory.strongly_measurable.ae_strongly_measurable' {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → β}  :
theorem measure_theory.ae_eq_trim_iff_of_ae_strongly_measurable' {α : Type u_1} {β : Type u_2} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → β} (hm : m m0) (hfm : μ) (hgm : μ) :
f =ᵐ[μ] g
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 α} [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 : μ) (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 #

def measure_theory.Lp_meas_subgroup {α : Type u_1} (F : Type u_6) [normed_group F] (m : measurable_space α) (p : ennreal) (μ : measure_theory.measure α) :

`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] [ F] (m : 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_subgroup_iff_ae_strongly_measurable' {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : μ)} :
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : μ)} :
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (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] [ F] {m0 : measurable_space α} (μ : measure_theory.measure α) (f : μ)) :
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 : μ)} :
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {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] [ F] {m m0 : measurable_space α} (hm : m m0) {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (hμs : μ s ) {c : F} :
c p μ

## 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 : μ)) (hf_meas : f ) :
(μ.trim hm)

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`.

theorem measure_theory.mem_Lp_meas_subgroup_to_Lp_of_trim {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (μ.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 : μ)) :
(μ.trim hm))

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] [ F] {m m0 : measurable_space α} (μ : measure_theory.measure α) (hm : m m0) (f : m p μ)) :
(μ.trim hm))

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

Equations
• hm f =
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 : (μ.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] [ F] {m m0 : measurable_space α} (μ : measure_theory.measure α) (hm : m m0) (f : (μ.trim hm))) :
m p μ)

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

Equations
theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_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 : μ)) :
f) =ᵐ[μ] f
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 : (μ.trim hm))) :
f) =ᵐ[μ] f
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : m p μ)) :
hm f) =ᵐ[μ] f
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : (μ.trim hm))) :
hm f) =ᵐ[μ] f
theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_right_inv {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) :

`Lp_trim_to_Lp_meas_subgroup` is a right inverse of `Lp_meas_subgroup_to_Lp_trim`.

theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_left_inv {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) :

`Lp_trim_to_Lp_meas_subgroup` is a left inverse of `Lp_meas_subgroup_to_Lp_trim`.

theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_add {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f g : μ)) :
(f + g) = +
theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_neg {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
(-f) = -
theorem measure_theory.Lp_meas_subgroup_to_Lp_trim_sub {α : Type u_1} {F : Type u_6} {p : ennreal} [normed_group F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f g : μ)) :
(f - g) = -
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (c : 𝕜) (f : m p μ)) :
hm (c f) = c hm f
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 : μ)) :

`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) :
μ) ≃ᵢ (μ.trim hm))

`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] [ F] {m m0 : measurable_space α} (μ : measure_theory.measure α) [hp : fact (1 p)] :
μ) ≃ᵢ m 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] [ F] {m m0 : measurable_space α} (μ : measure_theory.measure α) [hp : fact (1 p)] (hm : m m0) :
m p μ) ≃ₗᵢ[𝕜] (μ.trim hm))

`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)] [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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} [hm : fact (m m0)] [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)] (hm : m m0) :
is_complete {f : μ) |
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)] (hm : m m0) :
is_closed {f : μ) |
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) :
∃ (g : α → F), 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)] [ F] {hm : m m0} {s : set α} {μ : measure_theory.measure α} (hs : measurable_set s) (hμs : (μ.trim hm) s ) (c : F) :
( hm).symm) hμs c)) =

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)] [ F] (hm : m m0) (f : α → F) (hf : (μ.trim hm)) :
( hm).symm) hf)) =
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)] [ F] (hm : m m0) (hp_ne_top : p ) (P : μ) → Prop) (h_ind : ∀ (c : F) {s : set α} (hs : (hμs : μ s < ), ) (h_add : ∀ ⦃f g : α → F⦄ (hf : μ) (hg : μ), P P P ) (h_closed : is_closed {f : p μ) | P f}) (f : μ)) :
P f

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)] [ F] (hm : m m0) (hp_ne_top : p ) (P : μ) → Prop) (h_ind : ∀ (c : F) {s : set α} (hs : (hμs : μ s < ), ) (h_add : ∀ ⦃f g : α → F⦄ (hf : μ) (hg : μ), P P P ) (h_closed : is_closed {f : p μ) | P f}) (f : μ)) :
P f

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`;
• 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)] [ F] (hm : m m0) (hp_ne_top : p ) (P : (α → F) → Prop) (h_ind : ∀ (c : F) ⦃s : set α⦄, μ s < P (s.indicator (λ (_x : α), c))) (h_add : ∀ ⦃f g : α → F⦄, P fP gP (f + g)) (h_closed : is_closed {f : p μ) | P f}) (h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] gP fP g) ⦃f : α → F⦄ (hf : μ) (hfm : μ) :
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`;
• 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 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : m p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), μ s < ) (hf_zero : ∀ (s : set α), μ 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 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), μ s < ) (hf_zero : ∀ (s : set α), μ s < (x : α) in s, f x μ = 0) (hf_meas : μ) :
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 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f g : p μ)) (hp_ne_zero : p 0) (hp_ne_top : p ) (hf_int_finite : ∀ (s : set α), μ s < ) (hg_int_finite : ∀ (s : set α), μ s < ) (hfg : ∀ (s : set α), μ s < (x : α) in s, f x μ = (x : α) in s, g x μ) (hf_meas : μ) (hg_meas : μ) :

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'] [ 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 α), μ s < ) (hg_int_finite : ∀ (s : set α), μ s < ) (hfg_eq : ∀ (s : set α), μ s < (x : α) in s, f x μ = (x : α) in s, g x μ) (hfm : μ) (hgm : μ) :
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 : α → } (hfi : μ) (hgi : μ) (hgf : ∀ (t : set α), μ 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 : α → } (hfi : μ) (hgi : μ) (hgf : ∀ (t : set α), μ 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 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) :
μ) →L[𝕜] m 2 μ)

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 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
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 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hμs : μ s ) (f : μ)) :
μ
theorem measure_theory.integrable_condexp_L2_of_is_finite_measure {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f : μ)} :
μ
theorem measure_theory.norm_condexp_L2_le_one {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ 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 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
theorem measure_theory.snorm_condexp_L2_le {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
2 μ
theorem measure_theory.norm_condexp_L2_coe_le {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) :
theorem measure_theory.inner_condexp_L2_left_eq_right {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) {f g : μ)} :
theorem measure_theory.condexp_L2_indicator_of_measurable {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (c : E) :
( c)) = c
theorem measure_theory.inner_condexp_L2_eq_inner_fun {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f g : μ)) (hg : μ) :
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 : μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ( 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 : μ)) :
∫⁻ (x : α) in s, ( f) x∥₊ μ ∫⁻ (x : α) in s, f x∥₊ μ
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 : μ)} (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 ) :
∫⁻ (a : α) in t, ( hμs 1)) a∥₊ μ μ (s t)
theorem measure_theory.condexp_L2_const_inner {α : Type u_1} {E : Type u_4} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (f : μ)) (c : E) :
( (measure_theory.mem_ℒp.to_Lp (λ (a : α), (f a)) _)) =ᵐ[μ] λ (a : α), (( f) a)

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

theorem measure_theory.integral_condexp_L2_eq {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (f : 2 μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ( 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 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {E'' : Type u_12} (𝕜' : Type u_13) [is_R_or_C 𝕜'] [ E''] [complete_space E''] [ E''] (hm : m m0) (T : E' →L[] E'') (f : 2 μ)) :
( hm) (T.comp_Lp f)) =ᵐ[μ] (T.comp_Lp ( f))
theorem measure_theory.condexp_L2_indicator_ae_eq_smul {α : Type u_1} {E' : Type u_5} (𝕜 : Type u_11) [is_R_or_C 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') :
( hμs x)) =ᵐ[μ] λ (a : α), ( hμs 1)) a x
theorem measure_theory.condexp_L2_indicator_eq_to_span_singleton_comp {α : Type u_1} {E' : Type u_5} (𝕜 : Type u_11) [is_R_or_C 𝕜] [ E'] [complete_space E'] [ E'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : E') :
( hμs x)) = ( hμs 1))
theorem measure_theory.set_lintegral_nnnorm_condexp_L2_indicator_le {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ 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 ) :
∫⁻ (a : α) in t, ( hμs x)) a∥₊ μ μ (s t) * x∥₊
theorem measure_theory.lintegral_nnnorm_condexp_L2_indicator_le {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ 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)] :
∫⁻ (a : α), ( hμs x)) a∥₊ μ μ s * x∥₊
theorem measure_theory.integrable_condexp_L2_indicator {α : Type u_1} {E' : Type u_5} {𝕜 : Type u_11} [is_R_or_C 𝕜] [ E'] [complete_space E'] [ 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 α} [ 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 α} [ 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 α} [ G] {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (x y : G) :
hμs (x + y) = hμs x + hμs y
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 α} [ G] {hm : m m0} (hs : measurable_set s) (hμs : μ s ) (c : ) (x : G) :
hμs (c x) = c hμs x
theorem measure_theory.condexp_ind_smul_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_group F] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [ F] [ F] (hs : measurable_set s) (hμs : μ s ) (c : 𝕜) (x : F) :
hμs (c x) = c hμs x
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 α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) :
hμs x) =ᵐ[μ] λ (a : α), ( hμs 1)) a x
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 α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) {t : set α} (ht : measurable_set t) (hμt : μ t ) :
∫⁻ (a : α) in t, hμs x) a∥₊ μ μ (s t) * x∥₊
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 α} [ G] (hm : m m0) (hs : measurable_set s) (hμs : μ s ) (x : G) [measure_theory.sigma_finite (μ.trim hm)] :
∫⁻ (a : α), hμs x) a∥₊ μ μ s * x∥₊
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 α} [ 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 α} [ G] {hm : m m0} {x : G} :
theorem measure_theory.set_integral_condexp_ind_smul {α : Type u_1} {G' : Type u_9} [normed_group G'] [ 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, 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 α} [ 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
• hμs x = _
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 α} [ G] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
hμs x) =ᵐ[μ] hμs x)
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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x y : G) :
hμs (x + y) = hμs x + hμs y
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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (c : ) (x : G) :
hμs (c x) = c hμs x
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] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [ F] [ F] (hs : measurable_set s) (hμs : μ s ) (c : 𝕜) (x : F) :
hμs (c x) = c hμs x
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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
hμs x (μ s).to_real * x
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 α} [ 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) :
= hμs x + hμt x
noncomputable def measure_theory.condexp_ind_L1 {α : Type u_1} {G : Type u_8} [normed_group G] [ 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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
x = hμs x
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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hμs : μ s = ) (x : G) :
x = 0
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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : ¬) (x : G) :
x = 0
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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (x y : G) :
(x + y) = x + y
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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : ) (x : G) :
(c x) = c x
theorem measure_theory.condexp_ind_L1_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_group F] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [ F] [ F] (c : 𝕜) (x : F) :
(c x) = c x
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 α} [ 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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
continuous (λ (x : G), x)
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 α} [ 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) :
(s t) x = x + x
noncomputable def measure_theory.condexp_ind {α : Type u_1} {G : Type u_8} [normed_group G] [ 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 α} [ G] (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (x : G) :
( s) x) =ᵐ[μ] hμs x)
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 α} [ 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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
= 0
theorem measure_theory.condexp_ind_smul' {α : Type u_1} {F : Type u_6} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_group F] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] [ F] [ F] (c : 𝕜) (x : F) :
s) (c x) = c s) x
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 α} [ 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 α} [ 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 α} [ 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) :
(s t)) x = s) x + t) x
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 α} [ 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 = ) :
(s t) = +
theorem measure_theory.dominated_fin_meas_additive_condexp_ind {α : Type u_1} (G : Type u_8) [normed_group G] {m m0 : measurable_space α} [ G] (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.set_integral_condexp_ind {α : Type u_1} {G' : Type u_9} [normed_group G'] [ 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, ( 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 α} [ G] {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (hs : measurable_set s) (hμs : μ s ) (c : G) :
s) c = c
noncomputable def measure_theory.condexp_L1_clm {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] :
1 μ) →L[] 1 μ)

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'] [ F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : 𝕜) (f : 1 μ)) :
(c f) = c f
theorem measure_theory.condexp_L1_clm_indicator_const_Lp {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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') :
hμs x) = s) x
theorem measure_theory.condexp_L1_clm_indicator_const {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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') :
x) = s) x
theorem measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {s : set α} (f : 1 μ)) (hs : measurable_set s) (hμs : μ s ) :
(x : α) in s, ( 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'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {s : set α} (f : 1 μ)) (hs : measurable_set s) :
(x : α) in s, ( 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`.

theorem measure_theory.ae_strongly_measurable'_condexp_L1_clm {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : 1 μ)) :
theorem measure_theory.condexp_L1_clm_Lp_meas {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : m 1 μ)) :
f = f
theorem measure_theory.condexp_L1_clm_of_ae_strongly_measurable' {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : 1 μ)) (hfm : μ) :
f = f
noncomputable def measure_theory.condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} (hm : m m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite (μ.trim hm)] (f : α → F') :
1 μ)

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
• = f
theorem measure_theory.condexp_L1_undef {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hf : ¬) :
= 0
theorem measure_theory.condexp_L1_eq {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hf : μ) :
=
theorem measure_theory.condexp_L1_zero {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] :
= 0
theorem measure_theory.ae_strongly_measurable'_condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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_congr_ae {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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'] [ 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'] [ 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 : μ) (hs : measurable_set s) :
(x : α) in s, 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'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f g : α → F'} (hf : μ) (hg : μ) :
(f + g) = +
theorem measure_theory.condexp_L1_neg {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (f : α → 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'] [ F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] (c : 𝕜) (f : α → F') :
(c f) = c
theorem measure_theory.condexp_L1_sub {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f g : α → F'} (hf : μ) (hg : μ) :
(f - g) = -
theorem measure_theory.condexp_L1_of_ae_strongly_measurable' {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hfm : μ) (hfi : μ) :
f) =ᵐ[μ] f

### Conditional expectation of a function #

noncomputable def measure_theory.condexp {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} (hm_not : ¬m m0) :
= 0
theorem measure_theory.condexp_of_not_sigma_finite {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} (hm : m m0) (hμm_not : ¬) :
= 0
theorem measure_theory.condexp_of_sigma_finite {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] :
theorem measure_theory.condexp_of_strongly_measurable {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hfi : μ) :
= f
theorem measure_theory.condexp_const {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) (c : F')  :
(λ (x : α), c) = λ (_x : α), c
theorem measure_theory.condexp_ae_eq_condexp_L1 {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] (f : α → F') :
=ᵐ[μ] f)
theorem measure_theory.condexp_ae_eq_condexp_L1_clm {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hf : μ) :
theorem measure_theory.condexp_undef {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} (hf : ¬) :
=ᵐ[μ] 0
@[simp]
theorem measure_theory.condexp_zero {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} :
= 0
theorem measure_theory.strongly_measurable_condexp {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} :
theorem measure_theory.condexp_congr_ae {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (hm : m m0) [hμm : measure_theory.sigma_finite (μ.trim hm)] {f : α → F'} (hf : μ) (hfi : μ) :
=ᵐ[μ] f
theorem measure_theory.integrable_condexp {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} {s : set α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (hf : μ) (hs : measurable_set s) :
(x : α) in s, x μ = (x : α) in s, f x μ

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

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

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

theorem measure_theory.condexp_add {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → F'} (hf : μ) (hg : μ) :
(f + g) =ᵐ[μ] +
theorem measure_theory.condexp_smul {α : Type u_1} {F' : Type u_7} {𝕜 : Type u_11} [is_R_or_C 𝕜] [normed_group F'] [ F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (c : 𝕜) (f : α → F') :
(c f) =ᵐ[μ] c
theorem measure_theory.condexp_neg {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : α → F') :
(-f) =ᵐ[μ] -
theorem measure_theory.condexp_sub {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → F'} (hf : μ) (hg : μ) :
(f - g) =ᵐ[μ] -
theorem measure_theory.condexp_condexp_of_le {α : Type u_1} {F' : Type u_7} [normed_group F'] [ F'] [complete_space F'] {f : α → F'} {m₁ m₂ m0 : measurable_space α} {μ : measure_theory.measure α} (hm₁₂ : m₁ m₂) (hm₂ : m₂ m0) [measure_theory.sigma_finite (μ.trim hm₂)] :
f) =ᵐ[μ] f
theorem measure_theory.rn_deriv_ae_eq_condexp {α : Type u_1} {m m0 : measurable_space α} {μ : measure_theory.measure α} {hm : m m0} [hμm : measure_theory.sigma_finite (μ.trim hm)] {f : α → } (hf : μ) :
(μ.trim hm) =ᵐ[μ]
theorem measure_theory.condexp_ae_eq_restrict_zero {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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'] [ F'] [complete_space F'] {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → F'} {s : set α} (hs : measurable_set s) (hf : f =ᵐ[μ.restrict s] 0) :
(s.indicator f) =ᵐ[μ] s.indicator f)

Auxiliary lemma for `condexp_indicator`.

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

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'] [ 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 : μ) :
(μ.restrict s) f =ᵐ[μ.restrict s]
theorem measure_theory.condexp_ae_eq_restrict_of_measurable_space_eq_on {α : Type u_1} {F' : Type u_7} [normed_group F'] [ 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₂]`.