Ben Green's Open Problem 37

What is the smallest subset of ℕ containing, for each d = 1, …, N, an arithmetic progression of length k with common difference d?

References:

• Ben Green's Open Problem 37
• Green & Tao, The primes contain arbitrarily long arithmetic progressions (arXiv:math/0404188)

def Green37.IsAPCover (A : Set ℕ) (N k : ℕ) : Prop

A contains an arithmetic progression of length k and common difference d for every d ∈ {1, …, N}.

Equations

• Green37.IsAPCover A N k = ∀ (d : ℕ), 1 ≤ d ∧ d ≤ N → A.ContainsAP k d

noncomputable def Green37.m (N k : ℕ) : ℕ

The minimum size of a subset of ℕ that contains, for each d = 1, …, N, an arithmetic progression of length k with common difference d.

Equations

• Green37.m N k = sInf {m : ℕ | ∃ (A : Finset ℕ), A.card = m ∧ Green37.IsAPCover (↑A) N k}

theorem Green37.green_37 (N k : ℕ) : IsLeast {m : ℕ | ∃ (A : Finset ℕ), A.card = m ∧ IsAPCover (↑A) N k} sorry

Given a natural number N, what is the smallest size of a subset of ℕ that contains, for each d = 1, …, N, an arithmetic progression of length k with common difference d.

theorem Green37.green_37_asymptotic (k : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ↑(m N k) = sorry N

Asymptotic version: determine the asymptotic behavior of m(N, k) as N grows. The solver should determine what function f : ℕ → ℝ eventually equals (fun N ↦ (m N k : ℝ)).

theorem Green37.green_37_theta (k : ℕ) : (fun (N : ℕ) => ↑(m N k)) =Θ[Filter.atTop] sorry

Determine the asymptotic equivalence class (theta) of m(N, k).

theorem Green37.green_37_bigO (k : ℕ) : (fun (N : ℕ) => ↑(m N k)) =O[Filter.atTop] sorry

Determine an upper bound (big O) for m(N, k).

theorem Green37.green_37_littleO (k : ℕ) : (fun (N : ℕ) => ↑(m N k)) =o[Filter.atTop] sorry

Determine a strict upper bound (little o) for m(N, k).