mathlib3documentation

measure_theory.function.conditional_expectation.ae_measurable

Functions a.e. measurable with respect to a sub-σ-algebra #

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

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.

We define Lp_meas F 𝕜 m p μ, 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.

Main statements #

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

Lp.induction_strongly_measurable (see also mem_ℒp.induction_strongly_measurable): To prove something for an Lp function a.e. strongly measurable with respect to a sub-σ-algebra m in a normed space, it suffices to show that

• the property holds for (multiples of) characteristic functions which are measurable w.r.t. m;
• the set of functions in Lp strongly measurable w.r.t. m for which the property holds is closed.
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
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.comp_ae_measurable' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : measurable_space α} {mγ : measurable_space γ} {f : α β} {μ : measure_theory.measure γ} {g : γ α} (hg : μ) :
μ
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_3) (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_3) (𝕜 : Type u_5) [is_R_or_C 𝕜] [ 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_iff_ae_strongly_measurable' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ F] {m m0 : measurable_space α} {μ : measure_theory.measure α} (f : m p μ)) :
theorem measure_theory.mem_Lp_meas_self {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ F] {m0 : measurable_space α} (μ : measure_theory.measure α) (f : μ)) :
f m0 p μ
theorem measure_theory.Lp_meas_subgroup_coe {α : Type u_1} {F : Type u_3} {p : ennreal} {m m0 : measurable_space α} {μ : measure_theory.measure α} {f : μ)} :
theorem measure_theory.Lp_meas_coe {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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 isometry_equiv between Lp_meas_subgroup and the Lp space corresponding to the measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of Lp_meas_subgroup (and Lp_meas).

theorem measure_theory.mem_ℒp_trim_of_mem_Lp_meas_subgroup {α : Type u_1} {F : Type u_3} {p : ennreal} {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_3} {p : ennreal} {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_3) (p : ennreal) {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_3) (𝕜 : Type u_5) (p : ennreal) [is_R_or_C 𝕜] [ 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_3) (p : ennreal) {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_3) (𝕜 : Type u_5) (p : ennreal) [is_R_or_C 𝕜] [ 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_3} {p : ennreal} {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_3} {p : ennreal} {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_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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_3} {p : ennreal} {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_3} {p : ennreal} {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_3} {p : ennreal} {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_3} {p : ennreal} {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_3} {p : ennreal} {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_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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_3} {p : ennreal} {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_3} {p : ennreal} {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_3) (p : ennreal) {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_3) (𝕜 : Type u_5) (p : ennreal) [is_R_or_C 𝕜] [ 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_3) (𝕜 : Type u_5) (p : ennreal) [is_R_or_C 𝕜] [ 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_3} {p : ennreal} {m m0 : measurable_space α} {μ : measure_theory.measure α} [hm : fact (m m0)] [hp : fact (1 p)] :
@[protected, nolint, instance]
def measure_theory.Lp_meas.complete_space {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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_3} {p : ennreal} {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_3} {p : ennreal} {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_3} {𝕜 : Type u_5} {p : ennreal} [is_R_or_C 𝕜] [ 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_3} {p : ennreal} {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_3} {p : ennreal} {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_3} {p : ennreal} {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 : μ)) :

Auxiliary lemma for Lp.induction_strongly_measurable.

theorem measure_theory.Lp.induction_strongly_measurable {α : Type u_1} {F : Type u_3} {p : ennreal} {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 : μ)) :

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