True ↔ ∃ ε > 0, ∀ (q : ℝ), 1 < q → q < 1 + ε → ∀ (x : ℕ → ℝ), StrictMono x → Set.range x = {x | ∃ S, ∑ i ∈ S, q ^ i = x} → Filter.Tendsto (fun k => x (k + 1) - x k) Filter.atTop (nhds 0)