# Absolute values in ordered groups #

The absolute value of an element in a group which is also a lattice is its supremum with its negation. This generalizes the usual absolute value on real numbers (|x| = max x (-x)).

## Notations #

• |a|: The absolute value of an element a of an additive lattice ordered group
• |a|ₘ: The absolute value of an element a of a multiplicative lattice ordered group
theorem abs_nsmul {α : Type u_1} (n : ) (a : α) :
|n a| = n |a|
theorem mabs_pow {α : Type u_1} (n : ) (a : α) :
mabs (a ^ n) = mabs a ^ n
theorem abs_add_eq_add_abs_iff {α : Type u_1} (a : α) (b : α) :
|a + b| = |a| + |b| 0 a 0 b a 0 b 0
theorem mabs_mul_eq_mul_mabs_iff {α : Type u_1} (a : α) (b : α) :
mabs (a * b) = mabs a * mabs b 1 a 1 b a 1 b 1
theorem abs_le {α : Type u_1} {a : α} {b : α} :
|a| b -b a a b
theorem le_abs' {α : Type u_1} {a : α} {b : α} :
a |b| b -a a b
theorem neg_le_of_abs_le {α : Type u_1} {a : α} {b : α} (h : |a| b) :
-b a
theorem le_of_abs_le {α : Type u_1} {a : α} {b : α} (h : |a| b) :
a b
theorem apply_abs_le_add_of_nonneg' {α : Type u_1} {β : Type u_2} [] [] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] [CovariantClass β β (Function.swap fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] {f : αβ} {a : α} (h₁ : 0 f a) (h₂ : 0 f (-a)) :
f |a| f a + f (-a)
theorem apply_abs_le_mul_of_one_le' {α : Type u_1} {β : Type u_2} [] [] [CovariantClass β β (fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x x_1] [CovariantClass β β (Function.swap fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x x_1] {f : αβ} {a : α} (h₁ : 1 f a) (h₂ : 1 f (-a)) :
f |a| f a * f (-a)
theorem apply_abs_le_add_of_nonneg {α : Type u_1} {β : Type u_2} [] [] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] [CovariantClass β β (Function.swap fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x x_1] {f : αβ} (h : ∀ (x : α), 0 f x) (a : α) :
f |a| f a + f (-a)
theorem apply_abs_le_mul_of_one_le {α : Type u_1} {β : Type u_2} [] [] [CovariantClass β β (fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x x_1] [CovariantClass β β (Function.swap fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x x_1] {f : αβ} (h : ∀ (x : α), 1 f x) (a : α) :
f |a| f a * f (-a)
theorem abs_add {α : Type u_1} (a : α) (b : α) :
|a + b| |a| + |b|

The triangle inequality in LinearOrderedAddCommGroups.

theorem abs_add' {α : Type u_1} (a : α) (b : α) :
|a| |b| + |b + a|
theorem abs_sub {α : Type u_1} (a : α) (b : α) :
|a - b| |a| + |b|
theorem abs_sub_le_iff {α : Type u_1} {a : α} {b : α} {c : α} :
|a - b| c a - b c b - a c
theorem abs_sub_lt_iff {α : Type u_1} {a : α} {b : α} {c : α} :
|a - b| < c a - b < c b - a < c
theorem sub_le_of_abs_sub_le_left {α : Type u_1} {a : α} {b : α} {c : α} (h : |a - b| c) :
b - c a
theorem sub_le_of_abs_sub_le_right {α : Type u_1} {a : α} {b : α} {c : α} (h : |a - b| c) :
a - c b
theorem sub_lt_of_abs_sub_lt_left {α : Type u_1} {a : α} {b : α} {c : α} (h : |a - b| < c) :
b - c < a
theorem sub_lt_of_abs_sub_lt_right {α : Type u_1} {a : α} {b : α} {c : α} (h : |a - b| < c) :
a - c < b
theorem abs_sub_abs_le_abs_sub {α : Type u_1} (a : α) (b : α) :
|a| - |b| |a - b|
theorem abs_abs_sub_abs_le_abs_sub {α : Type u_1} (a : α) (b : α) :
||a| - |b|| |a - b|
theorem abs_sub_le_of_nonneg_of_le {α : Type u_1} {a : α} {b : α} {n : α} (a_nonneg : 0 a) (a_le_n : a n) (b_nonneg : 0 b) (b_le_n : b n) :
|a - b| n

|a - b| ≤ n if 0 ≤ a ≤ n and 0 ≤ b ≤ n.

theorem abs_sub_lt_of_nonneg_of_lt {α : Type u_1} {a : α} {b : α} {n : α} (a_nonneg : 0 a) (a_lt_n : a < n) (b_nonneg : 0 b) (b_lt_n : b < n) :
|a - b| < n

|a - b| < n if 0 ≤ a < n and 0 ≤ b < n.

theorem abs_eq {α : Type u_1} {a : α} {b : α} (hb : 0 b) :
|a| = b a = b a = -b
theorem abs_le_max_abs_abs {α : Type u_1} {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
|b| max |a| |c|
theorem min_abs_abs_le_abs_max {α : Type u_1} {a : α} {b : α} :
min |a| |b| |max a b|
theorem min_abs_abs_le_abs_min {α : Type u_1} {a : α} {b : α} :
min |a| |b| |min a b|
theorem abs_max_le_max_abs_abs {α : Type u_1} {a : α} {b : α} :
|max a b| max |a| |b|
theorem abs_min_le_max_abs_abs {α : Type u_1} {a : α} {b : α} :
|min a b| max |a| |b|
theorem eq_of_abs_sub_eq_zero {α : Type u_1} {a : α} {b : α} (h : |a - b| = 0) :
a = b
theorem abs_sub_le {α : Type u_1} (a : α) (b : α) (c : α) :
|a - c| |a - b| + |b - c|
theorem abs_add_three {α : Type u_1} (a : α) (b : α) (c : α) :
|a + b + c| |a| + |b| + |c|
theorem dist_bdd_within_interval {α : Type u_1} {a : α} {b : α} {lb : α} {ub : α} (hal : lb a) (hau : a ub) (hbl : lb b) (hbu : b ub) :
|a - b| ub - lb
theorem eq_of_abs_sub_nonpos {α : Type u_1} {a : α} {b : α} (h : |a - b| 0) :
a = b
theorem abs_sub_nonpos {α : Type u_1} {a : α} {b : α} :
|a - b| 0 a = b
theorem abs_sub_pos {α : Type u_1} {a : α} {b : α} :
0 < |a - b| a b
@[simp]
theorem abs_eq_self {α : Type u_1} {a : α} :
|a| = a 0 a
@[simp]
theorem abs_eq_neg_self {α : Type u_1} {a : α} :
|a| = -a a 0
theorem abs_cases {α : Type u_1} (a : α) :
|a| = a 0 a |a| = -a a < 0

For an element a of a linear ordered ring, either abs a = a and 0 ≤ a, or abs a = -a and a < 0. Use cases on this lemma to automate linarith in inequalities

@[simp]
theorem max_zero_add_max_neg_zero_eq_abs_self {α : Type u_1} (a : α) :
max a 0 + max (-a) 0 = |a|