avewright/proofwiki-math huggingface dataset:
Theorem: Characterization of Generalized Hilbert Sequence Space

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $H^\alpha = \struct{A, d_2}$ be the generalized Hilbert sequence space of weight $\alpha$ where:
:$A$ denotes the set of all real-valued functions $x : I \to \R$ such that:
::$(1)\quad \set{i \in I: x_i \ne 0}$ is countable
::$(2)\quad$ the generalized sum $\ds \sum_{i \mathop \in I} x_i^2$ is a convergent net.
Let $H = \struct{\ell^2, d_{\ell^2}}$ denote the Hilbert sequence space, where:
:$\ell^2$ denotes the real $2$-sequence space, that is, the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{n \mathop = 0}^\infty x_n^2$ is convergent
Let $x_1, x_2, \ldots, x_m : I \to \R$ be real-valued functions.
Then:
:$x_1, x_2, \ldots, x_m \in A$ 
{{iff}}
:there exists an enumeration $\set{j_0, j_1, j_2, \ldots}$ of a countably infinite subset of $I$ such that $\forall k \in \closedint 1 m$:
::$(1)\quad\set{i \in I : \paren{x_k}_i \ne 0} \subseteq \set{j_0, j_1, j_2, \ldots}$
::$(2)\quad\sequence{\paren{x_k}_{j_n}} \in \ell^2$   
In which case:
:$\forall k \in \closedint 1 m : \ds \sum_{i \mathop \in I} \paren{\paren{x_k}_i}^2 = \sum_{n \mathop = 0}^\infty \paren{\paren{x_k}_{j_n}}^2$

Proof:
=== Necessary Condition ===
Let $x_1, x_2, \ldots, x_m \in A$.
{{:Characterization of Generalized Hilbert Sequence Space/Necessary Condition}}{{qed|lemma}}
Theorem: Angle is not Invariant under Affine Transformation

The angle between two (straight) lines does not necessarily stay the same under an affine transformation.

Proof:
{{tidy}}
{{Proofread}}
In order to prove this, we can supply a counter example. Consider the transformation:
\[ \LL : \mathbb{R}^2 \rightarrow \mathbb{R}^2 \\ \LL : \paren {x, y} \mapsto \paren{x, x + y} \]
We can check that $\LL$ is an affine transformation. Indeed, if we denote $A = \paren{x_A, y_A}$ and $B = \paren{x_B, y_B}$ two points of the Euclidean plane, then we have:
\[ \LL (A) - \LL (B) = \paren{x_A - x_B, x_A - x_B + y_A - y_B} = \paren{x_\vec{AB}, x_\vec{AB} + y_\vec{AB}}\]
This final expression being a linear transformation of $\vec{AB}$, it follows that $\LL$ is indeed an affine transformation.
Furthermore, the $x$-axis represented by the equation $Ox: y=0$ is transformed into $\LL (Ox) : x + y = 0$, and the $y$-axis represented by the equation $Oy: x=0$ is transformed into $\LL (Oy) : x = 0$.
Finally putting the pieces together, we see that $\angle \paren{Ox,Oy} = \frac{\pi}{2} \ne \frac{\pi}{4} = \angle \paren{\LL (Ox), \LL (Oy)}$.
That is to say, the angle between two lines does not necessarily stay the same under an affine transformation.
Theorem: Term of Computable Real Sequence is Computable

Let $\sequence {x_i}$ be a computable real sequence.
Then, for each $i \in \N$:
:$x_i$ is a computable real number.

Proof:
By definition of computable real sequence, there exists a total recursive function $f : \N^2 \to \N$ such that:
:For every $m,n \in \N$, $\map f {m, n}$ codes an integer $k$ such that:
::$\dfrac {k - 1} {n + 1} < x_m < \dfrac {k + 1} {n + 1}$
Let $g : \N \to \N$ be defined as:
:$\map g n = \map f {i, n}$
By:
* Constant Function is Primitive Recursive
* Primitive Recursive Function is Total Recursive Function
it follows that $g$ is a total recursive function.
Additionally, for every $n \in \N$, $\map g n$ codes an integer $k$ such that:
:$\dfrac {k - 1} {n + 1} < x_i < \dfrac {k + 1} {n + 1}$
Thus, by definition, $x_i$ is a computable real number.
{{qed}}
Category:Computability Theory
o5ch5dfax0a4fd0u22hwmhk4nmtbm5w
Theorem: Composition of Sequentially Computable Real Functions is Sequentially Computable

