XiHadamardIdentification
plain-language theorem explainer
XiHadamardIdentification packages a sequence of nonzero complex zeros together with constants A and B such that the completed Riemann zeta function equals exp(A + B s) times the infinite product of genus-one Weierstrass factors E1(s over each zero). Analytic number theorists formalizing entire-function representations of zeta would cite the structure once the order bound and zero summability are supplied. The declaration itself is a bare structure definition whose analytic content is the classical Hadamard theorem, external to the current Mathl
Claim. A structure consisting of a sequence of nonzero complex numbers $ρ_n$, constants $A,B∈ℂ$, and the identity $ξ_0(s)=e^{A+Bs}∏'_n E_1(s/ρ_n)$ for all $s∈ℂ$, where $E_1(z)=(1-z)e^z$ and the product converges absolutely.
background
The module supplies the concrete analytic substrate for the genus-one Hadamard factorization of the completed Riemann zeta function. Mathlib does not package the Hadamard factorization theorem for entire functions of order ≤1, so the module proves only the unconditional prerequisites for the elementary Weierstrass factor E1(z)=(1-z)exp(z): the per-factor norm bound ‖E1(z)−1‖≤3‖z‖² for ‖z‖≤1, absolute summability of the corrections E1(z_n)−1 from summability of ‖z_n‖², and multipliability of the partial products. Three named pieces remain open: the order bound XiOrderBound, the inverse-square summability XiZeroSummability, and the identification XiHadamardIdentification itself.
proof idea
This declaration is a structure definition that collects the data and the identification equality; it contains no proof steps, tactics, or lemmas.
why it matters
It is the third open analytic piece listed in the module documentation and is used directly by the theorem completedRiemannZeta0_genus_one_factorization to instantiate the factorization ξ₀(s)=exp(A+Bs)∏ E1(s/ρ_n). It also appears inside the status bundle HadamardGenusOneStatus. In the Recognition framework the structure supplies the zero-product representation required for further arguments about the zeta function once the missing order and summability hypotheses are discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.