Mathlib.Data.Sign

SignType inductive

Full source

/-- The type of signs. -/
inductive SignType
  | zero
  | neg
  | pos
  deriving DecidableEq, Inhabited, Fintype

Type of signs (negative/zero/positive)

Informal description

The inductive type `SignType` represents the possible signs of a value in a type with zero and a decidable order relation. It consists of three constructors: `neg` (negative), `zero` (zero), and `pos` (positive).

instDecidableEqSignType instance

: DecidableEq✝ SignType

Full source

DecidableEq, Inhabited, Fintype

Decidable Equality for SignType

Informal description

The type `SignType` has decidable equality, meaning that for any two elements `s₁` and `s₂` in `SignType`, it is possible to determine whether `s₁ = s₂` holds.

instInhabitedSignType instance

: Inhabited✝ (@SignType)

Full source

Inhabited, Fintype

Inhabitedness of SignType

Informal description

The type `SignType` is inhabited, meaning it contains at least one element. Specifically, it has constructors for negative (`neg`), zero (`zero`), and positive (`pos`) values.

instFintypeSignType instance

: Fintype✝ SignType

Full source

Fintype

Finiteness of the Sign Type

Informal description

The type `SignType` representing signs (negative, zero, positive) is finite.

SignType.instZero instance

: Zero SignType

Full source

instance : Zero SignType :=
  ⟨zero⟩

Zero Element in SignType

Informal description

The type `SignType` has a zero element, corresponding to the `zero` constructor.

SignType.instOne instance

: One SignType

Full source

instance : One SignType :=
  ⟨pos⟩

Multiplicative Identity in SignType

Informal description

The type `SignType` representing signs (negative, zero, positive) has a multiplicative identity element, corresponding to the `pos` constructor.

SignType.instNeg instance

: Neg SignType

Full source

instance : Neg SignType :=
  ⟨fun s =>
    match s with
    | neg => pos
    | zero => zero
    | pos => neg⟩

Negation Operation on SignType

Informal description

The type `SignType` representing signs (negative, zero, positive) has a negation operation defined by `neg = -1`.

SignType.zero_eq_zero theorem

: zero = 0

Full source

@[simp]
theorem zero_eq_zero : zero = 0 :=
  rfl

Zero Constructor Equals Zero in SignType

Informal description

The zero constructor of the `SignType` type is equal to the zero element, i.e., $\text{zero} = 0$.

SignType.neg_eq_neg_one theorem

: neg = -1

Full source

@[simp]
theorem neg_eq_neg_one : neg = -1 :=
  rfl

Negative Sign Equals Negative One in SignType

Informal description

The negative sign constructor `neg` in the `SignType` type is equal to the negative of the multiplicative identity element, i.e., $\text{neg} = -1$.

SignType.pos_eq_one theorem

: pos = 1

Full source

@[simp]
theorem pos_eq_one : pos = 1 :=
  rfl

Positive Sign Equals One in SignType

Informal description

The positive sign constructor `pos` in the `SignType` type is equal to the multiplicative identity element `1`.

SignType.instMul instance

: Mul SignType

Full source

instance : Mul SignType :=
  ⟨fun x y =>
    match x with
    | neg => -y
    | zero => zero
    | pos => y⟩

Multiplication Operation on SignType

Informal description

The type `SignType` representing signs (negative, zero, positive) is equipped with a multiplication operation.

SignType.LE inductive

: SignType → SignType → Prop

Full source

/-- The less-than-or-equal relation on signs. -/
protected inductive LE : SignType → SignType → Prop
  | of_neg (a) : SignType.LE neg a
  | zero : SignType.LE zero zero
  | of_pos (a) : SignType.LE a pos

Less-than-or-equal relation on signs

Informal description

The less-than-or-equal relation on signs, where `SignType` is an inductive type with three constructors: `neg` (negative), `zero` (zero), and `pos` (positive). This relation defines an ordering between these sign values.

SignType.instLE instance

: LE SignType

Full source

instance : LE SignType :=
  ⟨SignType.LE⟩

The Less-Than-or-Equal Relation on Signs

Informal description

The type `SignType` of signs (negative, zero, positive) is equipped with a canonical less-than-or-equal relation.

SignType.LE.decidableRel instance

: DecidableRel SignType.LE

Full source

instance LE.decidableRel : DecidableRel SignType.LE := fun a b => by
  cases a <;> cases b <;> first | exact isTrue (by constructor)| exact isFalse (by rintro ⟨_⟩)

Decidability of the Order on Signs

Informal description

The less-than-or-equal relation on the type of signs (negative, zero, positive) is decidable.

SignType.decidableEq instance

: DecidableEq SignType

Full source

instance decidableEq : DecidableEq SignType := fun a b => by
  cases a <;> cases b <;> first | exact isTrue (by constructor)| exact isFalse (by rintro ⟨_⟩)

Decidable Equality for Sign Types

Informal description

The type of signs (negative, zero, positive) has decidable equality.

SignType.instCommGroupWithZero instance

: CommGroupWithZero SignType

Full source

instance : CommGroupWithZero SignType where
  zero := 0
  one := 1
  mul := (· * ·)
  inv := id
  mul_zero a := by cases a <;> rfl
  zero_mul a := by cases a <;> rfl
  mul_one a := by cases a <;> rfl
  one_mul a := by cases a <;> rfl
  mul_inv_cancel a ha := by cases a <;> trivial
  mul_comm := mul_comm
  mul_assoc := mul_assoc
  exists_pair_ne := ⟨0, 1, by rintro ⟨_⟩⟩
  inv_zero := rfl

SignType as a Commutative Group with Zero

Informal description

The type `SignType` representing signs (negative, zero, positive) forms a commutative group with zero under multiplication.

SignType.instLinearOrder instance

: LinearOrder SignType

Full source

