# Documentation

Mathlib.Order.Iterate

# Inequalities on iterates #

In this file we prove some inequalities comparing f^[n] x and g^[n] x where f and g are two self-maps that commute with each other.

Current selection of inequalities is motivated by formalization of the rotation number of a circle homeomorphism.

### Comparison of two sequences #

If $f$ is a monotone function, then $∀ k, x_{k+1} ≤ f(x_k)$ implies that $x_k$ grows slower than $f^k(x_0)$, and similarly for the reversed inequalities. If $x_k$ and $y_k$ are two sequences such that $x_{k+1} ≤ f(x_k)$ and $y_{k+1} ≥ f(y_k)$ for all $k < n$, then $x_0 ≤ y_0$ implies $x_n ≤ y_n$, see Monotone.seq_le_seq.

If some of the inequalities in this lemma are strict, then we have $x_n < y_n$. The rest of the lemmas in this section formalize this fact for different inequalities made strict.

theorem Monotone.seq_le_seq {α : Type u_1} [inst : ] {f : αα} {x : α} {y : α} (hf : ) (n : ) (h₀ : x 0 y 0) (hx : ∀ (k : ), k < nx (k + 1) f (x k)) (hy : ∀ (k : ), k < nf (y k) y (k + 1)) :
x n y n
theorem Monotone.seq_pos_lt_seq_of_lt_of_le {α : Type u_1} [inst : ] {f : αα} {x : α} {y : α} (hf : ) {n : } (hn : 0 < n) (h₀ : x 0 y 0) (hx : ∀ (k : ), k < nx (k + 1) < f (x k)) (hy : ∀ (k : ), k < nf (y k) y (k + 1)) :
x n < y n
theorem Monotone.seq_pos_lt_seq_of_le_of_lt {α : Type u_1} [inst : ] {f : αα} {x : α} {y : α} (hf : ) {n : } (hn : 0 < n) (h₀ : x 0 y 0) (hx : ∀ (k : ), k < nx (k + 1) f (x k)) (hy : ∀ (k : ), k < nf (y k) < y (k + 1)) :
x n < y n
theorem Monotone.seq_lt_seq_of_lt_of_le {α : Type u_1} [inst : ] {f : αα} {x : α} {y : α} (hf : ) (n : ) (h₀ : x 0 < y 0) (hx : ∀ (k : ), k < nx (k + 1) < f (x k)) (hy : ∀ (k : ), k < nf (y k) y (k + 1)) :
x n < y n
theorem Monotone.seq_lt_seq_of_le_of_lt {α : Type u_1} [inst : ] {f : αα} {x : α} {y : α} (hf : ) (n : ) (h₀ : x 0 < y 0) (hx : ∀ (k : ), k < nx (k + 1) f (x k)) (hy : ∀ (k : ), k < nf (y k) < y (k + 1)) :
x n < y n

### Iterates of two functions #

In this section we compare the iterates of a monotone function f : α → α→ α to iterates of any function g : β → β→ β. If h : β → α→ α satisfies h ∘ g ≤ f ∘ h∘ g ≤ f ∘ h≤ f ∘ h∘ h, then h (g^[n] x) grows slower than f^[n] (h x), and similarly for the reversed inequality.

Then we specialize these two lemmas to the case β = α, h = id.

theorem Monotone.le_iterate_comp_of_le {α : Type u_1} {β : Type u_2} [inst : ] {f : αα} {g : ββ} {h : βα} (hf : ) (H : h g f h) (n : ) :
h g^[n] f^[n] h
theorem Monotone.iterate_comp_le_of_le {α : Type u_1} {β : Type u_2} [inst : ] {f : αα} {g : ββ} {h : βα} (hf : ) (H : f h h g) (n : ) :
f^[n] h h g^[n]
theorem Monotone.iterate_le_of_le {α : Type u_1} [inst : ] {f : αα} {g : αα} (hf : ) (h : f g) (n : ) :
f^[n] g^[n]

If f ≤ g≤ g and f is monotone, then f^[n] ≤ g^[n]≤ g^[n].

theorem Monotone.le_iterate_of_le {α : Type u_1} [inst : ] {f : αα} {g : αα} (hg : ) (h : f g) (n : ) :
f^[n] g^[n]

