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