nyuuzyou/wikis huggingface dataset:
Positive Linear Functional on C*-Algebra induces Semi-Inner Product

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $f : A \to \C$ be a positive linear functional. 
Define $\innerprod \cdot \cdot : A^2 \to A$ by:
:$\innerprod x y = \map f {y^\ast x}$
for each $x, y \in A$. 
Then $\innerprod \cdot \cdot$ is a semi-inner product on $A$. 
=== Corollary ===
== Proof ==
=== Proof of Conjugate Symmetry ===
Let $x, y \in A$ we have:
=== Proof of linearity ===
Let $x, y, z \in A$ and $\alpha \in \C$.
Then we have:
=== Proof of non-negative definiteness ===
Let $x \in A$.
Then we have:
:$\innerprod x x = \map f {x^\ast x}$
From Product of Element of C*-Algebra with its Star is Positive, $x^\ast x$ is positive.
So $\map f {x^\ast x} \in \R_{\ge 0}$.
Hence $\innerprod x x \in \R_{\ge 0}$. 
== Sources ==
* $\text {VIII}.5.11$
Category:Semi-Inner Product Spaces
Category:C*-Algebras
Category:Positive Linear Functionals
Category:Positive Linear Functional on C*-Algebra induces Semi-Inner Product
Positive Linear Functional on C*-Algebra induces Semi-Inner Product/Corollary

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $f : A \to \C$ be a positive linear functional. 
Let $x, y \in A$.
Then:
:$\cmod {\map f {y^\ast x} }^2 \le \map f {y^\ast y} \map f {x^\ast x}$
== Proof ==
Define $\innerprod \cdot \cdot : A^2 \to A$ by:
:$\innerprod x y = \map f {y^\ast x}$
for each $x, y \in A$. 
By Positive Linear Functional on C*-Algebra induces Semi-Inner Product, $\innerprod \cdot \cdot$ is a semi-inner product.
Hence from Cauchy-Bunyakovsky-Schwarz Inequality: Inner Product Spaces, we have:
:$\cmod {\innerprod x y}^2 \le \innerprod x x \innerprod y y$
so that:
:$\cmod {\map f {y^\ast x} }^2 \le \map f {y^\ast y} \map f {x^\ast x}$
== Sources ==
* $\text {VIII}.5.11$
Category:Positive Linear Functional on C*-Algebra induces Semi-Inner Product
Positive Linear Functional on C*-Algebra is Bounded

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,}_A}$ be a $\text C^\ast$-algebra.
Let $f : A \to \C$ be a positive linear functional.
Then $f$ is bounded.
== Proof ==
From Linear Transformation from C*-Algebra is Bounded if Bounded on Positive Elements, it is enough to show that:
:there exists $c > 0$ such that for all positive $x \in A$ we have $\cmod {\map f x} \le c \norm x$.
 suppose that:
