Source indexedtheorem · leanprover/lean4:v4.32.0

ArithmeticFunction.LSeries_tau_eq_riemannZeta_sq

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:169 to 185

Source documentation

The L-series of $\tau$ equals the square of the Riemann zeta function for $\Re(s) > 1$ .

Exact Lean statement

@[blueprint
  "LSeries_tau_eq_riemannZeta_sq"
  (title := "LSeries tau eq riemannZeta sq")
  (statement := /-- The L-series of $\tau$ equals the square of the Riemann zeta function for $\Re(s) > 1$. -/)
  (proof := /--
  From the previous theorem, we have that the Dirichlet convolution of $\zeta$ with itself is $\tau$.
  Taking L-series on both sides, we get $L(\tau, s) = L(\zeta, s) \cdot L(\zeta, s)$.
  Since $L(\zeta, s)$ is the Riemann zeta function $\zeta(s)$, we conclude that
  $L(\tau, s) = \zeta(s)^2$ for $\Re(s) > 1$.
  -/)]
theorem LSeries_tau_eq_riemannZeta_sq {s : ℂ} (hs : 1 < s.re) :
    LSeries (↗τ) s = riemannZeta s ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "LSeries_tau_eq_riemannZeta_sq"  (title := "LSeries tau eq riemannZeta sq")  (statement := /-- The L-series of $\tau$ equals the square of the Riemann zeta function for $\Re(s) > 1$. -/)  (proof := /--  From the previous theorem, we have that the Dirichlet convolution of $\zeta$ with itself is $\tau$.  Taking L-series on both sides, we get $L(\tau, s) = L(\zeta, s) \cdot L(\zeta, s)$.  Since $L(\zeta, s)$ is the Riemann zeta function $\zeta(s)$, we conclude that  $L(\tau, s) = \zeta(s)^2$ for $\Re(s) > 1$.  -/)]theorem LSeries_tau_eq_riemannZeta_sq {s : ℂ} (hs : 1 < s.re) :    LSeries (↗τ) s = riemannZeta s ^ 2 := by  have h1 : LSeries (↗(ζ * ζ)) s = LSeries (↗((ζ : ArithmeticFunction ℂ) * ζ)) s := by    congr 1; ext n; simp only [← natCoe_mul, natCoe_apply]  have h2 : LSeries (↗((ζ : ArithmeticFunction ℂ) * ζ)) s = LSeries (↗ζ) s * LSeries (↗ζ) s :=    LSeries_mul' (LSeriesSummable_zeta_iff.mpr hs) (LSeriesSummable_zeta_iff.mpr hs)  rw [← zeta_mul_zeta, h1, h2, LSeries_zeta_eq_riemannZeta hs, pow_two]