universalCost_add

formal source

 111  rw [universalCost_single]
 112  ring
 113
 114theorem universalCost_add (f g : P →₀ ℕ) :
 115    universalCost (f + g) = universalCost f + universalCost g := by
 116  unfold universalCost
 117  rw [Finsupp.sum_add_index']
 118  · intro p; simp
 119  · intro p i j; push_cast; ring
 120
 121theorem universalCost_nonneg (f : P →₀ ℕ) : 0 ≤ universalCost f := by
 122  apply Finsupp.sum_nonneg
 123  intro p _
 124  apply mul_nonneg
 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