FormalConjectures/Wikipedia/LonelyRunnerConjecture.lean

GitHub source file

4 declarations, 2 contain sorry, 0 declared as axioms

1. theorem LonelyRunnerConjecture.lonely_runner_conjecture Consider $n$ runners on a circular track of unit length sorry line 39 source

   Source documentation

   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.

   depends on sorry what this means

   Statement uses: Nat, Function.Embedding, Fin, Real, Iff, Ne, GE.ge, Dist.dist, HasQuotient.Quotient, AddSubgroup, AddSubgroup.zmultiples, OfNat.ofNat, HMul.hMul, HDiv.hDiv, Exists, And

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   53 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

2. def LonelyRunnerConjecture.deltaTuple 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 line 56 source

   Source documentation

   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.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Fin, Int, Real

   Proof uses: SupSet.sSup, Set.ofPred, Exists, AddCircle, OfNat.ofNat, LE.le, Dist.dist, AddSubgroup.zmultiples, HSMul.hSMul

   27 instances, coercions and auxiliary constants left out.

   noncomputable def deltaTuple {n : ℕ} (v : Fin n → ℤ) : ℝ :=
   …

3. def LonelyRunnerConjecture.deltaGap The $n$th gap of loneliness $\delta_n$: the infimum of deltaTuple over all $n$-tuples of distinct nonzero integer velocities line 63 source

   Source documentation

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

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Real

   Proof uses: InfSet.sInf, Set.ofPred, Exists, Function.Embedding, Fin, Int, And, Ne, OfNat.ofNat, Eq, LonelyRunnerConjecture.deltaTuple

   4 instances, coercions and auxiliary constants left out.

   noncomputable def deltaGap (n : ℕ) : ℝ :=
   …

4. theorem LonelyRunnerConjecture.lonely_runner_conjecture.variants.tao_2017 Theorem 1.3 (Tao, 2017; arXiv:1701.02048) sorry line 73 source

   Source documentation

   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}$.

   depends on sorry what this means

   Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, GE.ge, LonelyRunnerConjecture.deltaGap, HAdd.hAdd, HDiv.hDiv, HMul.hMul, Real.log, HPow.hPow, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   48 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem 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))) := by
   …

   Mentions: c, LonelyRunnerConjecture.deltaGap