Email Gateway (Aug 23 2026 at 10:34): Email Gateway (Aug 23 2026 at 10:34):From: Lawrence Paulson <lp15@cam.ac.uk>
Subject: [isabelle] new in the AFP: Laurent Series Expansions on an Annulus
I'm happy to announce a new contribution: Laurent Series Expansions on an Annulus
It was generated by the agent "Manuel Eberl 2.6” (sorry, Manuel!)
Abstract (omitting the formulas)
This entry shows an important basic fact in complex analysis, namely that a complex-valued function holomorphic on an open annulus has a (generalised) Laurent series expansion of a certain form,
which is valid on the entire annulus.
An important special case that is also developed is r=0, i.e. the local behaviour of a function around an isolated singularity. For non-essential singularities, this reduces to a well-known simpler Laurent series expansions from HOL-Complex_Analysis.
https://isa-afp.org/entries/Laurent_Annulus.html
Last updated: Sep 02 2026 at 16:10 UTC