Weak PFR over the integers

Stream: Polynomial Freiman-Ruzsa conjecture

[Thomas Bloom]

I have just (I hope, although I don't fully understand git) pushed/pulled the new additions to the blueprint for deducing 'weak PFR over the integers'. Everything should compile fine as far as I can see, but sorry if there are any lingering bugs.

This deduction is exactly as proved by Green, Manners, and Tao in https://arxiv.org/pdf/2306.13403.pdf - I only made a couple of obvious simplifications given the actual form of PFR proven. Any mistakes are, of course, entirely due to me. If anyone is confused by a proof, feels that something is wrong or missing, then please check the original paper and/or post in this thread.

[Yaël Dillies]

Merged the PR!

[Yaël Dillies]

There are a few issues with the new items. Fixing them now.

[Yaël Dillies]

Update: Everything is now visible on the blueprint!

[Sebastien Gouezel]

I'd like to claim ImprovedPFR if no-one is working on it.