hadamardE1_zero

formal source

  42def hadamardE1 (z : ℂ) : ℂ :=
  43  (1 - z) * Complex.exp z
  44
  45@[simp] theorem hadamardE1_zero : hadamardE1 0 = 1 := by
  46  simp [hadamardE1]
  47
  48/-- The finite genus-one product over the first `N` listed zeros. -/
  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)