theorem Erdos_987 (z : ℕ → Circle) : Filter.limsup (fun (k : ℕ) => Filter.limsup (fun (n : ℕ) => ↑‖∑ j ∈ Finset.range n, ↑(z j) ^ k‖) Filter.atTop) Filter.atTop = ⊤