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
    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.

      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.instCoeTCSignType {α : Type u_1} [Zero α] [One α] [Neg α] :
          Equations
          • SignType.instCoeTCSignType = { coe := SignType.cast }
          @[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.castHom_apply {α : Type u_1} [MulZeroOneClass α] [HasDistribNeg α] :
          ∀ (a : SignType), SignType.castHom a = a

          SignType.cast as a MulWithZeroHom.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem SignType.univ_eq :
            Finset.univ = {0, -1, 1}
            def SignType.sign {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] :

            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.
            Instances For
              theorem sign_apply {α : Type u_1} [Zero α] [Preorder α] [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} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] :
              SignType.sign 0 = 0
              @[simp]
              theorem sign_pos {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] {a : α} (ha : 0 < a) :
              SignType.sign a = 1
              @[simp]
              theorem sign_neg {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] {a : α} (ha : a < 0) :
              SignType.sign a = -1
              theorem sign_eq_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] {a : α} :
              SignType.sign a = 1 0 < a
              theorem sign_eq_neg_one_iff {α : Type u_1} [Zero α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] {a : α} :
              SignType.sign a = -1 a < 0
              @[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 x x_1 => x < x_1] [Nontrivial α] :
              SignType.sign 1 = 1
              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

              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
              • One or more equations did not get rendered due to their size.
              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 x x_1 => x < x_1] [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} [AddGroup α] [Preorder α] [DecidableRel fun x x_1 => x < x_1] [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_1} [LinearOrderedAddCommGroup α] {ι : Type u_2} {s : Finset ι} {f : ια} (hs : Finset.Nonempty s) (t : SignType) (h : ∀ (i : ι), i sSignType.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} [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} [Nonempty α] [DecidableEq α] (s : Finset α) (f : α) (n : ) (h : (Finset.sum s fun i => Int.natAbs (f i)) n) :
                β x sgn g, (∀ (b : β), ¬g b ssgn 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.