IndisputableMonolith.NumberTheory.HadamardFactorization

   1import IndisputableMonolith.NumberTheory.ZetaFromTheta
   2
   3/-!
   4  HadamardFactorization.lean
   5
   6  Track D of the RH unconditional-closure plan.
   7
   8  Mathlib gives the completed zeta function and the entire pole-removed
   9  function `completedRiemannZeta₀`, together with differentiability and the
  10  functional equation. It does not currently provide a Hadamard product for
  11  `completedRiemannZeta₀`.
  12
  13  This module introduces the product interface needed by later explicit-formula
  14  work. It defines the genus-one primary factor and finite partial products,
  15  then states the exact data required to identify their limit with
  16  `completedRiemannZeta₀`.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace NumberTheory
  21namespace HadamardFactorization
  22
  23open Filter
  24
  25noncomputable section
  26
  27/-! ## 1. Mathlib facts available for the pole-removed completed zeta -/
  28
  29/-- Completed zeta with poles removed is differentiable everywhere in Mathlib. -/
  30theorem completedZeta0_differentiable :
  31    Differentiable ℂ completedRiemannZeta₀ :=
  32  differentiable_completedZeta₀
  33
  34/-- The pole-removed completed zeta has the same functional equation. -/
  35theorem completedZeta0_functional_equation (s : ℂ) :
  36    completedRiemannZeta₀ s = completedRiemannZeta₀ (1 - s) :=
  37  (completedRiemannZeta₀_one_sub s).symm
  38
  39/-! ## 2. Genus-one Hadamard factors -/
  40
  41/-- The genus-one elementary Hadamard factor `E₁(z) = (1-z) exp(z)`. -/
  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)
  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
  83/-- Once Hadamard product data is supplied, the pole-removed completed zeta has
  84the expected genus-one factorization. -/
  85theorem completedRiemannZeta0_hadamard_product
  86    (data : CompletedZetaHadamardProduct) (s : ℂ) :
  87    completedRiemannZeta₀ s =
  88      Complex.exp (data.A + data.B * s) * data.productLimit s :=
  89  data.completedZeta0_eq_hadamard s
  90
  91/-! ## 4. Track D attack surface -/
  92
  93/-- Practical Track D bundle: the proved Mathlib inputs plus the open Hadamard
  94product data type. -/
  95structure HadamardFactorizationStatus where
  96  completed_zeta0_entire :
  97    Differentiable ℂ completedRiemannZeta₀
  98  completed_zeta0_functional_equation :
  99    ∀ s : ℂ, completedRiemannZeta₀ s = completedRiemannZeta₀ (1 - s)
 100  hadamard_data_to_product :
 101    ∀ data : CompletedZetaHadamardProduct,
 102      ∀ s : ℂ,
 103        completedRiemannZeta₀ s =
 104          Complex.exp (data.A + data.B * s) * data.productLimit s
 105
 106def hadamardFactorizationStatus : HadamardFactorizationStatus where
 107  completed_zeta0_entire := completedZeta0_differentiable
 108  completed_zeta0_functional_equation := completedZeta0_functional_equation
 109  hadamard_data_to_product := completedRiemannZeta0_hadamard_product
 110
 111end
 112
 113end HadamardFactorization
 114end NumberTheory
 115end IndisputableMonolith
 116