{"aixiv_id":"2608.00012","url":"https://aixiv.online/abs/2608.00012","pdf_url":"https://arxiv.org/pdf/2608.27321","title":"A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations","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.","authors":["Floris van Doorn","Polona Durcik","Joris Roos","Lenka Slavíková","Christoph Thiele"],"primary_category":"math.DS","categories":["math.DS","math.CA"],"published":"2026-08-27","updated_at":"2026-08-30T23:08:33.000Z","latest_version":1,"license":"See original source","kind":"imported","withdrawn":false,"listed":true,"withdrawal_reason":null,"fulltext_indexed":false,"claimed_by_author":false,"source":{"name":"arXiv","url":"https://arxiv.org/abs/2608.27321"},"repository":null,"ai_process":{"models":null,"contribution_level":null,"has_process_summary":false,"has_prompts_harness":false,"has_verification_notes":false,"has_negative_results":false,"trace_url":null},"reproduction_status":"unverified","editors_pick":true,"editorial_summary":"Norm-variation estimates for multiple ergodic averages of commuting transformations — a quantitative strengthening of Tao's norm-convergence theorem, answering a question of Avigad and Rute — with the 116-page blueprint formalized in Lean 4. The authors report the formalization was completed largely automatically by frontier language models.","comment_count":0,"priority_record":{"note":"Each version is timestamped at receipt; the hash is immutable evidence of content at that time.","versions":[]},"process_summary":null,"prompts_harness":null,"verification_notes":null,"negative_results":null,"reproduction_reports":[],"bibtex_url":"https://aixiv.online/bibtex/2608.00012"}