Anthony Bordg (Apr 14 2021 at 12:42): Anthony Bordg (Apr 14 2021 at 12:42):I know it is partly subjective, but what is the most advanced/impressive result in analysis available in Isabelle/HOL?
Jakub Kądziołka (Apr 14 2021 at 12:54):I have virtually no experience with analysis, but one theorem very interesting to me that happens to have been formalized in Isabelle is Dirichlet's arithmetic progression theorem: https://www.isa-afp.org/entries/Dirichlet_L.html
Manuel Eberl (Apr 14 2021 at 13:16):Not sure I would call this an analysis result though…
Manuel Eberl (Apr 14 2021 at 13:17):I mean it uses techniques from complex analysis I guess…
Manuel Eberl (Apr 14 2021 at 13:17):There's all kinds of things like invariance of domain/invariance of dimension, the Riemann theorem, a very general form of multivariate change of variables for integration
Manuel Eberl (Apr 14 2021 at 13:18):Green's theorem (albeit still with some technical assumptions where it is not entirely clear if and how they can be lifted)
Manuel Eberl (Apr 14 2021 at 13:19):Ah, and there's Apéry's Theorem. Not sure if that's impressive; it's certainly well-known, but at the end of the day the proof just boils down to a few integrals and applying the Prime Number Theorem.
Last updated: Dec 21 2024 at 12:33 UTC