Source indexedtheorem · leanprover/lean4:v4.32.0

existsUnique_riemannXi_hadamard_polynomial_derivative_eval_zero

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean:354 to 364

Source documentation

There is a unique complex number obtained as Polynomial.eval 0 P.derivative from a degree-one no-monomial Hadamard factorization of Riemann's xi function. This is the canonical theorem-level formulation of Kadiri's Hadamard constant, without choosing a global witness.

Exact Lean statement

theorem existsUnique_riemannXi_hadamard_polynomial_derivative_eval_zero :
    ∃! B : ℂ, ∃ P : Polynomial ℂ, P.degree ≤ 1 ∧ (∀ z : ℂ, riemannXi z =
        Complex.exp (Polynomial.eval z P) *
          Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) z) ∧
      B = Polynomial.eval 0 P.derivative

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem existsUnique_riemannXi_hadamard_polynomial_derivative_eval_zero :    ∃! B : ℂ, ∃ P : Polynomial ℂ, P.degree ≤ 1 ∧ (∀ z : ℂ, riemannXi z =        Complex.exp (Polynomial.eval z P) *          Complex.Hadamard.divisorCanonicalProduct 1 riemannXi (Set.univ : Set ℂ) z) ∧      B = Polynomial.eval 0 P.derivative := by  rcases riemannXi_hadamard_factorization_no_monomial with ⟨P, hdeg, hfac⟩  refine ⟨Polynomial.eval 0 P.derivative, ⟨P, hdeg, hfac, rfl⟩, ?_⟩  intro B hB  rcases hB with ⟨Q, _hQdeg, hQfac, rfl⟩  exact (riemannXi_hadamard_polynomial_derivative_eval_zero_eq    (P := P) (Q := Q) hfac hQfac).symm