polyCost_mul

formal source

 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
 153  rw [h_norm]
 154  simp
 155
 156/-- Cost on a power: `c(P^k) = k · c(P)` for any nonzero `P`. -/
 157theorem polyCost_pow {P : Polynomial F} (hP : P ≠ 0) (k : ℕ) :
 158    polyCost (P ^ k) = (k : ℝ) * polyCost P := by
 159  induction k with
 160  | zero => simp [polyCost_one]
 161  | succ k ih =>
 162    have hPk : P ^ k ≠ 0 := pow_ne_zero k hP
 163    rw [pow_succ, polyCost_mul hPk hP, ih]
 164    push_cast