Iterations of a function #

In this file we prove simple properties of Nat.iterate f n a.k.a. f^[n]:

iterate_zero, iterate_succ, iterate_succ', iterate_add, iterate_mul: formulas for f^[0], f^[n+1] (two versions), f^[n+m], and f^[n*m];
iterate_id : id^[n]=id;
Injective.iterate, Surjective.iterate, Bijective.iterate : iterates of an injective/surjective/bijective function belong to the same class;
LeftInverse.iterate, RightInverse.iterate, Commute.iterate_left, Commute.iterate_right, Commute.iterate_iterate: some properties of pairs of functions survive under iterations
iterate_fixed, Function.Semiconj.iterate_*, Function.Semiconj₂.iterate: if f fixes a point (resp., semiconjugates unary/binary operarations), then so does f^[n].

source

ink

@[simp]

theorem Function.iterate_zero {α : Type u} (f : α → α) :

f^[0] = id

source

ink

theorem Function.iterate_zero_apply {α : Type u} (f : α → α) (x : α) :

(f ^[0]) x = x

source

ink

@[simp]

theorem Function.iterate_succ {α : Type u} (f : α → α) (n : ℕ) :

f^[Nat.succ n] = f^[n] ∘ f

source

ink

theorem Function.iterate_succ_apply {α : Type u} (f : α → α) (n : ℕ) (x : α) :

(f ^[Nat.succ n]) x = (f ^[n]) (f x)

source

ink

@[simp]

theorem Function.iterate_id {α : Type u} (n : ℕ) :

id^[n] = id

source

ink

theorem Function.iterate_add {α : Type u} (f : α → α) (m : ℕ) (n : ℕ) :

f^[m + n] = f^[m] ∘ f^[n]

source

ink

theorem Function.iterate_add_apply {α : Type u} (f : α → α) (m : ℕ) (n : ℕ) (x : α) :

(f ^[m + n]) x = (f ^[m]) ((f ^[n]) x)

source

ink

@[simp]

theorem Function.iterate_one {α : Type u} (f : α → α) :

f^[1] = f

source

ink

theorem Function.iterate_mul {α : Type u} (f : α → α) (m : ℕ) (n : ℕ) :

f^[m * n] = f^[m]^[n]

source

ink

theorem Function.iterate_fixed {α : Type u} {f : α → α} {x : α} (h : f x = x) (n : ℕ) :

(f ^[n]) x = x

source

ink

theorem Function.Injective.iterate {α : Type u} {f : α → α} (Hinj : Function.Injective f) (n : ℕ) :

Function.Injective (f^[n])

source

ink

theorem Function.Surjective.iterate {α : Type u} {f : α → α} (Hsurj : Function.Surjective f) (n : ℕ) :

Function.Surjective (f^[n])

source

ink

theorem Function.Bijective.iterate {α : Type u} {f : α → α} (Hbij : Function.Bijective f) (n : ℕ) :

Function.Bijective (f^[n])

source

ink

theorem Function.Semiconj.iterate_right {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β} (h : Function.Semiconj f ga gb) (n : ℕ) :

Function.Semiconj f (ga^[n]) (gb^[n])

source

ink

theorem Function.Semiconj.iterate_left {α : Type u} {f : α → α} {g : ℕ → α → α} (H : ∀ (n : ℕ), Function.Semiconj f (g n) (g (n + 1))) (n : ℕ) (k : ℕ) :

Function.Semiconj (f^[n]) (g k) (g (n + k))

source

ink

theorem Function.Commute.iterate_right {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) (n : ℕ) :

Function.Commute f (g^[n])

source

ink

theorem Function.Commute.iterate_left {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) (n : ℕ) :

Function.Commute (f^[n]) g

source

ink

theorem Function.Commute.iterate_iterate {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) (m : ℕ) (n : ℕ) :

Function.Commute (f^[m]) (g^[n])

source

ink

theorem Function.Commute.iterate_eq_of_map_eq {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) (n : ℕ) {x : α} (hx : f x = g x) :

(f ^[n]) x = (g ^[n]) x

source

ink

theorem Function.Commute.comp_iterate {α : Type u} {f : α → α} {g : α → α} (h : Function.Commute f g) (n : ℕ) :

(f ∘ g)^[n] = f^[n] ∘ g^[n]

