universalCost_pos

formal source

 125  · exact_mod_cast Nat.zero_le _
 126  · exact primeJcost_nonneg p
 127
 128theorem universalCost_pos {f : P →₀ ℕ} (hf : f ≠ 0) : 0 < universalCost f := by
 129  obtain ⟨p, hp_mem⟩ := Finsupp.support_nonempty_iff.mpr hf
 130  have hk_pos : 0 < f p := by
 131    have := Finsupp.mem_support_iff.mp hp_mem
 132    exact Nat.pos_of_ne_zero this
 133  have hJ_pos : 0 < primeJcost p := primeJcost_pos p
 134  have hsummand_pos : 0 < (f p : ℝ) * primeJcost p := by
 135    have hk_real : (0 : ℝ) < (f p : ℝ) := by exact_mod_cast hk_pos
 136    exact mul_pos hk_real hJ_pos
 137  unfold universalCost
 138  rw [Finsupp.sum, ← Finset.sum_erase_add _ _ hp_mem]
 139  apply add_pos_of_nonneg_of_pos
 140  · apply Finset.sum_nonneg
 141    intro q _
 142    apply mul_nonneg
 143    · exact_mod_cast Nat.zero_le _
 144    · exact primeJcost_nonneg q
 145  · exact hsummand_pos
 146
 147/-! ## Power and multiplicative structure -/
 148
 149/-- The cost of a power `n · single p 1`: `c(n · single p 1) = n · J(‖p‖)`.
 150    More generally, scaling a single-prime Finsupp scales the cost. -/
 151theorem universalCost_smul_single (n : ℕ) (p : P) :
 152    universalCost (n • Finsupp.single p 1) = (n : ℝ) * primeJcost p := by
 153  rw [show n • Finsupp.single p (1 : ℕ) = Finsupp.single p n by
 154        ext q; by_cases hpq : q = p
 155        · subst hpq; simp
 156        · simp [Finsupp.single_apply, hpq]]
 157  exact universalCost_single p n
 158