twistedCostSpectrumValue_mul

formal source

  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
  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 _