Mathlib.Logic.Function.Iterate

Nat.iterate definition

{α : Sort u} (op : α → α) : ℕ → α → α

Full source

/-- Iterate a function. -/
def Nat.iterate {α : Sort u} (op : α → α) : ℕ → α → α
  | 0, a => a
  | succ k, a => iterate op k (op a)

Iteration of a function

Informal description

The $n$-th iterate of a function $f : \alpha \to \alpha$ is the function obtained by composing $f$ with itself $n$ times. Formally, it is defined recursively as: - $f^[0](x) = x$ (the identity function), - $f^[n+1](x) = f^[n](f(x))$ for any natural number $n$.

term_^[_] definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc Nat.iterate]
notation:max f "^["n"]" => Nat.iterate f n

Iterated function application $ f^{[n]} $

Informal description

The notation $ f^{[n]} $ denotes the $ n $-th iterate of the function $ f $, defined as applying $ f $ $ n $ times to its argument. For example, $ f^{[0]} $ is the identity function, and $ f^{[n+1]} = f \circ f^{[n]} $.

Function.iterate_zero theorem

: f^[0] = id

Full source

@[simp]
theorem iterate_zero : f^[0] = id :=
  rfl

Zeroth Iteration is Identity Function

Informal description

The zeroth iteration of any function $f$ is equal to the identity function, i.e., $f^[0] = \text{id}$.

Function.iterate_zero_apply theorem

(x : α) : f^[0] x = x

Full source

theorem iterate_zero_apply (x : α) : f^[0] x = x :=
  rfl

Zeroth Iteration Acts as Identity on Elements

Informal description

For any element $x$ of type $\alpha$, the zeroth iteration of a function $f$ applied to $x$ equals $x$, i.e., $f^[0](x) = x$.

Function.iterate_succ theorem

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

Full source

@[simp]
theorem iterate_succ (n : ℕ) : f^[n.succ] = f^[n]f^[n] ∘ f :=
  rfl

Iteration Composition: $f^{[n+1]} = f^{[n]} \circ f$

Informal description

For any function $f : \alpha \to \alpha$ and natural number $n$, the $(n+1)$-th iterate of $f$ is equal to the composition of the $n$-th iterate of $f$ with $f$ itself, i.e., $f^{[n+1]} = f^{[n]} \circ f$.

Function.iterate_succ_apply theorem

(n : ℕ) (x : α) : f^[n.succ] x = f^[n] (f x)

Full source

theorem iterate_succ_apply (n : ℕ) (x : α) : f^[n.succ] x = f^[n] (f x) :=
  rfl

Recursive Formula for Function Iteration: $f^{[n+1]}(x) = f^{[n]}(f(x))$

Informal description

For any natural number $n$ and any element $x \in \alpha$, the $(n+1)$-th iterate of a function $f : \alpha \to \alpha$ satisfies $f^{[n+1]}(x) = f^{[n]}(f(x))$.

Function.iterate_id theorem

(n : ℕ) : (id : α → α)^[n] = id

Full source

@[simp]
theorem iterate_id (n : ℕ) : (id : α → α)^[n] = id :=
  Nat.recOn n rfl fun n ihn ↦ by rw [iterate_succ, ihn, id_comp]

Iteration of Identity Function: $\mathrm{id}^{[n]} = \mathrm{id}$

Informal description

For any natural number $n$, the $n$-th iterate of the identity function $\mathrm{id} \colon \alpha \to \alpha$ is equal to the identity function itself, i.e., $\mathrm{id}^{[n]} = \mathrm{id}$.

Function.iterate_add theorem

(m : ℕ) : ∀ n : ℕ, f^[m + n] = f^[m] ∘ f^[n]

Full source

theorem iterate_add (m : ℕ) : ∀ n : ℕ, f^[m + n] = f^[m]f^[m] ∘ f^[n]
  | 0 => rfl
  | Nat.succ n => by rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]; rfl

Additivity of Function Iteration: $f^{[m+n]} = f^{[m]} \circ f^{[n]}$

Informal description

