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} [Preorder α] {f : α → α} {x y : ℕ → α} (hf : Monotone f) (n : ℕ) (h₀ : x 0 ≤ y 0) (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) : x n ≤ y n

theorem Monotone.seq_pos_lt_seq_of_lt_of_le {α : Type u_1} [Preorder α] {f : α → α} {x y : ℕ → α} (hf : Monotone f) {n : ℕ} (hn : 0 < n) (h₀ : x 0 ≤ y 0) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) : x n < y n

theorem Monotone.seq_pos_lt_seq_of_le_of_lt {α : Type u_1} [Preorder α] {f : α → α} {x y : ℕ → α} (hf : Monotone f) {n : ℕ} (hn : 0 < n) (h₀ : x 0 ≤ y 0) (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) < y (k + 1)) : x n < y n

theorem Monotone.seq_lt_seq_of_lt_of_le {α : Type u_1} [Preorder α] {f : α → α} {x y : ℕ → α} (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) : x n < y n

theorem Monotone.seq_lt_seq_of_le_of_lt {α : Type u_1} [Preorder α] {f : α → α} {x y : ℕ → α} (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0) (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (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, 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} [Preorder α] {f : α → α} {β : Type u_2} {g : β → β} {h : β → α} (hf : Monotone f) (H : h ∘ g ≤ f ∘ h) (n : ℕ) : h ∘ g^[n] ≤ f^[n] ∘ h

theorem Monotone.iterate_comp_le_of_le {α : Type u_1} [Preorder α] {f : α → α} {β : Type u_2} {g : β → β} {h : β → α} (hf : Monotone f) (H : f ∘ h ≤ h ∘ g) (n : ℕ) : f^[n] ∘ h ≤ h ∘ g^[n]

theorem Monotone.iterate_le_of_le {α : Type u_1} [Preorder α] {f g : α → α} (hf : Monotone f) (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n]

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

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

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

Comparison of iterations and the identity function

If $f(x) ≤ x$ for all $x$ (we express this as f ≤ 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} [Preorder α] {f : α → α} (h : id ≤ f) (n : ℕ) : id ≤ f^[n]

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

theorem Function.iterate_le_id_of_le_id {α : Type u_1} [Preorder α] {f : α → α} (h : f ≤ id) (n : ℕ) : f^[n] ≤ id

theorem Function.monotone_iterate_of_id_le {α : Type u_1} [Preorder α] {f : α → α} (h : id ≤ f) : Monotone fun (m : ℕ) => f^[m]

theorem Function.antitone_iterate_of_le_id {α : Type u_1} [Preorder α] {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 implies f^[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} [Preorder α] {f g : α → α} (h : Function.Commute f g) (hf : Monotone f) (hg : Monotone g) {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} [Preorder α] {f g : α → α} (h : Function.Commute f g) (hf : Monotone f) (hg : StrictMono g) {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} [Preorder α] {f g : α → α} (h : Function.Commute f g) (hf : StrictMono f) (hg : Monotone g) {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} [LinearOrder α] {f g : α → α} (h : Function.Commute f g) (hf : Monotone f) (hg : StrictMono g) {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} [LinearOrder α] {f g : α → α} (h : Function.Commute f g) (hf : StrictMono f) (hg : Monotone g) {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} [LinearOrder α] {f g : α → α} (h : Function.Commute f g) (hf : Monotone f) (hg : StrictMono g) {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} [LinearOrder α] {f g : α → α} (h : Function.Commute f g) (hf : StrictMono f) (hg : Monotone g) {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} [LinearOrder α] {f g : α → α} (h : Function.Commute f g) (hf : Monotone f) (hg : StrictMono g) {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} [Preorder α] {f : α → α} {x : α} (hf : Monotone f) (hx : x ≤ f x) : Monotone fun (n : ℕ) => f^[n] x

If f is a monotone map and 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} [Preorder α] {f : α → α} {x : α} (hf : Monotone f) (hx : f x ≤ x) : Antitone fun (n : ℕ) => f^[n] x

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

theorem StrictMono.strictMono_iterate_of_lt_map {α : Type u_1} [Preorder α] {f : α → α} {x : α} (hf : StrictMono f) (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} [Preorder α] {f : α → α} {x : α} (hf : StrictMono f) (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.