From 7eacca31fa6f5980038bf433fc8e75a4df6ac803 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 5 May 2022 07:41:33 +0000
Subject: [PATCH] =?UTF-8?q?feat(analysis/normed/normed=5Ffield):=20limit?=
 =?UTF-8?q?=20of=20`=E2=88=A5a=20*=20x=E2=88=A5`=20as=20`=E2=88=A5x?=
 =?UTF-8?q?=E2=88=A5=20=E2=86=92=20=E2=88=9E`=20(#13819)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

These lemmas should use `bornology.cobounded` but we don't have an instance `pseudo_metric_space α -> bornology α` yet.
---
 src/analysis/normed/group/basic.lean  |  6 ++++++
 src/analysis/normed/normed_field.lean | 16 ++++++++++++++--
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/src/analysis/normed/group/basic.lean b/src/analysis/normed/group/basic.lean
index fe3da3b684567..05c587581b6df 100644
--- a/src/analysis/normed/group/basic.lean
+++ b/src/analysis/normed/group/basic.lean
@@ -166,6 +166,12 @@ by rw [sub_eq_add_neg, dist_self_add_right, norm_neg]
 @[simp] theorem dist_self_sub_left (g h : E) : dist (g - h) g = ∥h∥ :=
 by rw [dist_comm, dist_self_sub_right]
 
+/-- In a (semi)normed group, negation `x ↦ -x` tends to infinity at infinity. TODO: use
+`bornology.cobounded` instead of `filter.comap has_norm.norm filter.at_top`. -/
+lemma filter.tendsto_neg_cobounded :
+  tendsto (has_neg.neg : E → E) (comap norm at_top) (comap norm at_top) :=
+by simpa only [norm_neg, tendsto_comap_iff, (∘)] using tendsto_comap
+
 /-- **Triangle inequality** for the norm. -/
 lemma norm_add_le (g h : E) : ∥g + h∥ ≤ ∥g∥ + ∥h∥ :=
 by simpa [dist_eq_norm] using dist_triangle g 0 (-h)
diff --git a/src/analysis/normed/normed_field.lean b/src/analysis/normed/normed_field.lean
index 2247519ba7780..ba363db236272 100644
--- a/src/analysis/normed/normed_field.lean
+++ b/src/analysis/normed/normed_field.lean
@@ -385,8 +385,6 @@ instance normed_division_ring.to_norm_one_class : norm_one_class α :=
 ⟨mul_left_cancel₀ (mt norm_eq_zero.1 (@one_ne_zero α _ _)) $
   by rw [← norm_mul, mul_one, mul_one]⟩
 
-export norm_one_class (norm_one)
-
 @[simp] lemma nnnorm_mul (a b : α) : ∥a * b∥₊ = ∥a∥₊ * ∥b∥₊ :=
 nnreal.eq $ norm_mul a b
 
@@ -422,6 +420,20 @@ nnreal.eq $ by simp
 @[simp] lemma nnnorm_zpow : ∀ (a : α) (n : ℤ), ∥a ^ n∥₊ = ∥a∥₊ ^ n :=
 (nnnorm_hom : α →*₀ ℝ≥0).map_zpow
 
+/-- Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
+infinity. TODO: use `bornology.cobounded` instead of `filter.comap has_norm.norm filter.at_top`. -/
+lemma filter.tendsto_mul_left_cobounded {a : α} (ha : a ≠ 0) :
+  tendsto ((*) a) (comap norm at_top) (comap norm at_top) :=
+by simpa only [tendsto_comap_iff, (∘), norm_mul]
+  using tendsto_const_nhds.mul_at_top (norm_pos_iff.2 ha) tendsto_comap
+
+/-- Multiplication on the right by a nonzero element of a normed division ring tends to infinity at
+infinity. TODO: use `bornology.cobounded` instead of `filter.comap has_norm.norm filter.at_top`. -/
+lemma filter.tendsto_mul_right_cobounded {a : α} (ha : a ≠ 0) :
+  tendsto (λ x, x * a) (comap norm at_top) (comap norm at_top) :=
+by simpa only [tendsto_comap_iff, (∘), norm_mul]
+  using tendsto_comap.at_top_mul (norm_pos_iff.2 ha) tendsto_const_nhds
+
 @[priority 100] -- see Note [lower instance priority]
 instance normed_division_ring.to_has_continuous_inv₀ : has_continuous_inv₀ α :=
 begin