Green's Open Problem 25

References:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [ESS89] Erdős, Pál, András Sárközy, and V. T. Sós. "On a conjecture of Roth and some related problems I." Irregularities of partitions. Berlin, Heidelberg: Springer Berlin Heidelberg, 1989. 47-59.
• [Ru04] Ruzsa, Imre Z. "A problem on restricted sumsets." CONTEMPORARY MATHEMATICS 342 (2004): 245-248.

def Green25.Property25 (k N : ℕ) : Prop

For which values of $k$ is the following true: whenever we partition $[N] = A_1 \cup \dots \cup A_k$, $\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| \geq \frac{1}{10} N$?

Equations

• Green25.Property25 k N = (1 ≤ k ∧ k ≤ N ∧ ∀ (P : Finpartition (Finset.Icc 1 N)), P.parts.card = k → 10 * (P.parts.biUnion Finset.restrictedSumset).card ≥ N)

noncomputable def Green25.bestLower (N : ℕ) : ℝ

The best-known lower bound [ESS89].

Equations

• Green25.bestLower N = Real.log (Real.log ↑N)

noncomputable def Green25.bestUpper (N : ℕ) : ℝ

The best-known upper bound [ESS89].

Equations

• Green25.bestUpper N = ↑N / Real.log ↑N

theorem Green25.green_25 : {k : ℕ → ℕ | ∀ᶠ (N : ℕ) in Filter.atTop, Property25 (k N) N} = sorry

For which values of $k$ is the following true: whenever we partition $[N] = A_1 \cup \dots \cup A_k$, $\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| \geq \frac{1}{10} N$?

theorem Green25.green_25.upper : have ans := sorry; (∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ ans N ∧ ans N ≤ N) ∧ (fun (N : ℕ) => ↑(ans N)) =o[Filter.atTop] bestUpper ∧ ¬∀ᶠ (N : ℕ) in Filter.atTop, Property25 (ans N) N

We conjecture that the best-known upper bound can be lowered.

theorem Green25.green_25.lower : have ans := sorry; bestLower =o[Filter.atTop] ans ∧ (∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ ans N ∧ ans N ≤ ↑N) ∧ ∀ (k : ℕ → ℕ), (∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ k N ∧ k N ≤ N) ∧ (fun (N : ℕ) => ↑(k N)) =O[Filter.atTop] ans → ∀ᶠ (N : ℕ) in Filter.atTop, Property25 (k N) N

We conjecture that the best-known lower bound can be raised.

theorem Green25.green_25.variants.lower_ess89 (k : ℕ → ℕ) : (∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ k N ∧ k N ≤ N) ∧ (fun (N : ℕ) => ↑(k N)) =o[Filter.atTop] bestLower → ∀ᶠ (N : ℕ) in Filter.atTop, Property25 (k N) N

For $k \ll \log \log N$, this is true [Gr24].

NOTE: [ESS89] derive a precise constant for which this is true, but $\ll$ would imply that it works for any constant. We thus prefer a little-o statement.

theorem Green25.green_25.variants.upper_ess89 : ∃ (k : ℕ → ℕ), (∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ k N ∧ k N ≤ N) ∧ (fun (N : ℕ) => ↑(k N)) =Θ[Filter.atTop] bestUpper ∧ ¬∀ᶠ (N : ℕ) in Filter.atTop, Property25 (k N) N

For $k \gg N / \log N$, it need not be true [Gr24].

We formalize by enforcing a $N / \log N$ growth rate on $k(N)$. This avoids cases like $k(N) = N$ or $N-1$, which produce trivial counter examples with singletons and thus empty restricted sumsets.

theorem Green25.green_25.variants.upper_ess89_trivial : ∃ (k : ℕ → ℕ), (∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ k N ∧ k N ≤ N) ∧ (bestUpper =O[Filter.atTop] fun (N : ℕ) => ↑(k N)) ∧ ¬∀ᶠ (N : ℕ) in Filter.atTop, Property25 (k N) N

For $k \gg N / \log N$, it need not be true [Gr24].

In this version, cases like $k(N) = N$ or $N-1$ can produce trivial counter examples.