order.iterate

# Inequalities on iterates #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} {β : 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 : ) :
theorem function.monotone_iterate_of_id_le {α : Type u_1} [preorder α] {f : α α} (h : id f) :
monotone (λ (m : ), f^[m])
theorem function.antitone_iterate_of_le_id {α : Type u_1} [preorder α] {f : α α} (h : f id) :
antitone (λ (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 : 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 : g) (hf : monotone f) (hg : strict_mono 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 : g) (hf : strict_mono 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} [linear_order α] {f g : α α} (h : g) (hf : monotone f) (hg : strict_mono 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} [linear_order α] {f g : α α} (h : g) (hf : strict_mono 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} [linear_order α] {f g : α α} (h : g) (hf : monotone f) (hg : strict_mono 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} [linear_order α] {f g : α α} (h : g) (hf : strict_mono 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} [linear_order α] {f g : α α} (h : g) (hf : monotone f) (hg : strict_mono 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 (λ (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 (λ (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 a antitone sequence.

theorem strict_mono.strict_mono_iterate_of_lt_map {α : Type u_1} [preorder α] {f : α α} {x : α} (hf : strict_mono f) (hx : x < f x) :
strict_mono (λ (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 strict_mono.strict_anti_iterate_of_map_lt {α : Type u_1} [preorder α] {f : α α} {x : α} (hf : strict_mono f) (hx : f x < x) :
strict_anti (λ (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.