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 operations), then so does f^[n].

def Nat.iterate {α : Sort u} (op : α → α) : ℕ → α → α

Iterate a function.

def «term_^[_]» : Lean.TrailingParserDescr

Iterate a function.

@[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 : ℕ) : id^[n] = id

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.iterate_invariant {α : Type u} {β : Type v} {f : α → α} {g : α → β} (h : g ∘ f = g) (n : ℕ) : g ∘ f^[n] = g

If a function g is invariant under composition with a function f (i.e., g ∘ f = g), then g is invariant under composition with any iterate of f.

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

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

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

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

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

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

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

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

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

theorem Function.Commute.comp_iterate {α : Type u} {f g : α → α} (h : Function.Commute f g) (n : ℕ) : (f ∘ g)^[n] = f^[n] ∘ g^[n]

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

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

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

theorem Function.Semiconj₂.iterate {α : Type u} {f : α → α} {op : α → α → α} (hf : Semiconj₂ f op op) (n : ℕ) : Semiconj₂ f^[n] op 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} (motive : α → Sort u_1) {a : α} (arg : motive a) {f : α → α} (app : (a : α) → motive a → motive (f a)) (n : ℕ) : motive (f^[n] a)

A recursor for the iterate of a function.

theorem Function.Iterate.rec_zero {α : Type u} (motive : α → Sort u_1) {f : α → α} (app : (a : α) → motive a → motive (f a)) {a : α} (arg : motive a) : rec motive arg app 0 = arg

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

theorem Function.RightInverse.iterate {α : Type u} {f g : α → α} (hg : RightInverse g f) (n : ℕ) : RightInverse g^[n] 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 (fun (f : α → α) => f^[m]) fun (f : α → α) => f^[n]

theorem Function.iterate_add_eq_iterate {α : Type u} {f : α → α} {m n : ℕ} {a : α} (hf : 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 : 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 : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a = a

theorem Function.involutive_iff_iter_2_eq_id {α : Sort u_1} {f : α → α} : Involutive f ↔ f^[2] = id

theorem List.foldl_const {α : Type u} {β : Type v} (f : α → α) (a : α) (l : List β) : foldl (fun (b : α) (x : β) => f b) a l = f^[l.length] a

theorem List.foldr_const {α : Type u} {β : Type v} (f : β → β) (b : β) (l : List α) : foldr (fun (x : α) => f) b l = f^[l.length] b

@[simp]

theorem Pi.map_iterate {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i → α i) (n : ℕ) : (Pi.map f)^[n] = Pi.map fun (i : ι) => (f i)^[n]