def IsLacunary (n : ℕ → ℕ) : Prop

Say a sequence is lacunary if there exists some $\lambda > 1$ such that $a_{n+1}/a_n > \lambda$ for all sufficiently large $n$.

Equations

• IsLacunary n = ∃ c > 1, ∀ᶠ (k : ℕ) in Filter.atTop, c * ↑(n k) < ↑(n (k + 1))

theorem IsLacunary.eventually_lt {n : ℕ → ℕ} (hn : IsLacunary n) : ∀ᶠ (k : ℕ) in Filter.atTop, n k < n (k + 1)

Every lacunary sequence is eventually strictly increasing.