A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, Christoph Thiele
math.DS
Aug 27, 2026 · v1
math.CA
TL;DR
Provides a blueprint underlying a Lean 4 formalization, completed largely automatically with LLMs, of norm-variation estimates for multiple ergodic averages.
Abstract
This blueprint serves as a companion to a forthcoming, shorter traditional mathematical paper. The purpose of this blueprint is two-fold: first, it has served as the foundation for a formalization in Lean 4 of these results. This formalization has been completed largely automatically, making essential use of current frontier large language models. Second, it will serve as a resource to readers of the main paper who are interested in further technical details of the proofs. The main result concerns norm-variation estimates for multiple ergodic averages associated with $n\ge 2$ commuting measure preserving transformations, providing a quantitative strengthening of Tao's norm-convergence theorem and answering an open question of Avigad and Rute. At the core of the analysis lies an explicit real-variable estimate for twisted multilinear averages that is closely related to certain singular Brascamp–Lieb inequalities.
Problem
Establishing norm-variation estimates for multiple ergodic averages associated with n>=2 commuting measure preserving transformations, quantitatively strengthening Tao's norm-convergence theorem and answering an open question of Avigad and Rute.
Approach
A detailed blueprint reduces the ergodic theorem to a real-variable estimate for twisted multilinear averages related to singular Brascamp–Lieb inequalities, using the Calderón transference principle and multilinear interpolation. The blueprint serves as the foundation for a Lean 4 formalization of the results. The formalization was completed largely automatically using frontier large language models. It relies on external theorems such as multilinear complex interpolation and a previously Lean-formalized Calderón transference principle.
Results
The main ergodic theorem yields r-variation norm bounds with explicit constants, recovering Tao's convergence theorem and answering the Avigad–Rute question. The results were formalized in Lean 4.
