mathlib documentation

dynamics.periodic_pts

Periodic points

A point x : α is a periodic point of f : α → α of period n if f^[n] x = x.

Main definitions

Main statements

We provide “dot syntax”-style operations on terms of the form h : is_periodic_pt f n x including arithmetic operations on n and h.map (hg : semiconj_by g f f'). We also prove that f is bijective on each set pts_of_period f n and on periodic_pts f. Finally, we prove that x is a periodic point of f of period n if and only if minimal_period f x | n.

References

def function.is_periodic_pt {α : Type u_1} :
(α → α)α → Prop

A point x is a periodic point of f : α → α of period n if f^[n] x = x. Note that we do not require 0 < n in this definition. Many theorems about periodic points need this assumption.

Equations
theorem function.is_fixed_pt.is_periodic_pt {α : Type u_1} {f : α → α} {x : α} (hf : function.is_fixed_pt f x) (n : ) :

A fixed point of f is a periodic point of f of any prescribed period.

theorem function.is_periodic_id {α : Type u_1} (n : ) (x : α) :

For the identity map, all points are periodic.

theorem function.is_periodic_pt_zero {α : Type u_1} (f : α → α) (x : α) :

Any point is a periodic point of period 0.

theorem function.is_periodic_pt.is_fixed_pt {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.is_periodic_pt.map {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {x : α} {n : } (hx : function.is_periodic_pt fa n x) {g : α → β} :

theorem function.is_periodic_pt.apply_iterate {α : Type u_1} {f : α → α} {x : α} {n : } (hx : function.is_periodic_pt f n x) (m : ) :

theorem function.is_periodic_pt.apply {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.is_periodic_pt.add {α : Type u_1} {f : α → α} {x : α} {m n : } :

theorem function.is_periodic_pt.left_of_add {α : Type u_1} {f : α → α} {x : α} {m n : } :

theorem function.is_periodic_pt.right_of_add {α : Type u_1} {f : α → α} {x : α} {m n : } :

theorem function.is_periodic_pt.sub {α : Type u_1} {f : α → α} {x : α} {m n : } :

theorem function.is_periodic_pt.mul_const {α : Type u_1} {f : α → α} {x : α} {m : } (hm : function.is_periodic_pt f m x) (n : ) :

theorem function.is_periodic_pt.const_mul {α : Type u_1} {f : α → α} {x : α} {m : } (hm : function.is_periodic_pt f m x) (n : ) :

theorem function.is_periodic_pt.trans_dvd {α : Type u_1} {f : α → α} {x : α} {m : } (hm : function.is_periodic_pt f m x) {n : } :

theorem function.is_periodic_pt.iterate {α : Type u_1} {f : α → α} {x : α} {n : } (hf : function.is_periodic_pt f n x) (m : ) :

theorem function.is_periodic_pt.mod {α : Type u_1} {f : α → α} {x : α} {m n : } :

theorem function.is_periodic_pt.gcd {α : Type u_1} {f : α → α} {x : α} {m n : } :

theorem function.is_periodic_pt.eq_of_apply_eq_same {α : Type u_1} {f : α → α} {x y : α} {n : } :
function.is_periodic_pt f n xfunction.is_periodic_pt f n y0 < nf x = f yx = y

If f sends two periodic points x and y of the same positive period to the same point, then x = y. For a similar statement about points of different periods see eq_of_apply_eq.

theorem function.is_periodic_pt.eq_of_apply_eq {α : Type u_1} {f : α → α} {x y : α} {m n : } :
function.is_periodic_pt f m xfunction.is_periodic_pt f n y0 < m0 < nf x = f yx = y

If f sends two periodic points x and y of positive periods to the same point, then x = y.

def function.pts_of_period {α : Type u_1} :
(α → α)set α

The set of periodic points of a given (possibly non-minimal) period.

Equations
@[simp]
theorem function.mem_pts_of_period {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.semiconj.maps_to_pts_of_period {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β} (h : function.semiconj g fa fb) (n : ) :

theorem function.bij_on_pts_of_period {α : Type u_1} (f : α → α) {n : } :

theorem function.directed_pts_of_period_pnat {α : Type u_1} (f : α → α) :

def function.periodic_pts {α : Type u_1} :
(α → α)set α

The set of periodic points of a map f : α → α.

Equations
theorem function.mk_mem_periodic_pts {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.mem_periodic_pts {α : Type u_1} {f : α → α} {x : α} :
x function.periodic_pts f ∃ (n : ) (H : n > 0), function.is_periodic_pt f n x

theorem function.bUnion_pts_of_period {α : Type u_1} (f : α → α) :
(⋃ (n : ) (H : n > 0), function.pts_of_period f n) = function.periodic_pts f

theorem function.Union_pnat_pts_of_period {α : Type u_1} (f : α → α) :

theorem function.bij_on_periodic_pts {α : Type u_1} (f : α → α) :

theorem function.semiconj.maps_to_periodic_pts {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β} :

def function.minimal_period {α : Type u_1} :
(α → α)α →

Minimal period of a point x under an endomorphism f. If x is not a periodic point of f, then minimal_period f x = 0.

Equations
theorem function.is_periodic_pt_minimal_period {α : Type u_1} (f : α → α) (x : α) :

theorem function.minimal_period_pos_of_mem_periodic_pts {α : Type u_1} {f : α → α} {x : α} :

theorem function.is_periodic_pt.minimal_period_pos {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.minimal_period_pos_iff_mem_periodic_pts {α : Type u_1} {f : α → α} {x : α} :

theorem function.is_periodic_pt.minimal_period_le {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.is_periodic_pt.eq_zero_of_lt_minimal_period {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.is_periodic_pt.minimal_period_dvd {α : Type u_1} {f : α → α} {x : α} {n : } :

theorem function.is_periodic_pt_iff_minimal_period_dvd {α : Type u_1} {f : α → α} {x : α} {n : } :