costSpectrumValue_pow_general

formal source

 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
 276  have hn_ge_one : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn_pos
 277  -- Bound each summand: k · J(p) ≤ k · J(n) for prime p dividing n,
 278  -- since p ≤ n and J is monotonic on [1, ∞).
 279  have h_per_summand : ∀ p ∈ n.factorization.support,
 280      (n.factorization p : ℝ) * primeCost p
 281        ≤ (n.factorization p : ℝ) * Jcost (n : ℝ) := by
 282    intro p hp_mem
 283    have hp_prime : Nat.Prime p := Nat.prime_of_mem_primeFactors
 284      (Nat.support_factorization n ▸ hp_mem)
 285    have hp_dvd : p ∣ n :=
 286      Nat.dvd_of_mem_primeFactors (Nat.support_factorization n ▸ hp_mem)
 287    have hp_le_n : p ≤ n := Nat.le_of_dvd hn_pos hp_dvd
 288    have hk_nonneg : (0 : ℝ) ≤ (n.factorization p : ℝ) := by
 289      exact_mod_cast Nat.zero_le _