instance : LinearOrder SignType where
  le := (· ≤ ·)
  le_refl a := by cases a <;> constructor
  le_total a b := by cases a <;> cases b <;> first | left; constructor | right; constructor
  le_antisymm := le_antisymm
  le_trans := le_trans
  toDecidableLE := LE.decidableRel
  toDecidableEq := SignType.decidableEq

Linear Order on SignType

Informal description

The type `SignType` of signs (negative, zero, positive) is equipped with a linear order structure, where the ordering is given by `neg ≤ zero ≤ pos`.

SignType.instBoundedOrder instance

: BoundedOrder SignType

Full source

instance : BoundedOrder SignType where
  top := 1
  le_top := LE.of_pos
  bot := -1
  bot_le :=
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/6053
    Added `by exact`, but don't understand why it was needed. -/
    by exact LE.of_neg

Bounded Order Structure on SignType

Informal description

The type `SignType` of signs (negative, zero, positive) is equipped with a bounded order structure, having both a greatest element (positive) and a least element (negative).

SignType.instHasDistribNeg instance

: HasDistribNeg SignType

Full source

instance : HasDistribNeg SignType :=
  { neg_neg := fun x => by cases x <;> rfl
    neg_mul := fun x y => by cases x <;> cases y <;> rfl
    mul_neg := fun x y => by cases x <;> cases y <;> rfl }

Distributive Negation on SignType

Informal description

The type `SignType` representing signs (negative, zero, positive) has a negation operation that distributes over multiplication. That is, for any signs $a$ and $b$, we have $-(a * b) = (-a) * b = a * (-b)$.

SignType.fin3Equiv definition

: SignType ≃* Fin 3

Full source

/-- `SignType` is equivalent to `Fin 3`. -/
def fin3Equiv : SignTypeSignType ≃* Fin 3 where
  toFun a :=
    match a with
    | 0 => ⟨0, by simp⟩
    | 1 => ⟨1, by simp⟩
    | -1 => ⟨2, by simp⟩
  invFun a :=
    match a with
    | ⟨0, _⟩ => 0
    | ⟨1, _⟩ => 1
    | ⟨2, _⟩ => -1
  left_inv a := by cases a <;> rfl
  right_inv a :=
    match a with
    | ⟨0, _⟩ => by simp
    | ⟨1, _⟩ => by simp
    | ⟨2, _⟩ => by simp
  map_mul' a b := by
    cases a <;> cases b <;> rfl

Multiplicative equivalence between SignType and Fin 3

Informal description

The multiplicative equivalence between the type `SignType` (representing negative, zero, and positive signs) and the finite type `Fin 3` (the canonical type with 3 elements). The mapping is defined as: - `0` (zero) maps to `⟨0, _⟩` (the first element of `Fin 3`) - `1` (positive) maps to `⟨1, _⟩` (the second element of `Fin 3`) - `-1` (negative) maps to `⟨2, _⟩` (the third element of `Fin 3`) This equivalence preserves the multiplicative structure of both types.

SignType.nonneg_iff theorem

{a : SignType} : 0 ≤ a ↔ a = 0 ∨ a = 1

Full source

theorem nonneg_iff {a : SignType} : 0 ≤ a ↔ a = 0 ∨ a = 1 := by decide +revert

Nonnegativity Criterion for Signs: $0 \leq a \iff a = 0 \lor a = 1$

Informal description

For any sign $a$ in `SignType` (representing negative, zero, or positive), the inequality $0 \leq a$ holds if and only if $a$ is either zero or positive (i.e., $a = 0$ or $a = 1$).

SignType.nonneg_iff_ne_neg_one theorem

{a : SignType} : 0 ≤ a ↔ a ≠ -1

Full source

theorem nonneg_iff_ne_neg_one {a : SignType} : 0 ≤ a ↔ a ≠ -1 := by decide +revert

Nonnegativity of Sign Equivalent to Not Being Negative

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the nonnegativity condition $0 \leq a$ holds if and only if $a$ is not equal to $\text{neg}$ (i.e., $-1$).

SignType.neg_one_lt_iff theorem

{a : SignType} : -1 < a ↔ 0 ≤ a

Full source

theorem neg_one_lt_iff {a : SignType} : -1 < a ↔ 0 ≤ a := by decide +revert

Negation of SignType is Less Than iff Nonnegative

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the inequality $-1 < a$ holds if and only if $0 \leq a$.

SignType.nonpos_iff theorem

{a : SignType} : a ≤ 0 ↔ a = -1 ∨ a = 0

Full source

theorem nonpos_iff {a : SignType} : a ≤ 0 ↔ a = -1 ∨ a = 0 := by decide +revert

Non-positive Signs Characterization: $a \leq 0 \leftrightarrow a = -1 \lor a = 0$

Informal description

For any sign $a$ in `SignType`, $a$ is non-positive (i.e., $a \leq 0$) if and only if $a$ is either negative ($a = -1$) or zero ($a = 0$).

SignType.nonpos_iff_ne_one theorem

{a : SignType} : a ≤ 0 ↔ a ≠ 1

Full source

theorem nonpos_iff_ne_one {a : SignType} : a ≤ 0 ↔ a ≠ 1 := by decide +revert

Nonpositive Signs are Not Positive

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, $a \leq 0$ if and only if $a \neq \text{pos}$.

SignType.lt_one_iff theorem

{a : SignType} : a < 1 ↔ a ≤ 0

Full source

theorem lt_one_iff {a : SignType} : a < 1 ↔ a ≤ 0 := by decide +revert

Positive Sign Characterization: $a < 1 \leftrightarrow a \leq 0$

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the inequality $a < 1$ holds if and only if $a \leq 0$, where $1$ represents the positive sign and $0$ represents the zero sign.

SignType.neg_iff theorem

{a : SignType} : a < 0 ↔ a = -1

