English
For any f and x, the minimalPeriod f x equals 0 if x is not periodic, otherwise it is the least positive n with f^n(x)=x.
Русский
Для любых f и x minimalPeriod f x равно 0, если x не периодично; иначе — наименьшее положительное n такое, что f^n(x)=x.
LaTeX
$$$$ \\operatorname{minimalPeriod}(f,x) = \\begin{cases} 0, & x \\notin \\operatorname{periodicPts}(f), \\\\ \\min\\{ n \\ge 1 : f^n(x) = x \\} , & x \\in \\operatorname{periodicPts}(f). \\end{cases} $$$$
Lean4
/-- Minimal period of a point `x` under an endomorphism `f`. If `x` is not a periodic point of `f`,
then `minimalPeriod f x = 0`. -/
def minimalPeriod (f : α → α) (x : α) :=
if h : x ∈ periodicPts f then Nat.find h else 0
