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.

@[simp]

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

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

theorem SignType.pow_odd (s : SignType) {n : ℕ} (hn : Odd n) : s ^ n = s

theorem SignType.zpow_odd (s : SignType) {z : ℤ} (hz : Odd z) : s ^ z = s

theorem SignType.pow_even (s : SignType) {n : ℕ} (hn : Even n) (hs : s ≠ 0) : s ^ n = 1

theorem SignType.zpow_even (s : SignType) {z : ℤ} (hz : Even z) (hs : s ≠ 0) : s ^ z = 1

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

SignType.cast as a MulWithZeroHom.

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

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

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

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

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.