primePostingWeight

formal source

  22noncomputable section
  23
  24/-- One prime posting weighted at complex scale `s`. -/
  25def primePostingWeight (s : ℂ) (p : ℕ) : ℂ :=
  26  (p : ℂ) ^ (-s)
  27
  28/-- Local geometric partition attached to one prime ledger atom. -/
  29def primeLedgerLocalPartition (s : ℂ) (p : ℕ) : ℂ :=
  30  (1 - primePostingWeight s p)⁻¹
  31
  32/-- A finite prime-ledger partition over a finite set of primes. -/
  33def finitePrimeLedgerPartition (s : ℂ) (S : Finset ℕ) : ℂ :=
  34  ∏ p ∈ S, if Nat.Prime p then primeLedgerLocalPartition s p else 1
  35
  36/-- Finite prime-ledger partition is insensitive to non-prime entries. -/
  37theorem finitePrimeLedgerPartition_insert_nonprime
  38    (s : ℂ) (S : Finset ℕ) {n : ℕ} (hnS : n ∉ S) (hn : ¬ Nat.Prime n) :
  39    finitePrimeLedgerPartition s (insert n S) = finitePrimeLedgerPartition s S := by
  40  unfold finitePrimeLedgerPartition
  41  simp [hnS, hn]
  42
  43/-- Inserting a new prime multiplies the partition by its local factor. -/
  44theorem finitePrimeLedgerPartition_insert_prime
  45    (s : ℂ) (S : Finset ℕ) {p : ℕ} (hpS : p ∉ S) (hp : Nat.Prime p) :
  46    finitePrimeLedgerPartition s (insert p S) =
  47      primeLedgerLocalPartition s p * finitePrimeLedgerPartition s S := by
  48  unfold finitePrimeLedgerPartition
  49  simp [hpS, hp]
  50
  51/-- The Euler ledger partition as a formal infinite product over prime atoms. -/
  52def PrimeLedgerPartition (s : ℂ) : Prop :=
  53  ∃ F : (Finset ℕ → ℂ), ∀ S, F S = finitePrimeLedgerPartition s S
  54
  55/-- The formal partition exists, by finite partial products. -/