Eventually periodic sequences on ℕ

A sequence a : ℕ → α with a (n + p) = a n for all n ≥ N is periodic of period p beyond the preperiod N. This file reduces its values beyond N to the window [N, N + p), the eventually periodic variant of Mathlib's Function.Periodic.map_mod_nat.

Main results

• TauCeti.Nat.apply_eq_apply_add_sub_mod: beyond the preperiod N, the value at n is the value at N + (n - N) % p.

theorem TauCeti.Nat.apply_eq_apply_add_sub_mod {α : Type u_1} {a : ℕ → α} {N p : ℕ} (h : ∀ (n : ℕ), N ≤ n → a (n + p) = a n) {n : ℕ} (hn : N ≤ n) : a n = a (N + (n - N) % p)

Beyond the preperiod N, an eventually periodic sequence takes at n its value at the representative of n modulo p in [N, N + p).