Full source

@[simp]
theorem neg_iff {a : SignType} : a < 0 ↔ a = -1 := by decide +revert

Characterization of Negative Sign: $a < 0 \leftrightarrow a = -1$

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the inequality $a < 0$ holds if and only if $a = -1$, where $-1$ represents the negative sign.

SignType.le_neg_one_iff theorem

{a : SignType} : a ≤ -1 ↔ a = -1

Full source

@[simp]
theorem le_neg_one_iff {a : SignType} : a ≤ -1 ↔ a = -1 :=
  le_bot_iff

Characterization of Negative Sign: $a \leq -1 \leftrightarrow a = -1$

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the inequality $a \leq -1$ holds if and only if $a = -1$, where $-1$ represents the negative sign.

SignType.pos_iff theorem

{a : SignType} : 0 < a ↔ a = 1

Full source

@[simp]
theorem pos_iff {a : SignType} : 0 < a ↔ a = 1 := by decide +revert

Characterization of Positive Sign: $0 < a \leftrightarrow a = 1$

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the inequality $0 < a$ holds if and only if $a = 1$, where $1$ represents the positive sign.

SignType.one_le_iff theorem

{a : SignType} : 1 ≤ a ↔ a = 1

Full source

@[simp]
theorem one_le_iff {a : SignType} : 1 ≤ a ↔ a = 1 :=
  top_le_iff

Characterization of Positive Sign: $1 \leq a \leftrightarrow a = 1$

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the inequality $1 \leq a$ holds if and only if $a = 1$, where $1$ represents the positive sign.

SignType.neg_one_le theorem

(a : SignType) : -1 ≤ a

Full source

@[simp]
theorem neg_one_le (a : SignType) : -1 ≤ a :=
  bot_le

Negation of One is Least Element in SignType

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, we have $-1 \leq a$.

SignType.le_one theorem

(a : SignType) : a ≤ 1

Full source

@[simp]
theorem le_one (a : SignType) : a ≤ 1 :=
  le_top

Every sign is less than or equal to positive

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, we have $a \leq 1$, where $1$ represents the positive sign.

SignType.not_lt_neg_one theorem

(a : SignType) : ¬a < -1

Full source

@[simp]
theorem not_lt_neg_one (a : SignType) : ¬a < -1 :=
  not_lt_bot

No Sign is Less Than Negative One: $\neg (a < -1)$ for $a \in \{\text{neg}, \text{zero}, \text{pos}\}$

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, it is not the case that $a$ is strictly less than $-1$.

SignType.not_one_lt theorem

(a : SignType) : ¬1 < a

Full source

@[simp]
theorem not_one_lt (a : SignType) : ¬1 < a :=
  not_top_lt

No Sign is Greater Than Positive: $\neg (1 < a)$

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, it is not the case that the positive sign is strictly less than $a$, i.e., $\neg (\text{pos} < a)$.

SignType.self_eq_neg_iff theorem

(a : SignType) : a = -a ↔ a = 0

Full source

@[simp]
theorem self_eq_neg_iff (a : SignType) : a = -a ↔ a = 0 := by decide +revert

Sign Equals Its Negation if and only if Zero

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the equality $a = -a$ holds if and only if $a$ is the zero sign, i.e., $a = \text{zero}$.

SignType.neg_eq_self_iff theorem

(a : SignType) : -a = a ↔ a = 0

Full source

@[simp]
theorem neg_eq_self_iff (a : SignType) : -a = a ↔ a = 0 := by decide +revert

Negation Equals Self if and only if Zero

Informal description

For any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$, the negation of $a$ equals $a$ if and only if $a$ is the zero sign, i.e., $-a = a \leftrightarrow a = \text{zero}$.

SignType.neg_one_lt_one theorem

: (-1 : SignType) < 1

Full source

@[simp]
theorem neg_one_lt_one : (-1 : SignType) < 1 :=
  bot_lt_top

Negative Sign is Less Than Positive Sign in `SignType`

Informal description

In the type `SignType` representing signs (negative, zero, positive), the negative sign $-1$ is strictly less than the positive sign $1$, i.e., $-1 < 1$.

SignType.cast definition

: SignType → α

Full source

/-- Turn a `SignType` into zero, one, or minus one. This is a coercion instance. -/
@[coe]
def cast : SignType → α
  | zero => 0
  | pos => 1
  | neg => -1

Sign to value conversion

Informal description

The function maps a `SignType` element to its corresponding value in a type `α` with zero, one, and negation operations. Specifically: - `zero` maps to $0$, - `pos` maps to $1$, - `neg` maps to $-1$.

SignType.instCoeTail instance

: CoeTail SignType α

Full source

/-- 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 `α`.
-/
instance : CoeTail SignType α :=
  ⟨cast⟩

Canonical Interpretation of Signs in a Type with Zero, One, and Negation

Informal description

For any type $\alpha$ with zero, one, and negation operations, there is a canonical way to interpret elements of `SignType` (negative/zero/positive) as elements of $\alpha$, where `neg` maps to $-1$, `zero` maps to $0$, and `pos` maps to $1$.

SignType.map_cast' theorem

 {β : Type*} [One β] [Neg β] [Zero β] (f : α → β) (h₁ : f 1 = 1) (h₂ : f 0 = 0) (h₃ : f (-1) = -1) (s : SignType) :
  f s = s

Full source

/-- Casting out of `SignType` respects composition with functions preserving `0, 1, -1`. -/
lemma map_cast' {β : Type*} [One β] [Neg β] [Zero β]
    (f : α → β) (h₁ : f 1 = 1) (h₂ : f 0 = 0) (h₃ : f (-1) = -1) (s : SignType) :
    f s = s := by
  cases s <;> simp only [SignType.cast, h₁, h₂, h₃]

Preservation of Sign Under Zero/One/Negation-Preserving Maps

Informal description

Let $\alpha$ and $\beta$ be types with zero, one, and negation operations. For any function $f : \alpha \to \beta$ satisfying: - $f(1) = 1$, - $f(0) = 0$, - $f(-1) = -1$, and for any sign $s \in \text{SignType}$ (where $\text{SignType}$ is the type with elements $\text{neg}$, $\text{zero}$, $\text{pos}$), we have $f(s) = s$ when interpreting $s$ as an element of $\beta$ via the canonical map.

SignType.map_cast theorem

 {α β F : Type*} [AddGroupWithOne α] [One β] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β]
  [OneHomClass F α β] (f : F) (s : SignType) : f s = s

Full source

/-- Casting out of `SignType` respects composition with suitable bundled homomorphism types. -/
lemma map_cast {α β F : Type*} [AddGroupWithOne α] [One β] [SubtractionMonoid β]
    [FunLike F α β] [AddMonoidHomClass F α β] [OneHomClass F α β] (f : F) (s : SignType) :
    f s = s := by
  apply map_cast' <;> simp

Preservation of Sign Under Additive Monoid Homomorphisms

Informal description

Let $\alpha$ and $\beta$ be types with additive group with one and subtraction monoid structures respectively, and let $F$ be a type of functions from $\alpha$ to $\beta$ that are additive monoid homomorphisms and preserve the identity element. For any $f \in F$ and any sign $s \in \text{SignType}$, the image of $s$ under $f$ is equal to $s$ when interpreted in $\beta$, i.e., $f(s) = s$.

SignType.coe_zero theorem

: ↑(0 : SignType) = (0 : α)

Full source

@[simp]
theorem coe_zero : ↑(0 : SignType) = (0 : α) :=
  rfl

Canonical Map of Zero in SignType Equals Zero in $\alpha$

Informal description

The canonical map from the `SignType` element $0$ (representing the zero sign) to an element of type $\alpha$ with a zero structure yields $0$ in $\alpha$, i.e., $\uparrow(0 : \text{SignType}) = (0 : \alpha)$.

SignType.coe_one theorem

: ↑(1 : SignType) = (1 : α)

Full source

@[simp]
theorem coe_one : ↑(1 : SignType) = (1 : α) :=
  rfl

Canonical Map of Positive One in SignType Equals One in $\alpha$

Informal description

The canonical map from the `SignType` element $1$ (representing the positive sign) to an element of type $\alpha$ with a one and subtraction monoid structure yields $1$ in $\alpha$, i.e., $\uparrow(1 : \text{SignType}) = (1 : \alpha)$.

SignType.coe_neg_one theorem

: ↑(-1 : SignType) = (-1 : α)

Full source

@[simp]
theorem coe_neg_one : ↑(-1 : SignType) = (-1 : α) :=
  rfl

Canonical Map of Negative One in SignType Equals Negative One in $\alpha$

Informal description

The canonical map from the `SignType` element $-1$ (representing the negative sign) to an element of type $\alpha$ with a subtraction monoid structure yields $-1$ in $\alpha$, i.e., $\uparrow(-1 : \text{SignType}) = (-1 : \alpha)$.

SignType.coe_neg theorem

{α : Type*} [One α] [SubtractionMonoid α] (s : SignType) : (↑(-s) : α) = -↑s

Full source

@[simp, norm_cast]
lemma coe_neg {α : Type*} [One α] [SubtractionMonoid α] (s : SignType) :
    (↑(-s) : α) = -↑s := by
  cases s <;> simp

Negation Commutes with Canonical Map in SignType

Informal description

For any type $\alpha$ equipped with a multiplicative identity and a subtraction monoid structure, and for any sign $s \in \text{SignType}$, the canonical map satisfies $\uparrow(-s) = -\uparrow s$ in $\alpha$.

SignType.intCast_cast theorem

{α : Type*} [AddGroupWithOne α] (s : SignType) : ((s : ℤ) : α) = s

Full source

/-- Casting `SignType → ℤ → α` is the same as casting directly `SignType → α`. -/
@[simp, norm_cast]
lemma intCast_cast {α : Type*} [AddGroupWithOne α] (s : SignType) : ((s : ℤ) : α) = s :=
  map_cast' _ Int.cast_one Int.cast_zero (@Int.cast_one α _ ▸ Int.cast_neg 1) _

Compatibility of SignType and Integer Casting to $\alpha$

Informal description

For any type $\alpha$ with an additive group structure with one, and for any sign $s \in \text{SignType}$, the canonical map from $\mathbb{Z}$ to $\alpha$ applied to $s$ (interpreted as an integer) equals the canonical map from $\text{SignType}$ to $\alpha$ applied to $s$. That is, $(s : \mathbb{Z}) : \alpha = s : \alpha$.

SignType.castHom definition

{α} [MulZeroOneClass α] [HasDistribNeg α] : SignType →*₀ α

Full source

/-- `SignType.cast` as a `MulWithZeroHom`. -/
@[simps]
def castHom {α} [MulZeroOneClass α] [HasDistribNeg α] : SignTypeSignType →*₀ α where
  toFun := cast
  map_zero' := rfl
  map_one' := rfl
  map_mul' x y := by cases x <;> cases y <;> simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Sign to value multiplicative homomorphism with zero

Informal description

The function `SignType.castHom` is a multiplicative homomorphism with zero from `SignType` to a type `α` equipped with a multiplicative monoid structure with zero and a distributive negation operation. It maps: - `zero` to $0$, - `pos` to $1$, - `neg` to $-1$, and preserves multiplication, zero, and one.

SignType.univ_eq theorem

: (Finset.univ : Finset SignType) = {0, -1, 1}

Full source

theorem univ_eq : (Finset.univ : Finset SignType) = {0, -1, 1} := by
  decide

