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 α} → (α → β) → MeasureTheory.Measure α → Prop
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
theorem
MeasureTheory.AEStronglyMeasurable'.congr
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
(hfg : f =ᵐ[μ] g)
:
theorem
MeasureTheory.AEStronglyMeasurable'.mono
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
{m' : MeasurableSpace α}
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
(hm : m ≤ m')
:
theorem
MeasureTheory.AEStronglyMeasurable'.add
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
{g : α → β}
[Add β]
[ContinuousAdd β]
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
(hg : MeasureTheory.AEStronglyMeasurable' m g μ)
:
MeasureTheory.AEStronglyMeasurable' m (f + g) μ
theorem
MeasureTheory.AEStronglyMeasurable'.neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
[AddGroup β]
[TopologicalAddGroup β]
{f : α → β}
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable'.sub
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
[AddGroup β]
[TopologicalAddGroup β]
{f : α → β}
{g : α → β}
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
(hgm : MeasureTheory.AEStronglyMeasurable' m g μ)
:
MeasureTheory.AEStronglyMeasurable' m (f - g) μ
theorem
MeasureTheory.AEStronglyMeasurable'.const_smul
{α : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
[SMul 𝕜 β]
[ContinuousConstSMul 𝕜 β]
(c : 𝕜)
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
:
MeasureTheory.AEStronglyMeasurable' m (c • f) μ
theorem
MeasureTheory.AEStronglyMeasurable'.const_inner
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_4}
{β : Type u_5}
[RCLike 𝕜]
[NormedAddCommGroup β]
[InnerProductSpace 𝕜 β]
{f : α → β}
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
(c : β)
:
MeasureTheory.AEStronglyMeasurable' m (fun (x : α) => inner c (f x)) μ
@[simp]
theorem
MeasureTheory.AEStronglyMeasurable'.of_subsingleton
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
[Subsingleton β]
:
@[simp]
theorem
MeasureTheory.AEStronglyMeasurable'.of_subsingleton'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
[Subsingleton α]
:
noncomputable def
MeasureTheory.AEStronglyMeasurable'.mk
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
(f : α → β)
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
:
α → β
An m-strongly measurable function almost everywhere equal to f.
Equations
theorem
MeasureTheory.AEStronglyMeasurable'.stronglyMeasurable_mk
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable'.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{f : α → β}
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable'.continuous_comp
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace β]
{γ : Type u_4}
[TopologicalSpace γ]
{f : α → β}
{g : β → γ}
(hg : Continuous g)
(hf : MeasureTheory.AEStronglyMeasurable' m f μ)
:
MeasureTheory.AEStronglyMeasurable' m (g ∘ f) μ
theorem
MeasureTheory.aeStronglyMeasurable'_of_aeStronglyMeasurable'_trim
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{m0' : MeasurableSpace α}
[TopologicalSpace β]
(hm0 : m0 ≤ m0')
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : MeasureTheory.AEStronglyMeasurable' m f (μ.trim hm0))
:
theorem
MeasureTheory.StronglyMeasurable.aeStronglyMeasurable'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
:
∀ {x : MeasurableSpace α} [inst : TopologicalSpace β] {μ : MeasureTheory.Measure α} {f : α → β},
MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable' m f μ
theorem
MeasureTheory.ae_eq_trim_iff_of_aeStronglyMeasurable'
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace β]
[TopologicalSpace.MetrizableSpace β]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → β}
{g : α → β}
(hm : m ≤ m0)
(hfm : MeasureTheory.AEStronglyMeasurable' m f μ)
(hgm : MeasureTheory.AEStronglyMeasurable' m g μ)
:
MeasureTheory.AEStronglyMeasurable'.mk f hfm =ᵐ[μ.trim hm] MeasureTheory.AEStronglyMeasurable'.mk g hgm ↔ f =ᵐ[μ] g
theorem
MeasureTheory.AEStronglyMeasurable.comp_ae_measurable'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace β]
{mα : MeasurableSpace α}
:
∀ {x : MeasurableSpace γ} {f : α → β} {μ : MeasureTheory.Measure γ} {g : γ → α},
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map g μ) →
AEMeasurable g μ → MeasureTheory.AEStronglyMeasurable' (MeasurableSpace.comap g mα) (f ∘ g) μ
theorem
MeasureTheory.AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m₂ : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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 : MeasureTheory.AEStronglyMeasurable' m f μ)
(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.
def
MeasureTheory.lpMeasSubgroup
{α : Type u_1}
(F : Type u_3)
[NormedAddCommGroup F]
(m : MeasurableSpace α)
[MeasurableSpace α]
(p : ENNReal)
(μ : MeasureTheory.Measure α)
:
AddSubgroup ↥(MeasureTheory.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' := ⋯ }
def
MeasureTheory.lpMeas
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(m : MeasurableSpace α)
[MeasurableSpace α]
(p : ENNReal)
(μ : MeasureTheory.Measure α)
:
Submodule 𝕜 ↥(MeasureTheory.Lp F p μ)
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' := ⋯ }
theorem
MeasureTheory.mem_lpMeasSubgroup_iff_aeStronglyMeasurable'
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ↥(MeasureTheory.Lp F p μ)}
:
f ∈ MeasureTheory.lpMeasSubgroup F m p μ ↔ MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ
theorem
MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ↥(MeasureTheory.Lp F p μ)}
:
f ∈ MeasureTheory.lpMeas F 𝕜 m p μ ↔ MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ
theorem
MeasureTheory.lpMeas.aeStronglyMeasurable'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
:
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)),
MeasureTheory.AEStronglyMeasurable' m (↑↑↑f) μ
theorem
MeasureTheory.mem_lpMeas_self
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(f : ↥(MeasureTheory.Lp F p μ))
:
f ∈ MeasureTheory.lpMeas F 𝕜 m0 p μ
theorem
MeasureTheory.lpMeasSubgroup_coe
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
:
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)}, ↑↑↑f = ↑↑↑f
theorem
MeasureTheory.lpMeas_coe
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
:
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)}, ↑↑↑f = ↑↑↑f
theorem
MeasureTheory.mem_lpMeas_indicatorConstLp
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(hm : m ≤ m0)
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
{c : F}
:
MeasureTheory.indicatorConstLp p ⋯ hμs c ∈ 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}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(MeasureTheory.Lp F p μ))
(hf_meas : f ∈ MeasureTheory.lpMeasSubgroup F m p μ)
:
MeasureTheory.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_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(MeasureTheory.Lp F p (μ.trim hm)))
:
MeasureTheory.Memℒp.toLp ↑↑f ⋯ ∈ MeasureTheory.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_3)
(p : ENNReal)
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
:
↥(MeasureTheory.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 ⋯) ⋯
noncomputable def
MeasureTheory.lpMeasToLpTrim
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ))
:
↥(MeasureTheory.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 ⋯) ⋯
noncomputable def
MeasureTheory.lpTrimToLpMeasSubgroup
{α : Type u_1}
(F : Type u_3)
(p : ENNReal)
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ m0)
(f : ↥(MeasureTheory.Lp F p (μ.trim hm)))
:
↥(MeasureTheory.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 ⋯, ⋯⟩
noncomputable def
MeasureTheory.lpTrimToLpMeas
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ m0)
(f : ↥(MeasureTheory.Lp F p (μ.trim hm)))
:
↥(MeasureTheory.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 ⋯, ⋯⟩
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
:
↑↑(MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f) =ᵐ[μ] ↑↑↑f
theorem
MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(MeasureTheory.Lp F p (μ.trim hm)))
:
↑↑↑(MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm f) =ᵐ[μ] ↑↑f
theorem
MeasureTheory.lpMeasToLpTrim_ae_eq
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(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}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(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}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
:
Function.RightInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm) (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
lpTrimToLpMeasSubgroup is a right inverse of lpMeasSubgroupToLpTrim.
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_left_inv
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
:
Function.LeftInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm) (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
lpTrimToLpMeasSubgroup is a left inverse of lpMeasSubgroupToLpTrim.
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_add
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
(g : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
:
MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (f + g) = MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f + MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm g
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_neg
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
:
MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (-f) = -MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f
theorem
MeasureTheory.lpMeasSubgroupToLpTrim_sub
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
(g : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
:
MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (f - g) = MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f - MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm g
theorem
MeasureTheory.lpMeasToLpTrim_smul
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(c : 𝕜)
(f : ↥(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}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[hp : Fact (1 ≤ p)]
(hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeasSubgroup F m p μ))
:
lpMeasSubgroupToLpTrim preserves the norm.
theorem
MeasureTheory.isometry_lpMeasSubgroupToLpTrim
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[hp : Fact (1 ≤ p)]
(hm : m ≤ m0)
:
Isometry (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
noncomputable def
MeasureTheory.lpMeasSubgroupToLpTrimIso
{α : Type u_1}
(F : Type u_3)
(p : ENNReal)
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[Fact (1 ≤ p)]
(hm : m ≤ m0)
:
↥(MeasureTheory.lpMeasSubgroup F m p μ) ≃ᵢ ↥(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.
noncomputable def
MeasureTheory.lpMeasSubgroupToLpMeasIso
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[Fact (1 ≤ p)]
:
↥(MeasureTheory.lpMeasSubgroup F m p μ) ≃ᵢ ↥(MeasureTheory.lpMeas F 𝕜 m 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_3)
(𝕜 : Type u_5)
(p : ENNReal)
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[Fact (1 ≤ p)]
(hm : m ≤ m0)
:
↥(MeasureTheory.lpMeas F 𝕜 m p μ) ≃ₗᵢ[𝕜] ↥(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.
instance
MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[hm : Fact (m ≤ m0)]
[CompleteSpace F]
[hp : Fact (1 ≤ p)]
:
CompleteSpace ↥(MeasureTheory.lpMeasSubgroup F m p μ)
Equations
- ⋯ = ⋯
instance
MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[hm : Fact (m ≤ m0)]
[CompleteSpace F]
[hp : Fact (1 ≤ p)]
:
CompleteSpace ↥(MeasureTheory.lpMeas F 𝕜 m p μ)
Equations
- ⋯ = ⋯
theorem
MeasureTheory.isComplete_aeStronglyMeasurable'
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[hp : Fact (1 ≤ p)]
[CompleteSpace F]
(hm : m ≤ m0)
:
IsComplete {f : ↥(MeasureTheory.Lp F p μ) | MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ}
theorem
MeasureTheory.isClosed_aeStronglyMeasurable'
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Fact (1 ≤ p)]
[CompleteSpace F]
(hm : m ≤ m0)
:
IsClosed {f : ↥(MeasureTheory.Lp F p μ) | MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ}
theorem
MeasureTheory.lpMeas.ae_fin_strongly_measurable'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ENNReal}
[RCLike 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(f : ↥(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}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
[one_le_p : Fact (1 ≤ p)]
[NormedSpace ℝ F]
{hm : m ≤ m0}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hs : MeasurableSet s)
(hμs : (μ.trim hm) s ≠ ⊤)
(c : F)
:
↑((MeasureTheory.lpMeasToLpTrimLie F ℝ p μ hm).symm (MeasureTheory.indicatorConstLp p hs hμs c)) = MeasureTheory.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_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[one_le_p : Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(f : α → F)
(hf : MeasureTheory.Memℒp f p (μ.trim hm))
:
↑((MeasureTheory.lpMeasToLpTrimLie F ℝ p μ hm).symm (MeasureTheory.Memℒp.toLp f hf)) = MeasureTheory.Memℒp.toLp f ⋯
theorem
MeasureTheory.Lp.induction_stronglyMeasurable_aux
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(MeasureTheory.Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c))
(h_add : ∀ ⦃f g : α → F⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ),
MeasureTheory.AEStronglyMeasurable' m f μ →
MeasureTheory.AEStronglyMeasurable' m g μ →
Disjoint (Function.support f) (Function.support g) →
P (MeasureTheory.Memℒp.toLp f hf) →
P (MeasureTheory.Memℒp.toLp g hg) → P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg))
(h_closed : IsClosed {f : ↥(MeasureTheory.lpMeas F ℝ m p μ) | P ↑f})
(f : ↥(MeasureTheory.Lp F p μ))
:
MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ → P f
Auxiliary lemma for Lp.induction_stronglyMeasurable.
theorem
MeasureTheory.Lp.induction_stronglyMeasurable
{α : Type u_1}
{F : Type u_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Fact (1 ≤ p)]
[NormedSpace ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(MeasureTheory.Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c))
(h_add : ∀ ⦃f g : α → F⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ),
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g →
Disjoint (Function.support f) (Function.support g) →
P (MeasureTheory.Memℒp.toLp f hf) →
P (MeasureTheory.Memℒp.toLp g hg) → P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg))
(h_closed : IsClosed {f : ↥(MeasureTheory.lpMeas F ℝ m p μ) | P ↑f})
(f : ↥(MeasureTheory.Lp F p μ))
:
MeasureTheory.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_3}
{p : ENNReal}
[NormedAddCommGroup F]
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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) →
MeasureTheory.Memℒp f p μ →
MeasureTheory.Memℒp g p μ →
MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → P f → P g → P (f + g))
(h_closed : IsClosed {f : ↥(MeasureTheory.lpMeas F ℝ m p μ) | P ↑↑↑f})
(h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MeasureTheory.Memℒp f p μ → P f → P g)
⦃f : α → F⦄
:
MeasureTheory.Memℒp f p μ → MeasureTheory.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.