Stream: General

Topic: Analysis


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Apr 14 2021 at 13:16):

Not sure I would call this an analysis result though…

view this post on Zulip Manuel Eberl (Apr 14 2021 at 13:17):

I mean it uses techniques from complex analysis I guess…

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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: Aug 15 2022 at 02:13 UTC