---
tag: FHFWE27514
kind: definition
name: Minimal period
msc: [37C25, 37B02]
defines: VFZRVZ9SD8
uses: [T75CZ5H47N, AYVTR2ES5B]
sources:
  - url: https://en.wikipedia.org/wiki/Periodic_point
---

## Definition

Let $X$ be a set, let $f \colon X \to X$ be a map, and let $x \in X$ be a [[periodic point|T75CZ5H47N]] of $f$.
The *minimal period*, or *prime period*, of $x$ is the least integer $n \ge 1$ such that $f^n(x) = x$, where $f^n$ is the $n$-th [[iterate|AYVTR2ES5B]] of $f$.

## Remarks

Let $p$ be the minimal period of $x$.
Then $f^m(x) = x$ holds exactly when $p$ divides $m$: write $m = qp + r$ with $0 \le r < p$; then $x = f^m(x) = f^r(x)$, so $r = 0$ by minimality.
The points $x, f(x), \dots, f^{p-1}(x)$ are distinct, so the orbit of $x$ has exactly $p$ points.
A point has minimal period $1$ exactly when it is a fixed point.

Example: for $f(x) = -x$ on $\R$ and $x = 1$, one has $f(1) = -1 \ne 1$ and $f^2(1) = 1$, so the minimal period is $2$.

Non-example: for the same map, $2$ is not the minimal period of $0$.
It is a period, since $f^2(0) = 0$, but already $f(0) = 0$, so the minimal period of $0$ is $1$.

In Lean's Mathlib, `Function.minimalPeriod f x` is defined for all $x$ and takes the value $0$ when $x$ is not periodic.