Source indexedtheorem · leanprover/lean4:v4.32.0

LogDerivativeDirichlet

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:58 to 73

Source documentation

It has already been established that zeta doesn't vanish on the 1 line, and has a pole at $s=1$ of order 1. We also have the following.

Exact Lean statement

@[blueprint "LogDerivativeDirichlet"
  (title := "LogDerivativeDirichlet")
  (statement := /--
  We have that, for $\Re(s)>1$,
  $$-\frac{\zeta'(s)}{\zeta(s)} = \sum_{n=1}^\infty \frac{\Lambda(n)}{n^s}. $$-/)
  (proof := /-- Already in Mathlib. -/)]
theorem LogDerivativeDirichlet (s : ℂ) (hs : 1 < s.re) :
    - deriv riemannZeta s / riemannZeta s = ∑' n, Λ n / (n : ℂ) ^ s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "LogDerivativeDirichlet"  (title := "LogDerivativeDirichlet")  (statement := /--  We have that, for $\Re(s)>1$,  $$-\frac{\zeta'(s)}{\zeta(s)} = \sum_{n=1}^\infty \frac{\Lambda(n)}{n^s}. $$-/)  (proof := /-- Already in Mathlib. -/)]theorem LogDerivativeDirichlet (s : ℂ) (hs : 1 < s.re) :    - deriv riemannZeta s / riemannZeta s = ∑' n, Λ n / (n : ℂ) ^ s := by  rw [← ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs]  dsimp [LSeries, LSeries.term]  nth_rewrite 2 [Summable.tsum_eq_add_tsum_ite (b := 0) ?_]  · simp  · have := ArithmeticFunction.LSeriesSummable_vonMangoldt hs    dsimp [LSeriesSummable] at this    convert! this; rename ℕ => n    by_cases h : n = 0 <;> simp [LSeries.term, h]