# 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
Equations
• = if h : x.toCtorIdx = y.toCtorIdx then else
@[simp]
@[simp]
instance SignType.instMul :
Equations
inductive SignType.LE :

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

Instances For
instance SignType.instLE :
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations

SignType is equivalent to Fin 3.

Equations
• One or more equations did not get rendered due to their size.
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].

Equations
Instances For
instance SignType.instCoeTC {α : Type u_1} [Zero α] [One α] [Neg α] :
Equations
• SignType.instCoeTC = { coe := SignType.cast }
theorem SignType.map_cast' {α : Type u_1} [Zero α] [One α] [Neg α] {β : Type u_2} [One β] [Neg β] [Zero β] (f : αβ) (h₁ : f 1 = 1) (h₂ : f 0 = 0) (h₃ : f (-1) = -1) (s : SignType) :
f s = s

Casting out of SignType respects composition with functions preserving 0, 1, -1.

theorem SignType.map_cast {α : Type u_2} {β : Type u_3} {F : Type u_4} [] [One β] [FunLike F α β] [] [OneHomClass F α β] (f : F) (s : SignType) :
f s = s

Casting out of SignType respects composition with suitable bundled homomorphism types.

@[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.coe_neg {α : Type u_2} [One α] (s : SignType) :
(-s) = -s
@[simp]
theorem SignType.intCast_cast {α : Type u_2} [] (s : SignType) :
s = s

Casting SignType → ℤ → α is the same as casting directly SignType → α.

@[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.

Equations
• SignType.castHom = { toFun := SignType.cast, map_zero' := , map_one' := , map_mul' := }
Instances For
theorem SignType.univ_eq :
Finset.univ = {0, -1, 1}
theorem SignType.range_eq {α : Type u_1} (f : SignTypeα) :
= {, , }
@[simp]
theorem SignType.coe_mul {α : Type u_1} [] [] (a : SignType) (b : SignType) :
(a * b) = a * b
@[simp]
theorem SignType.coe_pow {α : Type u_1} [] [] (a : SignType) (k : ) :
(a ^ k) = a ^ k
@[simp]
theorem SignType.coe_zpow {α : Type u_1} [] [] (a : SignType) (k : ) :
(a ^ k) = a ^ k
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.

Equations
• SignType.sign = { toFun := fun (a : α) => if 0 < a then 1 else if a < 0 then -1 else 0, monotone' := }
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
theorem StrictMono.sign_comp {α : Type u_1} [Zero α] [] {β : Type u_2} {F : Type u_3} [Zero β] [] [DecidableRel fun (x x_1 : β) => x < x_1] [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : ) (a : α) :
SignType.sign (f a) = SignType.sign a

SignType.sign respects strictly monotone zero-preserving maps.

@[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
@[simp]
theorem sign_intCast {α : Type u_2} [] [] [DecidableRel fun (x x_1 : α) => x < x_1] (n : ) :
SignType.sign n = SignType.sign n
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
@[simp]
theorem sign_mul_self {α : Type u_1} (x : α) :
(SignType.sign x) * x = |x|
@[simp]
theorem self_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)

Equations
• signHom = { toFun := SignType.sign, map_zero' := , map_one' := , map_mul' := }
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 : s.Nonempty) (t : SignType) (h : is, SignType.sign (f i) = t) :
SignType.sign (is, f i) = t
theorem Int.sign_eq_sign (n : ) :
n.sign = (SignType.sign n)
theorem exists_signed_sum {α : Type u_1} [] (s : ) (f : α) :
∃ (β : Type u_1) (x : ) (sgn : βSignType) (g : βα), (∀ (b : β), g b s) = as, (f a).natAbs as, (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 : is, (f i).natAbs n) :
∃ (β : Type u_1) (x : ) (sgn : βSignType) (g : βα), (∀ (b : β), g bssgn b = 0) as, (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.