nyuuzyou/wikis huggingface dataset:
Sum of Cauchy Sequences in Topological Vector Space is Cauchy Sequence

== Theorem ==
Let $K$ be a topological field. 
Let $X$ be a topological vector space over $K$.
Let $\sequence {x_n}_{n \in \N}$ and $\sequence {y_n}_{n \in \N}$ be Cauchy sequences in $X$.
Then $\sequence {x_n + y_n}_{n \in \N}$ is a Cauchy sequence in $X$.
== Proof ==
Let $U$ be an open neighborhood of ${\mathbf 0}_X$.
From Open Neighborhood of Point in Topological Vector Space contains Sum of Open Neighborhoods: Corollary 1, there exists an open neighborhood $V$ of ${\mathbf 0}_X$ such that:
:$V + V \subseteq U$
Since $\sequence {x_n}_{n \in \N}$ is Cauchy, there exists $N_1 \in N$ such that:
:$x_n - x_m \in V$ for $n, m \ge N_1$.
Since $\sequence {y_n}_{n \in \N}$ is Cauchy, there exists $N_2 \in \N$ such that:
:$y_n - y_m \in V$ for $n, m \ge N_2$.
Let $N = \max \set {N_1, N_2}$. 
Then, for $n, m \ge N$, we have: 
Hence $\sequence {x_n + y_n}_{n \in \N}$ is a Cauchy sequence in $X$.
Category:Cauchy Sequences in Topological Vector Spaces
Sum of Ceilings not less than Ceiling of Sum

== Theorem ==
Let $\ceiling x$ be the ceiling function.
Then:
:$\ceiling x + \ceiling y \ge \ceiling {x + y}$
The equality holds:
:$\ceiling x + \ceiling y = \ceiling {x + y}$
 either:
:$x \in \Z$ or $y \in \Z$
or:
:$x \bmod 1 + y \bmod 1 > 1$
where $x \bmod 1$ denotes the modulo operation.
== Proof ==
From the definition of the modulo operation, we have that:
:$x = \floor x + \paren {x \bmod 1}$
from which we obtain:
:$x = \ceiling x - \sqbrk {x \notin \Z} + \paren {x \bmod 1}$
where $\sqbrk {x \notin \Z}$ uses Iverson's convention.
We have that:
:$x \notin \Z \implies x \bmod 1 > 0$
As $0 \le x \bmod 1 < 1$ it follows that:
:$\sqbrk {x \notin \Z} \ge x \bmod 1$
Hence the inequality.
The equality holds :
:$\ceiling {\paren {x \bmod 1} + \paren {y \bmod 1} } = \sqbrk {x \notin \Z} + \sqbrk {y \notin \Z}$
that is, one of the following holds:
:$x \in \Z$, in which case $x \bmod 1 = 0$
:$y \in \Z$, in which case $y \bmod 1 = 0$
:both $x, y \in \Z$, in which case $\paren {x \bmod 1} + \paren {y \bmod 1} = 0$
:both $x, y \notin \Z$ and $\paren {x \bmod 1} + \paren {y \bmod 1} > 1$.
== Sources ==
* : $\S 1.2.4$: Integer Functions and Elementary Number Theory: Exercise $7$
Category:Ceiling Function
Sum of Chi-Squared Random Variables

== Theorem ==
Let $n_1, n_2, \ldots, n_k$ be strictly positive integers which sum to $N$.
Let $X_i \sim {\chi^2}_{n_i}$ for $1 \le i \le k$, where ${\chi^2}_{n_i}$ is the chi-squared distribution with $n_i$ degrees of freedom. 
Then: 
:$\ds X = \sum_{i \mathop = 1}^k X_i \sim {\chi^2}_N$
== Proof == 
Let $Y \sim {\chi^2}_N$. 
By Moment Generating Function of Chi-Squared Distribution, the moment generating function of $X_i$ is given by: 
:$\map {M_{X_i} } t = \paren {1 - 2 t}^{-n_i / 2}$
Similarly, the moment generating function of $Y$ is given by: 
:$\map {M_Y} t = \paren {1 - 2 t}^{-N / 2}$
By Moment Generating Function of Linear Combination of Independent Random Variables, the moment generating function of $X$ is given by: 
:$\ds \map {M_X} t = \prod_{i \mathop = 1}^k \map {M_{X_i} } t$
We aim to show that: 
:$\map {M_X} t = \map {M_Y} t$
By Moment Generating Function is Unique, this ensures $X = Y$.
We have:
Category:Chi-Squared Distribution
Sum of Closable Densely-Defined Linear Operator and Densely-Defined Bounded Linear Operator is Closable/Corollary

== Corollary ==
Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space over $\C$.
Let $\tuple {\map D T, T}$ be a closed densely-defined linear operator.
Let $\tuple {\HH, S}$ be a bounded linear operator.
Let $\tuple {\map D T, T + S}$ be the sum of $\tuple {\map D T, T}$ and $\tuple {\HH, S}$.
Then $\tuple {\map D T, T + S}$ be a closed.
== Proof ==
Let $\tuple {\map D {\overline T}, \overline T}$ and $\tuple {\HH, \overline S}$ be the closures of $\tuple {\map D T, T}$ and $\tuple {\HH, S}$ respectively. 
From Sum of Closable Densely-Defined Linear Operator and Densely-Defined Bounded Linear Operator is Closable:
:$\tuple {\map D T, T + S}$ is closable densely-defined linear operator with closure $\tuple {\map D {\overline T}, \overline T + \overline S}$.
From Closable Densely-Defined Operator is Closed iff Equal to Closure, we have $\tuple {\map D {\overline T}, \overline T} = \tuple {\map D T, T}$
From Closure of Densely-Defined Bounded Linear Operator and Closable Densely-Defined Operator is Closed iff Equal to Closure, we also have $\tuple {\HH, S} = \tuple {\HH, \overline S}$. 
Hence we have $\tuple {\map D {\overline T}, \overline T + \overline S} = \tuple {\map D T, T + S}$.
Hence from Closable Densely-Defined Operator is Closed iff Equal to Closure, we have that $\tuple {\map D T, T + S}$ be a closed.
Category:Sum of Closable Densely-Defined Linear Operator and Densely-Defined Bounded Linear Operator is Closable
Sum of Closed Linear Subspace and Finite-Dimensional Subspace of Hausdorff Topological Vector Space

== Theorem ==
Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a Hausdorff topological vector space over $\GF$.
Let $N$ be a closed linear subspace of $X$.
Let $F$ be a finite dimensional linear subspace of $X$.
Then $N + F$ is closed in $\struct {X, \tau}$. 
== Proof ==
Let $\struct {X/N, \tau_N}$ be the quotient topological vector space of $X$ modulo $N$.
From Characterization of Hausdorff Topological Vector Space, $X/N$ is Hausdorff.
Let $\pi : X \to X/N$ be the quotient mapping.
From Image of Linear Transformation is Submodule and Dimension of Image of Vector Space under Linear Transformation is Bounded Above by Dimension of Vector Space, we have that $\pi \sqbrk F$ is a finite dimensional linear subspace of $\struct {X/N, \tau_N}$.
From Finite-Dimensional Subspace of Hausdorff Topological Vector Space is Closed, $\pi \sqbrk F$ is closed in $\struct {X/N, \tau_N}$.
From the definition of the quotient topology, $\pi$ is continuous.
So $\pi^{-1} \sqbrk F$ is closed in $\struct {X/N, \tau_N}$.
From Preimage of Image of Linear Transformation, we have:
:$\pi^{-1} \sqbrk {\pi \sqbrk F} = \ker \pi + F$
From Kernel of Quotient Mapping, we have $\ker \pi = N$ and so:
:$\pi^{-1} \sqbrk {\pi \sqbrk F} = N + F$
Hence $N + F$ is closed in $\struct {X/N, \tau_N}$.
== Sources ==
* : $1.41$: Theorem
Category:Quotient Topological Vector Spaces
Category:Hausdorff Topological Vector Spaces
Sum of Closures is Subset of Closure of Sum in Topological Vector Space

== Theorem ==
Let $K$ be a topological field.
Let $X$ be a topological vector space over $K$. 
Let $A, B \subseteq X$. 
Then: 
:$A^- + B^- \subseteq \paren {A + B}^-$
where $A^-$, $B^-$ and $\paren {A + B}^-$ denote the closures of $A$, $B$ and $A + B$.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $1.13$: Theorem
Category:Topological Vector Spaces
Category:Set Closures
Category:Sum of Closures is Subset of Closure of Sum in Topological Vector Space
Sum of Closures is Subset of Closure of Sum in Topological Vector Space/Proof 1

