IndisputableMonolith.NumberTheory.HadamardRegularTail

   1import IndisputableMonolith.NumberTheory.HadamardGenusOne
   2
   3/-!
   4  HadamardRegularTail.lean
   5
   6  From a `XiHadamardIdentification` we want to split `ξ₀` at any chosen
   7  zero index `k` into a local elementary factor `E₁(s/zeros k)` and a
   8  regular tail consisting of the remaining genus-one product times the
   9  exponential prefactor.
  10
  11  Mathlib's `Multipliable.tprod_eq_mul_tprod_ite` applies to commutative
  12  groups; `ℂ` under multiplication is only a commutative monoid (it has
  13  zero), and the monoid version `Multipliable.tprod_eq_mul_tprod_ite'`
  14  requires a separately-supplied multipliability hypothesis for the
  15  "skipped" product.
  16
  17  This module defines the regular tail and packages the local-split
  18  identity as the named hypothesis a future analytic Lean step needs to
  19  inhabit:
  20
  21  * `regularTail H k s`            : the genus-one product over indices
  22                                     `≠ k`, times `exp(A + B s)`.
  23  * `LocalSplittingHypothesis H k s`: states that the genus-one product
  24                                     factors as
  25                                     `E₁(s / zeros k) * skipped product`
  26                                     at the given `s`. Provable from
  27                                     `Multipliable (fun n => E₁(s / zeros n))`
  28                                     and `Multipliable (update _ k 1)`.
  29  * `completedRiemannZeta0_local_split` : the consequence on `ξ₀`.
  30
  31  Two pieces are intentionally not provided:
  32
  33  * Global cost domination on the strip. As shown in
  34    `EnergyBudgetDecomposition.lean` and `AnalyticTrace.lean`, the bridge
  35    `HonestPhaseCostBridge` is RH-equivalent. A global cost bound coming
  36    from these data alone is therefore not derivable without further
  37    analytic content (the explicit formula).
  38  * Holomorphy of the regular tail. This needs uniform-on-compact-set
  39    convergence of the truncated products.
  40-/
  41
  42namespace IndisputableMonolith
  43namespace NumberTheory
  44namespace HadamardRegularTail
  45
  46open HadamardGenusOne
  47
  48noncomputable section
  49
  50variable (H : XiHadamardIdentification)
  51
  52/-! ## 1. The regular tail -/
  53
  54/-- The Hadamard regular tail at index `k` and point `s`: the genus-one
  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. -/
  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
 100theorem-grade given the local splitting hypothesis. The remaining open
 101content (proving the local splitting unconditionally on `ℂ` and the global
 102cost domination) is documented as named follow-on work. -/
 103structure HadamardRegularTailStatus where
 104  splitting :
 105    ∀ (k : ℕ) (s : ℂ),
 106      LocalSplittingHypothesis H k s →
 107        completedRiemannZeta₀ s =
 108          E1 (s / H.zeros k) * regularTail H k s
 109
 110def hadamardRegularTailStatus : HadamardRegularTailStatus H where
 111  splitting := completedRiemannZeta0_local_split_regularTail H
 112
 113end
 114
 115end HadamardRegularTail
 116end NumberTheory
 117end IndisputableMonolith
 118