Erdős Problem 480

Reference: erdosproblems.com/480

theorem Erdos480.erdos_480 : (∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → {x_1 : ℕ × ℕ | ∃ (m : ℕ) (n : ℕ) (_ : m ≠ 0) (_ : |x (m + n) - x m| ≤ 1 / (√5 * ↑n)), (m, n) = x_1}.Infinite) ↔ True

Let $x_1,x_2,\dots \in [0, 1]$ be an infinite sequence. Is it true that there are infinitely many $m, n$ such that $|x_{m+n} - x_m| \le \frac 1 {\sqrt 5 n}$?

This was proved Chung and Graham.

theorem Erdos480.erdos_480.variants.chung_graham : have c := 1 + ∑' (k : ℕ+), 1 / ↑(Nat.fib (2 * ↑k)); IsGreatest {C : ℝ | C > 0 ∧ ∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ∀ ε ∈ Set.Ioo 0 C, ∃ (n : ℕ), {m : ℕ | m ≠ 0 ∧ |x (n + m) - x m| < 1 / ((C - ε) * ↑n)}.Infinite} c

For any $ϵ>0$ there must exist some $n$ such that there are infinitely many $m$ for which $|x_{m+n} - x_m| < \frac 1 {(c-ϵ)n}$, where $c= 1 + \sum_{k \ge 1} \frac 1 {F_{2k}} =2.535370508\dots$ and $F_m$ is the $m$th Fibonacci number. This constant is best possible.