The sign variations of a sequence of nonzero signs

A candidate for Mathlib.Data.List.SignVariations: for a sequence s 0, …, s k of integer signs ±1, the number of neighbours that differ is its number of sign variations (List.countP_ne_eq_signVariations).

Main statements

• List.countP_ne_eq_signVariations: the sign variations of a sequence of nonzero signs.

theorem List.countP_ne_eq_signVariations {s : ℕ → ℤ} {k : ℕ} (hs : ∀ n ≤ k, s n = -1 ∨ s n = 1) : countP (fun (n : ℕ) => s n != s (n + 1)) (range k) = (map s (range (k + 1))).signVariations

The number of neighbours that differ in a sequence of nonzero signs is its number of sign variations.