Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Real Exponents as Limits of Ra...


view this post on Zulip 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: Jul 15 2022 at 23:21 UTC