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
Instances for function.is_periodic_pt
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.

@[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 : function.is_periodic_pt f n x) :
@[protected]
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 : ) :
@[protected]
theorem function.is_periodic_pt.apply {α : Type u_1} {f : α → α} {x : α} {n : } (hx : function.is_periodic_pt f n x) :
@[protected]
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) :
@[protected]
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) :
@[protected]
theorem function.is_periodic_pt.mul_const {α : Type u_1} {f : α → α} {x : α} {m : } (hm : function.is_periodic_pt f m x) (n : ) :
@[protected]
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) :
@[protected]
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.comp {α : Type u_1} {f : α → α} {x : α} {n : } {g : α → α} (hco : function.commute f g) (hf : function.is_periodic_pt f n x) (hg : function.is_periodic_pt g n x) :
theorem function.is_periodic_pt.comp_lcm {α : Type u_1} {f : α → α} {x : α} {m n : } {g : α → α} (hco : function.commute f g) (hf : function.is_periodic_pt f m x) (hg : function.is_periodic_pt g n x) :
theorem function.is_periodic_pt.left_of_comp {α : Type u_1} {f : α → α} {x : α} {n : } {g : α → α} (hco : function.commute f g) (hfg : function.is_periodic_pt (f g) n x) (hg : function.is_periodic_pt g n x) :
theorem function.is_periodic_pt.iterate_mod_apply {α : Type u_1} {f : α → α} {x : α} {n : } (h : function.is_periodic_pt f n x) (m : ) :
f^[m % n] x = f^[m] x
@[protected]
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) :
@[protected]
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.is_periodic_pt_of_mem_periodic_pts_of_is_periodic_pt_iterate {α : Type u_1} {f : α → α} {x : α} {m n : } (hx : x function.periodic_pts f) (hm : function.is_periodic_pt f m (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) :
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 : α} :
@[simp]
theorem function.iterate_add_minimal_period_eq {α : Type u_1} {f : α → α} {x : α} {n : } :
@[simp]
theorem function.iterate_mod_minimal_period_eq {α : 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.minimal_period_eq_zero_of_nmem_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_apply_iterate {α : Type u_1} {f : α → α} {x : α} (hx : x function.periodic_pts f) (n : ) :
theorem function.minimal_period_apply {α : Type u_1} {f : α → α} {x : α} (hx : x function.periodic_pts f) :
theorem function.le_of_lt_minimal_period_of_iterate_eq {α : Type u_1} {f : α → α} {x : α} {m n : } (hm : m < function.minimal_period f x) (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 < function.minimal_period f x) (hn : n < function.minimal_period f x) (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 < function.minimal_period f x) (hn : n < function.minimal_period f x) :
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 : 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.commute.minimal_period_of_comp_dvd_mul {α : 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) :
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 : α) :

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

theorem function.periodic_orbit_eq_cycle_map {α : Type u_1} (f : α → α) (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.mem_periodic_orbit_iff {α : Type u_1} {f : α → α} {x y : α} (hx : x function.periodic_pts f) :
y function.periodic_orbit f x ∃ (n : ), f^[n] x = y
@[simp]
theorem function.iterate_mem_periodic_orbit {α : Type u_1} {f : α → α} {x : α} (hx : x function.periodic_pts f) (n : ) :
@[simp]
theorem function.self_mem_periodic_orbit {α : Type u_1} {f : α → α} {x : α} (hx : x function.periodic_pts f) :
theorem function.nodup_periodic_orbit {α : Type u_1} {f : α → α} {x : α} :
theorem function.periodic_orbit_apply_iterate_eq {α : Type u_1} {f : α → α} {x : α} (hx : x function.periodic_pts f) (n : ) :
theorem function.periodic_orbit_apply_eq {α : Type u_1} {f : α → α} {x : α} (hx : x function.periodic_pts f) :
theorem function.periodic_orbit_chain {α : Type u_1} (r : α → α → Prop) {f : α → α} {x : α} :
cycle.chain r (function.periodic_orbit f x) ∀ (n : ), n < function.minimal_period f xr (f^[n] x) (f^[n + 1] x)
theorem function.periodic_orbit_chain' {α : Type u_1} (r : α → α → Prop) {f : α → α} {x : α} (hx : x function.periodic_pts f) :
cycle.chain r (function.periodic_orbit f x) ∀ (n : ), r (f^[n] x) (f^[n + 1] x)
theorem add_action.nsmul_vadd_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [add_group α] [add_action α β] {a : α} {b : β} {n : } :
theorem mul_action.pow_smul_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [group α] [mul_action α β] {a : α} {b : β} {n : } :
theorem add_action.zsmul_vadd_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [add_group α] [add_action α β] {a : α} {b : β} {n : } :
theorem mul_action.zpow_smul_eq_iff_minimal_period_dvd {α : Type u_1} {β : Type u_2} [group α] [mul_action α β] {a : α} {b : β} {n : } :
@[simp]
theorem add_action.nsmul_vadd_mod_minimal_period {α : Type u_1} {β : Type u_2} [add_group α] [add_action α β] (a : α) (b : β) (n : ) :
@[simp]
theorem mul_action.pow_smul_mod_minimal_period {α : Type u_1} {β : Type u_2} [group α] [mul_action α β] (a : α) (b : β) (n : ) :
@[simp]
theorem add_action.zsmul_vadd_mod_minimal_period {α : Type u_1} {β : Type u_2} [add_group α] [add_action α β] (a : α) (b : β) (n : ) :
@[simp]
theorem mul_action.zpow_smul_mod_minimal_period {α : Type u_1} {β : Type u_2} [group α] [mul_action α β] (a : α) (b : β) (n : ) :