avewright/proofwiki-math huggingface dataset:
Theorem: Generalized Sum with Countable Non-zero Summands

Let $V$ be a Banach space.
Let $\norm {\, \cdot \,}$ denote the norm on $V$.
Let $\family {v_i}_{i \mathop \in I}$ be an indexed family of elements of $V$.
Let $J$ be a countably infinite subset of $I$ such that $\set{i \in I : v_i \ne 0} \subseteq J$.
Let $\set {j_0, j_1, j_2, \ldots}$ be a countably infinite enumeration of $J$.
Let $r \in \R_{\mathop > 0}$.
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} v_i$ converges absolutely to $r$ 
{{iff}}:
:the series $\ds \sum_{n \mathop = 1}^\infty v_{j_n}$ converges absolutely to $r$

Proof:
From {{Corollary|Generalized Sum Restricted to Non-zero Summands}}:
:the generalized sum $\ds \sum_{i \mathop \in I} v_i$ converges absolutely to $r$ 
{{iff}}
:the generalized sum $\ds \sum_{j \mathop \in J} v_j$ converges absolutely to $r$ 
From Absolute Net Convergence Equivalent to Absolute Convergence: 
:the generalized sum $\ds \sum_{j \mathop \in J} v_j$ converges absolutely to $r$ 
{{iff}}:
:the series $\ds \sum_{n \mathop = 1}^\infty v_{j_n}$ converges absolutely to $r$
{{qed}}
Category:Generalized Sums
Category:Banach Spaces
Category:Generalized Sum with Countable Non-zero Summands
clepfyzn18sj2ko14atmcsjqynsss1u
Theorem: Neumann Series Theorem/Corollary 2

The mapping $\paren {I - A}^{-1} : X \to X$ is continuous.

Proof:
{{ProofWanted|Obviously, we have invertibility in $CL(X)$, but the source mentions $\norm x \le \frac 1 {1 - \norm A} \norm y$. A chance to have two proofs?}}
Theorem: System of Linear Equations as Continuous Linear Transformation

