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) : eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f 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 : 𝕜} : eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * eLpNormEssSup f μ

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 : 𝕜} : eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ

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 : 𝕜) : MemLp (c • f) p μ

theorem MeasureTheory.MemLp.const_mul {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_3} [NormedRing 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) (c : 𝕜) : MemLp (fun (x : α) => c * f x) p μ

theorem MeasureTheory.MemLp.mul_const {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_3} [NormedRing 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) (c : 𝕜) : MemLp (fun (x : α) => f x * c) p μ

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) : eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f 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 : α → ε} : eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_const_smul_le' {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_3} [NormedRing 𝕜] {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [SMulWithZero 𝕜 ε] [ENormSMulClass 𝕜 ε] {c : 𝕜} {f : α → ε} [ContinuousConstSMul 𝕜 ε] : eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ

theorem MeasureTheory.MemLp.const_smul' {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_3} [NormedRing 𝕜] {ε : Type u_4} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [SMulWithZero 𝕜 ε] [ENormSMulClass 𝕜 ε] {f : α → ε} [ContinuousConstSMul 𝕜 ε] (hf : MemLp f p μ) (c : 𝕜) : MemLp (c • f) p μ

theorem MeasureTheory.MemLp.const_mul' {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_3} [NormedRing 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) (c : 𝕜) : MemLp (fun (x : α) => c * f x) p μ

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) : eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f 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) : eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup 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 α) : eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

theorem MeasureTheory.eLpNorm_nsmul {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : α → F) : eLpNorm (n • f) p μ = ↑n * eLpNorm f p μ

theorem MeasureTheory.eLpNorm'_const_mul_ennreal {α : Type u_1} {m : MeasurableSpace α} {q : ℝ} {μ : Measure α} {f : α → ENNReal} {c : ENNReal} (hq_pos : 0 < q) (hf : AEStronglyMeasurable f μ) : eLpNorm' (fun (x : α) => c * f x) q μ = c * eLpNorm' f q μ

theorem MeasureTheory.eLpNorm_const_mul_ennreal {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ENNReal} {c : ENNReal} (hf : AEStronglyMeasurable f μ) : eLpNorm (fun (x : α) => c * f x) p μ = c * eLpNorm f p μ

theorem MeasureTheory.eLpNorm_const_mul_ennreal_of_pos {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ENNReal} {c : ENNReal} (hp : 0 < p) : eLpNorm (fun (x : α) => c * f x) p μ = c * eLpNorm f p μ

theorem MeasureTheory.eLpNorm_const_smul_nnreal {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [MulActionWithZero NNReal ε] [ContinuousConstSMul NNReal ε] [ENormSMulClass NNReal ε] {f : α → ε} {c : NNReal} : eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