ArithmeticFunction.moebius_sq_tsum_prime_pow

@[blueprint  "moebius_sq_tsum_prime_pow"  (title := "moebius-sq-tsum-prime-pow")  (statement := /--    For $p$ prime, we have that    $$\sum_{0\leq k}\mu^2(p^k)p^{-ks}=1+p^{-s}.$$  -/)  (proof := /--    Note that $\mu^2(p^0)=1$ and $\mu^2(p^1)=1$ but $\mu^2(p^k)=0$ whenever $1<k$. Thus,    $$\sum_{0\leq k}\mu^2(p^k)p^{-ks}=1+p^{-s}.$$  -/)]lemma moebius_sq_tsum_prime_pow {s : ℂ} (p : Nat.Primes) :    sumOnPrimePows (LSeries.term (fun n ↦ (μ n) ^ 2) s) p = (1 + (p : ℂ) ^ (-s)) := by  have h_rw : 1 + ↑↑p ^ (-s) = ∑' (e : ℕ), (if e ≤ 1 then 1 else 0) / ((p : ℂ) ^ e) ^ s := by    rw [tsum_eq_sum (s := {0, 1})]    · simp only [mem_singleton, zero_ne_one, not_false_eq_true, sum_insert, _root_.zero_le,        ↓reduceIte, pow_zero, Complex.one_cpow, ne_eq, one_ne_zero, div_self, sum_singleton,        le_refl, pow_one, one_div, Complex.cpow_neg]    · intro e he; simp at he      simp [show ¬e ≤ 1 by omega]  simp only [sumOnPrimePows_apply, LSeries.term, Nat.pow_eq_zero, ne_eq, cast_pow, Nat.Prime.ne_zero p.prop, false_and, ↓reduceIte, ← Int.cast_pow, moebius_sq, h_rw]  apply tsum_congr  intro e  congr 1  by_cases h : (e ≤ 1) <;> simp only [Int.cast_ite, Int.cast_one, Int.cast_zero, h, ↓reduceIte, ite_eq_left_iff,    zero_ne_one, imp_false, Decidable.not_not, ite_eq_right_iff, one_ne_zero, imp_false]  · rw [Nat.squarefree_iff_factorization_le_one (pow_ne_zero _ (Nat.Prime.ne_zero p.prop))]    simp only [factorization_pow, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]    interval_cases e    · simp only [zero_mul, zero_le, implies_true]    · simp only [one_mul, ← Nat.squarefree_iff_factorization_le_one (Nat.Prime.ne_zero p.prop)]      exact (Nat.squarefree_and_prime_pow_iff_prime.mpr p.prop).1  · rw [Nat.squarefree_iff_factorization_le_one (pow_ne_zero _ (Nat.Prime.ne_zero p.prop))]    simp only [factorization_pow, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, not_forall, not_le]    use p    simp only [Nat.Prime.factorization_self p.prop, mul_one]    exact Nat.lt_of_not_le h