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: 2021-11-08
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_Power-AFP,
  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://isa-afp.org/entries/Real_Power.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License