polyCost_nonneg

formal source

 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`. -/
 134theorem polyCost_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) :
 135    polyCost (f * g) = polyCost f + polyCost g := by
 136  unfold polyCost
 137  rw [normalizedFactors_mul hf hg]
 138  rw [Multiset.map_add, Multiset.sum_add]
 139
 140/-! ## Cost on irreducibles and powers -/
 141
 142/-- For a monic irreducible polynomial `P`, the cost equals `J(‖P‖)`.
 143    Mathlib's `normalizedFactors` returns the multiset of monic
 144    irreducible factors. -/
 145theorem polyCost_irreducible {P : Polynomial F}
 146    (hP_irr : Irreducible P) (hP_monic : P.Monic) :
 147    polyCost P = polyPrimeCost P := by
 148  unfold polyCost
 149  rw [normalizedFactors_irreducible hP_irr]
 150  have hP_ne : P ≠ 0 := hP_irr.ne_zero
 151  have h_norm : normalize P = P :=
 152    (normalize_eq_self_iff_monic hP_ne).mpr hP_monic