Source indexedtheorem · leanprover/lean4:v4.32.0

logDeriv_riemannXi_eq_polynomial_derivative_add_tsum

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean:244 to 290

Source documentation

Logarithmic derivative identity for a chosen ξ Hadamard factorization.

The divisor-product differentiability is supplied by Complex.Hadamard.differentiableAt_divisorCanonicalProduct_univ, and xi zero summability is supplied by summable_riemannXi_divisorZeroIndex₀_norm_inv_sq. The remaining hypotheses are the point-not-a-zero assumptions needed for the logarithmic derivative and zero-sum terms; the product nonvanishing is derived from the generic divisor-product nonvanishing theorem.

Exact Lean statement

theorem logDeriv_riemannXi_eq_polynomial_derivative_add_tsum
    {P : Polynomial ℂ} {z : ℂ}
    (hfac : ∀ w : ℂ, riemannXi w =
      Complex.exp (Polynomial.eval w P) *
        Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) w)
    (hz : ∀ p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),
      z ≠ Complex.Hadamard.divisorZeroIndex₀_val p) :
    logDeriv riemannXi z =
      Polynomial.eval z P.derivative +
        ∑' p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),
          (1 / (z - Complex.Hadamard.divisorZeroIndex₀_val p) +
            1 / Complex.Hadamard.divisorZeroIndex₀_val p)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem logDeriv_riemannXi_eq_polynomial_derivative_add_tsum    {P : Polynomial ℂ} {z : ℂ}    (hfac : ∀ w : ℂ, riemannXi w =      Complex.exp (Polynomial.eval w P) *        Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) w)    (hz : ∀ p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),      z ≠ Complex.Hadamard.divisorZeroIndex₀_val p) :    logDeriv riemannXi z =      Polynomial.eval z P.derivative +        ∑' p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),          (1 / (z - Complex.Hadamard.divisorZeroIndex₀_val p) +            1 / Complex.Hadamard.divisorZeroIndex₀_val p) := by  let G : ℂ → ℂ :=    Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ)  have hfun : riemannXi = fun w : ℂ => Complex.exp (Polynomial.eval w P) * G w := by    funext w    simpa [G] using hfac w  have hdiff_exp : DifferentiableAt ℂ (fun w : ℂ => Complex.exp (Polynomial.eval w P)) z :=    ((Complex.hasDerivAt_exp (Polynomial.eval z P)).comp z (P.hasDerivAt z)).differentiableAt  have hprod_ne :      Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) z ≠ 0 :=    Complex.Hadamard.divisorCanonicalProduct_ne_zero_of_forall_ne      1 riemannXi summable_riemannXi_divisorZeroIndex₀_norm_inv_sq hz  calc    logDeriv riemannXi z =        logDeriv (fun w : ℂ => Complex.exp (Polynomial.eval w P) * G w) z := by          rw [hfun]    _ = logDeriv (fun w : ℂ => Complex.exp (Polynomial.eval w P)) z + logDeriv G z := by          exact logDeriv_mul z (Complex.exp_ne_zero _) (by simpa [G] using hprod_ne)            hdiff_exp            (by              simpa [G] using                Complex.Hadamard.differentiableAt_divisorCanonicalProduct_univ                  1 riemannXi summable_riemannXi_divisorZeroIndex₀_norm_inv_sq z)    _ = Polynomial.eval z P.derivative +        ∑' p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),          (1 / (z - Complex.Hadamard.divisorZeroIndex₀_val p) +            1 / Complex.Hadamard.divisorZeroIndex₀_val p) := by          rw [Polynomial.logDeriv_exp_eval]          rw [show logDeriv G z =              ∑' p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),                (1 / (z - Complex.Hadamard.divisorZeroIndex₀_val p) +                  1 / Complex.Hadamard.divisorZeroIndex₀_val p) from            by              simpa [G] using                logDeriv_riemannXi_divisorCanonicalProduct_one_eq_tsum                  hz]