ArithmeticFunction.zeta_pow_two

@[blueprint  "zeta_pow_two"  (title := "zeta pow two")  (statement := /--  $$\zeta(s)^2 =\zeta(2s) \sum_{n=1}^{\infty} 2^{\omega(n)} n^{-s}$$ for $\Re(s) > 1$.  \begin{verbatim}    An expression for `ζ^2`, in IK (1.31).  \end{verbatim}  -/)  (proof := /--    Note that    $$\zeta(s)^2=\prod_p\frac{1}{(1-p^{-s})^2}.$$    Similarly    $$\zeta(2s)=\prod_p\frac{1}{(1-p^{-2s})}.$$    Applying Theorems \ref{two-pow-omega-LSeries-eulerProduct-tprod} and \ref{two-pow-omega-LSeries-eulerProduct-hasProd} we have    $$\sum_{1\leq n}2^{\omega(n)}n^{-s}=\prod_p\frac{1+p^{-s}}{1-p^{-s}}.$$    Thus    $$\zeta(2s)\left(\sum_{1\leq n}2^{\omega(n)}n^{-s}\right)=\prod_p\frac{1+p^{-s}}{(1-p^{-s})(1-p^{-2s})}=\prod_p\frac{1}{(1-p^{-s})^2}$$    by the difference of squares. This is exactly the Euler product for $\zeta(s)^2$ mentioned earlier.  -/)]lemma zeta_pow_two (s : ℂ) (hs : 1 < s.re) :    riemannZeta s ^ 2 =    riemannZeta (2 * s) * LSeries (fun n ↦ 2 ^ (ω n)) s := by  have hs' : 1 < (2 * s).re := by rw [Complex.mul_re]; norm_num; linarith  have mulable := (riemannZeta_eulerProduct_hasProd hs).multipliable  rw [sq, ← riemannZeta_eulerProduct_tprod hs, ← Multipliable.tprod_mul mulable mulable,    mul_comm, ← riemannZeta_eulerProduct_tprod hs',    two_pow_omega_LSeries_eulerProduct_tprod s hs, ← Multipliable.tprod_mul, tprod_congr]  · intro p    have hsub := Complex.one_sub_prime_cpow_ne_zero p.2 hs    have hsq : 1 - ((p : ℂ) ^ (-s)) ^ 2 ≠ 0 := by      rw [show 1 - ((p : ℂ) ^ (-s)) ^ 2 = (1 - (p : ℂ) ^ (-s)) * (1 + (p : ℂ) ^ (-s)) from by ring]      exact mul_ne_zero hsub (Complex.one_add_prime_cpow_ne_zero p.2 hs)    rw [show (-(2 * s) : ℂ) = -s + -s from by ring, Complex.cpow_add _ _ (Nat.cast_ne_zero.mpr p.2.ne_zero)]    field_simp    ring  · exact ⟨LSeries (fun n ↦ 2 ^ (ω n)) s, two_pow_omega_LSeries_eulerProduct_hasProd s hs⟩  · exact ⟨riemannZeta (2 * s), riemannZeta_eulerProduct_hasProd hs'⟩