PFR extensions

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Just a heads up that over the weekend I will try to extend the blueprint to cover two extensions of PFR:

1. An application of PFR to approximate homomorphisms (a variant of the application of PFR to homomorphisms that we already have);
2. The recent refinement of the argument given by Jyun-Jie Liao that improves the exponent in PFR from 12 to 11 (see https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/#comment-682353 ).

These are relatively minor modifications of the existing arguments (except that part 1 uses the Balog-Szemeredi Lemma as a black box, and so would have to merge with @Yaël Dillies and @Bhavik Mehta's project to formalize that lemma). I have just pushed a preliminary version of #1 and will keep working on #1 and #2 over the weekend.

In about a week, my coauthors and I will also be ready to release our preprint for PFR in the odd torsion case, and I will also work on extending the blueprint to cover this case also (though this is a more substantial extension). Finally, @Thomas Bloom has volunteered to write a blueprint on an application of PFR to a weak Freiman-Ruzsa theorem over the integers.

I am then hoping to get these extensions worked out slowly over the next few weeks, possibly also testing experimental Blueprint features along the way. I don't anticipate the pace of this second phase of PFR being anywhere near has hectic as the first phase (at its height we were receiving multiple pull requests every hour), but there should still be a steady pace of progress, now that we have some experience with the workflow.

EDIT: Now that things are starting up again, I am reviving the "Outstanding tasks" thread. This is version 6.0; the previous version can be found here.

A. Existing claims

1. @Yaël Dillies is gradually porting various stable PFR files over to Mathlib. Expect frequent Mathlib bumps during this process. It should be possible to work on extensions concurrently with this porting.
2. @Paul Lezeau has formalized Additive energy and Cauchy-Schwarz bound, and claims the proof of the latter.
3. @Yaël Dillies and @Bhavik Mehta claim the proof of Balog-Szemeredi-Gowers
4. @Thomas Bloom has nearly finished the writing of a blueprint for "weak PFR over Z".
5. @Terence Tao has completed the writing of a blueprint for "improved exponent for PFR"

B. Outstanding proof formalization tasks:

1. Approximate homomorphism form of PFR. This is a variant of the already-proven Homomorphism form of PFR and should be relatively straightforward to prove by an adaptation of that proof.
2. Constructing good variables, I' This should be a slight modification of Constructing good variables, I.
3. Constructing good variables, II' This should be a routine variant of Constructing good variables, II. Awaits C.3.
4. Constructing good variables, III' Should follow from preceding result and the arguments used to prove tau decrement. Awaits C.3, C.4.
5. General inequality Mostly taking linear combinations of other inequalities. There is one tricky new thing, which is to show that a certain conditioned random variable has identical distribution to the sum of two other conditioned random variables.
6. Bound on distance differences Mostly taking linear combinations of other inequalities. A slight refactoring of Second estimate will be needed. Awaits C.6.
7. Improved tau decrement A straightforward variant of (the second half of the proof of) tau decrement. Awaits C.4, C.6.
8. Entropy form of PFR' Straightforward modification of Entropy form of PFR.
9. Improved PFR Straightforward modification of PFR, with one additional limiting argument needed to send eta to 1/8.

C. Outstanding documentation/blueprint/examples/statement formalization tasks:

1. Approximate homomorphism form of PFR. A statement is given in the blueprint, It requires some constants from BSG that are not yet determined, but we have put placeholder values in the Lean code for now. Established by @Terence Tao
2. Constructing good variables, I' Should just be a matter of following the blueprint. Established by @Terence Tao
3. Constructing good variables, II' Here the sum involves 12 terms, one may need to think about the cleanest way to express this formula.
4. Constructing good variables, III' Similar issue to preceding.
5. General inequality Should be straightforward to state. Established by @Terence Tao
6. Bound on distance differences Involves the sum of 12 terms appearing in C.3, but should otherwise be simple to state.
7. Add an example showcasing Approximate homomorphism form of PFR to the examples.lean file. Established by @Terence Tao

D. Outstanding administrative tasks: No unclaimed tasks currently.

[Paul Lezeau]

Hi! Would it be possible to claim lemma 9.2?

[Paul Lezeau]

If the statement hasn't been formalized yet I'm happy to do that too

[Terence Tao]

Paul Lezeau said:

Hi! Would it be possible to claim lemma 9.2?

Sure! You will also have to formalize Definition 9.1 as well of course, but that should not be too difficult. I just created a stub file ApproximateHomomorphism.lean (using the brand new proof_wanted feature) to contain all the Section 9 material. I guess the "outstanding tasks" board will need to be revived, so I will edit my previous announcement next to get that set up.

[Yaël Dillies]

Just mentioning that docs#Finset.additiveEnergy already exists.

[Paul Lezeau]

Just opened a PR with the statement and local notation for additive energy

[Paul Lezeau]

(deleted)

[Terence Tao]

Paul Lezeau said:

Just opened a PR with the statement and local notation for additive energy

Great! I've now also taken the liberty of making a tentative formalization of BSG (using our new additive energy notation) in order to unblock the various tasks around "approximate homomorphism form of PFR". In particular I put in some placeholder values for the constants that will show up in these theorems, though they may be subject to change later once BSG actually gets formalized.

[Terence Tao]

Another update: in the previous build, η was hardcoded to be 1/9. In preparation for the extension in which we lower the PFR constant from 12 to 11, I have moved η into the reference package p and it is now permitted to range between 0 and 1/8 exclusive, though some key steps in our previous argument only apply when η = 1/9. I have refactored the proofs accordingly and it looks like everything compiles, so I should be ready to roll out some stubs for the constant improvement and add to the outstanding tasks.

[Terence Tao]

OK, the argument for lowering the 12 exponent to 11 is now fully written up in the blueprint, and stubs to code are in the lean files, and now there are a dozen or so additional tasks outstanding to complete (but the formalizations ones should be relatively quick).

[Thomas Bloom]

Update: I have written up the lemmas and proofs of deducing weak integer PFR, now I just need to turn it into a blueprint formatting and add the appropriate references and labels. I need to stop for today, but hopefully will finish the blueprint conversion and push it tomorrow morning.