XiHadamardIdentification

formal source

 186Once supplied, `ξ₀(s) = exp(A + B s) · ∏ E₁(s/ρ_n)`. The actual analytic
 187proof of this identification is the classical Hadamard theorem, not yet in
 188Mathlib. -/
 189structure XiHadamardIdentification where
 190  zeros : ℕ → ℂ
 191  zeros_ne_zero : ∀ n, zeros n ≠ 0
 192  inv_sq_summable : Summable (fun n => 1 / ‖zeros n‖ ^ 2)
 193  A : ℂ
 194  B : ℂ
 195  identification :
 196    ∀ s : ℂ,
 197      completedRiemannZeta₀ s =
 198        Complex.exp (A + B * s) * ∏' n, E1 (s / zeros n)
 199
 200/-! ## 7. What the supplied data gives -/
 201
 202/-- Once `XiHadamardIdentification` is supplied, `completedRiemannZeta₀`
 203factors as the genus-one product times an exponential. -/
 204theorem completedRiemannZeta0_genus_one_factorization
 205    (H : XiHadamardIdentification) (s : ℂ) :
 206    completedRiemannZeta₀ s =
 207      Complex.exp (H.A + H.B * s) * ∏' n, E1 (s / H.zeros n) :=
 208  H.identification s
 209
 210/-! ## 8. Status -/
 211
 212/-- Track-D status bundle: per-factor estimate proved, summability proved,
 213multipliability proved; the order bound, zero-summability, and Hadamard
 214identification remain open analytic content. -/
 215structure HadamardGenusOneStatus where
 216  per_factor_estimate :
 217    ∀ z : ℂ, ‖z‖ ≤ 1 → ‖E1 z - 1‖ ≤ 3 * ‖z‖ ^ 2
 218  summability_from_sq :
 219    ∀ z : ℕ → ℂ, (∀ n, ‖z n‖ ≤ 1) →