Polynomial sign counts and Tarski queries

Finset.signCount counts the points of a finite set realizing a given polynomial sign condition. Finset.signSum sums a polynomial's signs on that set. Polynomial.tarskiQuery p q specializes the sum to the distinct roots of p. For nonzero p its cardinality characterization counts the actual zeros of p; for p = 0 the value is zero and does not describe the infinite zero set.

The definitions and their basic API are independent of matrix inversion.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 10, for sign conditions and Tarski queries.

noncomputable def Finset.signCount {R : Type u_1} [Semiring R] [LinearOrder R] {J : Type u_2} (Z : Finset R) (Q : J → Polynomial R) (σ : J → SignType) : ℕ

The number of points realizing a specified polynomial sign condition.

Equations

• Z.signCount Q σ = Function.occCount (fun (x : ↥Z) (j : J) => SignType.sign (Polynomial.eval (↑x) (Q j))) σ

theorem Finset.signCount_eq_occCount {R : Type u_1} [Semiring R] [LinearOrder R] {J : Type u_2} (Z : Finset R) (Q : J → Polynomial R) (σ : J → SignType) : Z.signCount Q σ = Function.occCount (fun (x : ↥Z) (j : J) => SignType.sign (Polynomial.eval (↑x) (Q j))) σ

Polynomial sign counts are multiplicities in the finite family of pointwise signs.

theorem Finset.signCount_eq_card_filter {R : Type u_1} [Semiring R] [LinearOrder R] {J : Type u_2} (Z : Finset R) (Q : J → Polynomial R) (σ : J → SignType) : Z.signCount Q σ = {x ∈ Z | ∀ (j : J), SignType.sign (Polynomial.eval x (Q j)) = σ j}.card

Sign counts are cardinalities of the realizing subset of the original finite set.

@[simp]

theorem Finset.signCount_empty {R : Type u_1} [Semiring R] [LinearOrder R] {J : Type u_2} (Q : J → Polynomial R) (σ : J → SignType) : ∅.signCount Q σ = 0

theorem Finset.sum_signCount {R : Type u_1} [Semiring R] [LinearOrder R] {J : Type u_2} [Fintype J] [DecidableEq J] (Z : Finset R) (Q : J → Polynomial R) : ∑ σ : J → SignType, Z.signCount Q σ = Z.card

The sign conditions partition the original finite set of points.

@[simp]

theorem Finset.signCount_pos {R : Type u_1} [Semiring R] [LinearOrder R] {J : Type u_2} (Z : Finset R) (Q : J → Polynomial R) (σ : J → SignType) : 0 < Z.signCount Q σ ↔ ∃ x ∈ Z, ∀ (j : J), SignType.sign (Polynomial.eval x (Q j)) = σ j

A positive sign count is equivalent to realization at a point of the finite set.

noncomputable def Finset.signSum {R : Type u_1} [Semiring R] [LinearOrder R] (Z : Finset R) (p : Polynomial R) : ℤ

The integer sum of signs at a specified finite set of points.

Equations

• Z.signSum p = ∑ x : ↥Z, ↑(SignType.sign (Polynomial.eval (↑x) p))

theorem Finset.signSum_eq_sum_subtype {R : Type u_1} [Semiring R] [LinearOrder R] (Z : Finset R) (p : Polynomial R) : Z.signSum p = ∑ x : ↥Z, ↑(SignType.sign (Polynomial.eval (↑x) p))

Sign sums are integer sums of pointwise polynomial signs.

theorem Finset.signSum_eq_sum {R : Type u_1} [Semiring R] [LinearOrder R] (Z : Finset R) (p : Polynomial R) : Z.signSum p = ∑ x ∈ Z, ↑(SignType.sign (Polynomial.eval x p))

Sign sums expressed directly over the original finite set.

@[simp]

theorem Finset.signSum_empty {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) : ∅.signSum p = 0

@[simp]

theorem Finset.signSum_zero {R : Type u_1} [Semiring R] [LinearOrder R] (Z : Finset R) : Z.signSum 0 = 0

@[simp]

theorem Finset.signSum_one {R : Type u_1} [Semiring R] [LinearOrder R] [ZeroLEOneClass R] [NeZero 1] (Z : Finset R) : Z.signSum 1 = ↑Z.card

theorem Finset.signSum_eq_card_sub_card {R : Type u_1} [Semiring R] [LinearOrder R] (Z : Finset R) (p : Polynomial R) : Z.signSum p = ↑{x ∈ Z | 0 < Polynomial.eval x p}.card - ↑{x ∈ Z | Polynomial.eval x p < 0}.card

A finite sign sum is the number of positive evaluations minus the number of negative ones.

noncomputable def Polynomial.tarskiQuery {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] (p q : Polynomial R) : ℤ

Sum of the signs of q at the distinct roots of p, with value zero when p = 0.

Equations

• p.tarskiQuery q = p.roots.toFinset.signSum q

theorem Polynomial.tarskiQuery_eq_signSum {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] (p q : Polynomial R) : p.tarskiQuery q = p.roots.toFinset.signSum q

theorem Polynomial.tarskiQuery_eq_sum {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] (p q : Polynomial R) : p.tarskiQuery q = ∑ x ∈ p.roots.toFinset, ↑(SignType.sign (eval x q))

The Tarski query expressed as a sum over distinct polynomial roots.

theorem Polynomial.tarskiQuery_eq_card_sub_card {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] (p q : Polynomial R) : p.tarskiQuery q = ↑{x ∈ p.roots.toFinset | 0 < eval x q}.card - ↑{x ∈ p.roots.toFinset | eval x q < 0}.card

The number of distinct roots of p where q is positive minus the number where q is negative.

@[simp]

theorem Polynomial.tarskiQuery_zero_left {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] (q : Polynomial R) : tarskiQuery 0 q = 0

@[simp]

theorem Polynomial.tarskiQuery_zero_right {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] (p : Polynomial R) : p.tarskiQuery 0 = 0

@[simp]

theorem Polynomial.tarskiQuery_one_right {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] [ZeroLEOneClass R] (p : Polynomial R) : p.tarskiQuery 1 = ↑p.roots.toFinset.card

theorem Polynomial.signCount_roots_eq_natCard {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] {J : Type u_2} {p : Polynomial R} (hp : p ≠ 0) (Q : J → Polynomial R) (σ : J → SignType) : p.roots.toFinset.signCount Q σ = Nat.card { x : R // eval x p = 0 ∧ ∀ (j : J), SignType.sign (eval x (Q j)) = σ j }

Counts at the roots of a nonzero polynomial count exactly its realizing zeros.

theorem Polynomial.tarskiQuery_eq_sub {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] {p : Polynomial R} (hp : p ≠ 0) (q : Polynomial R) : p.tarskiQuery q = ↑(Nat.card { x : R // eval x p = 0 ∧ 0 < eval x q }) - ↑(Nat.card { x : R // eval x p = 0 ∧ eval x q < 0 })

A Tarski query counts the zeros of p where q is positive, minus those where q is negative.

theorem Polynomial.signCount_roots_pos {R : Type u_1} [CommRing R] [IsDomain R] [LinearOrder R] {J : Type u_2} {p : Polynomial R} (hp : p ≠ 0) (Q : J → Polynomial R) (σ : J → SignType) : 0 < p.roots.toFinset.signCount Q σ ↔ ∃ (x : R), eval x p = 0 ∧ ∀ (j : J), SignType.sign (eval x (Q j)) = σ j

A positive count at the roots of a nonzero polynomial is an actual realizable condition.