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: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.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 #
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
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 : ℕ) :
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)
@[simp]
theorem
function.iterate_minimal_period
{α : Type u_1}
{f : α → α}
{x : α} :
f^[function.minimal_period f x] x = x
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.minimal_period_eq_zero_of_nmem_periodic_pts
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∉ function.periodic_pts f) :
function.minimal_period f x = 0
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.minimal_period_eq_zero_iff_nmem_periodic_pts
{α : Type u_1}
{f : α → α}
{x : α} :
function.minimal_period f x = 0 ↔ 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.minimal_period_apply_iterate
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ function.periodic_pts f)
(n : ℕ) :
function.minimal_period f (f^[n] x) = function.minimal_period f x
theorem
function.minimal_period_apply
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ function.periodic_pts f) :
function.minimal_period f (f x) = function.minimal_period f x
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.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
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
- function.periodic_orbit f x = ↑(list.map (λ (n : ℕ), f^[n] x) (list.range (function.minimal_period f x)))
theorem
function.periodic_orbit_def
{α : Type u_1}
(f : α → α)
(x : α) :
function.periodic_orbit f x = ↑(list.map (λ (n : ℕ), f^[n] x) (list.range (function.minimal_period 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 : α) :
function.periodic_orbit f x = cycle.map (λ (n : ℕ), f^[n] x) ↑(list.range (function.minimal_period f x))
The definition of a periodic orbit, in terms of cycle.map.
@[simp]
@[simp]
theorem
function.periodic_orbit_eq_nil_of_not_periodic_pt
{α : Type u_1}
{f : α → α}
{x : α}
(h : x ∉ function.periodic_pts f) :
@[simp]
theorem
function.mem_periodic_orbit_iff
{α : Type u_1}
{f : α → α}
{x y : α}
(hx : x ∈ function.periodic_pts f) :
@[simp]
theorem
function.iterate_mem_periodic_orbit
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ function.periodic_pts f)
(n : ℕ) :
f^[n] x ∈ function.periodic_orbit f x
@[simp]
theorem
function.self_mem_periodic_orbit
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ function.periodic_pts f) :
x ∈ function.periodic_orbit f x
theorem
function.nodup_periodic_orbit
{α : Type u_1}
{f : α → α}
{x : α} :
(function.periodic_orbit f x).nodup
theorem
function.periodic_orbit_apply_iterate_eq
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ function.periodic_pts f)
(n : ℕ) :
function.periodic_orbit f (f^[n] x) = function.periodic_orbit f x
theorem
function.periodic_orbit_apply_eq
{α : Type u_1}
{f : α → α}
{x : α}
(hx : x ∈ function.periodic_pts f) :
function.periodic_orbit f (f x) = function.periodic_orbit f x
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 x → r (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)
@[simp]
theorem
function.is_fixed_pt_prod_map
{α : Type u_1}
{β : Type u_2}
{f : α → α}
{g : β → β}
(x : α × β) :
function.is_fixed_pt (prod.map f g) x ↔ function.is_fixed_pt f x.fst ∧ function.is_fixed_pt g x.snd
@[simp]
theorem
function.is_periodic_pt_prod_map
{α : Type u_1}
{β : Type u_2}
{f : α → α}
{g : β → β}
{n : ℕ}
(x : α × β) :
function.is_periodic_pt (prod.map f g) n x ↔ function.is_periodic_pt f n x.fst ∧ function.is_periodic_pt g n x.snd
theorem
function.minimal_period_prod_map
{α : Type u_1}
{β : Type u_2}
(f : α → α)
(g : β → β)
(x : α × β) :
function.minimal_period (prod.map f g) x = (function.minimal_period f x.fst).lcm (function.minimal_period g x.snd)
theorem
function.minimal_period_fst_dvd
{α : Type u_1}
{β : Type u_2}
{f : α → α}
{g : β → β}
{x : α × β} :
function.minimal_period f x.fst ∣ function.minimal_period (prod.map f g) x
theorem
function.minimal_period_snd_dvd
{α : Type u_1}
{β : Type u_2}
{f : α → α}
{g : β → β}
{x : α × β} :
function.minimal_period g x.snd ∣ function.minimal_period (prod.map f g) x
theorem
add_action.nsmul_vadd_eq_iff_minimal_period_dvd
{α : Type u_1}
{β : Type u_2}
[add_group α]
[add_action α β]
{a : α}
{b : β}
{n : ℕ} :
n • a +ᵥ b = b ↔ function.minimal_period (has_vadd.vadd 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 : ℕ} :
a ^ n • b = b ↔ function.minimal_period (has_smul.smul 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 : ℤ} :
n • a +ᵥ b = b ↔ ↑(function.minimal_period (has_vadd.vadd 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 : ℤ} :
a ^ n • b = b ↔ ↑(function.minimal_period (has_smul.smul 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 : ℕ) :
(n % function.minimal_period (has_vadd.vadd a) b) • a +ᵥ b = n • a +ᵥ b
@[simp]
theorem
mul_action.pow_smul_mod_minimal_period
{α : Type u_1}
{β : Type u_2}
[group α]
[mul_action α β]
(a : α)
(b : β)
(n : ℕ) :
a ^ (n % function.minimal_period (has_smul.smul a) b) • b = a ^ n • b
@[simp]
theorem
add_action.zsmul_vadd_mod_minimal_period
{α : Type u_1}
{β : Type u_2}
[add_group α]
[add_action α β]
(a : α)
(b : β)
(n : ℤ) :
(n % ↑(function.minimal_period (has_vadd.vadd a) b)) • a +ᵥ b = n • a +ᵥ b
@[simp]
theorem
mul_action.zpow_smul_mod_minimal_period
{α : Type u_1}
{β : Type u_2}
[group α]
[mul_action α β]
(a : α)
(b : β)
(n : ℤ) :
a ^ (n % ↑(function.minimal_period (has_smul.smul a) b)) • b = a ^ n • b