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)).

Notation

• |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 mabs_pow {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (n : ℕ) (a : G) : |a ^ n|ₘ = |a|ₘ ^ n

theorem abs_nsmul {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (n : ℕ) (a : G) : |n • a| = n • |a|

theorem mabs_mul_eq_mul_mabs_iff {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b : G) : |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

theorem abs_add_eq_add_abs_iff {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem mabs_le {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} : |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b

theorem abs_le {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : |a| ≤ b ↔ -b ≤ a ∧ a ≤ b

theorem le_mabs' {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} : a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b

theorem le_abs' {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : a ≤ |b| ↔ b ≤ -a ∨ a ≤ b

theorem inv_le_of_mabs_le {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (h : |a|ₘ ≤ b) : b⁻¹ ≤ a

theorem neg_le_of_abs_le {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a| ≤ b) : -b ≤ a

theorem le_of_mabs_le {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (h : |a|ₘ ≤ b) : a ≤ b

theorem le_of_abs_le {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a| ≤ b) : a ≤ b

theorem mabs_mul' {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b : G) : |a|ₘ ≤ |b|ₘ * |b * a|ₘ

theorem abs_add' {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a| ≤ |b| + |b + a|

theorem mabs_div {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b : G) : |a / b|ₘ ≤ |a|ₘ * |b|ₘ

theorem abs_sub {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a - b| ≤ |a| + |b|

theorem mabs_div_le_iff {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} : |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c

theorem abs_sub_le_iff {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} : |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c

theorem mabs_div_lt_iff {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} : |a / b|ₘ < c ↔ a / b < c ∧ b / a < c

theorem abs_sub_lt_iff {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} : |a - b| < c ↔ a - b < c ∧ b - a < c

theorem div_le_of_mabs_div_le_left {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} (h : |a / b|ₘ ≤ c) : b / c ≤ a

theorem sub_le_of_abs_sub_le_left {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| ≤ c) : b - c ≤ a

theorem div_le_of_mabs_div_le_right {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} (h : |a / b|ₘ ≤ c) : a / c ≤ b

theorem sub_le_of_abs_sub_le_right {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| ≤ c) : a - c ≤ b

theorem div_lt_of_mabs_div_lt_left {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} (h : |a / b|ₘ < c) : b / c < a

theorem sub_lt_of_abs_sub_lt_left {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| < c) : b - c < a

theorem div_lt_of_mabs_div_lt_right {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} (h : |a / b|ₘ < c) : a / c < b

theorem sub_lt_of_abs_sub_lt_right {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (h : |a - b| < c) : a - c < b

theorem mabs_div_mabs_le_mabs_div {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b : G) : |a|ₘ / |b|ₘ ≤ |a / b|ₘ

theorem abs_sub_abs_le_abs_sub {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a| - |b| ≤ |a - b|

theorem mabs_div_mabs_le_mabs_mul {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b : G) : |a|ₘ / |b|ₘ ≤ |a * b|ₘ

theorem abs_sub_abs_le_abs_add {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : |a| - |b| ≤ |a + b|

theorem mabs_mabs_div_mabs_le_mabs_div {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b : G) : ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ

theorem abs_abs_sub_abs_le_abs_sub {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b : G) : ||a| - |b|| ≤ |a - b|

theorem mabs_div_le_of_one_le_of_le {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b n : G} (one_le_a : 1 ≤ a) (a_le_n : a ≤ n) (one_le_b : 1 ≤ b) (b_le_n : b ≤ n) : |a / b|ₘ ≤ n

|a / b|ₘ ≤ n if 1 ≤ a ≤ n and 1 ≤ b ≤ n.

theorem abs_sub_le_of_nonneg_of_le {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b n : G} (nonneg_a : 0 ≤ a) (a_le_n : a ≤ n) (nonneg_b : 0 ≤ b) (b_le_n : b ≤ n) : |a - b| ≤ n

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

theorem mabs_div_lt_of_one_le_of_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b n : G} (one_le_a : 1 ≤ a) (a_lt_n : a < n) (one_le_b : 1 ≤ b) (b_lt_n : b < n) : |a / b|ₘ < n

|a / b|ₘ < n if 1 ≤ a < n and 1 ≤ b < n.

theorem abs_sub_lt_of_nonneg_of_lt {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b n : G} (nonneg_a : 0 ≤ a) (a_lt_n : a < n) (nonneg_b : 0 ≤ b) (b_lt_n : b < n) : |a - b| < n

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

theorem mabs_eq {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (hb : 1 ≤ b) : |a|ₘ = b ↔ a = b ∨ a = b⁻¹

theorem abs_eq {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b

theorem mabs_le_max_mabs_mabs {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} (hab : a ≤ b) (hbc : b ≤ c) : |b|ₘ ≤ max |a|ₘ |c|ₘ

theorem abs_le_max_abs_abs {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max |a| |c|

theorem min_mabs_mabs_le_mabs_max {G : Type u_1} [CommGroup G] [LinearOrder G] {a b : G} : min |a|ₘ |b|ₘ ≤ |max a b|ₘ

theorem min_abs_abs_le_abs_max {G : Type u_1} [AddCommGroup G] [LinearOrder G] {a b : G} : min |a| |b| ≤ |max a b|

theorem min_mabs_mabs_le_mabs_min {G : Type u_1} [CommGroup G] [LinearOrder G] {a b : G} : min |a|ₘ |b|ₘ ≤ |min a b|ₘ

theorem min_abs_abs_le_abs_min {G : Type u_1} [AddCommGroup G] [LinearOrder G] {a b : G} : min |a| |b| ≤ |min a b|

theorem mabs_max_le_max_mabs_mabs {G : Type u_1} [CommGroup G] [LinearOrder G] {a b : G} : |max a b|ₘ ≤ max |a|ₘ |b|ₘ

theorem abs_max_le_max_abs_abs {G : Type u_1} [AddCommGroup G] [LinearOrder G] {a b : G} : |max a b| ≤ max |a| |b|

theorem mabs_min_le_max_mabs_mabs {G : Type u_1} [CommGroup G] [LinearOrder G] {a b : G} : |min a b|ₘ ≤ max |a|ₘ |b|ₘ

theorem abs_min_le_max_abs_abs {G : Type u_1} [AddCommGroup G] [LinearOrder G] {a b : G} : |min a b| ≤ max |a| |b|

theorem eq_of_mabs_div_eq_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (h : |a / b|ₘ = 1) : a = b

theorem eq_of_abs_sub_eq_zero {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a - b| = 0) : a = b

theorem mabs_div_le {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b c : G) : |a / c|ₘ ≤ |a / b|ₘ * |b / c|ₘ

theorem abs_sub_le {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b c : G) : |a - c| ≤ |a - b| + |b - c|

theorem mabs_div_le_max_div {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b c : G} (hac : a ≤ b) (hcd : b ≤ c) (d : G) : |b / d|ₘ ≤ max (c / d) (d / a)

theorem abs_sub_le_max_sub {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b c : G} (hac : a ≤ b) (hcd : b ≤ c) (d : G) : |b - d| ≤ max (c - d) (d - a)

theorem mabs_mul_three {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a b c : G) : |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ

theorem abs_add_three {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a b c : G) : |a + b + c| ≤ |a| + |b| + |c|

theorem mabs_div_le_of_le_of_le {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : |a / b|ₘ ≤ ub / lb

theorem abs_sub_le_of_le_of_le {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : |a - b| ≤ ub - lb

theorem eq_of_mabs_div_le_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (h : |a / b|ₘ ≤ 1) : a = b

theorem eq_of_abs_sub_nonpos {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (h : |a - b| ≤ 0) : a = b

theorem eq_of_mabs_div_lt_all {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {x y : G} (h : ∀ (ε : G), ε > 1 → |x / y|ₘ < ε) : x = y

theorem eq_of_abs_sub_lt_all {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {x y : G} (h : ∀ (ε : G), ε > 0 → |x - y| < ε) : x = y

theorem eq_of_mabs_div_le_all {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [DenselyOrdered G] {x y : G} (h : ∀ (ε : G), ε > 1 → |x / y|ₘ ≤ ε) : x = y

theorem eq_of_abs_sub_le_all {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [DenselyOrdered G] {x y : G} (h : ∀ (ε : G), ε > 0 → |x - y| ≤ ε) : x = y

theorem mabs_div_le_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} : |a / b|ₘ ≤ 1 ↔ a = b

theorem abs_sub_nonpos {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : |a - b| ≤ 0 ↔ a = b

theorem mabs_div_pos {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} : 1 < |a / b|ₘ ↔ a ≠ b

theorem abs_sub_pos {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} : 0 < |a - b| ↔ a ≠ b

@[simp]

theorem mabs_eq_self {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a : G} : |a|ₘ = a ↔ 1 ≤ a

@[simp]

theorem abs_eq_self {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a : G} : |a| = a ↔ 0 ≤ a

@[simp]

theorem mabs_eq_inv_self {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a : G} : |a|ₘ = a⁻¹ ↔ a ≤ 1

@[simp]

theorem abs_eq_neg_self {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a : G} : |a| = -a ↔ a ≤ 0

theorem mabs_cases {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a : G) : |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

For an element a of a multiplicative linear ordered group, either |a|ₘ = a and 1 ≤ a, or |a|ₘ = a⁻¹ and a < 1.

theorem abs_cases {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a : G) : |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

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

@[simp]

theorem max_one_mul_max_inv_one_eq_mabs_self {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (a : G) : max a 1 * max a⁻¹ 1 = |a|ₘ

@[simp]

theorem max_zero_add_max_neg_zero_eq_abs_self {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (a : G) : max a 0 + max (-a) 0 = |a|

theorem apply_abs_le_mul_of_one_le' {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [MulOneClass H] [LE H] [MulLeftMono H] [MulRightMono H] {f : G → H} {a : G} (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) : f |a| ≤ f a * f (-a)

theorem apply_abs_le_add_of_nonneg' {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [AddZeroClass H] [LE H] [AddLeftMono H] [AddRightMono H] {f : G → H} {a : G} (h₁ : 0 ≤ f a) (h₂ : 0 ≤ f (-a)) : f |a| ≤ f a + f (-a)

theorem apply_abs_le_mul_of_one_le {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [MulOneClass H] [LE H] [MulLeftMono H] [MulRightMono H] {f : G → H} (h : ∀ (x : G), 1 ≤ f x) (a : G) : f |a| ≤ f a * f (-a)

theorem apply_abs_le_add_of_nonneg {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : Type u_2} [AddZeroClass H] [LE H] [AddLeftMono H] [AddRightMono H] {f : G → H} (h : ∀ (x : G), 0 ≤ f x) (a : G) : f |a| ≤ f a + f (-a)