Qexp deriv bound of coeff bound

lemma qexp_deriv_bound_of_coeff_bound {a : ℕ+ → ℂ} {k : ℕ}    (ha : ∀ n : ℕ+, ‖a n‖ ≤ (n : ℝ)^k) :    ∀ K : Set ℂ, K ⊆ {w : ℂ | 0 < w.im} → IsCompact K →      ∃ u : ℕ+ → ℝ, Summable u ∧ ∀ (n : ℕ+) (z : K),        ‖a n * (2 * π * I * ↑n) * cexp (2 * π * I * ↑n * z.1)‖ ≤ u n := by  intro K hK_sub hK_compact  by_cases hK_nonempty : K.Nonempty  · obtain ⟨k_min, hk_min_mem, hk_min_le⟩ := hK_compact.exists_isMinOn hK_nonempty      Complex.continuous_im.continuousOn    have hy_min_pos : 0 < k_min.im := hK_sub hk_min_mem    have hpos : 0 < 2 * π * k_min.im := by nlinarith [pi_pos]    have h := Real.summable_pow_mul_exp_neg_nat_mul (k + 1) hpos    have hconv : Summable (fun n : ℕ+ =>        2 * π * ((n : ℕ) : ℝ)^(k + 1) * rexp (-(2 * π * k_min.im) * (n : ℕ))) := by      have : Summable (fun n : ℕ+ =>          ((n : ℕ) : ℝ)^(k + 1) * rexp (-(2 * π * k_min.im) * (n : ℕ))) := h.subtype _      simpa [mul_assoc] using this.mul_left (2 * π)    use fun n => 2 * π * (n : ℝ)^(k + 1) * rexp (-2 * π * ↑n * k_min.im)    constructor    · apply hconv.of_nonneg_of_le      · intro n; positivity      · intro n        have h1 : -2 * π * ↑↑n * k_min.im = -(2 * π * k_min.im) * ↑↑n := by ring        simp only [h1]; exact le_refl _    · intro n ⟨z, hz_mem⟩      have hz_im : k_min.im ≤ z.im := hk_min_le hz_mem      have hn_pos : (0 : ℝ) < n := by exact_mod_cast n.pos      have h_norm_2pin : ‖(2 : ℂ) * π * I * ↑↑n‖ = 2 * π * n := by        rw [norm_mul, norm_mul, norm_mul, Complex.norm_ofNat, Complex.norm_real,            Complex.norm_I, mul_one, Complex.norm_natCast, Real.norm_of_nonneg pi_pos.le]      calc ‖a n * (2 * π * I * ↑↑n) * cexp (2 * π * I * ↑↑n * z)‖          = ‖a n‖ * ‖(2 * π * I * ↑↑n)‖ * ‖cexp (2 * π * I * ↑↑n * z)‖ := by            rw [norm_mul, norm_mul]        _ ≤ (n : ℝ)^k * (2 * π * n) * rexp (-2 * π * n * z.im) := by            rw [h_norm_2pin]            have hexp : ‖cexp (2 * π * I * ↑↑n * z)‖ ≤ rexp (-2 * π * n * z.im) := by              rw [Complex.norm_exp]              have : (2 * π * I * ↑↑n * z).re = -2 * π * n * z.im := by                simp only [Complex.mul_re, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im,                  Complex.I_re, Complex.I_im, Complex.natCast_re, Complex.natCast_im,                  mul_zero, mul_one, zero_add, add_zero, sub_zero]; ring              rw [this]            gcongr; exact ha n        _ ≤ (n : ℝ)^k * (2 * π * n) * rexp (-2 * π * n * k_min.im) := by            apply mul_le_mul_of_nonneg_left _ (by positivity)            apply Real.exp_le_exp_of_le            apply mul_le_mul_of_nonpos_left hz_im            nlinarith [pi_pos, hn_pos]        _ = 2 * π * (n : ℝ)^(k + 1) * rexp (-2 * π * n * k_min.im) := by ring  · use fun _ => 0    constructor    · exact summable_zero    · intro n ⟨z, hz_mem⟩      exfalso; exact hK_nonempty ⟨z, hz_mem⟩