Continuous functions in Lp space #
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.
def
MeasureTheory.Lp.boundedContinuousFunction
{α : Type u_1}
(E : Type u_2)
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
:
AddSubgroup ↥(Lp E p μ)
An additive subgroup of Lp E p μ, consisting of the equivalence classes which contain a
bounded continuous representative.
Equations
Instances For
theorem
MeasureTheory.Lp.mem_boundedContinuousFunction_iff
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
{f : ↥(Lp E p μ)}
:
f ∈ 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 α}
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E)
:
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 α}
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E)
:
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 α}
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[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 α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[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
Instances For
theorem
BoundedContinuousFunction.range_toLpHom
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
[Fact (1 ≤ p)]
:
noncomputable def
BoundedContinuousFunction.toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_3)
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
:
The bounded linear map of considering a bounded continuous function on a finite-measure space
as an element of Lp.
Equations
Instances For
theorem
BoundedContinuousFunction.coeFn_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_3)
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : BoundedContinuousFunction α E)
:
theorem
BoundedContinuousFunction.range_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
:
theorem
BoundedContinuousFunction.toLp_norm_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
[Fact (1 ≤ p)]
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
:
theorem
BoundedContinuousFunction.toLp_inj
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
{f g : BoundedContinuousFunction α E}
[μ.IsOpenPosMeasure]
:
theorem
BoundedContinuousFunction.toLp_injective
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
[μ.IsOpenPosMeasure]
:
Function.Injective ⇑(toLp p μ 𝕜)
noncomputable def
ContinuousMap.toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
(𝕜 : Type u_3)
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 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
Instances For
theorem
ContinuousMap.range_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
(p : ENNReal)
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
:
theorem
ContinuousMap.coeFn_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : C(α, E))
:
theorem
ContinuousMap.toLp_def
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : C(α, E))
:
@[simp]
theorem
ContinuousMap.toLp_comp_toContinuousMap
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : BoundedContinuousFunction α E)
:
@[simp]
theorem
ContinuousMap.coe_toLp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
(f : C(α, E))
:
theorem
ContinuousMap.toLp_injective
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
[μ.IsOpenPosMeasure]
:
Function.Injective ⇑(toLp p μ 𝕜)
theorem
ContinuousMap.toLp_inj
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
{f g : C(α, E)}
[μ.IsOpenPosMeasure]
:
theorem
ContinuousMap.hasSum_of_hasSum_Lp
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_3}
[Fact (1 ≤ p)]
[NormedRing 𝕜]
[Module 𝕜 E]
[IsBoundedSMul 𝕜 E]
{β : Type u_4}
[μ.IsOpenPosMeasure]
{g : β → C(α, E)}
{f : C(α, E)}
(hg : Summable g)
(hg2 : HasSum (⇑(toLp p μ 𝕜) ∘ g) ((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 α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
[Fact (1 ≤ p)]
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
:
theorem
ContinuousMap.toLp_norm_le
{α : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace α}
{p : ENNReal}
(μ : MeasureTheory.Measure α)
[TopologicalSpace α]
[BorelSpace α]
[NormedAddCommGroup E]
[SecondCountableTopologyEither α E]
[CompactSpace α]
[MeasureTheory.IsFiniteMeasure μ]
[Fact (1 ≤ p)]
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
:
Bound for the operator norm of ContinuousMap.toLp.