A formalisation of Gallagher's ergodic theorem
Logic in Computer Science
2023-02-02 v1 Number Theory
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.
Cite
@article{arxiv.2302.00448,
title = {A formalisation of Gallagher's ergodic theorem},
author = {Oliver Nash},
journal= {arXiv preprint arXiv:2302.00448},
year = {2023}
}
Comments
16 pages, 2 figures