Let $f,g : \R \to \R$ be sequentially computable real functions.
Let $h : \R \to \R$ be defined as:
:$\map h x = \map f {\map g x}$
Then $h$ is sequentially computable.

Proof:
Let $\sequence {x_n}$ be a computable real sequence.
As $g$ is sequentially computable:
:$\sequence {\map g {x_n}}$
is computable.
As $f$ is sequentially computable:
:$\sequence {\map f {\map g {x_n}}}$
is computable.
But:
:$\map f {\map g {x_n}} = \map h {x_n}$
Therefore:
:$\sequence {\map h {x_n}}$
is computable.
As $\sequence {x_n}$ was arbitrary, $h$ is sequentially computable by definition.
{{qed}}
Category:Computability Theory
f71114bmp0i8cocqjb94yp3aurxb77u
Theorem: Composition of Computably Uniformly Continuous Real Functions is Computably Uniformly Continuous

Let $f,g : \R \to \R$ be computably uniformly continuous real functions.
Let $h : \R \to \R$ be defined as:
:$\map h x = \map f {\map g x}$
Then $h$ is computably uniformly continuous.

Proof:
By definition of computably uniformly continuous, there exist total recursive functions $d_f, d_g : \N \to \N$ such that:
:For all $n \in \N$ and $x,y \in \R$ such that:
::$\size {x - y} < \dfrac 1 {\map {d_f} n + 1}$
:it holds that:
::$\size {\map f x - \map f y} < \dfrac 1 {n + 1}$
and:
:For all $n \in \N$ and $x,y \in \R$ such that:
::$\size {x - y} < \dfrac 1 {\map {d_g} n + 1}$
:it holds that:
::$\size {\map g x - \map g y} < \dfrac 1 {n + 1}$
Define:
:$\map {d_h} n = \map {d_g} {\map {d_f} n}$
As $d_h$ is obtained by substitution on recursive functions, it is also recursive.
As both of those functions are total, it follows that $d_h$ is also total.
Now, let $n \in \N$ and $x,y \in \R$ satisfy:
:$\size {x - y} < \dfrac 1 {\map {d_h} n + 1}$
By definition of $d_h$:
:$\size {x - y} < \dfrac 1 {\map {d_g} {\map {d_f} n} + 1}$
By assumption on $d_g$:
:$\size {\map g x - \map g y} < \dfrac 1 {\map {d_f} n + 1}$
By assumption on $d_f$:
:$\size {\map f {\map g x} - \map f {\map g y}} < \dfrac 1 {n + 1}$
But:
:$\map f {\map g x} = \map h x$
:$\map f {\map g y} = \map h y$
Thus:
:$\size {\map h x - \map h y} < \dfrac 1 {n + 1}$
As $n$, $x$, and $y$ were arbitrary, $h$ is computably uniformly continuous by definition.
{{qed}}
Category:Computability Theory
97moztss00yewjkj6imm7rnv9oin66l
Theorem: Composition of Computable Real Functions is Computable

Let $f,g : \R \to \R$ be computable real functions.
Let $h : \R \to \R$ be defined as:
:$\map h x = \map f {\map g x}$
Then $h$ is computable.

Proof:
Follows immediately from:
* Composition of Sequentially Computable Real Functions is Sequentially Computable
* Composition of Computably Uniformly Continuous Real Functions is Computably Uniformly Continuous
{{qed}}
Category:Computability Theory
ofoolc2elb33ytmx1gwfgj53r7qe4hk
Theorem: Constant Sequence of Computable Real Number is Computable

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

Proof:
By definition of computable real number, there exists a total recursive function $f : \N \to \N$ such that:
:For every $n \in \N$, $\map f n$ codes an integer $k$ such that:
::$\dfrac {k - 1} {n + 1} < a < \dfrac {k + 1} {n + 1}$
Let $g : \N^2 \to \N$ be defined as:
:$\map g {m, n} = \map f n$
As $f$ is total recursive, it follows immediately that $g$ is also total recursive.
Let $m, n \in \N$ be arbitrary.
By definition of $g$:
:$\map g {m, n} = \map f n$
Thus, by assumption:
:$\map g {m, n}$ codes an integer $k$ such that:
::$\dfrac {k - 1} {n + 1} < a < \dfrac {k + 1} {n + 1}$
But, as $x_m = a$:
:$\map g {m, n}$ codes an integer $k$ such that:
::$\dfrac {k - 1} {n + 1} < x_m < \dfrac {k + 1} {n + 1}$
As $m$ and $n$ were arbitrary, $\sequence {x_n}$ is computable by definition.
{{qed}}
Category:Computability Theory
c9uik4y6j5edo7yxjlsys26jt928n2z
Theorem: Image of Computable Real Number over Sequentially Computable Real Function is Computable

