← All papers
A Formalisation of Gallagher's Ergodic Theorem
cs.LO
Feb 1, 2023 · v1
TL;DR
Formalizes Gallagher's ergodic theorem in Lean as groundwork toward the Duffin-Schaeffer conjecture.
Abstract
Gallagher's ergodic theorem is a result in metric number theory stating that the approximation of real numbers by rational numbers obeys a striking all-or-nothing behaviour. This paper discusses formalising this result in the Lean theorem prover. The result is a key preliminary for Koukoulopoulos and Maynard's proof of the Duffin-Schaeffer conjecture.
Problem
Gallagher's ergodic theorem states that the approximation of real numbers by rational numbers exhibits an all-or-nothing behavior. This result is a key preliminary for the proof of the Duffin-Schaeffer conjecture by Koukoulopoulos and Maynard, and had not been formally verified.
Approach
The authors formalize Gallagher's ergodic theorem in the Lean theorem prover. The formalization covers the metric number theory result establishing the dichotomy in rational approximation quality for almost all real numbers.
Results
The formalization of Gallagher's ergodic theorem is completed in Lean, providing a verified preliminary for the Duffin-Schaeffer conjecture proof.