Lazard delineations

Let F k, for k in an index type ι, be real polynomials in the variables X₀, …, Xₙ, with the last variable Xₙ distinguished, and let S ⊆ ℝⁿ be a set of base points. Moving Xₙ into the coefficients turns F k into a polynomial in X₀, …, Xₙ₋₁ with coefficients in ℝ[Xₙ], whose Lazard evaluation over α ∈ S is a univariate polynomial; for F k ≠ 0 it is nonzero, even where the ordinary fibre F k (α, Xₙ) vanishes identically. A Lazard delineation of the family over a nonempty S is a common stack of the real roots of these Lazard evaluations: continuous functions θ₀ < ⋯ < θₘ₋₁ on S such that

• the vector of base exponents removed by Lazard evaluation of each member is the same at every point of S;
• the roots of the Lazard evaluation of every nonzero member are among the values θᵢ α, every θᵢ is a root of some member, and the multiplicity of θᵢ α as a root of the Lazard evaluation of each member does not depend on α.

Unlike an ordinary delineation (TauCeti.Delineation), nothing is asked of the ordinary fibres: members may be nullified at some points of S, and the degrees of the Lazard evaluations may change along S.

By MvPolynomial.lazardValuation_snoc, the Lazard valuation of a nonzero member at a point (α, β) is the removed base exponent vector over α followed by the multiplicity of β as a root of the Lazard evaluation over α. Over a Lazard delineation it is therefore constant on every section, where it ends with the multiplicity of the section, and on every sector, where it ends with 0. Since a polynomial vanishes exactly where its Lazard valuation is positive, each member is then sign-invariant on every section and sector over a preconnected base.

The ambient stack convention places the distinguished coordinate first, while Lazard evaluation places it last. The valuation theorem retains the original Lazard coordinate order by evaluating at Fin.snoc (Fin.tail x) (x 0). For signs, this is evaluation of the polynomial renamed by finRotate; no invariance of Lazard valuation under permutation is asserted. These statements apply to the actual ambient stackCells used in cylindrical decompositions.

Where the removed exponents are constant, the coefficients of the Lazard evaluations are polynomial functions of the base point. So over an analytic submanifold of ℝⁿ the root functions of a Lazard delineation are analytic: their multiplicities are constant and positive. In other words, every Lazard delineation over an analytic submanifold is an analytic one.

The ordered list of root functions of a Lazard delineation is the increasing enumeration of the real roots of the Lazard evaluations of the nonzero members, so a family has at most one Lazard delineation over a given base. Lazard delineations restrict to nonempty subsets of the base.

Main declarations

• TauCeti.LazardDelineation: a common stack of the roots of the Lazard evaluations of a family.
• TauCeti.LazardDelineation.range_root: the root functions enumerate the real roots of the Lazard evaluations of the nonzero members.
• TauCeti.LazardDelineation.instSubsingleton: a family has at most one Lazard delineation over a given base.
• TauCeti.LazardDelineation.restrict: restriction of a Lazard delineation to a nonempty subset of its base.
• TauCeti.LazardDelineation.lazardValuation_snoc_of_mem_sectionSet, TauCeti.LazardDelineation.lazardValuation_snoc_of_mem_sectorSet: the Lazard valuations of a nonzero member on a section and on a sector.
• TauCeti.LazardDelineation.lazardValuation_snoc_eq_of_mem_sectionSet, TauCeti.LazardDelineation.lazardValuation_snoc_eq_of_mem_sectorSet: every member is Lazard valuation-invariant on each section and each sector.
• TauCeti.LazardDelineation.lazardValuation_snoc_eq_of_mem_stackCells: every member is Lazard valuation-invariant on each ambient stack cell in the original coordinate order.
• TauCeti.LazardDelineation.signInvariant_sectionSet, TauCeti.LazardDelineation.signInvariant_sectorSet: over a preconnected base, every member is sign-invariant on each section and each sector.
• TauCeti.LazardDelineation.signInvariant_rename_finRotate_of_mem_stackCells: over a preconnected base, every member is sign-invariant on each ambient stack cell after moving the distinguished coordinate to the front.
• TauCeti.LazardDelineation.analyticOnSubmanifold_root: over an analytic submanifold, the root functions are analytic.

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 (Lazard delineability and valuation-invariance in sections and sectors).

