structure
definition
def or abbrev
EulerLedgerPartitionCert
show as:
view Lean formalization →
formal statement (Lean)
61structure EulerLedgerPartitionCert where
62 /-- Euler product agrees with `riemannZeta` for `Re(s) > 1`, expressed as
63 convergence of finite prime-ledger partitions. -/
64 eulerProduct_eq_zeta :
65 ∀ s : ℂ, 1 < s.re →
66 Filter.Tendsto (fun n : ℕ ↦ finitePrimeLedgerPartition s (Nat.primesBelow n))
67 Filter.atTop (𝓝 (riemannZeta s))
68 /-- The formal prime-ledger partition exists at every complex scale. -/
69 formal_partition : ∀ s : ℂ, PrimeLedgerPartition s
70 /-- Primes are exactly the ledger atoms. -/
71 prime_atoms : PrimeLedgerCert
72
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. -/