polyPrimeCost

formal source

  78/-! ## Cost spectrum: per-irreducible and total -/
  79
  80/-- The cost of an irreducible polynomial `P`, equal to `J(‖P‖)`. -/
  81def polyPrimeCost (P : Polynomial F) : ℝ := Jcost (polyNorm P)
  82
  83/-- The cost of a polynomial `f`, computed by summing the per-factor
  84    cost over the multiset of normalized irreducible factors of `f`.
  85    By convention `polyCost 0 = 0`. -/
  86def polyCost (f : Polynomial F) : ℝ :=
  87  ((normalizedFactors f).map polyPrimeCost).sum
  88
  89/-! ## Elementary properties -/
  90
  91@[simp] theorem polyCost_zero : polyCost (0 : Polynomial F) = 0 := by
  92  unfold polyCost
  93  simp [normalizedFactors_zero]
  94
  95@[simp] theorem polyCost_one : polyCost (1 : Polynomial F) = 0 := by
  96  unfold polyCost
  97  simp [normalizedFactors_one]
  98
  99/-- The norm of a monic polynomial of positive degree is at least `q ≥ 2`,
 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 :=