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

The type of signs.

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

instance instDecidableEqSignType : DecidableEq SignType

Equations

• instDecidableEqSignType x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance instInhabitedSignType : Inhabited SignType

Equations

• instInhabitedSignType = { default := SignType.zero }

instance instFintypeSignType : Fintype SignType

Equations

• instFintypeSignType = { elems := { val := ↑SignType.enumList, nodup := SignType.enumList_nodup }, complete := instFintypeSignType._proof_3 }

instance SignType.instZero : Zero SignType

Equations

• SignType.instZero = { zero := SignType.zero }

instance SignType.instOne : One SignType

Equations

• SignType.instOne = { one := SignType.pos }

instance SignType.instNeg : Neg SignType

Equations

• SignType.instNeg = { neg := fun (s : SignType) => match s with | SignType.neg => SignType.pos | SignType.zero => SignType.zero | SignType.pos => SignType.neg }

@[simp]

theorem SignType.zero_eq_zero : zero = 0

@[simp]

theorem SignType.neg_eq_neg_one : neg = -1

@[simp]

theorem SignType.pos_eq_one : pos = 1

instance SignType.instMul : Mul SignType

Equations

• SignType.instMul = { mul := fun (x y : SignType) => match x with | SignType.neg => -y | SignType.zero => SignType.zero | SignType.pos => y }

inductive SignType.LE : SignType → SignType → Prop

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

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

instance SignType.instLE : LE SignType

Equations

• SignType.instLE = { le := SignType.LE }

instance SignType.LE.decidableRel : DecidableRel SignType.LE

Equations

• One or more equations did not get rendered due to their size.

instance SignType.decidableEq : DecidableEq SignType

Equations

• One or more equations did not get rendered due to their size.

instance SignType.instCommGroupWithZero : CommGroupWithZero SignType

Equations

• One or more equations did not get rendered due to their size.

instance SignType.instLinearOrder : LinearOrder SignType

Equations

• One or more equations did not get rendered due to their size.

instance SignType.instBoundedOrder : BoundedOrder SignType

Equations

• SignType.instBoundedOrder = { top := 1, le_top := SignType.LE.of_pos, bot := -1, bot_le := SignType.LE.of_neg }

instance SignType.instHasDistribNeg : HasDistribNeg SignType

Equations

• One or more equations did not get rendered due to their size.

def SignType.fin3Equiv : SignType ≃* Fin 3

SignType is equivalent to Fin 3.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• ↑SignType.zero = 0
• ↑SignType.pos = 1
• ↑SignType.neg = -1

instance SignType.instCoeTail {α : Type u_1} [Zero α] [One α] [Neg α] : CoeTail SignType α

This is a CoeTail since the type on the right (trivially) determines the type on the left.

outParam-wise it could be a Coe, but we don't want to try applying this instance for a coercion to any α.

Equations

• SignType.instCoeTail = { 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} [AddGroupWithOne α] [One β] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass 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 α] [SubtractionMonoid α] (s : SignType) : ↑(-s) = -↑s

@[simp]

theorem SignType.intCast_cast {α : Type u_2} [AddGroupWithOne α] (s : SignType) : ↑↑s = ↑s

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

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

SignType.cast as a MulWithZeroHom.

Equations

• SignType.castHom = { toFun := SignType.cast, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SignType.castHom_apply {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] (a✝ : SignType) : castHom a✝ = ↑a✝

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

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

@[simp]

theorem SignType.coe_mul {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] (a b : SignType) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem SignType.coe_pow {α : Type u_1} [MonoidWithZero α] [HasDistribNeg α] (a : SignType) (k : ℕ) : ↑(a ^ k) = ↑a ^ k

@[simp]

theorem SignType.coe_zpow {α : Type u_1} [GroupWithZero α] [HasDistribNeg α] (a : SignType) (k : ℤ) : ↑(a ^ k) = ↑a ^ k

def SignType.sign {α : Type u} [Zero α] [Preorder α] [DecidableLT α] : α →o SignType

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' := ⋯ }

theorem sign_apply {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = if 0 < a then 1 else if a < 0 then -1 else 0

@[simp]

theorem sign_zero {α : Type u} [Zero α] [Preorder α] [DecidableLT α] : SignType.sign 0 = 0

@[simp]

theorem sign_pos {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : 0 < a) : SignType.sign a = 1

@[simp]

theorem sign_neg {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : a < 0) : SignType.sign a = -1

theorem sign_eq_one_iff {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = 1 ↔ 0 < a

theorem sign_eq_neg_one_iff {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} : SignType.sign a = -1 ↔ a < 0

theorem StrictMono.sign_comp {α : Type u} [Zero α] [LinearOrder α] {β : Type u_1} {F : Type u_2} [Zero β] [Preorder β] [DecidableLT β] [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : StrictMono ⇑f) (a : α) : SignType.sign (f a) = SignType.sign a

SignType.sign respects strictly monotone zero-preserving maps.

@[simp]

theorem sign_eq_zero_iff {α : Type u} [Zero α] [LinearOrder α] {a : α} : SignType.sign a = 0 ↔ a = 0

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

@[simp]

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

@[simp]

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

theorem sign_one {α : Type u} [Semiring α] [PartialOrder α] [IsOrderedRing α] [DecidableLT α] [Nontrivial α] : SignType.sign 1 = 1

@[simp]

theorem sign_intCast {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] [DecidableLT α] (n : ℤ) : SignType.sign ↑n = SignType.sign n

theorem sign_mul {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x y : α) : SignType.sign (x * y) = SignType.sign x * SignType.sign y

@[simp]

theorem sign_mul_abs {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : ↑(SignType.sign x) * |x| = x

@[simp]

theorem abs_mul_sign {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : |x| * ↑(SignType.sign x) = x

@[simp]

theorem sign_mul_self {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : ↑(SignType.sign x) * x = |x|

@[simp]

theorem self_mul_sign {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) : x * ↑(SignType.sign x) = |x|

def signHom {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] : α →*₀ 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)

Equations

• signHom = { toFun := ⇑SignType.sign, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem sign_pow {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) (n : ℕ) : SignType.sign (x ^ n) = SignType.sign x ^ n

theorem Left.sign_neg {α : Type u} [AddGroup α] [Preorder α] [DecidableLT α] [AddLeftStrictMono α] (a : α) : SignType.sign (-a) = -SignType.sign a

theorem Right.sign_neg {α : Type u} [AddGroup α] [Preorder α] [DecidableLT α] [AddRightStrictMono α] (a : α) : SignType.sign (-a) = -SignType.sign a

theorem sign_sum {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {ι : Type u_1} {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (t : SignType) (h : ∀ i ∈ s, SignType.sign (f i) = t) : SignType.sign (∑ i ∈ s, f i) = t

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

In this section we explicitly handle universe variables, because Lean creates a fresh universe variable for the type whose existence is asserted. But we want the type to live in the same universe as the input type.

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