# mathlib3documentation

dynamics.periodic_pts

# Periodic points #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A point x : α is a periodic point of f : α → α of period n if f^[n] x = x.

## Main definitions #

• is_periodic_pt 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.
• pts_of_period f n : the set {x | is_periodic_pt f n x}. Note that n is not required to be the minimal period of x.
• periodic_pts f : the set of all periodic points of f.
• minimal_period 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.

## Main statements #

We provide “dot syntax”-style operations on terms of the form h : is_periodic_pt f n x including arithmetic operations on n and h.map (hg : semiconj_by g f f'). We also prove that f is bijective on each set pts_of_period f n and on periodic_pts f. Finally, we prove that x is a periodic point of f of period n if and only if minimal_period f x | n.

## References #

def function.is_periodic_pt {α : Type u_1} (f : α α) (n : ) (x : α) :
Prop

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 function.is_periodic_pt
theorem function.is_fixed_pt.is_periodic_pt {α : Type u_1} {f : α α} {x : α} (hf : x) (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.is_periodic_pt_zero {α : Type u_1} (f : α α) (x : α) :

Any point is a periodic point of period 0.

@[protected, instance]
def function.is_periodic_pt.decidable {α : Type u_1} [decidable_eq α] {f : α α} {n : } {x : α} :
Equations
@[protected]
theorem function.is_periodic_pt.is_fixed_pt {α : Type u_1} {f : α α} {x : α} {n : } (hf : x) :
@[protected]
theorem function.is_periodic_pt.map {α : Type u_1} {β : Type u_2} {fa : α α} {fb : β β} {x : α} {n : } (hx : x) {g : α β} (hg : fb) :
(g x)
theorem function.is_periodic_pt.apply_iterate {α : Type u_1} {f : α α} {x : α} {n : } (hx : x) (m : ) :
(f^[m] x)
@[protected]
theorem function.is_periodic_pt.apply {α : Type u_1} {f : α α} {x : α} {n : } (hx : x) :
(f x)
@[protected]
theorem function.is_periodic_pt.add {α : Type u_1} {f : α α} {x : α} {m n : } (hn : x) (hm : x) :
(n + m) x
theorem function.is_periodic_pt.left_of_add {α : Type u_1} {f : α α} {x : α} {m n : } (hn : (n + m) x) (hm : x) :
theorem function.is_periodic_pt.right_of_add {α : Type u_1} {f : α α} {x : α} {m n : } (hn : (n + m) x) (hm : x) :
@[protected]
theorem function.is_periodic_pt.sub {α : Type u_1} {f : α α} {x : α} {m n : } (hm : x) (hn : x) :
(m - n) x
@[protected]
theorem function.is_periodic_pt.mul_const {α : Type u_1} {f : α α} {x : α} {m : } (hm : x) (n : ) :
(m * n) x
@[protected]
theorem function.is_periodic_pt.const_mul {α : Type u_1} {f : α α} {x : α} {m : } (hm : x) (n : ) :
(n * m) x
theorem function.is_periodic_pt.trans_dvd {α : Type u_1} {f : α α} {x : α} {m : } (hm : x) {n : } (hn : m n) :
@[protected]
theorem function.is_periodic_pt.iterate {α : Type u_1} {f : α α} {x : α} {n : } (hf : x) (m : ) :
theorem function.is_periodic_pt.comp {α : Type u_1} {f : α α} {x : α} {n : } {g : α α} (hco : g) (hf : x) (hg : x) :
theorem function.is_periodic_pt.comp_lcm {α : Type u_1} {f : α α} {x : α} {m n : } {g : α α} (hco : g) (hf : x) (hg : x) :
theorem function.is_periodic_pt.left_of_comp {α : Type u_1} {f : α α} {x : α} {n : } {g : α α} (hco : g) (hfg : function.is_periodic_pt (f g) n x) (hg : x) :
theorem function.is_periodic_pt.iterate_mod_apply {α : Type u_1} {f : α α} {x : α} {n : } (h : x) (m : ) :
f^[m % n] x = f^[m] x
@[protected]
theorem function.is_periodic_pt.mod {α : Type u_1} {f : α α} {x : α} {m n : } (hm : x) (hn : x) :
(m % n) x
@[protected]
theorem function.is_periodic_pt.gcd {α : Type u_1} {f : α α} {x : α} {m n : } (hm : x) (hn : x) :
(m.gcd n) x
theorem function.is_periodic_pt.eq_of_apply_eq_same {α : Type u_1} {f : α α} {x y : α} {n : } (hx : x) (hy : 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.is_periodic_pt.eq_of_apply_eq {α : Type u_1} {f : α α} {x y : α} {m n : } (hx : x) (hy : 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.

def function.pts_of_period {α : Type u_1} (f : α α) (n : ) :
set α

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

Equations
• = {x : α | x}
@[simp]
theorem function.mem_pts_of_period {α : Type u_1} {f : α α} {x : α} {n : } :
theorem function.semiconj.maps_to_pts_of_period {α : Type u_1} {β : Type u_2} {fa : α α} {fb : β β} {g : α β} (h : fb) (n : ) :
n) n)
theorem function.bij_on_pts_of_period {α : Type u_1} (f : α α) {n : } (hn : 0 < n) :
theorem function.directed_pts_of_period_pnat {α : Type u_1} (f : α α) :
(λ (n : ℕ+),
def function.periodic_pts {α : Type u_1} (f : α α) :
set α

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

Equations
theorem function.mk_mem_periodic_pts {α : Type u_1} {f : α α} {x : α} {n : } (hn : 0 < n) (hx : x) :
theorem function.mem_periodic_pts {α : Type u_1} {f : α α} {x : α} :
(n : ) (H : n > 0),
theorem function.is_periodic_pt_of_mem_periodic_pts_of_is_periodic_pt_iterate {α : Type u_1} {f : α α} {x : α} {m n : } (hx : x ) (hm : (f^[n] x)) :
theorem function.bUnion_pts_of_period {α : Type u_1} (f : α α) :
( (n : ) (H : n > 0), =
theorem function.Union_pnat_pts_of_period {α : Type u_1} (f : α α) :
( (n : ℕ+), =
theorem function.bij_on_periodic_pts {α : Type u_1} (f : α α) :
theorem function.semiconj.maps_to_periodic_pts {α : Type u_1} {β : Type u_2} {fa : α α} {fb : β β} {g : α β} (h : fb) :
noncomputable def function.minimal_period {α : 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 minimal_period f x = 0.

Equations
Instances for function.minimal_period
theorem function.is_periodic_pt_minimal_period {α : Type u_1} (f : α α) (x : α) :
@[simp]
theorem function.iterate_minimal_period {α : Type u_1} {f : α α} {x : α} :
= x
@[simp]
theorem function.iterate_add_minimal_period_eq {α : Type u_1} {f : α α} {x : α} {n : } :
f^[] x = f^[n] x
@[simp]
theorem function.iterate_mod_minimal_period_eq {α : Type u_1} {f : α α} {x : α} {n : } :
f^[] x = f^[n] x
theorem function.minimal_period_pos_of_mem_periodic_pts {α : Type u_1} {f : α α} {x : α} (hx : x ) :
theorem function.minimal_period_eq_zero_of_nmem_periodic_pts {α : Type u_1} {f : α α} {x : α} (hx : x ) :
theorem function.is_periodic_pt.minimal_period_pos {α : Type u_1} {f : α α} {x : α} {n : } (hn : 0 < n) (hx : x) :
theorem function.minimal_period_pos_iff_mem_periodic_pts {α : Type u_1} {f : α α} {x : α} :
theorem function.minimal_period_eq_zero_iff_nmem_periodic_pts {α : Type u_1} {f : α α} {x : α} :
theorem function.is_periodic_pt.minimal_period_le {α : Type u_1} {f : α α} {x : α} {n : } (hn : 0 < n) (hx : x) :
theorem function.minimal_period_apply_iterate {α : Type u_1} {f : α α} {x : α} (hx : x ) (n : ) :
(f^[n] x) =
theorem function.minimal_period_apply {α : Type u_1} {f : α α} {x : α} (hx : x ) :
(f x) =
theorem function.le_of_lt_minimal_period_of_iterate_eq {α : Type u_1} {f : α α} {x : α} {m n : } (hm : m < ) (hmn : f^[m] x = f^[n] x) :
m n
theorem function.eq_of_lt_minimal_period_of_iterate_eq {α : Type u_1} {f : α α} {x : α} {m n : } (hm : m < ) (hn : n < ) (hmn : f^[m] x = f^[n] x) :
m = n
theorem function.eq_iff_lt_minimal_period_of_iterate_eq {α : Type u_1} {f : α α} {x : α} {m n : } (hm : m < ) (hn : n < ) :
f^[m] x = f^[n] x m = n
theorem function.minimal_period_id {α : Type u_1} {x : α} :
theorem function.is_fixed_point_iff_minimal_period_eq_one {α : Type u_1} {f : α α} {x : α} :
theorem function.is_periodic_pt.eq_zero_of_lt_minimal_period {α : Type u_1} {f : α α} {x : α} {n : } (hx : x) (hn : n < ) :
n = 0
theorem function.not_is_periodic_pt_of_pos_of_lt_minimal_period {α : Type u_1} {f : α α} {x : α} {n : } (n0 : n 0) (hn : n < ) :
theorem function.is_periodic_pt.minimal_period_dvd {α : Type u_1} {f : α α} {x : α} {n : } (hx : x) :
theorem function.is_periodic_pt_iff_minimal_period_dvd {α : Type u_1} {f : α α} {x : α} {n : } :
theorem function.minimal_period_eq_minimal_period_iff {α : Type u_1} {β : Type u_2} {f : α α} {x : α} {g : β β} {y : β} :
(n : ),
theorem function.minimal_period_eq_prime {α : Type u_1} {f : α α} {x : α} {p : } [hp : fact (nat.prime p)] (hper : x) (hfix : ¬) :
theorem function.minimal_period_eq_prime_pow {α : Type u_1} {f : α α} {x : α} {p k : } [hp : fact (nat.prime p)] (hk : ¬ (p ^ k) x) (hk1 : (p ^ (k + 1)) x) :
= p ^ (k + 1)
theorem function.commute.minimal_period_of_comp_dvd_lcm {α : Type u_1} {f : α α} {x : α} {g : α α} (h : g) :
theorem function.commute.minimal_period_of_comp_dvd_mul {α : Type u_1} {f : α α} {x : α} {g : α α} (h : g) :
theorem function.commute.minimal_period_of_comp_eq_mul_of_coprime {α : Type u_1} {f : α α} {x : α} {g : α α} (h : g) (hco : ) :
theorem function.minimal_period_iterate_eq_div_gcd {α : Type u_1} {f : α α} {x : α} {n : } (h : n 0) :
= / .gcd n
theorem function.minimal_period_iterate_eq_div_gcd' {α : Type u_1} {f : α α} {x : α} {n : } (h : x ) :
= / .gcd n
noncomputable def function.periodic_orbit {α : 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
theorem function.periodic_orbit_def {α : Type u_1} (f : α α) (x : α) :
= (list.map (λ (n : ), f^[n] x) (list.range x)))

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

theorem function.periodic_orbit_eq_cycle_map {α : Type u_1} (f : α α) (x : α) :
= cycle.map (λ (n : ), f^[n] x)

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

@[simp]
theorem function.periodic_orbit_length {α : Type u_1} {f : α α} {x : α} :
@[simp]
theorem function.periodic_orbit_eq_nil_iff_not_periodic_pt {α : Type u_1} {f : α α} {x : α} :
theorem function.periodic_orbit_eq_nil_of_not_periodic_pt {α : Type u_1} {f : α α} {x : α} (h : x ) :
@[simp]
theorem function.mem_periodic_orbit_iff {α : Type u_1} {f : α α} {x y : α} (hx : x ) :
(n : ), f^[n] x = y
@[simp]
theorem function.iterate_mem_periodic_orbit {α : Type u_1} {f : α α} {x : α} (hx : x ) (n : ) :
f^[n] x
@[simp]
theorem function.self_mem_periodic_orbit {α : Type u_1} {f : α α} {x : α} (hx : x ) :
theorem function.nodup_periodic_orbit {α : Type u_1} {f : α α} {x : α} :
theorem function.periodic_orbit_apply_iterate_eq {α : Type u_1} {f : α α} {x : α} (hx : x ) (n : ) :
(f^[n] x) =
theorem function.periodic_orbit_apply_eq {α : Type u_1} {f : α α} {x : α} (hx : x ) :
(f x) =
theorem function.periodic_orbit_chain {α : Type u_1} (r : α α Prop) {f : α α} {x : α} :
(n : ), r (f^[n] x) (f^[n + 1] x)
theorem function.periodic_orbit_chain' {α : Type u_1} (r : α α Prop) {f : α α} {x : α} (hx : x ) :
(n : ), r (f^[n] x) (f^[n + 1] x)
@[simp]
theorem function.iterate_prod_map {α : Type u_1} {β : Type u_2} (f : α α) (g : β β) (n : ) :
g^[n] = g^[n]
@[simp]
theorem function.is_fixed_pt_prod_map {α : Type u_1} {β : Type u_2} {f : α α} {g : β β} (x : α × β) :
x
@[simp]
theorem function.is_periodic_pt_prod_map {α : Type u_1} {β : Type u_2} {f : α α} {g : β β} {n : } (x : α × β) :
n x
theorem function.minimal_period_prod_map {α : Type u_1} {β : Type u_2} (f : α α) (g : β β) (x : α × β) :
x = .lcm
theorem function.minimal_period_fst_dvd {α : Type u_1} {β : Type u_2} {f : α α} {g : β β} {x : α × β} :
theorem function.minimal_period_snd_dvd {α : Type u_1} {β : Type u_2} {f : α α} {g : β β} {x : α × β} :
theorem add_action.nsmul_vadd_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [add_group α] [ β] {a : α} {b : β} {n : } :
n a +ᵥ b = b
theorem mul_action.pow_smul_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [group α] [ β] {a : α} {b : β} {n : } :
a ^ n b = b
theorem add_action.zsmul_vadd_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [add_group α] [ β] {a : α} {b : β} {n : } :
n a +ᵥ b = b n
theorem mul_action.zpow_smul_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [group α] [ β] {a : α} {b : β} {n : } :
a ^ n b = b n
@[simp]
theorem add_action.nsmul_vadd_mod_minimal_period {α : Type u_1} {β : Type u_2} [add_group α] [ β] (a : α) (b : β) (n : ) :
(n % a +ᵥ b = n a +ᵥ b
@[simp]
theorem mul_action.pow_smul_mod_minimal_period {α : Type u_1} {β : Type u_2} [group α] [ β] (a : α) (b : β) (n : ) :
a ^ (n % b = a ^ n b
@[simp]
theorem add_action.zsmul_vadd_mod_minimal_period {α : Type u_1} {β : Type u_2} [add_group α] [ β] (a : α) (b : β) (n : ) :
(n % b)) a +ᵥ b = n a +ᵥ b
@[simp]
theorem mul_action.zpow_smul_mod_minimal_period {α : Type u_1} {β : Type u_2} [group α] [ β] (a : α) (b : β) (n : ) :
a ^ (n % b)) b = a ^ n b