Lonely runner conjecture

Reference: Wikipedia

theorem LonelyRunnerConjecture.lonely_runner_conjecture (n : ℕ) (speed : Fin n ↪ ℝ) (lonely : Fin n → ℝ → Prop) (lonely_def : ∀ (r : Fin n) (t : ℝ), lonely r t ↔ ∀ (r2 : Fin n), r2 ≠ r → dist ↑(t * speed r) ↑(t * speed r2) ≥ 1 / ↑n) (r : Fin n) : ∃ t ≥ 0, lonely r t

Consider $n$ runners on a circular track of unit length. At the initial time $t = 0$, all runners are at the same position and start to run; the runners' speeds are constant, all distinct, and may be negative. A runner is said to be lonely at time $t$ if they are at a distance (measured along the circle) of at least $\frac 1 n$ from every other runner. The lonely runner conjecture states that each runner is lonely at some time, no matter the choice of speeds.

noncomputable def LonelyRunnerConjecture.deltaTuple {n : ℕ} (v : Fin n → ℤ) : ℝ

For an $n$-tuple of distinct integer velocities $v_1,\dots,v_n$, deltaTuple v is the maximal value of $\min_i \|t v_i\|_{\mathbb{R}/\mathbb{Z}}$ over time.

Equations

• LonelyRunnerConjecture.deltaTuple v = sSup {δ : ℝ | ∃ (t : AddCircle 1), ∀ (i : Fin n), δ ≤ dist (v i • t) 0}

noncomputable def LonelyRunnerConjecture.deltaGap (n : ℕ) : ℝ

The $n$th *gap of loneliness* $\delta_n$: the infimum of deltaTuple over all $n$-tuples of distinct nonzero integer velocities.

Equations

• LonelyRunnerConjecture.deltaGap n = sInf {d : ℝ | ∃ (v : Fin n ↪ ℤ), (∀ (i : Fin n), v i ≠ 0) ∧ d = LonelyRunnerConjecture.deltaTuple ⇑v}

theorem LonelyRunnerConjecture.lonely_runner_conjecture.variants.tao_2017 : ∃ (c : ℝ), 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, deltaGap n ≥ 1 / (2 * ↑n) + c * Real.log ↑n / (↑n ^ 2 * Real.log (Real.log ↑n) ^ 2)

Theorem 1.3 (Tao, 2017; arXiv:1701.02048). There exists an absolute constant $c > 0$ such that for all sufficiently large $n$, the gap of loneliness satisfies $\delta_n \ge \frac{1}{2n} + \frac{c \log n}{n^2 (\log \log n)^2}$.