== Theorem ==
== Proof ==
Let $a \in A^-$ and $b \in B^-$.
We aim to show that $a + b \in \paren {A + B}^-$.
It suffices to show that for each open neighborhood $W$ of $a + b$ we have: 
:$W \cap \paren {A + B} \ne \O$ 
Fix an open neighborhood $W$ of $a + b$.
From Open Neighborhood of Point in Topological Vector Space contains Sum of Open Neighborhoods, there exists an open neighborhood $W_1$ of $a$ and an open neighborhood $W_2$ of $b$ such that: 
:$W_1 + W_2 \subseteq W$
Since $W_1$ is an open neighborhood of $a$ and $a \in A^-$ we have: 
:$W_1 \cap A \ne \O$
Since $W_2$ is an open neighborhood of $b$ and $b \in B^-$ we have: 
:$W_2 \cap B \ne \O$
Let:
:$x \in W_1 \cap A$
and:
:$y \in W_2 \cap B$
Then we have $x \in W_1$ and $y \in W_2$ so that: 
:$x + y \in W_1 + W_2$
Since $W_1 + W_2 \subseteq W$, we then obtain $x + y \in W$.
Since we also have $x \in W_1$ and $y \in W_2$, we have $x + y \in A + B$.
So: 
:$x + y \in W \cap \paren {A + B}$.
We can therefore conclude that: 
:$W \cap \paren {A + B} \ne \O$
Since $W$ was arbitrary, we have that $a + b \in \paren {A + B}^-$ as required.
Category:Sum of Closures is Subset of Closure of Sum in Topological Vector Space
Sum of Closures is Subset of Closure of Sum in Topological Vector Space/Proof 2

