twistedCostSpectrumValue_one_char

formal source

  90
  91/-- For the trivial character `chi = 1`, the twisted cost spectrum value
  92    reduces to the standard cost spectrum value. -/
  93theorem twistedCostSpectrumValue_one_char (n : ℕ) :
  94    twistedCostSpectrumValue (fun _ => 1) n = costSpectrumValue n := by
  95  unfold twistedCostSpectrumValue costSpectrumValue twistedPrimeCost
  96  refine Finsupp.sum_congr ?_
  97  intro p _
  98  ring
  99
 100/-- Negating the character flips the sign of the twisted cost. -/
 101theorem twistedCostSpectrumValue_eq_neg (chi : ℕ → ℝ) (n : ℕ) :
 102    twistedCostSpectrumValue (fun p => -chi p) n
 103      = -twistedCostSpectrumValue chi n := by
 104  unfold twistedCostSpectrumValue twistedPrimeCost
 105  rw [Finsupp.sum, Finsupp.sum]
 106  rw [← Finset.sum_neg_distrib]
 107  apply Finset.sum_congr rfl
 108  intro p _
 109  ring
 110
 111/-! ## The twisted prime cost sum
 112
 113The twisted analog of the prime cost sum `Π(x)`. -/
 114
 115/-- The twisted prime cost sum:
 116    `Π_chi(x) := Σ_{p ≤ x prime} J(p) · chi(p)`.
 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