The order of vanishing of a multivariate polynomial at a point

MvPolynomial.taylor a is the Taylor shift p ↦ p(X + a), which substitutes Xᵢ + aᵢ for each variable Xᵢ; the coefficients of taylor a p are the Taylor coefficients of p at a. The order of vanishing p.orderAt a : ℕ∞ is the least total degree of a nonzero Taylor coefficient of p at a, and ⊤ when p = 0. It is the order of taylor a p viewed as a multivariate power series, so it is positive exactly at the zeros of p, and over a domain it is additive on products.

This is the ambient order of p at a, computed in all variables at once. It is the invariant of order-invariant cylindrical algebraic decompositions in McCallum's projection theory: there each polynomial is required to have constant order on each cell, which is stronger than constant sign.

Over a ring without additive torsion, such as ℝ, the order is detected by partial derivatives: p has order at least n at a exactly when every iterated partial derivative of p of order less than n vanishes at a; since a nonzero polynomial vanishes to order at most its total degree, finitely many derivatives suffice. Substituting polynomials into p can only increase the order at corresponding points, and renaming the variables along an injective map does not change it. The Taylor shift itself preserves the degree in each variable (MvPolynomial.degreeOf_taylor).

Main definitions

• MvPolynomial.taylor: the Taylor shift p ↦ p(X + a).
• MvPolynomial.orderAt: the order of vanishing of p at a.

Main results

• MvPolynomial.orderAt_eq_top_iff: the order is ⊤ exactly for the zero polynomial.
• MvPolynomial.orderAt_eq_zero_iff, MvPolynomial.orderAt_pos_iff: the order is positive exactly at the zeros of p.
• MvPolynomial.orderAt_mul: over a domain, the order of a product is the sum of the orders.
• MvPolynomial.succ_le_orderAt_iff: p has order at least n + 1 at a if and only if p vanishes at a and every partial derivative of p has order at least n there.
• MvPolynomial.le_orderAt_iff_eval_foldl_pderiv: the order is at least n if and only if every iterated partial derivative of order less than n vanishes at a.
• MvPolynomial.orderAt_le_totalDegree: a nonzero polynomial vanishes to order at most its total degree.
• MvPolynomial.orderAt_eq_of_forall_eval_foldl_pderiv_eq_zero_iff: the order at a point is determined by which iterated partial derivatives, up to the total degree, vanish there.
• MvPolynomial.orderAt_le_orderAt_aeval: substitution does not decrease the order.
• MvPolynomial.orderAt_rename: renaming along an injective map preserves the order.
• MvPolynomial.finSuccEquiv_taylor, MvPolynomial.coeff_taylor_cons: singling out the variable X₀ turns the Taylor shift at a into the univariate Taylor shift at a₀ followed by the Taylor shift at the remaining coordinates.
• MvPolynomial.optionEquivRight_rename_finSuccEquivLast_taylor, MvPolynomial.coeff_taylor_snoc: moving the last variable Xₙ into the coefficients turns the Taylor shift at Fin.snoc α β into the Taylor shift at the first coordinates α, followed by the univariate Taylor shift at β of each coefficient.

References

• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, in Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer (1998), pp. 242–268, Section 2 (order of a polynomial at a point, order-invariance).

noncomputable def MvPolynomial.taylor {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) : MvPolynomial σ R →ₐ[R] MvPolynomial σ R

The Taylor shift of a multivariate polynomial at a: the substitution p ↦ p(X + a) of Xᵢ + aᵢ for each variable Xᵢ. The coefficients of taylor a p are the Taylor coefficients of p at a.

Equations

• MvPolynomial.taylor a = MvPolynomial.aeval fun (i : σ) => MvPolynomial.X i + MvPolynomial.C (a i)

theorem MvPolynomial.taylor_apply {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) (p : MvPolynomial σ R) : (taylor a) p = (aeval fun (i : σ) => X i + C (a i)) p

@[simp]

theorem MvPolynomial.taylor_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) (i : σ) : (taylor a) (X i) = X i + C (a i)

theorem MvPolynomial.taylor_C {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) (r : R) : (taylor a) (C r) = C r

@[simp]

theorem MvPolynomial.map_taylor {σ : Type u_1} {R : Type u_3} [CommSemiring R] {S : Type u_4} [CommSemiring S] (p : MvPolynomial σ R) (a : σ → R) (f : R →+* S) : (map f) ((taylor a) p) = (taylor fun (i : σ) => f (a i)) ((map f) p)

Taylor shifts commute with coefficient maps, with the center mapped along the same homomorphism.

@[simp]

theorem MvPolynomial.eval_coeff_taylor_map_C {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) (a : σ → R) (v : σ →₀ ℕ) : (eval a) (((taylor X) ((map C) p)).coeff v) = ((taylor a) p).coeff v

