refactor(data/real): generalize cau_seq to arbitrary metrics

the intent is to use this also for the complex numbers

analysis/metric_space.lean

@@ -9,7 +9,7 @@ Many definitions and theorems expected on metric spaces are already introduced o
 topological spaces. For example:
   open and closed sets, compactness, completeness, continuity and uniform continuity
 -/
-import data.real analysis.topology.topological_structures
+import data.real.basic analysis.topology.topological_structures
 open lattice set filter classical
 noncomputable theory
 

analysis/real.lean

@@ -65,7 +65,7 @@ theorem continuous_of_rat : continuous (coe : ℚ → ℝ) := uniform_continuous
 
 theorem real.uniform_continuous_add : uniform_continuous (λp : ℝ × ℝ, p.1 + p.2) :=
 uniform_continuous_of_metric.2 $ λ ε ε0,
-let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma ε0 in
+let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0 in
 ⟨δ, δ0, λ a b h, let ⟨h₁, h₂⟩ := max_lt_iff.1 h in Hδ h₁ h₂⟩
 
 -- TODO(Mario): Find a way to use rat_add_continuous_lemma
@@ -104,7 +104,7 @@ _ -/
 lemma real.uniform_continuous_inv (s : set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ x ∈ s, r ≤ abs x) :
   uniform_continuous (λp:s, p.1⁻¹) :=
 uniform_continuous_of_metric.2 $ λ ε ε0,
-let ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma ε0 r0 in
+let ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma abs ε0 r0 in
 ⟨δ, δ0, λ a b h, Hδ (H _ a.2) (H _ b.2) h⟩
 
 lemma real.uniform_continuous_abs : uniform_continuous (abs : ℝ → ℝ) :=
@@ -151,7 +151,7 @@ lemma real.uniform_continuous_mul (s : set (ℝ × ℝ))
   (H : ∀ x ∈ s, abs (x : ℝ × ℝ).1 < r₁ ∧ abs x.2 < r₂) :
   uniform_continuous (λp:s, p.1.1 * p.1.2) :=
 uniform_continuous_of_metric.2 $ λ ε ε0,
-let ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma ε0 r₁0 r₂0 in
+let ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma abs ε0 r₁0 r₂0 in
 ⟨δ, δ0, λ a b h,
   let ⟨h₁, h₂⟩ := max_lt_iff.1 h in Hδ (H _ a.2).1 (H _ b.2).2 h₁ h₂⟩
 
@@ -259,7 +259,7 @@ instance : complete_space ℝ :=
   { refine λ n, classical.choice _,
     cases inhabited_of_mem_sets cf.1 (F n).1.2 with x xS,
     exact ⟨⟨x, xS⟩⟩ },
-  let c : cau_seq ℝ,
+  let c : cau_seq ℝ abs,
   { refine ⟨λ n, G n, λ ε ε0, _⟩,
     cases hg _ ε0 with n hn,
     refine ⟨n, λ j jn, _⟩,

data/complex.lean

@@ -7,7 +7,7 @@ The complex numbers, modelled as R^2 in the obvious way.
 
 TODO: Add topology, and prove that the complexes are a topological ring.
 -/
-import data.real tactic.ring algebra.field
+import data.real.basic tactic.ring algebra.field
 
 structure complex : Type :=
 (re : ℝ) (im : ℝ)
@@ -253,37 +253,25 @@ by simp [abs, norm_sq_of_real, real.sqrt_mul_self_eq_abs]
 lemma abs_of_nonneg {r : ℝ} (h : 0 ≤ r) : abs r = r :=
 (abs_of_real _).trans (abs_of_nonneg h)
 
+lemma mul_self_abs (z : ℂ) : abs z * abs z = norm_sq z :=
+real.mul_self_sqrt (norm_sq_nonneg _)
+
 @[simp] lemma abs_zero : abs 0 = 0 := by simp [abs]
 @[simp] lemma abs_one : abs 1 = 1 := by simp [abs]
 @[simp] lemma abs_I : abs I = 1 := by simp [abs]
 
 lemma abs_nonneg (z : ℂ) : 0 ≤ abs z :=
 real.sqrt_nonneg _
 
-@[simp] lemma abs_abs (z : ℂ) : abs' (abs z) = abs z :=
-_root_.abs_of_nonneg (abs_nonneg _)
-
 @[simp] lemma abs_eq_zero {z : ℂ} : abs z = 0 ↔ z = 0 :=
 (real.sqrt_eq_zero $ norm_sq_nonneg _).trans norm_sq_eq_zero
 
-@[simp] lemma abs_pos {z : ℂ} : 0 < abs z ↔ z ≠ 0 :=
-real.sqrt_pos.trans norm_sq_pos
-
-@[simp] lemma abs_neg (z : ℂ) : abs (-z) = abs z :=
-by simp [abs]
-
-lemma abs_sub (z w : ℂ) : abs (z - w) = abs (w - z) :=
-by rw [← neg_sub, abs_neg]
-
 @[simp] lemma abs_conj (z : ℂ) : abs (conj z) = abs z :=
 by simp [abs]
 
 @[simp] lemma abs_mul (z w : ℂ) : abs (z * w) = abs z * abs w :=
 by rw [abs, norm_sq_mul, real.sqrt_mul (norm_sq_nonneg _)]; refl
 
-lemma mul_self_abs (z : ℂ) : abs z * abs z = norm_sq z :=
-real.mul_self_sqrt (norm_sq_nonneg _)
-
 lemma abs_re_le_abs (z : ℂ) : abs' z.re ≤ abs z :=
 by rw [mul_self_le_mul_self_iff (_root_.abs_nonneg z.re) (abs_nonneg _),
        abs_mul_abs_self, mul_self_abs];
@@ -310,8 +298,22 @@ begin
   simpa [-mul_re] using re_le_abs (z * conj w)
 end
 
-lemma abs_sub_le (a b c : ℂ) : abs (a - c) ≤ abs (a - b) + abs (b - c) :=
-by simpa using abs_add (a - b) (b - c)
+instance : is_absolute_value abs :=
+{ abv_nonneg  := abs_nonneg,
+  abv_eq_zero := λ _, abs_eq_zero,
+  abv_add     := abs_add,
+  abv_mul     := abs_mul }
+open is_absolute_value
+
+@[simp] lemma abs_abs (z : ℂ) : abs' (abs z) = abs z :=
+_root_.abs_of_nonneg (abs_nonneg _)
+
+@[simp] lemma abs_pos {z : ℂ} : 0 < abs z ↔ z ≠ 0 := abv_pos abs
+@[simp] lemma abs_neg : ∀ z, abs (-z) = abs z := abv_neg abs
+lemma abs_sub : ∀ z w, abs (z - w) = abs (w - z) := abv_sub abs
+lemma abs_sub_le : ∀ a b c, abs (a - c) ≤ abs (a - b) + abs (b - c) := abv_sub_le abs
+@[simp] theorem abs_inv : ∀ z, abs z⁻¹ = (abs z)⁻¹ := abv_inv abs
+@[simp] theorem abs_div : ∀ z w, abs (z / w) = abs z / abs w := abv_div abs
 
 -- TODO : instance : topological_ring ℂ := missing