# mathlib3documentation

logic.function.iterate

# Iterations of a function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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].

@[simp]
theorem function.iterate_zero {α : Type u} (f : α α) :
f^[0] = id
theorem function.iterate_zero_apply {α : Type u} (f : α α) (x : α) :
f^[0] x = x
@[simp]
theorem function.iterate_succ {α : Type u} (f : α α) (n : ) :
f^[n.succ] = f^[n] f
theorem function.iterate_succ_apply {α : Type u} (f : α α) (n : ) (x : α) :
f^[n.succ] x = f^[n] (f x)
@[simp]
theorem function.iterate_id {α : Type u} (n : ) :
theorem function.iterate_add {α : Type u} (f : α α) (m n : ) :
f^[m + n] = f^[m] (f^[n])
theorem function.iterate_add_apply {α : Type u} (f : α α) (m n : ) (x : α) :
f^[m + n] x = f^[m] (f^[n] x)
@[simp]
theorem function.iterate_one {α : Type u} (f : α α) :
f^[1] = f
theorem function.iterate_mul {α : Type u} (f : α α) (m n : ) :
f^[m * n] = (f^[m]^[n])
theorem function.iterate_fixed {α : Type u} {f : α α} {x : α} (h : f x = x) (n : ) :
f^[n] x = x
theorem function.injective.iterate {α : Type u} {f : α α} (Hinj : function.injective f) (n : ) :
theorem function.surjective.iterate {α : Type u} {f : α α} (Hsurj : function.surjective f) (n : ) :
theorem function.bijective.iterate {α : Type u} {f : α α} (Hbij : function.bijective f) (n : ) :
theorem function.semiconj.iterate_right {α : Type u} {β : Type v} {f : α β} {ga : α α} {gb : β β} (h : gb) (n : ) :
ga^[n] gb^[n]
theorem function.semiconj.iterate_left {α : Type u} {f : α α} {g : α α} (H : (n : ), (g n) (g (n + 1))) (n k : ) :
(g k) (g (n + k))
theorem function.commute.iterate_right {α : Type u} {f g : α α} (h : g) (n : ) :
theorem function.commute.iterate_left {α : Type u} {f g : α α} (h : g) (n : ) :
theorem function.commute.iterate_iterate {α : Type u} {f g : α α} (h : g) (m n : ) :
theorem function.commute.iterate_eq_of_map_eq {α : Type u} {f g : α α} (h : g) (n : ) {x : α} (hx : f x = g x) :
f^[n] x = g^[n] x
theorem function.commute.comp_iterate {α : Type u} {f g : α α} (h : g) (n : ) :
f g^[n] = f^[n] (g^[n])
theorem function.commute.iterate_self {α : Type u} (f : α α) (n : ) :
theorem function.commute.self_iterate {α : Type u} (f : α α) (n : ) :
theorem function.commute.iterate_iterate_self {α : Type u} (f : α α) (m n : ) :
theorem function.semiconj₂.iterate {α : Type u} {f : α α} {op : α α α} (hf : op) (n : ) :
op
theorem function.iterate_succ' {α : Type u} (f : α α) (n : ) :
f^[n.succ] = f (f^[n])
theorem function.iterate_succ_apply' {α : Type u} (f : α α) (n : ) (x : α) :
f^[n.succ] x = f (f^[n] x)
theorem function.iterate_pred_comp_of_pos {α : Type u} (f : α α) {n : } (hn : 0 < n) :
f^[n.pred] f = (f^[n])
theorem function.comp_iterate_pred_of_pos {α : Type u} (f : α α) {n : } (hn : 0 < n) :
f (f^[n.pred]) = (f^[n])
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
• ha n = nat.rec ha (λ (m : ), _.mpr (h (f^[m] a))) n
theorem function.iterate.rec_zero {α : Type u} (p : α Sort u_1) {f : α α} (h : Π (a : α), p a p (f a)) {a : α} (ha : p a) :
ha 0 = ha
theorem function.left_inverse.iterate {α : Type u} {f g : α α} (hg : f) (n : ) :
theorem function.right_inverse.iterate {α : Type u} {f g : α α} (hg : f) (n : ) :
theorem function.iterate_comm {α : Type u} (f : α α) (m n : ) :
f^[n]^[m] = (f^[m]^[n])
theorem function.iterate_commute {α : Type u} (m n : ) :
function.commute (λ (f : α α), f^[m]) (λ (f : α α), f^[n])
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
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.

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
theorem list.foldl_const {α : Type u} {β : Type v} (f : α α) (a : α) (l : list β) :
list.foldl (λ (b : α) (_x : β), f b) a l = f^[l.length] a
theorem list.foldr_const {α : Type u} {β : Type v} (f : β β) (b : β) (l : list α) :
list.foldr (λ (_x : α), f) b l = f^[l.length] b