feat(GreensOpenProblems): 51 (#4283)

# Description

> Suppose that $A \subset 𝔽_2^n$ is a set of density $\alpha$. What is
the largest size of coset guaranteed to be contained in $2A$?
>
[[Source](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.51)]

- Closes #1656
- Includes additional variants discussed by Green:
    - Best known bounds
    - Limit case at $\alpha \to \frac{1}{2}^{-}$
    - Arithmetic formulation
- 🤖 Initial draft by **Gemini 3.1 Pro**, then adjusted for
style/modularity, and to fix edge conditions.

### References
-
[[Gr24]](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.51)
Green, Ben. *Green's Open Problems*.
- [[Gr13]](http://people.maths.ox.ac.uk/greenbj/papers/rkp.pdf) Green,
Ben J. *Restriction and Kakeya phenomena* (Notes from a 2003 course).
- [[Sa11]](https://arxiv.org/pdf/1003.5649) Sanders, Tom. "Green's
sumset problem at density one half." *Acta Arithmetica* 146.1 (2011):
91-101.
- [[Gr02]](https://link.springer.com/article/10.1007/s00039-002-8258-4)
Green, Ben. "Arithmetic progressions in sumsets." *Geometric &
Functional Analysis GAFA* 12.3 (2002): 584-597.
- [[Ruz91]](https://matwbn.icm.edu.pl/ksiazki/aa/aa60/aa6027.pdf) Ruzsa,
Imre Z. "Arithmetic progressions in sumsets." *Acta Arithmetica* 60.2
(1991): 191-202.

# Testing
:white_check_mark: Builds fine.
```shell
$ lake build FormalConjectures/GreensOpenProblems/51.lean 
Build completed successfully (8030 jobs).
```

Author: jeangud

FormalConjectures/GreensOpenProblems/51.lean

@@ -0,0 +1,112 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Green's Open Problem 51
+
+*References:*
+- [Gr24] [Green's Open Problems](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.51)
+- [Gr13] B. J. Green, Restriction and Kakeya phenomena, notes from a 2003 course.
+  Available at http://people.maths.ox.ac.uk/greenbj/papers/rkp.pdf
+- [Sa11] Sanders, Tom. "Green's sumset problem at density one half."
+  Acta Arithmetica 146.1 (2011): 91-101.
+- [Gr02] Green, Ben. "Arithmetic progressions in sumsets."
+  Geometric & Functional Analysis GAFA 12.3 (2002): 584-597.
+- [Ruz91] Ruzsa, Imre Z. "Arithmetic progressions in sumsets."
+  Acta Arithmetica 60.2 (1991): 191-202.
+-/
+
+open Filter Real
+open scoped Pointwise
+
+namespace Green51
+
+/-- The group $G = \mathbb{F}_2^n = (Z/2Z)^n$. -/
+abbrev 𝔽₂ (n : ℕ) := Fin n → ZMod 2
+
+/-- The maximum dimension of a coset contained in the set $A$. -/
+noncomputable def maxCosetDim (n : ℕ) (A : Set (𝔽₂ n)) : ℕ :=
+  sSup { d | ∃ (W : Submodule (ZMod 2) (𝔽₂ n)) (v : 𝔽₂ n),
+    v +ᵥ (W : Set (𝔽₂ n)) ⊆ A ∧
+    Module.finrank (ZMod 2) W = d }
+
+/-- The largest dimension of a coset guaranteed to be contained in $2A$ for $A \subseteq \mathbb{F}_2^n$ with density $\alpha$. -/
+noncomputable def guaranteedMaxCosetDim (n : ℕ) (α : ℝ) : ℕ :=
+  sInf { maxCosetDim n ↑(A + A) | (A : Finset (𝔽₂ n)) (_h : A.dens ≥ α) }
+
+/--
+Suppose that $A \subset \mathbb{F}_2^n$ is a set of density $\alpha$. What is the largest size of coset
+guaranteed to be contained in $2A$?
+
+We phrase this by asking for the exact function $F(\alpha, n)$ giving the maximum dimension
+of a guaranteed coset.
+-/
+@[category research open, AMS 5 11]
+theorem green_51 : answer(sorry) = guaranteedMaxCosetDim := by
+  sorry
+
+/-- It is known that $A + A$ must contain a coset of dimension $\gg_\alpha n$ [Gr13]. -/
+@[category research solved, AMS 5 11]
+theorem green_51.lower :
+    ∀ (α : ℝ), 0 < α → α ≤ 1 →
+    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, c * (n : ℝ) ≤ guaranteedMaxCosetDim n α := by
+  sorry
+
+/-- It is known that $A + A$ need not contain a coset of dimension $n - \sqrt{n}$ [Gr13]. -/
+@[category research solved, AMS 5 11]
+theorem green_51.upper :
+    ∃ α > 0, α ≤ 1 ∧ ∀ᶠ (n : ℕ) in atTop, (guaranteedMaxCosetDim n α : ℝ) < (n : ℝ) - sqrt n := by
+  sorry
+
+/--
+Suppose that $A \subset \mathbb{F}_2^n$ has density $\alpha > 1/2 - C/\sqrt{n}$.
+Does $A + A$ contain a subspace of co-dimension $O_C(1)$? [Sa11, Question 5.1]
+-/
+@[category research open, AMS 5 11]
+theorem green_51.one_half :
+    answer(sorry) ↔ ∀ (k : ℝ), 0 < k →
+      ∃ (c : ℕ), ∀ᶠ (n : ℕ) in atTop,
+        ∀ (α : ℝ), α > (1/2 : ℝ) - k / sqrt (n : ℝ) → α ≤ 1 →
+          n ≤ guaranteedMaxCosetDim n α + c := by
+  sorry
+
+/--
+The largest length of an arithmetic progression guaranteed to be contained in $A+A$
+for $A \subseteq \{1, \dots, N\}$ with density $\alpha$.
+-/
+noncomputable def guaranteedMaxAPLength (N : ℕ) (α : ℝ) : ℕ :=
+  sInf { sSup {l : ℕ | ∃ s ⊆ (A + A : Set ℕ), s.IsAPOfLength (l : ℕ∞)}
+       | (A : Finset ℕ) (_hA : A ⊆ Finset.Icc 1 N) (_h : α * (N : ℝ) ≤ A.card) }
+
+/-- It is known that $A + A$ must contain an arithmetic progression of length $\sim \exp(c (\log N)^{1/2})$ [Gr02]. -/
+@[category research solved, AMS 5 11]
+theorem green_51.lower_ap :
+    ∀ (α : ℝ), 0 < α → α ≤ 1 →
+      ∃ c > 0, ∀ᶠ (N : ℕ) in atTop,
+        exp (c * log (N : ℝ) ^ (1/2 : ℝ)) ≤ guaranteedMaxAPLength N α := by
+  sorry
+
+/-- It is known that $A + A$ need not contain an arithmetic progression of length $\sim \exp(c (\log N)^{2/3})$ [Ruz91]. -/
+@[category research solved, AMS 5 11]
+theorem green_51.upper_ap :
+    ∀ (α : ℝ), 0 < α → α < 1/2 →
+      ∃ c > 0, ∀ᶠ (N : ℕ) in atTop,
+        guaranteedMaxAPLength N α ≤ exp (c * log (N : ℝ) ^ (2/3 : ℝ)) := by
+  sorry
+
+end Green51