polyNorm_one

formal source

  66def polyNorm (f : Polynomial F) : ℝ :=
  67  (Fintype.card F : ℝ) ^ f.natDegree
  68
  69@[simp] theorem polyNorm_one : polyNorm (1 : Polynomial F) = 1 := by
  70  unfold polyNorm; simp
  71
  72theorem polyNorm_pos (f : Polynomial F) : 0 < polyNorm f := by
  73  unfold polyNorm
  74  have hq : 0 < (Fintype.card F : ℝ) := by
  75    exact_mod_cast Fintype.card_pos
  76  exact pow_pos hq _
  77
  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`,