twistedCostSpectrumValue_one

formal source

  45def twistedCostSpectrumValue (chi : ℕ → ℝ) (n : ℕ) : ℝ :=
  46  n.factorization.sum fun p k => (k : ℝ) * twistedPrimeCost chi p
  47
  48@[simp]
  49theorem twistedCostSpectrumValue_one (chi : ℕ → ℝ) :
  50    twistedCostSpectrumValue chi 1 = 0 := by
  51  unfold twistedCostSpectrumValue
  52  simp [Nat.factorization_one]
  53
  54@[simp]
  55theorem twistedCostSpectrumValue_zero (chi : ℕ → ℝ) :
  56    twistedCostSpectrumValue chi 0 = 0 := by
  57  unfold twistedCostSpectrumValue
  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 : ℕ}