∀ (k l : ℕ) {f : ℕ → ℂ} {p : ℝ},
  0 < p →
    (f =O[Filter.atTop] fun n => ↑n ^ l) →
      SummableLocallyUniformlyOn
        (fun n =>
          f n •
            iteratedDerivWithin k (fun z => Complex.exp (2 * ↑Real.pi * Complex.I * z / ↑p) ^ n)
              UpperHalfPlane.upperHalfPlaneSet)
        UpperHalfPlane.upperHalfPlaneSet