# Documentation

Mathlib.Data.Sign

# Sign function #

This file defines the sign function for types with zero and a decidable less-than relation, and proves some basic theorems about it.

inductive SignType :

The type of signs.

Instances For
@[simp]
@[simp]
inductive SignType.LE :

The less-than-or-equal relation on signs.

Instances For

SignType is equivalent to Fin 3.

Instances For
theorem SignType.nonneg_iff {a : SignType} :
0 a a = 0 a = 1
theorem SignType.nonpos_iff {a : SignType} :
a 0 a = -1 a = 0
theorem SignType.lt_one_iff {a : SignType} :
a < 1 a 0
@[simp]
theorem SignType.neg_iff {a : SignType} :
a < 0 a = -1
@[simp]
theorem SignType.le_neg_one_iff {a : SignType} :
a -1 a = -1
@[simp]
theorem SignType.pos_iff {a : SignType} :
0 < a a = 1
@[simp]
theorem SignType.one_le_iff {a : SignType} :
1 a a = 1
@[simp]
theorem SignType.neg_one_le (a : SignType) :
-1 a
@[simp]
theorem SignType.le_one (a : SignType) :
a 1
@[simp]
@[simp]
theorem SignType.not_one_lt (a : SignType) :
¬1 < a
@[simp]
theorem SignType.self_eq_neg_iff (a : SignType) :
a = -a a = 0
@[simp]
theorem SignType.neg_eq_self_iff (a : SignType) :
-a = a a = 0
@[simp]
def SignType.cast {α : Type u_1} [Zero α] [One α] [Neg α] :
SignTypeα

Turn a SignType into zero, one, or minus one. This is a coercion instance, but note it is only a CoeTC instance: see note [use has_coe_t].

Instances For
instance SignType.instCoeTCSignType {α : Type u_1} [Zero α] [One α] [Neg α] :
@[simp]
theorem SignType.coe_zero {α : Type u_1} [Zero α] [One α] [Neg α] :
0 = 0
@[simp]
theorem SignType.coe_one {α : Type u_1} [Zero α] [One α] [Neg α] :
1 = 1
@[simp]
theorem SignType.coe_neg_one {α : Type u_1} [Zero α] [One α] [Neg α] :
↑(-1) = -1
@[simp]
theorem SignType.castHom_apply {α : Type u_1} [] [] :
∀ (a : SignType), SignType.castHom a = a
def SignType.castHom {α : Type u_1} [] [] :

SignType.cast as a MulWithZeroHom.

Instances For
theorem SignType.univ_eq :
Finset.univ = {0, -1, 1}
theorem SignType.range_eq {α : Type u_1} (f : SignTypeα) :
= {, , }
def SignType.sign {α : Type u_1} [Zero α] [] [DecidableRel fun x x_1 => x < x_1] :

The sign of an element is 1 if it's positive, -1 if negative, 0 otherwise.

Instances For
theorem sign_apply {α : Type u_1} [Zero α] [] [DecidableRel fun x x_1 => x < x_1] {a : α} :
SignType.sign a = if 0 < a then 1 else if a < 0 then -1 else 0
@[simp]
theorem sign_zero {α : Type u_1} [Zero α] [] [DecidableRel fun x x_1 => x < x_1] :
SignType.sign 0 = 0
@[simp]
theorem sign_pos {α : Type u_1} [Zero α] [] [DecidableRel fun x x_1 => x < x_1] {a : α} (ha : 0 < a) :
SignType.sign a = 1
@[simp]
theorem sign_neg {α : Type u_1} [Zero α] [] [DecidableRel fun x x_1 => x < x_1] {a : α} (ha : a < 0) :
SignType.sign a = -1
theorem sign_eq_one_iff {α : Type u_1} [Zero α] [] [DecidableRel fun x x_1 => x < x_1] {a : α} :
SignType.sign a = 1 0 < a
theorem sign_eq_neg_one_iff {α : Type u_1} [Zero α] [] [DecidableRel fun x x_1 => x < x_1] {a : α} :
SignType.sign a = -1 a < 0
@[simp]
theorem sign_eq_zero_iff {α : Type u_1} [Zero α] [] {a : α} :
SignType.sign a = 0 a = 0
theorem sign_ne_zero {α : Type u_1} [Zero α] [] {a : α} :
SignType.sign a 0 a 0
@[simp]
theorem sign_nonneg_iff {α : Type u_1} [Zero α] [] {a : α} :
0 SignType.sign a 0 a
@[simp]
theorem sign_nonpos_iff {α : Type u_1} [Zero α] [] {a : α} :
SignType.sign a 0 a 0
theorem sign_one {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] [] :
SignType.sign 1 = 1
theorem sign_mul {α : Type u_1} (x : α) (y : α) :
SignType.sign (x * y) = SignType.sign x * SignType.sign y
@[simp]
theorem sign_mul_abs {α : Type u_1} (x : α) :
↑(SignType.sign x) * |x| = x
@[simp]
theorem abs_mul_sign {α : Type u_1} (x : α) :
|x| * ↑(SignType.sign x) = x
def signHom {α : Type u_1} :

SignType.sign as a MonoidWithZeroHom for a nontrivial ordered semiring. Note that linearity is required; consider ℂ with the order z ≤ w iff they have the same imaginary part and z - w ≤ 0 in the reals; then 1 + I and 1 - I are incomparable to zero, and thus we have: 0 * 0 = SignType.sign (1 + I) * SignType.sign (1 - I) ≠ SignType.sign 2 = 1. (Complex.orderedCommRing)

Instances For
theorem sign_pow {α : Type u_1} (x : α) (n : ) :
SignType.sign (x ^ n) = SignType.sign x ^ n
theorem Left.sign_neg {α : Type u_1} [] [] [DecidableRel fun x x_1 => x < x_1] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) :
SignType.sign (-a) = -SignType.sign a
theorem Right.sign_neg {α : Type u_1} [] [] [DecidableRel fun x x_1 => x < x_1] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) :
SignType.sign (-a) = -SignType.sign a
theorem sign_sum {α : Type u_1} {ι : Type u_2} {s : } {f : ια} (hs : ) (t : SignType) (h : ∀ (i : ι), i sSignType.sign (f i) = t) :
SignType.sign (Finset.sum s fun i => f i) = t
theorem Int.sign_eq_sign (n : ) :
= ↑(SignType.sign n)
theorem exists_signed_sum {α : Type u_1} [] (s : ) (f : α) :
β x sgn g, (∀ (b : β), g b s) ( = Finset.sum s fun a => Int.natAbs (f a)) ∀ (a : α), a s(Finset.sum Finset.univ fun b => if g b = a then ↑(sgn b) else 0) = f a

We can decompose a sum of absolute value n into a sum of n signs.

theorem exists_signed_sum' {α : Type u_1} [] [] (s : ) (f : α) (n : ) (h : (Finset.sum s fun i => Int.natAbs (f i)) n) :
β x sgn g, (∀ (b : β), ¬g b ssgn b = 0) ∀ (a : α), a s(Finset.sum Finset.univ fun i => if g i = a then ↑(sgn i) else 0) = f a

We can decompose a sum of absolute value less than n into a sum of at most n signs.