:there does not exist $c > 0$ such that for all positive $x \in A$ we have $\cmod {\map f x} \le c \norm x$.
Then for each $n \in \N$ there exists $y_n \in A$ positive such that:
:$\cmod {\map f {y_n} } > 2^n \norm {y_n}$ 
Since $y_n \ne {\mathbf 0}_A$, setting:
:$\ds x_n = \frac {y_n} {\norm {y_n} }$
we have:
:$\ds \cmod {\map f {x_n} } > 2^n$
with $\norm {x_n} = 1$.
Further, $x_n$ is positive for each $n \in \N$ by Non-Negative Multiple of Positive Element of C*-Algebra is Positive.
Hence $\map f {x_n} \ge 0$ for each $n \in \N$, and we have:
:$\map f {x_n} > 2^n$
Hence we have, for each $n \in \N$:
:$\ds \map f {\frac {x_n} {2^n} } > 1$
and hence:
:$\ds \map f {\sum_{k \mathop = 1}^n \frac {x_k} {2^k} } > n$
by linearity.
We have:
:$\ds \sum_{k \mathop = 1}^\infty \norm {\frac {x_k} {2^k} } = \sum_{k \mathop = 1}^\infty \frac 1 {2^k} < \infty$
from Sum of Infinite Geometric Sequence.
Hence from Absolutely Convergent Series in Normed Vector Space is Convergent iff Space is Banach, we have that:
:$\ds \sum_{k \mathop = 1}^n \frac {x_k} {2^k} \to x$ as $n \to \infty$
for some $x \in A$.
From Convergent Series of Positive Elements of C*-Algebra is Positive, we have:
:$\ds x - \sum_{k \mathop = 1}^n \frac {x_k} {2^k} = \sum_{k \mathop = n + 1}^\infty \frac {x_n} {2^n}$ is positive. 
Since $f$ is a positive linear functional, we have:
:$\ds \map f {x - \sum_{k \mathop = 1}^n \frac {x_k} {2^k} } \ge 0$
Since $x$ and $\ds \sum_{k \mathop = 1}^n \frac {x_k} {2^k}$ are both positive, we have:
:$\map f x \in \R_{\ge 0}$
and:
:$\map f {\sum_{k \mathop = 1}^n \frac {x_k} {2^k} } \in \R_{\ge 0}$
since $f$ is positive.
Hence by linearity:
:$\ds \map f x \ge \map f {\sum_{k \mathop = 1}^n \frac {x_k} {2^k} } > n$
Since $\map f x < \infty$, by taking $n > \map f x$ we obtain a contradiction.
Hence:
:there exists $c > 0$ such that for all positive $x \in A$ we have $\cmod {\map f x} \le c \norm x$.
Hence $f$ is bounded by Linear Transformation from C*-Algebra is Bounded if Bounded on Positive Elements.
== Sources ==
* : $3.3$: Positive Linear Functionals 
Category:Positive Linear Functionals
Category:C*-Algebras
Positive Linear Functional on C*-Algebra is Increasing on Hermitian Elements

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra with identity element ${\mathbf 1}_A$. 
Let $f : A \to \C$ be a positive linear functional.
Let $\le_A$ be the canonical preordering of $A$. 
Let $x, y \in A$ be Hermitian such that $x \le_A y$.
Then $\map f x \le \map f y$.
== Proof ==
From the definition of the canonical preordering, we have:
:$y - x$ is positive.
From the definition of a positive linear functional we have:
:$\map f {y - x} \ge 0$
Since $f$ is linear, we have:
:$\map f y - \map f x \ge 0$ 
From Positive Linear Functional on C*-Algebra is Real on Hermitian Elements, we have $\map f x \in \R$ and $\map f y \in \R$.
Hence:
:$\map f x \le \map f y$
Category:Positive Linear Functionals
Category:C*-Algebras
Positive Linear Functional on C*-Algebra is Real on Hermitian Elements

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\phi : A \to \C$ be a positive linear functional.
Let $x \in A$ be Hermitian.
Then $\map \phi x \in \R$. 
== Proof ==
From Hermitian Element of C*-Algebra Decomposes into Positive Elements, there exists positive elements $x^+, x^- \in A$ such that:
:$x = x^+ - x^-$
Since $f$ is positive, we have $\map \phi {x^+} \ge 0$ and $\map \phi {x^-} \ge 0$. 
Hence from linearity:
:$\map \phi x = \map \phi {x^+} - \map \phi {x^-} \in \R$ 
Category:Positive Linear Functionals
Category:C*-Algebras
Positive Linear Functional on C*-Algebra preserves Star

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\phi : A \to \C$ be a positive linear functional.
Then:
:$\overline {\map \phi x} = \map \phi {x^\ast}$
== Proof ==
From Linear Functional on *-Algebra Real-Valued at Hermitian Elements preserves Star, it is enough to show that:
:$\map \phi x \in \R$ whenever $x \in A$ is Hermitian.
This is precisely Positive Linear Functional on C*-Algebra is Real on Hermitian Elements.
Category:Positive Linear Functionals
Category:C*-Algebras
Positive Multiple of Metric is Metric

== Theorem ==
Let $M = \struct {A, d}$ be a metric space.
Let $k \in \R_{>0}$ be a (strictly) positive real number.
Let $d_k: A \times A \to \R$ be the function defined as:
:$\forall \tuple {x, y} \in A: \map {d_k} {x, y} = k \cdot \map d {x, y}$
Then $M_k = \struct {A, d_k}$ is a metric space.
== Proof ==
=== ===
So holds for $d_k$.
=== ===
So holds for $d_k$.
=== ===
So holds for $d_k$.
=== ===
So holds for $d_k$.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 2$: Metric Spaces: Exercise $1$
Category:Metric Spaces
Positive Part of Composition of Functions

