Source indexedlemma · leanprover/lean4:v4.32.0

ArithmeticFunction.zeta_alt

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1183 to 1211

Source documentation

Zeta alt: ζ(s) = ζ(2*s) * ∑_n (|μ(n)|) n^(-s), where omega is the number of distinct prime factors.

Exact Lean statement

@[blueprint
  "zeta_alt"
  (title := "zeta alt")
  (statement := /--
  $$\zeta(s) =\zeta(2s) \sum_{n=1}^{\infty}\mu^2(n)n^{-s}.$$
  \begin{verbatim}
    An expression for `ζ`, in IK (1.32).
  \end{verbatim}
  -/)
  (proof := /--
  The series $\sum_{n=1}^{\infty}\mu^2(n)n^{-s}$ has Euler product $\prod_{p} (1 + p^{-s})$. On the other hand, $\zeta(2s)=\prod_p (1 - p^{-2s})^{-1}$. The product of these two Euler products is $\prod_p (1 - p^{-s})^{-1} = \zeta(s)$, which gives the desired formula.
  -/)]
lemma zeta_alt (s : ℂ) (hs : 1 < s.re) :
    riemannZeta s =
    riemannZeta (2 * s) * LSeries (fun (n : ℕ) ↦ (μ n : ℂ) ^ 2) s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "zeta_alt"  (title := "zeta alt")  (statement := /--  $$\zeta(s) =\zeta(2s) \sum_{n=1}^{\infty}\mu^2(n)n^{-s}.$$  \begin{verbatim}    An expression for `ζ`, in IK (1.32).  \end{verbatim}  -/)  (proof := /--  The series $\sum_{n=1}^{\infty}\mu^2(n)n^{-s}$ has Euler product $\prod_{p} (1 + p^{-s})$. On the other hand, $\zeta(2s)=\prod_p (1 - p^{-2s})^{-1}$. The product of these two Euler products is $\prod_p (1 - p^{-s})^{-1} = \zeta(s)$, which gives the desired formula.  -/)]lemma zeta_alt (s : ℂ) (hs : 1 < s.re) :    riemannZeta s =    riemannZeta (2 * s) * LSeries (fun (n : ℕ) ↦ (μ n : ℂ) ^ 2) s := by  have hs' : 1 < (2 * s).re := by rw [Complex.mul_re]; norm_num; linarith  have mulable := (riemannZeta_eulerProduct_hasProd hs).multipliable  rw [← riemannZeta_eulerProduct_tprod hs, ← riemannZeta_eulerProduct_tprod hs',    moebius_sq_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 ⟨riemannZeta (2 * s), riemannZeta_eulerProduct_hasProd hs'⟩  · exact ⟨LSeries (fun n ↦ (μ n) ^ 2) s, moebius_sq_LSeries_eulerProduct_hasProd s hs⟩