refactor: add has_abs class

archive/imo/imo2006_q3.lean

@@ -64,7 +64,7 @@ le_of_sub_nonneg $
 lemma zero_lt_32 : (0 : ℝ) < 32 := by norm_num
 
 theorem subst_wlog {x y z s : ℝ} (hxy : 0 ≤ x * y) (hxyz : x + y + z = 0) :
-  32 * abs (x * y * z * s) ≤ sqrt 2 * (x^2 + y^2 + z^2 + s^2)^2 :=
+  32 * |x * y * z * s| ≤ sqrt 2 * (x^2 + y^2 + z^2 + s^2)^2 :=
 have hz : (x + y)^2 = z^2 := neg_eq_of_add_eq_zero hxyz ▸ (neg_sq _).symm,
 have hs : 0 ≤ 2 * s ^ 2 := mul_nonneg zero_le_two (sq_nonneg s),
 have this : _ :=
@@ -76,7 +76,7 @@ have this : _ :=
             (add_nonneg (mul_nonneg zero_lt_three.le (sq_nonneg _)) hs)
             (add_le_add_right rhs_ineq _) _,
 le_of_pow_le_pow _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) nat.succ_pos' $
-  calc  (32 * abs (x * y * z * s)) ^ 2
+  calc  (32 * |x * y * z * s|) ^ 2
       = 32 * ((2 * s^2) * (16 * x^2 * y^2 * (x + y)^2)) :
           by rw [mul_pow, sq_abs, hz]; ring
   ... ≤ 32 * ((2 * (x^2 + y^2 + (x + y)^2) + 2 * s^2)^4 / 4^4) :
@@ -88,7 +88,7 @@ le_of_pow_le_pow _ (mul_nonneg (sqrt_nonneg _) (sq_nonneg _)) nat.succ_pos' $
 
 /-- Proof that `M = 9 * sqrt 2 / 32` works with the substitution. -/
 theorem subst_proof₁ (x y z s : ℝ) (hxyz : x + y + z = 0) :
