 129/-- The total cost of an integer `n`, defined via its prime factorization:
 130    `c(n) = Σ_{p^k ‖ n} k · J(p)`.
 131    By convention `c(0) = 0`. -/
 132def costSpectrumValue (n : ℕ) : ℝ :=
 133  n.factorization.sum fun p k => (k : ℝ) * primeCost p
 134
 135@[simp]
 136theorem costSpectrumValue_one : costSpectrumValue 1 = 0 := by
 137  unfold costSpectrumValue
 138  simp [Nat.factorization_one]
 139
 140@[simp]
 141theorem costSpectrumValue_zero : costSpectrumValue 0 = 0 := by
 142  unfold costSpectrumValue
 143  simp [Nat.factorization_zero]
 144
 145/-- For a prime `p`, `c(p) = J(p)`. -/
 146theorem costSpectrumValue_prime {p : ℕ} (hp : Nat.Prime p) :
 147    costSpectrumValue p = primeCost p := by
 148  unfold costSpectrumValue
 149  rw [Nat.Prime.factorization hp]
 150  simp [Finsupp.sum_single_index]
 151
 152/-- For a prime power `p^k`, `c(p^k) = k · J(p)`. -/
 153theorem costSpectrumValue_pow {p k : ℕ} (hp : Nat.Prime p) :
 154    costSpectrumValue (p ^ k) = (k : ℝ) * primeCost p := by
 155  unfold costSpectrumValue
 156  rw [Nat.Prime.factorization_pow hp]
 157  simp [Finsupp.sum_single_index]
 158
 159/-- The cost is completely additive over coprime products.
 160    For arbitrary products with positive factors, the same identity holds
 161    because `Nat.factorization` is additive on positive multiplications. -/
 162theorem costSpectrumValue_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.