exists_signed_sum
theorem exists_signed_sum :
∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (f : α → ℤ),
∃ β x sgn g,
(∀ (b : β), g b ∈ s) ∧
(Fintype.card β = s.sum fun a => (f a).natAbs) ∧
∀ a ∈ s, (Finset.univ.sum fun b => if g b = a then ↑(sgn b) else 0) = f a
This theorem states that for any finite set `s` of a type `α` with decidable equality, and for any function `f` from `α` to integers, there exist a type `β`, an element `x`, a function `sgn`, and a function `g`, such that for all `b` in `β`, `g b` belongs to `s`, the cardinality of `β` is equal to the sum of the absolute values of `f a` for all `a` in `s`, and for each `a` in `s`, the sum over all `b` in the universal finite set of `β` of the value 1 if `g b` equals `a` and 0 otherwise, multiplied by the sign of `b`, is equal to `f a`. In other words, it assures that an integer sum can be decomposed into a finite sum of signed unit quantities.
More concisely: For any finite set `s` of a type `α` with decidable equality and any function `f` from `α` to integers, there exist a type `β`, an element `x` of `β`, a function `sgn : β -> {-1, 0, 1}`, and a function `g : β -> s`, such that for all `a in s`, the sum over all `b in β` of `sgn b * (1 if g(b) = a else 0)` equals `f a`.
|
sign_pos
theorem sign_pos :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableRel fun x x_1 => x < x_1] {a : α},
0 < a → SignType.sign a = 1
This theorem, named `sign_pos`, states that for any type `α` that has a zero, a preorder (a binary relation that is reflexive and transitive), and a decidable relation for less than, if a certain element `a` of type `α` is greater than zero, then the sign of `a` is 1. The sign is determined by the `SignType.sign` function, which assigns 1 if the element is positive, -1 if it is negative, and 0 otherwise.
More concisely: If `α` is a type with a zero, a preorder, and decidable less-than relation, then for any `a` of type `α` with `a > 0`, `SignType.sign a = 1`.
|
exists_signed_sum'
theorem exists_signed_sum' :
∀ {α : Type u_1} [inst : Nonempty α] [inst : DecidableEq α] (s : Finset α) (f : α → ℤ) (n : ℕ),
(s.sum fun i => (f i).natAbs) ≤ n →
∃ β x sgn g,
(∀ (b : β), g b ∉ s → sgn b = 0) ∧
Fintype.card β = n ∧ ∀ a ∈ s, (Finset.univ.sum fun i => if g i = a then ↑(sgn i) else 0) = f a
The theorem `exists_signed_sum'` states the following:
For any type `α` that is nonempty and has decidable equality, given a finite set `s` of type `α`, a function `f` mapping from `α` to integers, and a natural number `n`, if the sum of the absolute values of the function `f` over the set `s` is less than or equal to `n`, then there exists a type `β`, a value `x`, a sign function `sgn`, and a function `g`, such that the following conditions hold:
- For every element `b` of `β`, if `g b` is not in the set `s`, then the sign of `b` is 0.
- The number of elements in `β` is `n`.
- For every element `a` in `s`, the sum over all elements in the universal set of `β` (which we assume is finite), of the function that gives the sign of `i` if `g i` equals `a`, and 0 otherwise, equals the value of `f` at `a`.
In other words, this theorem says that we can decompose a sum of absolute values less than `n` into a sum of at most `n` signs.
More concisely: Given a nonempty type `α` with decidable equality, a finite set `s` of `α`, a function `f : α → ℤ`, and a natural number `n`, if the absolute value sum of `f` over `s` is less than or equal to `n`, then there exist a set `β` with `n` elements, a sign function `sgn : β → {0,1,-1}`, and a function `g : β → α`, such that for all `a ∈ s`, the sum over all `i ∈ β` of `sgn i ⋅ (if g i = a then 1 else 0)` equals `f a`.
|
sign_one
theorem sign_one :
∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : DecidableRel fun x x_1 => x < x_1] [inst_2 : Nontrivial α],
SignType.sign 1 = 1
The theorem `sign_one` states that for any ordered semiring `α` in which a less than relation is decidable, and which is non-trivial (i.e., not all elements are equal), the sign of the number 1 is 1. This function `SignType.sign` gives the sign of an element: it returns 1 if the element is positive, -1 if it's negative, and 0 if it's neither (i.e., it's zero). According to this theorem, the sign of the number 1 in such a semiring is always 1.
More concisely: In any decidably ordered non-trivial semiring, the sign of 1 is 1.
|
sign_zero
theorem sign_zero :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableRel fun x x_1 => x < x_1],
SignType.sign 0 = 0
This theorem, `sign_zero`, states that for any type `α` that has a zero element and a preorder relation (i.e., a relation that is reflexive and transitive), and for which the relation `x < x_1` is decidable, the sign of the zero element is zero. In mathematical terms, it says that the sign of zero is zero.
More concisely: If `α` is a type with a zero element and a decidable preorder relation where `x < x_1` holds, then the sign of the zero element is zero.
|
sign_apply
theorem sign_apply :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : 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
The theorem `sign_apply` states that for any type `α` which has a zero element and a preorder relation (a binary relation that is reflexive and transitive), and for which it is decidable whether one element is less than another, the sign of any element `a` from `α` is determined as follows: if `a` is greater than zero, then the sign is `1`; if `a` is less than zero, then the sign is `-1`; if `a` is neither greater than nor less than zero, then the sign is `0`.
More concisely: For any type with a zero element and a decidable preorder relation, the sign function maps elements greater than zero to 1, elements less than zero to -1, and zero to 0.
|
sign_neg
theorem sign_neg :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableRel fun x x_1 => x < x_1] {a : α},
a < 0 → SignType.sign a = -1
The theorem `sign_neg` states that for any type `α` that has a zero, a defined ordering relation, and a decidable relation for whether one element is less than another, if an element `a` of this type is less than zero, then the sign of `a` is `-1`. In other words, this theorem asserts that the `SignType.sign` function will return `-1` for all negative elements in any ordered set where "less than" is a decidable relation.
More concisely: For any type with a zero, ordering relation, and decidable less-than relation, the sign of an element less than zero is -1.
|
Left.sign_neg
theorem Left.sign_neg :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [inst_2 : DecidableRel fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α),
SignType.sign (-a) = -SignType.sign a
This theorem states that for any element 'a' of type 'α', where 'α' is an additive group and has a preorder relation under which it is covariant, the sign of the negation of 'a' is the negation of the sign of 'a'. This means that if 'a' is positive, negative, or zero under this ordering, then negative 'a' will be negative, positive, or zero respectively. Here, the concept of positivity and negativity is defined using the `SignType.sign` function, which assigns 1 to positive elements, -1 to negative elements, and 0 to zero.
More concisely: For any element 'a' in an additive group with covariant preorder, the sign of -a is the negation of the sign of a.
|
sign_eq_zero_iff
theorem sign_eq_zero_iff :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a : α}, SignType.sign a = 0 ↔ a = 0
This theorem states that for any type `α` which has zero element and supports linear order operations, the `SignType.sign` of an element `a` of type `α` is equal to zero if and only if the element `a` itself is zero. In other words, a value in a linearly ordered type has a sign of zero precisely when it is zero. This theorem provides a bi-directional implication relationship between a value being zero and its sign being zero.
More concisely: For any linearly ordered type with a zero element, the sign of an element is zero if and only if the element is zero.
|