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 <[email protected] <mailto:[email protected]>> 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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
