CH2.summable_nterm_of_log_weight

lemma summable_nterm_of_log_weight {a : ℕ → ℂ} {β sig : ℝ}    (hsig : 1 < sig) (ha : Summable (fun n : ℕ ↦ ‖a n‖ / (n * Real.log n ^ β))) :    Summable (nterm a sig) := by  have hs : 0 < sig - 1 := sub_pos.mpr hsig  have hlo : (fun x : ℝ => Real.log x ^ β) =o[Filter.atTop] fun x => x ^ (sig - 1) :=    isLittleO_log_rpow_rpow_atTop β hs  have hlo_nat :      (fun n : ℕ => Real.log (n : ℝ) ^ β) =o[Filter.atTop] fun n => (n : ℝ) ^ (sig - 1) :=    hlo.comp_tendsto tendsto_natCast_atTop_atTop  have hlog_le : ∀ᶠ n : ℕ in Filter.atTop,      ‖Real.log (n : ℝ) ^ β‖ ≤ ‖(n : ℝ) ^ (sig - 1)‖ := by    simpa using hlo_nat.bound (show (0 : ℝ) < 1 by norm_num)  have h_event : ∀ᶠ n : ℕ in Filter.atTop,      ‖(if n = 0 then 0 else ‖a n‖ / (n : ℝ) ^ sig)‖ ≤ ‖a n‖ / ((n : ℝ) * Real.log n ^ β) := by    filter_upwards [hlog_le, Filter.eventually_ge_atTop (2 : ℕ)] with n hlog hn    have hnpos : 0 < (n : ℝ) := by positivity    have hlogpos : 0 < Real.log (n : ℝ) := Real.log_pos (by exact_mod_cast hn)    have hpowpos : 0 < Real.log (n : ℝ) ^ β := Real.rpow_pos_of_pos hlogpos _    have hlog_le' : Real.log (n : ℝ) ^ β ≤ (n : ℝ) ^ (sig - 1) := by      rwa [Real.norm_of_nonneg hpowpos.le, Real.norm_of_nonneg (Real.rpow_nonneg hnpos.le _)] at hlog    have hpow_split : (n : ℝ) ^ sig = (n : ℝ) * (n : ℝ) ^ (sig - 1) := by      conv_lhs => rw [show sig = 1 + (sig - 1) by ring]; rw [Real.rpow_add hnpos, Real.rpow_one]    rw [show (if n = 0 then 0 else ‖a n‖ / (n : ℝ) ^ sig) = ‖a n‖ / (n : ℝ) ^ sig from        by simp [show n ≠ 0 by omega], Real.norm_of_nonneg (div_nonneg (norm_nonneg _)        (Real.rpow_nonneg hnpos.le _)), hpow_split]    exact div_le_div_of_nonneg_left (norm_nonneg (a n)) (mul_pos hnpos hpowpos)      (mul_le_mul_of_nonneg_left hlog_le' hnpos.le)  have hbase : Summable (fun n : ℕ ↦ if n = 0 then 0 else ‖a n‖ / n ^ sig) :=    Summable.of_norm_bounded_eventually_nat ha h_event  simpa [nterm] using! hbase