# mathlibdocumentation

dynamics.periodic_pts

# Periodic points

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

## Main definitions

• is_periodic_pt f n x : x is a periodic point of f of period n, i.e. f^[n] x = x. We do not require n > 0 in the definition.
• pts_of_period f n : the set {x | is_periodic_pt f n x}. Note that n is not required to be the minimal period of x.
• periodic_pts f : the set of all periodic points of f.
• minimal_period f x : the minimal period of a point x under an endomorphism f or zero if x is not a periodic point of f.

## 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

• https://en.wikipedia.org/wiki/Periodic_point
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 : 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.

@[instance]
def function.is_periodic_pt.decidable {α : Type u_1} [decidable_eq α] {f : α → α} {n : } {x : α} :

Equations
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 : x) {g : α → β} :
fb (g x)

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

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

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

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

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

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

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

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

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

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

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

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

theorem function.is_periodic_pt.eq_of_apply_eq_same {α : Type u_1} {f : α → α} {x y : α} {n : } :
0 < 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 : } :
0 < 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
• = {x : α | x}
@[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 : fb) (n : ) :
n) n)

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

theorem function.directed_pts_of_period_pnat {α : Type u_1} (f : α → α) :
(λ (n : ℕ+),

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

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

Equations
• = {x : α | ∃ (n : ) (H : n > 0), x}
theorem function.mk_mem_periodic_pts {α : Type u_1} {f : α → α} {x : α} {n : } :
0 < n

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

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

theorem function.Union_pnat_pts_of_period {α : Type u_1} (f : α → α) :
(⋃ (n : ℕ+), =

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 : α → β} :
fb

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 : } :
0 < 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 : } :
0 < n

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

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