pith. machine review for the scientific record. sign in
theorem proved term proof

costSpectrumValue_pow

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 153theorem costSpectrumValue_pow {p k : ℕ} (hp : Nat.Prime p) :
 154    costSpectrumValue (p ^ k) = (k : ℝ) * primeCost p := by

proof body

Term-mode proof.

 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. -/

depends on (12)

Lean names referenced from this declaration's body.