Skip to content

Erdős problem 480

Let x1,x2,…∈[0,1]x_1,x_2,\ldots\in [0,1] be an infinite sequence. Is it true that inf⁡nlim inf⁡m→∞n∣xm+n−xm∣≤5−1/2≈0.447?\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.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

480.lean

Retained formal statement2 of 3

This was proved by Chung and Graham [ChGr84], who in fact prove that inf⁡nlim inf⁡m→∞n∣xm+n−xm∣≤1c≈0.3944\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq \frac{1}{c}\approx 0.3944 where c=1+∑k≥11F2k=2.5353705⋯c=1+\sum_{k\geq 1}\frac{1}{F_{2k}}=2.5353705\cdots and FmF_m is the mmth Fibonacci number.

FormalConjectures/ErdosProblems/480.leanErdos480.erdos_480.variants.chung_graham3 linesExact file
have c := 1 + ∑' (k : ℕ+), 1 / ↑(Nat.fib (2 * ↑k));∀ (x : ℕ → ℝ),  (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ n, Filter.liminf (fun m => ↑↑n * |x (m + ↑n) - x m|) Filter.atTop ≤ 1 / c
SolvedStatement only, no proof