Documentation

Mathlib.Data.Sign.Basic

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

SignType.cast as a MulWithZeroHom.

Equations
Instances For
    @[simp]
    theorem SignType.castHom_apply {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] (a✝ : SignType) :
    castHom a✝ = a✝
    theorem SignType.range_eq {α : Type u_1} (f : SignTypeα) :
    @[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 : ) :
    theorem sign_mul {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x 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|

    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
    Instances For
      theorem sign_pow {α : Type u} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (x : α) (n : ) :
      theorem sign_sum {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {ι : Type u_1} {s : Finset ι} {f : ια} (hs : s.Nonempty) (t : SignType) (h : is, SignType.sign (f i) = t) :
      SignType.sign (∑ is, 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 β = 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} [Nonempty α] [DecidableEq α] (s : Finset α) (f : α) (n : ) (h : is, (f i).natAbs n) :
      ∃ (β : Type u) (x : Fintype β) (sgn : βSignType) (g : βα), (∀ (b : β), g bssgn b = 0) Fintype.card β = n 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.