regularTail

formal source

  55product over all zeros except the one at index `k`, times the exponential
  56prefactor. The product is written using `ite (n = k) 1 _` to align with
  57Mathlib's `Multipliable.tprod_eq_mul_tprod_ite'` API. -/
  58def regularTail (k : ℕ) (s : ℂ) : ℂ :=
  59  Complex.exp (H.A + H.B * s) *
  60    ∏' n, ite (n = k) 1 (E1 (s / H.zeros n))
  61
  62/-! ## 2. The local splitting hypothesis -/
  63
  64/-- Local splitting of the genus-one product at index `k` and point `s`.
  65This isolates the single-factor extraction:
  66`∏' n, E₁(s / zeros n) = E₁(s / zeros k) * ∏' n, ite (n = k) 1 (E₁ ⋯)`.
  67On `ℂ`, this follows from Mathlib's `Multipliable.tprod_eq_mul_tprod_ite'`
  68once a multipliability hypothesis for the skipped product is supplied. -/
  69def LocalSplittingHypothesis (k : ℕ) (s : ℂ) : Prop :=
  70  (∏' n, E1 (s / H.zeros n)) =
  71    E1 (s / H.zeros k) *
  72      ∏' n, ite (n = k) 1 (E1 (s / H.zeros n))
  73
  74/-! ## 3. Consequences -/
  75
  76/-- The Hadamard product factorization in the local-split form, given the
  77local splitting hypothesis. -/
  78theorem completedRiemannZeta0_local_split
  79    (k : ℕ) (s : ℂ)
  80    (hsplit : LocalSplittingHypothesis H k s) :
  81    completedRiemannZeta₀ s =
  82      Complex.exp (H.A + H.B * s) *
  83        E1 (s / H.zeros k) *
  84          ∏' n, ite (n = k) 1 (E1 (s / H.zeros n)) := by
  85  rw [completedRiemannZeta0_genus_one_factorization H s, hsplit]
  86  ring
  87
  88/-- Equivalent form using the regular tail. -/