If f ≤ g≤ g and g is monotone, then f^[n] ≤ g^[n]≤ g^[n].

### Comparison of iterations and the identity function #

If $f(x) ≤ x$ for all $x$ (we express this as f ≤ id≤ id in the code), then the same is true for any iterate of $f$, and similarly for the reversed inequality.

theorem Function.id_le_iterate_of_id_le {α : Type u_1} [inst : ] {f : αα} (h : id f) (n : ) :
id f^[n]

If $x ≤ f x$ for all $x$ (we write this as id ≤ f≤ f), then the same is true for any iterate f^[n] of f.

theorem Function.iterate_le_id_of_le_id {α : Type u_1} [inst : ] {f : αα} (h : f id) (n : ) :
f^[n] id
theorem Function.monotone_iterate_of_id_le {α : Type u_1} [inst : ] {f : αα} (h : id f) :
Monotone fun m => f^[m]
theorem Function.antitone_iterate_of_le_id {α : Type u_1} [inst : ] {f : αα} (h : f id) :
Antitone fun m => f^[m]

### Iterates of commuting functions #

If f and g are monotone and commute, then f x ≤ g x≤ g x implies f^[n] x ≤ g^[n] x≤ g^[n] x, see Function.Commute.iterate_le_of_map_le. We also prove two strict inequality versions of this lemma, as well as iff versions.

theorem Function.Commute.iterate_le_of_map_le {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} (hx : f x g x) (n : ) :
(f^[n]) x (g^[n]) x
theorem Function.Commute.iterate_pos_lt_of_map_lt {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} (hx : f x < g x) {n : } (hn : 0 < n) :
(f^[n]) x < (g^[n]) x
theorem Function.Commute.iterate_pos_lt_of_map_lt' {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} (hx : f x < g x) {n : } (hn : 0 < n) :
(f^[n]) x < (g^[n]) x
theorem Function.Commute.iterate_pos_lt_iff_map_lt {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} {n : } (hn : 0 < n) :
(f^[n]) x < (g^[n]) x f x < g x
theorem Function.Commute.iterate_pos_lt_iff_map_lt' {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} {n : } (hn : 0 < n) :
(f^[n]) x < (g^[n]) x f x < g x
theorem Function.Commute.iterate_pos_le_iff_map_le {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} {n : } (hn : 0 < n) :
(f^[n]) x (g^[n]) x f x g x
theorem Function.Commute.iterate_pos_le_iff_map_le' {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} {n : } (hn : 0 < n) :
(f^[n]) x (g^[n]) x f x g x
theorem Function.Commute.iterate_pos_eq_iff_map_eq {α : Type u_1} [inst : ] {f : αα} {g : αα} (h : ) (hf : ) (hg : ) {x : α} {n : } (hn : 0 < n) :
(f^[n]) x = (g^[n]) x f x = g x
theorem Monotone.monotone_iterate_of_le_map {α : Type u_1} [inst : ] {f : αα} {x : α} (hf : ) (hx : x f x) :
Monotone fun n => (f^[n]) x

If f is a monotone map and x ≤ f x≤ f x at some point x, then the iterates f^[n] x form a monotone sequence.

theorem Monotone.antitone_iterate_of_map_le {α : Type u_1} [inst : ] {f : αα} {x : α} (hf : ) (hx : f x x) :
Antitone fun n => (f^[n]) x

If f is a monotone map and f x ≤ x≤ x at some point x, then the iterates f^[n] x form a antitone sequence.

theorem StrictMono.strictMono_iterate_of_lt_map {α : Type u_1} [inst : ] {f : αα} {x : α} (hf : ) (hx : x < f x) :
StrictMono fun n => (f^[n]) x

If f is a strictly monotone map and x < f x at some point x, then the iterates f^[n] x form a strictly monotone sequence.

theorem StrictMono.strictAnti_iterate_of_map_lt {α : Type u_1} [inst : ] {f : αα} {x : α} (hf : ) (hx : f x < x) :
StrictAnti fun n => (f^[n]) x

If f is a strictly antitone map and f x < x at some point x, then the iterates f^[n] x form a strictly antitone sequence.