eulerLedgerPartitionCert

formal source

  73/-- The structural Euler ledger certificate.  The analytic equality field now
  74uses Mathlib's Euler-product theorem for `riemannZeta` on `Re(s) > 1`; the
  75finite products are exactly the finite prime-ledger partitions. -/
  76def eulerLedgerPartitionCert : EulerLedgerPartitionCert where
  77  eulerProduct_eq_zeta := by
  78    intro s hs
  79    have hmathlib :
  80        Filter.Tendsto (fun n : ℕ ↦ ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹)
  81          Filter.atTop (𝓝 (riemannZeta s)) :=
  82      _root_.riemannZeta_eulerProduct hs
  83    have hpart : (fun n : ℕ ↦ finitePrimeLedgerPartition s (Nat.primesBelow n)) =
  84        (fun n : ℕ ↦ ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹) := by
  85      funext n
  86      unfold finitePrimeLedgerPartition primeLedgerLocalPartition primePostingWeight
  87      apply Finset.prod_congr rfl
  88      intro p hp
  89      have hprime : Nat.Prime p := (Nat.mem_primesBelow.mp hp).2
  90      simp [hprime]
  91    simpa [hpart] using hmathlib
  92  formal_partition := primeLedgerPartition_formal
  93  prime_atoms := primeLedgerCert
  94
  95end
  96
  97end NumberTheory
  98end IndisputableMonolith