Lp space #
This file provides the space Lp E p μ as the subtype of elements of α →ₘ[μ] E (see ae_eq_fun)
such that snorm f p μ is finite. For 1 ≤ p, snorm defines a norm and Lp is a complete metric
space.
Main definitions #
Lp E p μ: elements ofα →ₘ[μ] E(see ae_eq_fun) such thatsnorm f p μis finite. Defined as anAddSubgroupofα →ₘ[μ] E.
Lipschitz functions vanishing at zero act by composition on Lp. We define this action, and prove
that it is continuous. In particular,
ContinuousLinearMap.compLpdefines the action onLpof a continuous linear map.Lp.posPartis the positive part of anLpfunction.Lp.negPartis the negative part of anLpfunction.
When α is a topological space equipped with a finite Borel measure, there is a bounded linear map
from the normed space of bounded continuous functions (α →ᵇ E) to Lp E p μ. We construct this
as BoundedContinuousFunction.toLp.
Notations #
Implementation #
Since Lp is defined as an AddSubgroup, dot notation does not work. Use Lp.Measurable f to
say that the coercion of f to a genuine function is measurable, instead of the non-working
f.Measurable.
To prove that two Lp elements are equal, it suffices to show that their coercions to functions
coincide almost everywhere (this is registered as an ext rule). This can often be done using
filter_upwards. For instance, a proof from first principles that f + (g + h) = (f + g) + h
could read (in the Lp namespace)
example (f g h : Lp E p μ) : (f + g) + h = f + (g + h) := by
ext1
filter_upwards [coeFn_add (f + g) h, coeFn_add f g, coeFn_add f (g + h), coeFn_add g h]
with _ ha1 ha2 ha3 ha4
simp only [ha1, ha2, ha3, ha4, add_assoc]
The lemma coeFn_add states that the coercion of f + g coincides almost everywhere with the sum
of the coercions of f and g. All such lemmas use coeFn in their name, to distinguish the
function coercion from the coercion to almost everywhere defined functions.
Lp space #
The space of equivalence classes of measurable functions for which snorm f p μ < ∞.
@[simp]
theorem
MeasureTheory.snorm_aeeqFun
{α : Type u_5}
{E : Type u_6}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.snorm (↑(MeasureTheory.AEEqFun.mk f hf)) p μ = MeasureTheory.snorm f p μ
theorem
MeasureTheory.Memℒp.snorm_mk_lt_top
{α : Type u_5}
{E : Type u_6}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{f : α → E}
(hfp : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.snorm (↑(MeasureTheory.AEEqFun.mk f ⋯)) p μ < ⊤
def
MeasureTheory.Lp
{α : Type u_6}
(E : Type u_5)
{m : MeasurableSpace α}
[NormedAddCommGroup E]
(p : ENNReal)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
AddSubgroup (α →ₘ[μ] E)
Lp space
Equations
- MeasureTheory.Lp E p μ = { carrier := {f : α →ₘ[μ] E | MeasureTheory.snorm (↑f) p μ < ⊤}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.Memℒp.toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : α → E)
(h_mem_ℒp : MeasureTheory.Memℒp f p μ)
:
↥(MeasureTheory.Lp E p μ)
make an element of Lp from a function verifying Memℒp
Equations
- MeasureTheory.Memℒp.toLp f h_mem_ℒp = ⟨MeasureTheory.AEEqFun.mk f ⋯, ⋯⟩
Instances For
theorem
MeasureTheory.Memℒp.coeFn_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
↑↑(MeasureTheory.Memℒp.toLp f hf) =ᵐ[μ] f
theorem
MeasureTheory.Memℒp.toLp_congr
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
(hfg : f =ᵐ[μ] g)
:
@[simp]
theorem
MeasureTheory.Memℒp.toLp_eq_toLp_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp g hg ↔ f =ᵐ[μ] g
@[simp]
theorem
MeasureTheory.Memℒp.toLp_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(h : MeasureTheory.Memℒp 0 p μ)
:
MeasureTheory.Memℒp.toLp 0 h = 0
theorem
MeasureTheory.Memℒp.toLp_add
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.Memℒp.toLp (f + g) ⋯ = MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg
theorem
MeasureTheory.Memℒp.toLp_neg
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp.toLp (-f) ⋯ = -MeasureTheory.Memℒp.toLp f hf
theorem
MeasureTheory.Memℒp.toLp_sub
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.Memℒp.toLp (f - g) ⋯ = MeasureTheory.Memℒp.toLp f hf - MeasureTheory.Memℒp.toLp g hg
instance
MeasureTheory.Lp.instCoeFun
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
CoeFun ↥(MeasureTheory.Lp E p μ) fun (x : ↥(MeasureTheory.Lp E p μ)) => α → E
Equations
- MeasureTheory.Lp.instCoeFun = { coe := fun (f : ↥(MeasureTheory.Lp E p μ)) => ↑↑f }
theorem
MeasureTheory.Lp.ext
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : ↥(MeasureTheory.Lp E p μ)}
{g : ↥(MeasureTheory.Lp E p μ)}
(h : ↑↑f =ᵐ[μ] ↑↑g)
:
f = g
theorem
MeasureTheory.Lp.ext_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : ↥(MeasureTheory.Lp E p μ)}
{g : ↥(MeasureTheory.Lp E p μ)}
:
theorem
MeasureTheory.Lp.mem_Lp_iff_snorm_lt_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α →ₘ[μ] E}
:
f ∈ MeasureTheory.Lp E p μ ↔ MeasureTheory.snorm (↑f) p μ < ⊤
theorem
MeasureTheory.Lp.mem_Lp_iff_memℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α →ₘ[μ] E}
:
f ∈ MeasureTheory.Lp E p μ ↔ MeasureTheory.Memℒp (↑f) p μ
theorem
MeasureTheory.Lp.antitone
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
{p : ENNReal}
{q : ENNReal}
(hpq : p ≤ q)
:
MeasureTheory.Lp E q μ ≤ MeasureTheory.Lp E p μ
@[simp]
theorem
MeasureTheory.Lp.coeFn_mk
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α →ₘ[μ] E}
(hf : MeasureTheory.snorm (↑f) p μ < ⊤)
:
↑↑⟨f, hf⟩ = ↑f
theorem
MeasureTheory.Lp.coe_mk
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α →ₘ[μ] E}
(hf : MeasureTheory.snorm (↑f) p μ < ⊤)
:
↑⟨f, hf⟩ = f
@[simp]
theorem
MeasureTheory.Lp.toLp_coeFn
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(hf : MeasureTheory.Memℒp (↑↑f) p μ)
:
MeasureTheory.Memℒp.toLp (↑↑f) hf = f
theorem
MeasureTheory.Lp.snorm_lt_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
MeasureTheory.snorm (↑↑f) p μ < ⊤
theorem
MeasureTheory.Lp.snorm_ne_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
MeasureTheory.snorm (↑↑f) p μ ≠ ⊤
theorem
MeasureTheory.Lp.stronglyMeasurable
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
MeasureTheory.Lp.aestronglyMeasurable
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
MeasureTheory.Lp.memℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
MeasureTheory.Memℒp (↑↑f) p μ
theorem
MeasureTheory.Lp.coeFn_zero
{α : Type u_1}
(E : Type u_2)
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
:
theorem
MeasureTheory.Lp.coeFn_neg
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
MeasureTheory.Lp.coeFn_add
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
:
theorem
MeasureTheory.Lp.coeFn_sub
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
:
theorem
MeasureTheory.Lp.const_mem_Lp
{E : Type u_2}
{p : ENNReal}
[NormedAddCommGroup E]
(α : Type u_5)
:
∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (c : E) [inst : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.AEEqFun.const α c ∈ MeasureTheory.Lp E p μ
instance
MeasureTheory.Lp.instNorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
Norm ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.instNorm = { norm := fun (f : ↥(MeasureTheory.Lp E p μ)) => (MeasureTheory.snorm (↑↑f) p μ).toReal }
instance
MeasureTheory.Lp.instNNNorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
NNNorm ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.instNNNorm = { nnnorm := fun (f : ↥(MeasureTheory.Lp E p μ)) => ⟨‖f‖, ⋯⟩ }
instance
MeasureTheory.Lp.instDist
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
Dist ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.instDist = { dist := fun (f g : ↥(MeasureTheory.Lp E p μ)) => ‖f - g‖ }
instance
MeasureTheory.Lp.instEDist
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
EDist ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.instEDist = { edist := fun (f g : ↥(MeasureTheory.Lp E p μ)) => MeasureTheory.snorm (↑↑f - ↑↑g) p μ }
theorem
MeasureTheory.Lp.norm_def
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
‖f‖ = (MeasureTheory.snorm (↑↑f) p μ).toReal
theorem
MeasureTheory.Lp.nnnorm_def
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
‖f‖₊ = (MeasureTheory.snorm (↑↑f) p μ).toNNReal
@[simp]
theorem
MeasureTheory.Lp.coe_nnnorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
@[simp]
theorem
MeasureTheory.Lp.nnnorm_coe_ennreal
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
↑‖f‖₊ = MeasureTheory.snorm (↑↑f) p μ
@[simp]
theorem
MeasureTheory.Lp.norm_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : α → E)
(hf : MeasureTheory.Memℒp f p μ)
:
‖MeasureTheory.Memℒp.toLp f hf‖ = (MeasureTheory.snorm f p μ).toReal
@[simp]
theorem
MeasureTheory.Lp.nnnorm_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : α → E)
(hf : MeasureTheory.Memℒp f p μ)
:
‖MeasureTheory.Memℒp.toLp f hf‖₊ = (MeasureTheory.snorm f p μ).toNNReal
theorem
MeasureTheory.Lp.coe_nnnorm_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
↑‖MeasureTheory.Memℒp.toLp f hf‖₊ = MeasureTheory.snorm f p μ
theorem
MeasureTheory.Lp.dist_def
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
:
dist f g = (MeasureTheory.snorm (↑↑f - ↑↑g) p μ).toReal
theorem
MeasureTheory.Lp.edist_def
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
:
edist f g = MeasureTheory.snorm (↑↑f - ↑↑g) p μ
theorem
MeasureTheory.Lp.edist_dist
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
:
edist f g = ENNReal.ofReal (dist f g)
theorem
MeasureTheory.Lp.dist_edist
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
:
theorem
MeasureTheory.Lp.dist_eq_norm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(g : ↥(MeasureTheory.Lp E p μ))
:
@[simp]
theorem
MeasureTheory.Lp.edist_toLp_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : α → E)
(g : α → E)
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
edist (MeasureTheory.Memℒp.toLp f hf) (MeasureTheory.Memℒp.toLp g hg) = MeasureTheory.snorm (f - g) p μ
@[simp]
theorem
MeasureTheory.Lp.edist_toLp_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : α → E)
(hf : MeasureTheory.Memℒp f p μ)
:
edist (MeasureTheory.Memℒp.toLp f hf) 0 = MeasureTheory.snorm f p μ
@[simp]
theorem
MeasureTheory.Lp.nnnorm_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
@[simp]
theorem
MeasureTheory.Lp.norm_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
:
@[simp]
theorem
MeasureTheory.Lp.norm_measure_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p 0))
:
@[simp]
theorem
MeasureTheory.Lp.norm_exponent_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E 0 μ))
:
theorem
MeasureTheory.Lp.nnnorm_eq_zero_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : ↥(MeasureTheory.Lp E p μ)}
(hp : 0 < p)
:
theorem
MeasureTheory.Lp.norm_eq_zero_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : ↥(MeasureTheory.Lp E p μ)}
(hp : 0 < p)
:
theorem
MeasureTheory.Lp.eq_zero_iff_ae_eq_zero
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : ↥(MeasureTheory.Lp E p μ)}
:
@[simp]
theorem
MeasureTheory.Lp.nnnorm_neg
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
@[simp]
theorem
MeasureTheory.Lp.norm_neg
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{c : NNReal}
{f : ↥(MeasureTheory.Lp E p μ)}
{g : ↥(MeasureTheory.Lp F p μ)}
(h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊)
:
theorem
MeasureTheory.Lp.norm_le_mul_norm_of_ae_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{c : ℝ}
{f : ↥(MeasureTheory.Lp E p μ)}
{g : ↥(MeasureTheory.Lp F p μ)}
(h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖)
:
theorem
MeasureTheory.Lp.norm_le_norm_of_ae_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : ↥(MeasureTheory.Lp E p μ)}
{g : ↥(MeasureTheory.Lp F p μ)}
(h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖)
:
theorem
MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{c : NNReal}
{f : α →ₘ[μ] E}
{g : ↥(MeasureTheory.Lp F p μ)}
(h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ c * ‖↑↑g x‖₊)
:
f ∈ MeasureTheory.Lp E p μ
theorem
MeasureTheory.Lp.mem_Lp_of_ae_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{c : ℝ}
{f : α →ₘ[μ] E}
{g : ↥(MeasureTheory.Lp F p μ)}
(h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ c * ‖↑↑g x‖)
:
f ∈ MeasureTheory.Lp E p μ
theorem
MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α →ₘ[μ] E}
{g : ↥(MeasureTheory.Lp F p μ)}
(h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ ‖↑↑g x‖₊)
:
f ∈ MeasureTheory.Lp E p μ
theorem
MeasureTheory.Lp.mem_Lp_of_ae_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α →ₘ[μ] E}
{g : ↥(MeasureTheory.Lp F p μ)}
(h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ ‖↑↑g x‖)
:
f ∈ MeasureTheory.Lp E p μ
theorem
MeasureTheory.Lp.mem_Lp_of_ae_nnnorm_bound
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
{f : α →ₘ[μ] E}
(C : NNReal)
(hfC : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ C)
:
f ∈ MeasureTheory.Lp E p μ
theorem
MeasureTheory.Lp.mem_Lp_of_ae_bound
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
{f : α →ₘ[μ] E}
(C : ℝ)
(hfC : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ C)
:
f ∈ MeasureTheory.Lp E p μ
theorem
MeasureTheory.Lp.nnnorm_le_of_ae_bound
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
{f : ↥(MeasureTheory.Lp E p μ)}
{C : NNReal}
(hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C)
:
theorem
MeasureTheory.Lp.norm_le_of_ae_bound
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
{f : ↥(MeasureTheory.Lp E p μ)}
{C : ℝ}
(hC : 0 ≤ C)
(hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ C)
:
instance
MeasureTheory.Lp.instNormedAddCommGroup
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[hp : Fact (1 ≤ p)]
:
NormedAddCommGroup ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.instNormedAddCommGroup = let __src := { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }.toNormedAddCommGroup; NormedAddCommGroup.mk ⋯
theorem
MeasureTheory.Lp.const_smul_mem_Lp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
(c : 𝕜)
(f : ↥(MeasureTheory.Lp E p μ))
:
c • ↑f ∈ MeasureTheory.Lp E p μ
def
MeasureTheory.Lp.LpSubmodule
{α : Type u_1}
(E : Type u_2)
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
(𝕜 : Type u_5)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
:
The 𝕜-submodule of elements of α →ₘ[μ] E whose Lp norm is finite. This is Lp E p μ,
with extra structure.
Equations
- MeasureTheory.Lp.LpSubmodule E p μ 𝕜 = let __src := MeasureTheory.Lp E p μ; { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
Instances For
theorem
MeasureTheory.Lp.coe_LpSubmodule
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
:
(MeasureTheory.Lp.LpSubmodule E p μ 𝕜).toAddSubgroup = MeasureTheory.Lp E p μ
instance
MeasureTheory.Lp.instModule
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
:
Module 𝕜 ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.instModule = let __src := (MeasureTheory.Lp.LpSubmodule E p μ 𝕜).module; Module.mk ⋯ ⋯
theorem
MeasureTheory.Lp.coeFn_smul
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
(c : 𝕜)
(f : ↥(MeasureTheory.Lp E p μ))
:
instance
MeasureTheory.Lp.instIsCentralScalar
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
[Module 𝕜ᵐᵒᵖ E]
[BoundedSMul 𝕜ᵐᵒᵖ E]
[IsCentralScalar 𝕜 E]
:
IsCentralScalar 𝕜 ↥(MeasureTheory.Lp E p μ)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Lp.instSMulCommClass
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
{𝕜' : Type u_6}
[NormedRing 𝕜]
[NormedRing 𝕜']
[Module 𝕜 E]
[Module 𝕜' E]
[BoundedSMul 𝕜 E]
[BoundedSMul 𝕜' E]
[SMulCommClass 𝕜 𝕜' E]
:
SMulCommClass 𝕜 𝕜' ↥(MeasureTheory.Lp E p μ)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Lp.instIsScalarTower
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
{𝕜' : Type u_6}
[NormedRing 𝕜]
[NormedRing 𝕜']
[Module 𝕜 E]
[Module 𝕜' E]
[BoundedSMul 𝕜 E]
[BoundedSMul 𝕜' E]
[SMul 𝕜 𝕜']
[IsScalarTower 𝕜 𝕜' E]
:
IsScalarTower 𝕜 𝕜' ↥(MeasureTheory.Lp E p μ)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Lp.instBoundedSMul
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
[Fact (1 ≤ p)]
:
BoundedSMul 𝕜 ↥(MeasureTheory.Lp E p μ)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Lp.instNormedSpace
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[Fact (1 ≤ p)]
:
NormedSpace 𝕜 ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.instNormedSpace = NormedSpace.mk ⋯
theorem
MeasureTheory.Memℒp.toLp_const_smul
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
{f : α → E}
(c : 𝕜)
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp.toLp (c • f) ⋯ = c • MeasureTheory.Memℒp.toLp f hf
Indicator of a set as an element of Lᵖ #
For a set s with (hs : MeasurableSet s) and (hμs : μ s < ∞), we build
indicatorConstLp p hs hμs c, the element of Lp corresponding to s.indicator (fun _ => c).
theorem
MeasureTheory.snormEssSup_indicator_le
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
(s : Set α)
(f : α → G)
:
MeasureTheory.snormEssSup (s.indicator f) μ ≤ MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.snormEssSup_indicator_const_le
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
(s : Set α)
(c : G)
:
MeasureTheory.snormEssSup (s.indicator fun (x : α) => c) μ ≤ ↑‖c‖₊
theorem
MeasureTheory.snormEssSup_indicator_const_eq
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
(s : Set α)
(c : G)
(hμs : μ s ≠ 0)
:
MeasureTheory.snormEssSup (s.indicator fun (x : α) => c) μ = ↑‖c‖₊
theorem
MeasureTheory.snorm_indicator_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(f : α → E)
:
MeasureTheory.snorm (s.indicator f) p μ ≤ MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_indicator_const₀
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
{s : Set α}
{c : G}
(hs : MeasureTheory.NullMeasurableSet s μ)
(hp : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.snorm_indicator_const
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
{s : Set α}
{c : G}
(hs : MeasurableSet s)
(hp : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.snorm_indicator_const'
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
{s : Set α}
{c : G}
(hs : MeasurableSet s)
(hμs : μ s ≠ 0)
(hp : p ≠ 0)
:
theorem
MeasureTheory.snorm_indicator_const_le
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
{s : Set α}
(c : G)
(p : ENNReal)
:
theorem
MeasureTheory.Memℒp.indicator
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
(hs : MeasurableSet s)
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (s.indicator f) p μ
theorem
MeasureTheory.snormEssSup_indicator_eq_snormEssSup_restrict
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{s : Set α}
{f : α → F}
(hs : MeasurableSet s)
:
MeasureTheory.snormEssSup (s.indicator f) μ = MeasureTheory.snormEssSup f (μ.restrict s)
theorem
MeasureTheory.snorm_indicator_eq_snorm_restrict
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{s : Set α}
{f : α → F}
(hs : MeasurableSet s)
:
MeasureTheory.snorm (s.indicator f) p μ = MeasureTheory.snorm f p (μ.restrict s)
theorem
MeasureTheory.memℒp_indicator_iff_restrict
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.Memℒp (s.indicator f) p μ ↔ MeasureTheory.Memℒp f p (μ.restrict s)
theorem
MeasureTheory.Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
{q : ENNReal}
{f : α → E}
(hfq : MeasureTheory.Memℒp f q μ)
{s : Set α}
(hf : ∀ x ∉ s, f x = 0)
(hs : μ s ≠ ⊤)
(hpq : p ≤ q)
:
MeasureTheory.Memℒp f p μ
If a function is supported on a finite-measure set and belongs to ℒ^p, then it belongs to
ℒ^q for any q ≤ p.
theorem
MeasureTheory.memℒp_indicator_const
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(p : ENNReal)
(hs : MeasurableSet s)
(c : E)
(hμsc : c = 0 ∨ μ s ≠ ⊤)
:
MeasureTheory.Memℒp (s.indicator fun (x : α) => c) p μ
theorem
MeasureTheory.exists_snorm_indicator_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hp : p ≠ ⊤)
(c : E)
{ε : ENNReal}
(hε : ε ≠ 0)
:
The ℒ^p norm of the indicator of a set is uniformly small if the set itself has small measure,
for any p < ∞. Given here as an existential ∀ ε > 0, ∃ η > 0, ... to avoid later
management of ℝ≥0∞-arithmetic.
theorem
MeasureTheory.Memℒp.piecewise
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{s : Set α}
[DecidablePred fun (x : α) => x ∈ s]
{g : α → E}
(hs : MeasurableSet s)
(hf : MeasureTheory.Memℒp f p (μ.restrict s))
(hg : MeasureTheory.Memℒp g p (μ.restrict sᶜ))
:
MeasureTheory.Memℒp (s.piecewise f g) p μ
theorem
HasCompactSupport.memℒp_of_bound
{E : Type u_2}
{p : ENNReal}
[NormedAddCommGroup E]
{X : Type u_5}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
{f : X → E}
(hf : HasCompactSupport f)
(h2f : MeasureTheory.AEStronglyMeasurable f μ)
(C : ℝ)
(hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C)
:
MeasureTheory.Memℒp f p μ
A bounded measurable function with compact support is in L^p.
theorem
Continuous.memℒp_of_hasCompactSupport
{E : Type u_2}
{p : ENNReal}
[NormedAddCommGroup E]
{X : Type u_5}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
[OpensMeasurableSpace X]
{f : X → E}
(hf : Continuous f)
(h'f : HasCompactSupport f)
:
MeasureTheory.Memℒp f p μ
A continuous function with compact support is in L^p.
def
MeasureTheory.indicatorConstLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
(p : ENNReal)
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : E)
:
↥(MeasureTheory.Lp E p μ)
Indicator of a set as an element of Lp.
Equations
- MeasureTheory.indicatorConstLp p hs hμs c = MeasureTheory.Memℒp.toLp (s.indicator fun (x : α) => c) ⋯
Instances For
theorem
MeasureTheory.indicatorConstLp_add
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
{c' : E}
:
MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p hs hμs c' = MeasureTheory.indicatorConstLp p hs hμs (c + c')
A version of Set.indicator_add for MeasureTheory.indicatorConstLp.
theorem
MeasureTheory.indicatorConstLp_sub
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
{c' : E}
:
MeasureTheory.indicatorConstLp p hs hμs c - MeasureTheory.indicatorConstLp p hs hμs c' = MeasureTheory.indicatorConstLp p hs hμs (c - c')
A version of Set.indicator_sub for MeasureTheory.indicatorConstLp.
theorem
MeasureTheory.indicatorConstLp_coeFn
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
:
↑↑(MeasureTheory.indicatorConstLp p hs hμs c) =ᵐ[μ] s.indicator fun (x : α) => c
theorem
MeasureTheory.indicatorConstLp_coeFn_mem
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
:
∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = c
theorem
MeasureTheory.indicatorConstLp_coeFn_nmem
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
:
∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = 0
theorem
MeasureTheory.norm_indicatorConstLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
theorem
MeasureTheory.norm_indicatorConstLp_top
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
(hμs_ne_zero : μ s ≠ 0)
:
theorem
MeasureTheory.norm_indicatorConstLp'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
(hp_pos : p ≠ 0)
(hμs_pos : μ s ≠ 0)
:
theorem
MeasureTheory.norm_indicatorConstLp_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
:
theorem
MeasureTheory.edist_indicatorConstLp_eq_nnnorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
{t : Set α}
{ht : MeasurableSet t}
{hμt : μ t ≠ ⊤}
:
edist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) = ↑‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖₊
theorem
MeasureTheory.dist_indicatorConstLp_eq_norm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{hs : MeasurableSet s}
{hμs : μ s ≠ ⊤}
{c : E}
{t : Set α}
{ht : MeasurableSet t}
{hμt : μ t ≠ ⊤}
:
dist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) = ‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖
@[simp]
theorem
MeasureTheory.indicatorConstLp_empty
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{c : E}
:
MeasureTheory.indicatorConstLp p ⋯ ⋯ c = 0
theorem
MeasureTheory.indicatorConstLp_inj
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{t : Set α}
(hs : MeasurableSet s)
(hsμ : μ s ≠ ⊤)
(ht : MeasurableSet t)
(htμ : μ t ≠ ⊤)
{c : E}
(hc : c ≠ 0)
(h : MeasureTheory.indicatorConstLp p hs hsμ c = MeasureTheory.indicatorConstLp p ht htμ c)
:
theorem
MeasureTheory.memℒp_add_of_disjoint
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
{g : α → E}
(h : Disjoint (Function.support f) (Function.support g))
(hf : MeasureTheory.StronglyMeasurable f)
(hg : MeasureTheory.StronglyMeasurable g)
:
MeasureTheory.Memℒp (f + g) p μ ↔ MeasureTheory.Memℒp f p μ ∧ MeasureTheory.Memℒp g p μ
theorem
MeasureTheory.indicatorConstLp_disjoint_union
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{s : Set α}
{t : Set α}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
(hμs : μ s ≠ ⊤)
(hμt : μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(c : E)
:
MeasureTheory.indicatorConstLp p ⋯ ⋯ c = MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p ht hμt c
The indicator of a disjoint union of two sets is the sum of the indicators of the sets.
def
MeasureTheory.Lp.const
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
:
E →+ ↥(MeasureTheory.Lp E p μ)
Constant function as an element of MeasureTheory.Lp for a finite measure.
Equations
- MeasureTheory.Lp.const p μ = { toFun := fun (c : E) => ⟨MeasureTheory.AEEqFun.const α c, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
MeasureTheory.Lp.coeFn_const
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
:
↑↑((MeasureTheory.Lp.const p μ) c) =ᵐ[μ] Function.const α c
@[simp]
theorem
MeasureTheory.Lp.const_val
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
:
↑((MeasureTheory.Lp.const p μ) c) = MeasureTheory.AEEqFun.const α c
@[simp]
theorem
MeasureTheory.Memℒp.toLp_const
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
:
MeasureTheory.Memℒp.toLp (fun (x : α) => c) ⋯ = (MeasureTheory.Lp.const p μ) c
@[simp]
theorem
MeasureTheory.indicatorConstLp_univ
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
:
MeasureTheory.indicatorConstLp p ⋯ ⋯ c = (MeasureTheory.Lp.const p μ) c
theorem
MeasureTheory.Lp.norm_const
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
[NeZero μ]
(hp_zero : p ≠ 0)
:
theorem
MeasureTheory.Lp.norm_const'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
(hp_zero : p ≠ 0)
(hp_top : p ≠ ⊤)
:
theorem
MeasureTheory.Lp.norm_const_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(c : E)
:
@[simp]
theorem
MeasureTheory.Lp.constₗ_apply
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
(a : E)
:
(MeasureTheory.Lp.constₗ p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a
def
MeasureTheory.Lp.constₗ
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
:
E →ₗ[𝕜] ↥(MeasureTheory.Lp E p μ)
MeasureTheory.Lp.const as a LinearMap.
Equations
- MeasureTheory.Lp.constₗ p μ 𝕜 = { toFun := ⇑(MeasureTheory.Lp.const p μ), map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
MeasureTheory.Lp.constL_apply
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[Fact (1 ≤ p)]
(a : E)
:
(MeasureTheory.Lp.constL p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a
def
MeasureTheory.Lp.constL
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[NormedField 𝕜]
[NormedSpace 𝕜 E]
[Fact (1 ≤ p)]
:
E →L[𝕜] ↥(MeasureTheory.Lp E p μ)
Equations
- MeasureTheory.Lp.constL p μ 𝕜 = (MeasureTheory.Lp.constₗ p μ 𝕜).mkContinuous ((μ Set.univ).toReal ^ (1 / p.toReal)) ⋯
Instances For
theorem
MeasureTheory.Lp.norm_constL_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[Fact (1 ≤ p)]
:
theorem
MeasureTheory.Memℒp.norm_rpow_div
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(q : ENNReal)
:
MeasureTheory.Memℒp (fun (x : α) => ‖f x‖ ^ q.toReal) (p / q) μ
theorem
MeasureTheory.memℒp_norm_rpow_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{q : ENNReal}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(q_zero : q ≠ 0)
(q_top : q ≠ ⊤)
:
MeasureTheory.Memℒp (fun (x : α) => ‖f x‖ ^ q.toReal) (p / q) μ ↔ MeasureTheory.Memℒp f p μ
theorem
MeasureTheory.Memℒp.norm_rpow
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
MeasureTheory.Memℒp (fun (x : α) => ‖f x‖ ^ p.toReal) 1 μ
theorem
MeasureTheory.AEEqFun.compMeasurePreserving_mem_Lp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
{g : β →ₘ[μb] E}
(hg : g ∈ MeasureTheory.Lp E p μb)
{f : α → β}
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
g.compMeasurePreserving f hf ∈ MeasureTheory.Lp E p μ
Composition with a measure preserving function #
def
MeasureTheory.Lp.compMeasurePreserving
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
(f : α → β)
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
↥(MeasureTheory.Lp E p μb) →+ ↥(MeasureTheory.Lp E p μ)
Composition of an L^p function with a measure preserving function is an L^p function.
Equations
- MeasureTheory.Lp.compMeasurePreserving f hf = { toFun := fun (g : ↥(MeasureTheory.Lp E p μb)) => ⟨(↑g).compMeasurePreserving f hf, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
MeasureTheory.Lp.compMeasurePreserving_val
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
{f : α → β}
(g : ↥(MeasureTheory.Lp E p μb))
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) = (↑g).compMeasurePreserving f hf
theorem
MeasureTheory.Lp.coeFn_compMeasurePreserving
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
{f : α → β}
(g : ↥(MeasureTheory.Lp E p μb))
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
↑↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) =ᵐ[μ] ↑↑g ∘ f
@[simp]
theorem
MeasureTheory.Lp.norm_compMeasurePreserving
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
{f : α → β}
(g : ↥(MeasureTheory.Lp E p μb))
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
@[simp]
theorem
MeasureTheory.Lp.compMeasurePreservingₗ_apply
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
(𝕜 : Type u_6)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
(f : α → β)
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
∀ (a : ↥(MeasureTheory.Lp E p μb)),
(MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf) a = (↑(MeasureTheory.Lp.compMeasurePreserving f hf)).toFun a
def
MeasureTheory.Lp.compMeasurePreservingₗ
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
(𝕜 : Type u_6)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
(f : α → β)
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
↥(MeasureTheory.Lp E p μb) →ₗ[𝕜] ↥(MeasureTheory.Lp E p μ)
MeasureTheory.Lp.compMeasurePreserving as a linear map.
Equations
- MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf = let __spread.0 := MeasureTheory.Lp.compMeasurePreserving f hf; { toFun := (↑__spread.0).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
MeasureTheory.Lp.compMeasurePreservingₗᵢ_toFun_coe
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
(𝕜 : Type u_6)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
[Fact (1 ≤ p)]
(f : α → β)
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
∀ (a : ↥(MeasureTheory.Lp E p μb)),
↑((MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 f hf) a) = (↑a).compMeasurePreserving f hf
@[simp]
theorem
MeasureTheory.Lp.compMeasurePreservingₗᵢ_apply_coe
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
(𝕜 : Type u_6)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
[Fact (1 ≤ p)]
(f : α → β)
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
∀ (a : ↥(MeasureTheory.Lp E p μb)),
↑((MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 f hf) a) = (↑a).compMeasurePreserving f hf
def
MeasureTheory.Lp.compMeasurePreservingₗᵢ
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{β : Type u_5}
[MeasurableSpace β]
{μb : MeasureTheory.Measure β}
(𝕜 : Type u_6)
[NormedRing 𝕜]
[Module 𝕜 E]
[BoundedSMul 𝕜 E]
[Fact (1 ≤ p)]
(f : α → β)
(hf : MeasureTheory.MeasurePreserving f μ μb)
:
↥(MeasureTheory.Lp E p μb) →ₗᵢ[𝕜] ↥(MeasureTheory.Lp E p μ)
MeasureTheory.Lp.compMeasurePreserving as a linear isometry.
Equations
- MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 f hf = { toLinearMap := MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf, norm_map' := ⋯ }
Instances For
Composition on L^p #
We show that Lipschitz functions vanishing at zero act by composition on L^p, and specialize
this to the composition with continuous linear maps, and to the definition of the positive
part of an L^p function.
theorem
LipschitzWith.comp_memℒp
{p : ENNReal}
{α : Type u_5}
{E : Type u_6}
{F : Type u_7}
{K : NNReal}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : E → F}
(hg : LipschitzWith K g)
(g0 : g 0 = 0)
(hL : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (g ∘ f) p μ
theorem
MeasureTheory.Memℒp.of_comp_antilipschitzWith
{p : ENNReal}
{α : Type u_5}
{E : Type u_6}
{F : Type u_7}
{K' : NNReal}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : E → F}
(hL : MeasureTheory.Memℒp (g ∘ f) p μ)
(hg : UniformContinuous g)
(hg' : AntilipschitzWith K' g)
(g0 : g 0 = 0)
:
MeasureTheory.Memℒp f p μ
theorem
LipschitzWith.memℒp_comp_iff_of_antilipschitz
{p : ENNReal}
{α : Type u_5}
{E : Type u_6}
{F : Type u_7}
{K : NNReal}
{K' : NNReal}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : E → F}
(hg : LipschitzWith K g)
(hg' : AntilipschitzWith K' g)
(g0 : g 0 = 0)
:
MeasureTheory.Memℒp (g ∘ f) p μ ↔ MeasureTheory.Memℒp f p μ
def
LipschitzWith.compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{g : E → F}
{c : NNReal}
(hg : LipschitzWith c g)
(g0 : g 0 = 0)
(f : ↥(MeasureTheory.Lp E p μ))
:
↥(MeasureTheory.Lp F p μ)
When g is a Lipschitz function sending 0 to 0 and f is in Lp, then g ∘ f is well
defined as an element of Lp.
Equations
- hg.compLp g0 f = ⟨MeasureTheory.AEEqFun.comp g ⋯ ↑f, ⋯⟩
Instances For
theorem
LipschitzWith.coeFn_compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{g : E → F}
{c : NNReal}
(hg : LipschitzWith c g)
(g0 : g 0 = 0)
(f : ↥(MeasureTheory.Lp E p μ))
:
@[simp]
theorem
LipschitzWith.compLp_zero
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{g : E → F}
{c : NNReal}
(hg : LipschitzWith c g)
(g0 : g 0 = 0)
:
hg.compLp g0 0 = 0
theorem
LipschitzWith.norm_compLp_sub_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{g : E → F}
{c : NNReal}
(hg : LipschitzWith c g)
(g0 : g 0 = 0)
(f : ↥(MeasureTheory.Lp E p μ))
(f' : ↥(MeasureTheory.Lp E p μ))
:
theorem
LipschitzWith.norm_compLp_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{g : E → F}
{c : NNReal}
(hg : LipschitzWith c g)
(g0 : g 0 = 0)
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
LipschitzWith.lipschitzWith_compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{g : E → F}
{c : NNReal}
[Fact (1 ≤ p)]
(hg : LipschitzWith c g)
(g0 : g 0 = 0)
:
LipschitzWith c (hg.compLp g0)
theorem
LipschitzWith.continuous_compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{g : E → F}
{c : NNReal}
[Fact (1 ≤ p)]
(hg : LipschitzWith c g)
(g0 : g 0 = 0)
:
Continuous (hg.compLp g0)
def
ContinuousLinearMap.compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
↥(MeasureTheory.Lp F p μ)
Composing f : Lp with L : E →L[𝕜] F.
Equations
- L.compLp f = ⋯.compLp ⋯ f
Instances For
theorem
ContinuousLinearMap.coeFn_compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
∀ᵐ (a : α) ∂μ, ↑↑(L.compLp f) a = L (↑↑f a)
theorem
ContinuousLinearMap.coeFn_compLp'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
ContinuousLinearMap.comp_memℒp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
MeasureTheory.Memℒp (⇑L ∘ ↑↑f) p μ
theorem
ContinuousLinearMap.comp_memℒp'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (⇑L ∘ f) p μ
theorem
MeasureTheory.Memℒp.ofReal
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{K : Type u_6}
[RCLike K]
{f : α → ℝ}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (fun (x : α) => ↑(f x)) p μ
theorem
MeasureTheory.memℒp_re_im_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{K : Type u_6}
[RCLike K]
{f : α → K}
:
MeasureTheory.Memℒp (fun (x : α) => RCLike.re (f x)) p μ ∧ MeasureTheory.Memℒp (fun (x : α) => RCLike.im (f x)) p μ ↔ MeasureTheory.Memℒp f p μ
theorem
ContinuousLinearMap.add_compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
(L' : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
ContinuousLinearMap.smul_compLp
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
{𝕜' : Type u_6}
[NormedRing 𝕜']
[Module 𝕜' F]
[BoundedSMul 𝕜' F]
[SMulCommClass 𝕜 𝕜' F]
(c : 𝕜')
(L : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
theorem
ContinuousLinearMap.norm_compLp_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
def
ContinuousLinearMap.compLpₗ
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
(L : E →L[𝕜] F)
:
↥(MeasureTheory.Lp E p μ) →ₗ[𝕜] ↥(MeasureTheory.Lp F p μ)
Composing f : Lp E p μ with L : E →L[𝕜] F, seen as a 𝕜-linear map on Lp E p μ.
Equations
- ContinuousLinearMap.compLpₗ p μ L = { toFun := fun (f : ↥(MeasureTheory.Lp E p μ)) => L.compLp f, map_add' := ⋯, map_smul' := ⋯ }
Instances For
def
ContinuousLinearMap.compLpL
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[Fact (1 ≤ p)]
(L : E →L[𝕜] F)
:
↥(MeasureTheory.Lp E p μ) →L[𝕜] ↥(MeasureTheory.Lp F p μ)
Composing f : Lp E p μ with L : E →L[𝕜] F, seen as a continuous 𝕜-linear map on
Lp E p μ. See also the similar
LinearMap.compLeftfor functions,ContinuousLinearMap.compLeftContinuousfor continuous functions,ContinuousLinearMap.compLeftContinuousBoundedfor bounded continuous functions,ContinuousLinearMap.compLeftContinuousCompactfor continuous functions on compact spaces.
Equations
- ContinuousLinearMap.compLpL p μ L = (ContinuousLinearMap.compLpₗ p μ L).mkContinuous ‖L‖ ⋯
Instances For
theorem
ContinuousLinearMap.coeFn_compLpL
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[Fact (1 ≤ p)]
(L : E →L[𝕜] F)
(f : ↥(MeasureTheory.Lp E p μ))
:
↑↑((ContinuousLinearMap.compLpL p μ L) f) =ᵐ[μ] fun (a : α) => L (↑↑f a)
theorem
ContinuousLinearMap.add_compLpL
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[Fact (1 ≤ p)]
(L : E →L[𝕜] F)
(L' : E →L[𝕜] F)
:
ContinuousLinearMap.compLpL p μ (L + L') = ContinuousLinearMap.compLpL p μ L + ContinuousLinearMap.compLpL p μ L'
theorem
ContinuousLinearMap.smul_compLpL
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[Fact (1 ≤ p)]
{𝕜' : Type u_6}
[NormedRing 𝕜']
[Module 𝕜' F]
[BoundedSMul 𝕜' F]
[SMulCommClass 𝕜 𝕜' F]
(c : 𝕜')
(L : E →L[𝕜] F)
:
ContinuousLinearMap.compLpL p μ (c • L) = c • ContinuousLinearMap.compLpL p μ L
theorem
ContinuousLinearMap.norm_compLpL_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 F]
[Fact (1 ≤ p)]
(L : E →L[𝕜] F)
:
theorem
MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{s : Set α}
[NormedSpace ℝ F]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(x : F)
:
MeasureTheory.indicatorConstLp 2 hs hμs x = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (MeasureTheory.indicatorConstLp 2 hs hμs 1)
theorem
MeasureTheory.Memℒp.pos_part
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (fun (x : α) => max (f x) 0) p μ
theorem
MeasureTheory.Memℒp.neg_part
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (fun (x : α) => max (-f x) 0) p μ
def
MeasureTheory.Lp.posPart
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp ℝ p μ))
:
↥(MeasureTheory.Lp ℝ p μ)
Positive part of a function in L^p.
Equations
Instances For
def
MeasureTheory.Lp.negPart
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp ℝ p μ))
:
↥(MeasureTheory.Lp ℝ p μ)
Negative part of a function in L^p.
Equations
Instances For
theorem
MeasureTheory.Lp.coe_posPart
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp ℝ p μ))
:
↑(MeasureTheory.Lp.posPart f) = (↑f).posPart
theorem
MeasureTheory.Lp.coeFn_posPart
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp ℝ p μ))
:
↑↑(MeasureTheory.Lp.posPart f) =ᵐ[μ] fun (a : α) => max (↑↑f a) 0
theorem
MeasureTheory.Lp.coeFn_negPart_eq_max
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp ℝ p μ))
:
∀ᵐ (a : α) ∂μ, ↑↑(MeasureTheory.Lp.negPart f) a = max (-↑↑f a) 0
theorem
MeasureTheory.Lp.coeFn_negPart
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
(f : ↥(MeasureTheory.Lp ℝ p μ))
:
∀ᵐ (a : α) ∂μ, ↑↑(MeasureTheory.Lp.negPart f) a = -min (↑↑f a) 0
theorem
MeasureTheory.Lp.continuous_posPart
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[Fact (1 ≤ p)]
:
Continuous fun (f : ↥(MeasureTheory.Lp ℝ p μ)) => MeasureTheory.Lp.posPart f
theorem
MeasureTheory.Lp.continuous_negPart
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[Fact (1 ≤ p)]
:
Continuous fun (f : ↥(MeasureTheory.Lp ℝ p μ)) => MeasureTheory.Lp.negPart f
L^p is a complete space #
We show that L^p is a complete space for 1 ≤ p.
theorem
MeasureTheory.Lp.snorm'_lim_eq_lintegral_liminf
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
{ι : Type u_5}
[Nonempty ι]
[LinearOrder ι]
{f : ι → α → G}
{p : ℝ}
(hp_nonneg : 0 ≤ p)
{f_lim : α → G}
(h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x)))
:
MeasureTheory.snorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun (m : ι) => ↑‖f m a‖₊ ^ p) Filter.atTop ∂μ) ^ (1 / p)
theorem
MeasureTheory.Lp.snorm'_lim_le_liminf_snorm'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{f : ℕ → α → E}
{p : ℝ}
(hp_pos : 0 < p)
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
{f_lim : α → E}
(h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x)))
:
MeasureTheory.snorm' f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => MeasureTheory.snorm' (f n) p μ) Filter.atTop
theorem
MeasureTheory.Lp.snorm_exponent_top_lim_eq_essSup_liminf
{α : Type u_1}
{G : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup G]
{ι : Type u_5}
[Nonempty ι]
[LinearOrder ι]
{f : ι → α → G}
{f_lim : α → G}
(h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x)))
:
MeasureTheory.snorm f_lim ⊤ μ = essSup (fun (x : α) => Filter.liminf (fun (m : ι) => ↑‖f m x‖₊) Filter.atTop) μ
theorem
MeasureTheory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top
{α : Type u_1}
{F : Type u_3}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{ι : Type u_5}
[Nonempty ι]
[Countable ι]
[LinearOrder ι]
{f : ι → α → F}
{f_lim : α → F}
(h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x)))
:
MeasureTheory.snorm f_lim ⊤ μ ≤ Filter.liminf (fun (n : ι) => MeasureTheory.snorm (f n) ⊤ μ) Filter.atTop
theorem
MeasureTheory.Lp.snorm_lim_le_liminf_snorm
{α : Type u_1}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{f : ℕ → α → E}
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(f_lim : α → E)
(h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x)))
:
MeasureTheory.snorm f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => MeasureTheory.snorm (f n) p μ) Filter.atTop
theorem
MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
{fi : Filter ι}
[Fact (1 ≤ p)]
(f : ι → ↥(MeasureTheory.Lp E p μ))
(f_lim : ↥(MeasureTheory.Lp E p μ))
:
Filter.Tendsto f fi (nhds f_lim) ↔ Filter.Tendsto (fun (n : ι) => MeasureTheory.snorm (↑↑(f n) - ↑↑f_lim) p μ) fi (nhds 0)
theorem
MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
{fi : Filter ι}
[Fact (1 ≤ p)]
(f : ι → ↥(MeasureTheory.Lp E p μ))
(f_lim : α → E)
(f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ)
:
Filter.Tendsto f fi (nhds (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun (n : ι) => MeasureTheory.snorm (↑↑(f n) - f_lim) p μ) fi (nhds 0)
theorem
MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp''
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
{fi : Filter ι}
[Fact (1 ≤ p)]
(f : ι → α → E)
(f_ℒp : ∀ (n : ι), MeasureTheory.Memℒp (f n) p μ)
(f_lim : α → E)
(f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ)
:
Filter.Tendsto (fun (n : ι) => MeasureTheory.Memℒp.toLp (f n) ⋯) fi (nhds (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun (n : ι) => MeasureTheory.snorm (f n - f_lim) p μ) fi (nhds 0)
theorem
MeasureTheory.Lp.tendsto_Lp_of_tendsto_ℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
{fi : Filter ι}
[Fact (1 ≤ p)]
{f : ι → ↥(MeasureTheory.Lp E p μ)}
(f_lim : α → E)
(f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ)
(h_tendsto : Filter.Tendsto (fun (n : ι) => MeasureTheory.snorm (↑↑(f n) - f_lim) p μ) fi (nhds 0))
:
Filter.Tendsto f fi (nhds (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp))
theorem
MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_ℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{ι : Type u_5}
[Nonempty ι]
[SemilatticeSup ι]
[hp : Fact (1 ≤ p)]
(f : ι → ↥(MeasureTheory.Lp E p μ))
:
CauchySeq f ↔ Filter.Tendsto (fun (n : ι × ι) => MeasureTheory.snorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) Filter.atTop (nhds 0)
theorem
MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_ℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[hp : Fact (1 ≤ p)]
(H : ∀ (f : ℕ → α → E),
(∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) →
∀ (B : ℕ → ENNReal),
∑' (i : ℕ), B i < ⊤ →
(∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.snorm (f n - f m) p μ < B N) →
∃ (f_lim : α → E),
MeasureTheory.Memℒp f_lim p μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.snorm (f n - f_lim) p μ) Filter.atTop (nhds 0))
:
CompleteSpace ↥(MeasureTheory.Lp E p μ)
Prove that controlled Cauchy sequences of ℒp have limits in ℒp #
theorem
MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
{f : ℕ → α → E}
{p : ℝ}
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(hp1 : 1 ≤ p)
{B : ℕ → ENNReal}
(hB : ∑' (i : ℕ), B i ≠ ⊤)
(h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.snorm' (f n - f m) p μ < B N)
:
∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)
theorem
MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
{f : ℕ → α → E}
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(hp : 1 ≤ p)
{B : ℕ → ENNReal}
(hB : ∑' (i : ℕ), B i ≠ ⊤)
(h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.snorm (f n - f m) p μ < B N)
:
∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)
theorem
MeasureTheory.Lp.cauchy_tendsto_of_tendsto
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{f : ℕ → α → E}
(hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
(f_lim : α → E)
{B : ℕ → ENNReal}
(hB : ∑' (i : ℕ), B i ≠ ⊤)
(h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.snorm (f n - f m) p μ < B N)
(h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x)))
:
Filter.Tendsto (fun (n : ℕ) => MeasureTheory.snorm (f n - f_lim) p μ) Filter.atTop (nhds 0)
theorem
MeasureTheory.Lp.memℒp_of_cauchy_tendsto
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hp : 1 ≤ p)
{f : ℕ → α → E}
(hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ)
(f_lim : α → E)
(h_lim_meas : MeasureTheory.AEStronglyMeasurable f_lim μ)
(h_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.snorm (f n - f_lim) p μ) Filter.atTop (nhds 0))
:
MeasureTheory.Memℒp f_lim p μ
theorem
MeasureTheory.Lp.cauchy_complete_ℒp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
(hp : 1 ≤ p)
{f : ℕ → α → E}
(hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ)
{B : ℕ → ENNReal}
(hB : ∑' (i : ℕ), B i ≠ ⊤)
(h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.snorm (f n - f m) p μ < B N)
:
∃ (f_lim : α → E),
MeasureTheory.Memℒp f_lim p μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.snorm (f n - f_lim) p μ) Filter.atTop (nhds 0)
instance
MeasureTheory.Lp.instCompleteSpace
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
[hp : Fact (1 ≤ p)]
:
CompleteSpace ↥(MeasureTheory.Lp E p μ)
Equations
- ⋯ = ⋯
def
MeasureTheory.Lp.boundedContinuousFunction
{α : Type u_1}
(E : Type u_2)
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
:
AddSubgroup ↥(MeasureTheory.Lp E p μ)
An additive subgroup of Lp E p μ, consisting of the equivalence classes which contain a
bounded continuous representative.
Equations
- MeasureTheory.Lp.boundedContinuousFunction E p μ = ((ContinuousMap.toAEEqFunAddHom μ).comp (BoundedContinuousFunction.toContinuousMapAddHom α E)).range.addSubgroupOf (MeasureTheory.Lp E p μ)
Instances For
theorem
MeasureTheory.Lp.mem_boundedContinuousFunction_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
{f : ↥(MeasureTheory.Lp E p μ)}
:
f ∈ MeasureTheory.Lp.boundedContinuousFunction E p μ ↔ ∃ (f₀ : BoundedContinuousFunction α E), ContinuousMap.toAEEqFun μ f₀.toContinuousMap = ↑f
By definition, the elements of Lp.boundedContinuousFunction E p μ are the elements of
Lp E p μ which contain a bounded continuous representative.
theorem
BoundedContinuousFunction.mem_Lp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E)
:
ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ MeasureTheory.Lp E p μ
A bounded continuous function on a finite-measure space is in Lp.
theorem
BoundedContinuousFunction.Lp_nnnorm_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E)
:
‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ MeasureTheory.measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊
The Lp-norm of a bounded continuous function is at most a constant (depending on the measure
of the whole space) times its sup-norm.
theorem
BoundedContinuousFunction.Lp_norm_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E)
:
‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹ * ‖f‖
The Lp-norm of a bounded continuous function is at most a constant (depending on the measure
of the whole space) times its sup-norm.
def
BoundedContinuousFunction.toLpHom
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
[Fact (1 ≤ p)]
:
NormedAddGroupHom (BoundedContinuousFunction α E) ↥(MeasureTheory.Lp E p μ)
The normed group homomorphism of considering a bounded continuous function on a finite-measure
space as an element of Lp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
BoundedContinuousFunction.range_toLpHom
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
[Fact (1 ≤ p)]
:
(BoundedContinuousFunction.toLpHom p μ).range = MeasureTheory.Lp.boundedContinuousFunction E p μ
def
BoundedContinuousFunction.toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
BoundedContinuousFunction α E →L[𝕜] ↥(MeasureTheory.Lp E p μ)
The bounded linear map of considering a bounded continuous function on a finite-measure space
as an element of Lp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
BoundedContinuousFunction.coeFn_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
(f : BoundedContinuousFunction α E)
:
↑↑((BoundedContinuousFunction.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f
theorem
BoundedContinuousFunction.range_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
(LinearMap.range (BoundedContinuousFunction.toLp p μ 𝕜)).toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ
theorem
BoundedContinuousFunction.toLp_norm_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
:
‖BoundedContinuousFunction.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹
theorem
BoundedContinuousFunction.toLp_inj
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
{f : BoundedContinuousFunction α E}
{g : BoundedContinuousFunction α E}
[μ.IsOpenPosMeasure]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
(BoundedContinuousFunction.toLp p μ 𝕜) f = (BoundedContinuousFunction.toLp p μ 𝕜) g ↔ f = g
theorem
BoundedContinuousFunction.toLp_injective
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[μ.IsOpenPosMeasure]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
def
ContinuousMap.toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_5)
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
The bounded linear map of considering a continuous function on a compact finite-measure
space α as an element of Lp. By definition, the norm on C(α, E) is the sup-norm, transferred
from the space α →ᵇ E of bounded continuous functions, so this construction is just a matter of
transferring the structure from BoundedContinuousFunction.toLp along the isometry.
Equations
- ContinuousMap.toLp p μ 𝕜 = (BoundedContinuousFunction.toLp p μ 𝕜).comp (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toLinearIsometry.toContinuousLinearMap
Instances For
theorem
ContinuousMap.range_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
(LinearMap.range (ContinuousMap.toLp p μ 𝕜)).toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ
theorem
ContinuousMap.coeFn_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
(f : C(α, E))
:
↑↑((ContinuousMap.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f
theorem
ContinuousMap.toLp_def
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
(f : C(α, E))
:
(ContinuousMap.toLp p μ 𝕜) f = (BoundedContinuousFunction.toLp p μ 𝕜) ((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f)
@[simp]
theorem
ContinuousMap.toLp_comp_toContinuousMap
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
(f : BoundedContinuousFunction α E)
:
(ContinuousMap.toLp p μ 𝕜) f.toContinuousMap = (BoundedContinuousFunction.toLp p μ 𝕜) f
@[simp]
theorem
ContinuousMap.coe_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
(f : C(α, E))
:
↑((ContinuousMap.toLp p μ 𝕜) f) = ContinuousMap.toAEEqFun μ f
theorem
ContinuousMap.toLp_injective
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[μ.IsOpenPosMeasure]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
Function.Injective ⇑(ContinuousMap.toLp p μ 𝕜)
theorem
ContinuousMap.toLp_inj
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
{f : C(α, E)}
{g : C(α, E)}
[μ.IsOpenPosMeasure]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
:
(ContinuousMap.toLp p μ 𝕜) f = (ContinuousMap.toLp p μ 𝕜) g ↔ f = g
theorem
ContinuousMap.hasSum_of_hasSum_Lp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
{β : Type u_6}
[μ.IsOpenPosMeasure]
[NormedField 𝕜]
[NormedSpace 𝕜 E]
{g : β → C(α, E)}
{f : C(α, E)}
(hg : Summable g)
(hg2 : HasSum (⇑(ContinuousMap.toLp p μ 𝕜) ∘ g) ((ContinuousMap.toLp p μ 𝕜) f))
:
HasSum g f
If a sum of continuous functions g n is convergent, and the same sum converges in Lᵖ to h,
then in fact g n converges uniformly to h.
theorem
ContinuousMap.toLp_norm_eq_toLp_norm_coe
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
:
‖ContinuousMap.toLp p μ 𝕜‖ = ‖BoundedContinuousFunction.toLp p μ 𝕜‖
theorem
ContinuousMap.toLp_norm_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup E]
[TopologicalSpace α]
[BorelSpace α]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5}
[Fact (1 ≤ p)]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
:
‖ContinuousMap.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹
Bound for the operator norm of ContinuousMap.toLp.
theorem
MeasureTheory.Lp.pow_mul_meas_ge_le_norm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(ε : ENNReal)
:
theorem
MeasureTheory.Lp.mul_meas_ge_le_pow_norm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(ε : ENNReal)
:
theorem
MeasureTheory.Lp.mul_meas_ge_le_pow_norm'
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(ε : ENNReal)
:
A version of Markov's inequality with elements of Lp.
theorem
MeasureTheory.Lp.meas_ge_le_mul_pow_norm
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(f : ↥(MeasureTheory.Lp E p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
{ε : ENNReal}
(hε : ε ≠ 0)
: