chore(analysis/normed/group/basic): Earlier ℝ lemmas (#16972)

Move lemmas about the norm on `ℝ` from `analysis.normed.field.basic` to `analysis.normed.group.basic`.

This avoids having to import `normed_field` to use `real.norm_of_nonneg`.

src/analysis/normed/field/basic.lean

@@ -632,43 +632,11 @@ noncomputable instance : densely_normed_field ℝ :=
 
 namespace real
 
-lemma norm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ∥x∥ = x :=
-abs_of_nonneg hx
+lemma to_nnreal_mul_nnnorm {x : ℝ} (y : ℝ) (hx : 0 ≤ x) : x.to_nnreal * ∥y∥₊ = ∥x * y∥₊ :=
+by simp [real.to_nnreal_of_nonneg, nnnorm, norm_of_nonneg, hx]
 
-lemma norm_of_nonpos {x : ℝ} (hx : x ≤ 0) : ∥x∥ = -x :=
-abs_of_nonpos hx
-
-lemma le_norm_self (r : ℝ) : r ≤ ∥r∥ := le_abs_self r
-
-@[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℝ)∥ = n := abs_of_nonneg n.cast_nonneg
-
-@[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥(n : ℝ)∥₊ = n := nnreal.eq $ by simp
-
-@[simp] lemma norm_two : ∥(2 : ℝ)∥ = 2 := abs_of_pos (@zero_lt_two ℝ _ _)
-
-@[simp] lemma nnnorm_two : ∥(2 : ℝ)∥₊ = 2 := nnreal.eq $ by simp
-
-lemma nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ∥x∥₊ = ⟨x, hx⟩ :=
-nnreal.eq $ norm_of_nonneg hx
-
-lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (∥x∥₊ : ℝ≥0∞) = ennreal.of_real x :=
-by { rw [← of_real_norm_eq_coe_nnnorm, norm_of_nonneg hx] }
-
-lemma of_real_le_ennnorm (x : ℝ) : ennreal.of_real x ≤ ∥x∥₊ :=
-begin
-  by_cases hx : 0 ≤ x,
-  { rw real.ennnorm_eq_of_real hx, refl' },
-  { rw [ennreal.of_real_eq_zero.2 (le_of_lt (not_le.1 hx))],
-    exact bot_le }
-end
-
-lemma to_nnreal_mul_nnnorm {x : ℝ} (y : ℝ) (hr : 0 ≤ x) : x.to_nnreal * ∥y∥₊ = ∥x * y∥₊ :=
-begin
-  rw real.to_nnreal_of_nonneg hr,
-  simp only [nnnorm_mul, mul_eq_mul_right_iff],
-  refine or.inl (nnreal.eq _),
-  simp only [subtype.coe_mk, coe_nnnorm, real.norm_eq_abs, abs_of_nonneg hr]
-end
+lemma nnnorm_mul_to_nnreal (x : ℝ) {y : ℝ} (hy : 0 ≤ y) : ∥x∥₊ * y.to_nnreal = ∥x * y∥₊ :=
+by simp [real.to_nnreal_of_nonneg, nnnorm, norm_of_nonneg, hy]
 
 /-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points.
 This is a particular case of `module.punctured_nhds_ne_bot`. -/

src/analysis/normed/group/basic.lean

@@ -279,12 +279,6 @@ instance : normed_add_comm_group punit :=
 
 @[simp] lemma punit.norm_eq_zero (r : punit) : ∥r∥ = 0 := rfl
 
-instance : has_norm ℝ := { norm := λ x, |x| }
-
-@[simp] lemma real.norm_eq_abs (r : ℝ) : ∥r∥ = |r| := rfl
-
-instance : normed_add_comm_group ℝ := ⟨λ x y, rfl⟩
-
 section seminormed_group
 variables [seminormed_group E] [seminormed_group F] [seminormed_group G] {s : set E}
   {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : ℝ}
@@ -1160,13 +1154,47 @@ lemma nnnorm_prod_le_of_le (s : finset ι) {f : ι → E} {n : ι → ℝ≥0} (
   ∥∏ b in s, f b∥₊ ≤ ∑ b in s, n b :=
 (norm_prod_le_of_le s h).trans_eq nnreal.coe_sum.symm
 
-lemma real.to_nnreal_eq_nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) : r.to_nnreal = ∥r∥₊ :=
+namespace real
+
+instance : has_norm ℝ := { norm := λ r, |r| }
+
+@[simp] lemma norm_eq_abs (r : ℝ) : ∥r∥ = |r| := rfl
+
+instance : normed_add_comm_group ℝ := ⟨λ r y, rfl⟩
+
+lemma norm_of_nonneg (hr : 0 ≤ r) : ∥r∥ = r := abs_of_nonneg hr
+lemma norm_of_nonpos (hr : r ≤ 0) : ∥r∥ = -r := abs_of_nonpos hr
+lemma le_norm_self (r : ℝ) : r ≤ ∥r∥ := le_abs_self r
+
+@[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℝ)∥ = n := abs_of_nonneg n.cast_nonneg
+@[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥(n : ℝ)∥₊ = n := nnreal.eq $ norm_coe_nat _
+
+@[simp] lemma norm_two : ∥(2 : ℝ)∥ = 2 := abs_of_pos (@zero_lt_two ℝ _ _)
+
+@[simp] lemma nnnorm_two : ∥(2 : ℝ)∥₊ = 2 := nnreal.eq $ by simp
+
+lemma nnnorm_of_nonneg (hr : 0 ≤ r) : ∥r∥₊ = ⟨r, hr⟩ := nnreal.eq $ norm_of_nonneg hr
+
+lemma ennnorm_eq_of_real (hr : 0 ≤ r) : (∥r∥₊ : ℝ≥0∞) = ennreal.of_real r :=
+by { rw [← of_real_norm_eq_coe_nnnorm, norm_of_nonneg hr] }
+
+lemma to_nnreal_eq_nnnorm_of_nonneg (hr : 0 ≤ r) : r.to_nnreal = ∥r∥₊ :=
 begin
   rw real.to_nnreal_of_nonneg hr,
   congr,
   rw [real.norm_eq_abs, abs_of_nonneg hr],
 end
 
+lemma of_real_le_ennnorm (r : ℝ) : ennreal.of_real r ≤ ∥r∥₊ :=
+begin
+  obtain hr | hr := le_total 0 r,
+  { exact (real.ennnorm_eq_of_real hr).ge },
+  { rw [ennreal.of_real_eq_zero.2 hr],
+    exact bot_le }
+end
+
+end real
+
 namespace lipschitz_with
 variables [pseudo_emetric_space α] {K Kf Kg : ℝ≥0} {f g : α → E}