Properties of Finite Sums

Let $K$ be a field. Let $\mathbb{N}$ be the set of natural numbers with successor map $S$ as in that definition, ordered by the relation $\le$ of that definition, let $n\in\mathbb{N}$, and let $[n]$ be the initial segment determined by $n$, that is, the set of natural numbers $k$ with $k\le n$; every such $k$ also satisfies $1\le k$ by claim 4 of Properties of the Order on the Natural Numbers, so $[n]$ is the set of natural numbers $k$ with $1\le k\le n$. Let $a:[n]\to K$ and $b:[n]\to K$ be maps, with values written $a_{k}$ and $b_{k}$, and let $\lambda\in K$. All sums below are the finite sums of that definition.

Two different order relations occur below. In index ranges such as $1\le k\le n$ the symbol $\le$ is the order on $\mathbb{N}$ just cited; in claims 5 and 6 it is the order of the ordered field of real numbers. Then the following hold.

1. (Restriction and recursion) If $j\in[n]$ and $a'$ denotes the restriction of $a$ to $[j]$, then

so the value of a finite sum does not depend on which family extending the summands is used to form it. Moreover

2. (Additivity)

3. (Homogeneity)

4. (Conjugation) If $K$ is the field of complex numbers, then, with the complex conjugate,

5. (Nonnegative summands) If $K$ is the field of real numbers, with the order $\le$ of its ordered field structure, and $0\le a_{k}$ for every $k\in[n]$, then

and if in addition $\sum_{k=1}^{n}a_{k}=0$, then $a_{k}=0$ for every $k\in[n]$.

6. (Each summand is at most the sum) Under the hypotheses of claim 5,

7. (A single possibly nonzero summand) Let $i\in[n]$ and suppose that $a_{k}=0$ for every $k\in[n]$ with $k\ne i$. Then