fix(ErdosProblems/480): typo

FormalConjectures/ErdosProblems/480.lean

@@ -24,29 +24,41 @@ import FormalConjectures.Util.ProblemImports
 
 namespace Erdos480
 
-/--
-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}$?
+open Filter
 
-This was proved Chung and Graham.
+/--
+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.
 -/
 @[category research solved, AMS 11]
 theorem erdos_480 : answer(True) ↔ ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
-    {(m, n) | (m) (n) (_ : m ≠ 0) (_ : |x (m + n) - x m| ≤ 1 / (√5 * n))}.Infinite := by
+    ⨅ n, atTop.liminf (fun m => n * |x (m + n) - x m|) ≤ 1 / √5 := by
   sorry
 
 /--
-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.
+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.
 -/
 @[category research solved, AMS 11]
 theorem erdos_480.variants.chung_graham :
     let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib
-    IsGreatest {C : ℝ | C > 0 ∧ ∀ (x : ℕ → ℝ) (hx : ∀ 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 := by
+    ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
+    ⨅ n, atTop.liminf (fun m => n * |x (m + n) - x m|) ≤ 1 / c := by
+  sorry
+
+/--
+They also prove that this constant is best possible.
+-/
+@[category research solved, AMS 11]
+theorem erdos_480.variants.chung_graham_best_possible :
+    let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib
+    ∀ ε > (0 : ℝ), ¬ (∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
+    ⨅ n, atTop.liminf (fun m => n * |x (m + n) - x m|) ≤ 1 / c - ε) := by
   sorry
 
 end Erdos480