LIPIcs.ITP.2023.23.pdf
- Filesize: 0.79 MB
- 16 pages
Document
A Formalisation of Gallagher’s Ergodic Theorem
Author
Oliver Nash 
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Acknowledgements
It is a pleasure to thank Andrew Pollington who suggested this project during the conference Lean for the Curious Mathematician, held at Brown University (ICERM) in 2022. I also wish to thank Anatole Dedecker, Heather Macbeth, Patrick Massot, and Junyan Xu, all of whom were of direct assistance. Lastly I especially wish to thank Sébastien Gouëzel for many helpful suggestions and Kevin Buzzard for many useful conversations.
Cite AsGet BibTex
Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.23
https://doi.org/10.4230/LIPIcs.ITP.2023.23
Abstract
Gallagher’s ergodic theorem is a result in metric number theory. It states that the approximation of real numbers by rational numbers obeys a striking "all or nothing" behaviour. We discuss a formalisation of this result in the Lean theorem prover. As well as being notable in its own right, the result is a key preliminary, required for Koukoulopoulos and Maynard’s stunning recent proof of the Duffin-Schaeffer conjecture.
Subject Classification
ACM Subject Classification
- Mathematics of computing → Probability and statistics
Keywords
- Lean proof assistant
- measure theory
- metric number theory
- ergodicity
- Gallagher’s theorem
- Duffin-Schaeffer conjecture
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Christoph Aistleitner, Bence Borda, and Manuel Hauke. On the metric theory of approximations by reduced fractions: a quantitative Koukoulopoulos-Maynard theorem. Compos. Math., 159(2):207-231, 2023. URL: https://doi.org/10.1112/S0010437X22007837.
- Thomas F. Bloom. On a density conjecture about unit fractions. (to appear), 2021. URL: https://arxiv.org/abs/2112.03726.
- Thomas F. Bloom and Bhavik Mehta. The Unit Fractions Project. (to appear), 2022. URL: https://b-mehta.github.io/unit-fractions/.
- Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 299-312, 2020. URL: https://doi.org/10.1145/3372885.3373830.
- J. W. S. Cassels. Some metrical theorems in Diophantine approximation. I. Proc. Cambridge Philos. Soc., 46:209-218, 1950. URL: https://doi.org/10.1017/s0305004100025676.
- Johan Commelin, Adam Topaz, et al. The Liquid Tensor Experiment. (to appear), 2022. see also https://www.nature.com/articles/d41586-021-01627-2. URL: https://github.com/leanprover-community/lean-liquid.
- R. J. Duffin and A. C. Schaeffer. Khintchine’s problem in metric Diophantine approximation. Duke Math. J., 8:243-255, 1941. URL: http://projecteuclid.org/euclid.dmj/1077492641.
- Patrick Gallagher. Approximation by reduced fractions. J. Math. Soc. Japan, 13:342-345, 1961. URL: https://doi.org/10.2969/jmsj/01340342.
- Sébastien Gouëzel. Formalizing the Gromov-Hausdorff space. CoRR, abs/2108.13660, 2021. URL: https://arxiv.org/abs/2108.13660.
- Sébastien Gouëzel. A formalization of the change of variables formula for integrals in mathlib. In Kevin Buzzard and Temur Kutsia, editors, Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, volume 13467 of Lecture Notes in Computer Science, pages 3-18. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-16681-5_1.
-
Glyn Harman. Metric number theory, volume 18 of London Mathematical Society Monographs. New Series. The Clarendon Press, Oxford University Press, New York, 1998.
- Dimitris Koukoulopoulos and James Maynard. On the Duffin-Schaeffer conjecture. Ann. of Math. (2), 192(1):251-307, 2020. URL: https://doi.org/10.4007/annals.2020.192.1.5.
- A. D. Pollington and R. C. Vaughan. The k-dimensional Duffin and Schaeffer conjecture. Mathematika, 37(2):190-200, 1990. URL: https://doi.org/10.1112/S0025579300012900.
- The mathlib community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 367-381, 2020. URL: https://doi.org/10.1145/3372885.3373824.
- Floris van Doorn. Formalized Haar Measure. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:17, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.18.