mathlib documentation

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.

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
theorem function.id_le_iterate_of_id_le {α : Type u_1} [preorder α] {f : α → α} (h : id f) (n : ) :
id (f^[n])
theorem function.iterate_le_id_of_le_id {α : Type u_1} [preorder α] {f : α → α} (h : f id) (n : ) :
theorem function.iterate_le_iterate_of_id_le {α : Type u_1} [preorder α] {f : α → α} (h : id f) {m n : } (hmn : m n) :
f^[m] (f^[n])
theorem function.iterate_le_iterate_of_le_id {α : Type u_1} [preorder α] {f : α → α} (h : f id) {m n : } (hmn : m n) :
f^[n] (f^[m])
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.le_iterate_comp_of_le {α : Type u_1} {β : Type u_2} [preorder β] {f : α → α} {g : β → β} {h : α → β} (hg : monotone g) (H : ∀ (x : α), h (f x) g (h x)) (n : ) (x : α) :
h (f^[n] x) g^[n] (h x)
theorem monotone.iterate_comp_le_of_le {α : Type u_1} {β : Type u_2} [preorder β] {f : α → α} {g : β → β} {h : α → β} (hg : monotone g) (H : ∀ (x : α), g (h x) h (f x)) (n : ) (x : α) :
g^[n] (h x) h (f^[n] x)
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.iterate_ge_of_ge {α : Type u_1} [preorder α] {f g : α → α} (hg : monotone g) (h : f g) (n : ) :
f^[n] (g^[n])

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