mathlib3 documentation

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 : ℕ) :

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 : 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 : 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 : function.commute f 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 : function.commute f 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 : function.commute f 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 : function.commute f 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 : function.commute f 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 : function.commute f 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.