Taylor coefficients depend polynomially on the center. Evaluate the formal center in taylor X (map C p) at a to recover each coefficient of taylor a p.

@[simp]

theorem MvPolynomial.eval_taylor {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a x : σ → R) (p : MvPolynomial σ R) : (eval x) ((taylor a) p) = (eval (x + a)) p

@[simp]

theorem MvPolynomial.constantCoeff_taylor {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) (p : MvPolynomial σ R) : constantCoeff ((taylor a) p) = (eval a) p

The constant Taylor coefficient of p at a is the value of p at a.

@[simp]

theorem MvPolynomial.taylor_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) : (taylor 0) p = p

theorem MvPolynomial.taylor_taylor {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a b : σ → R) (p : MvPolynomial σ R) : (taylor a) ((taylor b) p) = (taylor (a + b)) p

theorem MvPolynomial.totalDegree_taylor_le {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) (p : MvPolynomial σ R) : ((taylor a) p).totalDegree ≤ p.totalDegree

The Taylor shift does not increase the total degree.

@[simp]

theorem MvPolynomial.pderiv_taylor {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) (i : σ) (p : MvPolynomial σ R) : (pderiv i) ((taylor a) p) = (taylor a) ((pderiv i) p)

Partial differentiation commutes with the Taylor shift.

theorem MvPolynomial.degreeOf_taylor_le {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) (i : σ) (p : MvPolynomial σ R) : degreeOf i ((taylor a) p) ≤ degreeOf i p

The Taylor shift does not increase the degree in any variable.

theorem MvPolynomial.finSuccEquiv_taylor {R : Type u_3} [CommSemiring R] {n : ℕ} (a : Fin (n + 1) → R) (p : MvPolynomial (Fin (n + 1)) R) : (finSuccEquiv R n) ((taylor a) p) = Polynomial.map (↑(taylor (Fin.tail a))) ((Polynomial.taylor (C (a 0))) ((finSuccEquiv R n) p))

Singling out the variable X₀ commutes with the Taylor shift: shifting X₀ by a₀ is the Taylor shift of the resulting univariate polynomial at a₀, and the remaining variables are shifted coefficientwise.

theorem MvPolynomial.coeff_taylor_cons {R : Type u_3} [CommSemiring R] {n : ℕ} (a : Fin (n + 1) → R) (p : MvPolynomial (Fin (n + 1)) R) (i : ℕ) (u : Fin n →₀ ℕ) : ((taylor a) p).coeff (Finsupp.cons i u) = ((taylor (Fin.tail a)) (((Polynomial.taylor (C (a 0))) ((finSuccEquiv R n) p)).coeff i)).coeff u

The Taylor coefficients of p at a, read off after singling out the variable X₀: the coefficient of X₀ ^ i * Xᵘ is the coefficient of Xᵘ in the Taylor shift at Fin.tail a of the i-th coefficient of the univariate Taylor expansion at a₀.

theorem MvPolynomial.optionEquivRight_rename_finSuccEquivLast_taylor {R : Type u_3} [CommSemiring R] {n : ℕ} (α : Fin n → R) (β : R) (f : MvPolynomial (Fin (n + 1)) R) : (optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) ((taylor (Fin.snoc α β)) f)) = (map ↑(Polynomial.taylorAlgHom β)) ((taylor (⇑Polynomial.C ∘ α)) ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)))

Moving the last variable Xₙ into the coefficients commutes with the Taylor shift: shifting at Fin.snoc α β becomes the Taylor shift at the constant polynomials α, followed by the univariate Taylor shift at β of every coefficient.

theorem MvPolynomial.coeff_taylor_snoc {R : Type u_3} [CommSemiring R] {n : ℕ} (α : Fin n → R) (β : R) (f : MvPolynomial (Fin (n + 1)) R) (u : Fin n →₀ ℕ) (k : ℕ) : ((taylor (Fin.snoc α β)) f).coeff (u.snoc k) = ((Polynomial.taylor β) (((taylor (⇑Polynomial.C ∘ α)) ((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f))).coeff u)).coeff k

The Taylor coefficients of f at Fin.snoc α β, read off after moving the last variable Xₙ into the coefficients: the coefficient of Xᵘ * Xₙ ^ k is the coefficient of Xₙ ^ k in the univariate Taylor expansion at β of the coefficient of Xᵘ in the Taylor shift at α.

@[simp]

theorem MvPolynomial.taylor_neg_taylor {σ : Type u_1} {R : Type u_3} [CommRing R] (a : σ → R) (p : MvPolynomial σ R) : (taylor (-a)) ((taylor a) p) = p

