Analysis · Aug 27, 2026
Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week
arXiv: A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
Contributors
Unnamed model · Floris van Doorn, Polona Durcik, Joris Roos +2
AI systems: Unnamed model