Formalizing F_2^n

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

The PFR conjecture is a statement about non-empty subsets A of finite dimensional vector spaces F_2^n over the field F_2 of two elements: it says that if A has doubling at most K in the sense that |A+A| ≤ K * |A| (where A+A is the Minkowski sum of A with itself), then A can be covered by at most 2 K^12 cosets of a subgroup H of F_2^n of cardinality at most A. (The specific constant 12 is what came out of our proof (see Theorem 1.1 of https://arxiv.org/abs/2311.05762); it is not optimal.)

That's the standard way of stating the theorem, but the vector space structure is not really used in the proof. Basically, what is needed is that A lives in a finite abelian group G in which every element has order at most 2, i.e. one has an axiom ∀ x:G, x+x=0 in the group. The rest of the proof basically takes place in this category (the category of elementary 2-groups, if you will). So perhaps the simplest thing to do is just to state the theorem in lean for subsets of a finite abelian group obeying this additional axiom, and not have to deal with vector spaces or finite fields at all.

In particular, it should be rather simple to at least state the PFR conjecture in Lean, even if the proof may take a little longer than that. I guess that would be one very early goal of the project.

[Johan Commelin]

But there isn't much downside to working with $\mathbb{F}_2$-vector spaces either, right?

[Johan Commelin]

Do you use that G is finite in the proof? Because you could drop it from the statement, right? (And just look at the subgroup/subspace generated by A, as first step of the proof.)

[Terence Tao]

Johan Commelin said:

But there isn't much downside to working with $\mathbb{F}_2$-vector spaces either, right?

No. And we will have a future paper working with $\mathbb{F}_p$-vector spaces for other primes p, so that's a case for phrasing things in that language. It seems that mathlib has vector spaces and finite fields pretty well covered.

It's convenient to make G finite for two reasons, one minor and one only moderately significant. The minor one is that it makes it slightly easier to set up the theory of Shannon entropy, as all random variables will take only finitely many values and so we can do everything with Finset.sum instead of tsum or whatever. (Though even when G is infinite, A will still be finite and all the random variables we will consider come from some finite number of operations applied to A, so they will still only take finitely many values within an infinite set.) I guess if one of the goals is to have a satisfactory library of Shannon information theory we would eventually want to generalize beyond the finite case, but at least in the near-term it is a minor convenience.

The more significant reason is that there is a compactness argument used in the proof. At some point (see Section 2 of https://arxiv.org/abs/2311.05762 ) we will use the fact that the set of all probability measures on G is compact, so that a certain continuous functional on those measures is guaranteed to have a minimizer. It is possible to get around this compactness argument by a number of ways (for instance, as you say, you could restrict attention to the group generated by A), but it is a minor convenience to be able to exploit this compactness (this might potentially make the proof Classical though. We do have a variant "algorithmic" proof that has slightly worse bounds but avoids compactness that one might also try to formalize as an additional side project perhaps.). One could perhaps state the main theorem in the finite case (and prove it using completely finitary methods), but then establish as a corollary that it also holds for infinite groups of characteristic 2.

[Frédéric Dupuis]

For what it's worth, formalizing Shannon theory has been on my todo list for a while now, so maybe this project is the push I needed to actually start coding! In any case I'd be happy to contribute.