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} [Preorder α] {f : αα} {x : α} {y : α} (hf : Monotone f) (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} [Preorder α] {f : αα} {x : α} {y : α} (hf : Monotone f) {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} [Preorder α] {f : αα} {x : α} {y : α} (hf : Monotone f) {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} [Preorder α] {f : αα} {x : α} {y : α} (hf : Monotone f) (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} [Preorder α] {f : αα} {x : α} {y : α} (hf : Monotone f) (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, 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} [Preorder α] {f : αα} {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} {β : Type u_2} [Preorder α] {f : αα} {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.