{"id":"arxiv/2608.27321","url":"https://arxiv.org/abs/2608.27321","tags":["math.DS","math.CA"],"score":0,"title":"A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations","domain":"math.DS","source":"arxiv","authors":["Floris van Doorn","Polona Durcik","Joris Roos","Lenka Slavíková","Christoph Thiele"],"reviews":0,"subject":"math.DS","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-27","reactions":{}}