Periodic points

A point x : α is a periodic point of f : α → α of period n if f^[n] x = x.

Main definitions

• IsPeriodicPt f n x : x is a periodic point of f of period n, i.e. f^[n] x = x. We do not require n > 0 in the definition.
• ptsOfPeriod f n : the set {x | IsPeriodicPt f n x}. Note that n is not required to be the minimal period of x.
• periodicPts f : the set of all periodic points of f.
• minimalPeriod f x : the minimal period of a point x under an endomorphism f or zero if x is not a periodic point of f.
• orbit f x: the cycle [x, f x, f (f x), ...] for a periodic point.
• MulAction.period g x : the minimal period of a point x under the multiplicative action of g; an equivalent AddAction.period g x is defined for additive actions.

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

• https://en.wikipedia.org/wiki/Periodic_point

def Function.IsPeriodicPt {α : 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

• Function.IsPeriodicPt f n x = Function.IsFixedPt f^[n] x

theorem Function.IsFixedPt.isPeriodicPt {α : Type u_1} {f : α → α} {x : α} (hf : Function.IsFixedPt f x) (n : ℕ) : Function.IsPeriodicPt f n x

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 : α) : Function.IsPeriodicPt id n x

For the identity map, all points are periodic.

theorem Function.isPeriodicPt_zero {α : Type u_1} (f : α → α) (x : α) : Function.IsPeriodicPt f 0 x

Any point is a periodic point of period 0.

instance Function.IsPeriodicPt.instDecidableOfDecidableEq {α : Type u_1} [DecidableEq α] {f : α → α} {n : ℕ} {x : α} : Decidable (Function.IsPeriodicPt f n x)

Equations

• Function.IsPeriodicPt.instDecidableOfDecidableEq = Function.IsFixedPt.decidable

theorem Function.IsPeriodicPt.isFixedPt {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hf : Function.IsPeriodicPt f n x) : Function.IsFixedPt 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) : Function.IsPeriodicPt fb n (g x)

theorem Function.IsPeriodicPt.apply_iterate {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hx : Function.IsPeriodicPt f n x) (m : ℕ) : Function.IsPeriodicPt f n (f^[m] x)

theorem Function.IsPeriodicPt.apply {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hx : Function.IsPeriodicPt f n x) : Function.IsPeriodicPt f n (f x)

theorem Function.IsPeriodicPt.add {α : Type u_1} {f : α → α} {x : α} {m : ℕ} {n : ℕ} (hn : Function.IsPeriodicPt f n x) (hm : Function.IsPeriodicPt f m x) : Function.IsPeriodicPt f (n + 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) : Function.IsPeriodicPt f n 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) : Function.IsPeriodicPt f m x

theorem Function.IsPeriodicPt.sub {α : Type u_1} {f : α → α} {x : α} {m : ℕ} {n : ℕ} (hm : Function.IsPeriodicPt f m x) (hn : Function.IsPeriodicPt f n x) : Function.IsPeriodicPt f (m - n) x

theorem Function.IsPeriodicPt.mul_const {α : Type u_1} {f : α → α} {x : α} {m : ℕ} (hm : Function.IsPeriodicPt f m x) (n : ℕ) : Function.IsPeriodicPt f (m * n) x

theorem Function.IsPeriodicPt.const_mul {α : Type u_1} {f : α → α} {x : α} {m : ℕ} (hm : Function.IsPeriodicPt f m x) (n : ℕ) : Function.IsPeriodicPt f (n * m) x

theorem Function.IsPeriodicPt.trans_dvd {α : Type u_1} {f : α → α} {x : α} {m : ℕ} (hm : Function.IsPeriodicPt f m x) {n : ℕ} (hn : m ∣ n) : Function.IsPeriodicPt f n x

theorem Function.IsPeriodicPt.iterate {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hf : Function.IsPeriodicPt f n x) (m : ℕ) : Function.IsPeriodicPt f^[m] n x

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) : Function.IsPeriodicPt (f ∘ 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) : Function.IsPeriodicPt (f ∘ g) (m.lcm 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) : Function.IsPeriodicPt f 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) : Function.IsPeriodicPt f (m % 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) : Function.IsPeriodicPt f (m.gcd 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

• Function.ptsOfPeriod f n = {x : α | Function.IsPeriodicPt f n x}

@[simp]

theorem Function.mem_ptsOfPeriod {α : Type u_1} {f : α → α} {x : α} {n : ℕ} : x ∈ Function.ptsOfPeriod f n ↔ Function.IsPeriodicPt f n x

theorem Function.Semiconj.mapsTo_ptsOfPeriod {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β} (h : Function.Semiconj g fa fb) (n : ℕ) : Set.MapsTo g (Function.ptsOfPeriod fa n) (Function.ptsOfPeriod fb n)

theorem Function.bijOn_ptsOfPeriod {α : Type u_1} (f : α → α) {n : ℕ} (hn : 0 < n) : Set.BijOn f (Function.ptsOfPeriod f n) (Function.ptsOfPeriod f n)

theorem Function.directed_ptsOfPeriod_pNat {α : Type u_1} (f : α → α) : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (n : ℕ+) => Function.ptsOfPeriod f ↑n

def Function.periodicPts {α : Type u_1} (f : α → α) : Set α

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

Equations

• Function.periodicPts f = {x : α | ∃ n > 0, Function.IsPeriodicPt f n x}

theorem Function.mk_mem_periodicPts {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) : x ∈ Function.periodicPts f

theorem Function.mem_periodicPts {α : Type u_1} {f : α → α} {x : α} : x ∈ Function.periodicPts f ↔ ∃ n > 0, Function.IsPeriodicPt f n x

theorem Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate {α : Type u_1} {f : α → α} {x : α} {m : ℕ} {n : ℕ} (hx : x ∈ Function.periodicPts f) (hm : Function.IsPeriodicPt f m (f^[n] x)) : Function.IsPeriodicPt f m x

theorem Function.bUnion_ptsOfPeriod {α : Type u_1} (f : α → α) : ⋃ (n : ℕ), ⋃ (_ : n > 0), Function.ptsOfPeriod f n = Function.periodicPts f

theorem Function.iUnion_pNat_ptsOfPeriod {α : Type u_1} (f : α → α) : ⋃ (n : ℕ+), Function.ptsOfPeriod f ↑n = Function.periodicPts f

theorem Function.bijOn_periodicPts {α : Type u_1} (f : α → α) : Set.BijOn f (Function.periodicPts f) (Function.periodicPts f)

theorem Function.Semiconj.mapsTo_periodicPts {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β} (h : Function.Semiconj g fa fb) : Set.MapsTo g (Function.periodicPts fa) (Function.periodicPts 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

• Function.minimalPeriod f x = if h : x ∈ Function.periodicPts f then Nat.find h else 0

theorem Function.isPeriodicPt_minimalPeriod {α : Type u_1} (f : α → α) (x : α) : Function.IsPeriodicPt f (Function.minimalPeriod f x) x

@[simp]

theorem Function.iterate_minimalPeriod {α : Type u_1} {f : α → α} {x : α} : f^[Function.minimalPeriod f x] x = x

@[simp]

theorem Function.iterate_add_minimalPeriod_eq {α : Type u_1} {f : α → α} {x : α} {n : ℕ} : f^[n + Function.minimalPeriod f x] x = f^[n] x

@[simp]

theorem Function.iterate_mod_minimalPeriod_eq {α : Type u_1} {f : α → α} {x : α} {n : ℕ} : f^[n % Function.minimalPeriod f x] x = f^[n] x

theorem Function.minimalPeriod_pos_of_mem_periodicPts {α : Type u_1} {f : α → α} {x : α} (hx : x ∈ Function.periodicPts f) : 0 < Function.minimalPeriod f x

theorem Function.minimalPeriod_eq_zero_of_nmem_periodicPts {α : Type u_1} {f : α → α} {x : α} (hx : x ∉ Function.periodicPts f) : Function.minimalPeriod f x = 0

theorem Function.IsPeriodicPt.minimalPeriod_pos {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) : 0 < Function.minimalPeriod f x

theorem Function.minimalPeriod_pos_iff_mem_periodicPts {α : Type u_1} {f : α → α} {x : α} : 0 < Function.minimalPeriod f x ↔ x ∈ Function.periodicPts f

theorem Function.minimalPeriod_eq_zero_iff_nmem_periodicPts {α : Type u_1} {f : α → α} {x : α} : Function.minimalPeriod f x = 0 ↔ x ∉ Function.periodicPts f

theorem Function.IsPeriodicPt.minimalPeriod_le {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hn : 0 < n) (hx : Function.IsPeriodicPt f n x) : Function.minimalPeriod f x ≤ n

theorem Function.minimalPeriod_apply_iterate {α : Type u_1} {f : α → α} {x : α} (hx : x ∈ Function.periodicPts f) (n : ℕ) : Function.minimalPeriod f (f^[n] x) = Function.minimalPeriod f x

theorem Function.minimalPeriod_apply {α : Type u_1} {f : α → α} {x : α} (hx : x ∈ Function.periodicPts f) : Function.minimalPeriod f (f x) = Function.minimalPeriod f x

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.iterate_injOn_Iio_minimalPeriod {α : Type u_1} {f : α → α} {x : α} : Set.InjOn (fun (x_1 : ℕ) => f^[x_1] x) (Set.Iio (Function.minimalPeriod f x))

theorem Function.iterate_eq_iterate_iff_of_lt_minimalPeriod {α : 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

@[simp]

theorem Function.minimalPeriod_id {α : Type u_1} {x : α} : Function.minimalPeriod id x = 1

theorem Function.minimalPeriod_eq_one_iff_isFixedPt {α : Type u_1} {f : α → α} {x : α} : Function.minimalPeriod f x = 1 ↔ Function.IsFixedPt f x

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 : ℕ} : n ≠ 0 → n < Function.minimalPeriod f x → ¬Function.IsPeriodicPt f n x

theorem Function.IsPeriodicPt.minimalPeriod_dvd {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (hx : Function.IsPeriodicPt f n x) : Function.minimalPeriod f x ∣ n

theorem Function.isPeriodicPt_iff_minimalPeriod_dvd {α : Type u_1} {f : α → α} {x : α} {n : ℕ} : Function.IsPeriodicPt f n x ↔ Function.minimalPeriod f x ∣ n

theorem Function.minimalPeriod_eq_minimalPeriod_iff {α : Type u_1} {β : Type u_2} {f : α → α} {x : α} {g : β → β} {y : β} : Function.minimalPeriod f x = Function.minimalPeriod g y ↔ ∀ (n : ℕ), Function.IsPeriodicPt f n x ↔ Function.IsPeriodicPt g n 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) : Function.minimalPeriod f x = p

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) : Function.minimalPeriod f x = p ^ (k + 1)

theorem Function.Commute.minimalPeriod_of_comp_dvd_lcm {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : Function.Commute f g) : Function.minimalPeriod (f ∘ g) x ∣ (Function.minimalPeriod f x).lcm (Function.minimalPeriod g x)

theorem Function.Commute.minimalPeriod_of_comp_dvd_mul {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : Function.Commute f g) : Function.minimalPeriod (f ∘ g) x ∣ Function.minimalPeriod f x * Function.minimalPeriod g x

theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : Function.Commute f g) (hco : (Function.minimalPeriod f x).Coprime (Function.minimalPeriod g x)) : Function.minimalPeriod (f ∘ g) x = Function.minimalPeriod f x * Function.minimalPeriod g x

