Mapping along a reversed range

Lists of the form [f (b - 1), …, f 0], that is (List.range b).reverse.map f, record coefficient sequences from the top index down. This file peels off the top entry and collapses a run of vanishing entries at the top into a block of zeros.

Main results

• List.map_reverse_range_succ: the list [f k, …, f 0] begins with f k.
• List.map_reverse_range_eq_replicate_append: if f vanishes on [a, b), then [f (b - 1), …, f 0] is b - a zeros followed by [f (a - 1), …, f 0].

theorem List.map_reverse_range_succ {α : Type u_1} (f : ℕ → α) (k : ℕ) : map f (range (k + 1)).reverse = f k :: map f (range k).reverse

The list [f k, …, f 0] begins with f k.

theorem List.map_reverse_range_eq_replicate_append {α : Type u_1} [Zero α] (f : ℕ → α) {a b : ℕ} (hab : a ≤ b) (h : ∀ (j : ℕ), a ≤ j → j < b → f j = 0) : map f (range b).reverse = replicate (b - a) 0 ++ map f (range a).reverse

Mapping a function along the reversed range [b - 1, …, 0], where it vanishes on [a, b), gives b - a zeros followed by the map along [a - 1, …, 0].