The Lazard valuation of a multivariate polynomial at a point

Fix a linear order on the variables σ, well-founded for > (for instance Fin n). The Lazard valuation p.lazardValuation a of a polynomial p at a point a is the lexicographically least exponent of a nonzero Taylor coefficient of p at a, that is, of a nonzero coefficient of the translate taylor a p = p(X + a), and ⊤ when p = 0. The lexicographic order is Mathlib's order on Lex (σ →₀ ℕ), in which the least variable is the most significant; this is the order in which Lazard evaluation divides out the powers of the Xᵢ - aᵢ. It is Mathlib's MvPowerSeries.lexOrder of the Taylor shift, just as the order of vanishing MvPolynomial.orderAt is the order of the Taylor shift; the two invariants differ in that the Lazard valuation retains the whole lexicographically leading exponent rather than only a total degree. The Lazard valuation is additive on products over a domain, it is zero exactly where p does not vanish, and its coordinates are bounded by the degrees of p, so a fixed polynomial takes only finitely many Lazard valuations.

Valuations turn into orders of vanishing along monomial curves. An evaluator for a set V of exponents is a weight vector c : σ → ℕ, positive everywhere, such that for every v ∈ V and every variable i, the c-weight of the coordinates of v less significant than i is less than c i (TauCeti.IsLazardEvaluator). Such weights turn the lexicographic comparison of an exponent in V with any other exponent into a comparison of c-weights (TauCeti.IsLazardEvaluator.weight_lt_weight). Every finite set of exponents has an evaluator (TauCeti.exists_isLazardEvaluator). Consequently, if the Lazard valuation v of p at a lies in V, then along the monomial curve y ↦ a + y ^ c with coordinates aᵢ + y ^ cᵢ (MvPolynomial.monomialCurve) the polynomial p restricts to a nonzero polynomial in y whose order of vanishing at y = 0 is the c-weight ∑ i, cᵢ vᵢ of v, with lowest coefficient the Taylor coefficient of p at a of exponent v (MvPolynomial.natTrailingDegree_aeval_monomialCurve). This is how Lazard's method for cylindrical algebraic decomposition converts constancy of Lazard valuations into constancy of orders of vanishing of one-variable restrictions.

Main definitions

• MvPolynomial.lazardValuation: the Lazard valuation of p at a.
• TauCeti.IsLazardEvaluator: c is an evaluator for the set of exponents V.
• MvPolynomial.monomialCurve: the monomial curve y ↦ a + y ^ c.

Main results

• MvPolynomial.lazardValuation_eq_coe_iff: the characterization of the Lazard valuation by Taylor coefficients.
• MvPolynomial.lazardValuation_mul: over a domain, the Lazard valuation is additive on products.
• MvPolynomial.lazardValuation_eq_zero_iff: the valuation is zero exactly where p does not vanish.
• MvPolynomial.finite_range_lazardValuation, MvPolynomial.finite_setOf_lazardValuation_eq: a polynomial has only finitely many Lazard valuations.
• TauCeti.exists_isLazardEvaluator: every finite set of exponents has an evaluator.
• MvPolynomial.natTrailingDegree_aeval_monomialCurve: the order of y ↦ p (a + y ^ c) at 0 is the c-weight of the Lazard valuation of p at a.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 2 (Lazard valuation) and Section 5.1 (evaluators and monomial test curves).

structure TauCeti.IsLazardEvaluator {σ : Type u_1} [LinearOrder σ] (V : Set (σ →₀ ℕ)) (c : σ → ℕ) : Prop

c is an evaluator for the set of exponents V: every weight c i is positive and, for every v ∈ V and every variable i, the c-weight ∑ j > i, c j * v j of the coordinates of v less significant than i is less than c i.

• pos (i : σ) : 0 < c i
• weight_filter_lt (v : σ →₀ ℕ) : v ∈ V → ∀ (i : σ), (Finsupp.weight c) (Finsupp.filter (fun (x : σ) => i < x) v) < c i

theorem TauCeti.IsLazardEvaluator.mono {σ : Type u_1} [LinearOrder σ] {V W : Set (σ →₀ ℕ)} {c : σ → ℕ} (hc : IsLazardEvaluator W c) (h : V ⊆ W) : IsLazardEvaluator V c

