Erdős Problem 260

Reference: erdosproblems.com/260

theorem Erdos260.erdos_260 : True ↔ ∀ (a : ℕ → ℤ) (s : ℝ), StrictMono a → Filter.Tendsto (fun (n : ℕ) => ↑(a n) / ↑n) Filter.atTop Filter.atTop → HasSum (fun (n : ℕ) => ↑(a n) / 2 ^ a n) s → Irrational s