Let $f : \R \to \R$ be a sequentially computable real function.
Let $a \in \R$ be a computable real number.
Then, $\map f a$ is a computable real number.

Proof:
Let $\sequence {x_n}$ be defined as:
:$x_n = a$
By Constant Sequence of Computable Real Number is Computable:
:$\sequence {x_n}$ is a computable real sequence.
As $f$ is sequentially computable:
:$\sequence {\map f {x_n}}$ is computable.
By Term of Computable Real Sequence is Computable:
:$\map f {x_0}$ is computable.
But, $x_0 = a$ by definition.
Thus:
:$\map f a$ is computable.
{{qed}}
Category:Computability Theory
0wiemvg96m12hzl747pbdgy21ik75ga
Theorem: Identity Function is Sequentially Computable Real Function

Let $I_\R : \R \to \R$ denote the identity function on $\R$.
Then $I_\R$ is a sequentially computable real function.

Proof:
Let $\sequence {x_n}$ be a computable real sequence.
By definition of identity function:
:$\map {I_\R} x = x$
Therefore:
:$\sequence {\map {I_\R} {x_n}} = \sequence {x_n}$
and is thus computable.
As $\sequence {x_n}$ was arbitrary, it follows that $I_\R$ is sequentially computable by definition.
{{qed}}
Category:Computability Theory
fyphnejsze7clxp14ho07muwku8v4ly
Theorem: Identity Function is Computably Uniformly Continuous Real Function

Let $I_\R : \R \to \R$ denote the identity function on $\R$.
Then, $I_\R$ is a computably uniformly continuous real function.

Proof:
Let $d : \N \to \N$ be defined as:
:$\map d n = n$
As $d$ is precisely the projection function $\pr_1^1$, it is primitive recursive.
By Primitive Recursive Function is Total Recursive Function, $d$ is a total recursive function.
Let $n \in \N$ and $x, y \in \R$ satisfy:
:$\size {x - y} < \dfrac 1 {\map d n + 1}$
By definition of identity function:
:$\map {I_\R} x = x$
:$\map {I_\R} y = y$
By definition of $d$:
:$\map d n = n$
Thus:
:$\size {\map {I_\R} x - \map {I_\R} y} < \dfrac 1 {n + 1}$
As $n$, $x$, and $y$ were arbitrary, it follows that $I_\R$ is computably uniformly continuous by definition.
{{qed}}
Category:Computability Theory
03wy32hnx1segpymx20c3bfz3ul8vml
Theorem: Identity Function is Computable Real Function

Let $I_\R : \R \to \R$ denote the identity function on $\R$.
Then $I_\R$ is a computable real function.

Proof:
Follows immediately from:
* Identity Function is Sequentially Computable Real Function
* Identity Function is Computably Uniformly Continuous Real Function
{{qed}}
Category:Computability Theory
fqylmaqzzlnf5gfo39vyysdlhkjki9y
Theorem: Absolute Value of Integer is Primitive Recursive

For every $n \in \N$, let $n$ code the integer $k_n$.
Let $a : \N \to \N$ be defined as:
:$\map a n = \size {k_n}$
Then, $a$ is primitive recursive.