== Theorem ==
Let $\struct {X, \Sigma}$ and $\struct {X', \Sigma'}$ be measurable spaces.
Let $T : X \to X'$ be a $\Sigma/\Sigma'$-measurable mapping.
Let $f : X' \to \overline \R$ be a function.
Then: 
:$\paren {f \circ T}^+ = f^+ \circ T$
where $\paren {f \circ T}^+$ denotes the positive part of $f \circ T$.
== Proof ==
Let $x \in X$ be such that $\map {\paren {f \circ T} } x = \map f {\map T x} \ge 0$.
Then $\map f {\map T x} = \map {f^+} {\map T x}$ by the definition of the positive part. 
So:
Now let $x \in X$ be such that $\map {\paren {f \circ T} } x = \map f {\map T x} < 0$.
Then $\map {f^+} {\map T x} = 0$ and $\map {\paren {f \circ T}^+} x = 0$ by the definition of the positive part.
So: 
:$\map {\paren {f \circ T}^+} x = \map {\paren {f^+ \circ T} } x$
for all $x \in X$.
Category:Positive Parts
Positive Part of Continuous Function is Continuous

== Theorem ==
Let $X$ be a topological space.
Let $f : X \to \R$ be continuous.
Let $f^+$ be the positive part of $f$. 
Then $f^+$ is continuous.
== Proof ==
From Constant Function is Continuous, we have that $\mathbf 0 : X \to \R$ defined by $\map {\mathbf 0} x = 0$ for each $x \in X$ is continuous.
From Maximum Rule for Continuous Real-Valued Functions, we have that the function $f \vee \mathbf 0 : X \to \R$ defined by:
:$\map {\paren {f \vee \mathbf 0} } x = \max \set {0, \map f x}$ for each $x \in X$
is continuous.
By the definition of the positive part, we have:
:$f^+ = f \vee \mathbf 0$
Hence the result.
== Also see ==
* Negative Part of Continuous Function is Continuous‎
Category:Positive Parts
Category:Continuous Real Functions
Positive Part of Darboux Integrable Function is Integrable

== Theorem ==
Let $f$ be a real function that is Darboux integrable over $\closedint a b$.
Let $f^+$ be the positive part of $f$.
Then $f^+$ is Darboux integrable over $\closedint a b$.
=== Corollary ===
== Proof ==
Let $\epsilon > 0$ be a strictly positive real number.
By Condition for Darboux Integrability, there is a finite subdivision $P = \sequence {x_i}_{0 \mathop \le i \mathop \le n}$ such that:
:$\map {U_f} P - \map {L_f} P < \epsilon$
where $\map {U_f} P$ and $\map {L_f} P$ are the upper Darboux sum and lower Darboux sum, respectively.
Consider the terms of $\map {U_f} P$ and $\map {L_f} P$ for an arbitrary index $i$.
By Supremum does not Precede Infimum:
:$m_i^{\paren f} \le M_i^{\paren f}$
where $m_i^{\paren f}$ and $M_i^{\paren f}$ are respectively the infimum and supremum of $f$ on $\closedint {x_{i - 1} } {x_i}$.
Therefore, there are three cases to consider:
If $0 \le m_i^{\paren f} \le M_i^{\paren f}$:
:In this case, it follows from the definition of infimum that:
::$\forall x \in \closedint {x_{i - 1} } {x_i}: \map f x \ge 0$
:Therefore, on that interval, $\map {f^+} x = \map f x$.
:So:
::$M_i^{\paren {f^+} } - m_i^{\paren f} = M_i^{\paren f} - m_i^{\paren f}$
If $m_i^{\paren f} < 0 \le M_i^{\paren f}$:
:Because $\map {f^+} x \ge 0$, it follows that $m_i^{\paren {f^+} } \ge 0 > m_i^{\paren f}$.
:As $0 \le M_i^{\paren f}$, it follows that $\sup \paren {f \closedint a b \cup \set 0} = M_i^{\paren f}$.
:But $f^+ \closedint {x_{i - 1} } {x_i} \subseteq f \closedint {x_{i - 1} } {x_i} \cup \set 0$, so by Supremum of Subset:
::$M_i^{\paren {f^+} } \leq M_i^{\paren f}$
:Therefore:
::$M_i^{\paren {f^+} } - m_i^{\paren {f^+} } < M_i^{\paren f} - m_i^{\paren f}$
If $m_i^{\paren f} \le M_i^{\paren f} < 0$:
:Because $M_i^{\paren f} < 0$, it follows that $f$ is strictly negative on $\closedint {x_{i - 1} } {x_i}$.
:Thus, $\forall x \in \closedint {x_{i - 1} } {x_i}: \map {f^+} x = 0$.
:Therefore:
::$m_i^{\paren {f^+} } = M_i^{\paren {f^+} } = 0$.
:And it follows that:
::$M_i^{\paren {f^+} } - m_i^{\paren {f^+} } = 0 \le M_i^{\paren f} - m_i^{\paren f}$
Then, in every case:
:$M_i^{\paren {f^+} } - m_i^{\paren {f^+} } \le M_i^{\paren f} - m_i^{\paren f}$
But:
Because $\epsilon$ was arbitrary, it follows from Condition for Darboux Integrability that $f^+$ is integrable on $\closedint a b$
Category:Definite Integrals
Positive Part of Darboux Integrable Function is Integrable/Negative Part

