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
    inductive SignType.Le :

    The less-than 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.
      theorem SignType.nonneg_iff {a : SignType} :
      0 a a = 0 a = 1
      theorem SignType.nonpos_iff {a : SignType} :
      a 0 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]
      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
      def SignType.cast {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :
      SignTypeα

      Turn a SignType into zero, one, or minus one. This is a coercion instance, but note it is only a has_coe_t instance: see note [use has_coe_t].

      Equations
      instance SignType.instCoeTCSignType {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :
      Equations
      • SignType.instCoeTCSignType = { coe := SignType.cast }
      @[simp]
      theorem SignType.coe_zero {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :
      0 = 0
      @[simp]
      theorem SignType.coe_one {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :
      1 = 1
      @[simp]
      theorem SignType.coe_neg_one {α : Type u_1} [inst : Zero α] [inst : One α] [inst : Neg α] :
      ↑(-1) = -1
      @[simp]
      theorem SignType.castHom_apply {α : Type u_1} [inst : MulZeroOneClass α] [inst : HasDistribNeg α] :
      ∀ (a : SignType), SignType.castHom a = a
      def SignType.castHom {α : Type u_1} [inst : MulZeroOneClass α] [inst : HasDistribNeg α] :

      SignType.cast as a MulWithZeroHom.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem SignType.univ_eq :
      Finset.univ = {0, -1, 1}
      def SignType.sign {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : 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.
      theorem sign_apply {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : 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} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] :
      SignType.sign 0 = 0
      @[simp]
      theorem sign_pos {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] {a : α} (ha : 0 < a) :
      SignType.sign a = 1
      @[simp]
      theorem sign_neg {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] {a : α} (ha : a < 0) :
      SignType.sign a = -1
      theorem sign_eq_one_iff {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] {a : α} :
      SignType.sign a = 1 0 < a
      theorem sign_eq_neg_one_iff {α : Type u_1} [inst : Zero α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] {a : α} :
      SignType.sign a = -1 a < 0
      @[simp]
      theorem sign_eq_zero_iff {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :
      SignType.sign a = 0 a = 0
      theorem sign_ne_zero {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :
      SignType.sign a 0 a 0
      @[simp]
      theorem sign_nonneg_iff {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :
      0 SignType.sign a 0 a
      @[simp]
      theorem sign_nonpos_iff {α : Type u_1} [inst : Zero α] [inst : LinearOrder α] {a : α} :
      SignType.sign a 0 a 0
      theorem sign_one {α : Type u_1} [inst : OrderedSemiring α] [inst : DecidableRel fun x x_1 => x < x_1] [inst : Nontrivial α] :
      SignType.sign 1 = 1
      theorem sign_mul {α : Type u_1} [inst : LinearOrderedRing α] (x : α) (y : α) :
      SignType.sign (x * y) = SignType.sign x * SignType.sign y
      @[simp]
      theorem sign_mul_abs {α : Type u_1} [inst : LinearOrderedRing α] (x : α) :
      ↑(SignType.sign x) * abs x = x
      @[simp]
      theorem abs_mul_sign {α : Type u_1} [inst : LinearOrderedRing α] (x : α) :
      abs x * ↑(SignType.sign x) = x
      def signHom {α : Type u_1} [inst : LinearOrderedRing α] :

      sign as a MonoidWithZeroHom for a nontrivial ordered semiring. Note that linearity is required; consider ℂ with the order z ≤ w≤ w iff they have the same imaginary part and z - w ≤ 0≤ 0 in the reals; then 1 + i and 1 - i are incomparable to zero, and thus we have: 0 * 0 = sign (1 + i) * sign (1 - i) ≠ sign 2 = 1≠ sign 2 = 1. (Complex.orderedCommRing)

      Equations
      • One or more equations did not get rendered due to their size.
      theorem sign_pow {α : Type u_1} [inst : LinearOrderedRing α] (x : α) (n : ) :
      SignType.sign (x ^ n) = SignType.sign x ^ n
      theorem Left.sign_neg {α : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] [inst : 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} [inst : AddGroup α] [inst : Preorder α] [inst : DecidableRel fun x x_1 => x < x_1] [inst : 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_2} [inst : LinearOrderedAddCommGroup α] {ι : Type u_1} {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} [inst : 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} [inst : Nonempty α] [inst : 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.