/-
Copyright 2025 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 FormalConjecturesUtilBen Green's Open Problem 50
Suppose that $A \subset \mathbb{F}_2^n$ is a set of density $\alpha$. Does $10A$ contain a coset of some subspace of dimension at least $n - O(\log(1/\alpha))$?
Here $kA$ denotes the $k$-fold iterated sumset, i.e., the set of all sums of $k$ elements from $A$
(with repetition allowed). In Mathlib, this is denoted k • A using pointwise scalar
multiplication on sets.
open scoped Pointwise
namespace Green50
Let $A \subset \mathbb{F}_2^n$ be a set of density $\alpha > 0$. Does $10A$ contain a coset of some subspace of dimension at least $n - O(\log(1/\alpha))$?
More precisely: does there exist an absolute constant $C > 0$ such that for all $n \geq 1$ and all nonempty $A \subseteq \mathbb{F}_2^n$ with density $\alpha > 0$, the sumset $10A$ contains a coset of some subspace of dimension at least $n - C \log_2(1/\alpha)$?
The sumset $10A$ is defined as ${a_1 + a_2 + \cdots + a_{10} : a_i \in A}$, using the pointwise
scalar multiplication notation 10 • A where • denotes the iterated addition of a set.
Note: We model $\mathbb{F}_2^n$ as Fin n → ZMod 2, which is an $n$-dimensional vector space
over $\mathbb{F}_2$.
@[category research open, AMS 5 11]
theorem green_50 : answer(sorry) ↔
∃ C > (0 : ℝ), ∀ n : ℕ, ∀ A : Finset (𝔽₂ n),
A.Nonempty →
let α : ℝ := A.dens
∃ (W : Submodule (ZMod 2) (𝔽₂ n)) (v : 𝔽₂ n),
v +ᵥ (W : Set (𝔽₂ n)) ⊆ ↑(10 • A) ∧
(n : ℝ) - C * Real.logb 2 (1 / α) ≤ Module.finrank (ZMod 2) W := ⊢ True ↔
∃ C > 0,
∀ (n : ℕ) (A : Finset (𝔽₂ n)),
A.Nonempty →
let α := ↑A.dens;
∃ W v, v +ᵥ ↑W ⊆ ↑(10 • A) ∧ ↑n - C * Real.logb 2 (1 / α) ≤ ↑(Module.finrank (ZMod 2) ↥W)
All goals completed! 🐙
end Green50