Omega

formal source

 227/-! ## Auxiliary arithmetic functions -/
 228
 229/-- The total prime factor count (with multiplicity) of `n`, written `Ω(n)`. -/
 230def Omega (n : ℕ) : ℕ := n.factorization.sum fun _ k => k
 231
 232/-- The total prime factor count (without multiplicity) of `n`, written `ω(n)`. -/
 233def omega (n : ℕ) : ℕ := n.factorization.support.card
 234
 235/-- The "sum of prime factors with multiplicity" function `sopfr(n) = Σ k·p`. -/
 236def sopfr (n : ℕ) : ℕ := n.factorization.sum fun p k => k * p
 237
 238/-- The reciprocal-sum-of-prime-factors `Σ k/p` as a real number. -/
 239noncomputable def reciprocalPrimeSum (n : ℕ) : ℝ :=
 240  n.factorization.sum fun p k => (k : ℝ) / (p : ℝ)
 241
 242/-- Per-summand identity: each prime-power contribution to `c(n)` decomposes
 243    into half of `k·p`, half of `k/p`, minus `k`.  Used to derive the
 244    closed-form decomposition below. -/
 245private lemma summand_decomposition (p k : ℕ) (hp : Nat.Prime p) :
 246    (k : ℝ) * primeCost p =
 247      (1/2) * ((k : ℝ) * (p : ℝ))
 248      + (1/2) * ((k : ℝ) / (p : ℝ)) - (k : ℝ) := by
 249  unfold primeCost Jcost
 250  have hp_pos : (0 : ℝ) < (p : ℝ) := by exact_mod_cast hp.pos
 251  have hp_ne : (p : ℝ) ≠ 0 := ne_of_gt hp_pos
 252  field_simp
 253
 254/-! ## Power formula and Omega bound -/
 255
 256/-- For any positive integer `n` and any natural `k`,
 257    `c(n^k) = k · c(n)`.  This is the complete-additivity of `c`
 258    extended to repeated multiplication. -/
 259theorem costSpectrumValue_pow_general {n : ℕ} (hn : n ≠ 0) (k : ℕ) :
 260    costSpectrumValue (n ^ k) = (k : ℝ) * costSpectrumValue n := by