feat(GreensOpenProblems): 19

[jeangud]

Description

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)$.

• Closes Green's Open Problems #19 #1554
• Note: original PDF says $A \subset \mathbb{F}_2^n$, which we understand as $A \subset \mathbb{F}_2^n \times \mathbb{F}_2^n$ for the corners $\in A$ to make sense.
• Using some helpful notation from [FSS20] and [Ma21].
• Solved as $C = 4$.
• Added previous best known bounds $3.13 \leq C \leq 4$ as intermediate proofs.

Testing

• Builds successfully

$ lake build FormalConjectures/GreensOpenProblems/19.lean 
Build completed successfully.