def IsLacunary (A : ℕ → ℕ) : Prop

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

Equations

• IsLacunary A = (A 0 ≠ 0 ∧ ∃ μ > 1, ∀ (n : ℕ), μ ≤ ↑(A (n + 1)) / ↑(A n))

theorem IsLacunary.pos {A : ℕ → ℕ} (hA : IsLacunary A) (n : ℕ) : 0 < A n

Every term of a lacunary sequence is positive.

theorem IsLacunary.StrictMono (A : ℕ → ℕ) (hA : IsLacunary A) : _root_.StrictMono A

Every lacunary sequence is strictly increasing.