Proof:
Let $a : \N \to \N$ be defined as:
:$\map a n = \map {\operatorname{quot}} {n + 1, 2}$
By:
* Constant Function is Primitive Recursive
* Quotient is Primitive Recursive
* Successor Function is Primitive Recursive
it follows that $a$ is primitive recursive.
By definition of code number for integer, either:
:$n = 2 k_n - 1$, with $k_n > 0$
or:
:$n = - 2 k_n$, with $k_n \le 0$
In the first case, with $k_n > 0$, we have:
:$k_n = \size {k_n}$
Then:
{{begin-eqn}}
{{eqn | l = \map a n
      | r = \map a {2 k_n - 1}
}}
{{eqn | r = \map {\operatorname{quot} } {\paren {2 \size {k_n} - 1} + 1, 2}
}}
{{eqn | r = \map {\operatorname{quot} } {2 \size {k_n}, 2}
}}
{{eqn | r = \size {k_n}
      | c = {{Defof|Quotient (Integer Division)|Quotient}}
}}
{{end-eqn}}
In the second case, with $k_n \le 0$, we have:
:$k_n = - \size {k_n}$
Then:
{{begin-eqn}}
{{eqn | l = \map a n
      | r = \map a {- 2 k_n}
}}
{{eqn | r = \map {\operatorname{quot} } {\paren {- 2 \paren {- \size {k_n} } } + 1, 2}
}}
{{eqn | r = \map {\operatorname{quot} } {2 \size {k_n} + 1, 2}
}}
{{eqn | r = \size {k_n}
      | c = {{Defof|Quotient (Integer Division)|Quotient}}
}}
{{end-eqn}}
{{qed}}
Category:Primitive Recursive Functions
q4jvuwovuotglcvohl5e4rqf0ksuqdr
Theorem: Set of Strictly Positive Integers is Primitive Recursive

Let $P \subseteq \N$ be the set of all $n \in \N$ such that:
:$n$ codes an integer $k$ such that $k > 0$.
Then $P$ is a primitive recursive set.

Proof:
Let $p : \N \to \N$ be defined as:
:$\map p n = \map {\operatorname{rem}} {n, 2}$
By:
* Constant Function is Primitive Recursive
* Remainder is Primitive Recursive
Suppose $n$ codes an integer $k$ such that $k > 0$.
Then:
:$n = 2 k - 1$
Therefore:
{{begin-eqn}}
{{eqn | l = \map p n
      | r = \map {\operatorname{rem} } {2 k - 1, 2}
}}
{{eqn | r = \map {\operatorname{rem} } {2 \paren {k - 1} + 1, 2}
}}
{{eqn | r = 1
      | c = {{Defof|Remainder}}
}}
{{end-eqn}}
Suppose $n$ codes an integer $k$ such that $k \le 0$.
Then:
:$n = - 2 k$
Therefore:
{{begin-eqn}}
{{eqn | l = \map p n
      | r = \map {\operatorname{rem} } {- 2 k, 2}
}}
{{eqn | r = \map {\operatorname{rem} } {2 \paren {- k}, 2}
}}
{{eqn | r = 0
      | c = {{Defof|Remainder}}
}}
{{end-eqn}}
By definition, $p$ is the characteristic function of $P$.
Thus, $P$ is primitive recursive by definition.
{{qed}}
Category:Primitive Recursive Functions
8luydwhh5h7kttonhd2cf3e1timpogw
Theorem: Code Number for Non-Negative Integer is Primitive Recursive

Let $c : \N \to \N$ be defined as:
:$\map c n = m$
where $m$ is the code number for the integer $n : \Z$.
Then $c$ is a primitive recursive function.

Proof:
Let $c : \N \to \N$ be defined as:
:$\map c n = \begin{cases}
\map {\operatorname{pred}} {n + n} & n > 0 \\
0 & n = 0
\end{cases}$
That $c$ is primitive recursive follows from:
* Definition by Cases is Primitive Recursive
* Predecessor Function is Primitive Recursive
* Addition is Primitive Recursive
* Ordering Relations are Primitive Recursive
* Equality Relation is Primitive Recursive
Suppose $n = 0$.
Then:
:$m = -2 n = 0$
But:
:$\map c n = 0 = m$
Suppose $n > 0$.
Then:
:$m = 2 n - 1$
But:
:$\map c n = \map {\operatorname{pred}} {n + n} = 2 n - 1$
as $n + n \ge 1$.
Thus, in all cases:
:$\map c n = m$
{{qed}}
Category:Primitive Recursive Functions
idfgoy49pmczgyhtuvq8ardlsvup6kg
Theorem: Code Number for Non-Positive Integer is Primitive Recursive

Let $c : \N \to \N$ be defined as:
:$\map c n = m$
where $m$ is the code number for the integer $-n : \Z$.
Then $c$ is a primitive recursive function.

