mathlib documentation

dynamics.periodic_pts

Periodic points #

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

Main definitions #

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

theorem function.is_periodic_pt.is_fixed_pt {α : Type u_1} {f : α → α} {x : α} {n : } (hf : function.is_periodic_pt f n x) :
theorem function.is_periodic_pt.map {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {x : α} {n : } (hx : function.is_periodic_pt fa n x) {g : α → β} (hg : function.semiconj g fa fb) :
theorem function.is_periodic_pt.apply_iterate {α : Type u_1} {f : α → α} {x : α} {n : } (hx : function.is_periodic_pt f n x) (m : ) :
theorem function.is_periodic_pt.apply {α : Type u_1} {f : α → α} {x : α} {n : } (hx : function.is_periodic_pt f n x) :
theorem function.is_periodic_pt.add {α : Type u_1} {f : α → α} {x : α} {m n : } (hn : function.is_periodic_pt f n x) (hm : function.is_periodic_pt f m x) :
theorem function.is_periodic_pt.left_of_add {α : Type u_1} {f : α → α} {x : α} {m n : } (hn : function.is_periodic_pt f (n + m) x) (hm : function.is_periodic_pt f m x) :
theorem function.is_periodic_pt.right_of_add {α : Type u_1} {f : α → α} {x : α} {m n : } (hn : function.is_periodic_pt f (n + m) x) (hm : function.is_periodic_pt f n x) :
theorem function.is_periodic_pt.sub {α : Type u_1} {f : α → α} {x : α} {m n : } (hm : function.is_periodic_pt f m x) (hn : function.is_periodic_pt f n x) :
theorem function.is_periodic_pt.mul_const {α : Type u_1} {f : α → α} {x : α} {m : } (hm : function.is_periodic_pt f m x) (n : ) :
theorem function.is_periodic_pt.const_mul {α : Type u_1} {f : α → α} {x : α} {m : } (hm : function.is_periodic_pt f m x) (n : ) :
theorem function.is_periodic_pt.trans_dvd {α : Type u_1} {f : α → α} {x : α} {m : } (hm : function.is_periodic_pt f m x) {n : } (hn : m n) :
theorem function.is_periodic_pt.iterate {α : Type u_1} {f : α → α} {x : α} {n : } (hf : function.is_periodic_pt f n x) (m : ) :
theorem function.is_periodic_pt.mod {α : Type u_1} {f : α → α} {x : α} {m n : } (hm : function.is_periodic_pt f m x) (hn : function.is_periodic_pt f n x) :
theorem function.is_periodic_pt.gcd {α : Type u_1} {f : α → α} {x : α} {m n : } (hm : function.is_periodic_pt f m x) (hn : function.is_periodic_pt f n x) :
theorem function.is_periodic_pt.eq_of_apply_eq_same {α : Type u_1} {f : α → α} {x y : α} {n : } (hx : function.is_periodic_pt f n x) (hy : function.is_periodic_pt 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.is_periodic_pt.eq_of_apply_eq {α : Type u_1} {f : α → α} {x y : α} {m n : } (hx : function.is_periodic_pt f m x) (hy : function.is_periodic_pt 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.

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

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

Equations
@[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 : function.semiconj g fa fb) (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 : α → α) :
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 : function.is_periodic_pt f n x) :
theorem function.mem_periodic_pts {α : Type u_1} {f : α → α} {x : α} :
x function.periodic_pts f ∃ (n : ) (H : n > 0), function.is_periodic_pt f n x
theorem function.bUnion_pts_of_period {α : Type u_1} (f : α → α) :
(⋃ (n : ) (H : n > 0), function.pts_of_period f n) = function.periodic_pts f
theorem function.Union_pnat_pts_of_period {α : Type u_1} (f : α → α) :
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 : function.semiconj g fa fb) :
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
theorem function.is_periodic_pt_minimal_period {α : Type u_1} (f : α → α) (x : α) :
theorem function.iterate_eq_mod_minimal_period {α : Type u_1} {f : α → α} {x : α} {n : } :
theorem function.minimal_period_pos_of_mem_periodic_pts {α : Type u_1} {f : α → α} {x : α} (hx : x function.periodic_pts f) :
theorem function.is_periodic_pt.minimal_period_pos {α : Type u_1} {f : α → α} {x : α} {n : } (hn : 0 < n) (hx : function.is_periodic_pt f n x) :
theorem function.minimal_period_pos_iff_mem_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 : function.is_periodic_pt f n x) :
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 : function.is_periodic_pt f n x) (hn : n < function.minimal_period f x) :
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 < function.minimal_period f x) :
theorem function.is_periodic_pt.minimal_period_dvd {α : Type u_1} {f : α → α} {x : α} {n : } (hx : function.is_periodic_pt f n 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 : β} :
theorem function.minimal_period_eq_prime {α : Type u_1} {f : α → α} {x : α} {p : } [hp : fact (nat.prime p)] (hper : function.is_periodic_pt f p x) (hfix : ¬function.is_fixed_pt f x) :
theorem function.minimal_period_eq_prime_pow {α : Type u_1} {f : α → α} {x : α} {p k : } [hp : fact (nat.prime p)] (hk : ¬function.is_periodic_pt f (p ^ k) x) (hk1 : function.is_periodic_pt f (p ^ (k + 1)) x) :
theorem function.commute.minimal_period_of_comp_dvd_lcm {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : function.commute f g) :
theorem function.minimal_period_iterate_eq_div_gcd {α : Type u_1} {f : α → α} {x : α} {n : } (h : n 0) :