== Theorem ==
Let $f$ be a real function that is Darboux integrable over $\closedint a b$.
Let $f^-$ be the negative part of $f$.
Then $f^-$ is Darboux integrable over $\closedint a b$.
== Proof ==
$f^-$ is the positive part of $\map g x = -\map f x$.
From Linear Combination of Definite Integrals, it follows that:
:$\ds \int_a^b \map g x \rd x = -\int_a^b \map f x \rd x$
Therefore, by Positive Part of Darboux Integrable Function is Integrable, $f^-$ is Darboux integrable over $\closedint a b$.
Category:Definite Integrals
Positive Part of Function Bounded above by Absolute Value

== Theorem ==
Let $X$ be a set.
Let $f : X \to \C$ be a function.
Let $f^+$ be the positive part of $f$.
Then $f^+ \le \cmod f$.
== Proof ==
By definition, we have $f^+ \ge 0$. 
Let $f^-$ be the negative part of $f$. 
By definition, we also have $f^- \ge 0$.
Hence $f^+ \le f^+ + f^-$.
By Sum of Positive and Negative Parts, we have $f^+ + f^- = \cmod f$. 
Hence $0 \le f^+ \le \cmod f$.
Category:Positive Parts
Positive Part of Horizontal Section of Function is Horizontal Section of Positive Part

== Theorem ==
Let $X$ and $Y$ be sets. 
Let $f : X \times Y \to \overline \R$ be a function.
Let $y \in Y$. 
Then: 
:$\paren {f^y}^+ = \paren {f^+}^y$
where:
:$f^y$ denotes the $y$-horizontal function of $f$
:$f^+$ denotes the positive part of $f$.
== Proof ==
Fix $y \in Y$.
Then, we have, for each $x \in X$:
Category:Horizontal Section of Functions
Category:Positive Parts
Positive Part of Multiple of Function