source

ink

theorem Function.Commute.iterate_self {α : Type u} (f : α → α) (n : ℕ) :

Function.Commute (f^[n]) f

source

ink

theorem Function.Commute.self_iterate {α : Type u} (f : α → α) (n : ℕ) :

Function.Commute f (f^[n])

source

ink

theorem Function.Commute.iterate_iterate_self {α : Type u} (f : α → α) (m : ℕ) (n : ℕ) :

Function.Commute (f^[m]) (f^[n])

source

ink

theorem Function.Semiconj₂.iterate {α : Type u} {f : α → α} {op : α → α → α} (hf : Function.Semiconj₂ f op op) (n : ℕ) :

Function.Semiconj₂ (f^[n]) op op

source

ink

theorem Function.iterate_succ' {α : Type u} (f : α → α) (n : ℕ) :

f^[Nat.succ n] = f ∘ f^[n]

source

ink

theorem Function.iterate_succ_apply' {α : Type u} (f : α → α) (n : ℕ) (x : α) :

(f ^[Nat.succ n]) x = f ((f ^[n]) x)

source

ink

theorem Function.iterate_pred_comp_of_pos {α : Type u} (f : α → α) {n : ℕ} (hn : 0 < n) :

f^[Nat.pred n] ∘ f = f^[n]

source

ink

theorem Function.comp_iterate_pred_of_pos {α : Type u} (f : α → α) {n : ℕ} (hn : 0 < n) :

f ∘ f^[Nat.pred n] = f^[n]

source

ink

def Function.Iterate.rec {α : Type u} (p : α → Sort u_1) {f : α → α} (h : (a : α) → p a → p (f a)) {a : α} (ha : p a) (n : ℕ) :

p ((f ^[n]) a)

A recursor for the iterate of a function.

Equations

Function.Iterate.rec p h ha 0 = ha
Function.Iterate.rec p h ha (Nat.succ m) = Function.Iterate.rec p h (h a ha) m

source

ink

theorem Function.Iterate.rec_zero {α : Type u} (p : α → Sort u_1) {f : α → α} (h : (a : α) → p a → p (f a)) {a : α} (ha : p a) :

Function.Iterate.rec p h ha 0 = ha

source

ink

theorem Function.LeftInverse.iterate {α : Type u} {f : α → α} {g : α → α} (hg : Function.LeftInverse g f) (n : ℕ) :

Function.LeftInverse (g^[n]) (f^[n])

source

ink

theorem Function.RightInverse.iterate {α : Type u} {f : α → α} {g : α → α} (hg : Function.RightInverse g f) (n : ℕ) :

Function.RightInverse (g^[n]) (f^[n])

source

ink

theorem Function.iterate_comm {α : Type u} (f : α → α) (m : ℕ) (n : ℕ) :

f^[n]^[m] = f^[m]^[n]

source

ink

theorem Function.iterate_commute {α : Type u} (m : ℕ) (n : ℕ) :

Function.Commute (fun f => f^[m]) fun f => f^[n]

source

ink

theorem Function.iterate_add_eq_iterate {α : Type u} {f : α → α} {m : ℕ} {n : ℕ} {a : α} (hf : Function.Injective f) :

(f ^[m + n]) a = (f ^[n]) a ↔ (f ^[m]) a = a

source

ink

theorem Function.iterate_cancel_of_add {α : Type u} {f : α → α} {m : ℕ} {n : ℕ} {a : α} (hf : Function.Injective f) :

(f ^[m + n]) a = (f ^[n]) a → (f ^[m]) a = a

Alias of the forward direction of Function.iterate_add_eq_iterate.

source

ink

theorem Function.iterate_cancel {α : Type u} {f : α → α} {m : ℕ} {n : ℕ} {a : α} (hf : Function.Injective f) (ha : (f ^[m]) a = (f ^[n]) a) :

(f ^[m - n]) a = a

source

ink

theorem List.foldl_const {α : Type u} {β : Type v} (f : α → α) (a : α) (l : List β) :

List.foldl (fun b x => f b) a l = (f ^[List.length l]) a

source

ink

theorem List.foldr_const {α : Type u} {β : Type v} (f : β → β) (b : β) (l : List α) :

List.foldr (fun x => f) b l = (f ^[List.length l]) b