Extending strictly monotone finite selections of naturals

A strictly monotone selection k : Fin m → ℕ of m natural numbers extends to a strictly monotone self-map φ : ℕ → ℕ agreeing with k on the first m inputs. The extension can be chosen to be an eventual translation, φ n = n + C for m ≤ n: past the selection it shifts by a constant. That clause is what is needed when a reindexing of a sequence by φ must agree, past a finite prefix, with a fixed iterate of the one-sided shift.

Main results

• StrictMono.exists_strictMono_nat_extending_fin_eventually_add: the extension, as an eventual translation.
• StrictMono.exists_strictMono_nat_extending_fin: the extension, without the translation clause.

The extension is adapted from cameronfreer/exchangeability, pinned at e0532e59ceff23edab44dda9ab0655debbc9cc22.

theorem StrictMono.exists_strictMono_nat_extending_fin_eventually_add {m : ℕ} {k : Fin m → ℕ} (hk : StrictMono k) : ∃ (φ : ℕ → ℕ) (C : ℕ), StrictMono φ ∧ (∀ (i : Fin m), φ ↑i = k i) ∧ ∀ (n : ℕ), m ≤ n → φ n = n + C

A strictly monotone finite selection k : Fin m → ℕ extends to a strictly increasing self-map of ℕ that agrees with k on the first m inputs and is eventually a translation: beyond the selection it adds a fixed constant C.

theorem StrictMono.exists_strictMono_nat_extending_fin {m : ℕ} {k : Fin m → ℕ} (hk : StrictMono k) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (i : Fin m), φ ↑i = k i

A strictly monotone finite selection k : Fin m → ℕ extends to a strictly increasing self-map of ℕ that agrees with k on the first m inputs.

StrictMono.exists_strictMono_nat_extending_fin_eventually_add additionally records that the extension is eventually a translation.