Permanences minus variations with zero gaps

List.permanencesMinusVariations is the integer-valued sign statistic used in signed subresultant formulas for Cauchy indices. Leading and trailing zeros are ignored. Two consecutive nonzero entries with k intervening zeros contribute (-1) ^ (Nat.choose k 2) * sign(a) * sign(b) when k is even, and zero otherwise. In particular, interior zeros cannot simply be deleted.

The zero-gap recursion characterizes the statistic, and sign-preserving and sign-reversing maps preserve it; in particular, so does scaling every entry by a nonzero constant. For a list without zeros it is the number of adjacent pairs minus twice Mathlib's List.signVariations.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4 (permanences minus variations of signed subresultants).

def List.permanencesMinusVariations {R : Type u_1} [Zero R] [LinearOrder R] (l : List R) : ℤ

Sum over consecutive nonzero entries, retaining the parity and length of each intervening zero gap. Leading and trailing zeros contribute nothing.

Equations

• l.permanencesMinusVariations = TauCeti.pmvAux✝ 0 0 (List.map (⇑SignType.sign) l)

@[simp]

theorem List.permanencesMinusVariations_nil {R : Type u_1} [Zero R] [LinearOrder R] : [].permanencesMinusVariations = 0

@[simp]

theorem List.permanencesMinusVariations_zero_cons {R : Type u_1} [Zero R] [LinearOrder R] (l : List R) : (0 :: l).permanencesMinusVariations = l.permanencesMinusVariations

@[simp]

theorem List.permanencesMinusVariations_singleton {R : Type u_1} [Zero R] [LinearOrder R] (a : R) : [a].permanencesMinusVariations = 0

@[simp]

theorem List.permanencesMinusVariations_replicate_zero {R : Type u_1} [Zero R] [LinearOrder R] (n : ℕ) : (replicate n 0).permanencesMinusVariations = 0

@[simp]

theorem List.permanencesMinusVariations_replicate_zero_append {R : Type u_1} [Zero R] [LinearOrder R] (n : ℕ) (l : List R) : (replicate n 0 ++ l).permanencesMinusVariations = l.permanencesMinusVariations

A prefix of zeros is ignored.

@[simp]

theorem List.permanencesMinusVariations_append_replicate_zero {R : Type u_1} [Zero R] [LinearOrder R] (l : List R) (n : ℕ) : (l ++ replicate n 0).permanencesMinusVariations = l.permanencesMinusVariations

A suffix of zeros is ignored.

@[simp]

theorem List.permanencesMinusVariations_cons_replicate_zero {R : Type u_1} [Zero R] [LinearOrder R] (a : R) (n : ℕ) : (a :: replicate n 0).permanencesMinusVariations = 0

A list with only its head possibly nonzero has no adjacent nonzero pair.

theorem List.permanencesMinusVariations_cons_replicate_zero_append {R : Type u_1} [Zero R] [LinearOrder R] {a b : R} (hb : b ≠ 0) (k : ℕ) (l : List R) : (a :: (replicate k 0 ++ b :: l)).permanencesMinusVariations = (if Even k then (-1) ^ k.choose 2 * ↑(SignType.sign a) * ↑(SignType.sign b) else 0) + (b :: l).permanencesMinusVariations

Recursion across a zero gap ending at a nonzero entry. This also specifies the sign correction for even gaps and the cancellation for odd gaps.

theorem List.permanencesMinusVariations_cons_cons {R : Type u_1} [Zero R] [LinearOrder R] {a b : R} (hb : b ≠ 0) (l : List R) : (a :: b :: l).permanencesMinusVariations = ↑(SignType.sign a) * ↑(SignType.sign b) + (b :: l).permanencesMinusVariations

Without an intervening zero, an adjacent pair contributes the product of its signs.

theorem List.permanencesMinusVariations_append_replicate_zero_cons {R : Type u_1} [Zero R] [LinearOrder R] (l m : List R) {a b : R} (ha : a ≠ 0) (hb : b ≠ 0) (k : ℕ) : (l ++ a :: (replicate k 0 ++ b :: m)).permanencesMinusVariations = ((l ++ [a]).permanencesMinusVariations + if Even k then (-1) ^ k.choose 2 * ↑(SignType.sign a) * ↑(SignType.sign b) else 0) + (b :: m).permanencesMinusVariations

Joining two blocks whose boundary entries are nonzero adds precisely the contribution of the intervening zero gap to their separate statistics.

theorem List.permanencesMinusVariations_congr {R : Type u_1} {S : Type u_2} [Zero R] [LinearOrder R] [Zero S] [LinearOrder S] {l : List R} {m : List S} (h : map (⇑SignType.sign) l = map (⇑SignType.sign) m) : l.permanencesMinusVariations = m.permanencesMinusVariations

The statistic depends only on the ordered list of signs, including zeros.

theorem List.permanencesMinusVariations_map {R : Type u_1} {S : Type u_2} [Zero R] [LinearOrder R] [Zero S] [LinearOrder S] {f : R → S} (hf : ∀ (x : R), SignType.sign (f x) = SignType.sign x) (l : List R) : (map f l).permanencesMinusVariations = l.permanencesMinusVariations

Sign-preserving maps preserve permanences minus variations.

@[simp]

theorem List.permanencesMinusVariations_map_sign {R : Type u_1} [Zero R] [LinearOrder R] (l : List R) : (map (⇑SignType.sign) l).permanencesMinusVariations = l.permanencesMinusVariations

theorem List.permanencesMinusVariations_map_of_sign_eq_neg {R : Type u_1} {S : Type u_2} [Zero R] [LinearOrder R] [Zero S] [LinearOrder S] {f : R → S} (hf : ∀ (x : R), SignType.sign (f x) = -SignType.sign x) (l : List R) : (map f l).permanencesMinusVariations = l.permanencesMinusVariations

Reversing every sign preserves the products of consecutive nonzero signs.

@[simp]

theorem List.permanencesMinusVariations_map_mul_left {K : Type u_3} [Ring K] [LinearOrder K] [IsStrictOrderedRing K] {c : K} (hc : c ≠ 0) (l : List K) : (map (fun (x : K) => c * x) l).permanencesMinusVariations = l.permanencesMinusVariations

Multiplying every entry by a nonzero constant preserves permanences minus variations.

theorem List.permanencesMinusVariations_eq_length_sub_two_mul_signVariations {R : Type u_1} [Zero R] [LinearOrder R] (l : List R) (h : ∀ a ∈ l, a ≠ 0) : l.permanencesMinusVariations = ↑(l.length - 1) - 2 * ↑l.signVariations

On a list with no zeros, permanences minus variations is the number of adjacent pairs minus twice the number of sign changes.