== Theorem ==
Let $X$ be a set.
Let $f : X \to \overline \R$ be an extended real-valued function.
Let $\alpha$ be a real number. 
Then:
:$\ds \paren {\alpha f}^+ = \begin{cases}\alpha f^+ & \alpha \ge 0 \\ -\alpha f^- & \alpha < 0\end{cases}$
where:
:$\paren {\alpha f}^+$ and $f^+$ are the positive parts of $\alpha f$ and $f$ respectively
:$f^-$ is the negative part of $f$.
== Proof ==
Let $x \in X$. 
First take $\alpha \ge 0$.
Suppose that $\map f x \ge 0$.
Then $\alpha \map f x \ge 0$.
So:
:$\max \set {\alpha \map f x, 0} = \alpha \map f x$
and:
:$\max \set {\map f x, 0} = \map f x$
So by the definition of the positive part and negative part, we have:
:$\map {\paren {\alpha f}^+} x = \alpha \map f x$
and: 
:$\map {f^+} x = \map f x$
So:
:$\map {\paren {\alpha f}^+} x = \alpha \map {f^+} x$
if $\map f x \ge 0$. 
Now suppose that $\map f x < 0$.
Then $\alpha \map f x < 0$.
So:
:$\max \set {\map f x, 0} = 0$
and:
:$\max \set {\alpha \map f x, 0} = 0$
So by the definition of the positive part and negative part, we have:
:$\map {\paren {\alpha f}^+} x = 0$
and:
:$\map {f^+} x = 0$
So:
:$\map {\paren {\alpha f}^+} x = \alpha \map {f^+} x$
if $\map f x < 0$.
So:
:$\paren {\alpha f}^+ = \alpha f^+$
if $\alpha \ge 0$. 
Now take $\alpha < 0$.
Suppose that $\map f x \ge 0$. 
Then $\alpha \map f x \le 0$. 
So:
:$\max \set {\alpha \map f x, 0} = 0$
and:
:$-\min \set {\map f x, 0} = 0$
So by the definition of the positive part and negative part, we have: 
:$\map {\paren {\alpha f}^+} x = 0$
and:
:$\map {f^-} x = 0$
So:
:$\map {\paren {\alpha f}^+} x = -\alpha \map {f^-} x$
if $\map f x \ge 0$. 
Now suppose that $\map f x < 0$.
Then $\alpha \map f x > 0$.
So:
:$\max \set {\alpha \map f x, 0} = \alpha \map f x$
and:
:$-\min \set {\map f x, 0} = -\map f x$
So:
:$\map {\paren {\alpha f}^+} x = \alpha \map f x$
and:
:$\map {f^-} x = -\map f x$
So:
:$\map {\paren {\alpha f}^+} x = -\alpha \map {f^-} x$ 
if $\map f x < 0$. 
So:
:$\paren {\alpha f}^+ = -\alpha f^-$
if $\alpha < 0$. 
Category:Positive Parts
Positive Part of Pointwise Product of Functions

== Theorem ==
Let $X$ be a set. 
Let $f, g : X \to \overline \R$ be extended real-valued functions.
Then: 
:$\map {\paren {f \cdot g}^+} x = \begin{cases}\map {f^+} x \map {g^+} x & \map f x \ge 0 \text { and } \map g x \ge 0 \\ \map {f^-} x \map {g^-} x & \map f x \le 0 \text { and } \map g x \le 0 \\ 0 & \text {otherwise}\end{cases}$
for each $x \in X$, where: 
:$f \cdot g$ is the pointwise product of $f$ and $g$
:$\paren {f \cdot g}^+$ denotes the positive part
== Proof ==
Let $x \in X$ be such that $\map f x \ge 0$ and $\map g x \ge 0$. 
Then:
:$\map {\paren {f \cdot g} } x = \map f x \map g x \ge 0$
From the definition of the positive part, we then have: 
:$\map {\paren {f \cdot g}^+} x = \map f x \map g x$
Now let $x \in X$ be such that $\map f x \le 0$ and $\map g x \le 0$.
Then, we have: 
:$\map {f^-} x = -\map f x$
and:
:$\map {g^-} x = -\map g x$
from the definition of the negative part. 
Then, we have: 
:$\map f x \map g x \ge 0$
So again:
Now suppose that $x \in X$ is such that neither of: 
:$\map f x \ge 0$ and $\map g x \ge 0$ 
or:
:$\map f x \le 0$ and $\map g x \le 0$
are true. 
Then, we have either $\map f x > 0$ and $\map g x < 0$, or $\map f x < 0$ and $\map g x > 0$.
In either case: 
:$\map f x \map g x < 0$
So, from the definition of the positive part, we have: 
:$\map {\paren {f \cdot g}^+} x = 0$ 
Category:Positive Parts
Positive Part of Real-Valued Function Vanishing at Infinity Vanishes at Infinity

== Theorem ==
Let $X$ be a topological space. 
Let $f : X \to \R$ be a real-valued function vanishing at infinity.
Let $f^+$ be the positive part of $f$. 
Then $f^+$ vanishes at infinity.
== Proof ==
From Positive Part of Function Bounded above by Absolute Value, we have:
:$0 \le f^+ \le \cmod f$
From Complex-Valued Function Dominated by Function Vanishing at Infinity also Vanishes at Infinity:
:$f^+$ vanishes at infinity.
Category:Positive Parts
Category:Complex-Valued Functions Vanishing at Infinity
Positive Part of Real-Valued Random Variable is Real-Valued Random Variable

