Multiplicities of labelled roots

If a finite family enumerates a polynomial's roots with multiplicity, the multiplicity at each label depends only on which labels coincide. Consequently an eventually constant collision relation gives eventually constant multiplicities, without any continuity or splitting assumptions on the polynomial family.

We also count the root zero: it occurs in f.roots with multiplicity the order of vanishing f.natTrailingDegree, so the roots satisfying a predicate that holds at zero number f.natTrailingDegree plus the nonzero roots satisfying it. Over any integral domain, summing f.rootMultiplicity over any finite set of points never exceeds f.natDegree (Polynomial.sum_rootMultiplicity_le_natDegree), including for f = 0.

theorem TauCeti.eventually_rootMultiplicity_eq_of_roots_eq_map {K : Type u_1} {B : Type u_2} {ι : Type u_3} [CommRing K] [IsDomain K] {I : Finset ι} {f : ι → B → K} {Q : B → Polynomial K} {x₀ : B} {l : Filter B} (hroots₀ : (Q x₀).roots = Multiset.map (fun (i : ι) => f i x₀) I.val) (hroots : ∀ᶠ (x : B) in l, (Q x).roots = Multiset.map (fun (i : ι) => f i x) I.val) (hrel : ∀ᶠ (x : B) in l, ∀ i ∈ I, ∀ j ∈ I, f i x = f j x ↔ f i x₀ = f j x₀) : ∀ᶠ (x : B) in l, ∀ i ∈ I, Polynomial.rootMultiplicity (f i x) (Q x) = Polynomial.rootMultiplicity (f i x₀) (Q x₀)

A finite enumeration of roots with an eventually constant collision relation has eventually constant multiplicity at each label. The parameter filter is arbitrary, and the root enumeration at the reference parameter is supplied separately.

theorem Polynomial.count_zero_roots {R : Type u_1} [CommRing R] [IsDomain R] [DecidableEq R] (f : Polynomial R) : Multiset.count 0 f.roots = f.natTrailingDegree

The root zero occurs in f.roots with multiplicity the order of vanishing of f at zero.

theorem Polynomial.card_filter_roots_eq_natTrailingDegree_add {R : Type u_1} [CommRing R] [IsDomain R] [DecidableEq R] (f : Polynomial R) {q : R → Prop} [DecidablePred q] (hq : q 0) : (Multiset.filter q f.roots).card = f.natTrailingDegree + (Multiset.filter (fun (α : R) => α ≠ 0 ∧ q α) f.roots).card

The number of roots satisfying a predicate that holds at zero is the order of vanishing at zero plus the number of nonzero roots satisfying it.

theorem Polynomial.sum_rootMultiplicity_le_natDegree {R : Type u_1} [CommRing R] [IsDomain R] (f : Polynomial R) (s : Finset R) : ∑ a ∈ s, rootMultiplicity a f ≤ f.natDegree

Over a domain, the sum of root multiplicities of a polynomial f across any finite set of points is at most f.natDegree (also when f = 0, where every multiplicity vanishes).

theorem Polynomial.isRoot_C_mul_prod_X_sub_C_iff {R : Type u_1} [CommRing R] [IsDomain R] {ι : Type u_2} [Fintype ι] {l : R} (hl : l ≠ 0) (r : ι → R) (z : R) : (C l * ∏ i : ι, (X - C (r i))).IsRoot z ↔ ∃ (i : ι), r i = z

A nonzero constant multiple of a product of linear factors vanishes exactly at the r i.