hom_PFR

Stream: Polynomial Freiman-Ruzsa conjecture

[Sébastien Gouëzel]

I've just improved the bounds in hom_PFR, from 4K^{22} to K^{12}, see https://github.com/teorth/pfr/pull/155. I did this by not using the final statement of PFR, but instead a technical lemma that came out of splitting the blueprint proof of PFR into two parts of comparable length: the first lemma in the formalization (called PFR_conjecture_aux) extracted the exact combinatorial statement one gets from the entropy bounds, and the second part of the proof converted the result of PFR_conjecture_aux to the desired statement PFR_conjecture. In a sense, PFR_conjecture_aux has a more messy statement, but it is more precise, so it's not really surprising it gives better bounds when one applies it.

I see this as a positive outcome of formalization, which forced us to extract the optimal intermediate statement just to avoid too lengthy proofs!

[Sébastien Gouëzel]

I expect it should be possible to improve the constants in the approximate homomorphism form of PFR with the same argument, by the way, but since it's not formalized yet I will not look further into this.

[Eric Rodriguez]

I'll get on it soon Sebastien, hopefully will have some time later today or tomorrow :)

[Sébastien Gouëzel]

No hurry!

[Sébastien Gouëzel]

In fact I've adapted the blueprint to get the stronger bounds also for approx_PFR in https://github.com/teorth/pfr/pull/155, so you might want to have a look there if it's not merged yet when you start on it.

[Terence Tao]

Sebastien Gouezel said:

I've just improved the bounds in hom_PFR, from 4K^{22} to K^{12}, see https://github.com/teorth/pfr/pull/155. I did this by not using the final statement of PFR, but instead a technical lemma that came out of splitting the blueprint proof of PFR into two parts of comparable length: the first lemma in the formalization (called PFR_conjecture_aux) extracted the exact combinatorial statement one gets from the entropy bounds, and the second part of the proof converted the result of PFR_conjecture_aux to the desired statement PFR_conjecture. In a sense, PFR_conjecture_aux has a more messy statement, but it is more precise, so it's not really surprising it gives better bounds when one applies it.

I see this as a positive outcome of formalization, which forced us to extract the optimal intermediate statement just to avoid too lengthy proofs!

Very nice! It's interesting that the formalization is revealing that the canonical formulation of PFR is slightly non-optimized for applications (though, if one doesn't care about specific exponents, it is certainly good enough).