# 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 : x is a periodic point of f of period n, i.e. f^[n] x = x. We do not require n > 0 in the definition.
• ptsOfPeriod f n : the set {x | IsPeriodicPt f n x}. Note that n is not required to be the minimal period of x.
• periodicPts f : the set of all periodic points of f.
• minimalPeriod f x : the minimal period of a point x under an endomorphism f or zero if x is not a periodic point of f.
• orbit f x: the cycle [x, f x, f (f x), ...] for a periodic point.
• MulAction.period g x : the minimal period of a point x under the multiplicative action of g; an equivalent AddAction.period g x is defined for additive actions.

## 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 #

def Function.IsPeriodicPt {α : Type u_1} (f : αα) (n : ) (x : α) :

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
Instances For
theorem Function.IsFixedPt.isPeriodicPt {α : Type u_1} {f : αα} {x : α} (hf : ) (n : ) :

A fixed point of f is a periodic point of f of any prescribed period.

theorem Function.is_periodic_id {α : Type u_1} (n : ) (x : α) :

For the identity map, all points are periodic.

theorem Function.isPeriodicPt_zero {α : Type u_1} (f : αα) (x : α) :

Any point is a periodic point of period 0.

instance Function.IsPeriodicPt.instDecidableOfDecidableEq {α : Type u_1} [] {f : αα} {n : } {x : α} :
Equations
• Function.IsPeriodicPt.instDecidableOfDecidableEq = Function.IsFixedPt.decidable
theorem Function.IsPeriodicPt.isFixedPt {α : Type u_1} {f : αα} {x : α} {n : } (hf : ) :
theorem Function.IsPeriodicPt.map {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {x : α} {n : } (hx : ) {g : αβ} (hg : Function.Semiconj g fa fb) :
theorem Function.IsPeriodicPt.apply_iterate {α : Type u_1} {f : αα} {x : α} {n : } (hx : ) (m : ) :
theorem Function.IsPeriodicPt.apply {α : Type u_1} {f : αα} {x : α} {n : } (hx : ) :
theorem Function.IsPeriodicPt.add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : ) (hm : ) :
theorem Function.IsPeriodicPt.left_of_add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f (n + m) x) (hm : ) :
theorem Function.IsPeriodicPt.right_of_add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f (n + m) x) (hm : ) :
theorem Function.IsPeriodicPt.sub {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : ) (hn : ) :
theorem Function.IsPeriodicPt.mul_const {α : Type u_1} {f : αα} {x : α} {m : } (hm : ) (n : ) :
theorem Function.IsPeriodicPt.const_mul {α : Type u_1} {f : αα} {x : α} {m : } (hm : ) (n : ) :
theorem Function.IsPeriodicPt.trans_dvd {α : Type u_1} {f : αα} {x : α} {m : } (hm : ) {n : } (hn : m n) :
theorem Function.IsPeriodicPt.iterate {α : Type u_1} {f : αα} {x : α} {n : } (hf : ) (m : ) :
theorem Function.IsPeriodicPt.comp {α : Type u_1} {f : αα} {x : α} {n : } {g : αα} (hco : ) (hf : ) (hg : ) :
theorem Function.IsPeriodicPt.comp_lcm {α : Type u_1} {f : αα} {x : α} {m : } {n : } {g : αα} (hco : ) (hf : ) (hg : ) :
Function.IsPeriodicPt (f g) (m.lcm n) x
theorem Function.IsPeriodicPt.left_of_comp {α : Type u_1} {f : αα} {x : α} {n : } {g : αα} (hco : ) (hfg : Function.IsPeriodicPt (f g) n x) (hg : ) :
theorem Function.IsPeriodicPt.iterate_mod_apply {α : Type u_1} {f : αα} {x : α} {n : } (h : ) (m : ) :
f^[m % n] x = f^[m] x
theorem Function.IsPeriodicPt.mod {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : ) (hn : ) :
theorem Function.IsPeriodicPt.gcd {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : ) (hn : ) :
Function.IsPeriodicPt f (m.gcd n) x
theorem Function.IsPeriodicPt.eq_of_apply_eq_same {α : Type u_1} {f : αα} {x : α} {y : α} {n : } (hx : ) (hy : ) (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 : ) (hy : ) (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.

def Function.ptsOfPeriod {α : Type u_1} (f : αα) (n : ) :
Set α

The set of periodic points of a given (possibly non-minimal) period.

Equations
• = {x : α | }
Instances For
@[simp]
theorem Function.mem_ptsOfPeriod {α : Type u_1} {f : αα} {x : α} {n : } :
theorem Function.Semiconj.mapsTo_ptsOfPeriod {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {g : αβ} (h : Function.Semiconj g fa fb) (n : ) :
Set.MapsTo g () ()
theorem Function.bijOn_ptsOfPeriod {α : Type u_1} (f : αα) {n : } (hn : 0 < n) :
Set.BijOn f () ()
theorem Function.directed_ptsOfPeriod_pNat {α : Type u_1} (f : αα) :
Directed (fun (x x_1 : Set α) => x x_1) fun (n : ℕ+) =>
def Function.periodicPts {α : Type u_1} (f : αα) :
Set α

The set of periodic points of a map f : α → α.

Equations
• = {x : α | n > 0, }
Instances For
theorem Function.mk_mem_periodicPts {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : ) :
theorem Function.mem_periodicPts {α : Type u_1} {f : αα} {x : α} :
n > 0,
theorem Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hx : ) (hm : Function.IsPeriodicPt f m (f^[n] x)) :
theorem Function.bUnion_ptsOfPeriod {α : Type u_1} (f : αα) :
⋃ (n : ), ⋃ (_ : n > 0), =
theorem Function.iUnion_pNat_ptsOfPeriod {α : Type u_1} (f : αα) :
⋃ (n : ℕ+), =
theorem Function.bijOn_periodicPts {α : Type u_1} (f : αα) :
theorem Function.Semiconj.mapsTo_periodicPts {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {g : αβ} (h : Function.Semiconj g fa fb) :
def Function.minimalPeriod {α : Type u_1} (f : αα) (x : α) :

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
• = if h : then else 0
Instances For
theorem Function.isPeriodicPt_minimalPeriod {α : Type u_1} (f : αα) (x : α) :
@[simp]
theorem Function.iterate_minimalPeriod {α : Type u_1} {f : αα} {x : α} :
= x
@[simp]
theorem Function.iterate_add_minimalPeriod_eq {α : Type u_1} {f : αα} {x : α} {n : } :
f^[] x = f^[n] x
@[simp]
theorem Function.iterate_mod_minimalPeriod_eq {α : Type u_1} {f : αα} {x : α} {n : } :
f^[] x = f^[n] x
theorem Function.minimalPeriod_pos_of_mem_periodicPts {α : Type u_1} {f : αα} {x : α} (hx : ) :
theorem Function.minimalPeriod_eq_zero_of_nmem_periodicPts {α : Type u_1} {f : αα} {x : α} (hx : ) :
theorem Function.IsPeriodicPt.minimalPeriod_pos {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : ) :
theorem Function.minimalPeriod_pos_iff_mem_periodicPts {α : Type u_1} {f : αα} {x : α} :
theorem Function.minimalPeriod_eq_zero_iff_nmem_periodicPts {α : Type u_1} {f : αα} {x : α} :
theorem Function.IsPeriodicPt.minimalPeriod_le {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : ) :
theorem Function.minimalPeriod_apply_iterate {α : Type u_1} {f : αα} {x : α} (hx : ) (n : ) :
theorem Function.minimalPeriod_apply {α : Type u_1} {f : αα} {x : α} (hx : ) :
theorem Function.le_of_lt_minimalPeriod_of_iterate_eq {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : ) (hmn : f^[m] x = f^[n] x) :
m n
theorem Function.iterate_injOn_Iio_minimalPeriod {α : Type u_1} {f : αα} {x : α} :
Set.InjOn (fun (x_1 : ) => f^[x_1] x) ()
theorem Function.iterate_eq_iterate_iff_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : ) (hn : ) :
f^[m] x = f^[n] x m = n
@[simp]
theorem Function.minimalPeriod_id {α : Type u_1} {x : α} :
= 1
theorem Function.minimalPeriod_eq_one_iff_isFixedPt {α : Type u_1} {f : αα} {x : α} :
theorem Function.IsPeriodicPt.eq_zero_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {n : } (hx : ) (hn : ) :
n = 0
theorem Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {n : } :
n 0¬
theorem Function.IsPeriodicPt.minimalPeriod_dvd {α : Type u_1} {f : αα} {x : α} {n : } (hx : ) :
theorem Function.isPeriodicPt_iff_minimalPeriod_dvd {α : Type u_1} {f : αα} {x : α} {n : } :
theorem Function.minimalPeriod_eq_minimalPeriod_iff {α : Type u_1} {β : Type u_2} {f : αα} {x : α} {g : ββ} {y : β} :
∀ (n : ),
theorem Function.minimalPeriod_eq_prime {α : Type u_1} {f : αα} {x : α} {p : } [hp : Fact ()] (hper : ) (hfix : ) :
theorem Function.minimalPeriod_eq_prime_pow {α : Type u_1} {f : αα} {x : α} {p : } {k : } [hp : Fact ()] (hk : ¬Function.IsPeriodicPt f (p ^ k) x) (hk1 : Function.IsPeriodicPt f (p ^ (k + 1)) x) :
= p ^ (k + 1)
theorem Function.Commute.minimalPeriod_of_comp_dvd_lcm {α : Type u_1} {f : αα} {x : α} {g : αα} (h : ) :
Function.minimalPeriod (f g) x ().lcm ()
theorem Function.Commute.minimalPeriod_of_comp_dvd_mul {α : Type u_1} {f : αα} {x : α} {g : αα} (h : ) :
theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime {α : Type u_1} {f : αα} {x : α} {g : αα} (h : ) (hco : ().Coprime ()) :
theorem Function.minimalPeriod_iterate_eq_div_gcd {α : Type u_1} {f : αα} {x : α} {n : } (h : n 0) :
= / ().gcd n
theorem Function.minimalPeriod_iterate_eq_div_gcd' {α : Type u_1} {f : αα} {x : α} {n : } (h : ) :
= / ().gcd n
def Function.periodicOrbit {α : Type u_1} (f : αα) (x : α) :

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
Instances For
theorem Function.periodicOrbit_def {α : Type u_1} (f : αα) (x : α) :
= (List.map (fun (n : ) => f^[n] x) ())

The definition of a periodic orbit, in terms of List.map.

theorem Function.periodicOrbit_eq_cycle_map {α : Type u_1} (f : αα) (x : α) :
= Cycle.map (fun (n : ) => f^[n] x) ()

The definition of a periodic orbit, in terms of Cycle.map.

@[simp]
theorem Function.periodicOrbit_length {α : Type u_1} {f : αα} {x : α} :
().length =
@[simp]
theorem Function.periodicOrbit_eq_nil_iff_not_periodic_pt {α : Type u_1} {f : αα} {x : α} :
= Cycle.nil
theorem Function.periodicOrbit_eq_nil_of_not_periodic_pt {α : Type u_1} {f : αα} {x : α} (h : ) :
= Cycle.nil
@[simp]
theorem Function.mem_periodicOrbit_iff {α : Type u_1} {f : αα} {x : α} {y : α} (hx : ) :
∃ (n : ), f^[n] x = y
@[simp]
theorem Function.iterate_mem_periodicOrbit {α : Type u_1} {f : αα} {x : α} (hx : ) (n : ) :
f^[n] x
@[simp]
theorem Function.self_mem_periodicOrbit {α : Type u_1} {f : αα} {x : α} (hx : ) :
theorem Function.nodup_periodicOrbit {α : Type u_1} {f : αα} {x : α} :
().Nodup
theorem Function.periodicOrbit_apply_iterate_eq {α : Type u_1} {f : αα} {x : α} (hx : ) (n : ) :
theorem Function.periodicOrbit_apply_eq {α : Type u_1} {f : αα} {x : α} (hx : ) :
theorem Function.periodicOrbit_chain {α : Type u_1} (r : ααProp) {f : αα} {x : α} :
n < , r (f^[n] x) (f^[n + 1] x)
theorem Function.periodicOrbit_chain' {α : Type u_1} (r : ααProp) {f : αα} {x : α} (hx : ) :
∀ (n : ), r (f^[n] x) (f^[n + 1] x)
@[simp]
theorem Function.iterate_prod_map {α : Type u_1} {β : Type u_2} (f : αα) (g : ββ) (n : ) :
@[simp]
theorem Function.isFixedPt_prod_map {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} (x : α × β) :
@[simp]
theorem Function.isPeriodicPt_prod_map {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} {n : } (x : α × β) :
theorem Function.minimalPeriod_prod_map {α : Type u_1} {β : Type u_2} (f : αα) (g : ββ) (x : α × β) :
= ().lcm ()
theorem Function.minimalPeriod_fst_dvd {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} {x : α × β} :
theorem Function.minimalPeriod_snd_dvd {α : Type u_1} {β : Type u_2} {f : αα} {g : ββ} {x : α × β} :
noncomputable def AddAction.period {α : Type v} {M : Type u} [] [] (m : M) (a : α) :

The period of an additive action of g on a is the smallest positive n such that (n • g) +ᵥ a = a, or 0 if such an n does not exist.

Equations
Instances For
noncomputable def MulAction.period {α : Type v} {M : Type u} [] [] (m : M) (a : α) :

The period of a multiplicative action of g on a is the smallest positive n such that g ^ n • a = a, or 0 if such an n does not exist.

Equations
Instances For
theorem AddAction.period_eq_minimalPeriod {α : Type v} {M : Type u} [] [] {m : M} {a : α} :
= Function.minimalPeriod (fun (x : α) => m +ᵥ x) a

AddAction.period m a is definitionally equal to Function.minimalPeriod (m +ᵥ ·) a

theorem MulAction.period_eq_minimalPeriod {α : Type v} {M : Type u} [] [] {m : M} {a : α} :
= Function.minimalPeriod (fun (x : α) => m x) a

MulAction.period m a is definitionally equal to Function.minimalPeriod (m • ·) a.

@[simp]
theorem AddAction.nsmul_period_vadd {α : Type v} {M : Type u} [] [] (m : M) (a : α) :
m +ᵥ a = a

(period m a) • m fixes a.

@[simp]
theorem MulAction.pow_period_smul {α : Type v} {M : Type u} [] [] (m : M) (a : α) :
m ^ a = a

m ^ (period m a) fixes a.

theorem AddAction.isPeriodicPt_vadd_iff {α : Type v} {M : Type u} [] [] {m : M} {a : α} {n : } :
Function.IsPeriodicPt (fun (x : α) => m +ᵥ x) n a n m +ᵥ a = a
theorem MulAction.isPeriodicPt_smul_iff {α : Type v} {M : Type u} [] [] {m : M} {a : α} {n : } :
Function.IsPeriodicPt (fun (x : α) => m x) n a m ^ n a = a

### Multiples of MulAction.period#

It is easy to convince oneself that if g ^ n • a = a (resp. (n • g) +ᵥ a = a), then n must be a multiple of period g a.

This also holds for negative powers/multiples.

theorem AddAction.nsmul_vadd_eq_iff_period_dvd {α : Type v} {M : Type u} [] [] {n : } {m : M} {a : α} :
n m +ᵥ a = a n
theorem MulAction.pow_smul_eq_iff_period_dvd {α : Type v} {M : Type u} [] [] {n : } {m : M} {a : α} :
m ^ n a = a n
theorem AddAction.zsmul_vadd_eq_iff_period_dvd {α : Type v} {G : Type u} [] [] {j : } {g : G} {a : α} :
j g +ᵥ a = a () j
theorem MulAction.zpow_smul_eq_iff_period_dvd {α : Type v} {G : Type u} [] [] {j : } {g : G} {a : α} :
g ^ j a = a () j
@[simp]
theorem AddAction.nsmul_mod_period_vadd {α : Type v} {M : Type u} [] [] (n : ) {m : M} {a : α} :
(n % ) m +ᵥ a = n m +ᵥ a
@[simp]
theorem MulAction.pow_mod_period_smul {α : Type v} {M : Type u} [] [] (n : ) {m : M} {a : α} :
m ^ (n % ) a = m ^ n a
@[simp]
theorem AddAction.zsmul_mod_period_vadd {α : Type v} {G : Type u} [] [] (j : ) {g : G} {a : α} :
(j % ()) g +ᵥ a = j g +ᵥ a
@[simp]
theorem MulAction.zpow_mod_period_smul {α : Type v} {G : Type u} [] [] (j : ) {g : G} {a : α} :
g ^ (j % ()) a = g ^ j a
@[simp]
theorem AddAction.nsmul_add_period_vadd {α : Type v} {M : Type u} [] [] (n : ) (m : M) (a : α) :
(n + ) m +ᵥ a = n m +ᵥ a
@[simp]
theorem MulAction.pow_add_period_smul {α : Type v} {M : Type u} [] [] (n : ) (m : M) (a : α) :
m ^ (n + ) a = m ^ n a
@[simp]
theorem AddAction.nsmul_period_add_vadd {α : Type v} {M : Type u} [] [] (n : ) (m : M) (a : α) :
( + n) m +ᵥ a = n m +ᵥ a
@[simp]
theorem MulAction.pow_period_add_smul {α : Type v} {M : Type u} [] [] (n : ) (m : M) (a : α) :
m ^ ( + n) a = m ^ n a
@[simp]
theorem AddAction.zsmul_add_period_vadd {α : Type v} {G : Type u} [] [] (i : ) (g : G) (a : α) :
(i + ()) g +ᵥ a = i g +ᵥ a
@[simp]
theorem MulAction.zpow_add_period_smul {α : Type v} {G : Type u} [] [] (i : ) (g : G) (a : α) :
g ^ (i + ()) a = g ^ i a
@[simp]
theorem AddAction.zsmul_period_add_vadd {α : Type v} {G : Type u} [] [] (i : ) (g : G) (a : α) :
(() + i) g +ᵥ a = i g +ᵥ a
@[simp]
theorem MulAction.zpow_period_add_smul {α : Type v} {G : Type u} [] [] (i : ) (g : G) (a : α) :
g ^ (() + i) a = g ^ i a
theorem AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [] [] {a : G} {b : α} {n : } :
n a +ᵥ b = b Function.minimalPeriod (fun (x : α) => a +ᵥ x) b n
theorem MulAction.pow_smul_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [] [] {a : G} {b : α} {n : } :
a ^ n b = b Function.minimalPeriod (fun (x : α) => a x) b n
theorem AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [] [] {a : G} {b : α} {n : } :
n a +ᵥ b = b (Function.minimalPeriod (fun (x : α) => a +ᵥ x) b) n
theorem MulAction.zpow_smul_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [] [] {a : G} {b : α} {n : } :
a ^ n b = b (Function.minimalPeriod (fun (x : α) => a x) b) n
@[simp]
theorem AddAction.nsmul_vadd_mod_minimalPeriod {α : Type v} {G : Type u} [] [] (a : G) (b : α) (n : ) :
(n % Function.minimalPeriod (fun (x : α) => a +ᵥ x) b) a +ᵥ b = n a +ᵥ b
@[simp]
theorem MulAction.pow_smul_mod_minimalPeriod {α : Type v} {G : Type u} [] [] (a : G) (b : α) (n : ) :
a ^ (n % Function.minimalPeriod (fun (x : α) => a x) b) b = a ^ n b
@[simp]
theorem AddAction.zsmul_vadd_mod_minimalPeriod {α : Type v} {G : Type u} [] [] (a : G) (b : α) (n : ) :
(n % (Function.minimalPeriod (fun (x : α) => a +ᵥ x) b)) a +ᵥ b = n a +ᵥ b
@[simp]
theorem MulAction.zpow_smul_mod_minimalPeriod {α : Type v} {G : Type u} [] [] (a : G) (b : α) (n : ) :
a ^ (n % (Function.minimalPeriod (fun (x : α) => a x) b)) b = a ^ n b