twistedPrimeCostSum

formal source

 117
 118    Defined as a finite sum over primes ≤ N (using the fact that
 119    `Nat.primesBelow` returns the finset of primes below N). -/
 120def twistedPrimeCostSum (chi : ℕ → ℝ) (N : ℕ) : ℝ :=
 121  (Finset.range (N + 1)).sum fun p =>
 122    if Nat.Prime p then primeCost p * chi p else 0
 123
 124@[simp]
 125theorem twistedPrimeCostSum_zero (chi : ℕ → ℝ) :
 126    twistedPrimeCostSum chi 0 = 0 := by
 127  simp [twistedPrimeCostSum, Nat.not_prime_zero]
 128
 129/-- For the trivial character, the twisted prime cost sum equals the
 130    untwisted version. -/
 131theorem twistedPrimeCostSum_one_char (N : ℕ) :
 132    twistedPrimeCostSum (fun _ => 1) N
 133      = (Finset.range (N + 1)).sum fun p =>
 134          if Nat.Prime p then primeCost p else 0 := by
 135  unfold twistedPrimeCostSum
 136  congr 1
 137  ext p
 138  by_cases hp : Nat.Prime p
 139  · simp [hp]
 140  · simp [hp]
 141
 142/-! ## Master certificate -/
 143
 144/-- Master certificate: the elementary properties of the cost-twisted
 145    arithmetic function. -/
 146theorem cost_twisted_certificate :
 147    -- (1) Twisted cost is zero at n = 1.
 148    (∀ (chi : ℕ → ℝ), twistedCostSpectrumValue chi 1 = 0) ∧
 149    -- (2) Twisted cost is completely additive over positive products.
 150    (∀ (chi : ℕ → ℝ) {m n : ℕ}, m ≠ 0 → n ≠ 0 →