data.sign - mathlib3 docs

sign_type.has_mul = {mul := λ (x y : sign_type), sign_type.has_mul._match_1 y x}
sign_type.has_mul._match_1 y sign_type.pos = y
sign_type.has_mul._match_1 y sign_type.neg = -y
sign_type.has_mul._match_1 y sign_type.zero = sign_type.zero

source

inductive sign_type.le :

sign_type → sign_type → Prop

of_neg : ∀ (a : sign_type), sign_type.neg.le a
zero : sign_type.zero.le sign_type.zero
of_pos : ∀ (a : sign_type), a.le sign_type.pos

The less-than relation on signs.

Instances for sign_type.le

sign_type.le.decidable_rel

source

@[protected, instance]

def sign_type.has_le :

has_le sign_type

Equations

sign_type.has_le = {le := sign_type.le}

source

@[protected, instance]

def sign_type.le.decidable_rel :

decidable_rel sign_type.le

Equations

sign_type.le.decidable_rel = λ (a b : sign_type), a.cases_on (b.cases_on (decidable.is_true sign_type.le.zero) (decidable.is_false sign_type.le.decidable_rel._proof_1) (decidable.is_true _)) (b.cases_on (decidable.is_true _) (decidable.is_true _) (decidable.is_true _)) (b.cases_on (decidable.is_false sign_type.le.decidable_rel._proof_2) (decidable.is_false sign_type.le.decidable_rel._proof_3) (decidable.is_true _))

source

@[protected, instance]

def sign_type.comm_group_with_zero :

comm_group_with_zero sign_type

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}

source

@[protected, instance]

def sign_type.linear_order :

linear_order sign_type

Equations

sign_type.linear_order = {le := has_le.le sign_type.has_le, lt := partial_order.lt._default has_le.le, le_refl := sign_type.linear_order._proof_1, le_trans := sign_type.linear_order._proof_2, lt_iff_le_not_le := sign_type.linear_order._proof_3, le_antisymm := sign_type.linear_order._proof_4, le_total := sign_type.linear_order._proof_5, decidable_le := sign_type.le.decidable_rel, decidable_eq := decidable_eq_of_decidable_le sign_type.le.decidable_rel, decidable_lt := decidable_lt_of_decidable_le sign_type.le.decidable_rel, max := max_default (λ (a b : sign_type), sign_type.le.decidable_rel a b), max_def := sign_type.linear_order._proof_10, min := min_default (λ (a b : sign_type), sign_type.le.decidable_rel a b), min_def := sign_type.linear_order._proof_11}

source

@[protected, instance]

def sign_type.bounded_order :

bounded_order sign_type

Equations

sign_type.bounded_order = {top := 1, le_top := sign_type.le.of_pos, bot := -1, bot_le := sign_type.le.of_neg}

source

@[protected, instance]

def sign_type.has_distrib_neg :

has_distrib_neg sign_type

Equations

sign_type.has_distrib_neg = {neg := has_neg.neg sign_type.has_neg, neg_neg := sign_type.has_distrib_neg._proof_1, neg_mul := sign_type.has_distrib_neg._proof_2, mul_neg := sign_type.has_distrib_neg._proof_3}

source

def sign_type.fin3_equiv :

sign_type ≃* fin 3

sign_type is equivalent to fin 3.

Equations

