Counting the roots below a point by a square substitution

Over an ordered real closed field, the roots of p.comp (C t - X ^ 2) are the square roots of t - r for the roots r ≤ t of p. A root r < t contributes the two roots ±√(t - r), a root at t contributes the single root 0, and roots above t contribute nothing. So, for nonzero p, the number of distinct roots of p below t is determined by the number of distinct roots of p.comp (C t - X ^ 2) and whether t is a root of p. The underlying count of the square roots of a single element a, namely two, one or none as a is positive, zero or negative, is Polynomial.card_nthRootsFinset_two.

Since the coefficients of p.comp (C t - X ^ 2) are polynomials in t and in the coefficients of p, this reduces counting the roots of p in (-∞, t) to counting all distinct roots of another polynomial. It is used to describe the roots of a polynomial family below a moving point by polynomial sign conditions.

theorem Polynomial.card_nthRootsFinset_two {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (a : R) : (nthRootsFinset 2 a).card = if 0 < a then 2 else if a = 0 then 1 else 0

Over an ordered real closed field, a has two square roots ±√a when 0 < a, the single square root 0 when a = 0, and none when a < 0.

theorem Polynomial.card_roots_toFinset_comp_C_sub_X_sq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hp : p ≠ 0) (t : R) : (p.comp (C t - X ^ 2)).roots.toFinset.card = 2 * {r ∈ p.roots.toFinset | r < t}.card + if p.IsRoot t then 1 else 0

Roots below a point by a square substitution. For nonzero p, every root of p below t gives two distinct roots ±√(t - r) of p.comp (C t - X ^ 2), a root at t gives the root 0, and these are all of its roots.