For any natural numbers $m$ and $n$, the $(m+n)$-th iterate of a function $f : \alpha \to \alpha$ is equal to the composition of the $m$-th iterate and the $n$-th iterate of $f$, i.e., $f^{[m+n]} = f^{[m]} \circ f^{[n]}$.

Function.iterate_add_apply theorem

(m n : ℕ) (x : α) : f^[m + n] x = f^[m] (f^[n] x)

Full source

theorem iterate_add_apply (m n : ℕ) (x : α) : f^[m + n] x = f^[m] (f^[n] x) := by
  rw [iterate_add f m n]
  rfl

Additivity of Function Iteration Applied to Point: $f^{[m+n]}(x) = f^{[m]}(f^{[n]}(x))$

Informal description

For any natural numbers $m$ and $n$ and any element $x \in \alpha$, the $(m+n)$-th iterate of a function $f : \alpha \to \alpha$ applied to $x$ equals the $m$-th iterate of $f$ applied to the $n$-th iterate of $f$ applied to $x$, i.e., $f^{[m+n]}(x) = f^{[m]}(f^{[n]}(x))$.

Function.iterate_one theorem

: f^[1] = f

Full source

@[simp high]
theorem iterate_one : f^[1] = f :=
  funext fun _ ↦ rfl

First Iterate Equals Original Function

Informal description

The first iterate of a function $f : \alpha \to \alpha$ is equal to $f$ itself, i.e., $f^[1] = f$.

Function.iterate_mul theorem

(m : ℕ) : ∀ n, f^[m * n] = f^[m]^[n]

Full source

theorem iterate_mul (m : ℕ) : ∀ n, f^[m * n] = f^[m]f^[m]^[n]
  | 0 => by simp only [Nat.mul_zero, iterate_zero]
  | n + 1 => by simp only [Nat.mul_succ, Nat.mul_one, iterate_one, iterate_add, iterate_mul m n]

Multiplicativity of Function Iteration: $f^{[m \cdot n]} = (f^{[m]})^{[n]}$

Informal description

For any natural numbers $m$ and $n$, the $(m \cdot n)$-th iterate of a function $f \colon \alpha \to \alpha$ is equal to the $n$-th iterate of the $m$-th iterate of $f$, i.e., $f^{[m \cdot n]} = (f^{[m]})^{[n]}$.

Function.iterate_fixed theorem

{x} (h : f x = x) (n : ℕ) : f^[n] x = x

Full source

theorem iterate_fixed {x} (h : f x = x) (n : ℕ) : f^[n] x = x :=
  Nat.recOn n rfl fun n ihn ↦ by rw [iterate_succ_apply, h, ihn]

Fixed Point Property Under Iteration: $f^{[n]}(x) = x$ when $f(x) = x$

Informal description

For any function $f \colon \alpha \to \alpha$ and any element $x \in \alpha$ such that $f(x) = x$, the $n$-th iterate of $f$ evaluated at $x$ satisfies $f^{[n]}(x) = x$ for all natural numbers $n$.

Function.Injective.iterate theorem

(Hinj : Injective f) (n : ℕ) : Injective f^[n]

Full source

theorem Injective.iterate (Hinj : Injective f) (n : ℕ) : Injective f^[n] :=
  Nat.recOn n injective_id fun _ ihn ↦ ihn.comp Hinj

Injectivity is Preserved Under Iteration

Informal description

If a function $f \colon \alpha \to \alpha$ is injective, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is also injective.

Function.Surjective.iterate theorem

(Hsurj : Surjective f) (n : ℕ) : Surjective f^[n]

Full source

theorem Surjective.iterate (Hsurj : Surjective f) (n : ℕ) : Surjective f^[n] :=
  Nat.recOn n surjective_id fun _ ihn ↦ ihn.comp Hsurj

Surjectivity is Preserved Under Iteration

Informal description

If a function $f \colon \alpha \to \alpha$ is surjective, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is also surjective.

Function.Bijective.iterate theorem

(Hbij : Bijective f) (n : ℕ) : Bijective f^[n]

Full source

theorem Bijective.iterate (Hbij : Bijective f) (n : ℕ) : Bijective f^[n] :=
  ⟨Hbij.1.iterate n, Hbij.2.iterate n⟩

