Lazard evaluation

Let p be a polynomial in variables X₀, …, Xₙ₋₁ over a commutative ring S, and let a : Fin n → S. Lazard evaluation of p at a eliminates the variables one at a time, in the order X₀, X₁, …: it divides p by the largest power of X₀ - a₀ dividing it, sets X₀ = a₀, and continues with the result at the remaining coordinates. The outcome p.lazardEval a : S is nonzero whenever p is, unlike the ordinary value eval a p, and the exponents of the removed powers form the vector p.lazardExponent a : Fin n →₀ ℕ.

The intended use is S = R[X], with a the constant polynomials C αᵢ at a point α ∈ Rⁿ: then p is a polynomial in the base coordinates x and one further variable z, and its Lazard evaluation is a nonzero polynomial in z even where the ordinary specialization p(α, z) vanishes identically. This replaces ordinary specialization in Lazard's projection for cylindrical algebraic decomposition, which needs no well-orientedness hypothesis.

Each step of the elimination is described by the univariate identity Polynomial.trailingCoeff_taylor: dividing q by the largest power of X - r and evaluating at r gives the trailing coefficient of the Taylor expansion q(X + r), which is its lowest nonzero coefficient when q ≠ 0. Iterating it, the removed exponents are the lexicographically least exponent u of a nonzero Taylor coefficient of p at a, and the Lazard evaluation is that coefficient (lazardExponent_eq_iff, coeff_taylor_lazardExponent). Here the lexicographic order on Fin n →₀ ℕ makes coordinate 0 the most significant, matching the order of elimination.

Main definitions

• MvPolynomial.lazardEval: the Lazard evaluation of p at a.
• MvPolynomial.lazardExponent: the exponents of the powers of Xᵢ - aᵢ it removes.

Main results

• MvPolynomial.lazardEval_ne_zero: the Lazard evaluation of a nonzero polynomial is nonzero.
• MvPolynomial.lazardEval_eq_eval, MvPolynomial.lazardExponent_eq_zero_iff: where p does not vanish, Lazard evaluation is ordinary evaluation, and these are exactly the points where no power is removed.
• MvPolynomial.coeff_taylor_lazardExponent, MvPolynomial.coeff_taylor_eq_zero_of_lt_lazardExponent, MvPolynomial.lazardExponent_eq_iff: the removed exponents are the lexicographically least exponent of a nonzero Taylor coefficient of p at a, and the Lazard evaluation is that Taylor coefficient.
• MvPolynomial.lazardEval_mul, MvPolynomial.lazardExponent_mul: without zero divisors, Lazard evaluation is multiplicative and the removed exponents add.

References

• D. Lazard, An improved projection for cylindrical algebraic decomposition, in Algebraic Geometry and its Applications, Springer (1994), 467–476.
• 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.

noncomputable def MvPolynomial.lazardEval {S : Type u_1} [CommRing S] {n : ℕ} : MvPolynomial (Fin n) S → (Fin n → S) → S

The Lazard evaluation of p at a. Divide p by the largest power of X₀ - a₀ dividing it and set X₀ = a₀; then continue with the result, a polynomial in the remaining variables, at the remaining coordinates Fin.tail a. With no variables left it is the constant value of p.

It is nonzero whenever p is (MvPolynomial.lazardEval_ne_zero), and it agrees with eval a p when that is nonzero (MvPolynomial.lazardEval_eq_eval).

Equations

• One or more equations did not get rendered due to their size.
• p.lazardEval a = (MvPolynomial.eval a) p

noncomputable def MvPolynomial.lazardExponent {S : Type u_1} [CommRing S] {n : ℕ} : MvPolynomial (Fin n) S → (Fin n → S) → Fin n →₀ ℕ

The exponents of the powers of Xᵢ - aᵢ removed by the Lazard evaluation of p at a (MvPolynomial.lazardEval). Its value at i is the exponent of the largest power of Xᵢ - aᵢ dividing the polynomial left after eliminating X₀, …, Xᵢ₋₁.

Equations

• One or more equations did not get rendered due to their size.
• p.lazardExponent a = 0

theorem MvPolynomial.lazardEval_fin_zero {S : Type u_1} [CommRing S] (p : MvPolynomial (Fin 0) S) (a : Fin 0 → S) : p.lazardEval a = (eval a) p

theorem MvPolynomial.lazardEval_fin_succ {S : Type u_1} [CommRing S] {n : ℕ} (p : MvPolynomial (Fin (n + 1)) S) (a : Fin (n + 1) → S) : p.lazardEval a = (Polynomial.eval (C (a 0)) ((finSuccEquiv S n) p /ₘ (Polynomial.X - Polynomial.C (C (a 0))) ^ Polynomial.rootMultiplicity (C (a 0)) ((finSuccEquiv S n) p))).lazardEval (Fin.tail a)

theorem MvPolynomial.lazardExponent_fin_zero {S : Type u_1} [CommRing S] (p : MvPolynomial (Fin 0) S) (a : Fin 0 → S) : p.lazardExponent a = 0

theorem MvPolynomial.lazardExponent_fin_succ {S : Type u_1} [CommRing S] {n : ℕ} (p : MvPolynomial (Fin (n + 1)) S) (a : Fin (n + 1) → S) : p.lazardExponent a = Finsupp.cons (Polynomial.rootMultiplicity (C (a 0)) ((finSuccEquiv S n) p)) ((Polynomial.eval (C (a 0)) ((finSuccEquiv S n) p /ₘ (Polynomial.X - Polynomial.C (C (a 0))) ^ Polynomial.rootMultiplicity (C (a 0)) ((finSuccEquiv S n) p))).lazardExponent (Fin.tail a))

@[simp]

