universalCost_single

formal source

 101@[simp] theorem universalCost_zero : universalCost (0 : P →₀ ℕ) = 0 := by
 102  simp [universalCost]
 103
 104theorem universalCost_single (p : P) (k : ℕ) :
 105    universalCost (Finsupp.single p k) = (k : ℝ) * primeJcost p := by
 106  unfold universalCost
 107  simp [Finsupp.sum_single_index]
 108
 109@[simp] theorem universalCost_single_one (p : P) :
 110    universalCost (Finsupp.single p 1) = primeJcost p := by
 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