theorem Function.minimalPeriod_iterate_eq_div_gcd {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (h : n ≠ 0) : Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n

theorem Function.minimalPeriod_iterate_eq_div_gcd' {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (h : x ∈ Function.periodicPts f) : Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n

def Function.periodicOrbit {α : Type u_1} (f : α → α) (x : α) : Cycle α

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.periodicOrbit f x = ↑(List.map (fun (n : ℕ) => f^[n] x) (List.range (Function.minimalPeriod f x)))

theorem Function.periodicOrbit_def {α : Type u_1} (f : α → α) (x : α) : Function.periodicOrbit f x = ↑(List.map (fun (n : ℕ) => f^[n] x) (List.range (Function.minimalPeriod f x)))

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

theorem Function.periodicOrbit_eq_cycle_map {α : Type u_1} (f : α → α) (x : α) : Function.periodicOrbit f x = Cycle.map (fun (n : ℕ) => f^[n] x) ↑(List.range (Function.minimalPeriod f x))

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

@[simp]

theorem Function.periodicOrbit_length {α : Type u_1} {f : α → α} {x : α} : (Function.periodicOrbit f x).length = Function.minimalPeriod f x

@[simp]

theorem Function.periodicOrbit_eq_nil_iff_not_periodic_pt {α : Type u_1} {f : α → α} {x : α} : Function.periodicOrbit f x = Cycle.nil ↔ x ∉ Function.periodicPts f

theorem Function.periodicOrbit_eq_nil_of_not_periodic_pt {α : Type u_1} {f : α → α} {x : α} (h : x ∉ Function.periodicPts f) : Function.periodicOrbit f x = Cycle.nil

@[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 : ℕ) : f^[n] x ∈ Function.periodicOrbit f x

@[simp]

theorem Function.self_mem_periodicOrbit {α : Type u_1} {f : α → α} {x : α} (hx : x ∈ Function.periodicPts f) : x ∈ Function.periodicOrbit f x

theorem Function.nodup_periodicOrbit {α : Type u_1} {f : α → α} {x : α} : (Function.periodicOrbit f x).Nodup

theorem Function.periodicOrbit_apply_iterate_eq {α : Type u_1} {f : α → α} {x : α} (hx : x ∈ Function.periodicPts f) (n : ℕ) : Function.periodicOrbit f (f^[n] x) = Function.periodicOrbit f x

theorem Function.periodicOrbit_apply_eq {α : Type u_1} {f : α → α} {x : α} (hx : x ∈ Function.periodicPts f) : Function.periodicOrbit f (f x) = Function.periodicOrbit f x

theorem Function.periodicOrbit_chain {α : Type u_1} (r : α → α → Prop) {f : α → α} {x : α} : Cycle.Chain r (Function.periodicOrbit f x) ↔ ∀ n < Function.minimalPeriod f x, r (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)

@[simp]

theorem Function.isFixedPt_prod_map {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} (x : α × β) : Function.IsFixedPt (Prod.map f g) x ↔ Function.IsFixedPt f x.1 ∧ Function.IsFixedPt g x.2

@[simp]

theorem Function.isPeriodicPt_prod_map {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {n : ℕ} (x : α × β) : Function.IsPeriodicPt (Prod.map f g) n x ↔ Function.IsPeriodicPt f n x.1 ∧ Function.IsPeriodicPt g n x.2

theorem Function.minimalPeriod_prod_map {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (x : α × β) : Function.minimalPeriod (Prod.map f g) x = (Function.minimalPeriod f x.1).lcm (Function.minimalPeriod g x.2)

theorem Function.minimalPeriod_fst_dvd {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} : Function.minimalPeriod f x.1 ∣ Function.minimalPeriod (Prod.map f g) x

theorem Function.minimalPeriod_snd_dvd {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} : Function.minimalPeriod g x.2 ∣ Function.minimalPeriod (Prod.map f g) x

noncomputable def AddAction.period {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (m : M) (a : α) : ℕ

The period of an additive action of g on a is the smallest positive n such that (n • g) +ᵥ a = a, or 0 if such an n does not exist.

Equations

• AddAction.period m a = Function.minimalPeriod (fun (x : α) => m +ᵥ x) a

noncomputable def MulAction.period {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (m : M) (a : α) : ℕ

The period of a multiplicative action of g on a is the smallest positive n such that g ^ n • a = a, or 0 if such an n does not exist.

Equations

• MulAction.period m a = Function.minimalPeriod (fun (x : α) => m • x) a

theorem AddAction.period_eq_minimalPeriod {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} : AddAction.period m a = Function.minimalPeriod (fun (x : α) => m +ᵥ x) a

AddAction.period m a is definitionally equal to Function.minimalPeriod (m +ᵥ ·) a

theorem MulAction.period_eq_minimalPeriod {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} : MulAction.period m a = Function.minimalPeriod (fun (x : α) => m • x) a

MulAction.period m a is definitionally equal to Function.minimalPeriod (m • ·) a.

@[simp]

theorem AddAction.nsmul_period_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (m : M) (a : α) : AddAction.period m a • m +ᵥ a = a

(period m a) • m fixes a.

@[simp]

theorem MulAction.pow_period_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (m : M) (a : α) : m ^ MulAction.period m a • a = a

m ^ (period m a) fixes a.

theorem AddAction.isPeriodicPt_vadd_iff {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} {n : ℕ} : Function.IsPeriodicPt (fun (x : α) => m +ᵥ x) n a ↔ n • m +ᵥ a = a

theorem MulAction.isPeriodicPt_smul_iff {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} {n : ℕ} : Function.IsPeriodicPt (fun (x : α) => m • x) n a ↔ m ^ n • a = a

Multiples of MulAction.period

It is easy to convince oneself that if g ^ n • a = a (resp. (n • g) +ᵥ a = a), then n must be a multiple of period g a.

This also holds for negative powers/multiples.

theorem AddAction.nsmul_vadd_eq_iff_period_dvd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {n : ℕ} {m : M} {a : α} : n • m +ᵥ a = a ↔ AddAction.period m a ∣ n

theorem MulAction.pow_smul_eq_iff_period_dvd {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {n : ℕ} {m : M} {a : α} : m ^ n • a = a ↔ MulAction.period m a ∣ n

theorem AddAction.zsmul_vadd_eq_iff_period_dvd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] {j : ℤ} {g : G} {a : α} : j • g +ᵥ a = a ↔ ↑(AddAction.period g a) ∣ j

theorem MulAction.zpow_smul_eq_iff_period_dvd {α : Type v} {G : Type u} [Group G] [MulAction G α] {j : ℤ} {g : G} {a : α} : g ^ j • a = a ↔ ↑(MulAction.period g a) ∣ j

@[simp]

theorem AddAction.nsmul_mod_period_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (n : ℕ) {m : M} {a : α} : (n % AddAction.period m a) • m +ᵥ a = n • m +ᵥ a

@[simp]

theorem MulAction.pow_mod_period_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (n : ℕ) {m : M} {a : α} : m ^ (n % MulAction.period m a) • a = m ^ n • a

@[simp]

theorem AddAction.zsmul_mod_period_vadd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (j : ℤ) {g : G} {a : α} : (j % ↑(AddAction.period g a)) • g +ᵥ a = j • g +ᵥ a

@[simp]

theorem MulAction.zpow_mod_period_smul {α : Type v} {G : Type u} [Group G] [MulAction G α] (j : ℤ) {g : G} {a : α} : g ^ (j % ↑(MulAction.period g a)) • a = g ^ j • a

@[simp]

theorem AddAction.nsmul_add_period_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (n : ℕ) (m : M) (a : α) : (n + AddAction.period m a) • m +ᵥ a = n • m +ᵥ a

@[simp]

theorem MulAction.pow_add_period_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (n : ℕ) (m : M) (a : α) : m ^ (n + MulAction.period m a) • a = m ^ n • a

@[simp]

theorem AddAction.nsmul_period_add_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (n : ℕ) (m : M) (a : α) : (AddAction.period m a + n) • m +ᵥ a = n • m +ᵥ a

@[simp]

theorem MulAction.pow_period_add_smul {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (n : ℕ) (m : M) (a : α) : m ^ (MulAction.period m a + n) • a = m ^ n • a

@[simp]

theorem AddAction.zsmul_add_period_vadd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (i : ℤ) (g : G) (a : α) : (i + ↑(AddAction.period g a)) • g +ᵥ a = i • g +ᵥ a

@[simp]

theorem MulAction.zpow_add_period_smul {α : Type v} {G : Type u} [Group G] [MulAction G α] (i : ℤ) (g : G) (a : α) : g ^ (i + ↑(MulAction.period g a)) • a = g ^ i • a

@[simp]

theorem AddAction.zsmul_period_add_vadd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (i : ℤ) (g : G) (a : α) : (↑(AddAction.period g a) + i) • g +ᵥ a = i • g +ᵥ a

@[simp]

theorem MulAction.zpow_period_add_smul {α : Type v} {G : Type u} [Group G] [MulAction G α] (i : ℤ) (g : G) (a : α) : g ^ (↑(MulAction.period g a) + i) • a = g ^ i • a

theorem AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] {a : G} {b : α} {n : ℕ} : n • a +ᵥ b = b ↔ Function.minimalPeriod (fun (x : α) => a +ᵥ x) b ∣ n

theorem MulAction.pow_smul_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [Group G] [MulAction G α] {a : G} {b : α} {n : ℕ} : a ^ n • b = b ↔ Function.minimalPeriod (fun (x : α) => a • x) b ∣ n

theorem AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] {a : G} {b : α} {n : ℤ} : n • a +ᵥ b = b ↔ ↑(Function.minimalPeriod (fun (x : α) => a +ᵥ x) b) ∣ n

theorem MulAction.zpow_smul_eq_iff_minimalPeriod_dvd {α : Type v} {G : Type u} [Group G] [MulAction G α] {a : G} {b : α} {n : ℤ} : a ^ n • b = b ↔ ↑(Function.minimalPeriod (fun (x : α) => a • x) b) ∣ n

@[simp]

theorem AddAction.nsmul_vadd_mod_minimalPeriod {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (a : G) (b : α) (n : ℕ) : (n % Function.minimalPeriod (fun (x : α) => a +ᵥ x) b) • a +ᵥ b = n • a +ᵥ b

@[simp]

theorem MulAction.pow_smul_mod_minimalPeriod {α : Type v} {G : Type u} [Group G] [MulAction G α] (a : G) (b : α) (n : ℕ) : a ^ (n % Function.minimalPeriod (fun (x : α) => a • x) b) • b = a ^ n • b

@[simp]

theorem AddAction.zsmul_vadd_mod_minimalPeriod {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (a : G) (b : α) (n : ℤ) : (n % ↑(Function.minimalPeriod (fun (x : α) => a +ᵥ x) b)) • a +ᵥ b = n • a +ᵥ b

@[simp]

theorem MulAction.zpow_smul_mod_minimalPeriod {α : Type v} {G : Type u} [Group G] [MulAction G α] (a : G) (b : α) (n : ℤ) : a ^ (n % ↑(Function.minimalPeriod (fun (x : α) => a • x) b)) • b = a ^ n • b