Universal Finite Set of Sign Types: $\text{univ} = \{0, -1, 1\}$

Informal description

The universal finite set of the type `SignType` (representing signs: negative, zero, positive) is equal to the set $\{0, -1, 1\}$.

SignType.range_eq theorem

{α} (f : SignType → α) : Set.range f = {f zero, f neg, f pos}

Full source

theorem range_eq {α} (f : SignType → α) : Set.range f = {f zero, f neg, f pos} := by
  classical rw [← Fintype.coe_image_univ, univ_eq]
  classical simp [Finset.coe_insert]

Range of a Function on Sign Types: $\text{range}(f) = \{f(0), f(-1), f(1)\}$

Informal description

For any function $f : \text{SignType} \to \alpha$, the range of $f$ is equal to the set $\{f(\text{zero}), f(\text{neg}), f(\text{pos})\}$.

SignType.coe_mul theorem

{α} [MulZeroOneClass α] [HasDistribNeg α] (a b : SignType) : ↑(a * b) = (a : α) * b

Full source

@[simp, norm_cast] lemma coe_mul {α} [MulZeroOneClass α] [HasDistribNeg α] (a b : SignType) :
    ↑(a * b) = (a : α) * b :=
  map_mul SignType.castHom _ _

Multiplicative Property of Sign Casting

Informal description

For any type $\alpha$ with a multiplicative monoid structure with zero and a distributive negation operation, and for any signs $a, b \in \text{SignType}$, the canonical map $\text{SignType} \to \alpha$ satisfies $\uparrow(a * b) = \uparrow a * \uparrow b$.

SignType.coe_pow theorem

{α} [MonoidWithZero α] [HasDistribNeg α] (a : SignType) (k : ℕ) : ↑(a ^ k) = (a : α) ^ k

Full source

@[simp, norm_cast] lemma coe_pow {α} [MonoidWithZero α] [HasDistribNeg α] (a : SignType) (k : ℕ) :
    ↑(a ^ k) = (a : α) ^ k :=
  map_pow SignType.castHom _ _

Power Preservation under Sign to Value Conversion: $(a^k : \alpha) = (a : \alpha)^k$

Informal description

Let $\alpha$ be a type equipped with a monoid structure with zero and a distributive negation operation. For any sign $a \in \text{SignType}$ and any natural number $k$, the image of $a^k$ under the canonical map $\text{SignType} \to \alpha$ equals the $k$-th power of the image of $a$ in $\alpha$, i.e., $(a^k : \alpha) = (a : \alpha)^k$.

SignType.coe_zpow theorem

{α} [GroupWithZero α] [HasDistribNeg α] (a : SignType) (k : ℤ) : ↑(a ^ k) = (a : α) ^ k

Full source

@[simp, norm_cast] lemma coe_zpow {α} [GroupWithZero α] [HasDistribNeg α] (a : SignType) (k : ℤ) :
    ↑(a ^ k) = (a : α) ^ k :=
  map_zpow₀ SignType.castHom _ _

Power Preservation in Sign to Value Conversion for Integer Exponents

Informal description

For any type $\alpha$ equipped with a group structure with zero and a distributive negation operation, and for any sign $a \in \{\text{neg}, \text{zero}, \text{pos}\}$ and any integer exponent $k$, the canonical map from `SignType` to $\alpha$ preserves integer powers, i.e., $(a^k) = (a)^k$ in $\alpha$.

SignType.sign definition

: α →o SignType

Full source

/-- The sign of an element is 1 if it's positive, -1 if negative, 0 otherwise. -/
def SignType.sign : α →o SignType :=
  ⟨fun a => if 0 < a then 1 else if a < 0 then -1 else 0, fun a b h => by
    dsimp
    split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃ <;> try constructor
    · cases lt_irrefl 0 (h₁.trans <| h.trans_lt h₃)
    · cases h₂ (h₁.trans_le h)
    · cases h₄ (h.trans_lt h₃)⟩

Sign function

Informal description

The sign function maps an element $a$ of a type $\alpha$ with zero and a decidable order to its sign: $1$ if $a$ is positive, $-1$ if $a$ is negative, and $0$ otherwise. This function is monotone (order-preserving) with respect to the order on $\alpha$ and the linear order on `SignType` (where $\text{neg} \leq \text{zero} \leq \text{pos}$).

sign_apply theorem

: sign a = ite (0 < a) 1 (ite (a < 0) (-1) 0)

Full source

theorem sign_apply : sign a = ite (0 < a) 1 (ite (a < 0) (-1) 0) :=
  rfl

Definition of the Sign Function via Cases

Informal description

For any element $a$ of a type $\alpha$ with zero and a decidable order relation, the sign function is defined as: \[ \text{sign}(a) = \begin{cases} 1 & \text{if } 0 < a, \\ -1 & \text{if } a < 0, \\ 0 & \text{otherwise.} \end{cases} \]

sign_zero theorem

: sign (0 : α) = 0

Full source

@[simp]
theorem sign_zero : sign (0 : α) = 0 := by simp [sign_apply]

Sign of Zero is Zero

Informal description

The sign function evaluated at zero equals zero, i.e., $\text{sign}(0) = 0$.

sign_pos theorem

(ha : 0 < a) : sign a = 1

Full source

@[simp]
theorem sign_pos (ha : 0 < a) : sign a = 1 := by rwa [sign_apply, if_pos]

Sign of Positive Element is One

Informal description

For any element $a$ of a type $\alpha$ with zero and a decidable order relation, if $0 < a$, then the sign function evaluated at $a$ equals $1$, i.e., $\text{sign}(a) = 1$.

sign_neg theorem

(ha : a < 0) : sign a = -1

Full source

@[simp]
theorem sign_neg (ha : a < 0) : sign a = -1 := by rwa [sign_apply, if_neg <| asymm ha, if_pos]

Sign of Negative Element is $-1$

