Scalar multiplication on ℒp space #
Bounded actions by normed rings #
In this section we show inequalities on the norm.
theorem
MeasureTheory.eLpNorm'_const_smul_le
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{𝕜 : Type u_3}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
{c : 𝕜}
(hq : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul_le
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{𝕜 : Type u_3}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
{c : 𝕜}
:
theorem
MeasureTheory.eLpNorm_const_smul_le
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{𝕜 : Type u_3}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
{c : 𝕜}
:
theorem
MeasureTheory.MemLp.const_smul
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
{f : α → F}
{𝕜 : Type u_3}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 F]
[IsBoundedSMul 𝕜 F]
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.MemLp.const_mul
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_3}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.MemLp.mul_const
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_3}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.eLpNorm'_const_smul_le'
{α : Type u_1}
{m : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
{𝕜 : Type u_3}
[NormedRing 𝕜]
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{c : 𝕜}
{f : α → ε}
(hq : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul_le'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_3}
[NormedRing 𝕜]
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{c : 𝕜}
{f : α → ε}
:
theorem
MeasureTheory.eLpNorm_const_smul_le'
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_3}
[NormedRing 𝕜]
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{c : 𝕜}
{f : α → ε}
:
theorem
MeasureTheory.MemLp.const_smul'
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_3}
[NormedRing 𝕜]
{ε : Type u_4}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
[SMul 𝕜 ε]
[ENormSMulClass 𝕜 ε]
{f : α → ε}
[ContinuousConstSMul 𝕜 ε]
(hf : MemLp f p μ)
(c : 𝕜)
:
theorem
MeasureTheory.MemLp.const_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{𝕜 : Type u_3}
[NormedRing 𝕜]
{f : α → 𝕜}
(hf : MemLp f p μ)
(c : 𝕜)
:
Bounded actions by normed division rings #
The inequalities in the previous section are now tight.
TODO: do these results hold for any NormedRing assuming NormSMulClass?
theorem
MeasureTheory.eLpNorm'_const_smul
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{q : ℝ}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_3}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[NormSMulClass 𝕜 F]
{f : α → F}
(c : 𝕜)
(hq_pos : 0 < q)
:
theorem
MeasureTheory.eLpNormEssSup_const_smul
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
{𝕜 : Type u_3}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[NormSMulClass 𝕜 F]
(c : 𝕜)
(f : α → F)
:
theorem
MeasureTheory.eLpNorm_const_smul
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup F]
{𝕜 : Type u_3}
[NormedDivisionRing 𝕜]
[Module 𝕜 F]
[NormSMulClass 𝕜 F]
(c : 𝕜)
(f : α → F)
(p : ENNReal)
(μ : Measure α)
:
theorem
MeasureTheory.eLpNorm_nsmul
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(n : ℕ)
(f : α → F)
: