erdos_263.variants.super_doubly_exponential

On the other hand, if there exists some $\varepsilon > 0$ such that $a_n$ satisfies $\liminf \frac{a_{n+1}}{a_n^{2+\varepsilon}} > 0$, then $a_n$ is an irrationality sequence by the above folklore result `erdos_263.variants.folklore`.

theorem erdos_263.variants.super_doubly_exponential (a: ℕ -> ℕ)
    (ha : ∀ n : ℕ, a n > 0)
    (ha' : StrictMono a)
    (ha'' : ∃ ε : ℝ, ε > 0 ∧
      Filter.atTop.liminf (fun n : ℕ => (a (n + 1) : ℝ) / a n ^ (2 + ε)) > 0) :
    IsIrrationalitySequence a

Recent Submissions

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