feat(Analysis/Normed/Group/Uniform): AntilipschitzWith is equivalent to being bounded below (leanprover-community#35247)

This PR proves that an operator is Antilipschitz if and only if it is bounded below.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -154,6 +154,15 @@ theorem AntilipschitzWith.le_mul_norm' {f : E → F} {K : ℝ≥0} (h : Antilips
     (hf : f 1 = 1) (x) : ‖x‖ ≤ K * ‖f x‖ := by
   simpa only [dist_one_right, hf] using h.le_mul_dist x 1
 
+@[to_additive antilipschitzWith_iff_exists_mul_le_mul]
+theorem antilipschitzWith_iff_exists_mul_le_mul' [MonoidHomClass 𝓕 E F] (f : 𝓕) :
+    (∃ K, AntilipschitzWith K f) ↔ ∃ c > 0, ∀ x, c * ‖x‖ ≤ ‖f x‖ := by
+  refine ⟨fun ⟨K, hK⟩ ↦ ⟨(K + 1)⁻¹, by positivity, fun x ↦ ?_⟩, fun ⟨c, hc0, hc⟩ ↦
+    ⟨⟨c⁻¹, by positivity⟩, MonoidHomClass.antilipschitz_of_bound f fun x ↦ ?_⟩⟩
+  · grw [hK.le_mul_norm' (map_one f), ← mul_assoc]
+    exact mul_le_of_le_one_left (norm_nonneg' (f x)) (by simp [field])
+  · grw [← hc, NNReal.coe_mk, inv_mul_cancel_left₀ hc0.ne']
+
 @[to_additive AntilipschitzWith.le_mul_nnnorm]
 theorem AntilipschitzWith.le_mul_nnnorm' {f : E → F} {K : ℝ≥0} (h : AntilipschitzWith K f)
     (hf : f 1 = 1) (x) : ‖x‖₊ ≤ K * ‖f x‖₊ :=

Mathlib/Topology/MetricSpace/Antilipschitz.lean

@@ -32,7 +32,8 @@ open scoped NNReal ENNReal Uniformity
 variable {α β γ : Type*}
 
 /-- We say that `f : α → β` is `AntilipschitzWith K` if for any two points `x`, `y` we have
-`edist x y ≤ K * edist (f x) (f y)`. -/
+`edist x y ≤ K * edist (f x) (f y)`. This can also be used as a predicate for bounded below
+linear operators, see `antilipschitzWith_iff_exists_mul_le_mul`. -/
 def AntilipschitzWith [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0) (f : α → β) :=
   ∀ x y, edist x y ≤ K * edist (f x) (f y)