pith. machine review for the scientific record. sign in
def definition def or abbrev high

E1

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  38def E1 (z : ℂ) : ℂ := (1 - z) * Complex.exp z

proof body

Definition body.

  39

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.