FormalConjectures/ErdosProblems/480.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 480

Reference: erdosproblems.com/480

Imports (1)
  1. theorem Erdos480.erdos_480 Let $x_1,x_2,\ldots\in [0,1]$ be an infinite sequence sorry line 39 source

    Source documentation

    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.

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, LE.le, iInf, PNat, Filter.liminf, HMul.hMul, abs, HSub.hSub, HAdd.hAdd, Filter.atTop, HDiv.hDiv, Real.sqrt

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

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_480 : answer(True) ↔ ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
    ⨅ (n : ℕ+), atTop.liminf (fun m => (n : ℕ) * |x (m + (n : ℕ)) - x m|) ≤ 1 / √5 := by
…
  2. theorem Erdos480.erdos_480.variants.chung_graham Documented declaration: chung_graham sorry line 51 source

    Source documentation

    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.

    depends on sorry what this means

    Statement uses: Real, HAdd.hAdd, OfNat.ofNat, tsum, PNat, HDiv.hDiv, Nat.fib, HMul.hMul, Nat, SummationFilter.unconditional, Membership.mem, Set, Set.Icc, LE.le, iInf, Filter.liminf, abs, HSub.hSub, Filter.atTop

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

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_480.variants.chung_graham :
    let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib
…

    Mentions: c

  3. theorem Erdos480.erdos_480.variants.chung_graham_best_possible They also prove that this constant is best possible sorry line 61 source

    Source documentation

    They also prove that this constant is best possible.

    depends on sorry what this means

    Statement uses: Real, HAdd.hAdd, OfNat.ofNat, tsum, PNat, HDiv.hDiv, Nat.fib, HMul.hMul, Nat, SummationFilter.unconditional, GT.gt, Not, Membership.mem, Set, Set.Icc, LE.le, iInf, Filter.liminf, abs, HSub.hSub and 1 more

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

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_480.variants.chung_graham_best_possible :
    let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib
…

    Mentions: c