Erdős Problem 480

Reference: erdosproblems.com/480

theorem Erdos480.erdos_480 : True ↔ ∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ (n : ℕ), Filter.liminf (fun (m : ℕ) => ↑n * |x (m + n) - x m|) Filter.atTop ≤ 1 / √5

Let $x_1,x_2,\ldots\in [0,1]$ be an infinite sequence. Is it true that $$\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq 5^{-1/2}\approx 0.447?$$ A conjecture of Newman.

theorem Erdos480.erdos_480.variants.chung_graham : have c := 1 + ∑' (k : ℕ+), 1 / ↑(Nat.fib (2 * ↑k)); ∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ (n : ℕ), Filter.liminf (fun (m : ℕ) => ↑n * |x (m + n) - x m|) Filter.atTop ≤ 1 / c

This was proved by Chung and Graham \cite{ChGr84}, who in fact prove that $$\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq \frac{1}{c}\approx 0.3944$$ where $$c=1+\sum_{k\geq 1}\frac{1}{F_{2k}}=2.5353705\cdots$$ and $F_m$ is the $m$th Fibonacci number.

theorem Erdos480.erdos_480.variants.chung_graham_best_possible : have c := 1 + ∑' (k : ℕ+), 1 / ↑(Nat.fib (2 * ↑k)); ∀ ε > 0, ¬∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ (n : ℕ), Filter.liminf (fun (m : ℕ) => ↑n * |x (m + n) - x m|) Filter.atTop ≤ 1 / c - ε

They also prove that this constant is best possible.