hadamardPartialProduct
plain-language theorem explainer
The finite genus-one Hadamard product over the first N zeros supplied as a sequence. Number theorists building explicit formulas or Hadamard representations of the completed zeta cite this truncation when passing to the infinite product limit. It is realized directly as the product of E1 factors applied to s divided by each listed zero.
Claim. Let $E_1(z)=(1-z)e^z$. For a sequence of zeros $z_n$ the partial product is defined by $P_N(s)=P_{n=0}^{N-1}E_1(s/z_n)$.
background
The HadamardFactorization module supplies the product interface required for Track D of the RH unconditional-closure plan. Mathlib already supplies the completed zeta function, its pole-removed version completedRiemannZeta0, differentiability, and the functional equation, but not the Hadamard product itself. The upstream genus-one elementary factor is the definition E1(z)=(1-z)exp(z).
proof idea
One-line definition that forms the product over Finset.range N of the hadamardE1 factor evaluated at s divided by the corresponding zero.
why it matters
This supplies the finite approximants required by the CompletedZetaHadamardProduct structure, the real target of Track D. That structure records the zero sequence, the constants A and B, and the product limit that must be shown to recover completedRiemannZeta0 up to the exponential prefactor. The definition therefore closes the finite-product side of the genus-one factorization needed for later explicit-formula work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.