== Theorem ==
== Proof ==
Let $x \in A^-$ and $y \in B^-$.
From Point in Set Closure iff Limit of Net, there exists directed sets $\struct {\Lambda_1, \preceq_1}$ and $\struct {\Lambda_2, \preceq_2}$ and nets $\sequence {x_\lambda}_{\lambda \mathop \in \Lambda_1}$ valued in $A$ and $\sequence {y_\lambda}_{\lambda \mathop \in \Lambda_2}$ valued in $B$ such that:
:$\sequence {x_\lambda}_{\lambda \mathop \in \Lambda_1}$ converges to $x$
:$\sequence {y_\lambda}_{\lambda \mathop \in \Lambda_2}$ converges to $y$.
Define a relation $\sqsubseteq$ on $\Lambda_1 \times \Lambda_2$ by: 
:$\tuple {\lambda_1, \lambda_2} \sqsubseteq \tuple {\mu_1, \mu_2}$
for $\tuple {\lambda_1, \lambda_2}, \tuple {\mu_1, \mu_2} \in \Lambda_1 \times \Lambda_2$ :
:$\lambda_1 \preceq_1 \mu_1$ and $\lambda_2 \preceq_2 \mu_2$
From Product of Directed Sets is Directed Set, $\struct {\Lambda_1 \times \Lambda_2, \sqsubseteq}$ is a directed set.
Define:
:$x'_{\tuple {\lambda, \mu} } = x_\lambda$
and:
:$y'_{\tuple {\lambda, \mu} } = y_\mu$
for each $\tuple {\lambda, \mu} \in \Lambda_1 \times \Lambda_2$.
We show that $\langle {x'_{\tuple {\lambda, \mu} } \rangle}_{\tuple {\lambda, \mu} \mathop \in \Lambda_1 \times \Lambda_2}$ converges to $x$.
Fix $\mu_0 \in \Lambda_2$.
Let $U$ be an open neighborhood of $x$. 
Since $\sequence {x_\lambda}_{\lambda \mathop \in \Lambda_1}$, there exists $\lambda_0 \in \Lambda$ such that for all $\lambda \in \Lambda$ with $\lambda \succeq \lambda_0$, we have $x_\lambda \in U$.
Then, if $\tuple {\lambda, \mu} \in \Lambda_1 \times \Lambda_2$ has $\tuple {\lambda, \mu} \sqsupseteq \tuple {\lambda_0, \mu_0}$, we in particular have $\lambda \succeq \lambda_0$ and so $x'_{\tuple {\lambda, \mu} } \in U$. 
Since $U$ was arbitrary, $\sequence {x'_{\tuple {\lambda, \mu} } }_{\tuple {\lambda, \mu} \mathop \in \Lambda_1 \times \Lambda_2}$ converges to $x$.
Similarly, $\sequence {y'_{\tuple {\lambda, \mu} } }_{\tuple {\lambda, \mu} \mathop \in \Lambda_1 \times \Lambda_2}$ converges to $y$.
From Sum of Convergent Nets in Topological Vector Space is Convergent, $\sequence {x'_{\tuple {\lambda, \mu} } + y'_{\tuple {\lambda, \mu} } }_{\tuple {\lambda, \mu} \mathop \in \Lambda_1 \times \Lambda_2}$ converges to $x + y$.
Since $x'_{\tuple {\lambda, \mu} } \in A$ and $y'_{\tuple {\lambda, \mu} } \in B$ for all $\tuple {\lambda, \mu} \in \Lambda_1 \times \Lambda_2$, we have that $x'_{\tuple {\lambda, \mu} } + y'_{\tuple {\lambda, \mu} } \in A + B$ for each $\tuple {\lambda, \mu} \in \Lambda_1 \times \Lambda_2$.
So $x + y$ is the limit of a net valued in $A + B$.
So by Point in Set Closure iff Limit of Net, we have $x + y \in \paren {A + B}^-$.
So, we have $A^- + B^- \subseteq \paren {A + B}^-$.
Category:Sum of Closures is Subset of Closure of Sum in Topological Vector Space
Sum of Compact Subsets of Topological Vector Space is Compact

== Theorem ==
Let $K$ be a topological field.
Let $X$ be a topological vector space over $K$.
Let $A$ and $B$ be compact (topological) subspaces of $X$. 
Then $A + B$ is compact.
== Proof ==
Since $X$ is a topological vector space, the map $+ : X \times X \to X$ defined by:
:$\map + {x, y} = x + y$
for each $x, y \in X$ is continuous.
We have:
:$A + B = + \sqbrk {A \times B}$
From Tychonoff's Theorem, $A \times B$ is compact.
From Continuous Image of Compact Space is Compact, $+ \sqbrk {A \times B} = A + B$ is therefore compact.
Category:Compact Spaces
Category:Topological Vector Spaces
Sum of Complex Conjugates

== Theorem ==
Let $z_1, z_2 \in \C$ be complex numbers.
Let $\overline z$ denote the complex conjugate of the complex number $z$.
Then:
:$\overline {z_1 + z_2} = \overline {z_1} + \overline {z_2}$
== Proof ==
Let $z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$.
Then:
== Sources ==
* : Chapter $\text I$: Functions of a Complex Variable: $\S 2$. Conjugate Complex Numbers
* : $\S 1.2$. The Algebraic Theory: $(1.6)$
* : $1$: Complex Numbers: Solved Problems: Fundamental Operations with Complex Numbers: $4 \ \text{(a)}$
* : $1$ The complex plane: Complex numbers $\S 1.3$ Complex conjugation: $(4)$
* 
Category:Complex Conjugates
Category:Complex Addition
Sum of Complex Exponentials of i times Arithmetic Sequence of Angles/Formulation 1

== Theorem ==
Let $\alpha \in \R$ be a real number such that $\alpha \ne 2 \pi k$ for $k \in \Z$.
Then:
:$\ds \sum_{k \mathop = 0}^n e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} } \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} }$
== Proof ==
First note that if $\alpha = 2 \pi k$ for $k \in \Z$, then $e^{i \alpha} = 1$.
Category:Exponential Function
Sum of Complex Exponentials of i times Arithmetic Sequence of Angles/Formulation 2

== Theorem ==
Let $\alpha \in \R$ be a real number such that $\alpha \ne 2 \pi k$ for $k \in \Z$.
Then:
:$\ds \sum_{k \mathop = 1}^n e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$
== Proof ==
First note that if $\alpha = 2 \pi k$ for $k \in \Z$, then $e^{i \alpha} = 1$.
== Sources ==
* : $\S 2$. Geometrical Representations: Example $1$
Category:Exponential Function
Sum of Complex Exponentials of i times Arithmetic Sequence of Angles/Formulation 3

