关于交换变换多重遍历平均的范数变差形式化的蓝图
A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
AI总结：
该研究以蓝图形式为Lean 4中交换变换多重遍历平均的范数变差结果的形式化提供基础，利用前沿大语言模型完成形式化，强化了陶哲轩的定理并回答了开放问题。
AI中文摘要：
本蓝图是即将发表的一篇篇幅较短的传统数学论文的配套资料，其用途有二：其一，它是Lean 4中这些结果形式化的基础，该形式化工作已基本自动完成，充分利用了当前前沿的大语言模型；其二，它将作为主论文读者的参考资料，为对证明的进一步技术细节感兴趣的读者提供帮助。主要结果涉及与n≥2个交换保测变换相关的多重遍历平均的范数变差估计，这是对陶哲轩的范数收敛定理的定量强化，同时回答了Avigad和Rute提出的一个开放问题。分析的核心是关于扭曲多重线性平均的显式实变量估计，该估计与某些奇异Brascamp–Lieb不等式密切相关。
英文摘要：
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.
