Documentation

Mathlib.Algebra.Order.Group.Unbundled.Abs

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 #

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

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

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

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

      Equations
        Instances For

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

          Equations
            Instances For

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

              Equations
                Instances For

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

                  Equations
                    Instances For

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

                      Equations
                        Instances For
                          theorem mabs_le' {α : Type u_1} [Lattice α] [Group α] {a b : α} :
                          mabs 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 mabs a
                          theorem le_abs_self {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                          a |a|
                          theorem inv_le_mabs {α : Type u_1} [Lattice α] [Group α] (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) :
                          theorem abs_le_abs {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} (h₀ : a b) (h₁ : -a b) :
                          @[simp]
                          theorem mabs_inv {α : Type u_1} [Lattice α] [Group α] (a : α) :
                          @[simp]
                          theorem abs_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
                          theorem mabs_div_comm {α : Type u_1} [Lattice α] [Group α] (a b : α) :
                          mabs (a / b) = mabs (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] :
                          mabs (if p then a else b) = if p then mabs a else mabs 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α) :
                          mabs (if h : p then a h else b h) = if h : p then mabs (a h) else mabs (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) :
                          mabs 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) :
                          mabs 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) :
                          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) :
                          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) :
                          theorem abs_le_abs_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a b : α} [AddLeftMono α] (ha : 0 a) (hab : a b) :
                          @[simp]
                          theorem mabs_one {α : Type u_1} [Lattice α] [Group α] [MulLeftMono α] :
                          mabs 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 mabs 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 : α) :
                          mabs (mabs a) = mabs a
                          @[simp]
                          theorem abs_abs {α : Type u_1} [Lattice α] [AddGroup α] [AddLeftMono α] [AddRightMono α] (a : α) :
                          theorem mabs_mul_le {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) :
                          mabs (a * b) mabs a * mabs 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 : α) :
                          mabs (mabs a / mabs b) mabs (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 : α) :
                          (ab) / (ab) = mabs (b / a)
                          theorem sup_sub_inf_eq_abs_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) :
                          ab - ab = |b - a|
                          theorem sup_sq_eq_mul_mul_mabs_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) :
                          (ab) ^ 2 = a * b * mabs (b / a)
                          theorem two_nsmul_sup_eq_add_add_abs_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) :
                          2 (ab) = a + b + |b - a|
                          theorem inf_sq_eq_mul_div_mabs_div {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b : α) :
                          (ab) ^ 2 = a * b / mabs (b / a)
                          theorem two_nsmul_inf_eq_add_sub_abs_sub {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b : α) :
                          2 (ab) = a + b - |b - a|
                          theorem mabs_div_sup_mul_mabs_div_inf {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) :
                          mabs ((ac) / (bc)) * mabs ((ac) / (bc)) = mabs (a / b)
                          theorem abs_sub_sup_add_abs_sub_inf {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) :
                          |ac - bc| + |ac - bc| = |a - b|
                          theorem mabs_sup_div_sup_le_mabs {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) :
                          mabs ((ac) / (bc)) mabs (a / b)
                          theorem abs_sup_sub_sup_le_abs {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) :
                          |ac - bc| |a - b|
                          theorem mabs_inf_div_inf_le_mabs {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) :
                          mabs ((ac) / (bc)) mabs (a / b)
                          theorem abs_inf_sub_inf_le_abs {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) :
                          |ac - bc| |a - b|
                          theorem m_Birkhoff_inequalities {α : Type u_1} [Lattice α] [CommGroup α] [MulLeftMono α] (a b c : α) :
                          mabs ((ac) / (bc))mabs ((ac) / (bc)) mabs (a / b)
                          theorem Birkhoff_inequalities {α : Type u_1} [Lattice α] [AddCommGroup α] [AddLeftMono α] (a b c : α) :
                          |ac - bc||ac - bc| |a - b|
                          theorem mabs_choice {α : Type u_1} [Group α] [LinearOrder α] (x : α) :
                          mabs x = x mabs 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 mabs 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 : α} :
                          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 < mabs 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 (mabs 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 : mabs 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 : α} :
                          mabs a = mabs 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 : α} :
                          theorem even_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} :
                          theorem lt_of_mabs_lt {α : Type u_1} [Group α] [LinearOrder α] {a b : α} :
                          mabs a < ba < b
                          theorem lt_of_abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] {a b : α} :
                          |a| < ba < b
                          @[simp]
                          theorem one_lt_mabs {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} :
                          1 < mabs 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 < mabs 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 < mabs 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 : α) :
                          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 * mabs 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 : α) :
                          theorem neg_abs_le_neg {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] (a : α) :
                          theorem mabs_ne_one {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α] :
                          mabs 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 α] :
                          mabs 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 α] :
                          mabs 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) :
                          theorem abs_le_abs_of_nonpos {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α] (ha : a 0) (hab : b a) :
                          theorem mabs_lt {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α] :
                          mabs 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 : mabs 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 = mabs (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 = mabs (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|

                          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.

                          Equations
                            Instances For

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

                              Equations
                                Instances For
                                  theorem LatticeOrderedAddCommGroup.solidClosure_min {α : Type u_1} [Lattice α] [AddCommGroup α] {s t : Set α} (hst : s t) (ht : IsSolid 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|