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 :

zero: SignType
neg: SignType
pos: SignType

The type of signs.

Instances For

instance instDecidableEqSignType :

DecidableEq SignType

Equations

instDecidableEqSignType x y = if h : SignType.toCtorIdx x = SignType.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

instance instInhabitedSignType :

Inhabited SignType

Equations

instInhabitedSignType = { default := SignType.zero }

instance SignType.instFintypeSignType :

Fintype SignType

Equations

SignType.instFintypeSignType = Fintype.ofMultiset (↑[SignType.zero, SignType.neg, SignType.pos]) SignType.instFintypeSignType.proof_1

instance SignType.instZeroSignType :

Equations

SignType.instZeroSignType = { zero := SignType.zero }

instance SignType.instOneSignType :

Equations

SignType.instOneSignType = { one := SignType.pos }

instance SignType.instNegSignType :

Equations

SignType.instNegSignType = { neg := fun s => match s with | SignType.neg => SignType.pos | SignType.zero => SignType.zero | SignType.pos => SignType.neg }

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

Equations

SignType.instMulSignType = { mul := fun x y => match x with | SignType.neg => -y | SignType.zero => SignType.zero | SignType.pos => y }

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 relation on signs.

Instances For

instance SignType.instLESignType :

Equations

SignType.instLESignType = { 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.instCommGroupWithZeroSignType :

CommGroupWithZero SignType

Equations

SignType.instCommGroupWithZeroSignType = CommGroupWithZero.mk zpowRec SignType.instCommGroupWithZeroSignType.proof_14 SignType.instCommGroupWithZeroSignType.proof_15

instance SignType.instLinearOrderSignType :

LinearOrder SignType

Equations

SignType.instLinearOrderSignType = LinearOrder.mk SignType.instLinearOrderSignType.proof_5 SignType.Le.decidableRel SignType.decidableEq decidableLT_of_decidableLE

instance SignType.instBoundedOrderSignTypeInstLESignType :

BoundedOrder SignType

Equations

SignType.instBoundedOrderSignTypeInstLESignType = BoundedOrder.mk

instance SignType.instHasDistribNegSignTypeInstMulSignType :

HasDistribNeg SignType

Equations

SignType.instHasDistribNegSignTypeInstMulSignType = HasDistribNeg.mk SignType.instHasDistribNegSignTypeInstMulSignType.proof_2 SignType.instHasDistribNegSignTypeInstMulSignType.proof_3

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} [inst : Zero α] [inst : One α] [inst : Neg α] :

SignType → α

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

Equations

↑x = match x with | SignType.zero => 0 | SignType.pos => 1 | SignType.neg => -1

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

CoeTC SignType α

Equations

SignType.instCoeTCSignType = { coe := SignType.cast }

@[simp]

theorem SignType.coe_zero {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :

↑0 = 0

@[simp]

theorem SignType.coe_one {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :

↑1 = 1

@[simp]

theorem SignType.coe_neg_one {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :

↑(-1) = -1

@[simp]

theorem SignType.castHom_apply {α : Type u_1} [inst : MulZeroOneClass α] [inst : HasDistribNeg α] :

∀ (a : SignType), ↑SignType.castHom a = ↑a

def SignType.castHom {α : Type u_1} [inst : MulZeroOneClass α] [inst : HasDistribNeg α] :

SignType →*₀ α

SignType.cast as a MulWithZeroHom.

Equations

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

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} [inst : Zero α] [inst : Preorder α] [inst : 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.

Equations

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

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

↑SignType.sign 0 = 0

@[simp]

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

↑SignType.sign a = 1

@[simp]

theorem sign_neg {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] {a : α} (ha : a < 0) :

↑SignType.sign a = -1

theorem sign_eq_one_iff {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] {a : α} :

↑SignType.sign a = 1 ↔ 0 < a

theorem sign_eq_neg_one_iff {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] {a : α} :

↑SignType.sign a = -1 ↔ a < 0

@[simp]

theorem sign_eq_zero_iff {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :

↑SignType.sign a = 0 ↔ a = 0

theorem sign_ne_zero {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :

↑SignType.sign a ≠ 0 ↔ a ≠ 0

@[simp]

theorem sign_nonneg_iff {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :

0 ≤ ↑SignType.sign a ↔ 0 ≤ a

@[simp]

theorem sign_nonpos_iff {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :

↑SignType.sign a ≤ 0 ↔ a ≤ 0

theorem sign_one {α : Type u_1} [inst : OrderedSemiring α] [inst : DecidableRel fun x x_1 => x < x_1] [inst : Nontrivial α] :

↑SignType.sign 1 = 1

theorem sign_mul {α : Type u_1} [inst : LinearOrderedRing α] (x : α) (y : α) :

↑SignType.sign (x * y) = ↑SignType.sign x * ↑SignType.sign y

@[simp]

theorem sign_mul_abs {α : Type u_1} [inst : LinearOrderedRing α] (x : α) :

↑(↑SignType.sign x) * abs x = x

@[simp]

theorem abs_mul_sign {α : Type u_1} [inst : LinearOrderedRing α] (x : α) :

abs x * ↑(↑SignType.sign x) = x

def signHom {α : Type u_1} [inst : LinearOrderedRing α] :

α →*₀ SignType

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

Equations

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

theorem sign_pow {α : Type u_1} [inst : LinearOrderedRing α] (x : α) (n : ℕ) :

↑SignType.sign (x ^ n) = ↑SignType.sign x ^ n

theorem Left.sign_neg {α : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] [inst : 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} [inst : AddGroup α] [inst : Preorder α] [inst : DecidableRel 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 : α) :

↑SignType.sign (-a) = -↑SignType.sign a

theorem sign_sum {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {ι : Type u_1} {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} [inst : 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} [inst : Nonempty α] [inst : 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.