Ben Green's Open Problem 19

References:

• [Gr26] Ben Green's Open Problems
• [FSS20] Fox, Jacob, et al. "Triforce and corners." Mathematical Proceedings of the Cambridge Philosophical Society. Vol. 169. No. 1. Cambridge University Press, 2020.
• [Ma21] Mandache, Matei. "A variant of the Corners theorem." Mathematical Proceedings of the Cambridge Philosophical Society. Vol. 171. No. 3. Cambridge University Press, 2021.
• [Ch11] Chu, Qing. "Multiple recurrence for two commuting transformations." Ergodic Theory and Dynamical Systems 31.3 (2011): 771-792.

def Green19.IsCorner {G : Type u_1} [AddCommGroup G] (A : Finset (G × G)) (x y d : G) : Prop

A corner in $A$ with common difference $d$ [FSS20].

Equations

• Green19.IsCorner A x y d = ((x, y) ∈ A ∧ (x + d, y) ∈ A ∧ (x, y + d) ∈ A)

noncomputable def Green19.S {G : Type u_1} [AddCommGroup G] [Fintype G] (d : G) (A : Finset (G × G)) : Finset (G × G)

From [FSS20]: given $A \subseteq G \times G$ and $d \in G$, let $$S_d(A) = \lbrace (x, y) \in G \times G : (x, y), (x + d, y), (x, y + d) \in A \rbrace$$

Equations

• Green19.S d A = {p : G × G | Green19.IsCorner A p.1 p.2 d}

@[reducible, inline]

abbrev Green19.𝔽₂ (n : ℕ) : Type

The group $G = \mathbb{F}_2^n = (Z/2Z)^n$.

Equations

• Green19.𝔽₂ n = (Fin n → ZMod 2)

def Green19.ValidExponent (c : ℝ) : Prop

True if the given exponent satisfies Green's conditions [Gr26].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Green19.C : ℝ

The infimum of all valid exponents [Gr26].

Equations

• Green19.C = sInf {c : ℝ | Green19.ValidExponent c}

theorem Green19.green_19 : C = 4

What is $C$, the infimum of all exponents $c$ for which the following is true, uniformly for $0 < \alpha < 1$? Suppose that $A \subset \mathbb{F}_2^n \times \mathbb{F}_2^n$ is a set of density $\alpha$. Write $N := 2^n$. Then there is some $d \neq 0$ such that $A$ contains $\gg \alpha^c N^2$ corners $(x,y), (x,y+d), (x+d,y)$.

This question has been resolved by [FSS20], showing that $C = 4$.

theorem Green19.green_19.lower : C ≥ 3.13

[Ma21] showed that $3.13 \leq C$.

theorem Green19.green_19.upper : C ≤ 4

[Ma21] showed that $C \leq 4$.