The approximate homomorphism form of PFR

Here we apply PFR to show that almost homomorphisms f from a 2-group to a 2-group often coincide with a (shifted) actual homomorphisms. Here, approximate is in the sense that f(x+y)=f(x)+f(y) is true for a positive proportion of x,y.

Main result

• approx_hom_pfr : If $f: G → G'$ is a map between finite abelian elementary 2-groups such that $f(x+y)=f(x)+f(y)$ for at least $|G|/K$ values, then then there is a homomorphism $\phi: G \to G'$ and a constant $c$ such that $f(x)=\phi(x)+c$ for a substantial set of values.

theorem approx_hom_pfr {G : Type u_1} {G' : Type u_2} [AddCommGroup G] [Fintype G] [AddCommGroup G'] [Fintype G'] [ElementaryAddCommGroup G 2] [ElementaryAddCommGroup G' 2] (f : G → G') (K : ℝ) (hK : K > 0) (hf : ↑(Nat.card ↑{x : G × G | f (x.1 + x.2) = f x.1 + f x.2}) ≥ ↑(Nat.card G) ^ 2 / K) : ∃ (φ : G →+ G') (c : G'), ↑(Nat.card ↑{x : G | f x = φ x + c}) ≥ ↑(Nat.card G) / (2 ^ 172 * K ^ 146)

Let $G, G'$ be finite abelian $2$-groups. Let $f : G \to G'$ be a function, and suppose that there are at least $|G|^2 / K$ pairs $(x,y) \in G^2$ such that $$ f(x+y) = f(x) + f(y).$$ Then there exists a homomorphism $\phi : G \to G'$ and a constant $c \in G'$ such that $f(x) = \phi(x)+c$ for at least $|G| / (2 ^ {172} * K ^ {146})$ values of $x \in G$.