structure TauCeti.LazardDelineation {ι : Type u_1} {n : ℕ} (F : ι → MvPolynomial (Fin (n + 1)) ℝ) (S : Set (Fin n → ℝ)) : Type u_1

A Lazard delineation of a family F k of real polynomials in n + 1 variables over a nonempty set S ⊆ ℝⁿ of base points. Move the last variable into the coefficients and Lazard-evaluate the base variables at α ∈ S. A Lazard delineation is a common stack of the roots of the resulting univariate polynomials: continuous functions root 0 < ⋯ < root (count - 1) on S such that the removed base exponents of each member are a constant exponent k, the roots of each nonzero member are among the root i α, each root i is a root of some member, and the multiplicity of root i α as a root of the Lazard evaluation of F k is a constant multiplicity k i.

• nonempty : S.Nonempty

  The base is nonempty, so that exponent and multiplicity are determined by the roots.

• count : ℕ

  The number of sections of the stack.

• root : Fin self.count → ↑S → ℝ

  The root functions, listed in increasing order.

• continuous_root (i : Fin self.count) : Continuous (self.root i)

  Each root function is continuous.

• strictMono_root (x : ↑S) : StrictMono fun (i : Fin self.count) => self.root i x

  At each point the root functions are strictly increasing in their index.

• exponent : ι → Fin n →₀ ℕ

  The vector of base exponents removed by Lazard evaluation of the k-th member.

• lazardExponent_eq (k : ι) (x : ↑S) : ((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardExponent (⇑Polynomial.C ∘ ↑x) = self.exponent k

  The base exponents removed by Lazard evaluation of F k over x are exponent k at every x.

• multiplicity : ι → Fin self.count → ℕ

  The multiplicity of the i-th root function as a root of the Lazard evaluation of the k-th member.

• rootMultiplicity_root (k : ι) (i : Fin self.count) (x : ↑S) : Polynomial.rootMultiplicity (self.root i x) (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑x)) = self.multiplicity k i

  The multiplicity of root i x as a root of the Lazard evaluation of F k over x is multiplicity k i at every x.

• exists_root_eq (k : ι) (x : ↑S) : F k ≠ 0 → ∀ (t : ℝ), (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑x)).IsRoot t → ∃ (i : Fin self.count), self.root i x = t

  Every root of the Lazard evaluation of a nonzero member is the value of a root function.

• exists_multiplicity_pos (i : Fin self.count) : ∃ (k : ι), 0 < self.multiplicity k i

  Every root function is a root of some member.

theorem TauCeti.LazardDelineation.multiplicity_pos_iff {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {k : ι} {i : Fin D.count} (x : ↑S) : 0 < D.multiplicity k i ↔ F k ≠ 0 ∧ (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑x)).IsRoot (D.root i x)

A member of the family has positive multiplicity in a root function exactly when it is nonzero and the root function is a root of its Lazard evaluation, at any base point.

