Absolute values in ordered groups. #

source

ink

instance Neg.toHasAbs {α : Type u_1} [inst : Neg α] [inst : Sup α] :

Abs α

abs a is the absolute value of a

Equations

Neg.toHasAbs = { abs := fun a => a ⊔ -a }

source

ink

instance Inv.toHasAbs {α : Type u_1} [inst : Inv α] [inst : Sup α] :

Abs α

abs a is the absolute value of a.

Equations

Inv.toHasAbs = { abs := fun a => a ⊔ a⁻¹ }

source

ink

theorem abs_eq_sup_neg {α : Type u_1} [inst : Neg α] [inst : Sup α] (a : α) :

abs a = a ⊔ -a

source

ink

theorem abs_eq_sup_inv {α : Type u_1} [inst : Inv α] [inst : Sup α] (a : α) :

abs a = a ⊔ a⁻¹

source

ink

theorem abs_eq_max_neg {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} :

abs a = max a (-a)

source

ink

theorem abs_choice {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] (x : α) :

abs x = x ∨ abs x = -x

source

ink

theorem abs_le' {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} :

abs a ≤ b ↔ a ≤ b ∧ -a ≤ b

source

ink

theorem le_abs {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} :

a ≤ abs b ↔ a ≤ b ∨ a ≤ -b

source

ink

theorem le_abs_self {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] (a : α) :

a ≤ abs a

source

ink

theorem neg_le_abs_self {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] (a : α) :

-a ≤ abs a

source

ink

theorem lt_abs {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} :

a < abs b ↔ a < b ∨ a < -b

source

ink

theorem abs_le_abs {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} (h₀ : a ≤ b) (h₁ : -a ≤ b) :

abs a ≤ abs b

source

ink

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

P (abs a)

source

ink

@[simp]

theorem abs_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] (a : α) :

abs (-a) = abs a

source

ink

theorem eq_or_eq_neg_of_abs_eq {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] {a : α} {b : α} (h : abs a = b) :

a = b ∨ a = -b

source

ink

theorem abs_eq_abs {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] {a : α} {b : α} :

abs a = abs b ↔ a = b ∨ a = -b

source

ink

theorem abs_sub_comm {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] (a : α) (b : α) :

abs (a - b) = abs (b - a)

source

ink

theorem abs_of_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 0 ≤ a) :

abs a = a

source

ink

theorem abs_of_pos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 0 < a) :

abs a = a

source

ink

theorem abs_of_nonpos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : a ≤ 0) :

abs a = -a

source

ink

theorem abs_of_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : a < 0) :

abs a = -a

source

ink

theorem abs_le_abs_of_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hab : a ≤ b) :

abs a ≤ abs b

source

ink

@[simp]

theorem abs_zero {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

abs 0 = 0

source

ink

@[simp]

theorem abs_pos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} :

0 < abs a ↔ a ≠ 0

source

ink

theorem abs_pos_of_pos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : 0 < a) :

0 < abs a

source

ink

theorem abs_pos_of_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} (h : a < 0) :

0 < abs a

source

ink

theorem neg_abs_le_self {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) :

-abs a ≤ a

source

ink

theorem add_abs_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) :

0 ≤ a + abs a

source

ink

theorem neg_abs_le_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) :

-abs a ≤ -a

source

ink

@[simp]

theorem abs_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) :

0 ≤ abs a

source

ink

@[simp]

theorem abs_abs {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) :

abs (abs a) = abs a

source

ink

@[simp]

theorem abs_eq_zero {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} :

abs a = 0 ↔ a = 0

source

ink

@[simp]

theorem abs_nonpos_iff {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} :

abs a ≤ 0 ↔ a = 0

source

ink

theorem abs_le_abs_of_nonpos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (ha : a ≤ 0) (hab : b ≤ a) :

abs a ≤ abs b

source

ink

theorem abs_lt {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] :

abs a < b ↔ -b < a ∧ a < b

source

ink

