def
definition
def or abbrev
eulerLedgerPartitionCert
show as:
view Lean formalization →
formal statement (Lean)
76def eulerLedgerPartitionCert : EulerLedgerPartitionCert where
77 eulerProduct_eq_zeta := by
proof body
Definition body.
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