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; - is closed under addition;
- the set of functions in
Lpstrongly measurable w.r.t.mfor which the property holds is closed.
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
- MeasureTheory.AEStronglyMeasurable' m f μ = ∃ (g : α → β), MeasureTheory.StronglyMeasurable g ∧ f =ᵐ[μ] g
Instances For
theorem
MeasureTheory.AEStronglyMeasurable'.congr
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f g : α → β}
(hf : AEStronglyMeasurable' m f μ)
(hfg : f =ᶠ[ae μ] g)
:
AEStronglyMeasurable' m g μ
theorem
MeasureTheory.AEStronglyMeasurable'.mono
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
{m' : MeasurableSpace α}
(hf : AEStronglyMeasurable' m f μ)
(hm : m ≤ m')
:
AEStronglyMeasurable' m' f μ
theorem
MeasureTheory.AEStronglyMeasurable'.add
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f g : α → β}
[Add β]
[ContinuousAdd β]
(hf : AEStronglyMeasurable' m f μ)
(hg : AEStronglyMeasurable' m g μ)
:
AEStronglyMeasurable' m (f + g) μ
theorem
MeasureTheory.AEStronglyMeasurable'.neg
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
[AddGroup β]
[TopologicalAddGroup β]
{f : α → β}
(hfm : AEStronglyMeasurable' m f μ)
:
AEStronglyMeasurable' m (-f) μ
theorem
MeasureTheory.AEStronglyMeasurable'.sub
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
[AddGroup β]
[TopologicalAddGroup β]
{f g : α → β}
(hfm : AEStronglyMeasurable' m f μ)
(hgm : AEStronglyMeasurable' m g μ)
:
AEStronglyMeasurable' m (f - g) μ
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' m f μ)
:
AEStronglyMeasurable' m (c • f) μ
theorem
MeasureTheory.AEStronglyMeasurable'.const_inner
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_4}
{β : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup β]
[InnerProductSpace 𝕜 β]
{f : α → β}
(hfm : AEStronglyMeasurable' m f μ)
(c : β)
:
AEStronglyMeasurable' m (fun (x : α) => inner c (f x)) μ
@[simp]
theorem
MeasureTheory.AEStronglyMeasurable'.of_subsingleton
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Subsingleton β]
:
AEStronglyMeasurable' m f μ
@[simp]
theorem
MeasureTheory.AEStronglyMeasurable'.of_subsingleton'
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
[Subsingleton α]
:
AEStronglyMeasurable' m f μ
noncomputable def
MeasureTheory.AEStronglyMeasurable'.mk
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
(f : α → β)
(hfm : AEStronglyMeasurable' m f μ)
:
α → β
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 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
(hfm : AEStronglyMeasurable' m f μ)
:
StronglyMeasurable (mk f hfm)
theorem
MeasureTheory.AEStronglyMeasurable'.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
(hfm : AEStronglyMeasurable' m f μ)
:
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' m f μ)
:
AEStronglyMeasurable' m (g ∘ f) μ
theorem
MeasureTheory.aeStronglyMeasurable'_of_aeStronglyMeasurable'_trim
{α : Type u_1}
{β : Type u_2}
{m m0 m0' : MeasurableSpace α}
[TopologicalSpace β]
(hm0 : m0 ≤ m0')
{μ : Measure α}
{f : α → β}
(hf : AEStronglyMeasurable' m f (μ.trim hm0))
:
AEStronglyMeasurable' m f μ
theorem
MeasureTheory.StronglyMeasurable.aeStronglyMeasurable'
{α : Type u_1}
{β : Type u_2}
{m x✝ : MeasurableSpace α}
[TopologicalSpace β]
{μ : Measure α}
{f : α → β}
(hf : StronglyMeasurable f)
:
AEStronglyMeasurable' m 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' m f μ)
(hgm : AEStronglyMeasurable' m g μ)
:
AEStronglyMeasurable'.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable'.mk g hgm ↔ f =ᶠ[ae μ] 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' (MeasurableSpace.comap g mα) (f ∘ g) μ
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' m f μ)
(hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0)
:
AEStronglyMeasurable' m₂ f μ
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' m (↑↑f) μ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
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
- MeasureTheory.lpMeas F 𝕜 m p μ = { carrier := {f : ↥(MeasureTheory.Lp F p μ) | MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
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 μ)}
:
f ∈ lpMeasSubgroup F m p μ ↔ AEStronglyMeasurable' m (↑↑f) μ
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 μ)}
:
f ∈ lpMeas F 𝕜 m p μ ↔ AEStronglyMeasurable' m (↑↑f) μ
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' m (↑↑↑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.lpMeasSubgroup_coe
{α : Type u_1}
{F : Type u_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m x✝ : MeasurableSpace α}
{μ : Measure α}
{f : ↥(lpMeasSubgroup F m p μ)}
:
↑↑↑f = ↑↑↑f
theorem
MeasureTheory.lpMeas_coe
{α : 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 μ)}
:
↑↑↑f = ↑↑↑f
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}
:
indicatorConstLp p ⋯ hμs c ∈ 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_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
(f : ↥(Lp F p μ))
(hf_meas : f ∈ lpMeasSubgroup F m p μ)
:
Memℒp (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)))
:
Memℒp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ
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 μ))
:
↥(Lp F p (μ.trim hm))
Map from lpMeasSubgroup to Lp F p (μ.trim hm).
Equations
- MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f = MeasureTheory.Memℒp.toLp (Exists.choose ⋯) ⋯
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 μ))
:
↥(Lp F p (μ.trim hm))
Map from lpMeas to Lp F p (μ.trim hm).
Equations
- MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f = MeasureTheory.Memℒp.toLp (Exists.choose ⋯) ⋯
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
- MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm f = ⟨MeasureTheory.Memℒp.toLp ↑↑f ⋯, ⋯⟩
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
- MeasureTheory.lpTrimToLpMeas F 𝕜 p μ hm f = ⟨MeasureTheory.Memℒp.toLp ↑↑f ⋯, ⋯⟩
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 μ))
:
↑↑(lpMeasSubgroupToLpTrim F p μ hm f) =ᶠ[ae μ] ↑↑↑f
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)))
:
↑↑↑(lpTrimToLpMeasSubgroup F p μ hm f) =ᶠ[ae μ] ↑↑f
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 μ))
:
↑↑(lpMeasToLpTrim F 𝕜 p μ hm f) =ᶠ[ae μ] ↑↑↑f
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)))
:
↑↑↑(lpTrimToLpMeas F 𝕜 p μ hm f) =ᶠ[ae μ] ↑↑f
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 μ))
:
lpMeasSubgroupToLpTrim F p μ hm (-f) = -lpMeasSubgroupToLpTrim F p μ hm f
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 μ))
:
lpMeasToLpTrim F 𝕜 p μ hm (c • f) = c • lpMeasToLpTrim F 𝕜 p μ hm f
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 F m p μ) ≃ᵢ ↥(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_2)
(𝕜 : Type u_3)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m m0 : MeasurableSpace α}
(μ : Measure α)
[Fact (1 ≤ p)]
:
↥(lpMeasSubgroup F m p μ) ≃ᵢ ↥(lpMeas F 𝕜 m p μ)
lpMeasSubgroup and lpMeas are isometric.
Equations
- MeasureTheory.lpMeasSubgroupToLpMeasIso F 𝕜 p μ = IsometryEquiv.refl ↥(MeasureTheory.lpMeasSubgroup F m p μ)
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
- One or more equations did not get rendered due to their size.
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' m (↑↑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)
:
IsClosed {f : ↥(Lp F p μ) | AEStronglyMeasurable' m (↑↑f) μ}
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 ≠ ⊤)
:
∃ (g : α → F), FinStronglyMeasurable g (μ.trim hm) ∧ ↑↑↑f =ᶠ[ae μ] 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_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)
:
↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (indicatorConstLp p hs hμs c)) = indicatorConstLp p ⋯ ⋯ 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_2}
{p : ENNReal}
[NormedAddCommGroup F]
{m m0 : MeasurableSpace α}
{μ : Measure α}
[one_le_p : Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(f : α → F)
(hf : Memℒp f p (μ.trim hm))
:
↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (Memℒp.toLp f hf)) = Memℒp.toLp f ⋯
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 : Memℒp f p μ) (hg : Memℒp g p μ),
AEStronglyMeasurable' m f μ →
AEStronglyMeasurable' m g μ →
Disjoint (Function.support f) (Function.support g) →
P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg))
(h_closed : IsClosed {f : ↥(lpMeas F ℝ m p μ) | P ↑f})
(f : ↥(Lp F p μ))
:
AEStronglyMeasurable' m (↑↑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 : Memℒp f p μ) (hg : Memℒp g p μ),
StronglyMeasurable f →
StronglyMeasurable g →
Disjoint (Function.support f) (Function.support g) →
P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg))
(h_closed : IsClosed {f : ↥(lpMeas F ℝ m p μ) | P ↑f})
(f : ↥(Lp F p μ))
:
AEStronglyMeasurable' m (↑↑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.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) →
Memℒp f p μ → Memℒp 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 → Memℒp f p μ → P f → P g)
⦃f : α → F⦄
:
Memℒp f p μ → AEStronglyMeasurable' m f μ → 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; - 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.