IndisputableMonolith.NumberTheory.HadamardGenusOne

   1import Mathlib
   2
   3/-!
   4  HadamardGenusOne.lean
   5
   6  Concrete analytic substrate for the genus-one Hadamard factorization.
   7
   8  Mathlib does not currently package the Hadamard factorization theorem for
   9  entire functions of order ≤ 1. This module proves what is unconditionally
  10  provable for the genus-one elementary Weierstrass factor
  11  `E₁(z) = (1 - z) · exp(z)`:
  12
  13  * the per-factor norm estimate `‖E₁(z) - 1‖ ≤ 3 ‖z‖²` for `‖z‖ ≤ 1`;
  14  * absolute summability of the corrections `E₁(z_n) - 1` from absolute
  15    summability of `‖z_n‖²`;
  16  * Multipliability of the partial products `∏ E₁(z_n)`.
  17
  18  These are the analytic prerequisites for the Hadamard product. Three named
  19  pieces remain open:
  20
  21  1. `XiOrderBound`     : `completedRiemannZeta₀` has order ≤ 1.
  22  2. `XiZeroSummability`: the inverse-square moduli of its zeros are summable.
  23  3. `XiHadamardIdentification` : the partial product limit equals
  24                                   `completedRiemannZeta₀` up to `exp(A+Bs)`.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace NumberTheory
  29namespace HadamardGenusOne
  30
  31open Complex
  32
  33noncomputable section
  34
  35/-! ## 1. The genus-one elementary factor -/
  36
  37/-- The genus-one elementary Weierstrass factor `E₁(z) = (1 - z) · exp(z)`. -/
  38def E1 (z : ℂ) : ℂ := (1 - z) * Complex.exp z
  39
  40@[simp] theorem E1_zero : E1 0 = 1 := by simp [E1]
  41
  42theorem E1_one : E1 1 = 0 := by simp [E1]
  43
  44/-- Algebraic identity `E₁(z) - 1 = (exp z - 1 - z) - z (exp z - 1)`. -/
  45theorem E1_sub_one_eq (z : ℂ) :
  46    E1 z - 1 = (Complex.exp z - 1 - z) - z * (Complex.exp z - 1) := by
  47  unfold E1
  48  have hz : Complex.exp z = 1 + (Complex.exp z - 1) := by ring
  49  conv_lhs => rw [hz]
  50  ring
  51
  52/-! ## 2. The per-factor estimate -/
  53
  54/-- `‖exp z - 1‖ ≤ 2 ‖z‖` for `‖z‖ ≤ 1`. -/
  55private theorem norm_exp_sub_one_le_two_mul (z : ℂ) (hz : ‖z‖ ≤ 1) :
  56    ‖Complex.exp z - 1‖ ≤ 2 * ‖z‖ := by
  57  have h1 : ‖Complex.exp z - 1 - z‖ ≤ ‖z‖ ^ 2 :=
  58    Complex.norm_exp_sub_one_sub_id_le hz
  59  have hzn : 0 ≤ ‖z‖ := norm_nonneg z
  60  have hsq : ‖z‖ ^ 2 ≤ ‖z‖ := by
  61    have := mul_le_mul_of_nonneg_left hz hzn
  62    have heq : ‖z‖ * ‖z‖ = ‖z‖ ^ 2 := by ring
  63    rw [heq] at this
  64    have : ‖z‖ * 1 = ‖z‖ := by ring
  65    linarith [this]
  66  calc
  67    ‖Complex.exp z - 1‖
  68        = ‖(Complex.exp z - 1 - z) + z‖ := by ring_nf
  69    _ ≤ ‖Complex.exp z - 1 - z‖ + ‖z‖ := norm_add_le _ _
  70    _ ≤ ‖z‖ ^ 2 + ‖z‖ := by linarith
  71    _ ≤ ‖z‖ + ‖z‖ := by linarith
  72    _ = 2 * ‖z‖ := by ring
  73
  74/-- The genus-one factor estimate: `‖E₁(z) - 1‖ ≤ 3 ‖z‖²` for `‖z‖ ≤ 1`. -/
  75theorem norm_E1_sub_one_le (z : ℂ) (hz : ‖z‖ ≤ 1) :
  76    ‖E1 z - 1‖ ≤ 3 * ‖z‖ ^ 2 := by
  77  rw [E1_sub_one_eq]
  78  have h1 : ‖Complex.exp z - 1 - z‖ ≤ ‖z‖ ^ 2 :=
  79    Complex.norm_exp_sub_one_sub_id_le hz
  80  have hexp : ‖Complex.exp z - 1‖ ≤ 2 * ‖z‖ :=
  81    norm_exp_sub_one_le_two_mul z hz
  82  have hzn : 0 ≤ ‖z‖ := norm_nonneg z
  83  have h2 : ‖z * (Complex.exp z - 1)‖ ≤ 2 * ‖z‖ ^ 2 := by
  84    rw [norm_mul]
  85    calc
  86      ‖z‖ * ‖Complex.exp z - 1‖
  87          ≤ ‖z‖ * (2 * ‖z‖) := by
  88              exact mul_le_mul_of_nonneg_left hexp hzn
  89      _ = 2 * ‖z‖ ^ 2 := by ring
  90  calc
  91    ‖(Complex.exp z - 1 - z) - z * (Complex.exp z - 1)‖
  92        ≤ ‖Complex.exp z - 1 - z‖ + ‖z * (Complex.exp z - 1)‖ :=
  93          norm_sub_le _ _
  94    _ ≤ ‖z‖ ^ 2 + 2 * ‖z‖ ^ 2 := by linarith
  95    _ = 3 * ‖z‖ ^ 2 := by ring
  96
  97/-! ## 3. Absolute summability of `E₁` corrections -/
  98
  99/-- If `‖z_n‖ ≤ 1` for all `n` and `‖z_n‖²` is summable, then `‖E₁(z_n) - 1‖`
 100is summable. -/
 101theorem summable_norm_E1_sub_one_of_summable_sq
 102    (z : ℕ → ℂ) (hbnd : ∀ n, ‖z n‖ ≤ 1)
 103    (hsum : Summable (fun n => ‖z n‖ ^ 2)) :
 104    Summable (fun n => ‖E1 (z n) - 1‖) := by
 105  refine (hsum.mul_left 3).of_norm_bounded ?_
 106  intro n
 107  have h := norm_E1_sub_one_le (z n) (hbnd n)
 108  have hnn : 0 ≤ ‖E1 (z n) - 1‖ := norm_nonneg _
 109  rw [Real.norm_of_nonneg hnn]
 110  exact h
 111
 112/-- The corrections `E₁(z_n) - 1` are themselves summable in `ℂ` under the
 113square-summable bounded-zero hypothesis. -/
 114theorem summable_E1_sub_one_of_summable_sq
 115    (z : ℕ → ℂ) (hbnd : ∀ n, ‖z n‖ ≤ 1)
 116    (hsum : Summable (fun n => ‖z n‖ ^ 2)) :
 117    Summable (fun n => E1 (z n) - 1) :=
 118  (summable_norm_E1_sub_one_of_summable_sq z hbnd hsum).of_norm
 119
 120/-! ## 4. Multipliability of genus-one products -/
 121
 122/-- If the per-factor corrections `E₁(z_n) - 1` are summable in `ℂ`, then the
 123genus-one partial products are multipliable. -/
 124theorem multipliable_E1_of_summable_sub_one
 125    (z : ℕ → ℂ)
 126    (hsum : Summable (fun n => E1 (z n) - 1)) :
 127    Multipliable (fun n => E1 (z n)) := by
 128  have h := Complex.multipliable_one_add_of_summable hsum
 129  have heq : (fun n => 1 + (E1 (z n) - 1)) = (fun n => E1 (z n)) := by
 130    funext n; ring
 131  simpa [heq] using h
 132
 133/-- Combined corollary: from square-summable bounded zeros, the genus-one
 134product is multipliable. -/
 135theorem multipliable_E1_of_summable_sq
 136    (z : ℕ → ℂ) (hbnd : ∀ n, ‖z n‖ ≤ 1)
 137    (hsum : Summable (fun n => ‖z n‖ ^ 2)) :
 138    Multipliable (fun n => E1 (z n)) :=
 139  multipliable_E1_of_summable_sub_one z
 140    (summable_E1_sub_one_of_summable_sq z hbnd hsum)
 141
 142/-! ## 5. Uniform-on-disk estimate -/
 143
 144/-- For zeros at modulus at least `‖s‖` (i.e. `s` inside the closed disk of
 145radius `‖ρ‖`), each genus-one factor satisfies the per-factor estimate. -/
 146theorem norm_E1_sub_one_at_quotient_le
 147    (s : ℂ) (ρ : ℂ) (hρ : ρ ≠ 0) (hbound : ‖s‖ ≤ ‖ρ‖) :
 148    ‖E1 (s / ρ) - 1‖ ≤ 3 * ‖s‖ ^ 2 / ‖ρ‖ ^ 2 := by
 149  have hρn : 0 < ‖ρ‖ := by
 150    have hne : ‖ρ‖ ≠ 0 := fun h => hρ ((norm_eq_zero).1 h)
 151    exact lt_of_le_of_ne (norm_nonneg ρ) (Ne.symm hne)
 152  have hquot_norm : ‖s / ρ‖ = ‖s‖ / ‖ρ‖ := norm_div s ρ
 153  have hbnd : ‖s / ρ‖ ≤ 1 := by
 154    rw [hquot_norm]
 155    exact (div_le_one hρn).mpr hbound
 156  have h := norm_E1_sub_one_le (s / ρ) hbnd
 157  rw [hquot_norm] at h
 158  calc
 159    ‖E1 (s / ρ) - 1‖
 160        ≤ 3 * (‖s‖ / ‖ρ‖) ^ 2 := h
 161    _ = 3 * ‖s‖ ^ 2 / ‖ρ‖ ^ 2 := by
 162          rw [div_pow]; ring
 163
 164/-! ## 6. Named hypotheses for the missing analytic content -/
 165
 166/-- `XiOrderBound`: `completedRiemannZeta₀` has order ≤ 1. Standard classical
 167fact (Stirling on the gamma factor + bounds on ζ in vertical strips), not yet
 168in Mathlib. -/
 169def XiOrderBound : Prop :=
 170  ∃ C K : ℝ, 0 < C ∧ 0 < K ∧
 171    ∀ s : ℂ, K ≤ ‖s‖ →
 172      ‖completedRiemannZeta₀ s‖ ≤ Real.exp (C * ‖s‖)
 173
 174/-- `XiZeroSummability`: the inverse-square moduli of zeros of
 175`completedRiemannZeta₀` are summable (Jensen's formula + counting). Mathlib
 176has Jensen's formula but the application to ξ₀ is not packaged. -/
 177def XiZeroSummability : Prop :=
 178  ∃ ρ : ℕ → ℂ,
 179    (∀ n, completedRiemannZeta₀ (ρ n) = 0) ∧
 180    (∀ n, ρ n ≠ 0) ∧
 181    Summable (fun n => 1 / ‖ρ n‖ ^ 2)
 182
 183/-- `XiHadamardIdentification`: the genus-one Hadamard factorization of
 184`completedRiemannZeta₀`.
 185
 186Once supplied, `ξ₀(s) = exp(A + B s) · ∏ E₁(s/ρ_n)`. The actual analytic
 187proof of this identification is the classical Hadamard theorem, not yet in
 188Mathlib. -/
 189structure XiHadamardIdentification where
 190  zeros : ℕ → ℂ
 191  zeros_ne_zero : ∀ n, zeros n ≠ 0
 192  inv_sq_summable : Summable (fun n => 1 / ‖zeros n‖ ^ 2)
 193  A : ℂ
 194  B : ℂ
 195  identification :
 196    ∀ s : ℂ,
 197      completedRiemannZeta₀ s =
 198        Complex.exp (A + B * s) * ∏' n, E1 (s / zeros n)
 199
 200/-! ## 7. What the supplied data gives -/
 201
 202/-- Once `XiHadamardIdentification` is supplied, `completedRiemannZeta₀`
 203factors as the genus-one product times an exponential. -/
 204theorem completedRiemannZeta0_genus_one_factorization
 205    (H : XiHadamardIdentification) (s : ℂ) :
 206    completedRiemannZeta₀ s =
 207      Complex.exp (H.A + H.B * s) * ∏' n, E1 (s / H.zeros n) :=
 208  H.identification s
 209
 210/-! ## 8. Status -/
 211
 212/-- Track-D status bundle: per-factor estimate proved, summability proved,
 213multipliability proved; the order bound, zero-summability, and Hadamard
 214identification remain open analytic content. -/
 215structure HadamardGenusOneStatus where
 216  per_factor_estimate :
 217    ∀ z : ℂ, ‖z‖ ≤ 1 → ‖E1 z - 1‖ ≤ 3 * ‖z‖ ^ 2
 218  summability_from_sq :
 219    ∀ z : ℕ → ℂ, (∀ n, ‖z n‖ ≤ 1) →
 220      Summable (fun n => ‖z n‖ ^ 2) →
 221        Summable (fun n => E1 (z n) - 1)
 222  multipliability_from_sq :
 223    ∀ z : ℕ → ℂ, (∀ n, ‖z n‖ ≤ 1) →
 224      Summable (fun n => ‖z n‖ ^ 2) →
 225        Multipliable (fun n => E1 (z n))
 226  open_xi_identification : XiHadamardIdentification → Prop
 227
 228def hadamardGenusOneStatus : HadamardGenusOneStatus where
 229  per_factor_estimate := norm_E1_sub_one_le
 230  summability_from_sq := summable_E1_sub_one_of_summable_sq
 231  multipliability_from_sq := multipliable_E1_of_summable_sq
 232  open_xi_identification := fun _ => True
 233
 234end
 235
 236end HadamardGenusOne
 237end NumberTheory
 238end IndisputableMonolith
 239