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.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].