# Documentation

Mathlib.Dynamics.PeriodicPts

# Periodic points #

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

## Main definitions #

• IsPeriodicPt 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.
• ptsOfPeriod f n : the set {x | IsPeriodicPt f n x}. Note that n is not required to be the minimal period of x.
• periodicPts f : the set of all periodic points of f.
• minimalPeriod f x : the minimal period of a point x under an endomorphism f or zero if x is not a periodic point of f.
• orbit f x: the cycle [x, f x, f (f x), ...] for a periodic point.

## Main statements #

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

• https://en.wikipedia.org/wiki/Periodic_point