ArithmeticFunction.LSeriesSummable_two_pow_omega

@[blueprint  "LSeriesSummable_two_pow_omega"  (title := "LSeriesSummable-two-pow-omega")  (statement := /--    The $L$-series with coefficients given by $2^{\omega(n)}$ converges on the region $1<\Re(s)$.  -/)  (proof := /--    This follows by comparison test against the $L$-series with coefficients given by $\sigma_0(n)$.  -/)]lemma LSeriesSummable_two_pow_omega {s : ℂ} (hs : 1 < s.re) :    LSeriesSummable (fun n ↦ 2 ^ (ω n)) s := by  have hgf : ∀ (n : ℕ), ‖LSeries.term (fun n ↦ 2 ^ ω n) s n‖ ≤ ‖LSeries.term (fun n ↦ σ 0 n) s n‖ := by    intro n    by_cases hn : n = 0    · simp only [LSeries.term, hn, ↓reduceIte, norm_zero, Std.le_refl]    · simp only [LSeries.term, hn, ↓reduceIte, Complex.norm_div, norm_pow, Complex.norm_ofNat,        RCLike.norm_natCast]      exact div_le_div_of_nonneg_right (by exact_mod_cast two_pow_omega_le_sigma_zero hn) (norm_nonneg _)  apply LSeriesSummable.of_norm_le_norm hgf  rw [summable_norm_iff, ← LSeriesSummable]  convert LSeries_d_summable 2 hs using 1;  exact funext fun n => by rw [d_two]; rfl