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.

def IsLacunaryReal (a : ℕ → ℝ) : Prop

The real-valued analogue of IsLacunary.

Equations

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

theorem isLacunary_iff_isLacunaryReal {n : ℕ → ℕ} : IsLacunary n ↔ IsLacunaryReal fun (k : ℕ) => ↑(n k)

An ℕ-valued sequence is lacunary iff its real cast is lacunary as a real sequence.

theorem IsLacunaryReal.eventually_lt {a : ℕ → ℝ} (ha : IsLacunaryReal a) (hpos : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < a k) : ∀ᶠ (k : ℕ) in Filter.atTop, a k < a (k + 1)

A positive lacunary real-valued sequence is eventually strictly increasing.