English
The chain of the periodic orbit with respect to a relation r is equivalent to checking r between consecutive iterates f^n x and f^{n+1} x for all n less than the minimal period.
Русский
Связь орбиты по отношению r эквивалентна проверке r между соседними элементами последовательности f^n x и f^{n+1} x для всех n < минимального периода.
LaTeX
$$$(\\operatorname{periodicOrbit}(f,x)).\\text{Chain}(r) \\iff \\forall n<\\operatorname{minimalPeriod}(f,x),\\ r\\left(f^{n}x, f^{n+1}x\\right)$$$
Lean4
theorem periodicOrbit_chain (r : α → α → Prop) {f : α → α} {x : α} :
(periodicOrbit f x).Chain r ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x) :=
by
by_cases hx : x ∈ periodicPts f
· have hx' := minimalPeriod_pos_of_mem_periodicPts hx
have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
refine ⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
· rintro ⟨hr, H⟩ n hn
rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
· rwa [hM', hM, iterate_minimalPeriod]
· exact H _ hM'
· rw [iterate_zero_apply]
nth_rw 3 [← @iterate_minimalPeriod α f x]
nth_rw 2 [← hM]
exact H _ (Nat.lt_succ_self _)
· rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_notMem_periodicPts hx]
simp
