TY - RPRT TI - A formalisation of Gallagher's ergodic theorem AU - Oliver Nash PY - 2023 UR - https://arxiv.org/abs/2302.00448 ID - 2302.00448 ER -