Proof of Sequences of Real-Valued Maps: the Map of Pointwise Limits on a Subset, and the Sequence of Pointwise Partial Sums

Proof of (i). For $k\in\mathbb{N}$, the restriction $f_{k}|_{S}$ is a map $S\to\mathbb{R}$ with $(f_{k}|_{S})(p)=f_{k}(p)$ for every $p\in S$, by Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii). Let $F$ be the sequence $k\mapsto f_{k}|_{S}$ in $\mathbb{R}^{S}$, a map $\mathbb{N}\to\mathbb{R}^{S}$ by Sets and Maps: Ordinary Notation (v), and write $F_{k}=F(k)=f_{k}|_{S}$. For $p\in S$, the sequences $(F_{k}(p))_{k}$ and $(f_{k}(p))_{k}$ in $\mathbb{R}$ of The Sequences k ↦ f_k(p) of a Sequence in ℝ^I, and the Map of Their Limits (i) (for the index sets $S$ and $D$) have the same $k$-th term $F_{k}(p)=f_{k}(p)$ for every $k\in\mathbb{N}$, so they are equal by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv); in particular $(F_{k}(p))_{k}$ is convergent. By The Sequences k ↦ f_k(p) of a Sequence in ℝ^I, and the Map of Their Limits (iii), applied with $I=S$ to $F$, there is $L\in\mathbb{R}^{S}$, a map $L:S\to\mathbb{R}$, with $L(p)=\lim_{k\to\infty}F_{k}(p)=\lim_{k\to\infty}f_{k}(p)$ for every $p\in S$. If $L':S\to\mathbb{R}$ also satisfies $L'(p)=\lim_{k\to\infty}f_{k}(p)$ for every $p\in S$, then $L'(p)=L(p)$ for every $p\in S$, so $L'=L$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

Proof of (ii): existence of a recursive sequence. Let $\oplus$ be the binary operation on $\mathbb{R}^{D}$ of Pointwise Operations on Real-Valued Maps Exist and Are Unique (i) for $+$, so that $(u\oplus v)(x)=u(x)+v(x)$ for all $u,v\in\mathbb{R}^{D}$ and $x\in D$. For $n\in\mathbb{N}$, $n+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi), so $g_{n+1}\in\mathbb{R}^{D}$ and $u\oplus g_{n+1}\in\mathbb{R}^{D}$ for $u\in\mathbb{R}^{D}$; let $G:\mathbb{N}\times\mathbb{R}^{D}\to\mathbb{R}^{D}$ be the map $(n,u)\mapsto u\oplus g_{n+1}$ of Sets and Maps: Ordinary Notation (v). By Recursion on the Natural Numbers Starting at One (i), with the set $\mathbb{R}^{D}$, the element $g_{1}$ and the map $G$, there is a map $s:\mathbb{N}\to\mathbb{R}^{D}$, a sequence $(s_{n})_{n\in\mathbb{N}}$ in $\mathbb{R}^{D}$, with $s_{1}=g_{1}$ and $s_{n+1}=s_{n}\oplus g_{n+1}$ for every $n\in\mathbb{N}$.

The values of $s$. Fix $x\in D$, and let $a=(g_{k}(x))_{k}$ and $\tau=(s_{n}(x))_{n}$ be the sequences in $\mathbb{R}$ of The Sequences k ↦ f_k(p) of a Sequence in ℝ^I, and the Map of Their Limits (i), with terms $a_{k}=g_{k}(x)$ and $\tau(n)=s_{n}(x)$. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (i), for the addition of $\mathbb{R}$, there is a map $\sigma:\mathbb{N}\to\mathbb{R}$ with $\sigma(n)=\sum_{k=1}^{n}a_{k}$ for every $n\in\mathbb{N}$, the sum being that of the restriction $a|_{[n]}$ as in Iterated Operations: Finite Sums and Finite Products (ii). For $n\in\mathbb{N}$, $a|_{[n]}$ has the value $a_{k}=g_{k}(x)$ at each $k\in[n]$ by Domains and Restrictions of Maps (iii), so it is the map $k\mapsto g_{k}(x)$ on $[n]$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv), and $\sigma(n)=\sum_{k=1}^{n}g_{k}(x)$.

The map $\sigma$ satisfies $\sigma(1)=a_{1}$: by Iterated Operations: Finite Sums and Finite Products (i), $\sum_{k=1}^{1}a_{k}$ is the value at $1$ of the map of Iterating a Binary Operation along a Finite List (i) for $a|_{[1]}$, which is $a_{1}$. For $n\in\mathbb{N}$, $\sigma(n+1)=\sigma(n)+a_{n+1}$: the addition of $\mathbb{R}$ is associative and commutative with neutral element $0$, so Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii), with $m=1$, gives $\sum_{k=1}^{n+1}a_{k}=\Big(\sum_{k=1}^{n}a_{k}\Big)+a_{n+1}$ for the sums over intervals of Sums and Products over a Finite Set and over an Interval (iv), and these agree with the sums of Iterated Operations: Finite Sums and Finite Products (ii) by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (v), applied to $a|_{[n]}$ and $a|_{[n+1]}$.

The map $\tau$ satisfies the same two equations: $\tau(1)=s_{1}(x)=g_{1}(x)=a_{1}$, and for $n\in\mathbb{N}$, $\tau(n+1)=(s_{n}\oplus g_{n+1})(x)=s_{n}(x)+g_{n+1}(x)=\tau(n)+a_{n+1}$. Let $H:\mathbb{N}\times\mathbb{R}\to\mathbb{R}$ be the map $(n,t)\mapsto t+a_{n+1}$ of Sets and Maps: Ordinary Notation (v). Then $\sigma$ and $\tau$ are maps $\mathbb{N}\to\mathbb{R}$ with value $a_{1}$ at $1$ and $f(n+1)=H(n,f(n))$ for every $n\in\mathbb{N}$, for $f=\sigma$ and $f=\tau$; by the uniqueness in Recursion on the Natural Numbers Starting at One (i), $\tau=\sigma$. Hence $s_{n}(x)=\tau(n)=\sigma(n)=\sum_{k=1}^{n}g_{k}(x)$ for every $n\in\mathbb{N}$.

As $x\in D$ was arbitrary, $s_{n}(x)=\sum_{k=1}^{n}g_{k}(x)$ for all $n\in\mathbb{N}$ and $x\in D$. Moreover, for each $x\in D$, $(s_{n}(x))_{n}=\tau=\sigma$ is the map $n\mapsto\sum_{k=1}^{n}a_{k}$ on $\mathbb{N}$, whose $n$-th term is the $n$-th partial sum of $(a_{k})=(g_{k}(x))_{k}$ by Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (i), the finite sum there being read as in Sums and Products over a Finite Set and over an Interval (iv), which agrees with $\sigma(n)$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (v). So $(s_{n}(x))_{n}$ is the sequence of partial sums of $(g_{k}(x))_{k}$.

Uniqueness. Let $(s'_{n})_{n\in\mathbb{N}}$ be a sequence in $\mathbb{R}^{D}$ with $s'_{n}(x)=\sum_{k=1}^{n}g_{k}(x)$ for all $n\in\mathbb{N}$ and $x\in D$. For each $n\in\mathbb{N}$, $s'_{n}(x)=s_{n}(x)$ for every $x\in D$, so $s'_{n}=s_{n}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv); hence $s'=s$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv) again.