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 mabs_pow {G : Type u_1} [LinearOrderedCommGroup G] (n : ℕ) (a : G) : mabs (a ^ n) = mabs a ^ n

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

theorem mabs_mul_eq_mul_mabs_iff {G : Type u_1} [LinearOrderedCommGroup G] (a b : G) : mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

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

theorem mabs_le {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : mabs a ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b

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

theorem le_mabs' {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : a ≤ mabs b ↔ b ≤ a⁻¹ ∨ a ≤ b

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

theorem inv_le_of_mabs_le {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} (h : mabs a ≤ b) : b⁻¹ ≤ a

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

theorem le_of_mabs_le {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} (h : mabs a ≤ b) : a ≤ b

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

theorem mabs_mul {G : Type u_1} [LinearOrderedCommGroup G] (a b : G) : mabs (a * b) ≤ mabs a * mabs b

The triangle inequality in LinearOrderedCommGroups.

theorem abs_add {G : Type u_1} [LinearOrderedAddCommGroup G] (a b : G) : |a + b| ≤ |a| + |b|

The triangle inequality in LinearOrderedAddCommGroups.

theorem mabs_mul' {G : Type u_1} [LinearOrderedCommGroup G] (a b : G) : mabs a ≤ mabs b * mabs (b * a)

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

theorem mabs_div {G : Type u_1} [LinearOrderedCommGroup G] (a b : G) : mabs (a / b) ≤ mabs a * mabs b

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

theorem mabs_div_le_iff {G : Type u_1} [LinearOrderedCommGroup G] {a b c : G} : mabs (a / b) ≤ c ↔ a / b ≤ c ∧ b / a ≤ c

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

theorem mabs_div_lt_iff {G : Type u_1} [LinearOrderedCommGroup G] {a b c : G} : mabs (a / b) < c ↔ a / b < c ∧ b / a < c

theorem abs_sub_lt_iff {G : Type u_1} [LinearOrderedAddCommGroup 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} [LinearOrderedCommGroup G] {a b c : G} (h : mabs (a / b) ≤ c) : b / c ≤ a

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

theorem div_le_of_mabs_div_le_right {G : Type u_1} [LinearOrderedCommGroup G] {a b c : G} (h : mabs (a / b) ≤ c) : a / c ≤ b

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

theorem div_lt_of_mabs_div_lt_left {G : Type u_1} [LinearOrderedCommGroup G] {a b c : G} (h : mabs (a / b) < c) : b / c < a

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

theorem div_lt_of_mabs_div_lt_right {G : Type u_1} [LinearOrderedCommGroup G] {a b c : G} (h : mabs (a / b) < c) : a / c < b

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

theorem mabs_div_mabs_le_mabs_div {G : Type u_1} [LinearOrderedCommGroup G] (a b : G) : mabs a / mabs b ≤ mabs (a / b)

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

theorem mabs_mabs_div_mabs_le_mabs_div {G : Type u_1} [LinearOrderedCommGroup G] (a b : G) : mabs (mabs a / mabs b) ≤ mabs (a / b)

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

theorem mabs_div_le_of_one_le_of_le {G : Type u_1} [LinearOrderedCommGroup 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) : mabs (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} [LinearOrderedAddCommGroup G] {a b n : G} (one_le_a : 0 ≤ a) (a_le_n : a ≤ n) (one_le_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} [LinearOrderedCommGroup 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) : mabs (a / b) < n

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

theorem abs_sub_lt_of_nonneg_of_lt {G : Type u_1} [LinearOrderedAddCommGroup G] {a b n : G} (one_le_a : 0 ≤ a) (a_lt_n : a < n) (one_le_b : 0 ≤ b) (b_lt_n : b < n) : |a - b| < n

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

theorem mabs_eq {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} (hb : 1 ≤ b) : mabs a = b ↔ a = b ∨ a = b⁻¹

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

theorem mabs_le_max_mabs_mabs {G : Type u_1} [LinearOrderedCommGroup G] {a b c : G} (hab : a ≤ b) (hbc : b ≤ c) : mabs b ≤ mabs a ⊔ mabs c

theorem abs_le_max_abs_abs {G : Type u_1} [LinearOrderedAddCommGroup G] {a b c : G} (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ |a| ⊔ |c|

theorem min_mabs_mabs_le_mabs_max {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : mabs a ⊓ mabs b ≤ mabs (a ⊔ b)

theorem min_abs_abs_le_abs_max {G : Type u_1} [LinearOrderedAddCommGroup G] {a b : G} : |a| ⊓ |b| ≤ |a ⊔ b|

theorem min_mabs_mabs_le_mabs_min {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : mabs a ⊓ mabs b ≤ mabs (a ⊓ b)

theorem min_abs_abs_le_abs_min {G : Type u_1} [LinearOrderedAddCommGroup G] {a b : G} : |a| ⊓ |b| ≤ |a ⊓ b|

theorem mabs_max_le_max_mabs_mabs {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : mabs (a ⊔ b) ≤ mabs a ⊔ mabs b

theorem abs_max_le_max_abs_abs {G : Type u_1} [LinearOrderedAddCommGroup G] {a b : G} : |a ⊔ b| ≤ |a| ⊔ |b|

theorem mabs_min_le_max_mabs_mabs {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : mabs (a ⊓ b) ≤ mabs a ⊔ mabs b

theorem abs_min_le_max_abs_abs {G : Type u_1} [LinearOrderedAddCommGroup G] {a b : G} : |a ⊓ b| ≤ |a| ⊔ |b|

theorem eq_of_mabs_div_eq_one {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} (h : mabs (a / b) = 1) : a = b

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

theorem mabs_div_le {G : Type u_1} [LinearOrderedCommGroup G] (a b c : G) : mabs (a / c) ≤ mabs (a / b) * mabs (b / c)

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

theorem mabs_mul_three {G : Type u_1} [LinearOrderedCommGroup G] (a b c : G) : mabs (a * b * c) ≤ mabs a * mabs b * mabs c

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

theorem mabs_div_le_of_le_of_le {G : Type u_1} [LinearOrderedCommGroup G] {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : mabs (a / b) ≤ ub / lb

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

@[deprecated abs_sub_le_of_le_of_le (since := "2025-03-02")]

theorem dist_bdd_within_interval {G : Type u_1} [LinearOrderedAddCommGroup G] {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : |a - b| ≤ ub - lb

Alias of abs_sub_le_of_le_of_le.

theorem eq_of_mabs_div_le_one {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} (h : mabs (a / b) ≤ 1) : a = b

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

theorem eq_of_mabs_div_lt_all {G : Type u_1} [LinearOrderedCommGroup G] {x y : G} (h : ∀ (ε : G), ε > 1 → mabs (x / y) < ε) : x = y

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

theorem eq_of_mabs_div_le_all {G : Type u_1} [LinearOrderedCommGroup G] [DenselyOrdered G] {x y : G} (h : ∀ (ε : G), ε > 1 → mabs (x / y) ≤ ε) : x = y

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

theorem mabs_div_le_one {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : mabs (a / b) ≤ 1 ↔ a = b

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

theorem mabs_div_pos {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} : 1 < mabs (a / b) ↔ a ≠ b

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

@[simp]

theorem mabs_eq_self {G : Type u_1} [LinearOrderedCommGroup G] {a : G} : mabs a = a ↔ 1 ≤ a

@[simp]

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

@[simp]

theorem mabs_eq_inv_self {G : Type u_1} [LinearOrderedCommGroup G] {a : G} : mabs a = a⁻¹ ↔ a ≤ 1

@[simp]

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

theorem mabs_cases {G : Type u_1} [LinearOrderedCommGroup G] (a : G) : mabs a = a ∧ 1 ≤ a ∨ mabs 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} [LinearOrderedAddCommGroup 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} [LinearOrderedCommGroup G] (a : G) : (a ⊔ 1) * (a⁻¹ ⊔ 1) = mabs a

@[simp]

theorem max_zero_add_max_neg_zero_eq_abs_self {G : Type u_1} [LinearOrderedAddCommGroup G] (a : G) : a ⊔ 0 + -a ⊔ 0 = |a|

theorem apply_abs_le_mul_of_one_le' {G : Type u_1} [LinearOrderedAddCommGroup 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} [LinearOrderedAddCommGroup 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} [LinearOrderedAddCommGroup 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} [LinearOrderedAddCommGroup 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)