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;
left_inverse.iterate, right_inverse.iterate, commute.iterate_left, commute.iterate_right, commute.iterate_iterate: some properties of pairs of functions survive under iterations
iterate_fixed, semiconj.iterate_*, semiconj₂.iterate: if f fixes a point (resp., semiconjugates unary/binary operarations), then so does f^[n].

source

@[simp]

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

f^[0] = id

source

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

f^[0] x = x

source

@[simp]

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

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

source

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

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

source

@[simp]

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

id ^[n] = id

source

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

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

source

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

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

source

@[simp]

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

f^[1] = f

source

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

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

source

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

f^[n] x = x

source

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

function.injective f^[n]

source

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

function.surjective f^[n]

source

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

function.bijective f^[n]

source

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

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

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

function.commute f g^[n]

source

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

function.commute f^[n] g

source

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

function.commute f^[m] g^[n]

source

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

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

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

source

theorem function.commute.iterate_self {α : Type u} (f : α → α) (n : ℕ) :

function.commute f^[n] f

source

theorem function.commute.self_iterate {α : Type u} (f : α → α) (n : ℕ) :

function.commute f f^[n]

source

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

function.commute f^[m] f^[n]

source

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

function.semiconj₂ f^[n] op op

source

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

f^[n.succ ] = f ∘ (f^[n])

source

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

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

source

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

f^[n.pred ] ∘ f = (f^[n])

source

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

f ∘ (f^[n.pred ]) = (f^[n])

source

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 n = nat.rec ha (λ (m : ℕ), _.mpr (h (f^[m] a))) n

source

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

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

function.left_inverse g^[n] f^[n]

source

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

function.right_inverse g^[n] f^[n]

source

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

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

source

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

function.commute (λ (f : α → α), f^[m]) (λ (f : α → α), f^[n])