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:xis a periodic point offof periodn, i.e.f^[n] x = x. We do not requiren > 0in the definition.ptsOfPeriod f n: the set{x | IsPeriodicPt f n x}. Note thatnis not required to be the minimal period ofx.periodicPts f: the set of all periodic points off.minimalPeriod f x: the minimal period of a pointxunder an endomorphismfor zero ifxis not a periodic point off.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.
References #
- https://en.wikipedia.org/wiki/Periodic_point
A point x is a periodic point of f : α → α→ α of period n if f^[n] x = x.
Note that we do not require 0 < n in this definition. Many theorems about periodic points
need this assumption.
Equations
- Function.IsPeriodicPt f n x = Function.IsFixedPt (f^[n]) x
theorem
Function.IsFixedPt.isPeriodicPt
{α : Type u_1}
{f : α → α}
{x : α}
(hf : Function.IsFixedPt f x)
(n : ℕ)
:
Function.IsPeriodicPt f n x
A fixed point of f is a periodic point of f of any prescribed period.
For the identity map, all points are periodic.
Any point is a periodic point of period 0.
instance
Function.IsPeriodicPt.instDecidableIsPeriodicPt
{α : Type u_1}
[inst : DecidableEq α]
{f : α → α}
{n : ℕ}
{x : α}
:
Decidable (Function.IsPeriodicPt f n x)
Equations
- Function.IsPeriodicPt.instDecidableIsPeriodicPt = Function.IsFixedPt.decidable
theorem
Function.IsPeriodicPt.isFixedPt
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hf : Function.IsPeriodicPt f n x)
:
Function.IsFixedPt (f^[n]) x
theorem
Function.IsPeriodicPt.map
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{x : α}
{n : ℕ}
(hx : Function.IsPeriodicPt fa n x)
{g : α → β}
(hg : Function.Semiconj g fa fb)
:
Function.IsPeriodicPt fb n (g x)
theorem
Function.IsPeriodicPt.apply_iterate
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hx : Function.IsPeriodicPt f n x)
(m : ℕ)
:
Function.IsPeriodicPt f n ((f^[m]) x)
theorem
Function.IsPeriodicPt.apply
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hx : Function.IsPeriodicPt f n x)
:
Function.IsPeriodicPt f n (f x)
theorem
Function.IsPeriodicPt.add
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
(hn : Function.IsPeriodicPt f n x)
(hm : Function.IsPeriodicPt f m x)
:
Function.IsPeriodicPt f (n + m) x
theorem
Function.IsPeriodicPt.left_of_add
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
(hn : Function.IsPeriodicPt f (n + m) x)
(hm : Function.IsPeriodicPt f m x)
:
Function.IsPeriodicPt f n x
theorem
Function.IsPeriodicPt.right_of_add
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
(hn : Function.IsPeriodicPt f (n + m) x)
(hm : Function.IsPeriodicPt f n x)
:
Function.IsPeriodicPt f m x
theorem
Function.IsPeriodicPt.sub
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
(hm : Function.IsPeriodicPt f m x)
(hn : Function.IsPeriodicPt f n x)
:
Function.IsPeriodicPt f (m - n) x
theorem
Function.IsPeriodicPt.mul_const
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
(hm : Function.IsPeriodicPt f m x)
(n : ℕ)
:
Function.IsPeriodicPt f (m * n) x
theorem
Function.IsPeriodicPt.const_mul
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
(hm : Function.IsPeriodicPt f m x)
(n : ℕ)
:
Function.IsPeriodicPt f (n * m) x
theorem
Function.IsPeriodicPt.trans_dvd
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
(hm : Function.IsPeriodicPt f m x)
{n : ℕ}
(hn : m ∣ n)
:
Function.IsPeriodicPt f n x
theorem
Function.IsPeriodicPt.iterate
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hf : Function.IsPeriodicPt f n x)
(m : ℕ)
:
Function.IsPeriodicPt (f^[m]) n x
theorem
Function.IsPeriodicPt.comp
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
{g : α → α}
(hco : Function.Commute f g)
(hf : Function.IsPeriodicPt f n x)
(hg : Function.IsPeriodicPt g n x)
:
Function.IsPeriodicPt (f ∘ g) n x
theorem
Function.IsPeriodicPt.comp_lcm
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
{g : α → α}
(hco : Function.Commute f g)
(hf : Function.IsPeriodicPt f m x)
(hg : Function.IsPeriodicPt g n x)
:
Function.IsPeriodicPt (f ∘ g) (Nat.lcm m n) x
theorem
Function.IsPeriodicPt.left_of_comp
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
{g : α → α}
(hco : Function.Commute f g)
(hfg : Function.IsPeriodicPt (f ∘ g) n x)
(hg : Function.IsPeriodicPt g n x)
:
Function.IsPeriodicPt f n x
theorem
Function.IsPeriodicPt.mod
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
(hm : Function.IsPeriodicPt f m x)
(hn : Function.IsPeriodicPt f n x)
:
Function.IsPeriodicPt f (m % n) x
theorem
Function.IsPeriodicPt.gcd
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
(hm : Function.IsPeriodicPt f m x)
(hn : Function.IsPeriodicPt f n x)
:
Function.IsPeriodicPt f (Nat.gcd m n) x
theorem
Function.IsPeriodicPt.eq_of_apply_eq_same
{α : Type u_1}
{f : α → α}
{x : α}
{y : α}
{n : ℕ}
(hx : Function.IsPeriodicPt f n x)
(hy : Function.IsPeriodicPt f n y)
(hn : 0 < n)
(h : f x = f y)
:
x = y
If f sends two periodic points x and y of the same positive period to the same point,
then x = y. For a similar statement about points of different periods see eq_of_apply_eq.
theorem
Function.IsPeriodicPt.eq_of_apply_eq
{α : Type u_1}
{f : α → α}
{x : α}
{y : α}
{m : ℕ}
{n : ℕ}
(hx : Function.IsPeriodicPt f m x)
(hy : Function.IsPeriodicPt f n y)
(hm : 0 < m)
(hn : 0 < n)
(h : f x = f y)
:
x = y
If f sends two periodic points x and y of positive periods to the same point,
then x = y.
The set of periodic points of a given (possibly non-minimal) period.
Equations
- Function.ptsOfPeriod f n = { x | Function.IsPeriodicPt f n x }
@[simp]
theorem
Function.mem_ptsOfPeriod
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
:
x ∈ Function.ptsOfPeriod f n ↔ Function.IsPeriodicPt f n x
theorem
Function.Semiconj.mapsTo_ptsOfPeriod
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{g : α → β}
(h : Function.Semiconj g fa fb)
(n : ℕ)
:
Set.MapsTo g (Function.ptsOfPeriod fa n) (Function.ptsOfPeriod fb n)
theorem
Function.bijOn_ptsOfPeriod
{α : Type u_1}
(f : α → α)
{n : ℕ}
(hn : 0 < n)
:
Set.BijOn f (Function.ptsOfPeriod f n) (Function.ptsOfPeriod f n)
theorem
Function.directed_ptsOfPeriod_pNat
{α : Type u_1}
(f : α → α)
:
Directed (fun x x_1 => x ⊆ x_1) fun n => Function.ptsOfPeriod f ↑n
The set of periodic points of a map f : α → α→ α.
Equations
- Function.periodicPts f = { x | ∃ n, n > 0 ∧ Function.IsPeriodicPt f n x }
theorem
Function.mk_mem_periodicPts
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hn : 0 < n)
(hx : Function.IsPeriodicPt f n x)
:
theorem
Function.mem_periodicPts
{α : Type u_1}
{f : α → α}
{x : α}
:
x ∈ Function.periodicPts f ↔ ∃ n, n > 0 ∧ Function.IsPeriodicPt f n x
theorem
Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
{n : ℕ}
(hx : x ∈ Function.periodicPts f)
(hm : Function.IsPeriodicPt f m ((f^[n]) x))
:
Function.IsPeriodicPt f m x
theorem
Function.bUnion_ptsOfPeriod
{α : Type u_1}
(f : α → α)
:
(Set.unionᵢ fun n => Set.unionᵢ fun h => Function.ptsOfPeriod f n) = Function.periodicPts f
theorem
Function.unionᵢ_pNat_ptsOfPeriod
{α : Type u_1}
(f : α → α)
:
(Set.unionᵢ fun n => Function.ptsOfPeriod f ↑n) = Function.periodicPts f
theorem
Function.Semiconj.mapsTo_periodicPts
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{g : α → β}
(h : Function.Semiconj g fa fb)
:
Set.MapsTo g (Function.periodicPts fa) (Function.periodicPts fb)
Minimal period of a point x under an endomorphism f. If x is not a periodic point of f,
then minimalPeriod f x = 0.
Equations
- Function.minimalPeriod f x = if h : x ∈ Function.periodicPts f then Nat.find h else 0
theorem
Function.isPeriodicPt_minimalPeriod
{α : Type u_1}
(f : α → α)
(x : α)
:
Function.IsPeriodicPt f (Function.minimalPeriod f x) x
@[simp]
theorem
Function.iterate_minimalPeriod
{α : Type u_1}
{f : α → α}
{x : α}
:
(f^[Function.minimalPeriod f x]) x = x
theorem
Function.minimalPeriod_pos_of_mem_periodicPts
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
:
0 < Function.minimalPeriod f x
theorem
Function.minimalPeriod_eq_zero_of_nmem_periodicPts
{α : Type u_1}
{f : α → α}
{x : α}
(hx : ¬x ∈ Function.periodicPts f)
:
Function.minimalPeriod f x = 0
theorem
Function.IsPeriodicPt.minimalPeriod_pos
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hn : 0 < n)
(hx : Function.IsPeriodicPt f n x)
:
0 < Function.minimalPeriod f x
theorem
Function.minimalPeriod_pos_iff_mem_periodicPts
{α : Type u_1}
{f : α → α}
{x : α}
:
0 < Function.minimalPeriod f x ↔ x ∈ Function.periodicPts f
theorem
Function.minimalPeriod_eq_zero_iff_nmem_periodicPts
{α : Type u_1}
{f : α → α}
{x : α}
:
Function.minimalPeriod f x = 0 ↔ ¬x ∈ Function.periodicPts f
theorem
Function.IsPeriodicPt.minimalPeriod_le
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hn : 0 < n)
(hx : Function.IsPeriodicPt f n x)
:
Function.minimalPeriod f x ≤ n
theorem
Function.minimalPeriod_apply_iterate
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
(n : ℕ)
:
Function.minimalPeriod f ((f^[n]) x) = Function.minimalPeriod f x
theorem
Function.minimalPeriod_apply
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
:
Function.minimalPeriod f (f x) = Function.minimalPeriod f x
theorem
Function.is_fixed_point_iff_minimalPeriod_eq_one
{α : Type u_1}
{f : α → α}
{x : α}
:
Function.minimalPeriod f x = 1 ↔ Function.IsFixedPt f x
theorem
Function.IsPeriodicPt.eq_zero_of_lt_minimalPeriod
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hx : Function.IsPeriodicPt f n x)
(hn : n < Function.minimalPeriod f x)
:
n = 0
theorem
Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
:
n ≠ 0 → n < Function.minimalPeriod f x → ¬Function.IsPeriodicPt f n x
theorem
Function.IsPeriodicPt.minimalPeriod_dvd
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hx : Function.IsPeriodicPt f n x)
:
Function.minimalPeriod f x ∣ n
theorem
Function.isPeriodicPt_iff_minimalPeriod_dvd
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
:
Function.IsPeriodicPt f n x ↔ Function.minimalPeriod f x ∣ n
theorem
Function.minimalPeriod_eq_minimalPeriod_iff
{α : Type u_1}
{β : Type u_2}
{f : α → α}
{x : α}
{g : β → β}
{y : β}
:
Function.minimalPeriod f x = Function.minimalPeriod g y ↔ ∀ (n : ℕ), Function.IsPeriodicPt f n x ↔ Function.IsPeriodicPt g n y
theorem
Function.minimalPeriod_eq_prime
{α : Type u_1}
{f : α → α}
{x : α}
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(hper : Function.IsPeriodicPt f p x)
(hfix : ¬Function.IsFixedPt f x)
:
Function.minimalPeriod f x = p
theorem
Function.minimalPeriod_eq_prime_pow
{α : Type u_1}
{f : α → α}
{x : α}
{p : ℕ}
{k : ℕ}
[hp : Fact (Nat.Prime p)]
(hk : ¬Function.IsPeriodicPt f (p ^ k) x)
(hk1 : Function.IsPeriodicPt f (p ^ (k + 1)) x)
:
Function.minimalPeriod f x = p ^ (k + 1)
theorem
Function.Commute.minimalPeriod_of_comp_dvd_lcm
{α : Type u_1}
{f : α → α}
{x : α}
{g : α → α}
(h : Function.Commute f g)
:
Function.minimalPeriod (f ∘ g) x ∣ Nat.lcm (Function.minimalPeriod f x) (Function.minimalPeriod g x)
theorem
Function.Commute.minimalPeriod_of_comp_dvd_mul
{α : Type u_1}
{f : α → α}
{x : α}
{g : α → α}
(h : Function.Commute f g)
:
Function.minimalPeriod (f ∘ g) x ∣ Function.minimalPeriod f x * Function.minimalPeriod g x
theorem
Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime
{α : Type u_1}
{f : α → α}
{x : α}
{g : α → α}
(h : Function.Commute f g)
(hco : Nat.coprime (Function.minimalPeriod f x) (Function.minimalPeriod g x))
:
Function.minimalPeriod (f ∘ g) x = Function.minimalPeriod f x * Function.minimalPeriod g x
theorem
Function.minimalPeriod_iterate_eq_div_gcd
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(h : n ≠ 0)
:
Function.minimalPeriod (f^[n]) x = Function.minimalPeriod f x / Nat.gcd (Function.minimalPeriod f x) n
theorem
Function.minimalPeriod_iterate_eq_div_gcd'
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(h : x ∈ Function.periodicPts f)
:
Function.minimalPeriod (f^[n]) x = Function.minimalPeriod f x / Nat.gcd (Function.minimalPeriod f x) n
The orbit of a periodic point x of f is the cycle [x, f x, f (f x), ...]. Its length is
the minimal period of x.
If x is not a periodic point, then this is the empty (aka nil) cycle.
Equations
- Function.periodicOrbit f x = ↑(List.map (fun n => (f^[n]) x) (List.range (Function.minimalPeriod f x)))
theorem
Function.periodicOrbit_def
{α : Type u_1}
(f : α → α)
(x : α)
:
Function.periodicOrbit f x = ↑(List.map (fun n => (f^[n]) x) (List.range (Function.minimalPeriod f x)))
The definition of a periodic orbit, in terms of List.map.
theorem
Function.periodicOrbit_eq_cycle_map
{α : Type u_1}
(f : α → α)
(x : α)
:
Function.periodicOrbit f x = Cycle.map (fun n => (f^[n]) x) ↑(List.range (Function.minimalPeriod f x))
The definition of a periodic orbit, in terms of Cycle.map.
@[simp]
@[simp]
theorem
Function.periodicOrbit_eq_nil_iff_not_periodic_pt
{α : Type u_1}
{f : α → α}
{x : α}
:
Function.periodicOrbit f x = Cycle.nil ↔ ¬x ∈ Function.periodicPts f
theorem
Function.periodicOrbit_eq_nil_of_not_periodic_pt
{α : Type u_1}
{f : α → α}
{x : α}
(h : ¬x ∈ Function.periodicPts f)
:
Function.periodicOrbit f x = Cycle.nil
@[simp]
theorem
Function.mem_periodicOrbit_iff
{α : Type u_1}
{f : α → α}
{x : α}
{y : α}
(hx : x ∈ Function.periodicPts f)
:
@[simp]
theorem
Function.iterate_mem_periodicOrbit
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
(n : ℕ)
:
(f^[n]) x ∈ Function.periodicOrbit f x
@[simp]
theorem
Function.self_mem_periodicOrbit
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
:
x ∈ Function.periodicOrbit f x
theorem
Function.periodicOrbit_apply_iterate_eq
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
(n : ℕ)
:
Function.periodicOrbit f ((f^[n]) x) = Function.periodicOrbit f x
theorem
Function.periodicOrbit_apply_eq
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
:
Function.periodicOrbit f (f x) = Function.periodicOrbit f x
theorem
Function.periodicOrbit_chain
{α : Type u_1}
(r : α → α → Prop)
{f : α → α}
{x : α}
:
Cycle.Chain r (Function.periodicOrbit f x) ↔ (n : ℕ) → n < Function.minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
theorem
Function.periodicOrbit_chain'
{α : Type u_1}
(r : α → α → Prop)
{f : α → α}
{x : α}
(hx : x ∈ Function.periodicPts f)
: