Sum of Computable Real Sequences is Computable/Proof 1

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\sequence {x_n}$ and $\sequence {y_n}$ be computable real sequences.

Then $\sequence {x_n + y_n}$ is a computable real sequence.


Proof

By definition, there exist total recursive $f,g : \N^2 \to \N$ such that:

For every $m,n \in \N$, $\map f {m, n}$ and $\map g {m, n}$ respectively code integers $k$ and $\ell$ such that:
$\dfrac {k - 1} {n + 1} < x_m < \dfrac {k + 1} {n + 1}$
$\dfrac {\ell - 1} {n + 1} < y_m < \dfrac {\ell + 1} {n + 1}$

Define $h : \N^2 \to \N$ as:

$\map h {m, n} = \map {\operatorname{quot}_\Z} {\map f {m, 4 n + 3} +_\Z \map g {m, 4 n + 3} +_\Z 2, 4_\Z}$

which is total recursive by:


Now, let $m, n \in \N$ be arbitrary.

Let $k'$ and $\ell'$ be the integers coded by $\map f {m, 4 n + 3}$ and $\map g {m, 4 n + 3}$, respectively.

Then, $\map h {m, n} = \floor {\dfrac {k' + \ell' + 2} 4}$.

Thus, by Floor is between Number and One Less:

$\dfrac {k' + \ell' - 2} 4 < \map h {m, n} \le \dfrac {k' + \ell' + 2} 4$

Hence:

$\map h {m, n} - 1 \le \dfrac {k' + \ell' - 2} 4$
$\dfrac {k' + \ell' + 2} 4 < \map h {m, n} + 1$

From the inequalities above, we have:

\(\ds \dfrac {k' - 1} {\paren {4 n + 3} + 1} + \dfrac {\ell' - 1} {\paren {4 n + 3} + 1}\) \(<\) \(\, \ds x_m + y_m \, \) \(\, \ds < \, \) \(\ds \dfrac {k' + 1} {\paren {4 n + 3} + 1} + \dfrac {\ell' + 1} {\paren {4 n + 3} + 1}\)
\(\ds \dfrac {k' + \ell' - 2} {4 n + 4}\) \(<\) \(\, \ds x_m + y_m \, \) \(\, \ds < \, \) \(\ds \dfrac {k' + \ell' + 2} {4 n + 4}\)
\(\ds \dfrac {\map h {m, n} - 1} {n + 1}\) \(<\) \(\, \ds x_m + y_m \, \) \(\, \ds < \, \) \(\ds \dfrac {\map h {m, n} + 1} {n + 1}\)

Thus, $\sequence {x_n + y_n}$ is computable by definition.

$\blacksquare$

Retrieved from "https://proofwiki.org/w/index.php?title=Sum_of_Computable_Real_Sequences_is_Computable/Proof_1&oldid=650354"