Sum of Computable Real Sequences is Computable/Proof 2

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 Computable Real Sequence iff Limits of Computable Rational Sequences, there exist:

such that:

$\forall m, p \in \N: \forall n \ge \map {\psi_x} {m, p}: \size {a_{\map {\phi_x} {m, n}} - x_m} < \dfrac 1 {p + 1}$
$\forall m, p \in \N: \forall n \ge \map {\psi_y} {m, p}: \size {a_{\map {\phi_y} {m, n}} - y_m} < \dfrac 1 {p + 1}$


By Computable Subsequence of Computable Rational Sequence is Computable/Corollary, there exist:

Computable rational sequences $\sequence {a'_k}, \sequence {b'_k}$

such that, for all $m, n \in \N$:

$a_{\map {\phi_x} {m, n}} = a'_{\map \pi {m, n}}$
$b_{\map {\phi_y} {m, n}} = b'_{\map \pi {m, n}}$

By Sum of Computable Rational Sequences is Computable:

$\sequence {a'_k + b'_k}$

is a computable rational sequence.

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

$\map \psi {m, p} = \map \max {\map {\psi_x} {m, 2 p + 1}, \map {\psi_y} {m, 2 p + 1}}$

which is total recursive by:

If we can show:

$\forall m, p \in \N: \forall n \ge \map \psi {m, p}: \size {\paren {a'_{\map \pi {m, n}} + b'_{\map \pi {m, n}}} - \paren {x_m - y_m}} < \dfrac 1 {p + 1}$

then the result will follow by Computable Real Sequence iff Limits of Computable Rational Sequences.


Let $m, n, p \in \N$ be arbitrary, and suppose that $n \ge \map \psi {m, p}$.

Then:

$n \ge \map {\psi_x} {m, 2 p + 1}$
$n \ge \map {\psi_y} {m, 2 p + 1}$

Thus, by assumption, we have:

$\size {a_{\map {\phi_x} {m, n}} - x_m} < \dfrac 1 {2 p + 2}$
$\size {b_{\map {\phi_y} {m, n}} - y_m} < \dfrac 1 {2 p + 2}$

Hence:

\(\ds \size {\paren {a'_{\map \pi {m, n} } + b'_{\map \pi {m, n} } } - \paren {x_m - y_m} }\) \(=\) \(\ds \size {\paren {a'_{\map \pi {m, n} } - x_m} + \paren {b'_{\map \pi {m, n} } - y_m} }\)
\(\ds \) \(\le\) \(\ds \size {a'_{\map \pi {m, n} } - x_m} + \size {b'_{\map \pi {m, n} } - y_m}\) Triangle Inequality for Real Numbers
\(\ds \) \(=\) \(\ds \size {a_{\map {\phi_x} {m, n} } - x_m} + \size {b_{\map {\phi_y} {m, n} } - y_m}\) Definitions of $\sequence {a'_k}, \sequence {b'_k}$
\(\ds \) \(<\) \(\ds \frac 1 {2 p + 2} + \frac 1 {2 p + 2}\) Above
\(\ds \) \(=\) \(\ds \frac 1 {p + 1}\)

$\blacksquare$