== Theorem ==
Let $\alpha \in \R$ be a real number such that $\alpha \ne 2 \pi k$ for $k \in \Z$.
Then:
:$\ds \sum_{k \mathop = p}^q e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {\paren {p + q} \alpha} 2} + i \map \sin {\theta + \frac {\paren {p + q} \alpha} 2} } \frac {\map \sin {\paren {q - p + 1} \alpha / 2} } {\map \sin {\alpha / 2} }$
== Proof ==
First note that if $\alpha = 2 \pi k$ for $k \in \Z$, then $e^{i \alpha} = 1$.
Category:Exponential Function
Sum of Complex Indices of Real Number

== Theorem ==
Let $r \in \R_{> 0}$ be a (strictly) positive real number.
Let $\psi, \tau \in \C$ be complex numbers.
Let $r^\lambda$ be defined as the the principal branch of a positive real number raised to a complex number.
Then:
:$r^{\psi \mathop + \tau} = r^\psi \times r^\tau$
== Proof ==
Then:
Category:Powers
Sum of Complex Integrals on Adjacent Intervals

== Theorem ==
Let $\closedint a b$ be a closed real interval.
Let $f: \closedint a b \to \C$ be a continuous complex function.
Let $c \in \closedint a b$.
Then:
:$\ds \int_a^c \map f t \rd t + \int_c^b \map f t \rd t = \int_a^b \map f t \rd t$
== Proof ==
From Continuous Complex Function is Complex Riemann Integrable, it follows that all three complex Riemann integrals are well defined.
From Real and Imaginary Part Projections are Continuous, it follows that $\Re: \C \to \R$ and $\Im: \C \to \R$ are continuous functions.
From Composite of Continuous Mappings is Continuous, it follows that $\Re \circ f: \R \to \R$ and $\Im \circ f: \R \to \R$ are continuous real functions.
Then:
Category:Complex Analysis
Sum of Complex Number with Conjugate

== Theorem ==
Let $z \in \C$ be a complex number.
Let $\overline z$ be the complex conjugate of $z$.
Let $\map \Re z$ be the real part of $z$.
Then:
:$z + \overline z = 2 \, \map \Re z$
== Proof ==
Let $z = x + i y$.
Then:
== Also defined as ==
This result is also reported as:
:$\map \Re z = \dfrac {z + \overline z} 2$
== Sources ==
* : Chapter $\text I$: Functions of a Complex Variable: $\S 2$. Conjugate Complex Numbers
* : $1$: Complex Numbers: Supplementary Problems: Fundamental Operations with Complex Numbers: $58 \ \text{(a)}$
* : $1$ The complex plane: Complex numbers $\S 1.3$ Complex conjugation: $(2)$
* 
Category:Complex Conjugates
Sum of Complex Numbers in Exponential Form

== Theorem ==
Let $z_1 = r_1 e^{i \theta_1}$ and $z_2 = r_2 e^{i \theta_2}$ be complex numbers expressed in exponential form.
Let $z_3 = r_3 e^{i \theta_3} = z_1 + z_2$.
Then:
:$r_3 = \sqrt { {r_1}^2 + {r_2}^2 + 2 r_1 r_2 \map \cos {\theta_1 - \theta_2} }$
:$\theta_3 = \map \arctan {\dfrac {r_1 \sin \theta_1 + r_2 \sin \theta_2} {r_1 \cos \theta_1 + r_2 \cos \theta_2} }$
=== General Result ===
== Proof ==
We have:
Then:
and similarly:
:$\theta_3 = \map \arctan {\dfrac {r_1 \sin \theta_1 + r_2 \sin \theta_2} {r_1 \cos \theta_1 + r_2 \cos \theta_2} }$
== Sources ==
* : $1$: Complex Numbers: Supplementary Problems: Polar Form of Complex Numbers: $88 \ \text{(a)}$
Category:Complex Addition
Sum of Complex Numbers in Exponential Form/General Result

