Erdős problem 247

Let $n_1 < n_2 < \cdots$ be a sequence of integers such that $\limsup \frac{n_k}{k} = \infty.$ Is $\sum_{k=1}^{\infty} \frac{1}{2^{n_k}}$ transcendental?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

247.lean

Retained formal statement2 of 2

Erdős proved the answer is yes under the stronger condition that $\limsup \frac{n_k}{k^t} = \infty$ for all $t\geq 1$ .

[ErGr80] Erdős, P. and Graham, R., _Old and new problems and results in combinatorial number theory_. Monographies de L'Enseignement Mathematique (1980).

FormalConjectures/ErdosProblems/247.leanErdos247.erdos_247.variants.strong_condition4 linesExact file

1∀ (n : ℕ → ℕ),2  StrictMono n →3    (∀ t ≥ 1, Filter.limsup (fun k => ↑(↑(n k) / ↑k.succ ^ t)) Filter.atTop = ⊤) →4      Transcendental ℚ (∑' (k : ℕ), 1 / 2 ^ n k)

SolvedStatement only, no proof