 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) →
 220      Summable (fun n => ‖z n‖ ^ 2) →
 221        Summable (fun n => E1 (z n) - 1)
 222  multipliability_from_sq :
 223    ∀ z : ℕ → ℂ, (∀ n, ‖z n‖ ≤ 1) →
 224      Summable (fun n => ‖z n‖ ^ 2) →
 225        Multipliable (fun n => E1 (z n))
 226  open_xi_identification : XiHadamardIdentification → Prop
 227
 228def hadamardGenusOneStatus : HadamardGenusOneStatus where
 229  per_factor_estimate := norm_E1_sub_one_le
 230  summability_from_sq := summable_E1_sub_one_of_summable_sq
 231  multipliability_from_sq := multipliable_E1_of_summable_sq
 232  open_xi_identification := fun _ => True
 233
 234end
 235
 236end HadamardGenusOne
 237end NumberTheory
 238end IndisputableMonolith

papers checked against this theorem

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