Erdős problem 480 · problems.science

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.

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

480.lean

Retained formal statement3 of 3

They also prove that this constant is best possible.

FormalConjectures/ErdosProblems/480.leanErdos480.erdos_480.variants.chung_graham_best_possible4 linesExact file

1have c := 1 + ∑' (k : ℕ+), 1 / ↑(Nat.fib (2 * ↑k));2∀ ε > 0,3  ¬∀ (x : ℕ → ℝ),4      (∀ (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

Sources

Search problems.science