[isabelle-dev] Reorganising Analysis
immler at in.tum.de
Mon Nov 4 16:50:03 CET 2019
On 11/4/2019 7:44 AM, Lawrence Paulson wrote:
> Then the obvious stopping point is one line above: Derivative.
Yes (with some additional theories):
In afp-devel/49f30bd (and its parent changesets) Tobias and I
experimented with reducing the imports of many AFP-entries that build on
We introduced a theory Multivariate_Analysis to collect the theories
that we deemed "Basic Analysis" material (perhaps Basic_Analysis.thy
would be a better name).
Currently (afp/c5c88012f116) we have 20 imports of
"HOL-Analysis.Multivariate_Analysis", and 35 imports of
"HOL-Analysis.Analysis", so Multivariate_Analysis seems like a
reasonable point to split HOL-Analysis.
The imports of Multivariate_Analysis can (or should) still be refined:
It currently(isa/c85efa2be619) imports Path_Connected and Starlike and I
am pretty sure much of the material in those theories is not necessary
for a "Basic Analysis" library.
> The problem at the moment with basing a development around the Cauchy integral theorem is that you might also want to include Winding_Numbers, but that theory inherits almost the whole of Analysis: even the Jordan curve theorem.
>> On 4 Nov 2019, at 12:19, Manuel Eberl <eberlm at in.tum.de> wrote:
>> Great work, thanks for taking care of this!
>> Just abstractly speaking, it would seem very odd to me to have a "complex analysis" directory without integration. Complex integration and the Cauchy integral formula are such basic tools in complex analysis that not including them in a "complex analysis" entry would seem… unusual to me.
>> Perhaps "complex analysis prerequisites".
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev