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

def mabs {α : Type u_1} [Lattice α] [Group α] (a : α) : α

mabs a, denoted |a|ₘ, is the absolute value of a.

def abs {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : α

abs a, denoted |a|, is the absolute value of a

def «term|___|ₘ» : Lean.ParserDescr

mabs a, denoted |a|ₘ, is the absolute value of a.

def «term|___|» : Lean.ParserDescr

abs a, denoted |a|, is the absolute value of a

def mabs.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the notation |a|ₘ for mabs a. Tries to add discretionary parentheses in unparsable cases.

def abs.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the notation |a| for abs a. Tries to add discretionary parentheses in unparsable cases.

theorem mabs_le' {α : Type u_1} [Lattice α] [Group α] {a b : α} : |a|ₘ ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b

theorem abs_le' {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} : |a| ≤ b ↔ a ≤ b ∧ -a ≤ b

theorem le_mabs_self {α : Type u_1} [Lattice α] [Group α] (a : α) : a ≤ |a|ₘ

theorem le_abs_self {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : a ≤ |a|

theorem inv_le_mabs {α : Type u_1} [Lattice α] [Group α] (a : α) : a⁻¹ ≤ |a|ₘ

theorem neg_le_abs {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : -a ≤ |a|

theorem mabs_le_mabs {α : Type u_1} [Lattice α] [Group α] {a b : α} (h₀ : a ≤ b) (h₁ : a⁻¹ ≤ b) : |a|ₘ ≤ |b|ₘ

theorem abs_le_abs {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} (h₀ : a ≤ b) (h₁ : -a ≤ b) : |a| ≤ |b|

@[simp]

theorem mabs_inv {α : Type u_1} [Lattice α] [Group α] (a : α) : |a⁻¹|ₘ = |a|ₘ

@[simp]

theorem abs_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : |(-a)| = |a|

theorem mabs_div_comm {α : Type u_1} [Lattice α] [Group α] (a b : α) : |a / b|ₘ = |b / a|ₘ

theorem abs_sub_comm {α : Type u_1} [Lattice α] [AddGroup α] (a b : α) : |a - b| = |b - a|

theorem mabs_ite {α : Type u_1} [Lattice α] [Group α] {a b : α} (p : Prop) [Decidable p] : |if p then a else b|ₘ = if p then |a|ₘ else |b|ₘ

theorem abs_ite {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} (p : Prop) [Decidable p] : |if p then a else b| = if p then |a| else |b|

theorem mabs_dite {α : Type u_1} [Lattice α] [Group α] (p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) : |if h : p then a h else b h|ₘ = if h : p then |a h|ₘ else |b h|ₘ

theorem abs_dite {α : Type u_1} [Lattice α] [AddGroup α] (p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) : |if h : p then a h else b h| = if h : p then |a h| else |b h|

theorem mabs_of_one_le {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : 1 ≤ a) : |a|ₘ = a

theorem abs_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (h : 0 ≤ a) : |a| = a

theorem mabs_of_one_lt {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : 1 < a) : |a|ₘ = a

theorem abs_of_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (h : 0 < a) : |a| = a

theorem mabs_of_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : a ≤ 1) : |a|ₘ = a⁻¹

theorem abs_of_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (h : a ≤ 0) : |a| = -a

theorem mabs_of_lt_one {α : Type u_1} [Lattice α] [Group α] {a : α} [MulLeftMono α] (h : a < 1) : |a|ₘ = a⁻¹

theorem abs_of_neg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [AddLeftMono α] (h : a < 0) : |a| = -a

theorem mabs_le_mabs_of_one_le {α : Type u_1} [Lattice α] [Group α] {a b : α} [MulLeftMono α] (ha : 1 ≤ a) (hab : a ≤ b) : |a|ₘ ≤ |b|ₘ

theorem abs_le_abs_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} [AddLeftMono α] (ha : 0 ≤ a) (hab : a ≤ b) : |a| ≤ |b|

@[simp]

theorem mabs_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] : |1|ₘ = 1

@[simp]

theorem abs_zero {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] : |0| = 0

@[simp]

theorem one_le_mabs {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : 1 ≤ |a|ₘ

@[simp]

theorem abs_nonneg {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : 0 ≤ |a|

@[simp]

theorem mabs_mabs {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] [MulRightMono α] (a : α) : |(|a|ₘ)|ₘ = |a|ₘ

@[simp]

theorem abs_abs {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) : |(|a|)| = |a|

theorem mabs_mul_le {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : |a * b|ₘ ≤ |a|ₘ * |b|ₘ

The absolute value satisfies the triangle inequality.

theorem abs_add_le {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : |a + b| ≤ |a| + |b|

The absolute value satisfies the triangle inequality.

theorem mabs_mabs_div_mabs_le {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ

theorem abs_abs_sub_abs_le {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : ||a| - |b|| ≤ |a - b|

theorem sup_div_inf_eq_mabs_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : (a ⊔ b) / (a ⊓ b) = |b / a|ₘ

theorem sup_sub_inf_eq_abs_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : a ⊔ b - a ⊓ b = |b - a|

theorem sup_sq_eq_mul_mul_mabs_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : (a ⊔ b) ^ 2 = a * b * |b / a|ₘ

theorem two_nsmul_sup_eq_add_add_abs_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : 2 • (a ⊔ b) = a + b + |b - a|

theorem inf_sq_eq_mul_div_mabs_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) : (a ⊓ b) ^ 2 = a * b / |b / a|ₘ

theorem two_nsmul_inf_eq_add_sub_abs_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) : 2 • (a ⊓ b) = a + b - |b - a|

theorem mabs_div_sup_mul_mabs_div_inf {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ

theorem abs_sub_sup_add_abs_sub_inf {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) : |a ⊔ c - b ⊔ c| + |a ⊓ c - b ⊓ c| = |a - b|

theorem mabs_sup_div_sup_le_mabs {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ

theorem abs_sup_sub_sup_le_abs {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) : |a ⊔ c - b ⊔ c| ≤ |a - b|

theorem mabs_inf_div_inf_le_mabs {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) : |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

theorem abs_inf_sub_inf_le_abs {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) : |a ⊓ c - b ⊓ c| ≤ |a - b|

theorem m_Birkhoff_inequalities {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ⊔ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

theorem Birkhoff_inequalities {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) : |a ⊔ c - b ⊔ c| ⊔ |a ⊓ c - b ⊓ c| ≤ |a - b|

theorem mabs_choice {α : Type u_1} [Group α] [LinearOrder α] (x : α) : |x|ₘ = x ∨ |x|ₘ = x⁻¹

theorem abs_choice {α : Type u_1} [AddGroup α] [LinearOrder α] (x : α) : |x| = x ∨ |x| = -x

theorem le_mabs {α : Type u_1} [Group α] [LinearOrder α] {a b : α} : a ≤ |b|ₘ ↔ a ≤ b ∨ a ≤ b⁻¹

theorem le_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a b : α} : a ≤ |b| ↔ a ≤ b ∨ a ≤ -b

theorem mabs_eq_max_inv {α : Type u_1} [Group α] [LinearOrder α] {a : α} : |a|ₘ = max a a⁻¹

theorem abs_eq_max_neg {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} : |a| = max a (-a)

theorem lt_mabs {α : Type u_1} [Group α] [LinearOrder α] {a b : α} : a < |b|ₘ ↔ a < b ∨ a < b⁻¹

theorem lt_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a b : α} : a < |b| ↔ a < b ∨ a < -b

theorem mabs_by_cases {α : Type u_1} [Group α] [LinearOrder α] {a : α} (P : α → Prop) (h1 : P a) (h2 : P a⁻¹) : P |a|ₘ

theorem abs_by_cases {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} (P : α → Prop) (h1 : P a) (h2 : P (-a)) : P |a|

theorem eq_or_eq_inv_of_mabs_eq {α : Type u_1} [Group α] [LinearOrder α] {a b : α} (h : |a|ₘ = b) : a = b ∨ a = b⁻¹

theorem eq_or_eq_neg_of_abs_eq {α : Type u_1} [AddGroup α] [LinearOrder α] {a b : α} (h : |a| = b) : a = b ∨ a = -b

theorem mabs_eq_mabs {α : Type u_1} [Group α] [LinearOrder α] {a b : α} : |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹

theorem abs_eq_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a b : α} : |a| = |b| ↔ a = b ∨ a = -b

theorem isSquare_mabs {α : Type u_1} [Group α] [LinearOrder α] {a : α} : IsSquare |a|ₘ ↔ IsSquare a

theorem even_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} : Even |a| ↔ Even a

theorem lt_of_mabs_lt {α : Type u_1} [Group α] [LinearOrder α] {a b : α} : |a|ₘ < b → a < b

theorem lt_of_abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] {a b : α} : |a| < b → a < b

@[simp]

theorem map_mabs {α : Type u_1} [Group α] [LinearOrder α] {β : Type u_2} {F : Type u_3} [Group β] [LinearOrder β] [FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) (a : α) : f |a|ₘ = |f a|ₘ

@[simp]

theorem map_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {β : Type u_2} {F : Type u_3} [AddGroup β] [LinearOrder β] [FunLike F α β] [OrderHomClass F α β] [AddMonoidHomClass F α β] (f : F) (a : α) : f |a| = |f a|

@[simp]

theorem one_lt_mabs {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} : 1 < |a|ₘ ↔ a ≠ 1

@[simp]

theorem abs_pos {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} : 0 < |a| ↔ a ≠ 0

theorem one_lt_mabs_pos_of_one_lt {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} (h : 1 < a) : 1 < |a|ₘ

theorem abs_pos_of_pos {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} (h : 0 < a) : 0 < |a|

theorem one_lt_mabs_of_lt_one {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} (h : a < 1) : 1 < |a|ₘ

theorem abs_pos_of_neg {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} (h : a < 0) : 0 < |a|

theorem inv_mabs_le {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : |a|ₘ⁻¹ ≤ a

theorem neg_abs_le {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] (a : α) : -|a| ≤ a

theorem one_le_mul_mabs {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : 1 ≤ a * |a|ₘ

theorem add_abs_nonneg {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] (a : α) : 0 ≤ a + |a|

theorem inv_mabs_le_inv {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : |a|ₘ⁻¹ ≤ a⁻¹

theorem neg_abs_le_neg {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] (a : α) : -|a| ≤ -a

theorem mabs_ne_one {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] : |a|ₘ ≠ 1 ↔ a ≠ 1

theorem abs_ne_zero {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α] : |a| ≠ 0 ↔ a ≠ 0

@[simp]

theorem mabs_eq_one {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] : |a|ₘ = 1 ↔ a = 1

@[simp]

theorem abs_eq_zero {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α] : |a| = 0 ↔ a = 0

@[simp]

theorem mabs_le_one {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] : |a|ₘ ≤ 1 ↔ a = 1

@[simp]

theorem abs_nonpos_iff {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α] : |a| ≤ 0 ↔ a = 0

theorem mabs_le_mabs_of_le_one {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] (ha : a ≤ 1) (hab : b ≤ a) : |a|ₘ ≤ |b|ₘ

theorem abs_le_abs_of_nonpos {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] (ha : a ≤ 0) (hab : b ≤ a) : |a| ≤ |b|

theorem mabs_lt {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] : |a|ₘ < b ↔ b⁻¹ < a ∧ a < b

theorem abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] : |a| < b ↔ -b < a ∧ a < b

theorem inv_lt_of_mabs_lt {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] (h : |a|ₘ < b) : b⁻¹ < a

theorem neg_lt_of_abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] (h : |a| < b) : -b < a

theorem max_div_min_eq_mabs' {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] (a b : α) : max a b / min a b = |a / b|ₘ

theorem max_sub_min_eq_abs' {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] (a b : α) : max a b - min a b = |a - b|

theorem max_div_min_eq_mabs {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] (a b : α) : max a b / min a b = |b / a|ₘ

theorem max_sub_min_eq_abs {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] (a b : α) : max a b - min a b = |b - a|

def LatticeOrderedAddCommGroup.IsSolid {α : Type u_1} [Lattice α] [AddCommGroup α] (s : Set α) : Prop

A set s in a lattice ordered group is solid if for all x ∈ s and all y ∈ α such that |y| ≤ |x|, then y ∈ s.

def LatticeOrderedAddCommGroup.solidClosure {α : Type u_1} [Lattice α] [AddCommGroup α] (s : Set α) : Set α

The solid closure of a subset s is the smallest superset of s that is solid.

theorem LatticeOrderedAddCommGroup.isSolid_solidClosure {α : Type u_1} [Lattice α] [AddCommGroup α] (s : Set α) : IsSolid (solidClosure s)

theorem LatticeOrderedAddCommGroup.solidClosure_min {α : Type u_1} [Lattice α] [AddCommGroup α] {s t : Set α} (hst : s ⊆ t) (ht : IsSolid t) : solidClosure s ⊆ t

@[simp]

theorem Pi.abs_apply {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → AddGroup (α i)] [(i : ι) → Lattice (α i)] (f : (i : ι) → α i) (i : ι) : |f| i = |f i|

theorem Pi.abs_def {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → AddGroup (α i)] [(i : ι) → Lattice (α i)] (f : (i : ι) → α i) : |f| = fun (i : ι) => |f i|