Skip to content

Erdős problem 263

Must every irrationality sequence ana_n in the above sense satisfy an1/n→∞a_n^{1/n} \to \infty as n→∞n \to \infty?

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

263.lean

Retained formal statement4 of 6

A folklore result states that any ana_n satisfying lim⁡n→∞an12n=∞\lim_{n \to \infty} a_n^{\frac{1}{2^n}} = \infty has ∑1an\sum \frac{1}{a_n} converging to an irrational number.

FormalConjectures/ErdosProblems/263.leanErdos263.erdos_263.variants.folklore2 linesExact file
∀ (a : ℕ → ℕ),  Filter.Tendsto (fun n => ↑(a n) ^ (1 / 2 ^ n)) Filter.atTop Filter.atTop → Irrational (∑' (n : ℕ), 1 / ↑(a n))
SolvedStatement only, no proof