[isabelle-dev] Reorganising Analysis
eberlm at in.tum.de
Mon Nov 4 13:48:21 CET 2019
Absolutely. The Residue theorem is the bare minimum of what I would
expect to be included in a development of complex analysis, and that
requires winding numbers.
I don't really have an idea of what material you really need for winding
numbers. I recall that Wenda had some problems with them (about what
happens when there's a pole on the path) – perhaps it would make sense
to give that theory an overhaul altogether? Perhaps he can chime in on
this; he probably knows much more about this than I do.
On 04/11/2019 13:44, Lawrence Paulson wrote:
> Then the obvious stopping point is one line above: Derivative.
> The problem at the moment with basing a development around the Cauchy integral theorem is that you might also want to include Winding_Numbers, but that theory inherits almost the whole of Analysis: even the Jordan curve theorem.
>> On 4 Nov 2019, at 12:19, Manuel Eberl <eberlm at in.tum.de> wrote:
>> Great work, thanks for taking care of this!
>> Just abstractly speaking, it would seem very odd to me to have a "complex analysis" directory without integration. Complex integration and the Cauchy integral formula are such basic tools in complex analysis that not including them in a "complex analysis" entry would seem… unusual to me.
>> Perhaps "complex analysis prerequisites".
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev