Improved PFR

Stream: Polynomial Freiman-Ruzsa conjecture

[Sebastien Gouezel]

@Terence Tao , I'm confused by the proof of the general inequality in the blueprint.

First, on line https://github.com/teorth/pfr/blob/a7a1dee407f3290a6b7df07df60c9910f992be63/blueprint/src/chapter/improved_exponent.tex#L101, I get a bound with H[X3 + X4] instead of H[X1 + X3], which is probably just a typo. Then, when I try to unify the bounds coming from the two different arguments, we have on the one hand d[X_1+X_2;X_3+X_4] coming from the first bit, and on the other hand d[X_1|X_1+X_3;X_2|X_2+X_4] coming from the second bit. They don't seem tailored to an application of the fibring identity https://github.com/teorth/pfr/blob/a7a1dee407f3290a6b7df07df60c9910f992be63/blueprint/src/chapter/fibring.tex#L49, as for this one would rather need d[X_1|X_1+X_2;X_3|X_3+X_4] say. Of course, this shouldn't create any issue then, because we sum over all permutations so we should get all the terms we want, but for now I don't see how to prove the general inequality as stated. Could you add a few details to clarify things?

[Terence Tao]

Oof, you are right, there are typos, but as you say in the end the modifications do seem to cancel each other out after symmetrizing. (This is one place where formalization really shines over pen and paper!) I was admittedly sloppy with the calculations of these lower order terms because I knew from experience that the symmetrization would deal with them anyway, but of course one needs to get it right.

I just pushed an update to the blueprint to address these, it should appear in like 15 mins.

[Sebastien Gouezel]

Thanks!