1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9

import Mathlib

open Finset Filter Topology

theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by
  rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)]
  intro ε εpos
  simp only [true_and, Set.mem_Ici, Set.mem_Ioo]
  sorry