Proof:
Let $c : \N \to \N$ be defined as:
:$\map c n = n + n$
which is primitive recursive by:
* Addition is Primitive Recursive
For every $n \in \N$, we have:
:$-n \le 0$
Thus:
:$m = -2 \paren {-n} = 2 n$
Therefore:
:$\map c n = m$
{{qed}}
Category:Primitive Recursive Functions
osaywp6nxnog01v2qyhmzy9ro60wlie
Theorem: Set of Strictly Negative Integers is Primitive Recursive

Let $N \subseteq \N$ be the set of all $n \in \N$ such that:
:$n$ codes an integer $k$ such that $k < 0$.
Then $N$ is a primitive recursive set.

Proof:
By Set of Strictly Positive Integers is Primitive Recursive:
:$P = \set {n \in \N : k > 0}$
is primitive recursive.
By Complement of Primitive Recursive Set:
:$P^c = \set {n \in \N : k \le 0}$
is primitive recursive.
It is clear that:
:$N = P^c \setminus \set {n \in \N : k = 0}$
By Set Difference as Intersection with Relative Complement:
:$N = P^c \cap \relcomp \N {\set {n \in \N : k = 0}}$
By:
* Intersection of Primitive Recursive Sets
* Complement of Primitive Recursive Set
we only need to show that:
:$\set {n \in \N : k = 0}$
is primitive recursive.
As $k = 0 \le 0$:
:$n = - 2 k = 0$
Therefore:
:$\set {n \in \N : k = 0} = \set 0$
which is primitive recursive by:
:Set Containing Only Zero is Primitive Recursive
{{qed}}
Category:Primitive Recursive Functions
kata1afabld68b0rb7b0t8cw1f60kcv
Theorem: Multiplication of Integers is Primitive Recursive

Let $t : \N^2 \to \N$ be defined as:
:$\map t {m, n} = p$
where:
:$m$ is the code number for the integer $k$
:$n$ is the code number for the integer $\ell$
:$p$ is the code number for the integer $k \times \ell$
Then $t$ is a primitive recursive function.

Proof:
We have:
:$\size {k \times \ell} = \size k \times \size \ell$
By:
* Multiplication is Primitive Recursive
* Absolute Value of Integer is Primitive Recursive
we have that:
:$\map a {m, n} = \size {k \times \ell}$
is primitive recursive.
Additionally, we have that:
:$k \times \ell > 0$
{{iff}} either:
:$k > 0 \land \ell > 0$
or:
:$k < 0 \land \ell < 0$
By
* Set of Strictly Positive Integers is Primitive Recursive
* Set of Strictly Negative Integers is Primitive Recursive
* Set Operations on Primitive Recursive Relations
the above statement is a primitive recursive relation.
Let $c^+ : \N \to \N$ be defined as:
:$\map {c^+} n = k_{\mathop + n}$
where $k_{\mathop + n}$ is the code number for the integer $+n : \Z$.
Let $c^- : \N \to \N$ be defined as:
:$\map {c^-} n = k_{\mathop - n}$
where $k_{\mathop - n}$ is the code number for the integer $-n : \Z$.
By
* Code Number for Non-Negative Integer is Primitive Recursive
* Code Number for Non-Positive Integer is Primitive Recursive
both $c^+$ and $c^-$ are primitive recursive.
We now have:
:$\map t {m, n} = \begin{cases}
\map {c^+} {\map a {m, n}} & : \paren {k > 0 \land \ell > 0} \lor \paren {k < 0 \land \ell < 0} \\
\map {c^-} {\map a {m, n}} & : \text{otherwise}
\end{cases}$
which is primitive recursive by:
:Definition by Cases is Primitive Recursive/Corollary
{{qed}}
Category:Primitive Recursive Functions
kkruaqqmjwek9z8fznr05dfje13oz5w
Theorem: Signum Function on Integers is Primitive Recursive

Let $\sgn_\Z : \Z \to \set {-1, 0, 1}$ denote the signum function on the integers.
Let $s : \N \to \N$ be defined as:
:$\map s n = m$
where:
:$n$ codes the integer $k$
:$m$ codes the integer $\map {\sgn_\Z} k$
Then $s$ is a primitive recursive function.

