[isabelle-dev] Reorganising Analysis

[Wenda Li]

> On 4 Nov 2019, at 12:48, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> 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?

Our definition of winding numbers is fine to me, as it follows classic analytical textbook definition which usually does not allow the target point on the path. Unless we want to further generalise the definition in a topological or algebraic direction (which does not seem too necessary at the moment), this point-on-the-path issue is probably what we have to live with. 

My two cents about our winding numbers is the organisation: winding numbers are (kind of secretly) defined in Cauchy_Integral_Theorem.thy rather than in Winding_Numbers.thy <https://isabelle.in.tum.de/repos/isabelle/file/c85efa2be619/src/HOL/Analysis/Winding_Numbers.thy>, which only contains advanced facts related to winding numbers.  Maybe it is worth having two theories about winding numbers — a basic one for the integral theorem and an advanced one that is on the top of Jordan_Curve & Riemann_Mapping.

Wenda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191105/619da84c/attachment.html>