LocalSplittingHypothesis

formal source

  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. -/
  89theorem completedRiemannZeta0_local_split_regularTail
  90    (k : ℕ) (s : ℂ)
  91    (hsplit : LocalSplittingHypothesis H k s) :
  92    completedRiemannZeta₀ s =
  93      E1 (s / H.zeros k) * regularTail H k s := by
  94  rw [completedRiemannZeta0_local_split H k s hsplit, regularTail]
  95  ring
  96
  97/-! ## 4. Status -/
  98
  99/-- Track-D regular-tail status bundle. The local-split decomposition is