[isabelle] New in the AFP: Real Exponents as Limits of Rationals

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.