Source indexedtheorem · leanprover/lean4:v4.32.0

ArithmeticFunction.LSeries_d_eq_riemannZeta_pow

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:258 to 279

Source documentation

The L-series of d k equals ζ(s)^k for Re(s) > 1.

Exact Lean statement

@[blueprint
  "LSeries_d_eq_riemannZeta_pow"
  (title := "LSeries d eq riemannZeta pow")
  (statement := /-- The $L$-series of $d_k$ equals $\zeta(s)^k$ for $\Re(s) > 1$. -/)
  (proof := /--
  From the definition of $d_k$ as the $k$-fold Dirichlet convolution of $\zeta$, we can express $d_k$ as $\zeta^k$. The L-series of a Dirichlet convolution corresponds to the product of the L-series of the individual functions. Since $L(\zeta, s)$ is the Riemann zeta function $\zeta(s)$, it follows that $L(d_k, s) = L(\zeta^k, s) = (L(\zeta, s))^k = \zeta(s)^k$ for $\Re(s) > 1$ where the series converges.
  -/)]
theorem LSeries_d_eq_riemannZeta_pow (k : ℕ) {s : ℂ} (hs : 1 < s.re) :
    LSeries (↗(d k)) s = riemannZeta s ^ k

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "LSeries_d_eq_riemannZeta_pow"  (title := "LSeries d eq riemannZeta pow")  (statement := /-- The $L$-series of $d_k$ equals $\zeta(s)^k$ for $\Re(s) > 1$. -/)  (proof := /--  From the definition of $d_k$ as the $k$-fold Dirichlet convolution of $\zeta$, we can express $d_k$ as $\zeta^k$. The L-series of a Dirichlet convolution corresponds to the product of the L-series of the individual functions. Since $L(\zeta, s)$ is the Riemann zeta function $\zeta(s)$, it follows that $L(d_k, s) = L(\zeta^k, s) = (L(\zeta, s))^k = \zeta(s)^k$ for $\Re(s) > 1$ where the series converges.  -/)]theorem LSeries_d_eq_riemannZeta_pow (k : ℕ) {s : ℂ} (hs : 1 < s.re) :    LSeries (↗(d k)) s = riemannZeta s ^ k := by  change LSeries (↗(d k : ArithmeticFunction ℂ)) s = riemannZeta s ^ k  induction k with  | zero =>    simp only [d_zero, natCoe_one, pow_zero, one_eq_delta]    exact congr_fun LSeries_delta s  | succ j ih =>    have hζ : LSeriesSummable (↗(ζ : ArithmeticFunction ℂ)) s :=      LSeriesSummable_zeta_iff.mpr hs    rw [pow_succ, LSeries_congr (fun {n} _ => show (d (j + 1) : ArithmeticFunction ℂ) n =        ((d j : ArithmeticFunction ℂ) * ζ) n by rw [d_succ, natCoe_mul]) s,        LSeries_mul' (LSeries_d_summable j hs) hζ, ih]    congr 1    exact LSeries_zeta_eq_riemannZeta hs