Email Gateway (Nov 09 2021 at 11:50): Email Gateway (Nov 09 2021 at 11:50):From: Lawrence Paulson <lp15@cam.ac.uk>
Today we have an unusual contribution from Jacques Fleuriot:
Real Exponents as the Limits of Sequences of Rational Exponents
"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."
It is online at https://www.isa-afp.org/entries/Real_Power.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC