[isabelle-dev] Reorganising Analysis
Tobias Nipkow
nipkow at in.tum.de
Tue Nov 5 13:55:52 CET 2019
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>
More information about the isabelle-dev
mailing list