E1
plain-language theorem explainer
The definition introduces the genus-one Weierstrass elementary factor E₁(z) = (1 - z) exp(z) for complex z. Analysts constructing Hadamard products for entire functions of order at most one cite this as the canonical per-zero correction. The declaration is a direct algebraic assignment with no reduction steps.
Claim. The genus-one Weierstrass factor is defined by $E_1(z) := (1 - z) e^z$ for $z$ complex.
background
The module HadamardGenusOne supplies the concrete analytic substrate for genus-one Hadamard factorization of entire functions of order ≤1. It proves the per-factor norm bound ‖E₁(z) - 1‖ ≤ 3‖z‖² for ‖z‖ ≤ 1, absolute summability of the corrections E₁(z_n) - 1 from square-summability of the z_n, and multipliability of the partial products. Three pieces remain open: the order bound on completedRiemannZeta₀, summability of the inverse-square zero moduli, and the identification of the product limit with completedRiemannZeta₀ up to an exponential prefactor.
proof idea
The declaration is a direct definition of the genus-one Weierstrass factor.
why it matters
This definition supplies the per-factor building block for the genus-one Hadamard product. It is invoked in completedRiemannZeta0_genus_one_factorization to express completedRiemannZeta₀(s) as exp(A + B s) times the infinite product of E1(s / z_n) once the identification hypothesis is supplied. The construction fills the elementary-factor step of the Hadamard factorization for order-one functions while leaving open XiOrderBound, zero summability, and the full identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.