Let $x_1, x_2 \in \R$ be real numbers.
Consider the following system of simultaneous linear equations $\paren S$:
{{begin-eqn}}
{{eqn | l = x_1
      | r = \frac 1 2 x_1 + \frac 1 3 x_2 + 1
}}
{{eqn | l = x_2
      | r = \frac 1 3 x_1 + \frac 1 4 x_2 + 2
}}
{{end-eqn}}
Let $\norm {\, \cdot \,}_2$ be the Euclidean norm.
Let $\norm {\, \cdot \,}$ be the supremum operator norm.
Let $I$ be the $2 \times 2$ identity matrix.
Then:
:$S$ is expressible as $\paren {I - K} x = y$ where $x = \begin{pmatrix} x_1 \\ x_2 \end{pmatrix}$, $y = \begin{pmatrix} 1 \\ 2 \end{pmatrix}$, $K = \begin{pmatrix} \frac 1 2 & \frac 1 3 \\ \frac 1 3 & \frac 1 4 \end{pmatrix}$;
:$\norm K < 1$;
:$S$ admits a unique solution.
{{WIP|There is also a convergence rate estimation subproblem, but it's numerical. I would like to write an analytical analogue, but more theory is needed before I can do that.}}

Proof:
=== $\paren S$ is expressible as $\paren {I - K} x = y$ ===
We have that:
{{begin-eqn}}
{{eqn | l = x_1
     | r = \frac 1 2 x_1 + \frac 1 3 x_2 + 1
}}
{{eqn | ll = \leadsto
      | l = \frac 1 2 x_1 - \frac 1 3 x_2
      | r = 1
}}
{{end-eqn}}
Furthermore:
{{begin-eqn}}
{{eqn | l = x_1
     | r = \frac 1 2 x_1 + \frac 1 3 x_2 + 1
}}
{{eqn | l = x_2
      | r = \frac 1 3 x_1 + \frac 1 4 x_2 + 2
}}
{{eqn | ll = \leadsto
      | l = - \frac 1 3 x_1 + \frac 3 4 x_2
      | r = 2
}}
{{end-eqn}}
Hence, $\paren S$ can be rewritten as:
{{begin-eqn}}
{{eqn | l = \frac 1 2 x_1 - \frac 1 3 x_2
      | r = 1
}}
{{eqn | l = - \frac 1 3 x_1 + \frac 3 4 x_2
      | r = 2
}}
{{end-eqn}}
Moreover:
{{begin-eqn}}
{{eqn | l = I - K
      | r = \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix} - \begin{pmatrix} \frac 1 2 & \frac 1 3 \\ \frac 1 3 & \frac 1 4 \end{pmatrix}
}}
{{eqn | r = \begin{pmatrix} \frac 1 2 & -\frac 1 3 \\ -\frac 1 3 & \frac 3 4 \end{pmatrix}
}}
{{end-eqn}}
By a simple inspection it is evident that $\paren S$ is expressible as $\paren {I - K} x = y$.
{{qed|lemma}}
Theorem: Continuous Linear Transformation between Topological Vector Spaces is Bounded

Let $\GF \in \set {\R, \C}$. 
Let $X$ and $Y$ be topological vector spaces over $\GF$. 
Let $T : X \to Y$ be a continuous linear transformation.
Then $T$ is bounded.

Proof:
Let $E$ be a von Neumann-bounded subset of $X$. 
We want to show that $T \sqbrk E$ is a von Neumann-bounded subset of $Y$. 
Let $W$ be a open neighborhood of ${\mathbf 0}_Y$ in $Y$.
Since $T$ is continuous, it is continuous at $\mathbf 0_X$.
Since $\map T {\mathbf 0_X} = \mathbf 0_Y$, there exists an open neighborhood $V$ of $\mathbf 0_X$ in $X$ such that: 
:$T \sqbrk V \subseteq W$
Since $E$ is von Neumann-bounded subset, there exists $s > 0$ such that: 
:$E \subseteq t V$ for $t > s$.
Then we have: 
{{begin-eqn}}
{{eqn	| l = T \sqbrk E
		| o = \subseteq
		| r = T \sqbrk {t V}
		| c = Image of Subset under Mapping is Subset of Image
}}
{{eqn	| r = t T \sqbrk V
		| c = Image of Dilation of Set under Linear Transformation is Dilation of Image
}}
{{eqn	| o = \subseteq
		| r = t W
}}
{{end-eqn}}
for $t > s$. 
Since $W$ was an arbitrary open neighborhood of ${\mathbf 0}_Y$ in $Y$, we have that $T \sqbrk E$ is von Neumann-bounded.
So $T$ is bounded.
{{qed}}
Theorem: Image of Convergent Sequence in Topological Vector Space under Bounded Linear Transformation is von Neumann-Bounded

Let $\GF \in \set {\R, \C}$. 
Let $X$ and $Y$ be topological vector spaces over $\GF$. 
Let $T : X \to Y$ be a bounded linear transformation.
Let $\sequence {x_n}_{n \in \N}$ be a convergent sequence in $X$. 
Then $\set {T x_n : n \in \N}$ is a von Neumann-bounded subset of $Y$.

Proof:
Let:
:$E = \set {x_n : n \in \N}$
From Image of Convergent Sequence in Topological Vector Space is von Neumann-Bounded, $E$ is von Neumann-bounded.
So, from the definition of a bounded linear transformation:
:$T \sqbrk E = \set {T x_n : n \in \N}$ is von Neumann-bounded.
{{qed}}
Theorem: Uniform Mean Ergodic Theorem

Let $\GF \in \set {\R, \C}$.
Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space over $\mathbb F$.
Let $U : \HH \to \HH$ be a bounded linear operator such that:
:$\forall f \in \HH : \norm {\map U f} \le \norm f$
Then for each $f \in \HH$:
:$\ds \lim_{N - M \mathop \to \infty} \dfrac 1 {N - M} \sum_{n \mathop = M}^{N - 1} \map {U^n} f = \map P f$
i.e.
:$\ds \forall \epsilon \in \R_{>0}: \exists K \in \N: \forall M,N \in \N: N - M \ge K \implies  \norm {\frac 1 {N - M} \sum_{n \mathop = M}^{N - 1} \map {U^n} f - \map P f} \le \epsilon$
where:
:$U^n$ denotes the $n$ times composition of $U$
:$I := \set {f \in \HH : \map U f = f}$
:$P : \HH \to I$ denotes the orthogonal projection on $I$

Proof:
{{begin-eqn}}
{{eqn | l = \norm {\frac 1 {N - M} \sum_{n \mathop = M}^{N - 1} \map {U^n} f - \map P f}
      | r = \norm {\frac 1 {N - M} \sum_{n \mathop = 0}^{N - M - 1} \map {U^{M+n} } f - \map P f}
}}
{{eqn | r = \norm {\frac 1 {N - M} \sum_{n \mathop = M}^{N - 1} \map {U^{M+n} } f - \map {U^M} {\map P f} }
      | c  = as $\map P f \in I$
}}
{{eqn | r = \norm {\map {U^M} {\frac 1 {N - M} \sum_{n \mathop = 0}^{N - M - 1} \map {U^n} f - \map P f} }
}}
{{eqn | o = \le
      | r = \norm {\frac 1 {N - M} \sum_{n \mathop = 0}^{N - M - 1} \map {U^n} f - \map P f}
      | c = {{hypothesis}}
}}
{{eqn | o = \to
      | r = 0
      | c = as $N - M \to \infty$ due to Mean Ergodic Theorem
}}
{{end-eqn}}
{{qed}}
Theorem: Cantor Pairing Function is Well-Defined

The Cantor pairing function is well-defined.

Proof:
By definition, the Cantor pairing function $\pi : \N^2 \to \N$ is:
:$\ds \map \pi {m, n} = \frac 1 2 \paren {m + n} \paren {m + n + 1} + m$
It suffices to show that, for every $m, n \in \N$:
:$\paren {m + n} \paren {m + n + 1}$
is divisible by $2$.
Suppose that $m + n$ is even.
Then, by definition, $2 \divides \paren {m + n}$.
Thus, by Divisor Divides Multiple:
:$2 \divides \paren {m + n} \paren {m + n + 1}$
Suppose that $m + n$ is not even.
Then, by definition, $m + n$ is odd.
But then, by definition, there exists some $k \in \Z$ such that:
:$m + n = 2k + 1$
Then:
{{begin-eqn}}
{{eqn | l = \paren {m + n} \paren {m + n + 1}
      | r = \paren {2k + 1} \paren {2k + 2}
}}
{{eqn | r = \paren {2k + 1} \paren {2 \paren {k + 1} } }}
{{end-eqn}}
By definition, $2 \paren {k + 1}$ is even.
But then, by definition, $2 \divides 2 \paren {k + 1}$.
Therefore, by Divisor Divides Multiple:
:$2 \divides \paren {2k + 1} \paren {2 \paren {k + 1} } = \paren {m + n} \paren {m + n + 1}$
By Proof by Cases, $\paren {m + n} \paren {m + n + 1}$ is divisible by $2$.
{{qed}}
Category:Cantor Pairing Function
5ek6gxyc5211ff8s0w5tb9y183hnusx
Theorem: Inverse of Cantor Pairing Function

Let $\pi : \N^2 \to \N$ be the Cantor pairing function.
Define $k : \N \to \N$ as:
:$\map k z$ is the largest $k$ such that $T_k \le z$
where $T_k$ is the $k$-th triangular number.
Let $\pi_1 : \N \to \N$ be defined as:
:$\ds \map {\pi_1} z = z - T_{\map k z}$
Let $\pi_2 : \N \to \N$ be defined as:
:$\map {\pi_2} z = \map k z - \map {\pi_1} z$
Then:
* $\pi_1$ and $\pi_2$ are well-defined
* For every $z \in \N$:
::$\map \pi {\map {\pi_1} z, \map {\pi_2} z} = z$
* For every $x, y \in \N$:
::$\map {\pi_1} {\map \pi {x, y}} = x$
::$\map {\pi_2} {\map \pi {x, y}} = y$

Proof:
By definition of $\map k z$, we have $T_{\map k z} \le z$.
Thus, $z - T_{\map k z} \ge 0$.
Therefore, $\pi_1$ is well-defined.
{{AimForCont}} $\map {\pi_1} z > \map k z$.
That is:
:$z > T_{\map k z} + \map k z$
Or:
:$z \ge T_{\map k z} + \map k z + 1 = T_{\map k z + 1}$
which contradicts the maximality of $\map k z$.
Thus, by Proof by Contradiction:
:$\map {\pi_1} z \le \map k z$
Therefore:
:$\map k z - \map {\pi_1} z \ge 0$
and $\pi_2$ is well-defined.
{{qed|lemma}}
Let $z \in \N$ be arbitrary.
We have:
{{begin-eqn}}
{{eqn | l = \map \pi {\map {\pi_1} z, \map {\pi_2} z}
      | r = \frac 1 2 \paren {\map {\pi_1} z + \map {\pi_2} z} \paren {\map {\pi_1} z + \map {\pi_2} z + 1} + \map {\pi_1} z
      | c = {{Defof|Cantor Pairing Function}}
}}
{{eqn | r = \frac 1 2 \paren {\map k z} \paren {\map k z + 1} + \map {\pi_1} z
      | c = Definition of $\pi_2$
}}
{{eqn | r = T_{\map k z} + \map {\pi_1} z
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = z
      | c = Definition of $\pi_1$
}}
{{end-eqn}}{{qed|lemma}}
Let $x, y \in \N$ be arbitrary.
We have:
{{begin-eqn}}
{{eqn | l = \map \pi {x, y}
      | r = \frac 1 2 \paren {x + y} \paren {x + y + 1} + x
      | c = {{Defof|Cantor Pairing Function}}
}}
{{eqn | r = T_{x + y} + x
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
Since:
:$T_{x + y} + x \ge T_{x + y}$
we have:
:$\map k {\map \pi {x, y}} \ge x + y$
Since:
:$x \le x + y$
we have:
:$T_{x + y} + x \le T_{x + y} + \paren {x + y + 1} = T_{x + y + 1}$
Hence:
:$\map k {\map \pi {x, y}} < x + y + 1$
Therefore:
:$\map k {\map \pi {x, y}} = x + y$
It follows:
{{begin-eqn}}
{{eqn | l = \map {\pi_1} {\map \pi {x, y} }
      | r = \map \pi {x, y} - T_{\map k {\map \pi {x, y} } }
      | c = Definition of $\pi_1$
}}
{{eqn | r = \map \pi {x, y} - T_{x + y}
      | c = Above
}}
{{eqn | r = T_{x + y} + x - T_{x + y}
      | c = Above
}}
{{eqn | r = x
}}
{{end-eqn}}
And:
{{begin-eqn}}
{{eqn | l = \map {\pi_2} {\map \pi {x, y} }
      | r = \map k {\map \pi {x, y} } - \map {\pi_1} {\map \pi {x, y} }
      | c = Definition of $\pi_2$
}}
{{eqn | r = x + y - x
      | c = Both above
}}
{{eqn | r = y
}}
{{end-eqn}}{{qed}}
Category:Cantor Pairing Function
5i6sl7qok3kw7xvctgz527r83dxd8ho
Theorem: Expression for Closure of Set in Topological Vector Space/Corollary

Let $\BB$ be a local basis for ${\mathbf 0}_X$ in $\struct {X, \tau}$. 
Then:
:$\ds A^- = \bigcap_{V \in \BB} \paren {A + V}$
where $A^-$ is the closure of $A$.

Proof:
Let $\VV$ be the set of open neighborhoods of ${\mathbf 0}_X$ in $\struct {X, \tau}$.
From Intersection is Decreasing, we have: 
:$\ds \bigcap_{V \in \mathcal V} \paren {A + V} \subseteq \bigcap_{V \in \BB} \paren {A + V}$
Conversely, suppose that:
:$\ds x \in \bigcap_{V \in \BB} \paren {A + V}$
Let $O \in \VV$.
Since $\BB$ is a local basis for ${\mathbf 0}_X$ in $\struct {X, \tau}$, there exists $U \in \BB$ such that $U \subseteq O$.
Since $x \in A + V$ for each $V \in \BB$, we in particular have $x \in A + U$. 
Since $U \subseteq O$, we have that $x \in A + O$.
Since $O \in \VV$ was arbitrary, we have:
:$\ds x \in \bigcap_{V \in \BB} \paren {A + V}$
{{qed}}
Category:Expression for Closure of Set in Topological Vector Space
ohvirkbwuedzl34c9phizz1m5vf7sne
Theorem: Locally Compact Hausdorff Topological Vector Space has Finite Dimension

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \tau}$ be a locally compact Hausdorff topological vector space over $\GF$. 
Then $X$ is a finite dimensional vector space.

Proof:
Since $X$ is locally compact, there exists a von Neumann-bounded open neighborhood $V$ of ${\mathbf 0}_X$ such that: 
:$\map \cl V$ is compact.
From Dilations of von Neumann-Bounded Neighborhood of Origin in Topological Vector Space form Local Basis for Origin:
:$\BB = \set {2^{-n} V : n \in \N}$ is a local basis for ${\mathbf 0}_X$.
We have that:
:$\ds \map \cl V \subseteq \bigcup_{x \in X} \paren {x + \frac 1 2 V}$
Since $\map \cl V$ is compact, there exists $x_1, \ldots, x_m \in X$ such that:
:$\ds \map \cl V \subseteq \bigcup_{j \mathop = 1}^m \paren {x_j + \frac 1 2 V}$
Let:
:$Y = \span \set {x_j : 1 \le j \le m}$
Then $Y$ is finite dimensional.
We show that $Y = X$.
From Finite-Dimensional Subspace of Hausdorff Topological Vector Space is Closed, $Y$ is closed.
Theorem: Locally Bounded Hausdorff Topological Vector Space with Heine-Borel Property has Finite Dimension

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \tau}$ be a locally bounded Hausdorff topological vector space over $\GF$ with the Heine-Borel property.
Then $X$ is a finite dimensional vector space.

Proof:
Since $\struct {X, \tau}$ is locally bounded, there exists a von Neumann-bounded open neighborhood $V$ of ${\mathbf 0}_X$. 
From Closure of von Neumann-Bounded Subset of Topological Vector Space is von Neumann-Bounded, $\map \cl V$ is von Neumann-bounded.
From Topological Closure is Closed, $\map \cl V$ is closed.
So $\map \cl V$ is von Neumann-bounded and closed.
From the Heine-Borel property, $\map \cl V$ is compact.
So $V$ is an open neighborhood of ${\mathbf 0}_X$ with compact closure.
Hence $X$ is locally compact.
Hence from Locally Compact Hausdorff Topological Vector Space has Finite Dimension, $X$ is a finite dimensional vector space.
{{qed}}
Theorem: Union of Chain of Convex Sets in Vector Space is Convex

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$. 
Let $\Gamma$ be a chain of convex sets. 
Let:
:$\ds C = \bigcup \Gamma$
Then $C$ is convex.

Proof:
Let $t \in \closedint 0 1$ and $x, y \in C$. 
Then there exists $C_1, C_2 \in \Gamma$ such that $x \in C_1$ and $y \in C_2$.
Since $\Gamma$ is a chain, we have $C_1 \subseteq C_2$ or $C_2 \subseteq C_1$.
{{WLOG}} suppose that $C_1 \subseteq C_2$.
Then $x, y \in C_2$.
Since $C_2$ is convex, we have $t x + \paren {1 - t} y \in C_2$.
So $t x + \paren {1 - t} y \in \bigcup \Gamma = C$.
So $C$ is convex.
{{qed}}
Category:Convex Sets (Vector Spaces)
nb67luf9qq4hpjh290yl2slox1xx1li
Theorem: Least Fixed Point of Enumeration Operator

Let $\psi : \powerset \N \to \powerset \N$ be an enumeration operator.
Let $A_i$ be defined recursively as:
{{begin-eqn}}
{{eqn | l = A_0
      | r = \O
}}
{{eqn | l = A_{n + 1}
      | r = \map \psi {A_n}
}}
{{end-eqn}}
Let $A = \ds \bigcup_{i \mathop \in \N} A_i$.
Then:
* $A$ is a fixed point of $\psi$
* Every fixed point of $\psi$ is a superset of $A$

Proof:
=== Lemma ===
{{:Least Fixed Point of Enumeration Operator/Lemma}}{{qed|lemma}}
By definition of enumeration operator, let $\phi \subseteq \N$ be a recursively enumerable set that yields $\psi$.
Theorem: Image of Interior of Set under Homeomorphism is Interior of Image

Let $X$ and $Y$ be topological spaces.
Let $f : X \to Y$ be a homeomorphism.
Let $A \subseteq X$.
Then:
:$\paren {f \sqbrk A}^\circ = f \sqbrk {A^\circ}$
where:
:$A^\circ$ is the interior of $A$ in $X$
:$\paren {f \sqbrk A}^\circ$ is the interior of $f \sqbrk A$ in $Y$.

Proof:
First, we show that $f \sqbrk {A^\circ} \subseteq \paren {f \sqbrk A}^\circ$. 
Let $y \in f \sqbrk {A^\circ}$.
Then there exists $x \in A^\circ$ such that $y = \map f x$.
Since $x \in A^\circ$, there exists an open set $U \subseteq A$ in $X$ such that $x \in U$.
Then $y = \map f x \in f \sqbrk U \subseteq f \sqbrk A$.
By definition of a homeomorphism, $f$ is an open map.
So $f \sqbrk U$ is an open set in $Y$ contained in $f \sqbrk A$ and containing $y$.
So from the definition of interior, we have $y \in \paren {f \sqbrk A}^\circ$. 
Hence $y \in f \sqbrk {A^\circ}$ implies that $y \in \paren {f \sqbrk A}^\circ$.
So $f \sqbrk {A^\circ} \subseteq \paren {f \sqbrk A}^\circ$.
{{qed|lemma}}
Now we show that $\paren {f \sqbrk A}^\circ \subseteq f \sqbrk {A^\circ}$. 
Let $y \in \paren {f \sqbrk A}^\circ$.
Then there exists an open set $V \subseteq f \sqbrk A$ in $Y$ such that $y \in V$.
We then have $\map {f^{-1} } y \in f^{-1} \sqbrk V$.
Further, from Preimage of Image of Subset under Injection equals Subset and Image of Subset under Mapping is Subset of Image, we have $f^{-1} \sqbrk V \subseteq A$. 
Since $f$ is continuous, $f^{-1} \sqbrk V$ is open in $X$, is contained in $A$ and contains $\map {f^{-1} } y$.
So we have $\map {f^{-1} } y \in A^\circ$.
Since $y = \map f {\map {f^{-1} } y}$, we obtain $y \in f \sqbrk {A^\circ}$.
Hence $y \in \paren {f \sqbrk A}^\circ$ implies $y \in f \sqbrk {A^\circ}$.
So $\paren {f \sqbrk A}^\circ \subseteq f \sqbrk {A^\circ}$. 
Hence we obtain $\paren {f \sqbrk A}^\circ = f \sqbrk {A^\circ}$.
{{qed}}
Category:Homeomorphisms (Topological Spaces)
Category:Set Interiors
raoxoq7h8emvbockmhjtm0zwd6zmn2b
Theorem: Homeomorphic Image of Nowhere Dense Set is Nowhere Dense

Let $X$ and $Y$ be topological spaces.
Let $f : X \to Y$ be a homeomorphism.
Let $A$ be a nowhere dense subset of $X$.
Then $f \sqbrk A$ is a nowhere dense subset of $Y$.

Proof:
Since $A$ is nowhere dense, we have:
:$\paren {A^-}^\circ = \O$
where $A^-$ is the closure of $A$ and $\paren {A^-}^\circ$ is the interior of $A^-$.
From Image of Empty Set is Empty Set, we have:
:$\O = f \sqbrk {\paren {A^-}^\circ}$
So, we have:
{{begin-eqn}}
{{eqn	| l = f \sqbrk {\paren {A^-}^\circ}
		| r = \paren {f \sqbrk {A^-} }^\circ
		| c = Image of Interior of Set under Homeomorphism is Interior of Image
}}
{{eqn	| r = \paren {\paren {f \sqbrk A}^-}^\circ
		| c = Homeomorphism iff Image of Closure equals Closure of Image
}}
{{eqn	| r = \O
}}
{{end-eqn}}
Hence $f \sqbrk A$ is a nowhere dense subset of $Y$.
{{qed}}
Category:Nowhere Dense
Category:Homeomorphisms (Topological Spaces)
cgvwkv9ngwv7kr3odqzkpxsvrntif2j
Theorem: Cantor Pairing Function is Primitive Recursive

The Cantor pairing function is primitive recursive.

Proof:
The Cantor pairing function $\pi : \N^2 \to \N$ is defined as:
:$\map \pi {m, n} = \frac 1 2 \paren {m + n} \paren {m + n + 1} + m$
As Cantor Pairing Function is Well-Defined, the function could also be defined as:
:$\map \pi {m, n} = \map {\operatorname{quot}} {\paren {m + n} \paren {m + n + 1}, 2} + m$
which is primitive recursive, as it is obtained by substitution from:
* Addition is Primitive Recursive
* Quotient is Primitive Recursive
* Constant Function is Primitive Recursive
{{qed}}
Category:Cantor Pairing Function
dhvml6c4gt35exz9lmh57hktw72otzd
Theorem: Generalized Sum with Countable Non-zero Summands/Corollary

Let $\set{j_0, j_1, j_2, \ldots}$ and $\set{k_0, k_1, k_2, \ldots}$ be countably infinite enumerations of $J$ and $K$ respectively.
Let $r \in \R_{\mathop > 0}$.
Then:
:the series $\ds \sum_{n \mathop = 1}^\infty v_{j_n}$ converges absolutely to $r$
{{iff}}:
:the series $\ds \sum_{n \mathop = 1}^\infty v_{k_n}$ converges absolutely to $r$

Proof:
From Generalized Sum with Countable Non-zero Summands:
:the series $\ds \sum_{n \mathop = 1}^\infty v_{j_n}$ converges absolutely to $r$
{{iff}}
:the generalized sum $\ds \sum_{i \mathop \in I} v_i$ converges absolutely to $r$
{{iff}}:
:the series $\ds \sum_{n \mathop = 1}^\infty v_{k_n}$ converges absolutely to $r$
{{qed}}
Category:Generalized Sum with Countable Non-zero Summands
nlx2jm7qidq8vq42a1pe40zz5rb0y7c
Theorem: Length of Basis Representation is Primitive Recursive

Define $\operatorname{basislen} : \N^2 \to \N$ as:
:$\map {\operatorname{basislen}} {b, n} = \begin{cases}m + 1 & : b > 1 \land n > 0 \\n & : b = 1 \\0 & : b = 0 \lor n = 0\end{cases}$
where $\sqbrk {r_m r_{m - 1} \dotsm r_1 r_0}_b$ is the base-$b$ representation of $n$.
Then $\operatorname{basislen}$ is primitive recursive.

Proof:
By:
* Definition by Cases is Primitive Recursive
* Ordering Relations are Primitive Recursive
* Equality Relation is Primitive Recursive
* Constant Function is Primitive Recursive
* Set Operations on Primitive Recursive Relations
all that needs to be shown is that $m + 1$ can be computed from $n$ in the case that $b > 1$ and $n > 0$.
By the definition of base-$b$ representation:
:$\ds n = \sum_{i \mathop = 0}^m r_i b^i$
Let $m' \le m$ be arbitrary.
Since $r_m > 0$, it follows that:
:$b^{m'} \le r_m b^m \le n$
Therefore:
:$m' \le m \implies b^{m'} \le n$
Now, let $m' > m$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = n
      | r = \sum_{j \mathop = 0}^m r_j b^j
}}
{{eqn | o = \le
      | r = \sum_{j \mathop = 0}^m \paren {b - 1} b^j
      | c = Every $r_j \le b - 1$
}}
{{eqn | o = \le
      | r = \sum_{j \mathop = 0}^{m'} \paren {b - 1} b^j
      | c = $m \le m' - 1$
}}
{{eqn | r = \frac {\paren {b - 1} \paren {b^{m'} - 1} } {b - 1}
      | c = {{Corollary|Sum of Geometric Sequence|1}}
}}
{{eqn | r = b^{m'} - 1
}}
{{eqn | o = <
      | r = b^{m'}
}}
{{end-eqn}}
Therefore:
:$m' > m \implies b^{m'} > n$
Thus, $m + 1$ is the smallest $k \in \N$ such that:
:$b^k > n$
The result follows from:
* Exponentiation is Primitive Recursive
* Ordering Relations are Primitive Recursive
* Bounded Minimization is Primitive Recursive
assuming we can find some function $\map g n$ such that:
:$\map g n \ge m + 1$
for every $n$.
By Basis Representation is No Longer than Number:
:$\map g n = n$
suffices.
{{qed}}
Category:Basis Representations
Category:Primitive Recursive Functions
8z7sgz48c7lp4e31xyapnsmmcfee7pw
Theorem: Basis Representation is No Longer than Number

Let $b > 1$ and $n > 0$ be natural numbers.
Let the base-$b$ representation of $n$ be:
:$\sqbrk {r_m r_{m - 1} \dotsm r_1 r_0}_b$
Then:
:$n > m$

Proof:
{{Tidy}}
;Base case: $(n=1)$
{{begin-eqn}}
{{eqn | l = \sqbrk 1_b
      | r = b^0
      | c = From Basis Representation Theorem
}}
{{eqn | r = 1
      | c = From Zeroth Power of Real Number equals One
}}
{{end-eqn}}
;Inductive case: $(k\implies k+1)$
;; Subcase 1: $\exists i \in \set {0, \dots, m}, j < i \implies r_j = b - 1$
{{begin-eqn}}
{{eqn | l = n + 1
      | r = \sum_{j \mathop = 0}^m r_j b^j + 1
      | c = {{hypothesis}} and Basis Representation Theorem
}}
{{eqn | r = \sum_{j \mathop = i}^m r_j b^j + \sum_{j \mathop = 0}^{i - 1} \paren {b - 1} b^j + 1
      | c = From subcase hypothesis
}}
{{eqn | r = \sum_{j \mathop = i}^m r_j b^j + \sum_{j \mathop = 0}^{i - 1} b^{j + 1} - b^j + 1
}}
{{eqn | r = \sum_{j \mathop = i}^m r_j b^j + b^i - b^0 + 1
      | c = From Telescoping Series with $a_n = b^{n + 1}$
}}
{{eqn | r = \sum_{j \mathop = i}^m r_j b^j + b^i - 1 + 1
      | c = Zeroth Power of Real Number equals One
}}
{{eqn | r = \sum_{j \mathop = i + 1}^m r_j b^j + r_i b^i + b^i
}}
{{eqn | r = \sum_{j \mathop = i + 1}^m r_j b^j + \paren {r_i + 1} b^i
}}
{{end-eqn}}
Then from Basis Representation Theorem:
:$n + 1 = \sqbrk {r_m r_{m - 1} \dots r_{i + 1} \paren {r_i + 1} 0 \dots 0}_b$
thus the length of the base-$b$ representation of $n + 1$ is $m$.
From the induction hypothesis we have that $m < n$, then
:$n + 1 > n > m$
;;Subcase 2: $\forall i \in \set {0, \dots, m}, r_i = b-1$
{{begin-eqn}}
{{eqn | l = n + 1
      | r = \sum_{i \mathop = 0}^m \paren {b - 1} b^i + 1
      | c = from original and subcase hypotheses and Basis Representation Theorem
}}
{{eqn | r = \sum_{i \mathop = 0}^m b^{i + 1} - b^i + 1
}}
{{eqn | r = b^{m + 1} - b^0 + 1
      | c = Telescoping Series with $a_n = b^{n + 1}$
}}
{{eqn | r = b^{m + 1} 
      | c = Zeroth Power of Real Number equals One and simplifying
}}
{{end-eqn}}
Then from Basis Representation Theorem we see that:
:$n + 1 = \sqbrk {1 \underbrace {0 \dots 0}_{m \text{ times} } }_b$
thus the length of the base-$b$ representation of $n + 1$ is $m + 1$.
From inductive hypothesis, we have that $n > m$, then we have:
:$n + 1 > m + 1$
{{qed}}
Category:Number Bases
be9upagma9ulfa5debt8b4w1wjj9us0