ArithmeticFunction.LSeriesSummable_moebius_sq

@[blueprint  "LSeriesSummable_moebius_sq"  (title := "LSeriesSummable-moebius-sq")  (statement := /--    The $L$-series with coefficients given by $\mu^2(n)$ converges on the region $1<\Re(s)$.  -/)  (proof := /--    This follows by comparison test against the Riemann zeta function.  -/)]lemma LSeriesSummable_moebius_sq {s : ℂ} (hs : 1 < s.re) :    LSeriesSummable (fun n ↦ (μ n) ^ 2) s := by  have hgf : ∀ (n : ℕ), ‖LSeries.term (fun n ↦ (μ n) ^ 2) s n‖ ≤ ‖LSeries.term (fun n ↦ 1) 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]      refine div_le_div_of_nonneg_right ?_ (norm_nonneg _)      simp only [Complex.norm_intCast, sq_abs, one_mem, CStarRing.norm_of_mem_unitary,        sq_le_one_iff_abs_le_one]      exact_mod_cast ArithmeticFunction.abs_moebius_le_one  have zetaSummable : LSeriesSummable 1 s := LSeriesSummable_one_iff.mpr hs  rw [LSeriesSummable, ← summable_norm_iff] at zetaSummable;  apply LSeriesSummable.of_norm_le_norm hgf zetaSummable