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 $n\geq 1$.

Equations

• IsLacunary n = ∃ c > 1, ∀ (k : ℕ), c * ↑(n k) < ↑(n (k + 1))

theorem IsLacunary.strictMono {n : ℕ → ℕ} (hn : IsLacunary n) : StrictMono n

Every lacunary sequence is strictly increasing.