Sign-pattern counts from integer product queries

A quadratic polynomial on {-1, 0, 1} gives twice the indicator of a requested sign. Multiplying these indicators expresses 2 ^ k times a sign-pattern count as an integer combination of 3 ^ k product-sign queries. No division or selection of matrix rows is needed.

For a polynomial's roots, the queries and counts use roots.toFinset, so each distinct real root contributes once, independently of its multiplicity. Mathlib assigns the zero polynomial an empty root multiset. The equivalence with existence of a real root therefore requires a nonzero polynomial.

This is a counting identity. It does not supply an algorithm for evaluating a sign query or a time or space bound for sign determination.

Main definitions

• Cslib.SignQueries.signCount: the number of points realizing a sign pattern.
• Cslib.SignQueries.weight: the coefficients of the quadratics giving twice the indicator of a sign.
• Cslib.SignQueries.patternWeight: the coefficient of an exponent vector in the expanded indicator product.
• Cslib.SignQueries.queryPolynomial: a product with exponents in {0, 1, 2}.
• Cslib.SignQueries.signSum: the sum of the signs of a polynomial on a finite set of points.
• Cslib.SignQueries.tarskiQuery: the sum of signs at distinct real roots.
• Cslib.SignQueries.scaledRootCount: the integer combination of root sign queries.

Main results

• Cslib.SignQueries.weighted_queries_eq_count: the finite sign-pattern counting identity.
• Cslib.SignQueries.scaledRootCount_eq: its specialization to distinct real roots.
• Cslib.SignQueries.scaledRootCount_pos_iff: for a nonzero polynomial, a positive scaled count is equivalent to existence of a root realizing the requested sign pattern.

References

Adapted from LeanCanny/Algebra/ScaledSignQueries.lean in [lea26].

def Cslib.SignQueries.weight (s : SignType) (e : Fin 3) : ℤ

The coefficient of X ^ e in the quadratic that gives twice the indicator of sign s. The three quadratics are 2 - 2 * X ^ 2, X ^ 2 - X, and X ^ 2 + X.

theorem Cslib.SignQueries.query_count {J : Type u_1} [Fintype J] [DecidableEq J] : Fintype.card (J → Fin 3) = 3 ^ Fintype.card J

There are 3 ^ k exponent choices for a family of k polynomials.

def Cslib.SignQueries.patternWeight {J : Type u_1} [Fintype J] (σ : J → SignType) (e : J → Fin 3) : ℤ

The coefficient assigned to an exponent vector when expanding the indicator product.

noncomputable def Cslib.SignQueries.signSum (Z : Finset ℝ) (q : Polynomial ℝ) : ℤ

The sum of the signs of q on a finite set of real points.

noncomputable def Cslib.SignQueries.signCount {J : Type u_1} (Z : Finset ℝ) (Q : J → Polynomial ℝ) (σ : J → SignType) : ℕ

The number of points in Z at which every polynomial has its requested sign.

noncomputable def Cslib.SignQueries.queryPolynomial {R : Type u_1} [CommSemiring R] {J : Type u_2} [Fintype J] (Q : J → Polynomial R) (e : J → Fin 3) : Polynomial R

The product query polynomial, with each input polynomial raised to 0, 1, or 2.

theorem Cslib.SignQueries.weighted_queries_eq_count {J : Type u_1} [Fintype J] [DecidableEq J] (Z : Finset ℝ) (Q : J → Polynomial ℝ) (σ : J → SignType) : ∑ e : J → Fin 3, patternWeight σ e * signSum Z (queryPolynomial Q e) = 2 ^ Fintype.card J * ↑(signCount Z Q σ)

The weighted product-sign queries equal 2 ^ k times the number of matching points.

noncomputable def Cslib.SignQueries.tarskiQuery (p q : Polynomial ℝ) : ℤ

The Tarski query of q at the distinct real roots of p. For p = 0, this is zero by Mathlib's root-multiset convention.

noncomputable def Cslib.SignQueries.scaledRootCount {J : Type u_1} [Fintype J] [DecidableEq J] (p : Polynomial ℝ) (Q : J → Polynomial ℝ) (σ : J → SignType) : ℤ

The weighted sum of product-sign queries for roots realizing a sign pattern.

theorem Cslib.SignQueries.scaledRootCount_eq {J : Type u_1} [Fintype J] [DecidableEq J] (p : Polynomial ℝ) (Q : J → Polynomial ℝ) (σ : J → SignType) : scaledRootCount p Q σ = 2 ^ Fintype.card J * ↑(signCount p.roots.toFinset Q σ)

The scaled count is 2 ^ k times the number of distinct matching real roots.

@[simp]

theorem Cslib.SignQueries.scaledRootCount_zero_left {J : Type u_1} [Fintype J] [DecidableEq J] (Q : J → Polynomial ℝ) (σ : J → SignType) : scaledRootCount 0 Q σ = 0

The zero polynomial's scaled count is zero, since its root multiset is empty.

theorem Cslib.SignQueries.signCount_roots_pos_iff {J : Type u_1} (p : Polynomial ℝ) (hp : p ≠ 0) (Q : J → Polynomial ℝ) (σ : J → SignType) : 0 < signCount p.roots.toFinset Q σ ↔ ∃ (x : ℝ), Polynomial.eval x p = 0 ∧ ∀ (i : J), SignType.sign (Polynomial.eval x (Q i)) = σ i

For a nonzero polynomial, a positive count means a real root realizes the sign pattern.

theorem Cslib.SignQueries.scaledRootCount_pos_iff {J : Type u_1} [Fintype J] [DecidableEq J] (p : Polynomial ℝ) (hp : p ≠ 0) (Q : J → Polynomial ℝ) (σ : J → SignType) : 0 < scaledRootCount p Q σ ↔ ∃ (x : ℝ), Polynomial.eval x p = 0 ∧ ∀ (i : J), SignType.sign (Polynomial.eval x (Q i)) = σ i

For a nonzero polynomial, the integer combination of sign queries is positive exactly when a real root realizes the requested sign pattern.