costSpectrumValue_pos

formal source

 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
 206    exact Nat.pos_of_ne_zero this
 207  have hJ_pos : 0 < primeCost p := primeCost_pos hp_prime
 208  have hsummand_pos : 0 < (n.factorization p : ℝ) * primeCost p := by
 209    have hk_real_pos : (0 : ℝ) < (n.factorization p : ℝ) := by
 210      exact_mod_cast hk_pos
 211    exact mul_pos hk_real_pos hJ_pos
 212  unfold costSpectrumValue
 213  -- Split the Finsupp sum into the p-summand plus the rest, both nonneg.
 214  rw [Finsupp.sum, ← Finset.sum_erase_add _ _ hp_mem]
 215  apply add_pos_of_nonneg_of_pos
 216  · apply Finset.sum_nonneg
 217    intro q hq_mem
 218    have hq_in_support : q ∈ n.factorization.support :=
 219      (Finset.mem_erase.mp hq_mem).2
 220    have hq_prime : Nat.Prime q := Nat.prime_of_mem_primeFactors
 221      (Nat.support_factorization n ▸ hq_in_support)
 222    have hk_nonneg : (0 : ℝ) ≤ (n.factorization q : ℝ) := by
 223      exact_mod_cast Nat.zero_le _
 224    exact mul_nonneg hk_nonneg (le_of_lt (primeCost_pos hq_prime))
 225  · exact hsummand_pos
 226