Green's Open Problem 32

Reference:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [Sh20] Shakan, George. "A Large Gap in a Dilate of a Set." SIAM Journal on Discrete Mathematics 34.4 (2020): 2553-2555.

def Green32.HasGap {p : ℕ} (A : Finset (ZMod p)) (L : ℕ) : Prop

A set $A$ has a gap of length $L$ if there exists $x$ such that $x, x+1, \dots, x+L-1$ are all not in $A$.

Equations

• Green32.HasGap A L = ∃ (x : ZMod p), ∀ i < L, x + ↑i ∉ A

theorem Green32.hasGap_zero {p : ℕ} (A : Finset (ZMod p)) : HasGap A 0

Any set has a gap of length 0 (vacuously true).

theorem Green32.hasGap_empty {p : ℕ} (L : ℕ) : HasGap ∅ L

The empty set has a gap of any length.

theorem Green32.not_hasGap_univ {p : ℕ} [NeZero p] : ¬HasGap Finset.univ 1

The full set in $\mathbb{Z}/p\mathbb{Z}$ has no gap of positive length.

theorem Green32.hasGap_concrete : HasGap {0} 4

Concrete: $\{0\}$ in $\mathbb{Z}/5\mathbb{Z}$ has a gap of length 4 starting at 1.

def Green32.HasLargeGapDilate (ω : ℕ → ℝ) : Prop

The generalized problem: for a prime $p$ and a set $A \subset \mathbb{Z}/p\mathbb{Z}$ of size $\lfloor \omega(p) \rfloor$, is there a dilate of $A$ containing a gap of length $\lfloor 100p/\omega(p) \rfloor$?

Equations

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

theorem Green32.green_32 : True ↔ HasLargeGapDilate fun (p : ℕ) => √↑p

Let $p$ be a prime and let $A \subset \mathbb{Z}/p\mathbb{Z}$ be a set of size $\lfloor \sqrt{p} \rfloor$. Is there a dilate of $A$ containing a gap of length $100\sqrt{p}$?

theorem Green32.green_32.variants.sh20_general (p : ℕ) : Nat.Prime p → ∀ (A : Finset (ZMod p)), 1 < A.card → ∃ (c : (ZMod p)ˣ), HasGap (c • A) ⌊2 * ↑p / ↑A.card - 2⌋₊

[Sh20, Theorem 1] implies a gap of at least $\lfloor 2p/|A| - 2 \rfloor$.

theorem Green32.green_32.variants.sh20_sqrt : ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (A : Finset (ZMod p)), A.card = ⌊√↑p⌋₊ → ∃ (c : (ZMod p)ˣ), HasGap (c • A) (⌊2 * √↑p⌋₊ - 2)

[Sh20] has used the polynomial method to show that this is true with 100 replaced by 2 [Gr24].

Note: More precisely [Sh20, Theorem 1] implies a gap of at least $\lfloor 2p/|A| - 2 \rfloor$. For a set $A$ of size $\lfloor \sqrt{p} \rfloor$, this guarantees a gap of at least $\lfloor 2\sqrt{p} \rfloor - 2$.

theorem Green32.green_32.variants.szemeredi_regime (c : ℝ) : 0 < c ∧ c < 1 → ∀ (ω : ℕ → ℝ), (Asymptotics.IsEquivalent Filter.atTop ω fun (p : ℕ) => c * ↑p) → HasLargeGapDilate ω

In the regime $\omega(p) \sim c p$, this is Szemerédi's theorem [Gr24].

theorem Green32.green_32.variants.dirichlet_regime : ∃ c > 0, ∀ (ω : ℕ → ℝ), (∀ᶠ (p : ℕ) in Filter.atTop, 100 < ω p ∧ ω p ≤ c * Real.log ↑p) → HasLargeGapDilate ω

In the regime $\omega(p) \le c \log p$, this is basically Dirichlet's lower bound for the size of Bohr sets [Gr24].

theorem Green32.green_32.variants.log_regime : True ↔ ∀ (ω : ℕ → ℝ), (Asymptotics.IsEquivalent Filter.atTop ω fun (p : ℕ) => 10 * Real.log ↑p) → HasLargeGapDilate ω

Even what happens in the regime $\omega(p) \sim 10 \log p$ is unclear [Gr24].

def Green32.HasCosetHole {n : ℕ} (A : Finset (Fin n → ZMod 2)) (L : ℕ) : Prop

A set $A$ has a coset hole of size $L$ if there exists a subspace $W$ and a vector $v$ such that the affine space $v + W$ has size at least $L$ and is disjoint from $A$.

Equations

• Green32.HasCosetHole A L = ∃ (W : Submodule (ZMod 2) (Fin n → ZMod 2)) (v : Fin n → ZMod 2), L ≤ Nat.card ↥W ∧ ∀ (w : ↥W), v + ↑w ∉ A

theorem Green32.hasCosetHole_empty (n : ℕ) : HasCosetHole ∅ 0

The empty set in $\mathbb{F}_2^n$ has a coset hole (using the trivial subspace).

theorem Green32.green_32.variants.finite_field : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (Fin n → ZMod 2)), A.card = ⌊√(2 ^ n)⌋₊ → HasCosetHole A ⌊100 * √(2 ^ n)⌋₊

Tom Sanders' finite field variant [Gr24]. If $N = 2^n$ and $A$ is a subset of size $\lfloor \sqrt{N} \rfloor$, then $A^c$ contains a coset of size at least $100\sqrt{N}$ for sufficiently large $n$.