mathlib3 documentation

data.sign

Sign function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the sign function for types with zero and a decidable less-than relation, and proves some basic theorems about it.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
inductive sign_type.le  :

The less-than relation on signs.

Instances for sign_type.le
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
  • sign_type.comm_group_with_zero = {mul := has_mul.mul sign_type.has_mul, mul_assoc := sign_type.comm_group_with_zero._proof_1, one := 1, one_mul := sign_type.comm_group_with_zero._proof_2, mul_one := sign_type.comm_group_with_zero._proof_3, npow := comm_monoid_with_zero.npow._default 1 has_mul.mul sign_type.comm_group_with_zero._proof_4 sign_type.comm_group_with_zero._proof_5, npow_zero' := sign_type.comm_group_with_zero._proof_6, npow_succ' := sign_type.comm_group_with_zero._proof_7, mul_comm := sign_type.comm_group_with_zero._proof_8, zero := 0, zero_mul := sign_type.comm_group_with_zero._proof_9, mul_zero := sign_type.comm_group_with_zero._proof_10, inv := id sign_type, div := group_with_zero.div._default has_mul.mul sign_type.comm_group_with_zero._proof_11 1 sign_type.comm_group_with_zero._proof_12 sign_type.comm_group_with_zero._proof_13 (comm_monoid_with_zero.npow._default 1 has_mul.mul sign_type.comm_group_with_zero._proof_4 sign_type.comm_group_with_zero._proof_5) sign_type.comm_group_with_zero._proof_14 sign_type.comm_group_with_zero._proof_15 id, div_eq_mul_inv := sign_type.comm_group_with_zero._proof_16, zpow := group_with_zero.zpow._default has_mul.mul sign_type.comm_group_with_zero._proof_17 1 sign_type.comm_group_with_zero._proof_18 sign_type.comm_group_with_zero._proof_19 (comm_monoid_with_zero.npow._default 1 has_mul.mul sign_type.comm_group_with_zero._proof_4 sign_type.comm_group_with_zero._proof_5) sign_type.comm_group_with_zero._proof_20 sign_type.comm_group_with_zero._proof_21 id, zpow_zero' := sign_type.comm_group_with_zero._proof_22, zpow_succ' := sign_type.comm_group_with_zero._proof_23, zpow_neg' := sign_type.comm_group_with_zero._proof_24, exists_pair_ne := sign_type.comm_group_with_zero._proof_25, inv_zero := sign_type.comm_group_with_zero._proof_26, mul_inv_cancel := sign_type.comm_group_with_zero._proof_27}
@[protected, instance]
Equations
@[protected, instance]
Equations

sign_type is equivalent to fin 3.

Equations
theorem sign_type.nonneg_iff {a : sign_type} :
0 a a = 0 a = 1
theorem sign_type.neg_one_lt_iff {a : sign_type} :
-1 < a 0 a
theorem sign_type.nonpos_iff {a : sign_type} :
a 0 a = -1 a = 0
theorem sign_type.lt_one_iff {a : sign_type} :
a < 1 a 0
@[simp]
theorem sign_type.neg_iff {a : sign_type} :
a < 0 a = -1
@[simp]
theorem sign_type.le_neg_one_iff {a : sign_type} :
a -1 a = -1
@[simp]
theorem sign_type.pos_iff {a : sign_type} :
0 < a a = 1
@[simp]
theorem sign_type.one_le_iff {a : sign_type} :
1 a a = 1
@[simp]
theorem sign_type.neg_one_le (a : sign_type) :
-1 a
@[simp]
theorem sign_type.le_one (a : sign_type) :
a 1
@[simp]
theorem sign_type.not_lt_neg_one (a : sign_type) :
¬a < -1
@[simp]
theorem sign_type.not_one_lt (a : sign_type) :
¬1 < a
@[simp]
theorem sign_type.self_eq_neg_iff (a : sign_type) :
a = -a a = 0
@[simp]
theorem sign_type.neg_eq_self_iff (a : sign_type) :
-a = a a = 0
@[simp]
theorem sign_type.neg_one_lt_one  :
-1 < 1
def sign_type.cast {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :

Turn a sign_type 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
@[protected, instance]
def sign_type.has_coe_t {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
Equations
@[simp]
theorem sign_type.cast_eq_coe {α : Type u_1} [has_zero α] [has_one α] [has_neg α] (a : sign_type) :
@[simp]
theorem sign_type.coe_zero {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
0 = 0
@[simp]
theorem sign_type.coe_one {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
1 = 1
@[simp]
theorem sign_type.coe_neg_one {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :
-1 = -1
def sign {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] :

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

Equations
theorem sign_apply {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} :
sign a = ite (0 < a) 1 (ite (a < 0) (-1) 0)
@[simp]
theorem sign_zero {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] :
@[simp]
theorem sign_pos {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} (ha : 0 < a) :
@[simp]
theorem sign_neg {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} (ha : a < 0) :
sign a = -1
theorem sign_eq_one_iff {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} :
sign a = 1 0 < a
theorem sign_eq_neg_one_iff {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} :
sign a = -1 a < 0
@[simp]
theorem sign_eq_zero_iff {α : Type u_1} [has_zero α] [linear_order α] {a : α} :
sign a = 0 a = 0
theorem sign_ne_zero {α : Type u_1} [has_zero α] [linear_order α] {a : α} :
sign a 0 a 0
@[simp]
theorem sign_nonneg_iff {α : Type u_1} [has_zero α] [linear_order α] {a : α} :
0 sign a 0 a
@[simp]
theorem sign_nonpos_iff {α : Type u_1} [has_zero α] [linear_order α] {a : α} :
sign a 0 a 0
@[simp]
theorem sign_one {α : Type u_1} [ordered_semiring α] [decidable_rel has_lt.lt] [nontrivial α] :
theorem sign_mul {α : Type u_1} [linear_ordered_ring α] (x y : α) :
def sign_hom {α : Type u_1} [linear_ordered_ring α] :

sign as a monoid_with_zero_hom 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 = sign (1 + i) * sign (1 - i) ≠ sign 2 = 1. (complex.ordered_comm_ring)

Equations
theorem sign_pow {α : Type u_1} [linear_ordered_ring α] (x : α) (n : ) :
sign (x ^ n) = sign x ^ n
theorem sign_sum {α : Type u_1} [linear_ordered_add_comm_group α] {ι : Type u_2} {s : finset ι} {f : ι α} (hs : s.nonempty) (t : sign_type) (h : (i : ι), i s sign (f i) = t) :
sign (s.sum (λ (i : ι), f i)) = t
theorem int.sign_eq_sign (n : ) :
theorem exists_signed_sum {α : Type u_1} [decidable_eq α] (s : finset α) (f : α ) :
(β : Type u_1) (_x : fintype β) (sgn : β sign_type) (g : β α), ( (b : β), g b s) fintype.card β = s.sum (λ (a : α), (f a).nat_abs) (a : α), a s finset.univ.sum (λ (b : β), ite (g b = a) (sgn b) 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 α] [decidable_eq α] (s : finset α) (f : α ) (n : ) (h : s.sum (λ (i : α), (f i).nat_abs) n) :
(β : Type u_1) (_x : fintype β) (sgn : β sign_type) (g : β α), ( (b : β), g b s sgn b = 0) fintype.card β = n (a : α), a s finset.univ.sum (λ (i : β), ite (g i = a) (sgn i) 0) = f a

We can decompose a sum of absolute value less than n into a sum of at most n signs.