feat: port Analysis.Normed.MulAction + #19053 (#4288)

Both the new file and the other fixes are done in the same PR, since according to the description of leanprover-community/mathlib3#19053 "this should be very easy to forward-port".

Author: Parcly-Taxel

Mathlib.lean

@@ -455,6 +455,7 @@ import Mathlib.Analysis.Normed.Group.InfiniteSum
 import Mathlib.Analysis.Normed.Group.Pointwise
 import Mathlib.Analysis.Normed.Group.Quotient
 import Mathlib.Analysis.Normed.Group.Seminorm
+import Mathlib.Analysis.Normed.MulAction
 import Mathlib.Analysis.Normed.Order.Basic
 import Mathlib.Analysis.Normed.Order.Lattice
 import Mathlib.Analysis.Normed.Order.UpperLower

Mathlib/Analysis/Normed/MulAction.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module analysis.normed.mul_action
+! leanprover-community/mathlib commit ba5ff5ad5d120fb0ef094ad2994967e9bfaf5112
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.MetricSpace.Algebra
+import Mathlib.Analysis.Normed.Field.Basic
+
+/-!
+# Lemmas for `BoundedSMul` over normed additive groups
+
+Lemmas which hold only in `NormedSpace α β` are provided in another file.
+
+Notably we prove that `NonUnitalSeminormedRing`s have bounded actions by left- and right-
+multiplication. This allows downstream files to write general results about `BoundedSMul`, and then
+deduce `const_mul` and `mul_const` results as an immediate corollary.
+-/
+
+
+variable {α β : Type _}
+
+section SeminormedAddGroup
+
+variable [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β]
+
+variable [BoundedSMul α β]
+
+theorem norm_smul_le (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖ := by
+  simpa [smul_zero] using dist_smul_pair r 0 x
+#align norm_smul_le norm_smul_le
+
+theorem nnnorm_smul_le (r : α) (x : β) : ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊ :=
+  norm_smul_le _ _
+#align nnnorm_smul_le nnnorm_smul_le
+
+theorem dist_smul_le (s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y := by
+  simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y
+#align dist_smul_le dist_smul_le
+
+theorem nndist_smul_le (s : α) (x y : β) : nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y :=
+  dist_smul_le s x y
+#align nndist_smul_le nndist_smul_le
+
+theorem lipschitzWith_smul (s : α) : LipschitzWith ‖s‖₊ ((· • ·) s : β → β) :=
+  lipschitzWith_iff_dist_le_mul.2 <| dist_smul_le _
+#align lipschitz_with_smul lipschitzWith_smul
+
+end SeminormedAddGroup
+
+/-- Left multiplication is bounded. -/
+instance NonUnitalSeminormedRing.to_boundedSMul [NonUnitalSeminormedRing α] : BoundedSMul α α where
+  dist_smul_pair' x y₁ y₂ := by simpa [mul_sub, dist_eq_norm] using norm_mul_le x (y₁ - y₂)
+  dist_pair_smul' x₁ x₂ y := by simpa [sub_mul, dist_eq_norm] using norm_mul_le (x₁ - x₂) y
+#align non_unital_semi_normed_ring.to_has_bounded_smul NonUnitalSeminormedRing.to_boundedSMul
+
+/-- Right multiplication is bounded. -/
+instance NonUnitalSeminormedRing.to_has_bounded_op_smul [NonUnitalSeminormedRing α] :
+    BoundedSMul αᵐᵒᵖ α where
+  dist_smul_pair' x y₁ y₂ := by
+    simpa [sub_mul, dist_eq_norm, mul_comm] using norm_mul_le (y₁ - y₂) x.unop
+  dist_pair_smul' x₁ x₂ y := by
+    simpa [mul_sub, dist_eq_norm, mul_comm] using norm_mul_le y (x₁ - x₂).unop
+#align non_unital_semi_normed_ring.to_has_bounded_op_smul NonUnitalSeminormedRing.to_has_bounded_op_smul
+
+section SeminormedRing
+
+variable [SeminormedRing α] [SeminormedAddCommGroup β] [Module α β]
+
+theorem BoundedSMul.of_norm_smul_le (h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) :
+    BoundedSMul α β :=
+  { dist_smul_pair' := fun a b₁ b₂ => by simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)
+    dist_pair_smul' := fun a₁ a₂ b => by simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b }
+#align has_bounded_smul.of_norm_smul_le BoundedSMul.of_norm_smul_le
+
+end SeminormedRing
+
+section NormedDivisionRing
+
+variable [NormedDivisionRing α] [SeminormedAddGroup β]
+
+variable [MulActionWithZero α β] [BoundedSMul α β]
+
+theorem norm_smul (r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖ := by
+  by_cases h : r = 0
+  · simp [h, zero_smul α x]
+  · refine' le_antisymm (norm_smul_le r x) _
+    calc
+      ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
+      _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := (mul_le_mul_of_nonneg_left (norm_smul_le _ _) (norm_nonneg _))
+      _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul]
+#align norm_smul norm_smul
+
+theorem nnnorm_smul (r : α) (x : β) : ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊ :=
+  NNReal.eq <| norm_smul r x
+#align nnnorm_smul nnnorm_smul
+
+end NormedDivisionRing
+
+section NormedDivisionRingModule
+
+variable [NormedDivisionRing α] [SeminormedAddCommGroup β]
+
+variable [Module α β] [BoundedSMul α β]
+
+theorem dist_smul₀ (s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y := by
+  simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]
+#align dist_smul₀ dist_smul₀
+
+theorem nndist_smul₀ (s : α) (x y : β) : nndist (s • x) (s • y) = ‖s‖₊ * nndist x y :=
+  NNReal.eq <| dist_smul₀ s x y
+#align nndist_smul₀ nndist_smul₀
+
+end NormedDivisionRingModule

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -4,13 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 
 ! This file was ported from Lean 3 source module analysis.normed_space.basic
-! leanprover-community/mathlib commit f9dd3204df14a0749cd456fac1e6849dfe7d2b88
+! leanprover-community/mathlib commit ba5ff5ad5d120fb0ef094ad2994967e9bfaf5112
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Algebra.Pi
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Analysis.Normed.Field.Basic
+import Mathlib.Analysis.Normed.MulAction
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Topology.Algebra.Module.Basic
 
@@ -53,47 +54,18 @@ end Prio
 
 variable [NormedField α] [SeminormedAddCommGroup β]
 
--- note: while these are currently strictly weaker than the versions without `le`, they will cease
--- to be if we eventually generalize `NormedSpace` from `NormedField α` to `NormedRing α`.
-section LE
-
-theorem norm_smul_le [NormedSpace α β] (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖ :=
-  NormedSpace.norm_smul_le _ _
-#align norm_smul_le norm_smul_le
-
-theorem nnnorm_smul_le [NormedSpace α β] (s : α) (x : β) : ‖s • x‖₊ ≤ ‖s‖₊ * ‖x‖₊ :=
-  norm_smul_le s x
-#align nnnorm_smul_le nnnorm_smul_le
-
-theorem dist_smul_le [NormedSpace α β] (s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y :=
-  by simpa only [dist_eq_norm, ← smul_sub] using norm_smul_le _ _
-#align dist_smul_le dist_smul_le
-
-theorem nndist_smul_le [NormedSpace α β] (s : α) (x y : β) :
-    nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y :=
-  dist_smul_le s x y
-#align nndist_smul_le nndist_smul_le
-
-end LE
-
 -- see Note [lower instance priority]
-instance (priority := 100) NormedSpace.boundedSMul [NormedSpace α β] : BoundedSMul α β where
-  dist_smul_pair' 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 norm_smul_le (x₁ - x₂) y
+instance (priority := 100) NormedSpace.boundedSMul [NormedSpace α β] : BoundedSMul α β :=
+  BoundedSMul.of_norm_smul_le NormedSpace.norm_smul_le
 #align normed_space.has_bounded_smul NormedSpace.boundedSMul
 
 instance NormedField.toNormedSpace : NormedSpace α α where norm_smul_le a b := norm_mul_le a b
 #align normed_field.to_normed_space NormedField.toNormedSpace
 
-theorem norm_smul [NormedSpace α β] (s : α) (x : β) : ‖s • x‖ = ‖s‖ * ‖x‖ := by
-  by_cases h : s = 0
-  · simp [h]
-  · 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 (norm_smul_le _ _) (norm_nonneg _))
-      _ = ‖s • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul]
-#align norm_smul norm_smul
+-- shortcut instance
+instance NormedField.to_boundedSMul : BoundedSMul α α :=
+  NormedSpace.boundedSMul
+#align normed_field.to_has_bounded_smul NormedField.to_boundedSMul
 
 theorem norm_zsmul (α) [NormedField α] [NormedSpace α β] (n : ℤ) (x : β) :
     ‖n • x‖ = ‖(n : α)‖ * ‖x‖ := by rw [← norm_smul, ← Int.smul_one_eq_coe, smul_assoc, one_smul]
@@ -109,23 +81,6 @@ theorem inv_norm_smul_mem_closed_unit_ball [NormedSpace ℝ β] (x : β) :
     div_self_le_one]
 #align inv_norm_smul_mem_closed_unit_ball inv_norm_smul_mem_closed_unit_ball
 
-theorem dist_smul₀ [NormedSpace α β] (s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y := by
-  simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
-#align dist_smul₀ dist_smul₀
-
-theorem nnnorm_smul [NormedSpace α β] (s : α) (x : β) : ‖s • x‖₊ = ‖s‖₊ * ‖x‖₊ :=
-  NNReal.eq <| norm_smul s x
-#align nnnorm_smul nnnorm_smul
-
-theorem nndist_smul₀ [NormedSpace α β] (s : α) (x y : β) :
-    nndist (s • x) (s • y) = ‖s‖₊ * nndist x y :=
-  NNReal.eq <| dist_smul₀ s x y
-#align nndist_smul₀ nndist_smul₀
-
-theorem lipschitzWith_smul [NormedSpace α β] (s : α) : LipschitzWith ‖s‖₊ ((· • ·) s : β → β) :=
-  lipschitzWith_iff_dist_le_mul.2 fun x y => by rw [dist_smul₀, coe_nnnorm]
-#align lipschitz_with_smul lipschitzWith_smul
-
 theorem norm_smul_of_nonneg [NormedSpace ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) : ‖t • x‖ = t * ‖x‖ := by
   rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
 #align norm_smul_of_nonneg norm_smul_of_nonneg
@@ -291,7 +246,7 @@ instance Pi.normedSpace {E : ι → Type _} [Fintype ι] [∀ i, SeminormedAddCo
   norm_smul_le a f := by
     simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def,
       NNReal.mul_finset_sup]
-    exact Finset.sup_mono_fun fun _ _ => norm_smul_le _ _
+    exact Finset.sup_mono_fun fun _ _ => norm_smul_le a _
 #align pi.normed_space Pi.normedSpace
 
 instance MulOpposite.normedSpace : NormedSpace α Eᵐᵒᵖ :=

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 
 ! This file was ported from Lean 3 source module analysis.special_functions.exp
-! leanprover-community/mathlib commit 2c1d8ca2812b64f88992a5294ea3dba144755cd1
+! leanprover-community/mathlib commit ba5ff5ad5d120fb0ef094ad2994967e9bfaf5112
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -44,7 +44,6 @@ theorem exp_bound_sq (x z : ℂ) (hz : ‖z‖ ≤ 1) :
     _ = ‖exp x‖ * ‖exp z - 1 - z‖ := (norm_mul _ _)
     _ ≤ ‖exp x‖ * ‖z‖ ^ 2 :=
       mul_le_mul_of_nonneg_left (abs_exp_sub_one_sub_id_le hz) (norm_nonneg _)
-
 #align complex.exp_bound_sq Complex.exp_bound_sq
 
 theorem locally_lipschitz_exp {r : ℝ} (hr_nonneg : 0 ≤ r) (hr_le : r ≤ 1) (x y : ℂ)
@@ -64,7 +63,6 @@ theorem locally_lipschitz_exp {r : ℝ} (hr_nonneg : 0 ≤ r) (hr_le : r ≤ 1)
     _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) :=
       (add_le_add_left (mul_le_mul le_rfl hyx_sq_le (sq_nonneg _) (norm_nonneg _)) _)
     _ = (1 + r) * ‖exp x‖ * ‖y - x‖ := by ring
-
 #align complex.locally_lipschitz_exp Complex.locally_lipschitz_exp
 
 -- Porting note: proof by term mode `locally_lipschitz_exp zero_le_one le_rfl x`
@@ -236,7 +234,6 @@ theorem tendsto_exp_div_pow_atTop (n : ℕ) : Tendsto (fun x => exp x / x ^ n) a
       (div_le_div_of_le (mul_pos (exp_pos _) hC₀).le
         (exp_le_exp.2 <| (Nat.ceil_lt_add_one hx₀.le).le))
     _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
-
 #align real.tendsto_exp_div_pow_at_top Real.tendsto_exp_div_pow_atTop
 
 /-- The function `x^n * exp(-x)` tends to `0` at `+∞`, for any natural number `n`. -/