@[simp]

theorem MvPolynomial.totalDegree_taylor {σ : Type u_1} {R : Type u_3} [CommRing R] (a : σ → R) (p : MvPolynomial σ R) : ((taylor a) p).totalDegree = p.totalDegree

The Taylor shift preserves the total degree.

theorem MvPolynomial.taylor_injective {σ : Type u_1} {R : Type u_3} [CommRing R] (a : σ → R) : Function.Injective ⇑(taylor a)

@[simp]

theorem MvPolynomial.taylor_eq_zero {σ : Type u_1} {R : Type u_3} [CommRing R] {a : σ → R} {p : MvPolynomial σ R} : (taylor a) p = 0 ↔ p = 0

@[simp]

theorem MvPolynomial.degreeOf_taylor {σ : Type u_1} {R : Type u_3} [CommRing R] (a : σ → R) (i : σ) (p : MvPolynomial σ R) : degreeOf i ((taylor a) p) = degreeOf i p

The Taylor shift preserves the degree in each variable.

@[simp]

theorem MvPolynomial.constantCoeff_coe {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) : MvPowerSeries.constantCoeff ↑p = constantCoeff p

The constant coefficient of a polynomial viewed as a power series is its constant coefficient as a polynomial.

theorem MvPolynomial.order_coe_le_order_coe_aeval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {h : σ → MvPolynomial τ R} (hh : ∀ (i : σ), constantCoeff (h i) = 0) (q : MvPolynomial σ R) : (↑q).order ≤ (↑((aeval h) q)).order

Substituting polynomials without constant terms into a polynomial does not decrease its order.

noncomputable def MvPolynomial.orderAt {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) (a : σ → R) : ℕ∞

The order of vanishing of p at a: the least total degree of a nonzero Taylor coefficient of p at a, and ⊤ if there is none.

Equations

• p.orderAt a = (↑((MvPolynomial.taylor a) p)).order

theorem MvPolynomial.orderAt_def {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) (a : σ → R) : p.orderAt a = (↑((taylor a) p)).order

theorem MvPolynomial.le_orderAt_iff {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {n : ℕ∞} : n ≤ p.orderAt a ↔ ∀ (d : σ →₀ ℕ), ↑(Finsupp.degree d) < n → ((taylor a) p).coeff d = 0

p has order at least n at a exactly when every Taylor coefficient of p at a of total degree less than n vanishes.

theorem MvPolynomial.orderAt_le {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {d : σ →₀ ℕ} (h : ((taylor a) p).coeff d ≠ 0) : p.orderAt a ≤ ↑(Finsupp.degree d)

theorem MvPolynomial.orderAt_eq_coe_iff {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {n : ℕ} : p.orderAt a = ↑n ↔ (∃ (d : σ →₀ ℕ), ((taylor a) p).coeff d ≠ 0 ∧ Finsupp.degree d = n) ∧ ∀ (d : σ →₀ ℕ), Finsupp.degree d < n → ((taylor a) p).coeff d = 0

p has order exactly n at a when n is the least total degree of a nonzero Taylor coefficient of p at a: some Taylor coefficient of total degree n is nonzero, and every Taylor coefficient of smaller total degree vanishes.

@[simp]

theorem MvPolynomial.orderAt_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] (a : σ → R) : orderAt 0 a = ⊤

theorem MvPolynomial.orderAt_eq_zero_iff {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} : p.orderAt a = 0 ↔ (eval a) p ≠ 0

The order of p at a is zero exactly when p does not vanish at a.

theorem MvPolynomial.orderAt_pos_iff {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} : 0 < p.orderAt a ↔ (eval a) p = 0

The order of p at a is positive exactly when p vanishes at a.

theorem MvPolynomial.orderAt_C_of_ne_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] {r : R} (hr : r ≠ 0) (a : σ → R) : (C r).orderAt a = 0

@[simp]

theorem MvPolynomial.orderAt_one {σ : Type u_1} {R : Type u_3} [CommSemiring R] [Nontrivial R] (a : σ → R) : orderAt 1 a = 0

theorem MvPolynomial.min_orderAt_le_orderAt_add {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ R) (a : σ → R) : min (p.orderAt a) (q.orderAt a) ≤ (p + q).orderAt a

theorem MvPolynomial.le_orderAt_mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p q : MvPolynomial σ R) (a : σ → R) : p.orderAt a + q.orderAt a ≤ (p * q).orderAt a

@[simp]

theorem MvPolynomial.orderAt_eq_top_iff {σ : Type u_1} {R : Type u_3} [CommRing R] {p : MvPolynomial σ R} {a : σ → R} : p.orderAt a = ⊤ ↔ p = 0