Bijectivity is Preserved Under Iteration

Informal description

If a function $f \colon \alpha \to \alpha$ is bijective, then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is also bijective.

Function.Semiconj.iterate_right theorem

{f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) (n : ℕ) : Semiconj f ga^[n] gb^[n]

Full source

theorem iterate_right {f : α → β} {ga : α → α} {gb : β → β} (h : Semiconj f ga gb) (n : ℕ) :
    Semiconj f ga^[n] gb^[n] :=
  Nat.recOn n id_right fun _ ihn ↦ ihn.comp_right h

Iteration Preserves Semiconjugacy

Informal description

Let $f \colon \alpha \to \beta$ be a function that semiconjugates $g_a \colon \alpha \to \alpha$ to $g_b \colon \beta \to \beta$, i.e., $f \circ g_a = g_b \circ f$. Then for any natural number $n$, the $n$-th iterate $g_a^{[n]}$ is semiconjugate to $g_b^{[n]}$ via $f$, i.e., $f \circ g_a^{[n]} = g_b^{[n]} \circ f$.

Function.Semiconj.iterate_left theorem

{g : ℕ → α → α} (H : ∀ n, Semiconj f (g n) (g <| n + 1)) (n k : ℕ) : Semiconj f^[n] (g k) (g <| n + k)

Full source

theorem iterate_left {g : ℕ → α → α} (H : ∀ n, Semiconj f (g n) (g <| n + 1)) (n k : ℕ) :
    Semiconj f^[n] (g k) (g <| n + k) := by
  induction n generalizing k with
  | zero =>
    rw [Nat.zero_add]
    exact id_left
  | succ n ihn =>
    rw [Nat.add_right_comm, Nat.add_assoc]
    exact (H k).trans (ihn (k + 1))

Iterated Semiconjugacy for a Family of Functions: $f^{[n]} \circ g(k) = g(n + k) \circ f^{[n]}$

Informal description

Let $g : \mathbb{N} \to \alpha \to \alpha$ be a family of functions such that for every natural number $n$, the function $f$ semiconjugates $g(n)$ to $g(n+1)$. Then for any natural numbers $n$ and $k$, the $n$-th iterate of $f$ semiconjugates $g(k)$ to $g(n + k)$. In other words, $f^{[n]} \circ g(k) = g(n + k) \circ f^{[n]}$.

Function.Commute.iterate_right theorem

(h : Commute f g) (n : ℕ) : Commute f g^[n]

Full source

theorem iterate_right (h : Commute f g) (n : ℕ) : Commute f g^[n] :=
  Semiconj.iterate_right h n

Commutation of a Function with Iterates of a Commuting Function

Informal description

If two functions $f, g : \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then for any natural number $n$, the function $f$ commutes with the $n$-th iterate $g^{[n]}$ of $g$.

Function.Commute.iterate_left theorem

(h : Commute f g) (n : ℕ) : Commute f^[n] g

Full source

theorem iterate_left (h : Commute f g) (n : ℕ) : Commute f^[n] g :=
  (h.symm.iterate_right n).symm

Commutation of Iterates with a Commuting Function: $f^{[n]} \circ g = g \circ f^{[n]}$

Informal description

If two functions $f, g : \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then for any natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ commutes with $g$.

Function.Commute.iterate_iterate theorem

(h : Commute f g) (m n : ℕ) : Commute f^[m] g^[n]

Full source

theorem iterate_iterate (h : Commute f g) (m n : ℕ) : Commute f^[m] g^[n] :=
  (h.iterate_left m).iterate_right n

Commutation of Iterates of Commuting Functions: $f^{[m]} \circ g^{[n]} = g^{[n]} \circ f^{[m]}$

Informal description

If two functions $f, g : \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then for any natural numbers $m$ and $n$, the $m$-th iterate $f^{[m]}$ of $f$ commutes with the $n$-th iterate $g^{[n]}$ of $g$, i.e., $f^{[m]} \circ g^{[n]} = g^{[n]} \circ f^{[m]}$.

Function.Commute.iterate_eq_of_map_eq theorem

(h : Commute f g) (n : ℕ) {x} (hx : f x = g x) : f^[n] x = g^[n] x

