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

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

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

## Main statements #

We define an IsometryEquiv between lpMeasSubgroup and the Lp space corresponding to the measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of lpMeas.

Lp.induction_stronglyMeasurable (see also Memℒp.induction_stronglyMeasurable): 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 MeasureTheory.AEStronglyMeasurable' {α : Type u_1} {β : Type u_2} [] (m : ) :
{x : } → (αβ)

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

Equations
• = ∃ (g : αβ),
Instances For
theorem MeasureTheory.AEStronglyMeasurable'.congr {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {f : αβ} {g : αβ} (hf : ) (hfg : f =ᵐ[μ] g) :
theorem MeasureTheory.AEStronglyMeasurable'.mono {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {f : αβ} {m' : } (hf : ) (hm : m m') :
theorem MeasureTheory.AEStronglyMeasurable'.add {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {f : αβ} {g : αβ} [Add β] [] (hf : ) (hg : ) :
theorem MeasureTheory.AEStronglyMeasurable'.neg {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] [] {f : αβ} (hfm : ) :
theorem MeasureTheory.AEStronglyMeasurable'.sub {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] [] {f : αβ} {g : αβ} (hfm : ) (hgm : ) :
theorem MeasureTheory.AEStronglyMeasurable'.const_smul {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} {m : } {m0 : } {μ : } [] {f : αβ} [SMul 𝕜 β] [] (c : 𝕜) (hf : ) :
theorem MeasureTheory.AEStronglyMeasurable'.const_inner {α : Type u_1} {m : } {m0 : } {μ : } {𝕜 : Type u_4} {β : Type u_5} [] [] {f : αβ} (hfm : ) (c : β) :
MeasureTheory.AEStronglyMeasurable' m (fun (x : α) => c, f x⟫_𝕜) μ
@[simp]
theorem MeasureTheory.AEStronglyMeasurable'.of_subsingleton {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {f : αβ} [] :
@[simp]
theorem MeasureTheory.AEStronglyMeasurable'.of_subsingleton' {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {f : αβ} [] :
noncomputable def MeasureTheory.AEStronglyMeasurable'.mk {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] (f : αβ) (hfm : ) :
αβ

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

Equations
Instances For
theorem MeasureTheory.AEStronglyMeasurable'.stronglyMeasurable_mk {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {f : αβ} (hfm : ) :
theorem MeasureTheory.AEStronglyMeasurable'.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {f : αβ} (hfm : ) :
theorem MeasureTheory.AEStronglyMeasurable'.continuous_comp {α : Type u_1} {β : Type u_2} {m : } {m0 : } {μ : } [] {γ : Type u_4} [] {f : αβ} {g : βγ} (hg : ) (hf : ) :
theorem MeasureTheory.aeStronglyMeasurable'_of_aeStronglyMeasurable'_trim {α : Type u_1} {β : Type u_2} {m : } {m0 : } {m0' : } [] (hm0 : m0 m0') {μ : } {f : αβ} (hf : MeasureTheory.AEStronglyMeasurable' m f (μ.trim hm0)) :
theorem MeasureTheory.StronglyMeasurable.aeStronglyMeasurable' {α : Type u_1} {β : Type u_2} {m : } :
∀ {x : } [inst : ] {μ : } {f : αβ},
theorem MeasureTheory.ae_eq_trim_iff_of_aeStronglyMeasurable' {α : Type u_1} {β : Type u_2} [] {m : } {m0 : } {μ : } {f : αβ} {g : αβ} (hm : m m0) (hfm : ) (hgm : ) :
=ᵐ[μ.trim hm] f =ᵐ[μ] g
theorem MeasureTheory.AEStronglyMeasurable.comp_ae_measurable' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {mα : } :
∀ {x : } {f : αβ} {μ : } {g : γα},
theorem MeasureTheory.AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on {α : Type u_1} {E : Type u_2} {m : } {m₂ : } {m0 : } {μ : } [] [Zero E] (hm : m m0) {s : Set α} {f : αE} (hs_m : ) (hs : ∀ (t : Set α), MeasurableSet (s t)MeasurableSet (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 lpMeas of Lp functions a.e. measurable with respect to a sub-sigma-algebra #

def MeasureTheory.lpMeasSubgroup {α : Type u_1} (F : Type u_3) (m : ) [] (p : ENNReal) (μ : ) :
AddSubgroup { x : α →ₘ[μ] F // x }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MeasureTheory.lpMeas {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) [] [] (m : ) [] (p : ENNReal) (μ : ) :
Submodule 𝕜 { x : α →ₘ[μ] F // x }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MeasureTheory.mem_lpMeasSubgroup_iff_aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } {f : { x : α →ₘ[μ] F // x }} :
f
theorem MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } {m0 : } {μ : } {f : { x : α →ₘ[μ] F // x }} :
f MeasureTheory.lpMeas F 𝕜 m p μ
theorem MeasureTheory.lpMeas.aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } :
∀ {x : } {μ : } (f : { x_1 : { x_1 : α →ₘ[μ] F // x_1 } // x_1 MeasureTheory.lpMeas F 𝕜 m p μ }),
theorem MeasureTheory.mem_lpMeas_self {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m0 : } (μ : ) (f : { x : α →ₘ[μ] F // x }) :
f MeasureTheory.lpMeas F 𝕜 m0 p μ
theorem MeasureTheory.lpMeasSubgroup_coe {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } :
∀ {x : } {μ : } {f : { x_1 : { x_1 : α →ₘ[μ] F // x_1 } // x_1 }}, f = f
theorem MeasureTheory.lpMeas_coe {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } :
∀ {x : } {μ : } {f : { x_1 : { x_1 : α →ₘ[μ] F // x_1 } // x_1 MeasureTheory.lpMeas F 𝕜 m p μ }}, f = f
theorem MeasureTheory.mem_lpMeas_indicatorConstLp {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } {m0 : } (hm : m m0) {μ : } {s : Set α} (hs : ) (hμs : μ s ) {c : F} :
MeasureTheory.lpMeas F 𝕜 m p μ

## The subspace lpMeas is complete. #

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

theorem MeasureTheory.memℒp_trim_of_mem_lpMeasSubgroup {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) (f : { x : α →ₘ[μ] F // x }) (hf_meas : f ) :
MeasureTheory.Memℒp p (μ.trim hm)

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

theorem MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) (f : { x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }) :

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

noncomputable def MeasureTheory.lpMeasSubgroupToLpTrim {α : Type u_1} (F : Type u_3) (p : ENNReal) {m : } {m0 : } (μ : ) (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x }) :
{ x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }

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

Equations
Instances For
noncomputable def MeasureTheory.lpMeasToLpTrim {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [] [] {m : } {m0 : } (μ : ) (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ }) :
{ x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }

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

Equations
Instances For
noncomputable def MeasureTheory.lpTrimToLpMeasSubgroup {α : Type u_1} (F : Type u_3) (p : ENNReal) {m : } {m0 : } (μ : ) (hm : m m0) (f : { x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }) :
{ x : { x : α →ₘ[μ] F // x } // x }

Map from Lp F p (μ.trim hm) to lpMeasSubgroup, inverse of lpMeasSubgroupToLpTrim.

Equations
• = ⟨,
Instances For
noncomputable def MeasureTheory.lpTrimToLpMeas {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [] [] {m : } {m0 : } (μ : ) (hm : m m0) (f : { x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }) :
{ x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ }

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

Equations
Instances For
theorem MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x }) :
=ᵐ[μ] f
theorem MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) (f : { x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }) :
=ᵐ[μ] f
theorem MeasureTheory.lpMeasToLpTrim_ae_eq {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ }) :
(MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f) =ᵐ[μ] f
theorem MeasureTheory.lpTrimToLpMeas_ae_eq {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }) :
(MeasureTheory.lpTrimToLpMeas F 𝕜 p μ hm f) =ᵐ[μ] f
theorem MeasureTheory.lpMeasSubgroupToLpTrim_right_inv {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) :

lpTrimToLpMeasSubgroup is a right inverse of lpMeasSubgroupToLpTrim.

theorem MeasureTheory.lpMeasSubgroupToLpTrim_left_inv {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) :

lpTrimToLpMeasSubgroup is a left inverse of lpMeasSubgroupToLpTrim.

theorem MeasureTheory.lpMeasSubgroupToLpTrim_add {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x }) (g : { x : { x : α →ₘ[μ] F // x } // x }) :
theorem MeasureTheory.lpMeasSubgroupToLpTrim_neg {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x }) :
= -
theorem MeasureTheory.lpMeasSubgroupToLpTrim_sub {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x }) (g : { x : { x : α →ₘ[μ] F // x } // x }) :
theorem MeasureTheory.lpMeasToLpTrim_smul {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } {m0 : } {μ : } (hm : m m0) (c : 𝕜) (f : { x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ }) :
MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm (c f) = c MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f
theorem MeasureTheory.lpMeasSubgroupToLpTrim_norm_map {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [hp : Fact (1 p)] (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x }) :

lpMeasSubgroupToLpTrim preserves the norm.

theorem MeasureTheory.isometry_lpMeasSubgroupToLpTrim {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [hp : Fact (1 p)] (hm : m m0) :
noncomputable def MeasureTheory.lpMeasSubgroupToLpTrimIso {α : Type u_1} (F : Type u_3) (p : ENNReal) {m : } {m0 : } (μ : ) [Fact (1 p)] (hm : m m0) :
{ x : { x : α →ₘ[μ] F // x } // x } ≃ᵢ { x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def MeasureTheory.lpMeasSubgroupToLpMeasIso {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [] [] {m : } {m0 : } (μ : ) [Fact (1 p)] :
{ x : { x : α →ₘ[μ] F // x } // x } ≃ᵢ { x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ }

lpMeasSubgroup and lpMeas are isometric.

Equations
Instances For
noncomputable def MeasureTheory.lpMeasToLpTrimLie {α : Type u_1} (F : Type u_3) (𝕜 : Type u_5) (p : ENNReal) [] [] {m : } {m0 : } (μ : ) [Fact (1 p)] (hm : m m0) :
{ x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ } ≃ₗᵢ[𝕜] { x : α →ₘ[μ.trim hm] F // x MeasureTheory.Lp F p (μ.trim hm) }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [hm : Fact (m m0)] [] [hp : Fact (1 p)] :
CompleteSpace { x : { x : α →ₘ[μ] F // x } // x }
Equations
• =
instance MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } {m0 : } {μ : } [hm : Fact (m m0)] [] [hp : Fact (1 p)] :
CompleteSpace { x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ }
Equations
• =
theorem MeasureTheory.isComplete_aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [hp : Fact (1 p)] [] (hm : m m0) :
IsComplete {f : { x : α →ₘ[μ] F // x } | }
theorem MeasureTheory.isClosed_aeStronglyMeasurable' {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [Fact (1 p)] [] (hm : m m0) :
IsClosed {f : { x : α →ₘ[μ] F // x } | }
theorem MeasureTheory.lpMeas.ae_fin_strongly_measurable' {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [] [] {m : } {m0 : } {μ : } (hm : m m0) (f : { x : { x : α →ₘ[μ] F // x } // x MeasureTheory.lpMeas F 𝕜 m p μ }) (hp_ne_zero : p 0) (hp_ne_top : p ) :
∃ (g : αF), MeasureTheory.FinStronglyMeasurable 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 MeasureTheory.lpMeasToLpTrimLie_symm_indicator {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } [one_le_p : Fact (1 p)] [] {hm : m m0} {s : Set α} {μ : } (hs : ) (hμs : (μ.trim hm) s ) (c : F) :
(.symm (MeasureTheory.indicatorConstLp p hs hμs c)) =

When applying the inverse of lpMeasToLpTrimLie (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 MeasureTheory.lpMeasToLpTrimLie_symm_toLp {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [one_le_p : Fact (1 p)] [] (hm : m m0) (f : αF) (hf : MeasureTheory.Memℒp f p (μ.trim hm)) :
(.symm ) =
theorem MeasureTheory.Lp.induction_stronglyMeasurable_aux {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [Fact (1 p)] [] (hm : m m0) (hp_ne_top : p ) (P : { x : α →ₘ[μ] F // x }Prop) (h_ind : ∀ (c : F) {s : Set α} (hs : ) (hμs : μ s < ), P ) (h_add : ∀ ⦃f g : αF⦄ (hf : ) (hg : ), P P P ) (h_closed : IsClosed {f : { x : { x : α →ₘ[μ] F // x } // x } | P f}) (f : { x : α →ₘ[μ] F // x }) :
P f

Auxiliary lemma for Lp.induction_stronglyMeasurable.

theorem MeasureTheory.Lp.induction_stronglyMeasurable {α : Type u_1} {F : Type u_3} {p : ENNReal} {m : } {m0 : } {μ : } [Fact (1 p)] [] (hm : m m0) (hp_ne_top : p ) (P : { x : α →ₘ[μ] F // x }Prop) (h_ind : ∀ (c : F) {s : Set α} (hs : ) (hμs : μ s < ), P ) (h_add : ∀ ⦃f g : αF⦄ (hf : ) (hg : ), P P P ) (h_closed : IsClosed {f : { x : { x : α →ₘ[μ] F // x } // x } | P f}) (f : { x : α →ₘ[μ] F // x }) :
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.
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.