== Theorem ==
Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space. 
Let $X$ be a real-valued random variable. 
Then the positive part $X^+$ of $X$ is a real-valued random variable.
== Proof ==
Since $X$ is a real-valued random variable, $X$ is $\Sigma$-measurable.
From Function Measurable iff Positive and Negative Parts Measurable, $X^+$ is $\Sigma$-measurable.
So $X^+$ is a real-valued random variable.
Category:Random Variables
Category:Positive Parts
Positive Part of Simple Function is Simple Function

== Theorem ==
Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \R$ be a simple function.
Then $f^+: X \to \R$, the positive part of $f$, is also a simple function.
== Proof ==
Let $f$ have the following standard representation:
:$f = \ds \sum_{i \mathop = 0}^n a_i \chi_{E_i}$
Then we see that $f^+$ must satisfy:
:$f^+ = \ds \sum_{i \mathop = 0}^n \max \set {a_i, 0} \chi_{E_i}$
as the $E_i$ are disjoint, and $\chi_{E_i} \ge 0$ pointwise.
Since all of the $E_i$ are measurable, it follows that $f^+$ is a simple function.
== Also see ==
* Negative Part of Simple Function is Simple Function, a natural counterpart
== Sources ==
* : $8.7 \ \text{(v)}$
Category:Simple Functions
Category:Positive Parts
Positive Part of Vertical Section of Function is Vertical Section of Positive Part

== Theorem ==
Let $X$ and $Y$ be sets. 
Let $f : X \times Y \to \overline \R$ be a function.
Let $x \in X$. 
Then: 
:$\paren {f_x}^+ = \paren {f^+}_x$
where:
:$f_x$ denotes the $x$-vertical function of $f$
:$f^+$ denotes the positive part of $f$.
== Proof ==
Fix $x \in X$.
Then, we have, for each $y \in Y$:
Category:Vertical Section of Functions
Category:Positive Parts
Positive Power Function on Non-negative Reals is Strictly Increasing

== Theorem ==
Let $a \in \Q_{> 0}$ be a strictly positive rational number.
Let $f_a: \R_{\ge 0} \to \R$ be the real function defined as:
:$\map {f_a} x = x^a$
Then $f_a$ is strictly increasing.
=== Real Index ===
If $a \in \R_{>0}$ is a strictly positive real number, then the same result applies. Just use the real index variations of the theorems used to prove this one.
However, this result is specifically stated for a rational index, as this page is used to prove something else.
== Proof ==
By the power rule for derivatives:
:$\map {D_x} {x^a} = a x^{a - 1}$
By power of positive real number is positive, it is seen that:
:$x > 0 \implies x^{a - 1} > 0$
By Strictly Positive Real Numbers are Closed under Multiplication, it follows that $\map {D_x} {x^a} > 0$ for all $x \in \openint 0 {+\infty}$.
Hence by Derivative of Monotone Function, $f_a$ is strictly increasing
Category:Examples of Strictly Increasing Real Functions
Category:Powers
Positive Rational Number as Power of Number with Power of Itself

== Theorem ==
Every positive rational number can be written either as:
: $a^{a^a}$ for some irrational number $a$
or as:
: $n^{n^n}$ for some natural number $n$.
== Proof ==
For $\ln x \le 0$ and $\ln x \ge -1$, the above is positive.
For $-1 < \ln x < 0$, we have $e^{-1} < x < 1$.
so we have $\dfrac \d {\d x} x^{x^x} > 0$ for every $x > 0$.
We also have:
:$\ds \lim_{x \mathop \to 0^+} x^{x^x} = \lim_{x \mathop \to 0^+} x^{\lim_{x \mathop \to 0^+} x^x} = 0^1 = 0$
Thus $x^{x^x}: \R_{>0} \to \R_{>0}$ is bijective.
For each $y > 0$, we can find some $x > 0$ such that $y = x^{x^x}$.
The result above is therefore equivalent to:
:$a^{a^a}$ is irrational if $a$ is rational and not a natural number.
By Rational Number as Power of Number with Itself, as long as $a$ is not a natural number, $a^a$ is irrational.
Therefore if $a$ is not a natural number, by Gelfond-Schneider Theorem, $a^{a^a}$ is transcendental, so it is also irrational.
This proves the result.
== Also see ==
* Rational Number as Power of Number with Itself
== Sources ==
* 
Category:Number Theory
Positive Rational Numbers are Closed under Addition

== Theorem ==
Let $\Q_{\ge 0}$ denote the set of positive rational numbers:
:$\Q_{\ge 0} := \set {x \in \Q: x \ge 0}$
where $\Q$ denotes the set of rational numbers.
Then the algebraic structure $\struct {\Q_{\ge 0}, +}$ is closed in the sense that:
:$\forall a, b \in \Q_{\ge 0}: a + b \in \Q_{\ge 0}$
where $+$ denotes rational addition.
== Proof ==
Let $a$ and $b$ be expressed in canonical form:
:$a = \dfrac {p_1} {q_1}, b = \dfrac {p_2} {q_2}$
where $p_1, p_2 \in \Z$ and $q_1, q_2 \in \Z_{>0}$.
As $\forall a, b \in \Q_{\ge 0}$ it follows that:
:$p_1, p_2 \in \Z_{\ge 0}$
By definition of rational addition:
:$\dfrac {p_1} {q_1} + \dfrac {p_2} {q_2} = \dfrac {p_1 q_2 + p_2 q_1} {q_1 q_2}$
From Integers form Ordered Integral Domain, it follows that:
Category:Rational Addition
Category:Rational Numbers
Positive Rational Numbers under Addition form Commutative Monoid

== Theorem ==
Let $\Q_{\ge 0}$ denote the set of positive rational numbers.
The algebraic structure:
:$\struct {\Q_{\ge 0}, +}$
forms a commutative monoid.
== Proof ==
From Rational Numbers form Field, $\struct {\Q, +, \times}$ is a field.
Hence $\struct {\Q, +}$ is an abelian group.
From Positive Rational Numbers are Closed under Addition we have that $\struct {\Q_{\ge 0}, +}$ is closed.
Hence from Subsemigroup Closure Test, $\struct {\Q_{\ge 0}, +}$ is a subsemigroup of $\struct {\Q, +}$.
From Restriction of Commutative Operation is Commutative, $\struct {\Q_{\ge 0}, +}$ is a commutative semigroup.
We have that $0$ is the identity element of $\struct {\Q, +}$.
Hence from Identity of Subsemigroup of Group, $0$ is also the identity element of $\struct {\Q_{\ge 0}, +}$.
So $\struct {\Q_{\ge 0}, +}$ is a commutative monoid.
Category:Examples of Commutative Monoids
Category:Rational Numbers
Positive Rational Numbers under Addition form Ordered Semigroup

== Theorem ==
Let $\Q_{\ge 0}$ denote the set of positive rational numbers.
The algebraic structure:
:$\struct {\Q_{\ge 0}, +, \le}$
forms an ordered semigroup.
== Proof 1 ==
== Proof 2 ==
Category:Examples of Ordered Semigroups
Category:Rational Numbers
Category:Positive Rational Numbers under Addition form Ordered Semigroup
Positive Rational Numbers under Addition form Ordered Semigroup/Proof 1

== Theorem ==
== Proof ==
It is necessary to ascertain that $\struct {\Q_{\ge 0}, +, \le}$ fulfils the ordered semigroup axioms:
From Rational Numbers form Totally Ordered Field, $\struct {\Q, +, \times, \le}$ is a totally ordered field.
Hence $\struct {\Q, +, \le}$ is an ordered group, and so an ordered semigroup.
From Positive Rational Numbers are Closed under Addition we have that $\text {OS} 0$ holds.
From Restriction of Associative Operation is Associative we have that $\text {OS} 1$ holds.
From Restriction of Ordering is Ordering we have that $\text {OS} 2$ holds.
The result follows.
Category:Positive Rational Numbers under Addition form Ordered Semigroup
Positive Rational Numbers under Addition form Ordered Semigroup/Proof 2

== Theorem ==
== Proof ==
From Rational Numbers form Totally Ordered Field, $\struct {\Q, +, \times, \le}$ is a totally ordered field.
Hence $\struct {\Q, +, \le}$ is an ordered group, and so an ordered semigroup.
From Positive Rational Numbers are Closed under Addition we have that $\struct {\Q_{\ge 0}, +}$ is closed.
Hence from Subsemigroup Closure Test, $\struct {\Q_{\ge 0}, +}$ is a subsemigroup of $\struct {\Q, +}$.
From Subsemigroup of Ordered Semigroup is Ordered, $\struct {\Q_{\ge 0}, +, \le}$ is an ordered semigroup.
Category:Positive Rational Numbers under Addition form Ordered Semigroup