Full source

theorem iterate_eq_of_map_eq (h : Commute f g) (n : ℕ) {x} (hx : f x = g x) :
    f^[n] x = g^[n] x :=
  Nat.recOn n rfl fun n ihn ↦ by
    simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]

Iterated Commuting Functions with Common Fixed Point: $f^{[n]}(x) = g^{[n]}(x)$

Informal description

Let $f, g : \alpha \to \alpha$ be commuting functions (i.e., $f \circ g = g \circ f$). If for some $x \in \alpha$ we have $f(x) = g(x)$, then for any natural number $n$, the $n$-th iterates satisfy $f^{[n]}(x) = g^{[n]}(x)$.

Function.Commute.comp_iterate theorem

(h : Commute f g) (n : ℕ) : (f ∘ g)^[n] = f^[n] ∘ g^[n]

Full source

theorem comp_iterate (h : Commute f g) (n : ℕ) : (f ∘ g)^[n] = f^[n]f^[n] ∘ g^[n] := by
  induction n with
  | zero => rfl
  | succ n ihn =>
    funext x
    simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

Iterated Composition of Commuting Functions: $(f \circ g)^{[n]} = f^{[n]} \circ g^{[n]}$

Informal description

If two functions $f, g : \alpha \to \alpha$ commute (i.e., $f \circ g = g \circ f$), then for any natural number $n$, the $n$-th iterate of their composition $(f \circ g)^{[n]}$ is equal to the composition of their $n$-th iterates $f^{[n]} \circ g^{[n]}$.

Function.Commute.iterate_self theorem

(n : ℕ) : Commute f^[n] f

Full source

theorem iterate_self (n : ℕ) : Commute f^[n] f :=
  (refl f).iterate_left n

Self-commutation of iterates: $f^{[n]} \circ f = f \circ f^{[n]}$

Informal description

For any function $f : \alpha \to \alpha$ and any natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ commutes with $f$ itself, i.e., $f^{[n]} \circ f = f \circ f^{[n]}$.

Function.Commute.self_iterate theorem

(n : ℕ) : Commute f f^[n]

Full source

theorem self_iterate (n : ℕ) : Commute f f^[n] :=
  (refl f).iterate_right n

Self-Commutation of a Function with its Iterates

Informal description

For any function $f : \alpha \to \alpha$ and any natural number $n$, the function $f$ commutes with its $n$-th iterate $f^[n]$, i.e., $f \circ f^[n] = f^[n] \circ f$.

Function.Commute.iterate_iterate_self theorem

(m n : ℕ) : Commute f^[m] f^[n]

Full source

theorem iterate_iterate_self (m n : ℕ) : Commute f^[m] f^[n] :=
  (refl f).iterate_iterate m n

Commutation of Iterates: $f^{[m]} \circ f^{[n]} = f^{[n]} \circ f^{[m]}$

Informal description

For any function $f : \alpha \to \alpha$ and natural numbers $m, n$, the $m$-th iterate $f^{[m]}$ of $f$ commutes with the $n$-th iterate $f^{[n]}$ of $f$, i.e., $f^{[m]} \circ f^{[n]} = f^{[n]} \circ f^{[m]}$.

Function.Semiconj₂.iterate theorem

{f : α → α} {op : α → α → α} (hf : Semiconj₂ f op op) (n : ℕ) : Semiconj₂ f^[n] op op

Full source

theorem Semiconj₂.iterate {f : α → α} {op : α → α → α} (hf : Semiconj₂ f op op) (n : ℕ) :
    Semiconj₂ f^[n] op op :=
  Nat.recOn n (Semiconj₂.id_left op) fun _ ihn ↦ ihn.comp hf

Iterated Semiconjugacy of Binary Operations

Informal description

Let $f : \alpha \to \alpha$ be a function and $op : \alpha \to \alpha \to \alpha$ a binary operation such that $f$ semiconjugates $op$ to itself, i.e., $f(op(x, y)) = op(f(x), f(y))$ for all $x, y \in \alpha$. Then for any natural number $n$, the $n$-th iterate $f^[n]$ also semiconjugates $op$ to itself, i.e., $f^[n](op(x, y)) = op(f^[n](x), f^[n](y))$ for all $x, y \in \alpha$.

