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 :

The type of signs.

Instances For
    Equations
    Equations
    inductive SignType.LE :

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

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

      SignType is equivalent to Fin 3.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem SignType.nonneg_iff {a : SignType} :
        0 a a = 0 a = 1
        theorem SignType.nonpos_iff {a : SignType} :
        a 0 a = -1 a = 0
        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]
        @[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]
        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].

        Equations
        Instances For
          instance SignType.instCoeTC {α : Type u_1} [Zero α] [One α] [Neg α] :
          Equations
          • SignType.instCoeTC = { 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 → α.

          @[simp]
          theorem SignType.castHom_apply {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] :
          ∀ (a : SignType), SignType.castHom a = a

          SignType.cast as a MulWithZeroHom.

          Equations
          • SignType.castHom = { toFun := SignType.cast, map_zero' := , map_one' := , map_mul' := }
          Instances For
            theorem SignType.univ_eq :
            Finset.univ = {0, -1, 1}
            @[simp]
            theorem SignType.coe_mul {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] (a : SignType) (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_1} [Zero α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :

            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' := }
            Instances For
              theorem sign_apply {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {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 (x1 x2 : α) => x1 < x2] :
              SignType.sign 0 = 0
              @[simp]
              theorem sign_pos {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {a : α} (ha : 0 < a) :
              SignType.sign a = 1
              @[simp]
              theorem sign_neg {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {a : α} (ha : a < 0) :
              SignType.sign a = -1
              theorem sign_eq_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {a : α} :
              SignType.sign a = 1 0 < a
              theorem sign_eq_neg_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] {a : α} :
              SignType.sign a = -1 a < 0
              theorem StrictMono.sign_comp {α : Type u_1} [Zero α] [LinearOrder α] {β : Type u_2} {F : Type u_3} [Zero β] [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] [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_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 (x1 x2 : α) => x1 < x2] [Nontrivial α] :
              SignType.sign 1 = 1
              @[simp]
              theorem sign_intCast {α : Type u_2} [OrderedRing α] [Nontrivial α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (n : ) :
              SignType.sign n = SignType.sign n
              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
              @[simp]
              theorem sign_mul_self {α : Type u_1} [LinearOrderedRing α] (x : α) :
              (SignType.sign x) * x = |x|
              @[simp]
              theorem self_mul_sign {α : Type u_1} [LinearOrderedRing α] (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
              • signHom = { toFun := SignType.sign, map_zero' := , map_one' := , map_mul' := }
              Instances For
                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 (x1 x2 : α) => x1 < x2] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (a : α) :
                SignType.sign (-a) = -SignType.sign a
                theorem Right.sign_neg {α : Type u_1} [AddGroup α] [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (a : α) :
                SignType.sign (-a) = -SignType.sign a
                theorem sign_sum {α : Type u_1} [LinearOrderedAddCommGroup α] {ι : Type u_2} {s : Finset ι} {f : ια} (hs : s.Nonempty) (t : SignType) (h : is, SignType.sign (f i) = t) :
                SignType.sign (∑ is, f i) = t
                theorem Int.sign_eq_sign (n : ) :
                n.sign = (SignType.sign n)
                theorem exists_signed_sum {α : Type u_1} [DecidableEq α] (s : Finset α) (f : α) :
                ∃ (β : Type u_1) (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_1} [Nonempty α] [DecidableEq α] (s : Finset α) (f : α) (n : ) (h : is, (f i).natAbs n) :
                ∃ (β : Type u_1) (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.