Finite samples of the real line

Polynomial.signSamples p consists of the distinct roots of p and its derivative, together with two points beyond all roots of p. For nonzero p, these points meet every root and every complementary interval. More precisely, every point can be joined to a sample by a root-free closed interval, unless it is itself a root sample. This permits simultaneous sign sampling for any finite family of divisors of p, including over non-Archimedean real closed fields.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 10, for univariate sign determination using roots and complementary intervals.

noncomputable def Polynomial.signSamples {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) : Finset R

Roots and critical points, augmented by two points beyond all the roots. The zero polynomial has a finite sample set too; its infinite zero set is not represented.

Equations

• p.signSamples = p.roots.toFinset ∪ (Polynomial.derivative p).roots.toFinset ∪ {-(∑ x ∈ p.roots.toFinset, |x| + 1), ∑ x ∈ p.roots.toFinset, |x| + 1}

@[simp]

theorem Polynomial.mem_signSamples {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (x : R) : x ∈ p.signSamples ↔ x ∈ p.roots.toFinset ∨ x ∈ (derivative p).roots.toFinset ∨ x = -(∑ y ∈ p.roots.toFinset, |y| + 1) ∨ x = ∑ y ∈ p.roots.toFinset, |y| + 1

Membership in the sample set, with the outer points stated explicitly.

@[simp]

theorem Polynomial.signSamples_of_natDegree_eq_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hp : p.natDegree = 0) : p.signSamples = {-1, 1}

Constant polynomials have just the two outer samples.

@[simp]

theorem Polynomial.signSamples_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : signSamples 0 = {-1, 1}

The zero polynomial has the two outer samples, rather than its entire zero set.

theorem Polynomial.signSamples_nonempty {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) : p.signSamples.Nonempty

There is always an outer sample, even when the polynomial has no roots.

theorem Polynomial.exists_mem_signSamples {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) (hp : p ≠ 0) (x : R) : ∃ y ∈ p.signSamples, y = x ∨ ∀ z ∈ Set.uIcc x y, eval z p ≠ 0

Every point is a root sample or shares a root-free closed interval with a sample. Thus the samples meet all complementary intervals, without a completeness assumption.