feat: linear map from L^p (mu) to L^p (nu) when nu is bounded by a multiple of mu

Mathlib/Analysis/Normed/Group/Continuity.lean

@@ -313,6 +313,11 @@ theorem tendsto_iff_norm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E}
     Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0) := by
   simp only [← dist_eq_norm_div, ← tendsto_iff_dist_tendsto_zero]
 
+@[to_additive]
+theorem tendsto_iff_enorm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E} :
+    Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖ₑ) a (𝓝 0) := by
+  simp only [← edist_eq_enorm_div, ← tendsto_iff_edist_tendsto_0]
+
 @[to_additive]
 theorem SeminormedCommGroup.mem_closure_iff {s : Set E} :
     a ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε := by

Mathlib/Analysis/Normed/Operator/Bilinear.lean

@@ -165,6 +165,14 @@ theorem flip_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : f.flip.flip = f
 theorem opNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ = ‖f‖ :=
   le_antisymm (by simpa only [flip_flip] using le_norm_flip f.flip) (le_norm_flip f)
 
+@[simp]
+theorem opNNNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖₊ = ‖f‖₊ := by
+  simp [← NNReal.coe_inj]
+
+@[simp]
+theorem opENorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ₑ = ‖f‖ₑ := by
+  simp [enorm_eq_nnnorm]
+
 @[simp]
 lemma flip_zero : flip (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) = 0 := rfl
 

Mathlib/Analysis/Normed/Operator/Mul.lean

@@ -221,6 +221,10 @@ theorem opNNNorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖
   rw [← NNReal.coe_le_coe]
   simpa using opNorm_lsmul_le
 
+theorem opENorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ₑ ≤ 1 := by
+  rw [enorm_eq_nnnorm]
+  simpa using opNNNorm_lsmul_le
+
 end SMulLinear
 
 end ContinuousLinearMap
@@ -247,6 +251,10 @@ theorem opNorm_mul : ‖mul 𝕜 R‖ = 1 :=
 theorem opNNNorm_mul : ‖mul 𝕜 R‖₊ = 1 :=
   Subtype.ext <| opNorm_mul 𝕜 R
 
+@[simp]
+theorem opENorm_mul : ‖mul 𝕜 R‖ₑ = 1 := by
+  simp [enorm_eq_nnnorm]
+
 end
 
 /-- The norm of `lsmul` equals 1 in any nontrivial normed group.
