Sequence of Partial Sums of Computable Real Sequence is Computable

== Theorem ==
Let $\sequence {x_m}_{m \in \N}$ be a computable real sequence.
Let $\sequence{y_N}_{N \in \N}$ be defined as:
:$\ds y_N = \sum_{m = 0}^{N - 1} x_m$
Then $\sequence{y_N}$ is a computable real sequence.
== Proof ==
By definition of computable real sequence, there exists a total recursive function $f : \N^2 \to \N$ such that, for all $m, p \in \N$:
:$\dfrac {k_{m,p} - 1} {p + 1} < x_m < \dfrac {k_{m,p} + 1} {p + 1}$
where $\map f {m, p}$ codes the integer $k_{m,p}$
Define $g: \N^2 \to \N$ as:
:$\ds \map g {N, p} = \map {\operatorname{quot}_\Z} {\sum_{m = 0}^{N - 1} \map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}} +_\Z N_\Z, \paren {2 N}_\Z}$
where $\map {f_\Z} {m, p}$ denotes the integer coded by $\map f {m, p}$.
We have that $g$ is total recursive by:
* Bounded Summation of Integers is Primitive Recursive
* Predecessor Function is Primitive Recursive
* Constant Function is Primitive Recursive
* Addition is Primitive Recursive
* Multiplication is Primitive Recursive
* Code Number for Non-Negative Integer is Primitive Recursive
* Addition of Integers is Primitive Recursive
* Quotient of Integers is Primitive Recursive
It remains to show that:
:$\ds \frac {\map g {N, p} - 1} {p + 1} < \sum_{m = 0}^{N - 1} x_m < \frac {\map g {N, p} + 1} {p + 1}$
If $N = 0$, every summation is empty, so:
:$y_N = 0_\Z$
:$\map g {0, p} = \map {\operatorname{quot}_\Z} {0, 0} = 0_\Z$
and we get:
:$\dfrac {-1} {p + 1} < 0 < \dfrac 1 {p + 1}$
trivially.
Therefore, we will suppose $N \ne 0$ for the remainder of the proof.
We have:
:$\map g {N, p} = \floor {\dfrac {\sum_{m = 0}^{N - 1} \map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}} + N} {2 N}}_\Z$
Therefore, by Floor is between Number and One Less:
:$\ds \sum_{m = 0}^{N - 1} \frac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}}} {2 N} - \frac 1 2 < \map {g_\Z} {N, p} \le \sum_{m = 0}^{N - 1} \frac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}}} {2 N} + \frac 1 2$
Or, alternatively:
:$\ds \map {g_\Z} {N, p} - 1 \le \sum_{m = 0}^{N - 1} \frac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}}} {2 N} - \frac 1 2$
:$\ds \sum_{m = 0}^{N - 1} \frac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}}} {2 N} + \frac 1 2 < \map {g_\Z} {N, p} + 1$
By definition of $f$, and for every $m \in \N$:
:$\dfrac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}} - 1} {\map {\operatorname{pred}} {2 N \paren {p + 1}} + 1} < x_m < \dfrac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}} + 1} {\map {\operatorname{pred}} {2 N \paren {p + 1}} + 1}$
Since we have assumed $N > 0$, that is equivalent to:
:$\dfrac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}} - 1} {2 N \paren {p + 1}} < x_m < \dfrac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}} + 1} {2 N \paren {p + 1}}$
By summing all of these inequalities up to $N - 1$, we get:
:$\ds \frac 1 {p + 1} \paren {\sum_{m = 0}^{N - 1} \frac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}}} {2 N} - \frac 1 2} < \sum_{m = 0}^{N - 1} x_m < \frac 1 {p + 1} \paren {\sum_{m = 0}^{N - 1} \frac {\map {f_\Z} {m, \map {\operatorname{pred}} {2 N \paren {p + 1}}}} {2 N} + \frac 1 2}$
But due to the inequalities earlier stated, we find:
:$\ds \frac 1 {p + 1} \paren {\map {g_\Z} {N, p} - 1} < \sum_{m = 0}^{N - 1} x_m < \frac 1 {p + 1} \paren {\map {g_\Z} {N, p} + 1}$
which is precisely what was to be shown.