Informal description

For any element $a$ in a type with zero and a decidable order relation, if $a < 0$, then the sign function evaluated at $a$ equals $-1$, i.e., $\text{sign}(a) = -1$.

sign_eq_one_iff theorem

: sign a = 1 ↔ 0 < a

Full source

theorem sign_eq_one_iff : signsign a = 1 ↔ 0 < a := by
  refine ⟨fun h => ?_, fun h => sign_pos h⟩
  by_contra hn
  rw [sign_apply, if_neg hn] at h
  split_ifs at h

Sign Equals One if and only if Positive

Informal description

For any element $a$ of a type with zero and a decidable order relation, the sign function evaluated at $a$ equals $1$ if and only if $0 < a$, i.e., $\text{sign}(a) = 1 \leftrightarrow 0 < a$.

sign_eq_neg_one_iff theorem

: sign a = -1 ↔ a < 0

Full source

theorem sign_eq_neg_one_iff : signsign a = -1 ↔ a < 0 := by
  refine ⟨fun h => ?_, fun h => sign_neg h⟩
  rw [sign_apply] at h
  split_ifs at h
  assumption

Sign Equivalence for Negative Elements: $\text{sign}(a) = -1 \leftrightarrow a < 0$

Informal description

For any element $a$ of a type with zero and a decidable order relation, the sign function satisfies $\text{sign}(a) = -1$ if and only if $a < 0$.

StrictMono.sign_comp theorem

 {β F : Type*} [Zero β] [Preorder β] [DecidableLT β] [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : StrictMono f)
  (a : α) : sign (f a) = sign a

Full source

/-- `SignType.sign` respects strictly monotone zero-preserving maps. -/
lemma StrictMono.sign_comp {β F : Type*} [Zero β] [Preorder β] [DecidableLT β]
    [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : StrictMono f) (a : α) :
    sign (f a) = sign a := by
  simp only [sign_apply, ← map_zero f, hf.lt_iff_lt]

Sign Preservation under Strictly Monotone Zero-Preserving Maps

Informal description

Let $\alpha$ and $\beta$ be types with zero elements and decidable order relations, and let $F$ be a type of zero-preserving functions from $\alpha$ to $\beta$. Given a strictly monotone function $f \in F$ and an element $a \in \alpha$, the sign of $f(a)$ is equal to the sign of $a$, i.e., $\text{sign}(f(a)) = \text{sign}(a)$.

sign_eq_zero_iff theorem

: sign a = 0 ↔ a = 0

Full source

@[simp]
theorem sign_eq_zero_iff : signsign a = 0 ↔ a = 0 := by
  refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩
  rw [sign_apply] at h
  split_ifs at h with h_1 h_2
  cases h
  exact (le_of_not_lt h_1).eq_of_not_lt h_2

Sign Zero Equivalence: $\text{sign}(a) = 0 \leftrightarrow a = 0$

Informal description

For any element $a$ of a type $\alpha$ with zero and a decidable order relation, the sign function satisfies $\text{sign}(a) = 0$ if and only if $a = 0$.

sign_ne_zero theorem

: sign a ≠ 0 ↔ a ≠ 0

Full source

theorem sign_ne_zero : signsign a ≠ 0sign a ≠ 0 ↔ a ≠ 0 :=
  sign_eq_zero_iff.not

Nonzero Sign Equivalence: $\text{sign}(a) \neq 0 \leftrightarrow a \neq 0$

Informal description

For any element $a$ of a type $\alpha$ with zero and a decidable order relation, the sign function satisfies $\text{sign}(a) \neq 0$ if and only if $a \neq 0$.

sign_nonneg_iff theorem

: 0 ≤ sign a ↔ 0 ≤ a

Full source

@[simp]
theorem sign_nonneg_iff : 0 ≤ sign a ↔ 0 ≤ a := by
  rcases lt_trichotomy 0 a with (h | h | h)
  · simp [h, h.le]
  · simp [← h]
  · simp [h, h.not_le]

Nonnegativity of Sign Function: $0 \leq \text{sign}(a) \leftrightarrow 0 \leq a$

Informal description

For any element $a$ of a type $\alpha$ with zero and a decidable order relation, the sign of $a$ is nonnegative (i.e., $0 \leq \text{sign}(a)$) if and only if $a$ itself is nonnegative (i.e., $0 \leq a$).

sign_nonpos_iff theorem

: sign a ≤ 0 ↔ a ≤ 0

Full source

@[simp]
theorem sign_nonpos_iff : signsign a ≤ 0 ↔ a ≤ 0 := by
  rcases lt_trichotomy 0 a with (h | h | h)
  · simp [h, h.not_le]
  · simp [← h]
  · simp [h, h.le]

Sign Nonpositivity Criterion: $\text{sign}(a) \leq 0 \leftrightarrow a \leq 0$

Informal description

For any element $a$ in a type with zero and a decidable order relation, the sign of $a$ is nonpositive (i.e., $\text{sign}(a) \leq 0$) if and only if $a$ itself is nonpositive (i.e., $a \leq 0$).

sign_one theorem

: sign (1 : α) = 1

Full source

theorem sign_one : sign (1 : α) = 1 :=
  sign_pos zero_lt_one

Sign of One is One

Informal description

For any type $\alpha$ with zero and a decidable order relation, the sign function evaluated at the multiplicative identity $1$ is equal to $1$, i.e., $\text{sign}(1) = 1$.

sign_intCast theorem

 {α : Type*} [Ring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] [DecidableLT α] (n : ℤ) : sign (n : α) = sign n

Full source

@[simp]
lemma sign_intCast {α : Type*} [Ring α] [PartialOrder α] [IsOrderedRing α]
    [Nontrivial α] [DecidableLT α] (n : ℤ) :
    sign (n : α) = sign n := by
  simp only [sign_apply, Int.cast_pos, Int.cast_lt_zero]