Function.iterate_succ' theorem

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

Full source

theorem iterate_succ' (n : ℕ) : f^[n.succ] = f ∘ f^[n] := by
  rw [iterate_succ, (Commute.self_iterate f n).comp_eq]

Iteration Composition: $f^{[n+1]} = f \circ f^{[n]}$

Informal description

For any function $f : \alpha \to \alpha$ and natural number $n$, the $(n+1)$-th iterate of $f$ is equal to the composition of $f$ with the $n$-th iterate of $f$, i.e., $f^{[n+1]} = f \circ f^{[n]}$.

Function.iterate_succ_apply' theorem

(n : ℕ) (x : α) : f^[n.succ] x = f (f^[n] x)

Full source

theorem iterate_succ_apply' (n : ℕ) (x : α) : f^[n.succ] x = f (f^[n] x) := by
  rw [iterate_succ']
  rfl

Iteration Recursion: $f^{[n+1]}(x) = f(f^{[n]}(x))$

Informal description

For any function $f : \alpha \to \alpha$, natural number $n$, and element $x \in \alpha$, the $(n+1)$-th iterate of $f$ applied to $x$ equals $f$ applied to the $n$-th iterate of $f$ applied to $x$, i.e., $f^{[n+1]}(x) = f(f^{[n]}(x))$.

Function.iterate_pred_comp_of_pos theorem

{n : ℕ} (hn : 0 < n) : f^[n.pred] ∘ f = f^[n]

Full source

theorem iterate_pred_comp_of_pos {n : ℕ} (hn : 0 < n) : f^[n.pred]f^[n.pred] ∘ f = f^[n] := by
  rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]

Iteration Composition for Positive Iterates: $f^{[n-1]} \circ f = f^{[n]}$

Informal description

For any function $f : \alpha \to \alpha$ and positive natural number $n$, the composition of the $(n-1)$-th iterate of $f$ with $f$ itself is equal to the $n$-th iterate of $f$, i.e., $f^{[n-1]} \circ f = f^{[n]}$.

Function.comp_iterate_pred_of_pos theorem

{n : ℕ} (hn : 0 < n) : f ∘ f^[n.pred] = f^[n]

Full source

