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 #
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.
@[protected, instance]
def
function.is_periodic_pt.decidable
{α : Type u_1}
[decidable_eq α]
{f : α → α}
{n : ℕ}
{x : α} :
decidable (function.is_periodic_pt f n x)
@[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) :
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)
@[protected]
theorem
function.is_periodic_pt.apply
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hx : function.is_periodic_pt f n x) :
function.is_periodic_pt f n (f 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) :
function.is_periodic_pt f (n + 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) :
function.is_periodic_pt f n 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) :
function.is_periodic_pt f m 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) :
function.is_periodic_pt f (m - 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 : ℕ) :
function.is_periodic_pt f (m * n) x
@[protected]
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 : ℕ}
(hn : m ∣ n) :
function.is_periodic_pt f n x
@[protected]
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.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) :
function.is_periodic_pt (f ∘ 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) :
function.is_periodic_pt (f ∘ g) (m.lcm 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) :
function.is_periodic_pt f n 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) :
function.is_periodic_pt f (m % 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) :
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 : ℕ}
(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.
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 : ℕ}
(hn : 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 : ℕ}
(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)) :
function.is_periodic_pt f m 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 : α → β}
(h : 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 : α}
(hx : 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 : ℕ}
(hn : 0 < n)
(hx : 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 : ℕ}
(hn : 0 < n)
(hx : function.is_periodic_pt f n x) :
function.minimal_period f x ≤ n
theorem
function.is_fixed_point_iff_minimal_period_eq_one
{α : Type u_1}
{f : α → α}
{x : α} :
function.minimal_period f x = 1 ↔ function.is_fixed_pt 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) :
¬function.is_periodic_pt f n x
theorem
function.is_periodic_pt.minimal_period_dvd
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(hx : 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
theorem
function.minimal_period_eq_minimal_period_iff
{α : Type u_1}
{β : Type u_2}
{f : α → α}
{x : α}
{g : β → β}
{y : β} :
function.minimal_period f x = function.minimal_period g y ↔ ∀ (n : ℕ), function.is_periodic_pt f n x ↔ function.is_periodic_pt g n 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) :
function.minimal_period f x = p
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) :
function.minimal_period f x = p ^ (k + 1)
theorem
function.commute.minimal_period_of_comp_dvd_lcm
{α : Type u_1}
{f : α → α}
{x : α}
{g : α → α}
(h : function.commute f g) :
function.minimal_period (f ∘ g) x ∣ (function.minimal_period f x).lcm (function.minimal_period g x)
theorem
function.commute.minimal_period_of_comp_dvd_mul
{α : Type u_1}
{f : α → α}
{x : α}
{g : α → α}
(h : function.commute f g) :
function.minimal_period (f ∘ g) x ∣ (function.minimal_period f x) * function.minimal_period g x
theorem
function.commute.minimal_period_of_comp_eq_mul_of_coprime
{α : Type u_1}
{f : α → α}
{x : α}
{g : α → α}
(h : function.commute f g)
(hco : (function.minimal_period f x).coprime (function.minimal_period g x)) :
function.minimal_period (f ∘ g) x = (function.minimal_period f x) * function.minimal_period g x
theorem
function.minimal_period_iterate_eq_div_gcd
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(h : n ≠ 0) :
function.minimal_period f^[n] x = function.minimal_period f x / (function.minimal_period f x).gcd n
theorem
function.minimal_period_iterate_eq_div_gcd'
{α : Type u_1}
{f : α → α}
{x : α}
{n : ℕ}
(h : x ∈ function.periodic_pts f) :
function.minimal_period f^[n] x = function.minimal_period f x / (function.minimal_period f x).gcd n