Functions a.e. measurable with respect to a sub-σ-algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A function f verifies ae_strongly_measurable' m f μ if it is μ-a.e. equal to
an m-strongly measurable function. This is similar to ae_strongly_measurable, but the
measurable_space structures used for the measurability statement and for the measure are
different.
We define Lp_meas F 𝕜 m p μ, the subspace of Lp F p μ containing functions f verifying
ae_strongly_measurable' m f μ, i.e. functions which are μ-a.e. equal to an m-strongly
measurable function.
Main statements #
We define an isometry_equiv between Lp_meas_subgroup and the Lp space corresponding to the
measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of Lp_meas.
Lp.induction_strongly_measurable (see also mem_ℒp.induction_strongly_measurable):
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
measure_theory.ae_strongly_measurable'
{α : Type u_1}
{β : Type u_2}
[topological_space β]
(m : measurable_space α)
{m0 : measurable_space α}
(f : α → β)
(μ : measure_theory.measure α) :
Prop
A function f verifies ae_strongly_measurable' m f μ if it is μ-a.e. equal to
an m-strongly measurable function. This is similar to ae_strongly_measurable, but the
measurable_space structures used for the measurability statement and for the measure are
different.
Equations
- measure_theory.ae_strongly_measurable' m f μ = ∃ (g : α → β), measure_theory.strongly_measurable g ∧ f =ᵐ[μ] g
theorem
measure_theory.ae_strongly_measurable'.congr
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hfg : f =ᵐ[μ] g) :
theorem
measure_theory.ae_strongly_measurable'.add
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[has_add β]
[has_continuous_add β]
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hg : measure_theory.ae_strongly_measurable' m g μ) :
measure_theory.ae_strongly_measurable' m (f + g) μ
theorem
measure_theory.ae_strongly_measurable'.neg
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[add_group β]
[topological_add_group β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
theorem
measure_theory.ae_strongly_measurable'.sub
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[add_group β]
[topological_add_group β]
{f g : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hgm : measure_theory.ae_strongly_measurable' m g μ) :
measure_theory.ae_strongly_measurable' m (f - g) μ
theorem
measure_theory.ae_strongly_measurable'.const_smul
{α : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_smul 𝕜 β]
[has_continuous_const_smul 𝕜 β]
(c : 𝕜)
(hf : measure_theory.ae_strongly_measurable' m f μ) :
measure_theory.ae_strongly_measurable' m (c • f) μ
theorem
measure_theory.ae_strongly_measurable'.const_inner
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_2}
{β : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group β]
[inner_product_space 𝕜 β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(c : β) :
measure_theory.ae_strongly_measurable' m (λ (x : α), has_inner.inner c (f x)) μ
noncomputable
def
measure_theory.ae_strongly_measurable'.mk
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
(f : α → β)
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
α → β
An m-strongly measurable function almost everywhere equal to f.
Equations
theorem
measure_theory.ae_strongly_measurable'.strongly_measurable_mk
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
theorem
measure_theory.ae_strongly_measurable'.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
theorem
measure_theory.ae_strongly_measurable'.continuous_comp
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{γ : Type u_3}
[topological_space γ]
{f : α → β}
{g : β → γ}
(hg : continuous g)
(hf : measure_theory.ae_strongly_measurable' m f μ) :
measure_theory.ae_strongly_measurable' m (g ∘ f) μ
theorem
measure_theory.ae_strongly_measurable'_of_ae_strongly_measurable'_trim
{α : Type u_1}
{β : Type u_2}
{m m0 m0' : measurable_space α}
[topological_space β]
(hm0 : m0 ≤ m0')
{μ : measure_theory.measure α}
{f : α → β}
(hf : measure_theory.ae_strongly_measurable' m f (μ.trim hm0)) :
theorem
measure_theory.strongly_measurable.ae_strongly_measurable'
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
[topological_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measure_theory.strongly_measurable f) :
theorem
measure_theory.ae_eq_trim_iff_of_ae_strongly_measurable'
{α : Type u_1}
{β : Type u_2}
[topological_space β]
[topological_space.metrizable_space β]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → β}
(hm : m ≤ m0)
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hgm : measure_theory.ae_strongly_measurable' m g μ) :
measure_theory.ae_strongly_measurable'.mk f hfm =ᵐ[μ.trim hm] measure_theory.ae_strongly_measurable'.mk g hgm ↔ f =ᵐ[μ] g
theorem
measure_theory.ae_strongly_measurable.comp_ae_measurable'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
{mα : measurable_space α}
{mγ : measurable_space γ}
{f : α → β}
{μ : measure_theory.measure γ}
{g : γ → α}
(hf : measure_theory.ae_strongly_measurable f (measure_theory.measure.map g μ))
(hg : ae_measurable g μ) :
measure_theory.ae_strongly_measurable' (measurable_space.comap g mα) (f ∘ g) μ
theorem
measure_theory.ae_strongly_measurable'.ae_strongly_measurable'_of_measurable_space_le_on
{α : Type u_1}
{E : Type u_2}
{m m₂ m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space E]
[has_zero E]
(hm : m ≤ m0)
{s : set α}
{f : α → E}
(hs_m : measurable_set s)
(hs : ∀ (t : set α), measurable_set (s ∩ t) → measurable_set (s ∩ t))
(hf : measure_theory.ae_strongly_measurable' 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.
The subset Lp_meas of Lp functions a.e. measurable with respect to a sub-sigma-algebra #
def
measure_theory.Lp_meas_subgroup
{α : Type u_1}
(F : Type u_3)
[normed_add_comm_group F]
(m : measurable_space α)
[measurable_space α]
(p : ennreal)
(μ : measure_theory.measure α) :
add_subgroup ↥(measure_theory.Lp F p μ)
Lp_meas_subgroup F m p μ is the subspace of Lp F p μ containing functions f verifying
ae_strongly_measurable' m f μ, i.e. functions which are μ-a.e. equal to
an m-strongly measurable function.
Equations
- measure_theory.Lp_meas_subgroup F m p μ = {carrier := {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}, add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for ↥measure_theory.Lp_meas_subgroup
def
measure_theory.Lp_meas
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
(m : measurable_space α)
[measurable_space α]
(p : ennreal)
(μ : measure_theory.measure α) :
submodule 𝕜 ↥(measure_theory.Lp F p μ)
Lp_meas F 𝕜 m p μ is the subspace of Lp F p μ containing functions f verifying
ae_strongly_measurable' m f μ, i.e. functions which are μ-a.e. equal to
an m-strongly measurable function.
Equations
- measure_theory.Lp_meas F 𝕜 m p μ = {carrier := {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}, add_mem' := _, zero_mem' := _, smul_mem' := _}
Instances for ↥measure_theory.Lp_meas
theorem
measure_theory.mem_Lp_meas_subgroup_iff_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp F p μ)} :
f ∈ measure_theory.Lp_meas_subgroup F m p μ ↔ measure_theory.ae_strongly_measurable' m ⇑f μ
theorem
measure_theory.mem_Lp_meas_iff_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp F p μ)} :
f ∈ measure_theory.Lp_meas F 𝕜 m p μ ↔ measure_theory.ae_strongly_measurable' m ⇑f μ
theorem
measure_theory.Lp_meas.ae_strongly_measurable'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
theorem
measure_theory.mem_Lp_meas_self
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m0 : measurable_space α}
(μ : measure_theory.measure α)
(f : ↥(measure_theory.Lp F p μ)) :
f ∈ measure_theory.Lp_meas F 𝕜 m0 p μ
theorem
measure_theory.Lp_meas_subgroup_coe
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp_meas_subgroup F m p μ)} :
theorem
measure_theory.Lp_meas_coe
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)} :
theorem
measure_theory.mem_Lp_meas_indicator_const_Lp
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(hm : m ≤ m0)
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
{c : F} :
measure_theory.indicator_const_Lp p _ hμs c ∈ measure_theory.Lp_meas F 𝕜 m p μ
The subspace Lp_meas is complete. #
We define an isometry_equiv between Lp_meas_subgroup and the Lp space corresponding to the
measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of
Lp_meas_subgroup (and Lp_meas).
theorem
measure_theory.mem_ℒp_trim_of_mem_Lp_meas_subgroup
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p μ))
(hf_meas : f ∈ measure_theory.Lp_meas_subgroup F m p μ) :
measure_theory.mem_ℒp (Exists.some _) p (μ.trim hm)
If f belongs to Lp_meas_subgroup F m p μ, then the measurable function it is almost
everywhere equal to (given by ae_measurable.mk) belongs to ℒp for the measure μ.trim hm.
theorem
measure_theory.mem_Lp_meas_subgroup_to_Lp_of_trim
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
If f belongs to Lp for the measure μ.trim hm, then it belongs to the subgroup
Lp_meas_subgroup F m p μ.
noncomputable
def
measure_theory.Lp_meas_subgroup_to_Lp_trim
{α : Type u_1}
(F : Type u_3)
(p : ennreal)
[normed_add_comm_group F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
↥(measure_theory.Lp F p (μ.trim hm))
Map from Lp_meas_subgroup to Lp F p (μ.trim hm).
Equations
noncomputable
def
measure_theory.Lp_meas_to_Lp_trim
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
↥(measure_theory.Lp F p (μ.trim hm))
Map from Lp_meas to Lp F p (μ.trim hm).
Equations
- measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm f = measure_theory.mem_ℒp.to_Lp (Exists.some _) _
noncomputable
def
measure_theory.Lp_trim_to_Lp_meas_subgroup
{α : Type u_1}
(F : Type u_3)
(p : ennreal)
[normed_add_comm_group F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
↥(measure_theory.Lp_meas_subgroup F m p μ)
Map from Lp F p (μ.trim hm) to Lp_meas_subgroup, inverse of
Lp_meas_subgroup_to_Lp_trim.
Equations
- measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm f = ⟨measure_theory.mem_ℒp.to_Lp ⇑f _, _⟩
noncomputable
def
measure_theory.Lp_trim_to_Lp_meas
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
↥(measure_theory.Lp_meas F 𝕜 m p μ)
Map from Lp F p (μ.trim hm) to Lp_meas, inverse of Lp_meas_to_Lp_trim.
Equations
- measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm f = ⟨measure_theory.mem_ℒp.to_Lp ⇑f _, _⟩
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_ae_eq
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
⇑(measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_trim_to_Lp_meas_subgroup_ae_eq
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
⇑(measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_meas_to_Lp_trim_ae_eq
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
⇑(measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_trim_to_Lp_meas_ae_eq
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
⇑(measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_right_inv
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
Lp_trim_to_Lp_meas_subgroup is a right inverse of Lp_meas_subgroup_to_Lp_trim.
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_left_inv
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
Lp_trim_to_Lp_meas_subgroup is a left inverse of Lp_meas_subgroup_to_Lp_trim.
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_add
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm (f + g) = measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f + measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm g
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_neg
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm (-f) = -measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_sub
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm (f - g) = measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f - measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm g
theorem
measure_theory.Lp_meas_to_Lp_trim_smul
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(c : 𝕜)
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm (c • f) = c • measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm f
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_norm_map
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
Lp_meas_subgroup_to_Lp_trim preserves the norm.
theorem
measure_theory.isometry_Lp_meas_subgroup_to_Lp_trim
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
(hm : m ≤ m0) :
noncomputable
def
measure_theory.Lp_meas_subgroup_to_Lp_trim_iso
{α : Type u_1}
(F : Type u_3)
(p : ennreal)
[normed_add_comm_group F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
[hp : fact (1 ≤ p)]
(hm : m ≤ m0) :
↥(measure_theory.Lp_meas_subgroup F m p μ) ≃ᵢ ↥(measure_theory.Lp F p (μ.trim hm))
Lp_meas_subgroup and Lp F p (μ.trim hm) are isometric.
Equations
- measure_theory.Lp_meas_subgroup_to_Lp_trim_iso F p μ hm = {to_equiv := {to_fun := measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm, inv_fun := measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm, left_inv := _, right_inv := _}, isometry_to_fun := _}
noncomputable
def
measure_theory.Lp_meas_subgroup_to_Lp_meas_iso
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
[hp : fact (1 ≤ p)] :
↥(measure_theory.Lp_meas_subgroup F m p μ) ≃ᵢ ↥(measure_theory.Lp_meas F 𝕜 m p μ)
Lp_meas_subgroup and Lp_meas are isometric.
Equations
noncomputable
def
measure_theory.Lp_meas_to_Lp_trim_lie
{α : Type u_1}
(F : Type u_3)
(𝕜 : Type u_5)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
[hp : fact (1 ≤ p)]
(hm : m ≤ m0) :
↥(measure_theory.Lp_meas F 𝕜 m p μ) ≃ₗᵢ[𝕜] ↥(measure_theory.Lp F p (μ.trim hm))
Lp_meas and Lp F p (μ.trim hm) are isometric, with a linear equivalence.
Equations
- measure_theory.Lp_meas_to_Lp_trim_lie F 𝕜 p μ hm = {to_linear_equiv := {to_fun := measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm, map_add' := _, map_smul' := _, inv_fun := measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm, left_inv := _, right_inv := _}, norm_map' := _}
@[protected, instance]
def
measure_theory.Lp_meas_subgroup.complete_space
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hm : fact (m ≤ m0)]
[complete_space F]
[hp : fact (1 ≤ p)] :
@[protected, nolint, instance]
def
measure_theory.Lp_meas.complete_space
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hm : fact (m ≤ m0)]
[complete_space F]
[hp : fact (1 ≤ p)] :
complete_space ↥(measure_theory.Lp_meas F 𝕜 m p μ)
theorem
measure_theory.is_complete_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
[complete_space F]
(hm : m ≤ m0) :
is_complete {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}
theorem
measure_theory.is_closed_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
[complete_space F]
(hm : m ≤ m0) :
is_closed {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}
theorem
measure_theory.Lp_meas.ae_fin_strongly_measurable'
{α : Type u_1}
{F : Type u_3}
{𝕜 : Type u_5}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas 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
measure_theory.Lp_meas_to_Lp_trim_lie_symm_indicator
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
[one_le_p : fact (1 ≤ p)]
[normed_space ℝ F]
{hm : m ≤ m0}
{s : set α}
{μ : measure_theory.measure α}
(hs : measurable_set s)
(hμs : ⇑(μ.trim hm) s ≠ ⊤)
(c : F) :
↑(⇑((measure_theory.Lp_meas_to_Lp_trim_lie F ℝ p μ hm).symm) (measure_theory.indicator_const_Lp p hs hμs c)) = measure_theory.indicator_const_Lp p _ _ c
When applying the inverse of Lp_meas_to_Lp_trim_lie (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
measure_theory.Lp_meas_to_Lp_trim_lie_symm_to_Lp
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[one_le_p : fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(f : α → F)
(hf : measure_theory.mem_ℒp f p (μ.trim hm)) :
↑(⇑((measure_theory.Lp_meas_to_Lp_trim_lie F ℝ p μ hm).symm) (measure_theory.mem_ℒp.to_Lp f hf)) = measure_theory.mem_ℒp.to_Lp f _
theorem
measure_theory.Lp.induction_strongly_measurable_aux
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(measure_theory.Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : set α} (hs : measurable_set s) (hμs : ⇑μ s < ⊤), P ↑(measure_theory.Lp.simple_func.indicator_const p _ _ c))
(h_add : ∀ ⦃f g : α → F⦄ (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ), measure_theory.ae_strongly_measurable' m f μ → measure_theory.ae_strongly_measurable' m g μ → disjoint (function.support f) (function.support g) → P (measure_theory.mem_ℒp.to_Lp f hf) → P (measure_theory.mem_ℒp.to_Lp g hg) → P (measure_theory.mem_ℒp.to_Lp f hf + measure_theory.mem_ℒp.to_Lp g hg))
(h_closed : is_closed {f : ↥(measure_theory.Lp_meas F ℝ m p μ) | P ↑f})
(f : ↥(measure_theory.Lp F p μ)) :
measure_theory.ae_strongly_measurable' m ⇑f μ → P f
Auxiliary lemma for Lp.induction_strongly_measurable.
theorem
measure_theory.Lp.induction_strongly_measurable
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(measure_theory.Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : set α} (hs : measurable_set s) (hμs : ⇑μ s < ⊤), P ↑(measure_theory.Lp.simple_func.indicator_const p _ _ c))
(h_add : ∀ ⦃f g : α → F⦄ (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ), measure_theory.strongly_measurable f → measure_theory.strongly_measurable g → disjoint (function.support f) (function.support g) → P (measure_theory.mem_ℒp.to_Lp f hf) → P (measure_theory.mem_ℒp.to_Lp g hg) → P (measure_theory.mem_ℒp.to_Lp f hf + measure_theory.mem_ℒp.to_Lp g hg))
(h_closed : is_closed {f : ↥(measure_theory.Lp_meas F ℝ m p μ) | P ↑f})
(f : ↥(measure_theory.Lp F p μ)) :
measure_theory.ae_strongly_measurable' 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
measure_theory.mem_ℒp.induction_strongly_measurable
{α : Type u_1}
{F : Type u_3}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : (α → F) → Prop)
(h_ind : ∀ (c : F) ⦃s : set α⦄, measurable_set s → ⇑μ s < ⊤ → P (s.indicator (λ (_x : α), c)))
(h_add : ∀ ⦃f g : α → F⦄, disjoint (function.support f) (function.support g) → measure_theory.mem_ℒp f p μ → measure_theory.mem_ℒp g p μ → measure_theory.strongly_measurable f → measure_theory.strongly_measurable g → P f → P g → P (f + g))
(h_closed : is_closed {f : ↥(measure_theory.Lp_meas F ℝ m p μ) | P ⇑f})
(h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → measure_theory.mem_ℒp f p μ → P f → P g)
⦃f : α → F⦄
(hf : measure_theory.mem_ℒp f p μ)
(hfm : measure_theory.ae_strongly_measurable' 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.