Proof of Finite Sums of Real-Valued Maps: Continuity, Integral and Derivative

The common argument. Let $D$ be a set. By Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation (i), $\mathbb{R}^{D}$ with the sum $+$ of Pointwise Operations on Real-Valued Maps (i) and the constant map $0$ of Pointwise Operations on Real-Valued Maps (ii) is a commutative ring, so $+$ is an associative and commutative binary operation on $\mathbb{R}^{D}$ with neutral element $0$; the addition of $\mathbb{R}$ is associative and commutative with neutral element $0$. For a family $(f_{j})_{j\in J}$ of maps $D\to\mathbb{R}$, let $\Sigma$ be the sum of the $f_{j}$ formed in $\mathbb{R}^{D}$. By Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation (vi), $\Sigma(p)=\sum_{j\in J}f_{j}(p)$ for every $p\in D$, so $\Sigma$ is the map $\sum_{j\in J}f_{j}$ of the statement, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

Let now $G\subseteq\mathbb{R}^{D}$ be a set with $0\in G$ and $g+h\in G$ for all $g,h\in G$. Then $+$ restricted to $G\times G$ is a binary operation on $G$, associative and commutative with neutral element $0$ as $+$ is so on $\mathbb{R}^{D}$, and the inclusion $\iota:G\to\mathbb{R}^{D}$, $g\mapsto g$, satisfies $\iota(0)=0$ and $\iota(g+h)=\iota(g)+\iota(h)$. Let $f_{j}\in G$ for every $j\in J$, so that $j\mapsto f_{j}$ is a map from $J$ to $G$, and let $\Sigma_{G}$ be the sum of the $f_{j}$ formed in $G$. By Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set (ii), $\Sigma_{G}\in G$, and by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi), applied to $\iota$, $\Sigma_{G}=\iota(\Sigma_{G})=\Sigma$. Hence:

(A) $\Sigma\in G$;

(B) if $\Phi:G\to\mathbb{R}$ is a map with $\Phi(0)=0$ and $\Phi(g+h)=\Phi(g)+\Phi(h)$ for all $g,h\in G$, then $\Phi(\Sigma)=\Phi(\Sigma_{G})=\sum_{j\in J}\Phi(f_{j})$, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi) applied to $\Phi$.

Proof of (i). Take $D=S$, and let $G=C_{s_{0}}(S,d)$ of A Predicative Formula for Continuity at a Point, and the Set of Real-Valued Maps Continuous at a Point (ii): a subset of $\mathbb{R}^{S}$ whose elements are the maps $S\to\mathbb{R}$ that are continuous at $s_{0}$ relative to $S$. By Continuity of Sums and Products of Real-Valued Functions on a Metric Space (i) with $b=0$, $0\in G$, and by Continuity of Sums and Products of Real-Valued Functions on a Metric Space (ii), whose $f+g$ is the sum of Pointwise Operations on Real-Valued Maps (i), $g+h\in G$ for $g,h\in G$. As every $f_{j}$ lies in $G$, (A) shows that $\sum_{j\in J}f_{j}$ is continuous at $s_{0}$ relative to $S$.

Proof of (ii). Take $D=E$, and let $G$ be the set of $g\in\mathbb{R}^{E}$ such that $\int_{u}^{v}g$ is defined. It is a set: in the formula of A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i), $u$ and $v$ may be replaced by parameters with their present values, the result being predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i), and with $z$ existentially quantified (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)) it expresses a predicative condition on $g$, which for $g\in\mathbb{R}^{E}$ says that $\int_{u}^{v}g$ is defined; so $G$ is a set by Sets and Maps: Ordinary Notation (iii); let $\Phi:G\to\mathbb{R}$ be the map $g\mapsto\int_{u}^{v}g$, formed by A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v).

