Removing Affine Requirement from Approximate Homomorphism

Stream: Polynomial Freiman-Ruzsa conjecture

[Gareth Ma]

I notice that for the statement for approximate homomorphism, mathematically it translates to

Let $f \colon \mathbb{F}_2^n \to \mathbb{F}_2^m$ satisfy $f(x) + f(y) = f(x + y)$ for $\geq K 2^{2n}$ pairs of $(x, y)$. Then there exists affine linear $\phi \colon \mathbb{F}_2^n \to \mathbb{F}_2^m$ such that $\operatorname{Prob}[f = \phi] \geq 2^{-144}K^{-122}$.

But it is possible to remove the affine requirement. Terence gave a presentation that claims this too. Here is how to deduce the linear version from above. Let $T = \{x \colon f(x) = \phi(x)\}$ above, with $|T| \gg K^C 2^n$. The remainder of the proof is purely analysing $T$.

Claim: There exists $i$ such that $\{x \in T \colon x_i = 1\} \geq |T| / 4$

Proof: It suffices to show $\sum_{i = 1}^n \sum_{x \in T} [x_i = 1] = \sum_{x \in T} H(x) \geq n|T| / 4$, where $H(x)$ is the Hamming weight of $x \in \mathbb{F}_2^n$. Rearranging a bit, it suffices to show $\sum_{x \in T} \left(H(x) - \frac{n}{2}\right) \geq -n|T| / 4$. The $n / 2$ comes from $\mathbb{E}_x H(x) = n / 2$ by the way. Looking at the negative terms we have $\sum_{x \in T} (H(x) - n/2) \geq \sum_{x, H(x) < n / 2} (H(x) - n / 2) = \sum_{h < n / 2} \left(h - \frac{n}{2}\right)\binom{n}{h}$. This is approximately half the sum of a Pascal triangle row, so use Sterling's approximation or something to bound it. For sufficiently large $n$ (should be constant) the desired inequality does hold so we are done.

And once we have this $i$ we can replace the affine function $A\mathbf{x} + b$ by $A\mathbf{x} + b\mathbf{x}_i$. What do you all think about this, should we also formalise this?

(I hope my proof is correct...)

[Terence Tao]

Nice observation. The proof can be made a little cleaner by averaging over arbitrary homomorphisms into F_2 rather than just the coordinate ones, so that one does not need to mess around with Stirling's formula. I updated the blueprint with these new lemmas and am in the process of putting Lean stubs for the four new theorems needed (three lemmas and then the full theorem without the constant term). If anyone wants to claim them, please feel free to say so here; this should be a set of four relatively short formalization tasks.

EDIT: the four lemmas are now stated in Lean, and can be claimed as Lemmas 10.5-Corollary 10.8 in the blueprint: https://teorth.github.io/pfr/blueprint/sect0010.html