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 : Type

• zero: SignType
• neg: SignType
• pos: SignType

The type of signs.

instance instDecidableEqSignType : DecidableEq SignType

instance instInhabitedSignType : Inhabited SignType

instance SignType.instFintypeSignType : Fintype SignType

instance SignType.instZeroSignType : Zero SignType

instance SignType.instOneSignType : One SignType

instance SignType.instNegSignType : Neg SignType

@[simp]

theorem SignType.zero_eq_zero : SignType.zero = 0

@[simp]

theorem SignType.neg_eq_neg_one : SignType.neg = -1

@[simp]

theorem SignType.pos_eq_one : SignType.pos = 1

instance SignType.instMulSignType : Mul SignType

inductive SignType.LE : SignType → SignType → Prop

• of_neg: ∀ (a : SignType), SignType.LE SignType.neg a
• zero: SignType.LE SignType.zero SignType.zero
• of_pos: ∀ (a : SignType), SignType.LE a SignType.pos

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

instance SignType.instLESignType : LE SignType

instance SignType.LE.decidableRel : DecidableRel SignType.LE

instance SignType.decidableEq : DecidableEq SignType

instance SignType.instCommGroupWithZeroSignType : CommGroupWithZero SignType

instance SignType.instLinearOrderSignType : LinearOrder SignType

instance SignType.instBoundedOrderSignTypeInstLESignType : BoundedOrder SignType

instance SignType.instHasDistribNegSignTypeInstMulSignType : HasDistribNeg SignType

def SignType.fin3Equiv : SignType ≃* Fin 3

SignType is equivalent to Fin 3.

theorem SignType.nonneg_iff {a : SignType} : 0 ≤ a ↔ a = 0 ∨ a = 1

theorem SignType.nonneg_iff_ne_neg_one {a : SignType} : 0 ≤ a ↔ a ≠ -1

theorem SignType.neg_one_lt_iff {a : SignType} : -1 < a ↔ 0 ≤ a

theorem SignType.nonpos_iff {a : SignType} : a ≤ 0 ↔ a = -1 ∨ a = 0

theorem SignType.nonpos_iff_ne_one {a : SignType} : a ≤ 0 ↔ a ≠ 1

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]

theorem SignType.not_lt_neg_one (a : SignType) : ¬a < -1

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

theorem SignType.neg_one_lt_one : -1 < 1

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].

instance SignType.instCoeTCSignType {α : Type u_1} [Zero α] [One α] [Neg α] : CoeTC SignType α

@[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} [MulZeroOneClass α] [HasDistribNeg α] : ∀ (a : SignType), ↑SignType.castHom a = ↑a

def SignType.castHom {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] : SignType →*₀ α

SignType.cast as a MulWithZeroHom.

theorem SignType.univ_eq : Finset.univ = {0, -1, 1}

theorem SignType.range_eq {α : Type u_1} (f : SignType → α) : Set.range f = {f SignType.zero, f SignType.neg, f SignType.pos}

def SignType.sign {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] : α →o SignType

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

theorem sign_apply {α : Type u_1} [Zero α] [Preorder α] [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 α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] : ↑SignType.sign 0 = 0

@[simp]

theorem sign_pos {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] {a : α} (ha : 0 < a) : ↑SignType.sign a = 1

@[simp]

theorem sign_neg {α : Type u_1} [Zero α] [Preorder α] [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 α] [Preorder α] [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 α] [Preorder α] [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 α] [LinearOrder α] {a : α} : ↑SignType.sign a = 0 ↔ a = 0

theorem sign_ne_zero {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : ↑SignType.sign a ≠ 0 ↔ a ≠ 0

@[simp]

theorem sign_nonneg_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : 0 ≤ ↑SignType.sign a ↔ 0 ≤ a

@[simp]

theorem sign_nonpos_iff {α : Type u_1} [Zero α] [LinearOrder α] {a : α} : ↑SignType.sign a ≤ 0 ↔ a ≤ 0

theorem sign_one {α : Type u_1} [OrderedSemiring α] [DecidableRel fun x x_1 => x < x_1] [Nontrivial α] : ↑SignType.sign 1 = 1

theorem sign_mul {α : Type u_1} [LinearOrderedRing α] (x : α) (y : α) : ↑SignType.sign (x * y) = ↑SignType.sign x * ↑SignType.sign y

@[simp]

theorem sign_mul_abs {α : Type u_1} [LinearOrderedRing α] (x : α) : ↑(↑SignType.sign x) * |x| = x

@[simp]

theorem abs_mul_sign {α : Type u_1} [LinearOrderedRing α] (x : α) : |x| * ↑(↑SignType.sign x) = x

def signHom {α : Type u_1} [LinearOrderedRing α] : α →*₀ SignType

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)

theorem sign_pow {α : Type u_1} [LinearOrderedRing α] (x : α) (n : ℕ) : ↑SignType.sign (x ^ n) = ↑SignType.sign x ^ n

theorem Left.sign_neg {α : Type u_1} [AddGroup α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [LinearOrderedAddCommGroup α] {ι : Type u_2} {s : Finset ι} {f : ι → α} (hs : Finset.Nonempty s) (t : SignType) (h : ∀ (i : ι), i ∈ s → ↑SignType.sign (f i) = t) : ↑SignType.sign (Finset.sum s fun i => f i) = t

theorem Int.sign_eq_sign (n : ℤ) : Int.sign n = ↑(↑SignType.sign n)

theorem exists_signed_sum {α : Type u_1} [DecidableEq α] (s : Finset α) (f : α → ℤ) : ∃ β x sgn g, (∀ (b : β), g b ∈ s) ∧ (Fintype.card β = 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} [Nonempty α] [DecidableEq α] (s : Finset α) (f : α → ℤ) (n : ℕ) (h : (Finset.sum s fun i => Int.natAbs (f i)) ≤ n) : ∃ β x sgn g, (∀ (b : β), ¬g b ∈ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ (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.