summand_decomposition

formal source

 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
 270    `p_max` is the largest prime factor of `n`.  Specialized to the
 271    weaker bound `c(n) ≤ Ω(n) · J(n)` using monotonicity of `J` on
 272    `[1, ∞)`.  Useful for asymptotic upper bounds. -/
 273theorem costSpectrumValue_le_omega_mul_jcost {n : ℕ} (hn : 2 ≤ n) :
 274    costSpectrumValue n ≤ (Omega n : ℝ) * Jcost (n : ℝ) := by
 275  have hn_pos : 0 < n := by omega