Periodic points
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:xis a periodic point offof periodn, i.e.f^[n] x = x. We do not requiren > 0in the definition.pts_of_period f n: the set{x | is_periodic_pt f n x}. Note thatnis not required to be the minimal period ofx.periodic_pts f: the set of all periodic points off.minimal_period f x: the minimal period of a pointxunder an endomorphismfor zero ifxis not a periodic point off.
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
- 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.is_periodic_pt f n x = function.is_fixed_pt f^[n] x
theorem
function.is_fixed_pt.is_periodic_pt
{α : Type u_1}
{f : α → α}
{x : α}
(hf : function.is_fixed_pt f x)
(n : ℕ) :
function.is_periodic_pt 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.
theorem
function.is_periodic_pt_zero
{α : Type u_1}
(f : α → α)
(x : α) :
function.is_periodic_pt f 0 x
Any point is a periodic point of period 0.
@[instance]
def
function.is_periodic_pt.decidable
{α : Type u_1}
[decidable_eq α]
{f : α → α}
{n : ℕ}
{x : α} :
decidable (function.is_periodic_pt f n x)
theorem
function.is_periodic_pt.is_fixed_pt
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
function.is_periodic_pt f n x → function.is_fixed_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 : α → β} :
function.semiconj g fa fb → function.is_periodic_pt fb n (g x)
theorem
function.is_periodic_pt.apply_iterate
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hx : function.is_periodic_pt f n x)
(m : ℕ) :
function.is_periodic_pt f n (f^[m] x)
theorem
function.is_periodic_pt.apply
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
function.is_periodic_pt f n x → function.is_periodic_pt f n (f x)
theorem
function.is_periodic_pt.add
{α : Type u_1}
{f : α → α}
{x : α}
{m n : ℕ} :
function.is_periodic_pt f n x → function.is_periodic_pt f m x → function.is_periodic_pt f (n + m) x
theorem
function.is_periodic_pt.left_of_add
{α : Type u_1}
{f : α → α}
{x : α}
{m n : ℕ} :
function.is_periodic_pt f (n + m) x → function.is_periodic_pt f m x → function.is_periodic_pt f n x
theorem
function.is_periodic_pt.right_of_add
{α : Type u_1}
{f : α → α}
{x : α}
{m n : ℕ} :
function.is_periodic_pt f (n + m) x → function.is_periodic_pt f n x → function.is_periodic_pt f m x
theorem
function.is_periodic_pt.sub
{α : Type u_1}
{f : α → α}
{x : α}
{m n : ℕ} :
function.is_periodic_pt f m x → function.is_periodic_pt f n x → function.is_periodic_pt f (m - n) x
theorem
function.is_periodic_pt.mul_const
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
(hm : function.is_periodic_pt f m x)
(n : ℕ) :
function.is_periodic_pt f (m * n) x
theorem
function.is_periodic_pt.const_mul
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
(hm : function.is_periodic_pt f m x)
(n : ℕ) :
function.is_periodic_pt f (n * m) x
theorem
function.is_periodic_pt.trans_dvd
{α : Type u_1}
{f : α → α}
{x : α}
{m : ℕ}
(hm : function.is_periodic_pt f m x)
{n : ℕ} :
m ∣ n → function.is_periodic_pt f n x
theorem
function.is_periodic_pt.iterate
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hf : function.is_periodic_pt f n x)
(m : ℕ) :
function.is_periodic_pt f^[m] n x
theorem
function.is_periodic_pt.mod
{α : Type u_1}
{f : α → α}
{x : α}
{m n : ℕ} :
function.is_periodic_pt f m x → function.is_periodic_pt f n x → function.is_periodic_pt f (m % n) x
theorem
function.is_periodic_pt.gcd
{α : Type u_1}
{f : α → α}
{x : α}
{m n : ℕ} :
function.is_periodic_pt f m x → function.is_periodic_pt f n x → function.is_periodic_pt f (m.gcd n) x
theorem
function.is_periodic_pt.eq_of_apply_eq_same
{α : Type u_1}
{f : α → α}
{x y : α}
{n : ℕ} :
function.is_periodic_pt f n x → function.is_periodic_pt f n y → 0 < n → 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 : ℕ} :
function.is_periodic_pt f m x → function.is_periodic_pt f n y → 0 < m → 0 < n → 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.pts_of_period f n = {x : α | function.is_periodic_pt f n x}
@[simp]
theorem
function.mem_pts_of_period
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
x ∈ function.pts_of_period f n ↔ function.is_periodic_pt f n x
theorem
function.semiconj.maps_to_pts_of_period
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{g : α → β}
(h : function.semiconj g fa fb)
(n : ℕ) :
set.maps_to g (function.pts_of_period fa n) (function.pts_of_period fb n)
theorem
function.bij_on_pts_of_period
{α : Type u_1}
(f : α → α)
{n : ℕ} :
0 < n → set.bij_on f (function.pts_of_period f n) (function.pts_of_period f n)
theorem
function.directed_pts_of_period_pnat
{α : Type u_1}
(f : α → α) :
directed has_subset.subset (λ (n : ℕ+), function.pts_of_period f ↑n)
The set of periodic points of a map f : α → α.
Equations
- function.periodic_pts f = {x : α | ∃ (n : ℕ) (H : n > 0), function.is_periodic_pt f n x}
theorem
function.mk_mem_periodic_pts
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
0 < n → function.is_periodic_pt f n x → x ∈ function.periodic_pts f
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 : α → α) :
(⋃ (n : ℕ+), function.pts_of_period f ↑n) = function.periodic_pts f
theorem
function.semiconj.maps_to_periodic_pts
{α : Type u_1}
{β : Type u_2}
{fa : α → α}
{fb : β → β}
{g : α → β} :
function.semiconj g fa fb → set.maps_to g (function.periodic_pts fa) (function.periodic_pts fb)
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
- function.minimal_period f x = dite (x ∈ function.periodic_pts f) (λ (h : x ∈ function.periodic_pts f), nat.find h) (λ (h : x ∉ function.periodic_pts f), 0)
theorem
function.minimal_period_pos_of_mem_periodic_pts
{α : Type u_1}
{f : α → α}
{x : α} :
x ∈ function.periodic_pts f → 0 < function.minimal_period f x
theorem
function.is_periodic_pt.minimal_period_pos
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
0 < n → function.is_periodic_pt f n x → 0 < function.minimal_period f x
theorem
function.minimal_period_pos_iff_mem_periodic_pts
{α : Type u_1}
{f : α → α}
{x : α} :
0 < function.minimal_period f x ↔ x ∈ function.periodic_pts f
theorem
function.is_periodic_pt.minimal_period_le
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
0 < n → function.is_periodic_pt f n x → function.minimal_period f x ≤ n
theorem
function.is_periodic_pt.eq_zero_of_lt_minimal_period
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
function.is_periodic_pt f n x → n < function.minimal_period f x → n = 0
theorem
function.is_periodic_pt.minimal_period_dvd
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
function.is_periodic_pt f n x → function.minimal_period f x ∣ n
theorem
function.is_periodic_pt_iff_minimal_period_dvd
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ} :
function.is_periodic_pt f n x ↔ function.minimal_period f x ∣ n