Document Open Access Logo

A Formalisation of Gallagher’s Ergodic Theorem

Author Oliver Nash

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.23.pdf
  • Filesize: 0.79 MB
  • 16 pages

Document Identifiers

Author Details

Oliver Nash
  • Imperial College London, UK

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 As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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.
  2. Thomas F. Bloom. On a density conjecture about unit fractions. (to appear), 2021. URL: https://arxiv.org/abs/2112.03726.
  3. Thomas F. Bloom and Bhavik Mehta. The Unit Fractions Project. (to appear), 2022. URL: https://b-mehta.github.io/unit-fractions/.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. Patrick Gallagher. Approximation by reduced fractions. J. Math. Soc. Japan, 13:342-345, 1961. URL: https://doi.org/10.2969/jmsj/01340342.
  9. Sébastien Gouëzel. Formalizing the Gromov-Hausdorff space. CoRR, abs/2108.13660, 2021. URL: https://arxiv.org/abs/2108.13660.
  10. 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.
  11. Glyn Harman. Metric number theory, volume 18 of London Mathematical Society Monographs. New Series. The Clarendon Press, Oxford University Press, New York, 1998. Google Scholar
  12. 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.
  13. 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.
  14. 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.
  15. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact