chore(analysis/normed_space/basic): introduce norm_smul_le (#18650)

Currently `norm_smul_le x y` is just a special case of `(norm_smul x y).le`; but if in future we generalize `normed_space` to work over normed rings, it will continue to hold where `norm_smul` no longer does. This adjusts downstream proofs to use the weaker lemma too when the stronger one isn't needed, both so that we have less to fix if/when we make the suggested refactor, and because the new spelling is shorter.

This adds the corresponding `nnnorm` and `dist` and `nndist` lemmas too.

src/analysis/normed_space/basic.lean

@@ -42,28 +42,47 @@ end prio
 
 variables [normed_field α] [seminormed_add_comm_group β]
 
+-- note: while these are currently strictly weaker than the versions without `le`, they will cease
+-- to be if we eventually generalize `normed_space` from `normed_field α` to `normed_ring α`.
+section le
+
+lemma norm_smul_le [normed_space α β] (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖ :=
+normed_space.norm_smul_le _ _
+
+lemma nnnorm_smul_le [normed_space α β] (s : α) (x : β) : ‖s • x‖₊ ≤ ‖s‖₊ * ‖x‖₊ :=
+norm_smul_le s x
+
+lemma dist_smul_le [normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y :=
+by simpa only [dist_eq_norm, ←smul_sub] using norm_smul_le _ _
+
+lemma nndist_smul_le [normed_space α β] (s : α) (x y : β) :
+  nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y :=
+dist_smul_le s x y
+
+end le
+
 @[priority 100] -- see Note [lower instance priority]
 instance normed_space.has_bounded_smul [normed_space α β] : has_bounded_smul α β :=
 { dist_smul_pair' := λ x y₁ y₂,
-    by simpa [dist_eq_norm, smul_sub] using normed_space.norm_smul_le x (y₁ - y₂),
+    by simpa [dist_eq_norm, smul_sub] using norm_smul_le x (y₁ - y₂),
   dist_pair_smul' := λ x₁ x₂ y,
-    by simpa [dist_eq_norm, sub_smul] using normed_space.norm_smul_le (x₁ - x₂) y }
+    by simpa [dist_eq_norm, sub_smul] using norm_smul_le (x₁ - x₂) y }
 
 -- Shortcut instance, as otherwise this will be found by `normed_space.to_module` and be
 -- noncomputable.
 instance : module ℝ ℝ := by apply_instance
 
 instance normed_field.to_normed_space : normed_space α α :=
-{ norm_smul_le := λ a b, le_of_eq (norm_mul a b) }
+{ norm_smul_le := λ a b, norm_mul_le a b }
 
 lemma norm_smul [normed_space α β] (s : α) (x : β) : ‖s • x‖ = ‖s‖ * ‖x‖ :=
 begin
   by_cases h : s = 0,
   { simp [h] },
-  { refine le_antisymm (normed_space.norm_smul_le s x) _,
+  { refine le_antisymm (norm_smul_le s x) _,
     calc ‖s‖ * ‖x‖ = ‖s‖ * ‖s⁻¹ • s • x‖     : by rw [inv_smul_smul₀ h]
                ... ≤ ‖s‖ * (‖s⁻¹‖ * ‖s • x‖) :
-      mul_le_mul_of_nonneg_left (normed_space.norm_smul_le _ _) (norm_nonneg _)
+      mul_le_mul_of_nonneg_left (norm_smul_le _ _) (norm_nonneg _)
                ... = ‖s • x‖                 :
       by rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul] }
 end
@@ -108,12 +127,12 @@ this.eventually (gt_mem_nhds h)
 lemma filter.tendsto.zero_smul_is_bounded_under_le {f : ι → α} {g : ι → E} {l : filter ι}
   (hf : tendsto f l (𝓝 0)) (hg : is_bounded_under (≤) l (norm ∘ g)) :
   tendsto (λ x, f x • g x) l (𝓝 0) :=
-hf.op_zero_is_bounded_under_le hg (•) (λ x y, (norm_smul x y).le)
+hf.op_zero_is_bounded_under_le hg (•) norm_smul_le
 
 lemma filter.is_bounded_under.smul_tendsto_zero {f : ι → α} {g : ι → E} {l : filter ι}
   (hf : is_bounded_under (≤) l (norm ∘ f)) (hg : tendsto g l (𝓝 0)) :
   tendsto (λ x, f x • g x) l (𝓝 0) :=
-hg.op_zero_is_bounded_under_le hf (flip (•)) (λ x y, ((norm_smul y x).trans (mul_comm _ _)).le)
+hg.op_zero_is_bounded_under_le hf (flip (•)) (λ x y, (norm_smul_le y x).trans_eq (mul_comm _ _))
 
 theorem closure_ball [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
   closure (ball x r) = closed_ball x r :=
@@ -230,26 +249,26 @@ by simp [homeomorph_unit_ball]
 open normed_field
 
 instance : normed_space α (ulift E) :=
-{ norm_smul_le := λ s x, (normed_space.norm_smul_le s x.down : _),
+{ norm_smul_le := λ s x, (norm_smul_le s x.down : _),
   ..ulift.normed_add_comm_group,
   ..ulift.module' }
 
 /-- The product of two normed spaces is a normed space, with the sup norm. -/
 instance prod.normed_space : normed_space α (E × F) :=
-{ norm_smul_le := λ s x, le_of_eq $ by simp [prod.norm_def, norm_smul, mul_max_of_nonneg],
+{ norm_smul_le := λ s x, by simp [prod.norm_def, norm_smul_le, mul_max_of_nonneg],
   ..prod.normed_add_comm_group,
   ..prod.module }
 
 /-- The product of finitely many normed spaces is a normed space, with the sup norm. -/
 instance pi.normed_space {E : ι → Type*} [fintype ι] [∀i, seminormed_add_comm_group (E i)]
   [∀i, normed_space α (E i)] : normed_space α (Πi, E i) :=
-{ norm_smul_le := λ a f, le_of_eq $
-    show (↑(finset.sup finset.univ (λ (b : ι), ‖a • f b‖₊)) : ℝ) =
-      ‖a‖₊ * ↑(finset.sup finset.univ (λ (b : ι), ‖f b‖₊)),
-    by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
+{ norm_smul_le := λ a f, begin
+    simp_rw [←coe_nnnorm, ←nnreal.coe_mul, nnreal.coe_le_coe, pi.nnnorm_def, nnreal.mul_finset_sup],
+    exact finset.sup_mono_fun (λ _ _, norm_smul_le _ _),
+  end }
 
 instance mul_opposite.normed_space : normed_space α Eᵐᵒᵖ :=
-{ norm_smul_le := λ s x, (norm_smul s x.unop).le,
+{ norm_smul_le := λ s x, norm_smul_le s x.unop,
   ..mul_opposite.normed_add_comm_group,
   ..mul_opposite.module _ }
 
@@ -258,7 +277,7 @@ instance submodule.normed_space {𝕜 R : Type*} [has_smul 𝕜 R] [normed_field
   {E : Type*} [seminormed_add_comm_group E] [normed_space 𝕜 E] [module R E]
   [is_scalar_tower 𝕜 R E] (s : submodule R E) :
   normed_space 𝕜 s :=
-{ norm_smul_le := λc x, le_of_eq $ norm_smul c (x : E) }
+{ norm_smul_le := λc x, norm_smul_le c (x : E) }
 
 /-- If there is a scalar `c` with `‖c‖>1`, then any element with nonzero norm can be
 moved by scalar multiplication to any shell of width `‖c‖`. Also recap information on the norm of
@@ -304,7 +323,7 @@ See note [reducible non-instances] -/
 def normed_space.induced {F : Type*} (α β γ : Type*) [normed_field α] [add_comm_group β]
   [module α β] [seminormed_add_comm_group γ] [normed_space α γ] [linear_map_class F α β γ]
   (f : F) : @normed_space α β _ (seminormed_add_comm_group.induced β γ f) :=
-{ norm_smul_le := λ a b, by {unfold norm, exact (map_smul f a b).symm ▸ (norm_smul a (f b)).le } }
+{ norm_smul_le := λ a b, by {unfold norm, exact (map_smul f a b).symm ▸ norm_smul_le a (f b) } }
 
 section normed_add_comm_group
 
@@ -549,7 +568,7 @@ See note [reducible non-instances] -/
 def normed_algebra.induced {F : Type*} (α β γ : Type*) [normed_field α] [ring β]
   [algebra α β] [semi_normed_ring γ] [normed_algebra α γ] [non_unital_alg_hom_class F α β γ]
   (f : F) : @normed_algebra α β _ (semi_normed_ring.induced β γ f) :=
-{ norm_smul_le := λ a b, by {unfold norm, exact (map_smul f a b).symm ▸ (norm_smul a (f b)).le } }
+{ norm_smul_le := λ a b, by {unfold norm, exact (map_smul f a b).symm ▸ norm_smul_le a (f b) } }
 
 instance subalgebra.to_normed_algebra {𝕜 A : Type*} [semi_normed_ring A] [normed_field 𝕜]
   [normed_algebra 𝕜 A] (S : subalgebra 𝕜 A) : normed_algebra 𝕜 S :=
@@ -569,7 +588,7 @@ instance {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [I : normed_add_comm_group E
 /-- If `E` is a normed space over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
 `restrict_scalars.module` is additionally a `normed_space`. -/
 instance : normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E) :=
-{ norm_smul_le := λ c x, (normed_space.norm_smul_le (algebra_map 𝕜 𝕜' c) (_ : E)).trans_eq $
+{ norm_smul_le := λ c x, (norm_smul_le (algebra_map 𝕜 𝕜' c) (_ : E)).trans_eq $
     by rw norm_algebra_map',
   ..restrict_scalars.module 𝕜 𝕜' E }
 

src/analysis/normed_space/completion.lean

@@ -91,7 +91,7 @@ instance [semi_normed_comm_ring A] [normed_algebra 𝕜 A] [has_uniform_continuo
     { exact is_closed_le (continuous.comp (continuous_norm) (continuous_const_smul r))
       (continuous.comp (continuous_mul_left _) continuous_norm), },
     { intros x,
-      simp only [← coe_smul, norm_coe], exact normed_space.norm_smul_le r x }
+      simp only [← coe_smul, norm_coe], exact norm_smul_le r x }
   end,
   ..completion.algebra A 𝕜}
 

src/analysis/normed_space/operator_norm.lean

@@ -976,7 +976,7 @@ variables (𝕜) (𝕜' : Type*) [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'
 /-- Scalar multiplication as a continuous bilinear map. -/
 def lsmul : 𝕜' →L[𝕜] E →L[𝕜] E :=
 ((algebra.lsmul 𝕜 E).to_linear_map : 𝕜' →ₗ[𝕜] E →ₗ[𝕜] E).mk_continuous₂ 1 $
-  λ c x, by simpa only [one_mul] using (norm_smul c x).le
+  λ c x, by simpa only [one_mul] using norm_smul_le c x
 
 @[simp] lemma lsmul_apply (c : 𝕜') (x : E) : lsmul 𝕜 𝕜' c x = c • x := rfl
 
@@ -994,7 +994,7 @@ end
 variables {𝕜}
 
 lemma op_norm_lsmul_apply_le (x : 𝕜') : ‖(lsmul 𝕜 𝕜' x : E →L[𝕜] E)‖ ≤ ‖x‖ :=
-continuous_linear_map.op_norm_le_bound _ (norm_nonneg x) $ λ y, (norm_smul x y).le
+continuous_linear_map.op_norm_le_bound _ (norm_nonneg x) $ λ y, norm_smul_le x y
 
 /-- The norm of `lsmul` is at most 1 in any semi-normed group. -/
 lemma op_norm_lsmul_le : ‖(lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] E →L[𝕜] E)‖ ≤ 1 :=

src/analysis/normed_space/star/multiplier.lean

@@ -383,7 +383,7 @@ lemma norm_def' (a : 𝓜(𝕜, A)) : ‖a‖ = ‖a.to_prod_mul_opposite_hom‖
 lemma nnnorm_def' (a : 𝓜(𝕜, A)) : ‖a‖₊ = ‖a.to_prod_mul_opposite_hom‖₊ := rfl
 
 instance : normed_space 𝕜 𝓜(𝕜, A) :=
-{ norm_smul_le := λ k a, (norm_smul k a.to_prod_mul_opposite).le,
+{ norm_smul_le := λ k a, norm_smul_le k a.to_prod_mul_opposite,
   .. double_centralizer.module }
 
 instance : normed_algebra 𝕜 𝓜(𝕜, A) :=

src/analysis/quaternion.lean

@@ -77,7 +77,7 @@ noncomputable instance : normed_division_ring ℍ :=
                            exact real.sqrt_mul norm_sq_nonneg _ } }
 
 instance : normed_algebra ℝ ℍ :=
-{ norm_smul_le := λ a x, (norm_smul a x).le,
+{ norm_smul_le := norm_smul_le,
   to_algebra := (quaternion.algebra : algebra ℝ ℍ) }
 
 instance : cstar_ring ℍ :=

src/measure_theory/function/strongly_measurable/basic.lean

@@ -234,7 +234,7 @@ lemma norm_approx_bounded_le {β} {f : α → β} [seminormed_add_comm_group β]
   ‖hf.approx_bounded c n x‖ ≤ c :=
 begin
   simp only [strongly_measurable.approx_bounded, simple_func.coe_map, function.comp_app],
-  refine (norm_smul _ _).le.trans _,
+  refine (norm_smul_le _ _).trans _,
   by_cases h0 : ‖hf.approx n x‖ = 0,
   { simp only [h0, div_zero, min_eq_right, zero_le_one, norm_zero, mul_zero],
     exact hc, },

src/topology/continuous_function/bounded.lean

@@ -1165,7 +1165,7 @@ functions from `α` to `𝕜`. -/
 instance has_smul' : has_smul (α →ᵇ 𝕜) (α →ᵇ β) :=
 ⟨λ (f : α →ᵇ 𝕜) (g : α →ᵇ β), of_normed_add_comm_group (λ x, (f x) • (g x))
 (f.continuous.smul g.continuous) (‖f‖ * ‖g‖) (λ x, calc
-  ‖f x • g x‖ ≤ ‖f x‖ * ‖g x‖ : normed_space.norm_smul_le _ _
+  ‖f x • g x‖ ≤ ‖f x‖ * ‖g x‖ : norm_smul_le _ _
   ... ≤ ‖f‖ * ‖g‖ : mul_le_mul (f.norm_coe_le_norm _) (g.norm_coe_le_norm _) (norm_nonneg _)
     (norm_nonneg _)) ⟩
 

src/topology/continuous_function/compact.lean

@@ -227,7 +227,7 @@ section
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E]
 
 instance : normed_space 𝕜 C(α,E) :=
-{ norm_smul_le := λ c f, le_of_eq (norm_smul c (mk_of_compact f)) }
+{ norm_smul_le := λ c f, (norm_smul_le c (mk_of_compact f) : _) }
 
 section
 variables (α 𝕜 E)

src/topology/continuous_function/zero_at_infty.lean

@@ -411,7 +411,7 @@ normed_add_comm_group.induced C₀(α, β) (α →ᵇ β) (⟨to_bcf, rfl, λ x
 lemma norm_to_bcf_eq_norm {f : C₀(α, β)} : ‖f.to_bcf‖ = ‖f‖ := rfl
 
 instance : normed_space 𝕜 C₀(α, β) :=
-{ norm_smul_le := λ k f, (norm_smul k f.to_bcf).le }
+{ norm_smul_le := λ k f, norm_smul_le k f.to_bcf }
 
 end normed_space