A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2608.27321
curl -X POST /api/v1/records/arxiv/2608.27321/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.27321/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'