@@ -268,6 +276,11 @@ theorem opNNNorm_lsmul [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E
   rw [← NNReal.coe_inj]
   simp
 
+@[simp]
+theorem opENorm_lsmul [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E] [NormSMulClass R E]
+    [IsScalarTower 𝕜 R E] [Nontrivial E] : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ₑ = 1 := by
+  simp [enorm_eq_nnnorm]
+
 /-- The norm of `lsmul x` equals `‖x‖` in any nontrivial normed group.
 
 This is `ContinuousLinearMap.opNorm_lsmul_apply_le` as an equality. -/
@@ -288,6 +301,12 @@ theorem opNNNorm_lsmul_apply [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Modu
   rw [← NNReal.coe_inj]
   simp
 
+@[simp]
+theorem opENorm_lsmul_apply [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E]
+    [NormSMulClass R E] [IsScalarTower 𝕜 R E] [Nontrivial E] {a : R} :
+    ‖(lsmul 𝕜 R a : E →L[𝕜] E)‖ₑ = ‖a‖ₑ := by
+  simp [enorm_eq_nnnorm]
+
 end ContinuousLinearMap
 
 end Normed

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -661,6 +661,12 @@ theorem eLpNorm_smul_measure_of_ne_zero {c : ℝ≥0∞} (hc : c ≠ 0) (f : α
   · simp [*]
   exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c
 
+theorem eLpNorm_smul_measure_le (c : ℝ≥0∞) (f : α → ε) (p : ℝ≥0∞)
+    (μ : Measure α) : eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • eLpNorm f p μ := by
+  rcases eq_or_ne c 0 with rfl | hc
+  · simp
+  · exact (eLpNorm_smul_measure_of_ne_zero hc f p μ ).le
+
 /-- See `eLpNorm_smul_measure_of_ne_zero` for a version with scalar multiplication by `ℝ≥0∞`. -/
 lemma eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0} (hc : c ≠ 0) (f : α → ε) (p : ℝ≥0∞)
     (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ :=
@@ -684,15 +690,16 @@ theorem eLpNorm_one_smul_measure {f : α → ε} (c : ℝ≥0∞) :
     eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ := by
   rw [eLpNorm_smul_measure_of_ne_top] <;> simp
 
+theorem eLpNorm_le_of_measure_le_smul {c : ℝ≥0∞}
+    {μ μ' : Measure α} (h : μ' ≤ c • μ) {f : α → ε} {p : ℝ≥0∞} :
+    eLpNorm f p μ' ≤ c ^ (1 / p).toReal • eLpNorm f p μ := by
+  grw [eLpNorm_mono_measure f h, eLpNorm_smul_measure_le]
+
 theorem MemLp.of_measure_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞)
     (hμ'_le : μ' ≤ c • μ) {f : α → ε} (hf : MemLp f p μ) : MemLp f p μ' := by
   refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩
-  refine (eLpNorm_mono_measure f hμ'_le).trans_lt ?_
-  by_cases hc0 : c = 0
-  · simp [hc0]
-  rw [eLpNorm_smul_measure_of_ne_zero hc0, smul_eq_mul]
-  refine ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2
-  simp [hc, hc0]
+  grw [eLpNorm_le_of_measure_le_smul hμ'_le]
+  exact ENNReal.mul_lt_top (Ne.lt_top (by simp [hc])) hf.2
 
 theorem MemLp.smul_measure {f : α → ε} {c : ℝ≥0∞} (hf : MemLp f p μ) (hc : c ≠ ∞) :
     MemLp f p (c • μ) :=

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

@@ -232,7 +232,6 @@ theorem nnnorm_def (f : Lp E p μ) : ‖f‖₊ = ENNReal.toNNReal (eLpNorm f p
 protected theorem coe_nnnorm (f : Lp E p μ) : (‖f‖₊ : ℝ) = ‖f‖ :=
   rfl
 
-@[simp]
 theorem enorm_def (f : Lp E p μ) : ‖f‖ₑ = eLpNorm f p μ :=
   ENNReal.coe_toNNReal <| Lp.eLpNorm_ne_top f
 
@@ -245,6 +244,7 @@ theorem nnnorm_toLp (f : α → E) (hf : MemLp f p μ) :
     ‖hf.toLp f‖₊ = ENNReal.toNNReal (eLpNorm f p μ) :=
   NNReal.eq <| norm_toLp f hf
 
+@[simp]
 lemma enorm_toLp {f : α → E} (hf : MemLp f p μ) : ‖hf.toLp f‖ₑ = eLpNorm f p μ := by
   simp_rw [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne]
 
@@ -869,6 +869,66 @@ end ContinuousLinearMap
 
 namespace MeasureTheory.Lp
 
+section LpToLpOfMeasureLeSMul
+
+variable [NormedSpace ℝ E] {ν : Measure α} {c : ℝ≥0∞}
+
+/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a multiple of `ν`.
+This is the linear map version. Use instead the continuous linear map
+version `LpToLpOfMeasureLeSMul` -/
+noncomputable def LpToLpOfMeasureLeSMulₗ (hc : c ≠ ∞) (h : μ ≤ c • ν) :
+    Lp E p ν →ₗ[ℝ] Lp E p μ where
+  toFun f := ((Lp.memLp f).of_measure_le_smul hc h).toLp f
+  map_add' f g := by
+    ext
+    grw [MemLp.coeFn_toLp, Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp]
+    have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h
+    apply Measure.AbsolutelyContinuous.ae_eq this
+    grw [Lp.coeFn_add]
+  map_smul' c f := by
+    ext
+    grw [MemLp.coeFn_toLp, Lp.coeFn_smul, MemLp.coeFn_toLp]
+    have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h
+    apply Measure.AbsolutelyContinuous.ae_eq this
+    grw [Lp.coeFn_smul]
+    rfl
+
+lemma coeFn_LpToLpOfMeasureLeSMulₗ (hc : c ≠ ∞) (h : μ ≤ c • ν) (f : Lp E p ν) :
+    LpToLpOfMeasureLeSMulₗ hc h f =ᵐ[μ] f := by
+  simp [LpToLpOfMeasureLeSMulₗ, MemLp.coeFn_toLp]
+
+lemma enorm_LpToLpOfMeasureLeSMulₗ_apply_le
+    (hc : c ≠ ∞) (h : μ ≤ c • ν) [Fact (1 ≤ p)] {f : Lp E p ν} :
+    ‖LpToLpOfMeasureLeSMulₗ hc h f‖ₑ ≤ c ^ (1 / p).toReal * ‖f‖ₑ := by
+  simp only [Lp.enorm_def]
+  grw [eLpNorm_congr_ae (coeFn_LpToLpOfMeasureLeSMulₗ hc h f)]
+  exact eLpNorm_le_of_measure_le_smul h
+
+lemma norm_LpToLpOfMeasureLeSMulₗ_apply_le
+    (hc : c ≠ ∞) (h : μ ≤ c • ν) [Fact (1 ≤ p)] {f : Lp E p ν} :
+    ‖LpToLpOfMeasureLeSMulₗ hc h f‖ ≤ c.toReal ^ (1 / p).toReal * ‖f‖ := by
+  simp only [← toReal_enorm]
+  rw [ENNReal.toReal_rpow, ← ENNReal.toReal_mul]
+  apply (ENNReal.toReal_le_toReal (by simp only [ne_eq, enorm_ne_top, not_false_eq_true]) _).2
+    (enorm_LpToLpOfMeasureLeSMulₗ_apply_le hc h)
+  simp [ENNReal.mul_eq_top, hc]
+
+/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a multiple of `ν`. -/
+noncomputable def LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) :
+    Lp E p ν →L[ℝ] Lp E p μ :=
+  LinearMap.mkContinuous (LpToLpOfMeasureLeSMulₗ hc h) (c.toReal ^ (1 / p).toReal)
+    (fun _ ↦ norm_LpToLpOfMeasureLeSMulₗ_apply_le hc h)
+
+lemma coeFn_LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) (f : Lp E p ν) :
+    LpToLpOfMeasureLeSMul hc h f =ᵐ[μ] f :=
+  coeFn_LpToLpOfMeasureLeSMulₗ hc h f
+
+lemma norm_LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) :
+    ‖(LpToLpOfMeasureLeSMul hc h : Lp E p ν →L[ℝ] Lp E p μ)‖ ≤ c.toReal ^ (1 / p).toReal :=
+  LinearMap.mkContinuous_norm_le _ (Real.rpow_nonneg (by simp) _) _
+
+end LpToLpOfMeasureLeSMul
+
 section PosPart
 
 theorem lipschitzWith_pos_part : LipschitzWith 1 fun x : ℝ => max x 0 :=