Sigma qexp summable generic

lemma sigma_qexp_summable_generic (a b : ℕ) (z : UpperHalfPlane) :    Summable (fun n : ℕ+ => (n : ℂ)^a * (ArithmeticFunction.sigma b n : ℂ) *      Complex.exp (2 * Real.pi * Complex.I * n * z)) := by  apply Summable.of_norm  apply Summable.of_nonneg_of_le (fun n => norm_nonneg _)  · intro n    calc ‖(n : ℂ)^a * (ArithmeticFunction.sigma b n : ℂ) * Complex.exp (2 * π * Complex.I * n * z)‖        = ‖(n : ℂ)^a * (ArithmeticFunction.sigma b n : ℂ)‖ *            ‖Complex.exp (2 * π * Complex.I * n * z)‖ := norm_mul _ _      _ ≤ (n : ℝ)^(a + b + 1) * ‖Complex.exp (2 * π * Complex.I * n * z)‖ := by          apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)          rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_natCast, Complex.norm_natCast]          calc (n : ℝ)^a * (ArithmeticFunction.sigma b n : ℝ)              ≤ (n : ℝ)^a * (n : ℝ)^(b + 1) := by                exact_mod_cast mul_le_mul_of_nonneg_left                  (ArithmeticFunction.sigma_le_pow_succ b n) (pow_nonneg (Nat.cast_nonneg n) a)            _ = (n : ℝ)^(a + b + 1) := by ring      _ = ‖(n : ℂ)^(a + b + 1) * Complex.exp (2 * π * Complex.I * n * z)‖ := by          rw [norm_mul, Complex.norm_pow, Complex.norm_natCast]  · apply summable_norm_iff.mpr    have ha33 := summable_pow_mul_cexp (a + b + 1) 1 z    simp only [PNat.val_ofNat, Nat.cast_one, mul_one] at ha33    apply (ha33.comp_injective PNat.coe_injective).congr    intro n    simp only [Function.comp_apply]    rw [← Complex.exp_nat_mul]    (congr 2; ring)