feat(analysis/normed_space/basic): uniform_continuous_norm (#6162)

From `lean-liquid`

src/analysis/asymptotics/asymptotics.lean

@@ -1278,7 +1278,7 @@ by { convert is_o_pow_pow h, simp only [pow_one] }
 
 theorem is_o_norm_pow_id {n : ℕ} (h : 1 < n) :
   is_o (λ(x : E'), ∥x∥^n) (λx, x) (𝓝 0) :=
-by simpa only [pow_one, is_o_norm_right] using is_o_norm_pow_norm_pow h
+by simpa only [pow_one, is_o_norm_right] using @is_o_norm_pow_norm_pow E' _ _ _ h
 
 theorem is_O_with.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c f₁ f₂ l) (hc : c < 1) :
   is_O_with (1 / (1 - c)) f₂ (λx, f₂ x - f₁ x) l :=

src/analysis/normed_space/basic.lean

@@ -72,6 +72,12 @@ noncomputable def normed_group.of_core (α : Type*) [add_comm_group α] [has_nor
     calc ∥x - y∥ = ∥ -(y - x)∥ : by simp
              ... = ∥y - x∥ : by { rw [C.norm_neg] } }
 
+instance : normed_group ℝ :=
+{ norm := λ x, abs x,
+  dist_eq := assume x y, rfl }
+
+lemma real.norm_eq_abs (r : ℝ) : ∥r∥ = abs r := rfl
+
 section normed_group
 variables [normed_group α] [normed_group β]
 
@@ -84,6 +90,9 @@ by rw [dist_comm, dist_eq_norm]
 @[simp] lemma dist_zero_right (g : α) : dist g 0 = ∥g∥ :=
 by rw [dist_eq_norm, sub_zero]
 
+@[simp] lemma dist_zero_left : dist (0:α) = norm :=
+funext $ λ g, by rw [dist_comm, dist_zero_right]
+
 lemma tendsto_norm_cocompact_at_top [proper_space α] :
   tendsto norm (cocompact α) at_top :=
 by simpa only [dist_zero_right] using tendsto_dist_right_cocompact_at_top (0:α)
@@ -460,7 +469,7 @@ by { convert tendsto_iff_dist_tendsto_zero, simp [dist_eq_norm] }
 
 lemma tendsto_zero_iff_norm_tendsto_zero {f : γ → β} {a : filter γ} :
   tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥f e∥) a (𝓝 0) :=
-by simp [tendsto_iff_norm_tendsto_zero]
+by { rw [tendsto_iff_norm_tendsto_zero], simp only [sub_zero] }
 
 /-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real
 function `g` which tends to `0`, then `f` tends to `0`.
@@ -496,6 +505,15 @@ by simpa using continuous_id.dist (continuous_const : continuous (λ g, (0:α)))
 lemma continuous_nnnorm : continuous (nnnorm : α → ℝ≥0) :=
 continuous_subtype_mk _ continuous_norm
 
+lemma lipschitz_with_one_norm : lipschitz_with 1 (norm : α → ℝ) :=
+by simpa only [dist_zero_left] using lipschitz_with.dist_right (0 : α)
+
+lemma uniform_continuous_norm : uniform_continuous (norm : α → ℝ) :=
+lipschitz_with_one_norm.uniform_continuous
+
+lemma uniform_continuous_nnnorm : uniform_continuous (nnnorm : α → ℝ≥0) :=
+uniform_continuous_subtype_mk uniform_continuous_norm _
+
 lemma tendsto_norm_nhds_within_zero : tendsto (norm : α → ℝ) (𝓝[{0}ᶜ] 0) (𝓝[set.Ioi 0] 0) :=
 (continuous_norm.tendsto' (0 : α) 0 norm_zero).inf $ tendsto_principal_principal.2 $
   λ x, norm_pos_iff.2
@@ -850,17 +868,14 @@ by simpa only [is_unit_iff_ne_zero] using punctured_nhds_ne_bot (0:α)
 end normed_field
 
 instance : normed_field ℝ :=
-{ norm := λ x, abs x,
-  dist_eq := assume x y, rfl,
-  norm_mul' := abs_mul }
+{ norm_mul' := abs_mul,
+  .. real.normed_group }
 
 instance : nondiscrete_normed_field ℝ :=
 { non_trivial := ⟨2, by { unfold norm, rw abs_of_nonneg; norm_num }⟩ }
 
 namespace real
 
-lemma norm_eq_abs (r : ℝ) : ∥r∥ = abs r := rfl
-
 lemma norm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ∥x∥ = x :=
 abs_of_nonneg hx