sign_type.fin3_equiv = {to_fun := λ (a : sign_type), a.rec_on 0 (-1) 1, inv_fun := λ (a : fin 3), sign_type.fin3_equiv._match_1 a, left_inv := sign_type.fin3_equiv._proof_3, right_inv := sign_type.fin3_equiv._proof_4, map_mul' := sign_type.fin3_equiv._proof_5}
sign_type.fin3_equiv._match_1 ⟨n + 3, h⟩ = _.elim
sign_type.fin3_equiv._match_1 ⟨2, h⟩ = -1
sign_type.fin3_equiv._match_1 ⟨1, h⟩ = 1
sign_type.fin3_equiv._match_1 ⟨0, h⟩ = 0

source

theorem sign_type.nonneg_iff {a : sign_type} :

0 ≤ a ↔ a = 0 ∨ a = 1

source

theorem sign_type.nonneg_iff_ne_neg_one {a : sign_type} :

0 ≤ a ↔ a ≠ -1

source

theorem sign_type.neg_one_lt_iff {a : sign_type} :

-1 < a ↔ 0 ≤ a

source

theorem sign_type.nonpos_iff {a : sign_type} :

a ≤ 0 ↔ a = -1 ∨ a = 0

source

theorem sign_type.nonpos_iff_ne_one {a : sign_type} :

a ≤ 0 ↔ a ≠ 1

source

theorem sign_type.lt_one_iff {a : sign_type} :

a < 1 ↔ a ≤ 0

source

@[simp]

theorem sign_type.neg_iff {a : sign_type} :

a < 0 ↔ a = -1

source

@[simp]

theorem sign_type.le_neg_one_iff {a : sign_type} :

a ≤ -1 ↔ a = -1

source

@[simp]

theorem sign_type.pos_iff {a : sign_type} :

0 < a ↔ a = 1

source

@[simp]

theorem sign_type.one_le_iff {a : sign_type} :

1 ≤ a ↔ a = 1

source

@[simp]

theorem sign_type.neg_one_le (a : sign_type) :

-1 ≤ a

source

@[simp]

theorem sign_type.le_one (a : sign_type) :

a ≤ 1

source

@[simp]

theorem sign_type.not_lt_neg_one (a : sign_type) :

¬a < -1

source

@[simp]

theorem sign_type.not_one_lt (a : sign_type) :

¬1 < a

source

@[simp]

theorem sign_type.self_eq_neg_iff (a : sign_type) :

a = -a ↔ a = 0

source

@[simp]

theorem sign_type.neg_eq_self_iff (a : sign_type) :

-a = a ↔ a = 0

source

@[simp]

theorem sign_type.neg_one_lt_one :

-1 < 1

source

def sign_type.cast {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :

sign_type → α

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

source

@[protected, instance]

def sign_type.has_coe_t {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :

has_coe_t sign_type α

Equations

sign_type.has_coe_t = {coe := sign_type.cast _inst_3}

source

@[simp]

theorem sign_type.cast_eq_coe {α : Type u_1} [has_zero α] [has_one α] [has_neg α] (a : sign_type) :

a.cast = ↑a

source

@[simp]

theorem sign_type.coe_zero {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :

↑0 = 0

source

@[simp]

theorem sign_type.coe_one {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :

↑1 = 1

source

@[simp]

theorem sign_type.coe_neg_one {α : Type u_1} [has_zero α] [has_one α] [has_neg α] :

↑-1 = -1

source

@[simp]

theorem sign_type.cast_hom_apply {α : Type u_1} [mul_zero_one_class α] [has_distrib_neg α] (ᾰ : sign_type) :

⇑sign_type.cast_hom ᾰ = ᾰ.cast

source

def sign_type.cast_hom {α : Type u_1} [mul_zero_one_class α] [has_distrib_neg α] :

sign_type →*₀ α

sign_type.cast as a mul_with_zero_hom.

Equations

sign_type.cast_hom = {to_fun := sign_type.cast (neg_zero_class.to_has_neg α), map_zero' := _, map_one' := _, map_mul' := _}

source

theorem sign_type.range_eq {α : Type u_1} (f : sign_type → α) :

set.range f = {f sign_type.zero, f sign_type.neg, f sign_type.pos}

source

def sign {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] :

α →o sign_type

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

Equations

sign = {to_fun := λ (a : α), ite (0 < a) 1 (ite (a < 0) (-1) 0), monotone' := _}

source

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)

source

@[simp]

theorem sign_zero {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] :

⇑sign 0 = 0

source

@[simp]

theorem sign_pos {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} (ha : 0 < a) :

⇑sign a = 1

source

@[simp]

theorem sign_neg {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} (ha : a < 0) :

⇑sign a = -1

source

theorem sign_eq_one_iff {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} :

⇑sign a = 1 ↔ 0 < a

source

theorem sign_eq_neg_one_iff {α : Type u_1} [has_zero α] [preorder α] [decidable_rel has_lt.lt] {a : α} :

⇑sign a = -1 ↔ a < 0

source

@[simp]

theorem sign_eq_zero_iff {α : Type u_1} [has_zero α] [linear_order α] {a : α} :

⇑sign a = 0 ↔ a = 0

source

theorem sign_ne_zero {α : Type u_1} [has_zero α] [linear_order α] {a : α} :

⇑sign a ≠ 0 ↔ a ≠ 0

source

@[simp]

theorem sign_nonneg_iff {α : Type u_1} [has_zero α] [linear_order α] {a : α} :

0 ≤ ⇑sign a ↔ 0 ≤ a

source

@[simp]

theorem sign_nonpos_iff {α : Type u_1} [has_zero α] [linear_order α] {a : α} :

⇑sign a ≤ 0 ↔ a ≤ 0

source

@[simp]

theorem sign_one {α : Type u_1} [ordered_semiring α] [decidable_rel has_lt.lt] [nontrivial α] :

⇑sign 1 = 1

source

theorem sign_mul {α : Type u_1} [linear_ordered_ring α] (x y : α) :

⇑sign (x * y) = ⇑sign x * ⇑sign y

source

def sign_hom {α : Type u_1} [linear_ordered_ring α] :

α →*₀ sign_type

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

sign_hom = {to_fun := ⇑sign, map_zero' := _, map_one' := _, map_mul' := _}

source

theorem sign_pow {α : Type u_1} [linear_ordered_ring α] (x : α) (n : ℕ) :

⇑sign (x ^ n) = ⇑sign x ^ n

source

theorem left.sign_neg {α : Type u_1} [add_group α] [preorder α] [decidable_rel has_lt.lt] [covariant_class α α has_add.add has_lt.lt] (a : α) :

⇑sign (-a) = -⇑sign a

source

theorem right.sign_neg {α : Type u_1} [add_group α] [preorder α] [decidable_rel has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) :

⇑sign (-a) = -⇑sign a

source

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

source

theorem int.sign_eq_sign (n : ℤ) :

n.sign = ↑(⇑sign n)

source

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.

source

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.

mathlib3 documentation

Sign function #