Documentation

Mathlib.Dynamics.PeriodicPts

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 : IsPeriodicPt f n x including arithmetic operations on n and h.map (hg : SemiconjBy g f f'). We also prove that f is bijective on each set ptsOfPeriod f n and on periodicPts f. Finally, we prove that x is a periodic point of f of period n if and only if minimalPeriod f x | n.

References #

def Function.IsPeriodicPt {α : Type u_1} (f : αα) (n : ) (x : α) :

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.IsFixedPt.isPeriodicPt {α : Type u_1} {f : αα} {x : α} (hf : Function.IsFixedPt 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.isPeriodicPt_zero {α : Type u_1} (f : αα) (x : α) :

Any point is a periodic point of period 0.

instance Function.IsPeriodicPt.instDecidableIsPeriodicPt {α : Type u_1} [inst : DecidableEq α] {f : αα} {n : } {x : α} :
Equations
  • Function.IsPeriodicPt.instDecidableIsPeriodicPt = Function.IsFixedPt.decidable
theorem Function.IsPeriodicPt.isFixedPt {α : Type u_1} {f : αα} {x : α} {n : } (hf : Function.IsPeriodicPt f n x) :
theorem Function.IsPeriodicPt.map {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {x : α} {n : } (hx : Function.IsPeriodicPt fa n x) {g : αβ} (hg : Function.Semiconj g fa fb) :
theorem Function.IsPeriodicPt.apply_iterate {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) (m : ) :
theorem Function.IsPeriodicPt.apply {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) :
theorem Function.IsPeriodicPt.add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f n x) (hm : Function.IsPeriodicPt f m x) :
theorem Function.IsPeriodicPt.left_of_add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f (n + m) x) (hm : Function.IsPeriodicPt f m x) :
theorem Function.IsPeriodicPt.right_of_add {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hn : Function.IsPeriodicPt f (n + m) x) (hm : Function.IsPeriodicPt f n x) :
theorem Function.IsPeriodicPt.sub {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : Function.IsPeriodicPt f m x) (hn : Function.IsPeriodicPt f n x) :
theorem Function.IsPeriodicPt.mul_const {α : Type u_1} {f : αα} {x : α} {m : } (hm : Function.IsPeriodicPt f m x) (n : ) :
theorem Function.IsPeriodicPt.const_mul {α : Type u_1} {f : αα} {x : α} {m : } (hm : Function.IsPeriodicPt f m x) (n : ) :
theorem Function.IsPeriodicPt.trans_dvd {α : Type u_1} {f : αα} {x : α} {m : } (hm : Function.IsPeriodicPt f m x) {n : } (hn : m n) :
theorem Function.IsPeriodicPt.iterate {α : Type u_1} {f : αα} {x : α} {n : } (hf : Function.IsPeriodicPt f n x) (m : ) :
theorem Function.IsPeriodicPt.comp {α : Type u_1} {f : αα} {x : α} {n : } {g : αα} (hco : Function.Commute f g) (hf : Function.IsPeriodicPt f n x) (hg : Function.IsPeriodicPt g n x) :
theorem Function.IsPeriodicPt.comp_lcm {α : Type u_1} {f : αα} {x : α} {m : } {n : } {g : αα} (hco : Function.Commute f g) (hf : Function.IsPeriodicPt f m x) (hg : Function.IsPeriodicPt g n x) :
theorem Function.IsPeriodicPt.left_of_comp {α : Type u_1} {f : αα} {x : α} {n : } {g : αα} (hco : Function.Commute f g) (hfg : Function.IsPeriodicPt (f g) n x) (hg : Function.IsPeriodicPt g n x) :
theorem Function.IsPeriodicPt.iterate_mod_apply {α : Type u_1} {f : αα} {x : α} {n : } (h : Function.IsPeriodicPt f n x) (m : ) :
(f^[m % n]) x = (f^[m]) x
theorem Function.IsPeriodicPt.mod {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : Function.IsPeriodicPt f m x) (hn : Function.IsPeriodicPt f n x) :
theorem Function.IsPeriodicPt.gcd {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : Function.IsPeriodicPt f m x) (hn : Function.IsPeriodicPt f n x) :
theorem Function.IsPeriodicPt.eq_of_apply_eq_same {α : Type u_1} {f : αα} {x : α} {y : α} {n : } (hx : Function.IsPeriodicPt f n x) (hy : Function.IsPeriodicPt 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.IsPeriodicPt.eq_of_apply_eq {α : Type u_1} {f : αα} {x : α} {y : α} {m : } {n : } (hx : Function.IsPeriodicPt f m x) (hy : Function.IsPeriodicPt 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.ptsOfPeriod {α : Type u_1} (f : αα) (n : ) :
Set α

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

Equations
@[simp]
theorem Function.mem_ptsOfPeriod {α : Type u_1} {f : αα} {x : α} {n : } :
theorem Function.Semiconj.mapsTo_ptsOfPeriod {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {g : αβ} (h : Function.Semiconj g fa fb) (n : ) :
theorem Function.bijOn_ptsOfPeriod {α : Type u_1} (f : αα) {n : } (hn : 0 < n) :
theorem Function.directed_ptsOfPeriod_pNat {α : Type u_1} (f : αα) :
Directed (fun x x_1 => x x_1) fun n => Function.ptsOfPeriod f n
def Function.periodicPts {α : Type u_1} (f : αα) :
Set α

The set of periodic points of a map f : α → α→ α.

Equations
theorem Function.mk_mem_periodicPts {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) :
theorem Function.mem_periodicPts {α : Type u_1} {f : αα} {x : α} :
theorem Function.Semiconj.mapsTo_periodicPts {α : Type u_1} {β : Type u_2} {fa : αα} {fb : ββ} {g : αβ} (h : Function.Semiconj g fa fb) :
def Function.minimalPeriod {α : 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 minimalPeriod f x = 0.

Equations
@[simp]
theorem Function.iterate_minimalPeriod {α : Type u_1} {f : αα} {x : α} :
@[simp]
theorem Function.iterate_add_minimalPeriod_eq {α : Type u_1} {f : αα} {x : α} {n : } :
@[simp]
theorem Function.iterate_mod_minimalPeriod_eq {α : Type u_1} {f : αα} {x : α} {n : } :
theorem Function.IsPeriodicPt.minimalPeriod_pos {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) :
theorem Function.IsPeriodicPt.minimalPeriod_le {α : Type u_1} {f : αα} {x : α} {n : } (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) :
theorem Function.minimalPeriod_apply_iterate {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) (n : ) :
theorem Function.minimalPeriod_apply {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) :
theorem Function.le_of_lt_minimalPeriod_of_iterate_eq {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : m < Function.minimalPeriod f x) (hmn : (f^[m]) x = (f^[n]) x) :
m n
theorem Function.eq_of_lt_minimalPeriod_of_iterate_eq {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : m < Function.minimalPeriod f x) (hn : n < Function.minimalPeriod f x) (hmn : (f^[m]) x = (f^[n]) x) :
m = n
theorem Function.eq_iff_lt_minimalPeriod_of_iterate_eq {α : Type u_1} {f : αα} {x : α} {m : } {n : } (hm : m < Function.minimalPeriod f x) (hn : n < Function.minimalPeriod f x) :
(f^[m]) x = (f^[n]) x m = n
theorem Function.IsPeriodicPt.eq_zero_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) (hn : n < Function.minimalPeriod f x) :
n = 0
theorem Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod {α : Type u_1} {f : αα} {x : α} {n : } :
theorem Function.IsPeriodicPt.minimalPeriod_dvd {α : Type u_1} {f : αα} {x : α} {n : } (hx : Function.IsPeriodicPt f n x) :
theorem Function.minimalPeriod_eq_minimalPeriod_iff {α : Type u_1} {β : Type u_2} {f : αα} {x : α} {g : ββ} {y : β} :
theorem Function.minimalPeriod_eq_prime {α : Type u_1} {f : αα} {x : α} {p : } [hp : Fact (Nat.Prime p)] (hper : Function.IsPeriodicPt f p x) (hfix : ¬Function.IsFixedPt f x) :
theorem Function.minimalPeriod_eq_prime_pow {α : Type u_1} {f : αα} {x : α} {p : } {k : } [hp : Fact (Nat.Prime p)] (hk : ¬Function.IsPeriodicPt f (p ^ k) x) (hk1 : Function.IsPeriodicPt f (p ^ (k + 1)) x) :
def Function.periodicOrbit {α : 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.periodicOrbit_def {α : Type u_1} (f : αα) (x : α) :

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

theorem Function.periodicOrbit_eq_cycle_map {α : Type u_1} (f : αα) (x : α) :

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

@[simp]
theorem Function.periodicOrbit_length {α : Type u_1} {f : αα} {x : α} :
@[simp]
theorem Function.periodicOrbit_eq_nil_of_not_periodic_pt {α : Type u_1} {f : αα} {x : α} (h : ¬x Function.periodicPts f) :
@[simp]
theorem Function.mem_periodicOrbit_iff {α : Type u_1} {f : αα} {x : α} {y : α} (hx : x Function.periodicPts f) :
y Function.periodicOrbit f x n, (f^[n]) x = y
@[simp]
theorem Function.iterate_mem_periodicOrbit {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) (n : ) :
@[simp]
theorem Function.self_mem_periodicOrbit {α : Type u_1} {f : αα} {x : α} (hx : x Function.periodicPts f) :
theorem Function.nodup_periodicOrbit {α : Type u_1} {f : αα} {x : α} :
theorem Function.periodicOrbit_chain {α : Type u_1} (r : ααProp) {f : αα} {x : α} :
Cycle.Chain r (Function.periodicOrbit f x) (n : ) → n < Function.minimalPeriod f xr ((f^[n]) x) ((f^[n + 1]) x)
theorem Function.periodicOrbit_chain' {α : Type u_1} (r : ααProp) {f : αα} {x : α} (hx : x Function.periodicPts f) :
Cycle.Chain r (Function.periodicOrbit f x) (n : ) → r ((f^[n]) x) ((f^[n + 1]) x)
theorem AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {a : α} {b : β} {n : } :
n a +ᵥ b = b Function.minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b n
theorem MulAction.pow_smul_eq_iff_minimalPeriod_dvd {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {a : α} {b : β} {n : } :
a ^ n b = b Function.minimalPeriod ((fun x x_1 => x x_1) a) b n
theorem AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {a : α} {b : β} {n : } :
n a +ᵥ b = b ↑(Function.minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) n
theorem MulAction.zpow_smul_eq_iff_minimalPeriod_dvd {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {a : α} {b : β} {n : } :
a ^ n b = b ↑(Function.minimalPeriod ((fun x x_1 => x x_1) a) b) n
@[simp]
theorem AddAction.nsmul_vadd_mod_minimalPeriod {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] (a : α) (b : β) (n : ) :
(n % Function.minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b) a +ᵥ b = n a +ᵥ b
@[simp]
theorem MulAction.pow_smul_mod_minimalPeriod {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] (a : α) (b : β) (n : ) :
a ^ (n % Function.minimalPeriod ((fun x x_1 => x x_1) a) b) b = a ^ n b
@[simp]
theorem AddAction.zsmul_vadd_mod_minimalPeriod {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] (a : α) (b : β) (n : ) :
(n % ↑(Function.minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)) a +ᵥ b = n a +ᵥ b
@[simp]
theorem MulAction.zpow_smul_mod_minimalPeriod {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] (a : α) (b : β) (n : ) :
a ^ (n % ↑(Function.minimalPeriod ((fun x x_1 => x x_1) a) b)) b = a ^ n b