theorem TauCeti.LazardDelineation.multiplicity_eq_zero {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {k : ι} (hk : F k = 0) (i : Fin D.count) : D.multiplicity k i = 0

A zero member of the family has multiplicity zero in every root function.

theorem TauCeti.LazardDelineation.isRoot_iff {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {k : ι} (hk : F k ≠ 0) (x : ↑S) (t : ℝ) : (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑x)).IsRoot t ↔ ∃ (i : Fin D.count), D.root i x = t ∧ 0 < D.multiplicity k i

The roots of the Lazard evaluation of a nonzero member over a base point are exactly the values of the root functions in which it has positive multiplicity.

theorem TauCeti.LazardDelineation.range_root {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (x : ↑S) : (Set.range fun (i : Fin D.count) => D.root i x) = {t : ℝ | ∃ (k : ι), F k ≠ 0 ∧ (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑x)).IsRoot t}

At every base point, the values of the root functions are exactly the real roots of the Lazard evaluations of the nonzero members of the family.

instance TauCeti.LazardDelineation.instSubsingleton {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} : Subsingleton (LazardDelineation F S)

A family has at most one Lazard delineation over a given base: the root functions are the increasing enumeration of the real roots of the Lazard evaluations of the nonzero members, and the removed base exponents and the multiplicities are then determined.

def TauCeti.LazardDelineation.restrict {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {T : Set (Fin n → ℝ)} (hT : T.Nonempty) (hTS : T ⊆ S) : LazardDelineation F T

Restriction of a Lazard delineation to a nonempty subset of its base.

@[simp]

theorem TauCeti.LazardDelineation.restrict_count {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {T : Set (Fin n → ℝ)} (hT : T.Nonempty) (hTS : T ⊆ S) : (D.restrict hT hTS).count = D.count

The restriction of a Lazard delineation has the same number of sections.

@[simp]

theorem TauCeti.LazardDelineation.restrict_root {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {T : Set (Fin n → ℝ)} (hT : T.Nonempty) (hTS : T ⊆ S) (i : Fin (D.restrict hT hTS).count) (x : ↑T) : (D.restrict hT hTS).root i x = D.root (Fin.cast ⋯ i) (Set.inclusion hTS x)

The root functions of the restriction of a Lazard delineation are the original root functions on the smaller base.

@[simp]

theorem TauCeti.LazardDelineation.restrict_exponent {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {T : Set (Fin n → ℝ)} (hT : T.Nonempty) (hTS : T ⊆ S) : (D.restrict hT hTS).exponent = D.exponent

The restriction of a Lazard delineation has the same removed base exponents.

@[simp]

theorem TauCeti.LazardDelineation.restrict_multiplicity {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {T : Set (Fin n → ℝ)} (hT : T.Nonempty) (hTS : T ⊆ S) (k : ι) (i : Fin (D.restrict hT hTS).count) : (D.restrict hT hTS).multiplicity k i = D.multiplicity k (Fin.cast ⋯ i)

The restriction of a Lazard delineation has the same multiplicities.

theorem TauCeti.LazardDelineation.rootMultiplicity_eq_zero_of_mem_sectorSet {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (k : ι) {j : Fin (D.count + 1)} {z : ↑S × ℝ} (hz : z ∈ sectorSet D.root j) : Polynomial.rootMultiplicity z.2 (((MvPolynomial.optionEquivRight ℝ (Fin n)) ((MvPolynomial.rename ⇑finSuccEquivLast) (F k))).lazardEval (⇑Polynomial.C ∘ ↑z.1)) = 0

On a sector of a Lazard delineation, the fibre coordinate is not a root of the Lazard evaluation of any member over the base point.

theorem TauCeti.LazardDelineation.lazardValuation_snoc_of_mem_sectionSet {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {k : ι} (hk : F k ≠ 0) {i : Fin D.count} {z : ↑S × ℝ} (hz : z ∈ sectionSet D.root i) : (F k).lazardValuation (Fin.snoc (↑z.1) z.2) = ↑(toLex ((D.exponent k).snoc (D.multiplicity k i)))

Lazard valuations on a section. At every point of the i-th section of a Lazard delineation, the Lazard valuation of a nonzero member F k is its removed base exponent vector followed by the multiplicity of the section as a root of its Lazard evaluation.

theorem TauCeti.LazardDelineation.lazardValuation_snoc_of_mem_sectorSet {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {k : ι} (hk : F k ≠ 0) {j : Fin (D.count + 1)} {z : ↑S × ℝ} (hz : z ∈ sectorSet D.root j) : (F k).lazardValuation (Fin.snoc (↑z.1) z.2) = ↑(toLex ((D.exponent k).snoc 0))

Lazard valuations on a sector. At every point of a sector of a Lazard delineation, the Lazard valuation of a nonzero member F k is its removed base exponent vector followed by 0.

theorem TauCeti.LazardDelineation.lazardValuation_snoc_eq_of_mem_sectionSet {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (k : ι) {i : Fin D.count} {z z' : ↑S × ℝ} (hz : z ∈ sectionSet D.root i) (hz' : z' ∈ sectionSet D.root i) : (F k).lazardValuation (Fin.snoc (↑z.1) z.2) = (F k).lazardValuation (Fin.snoc (↑z'.1) z'.2)

Every member of a family is Lazard valuation-invariant on each section of a Lazard delineation.

theorem TauCeti.LazardDelineation.lazardValuation_snoc_eq_of_mem_sectorSet {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (k : ι) {j : Fin (D.count + 1)} {z z' : ↑S × ℝ} (hz : z ∈ sectorSet D.root j) (hz' : z' ∈ sectorSet D.root j) : (F k).lazardValuation (Fin.snoc (↑z.1) z.2) = (F k).lazardValuation (Fin.snoc (↑z'.1) z'.2)

Every member of a family is Lazard valuation-invariant on each sector of a Lazard delineation.

theorem TauCeti.LazardDelineation.lazardValuation_snoc_eq_of_mem_stackCells {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (k : ι) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ stackCells S D.root) {x y : Fin (n + 1) → ℝ} (hx : x ∈ E) (hy : y ∈ E) : (F k).lazardValuation (Fin.snoc (Fin.tail x) (x 0)) = (F k).lazardValuation (Fin.snoc (Fin.tail y) (y 0))

On every ambient stack cell the Lazard valuation is constant when its coordinates are read in the original order, with the distinguished coordinate last. This includes zero members.

theorem TauCeti.LazardDelineation.signInvariant_sectionSet {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hS : IsPreconnected S) (k : ι) (i : Fin D.count) : SignInvariant (fun (z : ↑S × ℝ) => (MvPolynomial.eval (Fin.snoc (↑z.1) z.2)) (F k)) (sectionSet D.root i)

Over a preconnected base, every member of a family is sign-invariant on each section of a Lazard delineation.

theorem TauCeti.LazardDelineation.signInvariant_sectorSet {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hS : IsPreconnected S) (k : ι) (j : Fin (D.count + 1)) : SignInvariant (fun (z : ↑S × ℝ) => (MvPolynomial.eval (Fin.snoc (↑z.1) z.2)) (F k)) (sectorSet D.root j)

Over a preconnected base, every member of a family is sign-invariant on each sector of a Lazard delineation.

theorem TauCeti.LazardDelineation.signInvariant_rename_finRotate_of_mem_stackCells {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) (hS : IsPreconnected S) (k : ι) {E : Set (Fin (n + 1) → ℝ)} (hE : E ∈ stackCells S D.root) : SignInvariant (fun (x : Fin (n + 1) → ℝ) => (MvPolynomial.eval x) ((MvPolynomial.rename ⇑(finRotate (n + 1))) (F k))) E

Over a preconnected base, every member of a Lazard delineation is sign-invariant on each ambient stack cell after moving the distinguished coordinate to the front.

theorem TauCeti.LazardDelineation.analyticOnSubmanifold_root {ι : Type u_1} {n : ℕ} {F : ι → MvPolynomial (Fin (n + 1)) ℝ} {S : Set (Fin n → ℝ)} (D : LazardDelineation F S) {d : ℕ} (hS : IsAnalyticSubmanifold d S) (i : Fin D.count) {r : (Fin n → ℝ) → ℝ} (hr : ∀ (x : ↑S), r ↑x = D.root i x) : AnalyticOnSubmanifold d r S

Lazard delineations over analytic submanifolds are analytic. Over an analytic submanifold S, the root functions of a Lazard delineation are analytic on S. Any ambient function agreeing with a root function on S gives the same conclusion.