Sign Preservation under Integer Cast in Ordered Rings

Informal description

Let $\alpha$ be a nontrivial ordered ring with a decidable less-than relation. For any integer $n \in \mathbb{Z}$, the sign of the cast of $n$ in $\alpha$ equals the sign of $n$ in $\mathbb{Z}$. That is, $\text{sign}(n : \alpha) = \text{sign}(n)$.

sign_mul theorem

(x y : α) : sign (x * y) = sign x * sign y

Full source

theorem sign_mul (x y : α) : sign (x * y) = sign x * sign y := by
  rcases lt_trichotomy x 0 with (hx | hx | hx) <;> rcases lt_trichotomy y 0 with (hy | hy | hy) <;>
    simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Sign of Product Equals Product of Signs

Informal description

For any elements $x$ and $y$ in a type $\alpha$ with zero and a decidable order relation, the sign of their product equals the product of their signs, i.e., $\text{sign}(x \cdot y) = \text{sign}(x) \cdot \text{sign}(y)$.

sign_mul_abs theorem

(x : α) : (sign x * |x| : α) = x

Full source

@[simp] theorem sign_mul_abs (x : α) : (sign x * |x| : α) = x := by
  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Sign-Absolute Value Product Identity: $\text{sign}(x) \cdot |x| = x$

Informal description

For any element $x$ in a type $\alpha$ with zero and a decidable order relation, the product of the sign of $x$ and the absolute value of $x$ equals $x$, i.e., $\text{sign}(x) \cdot |x| = x$.

abs_mul_sign theorem

(x : α) : (|x| * sign x : α) = x

Full source

@[simp] theorem abs_mul_sign (x : α) : (|x| * sign x : α) = x := by
  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Absolute Value and Sign Product Identity: $|x| \cdot \text{sign}(x) = x$

Informal description

For any element $x$ in a type $\alpha$ with zero and a decidable order relation, the product of the absolute value of $x$ and the sign of $x$ equals $x$, i.e., $|x| \cdot \text{sign}(x) = x$.

sign_mul_self theorem

(x : α) : sign x * x = |x|

Full source

@[simp]
theorem sign_mul_self (x : α) : sign x * x = |x| := by
  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Sign-Absolute Value Identity: $\text{sign}(x) \cdot x = |x|$

Informal description

For any element $x$ in a type $\alpha$ with zero and a decidable order relation, the product of the sign of $x$ and $x$ itself equals the absolute value of $x$, i.e., $\text{sign}(x) \cdot x = |x|$.

self_mul_sign theorem

(x : α) : x * sign x = |x|

Full source

@[simp]
theorem self_mul_sign (x : α) : x * sign x = |x| := by
  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Product of Element with its Sign Equals Absolute Value

Informal description

For any element $x$ in a type $\alpha$ with zero and a decidable order relation, the product of $x$ with its sign equals the absolute value of $x$, i.e., $x \cdot \text{sign}(x) = |x|$.

signHom definition

: α →*₀ SignType

Full source

/-- `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`) -/
def signHom : α →*₀ SignType where
  toFun := sign
  map_zero' := sign_zero
  map_one' := sign_one
  map_mul' := sign_mul

Sign homomorphism as a monoid with zero homomorphism

Informal description

The function `signHom` is a monoid homomorphism with zero from a type $\alpha$ (with zero and a decidable order relation) to `SignType`. It maps an element to its sign (negative, zero, or positive), preserves zero (`sign 0 = 0`), preserves one (`sign 1 = 1`), and is multiplicative (`sign (x * y) = sign x * sign y`).

sign_pow theorem

(x : α) (n : ℕ) : sign (x ^ n) = sign x ^ n

Full source

theorem sign_pow (x : α) (n : ℕ) : sign (x ^ n) = sign x ^ n := map_pow signHom x n

Sign Preservation under Powers: $\text{sign}(x^n) = (\text{sign}(x))^n$

Informal description

For any element $x$ in a type $\alpha$ with zero and a decidable order relation, and for any natural number $n$, the sign of $x^n$ equals the $n$-th power of the sign of $x$, i.e., $\text{sign}(x^n) = (\text{sign}(x))^n$.

Left.sign_neg theorem

[AddLeftStrictMono α] (a : α) : sign (-a) = -sign a

Full source

