feat(analysis/normed_space/operator_norm): norm of lsmul (#13538)

* From the sphere eversion project
* Required for convolutions

src/analysis/normed_space/operator_norm.lean

@@ -840,6 +840,7 @@ section smul_linear
 
 variables (𝕜) (𝕜' : Type*) [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
   [normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E]
+  [normed_space 𝕜' M₁] [is_scalar_tower 𝕜 𝕜' M₁]
 
 /-- Scalar multiplication as a continuous bilinear map. -/
 def lsmul : 𝕜' →L[𝕜] E →L[𝕜] E :=
@@ -859,6 +860,31 @@ begin
     exact (mul_le_mul_right (by simp)).mp h, },
 end
 
+variables {𝕜}
+
+/-- The norm of `lsmul` is at most 1 in any semi-normed group. -/
+lemma op_norm_lsmul_le : ∥(lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] E →L[𝕜] E)∥ ≤ 1 :=
+begin
+  refine continuous_linear_map.op_norm_le_bound _ zero_le_one (λ x, _),
+  simp_rw [one_mul],
+  refine continuous_linear_map.op_norm_le_bound _ (norm_nonneg x) (λ y, _),
+  simp_rw [lsmul_apply, norm_smul],
+end
+
+/-- The norm of `lsmul` equals 1 in any nontrivial normed group. -/
+@[simp] lemma op_norm_lsmul [nontrivial M₁] : ∥(lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] M₁ →L[𝕜] M₁)∥ = 1 :=
+begin
+  refine continuous_linear_map.op_norm_eq_of_bounds zero_le_one (λ x, _) (λ N hN h, _),
+  { simp_rw [one_mul],
+    refine continuous_linear_map.op_norm_le_bound _ (norm_nonneg x) (λ y, _),
+    simp_rw [lsmul_apply, norm_smul] },
+  obtain ⟨y, hy⟩ := exists_ne (0 : M₁),
+  have := le_of_op_norm_le _ (h 1) y,
+  simp_rw [lsmul_apply, one_smul, norm_one, mul_one] at this,
+  refine le_of_mul_le_mul_right _ (norm_pos_iff.mpr hy),
+  simp_rw [one_mul, this]
+end
+
 end smul_linear
 
 section restrict_scalars