erdos_263.variants.folklore

A folklore result states that any $a_n$ satisfying $\lim_{n \to \infty} a_n^{\frac{1}{2^n}} = \infty$ has $\sum \frac{1}{a_n}$ converging to an irrational number.

theorem erdos_263.variants.folklore (a : ℕ -> ℕ)
    (ha : atTop.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (2 ^ n : ℝ))) atTop) :
    Irrational <| ∑' n, (1 : ℝ) / (a n : ℝ)

Recent Submissions

No submissions yet. Be the first to attempt this problem.