theorem Left.sign_neg [AddLeftStrictMono α] (a : α) : sign (-a) = -sign a := by
  simp_rw [sign_apply, Left.neg_pos_iff, Left.neg_neg_iff]
  split_ifs with h h'
  · exact False.elim (lt_asymm h h')
  · simp
  · simp
  · simp

Sign of Negative Element Equals Negation of Sign under Left-Strictly Monotone Addition

Informal description

For any element $a$ in a type $\alpha$ with a strictly increasing addition operation, the sign of $-a$ is equal to the negation of the sign of $a$, i.e., $\text{sign}(-a) = -\text{sign}(a)$.

Right.sign_neg theorem

[AddRightStrictMono α] (a : α) : sign (-a) = -sign a

Full source

theorem Right.sign_neg [AddRightStrictMono α] (a : α) :
    sign (-a) = -sign a := by
  simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]
  split_ifs with h h'
  · exact False.elim (lt_asymm h h')
  · simp
  · simp
  · simp

Sign of Negative Element Equals Negation of Sign

Informal description

For any element $a$ in a type $\alpha$ with a strictly increasing right addition operation, the sign of $-a$ is equal to the negation of the sign of $a$, i.e., $\text{sign}(-a) = -\text{sign}(a)$.

sign_sum theorem

 {ι : Type*} {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (t : SignType) (h : ∀ i ∈ s, sign (f i) = t) :
  sign (∑ i ∈ s, f i) = t

Full source

theorem sign_sum {ι : Type*} {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (t : SignType)
    (h : ∀ i ∈ s, sign (f i) = t) : sign (∑ i ∈ s, f i) = t := by
  cases t
  · simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢
    exact Finset.sum_eq_zero h
  · simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
    exact Finset.sum_neg h hs
  · simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
    exact Finset.sum_pos h hs

Sign of Sum When All Terms Have the Same Sign

Informal description

Let $\alpha$ be a type with a zero element and a decidable order, and let $\iota$ be an index type. For any nonempty finite set $s \subseteq \iota$ and any function $f : \iota \to \alpha$, if there exists a sign $t \in \{\text{neg}, \text{zero}, \text{pos}\}$ such that for every $i \in s$, the sign of $f(i)$ equals $t$, then the sign of the sum $\sum_{i \in s} f(i)$ is also equal to $t$.

Int.sign_eq_sign theorem

(n : ℤ) : Int.sign n = SignType.sign n

Full source

theorem sign_eq_sign (n : ℤ) : Int.sign n = SignType.sign n := by
  obtain (n | _) | _ := n <;> simp [sign, Int.sign_neg, negSucc_lt_zero]

Equality of Integer Sign Function and SignType Sign Function

Informal description

For any integer $n$, the sign function defined on integers equals the sign function defined on the type `SignType`, i.e., $\text{Int.sign}(n) = \text{SignType.sign}(n)$.

exists_signed_sum theorem

 [DecidableEq α] (s : Finset α) (f : α → ℤ) :
  ∃ (β : Type u) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
    (∀ b, g b ∈ s) ∧ (Fintype.card β = ∑ a ∈ s, (f a).natAbs) ∧ ∀ a ∈ s, (∑ b, if g b = a then (sgn b : ℤ) else 0) = f a

Full source

/-- We can decompose a sum of absolute value `n` into a sum of `n` signs. -/
theorem exists_signed_sum [DecidableEq α] (s : Finset α) (f : α → ℤ) :
    ∃ (β : Type u) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
      (∀ b, g b ∈ s) ∧
        (Fintype.card β = ∑ a ∈ s, (f a).natAbs) ∧
          ∀ a ∈ s, (∑ b, if g b = a then (sgn b : ℤ) else 0) = f a :=
  let ⟨β, t, sgn, g, hg, ht, hf⟩ := exists_signed_sum_aux s f
  ⟨t, inferInstance, fun b => sgn b, fun b => g b, fun b => hg b, by simp [ht], fun a ha =>
    (sum_attach t fun b ↦ ite (g b = a) (sgn b : ℤ) 0).trans <| hf _ ha⟩

Decomposition of Integer-Valued Function into Signed Sum over Finite Set

Informal description

For any finite set $s$ in a type $\alpha$ with decidable equality and any function $f \colon \alpha \to \mathbb{Z}$, there exists a finite type $\beta$, a sign function $\operatorname{sgn} \colon \beta \to \{\text{neg}, \text{zero}, \text{pos}\}$, and a function $g \colon \beta \to \alpha$ such that: 1. For every $b \in \beta$, $g(b) \in s$, 2. The cardinality of $\beta$ equals the sum of the absolute values of $f$ over $s$, i.e., $|\beta| = \sum_{a \in s} |f(a)|$, 3. For every $a \in s$, the sum of the signs (interpreted as integers) of all $b \in \beta$ with $g(b) = a$ equals $f(a)$, i.e., $\sum_{b} \begin{cases} \operatorname{sgn}(b) & \text{if } g(b) = a \\ 0 & \text{otherwise} \end{cases} = f(a)$.

exists_signed_sum' theorem

 [Nonempty α] [DecidableEq α] (s : Finset α) (f : α → ℤ) (n : ℕ) (h : (∑ i ∈ s, (f i).natAbs) ≤ n) :
  ∃ (β : Type u) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
    (∀ b, g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then (sgn i : ℤ) else 0) = f a

Full source

/-- We can decompose a sum of absolute value less than `n` into a sum of at most `n` signs. -/
theorem exists_signed_sum' [Nonempty α] [DecidableEq α] (s : Finset α) (f : α → ℤ)
    (n : ℕ) (h : (∑ i ∈ s, (f i).natAbs) ≤ n) :
    ∃ (β : Type u) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
      (∀ b, g b ∉ s → sgn b = 0) ∧
        Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then (sgn i : ℤ) else 0) = f a := by
  obtain ⟨β, _, sgn, g, hg, hβ, hf⟩ := exists_signed_sum s f
  refine
    ⟨β ⊕ (Fin (n - ∑ i ∈ s, (f i).natAbs)), inferInstance, Sum.elim sgn 0,
      Sum.elim g (Classical.arbitrary (Fin (n - Finset.sum s fun i => Int.natAbs (f i)) → α)),
        ?_, by simp [hβ, h], fun a ha => by simp [hf _ ha]⟩
  rintro (b | b) hb
  · cases hb (hg _)
  · rfl

Decomposition of Integer-Valued Function into Extended Signed Sum

Informal description

Let $\alpha$ be a nonempty type with decidable equality, $s$ a finite subset of $\alpha$, and $f \colon \alpha \to \mathbb{Z}$ a function. For any natural number $n$ such that $\sum_{a \in s} |f(a)| \leq n$, there exists a finite type $\beta$, a sign function $\operatorname{sgn} \colon \beta \to \{-1, 0, 1\}$, and a function $g \colon \beta \to \alpha$ satisfying: 1. For all $b \in \beta$, if $g(b) \notin s$ then $\operatorname{sgn}(b) = 0$, 2. The cardinality of $\beta$ is $n$, 3. For every $a \in s$, $\sum_{b \in \beta} \begin{cases} \operatorname{sgn}(b) & \text{if } g(b) = a \\ 0 & \text{otherwise} \end{cases} = f(a)$.