theorem neg_lt_of_abs_lt {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (h : abs a < b) :

-b < a

source

ink

theorem lt_of_abs_lt {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (h : abs a < b) :

a < b

source

ink

theorem max_sub_min_eq_abs' {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) :

max a b - min a b = abs (a - b)

source

ink

theorem max_sub_min_eq_abs {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) :

max a b - min a b = abs (b - a)

source

ink

theorem abs_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :

abs a ≤ b ↔ -b ≤ a ∧ a ≤ b

source

ink

theorem le_abs' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :

a ≤ abs b ↔ b ≤ -a ∨ a ≤ b

source

ink

theorem neg_le_of_abs_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs a ≤ b) :

-b ≤ a

source

ink

theorem le_of_abs_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs a ≤ b) :

a ≤ b

source

ink

theorem apply_abs_le_add_of_nonneg' {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : AddZeroClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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 (abs a) ≤ f a + f (-a)

source

ink

theorem apply_abs_le_mul_of_one_le' {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : MulOneClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : 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 (abs a) ≤ f a * f (-a)

source

ink

theorem apply_abs_le_add_of_nonneg {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : AddZeroClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : 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 (abs a) ≤ f a + f (-a)

source

ink

theorem apply_abs_le_mul_of_one_le {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : MulOneClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : 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 (abs a) ≤ f a * f (-a)

source

ink

theorem abs_add {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :

abs (a + b) ≤ abs a + abs b

The triangle inequality in LinearOrderedAddCommGroups.

source

ink

theorem abs_add' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :

abs a ≤ abs b + abs (b + a)

source

ink

theorem abs_sub {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :

abs (a - b) ≤ abs a + abs b

source

ink

theorem abs_sub_le_iff {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} :

abs (a - b) ≤ c ↔ a - b ≤ c ∧ b - a ≤ c

source

ink

theorem abs_sub_lt_iff {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} :

abs (a - b) < c ↔ a - b < c ∧ b - a < c

source

ink

theorem sub_le_of_abs_sub_le_left {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) ≤ c) :

b - c ≤ a

source

ink

theorem sub_le_of_abs_sub_le_right {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) ≤ c) :

a - c ≤ b

source

ink

theorem sub_lt_of_abs_sub_lt_left {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) < c) :

b - c < a

source

ink

theorem sub_lt_of_abs_sub_lt_right {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) < c) :

a - c < b

source

ink

theorem abs_sub_abs_le_abs_sub {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :

abs a - abs b ≤ abs (a - b)

source

ink

theorem abs_abs_sub_abs_le_abs_sub {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :

abs (abs a - abs b) ≤ abs (a - b)

source

ink

theorem abs_eq {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (hb : 0 ≤ b) :

abs a = b ↔ a = b ∨ a = -b

source

ink

theorem abs_le_max_abs_abs {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (hab : a ≤ b) (hbc : b ≤ c) :

abs b ≤ max (abs a) (abs c)

source

ink

theorem min_abs_abs_le_abs_max {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :

min (abs a) (abs b) ≤ abs (max a b)

source

ink

theorem min_abs_abs_le_abs_min {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :

min (abs a) (abs b) ≤ abs (min a b)

source

ink

theorem abs_max_le_max_abs_abs {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :

abs (max a b) ≤ max (abs a) (abs b)

source

ink

theorem abs_min_le_max_abs_abs {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :

abs (min a b) ≤ max (abs a) (abs b)

source

ink

theorem eq_of_abs_sub_eq_zero {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs (a - b) = 0) :

a = b

source

ink

theorem abs_sub_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :

abs (a - c) ≤ abs (a - b) + abs (b - c)

source

ink

theorem abs_add_three {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :

abs (a + b + c) ≤ abs a + abs b + abs c

source

ink

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

abs (a - b) ≤ ub - lb

source

ink

theorem eq_of_abs_sub_nonpos {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs (a - b) ≤ 0) :

a = b