-  abs (x * y * z * s) ≤ sqrt 2 / 32 * (x^2 + y^2 + z^2 + s^2)^2 :=
+  |x * y * z * s| ≤ sqrt 2 / 32 * (x^2 + y^2 + z^2 + s^2)^2 :=
 begin
   wlog h' := mul_nonneg_of_three x y z using [x y z, y z x, z x y] tactic.skip,
   { rw [div_mul_eq_mul_div, le_div_iff' zero_lt_32],
@@ -109,15 +109,15 @@ lemma lhs_identity (a b c : ℝ) :
 by ring
 
 theorem proof₁ {a b c : ℝ} :
-  abs (a * b * (a^2 - b^2) + b * c * (b^2 - c^2) + c * a * (c^2 - a^2)) ≤
+  |a * b * (a^2 - b^2) + b * c * (b^2 - c^2) + c * a * (c^2 - a^2)| ≤
   9 * sqrt 2 / 32 * (a^2 + b^2 + c^2)^2 :=
 calc _ = _ : congr_arg _ $ lhs_identity a b c
    ... ≤ _ : subst_proof₁ (a - b) (b - c) (c - a) (-(a + b + c)) (by ring)
    ... = _ : by ring
 
 theorem proof₂ (M : ℝ)
   (h : ∀ a b c : ℝ,
-    abs (a * b * (a^2 - b^2) + b * c * (b^2 - c^2) + c * a * (c^2 - a^2)) ≤
+    |a * b * (a^2 - b^2) + b * c * (b^2 - c^2) + c * a * (c^2 - a^2)| ≤
     M * (a^2 + b^2 + c^2)^2) :
   9 * sqrt 2 / 32 ≤ M :=
 begin
@@ -137,7 +137,7 @@ end
 
 theorem imo2006_q3 (M : ℝ) :
   (∀ a b c : ℝ,
-    abs (a * b * (a^2 - b^2) + b * c * (b^2 - c^2) + c * a * (c^2 - a^2)) ≤
+    |a * b * (a^2 - b^2) + b * c * (b^2 - c^2) + c * a * (c^2 - a^2)| ≤
     M * (a^2 + b^2 + c^2)^2) ↔
   9 * sqrt 2 / 32 ≤ M :=
 ⟨proof₂ M, λ h _ _ _, le_trans proof₁ $ mul_le_mul_of_nonneg_right h $ sq_nonneg _⟩

archive/imo/imo2008_q4.lean

@@ -22,7 +22,7 @@ The desired theorem is that either `f = λ x, x` or `f = λ x, 1/x`
 
 open real
 
-lemma abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : abs x = 1 :=
+lemma abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : |x| = 1 :=
 by rw [← pow_left_inj (abs_nonneg x) zero_le_one (pos_iff_ne_zero.2 hn), one_pow, pow_abs, h,
   abs_one]
 

archive/sensitivity.lean

@@ -41,7 +41,6 @@ open_locale classical
 /-! We also want to use the notation `∑` for sums. -/
 open_locale big_operators
 
-notation `|`x`|` := abs x
 notation `√` := real.sqrt
 
 open function bool linear_map fintype finite_dimensional dual_pair

counterexamples/phillips.lean

@@ -156,7 +156,7 @@ and show that such an object can be split into a discrete part and a continuous
 structure bounded_additive_measure (α : Type u) :=
 (to_fun : set α → ℝ)
 (additive' : ∀ s t, disjoint s t → to_fun (s ∪ t) = to_fun s + to_fun t)
-(exists_bound : ∃ (C : ℝ), ∀ s, abs (to_fun s) ≤ C)
+(exists_bound : ∃ (C : ℝ), ∀ s, |to_fun s| ≤ C)
 
 instance : inhabited (bounded_additive_measure α) :=
 ⟨{ to_fun := λ s, 0,
@@ -175,7 +175,7 @@ lemma additive (f : bounded_additive_measure α) (s t : set α)
 f.additive' s t h
 
 lemma abs_le_bound (f : bounded_additive_measure α) (s : set α) :
-  abs (f s) ≤ f.C :=
+  |f s| ≤ f.C :=
 f.exists_bound.some_spec s
 
 lemma le_bound (f : bounded_additive_measure α) (s : set α) :

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/archimedean.lean

@@ -319,7 +319,7 @@ def round (x : α) : ℤ := ⌊x + 1 / 2⌋
 @[simp] lemma round_zero : round (0 : α) = 0 := floor_eq_iff.2 (by norm_num)
 @[simp] lemma round_one : round (1 : α) = 1 := floor_eq_iff.2 (by norm_num)
 
-lemma abs_sub_round (x : α) : abs (x - round x) ≤ 1 / 2 :=
+lemma abs_sub_round (x : α) : |x - round x| ≤ 1 / 2 :=
 begin
   rw [round, abs_sub_le_iff],
   have := floor_le (x + 1 / 2),
@@ -343,7 +343,7 @@ section
 variables [linear_ordered_field α] [archimedean α]
 
 theorem exists_rat_near (x : α) {ε : α} (ε0 : 0 < ε) :
-  ∃ q : ℚ, abs (x - q) < ε :=
+  ∃ q : ℚ, |x - q| < ε :=
 let ⟨q, h₁, h₂⟩ := exists_rat_btwn $
   lt_trans ((sub_lt_self_iff x).2 ε0) ((lt_add_iff_pos_left x).2 ε0) in
 ⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩

src/algebra/big_operators/order.lean

@@ -185,11 +185,11 @@ lemma prod_le_prod_fiberwise_of_prod_fiber_le_one' {t : finset ι'}
 end
 
 lemma abs_sum_le_sum_abs {G : Type*} [linear_ordered_add_comm_group G] (f : ι → G) (s : finset ι) :
-  abs (∑ i in s, f i) ≤ ∑ i in s, abs (f i) :=
+  |∑ i in s, f i| ≤ ∑ i in s, |f i| :=
 le_sum_of_subadditive _ abs_zero abs_add s f
 
 lemma abs_prod {R : Type*} [linear_ordered_comm_ring R] {f : ι → R} {s : finset ι} :
-  abs (∏ x in s, f x) = ∏ x in s, abs (f x) :=
+  |∏ x in s, f x| = ∏ x in s, |f x| :=
 (abs_hom.to_monoid_hom : R →* R).map_prod _ _
 
 section pigeonhole

src/algebra/continued_fractions/computation/approximation_corollaries.lean

@@ -71,7 +71,6 @@ We next show that `(generalized_continued_fraction.of v).convergents v` converge
 -/
 
 variable [archimedean K]
-local notation `|` x `|` := abs x
 open nat
 
 theorem of_convergence_epsilon :

src/algebra/continued_fractions/computation/approximations.lean

@@ -471,8 +471,6 @@ begin
       ... = (-1)^n / (B * (ifp.fr⁻¹ * B + pB))                      : by ac_refl }
 end
 
-local notation `|` x `|` := abs x
-
 /-- Shows that `|v - Aₙ / Bₙ| ≤ 1 / (Bₙ * Bₙ₊₁)` -/
 theorem abs_sub_convergents_le (not_terminated_at_n : ¬(gcf.of v).terminated_at n) :
     |v - (gcf.of v).convergents n|

src/algebra/field_power.lean

@@ -156,25 +156,25 @@ theorem fpow_odd_neg (ha : a < 0) (hn : odd n) : a ^ n < 0:=
 by cases hn with k hk; simpa only [hk, two_mul] using fpow_bit1_neg_iff.mpr ha
 
 lemma fpow_even_abs (a : K) {p : ℤ} (hp : even p) :
-  abs a ^ p = a ^ p :=
+  |a| ^ p = a ^ p :=
 begin
   cases abs_choice a with h h;
   simp only [h, fpow_even_neg _ hp],
 end
 
 @[simp] lemma fpow_bit0_abs (a : K) (p : ℤ) :
-  (abs a) ^ bit0 p = a ^ bit0 p :=
+  (|a|) ^ bit0 p = a ^ bit0 p :=
 fpow_even_abs _ (even_bit0 _)
 
 lemma abs_fpow_even (a : K) {p : ℤ} (hp : even p) :
-  abs (a ^ p) = a ^ p :=
+  |a ^ p| = a ^ p :=
 begin
   rw [abs_eq_self],
   exact fpow_even_nonneg _ hp
 end
 
 @[simp] lemma abs_fpow_bit0 (a : K) (p : ℤ) :
-  abs (a ^ bit0 p) = a ^ bit0 p :=
+  |a ^ bit0 p| = a ^ bit0 p :=
 abs_fpow_even _ (even_bit0 _)
 
 end ordered_field_power

src/algebra/floor.lean

@@ -114,7 +114,7 @@ eq.trans (by rw [int.cast_neg, sub_eq_add_neg]) (floor_add_int _ _)
 floor_sub_int x n
 
 lemma abs_sub_lt_one_of_floor_eq_floor {α : Type*} [linear_ordered_comm_ring α]
-  [floor_ring α] {x y : α} (h : ⌊x⌋ = ⌊y⌋) : abs (x - y) < 1 :=
+  [floor_ring α] {x y : α} (h : ⌊x⌋ = ⌊y⌋) : |x - y| < 1 :=
 begin
   have : x < ⌊x⌋ + 1         := lt_floor_add_one x,
   have : y < ⌊y⌋ + 1         :=  lt_floor_add_one y,

src/algebra/group_power/lemmas.lean

@@ -246,7 +246,7 @@ theorem gsmul_lt_gsmul' {n : ℤ} (hn : 0 < n) {a₁ a₂ : A} (h : a₁ < a₂)
 gsmul_strict_mono_right A hn h
 
 lemma abs_nsmul {α : Type*} [linear_ordered_add_comm_group α] (n : ℕ) (a : α) :
-  abs (n • a) = n • abs a :=
+  |n • a| = n • |a| :=
 begin
   cases le_total a 0 with hneg hpos,
   { rw [abs_of_nonpos hneg, ← abs_neg, ← neg_nsmul, abs_of_nonneg],
@@ -256,7 +256,7 @@ begin
 end
 
 lemma abs_gsmul {α : Type*} [linear_ordered_add_comm_group α] (n : ℤ) (a : α) :
-  abs (n • a) = (abs n) • abs a :=
+  |n • a| = |n| • |a| :=
 begin
   by_cases n0 : 0 ≤ n,
   { lift n to ℕ using n0,
@@ -268,15 +268,15 @@ begin
 end
 
 lemma abs_add_eq_add_abs_le {α : Type*} [linear_ordered_add_comm_group α] {a b : α} (hle : a ≤ b) :
-  abs (a + b) = abs a + abs b ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
+  |a + b| = |a| + |b| ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
 begin
   by_cases a0 : 0 ≤ a; by_cases b0 : 0 ≤ b,
   { simp [a0, b0, abs_of_nonneg, add_nonneg a0 b0] },
   { exact (lt_irrefl (0 : α) (a0.trans_lt (hle.trans_lt (not_le.mp b0)))).elim },
   any_goals { simp [(not_le.mp a0).le, (not_le.mp b0).le, abs_of_nonpos, add_nonpos, add_comm] },
   obtain F := (not_le.mp a0),
-  have : (abs (a + b) = -a + b ↔ b ≤ 0) ↔ (abs (a + b) =
-    abs a + abs b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0),
+  have : (|a + b| = -a + b ↔ b ≤ 0) ↔ (|a + b| =
+    |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0),
   { simp [a0, b0, abs_of_neg, abs_of_nonneg, F, F.le] },
   refine this.mp ⟨λ h, _, λ h, by simp only [le_antisymm h b0, abs_of_neg F, add_zero]⟩,
   by_cases ba : a + b ≤ 0,
@@ -288,7 +288,7 @@ begin
 end
 
 lemma abs_add_eq_add_abs_iff {α : Type*} [linear_ordered_add_comm_group α] (a b : α) :
-  abs (a + b) = abs a + abs b ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
+  |a + b| = |a| + |b| ↔ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) :=
 begin
   by_cases ab : a ≤ b,
   { exact abs_add_eq_add_abs_le ab },
@@ -499,7 +499,7 @@ section linear_ordered_ring
 
 variables [linear_ordered_ring R] {a : R} {n : ℕ}
 
-@[simp] lemma abs_pow (a : R) (n : ℕ) : abs (a ^ n) = abs a ^ n :=
+@[simp] lemma abs_pow (a : R) (n : ℕ) : |a ^ n| = |a| ^ n :=
 (pow_abs a n).symm
 
 @[simp] theorem pow_bit1_neg_iff : a ^ bit1 n < 0 ↔ a < 0 :=
@@ -534,14 +534,14 @@ theorem pow_odd_neg (ha : a < 0) (hn : odd n) : a ^ n < 0:=
 by cases hn with k hk; simpa only [hk, two_mul] using pow_bit1_neg_iff.mpr ha
 
 lemma pow_even_abs (a : R) {p : ℕ} (hp : even p) :
-  abs a ^ p = a ^ p :=
+  |a| ^ p = a ^ p :=
 begin
   rw [←abs_pow, abs_eq_self],
   exact pow_even_nonneg _ hp
 end
 
 @[simp] lemma pow_bit0_abs (a : R) (p : ℕ) :
-  abs a ^ bit0 p = a ^ bit0 p :=
+  |a| ^ bit0 p = a ^ bit0 p :=
 pow_even_abs _ (even_bit0 _)
 
 lemma strict_mono_pow_bit1 (n : ℕ) : strict_mono (λ a : R, a ^ bit1 n) :=

src/algebra/group_power/order.lean

@@ -217,10 +217,10 @@ section linear_ordered_ring
 
 variable [linear_ordered_ring R]
 
-lemma pow_abs (a : R) (n : ℕ) : (abs a) ^ n = abs (a ^ n) :=
+lemma pow_abs (a : R) (n : ℕ) : |a| ^ n = |a ^ n| :=
 ((abs_hom.to_monoid_hom : R →* R).map_pow a n).symm
 
-lemma abs_neg_one_pow (n : ℕ) : abs ((-1 : R) ^ n) = 1 :=
+lemma abs_neg_one_pow (n : ℕ) : |(-1 : R) ^ n| = 1 :=
 by rw [←pow_abs, abs_neg, abs_one, one_pow]
 
 theorem pow_bit0_nonneg (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n :=
@@ -241,28 +241,28 @@ alias sq_pos_of_ne_zero ← pow_two_pos_of_ne_zero
 
 variables {x y : R}
 
-theorem sq_abs (x : R) : abs x ^ 2 = x ^ 2 :=
+theorem sq_abs (x : R) : |x| ^ 2 = x ^ 2 :=
 by simpa only [sq] using abs_mul_abs_self x
 
-theorem abs_sq (x : R) : abs (x ^ 2) = x ^ 2 :=
+theorem abs_sq (x : R) : |x ^ 2| = x ^ 2 :=
 by simpa only [sq] using abs_mul_self x
 
-theorem sq_lt_sq (h : abs x < y) : x ^ 2 < y ^ 2 :=
+theorem sq_lt_sq (h : |x| < y) : x ^ 2 < y ^ 2 :=
 by simpa only [sq_abs] using pow_lt_pow_of_lt_left h (abs_nonneg x) (1:ℕ).succ_pos
 
 theorem sq_lt_sq' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 :=
 sq_lt_sq (abs_lt.mpr ⟨h1, h2⟩)
 
-theorem sq_le_sq (h : abs x ≤ abs y) : x ^ 2 ≤ y ^ 2 :=
+theorem sq_le_sq (h : |x| ≤ |y|) : x ^ 2 ≤ y ^ 2 :=
 by simpa only [sq_abs] using pow_le_pow_of_le_left (abs_nonneg x) h 2
 
 theorem sq_le_sq' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 :=
 sq_le_sq (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))
 
-theorem abs_lt_abs_of_sq_lt_sq (h : x^2 < y^2) : abs x < abs y :=
+theorem abs_lt_abs_of_sq_lt_sq (h : x^2 < y^2) : |x| < |y| :=
 lt_of_pow_lt_pow 2 (abs_nonneg y) $ by rwa [← sq_abs x, ← sq_abs y] at h
 
-theorem abs_lt_of_sq_lt_sq (h : x^2 < y^2) (hy : 0 ≤ y) : abs x < y :=
+theorem abs_lt_of_sq_lt_sq (h : x^2 < y^2) (hy : 0 ≤ y) : |x| < y :=
 begin
   rw [← abs_of_nonneg hy],
   exact abs_lt_abs_of_sq_lt_sq h,
@@ -271,10 +271,10 @@ end
 theorem abs_lt_of_sq_lt_sq' (h : x^2 < y^2) (hy : 0 ≤ y) : -y < x ∧ x < y :=
 abs_lt.mp $ abs_lt_of_sq_lt_sq h hy
 
-theorem abs_le_abs_of_sq_le_sq (h : x^2 ≤ y^2) : abs x ≤ abs y :=
+theorem abs_le_abs_of_sq_le_sq (h : x^2 ≤ y^2) : |x| ≤ |y| :=
 le_of_pow_le_pow 2 (abs_nonneg y) (1:ℕ).succ_pos $ by rwa [← sq_abs x, ← sq_abs y] at h
 
-theorem abs_le_of_sq_le_sq (h : x^2 ≤ y^2) (hy : 0 ≤ y) : abs x ≤ y :=
+theorem abs_le_of_sq_le_sq (h : x^2 ≤ y^2) (hy : 0 ≤ y) : |x| ≤ y :=
 begin
   rw [← abs_of_nonneg hy],
   exact abs_le_abs_of_sq_le_sq h,

src/algebra/ordered_field.lean

@@ -685,13 +685,13 @@ lemma max_div_div_right_of_nonpos {c : α} (hc : c ≤ 0) (a b : α) :
   max (a / c) (b / c) = (min a b) / c :=
 eq.symm $ @monotone.map_min α (order_dual α) _ _ _ _ _ (λ x y, div_le_div_of_nonpos_of_le hc)
 
-lemma abs_div (a b : α) : abs (a / b) = abs a / abs b :=
+lemma abs_div (a b : α) : |a / b| = |a| / |b| :=
 (abs_hom : monoid_with_zero_hom α α).map_div a b
 
-lemma abs_one_div (a : α) : abs (1 / a) = 1 / abs a :=
+lemma abs_one_div (a : α) : |1 / a| = 1 / |a| :=
 by rw [abs_div, abs_one]
 
-lemma abs_inv (a : α) : abs a⁻¹ = (abs a)⁻¹ :=
+lemma abs_inv (a : α) : |a⁻¹| = (|a|)⁻¹ :=
 (abs_hom : monoid_with_zero_hom α α).map_inv' a
 
 -- TODO: add lemmas with `a⁻¹`.