Ben Green's Open Problem 18

Reference:

• [Gr26] Ben Green's Open Problem 18
• [Au16] Austin, Tim. "Ajtai–Szemerédi theorems over quasirandom groups." Recent trends in combinatorics. Cham: Springer International Publishing, 2016. 453-484.
• [So13] Solymosi, Jozsef. "Roth-type theorems in finite groups." European Journal of Combinatorics 34.8 (2013): 1454-1458.
• [Go01] Gowers, William T. "A new proof of Szemerédi's theorem." Geometric & Functional Analysis GAFA 11.3 (2001): 465-588.

def Green18.numNaiveCorners {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (A : Finset (G × G)) : ℕ

The number of triples $(x, y, g)$ in $G^3$ such that $g \neq e$, and $(x, y), (gx, y), (x, gy)$ are all in $A$. These are called "naive corners" by [Au16].

Note: the shortened formulation from [Gr26] does not mention $g \neq e$, but this is the original statement from [Au16], which ensure non-trivial corners. Note however that [Au16] use more generally compact groups and not just finite discrete groups.

Equations

• Green18.numNaiveCorners A = {x : G × G × G | match x with | (x, y, g) => g ≠ 1 ∧ (x, y) ∈ A ∧ (g * x, y) ∈ A ∧ (x, g * y) ∈ A}.card

theorem Green18.green_18 : sorry ↔ ∀ α > 0, ∃ c > 0, ∃ (m₀ : ℕ), ∀ (G : Type u_1) [inst : Group G] [inst_1 : Fintype G] [inst_2 : DecidableEq G] (A : Finset (G × G)), Fintype.card G ≥ m₀ → ↑A.card ≥ α * ↑(Fintype.card G) ^ 2 → ↑(numNaiveCorners A) ≥ c * ↑(Fintype.card G) ^ 3

Suppose that $G$ is a finite group, and let $A \subset G \times G$ be a subset of density $\alpha$. Is it true that there are $\gg_\alpha |G|^3$ triples $x, y, g$ such that $(x, y), (gx, y), (x, gy)$ all lie in $A$?

Note: A is taken as $\alpha$-dense, i.e. $|A| \ge \alpha |G|^2$ [Au16, Question 2]

def Green18.numBmzCorners {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (A : Finset (G × G)) : ℕ

The number of triples $(x, y, g)$ in $G^3$ such that $g \neq e$, and $(x, y), (xg, y), (x, gy)$ are all in $A$. These are called "BMZ corners" by [Au16].

Equations

• Green18.numBmzCorners A = {x : G × G × G | match x with | (x, y, g) => g ≠ 1 ∧ (x, y) ∈ A ∧ (x * g, y) ∈ A ∧ (x, g * y) ∈ A}.card

theorem Green18.green_18.bmz_corners (α : ℝ) : α > 0 → ∃ c > 0, ∃ (m₀ : ℕ), ∀ (G : Type u_1) [inst : Group G] [inst_1 : Fintype G] [inst_2 : DecidableEq G] (A : Finset (G × G)), Fintype.card G ≥ m₀ → ↑A.card ≥ α * ↑(Fintype.card G) ^ 2 → ↑(numBmzCorners A) ≥ c * ↑(Fintype.card G) ^ 3

[So13] proved this is true for "BMZ corners". Follows from the proof of Theorem 2.1, p.1456-1457.