Condition for Limits of Computable Real Sequences to be Computable

Theorem

Let $\sequence {x_k}_{k \in \N}$ be a computable real sequence.

Let $\sequence {y_n}_{n \in \N}$ be a real sequence.

If there exists total recursive function $\phi : \N^2 \to \N$ such that:

$\forall n, p \in \N: \size {x_{\map \phi {n, p}} - y_n} < \dfrac 1 {p + 1}$

then:

$\sequence {y_n}_{n \in \N}$

$\size {a_{\map \pi {k, p} } - x_k} < \dfrac 1 {p + 1}$

Let $\psi : \N^2 \to \N$ be defined as:

$\map \psi {n, p} = \map \pi {\map \phi {n, 2 p + 1}, 2 p + 1}$

$b_{\map \pi {n, p}} = a_{\map \psi {n, p}}$

We have, for all $n, p \in \N$:

$\ds \size {b_{\map \pi {n, p} } - y_n}$

$=$

$\ds \size {a_{\map \psi {n, p} } - y_n}$

Definition of $\sequence {b_N}$

$\ds $

$=$

$\ds \size {a_{\map \pi {\map \phi {n, 2 p + 1}, 2 p + 1} } - y_n}$

Definition of $\psi$

$\ds $

$\le$

$\ds \size {a_{\map \pi {\map \phi {n, 2 p + 1}, 2 p + 1} } - x_{\map \phi {n, 2 p + 1} } } + \size {x_{\map \phi {n, 2 p + 1} } - y_n}$

$\ds $

$<$

$\ds \dfrac 1 {2 p + 2} + \dfrac 1 {2 p + 2}$

$\ds $

$=$

$\ds \dfrac 1 {p + 1}$

$\blacksquare$