[isabelle-dev] Reorganising Analysis

[Wenda Li]

No problem. I will take care of the split.

Wenda

> On 5 Nov 2019, at 12:55, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> I stumbled across this oddity - the important concept of winding numbers being defined in the middle of Cauchy_Integral_Theorem - myself this morning just looking at the toc. Thus I am all in favour of splitting off Winding Numbers from Cauchy_Integral_Theorem: the latter contains 1000 lines of material following the definition up to subsection "Cauchy's integral formula, again for a convex enclosing set". Later there is some more material:
> subsection ‹More winding number properties›
> 
> Wenda, would you mind performing this split that you suggested?
> Not sure about the names: Maybe Winding_Numbers and Winding_Numbers_Applied? Any better ideas?
> 
> Tobias
> 
> On 05/11/2019 01:54, Wenda Li wrote:
>>> On 4 Nov 2019, at 12:48, Manuel Eberl <eberlm at in.tum.de <mailto: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.th <http://cauchy_integral_theorem.th>y 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
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev