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 : IsFixedPt f x) (n : ℕ) : 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 : α) : IsPeriodicPt id n x

For the identity map, all points are periodic.

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

Any point is a periodic point of period 0.

theorem Function.IsPeriodicPt.of_subsingleton {α : Type u_1} [Subsingleton α] (f : α → α) (n : ℕ) (x : α) : IsPeriodicPt f n x

@[implicit_reducible]

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

Equations

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

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

theorem Function.IsPeriodicPt.map {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {x : α} {n : ℕ} (hx : IsPeriodicPt fa n x) {g : α → β} (hg : Semiconj g fa fb) : IsPeriodicPt fb n (g x)

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

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

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

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

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

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

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

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

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

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

theorem Function.IsPeriodicPt.comp {α : Type u_1} {f : α → α} {x : α} {n : ℕ} {g : α → α} (hco : Function.Commute f g) (hf : IsPeriodicPt f n x) (hg : IsPeriodicPt g n x) : IsPeriodicPt (f ∘ g) n x

theorem Function.IsPeriodicPt.comp_lcm {α : Type u_1} {f : α → α} {x : α} {m n : ℕ} {g : α → α} (hco : Function.Commute f g) (hf : IsPeriodicPt f m x) (hg : IsPeriodicPt g n x) : 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 : IsPeriodicPt (f ∘ g) n x) (hg : IsPeriodicPt g n x) : IsPeriodicPt f n x

theorem Function.IsPeriodicPt.iterate_mod_apply {α : Type u_1} {f : α → α} {x : α} {n : ℕ} (h : IsPeriodicPt f n x) (m : ℕ) : f^[m % n] x = f^[m] x

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

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

theorem Function.IsPeriodicPt.eq_of_apply_eq_same {α : Type u_1} {f : α → α} {x y : α} {n : ℕ} (hx : IsPeriodicPt f n x) (hy : 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 : IsPeriodicPt f m x) (hy : 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 ∈ ptsOfPeriod f n ↔ IsPeriodicPt f n x

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

theorem Function.bijOn_ptsOfPeriod {α : Type u_1} (f : α → α) {n : ℕ} (hn : 0 < n) : Set.BijOn f (ptsOfPeriod f n) (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 : IsPeriodicPt f n x) : x ∈ periodicPts f

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

theorem Function.periodicPts_subset_range {α : Type u_1} {f : α → α} : periodicPts f ⊆ Set.range f

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

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

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

theorem Function.Semiconj.mapsTo_periodicPts {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β} (h : Semiconj g fa fb) : Set.MapsTo g (periodicPts fa) (periodicPts fb)

noncomputable 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 : α) : IsPeriodicPt f (minimalPeriod f x) x

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

theorem Function.iterate_eq_iterate_iff_of_lt_minimalPeriod {α : Type u_1} {f : α → α} {x : α} {m n : ℕ} (hm : m < minimalPeriod f x) (hn : n < minimalPeriod f x) : f^[m] x = f^[n] x ↔ m = n

@[simp]

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

@[simp]

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

theorem Function.minimalPeriod_eq_one_of_subsingleton {α : Type u_1} {f : α → α} {x : α} [Subsingleton α] : minimalPeriod f x = 1

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

theorem Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod {α : Type u_1} {f : α → α} {x : α} {n : ℕ} : n ≠ 0 → n < minimalPeriod f x → ¬IsPeriodicPt f n x

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

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

theorem Function.minimalPeriod_eq_minimalPeriod_iff {α : Type u_1} {β : Type u_2} {f : α → α} {x : α} {g : β → β} {y : β} : minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y

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

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

theorem Function.periodicOrbit_chain {α : Type u_1} (r : α → α → Prop) {f : α → α} {x : α} : Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

theorem Function.periodicOrbit_chain' {α : Type u_1} (r : α → α → Prop) {f : α → α} {x : α} (hx : x ∈ periodicPts f) : Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)

@[simp]

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

theorem Function.IsFixedPt.prodMap {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {a : α} {b : β} (ha : IsFixedPt f a) (hb : IsFixedPt g b) : IsFixedPt (Prod.map f g) (a, b)

@[simp]

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

theorem Function.IsPeriodicPt.prodMap {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {a : α} {b : β} {n : ℕ} (ha : IsPeriodicPt f n a) (hb : IsPeriodicPt g n b) : IsPeriodicPt (Prod.map f g) n (a, b)

@[simp]

theorem Function.isFixedPt_piMap {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} : IsFixedPt (Pi.map f) x ↔ ∀ (i : ι), IsFixedPt (f i) (x i)

theorem Function.IsFixedPt.piMap {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} (h : ∀ (i : ι), IsFixedPt (f i) (x i)) : IsFixedPt (Pi.map f) x

@[simp]

theorem Function.isPeriodicPt_piMap {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} {n : ℕ} : IsPeriodicPt (Pi.map f) n x ↔ ∀ (i : ι), IsPeriodicPt (f i) n (x i)

theorem Function.IsPeriodicPt.piMap {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} {n : ℕ} (h : ∀ (i : ι), IsPeriodicPt (f i) n (x i)) : IsPeriodicPt (Pi.map f) n x

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

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

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

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

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

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

@[simp]

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

m ^ (period m a) fixes a.

@[simp]

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

(period m a) • m fixes 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

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

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 MulAction.pow_smul_eq_iff_period_dvd {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {n : ℕ} {m : M} {a : α} : m ^ n • a = a ↔ period m a ∣ n

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 ↔ period m a ∣ n

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 ↔ ↑(period g a) ∣ j

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 ↔ ↑(period g a) ∣ j

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem AddAction.nsmul_add_period_vadd {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (n : ℕ) (m : M) (a : α) : (n + period m a) • 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 ^ (period m a + n) • a = m ^ n • a

@[simp]

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

@[simp]

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

@[simp]

theorem AddAction.zsmul_add_period_vadd {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (i : ℤ) (g : G) (a : α) : (i + ↑(period g a)) • 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 ^ (↑(period g a) + i) • a = g ^ i • a

@[simp]

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

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.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.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

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

@[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.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.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

@[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