norm_E1_sub_one_le
plain-language theorem explainer
The genus-one Weierstrass factor satisfies a quadratic deviation bound inside the unit disk. Analysts constructing Hadamard products for order-one entire functions cite this estimate to control convergence of the infinite product. The proof rewrites the factor via its defining identity, invokes two standard exponential norm bounds, controls the cross term by a separate multiplication estimate, and closes with the triangle inequality plus algebraic simplification.
Claim. For any complex number $z$ satisfying $|z| ≤ 1$, the inequality $|E_1(z) - 1| ≤ 3 |z|^2$ holds, where the genus-one elementary factor is defined by $E_1(z) := (1 - z) exp(z)$.
background
The HadamardGenusOne module supplies the analytic substrate for the genus-one case of the Hadamard factorization theorem, which Mathlib does not yet package in full. The central object is the elementary factor $E_1(z) = (1 - z) exp(z)$. The module establishes three unconditional results: the per-factor norm bound, absolute summability of the corrections $E_1(z_n) - 1$ whenever the squared moduli are summable, and multipliability of the partial products. The remaining steps, including the order bound on the completed Riemann zeta function, are left open.
proof idea
The tactic proof rewrites via the sibling identity E1_sub_one_eq. It obtains the quadratic remainder bound from Complex.norm_exp_sub_one_sub_id_le and the linear bound from norm_exp_sub_one_le_two_mul. A separate calculation using norm_mul and mul_le_mul_of_nonneg_left produces the cross-term estimate $||z (exp z - 1)|| ≤ 2 ||z||^2$. The main calc then applies norm_sub_le, adds the two quadratic contributions, and simplifies by linarith and ring to reach the factor of 3.
why it matters
This theorem populates the per_factor_estimate field inside the HadamardGenusOneStatus record, which aggregates the estimates required for the genus-one Hadamard product. It directly enables the sibling results on summability of corrections and the quotient version of the bound. In the Recognition Science setting it supplies the concrete analytic control needed before the order and zero-distribution questions for the xi function can be addressed. The module lists the three open pieces explicitly: XiOrderBound, XiZeroSummability, and XiHadamardIdentification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.