### Abstract

In this formalisation, we construct real exponents as the limits of
sequences of rational exponents. In particular, if $a \ge 1$ and $x
\in \mathbb{R}$, we choose an increasing rational sequence $r_n$ such
that $\lim_{n\to\infty} {r_n} = x$. Then the sequence $a^{r_n}$ is
increasing and if $r$ is any rational number such that $r > x$,
$a^{r_n}$ is bounded above by $a^r$. By the convergence criterion for
monotone sequences, $a^{r_n}$ converges. We define $a^ x =
\lim_{n\to\infty} a^{r_n}$ and show that it has the expected
properties (for $a \ge 0$). This particular construction of real
exponents is needed instead of the usual one using the natural
logarithm and exponential functions (which already exists in Isabelle)
to support our mechanical derivation of Euler's exponential
series as an ``infinite polynomial". Aside from helping us avoid
circular reasoning, this is, as far as we are aware, the first time
real exponents are mechanised in this way within a proof assistant.

BSD License