== Theorem ==
Let $n \in \Z_{>0}$ be a positive integer.
For all $k \in \set {1, 2, \dotsc, n}$, let:
:$z_k = r_k e^{i \theta_k}$
be non-zero complex numbers in exponential form.
Let:
:$r e^{i \theta} = \ds \sum_{k \mathop = 1}^n z_k = z_1 + z_2 + \dotsb + z_k$
Then:
== Proof ==
Let:
By the definition of the complex modulus, with $z = x + i y$, $r$ is defined as:
:$r = \sqrt {\map {\Re^2} z + \map {\Im^2} z}$
Hence
In the above we have two types of pairs of terms:
Hence:
:$\ds r = \sqrt {\sum_{k \mathop = 1}^n {r_k}^2 + \sum_{1 \mathop \le j \mathop < k \mathop \le n} 2 {r_j} {r_k} \map \cos {\theta_j - \theta_k} }$
Note that $r > 0$ since $r_k > 0$ for all $k$.
Hence we may safely assume that $r > 0$ when determining the argument below.
By definition of the argument of a complex number, with $z = x + i y$, $\theta$ is defined as any solution to the pair of equations:
:$(1): \quad \dfrac x {\cmod z} = \map \cos \theta$
:$(2): \quad \dfrac y {\cmod z} = \map \sin \theta$
where $\cmod z$ is the modulus of $z$.
As $r > 0$ we have that $\cmod z \ne 0$ by definition of modulus.
Hence we can divide $(2)$ by $(1)$, to get:
Hence:
== Sources ==
* : $1$: Complex Numbers: Supplementary Problems: Polar Form of Complex Numbers: $88 \ \text{(b)}$
Category:Complex Addition
Sum of Components of Equal Ratios

== Theorem ==
That is:
:$a_1 : b_1 = a_2 : b_2 = a_3 : b_3 = \cdots \implies \left({a_1 + a_2 + a_3 + \cdots}\right) : \left({b_1 + b_2 + b_3 + \cdots}\right)$
== Proof ==
Let any number of magnitudes $A, B, C, D, E, F$ be proportional, so that:
:$A : B = C : D = E : F$
etc.
:
Of $A, C, E$ let equimultiples $G, H, K$ be taken, and of $B, D, F$ let other arbitrary equimultiples $L, M, N$ be taken.
We have that $A : B = C : D = E : F$.
Therefore:
:$G > L \implies H > M, K > N$
:$G = L \implies H = M, K = N$
:$G < L \implies H < M, K < N$
So, in addition: 
:$G > L \implies G + H + K > L + M + N$
:$G = L \implies G + H + K = L + M + N$
:$G < L \implies G + H + K < L + M + N$
It follows from Multiplication of Numbers is Left Distributive over Addition that $G$ and $G + H + K$ are equimultiples of $A$ and $A + C + E$.
For the same reason, $L$ and $L + M + N$ are equimultiples of $B$ and $B + D + F$.
The result follows from .
== Sources ==
* : Book $\text{V}$. Propositions
Category:Ratios
Sum of Computable Rational Sequences is Computable

== Theorem ==
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:
Category:Computability Theory
Sum of Computable Real Sequences is Computable/Corollary

== Corollary to Sum of Computable Real Sequences is Computable ==
Let $\sequence {x_n}$ be a computable real sequence.
Let $c \in \R$ be a computable real number.
Then, $\sequence {x_n + c}$ is a computable real sequence.
== Proof ==
By Constant Sequence of Computable Real Number is Computable, the sequence $\sequence {y_n}$ defined as:
:$y_n = c$
is computable.
Then, by Sum of Computable Real Sequences is Computable:
:$\sequence {x_n + y_n}$
is computable.
But:
:$x_n + y_n = x_n + c$
for all $n \in \N$.
The result follows.
Category:Computability Theory
Sum of Computable Real Sequences is Computable/Proof 1

== Theorem ==
== 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:
* Addition is Primitive Recursive
* Multiplication is Primitive Recursive
* Constant Function is Primitive Recursive
* Addition of Integers is Primitive Recursive
* Multiplication of Integers is Primitive Recursive
* Quotient of Integers is Primitive Recursive
* Primitive Recursive Function is Total Recursive Function
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:
Thus, $\sequence {x_n + y_n}$ is computable by definition.
Category:Computability Theory
Sum of Computable Real Sequences is Computable/Proof 2

== Theorem ==
== Proof ==
By Computable Real Sequence iff Limits of Computable Rational Sequences, there exist:
* Computable rational sequences $\sequence {a_k}, \sequence {b_k}$
* Total recursive functions $\phi_x, \psi_x, \phi_y, \psi_y : \N^2 \to \N$
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:
* Maximum Function is Primitive Recursive
* Addition is Primitive Recursive
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:
Category:Computability Theory