An evaluator for W is an evaluator for every subset of W.

theorem TauCeti.IsLazardEvaluator.smul {σ : Type u_1} [LinearOrder σ] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} (hc : IsLazardEvaluator V c) {k : ℕ} (hk : 0 < k) : IsLazardEvaluator V (k • c)

Positive multiples of an evaluator are evaluators.

theorem TauCeti.IsLazardEvaluator.weight_lt_weight {σ : Type u_1} [LinearOrder σ] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} (hc : IsLazardEvaluator V c) {v u : σ →₀ ℕ} (hv : v ∈ V) (h : toLex v < toLex u) : (Finsupp.weight c) v < (Finsupp.weight c) u

An evaluator for V turns the lexicographic comparison of an exponent in V with any other exponent into a comparison of c-weights.

theorem TauCeti.exists_isLazardEvaluator {σ : Type u_1} [LinearOrder σ] {V : Set (σ →₀ ℕ)} (hV : V.Finite) : ∃ (c : σ → ℕ), IsLazardEvaluator V c

Every finite set of exponents has an evaluator.

noncomputable def MvPolynomial.monomialCurve {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (c : σ → ℕ) : σ → Polynomial R

The monomial curve y ↦ a + y ^ c, given by its coordinates aᵢ + y ^ cᵢ as polynomials in y. Substituting it into a multivariate polynomial p with aeval restricts p to the curve.

Equations

• MvPolynomial.monomialCurve a c i = Polynomial.C (a i) + Polynomial.X ^ c i

@[simp]

theorem MvPolynomial.monomialCurve_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (c : σ → ℕ) (i : σ) : monomialCurve a c i = Polynomial.C (a i) + Polynomial.X ^ c i

theorem MvPolynomial.aeval_X_pow_left_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (c : σ → ℕ) (m : σ →₀ ℕ) (r : R) : (aeval fun (i : σ) => Polynomial.X ^ c i) ((monomial m) r) = (Polynomial.monomial ((Finsupp.weight c) m)) r

Substituting y ^ cᵢ for each variable Xᵢ sends the monomial X ^ m to y to the power of the c-weight of m.

theorem MvPolynomial.aeval_monomialCurve {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (c : σ → ℕ) (p : MvPolynomial σ R) : (aeval (monomialCurve a c)) p = (aeval fun (i : σ) => Polynomial.X ^ c i) ((taylor a) p)

Restricting p to the curve y ↦ a + y ^ c, with coordinates aᵢ + y ^ cᵢ, amounts to substituting y ^ cᵢ for each variable in the Taylor shift of p at a.

theorem MvPolynomial.coeff_aeval_monomialCurve {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ → R) (c : σ → ℕ) (p : MvPolynomial σ R) (k : ℕ) : ((aeval (monomialCurve a c)) p).coeff k = ∑ m ∈ ((taylor a) p).support with (Finsupp.weight c) m = k, ((taylor a) p).coeff m

The coefficients of the restriction of p to the curve y ↦ a + y ^ c: the coefficient of y ^ k is the sum of the Taylor coefficients of p at a with exponents of c-weight k.

noncomputable def MvPolynomial.lazardValuation {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (p : MvPolynomial σ R) (a : σ → R) : WithTop (Lex (σ →₀ ℕ))

The Lazard valuation of p at a: the lexicographically least exponent of a nonzero Taylor coefficient of p at a, and ⊤ if there is none. In the lexicographic order on Lex (σ →₀ ℕ) the least variable is the most significant.

Equations

• p.lazardValuation a = (↑((MvPolynomial.taylor a) p)).lexOrder

theorem MvPolynomial.lazardValuation_def {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (p : MvPolynomial σ R) (a : σ → R) : p.lazardValuation a = (↑((taylor a) p)).lexOrder

theorem MvPolynomial.coeff_taylor_ne_zero_of_lazardValuation_eq {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) : ((taylor a) p).coeff v ≠ 0

The Taylor coefficient of p at a whose exponent is the Lazard valuation is nonzero.

theorem MvPolynomial.coeff_taylor_eq_zero_of_lt_lazardValuation {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : ↑(toLex v) < p.lazardValuation a) : ((taylor a) p).coeff v = 0

The Taylor coefficients of p at a with exponents below the Lazard valuation vanish.

theorem MvPolynomial.lazardValuation_le_of_coeff_taylor_ne_zero {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : ((taylor a) p).coeff v ≠ 0) : p.lazardValuation a ≤ ↑(toLex v)

theorem MvPolynomial.le_lazardValuation_iff {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {w : WithTop (Lex (σ →₀ ℕ))} : w ≤ p.lazardValuation a ↔ ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → ((taylor a) p).coeff d = 0

The Lazard valuation of p at a is at least w exactly when every Taylor coefficient of p at a with exponent below w vanishes.

theorem MvPolynomial.lazardValuation_eq_coe_iff {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} : p.lazardValuation a = ↑(toLex v) ↔ ((taylor a) p).coeff v ≠ 0 ∧ ∀ (d : σ →₀ ℕ), toLex d < toLex v → ((taylor a) p).coeff d = 0

The Lazard valuation of p at a is v exactly when the Taylor coefficient of p at a with exponent v is nonzero and those with lexicographically smaller exponents vanish.

theorem MvPolynomial.toLex_lt_of_coeff_taylor_ne_zero {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) {d : σ →₀ ℕ} (hd : ((taylor a) p).coeff d ≠ 0) (hdv : d ≠ v) : toLex v < toLex d

A nonzero Taylor coefficient of p at a with exponent other than the Lazard valuation has a lexicographically larger exponent.

@[simp]

theorem MvPolynomial.lazardValuation_zero {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (a : σ → R) : lazardValuation 0 a = ⊤

theorem MvPolynomial.zero_le_lazardValuation {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (p : MvPolynomial σ R) (a : σ → R) : 0 ≤ p.lazardValuation a

theorem MvPolynomial.lazardValuation_eq_zero_iff {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} : p.lazardValuation a = 0 ↔ (eval a) p ≠ 0

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

theorem MvPolynomial.lazardValuation_pos_iff {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} : 0 < p.lazardValuation a ↔ (eval a) p = 0

The Lazard valuation of p at a is positive exactly when p vanishes at a.

theorem MvPolynomial.lazardValuation_C_of_ne_zero {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {r : R} (hr : r ≠ 0) (a : σ → R) : (C r).lazardValuation a = 0

@[simp]

theorem MvPolynomial.lazardValuation_one {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] [Nontrivial R] (a : σ → R) : lazardValuation 1 a = 0

theorem MvPolynomial.min_lazardValuation_le_lazardValuation_add {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (p q : MvPolynomial σ R) (a : σ → R) : min (p.lazardValuation a) (q.lazardValuation a) ≤ (p + q).lazardValuation a

theorem MvPolynomial.le_lazardValuation_mul {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (p q : MvPolynomial σ R) (a : σ → R) : p.lazardValuation a + q.lazardValuation a ≤ (p * q).lazardValuation a

theorem MvPolynomial.lazardValuation_mul {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] [NoZeroDivisors R] (p q : MvPolynomial σ R) (a : σ → R) : (p * q).lazardValuation a = p.lazardValuation a + q.lazardValuation a

Over a domain, the Lazard valuation of a product is the sum of the Lazard valuations.

theorem MvPolynomial.lazardValuation_pow {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] (p : MvPolynomial σ R) (a : σ → R) (n : ℕ) : (p ^ n).lazardValuation a = n • p.lazardValuation a

Over a domain, the Lazard valuation of p ^ n is n times that of p.

theorem MvPolynomial.lazardValuation_apply_le_degreeOf {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) (i : σ) : v i ≤ degreeOf i p

Each coordinate of the Lazard valuation of p is at most the degree of p in that variable.

theorem MvPolynomial.finite_range_lazardValuation {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (p : MvPolynomial σ R) : (Set.range p.lazardValuation).Finite

A polynomial has only finitely many Lazard valuations.

theorem MvPolynomial.finite_setOf_lazardValuation_eq {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] (p : MvPolynomial σ R) : {v : σ →₀ ℕ | ∃ (a : σ → R), p.lazardValuation a = ↑(toLex v)}.Finite

The exponents occurring as Lazard valuations of a fixed polynomial form a finite set.

@[simp]

theorem MvPolynomial.lazardValuation_eq_top_iff {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] {p : MvPolynomial σ R} {a : σ → R} : p.lazardValuation a = ⊤ ↔ p = 0

Only the zero polynomial has Lazard valuation ⊤.

@[simp]

theorem MvPolynomial.lazardValuation_neg {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] (p : MvPolynomial σ R) (a : σ → R) : (-p).lazardValuation a = p.lazardValuation a

theorem MvPolynomial.exists_lazardValuation_eq {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] {p : MvPolynomial σ R} (hp : p ≠ 0) (a : σ → R) : ∃ (v : σ →₀ ℕ), p.lazardValuation a = ↑(toLex v)

theorem MvPolynomial.lazardValuation_X_sub_C {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommRing R] [Nontrivial R] (a : σ → R) (i : σ) : (X i - C (a i)).lazardValuation a = ↑(toLex (Finsupp.single i 1))

The Lazard valuation of the coordinate function Xᵢ - aᵢ at a is the exponent of Xᵢ.

theorem MvPolynomial.weight_lt_weight_of_coeff_taylor_ne_zero {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) {m : σ →₀ ℕ} (hm : ((taylor a) p).coeff m ≠ 0) (hmv : m ≠ v) : (Finsupp.weight c) v < (Finsupp.weight c) m

If the Lazard valuation v of p at a lies in V and c is an evaluator for V, then every other exponent of a nonzero Taylor coefficient of p at a has larger c-weight than v.

theorem MvPolynomial.coeff_aeval_monomialCurve_eq_zero_of_lt_weight {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) {k : ℕ} (hk : k < (Finsupp.weight c) v) : ((aeval (monomialCurve a c)) p).coeff k = 0

If the Lazard valuation v of p at a lies in V and c is an evaluator for V, then the restriction of p to the curve y ↦ a + y ^ c has no terms of degree below the c-weight of v.

theorem MvPolynomial.coeff_aeval_monomialCurve_weight {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) : ((aeval (monomialCurve a c)) p).coeff ((Finsupp.weight c) v) = ((taylor a) p).coeff v

If the Lazard valuation v of p at a lies in V and c is an evaluator for V, then the coefficient of y to the c-weight of v in the restriction of p to the curve y ↦ a + y ^ c is the Taylor coefficient of p at a with exponent v.

theorem MvPolynomial.aeval_monomialCurve_ne_zero {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) : (aeval (monomialCurve a c)) p ≠ 0

If the Lazard valuation of p at a lies in a set with evaluator c, then p does not vanish identically on the curve y ↦ a + y ^ c.

theorem MvPolynomial.natTrailingDegree_aeval_monomialCurve {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) : ((aeval (monomialCurve a c)) p).natTrailingDegree = (Finsupp.weight c) v

Lazard valuations along monomial curves. If the Lazard valuation v of p at a lies in V and c is an evaluator for V, then the restriction y ↦ p (a + y ^ c) of p to the curve with coordinates aᵢ + y ^ cᵢ vanishes at y = 0 to order exactly the c-weight ∑ i, cᵢ vᵢ of v.

theorem MvPolynomial.trailingCoeff_aeval_monomialCurve {σ : Type u_1} {R : Type u_2} [LinearOrder σ] [WellFoundedGT σ] [CommSemiring R] {V : Set (σ →₀ ℕ)} {c : σ → ℕ} {p : MvPolynomial σ R} {a : σ → R} {v : σ →₀ ℕ} (h : p.lazardValuation a = ↑(toLex v)) (hv : v ∈ V) (hc : TauCeti.IsLazardEvaluator V c) : ((aeval (monomialCurve a c)) p).trailingCoeff = ((taylor a) p).coeff v

If the Lazard valuation v of p at a lies in V and c is an evaluator for V, then the lowest coefficient of y ↦ p (a + y ^ c) is the Taylor coefficient of p at a with exponent v.