@misc{indiciae3beb45e8a2b6, title = {A formalisation of Gallagher's ergodic theorem}, author = {Oliver Nash}, year = {2023}, url = {https://arxiv.org/abs/2302.00448}, note = {Source identifier: 2302.00448} }