
Real
Exponents
as
the
Limits
of
Sequences
of
Rational
Exponents
Title: 
Real Exponents as the Limits of Sequences of Rational Exponents 
Author:

Jacques D. Fleuriot

Submission date: 
20211108 
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. 
BibTeX: 
@article{Real_PowerAFP,
author = {Jacques D. Fleuriot},
title = {Real Exponents as the Limits of Sequences of Rational Exponents},
journal = {Archive of Formal Proofs},
month = nov,
year = 2021,
note = {\url{https://isaafp.org/entries/Real_Power.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
