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 MemLp.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; - is closed under addition;
- the set of functions in
Lpstrongly measurable w.r.t.mfor which the property holds is closed.
theorem
MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
[TopologicalSpace.MetrizableSpace β]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f g : α → β}
(hm : m ≤ m0)
(hfm : AEStronglyMeasurable f μ)
(hgm : AEStronglyMeasurable g μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.comp_ae_measurable'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace β]
{mα : MeasurableSpace α}
{x✝ : MeasurableSpace γ}
{f : α → β}
{μ : Measure γ}
{g : γ → α}
(hf : AEStronglyMeasurable f (Measure.map g μ))
(hg : AEMeasurable g μ)
:
AEStronglyMeasurable (f ∘ g) μ
def
MeasureTheory.lpMeasSubgroup
{α : Type u_1}
(F : Type u_2)
[NormedAddCommGroup F]
(m : MeasurableSpace α)
[MeasurableSpace α]
(p : ENNReal)
(μ : Measure α)
:
AddSubgroup ↥(Lp F p μ)
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
Instances For
def
MeasureTheory.lpMeas
{α : Type u_1}
(F : Type u_2)
(𝕜 : Type u_3)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(m : MeasurableSpace α)
[MeasurableSpace α]
(p : ENNReal)
(μ : Measure α)
:
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
Instances For
theorem
MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f : ↥(Lp F p μ)}
:
theorem
MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
{f : ↥(Lp F p μ)}
:
theorem
MeasureTheory.lpMeas.aestronglyMeasurable
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m x✝ : MeasurableSpace α}
{μ : Measure α}
(f : ↥(lpMeas F 𝕜 m p μ))
:
AEStronglyMeasurable (↑↑↑f) μ
theorem
MeasureTheory.mem_lpMeas_self
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m0 : MeasurableSpace α}
(μ : Measure α)
(f : ↥(Lp F p μ))
:
theorem
MeasureTheory.mem_lpMeas_indicatorConstLp
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
{μ : Measure α}
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
{c : F}
:
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.memLp_trim_of_mem_lpMeasSubgroup
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(Lp F p μ))
(hf_meas : f ∈ lpMeasSubgroup F m p μ)
:
MemLp (Exists.choose ⋯) 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_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(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_2)
(p : ENNReal)
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
(hm : m ≤ m0)
(f : ↥(lpMeasSubgroup F m p μ))
:
Map from lpMeasSubgroup to Lp F p (μ.trim hm).
Equations
Instances For
noncomputable def
MeasureTheory.lpMeasToLpTrim
{α : Type u_1}
(F : Type u_2)
(𝕜 : Type u_3)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
(hm : m ≤ m0)
(f : ↥(lpMeas F 𝕜 m p μ))
:
Map from lpMeas to Lp F p (μ.trim hm).
Equations
Instances For
noncomputable def
MeasureTheory.lpTrimToLpMeasSubgroup
{α : Type u_1}
(F : Type u_2)
(p : ENNReal)
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
(hm : m ≤ m0)
(f : ↥(Lp F p (μ.trim hm)))
:
↥(lpMeasSubgroup F m p μ)
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_2)
(𝕜 : Type u_3)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
(hm : m ≤ m0)
(f : ↥(Lp F p (μ.trim hm)))
:
↥(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_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(lpMeasSubgroup F m p μ))
:
theorem
MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(Lp F p (μ.trim hm)))
:
theorem
MeasureTheory.lpMeasToLpTrim_ae_eq
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(lpMeas F 𝕜 m p μ))
:
theorem
MeasureTheory.lpTrimToLpMeas_ae_eq
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(Lp F p (μ.trim hm)))
:
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_right_inv
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
:
Function.RightInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm)
lpTrimToLpMeasSubgroup is a right inverse of lpMeasSubgroupToLpTrim.
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_left_inv
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
:
Function.LeftInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm)
lpTrimToLpMeasSubgroup is a left inverse of lpMeasSubgroupToLpTrim.
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_add
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f g : ↥(lpMeasSubgroup F m p μ))
:
lpMeasSubgroupToLpTrim F p μ hm (f + g) = lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_neg
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(lpMeasSubgroup F m p μ))
:
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_sub
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f g : ↥(lpMeasSubgroup F m p μ))
:
lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g
theorem
MeasureTheory.lpMeasToLpTrim_smul
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(c : 𝕜)
(f : ↥(lpMeas F 𝕜 m p μ))
:
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_norm_map
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[hp : Fact (1 ≤ p)]
(hm : m ≤ m0)
(f : ↥(lpMeasSubgroup F m p μ))
:
lpMeasSubgroupToLpTrim preserves the norm.
theorem
MeasureTheory.isometry_lpMeasSubgroupToLpTrim
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[hp : Fact (1 ≤ p)]
(hm : m ≤ m0)
:
Isometry (lpMeasSubgroupToLpTrim F p μ hm)
noncomputable def
MeasureTheory.lpMeasSubgroupToLpTrimIso
{α : Type u_1}
(F : Type u_2)
(p : ENNReal)
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
[Fact (1 ≤ p)]
(hm : m ≤ m0)
:
lpMeasSubgroup and Lp F p (μ.trim hm) are isometric.
Equations
Instances For
noncomputable def
MeasureTheory.lpMeasSubgroupToLpMeasIso
{α : Type u_1}
(F : Type u_2)
(𝕜 : Type u_3)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
[Fact (1 ≤ p)]
:
lpMeasSubgroup and lpMeas are isometric.
Equations
Instances For
noncomputable def
MeasureTheory.lpMeasToLpTrimLie
{α : Type u_1}
(F : Type u_2)
(𝕜 : Type u_3)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
[Fact (1 ≤ p)]
(hm : m ≤ m0)
:
lpMeas and Lp F p (μ.trim hm) are isometric, with a linear equivalence.
Equations
Instances For
instance
MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[hm : Fact (m ≤ m0)]
[CompleteSpace F]
[hp : Fact (1 ≤ p)]
:
CompleteSpace ↥(lpMeasSubgroup F m p μ)
instance
MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[hm : Fact (m ≤ m0)]
[CompleteSpace F]
[hp : Fact (1 ≤ p)]
:
CompleteSpace ↥(lpMeas F 𝕜 m p μ)
theorem
MeasureTheory.isComplete_aestronglyMeasurable
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[hp : Fact (1 ≤ p)]
[CompleteSpace F]
(hm : m ≤ m0)
:
IsComplete {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑↑f) μ}
theorem
MeasureTheory.isClosed_aestronglyMeasurable
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[Fact (1 ≤ p)]
[CompleteSpace F]
(hm : m ≤ m0)
:
theorem
MeasureTheory.lpMeas.ae_fin_strongly_measurable'
{α : Type u_1}
{F : Type u_2}
{𝕜 : Type u_3}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(lpMeas F 𝕜 m p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
We do not get ae_fin_strongly_measurable f (μ.trim hm), since we don't have
f =ᵐ[μ.trim hm] Lp_meas_to_Lp_trim F 𝕜 p μ hm f but only the weaker
f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f.
theorem
MeasureTheory.lpMeasToLpTrimLie_symm_indicator
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
[one_le_p : Fact (1 ≤ p)]
[NormedSpace ℝ F]
{hm : m ≤ m0}
{s : Set α}
{μ : Measure α}
(hs : MeasurableSet s)
(hμs : (μ.trim hm) s ≠ ⊤)
(c : F)
:
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_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[one_le_p : Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(f : α → F)
(hf : MemLp f p (μ.trim hm))
:
theorem
MeasureTheory.Lp.induction_stronglyMeasurable_aux
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c))
(h_add :
∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
AEStronglyMeasurable f μ →
AEStronglyMeasurable g μ →
Disjoint (Function.support f) (Function.support g) →
P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg))
(h_closed : IsClosed {f : ↥(lpMeas F ℝ m p μ) | P ↑f})
(f : ↥(Lp F p μ))
:
AEStronglyMeasurable (↑↑f) μ → P f
Auxiliary lemma for Lp.induction_stronglyMeasurable.
theorem
MeasureTheory.Lp.induction_stronglyMeasurable
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c))
(h_add :
∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
StronglyMeasurable f →
StronglyMeasurable g →
Disjoint (Function.support f) (Function.support g) →
P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg))
(h_closed : IsClosed {f : ↥(lpMeas F ℝ m p μ) | P ↑f})
(f : ↥(Lp F p μ))
:
AEStronglyMeasurable (↑↑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; - is closed under addition;
- the set of functions in
Lpstrongly measurable w.r.t.mfor which the property holds is closed.
theorem
MeasureTheory.MemLp.induction_stronglyMeasurable
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : (α → F) → Prop)
(h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun (x : α) => c))
(h_add :
∀ ⦃f g : α → F⦄,
Disjoint (Function.support f) (Function.support g) →
MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g))
(h_closed : IsClosed {f : ↥(lpMeas F ℝ m p μ) | P ↑↑↑f})
(h_ae : ∀ ⦃f g : α → F⦄, f =ᶠ[ae μ] g → MemLp f p μ → P f → P g)
⦃f : α → F⦄
:
MemLp f p μ → AEStronglyMeasurable f μ → P f
To prove something for an arbitrary MemLp 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.mfor which the property holds is closed. - the property is closed under the almost-everywhere equal relation.