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
    @[simp]
    @[simp]
    inductive SignType.LE :

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

    Instances For
      Equations

        SignType is equivalent to Fin 3.

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

            Equations
              Instances For
                instance SignType.instCoeTail {α : Type u_1} [Zero α] [One α] [Neg α] :

                This is a CoeTail since the type on the right (trivially) determines the type on the left.

                outParam-wise it could be a Coe, but we don't want to try applying this instance for a coercion to any α.

                Equations
                  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 → α.

                  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
                      def SignType.sign {α : Type u} [Zero α] [Preorder α] [DecidableLT α] :

                      The sign of an element is 1 if it's positive, -1 if negative, 0 otherwise.

                      Equations
                        Instances For
                          theorem sign_apply {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} :
                          SignType.sign a = if 0 < a then 1 else if a < 0 then -1 else 0
                          @[simp]
                          theorem sign_zero {α : Type u} [Zero α] [Preorder α] [DecidableLT α] :
                          @[simp]
                          theorem sign_pos {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : 0 < a) :
                          @[simp]
                          theorem sign_neg {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} (ha : a < 0) :
                          theorem sign_eq_one_iff {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} :
                          theorem sign_eq_neg_one_iff {α : Type u} [Zero α] [Preorder α] [DecidableLT α] {a : α} :
                          SignType.sign a = -1 a < 0
                          theorem StrictMono.sign_comp {α : Type u} [Zero α] [LinearOrder α] {β : Type u_1} {F : Type u_2} [Zero β] [Preorder β] [DecidableLT β] [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : StrictMono f) (a : α) :

                          SignType.sign respects strictly monotone zero-preserving maps.

                          @[simp]
                          theorem sign_eq_zero_iff {α : Type u} [Zero α] [LinearOrder α] {a : α} :
                          theorem sign_ne_zero {α : Type u} [Zero α] [LinearOrder α] {a : α} :
                          @[simp]
                          theorem sign_nonneg_iff {α : Type u} [Zero α] [LinearOrder α] {a : α} :
                          @[simp]
                          theorem sign_nonpos_iff {α : Type u} [Zero α] [LinearOrder α] {a : α} :
                          @[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.