theorem MvPolynomial.lazardEval_zero {S : Type u_1} [CommRing S] {n : ℕ} (a : Fin n → S) : lazardEval 0 a = 0

@[simp]

theorem MvPolynomial.lazardExponent_zero {S : Type u_1} [CommRing S] {n : ℕ} (a : Fin n → S) : lazardExponent 0 a = 0

@[simp]

theorem MvPolynomial.lazardEval_C {S : Type u_1} [CommRing S] {n : ℕ} (s : S) (a : Fin n → S) : (C s).lazardEval a = s

@[simp]

theorem MvPolynomial.lazardExponent_C {S : Type u_1} [CommRing S] {n : ℕ} (s : S) (a : Fin n → S) : (C s).lazardExponent a = 0

theorem MvPolynomial.lazardEval_ne_zero {S : Type u_1} [CommRing S] {n : ℕ} {p : MvPolynomial (Fin n) S} (hp : p ≠ 0) (a : Fin n → S) : p.lazardEval a ≠ 0

The Lazard evaluation of a nonzero polynomial is nonzero.

theorem MvPolynomial.coeff_taylor_lazardExponent {S : Type u_1} [CommRing S] {n : ℕ} (p : MvPolynomial (Fin n) S) (a : Fin n → S) : ((taylor a) p).coeff (p.lazardExponent a) = p.lazardEval a

The Lazard evaluation of p at a is the Taylor coefficient of p at a whose exponent is the vector of removed exponents.

theorem MvPolynomial.coeff_taylor_eq_zero_of_lt_lazardExponent {S : Type u_1} [CommRing S] {n : ℕ} {p : MvPolynomial (Fin n) S} {a : Fin n → S} {w : Fin n →₀ ℕ} (hw : toLex w < toLex (p.lazardExponent a)) : ((taylor a) p).coeff w = 0

Every Taylor coefficient of p at a whose exponent is lexicographically less than the vector of removed exponents vanishes.

theorem MvPolynomial.lazardExponent_eq_iff {S : Type u_1} [CommRing S] {n : ℕ} {p : MvPolynomial (Fin n) S} (hp : p ≠ 0) {a : Fin n → S} {u : Fin n →₀ ℕ} : p.lazardExponent a = u ↔ ((taylor a) p).coeff u ≠ 0 ∧ ∀ (w : Fin n →₀ ℕ), toLex w < toLex u → ((taylor a) p).coeff w = 0

Lazard exponents as a lexicographic minimum. For p ≠ 0, the vector of exponents removed by Lazard evaluation at a is the lexicographically least exponent of a nonzero Taylor coefficient of p at a.

theorem MvPolynomial.lazardValuation_eq_lazardExponent {S : Type u_1} [CommRing S] {n : ℕ} {p : MvPolynomial (Fin n) S} (hp : p ≠ 0) (a : Fin n → S) : p.lazardValuation a = ↑(toLex (p.lazardExponent a))

For a nonzero polynomial, the Lazard valuation is the vector of removed exponents.

theorem MvPolynomial.finite_range_lazardExponent {S : Type u_1} [CommRing S] {n : ℕ} (p : MvPolynomial (Fin n) S) : (Set.range p.lazardExponent).Finite

A fixed polynomial has only finitely many vectors of removed Lazard exponents.

theorem MvPolynomial.lazardExponent_eq_zero_of_eval_ne_zero {S : Type u_1} [CommRing S] {n : ℕ} {p : MvPolynomial (Fin n) S} {a : Fin n → S} (h : (eval a) p ≠ 0) : p.lazardExponent a = 0

No power is removed by Lazard evaluation at a point where p does not vanish.

theorem MvPolynomial.lazardEval_eq_eval {S : Type u_1} [CommRing S] {n : ℕ} {p : MvPolynomial (Fin n) S} {a : Fin n → S} (h : (eval a) p ≠ 0) : p.lazardEval a = (eval a) p

Agreement with ordinary specialization. Where p does not vanish, its Lazard evaluation is its value.

theorem MvPolynomial.lazardExponent_eq_zero_iff {S : Type u_1} [CommRing S] {n : ℕ} {p : MvPolynomial (Fin n) S} (hp : p ≠ 0) {a : Fin n → S} : p.lazardExponent a = 0 ↔ (eval a) p ≠ 0

A nonzero polynomial loses no power under Lazard evaluation at a exactly when it does not vanish at a.

@[simp]

theorem MvPolynomial.lazardExponent_X_sub_C {S : Type u_1} [CommRing S] {n : ℕ} [Nontrivial S] (a : Fin n → S) (i : Fin n) : (X i - C (a i)).lazardExponent a = Finsupp.single i 1

Lazard evaluation removes exactly one power of Xᵢ - aᵢ from Xᵢ - aᵢ.

@[simp]

theorem MvPolynomial.lazardEval_X_sub_C {S : Type u_1} [CommRing S] {n : ℕ} (a : Fin n → S) (i : Fin n) : (X i - C (a i)).lazardEval a = 1

theorem MvPolynomial.lazardEval_mul {S : Type u_1} [CommRing S] {n : ℕ} [NoZeroDivisors S] (p q : MvPolynomial (Fin n) S) (a : Fin n → S) : (p * q).lazardEval a = p.lazardEval a * q.lazardEval a

Over a ring without zero divisors, Lazard evaluation is multiplicative.

theorem MvPolynomial.lazardExponent_mul {S : Type u_1} [CommRing S] {n : ℕ} [NoZeroDivisors S] {p q : MvPolynomial (Fin n) S} (hp : p ≠ 0) (hq : q ≠ 0) (a : Fin n → S) : (p * q).lazardExponent a = p.lazardExponent a + q.lazardExponent a

Over a ring without zero divisors, the exponents removed by Lazard evaluation of a product of nonzero polynomials are the sums of those removed from the factors.