Source indexedtheorem · leanprover/lean4:v4.32.0

riemannXi_hadamard_polynomial_derivative_eval_eq

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean:294 to 314

Source documentation

Any two xi Hadamard polynomials with the same divisor-canonical product have the same derivative at every point away from the nonzero divisor-indexed zero set.

Exact Lean statement

theorem riemannXi_hadamard_polynomial_derivative_eval_eq
    {P Q : Polynomial ℂ} {z : ℂ} (hPfac : ∀ w : ℂ, riemannXi w = Complex.exp (Polynomial.eval w P) *
        Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) w)
    (hQfac : ∀ w : ℂ, riemannXi w =
      Complex.exp (Polynomial.eval w Q) *
        Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) w)
    (hz : ∀ p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),
      z ≠ Complex.Hadamard.divisorZeroIndex₀_val p) :
    Polynomial.eval z P.derivative = Polynomial.eval z Q.derivative

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem riemannXi_hadamard_polynomial_derivative_eval_eq    {P Q : Polynomial ℂ} {z : ℂ} (hPfac : ∀ w : ℂ, riemannXi w = Complex.exp (Polynomial.eval w P) *        Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) w)    (hQfac : ∀ w : ℂ, riemannXi w =      Complex.exp (Polynomial.eval w Q) *        Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) w)    (hz : ∀ p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),      z ≠ Complex.Hadamard.divisorZeroIndex₀_val p) :    Polynomial.eval z P.derivative = Polynomial.eval z Q.derivative := by  let S : ℂ := ∑' p : Complex.Hadamard.divisorZeroIndex₀ riemannXi (Set.univ : Set ℂ),    (1 / (z - Complex.Hadamard.divisorZeroIndex₀_val p) +      1 / Complex.Hadamard.divisorZeroIndex₀_val p)  have hP :=    logDeriv_riemannXi_eq_polynomial_derivative_add_tsum      (P := P) (z := z) hPfac hz  have hQ :=    logDeriv_riemannXi_eq_polynomial_derivative_add_tsum      (P := Q) (z := z) hQfac hz  have hsum : Polynomial.eval z P.derivative + S = Polynomial.eval z Q.derivative + S := by    rw [← hP, ← hQ]  exact add_right_cancel hsum