Repetition of Functions

We define what it means to apply a function a given number of times. This only works for function where the types of domain and image coincide.

def Function.repeat_fun {α : Type u} (f : α → α) : Nat → α → α

Repetition of a Function defined in the obvious way. Repeating zero times is defined as the id function.

Equations

• Function.repeat_fun f Nat.zero = id
• Function.repeat_fun f j.succ = f ∘ Function.repeat_fun f j

theorem Function.repeat_zero {α : Type u} {f : α → α} {e : α} : repeat_fun f 0 e = e

Applying a zero-times repetition yields the original value.

theorem Function.repeat_succ {α : Type u} {f : α → α} {i : Nat} {e : α} : repeat_fun f i.succ e = f (repeat_fun f i e)

Applying a n+1-times repetition means applying the function to the result of the n-times repetition.

@[simp]

theorem Function.repeat_once {α : Type u} {f : α → α} : repeat_fun f 1 = f

Repeating a function once yields exactly the function.

theorem Function.repeat_swap_one {α : Type u} {f : α → α} {i : Nat} (e : α) : f (repeat_fun f i e) = repeat_fun f i (f e)

It does not matter if we add another repetition on the left or the right.

theorem Function.repeat_swap_one' {α : Type u} {f : α → α} {i : Nat} : f ∘ repeat_fun f i = repeat_fun f i ∘ f

It does not matter if we add another repetition on the left or the right.

theorem Function.repeat_swap {α : Type u} {f : α → α} {i j : Nat} (e : α) : repeat_fun f i (repeat_fun f j e) = repeat_fun f j (repeat_fun f i e)

The numbers of two composed repetitions can be swapped.

theorem Function.repeat_swap' {α : Type u} {f : α → α} {i j : Nat} : repeat_fun f i ∘ repeat_fun f j = repeat_fun f j ∘ repeat_fun f i

The numbers of two composed repetitions can be swapped.

@[simp]

theorem Function.repeat_add {α : Type u} {f : α → α} {i j : Nat} (e : α) : repeat_fun f (i + j) e = repeat_fun f i (repeat_fun f j e)

A (i+j)-times repetition can be split into the composition of an j-times repetition followed by an i-times repetition.

@[simp]

theorem Function.repeat_add' {α : Type u} {f : α → α} {i j : Nat} : repeat_fun f (i + j) = repeat_fun f i ∘ repeat_fun f j

A (i+j)-times repetition can be split into the composition of an j-times repetition followed by an i-times repetition.

theorem Function.repeat_cycle_mul {α : Type u} {f : α → α} (e : α) (i : Nat) (cycle : repeat_fun f i e = e) (j : Nat) : repeat_fun f (i * j) e = e

If a repetition maps a value to itself, then each multiple of the repetition must also map the value to itself.

theorem Function.repeat_move_cycle {α : Type u} (f : α → α) (e : α) (i : Nat) (cycle : repeat_fun f i e = e) (e' : α) (j : Nat) : repeat_fun f j e = e' → repeat_fun f i e' = e'

If some repetition maps a value to itself, then each other value that is part of this loop is also mapped to itself.

theorem Function.repeat_each_reaches_self_of_each_reachable {α : Type u} {f : α → α} (vs : List α) (each_reachable : ∀ (v : α), v ∈ vs → ∃ (k : Nat), 1 ≤ k ∧ ∃ (u : α), u ∈ vs ∧ repeat_fun f k u = v) (u : α) : u ∈ vs → ∃ (l : Nat), 1 ≤ l ∧ repeat_fun f l u = u

Consider a list of values. If each value is reachable by some non-zero number of repetitions from some value, then, for each value in the list, there is a non-zero number of repetitions that maps the value to itself. Intuitively this holds by a pigeonhole argument: if for each value you need to pick a value from that you can reach it, but only finitely many values are available, then eventually you need to complete a cycle.

theorem Function.repeat_globally_cyclic_of_each_cyclic {α : Type u} {f : α → α} (vs : List α) (each_repeats : ∀ (v : α), v ∈ vs → ∃ (l : Nat), 1 ≤ l ∧ repeat_fun f l v = v) : ∃ (l : Nat), 1 ≤ l ∧ ∀ (v : α), v ∈ vs → repeat_fun f l v = v

If each value from a (finite) list is mapped to itself after some number of repetitions, then there is a global repetition number that maps each value from the list to itself. Basically any common multiple of the individual repetition numbers works.

theorem Function.exists_repetition_that_is_inverse_of_surj {α : Type u} {f : α → α} (vs : List α) (surj : surjectiveList f vs vs) : ∃ (k : Nat), ∀ (v : α), v ∈ vs → repeat_fun f k (f v) = v

If a mapping is surjective for a given list of values, then there exists a repetition count $k$ such that repeating $k+1$ times maps each value from the list to itself. Note that we use $k+1$ repetitions as otherwise the result would be trivial for zero repetitions, which correspond to the id function by definition.