Closure. Let $g,h\in G$ and $c\in\mathbb{R}$; we show $g+h\in G$, $cg\in G$, $\Phi(g+h)=\Phi(g)+\Phi(h)$ and $\Phi(cg)=c\,\Phi(g)$, with the sum and scalar multiple of Pointwise Operations on Real-Valued Maps (i). If $u=v$, then $\int_{u}^{u}(g+h)$ and $\int_{u}^{u}cg$ are defined by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii), and all integrals from $u$ to $u$ equal $0$ by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vii), with $0=0+0=c\cdot0$. If $u<v$, then by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii), $[u,v]\subseteq E$ and $g$ and $h$ are integrable on $[u,v]$, that is, by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), $g|_{[u,v]}$ and $h|_{[u,v]}$ are bounded and integrable on $[u,v]$. As $(g+h)|_{[u,v]}=g|_{[u,v]}+h|_{[u,v]}$ and $(cg)|_{[u,v]}=c\,g|_{[u,v]}$, Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants (i) and Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants (ii) show that these restrictions are bounded and integrable on $[u,v]$ with integrals $\int_{u}^{v}g+\int_{u}^{v}h$ and $c\int_{u}^{v}g$; so $g+h$ and $cg$ are integrable on $[u,v]$ with these integrals by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), and $g+h,cg\in G$ by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii). If $v<u$, then by the third case of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii), $[v,u]\subseteq E$ and $g$ and $h$ are integrable on $[v,u]$; the case just treated, with $u$ and $v$ exchanged, shows that $g+h$ and $cg$ are integrable on $[v,u]$ with $\int_{v}^{u}(g+h)=\int_{v}^{u}g+\int_{v}^{u}h$ and $\int_{v}^{u}cg=c\int_{v}^{u}g$. So $g+h,cg\in G$ by the third case of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii), and The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vii), with Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field (ii), gives the values $\int_{u}^{v}(g+h)=-\int_{v}^{u}(g+h)=-\int_{v}^{u}g-\int_{v}^{u}h=\int_{u}^{v}g+\int_{u}^{v}h$ and $\int_{u}^{v}cg=-c\int_{v}^{u}g=c\int_{u}^{v}g$.

Conclusion. As $J\neq\emptyset$, there is $j_{0}\in J$, and $f_{j_{0}}\in G$. By Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation (iv), $0=0f_{j_{0}}$, so by the closure $0\in G$ and $\Phi(0)=0\cdot\Phi(f_{j_{0}})=0$ (Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field (i)); and $G$ is closed under $+$, with $\Phi(g+h)=\Phi(g)+\Phi(h)$. By the closure, $c_{j}f_{j}\in G$ with $\Phi(c_{j}f_{j})=c_{j}\int_{u}^{v}f_{j}$ for every $j\in J$. Apply the common argument to the family $j\mapsto c_{j}f_{j}$, a map from $J$ to $\mathbb{R}^{E}$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v)): its sum $\Sigma$ in $\mathbb{R}^{E}$ satisfies $\Sigma(t)=\sum_{j\in J}(c_{j}f_{j})(t)=\sum_{j\in J}c_{j}f_{j}(t)$ for $t\in E$, by Pointwise Operations on Real-Valued Maps (i), so $\Sigma$ is the map $t\mapsto\sum_{j\in J}c_{j}f_{j}(t)$; by (A), $\Sigma\in G$, that is, its integral from $u$ to $v$ is defined; and by (B), $\int_{u}^{v}\Sigma=\Phi(\Sigma)=\sum_{j\in J}c_{j}\int_{u}^{v}f_{j}$.

Proof of (iii). Take $D=I$, and let $G$ be the set of $g\in\mathbb{R}^{I}$ that are differentiable at $t$, that is, have a derivative at $t$. It is a set: in the formula of Predicative Formulas for the Derivative Condition and for Powers (i), with $g$ for $h$, the variable $x$ may be replaced by a parameter with the value $t$, the result being predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i), and with $L$ existentially quantified (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)) it expresses a predicative condition on $g$, which for $g\in\mathbb{R}^{I}$ says that $g$ has a derivative at $t$; so $G$ is a set by Sets and Maps: Ordinary Notation (iii). For $g\in G$, $g'(t)$ is the unique derivative of $g$ at $t$, by Derivative of a Real Function on an Interval (ii), and $\Phi:G\to\mathbb{R}$, $g\mapsto g'(t)$, is a map formed by Predicative Formulas for the Derivative Condition and for Powers (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v). By Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers (i) with $b=0$, $0\in G$ and $\Phi(0)=0$; by Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers (iv), $g+h\in G$ and $\Phi(g+h)=\Phi(g)+\Phi(h)$ for $g,h\in G$. As every $f_{j}$ lies in $G$, (A) shows that $\sum_{j\in J}f_{j}$ is differentiable at $t$, and (B) that its derivative at $t$ is $\Phi\bigl(\sum_{j\in J}f_{j}\bigr)=\sum_{j\in J}f_{j}'(t)$.