avewright/proofwiki-math huggingface dataset:
Theorem: Approximation/Examples/Sine of x

For small values of $x$ measured in radians:
:$\sin x \approx x$

Proof:
From Limit of Sine of X over X at Zero:
:$\ds \lim_{x \mathop \to 0} \frac {\sin x} x = 1$
Hence the result.
{{qed}}
Theorem: Absolutely Convergent Generalized Sum Converges to Supremum

Let $V$ be a Banach space.
Let $\family {v_i}_{i \mathop \in I}$ be an indexed family of elements of $V$.
Let $\FF$ denote the set of finite subsets of $I$.
Let the generalized sum $\ds \sum_{i \mathop \in I} v_i$ converge absolutely to $c \in \R$.
Then:
:$c = \sup \set{\ds \sum_{i \mathop \in F} \norm{v_i} : F \in \FF}$

Proof:
{{AimForCont}}:
:$\exists E \in \FF : \ds \sum_{i \mathop \in E} \norm{v_i} > c$
Let:
:$0 < \epsilon < \ds \sum_{i \mathop \in F} \norm{v_i} - c$
Let $F \in \FF$.
Let $E' = F \cup E$.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop \in E'} \norm{v_i}
      | r = \sum_{i \mathop \in F} \norm{v_i} + \sum_{i \mathop \in E' \setminus F} \norm{v_i}
      | c = Summation over Union of Disjoint Finite Index Sets
}}
{{eqn | o = \ge
      | r = \sum_{i \mathop \in F} \norm{v_i}
}}
{{eqn | o = >
      | r = c + \epsilon
      | c = Summation over Union of Disjoint Finite Index Sets
}}
{{eqn | ll = \leadsto
      | o = <
      | l = \epsilon
      | r = \size{\sum_{i \mathop \in E'} \norm{v_i} - c}
}}
{{end-eqn}}
Since $F$ was arbitrary, it follows:
:$\forall F \in \FF : \exists E' \in \FF : E' \supseteq F$ and $\size{\ds \sum_{i \mathop \in E'} \norm{v_i} - c} > \epsilon$
This contradicts the hypothesis that $\ds \sum_{i \mathop \in I} v_i$ converges absolutely to $c \in \R$.
Hence:
:$\forall E \in \FF : \ds \sum_{i \mathop \in E} \norm{v_i} \le c$
By definition of absolutely net convergence:
:$\forall \epsilon \in \R_{\mathop > 0}: \exists F \in \FF : \forall E \in \FF : E \supseteq F \leadsto \ds \sum_{i \mathop \in E} \norm{v_i} \in \hointl {c - \epsilon} c$
From Characterizing Property of Supremum of Subset of Real Numbers:
:$c = \sup \set{\ds \sum_{i \mathop \in F} \norm{v_i} : F \in \FF}$
{{qed}}
Category:Banach Spaces
Category:Generalized Sums
qyla2urakzscp21i29a0js66h1nssz9
Theorem: Characterization of T1 Space using Neighborhood Basis

Let $T = \struct {S, \tau}$ be a topological space.
For each $x \in S$, let $\NN_x$ be a neighborhood basis at $x$.
Then:
:$T$ is a $T_1$ Space
{{iff}}
:$\forall x, y \in S : x \ne y$, both: 
::$\exists N \in \NN_x : y \notin N$
:and:
::$\exists M \in \NN_y : x \notin M$

Proof:
=== Necessary Condition ===
Let $T$ be a $T_1$ Space.
Let $x, y \in S$ such that $x \ne y$.
By definition of $T_1$ Space:
:$\exists U \in \tau : x \in U, y \notin U$
From Set is Open iff Neighborhood of all its Points:
:$U$ is a neighborhood of $x$
By definition of neighborhood basis:
:$\exists N \in \NN_x : N \subseteq U$
It follows that:
:$y \notin N$
Similarly:
$\exists M \in \NN_y : x \notin M$
The result follows.
{{qed|lemma}}
Theorem: Control Path in Flow Chart is Unique

Let $C = \struct {F, P, V, E}$ be a flow chart.
Let $\struct {X, \set {f_g}, \set {p_q}}$ be an interpretation for $C$.
Let $b \in V$ and $x \in X$, and $N \in \N_{> 0}$.
Then, there is at most one length $N$ control path in $\struct {C, X}$, starting from $\tuple {b, x}$.

Proof:
We will proceed by induction on $N$.
Theorem: Characterization of T1 Space using Basis

Let $T = \struct {S, \tau}$ be a topological space.
Let $\BB$ be a basis for $T$.
Then:
:$T$ is a $T_1$ Space
{{iff}}
:$\forall x, y \in S : x \ne y$, both:
::$\exists B_x \in \BB : x \in B_x, y \notin B_x$
:and:
::$\exists B_y \in \BB : y \in B_y, x \notin B_y$

Proof:
=== Necessary Condition ===
From Basis induces Local Basis:
:$\forall x \in S : \BB_x = \set{B \in \BB : x \in B}$ is a local basis of $x$
By definition of local basis:
:$\forall x \in S : \BB_x$ is a neighborhood basis of open sets
From Characterization of $T_1$ Space using Neighborhood Basis:
:$\forall x, y \in S : x \ne y$, both:
::$\exists B_x \in \BB_x : y \notin B_x$
:and:
::$\exists B_y \in \BB_y : x \notin B_y$
Hence:
:$\forall x, y \in S : x \ne y$, both:
::$\exists B_x \in \BB : x \in B_x, y \notin B_x$
:and:
::$\exists B_y \in \BB : y \in B_y, x \notin B_y$
{{qed|lemma}}
Theorem: Choquet's Theorem

Let $X$ be a locally convex vector space over $\R$.
Let $K$ be a non-empty metrizable compact convex subspace of $X$.
Let $K_e$ be the set of extreme points of $K$.
Then each $x \in K$ is a barycenter of a Borel probability measure $m_x$ on $K$ such that:
:$\map {m_x} {K_e} = 1$
That is:
:$\ds \forall \ell \in X^\ast : \map \ell x = \int_{K_e} \map \ell u \rd \map {m_x} u$
where $X^\ast$ is the dual of $X$.

Proof:
{{ProofWanted}}
{{Namedfor|Gustave Alfred Arthur Choquet|cat = Choquet}}
Theorem: Ackermann-Péter Function at (1,y)

For every $y \in \N$:
:$\map A {1, y} = y + 2$
where $A$ is the Ackermann-Péter function.

Proof:
Proceed by induction on $y$.
Theorem: Ackermann-Péter Function at (2,y)

For every $y \in \N$:
:$\map A {2, y} = 2 y + 3$
where $A$ is the Ackermann-Péter function.

Proof:
Proceed by induction on $y$.
Theorem: Ackermann-Péter Function is Greater than Second Argument

For all $x, y \in \N$:
:$\map A {x, y} > y$
where $A$ is the Ackermann-Péter function.

Proof:
First, perform induction on $x$.
Theorem: Ackermann-Péter Function is Strictly Increasing on Second Argument

For all $x, y \in \N$:
:$\map A {x, y + 1} > \map A {x, y}$
where $A$ is the Ackermann-Péter function.

Proof:
Proceed by induction on $x$.
Theorem: Ackermann-Péter Function is Strictly Increasing on Second Argument/General Result

For all $x, y, z \in \N$ such that:
:$y < z$
we have:
:$\map A {x, y} < \map A {x, z}$
where $A$ is the Ackermann-Péter function.

Proof:
Let $z$ be expressed as:
:$z = y + k$
for some $k \in \N_{>0}$.
Proceed by induction on $k$.
Theorem: Euler Phi Function is not Completely Multiplicative

The Euler $\phi$ function is not a completely multiplicative function.
That is, it is not always the case that:
:$\map \phi {m n} = \map \phi m \map \phi n$
where $m, n \in \Z_{>0}$.

Proof:
;Proof by Counterexample
{{begin-eqn}}
{{eqn | l = \map \phi 6
      | r = 2
      | c = {{EulerPhiLink|6}}
}}
{{eqn | l = \map \phi {10}
      | r = 4
      | c = {{EulerPhiLink|10}}
}}
{{eqn | l = \map \phi {60}
      | r = 16
      | c = {{EulerPhiLink|60}}
}}
{{end-eqn}}
Hence we see:
:$6 \times 10 = 60$
but:
:$\map \phi 6 \times \map \phi {10} \ne \map \phi {60}$
{{qed}}
Theorem: Increasing Second Argument of Ackermann-Péter Function is Not Greater than Increasing First Argument

For all $x, y \in \N$:
:$\map A {x + 1, y} \ge \map A {x, y + 1}$
where $A$ is the Ackermann-Péter function.

Proof:
Proceed by induction on $y$.
Theorem: Ackermann-Péter Function is Strictly Increasing on First Argument

For all $x, y \in \N$:
:$\map A {x + 1, y} > \map A {x, y}$
where $A$ is the Ackermann-Péter function.

Proof:
{{begin-eqn}}
{{eqn | l = \map A {x + 1, y}
      | o = \ge
      | r = \map A {x, y + 1}
      | c = Increasing Second Argument of Ackermann-Péter Function is Not Greater than Increasing First Argument
}}
{{eqn | o = >
      | r = \map A {x, y}
      | c = Ackermann-Péter Function is Strictly Increasing on Second Argument
}}
{{end-eqn}}
{{qed}}
Category:Ackermann-Péter Function is Strictly Increasing on First Argument
Category:Ackermann-Péter Function
fi54dcrx8nsd7lj3ii3l2cr1aboc5tp
Theorem: Ackermann-Péter Function is Strictly Increasing on First Argument/General Result

Forall $x, y, z \in \N$ such that:
:$x < y$
we have:
:$\map A {x, z} < \map A {y, z}$
where $A$ is the Ackermann-Péter function.

Proof:
Let $y$ be expressed as:
:$y = x + k$
for some $k \in \N_{>0}$.
Proceed by induction on $k$.
Theorem: Strict Upper Bound for Composition of Ackermann-Péter Functions

For all $x, y, z \in \N$:
:$\map A {x + y + 2, z} > \map A {x, \map A {y, z}}$
where $A$ is the Ackermann-Péter function.

Proof:
We have:
:$x + y + 1 > y$
giving us:
:$\paren 1 \quad \map A {x + y + 1, z} > \map A {y, z}$
by Ackermann-Péter Function is Strictly Increasing on First Argument.
Therefore:
{{begin-eqn}}
{{eqn | l = \map A {x + y + 2, z}
      | o = \ge
      | r = \map A {x + y + 1, z + 1}
      | c = Increasing Second Argument of Ackermann-Péter Function is Not Greater than Increasing First Argument
}}
{{eqn | r = \map A {x + y, \map A {x + y + 1, z} }
      | c = {{Defof|Ackermann-Péter Function}}
}}
{{eqn | o = >
      | r = \map A {x + y, \map A {y, z} }
      | c = Ackermann-Péter Function is Strictly Increasing on Second Argument and $\paren 1$
}}
{{eqn | o = \ge
      | r = \map A {x, \map A {y, z} }
      | c = Ackermann-Péter Function is Strictly Increasing on First Argument
}}
{{end-eqn}}
{{qed}}
Category:Ackermann-Péter Function
i4zh89wtrcywb88ioh3c3nyxdtpkh9f
Theorem: Strict Upper Bound for Sum of Ackermann-Péter Functions

For all $x, y, z \in \N$:
:$\map A {\map \max {x, y} + 4, z} > \map A {x, z} + \map A {y, z}$
where $A$ is the Ackermann-Péter function.

Proof:
{{begin-eqn}}
{{eqn | l = \map A {\map \max {x, y} + 4, z}
      | o = >
      | r = \map A {2, \map A {\map \max {x, y}, z} }
      | c = Strict Upper Bound for Composition of Ackermann-Péter Functions
}}
{{eqn | r = 2 \map A {\map \max {x, y}, z} + 3
      | c = Ackermann-Péter Function at (2,y)
}}
{{eqn | o = >
      | r = 2 \map A {\map \max {x, y}, z}
}}
{{eqn | o = \ge
      | r = \map A {x, z} + \map A {y, z}
      | c = Ackermann-Péter Function is Strictly Increasing on First Argument
}}
{{end-eqn}}
{{qed}}
Category:Ackermann-Péter Function
mt8rgpeg71etfnil30c0d07ejohgli4
Theorem: Ackermann-Péter Function is not Primitive Recursive

The Ackermann-Péter function is not primitive recursive.

Proof:
Let $A : \N^2 \to \N$ denote the Ackermann-Péter function.
It suffices to show that, for every primitive recursive $f : \N^k \to \N$, there exists some $t_f \in \N$ such that:
:$\forall x_1, \dotsc, x_k \in \N: \map f {x_1, \dotsc, x_k} < \map A {t_f, \map \max {x_1, \dotsc, x_k}}$
For, if $A$ were primitive recursive, we would have:
:$\map A {t_A, t_A} < \map A {t_A, \map \max {t_A, t_A}} = \map A {t_A, t_A}$
which is a contradiction.
We will proceed by induction on the definition of $f$.
Theorem: Division on Numbers is Not Associative

The operation of division on the numbers is not associative.
That is, in general:
:$a \div \paren {b \div c} \ne \paren {a \div b} \div c$

Proof:
By definition of division:
{{begin-eqn}}
{{eqn | l = a \div \paren {b \div c}
      | r = a \times \paren {\dfrac 1 {b \times \dfrac 1 c} }
      | c = 
}}
{{eqn | r = a \times \paren {\dfrac c b}
      | c = 
}}
{{eqn | r = \dfrac {a c} b
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \paren {a \div b} \div c
      | r = \paren {a \times \dfrac 1 b} \times \dfrac 1 c
      | c = 
}}
{{eqn | r = \dfrac a {b c}
      | c = 
}}
{{end-eqn}}
So we see that:
:$a \div \paren {b \div c} = \paren {a \div b} \div c \iff c = 1$
and so in general:
:$a \div \paren {b \div c} \ne \paren {a \div b} \div c$
{{qed}}
Theorem: Real Addition is Sequentially Computable

Let $f : \R^2 \to \R$ be defined as:
:$\map f {x, y} = x + y$
Then $f$ is sequentially computable.

Proof:
Follows immediately from Sum of Computable Real Sequences is Computable.
{{qed}}
Category:Computability Theory
ggmlqw7st6j6105q4n1v41mushddqum
Theorem: Real Addition is Computably Uniformly Continuous

Let $f : \R^2 \to \R$ be defined as:
:$\map f {x, y} = x + y$
Then $f$ is computably uniformly continuous.

Proof:
We will define $d : \N \to \N$ as:
:$\map d n = 2 n + 1$
which is primitive recursive by:
* Addition is Primitive Recursive
* Constant Function is Primitive Recursive
and thus total recursive by:
* Primitive Recursive Function is Total Recursive Function
Let $x_1, y_1, x_2, y_2 \in \R$ and $n \in \N$ be arbitrary, and suppose:
:$\norm {\tuple {x_1, y_1} - \tuple {x_2, y_2}} < \dfrac 1 {\map d n + 1} = \dfrac 1 {2 n + 2}$
We have:
{{begin-eqn}}
{{eqn | l = \size {x_1 - x_2} + \size {y_1 - y_2}
      | r = \norm {\tuple {x_1 - x_2, 0} } + \norm {\tuple {0, y_1 - y_2} }
}}
{{eqn | o = \le
      | r = \norm {\tuple {x_1 - x_2, y_1 - y_2} }
}}
{{eqn | r = \norm {\tuple {x_1, y_1} - \tuple {x_2, y_2} }
      | c = Triangle Inequality for Vectors in Euclidean Space
}}
{{end-eqn}}
and thus:
:$\size {x_1 - x_2} \le \norm {\tuple {x_1, y_1} - \tuple {x_2, y_2}} < \dfrac 1 {2 n + 2}$
:$\size {y_1 - y_2} \le \norm {\tuple {x_1, y_1} - \tuple {x_2, y_2}} < \dfrac 1 {2 n + 2}$
Hence:
{{begin-eqn}}
{{eqn | l = \size {\map f {x_1, y_1} - \map f {x_2, y_2} }
      | r = \size {x_1 + y_1 - x_2 - y_2}
      | c = Definition of $f$
}}
{{eqn | r = \size {\paren {x_1 - x_2} + \paren {y_1 - y_2} }
}}
{{eqn | o = \le
      | r = \size {x_1 - x_2} + \size {y_1 - y_2}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = <
      | r = \dfrac 1 {2 n + 2} + \dfrac 1 {2 n + 2}
      | c = Inequality above
}}
{{eqn | r = \dfrac 1 {n + 1}
}}
{{end-eqn}}{{qed}}
Category:Computability Theory
d6lu3m8pgn7080lxny61wykeb02fhah
Theorem: Real Addition is Computable

Let $f : \R^2 \to \R$ be defined as:
:$\map f {x, y} = x + y$
Then $f$ is computable.

Proof:
Follows immediately from:
* Real Addition is Sequentially Computable
* Real Addition is Computably Uniformly Continuous
{{qed}}
Category:Computability Theory
q5v2d6lq0aqoiq11qx58a6tfb88roqr
Theorem: Sum of Computable Rational Sequences is Computable

Let $\sequence {x_n}$ and $\sequence {y_n}$ be computable rational sequences.
Then, $\sequence {x_n + y_n}$ is a computable rational sequence.

Proof:
By definition of computable rational sequence, there exist total recursive $f_x, g_x, f_y, g_y : \N \to \N$ such that:
:$x_n = \dfrac {k_n} {\map {g_x} n + 1}$
:$y_n = \dfrac {\ell_n} {\map {g_y} n + 1}$
where:
:$\map {f_x} n$ codes the integer $k_n$
:$\map {f_y} n$ codes the integer $\ell_n$
We define:
:$\map f n = \paren {\map {g_y} n + 1}_\Z \times_\Z \map {f_x} n +_\Z \paren {\map {g_x} n + 1}_\Z \times_\Z \map {f_y} n$
:$\map g n = \map {g_x} n \times \map {g_y} n + \map {g_x} n + \map {g_y} n$
which are both total recursive by:
* Code Number for Non-Negative Integer is Primitive Recursive
* Multiplication of Integers is Primitive Recursive
* Addition of Integers is Primitive Recursive
* Multiplication is Primitive Recursive
* Addition is Primitive Recursive
Thus, we have:
{{begin-eqn}}
{{eqn | l = \frac {p_n} {\map g n + 1}
      | r = \frac {\paren {\map {g_y} n + 1} k_n + \paren {\map {g_x} n + 1} \times \ell_n} {\map {g_x} n \map {g_y} n + \map {g_x} n + \map {g_y} n + 1}
      | c = $\map f n$ codes the integer $p_n$
}}
{{eqn | r = \frac {\paren {\map {g_y} n + 1} k_n} {\paren {\map {g_x} n + 1} \paren {\map {g_y} n + 1} } + \frac {\paren {\map {g_x} n + 1} \ell_n} {\paren {\map {g_x} n + 1} \paren {\map {g_y} n + 1} }
}}
{{eqn | r = \frac {k_n} {\map {g_x} n + 1} + \frac {\ell_n} {\map {g_y} n + 1}
}}
{{eqn | r = x_n + y_n
}}
{{end-eqn}}{{qed}}
Category:Computability Theory
kb21je8qia7w0pypa2g3b3qocn8jslo
Theorem: Product of Computable Rational Sequences is Computable

Let $\sequence {x_n}$ and $\sequence {y_n}$ be computable rational sequences.
Then, $\sequence {x_n y_n}$ is a computable rational sequence.

Proof:
By definition of computable rational sequence, there exist total recursive $f_x, g_x, f_y, g_y : \N \to \N$ such that:
:$x_n = \dfrac {k_n} {\map {g_x} n + 1}$
:$y_n = \dfrac {\ell_n} {\map {g_y} n + 1}$
where:
:$\map {f_x} n$ codes the integer $k_n$
:$\map {f_y} n$ codes the integer $\ell_n$
We define:
:$\map f n = \map {f_x} n \times_Z \map {f_y} n$
:$\map g n = \map {g_x} n \times \map {g_y} n + \map {g_x} n + \map {g_y} n$
which are total recursive by:
* Multiplication of Integers is Primitive Recursive
* Addition is Primitive Recursive
* Multiplication is Primitive Recursive
Thus, we have:
{{begin-eqn}}
{{eqn | l = \frac {p_n} {\map g n + 1}
      | r = \frac {k_n \ell_n} {\map {g_x} n \map {g_y} n + \map {g_x} n + \map {g_y} n + 1}
      | c = $\map f n$ codes the integer $p_n$
}}
{{eqn | r = \frac {k_n \ell_n} {\paren {\map {g_x} n + 1} \paren {\map {g_y} n + 1} }
}}
{{eqn | r = \frac {k_n} {\map {g_x} n + 1} \frac {\ell_n} {\map {g_y} n + 1}
}}
{{eqn | r = x_n y_n
}}
{{end-eqn}}{{qed}}
Category:Computability Theory
lbju6nwsrsc4npzaodrk42hu34bg2lg
Theorem: Condition for Closure of Open Ball to be Closed Ball of Same Radius

Let $\struct {M, d}$ be a metric space.
{{TFAE}}
:$(1) \quad$ for all $x \in X$ and $r > 0$ we have $\map \cl {\map {B_r} x} = \map { {B_r}^-} x$, where $\cl$ denotes closure
:$(2) \quad$ for each $\epsilon > 0$ and  $x, y \in X$ with $x \ne y$, there exists $z \in X$ with $\map d {z, y} < \epsilon$ and $\map d {x, z} < \map d {x, y}$.

Proof:
=== $(1)$ implies $(2)$ ===
Suppose that $(1)$ holds. 
Let $\epsilon > 0$. 
Let $x, y \in X$ have $x \ne y$.
We aim to show that there exists $z \in X$ with $\map d {z, y} < \epsilon$ and $\map d {x, z} < \map d {x, y}$.
Let $r = \map d {x, y}$. 
From $(1)$, we have $\map \cl {\map {B_r} x} = \map { {B_r}^-} x$.
So $y \in \map \cl {\map {B_r} x}$. 
Hence by the definition of topological closure, for each $\epsilon > 0$ we have:
:$\map {B_\epsilon} y \cap \map {B_r} x \ne \O$
Let $z \in \map {B_\epsilon} y \cap \map {B_r} x$.
Then $\map d {y, z} < \epsilon$ and $\map d {x, z} < r = \map d {x, y}$.
{{qed|lemma}}
Theorem: Computable Real Sequence iff Limits of Computable Rational Sequences

Let $\sequence {x_m}$ be a sequence of real numbers.
Then, $\sequence {x_m}$ is computable {{iff}} there exist:
* A computable rational sequence $\sequence {a_k}$
* Total recursive functions $\phi, \psi : \N^2 \to \N$
such that:
:$\forall m, p \in \N: \forall n \ge \map \psi {m, p}: \size {a_{\map \phi {m, n}} - x_m} < \dfrac 1 {p + 1}$

Proof:
=== Necessary Condition ===
Suppose $\sequence {x_m}$ is computable.
Then, there exists a total recursive $f : \N^2 \to \N$ such that, for all $m, p \in \N$:
:$\dfrac {c_{m,p} - 1} {p + 1} < x_m < \dfrac {c_{m,p} + 1} {p + 1}$
where $\map f {m, p}$ codes the integer $c_{m,p}$.
To produce the computable rational sequence, we will define:
:$\map N k = \map f {\map {\pi_1} k, \map {\pi_2} k}$
:$\map D k = \map {\pi_2} k$
where $\pi_1$ and $\pi_2$ are the projections of the Cantor pairing function.
Then:
:$a_k = \dfrac {d_k} {\map D k + 1}$
where $\map N k$ codes the integer $d_k$.
We will define:
:$\map \phi {m, n} = \map \pi {m, n}$
:$\map \psi {m, p} = p$
where $\pi$ is the Cantor pairing function.
All of the above defined function are total recursive by:
* Cantor Pairing Function is Primitive Recursive
* Inverse of Cantor Pairing Function is Primitive Recursive
* Primitive Recursive Function is Total Recursive Function
Now, let $m, p \in \N$ be arbitrary, and let $n \in \N$ satisfy:
:$n \ge \map \psi {m, p} = p$
We have:
{{begin-eqn}}
{{eqn | l = a_{\map \phi {m, n} }
      | r = \dfrac {d_{\map \pi {m, n} } } {\map D {\map \pi {m, n} } + 1}
}}
{{eqn | r = \dfrac {c_{\map {\pi_1} {\map \pi {m, n} }, \map {\pi_2} {\map \pi {m, n} } } } {\map {\pi_2} {\map \pi {m, n} } + 1}
}}
{{eqn | r = \dfrac {c_{m,n} } {n + 1}
}}
{{end-eqn}}
By assumption:
:$\dfrac {c_{m,n} - 1} {n + 1} < x_m < \dfrac {c_{m,n} + 1} {n + 1}$
Therefore:
{{begin-eqn}}
{{eqn | l = \size {a_{\map \phi {m,n} } - x_m}
      | r = \size {\frac {c_{m,n} } {n + 1} - x_m}
}}
{{eqn | o = <
      | r = \frac 1 {n + 1}
      | c = As $- \dfrac 1 {n + 1} < x_m - \dfrac {c_{m,n} } {n + 1} < \dfrac 1 {n + 1}$
}}
{{eqn | o = \le
      | r = \frac 1 {p + 1}
      | c = As $n \ge p$
}}
{{end-eqn}}{{qed|lemma}}
Theorem: Computable Rational Sequence is Computable Real Sequence

Let $\sequence {x_n}$ be a computable rational sequence.
Then, $\sequence {x_n}$ is a computable real sequence.

Proof:
By Computable Real Sequence iff Limits of Computable Rational Sequences, it suffices to show that there exist:
:A computable rational sequence $\sequence {a_k}$
:Total recursive functions $\phi, \psi : \N^2 \to \N$
such that:
:$\forall m, p \in \N: \forall n \ge \map \psi {m, p}: \size {a_{\map \phi {m, n}} - x_m} < \dfrac 1 {p + 1}$
We will choose:
:$\forall k \in \N: a_k = x_k$
:$\map \phi {m, n} = m$
:$\map \psi {m, p} = 0$
$\phi$ and $\psi$ are trivially primitive recursive, and thus total recursive by Primitive Recursive Function is Total Recursive Function.
As $\sequence {a_k} = \sequence {x_k}$, it is computable by assumption.
Finally, we have that, for any $m, n, p \in \N$:
{{begin-eqn}}
{{eqn | l = \size {a_{\map \phi {m, n} } - x_m}
      | r = \size {a_m - x_m}
}}
{{eqn | r = 0
}}
{{eqn | o = <
      | r = \dfrac 1 {p + 1}
}}
{{end-eqn}}{{qed}}
Category:Computability Theory
jumqy9m760xtucloodqktswo72uiy31
Theorem: Constant Sequence of Rational Number is Computable

Let $r \in \Q$ be a rational number.
Let $\sequence {x_n}$ be defined as:
:$x_n = r$
Then, $\sequence {x_n}$ is a computable rational sequence.

Proof:
By Existence of Canonical Form of Rational Number, let:
:$r = \dfrac p q$
where:
:$p \in \Z$
:$q \in \Z_{>0}$
Let $m$ be the code number for the integer $p$.
As $q \ge 1$, it follows that:
:$q - 1 \in \N$
We define $N, D : \N \to \N$ as:
:$\map N n = m$
:$\map D n = q - 1$
which are total recursive by:
* Constant Function is Primitive Recursive
* Primitive Recursive Function is Total Recursive Function
Then:
:$\dfrac {k_n} {\map D n + 1} = \dfrac p q = r = x_n$
where $\map N n = m$ codes the integer $k_n = p$
Therefore, $\sequence {x_n}$ is computable by definition.
{{qed}}
Category:Computability Theory
tq9k5cyho9z38zob2oglsk611d0z2p6
Theorem: Rational Number is Computable Real Number

Let $r \in \Q$ be a rational number.
Then, $r$ is a computable real number.

Proof:
Let $\sequence {x_n}$ be defined as:
:$x_n = r$
By Constant Sequence of Rational Number is Computable:
:$\sequence {x_n}$ is a computable rational sequence.
By Computable Rational Sequence is Computable Real Sequence:
:$\sequence {x_n}$ is a computable real sequence.
By Term of Computable Real Sequence is Computable:
:$x_0 = r$ is a computable real number.
{{qed}}
Category:Computability Theory
inqn25mgngdhb5xgamz80185ie2u3jy
Theorem: Computable Subsequence of Computable Rational Sequence is Computable

Let $\sequence {x_n}_{n \in \N}$ be a computable rational sequence.
Let $\phi : \N \to \N$ be a total recursive function.
Then:
:$\sequence {x_{\map \phi n}}_{n \in \N}$
is a computable rational sequence.

Proof:
By definition of computable rational sequence, there exist total recursive $N, D : \N \to \N$ such that, for every $n \in \N$:
:$x_n = \dfrac {k_n} {\map D n + 1}$
where $\map N n$ codes the integer $k_n$.
We define total recursive $N', D' : \N \to \N$ as:
:$\map {N'} n = \map N {\map \phi n}$
:$\map {D'} n = \map N {\map \phi n}$
Now, we just need to show that, for every $n \in \N$:
:$x_{\map \phi n} = \dfrac {k'_n} {\map {D'} n + 1}
where $\map {N'} n$ codes the integer $k'_n$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac {k'_n} {\map {D'} n + 1}
      | r = \dfrac {k_{\map \phi n} } {\map D {\map \phi n} + 1}
      | c = Definitions of $N'$ and $D'$
}}
{{eqn | r = x_{\map \phi n}
      | c = Assumption on $N$ and $D$
}}
{{end-eqn}}{{qed}}
Category:Computability Theory
81bxb872pkye4vslk2acfpgyrrl0g8z
Theorem: Computable Subsequence of Computable Rational Sequence is Computable/Corollary

Let $\sequence {x_k}$ be a computable rational sequence.
Let $\phi : \N^2 \to \N$ be a total recursive function.
Then, there exists a computable rational sequence $\sequence {y_k}$ such that, for all $n, m \in \N$:
:$y_{\map \pi {n, m}} = x_{\map \phi {n, m}}$
where $\pi : \N^2 \to \N$ is the Cantor pairing function.

Proof:
Let $\psi : \N^2 \to \N$ be defined as:
:$\map \psi k = \map \phi {\map {\pi_1} k, \map {\pi_2} k}$
where $\pi_1, \pi_2 : \N \to \N$ are the projections on the Cantor pairing function.
By Inverse of Cantor Pairing Function is Primitive Recursive, we have that $\psi$ is total recursive.
Therefore, by Computable Subsequence of Computable Rational Sequence is Computable:
:$\sequence {x_{\map \psi k}}$
is a computable rational sequence.
It remains to be shown that:
:$y_k = x_{\map \psi k}$
for all $k \in \N$.
We have:
{{begin-eqn}}
{{eqn | l = y_k
      | r = y_{\map \pi {\map {\pi_1} k, \map {\pi_2} k} }
      | c = Inverse of Cantor Pairing Function
}}
{{eqn | r = x_{\map \phi {\map {\pi_1} k, \map {\pi_2} k} }
      | c = Premise
}}
{{eqn | r = x_{\map \psi k}
      | c = Definition of $\psi$
}}{{qed}}
Category:Computability Theory
nwazx57gpwm4vkh9te4qiegykpwxn7v