costSpectrumValue_pow

formal source

 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) :
 163    costSpectrumValue (m * n) = costSpectrumValue m + costSpectrumValue n := by
 164  unfold costSpectrumValue
 165  rw [Nat.factorization_mul hm hn]
 166  rw [Finsupp.sum_add_index']
 167  · intro p
 168    simp
 169  · intro p i j
 170    push_cast
 171    ring
 172
 173/-- The cost is nonnegative for any positive `n`.
 174    Each summand `k · J(p) ≥ 0` by primality of `p`, so the sum is ≥ 0. -/
 175theorem costSpectrumValue_nonneg (n : ℕ) :
 176    0 ≤ costSpectrumValue n := by
 177  unfold costSpectrumValue
 178  apply Finsupp.sum_nonneg
 179  intro p hp_mem
 180  have hp_prime : Nat.Prime p := Nat.prime_of_mem_primeFactors
 181    (Nat.support_factorization n ▸ hp_mem)
 182  have hk_nonneg : (0 : ℝ) ≤ (n.factorization p : ℝ) := by
 183    exact_mod_cast Nat.zero_le _