[proofplan]
We compare every finite tail of the function series with the corresponding finite tail of the numerical majorant series. The tail modulus for $\sum M_n$ gives, at each precision $2^{-k}$, a lower index after which all numerical tails are bounded by $2^{-k}$. The pointwise bounds $|f_n(x)| \leq M_n$ and the finite triangle inequality turn this into a uniform Cauchy estimate for the partial-sum functions. Completeness of the modulus-bearing Cauchy reals then constructs the pointwise limit, and the same uniform tail control gives [uniform convergence](/page/Uniform%20Convergence) to that limit.
[/proofplan]
[step:Define the partial sums as functions on $X$]
For each $N \in \mathbb{N}$, define the partial-sum function
\begin{align*}
S_N: X &\to \mathbb{R}
\end{align*}
\begin{align*}
x &\mapsto \sum_{n=1}^{N} f_n(x).
\end{align*}
For integers $m > N$ and a point $x \in X$, subtraction of finite sums gives
\begin{align*}
S_m(x) - S_N(x) = \sum_{n=N+1}^{m} f_n(x).
\end{align*}
Here the finite sum is taken in the constructive real field $\mathbb{R}$, with each rational $M_n$ viewed through the canonical embedding $\mathbb{Q} \to \mathbb{R}$ when compared with $|f_n(x)|$.
[/step]
[step:Bound every function tail by the corresponding majorant tail]
Fix $k \in \mathbb{N}$, choose $N \geq \mu(k)$, let $m > N$, and let $x \in X$. By the finite triangle inequality applied to the finite family $(f_n(x))_{n=N+1}^{m}$,
\begin{align*}
|S_m(x) - S_N(x)| \leq \sum_{n=N+1}^{m} |f_n(x)|.
\end{align*}
Using the hypothesis $|f_n(x)| \leq M_n$ for each $n \in \{N+1,\dots,m\}$ and monotonicity of finite sums over non-negative terms,
\begin{align*}
\sum_{n=N+1}^{m} |f_n(x)| \leq \sum_{n=N+1}^{m} M_n.
\end{align*}
Since $N \geq \mu(k)$, the defining property of the tail modulus $\mu$ gives
\begin{align*}
\sum_{n=N+1}^{m} M_n \leq 2^{-k}.
\end{align*}
Combining these inequalities yields
\begin{align*}
|S_m(x) - S_N(x)| \leq 2^{-k}.
\end{align*}
[guided]
The goal is to prove a uniform Cauchy estimate: after a sufficiently large lower index, every later partial sum must be close to every earlier partial sum, with a bound independent of $x \in X$. Fix a precision index $k \in \mathbb{N}$. The majorant series gives exactly the index we should use: take any $N \geq \mu(k)$, where $\mu$ is the given tail Cauchy modulus for $\sum M_n$.
Now fix an upper index $m > N$ and a point $x \in X$. The difference between the two partial sums is not mysterious; cancellation of the first $N$ terms gives
\begin{align*}
S_m(x) - S_N(x) = \sum_{n=N+1}^{m} f_n(x).
\end{align*}
Taking absolute values and applying the finite triangle inequality to the constructive [real numbers](/page/Real%20Numbers) gives
\begin{align*}
|S_m(x) - S_N(x)| \leq \sum_{n=N+1}^{m} |f_n(x)|.
\end{align*}
This is the step where the pointwise majorization hypothesis enters. For every index $n$ and every point $x \in X$, the theorem assumes $|f_n(x)| \leq M_n$. Applying this for each $n \in \{N+1,\dots,m\}$, and using monotonicity of finite sums, gives
\begin{align*}
\sum_{n=N+1}^{m} |f_n(x)| \leq \sum_{n=N+1}^{m} M_n.
\end{align*}
Finally, because $N \geq \mu(k)$ and $m > N$, the definition of $\mu$ as a tail Cauchy modulus gives
\begin{align*}
\sum_{n=N+1}^{m} M_n \leq 2^{-k}.
\end{align*}
Putting the three estimates together,
\begin{align*}
|S_m(x) - S_N(x)| \leq 2^{-k}.
\end{align*}
The important point is that the final bound does not depend on $x$. That independence is precisely what turns pointwise Cauchy control into uniform Cauchy control.
[/guided]
[/step]
[step:Conclude that the partial sums are uniformly Cauchy with the inherited modulus]
The preceding estimate proves that for every $k \in \mathbb{N}$, every $N \geq \mu(k)$, every $m > N$, and every $x \in X$,
\begin{align*}
|S_m(x) - S_N(x)| \leq 2^{-k}.
\end{align*}
Thus the sequence of functions $(S_N)_{N \in \mathbb{N}}$ is uniformly Cauchy on $X$ with modulus $\mu$.
[/step]
[step:Use completeness to construct the limit function]
For each fixed $x \in X$, the sequence of constructive real numbers $(S_N(x))_{N \in \mathbb{N}}$ is Cauchy with modulus $\mu$, because the uniform Cauchy estimate applies in particular at that point $x$. By the completeness principle for modulus-bearing Cauchy reals (citing a result not yet in the wiki: Completeness of constructive reals), there exists a constructive real number, denoted $S(x)$, which is the limit of $(S_N(x))_{N \in \mathbb{N}}$.
Define
\begin{align*}
S: X &\to \mathbb{R}
\end{align*}
\begin{align*}
x &\mapsto \lim_{N \to \infty} S_N(x),
\end{align*}
where the limit is the one supplied by completeness from the Cauchy modulus $\mu$. Since the same modulus $\mu$ works for every $x \in X$, the construction of $S(x)$ is uniform in $x$.
[/step]
[step:Recover uniform convergence from the same tail estimate]
Let $k \in \mathbb{N}$ and choose $N \geq \mu(k+1)$. For every $x \in X$ and every $m > N$, the uniform Cauchy estimate gives
\begin{align*}
|S_m(x) - S_N(x)| \leq 2^{-(k+1)}.
\end{align*}
Passing to the limit in the constructive real variable $S_m(x)$ as $m \to \infty$, using the limit $S(x)$ constructed from completeness, gives
\begin{align*}
|S(x) - S_N(x)| \leq 2^{-k}.
\end{align*}
Thus $S_N \to S$ uniformly on $X$. In particular, the map
\begin{align*}
\nu: \mathbb{N} &\to \mathbb{N}
\end{align*}
\begin{align*}
k &\mapsto \mu(k+1)
\end{align*}
is a uniform convergence modulus computable from the given tail modulus $\mu$. Therefore the series $\sum_{n=1}^{\infty} f_n$ converges uniformly on $X$ to $S$, as claimed.
[/step]
