polyCost_zero

formal source

  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 :=
 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. -/