Proof:
Let $s : \N \to \N$ be defined as:
:$\map s n = \begin{cases}
1 & : k > 0 \\
2 & : k < 0 \\
0 & : \text{otherwise}
\end{cases}$
By:
* Set of Strictly Positive Integers is Primitive Recursive
* Set of Strictly Negative Integers is Primitive Recursive
we have that:
:$k > 0 \iff n \in P$
:$k < 0 \iff n \in N$
are primitive recursive relations.
Thus, by:
* Constant Function is Primitive Recursive
* Definition by Cases is Primitive Recursive/Corollary
the function $s$ defined above is primitive recursive.
First, suppose $k > 0$.
Then, we have:
:$\map {\sgn_\Z} k = 1$
As $1 > 0$, by definition, $m$ codes $1$ {{iff}}:
:$m = 2 \paren 1 - 1 = 1$
But $\map s n = 1$ in this case.
Next, suppose $k < 0$.
Then, we have:
:$\map {\sgn_\Z} k = -1$
As $-1 \le 0$, by definition, $m$ codes $-1$ {{iff}}:
:$m = -2 \paren {-1} = 2$
But $\map s n = 2$ in this case.
Lastly, suppose $k = 0$.
Then, we have:
:$\map {\sgn_\Z} k = 0$
As $0 \le 0$, by definition, $m$ codes $0$ {{iff}}:
:$m = -2 \paren 0 = 0$
But $\map s n = 0$ in this case.
In every case, $s$ satisfies the requirements.
{{qed}}
Category:Primitive Recursive Functions
n16g09tsfy5josgdegybhwbnokh7x27
Theorem: Addition of Integers is Primitive Recursive

Let $a : \N^2 \to \N$ be defined as:
:$\map a {m, n} = p$
where:
:$m$ codes an integer $k$
:$n$ codes an integer $\ell$
:$p$ codes the integer $k + \ell$
Then $a$ is a primitive recursive function.

Proof:
{{Proofread}}
Define:
:$<nowiki>\map a {m, n} = \begin{cases}
\map {\sgn_\Z} k \times_\Z \paren {\size k + \size \ell}_\Z & : \map {\sgn_\Z} k = \map {\sgn_\Z} \ell \\
\map {\sgn_\Z} k \times_\Z \paren {\size k {\dot -} \size \ell}_\Z & : \map {\sgn_\Z} k \ne \map {\sgn_\Z} \ell \land \size k \ge \size \ell \\
\map {\sgn_\Z} \ell \times_\Z \paren {\size \ell {\dot -} \size k}_\Z & : \map {\sgn_\Z} k \ne \map {\sgn_\Z} \ell \land \size k < \size \ell
\end{cases}</nowiki>$
where:
:$\times_\Z$ denotes integer multiplication
:$N_\Z$ denotes the code number for $N : \Z$
:$\sgn_\Z$ denotes the signum function on $\Z$
:$\dot -$ denotes partial subtraction
By:
* Ordering Relations are Primitive Recursive
* Equality Relation is Primitive Recursive
* Set Operations on Primitive Recursive Relations
* Signum Function on Integers is Primitive Recursive
* Multiplication of Integers is Primitive Recursive
* Absolute Value of Integer is Primitive Recursive
* Addition is Primitive Recursive
* Cut-Off Subtraction is Primitive Recursive
* Definition by Cases is Primitive Recursive
it follows that $a$ is primitive recursive.
Now, we will show that $a$ satisfies the definition in the theorem statement.
First, suppose:
:$\size k > \size \ell$
Then:
:$\map {\sgn_\Z} {k + \ell} = \map {\sgn_\Z} k$.
If the signs of $k$ and $\ell$ match, then:
:$\size {k + \ell} = \size k + \size \ell$
If they differ, then either:
:$\ell = 0$
or:
$k$ and $\ell$ have opposite signs.
Then:
:$\size {k + \ell} = \size k - \size \ell$ 
in either case.
But since:
:$\size k > \size \ell$
We have:
:$\size k - \size \ell = \size k {\dot -} \size \ell$
In both of those cases, $\map a {m, n}$ matches the value.
It can be seen that, when:
:$\size k < \size \ell$
the above holds with the roles of the two variables swapped.
Now, suppose:
:$\size k = \size \ell$
If:
:$\map {\sgn_\Z} k = \map {\sgn_\Z} \ell$
then:
:$\map {\sgn_\Z} {k + \ell} = \map {\sgn_\Z} k = \map {\sgn_\Z} \ell$
and:
:$\size {k + \ell} = \size k + \size \ell$
If:
:$\map {\sgn_\Z} k \ne \map {\sgn_\Z} \ell$
then either:
:One of the two is zero
or:
:One is positive, and the other is negative
In either of the two cases, we can again use cut-off subtraction to get the correct result.
Since, in every case, the defined $a : \N^2 \to \N$ satisfies the definition, the result follows.
{{qed}}
Category:Integer Addition
Category:Primitive Recursive Functions
dudp8gac4ct6ksfvw7w8iwpb997d5ni
Theorem: Negation of Integer is Primitive Recursive

