Gallagher遍历定理的形式化
A formalisation of Gallagher's ergodic theorem
摘要：
加拉格尔遍历定理是度量数论中的一个结果。它指出，实数的近似有理数服从一个惊人的“全有或全无”的行为。我们讨论了一个形式化的精益定理证明这一结果。这个结果不仅本身值得注意，而且是库库洛普洛斯和梅纳德最近对达芬-谢弗猜想的惊人证明所必需的一个关键的先决条件。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
