Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.re_inner_eq

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3411 to 3455

Mathematical statement

Exact Lean statement

@[blueprint
  "kadiri-re-inner-eq"
  (title := "Inner real-part identity: collapsing to $T_1$")
  (statement := /-- For every $s \in \mathbb{C}$ with $\Re s > 1$,
  $$ \Re \Bigl( \sum_{n \geq 1} \frac{\Lambda(n)}{n^s} - \frac{1}{s - 1}
                + \sum_{\rho \in Z(\zeta)} \Bigl( \frac{1}{\rho} + \frac{1}{s - \rho} \Bigr) \Bigr)
     - \sum_{\rho \in Z(\zeta)} \Re \frac{1}{\rho}
   = -\tfrac{1}{2} \log \pi
     + \tfrac{1}{2} \Re \tfrac{\Gamma'}{\Gamma}\!\left(\tfrac{s}{2}+1\right). $$
  The zero block is the absolutely convergent Hadamard pairing of
  \ref{kadiri-hadamard-identity}, and the $\Re(1/\rho)$ correction is absolutely
  convergent; the standalone $\sum_\rho 1/(s - \rho)$ does not converge
  unconditionally. This is the identity that turns the $f(0)$-coefficient of
  equation (16) into the $T_1$ form of \ref{kadiri-prop-2-1}. -/)
  (proof := /-- For $\Re s > 1$ the Dirichlet series gives
  $\sum \Lambda(n)/n^s = -\zeta'/\zeta(s)$; substitute \ref{kadiri-hadamard-identity}
  (treating the equation as one in $\mathbb{C}$, not yet taking $\Re$). The $1/(s-1)$
  terms and the paired zero blocks cancel exactly, leaving
  $-B - \tfrac{1}{2}\log\pi + \tfrac{1}{2}\Gamma'/\Gamma(s/2+1)$. Taking real parts and
  applying \ref{kadiri-re-hadamardB-eq} cancels $\Re B$ against the
  $\sum_\rho \Re(1/\rho)$ correction, leaving the claim. -/)
  (latexEnv := "lemma")
  (discussion := 1478)]
theorem re_inner_eq {s : ℂ} (hs : 1 < s.re) :
    ((∑' n : ℕ, (Λ n : ℂ) / (n : ℂ) ^ s) - 1 / (s - 1) +
       ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),
         (1 / (ρ.val : ℂ) + 1 / (s - ρ.val))).re -
      ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),
        (1 / (ρ.val : ℂ)).re =
    -(1 / 2 : ℝ) * Real.log Real.pi +
      (1 / 2 : ℝ) * (digamma (s / 2 + 1)).re

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "kadiri-re-inner-eq"  (title := "Inner real-part identity: collapsing to $T_1$")  (statement := /-- For every $s \in \mathbb{C}$ with $\Re s > 1$,  $$ \Re \Bigl( \sum_{n \geq 1} \frac{\Lambda(n)}{n^s} - \frac{1}{s - 1}                + \sum_{\rho \in Z(\zeta)} \Bigl( \frac{1}{\rho} + \frac{1}{s - \rho} \Bigr) \Bigr)     - \sum_{\rho \in Z(\zeta)} \Re \frac{1}{\rho}   = -\tfrac{1}{2} \log \pi     + \tfrac{1}{2} \Re \tfrac{\Gamma'}{\Gamma}\!\left(\tfrac{s}{2}+1\right). $$  The zero block is the absolutely convergent Hadamard pairing of  \ref{kadiri-hadamard-identity}, and the $\Re(1/\rho)$ correction is absolutely  convergent; the standalone $\sum_\rho 1/(s - \rho)$ does not converge  unconditionally. This is the identity that turns the $f(0)$-coefficient of  equation (16) into the $T_1$ form of \ref{kadiri-prop-2-1}. -/)  (proof := /-- For $\Re s > 1$ the Dirichlet series gives  $\sum \Lambda(n)/n^s = -\zeta'/\zeta(s)$; substitute \ref{kadiri-hadamard-identity}  (treating the equation as one in $\mathbb{C}$, not yet taking $\Re$). The $1/(s-1)$  terms and the paired zero blocks cancel exactly, leaving  $-B - \tfrac{1}{2}\log\pi + \tfrac{1}{2}\Gamma'/\Gamma(s/2+1)$. Taking real parts and  applying \ref{kadiri-re-hadamardB-eq} cancels $\Re B$ against the  $\sum_\rho \Re(1/\rho)$ correction, leaving the claim. -/)  (latexEnv := "lemma")  (discussion := 1478)]theorem re_inner_eq {s : ℂ} (hs : 1 < s.re) :    ((∑' n : ℕ, (Λ n : ℂ) / (n : ℂ) ^ s) - 1 / (s - 1) +       ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),         (1 / (ρ.val : ℂ) + 1 / (s - ρ.val))).re -      ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),        (1 / (ρ.val : ℂ)).re =    -(1 / 2 : ℝ) * Real.log Real.pi +      (1 / 2 : ℝ) * (digamma (s / 2 + 1)).re := by  have hs1 : s ≠ 1 := by    intro hs_eq    rw [hs_eq] at hs    norm_num at hs  have hsZ : s ∉ riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) := by    intro hz    exact (not_lt_of_gt hs) hz.1.2  rw [tsum_vonMangoldt_eq hs, hadamard_identity s hs1 hsZ]  ring_nf  simp only [Complex.add_re, Complex.neg_re, Complex.mul_re, Complex.ofReal_re,    Complex.ofReal_im, zero_mul, sub_zero]  rw [re_hadamardB_eq]  norm_num  ring_nf