### 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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Real_Power

- RatPower
- RealPower
- Log

## Cite

×

Real_Power-AFP

    @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   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Real_Power.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Nov 9, 2021 : Isabelle2021