Only the zero polynomial has infinite order at a point.

theorem MvPolynomial.orderAt_le_totalDegree {σ : Type u_1} {R : Type u_3} [CommRing R] {p : MvPolynomial σ R} (hp : p ≠ 0) (a : σ → R) : p.orderAt a ≤ ↑p.totalDegree

A nonzero polynomial vanishes at each point to order at most its total degree.

@[simp]

theorem MvPolynomial.orderAt_neg {σ : Type u_1} {R : Type u_3} [CommRing R] (p : MvPolynomial σ R) (a : σ → R) : (-p).orderAt a = p.orderAt a

theorem MvPolynomial.orderAt_X_sub_C {σ : Type u_1} {R : Type u_3} [CommRing R] [Nontrivial R] (a : σ → R) (i : σ) : (X i - C (a i)).orderAt a = 1

The coordinate function Xᵢ - aᵢ vanishes to order one at a.

theorem MvPolynomial.orderAt_mul {σ : Type u_1} {R : Type u_3} [CommRing R] [NoZeroDivisors R] (p q : MvPolynomial σ R) (a : σ → R) : (p * q).orderAt a = p.orderAt a + q.orderAt a

Over a domain, the order of a product is the sum of the orders.

theorem MvPolynomial.orderAt_pow {σ : Type u_1} {R : Type u_3} [CommRing R] [NoZeroDivisors R] [Nontrivial R] (p : MvPolynomial σ R) (a : σ → R) (n : ℕ) : (p ^ n).orderAt a = n • p.orderAt a

Over a domain, the order of p ^ n at a is n times the order of p at a.

theorem MvPolynomial.orderAt_prod {σ : Type u_1} {R : Type u_3} [CommRing R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_4} (p : ι → MvPolynomial σ R) (s : Finset ι) (a : σ → R) : (∏ i ∈ s, p i).orderAt a = ∑ i ∈ s, (p i).orderAt a

Over a domain, the order of a finite product is the sum of the orders of its factors.

theorem MvPolynomial.orderAt_le_orderAt_aeval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] (g : σ → MvPolynomial τ R) (b : τ → R) (p : MvPolynomial σ R) : (p.orderAt fun (i : σ) => (eval b) (g i)) ≤ ((aeval g) p).orderAt b

Substitution does not decrease the order: if g maps the point b to a, that is, eval b (g i) = a i for every i, then the order of aeval g p at b is at least the order of p at a.

theorem MvPolynomial.orderAt_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] {f : σ → τ} (hf : Function.Injective f) (p : MvPolynomial σ R) (b : τ → R) : ((rename f) p).orderAt b = p.orderAt (b ∘ f)

Renaming the variables along an injective map does not change the order.

theorem MvPolynomial.succ_le_orderAt_iff {σ : Type u_1} {R : Type u_3} [CommRing R] [IsAddTorsionFree R] {p : MvPolynomial σ R} {a : σ → R} {n : ℕ} : ↑(n + 1) ≤ p.orderAt a ↔ (eval a) p = 0 ∧ ∀ (i : σ), ↑n ≤ ((pderiv i) p).orderAt a

Over a ring without additive torsion, p has order at least n + 1 at a if and only if p vanishes at a and every partial derivative of p has order at least n at a.

theorem MvPolynomial.le_orderAt_iff_eval_foldl_pderiv {σ : Type u_1} {R : Type u_3} [CommRing R] [IsAddTorsionFree R] {p : MvPolynomial σ R} {a : σ → R} {n : ℕ} : ↑n ≤ p.orderAt a ↔ ∀ (l : List σ), l.length < n → (eval a) (List.foldl (fun (q : MvPolynomial σ R) (i : σ) => (pderiv i) q) p l) = 0

Over a ring without additive torsion, p has order at least n at a if and only if, for every list l of fewer than n variables, the iterated partial derivative of p along l vanishes at a.

theorem MvPolynomial.orderAt_eq_of_forall_eval_foldl_pderiv_eq_zero_iff {σ : Type u_1} {R : Type u_3} [CommRing R] [IsAddTorsionFree R] {p : MvPolynomial σ R} {a b : σ → R} (h : ∀ (l : List σ), l.length ≤ p.totalDegree → ((eval a) (List.foldl (fun (q : MvPolynomial σ R) (i : σ) => (pderiv i) q) p l) = 0 ↔ (eval b) (List.foldl (fun (q : MvPolynomial σ R) (i : σ) => (pderiv i) q) p l) = 0)) : p.orderAt a = p.orderAt b

Over a ring without additive torsion, the order of p at a point is determined by which iterated partial derivatives of p, of order at most the total degree of p, vanish there: if the same ones vanish at a and at b, then p has the same order at a and at b.