polyPrimeCost_pos

formal source

 100    hence at least `2`.  Combined with `Jcost_pos_of_ne_one`, this gives
 101    `polyPrimeCost P > 0` for any irreducible polynomial of positive degree
 102    over a field with at least 2 elements. -/
 103theorem polyPrimeCost_pos {P : Polynomial F} (hP : 0 < P.natDegree)
 104    (hF : 2 ≤ Fintype.card F) : 0 < polyPrimeCost P := by
 105  unfold polyPrimeCost
 106  have hnorm_pos : 0 < polyNorm P := polyNorm_pos P
 107  have hnorm_ne_one : polyNorm P ≠ 1 := by
 108    unfold polyNorm
 109    have hq_real : (1 : ℝ) < (Fintype.card F : ℝ) := by
 110      exact_mod_cast hF
 111    have h_pow_gt : 1 < (Fintype.card F : ℝ) ^ P.natDegree :=
 112      one_lt_pow₀ hq_real (Nat.pos_iff_ne_zero.mp hP)
 113    exact ne_of_gt h_pow_gt
 114  exact Jcost_pos_of_ne_one (polyNorm P) hnorm_pos hnorm_ne_one
 115
 116/-- `polyPrimeCost` is nonnegative on any polynomial (it is always `J`
 117    of a positive real). -/
 118theorem polyPrimeCost_nonneg (P : Polynomial F) : 0 ≤ polyPrimeCost P :=
 119  Jcost_nonneg (polyNorm_pos P)
 120
 121/-- `polyCost` is nonnegative on any polynomial. -/
 122theorem polyCost_nonneg (f : Polynomial F) : 0 ≤ polyCost f := by
 123  unfold polyCost
 124  apply Multiset.sum_nonneg
 125  intro x hx
 126  obtain ⟨P, _, hP_eq⟩ := Multiset.mem_map.mp hx
 127  rw [← hP_eq]
 128  exact polyPrimeCost_nonneg P
 129
 130/-! ## Multiplicativity over factorization -/
 131
 132/-- The total cost is additive under multiplication of nonzero polynomials.
 133    This is the function-field analog of `costSpectrumValue_mul`. -/