E1_sub_one_eq
plain-language theorem explainer
Algebraic identity rewrites the deviation E1(z) - 1 for the genus-one Weierstrass factor in terms of the exponential remainder (exp(z) - 1 - z) and a linear correction term. Analysts deriving norm bounds and summability statements for Hadamard products of order-1 entire functions cite this identity to isolate the quadratic contribution. The tactic proof unfolds the definition of E1, inserts a trivial ring identity for exp(z), and reduces both sides by ring normalization.
Claim. For any complex number $z$, let $E_1(z) := (1 - z) e^z$. Then $E_1(z) - 1 = (e^z - 1 - z) - z (e^z - 1)$.
background
The module HadamardGenusOne supplies the concrete analytic substrate for genus-one Hadamard factorization of entire functions of order at most 1. The elementary factor is defined by E1(z) := (1 - z) * Complex.exp z. The identity separates the quadratic remainder of the exponential from the linear term that appears when the factor is expanded around z = 0.
proof idea
The proof is a short tactic sequence: unfold E1 to expose the product definition, introduce the ring identity exp(z) = 1 + (exp(z) - 1), rewrite the left-hand side with that identity, and finish with ring normalization on both sides.
why it matters
The identity is the first algebraic step feeding the norm bound norm_E1_sub_one_le, which in turn supplies the per-factor estimate ||E1(z) - 1|| <= 3 ||z||^2 for ||z|| <= 1. That bound is required for absolute summability of the corrections E1(z_n) - 1 once the zeros satisfy summability of ||z_n||^2, a prerequisite listed in the module for the open XiHadamardIdentification step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.