hadamardPartialProduct_zero

formal source

  49def hadamardPartialProduct (zeros : ℕ → ℂ) (s : ℂ) (N : ℕ) : ℂ :=
  50  ∏ n ∈ Finset.range N, hadamardE1 (s / zeros n)
  51
  52@[simp] theorem hadamardPartialProduct_zero
  53    (zeros : ℕ → ℂ) (N : ℕ) :
  54    hadamardPartialProduct zeros 0 N = 1 := by
  55  simp [hadamardPartialProduct]
  56
  57/-! ## 3. Exact Hadamard product data needed downstream -/
  58
  59/-- Hadamard product data for the pole-removed completed zeta.
  60
  61This is the real Track D target. The missing analytic work is the proof that
  62`completedRiemannZeta₀` has order at most one, that its zeros can be enumerated
  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