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.
@[deprecated MeasureTheory.AEStronglyMeasurable (since := "2025-01-23")]
def
MeasureTheory.AEStronglyMeasurable'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
(m : MeasurableSpace α)
{x✝ : MeasurableSpace α}
(f : α → β)
(μ : Measure α)
:
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
@[deprecated MeasureTheory.AEStronglyMeasurable.congr (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.congr
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f g : α → β}
(hf : AEStronglyMeasurable f μ)
(hfg : f =ᶠ[ae μ] g)
:
@[deprecated MeasureTheory.AEStronglyMeasurable.mono (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.mono
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
{m' : MeasurableSpace α}
(hf : AEStronglyMeasurable f μ)
(hm : m ≤ m')
:
@[deprecated MeasureTheory.AEStronglyMeasurable.add (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.add
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f g : α → β}
[Add β]
[ContinuousAdd β]
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
:
AEStronglyMeasurable (f + g) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.neg (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.neg
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
[Neg β]
[ContinuousNeg β]
{f : α → β}
(hfm : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (-f) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.sub (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.sub
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
[AddGroup β]
[IsTopologicalAddGroup β]
{f g : α → β}
(hfm : AEStronglyMeasurable f μ)
(hgm : AEStronglyMeasurable g μ)
:
AEStronglyMeasurable (f - g) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.const_smul (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.const_smul
{α : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[SMul 𝕜 β]
[ContinuousConstSMul 𝕜 β]
(c : 𝕜)
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (c • f) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.const_inner (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.const_inner
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_4}
{β : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup β]
[InnerProductSpace 𝕜 β]
{f : α → β}
(hfm : AEStronglyMeasurable f μ)
(c : β)
:
AEStronglyMeasurable (fun (x : α) => inner 𝕜 c (f x)) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.of_subsingleton_cod (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.of_subsingleton
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Subsingleton β]
:
@[deprecated MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.of_subsingleton'
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Subsingleton α]
:
@[deprecated MeasureTheory.AEStronglyMeasurable.mk (since := "2025-01-23")]
noncomputable def
MeasureTheory.AEStronglyMeasurable'.mk
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
(f : α → β)
(hfm : AEStronglyMeasurable f μ)
:
α → β
An m-strongly measurable function almost everywhere equal to f.
Equations
@[deprecated MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.stronglyMeasurable_mk
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
(hfm : AEStronglyMeasurable f μ)
:
@[deprecated MeasureTheory.AEStronglyMeasurable.ae_eq_mk (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
(hfm : AEStronglyMeasurable f μ)
:
@[deprecated Continuous.comp_aestronglyMeasurable (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.continuous_comp
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{γ : Type u_4}
[TopologicalSpace γ]
{f : α → β}
{g : β → γ}
(hg : Continuous g)
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (g ∘ f) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.of_trim (since := "2025-01-23")]
theorem
MeasureTheory.aeStronglyMeasurable'_of_aeStronglyMeasurable'_trim
{α : Type u_1}
{β : Type u_2}
{m m0 m0' : MeasurableSpace α}
[TopologicalSpace β]
(hm0 : m0 ≤ m0')
{μ : Measure α}
{f : α → β}
(hf : AEStronglyMeasurable f (μ.trim hm0))
:
@[deprecated MeasureTheory.StronglyMeasurable.aestronglyMeasurable (since := "2025-01-23")]
theorem
MeasureTheory.StronglyMeasurable.aeStronglyMeasurable'
{α : Type u_1}
{β : Type u_2}
{m x✝ : MeasurableSpace α}
[TopologicalSpace β]
{μ : Measure α}
{f : α → β}
(hf : StronglyMeasurable f)
:
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 μ)
:
@[deprecated MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable (since := "2025-04-09")]
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 μ)
:
Alias of MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable.
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) μ
@[deprecated MeasureTheory.AEStronglyMeasurable.of_measurableSpace_le_on (since := "2025-01-23")]
theorem
MeasureTheory.AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on
{α : Type u_1}
{E : Type u_2}
{m m₂ m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace E]
[Zero E]
(hm : m ≤ m0)
{s : Set α}
{f : α → E}
(hs_m : MeasurableSet s)
(hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t))
(hf : AEStronglyMeasurable f μ)
(hf_zero : f =ᶠ[ae (μ.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.
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
- MeasureTheory.lpMeasSubgroup F m p μ = { carrier := {f : ↥(MeasureTheory.Lp F p μ) | MeasureTheory.AEStronglyMeasurable (↑↑f) μ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
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
- MeasureTheory.lpMeas F 𝕜 m p μ = { carrier := {f : ↥(MeasureTheory.Lp F p μ) | MeasureTheory.AEStronglyMeasurable (↑↑f) μ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
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 μ)}
:
@[deprecated MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable (since := "2025-01-24")]
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 μ)}
:
Alias of MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable.
@[deprecated MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable (since := "2025-04-09")]
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 μ)}
:
Alias of MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable.
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 μ)}
:
@[deprecated MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable (since := "2025-01-24")]
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 μ)}
:
@[deprecated MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable (since := "2025-04-09")]
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) μ
@[deprecated MeasureTheory.lpMeas.aestronglyMeasurable (since := "2025-01-24")]
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) μ
@[deprecated MeasureTheory.lpMeas.aestronglyMeasurable (since := "2025-04-09")]
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.
@[deprecated MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup (since := "2025-02-21")]
theorem
MeasureTheory.memℒp_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)
Alias of MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup.
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
- MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f = MeasureTheory.MemLp.toLp (Exists.choose ⋯) ⋯
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
- MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f = MeasureTheory.MemLp.toLp (Exists.choose ⋯) ⋯
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
- MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm f = ⟨MeasureTheory.MemLp.toLp ↑↑f ⋯, ⋯⟩
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
- MeasureTheory.lpTrimToLpMeas F 𝕜 p μ hm f = ⟨MeasureTheory.MemLp.toLp ↑↑f ⋯, ⋯⟩
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
- One or more equations did not get rendered due to their size.
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
- MeasureTheory.lpMeasSubgroupToLpMeasIso F 𝕜 p μ = IsometryEquiv.refl ↥(MeasureTheory.lpMeasSubgroup F m p μ)
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
- One or more equations did not get rendered due to their size.
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) μ}
@[deprecated MeasureTheory.isComplete_aestronglyMeasurable (since := "2025-04-09")]
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)
:
@[deprecated MeasureTheory.isClosed_aestronglyMeasurable (since := "2025-04-09")]
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.
@[deprecated MeasureTheory.MemLp.induction_stronglyMeasurable (since := "2025-02-21")]
theorem
MeasureTheory.Memℒp.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
Alias of MeasureTheory.MemLp.induction_stronglyMeasurable.
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.