Erdős Problem 160

Reference: erdosproblems.com/160

noncomputable def Erdos160.erdos_160.h (n : ℕ) : ℕ

Let $h(n)$ be the smallest $k$ such that $\{1,\ldots,n\}$ can be coloured with $k$ colours so that every four-term arithmetic progression must contain at least three distinct colours.

Equations

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

theorem Erdos160.erdos_160.known_upper : (fun (n : ℕ) => ↑(h n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (2 / 3)

On Mathoverflow user leechlattice shows that $h(n) \ll n^{\frac 2 3}$.

theorem Erdos160.erdos_160.known_lower : ∃ c > 0, (fun (n : ℕ) => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun (n : ℕ) => ↑(h n)

The observation of Zachary Hunter in that question coupled with the bounds of Kelley-Meka KeMe23 imply that $$h(N) \gg \exp(c(\log N)^{\frac 1 {12}})$$ for some $c > 0$.

theorem Erdos160.erdos_160.better_upper : let upper_bound := sorry; (fun (n : ℕ) => ↑(h n)) =O[Filter.atTop] upper_bound ∧ upper_bound =o[Filter.atTop] fun (n : ℕ) => ↑n ^ (2 / 3)

Estimate $h(n)$ by finding a better upper bound.

theorem Erdos160.erdos_160.better_lower : let lower_bound := sorry; (lower_bound =O[Filter.atTop] fun (n : ℕ) => ↑(h n)) ∧ ∀ c > 0, ((fun (n : ℕ) => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun (n : ℕ) => ↑(h n)) → ∀ c > 0, (fun (n : ℕ) => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound

Estimate $h(n)$ by finding a better lower bound.