twistedCostSpectrumValue_prime

formal source

  58  simp [Nat.factorization_zero]
  59
  60/-- For a prime `p`, the twisted cost is `J(p) · chi(p)`. -/
  61theorem twistedCostSpectrumValue_prime (chi : ℕ → ℝ) {p : ℕ}
  62    (hp : Nat.Prime p) :
  63    twistedCostSpectrumValue chi p = primeCost p * chi p := by
  64  unfold twistedCostSpectrumValue twistedPrimeCost
  65  rw [Nat.Prime.factorization hp]
  66  simp [Finsupp.sum_single_index]
  67
  68/-- For a prime power `p^k`, the twisted cost is `k · J(p) · chi(p)`. -/
  69theorem twistedCostSpectrumValue_pow (chi : ℕ → ℝ) {p k : ℕ}
  70    (hp : Nat.Prime p) :
  71    twistedCostSpectrumValue chi (p ^ k) = (k : ℝ) * (primeCost p * chi p) := by
  72  unfold twistedCostSpectrumValue twistedPrimeCost
  73  rw [Nat.Prime.factorization_pow hp]
  74  simp [Finsupp.sum_single_index]
  75
  76/-- The twisted cost is completely additive over coprime products.
  77    This generalizes `costSpectrumValue_mul`. -/
  78theorem twistedCostSpectrumValue_mul (chi : ℕ → ℝ) {m n : ℕ}
  79    (hm : m ≠ 0) (hn : n ≠ 0) :
  80    twistedCostSpectrumValue chi (m * n)
  81      = twistedCostSpectrumValue chi m + twistedCostSpectrumValue chi n := by
  82  unfold twistedCostSpectrumValue
  83  rw [Nat.factorization_mul hm hn]
  84  rw [Finsupp.sum_add_index']
  85  · intro p
  86    simp
  87  · intro p i j
  88    push_cast
  89    ring
  90
  91/-- For the trivial character `chi = 1`, the twisted cost spectrum value