costSpectrumValue_nonneg

formal source

 172
 173/-- The cost is nonnegative for any positive `n`.
 174    Each summand `k · J(p) ≥ 0` by primality of `p`, so the sum is ≥ 0. -/
 175theorem costSpectrumValue_nonneg (n : ℕ) :
 176    0 ≤ costSpectrumValue n := by
 177  unfold costSpectrumValue
 178  apply Finsupp.sum_nonneg
 179  intro p hp_mem
 180  have hp_prime : Nat.Prime p := Nat.prime_of_mem_primeFactors
 181    (Nat.support_factorization n ▸ hp_mem)
 182  have hk_nonneg : (0 : ℝ) ≤ (n.factorization p : ℝ) := by
 183    exact_mod_cast Nat.zero_le _
 184  have hJ_nonneg : 0 ≤ primeCost p := le_of_lt (primeCost_pos hp_prime)
 185  exact mul_nonneg hk_nonneg hJ_nonneg
 186
 187/-- Cost is monotonic under multiplication by positive integers
 188    (a direct consequence of additivity and nonnegativity of prime costs). -/
 189theorem costSpectrumValue_le_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
 190    costSpectrumValue m ≤ costSpectrumValue (m * n) := by
 191  rw [costSpectrumValue_mul hm hn]
 192  have := costSpectrumValue_nonneg n
 193  linarith
 194
 195/-- The cost is strictly positive for any integer `n ≥ 2`. -/
 196theorem costSpectrumValue_pos {n : ℕ} (hn : 2 ≤ n) :
 197    0 < costSpectrumValue n := by
 198  have hn_ne_zero : n ≠ 0 := by omega
 199  have hn_ne_one : n ≠ 1 := by omega
 200  obtain ⟨p, hp_prime, hp_dvd⟩ := Nat.exists_prime_and_dvd hn_ne_one
 201  have hp_mem : p ∈ n.factorization.support := by
 202    rw [Nat.support_factorization]
 203    exact Nat.mem_primeFactors.mpr ⟨hp_prime, hp_dvd, hn_ne_zero⟩
 204  have hk_pos : 0 < n.factorization p := by
 205    have := Finsupp.mem_support_iff.mp hp_mem