Proof of Real Sums over a Finite Index Set: Comparison, Nonnegativity, Monotonicity, Term Bounds, Absolute Values, Counting and Limits

Each result cited is universally quantified over the data in its own statement, and is applied here to the data named.

Claim 1 (An enumeration of $G$). Since $G$ is nonempty and finite, Finite Set gives a natural number $p$ such that $G$ has $p$ elements, and that definition then supplies a bijection $\varphi:[p]\to G$, where $[p]$ is the initial segment determined by $p$. By Sum over a Finite Index Set, for every map $u:G\to\mathbb{R}$,

$$\sum_{x\in G}u(x)=\sum_{k=1}^{p}u\bigl(\varphi(k)\bigr).$$

Claim 2 (Clause 1). Suppose $h(x)\le h'(x)$ for every $x\in G$. Then $h(\varphi(k))\le h'(\varphi(k))$ for every $k\in[p]$, because $\varphi(k)\in G$. By claim 1 of Comparison and Absolute Value Bounds for Finite Sums of Real Numbers,

$$\sum_{k=1}^{p}h\bigl(\varphi(k)\bigr)\le\sum_{k=1}^{p}h'\bigl(\varphi(k)\bigr),$$

and claim 1 identifies the two sides with $\sum_{x\in G}h(x)$ and $\sum_{x\in G}h'(x)$.

Claim 3 (Clause 2). Suppose $0\le h(x)$ for every $x\in G$. Each summand satisfies $0\le h(\varphi(k))$, because $\varphi(k)\in G$. Hence $0\le\sum_{k=1}^{p}h(\varphi(k))$ by claim 5 of Properties of Finite Sums, and claim 1 identifies that sum with $\sum_{x\in G}h(x)$.

Claim 4 (Clause 3). Suppose $0\le h(x)$ for every $x\in G$, and let $E\subseteq G$ be nonempty.

Suppose first $E=G$. Then the two sums are the same real number, and $t\le t$ for every real $t$ because the order of $\mathbb{R}$ is a total order, hence reflexive.

Suppose now $E\ne G$, and put $E'=G\setminus E$, which is nonempty because $E\subseteq G$ and $E\ne G$. Both $E$ and $E'$ are finite by claim 3 of Basic Properties of Finite Sets, applied to the finite set $G$ and to each of them. They are disjoint and their union is $G$, so claim 3 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set, applied to $G$, to $E$, to $E'$ and to $h$, gives

$$\sum_{x\in G}h(x)=\sum_{x\in E}h(x)+\sum_{x\in E'}h(x).$$

The restriction of $h$ to $E'$ is nonnegative at every point of $E'$, so clause 2, proved in claim 3 and applied to the nonempty finite set $E'$ and to that restriction, gives $0\le\sum_{x\in E'}h(x)$. Since

$$\sum_{x\in G}h(x)-\sum_{x\in E}h(x)=\sum_{x\in E'}h(x),$$

claim 3 of Elementary Arithmetic in an Ordered Field yields $\sum_{x\in E}h(x)\le\sum_{x\in G}h(x)$.

Claim 5 (Clause 4). Suppose $0\le h(x)$ for every $x\in G$, and let $y\in G$. The singleton $\{y\}$ is a nonempty subset of $G$, so clause 3, proved in claim 4, gives $\sum_{x\in\{y\}}h(x)\le\sum_{x\in G}h(x)$. By claim 1 of Peeling, Splitting, and Interchange for Sums over a Finite Index Set, applied to the restriction of $h$ to $\{y\}$, the left-hand side is $h(y)$.

Claim 6 (Clause 5). Let $|h|$ denote the map $x\mapsto|h(x)|$ on $G$. Claim 1, applied to $h$ and to $|h|$ with the same bijection $\varphi$, gives

$$\sum_{x\in G}h(x)=\sum_{k=1}^{p}h\bigl(\varphi(k)\bigr),\qquad\sum_{x\in G}|h(x)|=\sum_{k=1}^{p}\bigl|h\bigl(\varphi(k)\bigr)\bigr|.$$

Claim 2 of Comparison and Absolute Value Bounds for Finite Sums of Real Numbers, applied with $n=p$ and $a_{k}=h(\varphi(k))$, says that the absolute value of the first right-hand side is at most the second.

Claim 7 (Clause 6). As in the statement, a natural number $m$ is read in $\mathbb{R}$ as $\iota(m)$, where $\iota$ is the canonical map. Let $e:\mathbb{N}\to\mathbb{R}$ be the map with constant value $1$. The sum $\sum_{k=1}^{m}1$ is the finite sum of $e$ over $[m]$, whose value does not depend on the map extending the summands, by claim 1 of Properties of Finite Sums. Let $A$ be the set of $m\in\mathbb{N}$ with $\sum_{k=1}^{m}e(k)=\iota(m)$. By claim 1 of Properties of Finite Sums and claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field, $\sum_{k=1}^{1}e(k)=e(1)=1=\iota(1)$, so $1\in A$. Let $m\in A$ and let $S$ be the successor map. By claim 1 of Properties of Finite Sums, applied over $[S(m)]$ (which contains $S(m)$ by reflexivity, claim 1 of Properties of the Order on the Natural Numbers), $\sum_{k=1}^{S(m)}e(k)=\sum_{k=1}^{m}e(k)+1=\iota(m)+1$. Since $S(m)=m+1$ by claim 1 of Arithmetic of Addition on the Natural Numbers, claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field gives $\iota(m)+1=\iota(S(m))$, so $S(m)\in A$. By Principle of Induction for the Natural Numbers, applied to $A$, we get $A=\mathbb{N}$.

Now let $q$ be the number of elements of $G$ assumed in clause 6, where it is written $p$; the letter $p$ is already taken here by claim 1. Since $G$ also has $p$ elements (claim 1), $q=p$ by Uniqueness of the Number of Elements. Claim 1, applied to the map on $G$ with constant value $1$, together with $A=\mathbb{N}$, gives $\sum_{x\in G}1=\sum_{k=1}^{p}e(k)=\iota(p)=\iota(q)$.

Claim 8 (Clause 7). For each $m\in\mathbb{N}$, claim 1, applied to the map $x\mapsto a_{x,m}$, gives $\sum_{x\in G}a_{x,m}=\sum_{k=1}^{p}a_{\varphi(k),m}$. Applied to $x\mapsto A_{x}$, it gives $\sum_{x\in G}A_{x}=\sum_{k=1}^{p}A_{\varphi(k)}$. For each $k\in[p]$ the sequence $(a_{\varphi(k),m})_{m\in\mathbb{N}}$ converges to $A_{\varphi(k)}$, because $\varphi(k)\in G$. Since $p\le p$ by claim 1 of Properties of the Order on the Natural Numbers, we have $p\in[p]$. Then Finite Sums of Real Numbers: Nonnegativity, Domination by the Sum, and Limits §limit, applied with $N=p$ and $j=p$, shows that $\sum_{k=1}^{p}a_{\varphi(k),m}$ converges to $\sum_{k=1}^{p}A_{\varphi(k)}$ as $m\to\infty$. This is the assertion.