REVIEW 2 major objections 3 minor 23 references
A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
T0 review · 2 major / 3 minor · reviewed 2026-08-28 · deepseek-v4-flash
Pith's one-line read An explicit constant bounds the $r$-variation of multiple ergodic averages for any $n\ge 2$ commuting transformations ($2344$ for $n=2$), strengthening the norm-convergence theorem and answering an effective-ergodic-theory question; the…
desk verdict Main theorem is a real new result for general n, but the stated n=2 constant does not follow from the proof; the transference step and Lean repository also need pinning down. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing object is the family of sandwich kernels $M(\gamma,X,i)$: products in which all but one factor are two-dimensional Gaussians $G_{a(j),u}$ attached to multiplicatively spaced sequences $a:\mathbb{Z}\to(0,\infty)$ (satisfying $a(j+1)\ge 2a(j)$), with a single factor $X_{i,j}$ sandwiched between them. The argument's engine is an induction on the number $k$ of scales: 'InductPositiveTerms($k{+}1$)' implies 'IncreaseData($k$)', which implies 'DiagonalBand($k$)', which implies 'VanishingDiagonal($k$)', which implies 'InductPositiveTerms($k$)', with the base at $k=n$ given by a vanishing-kernel-integral cancellation. At every step the kernels are controlled by two exact Brascamp–Lieb inequalities (the cube and prism forms, each bounded by the $L^1$ norm of the test function) and by Gaussian domination, which dominates each $N$-multiplier pointwise by a sum of two-dimensional Gaussians with explicitly tracked constants. In the final reduction, the characteristic function $1_{[0,1]}$ is decomposed into a universal pair of windows satisfying $(\widehat\phi_0)^2+(1-\widehat\phi_1)^2=1$, which allows the real-variable estimate to be pushed through interpolation and the transference principle.
What would settle it
Open the Lean 4 repository accompanying the paper and inspect the declaration corresponding to Theorem 5.5: if the formalized transference principle is not instantiated with the exact averages $M_N(f)$ and the constant $2^{4n+6}$, the implication from Theorem 1.4 to Theorem 1.2 is not established by the formal proof.
Extended reading notes
Core claim
The central discovery is Theorem 1.2: for $n\ge 2$ mutually commuting measure-preserving transformations on a $\sigma$-finite measure space and functions $f_j\in L^{2n}(X)$, the multiple ergodic averages $M_N(f)$ satisfy $\|M_N(f)\|_{V^r(L^2(X))} \le C_{1.2,n,r} \prod_j \|f_j\|_{L^{2n}}$, where $C_{1.2,2,r}=2344$ and $C_{1.2,n,r}=2^{4n+337}\,(r/(r-2^{n-1}))^{1/r}$ for $n\ge 3$ and $r>2^{n-1}$. The paper obtains this by reducing it to an explicit real-variable estimate, Theorem 1.4, for twisted multilinear averages on $\mathbb{R}^n$; that estimate is proved by a recursive induction on the number of scales, driven by sandwich kernels built from two-dimensional Gaussians and by exact Brascamp–Lieb inequalities. The authors state that the entire argument has been formalized in the Lean 4 proof assistant, with this blueprint serving as the formalization's specification.
Load-bearing premise
The ergodic conclusion rests on the transference principle as applied with an explicit constant: the paper cites it as a 'slight restatement' of a previously formalized theorem rather than proving that exact statement for these averages, so if the cited version does not cover the stated constant and averages, the bridge from the real-variable estimate to Theorem 1.2 breaks.
Editorial extensions
If this is right
- For $n\ge 2$, the multiple ergodic averages converge in $L^2$ with an explicit quantitative rate encoded by a finite $r$-variation norm; in particular, the norm-convergence theorem for commuting transformations follows without any abstract compactness or ultrafilter argument.
- The open question about effective, quantitative norm-convergence of multiple ergodic averages is answered in the affirmative: the constants are fully explicit, with $C_{1.2,2,r}=2344$ for two transformations.
- The real-variable estimate (Theorem 1.4) is a stand-alone a priori bound for twisted averages with the characteristic-function kernel, holding for all $n\ge 2$ with constant $C_{1.4}=2^{666}$ and a polynomial factor $J^{1-2^{-n+2}}$ in the number of jumps.
- The entire analytic argument has been formally verified in the Lean 4 proof assistant, and the blueprint was explicitly designed to be the formalization's specification, with strict forward reasoning and named dependencies throughout.
- The transference step from the real line to arbitrary measure spaces is stated with an explicit factor $2^{4n+6}$, so the final ergodic bound inherits a fully effective constant from the real-variable estimate.
Reading between the lines
- The modular induction (positive terms → increase data → diagonal band → vanishing diagonal) does not appear to use any special property of the characteristic-function kernel beyond positivity and cancellations, so the same skeleton should adapt to other sandwich-type configurations, such as effective variation estimates for the simplex Hilbert transform or twisted paraproducts.
- If the Lean formalization is faithful, it demonstrates that LLM-assisted autoformalization can now cover a substantive harmonic-analysis argument in days rather than years; the blueprint's enforced conventions (strict forward reasoning, explicit constants, named dependencies) are likely the decisive enabling factor.
- The displayed constants compound extremely rapidly through the recursion (e.g., $C_{3.48}<2^{359}$, $C_{1.4}=2^{666}$), so a numerically practical bound for small $n$ would require re-running the argument with refined intermediate estimates rather than using the paper's displayed constants as they stand.
- A natural test extension is the nilpotent group setting: since the real-variable machinery does not seem to use commutativity beyond the twisted-average structure, the same scheme could plausibly yield explicit variation bounds for multiple ergodic averages on nilmanifolds.
Formalized claims in Lean
-
Claim #1: The central discovery is Theorem 1.2: for $n\ge 2$ mutually commuting measure-preserving transformations on a $\sigma$-finite measure space and functions $f_j\in L^{2n}(X)$, the multiple ergodic averages $M_N(f)$ satisfy $\|M_N(f)\|_{V^r(L^2(X))} \le C_{1.2,n,r} \prod_j \|f_j\|_{L^{2n}}$, where $C_{1.2,2,r}=2344$ and $C_{1.2,n,r}=2^{4n+337}\,(r/(r-2^{n-1}))^{1/r}$ for $n\ge 3$ and $r>2^{n-1}$. The
/-- @claim 1 The central discovery is Theorem 1.2: for $n\ge 2$ mutually commuting measure-preserving transformations on a $\sigma$-finite measure space and functions $f_j\in L^{2n}(X)$, the multiple ergodic averages $M_N(f)$ satisfy $\|M_N(f)\|_{V^r(L^2(X))} \le C_{1.2,n,r} \prod_j \|f_j\|_{L^{2n}}$, where $C_{1.2,2,r}=2344$ and $C_{1.2,n,r}=2^{4n+337}\,(r/(r-2^{n-1}))^{1/r}$ for $n\ge 3$ and $r>2^{n-1}$. The -/ def central_claim : Prop :=
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. This blueprint supports a claimed Lean 4 formalization and serves as a companion to a forthcoming paper. Its main theorem (Theorem 1.2) asserts that for n ≥ 2 commuting measure-preserving transformations on a σ-finite measure space and f_i ∈ L^{2n}(X), the r-variation norm of the multiple ergodic averages M_N(f) is bounded by C ∏_i ||f_i||_{2n} for r > 2^{n−1} (or r ≥ 2 for n = 2), with explicit constants C_{1.2,2,r} = 2344 and C_{1.2,n,r} = 2^{4n+337}(r/(r−2^{n−1}))^{1/r} for n ≥ 3. This would quantitatively strengthen Tao's norm-convergence theorem and answer a question of Avigad and Rute. The ergodic estimate is reduced via the Calderón transference principle (Theorem 5.5) to a real-variable estimate for twisted averages (Theorem 1.4, constant 2^{666}), proved by an extensive harmonic-analysis argument using sandwich kernels, Brascamp–Lieb inequalities, Gaussian domination, and an induction over scale dimensions. Every constant is explicitly named and recursively tracked, and the informal proofs are almost entirely machine-generated. The paper states that all proofs have been formally verified in Lean 4, with the repository linked by a GitHub URL only.
Significance. If Theorem 1.2 is correct, it is a substantial quantitative strengthening of Tao's norm-convergence theorem for commuting transformations, with new explicit-constant results for n ≥ 4 and a positive answer to the Avigad–Rute question. The manuscript's strengths are real: constants are constructed rather than fitted; every inequality carries an explicitly named, recursively defined constant (e.g., C_{3.48}, C_{4.75}, C_{5.7,n}); dependencies between statements are listed explicitly; and the claimed machine-checked formalization, if auditable, would be a milestone. As far as I checked, the constant propagation for n ≥ 3 is internally consistent. The main reservations are that the printed proof does not establish the stated n = 2 constant (it yields 2^{344}, not 2344), and the Calderón transference step is stated only 'up to slight restatement' of [20] with an unexplained constant; both points must be repaired for the main claim as stated. The formalization artifact is not yet versioned, so the paper's own justification for trusting unhand-checked informal proofs cannot be independently verified.
major comments (2)
- [Theorem 1.2; Section 5 (Theorem 5.7, Lemma 5.8)] The constant C_{1.2,2,r} = 2344 displayed in Theorem 1.2 is not established by the proof as printed. Theorem 5.7 gives C_{5.7,2} = 2^{688}; with D = 2^{688} ∏_i ||f_i||_4^2, Lemma 5.8 with r_0 = 2 (Eq. (5.19)) yields only ||M_N(f)||_{V^2(L^2)} ≤ D^{1/2} = 2^{344} ∏_i ||f_i||_4. The final proof of Theorem 1.2 says only 'If n=2, Lemma 5.8 gives the result for r=2, and the monotonicity of finite ℓ^r norms gives it for every r≥2'; no argument in Section 5 reduces 2^{344} to 2344, and the sharper n=2 results [6,17] are not invoked at that point. For n ≥ 3 the stated constant is consistent with the propagation, since 2^{1−2^{1−n}} C_{5.7,n}^{1/2} ≤ 2^{4n+337}; the gap is specific to the n=2 statement. Please supply the missing n=2 argument, change the stated constant to a value the proof actually supports (such as 2^{344}), or explicitly import the constant from [6,17] in the proof of Theorem 1.2, and reconcile the choice with the claim in §1.1 that constant discrepancies surfaced by the formalization were fixed.
- [Theorem 5.5 and §1.3] Section 5's final bridge from the real-variable estimate to the ergodic theorem is the Calderón transference principle, but the version used is not stated precisely. Theorem 5.5 is introduced as 'a standard result' found 'up to slight restatement' as Theorem 2.5 of Pernegger [20], carrying an explicit constant C_{5.5,n} = 2^{4n+6} and the specific averages of Definitions 1.1 and 1.3. Neither the restatement (translated into the present notation) nor the derivation of the constant is given, and no Lean statement is identified for this instance. Since C_{5.5,n} enters C_{5.6,n,(p_i)} and C_{5.7,n} multiplicatively, the constants of Theorem 1.2 inherit this step; if the formalization does not cover exactly this statement, the last step of the printed proof has a gap. Please provide the precise statement used, justify or cite the constant 2^{4n+6}, and identify the corresponding Lean statement, or state explicitly that this step is assumed rather than formalized.
minor comments (3)
- [§1.2] The formalization is linked only by a GitHub URL with no commit hash or archived DOI, and the ∀ annotations name Lean statements only for statements in the introduction. Please provide a versioned artifact and list the Lean statement names for Theorem 1.2, Theorem 1.4, and the transference instance used as Theorem 5.5, so that the assertion in §1.1 that unhand-checked informal proofs are acceptable because the proofs have been formalized can be verified.
- [§5, Theorem 5.6] The proof of Theorem 5.6 applies Proposition 5.4 with its complex-input constant 2^{2n} C_{1.4} to real-valued inputs and then adds another factor 2^{2n} for complex inputs at the ergodic level. As an upper-bound argument this is valid, but it makes C_{5.6,n,(p_i)} and hence C_{5.7,n} a factor 2^{2n} larger than the chain strictly requires; given the paper's emphasis on explicit constants, a streamlined accounting would be preferable.
- [Abstract and References] The abstract refers to a 'forthcoming, shorter traditional mathematical paper' that is not identified by a preprint number, and reference [9] is cited as published in Analysis & PDE 19 (2026); please provide arXiv identifiers or confirmation of the publication data so that cross-references can be checked.
Circularity Check
No significant circularity: constants are constructed explicitly, and each load-bearing reduction is either proved in this blueprint or delegated to standard external theorems.
full rationale
The argument is acyclic: Theorem 1.2 is obtained from the real-variable estimate Theorem 1.4 through the Calderón transference principle (Theorem 5.5), and Theorem 1.4 is proved in Section 4 from the independently proved inductive estimate Theorem 3.48 (InductPositiveTerms(2, C_3.48)). The constants are produced by explicit recursions in Sections 2–3; there is no fitted parameter that is then renamed as a prediction. The papers [6, 17, 9] are cited only as earlier versions of parts of Theorem 1.2, not as the proof of the present Theorem 1.2, so they are not load-bearing. The two external theorems, multilinear interpolation (Theorem 5.2) and Calderón transference (Theorem 5.5), are standard results attributed to [3] and to Pernegger's Lean formalization [20], respectively; no self-citation chain forces the conclusion. Two non-circular gaps are flagged: the printed n=2 step ('If n=2, Lemma 5.8 gives the result for r=2') yields C_{5.7,2}^{1/2} = 2^{344}, not the stated 2344, so the n=2 constant is either an unproved import or a typo; and Theorem 5.5 is said to be 'up to slight restatement' of [20, Theorem 2.5], with that exact restatement not shown. The machine-generated (/car) proofs are admittedly not hand-checked, but the claimed Lean formalization provides independent, non-circular support. No equation in the paper reduces a claimed output to its own input by construction.
Assumptions & free parameters
assumptions (3)
- standard math Multilinear complex interpolation theorem (Theorem 5.2)
- standard math Calderon transference principle with explicit constant C_{5.5,n}=2^{4n+6} (Theorem 5.5)
- ad hoc to paper Completeness of the linked Lean 4 formalization
Cite this review
Pith. "Pith review of A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations." pith.science (2026). https://pith.science/paper/WT3BBE2T
@misc{pith2026260827321,
author = {Pith},
title = {Pith review of: A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations},
year = {2026},
howpublished = {\url{https://pith.science/paper/WT3BBE2T}},
note = {Machine review of arXiv:2608.27321}
}
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.
Reference graph
Works this paper leans on
-
[20]
F. Pernegger,Formalisation of the Calder´ on Transference Principle in Ergodic Theory, Bachelor’s thesis, Rheinische Friedrich-Wilhelms-Universit¨ at Bonn, September 2025
work page 2025
-
[1]
Austin, On the norm convergence of non-conventional ergodic averages,Ergodic Theory Dynam
T. Austin, On the norm convergence of non-conventional ergodic averages,Ergodic Theory Dynam. Systems30(2010), 321–338
work page 2010
-
[2]
J. Avigad and J. Rute, Oscillation and the mean ergodic theorem for uniformly convex Banach spaces,Ergodic Theory Dynam. Systems35(2015), 1009–1027
work page 2015
-
[3]
J. Bergh and J. L¨ ofstr¨ om,Interpolation Spaces: An Introduction, Springer-Verlag, Berlin, 1976
work page 1976
-
[4]
A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
L. Becker, M. I. de Frutos-Fern´ andez, L. Diedering, F. van Doorn, S. Gou¨ ezel, A. Jamneshan, E. Karunus, E. van de Meent, P. Monticone, J. Mulder-Sohn, J. Portegies, J. Roos, M. Rothgang, R. Srivastava, J. Sundstrom, J. Tan, and C. Thiele,A blueprint for the formalization of Carleson’s theorem on convergence of Fourier series, arXiv:2405.06423v2, 2025
work page Pith review arXiv 2025
-
[5]
Carleson operators on doubling metric measure spaces
L. Becker, F. van Doorn, A. Jamneshan, R. Srivastava, and C. Thiele,Carleson operators on doubling metric measure spaces, arXiv:2508.05563, 2025
work page Pith review arXiv 2025
- [6]
- [7]
Show all 23 references
-
[8]
Durcik, L
P. Durcik, L. Slav´ ıkov´ a, and C. Thiele, Local bounds for singular Brascamp–Lieb forms with cubical structure,Math. Z.302(2022), 2375–2405
2022
-
[9]
Durcik, L
P. Durcik, L. Slav´ ıkov´ a, and C. Thiele, Norm-variation of triple ergodic averages for commuting transformations,Anal. PDE19(2026), 539–586
2026
-
[10]
Durcik and C
P. Durcik and C. Thiele, Singular Brascamp–Lieb: a survey, inGeometric Aspects of Harmonic Analysis, Springer INdAM Ser.45, Springer, Cham, 2021, 321–349
2021
-
[11]
Gr¨ ochenig,Foundations of Time-Frequency Analysis, Birkh¨ auser, 2001
K. Gr¨ ochenig,Foundations of Time-Frequency Analysis, Birkh¨ auser, 2001
2001
-
[12]
H¨ ormander,The Analysis of Linear Partial Differential Operators I: Distribution Theory and Fourier Analysis, second edition, Springer-Verlag, Berlin, 1990
L. H¨ ormander,The Analysis of Linear Partial Differential Operators I: Distribution Theory and Fourier Analysis, second edition, Springer-Verlag, Berlin, 1990
1990
-
[13]
Host, Ergodic seminorms for commuting transformations and applications,Studia Math.195 (2009), 31–49
B. Host, Ergodic seminorms for commuting transformations and applications,Studia Math.195 (2009), 31–49
2009
-
[14]
R. L. Jones, I. V. Ostrovskii, and J. M. Rosenblatt, Square functions in ergodic theory,Ergodic Theory Dynam. Systems16(1996), 267–305
1996
-
[15]
R. L. Jones, A. Seeger, and J. Wright, Strong variational and jump inequalities in harmonic analysis,Trans. Amer. Math. Soc.360(2008), 6711–6742
2008
-
[16]
Kovaˇ c, Boundedness of the twisted paraproduct,Rev
V. Kovaˇ c, Boundedness of the twisted paraproduct,Rev. Mat. Iberoam.28(2012), 1143–1164
2012
-
[17]
Kovaˇ c, Quantitative norm convergence of double ergodic averages associated with two com- muting group actions,Ergodic Theory Dynam
V. Kovaˇ c, Quantitative norm convergence of double ergodic averages associated with two com- muting group actions,Ergodic Theory Dynam. Systems36(2016), 860–874
2016
-
[18]
367–381, doi:10.1145/3372885.3373824
The mathlib Community,The Lean mathematical library, inProceedings of the 9th ACM SIG- PLAN International Conference on Certified Programs and Proofs (CPP 2020), Association for Computing Machinery, New York, 2020, pp. 367–381, doi:10.1145/3372885.3373824. 116 VAN DOORN, DURCI...
2020
-
[19]
de Moura and S
L. de Moura and S. Ullrich,The Lean 4 theorem prover and programming language, inAutomated Deduction – CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, 2021, pp. 625– 635
2021
-
[21]
Tao, Norm convergence of multiple ergodic averages for commuting transformations,Ergodic Theory Dynam
T. Tao, Norm convergence of multiple ergodic averages for commuting transformations,Ergodic Theory Dynam. Systems28(2008), 657–688
2008
-
[22]
M. N. Walsh, Norm convergence of nilpotent ergodic averages,Ann. of Math.175(2012), 1667– 1688
2012
-
[23]
Wiener, Tauberian theorems,Ann
N. Wiener, Tauberian theorems,Ann. of Math.33(1932), 1–100. Mathematical Institute, University of Bonn, Endenicher Allee 60, 53115 Bonn, Germany Email address:vdoorn@math.uni-bonn.de Schmid College of Science and Technology, Chapman University, One University Drive, Orange, CA...
1932
Reviewed August 28, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.