reciprocalPrimeSum

formal source

 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
 261  induction k with
 262  | zero => simp [costSpectrumValue_one]
 263  | succ k ih =>
 264    have hnk : n ^ k ≠ 0 := pow_ne_zero k hn
 265    rw [pow_succ, costSpectrumValue_mul hnk hn, ih]
 266    push_cast
 267    ring
 268
 269/-- The cost spectrum value is bounded by `Ω(n) · J(p_max)` where