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 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 : } :
0 < nf^[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 : } :
0 < nf^[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 : } :
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 : } :
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 : } :
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 : } :
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 : } :
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].