IndisputableMonolith.NumberTheory.EulerProductEqualsZeta

   1import Mathlib.NumberTheory.EulerProduct.DirichletLSeries
   2import IndisputableMonolith.NumberTheory.EulerLedgerPartition
   3import IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom
   4
   5/-!
   6  EulerProductEqualsZeta.lean
   7
   8  Phase 1 of the RS-native zeta program.
   9
  10  This module wires the formal RS prime-ledger partition to Mathlib's
  11  theorem that the Euler product over primes equals the Riemann zeta function
  12  on the half-plane `Re(s) > 1`.
  13
  14  The point is not to reprove analytic continuation here. The point is to
  15  replace the old `True` stub in `EulerLedgerPartitionCert` with a real
  16  analytic theorem: the Euler product over prime ledger atoms converges to
  17  `riemannZeta` in the domain where the product is classically valid.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace NumberTheory
  22namespace EulerProductEqualsZeta
  23
  24open Filter Topology
  25open LogicPrimeLedgerAtom
  26
  27noncomputable section
  28
  29/-- The Mathlib Euler product theorem for `riemannZeta`, restated under the
  30RS prime-ledger namespace. This is the convergence of finite prime partial
  31products to `riemannZeta s` on `Re(s) > 1`. -/
  32theorem rs_riemannZeta_eulerProduct_tendsto (s : ℂ) (hs : 1 < s.re) :
  33    Tendsto (fun n : ℕ ↦ ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹)
  34      atTop (𝓝 (riemannZeta s)) :=
  35  _root_.riemannZeta_eulerProduct hs
  36
  37/-- The equivalent infinite-product statement. -/
  38theorem rs_riemannZeta_eulerProduct_tprod (s : ℂ) (hs : 1 < s.re) :
  39    ∏' p : Nat.Primes, (1 - (p : ℂ) ^ (-s))⁻¹ = riemannZeta s :=
  40  _root_.riemannZeta_eulerProduct_tprod hs
  41
  42/-- `HasProd` form of the same theorem. -/
  43theorem rs_riemannZeta_eulerProduct_hasProd (s : ℂ) (hs : 1 < s.re) :
  44    HasProd (fun p : Nat.Primes ↦ (1 - (p : ℂ) ^ (-s))⁻¹) (riemannZeta s) :=
  45  _root_.riemannZeta_eulerProduct_hasProd hs
  46
  47/-- The finite prime-ledger partition is exactly Mathlib's finite Euler
  48partial product over `Nat.primesBelow n`. -/
  49theorem finitePrimeLedgerPartition_primesBelow (s : ℂ) (n : ℕ) :
  50    finitePrimeLedgerPartition s (Nat.primesBelow n) =
  51      ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹ := by
  52  unfold finitePrimeLedgerPartition primeLedgerLocalPartition primePostingWeight
  53  apply Finset.prod_congr rfl
  54  intro p hp
  55  have hprime : Nat.Prime p := by
  56    exact (Nat.mem_primesBelow.mp hp).2
  57  simp [hprime]
  58
  59/-- The RS finite prime-ledger partitions converge to `riemannZeta` on
  60`Re(s) > 1`. This is the ledger reading of Mathlib's Euler product theorem. -/
  61theorem ledger_partition_equals_zeta (s : ℂ) (hs : 1 < s.re) :
  62    Tendsto (fun n : ℕ ↦ finitePrimeLedgerPartition s (Nat.primesBelow n))
  63      atTop (𝓝 (riemannZeta s)) := by
  64  simpa [finitePrimeLedgerPartition_primesBelow] using
  65    rs_riemannZeta_eulerProduct_tendsto s hs
  66
  67/-- The recovered-prime ledger is compatible with the analytic Euler product:
  68prime postings in the recovered ledger transport to the classical prime
  69factors used by Mathlib's Euler product. -/
  70theorem recovered_prime_ledger_supports_euler_product :
  71    PrimeLedgerLogicCert ∧
  72      (∀ s : ℂ, 1 < s.re →
  73        Tendsto (fun n : ℕ ↦ finitePrimeLedgerPartition s (Nat.primesBelow n))
  74          atTop (𝓝 (riemannZeta s))) :=
  75  ⟨primeLedgerLogicCert, ledger_partition_equals_zeta⟩
  76
  77end
  78
  79end EulerProductEqualsZeta
  80end NumberTheory
  81end IndisputableMonolith
  82