Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.tsum_vonMangoldt_neg_mellin_line

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:94 to 110

Source documentation

Collapse the von Mangoldt Dirichlet series on the negative Mellin line.

Exact Lean statement

lemma tsum_vonMangoldt_neg_mellin_line {a : ℝ} (ha : 0 < a) (t : ℝ) :
    (∑' n : ℕ,
        (Λ n : ℂ) * (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) =
      -deriv riemannZeta (((1 + a : ℝ) : ℂ) - (t : ℂ) * I) /
        riemannZeta (((1 + a : ℝ) : ℂ) - (t : ℂ) * I)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tsum_vonMangoldt_neg_mellin_line {a : ℝ} (ha : 0 < a) (t : ℝ) :    (∑' n : ℕ,        (Λ n : ℂ) * (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) =      -deriv riemannZeta (((1 + a : ℝ) : ℂ) - (t : ℂ) * I) /        riemannZeta (((1 + a : ℝ) : ℂ) - (t : ℂ) * I) := by  have hs : 1 < (((1 + a : ℝ) : ℂ) - (t : ℂ) * I).re := by    simp    linarith  rw [← tsum_vonMangoldt_eq hs]  refine tsum_congr fun n ↦ ?_  rcases Nat.eq_zero_or_pos n with rfl | hn  · simp  · have hline :        ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) =          -(((1 + a : ℝ) : ℂ) - (t : ℂ) * I) := by      ring    rw [hline, Complex.cpow_neg, div_eq_mul_inv]