Erdős problem 1096 · problems.science

Let $1<q<1+\epsilon$ and consider the set of numbers of the shape $\sum_{i\in S}q^i$ (for all finite $S$ ), ordered by size as $0=x_1<x_2<\cdots$ .

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1096.lean

Retained formal statement1 of 1

Let $1<q<1+\epsilon$ and consider the set of numbers of the shape $\sum_{i\in S}q^i$ (for all finite $S$ ), ordered by size as $0=x_1<x_2<\cdots$ .

Is it true that, provided $\epsilon>0$ is sufficiently small, $x_{k+1}-x_k \to 0$ ?

This was solved affirmatively by Erdős and Komornik [ErKo98], who proved the conclusion whenever $1<q<\sqrt{q_1}$ , where $q_1$ is the second Pisot-Vijayaraghavan number.

FormalConjectures/ErdosProblems/1096.leanErdos1096.erdos_10969 linesExact file

1True ↔2  ∃ ε > 0,3    ∀ (q : ℝ),4      1 < q →5        q < 1 + ε →6          ∀ (x : ℕ → ℝ),7            StrictMono x →8              Set.range x = {x | ∃ S, ∑ i ∈ S, q ^ i = x} →9                Filter.Tendsto (fun k => x (k + 1) - x k) Filter.atTop (nhds 0)

SolvedStatement only, no proof

Sources

Search problems.science