 174/-- `XiZeroSummability`: the inverse-square moduli of zeros of
 175`completedRiemannZeta₀` are summable (Jensen's formula + counting). Mathlib
 176has Jensen's formula but the application to ξ₀ is not packaged. -/
 177def XiZeroSummability : Prop :=
 178  ∃ ρ : ℕ → ℂ,
 179    (∀ n, completedRiemannZeta₀ (ρ n) = 0) ∧
 180    (∀ n, ρ n ≠ 0) ∧
 181    Summable (fun n => 1 / ‖ρ n‖ ^ 2)
 182
 183/-- `XiHadamardIdentification`: the genus-one Hadamard factorization of
 184`completedRiemannZeta₀`.
 185
 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) :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.