CompletedZetaHadamardProduct

formal source

  63with the required convergence properties, and that the corresponding genus-one
  64partial products converge to the pole-removed completed zeta up to `exp(A+B s)`.
  65-/
  66structure CompletedZetaHadamardProduct where
  67  zeros : ℕ → ℂ
  68  zero_ne_zero : ∀ n : ℕ, zeros n ≠ 0
  69  A : ℂ
  70  B : ℂ
  71  productLimit : ℂ → ℂ
  72  partial_products_converge :
  73    ∀ s : ℂ,
  74      Filter.Tendsto
  75        (fun N : ℕ => hadamardPartialProduct zeros s N)
  76        Filter.atTop
  77        (nhds (productLimit s))
  78  completedZeta0_eq_hadamard :
  79    ∀ s : ℂ,
  80      completedRiemannZeta₀ s =
  81        Complex.exp (A + B * s) * productLimit s
  82
  83/-- Once Hadamard product data is supplied, the pole-removed completed zeta has
  84the expected genus-one factorization. -/
  85theorem completedRiemannZeta0_hadamard_product
  86    (data : CompletedZetaHadamardProduct) (s : ℂ) :
  87    completedRiemannZeta₀ s =
  88      Complex.exp (data.A + data.B * s) * data.productLimit s :=
  89  data.completedZeta0_eq_hadamard s
  90
  91/-! ## 4. Track D attack surface -/
  92
  93/-- Practical Track D bundle: the proved Mathlib inputs plus the open Hadamard
  94product data type. -/
  95structure HadamardFactorizationStatus where
  96  completed_zeta0_entire :