Uniformity norms

Stream: Polynomial Freiman-Ruzsa conjecture

[Yaël Dillies]

I know that PFR is connected to polynomial bounds on inverse uniformity norm theorems. Would it be interesting to formalise those as well? I have no idea how hard it is.

[Terence Tao]

Hmm. Defining the Gowers U^k norms and setting up the basic properties (in particular, that they are indeed norms, or at least seminorms for k=1) is certainly doable, and perhaps even a fun project (the underlying algebraic structure that these norms come from is called a "nilspace" - a sort of a higher order version of a group in which the multiplication operation is replaced by various cube corner completion maps - and actually has a rather pretty category-theoretic sort of structure, although if one is just interested in uniformity on finite abelian groups one can avoid all this generality and work with extremely concrete definitions for the norms). The inverse U^2 theorem is primarily driven by Plancherel's theorem and should also be easy (I would imagine for instance that APAP already has something close to this).

Polynomial Inverse U^3 for the specific case of elementary abelian 2-groups is an application of PFR that does have some uses. I estimate it would be comparable in difficulty to formalize as the ongoing Weak PFR formalization; weak PFR from PFR requires six pages of argument (Section 7 from https://arxiv.org/pdf/2306.13403.pdf) while polynomial inverse U^3 takes seven pages of argument (Appendix A from https://arxiv.org/pdf/math/0604353.pdf). One could certainly add this as an additional extension to the project if there is sufficient interest, although as with previous extensions I would expect a fairly slow pace in formalizing now that the project is not as high profile.

The inverse theory for anything beyond U^3 is still very difficult (proofs are routinely 30 or more pages, and often rely on previous papers of similar length), and also only marginally improved by PFR at our current level of technology. Here it is definitely best to wait for the mathematical understanding to improve and the proofs to simplify before attempting a formalization.

[Yaël Dillies]

Yes, I think I would need to add LeanAPAP as a dependency to PFR to even define the uniformity norms. With the API I already have, I believe I could define them now (in the finite abelian case) and prove their nestedness and the inverse U^2 theorem in about an afternoon.

[Yaël Dillies]

I'm particularly interested in the uniformity norms precisely because it would be a good stress test of my discrete Fourier analysis library.

[Yaël Dillies]

Where can I read about nilspaces? I assume they are related to nilsequences, but I cannot find them mentioned anywhere.

[Terence Tao]

The basic (algebraic) theory of these spaces is laid out here. For applications one often wants to deal with topological or measurable nilspaces (think of these as higher-order versions of topological groups or measurable groups), but for finite abelian groups the algebraic theory suffices. If there was someone planning on teaching additive combinatorics with some formal component, one could imagine contributing to an API for uniformity norms / nilspaces to be accepted for some form of course credit (there are a lot of little lemmas that could serve as essentially homework exercises, including a bunch from my book with Van Vu for instance), after setting out a blueprint to guide the students of course.

Another relatively easy fact about Gowers norms to establish is the 99% inverse theory if a 1-bounded function has a U^{k+1} norm close to 1, then it is close to a degree k (phase) polynomial, and conversely. See for instance Theorem 1.1 of https://arxiv.org/pdf/1012.3509.pdf (which handles the more general situation of compact abelian groups). That result should be relatively pleasant to prove (it's basically an induction on k, with Fourier analysis providing the k=2 base case).

[Yaël Dillies]

Sadly there are no such courses for me take in Cambridge. I do have a lot of free time this coming summer, though!