[isabelle-dev] Reorganising Analysis

[Tobias Nipkow]

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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191105/e7f29484/attachment-0001.bin>