refactor(algebra/abs): add has_abs class (#9172)

The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a `has_abs` notation class in #8673 for lattice ordered groups, along with the notation `|.|` and was asked by @eric-wieser and @jcommelin to add it in a separate PR and retro fit `has_abs` and the notation to mathlib.

I tried to introduce both the `has_abs` class and the `|.|` notation in #8891 . However, I'm finding such a large and wide-ranging PR unwieldy to work with, so I'm now opening this PR which just replaces the previous definitions of `abs : α → α` in the following locations:

https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/algebra/ordered_group.lean#L984

https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/topology/continuous_function/basic.lean#L113

Out of scope are the following `abs : α → β`:

https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/is_R_or_C.lean#L439

https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/basic.lean#L406

https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/real/nnreal.lean#L762

https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/num/basic.lean#L315

Replacing the `abs` notation with `|.|` can be considered in a subsequent PR.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

src/algebra/abs.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2021 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+
+/-!
+# Absolute value
+
+This file defines a notational class `has_abs` which adds the unary operator `abs` and the notation
+`|.|`. The concept of an absolute value occurs in lattice ordered groups and in GL and GM spaces.
+
+## Notations
+
+The notation `|.|` is introduced for the absolute value.
+
+## Tags
+
+absolute
+-/
+
+
+/--
+Absolute value is a unary operator with properties similar to the absolute value of a real number.
+-/
+class has_abs (α : Type*) := (abs : α → α)
+export has_abs (abs)
+
+notation `|`a`|` := abs a

src/algebra/lattice_ordered_group.lean

@@ -123,11 +123,6 @@ calc a⊓b * (a ⊔ b) = a ⊓ b * ((a * b) * (b⁻¹ ⊔ a⁻¹)) :
 ... = a⊓b * ((a * b) * (a ⊓ b)⁻¹) : by rw [inv_inf_eq_sup_inv, sup_comm]
 ... = a * b                       : by rw [mul_comm, inv_mul_cancel_right]
 
-/--
-Absolute value is a unary operator with properties similar to the absolute value of a real number.
--/
-local notation `|`a`|` := mabs a
-
 namespace lattice_ordered_comm_group
 
 -- Bourbaki A.VI.12 Definition 4
@@ -334,7 +329,7 @@ lemma pos_mul_neg [covariant_class α α (*) (≤)] (a : α) : |a| = a⁺ * a⁻
 begin
   rw le_antisymm_iff,
   split,
-  { unfold mabs,
+  { unfold has_abs.abs,
     rw sup_le_iff,
     split,
     { nth_rewrite 0 ← mul_one a,
@@ -484,7 +479,7 @@ equal to its absolute value `|a|`.
 @[to_additive abs_pos_eq]
 lemma mabs_pos_eq [covariant_class α α (*) (≤)] (a : α) (h: 1 ≤ a) : |a| = a :=
 begin
-  unfold mabs,
+  unfold has_abs.abs,
   rw [sup_eq_mul_pos_div, div_eq_mul_inv, inv_inv, ← pow_two, inv_mul_eq_iff_eq_mul,
     ← pow_two, m_pos_pos_id ],
   rw pow_two,

src/algebra/order/group.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import algebra.order.monoid
 import order.order_dual
+import algebra.abs
 
 /-!
 # Ordered groups
@@ -980,15 +981,14 @@ end linear_ordered_comm_group
 section covariant_add_le
 
 section has_neg
-variables [has_neg α] [linear_order α] {a b: α}
 
-/-- `mabs a` is the multiplicative absolute value of `a`. -/
-@[to_additive abs
-"`abs a` is the additive absolute value of `a`."
-]
-def mabs {α : Type*} [has_inv α] [lattice α] (a : α) : α := a ⊔ (a⁻¹)
+/-- `abs a` is the absolute value of `a`. -/
+@[to_additive, priority 100] -- see Note [lower instance priority]
+instance has_inv_lattice_has_abs [has_inv α] [lattice α] : has_abs (α)  := ⟨λa, a ⊔ (a⁻¹)⟩
+
+variables [has_neg α] [linear_order α] {a b: α}
 
-lemma abs_eq_max_neg {α : Type*} [has_neg α] [linear_order α] (a : α) : abs a = max a (-a) :=
+lemma abs_eq_max_neg (a : α) : abs a = max a (-a) :=
 begin
   exact rfl,
 end

src/analysis/complex/basic.lean

@@ -66,14 +66,14 @@ lemma dist_eq (z w : ℂ) : dist z w = abs (z - w) := rfl
 
 @[simp] lemma norm_real (r : ℝ) : ∥(r : ℂ)∥ = ∥r∥ := abs_of_real _
 
-@[simp] lemma norm_rat (r : ℚ) : ∥(r : ℂ)∥ = _root_.abs (r : ℝ) :=
-suffices ∥((r : ℝ) : ℂ)∥ = _root_.abs r, by simpa,
+@[simp] lemma norm_rat (r : ℚ) : ∥(r : ℂ)∥ = |(r : ℝ)| :=
+suffices ∥((r : ℝ) : ℂ)∥ = |r|, by simpa,
 by rw [norm_real, real.norm_eq_abs]
 
 @[simp] lemma norm_nat (n : ℕ) : ∥(n : ℂ)∥ = n := abs_of_nat _
 
-@[simp] lemma norm_int {n : ℤ} : ∥(n : ℂ)∥ = _root_.abs n :=
-suffices ∥((n : ℝ) : ℂ)∥ = _root_.abs n, by simpa,
+@[simp] lemma norm_int {n : ℤ} : ∥(n : ℂ)∥ = has_abs.abs n :=
+suffices ∥((n : ℝ) : ℂ)∥ = has_abs.abs n, by simpa,
 by rw [norm_real, real.norm_eq_abs]
 
 lemma norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ∥(n : ℂ)∥ = n :=

src/analysis/inner_product_space/basic.lean

@@ -381,7 +381,7 @@ end
 variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 local notation `IK` := @is_R_or_C.I 𝕜 _
-local notation `absR` := _root_.abs
+local notation `absR` := has_abs.abs
 local notation `absK` := @is_R_or_C.abs 𝕜 _
 local postfix `†`:90 := @is_R_or_C.conj 𝕜 _
 local postfix `⋆`:90 := complex.conj

src/analysis/inner_product_space/projection.lean

@@ -50,7 +50,7 @@ open_locale big_operators classical topological_space
 variables {𝕜 E F : Type*} [is_R_or_C 𝕜]
 variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
-local notation `absR` := _root_.abs
+local notation `absR` := has_abs.abs
 
 /-! ### Orthogonal projection in inner product spaces -/
 

src/data/complex/basic.lean

@@ -424,7 +424,7 @@ by simp only [sub_conj, of_real_mul, of_real_one, of_real_bit0, mul_right_comm,
 /-- The complex absolute value function, defined as the square root of the norm squared. -/
 @[pp_nodot] noncomputable def abs (z : ℂ) : ℝ := (norm_sq z).sqrt
 
-local notation `abs'` := _root_.abs
+local notation `abs'` := has_abs.abs
 
 @[simp, norm_cast] lemma abs_of_real (r : ℝ) : abs r = abs' r :=
 by simp [abs, norm_sq_of_real, real.sqrt_mul_self_eq_abs]

src/data/complex/exponential.lean

@@ -15,7 +15,7 @@ hyperbolic sine, hyperbolic cosine, and hyperbolic tangent functions.
 
 -/
 
-local notation `abs'` := _root_.abs
+local notation `abs'` := has_abs.abs
 open is_absolute_value
 open_locale classical big_operators nat
 
@@ -330,7 +330,7 @@ open cau_seq
 
 namespace complex
 
-lemma is_cau_abs_exp (z : ℂ) : is_cau_seq _root_.abs
+lemma is_cau_abs_exp (z : ℂ) : is_cau_seq has_abs.abs
   (λ n, ∑ m in range n, abs (z ^ m / m!)) :=
 let ⟨n, hn⟩ := exists_nat_gt (abs z) in
 have hn0 : (0 : ℝ) < n, from lt_of_le_of_lt (abs_nonneg _) hn,

src/data/complex/exponential_bounds.lean

@@ -13,7 +13,7 @@ import algebra.continued_fractions.computation.approximation_corollaries
 -/
 namespace real
 
-local notation `abs'` := _root_.abs
+local notation `abs'` := has_abs.abs
 open is_absolute_value finset cau_seq complex
 
 lemma exp_one_near_10 : abs' (exp 1 - 2244083/825552) ≤ 1/10^10 :=

src/data/complex/is_R_or_C.lean

@@ -438,7 +438,7 @@ end
 /-- The complex absolute value function, defined as the square root of the norm squared. -/
 @[pp_nodot] noncomputable def abs (z : K) : ℝ := (norm_sq z).sqrt
 
-local notation `abs'` := _root_.abs
+local notation `abs'` := has_abs.abs
 local notation `absK` := @abs K _
 
 @[simp, norm_cast] lemma abs_of_real (r : ℝ) : absK r = abs' r :=
@@ -699,7 +699,7 @@ local notation `norm_sqR` := @is_R_or_C.norm_sq ℝ _
 @[simp] lemma conj_to_real {x : ℝ} : conjR x = x := rfl
 @[simp] lemma I_to_real : IR = 0 := rfl
 @[simp] lemma norm_sq_to_real {x : ℝ} : norm_sq x = x*x := by simp [is_R_or_C.norm_sq]
-@[simp] lemma abs_to_real {x : ℝ} : absR x = _root_.abs x :=
+@[simp] lemma abs_to_real {x : ℝ} : absR x = has_abs.abs x :=
 by simp [is_R_or_C.abs, abs, real.sqrt_mul_self_eq_abs]
 
 @[simp] lemma coe_real_eq_id : @coe ℝ ℝ _ = id := rfl

src/measure_theory/function/l1_space.lean

@@ -344,7 +344,7 @@ hf.mono $ eventually_of_forall $ λ x, by simp [real.norm_eq_abs, abs_le, abs_no
 lemma has_finite_integral.min_zero {f : α → ℝ} (hf : has_finite_integral f μ) :
   has_finite_integral (λa, min (f a) 0) μ :=
 hf.mono $ eventually_of_forall $ λ x,
-  by simp [real.norm_eq_abs, abs_le, abs_nonneg, neg_le, neg_le_abs_self]
+  by simp [real.norm_eq_abs, abs_le, abs_nonneg, neg_le, neg_le_abs_self, abs_eq_max_neg, le_total]
 
 end pos_part
 

src/number_theory/zsqrtd/gaussian_int.lean

@@ -125,7 +125,7 @@ lemma to_complex_div_im (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).im = round ((x
 by rw [div_def, ← @rat.cast_round ℝ _ _, ← @rat.cast_round ℝ _ _];
   simp [-rat.cast_round, mul_assoc, div_eq_mul_inv, mul_add, add_mul]
 
-local notation `abs'` := _root_.abs
+local notation `abs'` := has_abs.abs
 
 lemma norm_sq_le_norm_sq_of_re_le_of_im_le {x y : ℂ} (hre : abs' x.re ≤ abs' y.re)
   (him : abs' x.im ≤ abs' y.im) : x.norm_sq ≤ y.norm_sq :=

src/topology/continuous_function/algebra.lean

@@ -605,11 +605,11 @@ variables {α : Type*} [topological_space α]
 variables {β : Type*} [linear_ordered_field β] [topological_space β]
   [order_topology β] [topological_ring β]
 
-lemma inf_eq (f g : C(α, β)) : f ⊓ g = (2⁻¹ : β) • (f + g - (f - g).abs) :=
+lemma inf_eq (f g : C(α, β)) : f ⊓ g = (2⁻¹ : β) • (f + g - |f - g|) :=
 ext (λ x, by simpa using min_eq_half_add_sub_abs_sub)
 
 -- Not sure why this is grosser than `inf_eq`:
-lemma sup_eq (f g : C(α, β)) : f ⊔ g = (2⁻¹ : β) • (f + g + (f - g).abs) :=
+lemma sup_eq (f g : C(α, β)) : f ⊔ g = (2⁻¹ : β) • (f + g + |f - g|) :=
 ext (λ x, by simpa [mul_add] using @max_eq_half_add_add_abs_sub _ _ (f x) (g x))
 
 end lattice

src/topology/continuous_function/basic.lean

@@ -112,9 +112,12 @@ variables [linear_ordered_add_comm_group β] [order_topology β]
 
 /-- The pointwise absolute value of a continuous function as a continuous function. -/
 def abs (f : C(α, β)) : C(α, β) :=
-{ to_fun := λ x, abs (f x), }
+{ to_fun := λ x, |f x|, }
 
-@[simp] lemma abs_apply (f : C(α, β)) (x : α) : f.abs x = _root_.abs (f x) :=
+@[priority 100] -- see Note [lower instance priority]
+instance : has_abs C(α, β) := ⟨λf, abs f⟩
+
+@[simp] lemma abs_apply (f : C(α, β)) (x : α) : |f| x = |f x| :=
 rfl
 
 end

src/topology/continuous_function/stone_weierstrass.lean

@@ -112,7 +112,7 @@ begin
   let M := ∥f∥,
   let f' := attach_bound (f : C(X, ℝ)),
   let abs : C(set.Icc (-∥f∥) (∥f∥), ℝ) :=
-  { to_fun := λ x : set.Icc (-∥f∥) (∥f∥), _root_.abs (x : ℝ) },
+  { to_fun := λ x : set.Icc (-∥f∥) (∥f∥), |(x : ℝ)| },
   change (abs.comp f') ∈ A.topological_closure,
   apply comp_attach_bound_mem_closure,
 end