Approximate homomorphism version of PFR

DefinitionAdditive energy#

If \(G\) is a finite additive group and \(A\) is a subset of \(G\), the additive energy \(E(A)\) of \(A\) is the normalized count

\[ E(A) := \frac{|\{(a_1,a_2,a_3,a_4) \in A^4 : a_1+a_2 = a_3+a_4\}|}{|G|^3}. \]

The normalization by \(|G|^3\) is the convention of Finset.addEnergy', and every statement in this chapter that mentions \(E(A)\) uses it.

Lean

Formalized as Finset.addEnergy'.

Sources
LeanFinset.addEnergy'
Used by 2
Used byBalog–Szemerédi–Gowers lemma · Cauchy–Schwarz bound

LemmaCauchy–Schwarz bound#

If \(G\) is a finite additive group and \(A,B\) are subsets of \(G\), then

\[ \left( \frac{|\{ (a,a') \in A \times A: a+a' \in B \}|}{|G|^2} \right)^2 \leq \frac{|B|}{|G|}\, E(A). \]

The left-hand side is the square of the density of a subset of \(G \times G\), and the right-hand side involves the density of a subset of \(G\).

Proof

If \(B\) is empty then the claim is trivial (with the Lean convention \(0/0\)), so without loss of generality \(B\) is non-empty. We can rewrite

\[ |\{ (a,a') \in A \times A: a+a' \in B \}| = \sum_{b \in B} r(b) \]

where \(r: G \to \mathbb{N}\) is the counting function

\[ r(b) := |\{ (a,a') \in A \times A: a+a' = b \}|. \]

From double counting we have

\[ \sum_{b \in G} r(b)^2 = |G|^3 E(A). \]

The Cauchy–Schwarz inequality then gives

\[ \Bigl( \sum_{b \in B} r(b) \Bigr)^2 \leq |B| \sum_{b \in B} r(b)^2 \leq |B| \sum_{b \in G} r(b)^2 = |B|\, |G|^3 E(A), \]

and the claim follows on dividing both sides by \(|G|^4\).

Lean

Formalized as Finset.card_sq_le_card_mul_addEnergy'.

Sources
LeanFinset.card_sq_le_card_mul_addEnergy'
Uses 1 · Used by 1
Statement usesAdditive energy
Used byApproximate homomorphism form of PFR

LemmaBalog–Szemerédi–Gowers lemma#

Let \(G\) be a finite abelian group, and let \(A\) be a non-empty subset of \(G\) with \(E(A) \geq \frac{1}{K} \left( \frac{|A|}{|G|} \right)^3\) for some \(K \geq 1\). Then there is a subset \(A'\) of \(A\) with \(|A'| \geq |A| / (C_1 K^{C_2})\) and \(|A'-A'| \leq C_3 K^{C_4} |A|\), where

\[ C_1 = 2^4, C_2 = 1, C_3 = 2^{10}, C_4 = 5. \]

The Lean statement gives the two conclusions as inequalities between densities; these are equivalent to the ones above, the common factor \(|G|\) cancelling.

Proof

See https://terrytao.files.wordpress.com/2024/01/simplebsg.pdf.

Lean

Formalized as BSG_self.

Sources
LeanBSG_self
Uses 1 · Used by 1
Statement usesAdditive energy
Used byApproximate homomorphism form of PFR

TheoremApproximate homomorphism form of PFR#

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 ^ {144} * K ^ {122})\) values of \(x \in G\).

Proof

Consider the graph \(A \subset G \times G'\) defined by

\[ A := \{ (x,f(x)): x \in G \}. \]

Clearly, \(|A| = |G|\). By hypothesis, we have \(a+a' \in A\) for at least \(|A|^2/K\) pairs \((a,a') \in A^2\). By Cauchy–Schwarz bound, this implies that \(E(A) \geq \frac{1}{K^2} \left( \frac{|A|}{|G \times G'|} \right)^3\). Applying Balog–Szemerédi–Gowers lemma, we conclude that there exists a subset \(A' \subset A\) with \(|A'| \geq |A|/C_1 K^{2C_2}\) and \(|A'+A'| \leq C_1C_3 K^{2(C_2+C_4)} |A'|\). Applying Corollary pfr-9-aux', we may find a subspace \(H \subset G \times G'\) such that \(|H| / |A'| \in [L^{-8}, L^{8}]\) and a subset \(c\) of cardinality at most \(L^5 |A'|^{1/2} / |H|^{1/2}\) such that \(A' \subseteq c + H\), where \(L = C_1C_3 K^{2(C_2+C_4)}\). If we let \(H_0,H_1\) be as in Goursat type theorem, this implies on taking projections the projection of \(A'\) to \(G\) is covered by at most \(|c|\) translates of \(H_0\). This implies that

\[ |c| |H_0| \geq |A'|; \]

since \(|H_0| |H_1| = |H|\), we conclude that

\[ |H_1| \leq |c| |H|/|A'|. \]

By hypothesis, \(A'\) is covered by at most \(|c|\) translates of \(H\), and hence by at most \(|c| |H_1|\) translates of \(\{ (x,\phi(x)): x \in G \}\). As \(\phi\) is a homomorphism, each such translate can be written in the form \(\{ (x,\phi(x)+c): x \in G \}\) for some \(c \in G'\). The number of translates is bounded by

\[ |c|^2 \frac{|H|}{|A'|} \leq \left(L^5 \frac{|A'|^{1/2}}{|H|^{1/2}}\right)^2 \frac{|H|}{|A'|} = L^{10}. \]

By the pigeonhole principle, one of these translates must then contain at least \(|A'|/L^{10} \geq |G| / (C_1C_3 K^{2(C_2+C_4)})^{10} (C_1 K^{2C_2})\) elements of \(A'\) (and hence of \(A\)), and the claim follows.

Lean

Formalized as approx_hom_pfr.

Sources
Leanapprox_hom_pfr
Uses 4 · Used by 1
Proof usesGoursat type theorem · Cauchy–Schwarz bound · Balog–Szemerédi–Gowers lemma · pfr-9-aux'
Used byApproximate homomorphism form of PFR, no constant term

With a bit more effort, we can remove the constant term \(c\), at the cost of reducing the set of agreement slightly. We need some preliminary lemmas.

LemmaDuality#

Let \(G\) be a finite abelian \(2\)-group. Then the finite abelian \(2\)-group \(\mathrm{Hom}(G,\mathbb{Z}/2\mathbb{Z})\) of homomorphisms from \(G\) to \(\mathbb{Z}/2\mathbb{Z}\) has the same order as \(G\).

Proof

By the classification of finite abelian groups, \(G\) is isomorphic to \((\mathbb{Z}/2\mathbb{Z})^n\). Then \(\mathrm{Hom}(G,\mathbb{Z}/2\mathbb{Z})\) is isomorphic to \((\mathbb{Z}/2\mathbb{Z})^n\) as well, and hence has the same order.

Lean

Formalized as card_of_dual.

Sources
Leancard_of_dual
Used by 2
Used byCounting · Slicing

LemmaCounting#

Let \(G\) be a finite abelian \(2\)-group, and let \(x \in G\) be non-zero. Then there are \(|G|/2\) homomorphisms \(\phi: G \to \mathbb{Z}/2\mathbb{Z}\) such that \(\phi(x) = 1\).

Proof

The map \(\phi \mapsto \phi(x)\) is a homomorphism from \(\mathrm{Hom}(G,\mathbb{Z}/2\mathbb{Z})\) to \(\mathbb{Z}/2\mathbb{Z}\), and by Lemma Duality the kernel has order equal to the order of \(G / \{0,x\}\), which is \(|G|/2\). Then the preimage of \(1\) must also be of order \(|G|/2\).

Lean

Formalized as card_of_dual_constrained.

Sources
Leancard_of_dual_constrained
Uses 1 · Used by 1
Proof usesDuality
Used bySlicing

LemmaSlicing#

Let \(G\) be a finite abelian \(2\)-group, and let \(A\) be a subset of \(G\). Then there exists a homomorphism \(\phi: G \to \mathbb{Z}/2\mathbb{Z}\) such that \(|A \cap \phi^{-1}(1)| \geq (|A|-1)/2\).

Proof

We have

\[ \sum_{\phi \in \mathrm{Hom}(G,\mathbb{Z}/2\mathbb{Z})} |A \cap \phi^{-1}(1)| = \sum_{x \in A} |\{ \phi \in \mathrm{Hom}(G,\mathbb{Z}/2\mathbb{Z}): \phi(x) = 1 \}| \]
\[ \geq (|A|-1) |G|/2 \]

thanks to Lemma Counting. The claim now follows from Lemma Duality and the pigeonhole principle.

Lean

Formalized as card_of_slice.

Sources
Leancard_of_slice
Uses 2 · Used by 1
Proof usesDuality · Counting
Used byApproximate homomorphism form of PFR, no constant term

CorollaryApproximate homomorphism form of PFR, no constant term#

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'\) such that \(f(x) = \phi''(x)\) for at least \((|G| / (2 ^ {144} * K ^ {122}) - 1)/2\) values of \(x \in G\).

Proof

By Theorem Approximate homomorphism form of PFR, there exists a homomorphism \(\phi: G \to G'\) and a constant \(c \in G'\) such that the set \(A := \{ x \in G: f(x) = \phi(x) + c\}\) has cardinality at least \(|G| / (2 ^ {144} * K ^ {122})\). By Lemma Slicing, there exists a homomorphism \(\phi': G \to \mathbb{Z}/2\mathbb{Z}\) such that

\[ |A \cap \phi'^{-1}(1)| \geq (|A|-1)/2 \geq (|G| / (2 ^ {144} * K ^ {122}) - 1)/2. \]

Then the claim follows by taking \(\phi'' = \phi + \phi' \bullet c\) (where we view \(G'\) as a \(\mathbb{Z}/2\mathbb{Z}\)-module).

Lean

Formalized as approx_hom_pfr'.

Sources
Leanapprox_hom_pfr'
Uses 2
Proof usesApproximate homomorphism form of PFR · Slicing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.