Let $f^- : \N \to \N$ be defined as:
:$\map {f^-} {x_\Z} = \paren {-x}_\Z$
where:
:$k_\Z$ denotes the code number for the integer $k$
Then $f^-$ is a primitive recursive function.

Proof:
Define $f^-$ as:
$\quad\map {f^-} {x_\Z} = \begin{cases}
\map {c^-} {\size x} & : x > 0 \\
\map {c^+} {\size x} & : \text{otherwise}
\end{cases}$
where:
:$\map {c^-} x = \paren {-x}_\Z$
:$\map {c^+} x = x_\Z$
The function is primitive recursive by:
* Definition by Cases is Primitive Recursive/Corollary
* Set of Strictly Positive Integers is Primitive Recursive
* Code Number for Non-Negative Integer is Primitive Recursive
* Code Number for Non-Positive Integer is Primitive Recursive
For $x > 0$, we have:
:$x = \size x$
Thus:
:$\map {f^-} x = \paren {-x}_\Z$
by definition of $c^-$, as required.
For $x = 0$, we have:
:$x = 0 = -\size x$
Thus:
:$\map {f^-} 0 = 0_\Z = \paren {-0}_\Z$
by definition of $c^+$, as required.
For $x < 0$, we have:
:$x = -\size x$
Thus:
:$\map {f^-} x = x_\Z = \paren {-\paren {-x}}_\Z$
by definition of $c^+$, as required.
{{qed}}
Category:Primitive Recursive Functions
g9bd60r9kxdwfv3fmczpxahvvcumlcx
Theorem: Entropy of Measure-Preserving Transformation with respect to Finite Sub-Sigma Algebra is Well-Defined

Let $\struct {X, \BB, \mu}$ be a probability space.
Let $T: X \to X$ be a $\mu$-preserving transformation.
Let $\AA \subseteq \BB$ be a finite sub-$\sigma$-algebra.
Then the entropy of $T$ with respect to $\AA$:
:$\ds \map h {T, \AA} := \lim_{n \mathop \to \infty} \frac 1 n \map H {\bigvee_{k \mathop = 0}^{n - 1} T^{-k} \AA}$
is well-defined.

Proof:
Let:
:$\ds a_n := \map H {\bigvee_{k \mathop = 0}^{n - 1} T^{-k} \AA}$
We need to show that the limit:
:$\ds \lim_{n \mathop \to \infty} \frac {a_n} n$
exists.
In view of Fekete's Subadditive Lemma, it suffices to show the subadditivity of $\sequence {a_n}$.
To this end, let $m, n \ge 1$.
Then:
{{begin-eqn}}
{{eqn | l = a_{m + n}
      | r = \map H {\bigvee_{k \mathop = 0}^{m - 1} T^{-k} \AA \vee \bigvee_{k \mathop = m}^{m + n - 1} T^{-k} \AA  }
}}
{{eqn | o = \le
      | r = \map H {\bigvee_{k \mathop = 0}^{m - 1} T^{-k} \AA} + \map H {\bigvee_{k \mathop = m}^{m + n - 1} T^{-k} \AA  }
      | c = {{Corollary|Conditional Entropy of Join as Sum|5}}
}}
{{eqn | r = \map H {\bigvee_{k \mathop = 0}^{m - 1} T^{-k} \AA} + \map H {T^{-m} \sqbrk {\bigvee_{k \mathop = 0}^{n - 1} T^{-k} \AA } }
}}
{{eqn | r = \map H {\bigvee_{k \mathop = 0}^{m - 1} T^{-k} \AA} + \map H {\bigvee_{k \mathop = 0}^{n - 1} T^{-k} \AA  }
      | c = {{Corollary|Measure-Preserving Transformation Preserves Conditional Entropy}}
}}
{{eqn | r = a_m + a_n
}}
{{end-eqn}}
{{qed}}
Category:Definitions/Ergodic Theory
mkaj8olaurfotibvcork17vpiqhjjuz