Re: [isabelle-dev] Gromov Hyperbolicity
Oh, well, yes, a special case of metric completion (the reals) was mentioned in passing, I think. And a more general notion (something like the completion of a topological group, I think?) featured in my Algebra 1 course, which was an elective. But "metric completion" as such I have not heard before. Lipschitz continuity is certainly undergraduate material. That probably appears in any introductory Analysis lecture, even those for computer scientists. Manuel On 2018-01-19 12:01, Tjark Weber wrote: > On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote: >>> One possible criterion: which results >>> are part of a standard undergraduate athematics curriculum? >> It sounds like a reasonable criterion. Can you tell us what that means for >> Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)? > Metric completion features prominently, e.g., in the construction of > the reals. Lipschitz continuity (along with the Picard–Lindelöf > theorem) should be part of any course on differential equations. > > I can't recall whether I've been taught about Hausdorff distance or > even isometries during my undergraduate years. Of course, these are > fairly simple concepts. > > Best, > Tjark > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote: > > One possible criterion: which results > > are part of a standard undergraduate athematics curriculum? > > It sounds like a reasonable criterion. Can you tell us what that means for > Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)? Metric completion features prominently, e.g., in the construction of the reals. Lipschitz continuity (along with the Picard–Lindelöf theorem) should be part of any course on differential equations. I can't recall whether I've been taught about Hausdorff distance or even isometries during my undergraduate years. Of course, these are fairly simple concepts. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
I'm afraid I've no idea. I didn't study much analysis for my first degree, not even the basics of complex analysis. Larry > On 18 Jan 2018, at 14:29, Tobias Nipkowwrote: > > So what is the situation wrt the theories I asked about? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
I for one have not encountered any of these things in my undergraduate mathematics lectures. But the situation may well be different in other universities. On 2018-01-18 15:29, Tobias Nipkow wrote: > So what is the situation wrt the theories I asked about? > > Tobias > > On 18/01/2018 15:11, Lawrence Paulson wrote: >> This is mainly a negative criterion, i.e., something outside the >> undergraduate curriculum probably should not be in our core >> libraries. But I would guess for example mathematicians cover Gödel's >> theorem, which we would not want to move to our core libraries. >> >> Larry >> >>> On 18 Jan 2018, at 13:31, Tobias Nipkowwrote: >>> >>> It sounds like a reasonable criterion. Can you tell us what that >>> means for Hausdorff_Distance, Metric_Completion and Isometries (as >>> detailed by Fabian)? >> > > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
So what is the situation wrt the theories I asked about? Tobias On 18/01/2018 15:11, Lawrence Paulson wrote: This is mainly a negative criterion, i.e., something outside the undergraduate curriculum probably should not be in our core libraries. But I would guess for example mathematicians cover Gödel's theorem, which we would not want to move to our core libraries. Larry On 18 Jan 2018, at 13:31, Tobias Nipkowwrote: It sounds like a reasonable criterion. Can you tell us what that means for Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)? smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
This is mainly a negative criterion, i.e., something outside the undergraduate curriculum probably should not be in our core libraries. But I would guess for example mathematicians cover Gödel's theorem, which we would not want to move to our core libraries. Larry > On 18 Jan 2018, at 13:31, Tobias Nipkowwrote: > > It sounds like a reasonable criterion. Can you tell us what that means for > Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
> Am 18.01.2018 um 14:36 schrieb Tobias Nipkow: > > > > On 18/01/2018 11:06, Fabian Immler wrote: >>> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow : >>> >>> 1. Library/Complement contains both new generic material like "t3_space" >>> but also new concepts like [mono_intros] for more automation in proving of >>> inequalities. In short, there is a wealth of material that might be >>> suitable for inclusion in HOL-Analysis. >>> I have already made a start by moving a few [simp] rules but that is it >>> from me because I am not familiar enough with the Analysis material. >> Most of this looks like it could go to HOL-Analysis. >>> 2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of >>> generic concepts that should go somewhere else. >>> We need a discussion on whether any of the theories deserve a separate AFP >>> entry. >> In my opinion, Hausdorff_Distance and Metric_Completion are general enough >> to put them to HOL-Analysis. >> (They are also relatively short, so I am not sure if it is worth to create >> separate AFP entries.) >> The theory Isometries contains Lipschitz maps, isometries, geodesic spaces, >> and quasi-isometries. >> The very same definition of Lipschitz maps is also in >> AFP/Ordinary_Differential_Equations, so I take this as a strong indication >> to move Lipschitz maps to HOL-Analysis. Isometries also seem like a >> generically useful concept and could go to HOL-Analysis. > > A lot of things are useful, but Isometries.thy is large and would also make a > nice AFP entry. With "Isometries" I meant the part of Isometries.thy that introduces isometry_on (this is only 150 lines). Lipschitz maps are another 350 lines. The rest of Isometries.thy seems to be about geodesic spaces and quasi-isometries could indeed make a separate AFP entry. Fabian >> My impression is that geodesic spaces and quasi-isometries are more >> specialised concepts (but that might also be just because I have never come >> across them up to now...). I have no real opinion on what to do with them. >> We do not have a precise specification of what HOL-Analysis is or should be. >> I think that makes it very hard to draw a line between material that should >> go to HOL-Analysis and what should remain in the AFP. So take this as just >> my personal view. >> Fabian > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
On 18/01/2018 11:06, Fabian Immler wrote: Am 18.01.2018 um 08:32 schrieb Tobias Nipkow: 1. Library/Complement contains both new generic material like "t3_space" but also new concepts like [mono_intros] for more automation in proving of inequalities. In short, there is a wealth of material that might be suitable for inclusion in HOL-Analysis. I have already made a start by moving a few [simp] rules but that is it from me because I am not familiar enough with the Analysis material. Most of this looks like it could go to HOL-Analysis. 2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of generic concepts that should go somewhere else. We need a discussion on whether any of the theories deserve a separate AFP entry. In my opinion, Hausdorff_Distance and Metric_Completion are general enough to put them to HOL-Analysis. (They are also relatively short, so I am not sure if it is worth to create separate AFP entries.) The theory Isometries contains Lipschitz maps, isometries, geodesic spaces, and quasi-isometries. The very same definition of Lipschitz maps is also in AFP/Ordinary_Differential_Equations, so I take this as a strong indication to move Lipschitz maps to HOL-Analysis. Isometries also seem like a generically useful concept and could go to HOL-Analysis. A lot of things are useful, but Isometries.thy is large and would also make a nice AFP entry. Tobias My impression is that geodesic spaces and quasi-isometries are more specialised concepts (but that might also be just because I have never come across them up to now...). I have no real opinion on what to do with them. We do not have a precise specification of what HOL-Analysis is or should be. I think that makes it very hard to draw a line between material that should go to HOL-Analysis and what should remain in the AFP. So take this as just my personal view. Fabian smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
On 18/01/2018 12:48, Lawrence Paulson wrote: We certainly need to solve this problem. Absolutely. For practical reasons I would put as much in the AFP as possible, (One could make exceptions for small theories, but this could get out of hand again). One possible criterion: which results are part of a standard undergraduate athematics curriculum? It sounds like a reasonable criterion. Can you tell us what that means for Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)? Tobias Larry On 18 Jan 2018, at 10:06, Fabian Immler> wrote: We do not have a precise specification of what HOL-Analysis is or should be. I think that makes it very hard to draw a line between material that should go to HOL-Analysis and what should remain in the AFP. So take this as just my personal view. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
We certainly need to solve this problem. One possible criterion: which results are part of a standard undergraduate athematics curriculum? Larry > On 18 Jan 2018, at 10:06, Fabian Immlerwrote: > > We do not have a precise specification of what HOL-Analysis is or should be. > I think that makes it very hard to draw a line between material that should > go to HOL-Analysis and what should remain in the AFP. So take this as just my > personal view. signature.asc Description: Message signed with OpenPGP ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Gromov Hyperbolicity
> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow: > > 1. Library/Complement contains both new generic material like "t3_space" but > also new concepts like [mono_intros] for more automation in proving of > inequalities. In short, there is a wealth of material that might be suitable > for inclusion in HOL-Analysis. > I have already made a start by moving a few [simp] rules but that is it from > me because I am not familiar enough with the Analysis material. Most of this looks like it could go to HOL-Analysis. > 2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of > generic concepts that should go somewhere else. > We need a discussion on whether any of the theories deserve a separate AFP > entry. In my opinion, Hausdorff_Distance and Metric_Completion are general enough to put them to HOL-Analysis. (They are also relatively short, so I am not sure if it is worth to create separate AFP entries.) The theory Isometries contains Lipschitz maps, isometries, geodesic spaces, and quasi-isometries. The very same definition of Lipschitz maps is also in AFP/Ordinary_Differential_Equations, so I take this as a strong indication to move Lipschitz maps to HOL-Analysis. Isometries also seem like a generically useful concept and could go to HOL-Analysis. My impression is that geodesic spaces and quasi-isometries are more specialised concepts (but that might also be just because I have never come across them up to now...). I have no real opinion on what to do with them. We do not have a precise specification of what HOL-Analysis is or should be. I think that makes it very hard to draw a line between material that should go to HOL-Analysis and what should remain in the AFP. So take this as just my personal view. Fabian smime.p7s Description: S/MIME cryptographic signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Gromov Hyperbolicity
For those of you interested in formalization of Analysis https://devel.isa-afp.org/entries/Gromov_Hyperbolicity.html I would like to call your attention to this entry because it is rich in concepts and theorems that are more general than the actual focus of the article. I believe quite a bit of the material could be pulled out and made more visible. Here are some pointers: 1. Library/Complement contains both new generic material like "t3_space" but also new concepts like [mono_intros] for more automation in proving of inequalities. In short, there is a wealth of material that might be suitable for inclusion in HOL-Analysis. I have already made a start by moving a few [simp] rules but that is it from me because I am not familiar enough with the Analysis material. 2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of generic concepts that should go somewhere else. We need a discussion on whether any of the theories deserve a separate AFP entry. Sebbastien has already made an effort to separate the generic from the specific. We should capitalize on that, but it needs a bit of voluntary work. Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev