Sign variations of a list

This file defines List.signVariations, for counting the number of changes of sign in a list after all zeroes were removed. For example, [1, 0, -2, 3, 3] has two sign variations, and so does [1, -2, 3].

This is the counting device behind Descartes' rule of signs (applied to the list of coefficients of the polynomial) and Sturm's theorem (applied to the values of a Sturm sequence at a point, or to the signs of its leading coefficients, adjusted by degree parity at -∞, for the count at infinity).

Main definitions

• List.signVariations l: the number of sign variations of l.

Main results

• List.signVariations_cons_cons_of_ne_zero: the recursion for a list starting with two nonzero entries: prepending a to b :: l adds one variation exactly when sign a ≠ sign b.
• List.signVariations_zero_cons, List.signVariations_cons_zero_cons: zero entries are ignored.
• List.signVariations_map: signVariations only depends on the signs of the entries, so it is invariant under any map preserving signs (for instance the cast ℚ → ℝ, or SignType.sign itself).

def List.signVariations {α : Type u_1} [Zero α] [LinearOrder α] (l : List α) : ℕ

The number of sign variations of a list: the number of adjacent pairs of opposite sign once all zero entries have been removed.

Equations

• l.signVariations = (List.destutter (fun (x1 x2 : SignType) => x1 ≠ x2) (List.filter (fun (x : SignType) => decide (x ≠ 0)) (List.map (⇑SignType.sign) l))).length - 1

@[simp]

theorem List.signVariations_nil {α : Type u_1} [Zero α] [LinearOrder α] : [].signVariations = 0

@[simp]

theorem List.signVariations_singleton {α : Type u_1} [Zero α] [LinearOrder α] (a : α) : [a].signVariations = 0

@[simp]

theorem List.signVariations_zero_cons {α : Type u_1} [Zero α] [LinearOrder α] (l : List α) : (0 :: l).signVariations = l.signVariations

A leading zero entry does not change the sign variations.

@[simp]

theorem List.signVariations_filter_ne_zero {α : Type u_1} [Zero α] [LinearOrder α] (l : List α) : (filter (fun (x : α) => !decide (x = 0)) l).signVariations = l.signVariations

Zero entries do not contribute to the sign variations.

@[simp]

theorem List.signVariations_cons_zero_cons {α : Type u_1} [Zero α] [LinearOrder α] (a : α) (as : List α) : (a :: 0 :: as).signVariations = (a :: as).signVariations

A zero entry in second position does not change the sign variations.

theorem List.signVariations_cons_cons_of_ne_zero {α : Type u_1} [Zero α] [LinearOrder α] {a b : α} (as : List α) (ha : a ≠ 0) (hb : b ≠ 0) : (a :: b :: as).signVariations = (b :: as).signVariations + if SignType.sign a = SignType.sign b then 0 else 1

Prepending a nonzero entry a to a list starting with a nonzero entry b adds one sign variation exactly when a and b have opposite signs.

theorem List.signVariations_congr {α : Type u_1} [Zero α] [LinearOrder α] {β : Type u_2} [Zero β] [LinearOrder β] {l₁ : List α} {l₂ : List β} (h : map (⇑SignType.sign) l₁ = map (⇑SignType.sign) l₂) : l₁.signVariations = l₂.signVariations

signVariations only depends on the signs of the entries.

theorem List.signVariations_map {α : Type u_1} [Zero α] [LinearOrder α] {β : Type u_2} [Zero β] [LinearOrder β] {f : α → β} (hf : ∀ (x : α), SignType.sign (f x) = SignType.sign x) (l : List α) : (map f l).signVariations = l.signVariations

signVariations is invariant under any map that preserves signs (e.g. casts).

@[simp]

theorem List.signVariations_map_sign {α : Type u_1} [Zero α] [LinearOrder α] (l : List α) : (map (⇑SignType.sign) l).signVariations = l.signVariations

@[simp]

theorem List.signVariations_cons_replicate_zero_append {α : Type u_1} [Zero α] [LinearOrder α] (a : α) (n : ℕ) (l : List α) : (a :: (replicate n 0 ++ l)).signVariations = (a :: l).signVariations

A run of zero entries after the head does not change the sign variations.

@[simp]

theorem List.signVariations_cons_replicate_zero {α : Type u_1} [Zero α] [LinearOrder α] (a : α) (n : ℕ) : (a :: replicate n 0).signVariations = 0

A list whose only nonzero entry is the head has no sign variations.

theorem List.signVariations_map_of_sign_eq_neg {α : Type u_1} [Zero α] [LinearOrder α] {β : Type u_2} [Zero β] [LinearOrder β] {f : α → β} (hf : ∀ (x : α), SignType.sign (f x) = -SignType.sign x) (l : List α) : (map f l).signVariations = l.signVariations

signVariations is invariant under any map that negates signs (e.g. negation).