theorem comp_iterate_pred_of_pos {n : ℕ} (hn : 0 < n) : f ∘ f^[n.pred] = f^[n] := by
  rw [← iterate_succ', Nat.succ_pred_eq_of_pos hn]

Composition of Function with Iterate: $f \circ f^{[n-1]} = f^{[n]}$ for $n > 0$

Informal description

For any function $f : \alpha \to \alpha$ and positive natural number $n$, the composition of $f$ with the $(n-1)$-th iterate of $f$ is equal to the $n$-th iterate of $f$, i.e., $f \circ f^{[n-1]} = f^{[n]}$.

Function.Iterate.rec definition

(p : α → Sort*) {f : α → α} (h : ∀ a, p a → p (f a)) {a : α} (ha : p a) (n : ℕ) : p (f^[n] a)

Full source

/-- A recursor for the iterate of a function. -/
def Iterate.rec (p : α → Sort*) {f : α → α} (h : ∀ a, p a → p (f a)) {a : α} (ha : p a) (n : ℕ) :
    p (f^[n] a) :=
  match n with
  | 0 => ha
  | m+1 => Iterate.rec p h (h _ ha) m

Recursion principle for iterated function application

Informal description

Given a predicate $p : \alpha \to \text{Sort}*$, a function $f : \alpha \to \alpha$, and a proof $h : \forall a, p(a) \to p(f(a))$, if $p(a)$ holds for some $a \in \alpha$, then $p(f^{[n]}(a))$ holds for any natural number $n$, where $f^{[n]}$ denotes the $n$-th iterate of $f$.

Function.Iterate.rec_zero theorem

(p : α → Sort*) {f : α → α} (h : ∀ a, p a → p (f a)) {a : α} (ha : p a) : Iterate.rec p h ha 0 = ha

Full source

theorem Iterate.rec_zero (p : α → Sort*) {f : α → α} (h : ∀ a, p a → p (f a)) {a : α} (ha : p a) :
    Iterate.rec p h ha 0 = ha :=
  rfl

Base Case of Recursion Principle for Iterated Function Application

Informal description

Given a predicate $p : \alpha \to \text{Sort}*$, a function $f : \alpha \to \alpha$, and a proof $h : \forall a, p(a) \to p(f(a))$, if $p(a)$ holds for some $a \in \alpha$, then the recursion principle for the zeroth iterate satisfies $\text{Iterate.rec}\, p\, h\, ha\, 0 = ha$.

Function.LeftInverse.iterate theorem

{g : α → α} (hg : LeftInverse g f) (n : ℕ) : LeftInverse g^[n] f^[n]

Full source

theorem LeftInverse.iterate {g : α → α} (hg : LeftInverse g f) (n : ℕ) :
    LeftInverse g^[n] f^[n] :=
  Nat.recOn n (fun _ ↦ rfl) fun n ihn ↦ by
    rw [iterate_succ', iterate_succ]
    exact ihn.comp hg

Iteration Preserves Left Inverses: $g^{[n]} \circ f^{[n]} = \text{id}$

Informal description

Let $f, g : \alpha \to \alpha$ be functions such that $g$ is a left inverse of $f$, i.e., $g \circ f = \text{id}$. Then for any natural number $n$, the $n$-th iterate $g^{[n]}$ is a left inverse of the $n$-th iterate $f^{[n]}$, i.e., $g^{[n]} \circ f^{[n]} = \text{id}$.

Function.RightInverse.iterate theorem

{g : α → α} (hg : RightInverse g f) (n : ℕ) : RightInverse g^[n] f^[n]

Full source

theorem RightInverse.iterate {g : α → α} (hg : RightInverse g f) (n : ℕ) :
    RightInverse g^[n] f^[n] :=
  LeftInverse.iterate hg n

Iteration Preserves Right Inverses: $f^{[n]} \circ g^{[n]} = \text{id}$

Informal description

Let $f, g \colon \alpha \to \alpha$ be functions such that $g$ is a right inverse of $f$, i.e., $f \circ g = \text{id}$. Then for any natural number $n$, the $n$-th iterate $g^{[n]}$ is a right inverse of the $n$-th iterate $f^{[n]}$, i.e., $f^{[n]} \circ g^{[n]} = \text{id}$.

Function.iterate_comm theorem

(f : α → α) (m n : ℕ) : f^[n]^[m] = f^[m]^[n]

Full source

theorem iterate_comm (f : α → α) (m n : ℕ) : f^[n]f^[n]^[m] = f^[m]f^[m]^[n] :=
  (iterate_mul _ _ _).symm.trans (Eq.trans (by rw [Nat.mul_comm]) (iterate_mul _ _ _))

Commutativity of Function Iteration: $(f^{[n]})^{[m]} = (f^{[m]})^{[n]}$

Informal description

For any function $f \colon \alpha \to \alpha$ and natural numbers $m, n$, the $m$-th iterate of the $n$-th iterate of $f$ is equal to the $n$-th iterate of the $m$-th iterate of $f$, i.e., $(f^{[n]})^{[m]} = (f^{[m]})^{[n]}$.

Function.iterate_commute theorem

(m n : ℕ) : Commute (fun f : α → α ↦ f^[m]) fun f ↦ f^[n]

Full source

theorem iterate_commute (m n : ℕ) : Commute (fun f : α → α ↦ f^[m]) fun f ↦ f^[n] :=
  fun f ↦ iterate_comm f m n

Commutativity of Iteration Operations: $(f^{[m]})^{[n]} = (f^{[n]})^{[m]}$

Informal description

For any natural numbers $m$ and $n$, the operations of taking the $m$-th iterate and the $n$-th iterate of a function $f \colon \alpha \to \alpha$ commute. That is, for any function $f$, we have $(f^{[m]})^{[n]} = (f^{[n]})^{[m]}$.

Function.iterate_add_eq_iterate theorem

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

Full source

lemma iterate_add_eq_iterate (hf : Injective f) : f^[m + n]f^[m + n] a = f^[n] a ↔ f^[m] a = a :=
  Iff.trans (by rw [← iterate_add_apply, Nat.add_comm]) (hf.iterate n).eq_iff

Fixed Point Criterion for Iterates of an Injective Function: $f^{[m+n]}(a) = f^{[n]}(a) \leftrightarrow f^{[m]}(a) = a$

Informal description

Let $f : \alpha \to \alpha$ be an injective function. For any natural numbers $m, n$ and any element $a \in \alpha$, the $(m+n)$-th iterate of $f$ applied to $a$ equals the $n$-th iterate of $f$ applied to $a$ if and only if the $m$-th iterate of $f$ applied to $a$ equals $a$ itself. In other words: $$ f^{[m+n]}(a) = f^{[n]}(a) \leftrightarrow f^{[m]}(a) = a. $$

Function.iterate_cancel theorem

(hf : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a = a

Full source

lemma iterate_cancel (hf : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a = a := by
  obtain h | h := Nat.le_total m n
  { simp [Nat.sub_eq_zero_of_le h] }
  { exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h]) }

Cancellation Property for Iterates of an Injective Function: $f^{[m]}(a) = f^{[n]}(a) \implies f^{[m - n]}(a) = a$

Informal description

Let $f : \alpha \to \alpha$ be an injective function. For any natural numbers $m, n$ and any element $a \in \alpha$, if the $m$-th iterate of $f$ applied to $a$ equals the $n$-th iterate of $f$ applied to $a$, then the $(m - n)$-th iterate of $f$ applied to $a$ equals $a$ itself. In other words: $$ f^{[m]}(a) = f^{[n]}(a) \implies f^{[m - n]}(a) = a. $$

Function.involutive_iff_iter_2_eq_id theorem

{α} {f : α → α} : Involutive f ↔ f^[2] = id

Full source

theorem involutive_iff_iter_2_eq_id {α} {f : α → α} : InvolutiveInvolutive f ↔ f^[2] = id :=
  funext_iff.symm

Involutive Function Characterization via Second Iterate

Informal description

A function $f : \alpha \to \alpha$ is involutive (i.e., satisfies $f(f(x)) = x$ for all $x \in \alpha$) if and only if its second iterate equals the identity function, i.e., $f^[2] = \text{id}$.

List.foldl_const theorem

(f : α → α) (a : α) (l : List β) : l.foldl (fun b _ ↦ f b) a = f^[l.length] a

Full source

theorem foldl_const (f : α → α) (a : α) (l : List β) :
    l.foldl (fun b _ ↦ f b) a = f^[l.length] a := by
  induction l generalizing a with
  | nil => rfl
  | cons b l H => rw [length_cons, foldl, iterate_succ_apply, H]

Left Fold with Constant Function Equals Iteration

Informal description

For any function $f : \alpha \to \alpha$, any element $a \in \alpha$, and any list $l$ of elements of type $\beta$, the left fold of $l$ with the constant function $\lambda b \_, f(b)$ and initial value $a$ is equal to the $n$-th iterate of $f$ applied to $a$, where $n$ is the length of $l$. In other words, \[ \text{foldl} \, (\lambda b \_, f(b)) \, a \, l = f^{[|l|]}(a). \]

List.foldr_const theorem

(f : β → β) (b : β) : ∀ l : List α, l.foldr (fun _ ↦ f) b = f^[l.length] b

Full source

theorem foldr_const (f : β → β) (b : β) : ∀ l : List α, l.foldr (fun _ ↦ f) b = f^[l.length] b
  | [] => rfl
  | a :: l => by rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']

Right Fold with Constant Function Equals Iteration

Informal description

For any function $f : \beta \to \beta$, any element $b \in \beta$, and any list $l$ of elements of type $\alpha$, the right fold of $l$ with the constant function $\lambda \_, f$ and initial value $b$ is equal to the $n$-th iterate of $f$ applied to $b$, where $n$ is the length of $l$. In other words, \[ \text{foldr} \, (\lambda \_, f) \, b \, l = f^{[|l|]}(b). \]