[isabelle-dev] Reorganising Analysis

[Manuel Eberl]

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.

Manuel


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.
>
> Larry
>
>> 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...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191104/ee02a0c2/attachment.html>