 166/-- `XiOrderBound`: `completedRiemannZeta₀` has order ≤ 1. Standard classical
 167fact (Stirling on the gamma factor + bounds on ζ in vertical strips), not yet
 168in Mathlib. -/
 169def XiOrderBound : Prop :=
 170  ∃ C K : ℝ, 0 < C ∧ 0 < K ∧
 171    ∀ s : ℂ, K ≤ ‖s‖ →
 172      ‖completedRiemannZeta₀ s‖ ≤ Real.exp (C * ‖s‖)
 173
 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

papers checked against this theorem

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