English
For any hx ∈ periodicPts f and any n, minimalPeriod f (f^[n] x) = minimalPeriod f x.
Русский
Для любого х из периодических точек f и любого n: минимальный период от f^n(x) равен минимальному периоду от x.
LaTeX
$$$$ \\text{If } x \\in \\operatorname{periodicPts}(f), \\ \\operatorname{minimalPeriod}(f, f^{[n]}(x)) = \\operatorname{minimalPeriod}(f,x). $$$$
Lean4
theorem minimalPeriod_apply_iterate (hx : x ∈ periodicPts f) (n : ℕ) : minimalPeriod f (f^[n] x) = minimalPeriod f x :=
by
apply
(IsPeriodicPt.minimalPeriod_le (minimalPeriod_pos_of_mem_periodicPts hx) _).antisymm
((isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate hx (isPeriodicPt_minimalPeriod f _)).minimalPeriod_le
(minimalPeriod_pos_of_mem_periodicPts _))
· exact (isPeriodicPt_minimalPeriod f x).apply_iterate n
· rcases hx with ⟨m, hm, hx⟩
exact ⟨m, hm, hx.apply_iterate n⟩
