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 #

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.

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 : α) :

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

Instances For

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.instDecidableIsPeriodicPt {α : Type u_1} [DecidableEq α] {f : α → α} {n : ℕ} {x : α} :

Decidable (Function.IsPeriodicPt 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) :

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) (Nat.lcm m 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 (Nat.gcd m 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}

Instances For

@[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 (x x_1 : Set α) => 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

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

Instances For

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

Instances For

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 ∣ Nat.lcm (Function.minimalPeriod f x) (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 : Nat.Coprime (Function.minimalPeriod f x) (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 / Nat.gcd (Function.minimalPeriod f x) 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 / Nat.gcd (Function.minimalPeriod f x) n

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

Function.periodicOrbit f x = ↑(List.map (fun (n : ℕ) => f ^[n] x) (List.range (Function.minimalPeriod f x)))

Instances For

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 : α} :

Cycle.length (Function.periodicOrbit f x) = 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 : α} :

Cycle.Nodup (Function.periodicOrbit f x)

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.iterate_prod_map {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (n : ℕ) :

(Prod.map f g)^[n] = Prod.map f^[n] g^[n]

@[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 = Nat.lcm (Function.minimalPeriod f x.1) (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

theorem AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] {a : α} {b : β} {n : ℕ} :

n • a +ᵥ b = b ↔ Function.minimalPeriod (fun (x : β) => a +ᵥ x) b ∣ n

theorem MulAction.pow_smul_eq_iff_minimalPeriod_dvd {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] {a : α} {b : β} {n : ℕ} :

a ^ n • b = b ↔ Function.minimalPeriod (fun (x : β) => a • x) b ∣ n

theorem AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] {a : α} {b : β} {n : ℤ} :

n • a +ᵥ b = b ↔ ↑(Function.minimalPeriod (fun (x : β) => a +ᵥ x) b) ∣ n

theorem MulAction.zpow_smul_eq_iff_minimalPeriod_dvd {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] {a : α} {b : β} {n : ℤ} :

a ^ n • b = b ↔ ↑(Function.minimalPeriod (fun (x : β) => a • x) b) ∣ n

@[simp]

theorem AddAction.nsmul_vadd_mod_minimalPeriod {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (a : α) (b : β) (n : ℕ) :

(n % Function.minimalPeriod (fun (x : β) => a +ᵥ x) b) • a +ᵥ b = n • a +ᵥ b

@[simp]

theorem MulAction.pow_smul_mod_minimalPeriod {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (a : α) (b : β) (n : ℕ) :

a ^ (n % Function.minimalPeriod (fun (x : β) => a • x) b) • b = a ^ n • b

@[simp]

theorem AddAction.zsmul_vadd_mod_minimalPeriod {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (a : α) (b : β) (n : ℤ) :

(n % ↑(Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) • a +ᵥ b = n • a +ᵥ b

@[simp]

theorem MulAction.zpow_smul_mod_minimalPeriod {α : Type u_1} {β : Type u_2} [Group α] [MulAction α β] (a : α) (b : β) (n : ℤ) :

a ^ (n % ↑(Function.minimalPeriod (fun (x : β) => a • x) b)) • b = a ^ n • b