Mathlib.Dynamics.PeriodicPts.Defs

Function.IsPeriodicPt definition

(f : α → α) (n : ℕ) (x : α)

Full source

/-- 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. -/
def IsPeriodicPt (f : α → α) (n : ℕ) (x : α) :=
  IsFixedPt f^[n] x

Periodic point of a function

Informal description

A point $ x $ in a type $ \alpha $ is called a periodic point of a function $ f : \alpha \to \alpha $ with period $ n $ if the $ n $-th iterate of $ f $ applied to $ x $ equals $ x $, i.e., $ f^[n](x) = x $. Note that $ n $ is allowed to be zero in this definition.

Function.IsFixedPt.isPeriodicPt theorem

(hf : IsFixedPt f x) (n : ℕ) : IsPeriodicPt f n x

Full source

/-- A fixed point of `f` is a periodic point of `f` of any prescribed period. -/
theorem IsFixedPt.isPeriodicPt (hf : IsFixedPt f x) (n : ℕ) : IsPeriodicPt f n x :=
  hf.iterate n

Fixed Points are Periodic Points of Any Period

Informal description

If $x$ is a fixed point of a function $f : \alpha \to \alpha$ (i.e., $f(x) = x$), then for any natural number $n$, $x$ is a periodic point of $f$ with period $n$ (i.e., $f^[n](x) = x$).

Function.is_periodic_id theorem

(n : ℕ) (x : α) : IsPeriodicPt id n x

Full source

/-- For the identity map, all points are periodic. -/
theorem is_periodic_id (n : ℕ) (x : α) : IsPeriodicPt id n x :=
  (isFixedPt_id x).isPeriodicPt n

Identity Function Has All Points as Periodic Points

Informal description

For any natural number $n$ and any point $x$ in a type $\alpha$, the identity function $\mathrm{id}$ satisfies $\mathrm{id}^n(x) = x$, meaning $x$ is a periodic point of $\mathrm{id}$ with period $n$.

Function.isPeriodicPt_zero theorem

(f : α → α) (x : α) : IsPeriodicPt f 0 x

Full source

/-- Any point is a periodic point of period `0`. -/
theorem isPeriodicPt_zero (f : α → α) (x : α) : IsPeriodicPt f 0 x :=
  isFixedPt_id x

Every Point is Periodic with Period Zero

Informal description

For any function $f : \alpha \to \alpha$ and any point $x \in \alpha$, $x$ is a periodic point of $f$ with period $0$, i.e., $f^[0](x) = x$.

Function.IsPeriodicPt.instDecidableOfDecidableEq instance

[DecidableEq α] {f : α → α} {n : ℕ} {x : α} : Decidable (IsPeriodicPt f n x)

Full source

instance [DecidableEq α] {f : α → α} {n : ℕ} {x : α} : Decidable (IsPeriodicPt f n x) :=
  IsFixedPt.decidable

Decidability of Periodic Points for Functions with Decidable Equality

Informal description

For any type $\alpha$ with decidable equality, a function $f : \alpha \to \alpha$, a natural number $n$, and a point $x \in \alpha$, it is decidable whether $x$ is a periodic point of $f$ with period $n$ (i.e., whether $f^[n](x) = x$).

Function.IsPeriodicPt.isFixedPt theorem

(hf : IsPeriodicPt f n x) : IsFixedPt f^[n] x

Full source

protected theorem isFixedPt (hf : IsPeriodicPt f n x) : IsFixedPt f^[n] x :=
  hf

Periodic Points are Fixed Points of Their Iterates

Informal description

If $x$ is a periodic point of a function $f : \alpha \to \alpha$ with period $n$, then $x$ is a fixed point of the $n$-th iterate of $f$, i.e., $f^[n](x) = x$.

Function.IsPeriodicPt.map theorem

(hx : IsPeriodicPt fa n x) {g : α → β} (hg : Semiconj g fa fb) : IsPeriodicPt fb n (g x)

Full source

protected theorem map (hx : IsPeriodicPt fa n x) {g : α → β} (hg : Semiconj g fa fb) :
    IsPeriodicPt fb n (g x) :=
  IsFixedPt.map hx (hg.iterate_right n)

Periodic Points are Preserved under Semiconjugacy

Informal description

Let $x$ be a periodic point of a function $f_a \colon \alpha \to \alpha$ with period $n$, i.e., $f_a^{[n]}(x) = x$. If a function $g \colon \alpha \to \beta$ semiconjugates $f_a$ to $f_b \colon \beta \to \beta$ (i.e., $g \circ f_a = f_b \circ g$), then $g(x)$ is a periodic point of $f_b$ with the same period $n$.

Function.IsPeriodicPt.apply_iterate theorem

(hx : IsPeriodicPt f n x) (m : ℕ) : IsPeriodicPt f n (f^[m] x)

Full source

theorem apply_iterate (hx : IsPeriodicPt f n x) (m : ℕ) : IsPeriodicPt f n (f^[m] x) :=
  hx.map <| Commute.iterate_self f m

Iterates of Periodic Points Remain Periodic with Same Period

Informal description

Let $x$ be a periodic point of a function $f : \alpha \to \alpha$ with period $n$, i.e., $f^{[n]}(x) = x$. Then for any natural number $m$, the $m$-th iterate $f^{[m]}(x)$ is also a periodic point of $f$ with the same period $n$.

Function.IsPeriodicPt.apply theorem

(hx : IsPeriodicPt f n x) : IsPeriodicPt f n (f x)

Full source

protected theorem apply (hx : IsPeriodicPt f n x) : IsPeriodicPt f n (f x) :=
  hx.apply_iterate 1

Image of Periodic Point is Periodic with Same Period

Informal description

Let $x$ be a periodic point of a function $f \colon \alpha \to \alpha$ with period $n$, i.e., $f^{[n]}(x) = x$. Then the image $f(x)$ is also a periodic point of $f$ with the same period $n$.

Function.IsPeriodicPt.add theorem

(hn : IsPeriodicPt f n x) (hm : IsPeriodicPt f m x) : IsPeriodicPt f (n + m) x

Full source

protected theorem add (hn : IsPeriodicPt f n x) (hm : IsPeriodicPt f m x) :
    IsPeriodicPt f (n + m) x := by
  rw [IsPeriodicPt, iterate_add]
  exact hn.comp hm

Sum of Periods Preserves Periodicity

Informal description

If $x$ is a periodic point of $f : \alpha \to \alpha$ with periods $n$ and $m$, then $x$ is also a periodic point of $f$ with period $n + m$. In other words, if $f^{[n]}(x) = x$ and $f^{[m]}(x) = x$, then $f^{[n + m]}(x) = x$.

Function.IsPeriodicPt.left_of_add theorem

(hn : IsPeriodicPt f (n + m) x) (hm : IsPeriodicPt f m x) : IsPeriodicPt f n x

Full source

theorem left_of_add (hn : IsPeriodicPt f (n + m) x) (hm : IsPeriodicPt f m x) :
    IsPeriodicPt f n x := by
  rw [IsPeriodicPt, iterate_add] at hn
  exact hn.left_of_comp hm

Periodicity Preservation Under Left Subtraction of Periods

Informal description

Let $f : \alpha \to \alpha$ be a function and $x \in \alpha$ a point. If $x$ is a periodic point of $f$ with period $n + m$ and also with period $m$, then $x$ is a periodic point of $f$ with period $n$. In other words, if $f^{[n+m]}(x) = x$ and $f^{[m]}(x) = x$, then $f^{[n]}(x) = x$.

Function.IsPeriodicPt.right_of_add theorem

(hn : IsPeriodicPt f (n + m) x) (hm : IsPeriodicPt f n x) : IsPeriodicPt f m x

Full source

theorem right_of_add (hn : IsPeriodicPt f (n + m) x) (hm : IsPeriodicPt f n x) :
    IsPeriodicPt f m x := by
  rw [add_comm] at hn
  exact hn.left_of_add hm

Periodicity Preservation Under Right Subtraction of Periods

Informal description

For a function $f \colon \alpha \to \alpha$ and a point $x \in \alpha$, if $x$ is a periodic point of $f$ with period $n + m$ and also with period $n$, then $x$ is a periodic point of $f$ with period $m$. In other words, if $f^{[n+m]}(x) = x$ and $f^{[n]}(x) = x$, then $f^{[m]}(x) = x$.

Function.IsPeriodicPt.sub theorem

(hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) : IsPeriodicPt f (m - n) x

Full source

protected theorem sub (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) :
    IsPeriodicPt f (m - n) x := by
  rcases le_total n m with h | h
  · refine left_of_add ?_ hn
    rwa [tsub_add_cancel_of_le h]
  · rw [tsub_eq_zero_iff_le.mpr h]
    apply isPeriodicPt_zero

Periodicity Preservation Under Subtraction of Periods

Informal description

For a function $f \colon \alpha \to \alpha$ and a point $x \in \alpha$, if $x$ is a periodic point of $f$ with period $m$ and also with period $n$, then $x$ is a periodic point of $f$ with period $m - n$. In other words, if $f^{[m]}(x) = x$ and $f^{[n]}(x) = x$, then $f^{[m - n]}(x) = x$.

Function.IsPeriodicPt.mul_const theorem

(hm : IsPeriodicPt f m x) (n : ℕ) : IsPeriodicPt f (m * n) x

Full source

protected theorem mul_const (hm : IsPeriodicPt f m x) (n : ℕ) : IsPeriodicPt f (m * n) x := by
  simp only [IsPeriodicPt, iterate_mul, hm.isFixedPt.iterate n]

Periodicity Preservation under Multiplication: $f^[m \cdot n](x) = x$ when $f^[m](x) = x$

Informal description

If $x$ is a periodic point of a function $f \colon \alpha \to \alpha$ with period $m$, then for any natural number $n$, $x$ is also a periodic point of $f$ with period $m \cdot n$. In other words, if $f^[m](x) = x$, then $f^[m \cdot n](x) = x$ for any $n \in \mathbb{N}$.

Function.IsPeriodicPt.const_mul theorem

(hm : IsPeriodicPt f m x) (n : ℕ) : IsPeriodicPt f (n * m) x

Full source

protected theorem const_mul (hm : IsPeriodicPt f m x) (n : ℕ) : IsPeriodicPt f (n * m) x := by
  simp only [mul_comm n, hm.mul_const n]

Periodicity Preservation under Commutative Multiplication: $f^[n \cdot m](x) = x$ when $f^[m](x) = x$

Informal description

If $x$ is a periodic point of a function $f \colon \alpha \to \alpha$ with period $m$, then for any natural number $n$, $x$ is also a periodic point of $f$ with period $n \cdot m$. In other words, if $f^[m](x) = x$, then $f^[n \cdot m](x) = x$ for any $n \in \mathbb{N}$.

Function.IsPeriodicPt.trans_dvd theorem

(hm : IsPeriodicPt f m x) {n : ℕ} (hn : m ∣ n) : IsPeriodicPt f n x

Full source

theorem trans_dvd (hm : IsPeriodicPt f m x) {n : ℕ} (hn : m ∣ n) : IsPeriodicPt f n x :=
  let ⟨k, hk⟩ := hn
  hk.symm ▸ hm.mul_const k

Periodicity Preservation Under Divisibility: $f^[n](x) = x$ when $m \mid n$ and $f^[m](x) = x$

Informal description

If $x$ is a periodic point of a function $f \colon \alpha \to \alpha$ with period $m$, and $m$ divides $n$, then $x$ is also a periodic point of $f$ with period $n$. In other words, if $f^[m](x) = x$ and $m \mid n$, then $f^[n](x) = x$.

Function.IsPeriodicPt.iterate theorem

(hf : IsPeriodicPt f n x) (m : ℕ) : IsPeriodicPt f^[m] n x

Full source

protected theorem iterate (hf : IsPeriodicPt f n x) (m : ℕ) : IsPeriodicPt f^[m] n x := by
  rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]
  exact hf.isFixedPt.iterate m

Periodicity Preservation Under Iteration: $x$ is periodic for $f^{[m]}$ with same period $n$

Informal description

If $x$ is a periodic point of a function $f \colon \alpha \to \alpha$ with period $n$, then for any natural number $m$, the point $x$ is also a periodic point of the $m$-th iterate $f^{[m]}$ with the same period $n$.

Function.IsPeriodicPt.comp theorem

{g : α → α} (hco : Commute f g) (hf : IsPeriodicPt f n x) (hg : IsPeriodicPt g n x) : IsPeriodicPt (f ∘ g) n x

Full source

theorem comp {g : α → α} (hco : Commute f g) (hf : IsPeriodicPt f n x) (hg : IsPeriodicPt g n x) :
    IsPeriodicPt (f ∘ g) n x := by
  rw [IsPeriodicPt, hco.comp_iterate]
  exact IsFixedPt.comp hf hg

Periodicity Preservation Under Composition of Commuting Functions: $(f \circ g)^[n](x) = x$

Informal description

Let $f, g : \alpha \to \alpha$ be commuting functions (i.e., $f \circ g = g \circ f$). If $x$ is a periodic point of both $f$ and $g$ with the same period $n$, then $x$ is also a periodic point of the composition $f \circ g$ with period $n$. In other words, if $f^[n](x) = x$ and $g^[n](x) = x$, then $(f \circ g)^[n](x) = x$.

Function.IsPeriodicPt.comp_lcm theorem

 {g : α → α} (hco : Commute f g) (hf : IsPeriodicPt f m x) (hg : IsPeriodicPt g n x) :
  IsPeriodicPt (f ∘ g) (Nat.lcm m n) x

Full source

theorem comp_lcm {g : α → α} (hco : Commute f g) (hf : IsPeriodicPt f m x)
    (hg : IsPeriodicPt g n x) : IsPeriodicPt (f ∘ g) (Nat.lcm m n) x :=
  (hf.trans_dvd <| Nat.dvd_lcm_left _ _).comp hco (hg.trans_dvd <| Nat.dvd_lcm_right _ _)

Periodicity of Composition: $(f \circ g)^[\text{lcm}(m, n)](x) = x$ for Commuting Functions

Informal description

Let $f, g \colon \alpha \to \alpha$ be commuting functions (i.e., $f \circ g = g \circ f$). If $x$ is a periodic point of $f$ with period $m$ and a periodic point of $g$ with period $n$, then $x$ is a periodic point of the composition $f \circ g$ with period equal to the least common multiple of $m$ and $n$. In other words, if $f^[m](x) = x$ and $g^[n](x) = x$, then $(f \circ g)^[\text{lcm}(m, n)](x) = x$.

Function.IsPeriodicPt.left_of_comp theorem

{g : α → α} (hco : Commute f g) (hfg : IsPeriodicPt (f ∘ g) n x) (hg : IsPeriodicPt g n x) : IsPeriodicPt f n x

Full source

theorem left_of_comp {g : α → α} (hco : Commute f g) (hfg : IsPeriodicPt (f ∘ g) n x)
    (hg : IsPeriodicPt g n x) : IsPeriodicPt f n x := by
  rw [IsPeriodicPt, hco.comp_iterate] at hfg
  exact hfg.left_of_comp hg

Periodicity of Commuting Functions: If $x$ is periodic for $f \circ g$ and $g$, then it is periodic for $f$ with the same period.

Informal description

Let $f, g : \alpha \to \alpha$ be commuting functions (i.e., $f \circ g = g \circ f$). If $x$ is a periodic point of the composition $f \circ g$ with period $n$, and $x$ is also a periodic point of $g$ with the same period $n$, then $x$ is a periodic point of $f$ with period $n$.

Function.IsPeriodicPt.iterate_mod_apply theorem

(h : IsPeriodicPt f n x) (m : ℕ) : f^[m % n] x = f^[m] x

Full source

theorem iterate_mod_apply (h : IsPeriodicPt f n x) (m : ℕ) : f^[m % n] x = f^[m] x := by
  conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

Iteration Modulo Period: $f^[m](x) = f^[m \bmod n](x)$ for Periodic Points

Informal description

Let $f : \alpha \to \alpha$ be a function and $x \in \alpha$ be a periodic point of $f$ with period $n$, i.e., $f^[n](x) = x$. Then for any natural number $m$, the $m$-th iterate of $f$ applied to $x$ equals the $(m \bmod n)$-th iterate of $f$ applied to $x$, i.e., $f^[m](x) = f^[m \bmod n](x)$.

Function.IsPeriodicPt.mod theorem

(hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) : IsPeriodicPt f (m % n) x

Full source

protected theorem mod (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) :
    IsPeriodicPt f (m % n) x :=
  (hn.iterate_mod_apply m).trans hm

Periodicity Preservation Under Modulo Operation

Informal description

Let $f : \alpha \to \alpha$ be a function and $x \in \alpha$ be a periodic point of $f$ with periods $m$ and $n$, i.e., $f^[m](x) = x$ and $f^[n](x) = x$. Then $x$ is also a periodic point of $f$ with period $m \bmod n$.

Function.IsPeriodicPt.gcd theorem

(hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) : IsPeriodicPt f (m.gcd n) x

Full source

protected theorem gcd (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) :
    IsPeriodicPt f (m.gcd n) x := by
  revert hm hn
  refine Nat.gcd.induction m n (fun n _ hn => ?_) fun m n _ ih hm hn => ?_
  · rwa [Nat.gcd_zero_left]
  · rw [Nat.gcd_rec]
    exact ih (hn.mod hm) hm

Periodicity Preservation Under GCD Operation

Informal description

Let $f : \alpha \to \alpha$ be a function and $x \in \alpha$ be a periodic point of $f$ with periods $m$ and $n$, i.e., $f^[m](x) = x$ and $f^[n](x) = x$. Then $x$ is also a periodic point of $f$ with period $\gcd(m, n)$.

Function.ptsOfPeriod definition

(f : α → α) (n : ℕ) : Set α

Full source

/-- The set of periodic points of a given (possibly non-minimal) period. -/
def ptsOfPeriod (f : α → α) (n : ℕ) : Set α :=
  { x : α | IsPeriodicPt f n x }

Set of periodic points with period $ n $

Informal description

The set of all points $ x $ in a type $ \alpha $ that are periodic points of a function $ f : \alpha \to \alpha $ with period $ n $, i.e., points satisfying $ f^[n](x) = x $. Here $ n $ is not required to be the minimal period of $ x $.

Function.mem_ptsOfPeriod theorem

: x ∈ ptsOfPeriod f n ↔ IsPeriodicPt f n x

Full source

@[simp]
theorem mem_ptsOfPeriod : x ∈ ptsOfPeriod f nx ∈ ptsOfPeriod f n ↔ IsPeriodicPt f n x :=
  Iff.rfl

Membership in Periodic Points Set Characterization

Informal description

A point $x$ belongs to the set of periodic points of $f$ with period $n$ if and only if $x$ is a periodic point of $f$ with period $n$, i.e., $f^n(x) = x$.

Function.Semiconj.mapsTo_ptsOfPeriod theorem

{g : α → β} (h : Semiconj g fa fb) (n : ℕ) : MapsTo g (ptsOfPeriod fa n) (ptsOfPeriod fb n)

Full source

theorem Semiconj.mapsTo_ptsOfPeriod {g : α → β} (h : Semiconj g fa fb) (n : ℕ) :
    MapsTo g (ptsOfPeriod fa n) (ptsOfPeriod fb n) :=
  (h.iterate_right n).mapsTo_fixedPoints

Semiconjugacy Preserves Periodic Points of Given Period

Informal description

Let $g \colon \alpha \to \beta$ be a function that semiconjugates $f_a \colon \alpha \to \alpha$ to $f_b \colon \beta \to \beta$, meaning $g \circ f_a = f_b \circ g$. Then for any natural number $n$, the function $g$ maps the set of periodic points of $f_a$ with period $n$ into the set of periodic points of $f_b$ with period $n$. In other words, if $x$ is a periodic point of $f_a$ with period $n$ (i.e., $f_a^{[n]}(x) = x$), then $g(x)$ is a periodic point of $f_b$ with the same period $n$ (i.e., $f_b^{[n]}(g(x)) = g(x)$).

Function.bijOn_ptsOfPeriod theorem

(f : α → α) {n : ℕ} (hn : 0 < n) : BijOn f (ptsOfPeriod f n) (ptsOfPeriod f n)

Full source

theorem bijOn_ptsOfPeriod (f : α → α) {n : ℕ} (hn : 0 < n) :
    BijOn f (ptsOfPeriod f n) (ptsOfPeriod f n) :=
  ⟨(Commute.refl f).mapsTo_ptsOfPeriod n, fun _ hx _ hy hxy => hx.eq_of_apply_eq_same hy hn hxy,
    fun x hx =>
    ⟨f^[n.pred] x, hx.apply_iterate _, by
      rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]⟩⟩

Bijectivity of Function on Periodic Points with Period $n$

Informal description

For any function $f \colon \alpha \to \alpha$ and positive natural number $n$, the restriction of $f$ to the set of periodic points with period $n$ is a bijection. That is, $f$ is both injective and surjective when restricted to $\{x \in \alpha \mid f^n(x) = x\}$.

Function.periodicPts definition

(f : α → α) : Set α

Full source

/-- The set of periodic points of a map `f : α → α`. -/
def periodicPts (f : α → α) : Set α :=
  { x : α | ∃ n > 0, IsPeriodicPt f n x }

Set of periodic points of a function

Informal description

The set of all periodic points of a function $ f : \alpha \to \alpha $, defined as $ \{ x \in \alpha \mid \exists n > 0, f^[n](x) = x \} $, where $ f^[n] $ denotes the $ n $-th iterate of $ f $.

Function.mk_mem_periodicPts theorem

(hn : 0 < n) (hx : IsPeriodicPt f n x) : x ∈ periodicPts f

Full source

theorem mk_mem_periodicPts (hn : 0 < n) (hx : IsPeriodicPt f n x) : x ∈ periodicPts f :=
  ⟨n, hn, hx⟩

Inclusion of Periodic Points with Positive Period

Informal description

For any function $ f : \alpha \to \alpha $, if $ x $ is a periodic point of $ f $ with a positive period $ n $ (i.e., $ f^n(x) = x $ and $ n > 0 $), then $ x $ belongs to the set of periodic points of $ f $.

Function.mem_periodicPts theorem

: x ∈ periodicPts f ↔ ∃ n > 0, IsPeriodicPt f n x

Full source

theorem mem_periodicPts : x ∈ periodicPts fx ∈ periodicPts f ↔ ∃ n > 0, IsPeriodicPt f n x :=
  Iff.rfl

Characterization of Periodic Points: $x \in \text{periodicPts}(f) \leftrightarrow \exists n > 0, f^n(x) = x$

Informal description

A point $x$ belongs to the set of periodic points of a function $f : \alpha \to \alpha$ if and only if there exists a positive integer $n$ such that $x$ is a periodic point of $f$ with period $n$, i.e., $f^n(x) = x$.

Function.periodicPts_subset_range theorem

: periodicPts f ⊆ range f

Full source

theorem periodicPts_subset_range : periodicPtsperiodicPts f ⊆ range f := by
  intro x h
  rw [mem_periodicPts] at h
  rcases h with ⟨n, _, h⟩
  use f^[n - 1] x
  nth_rw 1 [← iterate_one f]
  rw [← iterate_add_apply, Nat.add_sub_cancel' (by omega)]
  exact h

Periodic Points are Contained in the Range of the Function

Informal description

The set of periodic points of a function $f : \alpha \to \alpha$ is a subset of the range of $f$, i.e., $\text{periodicPts}(f) \subseteq \text{range}(f)$.

Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate theorem

(hx : x ∈ periodicPts f) (hm : IsPeriodicPt f m (f^[n] x)) : IsPeriodicPt f m x

Full source

theorem isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate (hx : x ∈ periodicPts f)
    (hm : IsPeriodicPt f m (f^[n] x)) : IsPeriodicPt f m x := by
  rcases hx with ⟨r, hr, hr'⟩
  suffices n ≤ (n / r + 1) * r by
    unfold IsPeriodicPt IsFixedPt
    convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
      rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]
  rw [Nat.add_mul, one_mul]
  exact (Nat.lt_div_mul_add hr).le

Periodicity Transfer from Iterate to Original Point: $x$ periodic and $f^n(x)$ periodic implies $x$ periodic with same period

Informal description

Let $f : \alpha \to \alpha$ be a function and $x$ a periodic point of $f$ (i.e., $x \in \text{periodicPts}(f)$). If the $n$-th iterate $f^{[n]}(x)$ is a periodic point of $f$ with period $m$, then $x$ itself is also a periodic point of $f$ with period $m$.

Function.bUnion_ptsOfPeriod theorem

: ⋃ n > 0, ptsOfPeriod f n = periodicPts f

Full source

theorem bUnion_ptsOfPeriod : ⋃ n > 0, ptsOfPeriod f n = periodicPts f :=
  Set.ext fun x => by simp [mem_periodicPts]

Union of Periodic Points with Positive Period Equals All Periodic Points

Informal description

The union of all sets of periodic points with positive period $n$ for a function $f : \alpha \to \alpha$ equals the set of all periodic points of $f$. In other words, $\bigcup_{n > 0} \{x \mid f^n(x) = x\} = \{x \mid \exists n > 0, f^n(x) = x\}$.

Function.iUnion_pnat_ptsOfPeriod theorem

: ⋃ n : ℕ+, ptsOfPeriod f n = periodicPts f

Full source

theorem iUnion_pnat_ptsOfPeriod : ⋃ n : ℕ+, ptsOfPeriod f n = periodicPts f :=
  iSup_subtype.trans <| bUnion_ptsOfPeriod f

Union of Periodic Points with Positive Period Equals All Periodic Points

Informal description

The union of all sets of periodic points with positive period $n$ (where $n$ is a positive natural number) for a function $f : \alpha \to \alpha$ equals the set of all periodic points of $f$. In other words, $\bigcup_{n \in \mathbb{N}^+} \{x \mid f^n(x) = x\} = \{x \mid \exists n > 0, f^n(x) = x\}$.

Function.Semiconj.mapsTo_periodicPts theorem

{g : α → β} (h : Semiconj g fa fb) : MapsTo g (periodicPts fa) (periodicPts fb)

Full source

theorem Semiconj.mapsTo_periodicPts {g : α → β} (h : Semiconj g fa fb) :
    MapsTo g (periodicPts fa) (periodicPts fb) := fun _ ⟨n, hn, hx⟩ => ⟨n, hn, hx.map h⟩

Semiconjugacy Preserves Periodic Points

Informal description

Let $g \colon \alpha \to \beta$ be a function that semiconjugates $f_a \colon \alpha \to \alpha$ to $f_b \colon \beta \to \beta$, i.e., $g \circ f_a = f_b \circ g$. Then $g$ maps periodic points of $f_a$ to periodic points of $f_b$. In other words, if $x$ is a periodic point of $f_a$, then $g(x)$ is a periodic point of $f_b$.

Function.minimalPeriod definition

(f : α → α) (x : α)

Full source

/-- Minimal period of a point `x` under an endomorphism `f`. If `x` is not a periodic point of `f`,
then `minimalPeriod f x = 0`. -/
def minimalPeriod (f : α → α) (x : α) :=
  if h : x ∈ periodicPts f then Nat.find h else 0

Minimal period of a point under an endomorphism

Informal description

The minimal period of a point $ x $ under an endomorphism $ f : \alpha \to \alpha $ is the smallest positive integer $ n $ such that $ f^[n](x) = x $. If $ x $ is not a periodic point of $ f $, the minimal period is defined to be zero.

Function.isPeriodicPt_minimalPeriod theorem

(f : α → α) (x : α) : IsPeriodicPt f (minimalPeriod f x) x

Full source

theorem isPeriodicPt_minimalPeriod (f : α → α) (x : α) : IsPeriodicPt f (minimalPeriod f x) x := by
  classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x

Minimal Period Yields Periodic Point

Informal description

For any function $f : \alpha \to \alpha$ and any point $x \in \alpha$, $x$ is a periodic point of $f$ with period equal to its minimal period, i.e., $f^{[\text{minimalPeriod}(f, x)]}(x) = x$.

Function.iterate_minimalPeriod theorem

: f^[minimalPeriod f x] x = x

Full source

@[simp]
theorem iterate_minimalPeriod : f^[minimalPeriod f x] x = x :=
  isPeriodicPt_minimalPeriod f x

Iteration at Minimal Period Returns to Original Point

Informal description

For any function $f : \alpha \to \alpha$ and any point $x \in \alpha$, the $n$-th iterate of $f$ at $x$ equals $x$, where $n$ is the minimal period of $x$ under $f$, i.e., $f^n(x) = x$ where $n = \text{minimalPeriod}(f, x)$.

Function.iterate_add_minimalPeriod_eq theorem

: f^[n + minimalPeriod f x] x = f^[n] x

Full source

@[simp]
theorem iterate_add_minimalPeriod_eq : f^[n + minimalPeriod f x] x = f^[n] x := by
  rw [iterate_add_apply]
  congr
  exact isPeriodicPt_minimalPeriod f x

Iteration Invariance Under Minimal Period Addition: $f^{[n + k]}(x) = f^{[n]}(x)$ where $k$ is the minimal period of $x$ under $f$

Informal description

For any function $f : \alpha \to \alpha$, any point $x \in \alpha$, and any natural number $n$, the $(n + \text{minimalPeriod}(f, x))$-th iterate of $f$ applied to $x$ equals the $n$-th iterate of $f$ applied to $x$, i.e., $$f^{[n + \text{minimalPeriod}(f, x)]}(x) = f^{[n]}(x).$$

Function.iterate_mod_minimalPeriod_eq theorem

: f^[n % minimalPeriod f x] x = f^[n] x

Full source

@[simp]
theorem iterate_mod_minimalPeriod_eq : f^[n % minimalPeriod f x] x = f^[n] x :=
  (isPeriodicPt_minimalPeriod f x).iterate_mod_apply n

Iteration Modulo Minimal Period: $f^{[n]}(x) = f^{[n \bmod k]}(x)$ where $k$ is the minimal period of $x$ under $f$

Informal description

For any function $f : \alpha \to \alpha$ and any point $x \in \alpha$, the $n$-th iterate of $f$ applied to $x$ equals the $(n \bmod \text{minimalPeriod}(f, x))$-th iterate of $f$ applied to $x$, i.e., $$ f^{[n]}(x) = f^{[n \bmod k]}(x) $$ where $k = \text{minimalPeriod}(f, x)$ is the minimal period of $x$ under $f$.

Function.minimalPeriod_pos_of_mem_periodicPts theorem

(hx : x ∈ periodicPts f) : 0 < minimalPeriod f x

Full source

theorem minimalPeriod_pos_of_mem_periodicPts (hx : x ∈ periodicPts f) : 0 < minimalPeriod f x := by
  classical
  simp only [minimalPeriod, dif_pos hx, (Nat.find_spec hx).1.lt]

Positivity of Minimal Period for Periodic Points

Informal description

For any point $ x $ in the set of periodic points of a function $ f : \alpha \to \alpha $, the minimal period of $ x $ under $ f $ is positive. In other words, if $ x $ is a periodic point of $ f $, then the smallest positive integer $ n $ such that $ f^[n](x) = x $ exists and is greater than zero.

Function.minimalPeriod_eq_zero_of_nmem_periodicPts theorem

(hx : x ∉ periodicPts f) : minimalPeriod f x = 0

Full source

theorem minimalPeriod_eq_zero_of_nmem_periodicPts (hx : x ∉ periodicPts f) :
    minimalPeriod f x = 0 := by simp only [minimalPeriod, dif_neg hx]

Minimal Period is Zero for Non-Periodic Points

Informal description

For any point $x$ not in the set of periodic points of a function $f : \alpha \to \alpha$, the minimal period of $x$ under $f$ is zero. That is, if $x$ is not a periodic point of $f$, then $\text{minimalPeriod}(f, x) = 0$.

Function.IsPeriodicPt.minimalPeriod_pos theorem

(hn : 0 < n) (hx : IsPeriodicPt f n x) : 0 < minimalPeriod f x

Full source

theorem IsPeriodicPt.minimalPeriod_pos (hn : 0 < n) (hx : IsPeriodicPt f n x) :
    0 < minimalPeriod f x :=
  minimalPeriod_pos_of_mem_periodicPts <| mk_mem_periodicPts hn hx

Positivity of Minimal Period for Periodic Points with Positive Period

Informal description

For any function $ f : \alpha \to \alpha $ and point $ x \in \alpha $, if $ x $ is a periodic point of $ f $ with a positive period $ n $ (i.e., $ f^[n](x) = x $ and $ n > 0 $), then the minimal period of $ x $ under $ f $ is also positive.

Function.minimalPeriod_pos_iff_mem_periodicPts theorem

: 0 < minimalPeriod f x ↔ x ∈ periodicPts f

Full source

theorem minimalPeriod_pos_iff_mem_periodicPts : 0 < minimalPeriod f x ↔ x ∈ periodicPts f :=
  ⟨not_imp_not.1 fun h => by simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff],
    minimalPeriod_pos_of_mem_periodicPts⟩

Minimal Period Positivity Criterion for Periodic Points

Informal description

For a function $ f : \alpha \to \alpha $ and a point $ x \in \alpha $, the minimal period of $ x $ under $ f $ is positive if and only if $ x $ is a periodic point of $ f $. In other words, $ \text{minimalPeriod}(f, x) > 0 \leftrightarrow x \in \text{periodicPts}(f) $.

Function.minimalPeriod_eq_zero_iff_nmem_periodicPts theorem

: minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Full source

theorem minimalPeriod_eq_zero_iff_nmem_periodicPts : minimalPeriodminimalPeriod f x = 0 ↔ x ∉ periodicPts f := by
  rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]

Minimal Period Zero Criterion for Non-Periodic Points

Informal description

For a function $f : \alpha \to \alpha$ and a point $x \in \alpha$, the minimal period of $x$ under $f$ is zero if and only if $x$ is not a periodic point of $f$. In other words, $\text{minimalPeriod}(f, x) = 0 \leftrightarrow x \notin \text{periodicPts}(f)$.

Function.IsPeriodicPt.minimalPeriod_le theorem

(hn : 0 < n) (hx : IsPeriodicPt f n x) : minimalPeriod f x ≤ n

Full source

theorem IsPeriodicPt.minimalPeriod_le (hn : 0 < n) (hx : IsPeriodicPt f n x) :
    minimalPeriod f x ≤ n := by
  classical
  rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
  exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

Minimal Period Bound for Periodic Points

Informal description

For any function $ f : \alpha \to \alpha $, if $ x $ is a periodic point of $ f $ with a positive period $ n $ (i.e., $ f^[n](x) = x $ and $ n > 0 $), then the minimal period of $ x $ under $ f $ is less than or equal to $ n $.

Function.minimalPeriod_apply_iterate theorem

(hx : x ∈ periodicPts f) (n : ℕ) : minimalPeriod f (f^[n] x) = minimalPeriod f x

Full source

theorem minimalPeriod_apply_iterate (hx : x ∈ periodicPts f) (n : ℕ) :
    minimalPeriod f (f^[n] x) = minimalPeriod f x := by
  apply
    (IsPeriodicPt.minimalPeriod_le (minimalPeriod_pos_of_mem_periodicPts hx) _).antisymm
      ((isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate hx
            (isPeriodicPt_minimalPeriod f _)).minimalPeriod_le
        (minimalPeriod_pos_of_mem_periodicPts _))
  · exact (isPeriodicPt_minimalPeriod f x).apply_iterate n
  · rcases hx with ⟨m, hm, hx⟩
    exact ⟨m, hm, hx.apply_iterate n⟩

Invariance of Minimal Period under Iteration

Informal description

For any periodic point $x$ of a function $f : \alpha \to \alpha$ (i.e., $x \in \text{periodicPts}(f)$) and any natural number $n$, the minimal period of the $n$-th iterate $f^{[n]}(x)$ under $f$ is equal to the minimal period of $x$ itself. In other words, $\text{minimalPeriod}(f, f^{[n]}(x)) = \text{minimalPeriod}(f, x)$.

Function.minimalPeriod_apply theorem

(hx : x ∈ periodicPts f) : minimalPeriod f (f x) = minimalPeriod f x

Full source

theorem minimalPeriod_apply (hx : x ∈ periodicPts f) : minimalPeriod f (f x) = minimalPeriod f x :=
  minimalPeriod_apply_iterate hx 1

Invariance of Minimal Period under Function Application

Informal description

For any periodic point $x$ of a function $f : \alpha \to \alpha$ (i.e., $x \in \text{periodicPts}(f)$), the minimal period of $f(x)$ under $f$ is equal to the minimal period of $x$ itself. In other words, $\text{minimalPeriod}(f, f(x)) = \text{minimalPeriod}(f, x)$.

Function.le_of_lt_minimalPeriod_of_iterate_eq theorem

{m n : ℕ} (hm : m < minimalPeriod f x) (hmn : f^[m] x = f^[n] x) : m ≤ n

Full source

theorem le_of_lt_minimalPeriod_of_iterate_eq {m n : ℕ} (hm : m < minimalPeriod f x)
    (hmn : f^[m] x = f^[n] x) : m ≤ n := by
  by_contra! hmn'
  rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn
  exact
    ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
              (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
                (minimalPeriod_pos_iff_mem_periodicPts.1 ((zero_le m).trans_lt hm)) hmn)).trans
          (Nat.sub_le m n)).not_lt
      hm

Minimal Period Implies Ordering of Iterates: $m < \text{minimalPeriod}(f,x)$ and $f^{[m]}(x) = f^{[n]}(x)$ implies $m \leq n$

Informal description

Let $f : \alpha \to \alpha$ be a function and $x \in \alpha$ a point with minimal period $k = \text{minimalPeriod}(f, x)$. For any natural numbers $m, n$ such that $m < k$ and $f^{[m]}(x) = f^{[n]}(x)$, we have $m \leq n$.

Function.iterate_injOn_Iio_minimalPeriod theorem

: (Iio <| minimalPeriod f x).InjOn (f^[·] x)

Full source

theorem iterate_injOn_Iio_minimalPeriod : (Iio <| minimalPeriod f x).InjOn (f^[·] x) :=
  fun _m hm _n hn hmn ↦ (le_of_lt_minimalPeriod_of_iterate_eq hm hmn).antisymm
    (le_of_lt_minimalPeriod_of_iterate_eq hn hmn.symm)

Injectivity of Iterates Below Minimal Period

Informal description

For a function $f : \alpha \to \alpha$ and a point $x \in \alpha$, the iteration map $n \mapsto f^{[n]}(x)$ is injective on the interval $\{n \in \mathbb{N} \mid n < \text{minimalPeriod}(f, x)\}$.

Function.iterate_eq_iterate_iff_of_lt_minimalPeriod theorem

{m n : ℕ} (hm : m < minimalPeriod f x) (hn : n < minimalPeriod f x) : f^[m] x = f^[n] x ↔ m = n

Full source

theorem iterate_eq_iterate_iff_of_lt_minimalPeriod {m n : ℕ} (hm : m < minimalPeriod f x)
    (hn : n < minimalPeriod f x) : f^[m]f^[m] x = f^[n] x ↔ m = n :=
  iterate_injOn_Iio_minimalPeriod.eq_iff hm hn

Injectivity of Iterates Below Minimal Period: $f^{[m]}(x) = f^{[n]}(x) \leftrightarrow m = n$ for $m, n < \text{minimalPeriod}(f,x)$

Informal description

For a function $f : \alpha \to \alpha$ and a point $x \in \alpha$, let $k$ be the minimal period of $x$ under $f$. For any natural numbers $m, n < k$, the iterates $f^{[m]}(x)$ and $f^{[n]}(x)$ are equal if and only if $m = n$.

Function.minimalPeriod_id theorem

: minimalPeriod id x = 1

Full source

@[simp] theorem minimalPeriod_id : minimalPeriod id x = 1 :=
  ((is_periodic_id _ _).minimalPeriod_le Nat.one_pos).antisymm
    (Nat.succ_le_of_lt ((is_periodic_id _ _).minimalPeriod_pos Nat.one_pos))

Minimal Period of Identity Function is One

Informal description

For any point $x$ in a type $\alpha$, the minimal period of $x$ under the identity function $\mathrm{id}$ is $1$.

Function.minimalPeriod_eq_one_iff_isFixedPt theorem

: minimalPeriod f x = 1 ↔ IsFixedPt f x

Full source

theorem minimalPeriod_eq_one_iff_isFixedPt : minimalPeriodminimalPeriod f x = 1 ↔ IsFixedPt f x := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← iterate_one f]
    refine Function.IsPeriodicPt.isFixedPt ?_
    rw [← h]
    exact isPeriodicPt_minimalPeriod f x
  · exact
      ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
        (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

Minimal Period One if and only if Fixed Point

Informal description

For a function $ f : \alpha \to \alpha $ and a point $ x \in \alpha $, the minimal period of $ x $ under $ f $ is equal to 1 if and only if $ x $ is a fixed point of $ f $, i.e., $ f(x) = x $.

Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod theorem

: ∀ {n : ℕ} (_ : n ≠ 0) (_ : n < minimalPeriod f x), ¬IsPeriodicPt f n x

Full source

theorem not_isPeriodicPt_of_pos_of_lt_minimalPeriod :
    ∀ {n : ℕ} (_ : n ≠ 0) (_ : n < minimalPeriod f x), ¬IsPeriodicPt f n x
  | 0, n0, _ => (n0 rfl).elim
  | _ + 1, _, hn => fun hp => Nat.succ_ne_zero _ (hp.eq_zero_of_lt_minimalPeriod hn)

Non-periodicity for Subminimal Iterations

Informal description

For any positive integer $n$ such that $n$ is less than the minimal period of a point $x$ under a function $f : \alpha \to \alpha$, the point $x$ is not a periodic point of $f$ with period $n$. In other words, if $0 < n < \text{minimalPeriod}(f, x)$, then $f^{[n]}(x) \neq x$.

Function.IsPeriodicPt.minimalPeriod_dvd theorem

(hx : IsPeriodicPt f n x) : minimalPeriod f x ∣ n

Full source

theorem IsPeriodicPt.minimalPeriod_dvd (hx : IsPeriodicPt f n x) : minimalPeriodminimalPeriod f x ∣ n :=
  (eq_or_lt_of_le <| n.zero_le).elim (fun hn0 => hn0 ▸ Nat.dvd_zero _) fun hn0 =>
    Nat.dvd_iff_mod_eq_zero.2 <|
      (hx.mod <| isPeriodicPt_minimalPeriod f x).eq_zero_of_lt_minimalPeriod <|
        Nat.mod_lt _ <| hx.minimalPeriod_pos hn0

Minimal Period Divides Any Period

Informal description

For any function $f : \alpha \to \alpha$ and point $x \in \alpha$, if $x$ is a periodic point of $f$ with period $n$ (i.e., $f^[n](x) = x$), then the minimal period of $x$ under $f$ divides $n$.

Function.isPeriodicPt_iff_minimalPeriod_dvd theorem

: IsPeriodicPt f n x ↔ minimalPeriod f x ∣ n

Full source

theorem isPeriodicPt_iff_minimalPeriod_dvd : IsPeriodicPtIsPeriodicPt f n x ↔ minimalPeriod f x ∣ n :=
  ⟨IsPeriodicPt.minimalPeriod_dvd, fun h => (isPeriodicPt_minimalPeriod f x).trans_dvd h⟩

Characterization of Periodic Points via Minimal Period Divisibility

Informal description

For a function $f \colon \alpha \to \alpha$, a point $x \in \alpha$, and a natural number $n$, the point $x$ is a periodic point of $f$ with period $n$ (i.e., $f^[n](x) = x$) if and only if the minimal period of $x$ under $f$ divides $n$.

Function.minimalPeriod_eq_minimalPeriod_iff theorem

{g : β → β} {y : β} : minimalPeriod f x = minimalPeriod g y ↔ ∀ n, IsPeriodicPt f n x ↔ IsPeriodicPt g n y

Full source

theorem minimalPeriod_eq_minimalPeriod_iff {g : β → β} {y : β} :
    minimalPeriodminimalPeriod f x = minimalPeriod g y ↔ ∀ n, IsPeriodicPt f n x ↔ IsPeriodicPt g n y := by
  simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]

Minimal Period Equality Criterion via Periodic Points

Informal description

For two functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, and points $x \in \alpha$ and $y \in \beta$, the minimal period of $x$ under $f$ equals the minimal period of $y$ under $g$ if and only if for every natural number $n$, $x$ is a periodic point of $f$ with period $n$ precisely when $y$ is a periodic point of $g$ with period $n$. In other words, $\text{minimalPeriod}(f, x) = \text{minimalPeriod}(g, y) \leftrightarrow (\forall n, f^[n](x) = x \leftrightarrow g^[n](y) = y)$.

Function.Commute.minimalPeriod_of_comp_dvd_lcm theorem

{g : α → α} (h : Commute f g) : minimalPeriod (f ∘ g) x ∣ Nat.lcm (minimalPeriod f x) (minimalPeriod g x)

Full source

theorem Commute.minimalPeriod_of_comp_dvd_lcm {g : α → α} (h : Commute f g) :
    minimalPeriodminimalPeriod (f ∘ g) x ∣ Nat.lcm (minimalPeriod f x) (minimalPeriod g x) := by
  rw [← isPeriodicPt_iff_minimalPeriod_dvd]
  exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)

Minimal Period of Composition Divides LCM of Minimal Periods for Commuting Functions

Informal description

Let $f, g \colon \alpha \to \alpha$ be commuting functions (i.e., $f \circ g = g \circ f$). Then for any point $x \in \alpha$, the minimal period of $x$ under the composition $f \circ g$ divides the least common multiple of the minimal periods of $x$ under $f$ and under $g$. In other words, $$\text{minimalPeriod}(f \circ g, x) \mid \text{lcm}(\text{minimalPeriod}(f, x), \text{minimalPeriod}(g, x)).$$

Function.minimalPeriod_iterate_eq_div_gcd theorem

(h : n ≠ 0) : minimalPeriod f^[n] x = minimalPeriod f x / Nat.gcd (minimalPeriod f x) n

Full source

theorem minimalPeriod_iterate_eq_div_gcd (h : n ≠ 0) :
    minimalPeriod f^[n] x = minimalPeriod f x / Nat.gcd (minimalPeriod f x) n :=
  minimalPeriod_iterate_eq_div_gcd_aux <| gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero h)

Minimal Period of Iterated Function via GCD Division

Informal description

For any endomorphism $f : \alpha \to \alpha$, point $x \in \alpha$, and nonzero natural number $n$, the minimal period of $x$ under the $n$-th iterate $f^{[n]}$ is equal to the minimal period of $x$ under $f$ divided by the greatest common divisor of the minimal period and $n$, i.e., $$\text{minimalPeriod}\, f^{[n]}\, x = \frac{\text{minimalPeriod}\, f\, x}{\gcd(\text{minimalPeriod}\, f\, x, n)}.$$

Function.minimalPeriod_iterate_eq_div_gcd' theorem

(h : x ∈ periodicPts f) : minimalPeriod f^[n] x = minimalPeriod f x / Nat.gcd (minimalPeriod f x) n

Full source

theorem minimalPeriod_iterate_eq_div_gcd' (h : x ∈ periodicPts f) :
    minimalPeriod f^[n] x = minimalPeriod f x / Nat.gcd (minimalPeriod f x) n :=
  minimalPeriod_iterate_eq_div_gcd_aux <|
    gcd_pos_of_pos_left n (minimalPeriod_pos_iff_mem_periodicPts.mpr h)

Minimal Period of Iterated Function for Periodic Points via GCD Division

Informal description

For a function $f : \alpha \to \alpha$ and a periodic point $x \in \alpha$ (i.e., $x \in \text{periodicPts}(f)$), the minimal period of $x$ under the $n$-th iterate $f^{[n]}$ is equal to the minimal period of $x$ under $f$ divided by the greatest common divisor of the minimal period and $n$, i.e., $$\text{minimalPeriod}\, f^{[n]}\, x = \frac{\text{minimalPeriod}\, f\, x}{\gcd(\text{minimalPeriod}\, f\, x, n)}.$$

Function.periodicOrbit definition

(f : α → α) (x : α) : Cycle α

Full source

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

Orbit of a periodic point

Informal description

The orbit of a periodic point $ x $ under an endomorphism $ f : \alpha \to \alpha $ is the cycle $[x, f(x), f^2(x), \ldots]$, where the length of the cycle is equal to the minimal period of $ x $. If $ x $ is not a periodic point of $ f $, the orbit is the empty cycle.

Function.periodicOrbit_def theorem

(f : α → α) (x : α) : periodicOrbit f x = (List.range (minimalPeriod f x)).map fun n => f^[n] x

Full source

/-- The definition of a periodic orbit, in terms of `List.map`. -/
theorem periodicOrbit_def (f : α → α) (x : α) :
    periodicOrbit f x = (List.range (minimalPeriod f x)).map fun n => f^[n] x :=
  rfl

Definition of Periodic Orbit via Minimal Period and Iteration

Informal description

For an endomorphism $f : \alpha \to \alpha$ and a point $x \in \alpha$, the periodic orbit of $x$ under $f$ is given by the list $[f^0(x), f^1(x), \ldots, f^{n-1}(x)]$, where $n$ is the minimal period of $x$ under $f$. That is, $\text{periodicOrbit}\,f\,x = \text{map}\,(\lambda n.\,f^n\,x)\,(\text{range}\,(\text{minimalPeriod}\,f\,x))$.

Function.periodicOrbit_eq_cycle_map theorem

(f : α → α) (x : α) : periodicOrbit f x = (List.range (minimalPeriod f x) : Cycle ℕ).map fun n => f^[n] x

Full source

/-- The definition of a periodic orbit, in terms of `Cycle.map`. -/
theorem periodicOrbit_eq_cycle_map (f : α → α) (x : α) :
    periodicOrbit f x = (List.range (minimalPeriod f x) : Cycle ℕ).map fun n => f^[n] x :=
  rfl

Periodic Orbit as Cycle Map of Iterates

Informal description

For any endomorphism $f : \alpha \to \alpha$ and any point $x \in \alpha$, the periodic orbit of $x$ under $f$ is equal to the cycle obtained by mapping the function $\lambda n, f^{[n]}(x)$ over the list of natural numbers from $0$ to $\text{minimalPeriod}\, f\, x - 1$.

Function.periodicOrbit_length theorem

: (periodicOrbit f x).length = minimalPeriod f x

Full source

@[simp]
theorem periodicOrbit_length : (periodicOrbit f x).length = minimalPeriod f x := by
  rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]

Periodic Orbit Length Equals Minimal Period

Informal description

For any function $f : \alpha \to \alpha$ and point $x \in \alpha$, the length of the periodic orbit of $x$ under $f$ is equal to the minimal period of $x$ under $f$. That is, $|\text{orbit}(f, x)| = \text{minimalPeriod}(f, x)$.

Function.periodicOrbit_eq_nil_iff_not_periodic_pt theorem

: periodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f

Full source

@[simp]
theorem periodicOrbit_eq_nil_iff_not_periodic_pt :
    periodicOrbitperiodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f := by
  simp only [periodicOrbit.eq_1, Cycle.coe_eq_nil, List.map_eq_nil_iff, List.range_eq_nil]
  exact minimalPeriod_eq_zero_iff_nmem_periodicPts

Empty Orbit Criterion for Non-Periodic Points

Informal description

For a function $f : \alpha \to \alpha$ and a point $x \in \alpha$, the periodic orbit of $x$ under $f$ is empty if and only if $x$ is not a periodic point of $f$. In other words, $\text{orbit}(f, x) = \emptyset \leftrightarrow x \notin \text{periodicPts}(f)$.

Function.periodicOrbit_eq_nil_of_not_periodic_pt theorem

(h : x ∉ periodicPts f) : periodicOrbit f x = Cycle.nil

Full source

theorem periodicOrbit_eq_nil_of_not_periodic_pt (h : x ∉ periodicPts f) :
    periodicOrbit f x = Cycle.nil :=
  periodicOrbit_eq_nil_iff_not_periodic_pt.2 h

Empty Periodic Orbit for Non-Periodic Points

Informal description

For a function $f : \alpha \to \alpha$ and a point $x \in \alpha$, if $x$ is not a periodic point of $f$, then the periodic orbit of $x$ under $f$ is empty.

Function.mem_periodicOrbit_iff theorem

(hx : x ∈ periodicPts f) : y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y

Full source

@[simp]
theorem mem_periodicOrbit_iff (hx : x ∈ periodicPts f) :
    y ∈ periodicOrbit f xy ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y := by
  simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]
  use fun ⟨a, _, ha'⟩ => ⟨a, ha'⟩
  rintro ⟨n, rfl⟩
  use n % minimalPeriod f x, mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx)
  rw [iterate_mod_minimalPeriod_eq]

Characterization of Points in Periodic Orbit via Iterates

Informal description

For a periodic point $x$ of a function $f : \alpha \to \alpha$, a point $y$ belongs to the periodic orbit of $x$ if and only if there exists a natural number $n$ such that the $n$-th iterate of $f$ at $x$ equals $y$, i.e., $$ y \in \text{periodicOrbit}(f, x) \leftrightarrow \exists n \in \mathbb{N}, f^{[n]}(x) = y. $$

Function.iterate_mem_periodicOrbit theorem

(hx : x ∈ periodicPts f) (n : ℕ) : f^[n] x ∈ periodicOrbit f x

Full source

@[simp]
theorem iterate_mem_periodicOrbit (hx : x ∈ periodicPts f) (n : ℕ) :
    f^[n]f^[n] x ∈ periodicOrbit f x :=
  (mem_periodicOrbit_iff hx).2 ⟨n, rfl⟩

Iterates of Periodic Points Belong to Their Orbit

Informal description

For a periodic point $x$ of a function $f : \alpha \to \alpha$ and any natural number $n$, the $n$-th iterate of $f$ at $x$ belongs to the periodic orbit of $x$, i.e., $f^{[n]}(x) \in \text{periodicOrbit}(f, x)$.

Function.self_mem_periodicOrbit theorem

(hx : x ∈ periodicPts f) : x ∈ periodicOrbit f x

Full source

@[simp]
theorem self_mem_periodicOrbit (hx : x ∈ periodicPts f) : x ∈ periodicOrbit f x :=
  iterate_mem_periodicOrbit hx 0

Periodic Point Belongs to Its Own Orbit

Informal description

For any periodic point $x$ of a function $f : \alpha \to \alpha$, the point $x$ itself belongs to its periodic orbit under $f$, i.e., $x \in \text{periodicOrbit}(f, x)$.

Function.nodup_periodicOrbit theorem

: (periodicOrbit f x).Nodup

Full source

theorem nodup_periodicOrbit : (periodicOrbit f x).Nodup := by
  rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on List.nodup_range]
  intro m hm n hn hmn
  rw [List.mem_range] at hm hn
  rwa [iterate_eq_iterate_iff_of_lt_minimalPeriod hm hn] at hmn

Distinctness of Elements in Periodic Orbit: $\text{periodicOrbit}(f, x)$ is nodup

Informal description

The periodic orbit of a point $x$ under a function $f : \alpha \to \alpha$ has no duplicate elements, i.e., the cycle $[x, f(x), f^2(x), \ldots]$ contains distinct elements when $x$ is a periodic point of $f$.

Function.periodicOrbit_apply_iterate_eq theorem

(hx : x ∈ periodicPts f) (n : ℕ) : periodicOrbit f (f^[n] x) = periodicOrbit f x

Full source

theorem periodicOrbit_apply_iterate_eq (hx : x ∈ periodicPts f) (n : ℕ) :
    periodicOrbit f (f^[n] x) = periodicOrbit f x :=
  Eq.symm <| Cycle.coe_eq_coe.2 <| .intro n <|
    List.ext_get (by simp [minimalPeriod_apply_iterate hx]) fun m _ _ ↦ by
      simp [List.getElem_rotate, iterate_add_apply]

Invariance of Periodic Orbit under Iteration: $\text{orbit}(f^n(x)) = \text{orbit}(x)$

Informal description

For any periodic point $x$ of a function $f : \alpha \to \alpha$ and any natural number $n$, the periodic orbit of the $n$-th iterate $f^{[n]}(x)$ under $f$ is equal to the periodic orbit of $x$ itself. That is, $$\text{periodicOrbit}(f, f^{[n]}(x)) = \text{periodicOrbit}(f, x).$$

Function.periodicOrbit_apply_eq theorem

(hx : x ∈ periodicPts f) : periodicOrbit f (f x) = periodicOrbit f x

Full source

theorem periodicOrbit_apply_eq (hx : x ∈ periodicPts f) :
    periodicOrbit f (f x) = periodicOrbit f x :=
  periodicOrbit_apply_iterate_eq hx 1

Invariance of Periodic Orbit under Function Application: $\text{orbit}(f(x)) = \text{orbit}(x)$

Informal description

For any periodic point $x$ of a function $f : \alpha \to \alpha$, the periodic orbit of $f(x)$ under $f$ is equal to the periodic orbit of $x$ itself, i.e., $$\text{orbit}(f, f(x)) = \text{orbit}(f, x).$$

Function.periodicOrbit_chain theorem

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

Full source

theorem periodicOrbit_chain (r : α → α → Prop) {f : α → α} {x : α} :
    (periodicOrbit f x).Chain r ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x) := by
  by_cases hx : x ∈ periodicPts f
  · have hx' := minimalPeriod_pos_of_mem_periodicPts hx
    have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
    rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
    refine ⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
    · rintro ⟨hr, H⟩ n hn
      rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
      · rwa [hM', hM, iterate_minimalPeriod]
      · exact H _ hM'
    · rw [iterate_zero_apply]
      nth_rw 3 [← @iterate_minimalPeriod α f x]
      nth_rw 2 [← hM]
      exact H _ (Nat.lt_succ_self _)
  · rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_nmem_periodicPts hx]
    simp

Chain Condition for Periodic Orbits

Informal description

For any binary relation $r$ on $\alpha$, a function $f : \alpha \to \alpha$, and a point $x \in \alpha$, the periodic orbit of $x$ under $f$ forms a chain with respect to $r$ if and only if for every natural number $n$ less than the minimal period of $x$ under $f$, the relation $r$ holds between the $n$-th iterate $f^n(x)$ and the $(n+1)$-th iterate $f^{n+1}(x)$. In other words, the cycle $[x, f(x), f^2(x), \ldots]$ is a chain under $r$ if and only if $r(f^n(x), f^{n+1}(x))$ holds for all $n < \text{minimalPeriod}(f, x)$.

Function.periodicOrbit_chain' theorem

 (r : α → α → Prop) {f : α → α} {x : α} (hx : x ∈ periodicPts f) :
  (periodicOrbit f x).Chain r ↔ ∀ n, r (f^[n] x) (f^[n + 1] x)

Full source

theorem periodicOrbit_chain' (r : α → α → Prop) {f : α → α} {x : α} (hx : x ∈ periodicPts f) :
    (periodicOrbit f x).Chain r ↔ ∀ n, r (f^[n] x) (f^[n + 1] x) := by
  rw [periodicOrbit_chain r]
  refine ⟨fun H n => ?_, fun H n _ => H n⟩
  rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
    ← iterate_succ_apply, minimalPeriod_apply hx]
  exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))

Chain Condition for Periodic Orbits of Periodic Points

Informal description

For any binary relation $r$ on $\alpha$, a function $f : \alpha \to \alpha$, and a periodic point $x \in \alpha$ (i.e., $x \in \text{periodicPts}(f)$), the periodic orbit of $x$ under $f$ forms a chain with respect to $r$ if and only if for every natural number $n$, the relation $r$ holds between the $n$-th iterate $f^{[n]}(x)$ and the $(n+1)$-th iterate $f^{[n+1]}(x)$. In other words, the cycle $[x, f(x), f^2(x), \ldots]$ is a chain under $r$ if and only if $r(f^{[n]}(x), f^{[n+1]}(x))$ holds for all $n \in \mathbb{N}$.

Function.isFixedPt_prodMap theorem

(x : α × β) : IsFixedPt (Prod.map f g) x ↔ IsFixedPt f x.1 ∧ IsFixedPt g x.2

Full source

@[simp]
theorem isFixedPt_prodMap (x : α × β) :
    IsFixedPtIsFixedPt (Prod.map f g) x ↔ IsFixedPt f x.1 ∧ IsFixedPt g x.2 :=
  Prod.ext_iff

Fixed Point Characterization for Product Map

Informal description

For any pair $x = (x_1, x_2) \in \alpha \times \beta$, the point $x$ is a fixed point of the product map $\text{Prod.map}\,f\,g$ if and only if $x_1$ is a fixed point of $f$ and $x_2$ is a fixed point of $g$. In other words, $\text{Prod.map}\,f\,g\,x = x \leftrightarrow f(x_1) = x_1 \land g(x_2) = x_2$.

Function.IsFixedPt.prodMap theorem

(ha : IsFixedPt f a) (hb : IsFixedPt g b) : IsFixedPt (Prod.map f g) (a, b)

Full source

theorem IsFixedPt.prodMap (ha : IsFixedPt f a) (hb : IsFixedPt g b) :
    IsFixedPt (Prod.map f g) (a, b) :=
  (isFixedPt_prodMap _).mpr ⟨ha, hb⟩

Fixed Points of Product Map from Component Fixed Points

Informal description

Given functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, if $a \in \alpha$ is a fixed point of $f$ and $b \in \beta$ is a fixed point of $g$, then the pair $(a, b) \in \alpha \times \beta$ is a fixed point of the product map $\text{Prod.map}\,f\,g$.

Function.isPeriodicPt_prodMap theorem

(x : α × β) : IsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.1 ∧ IsPeriodicPt g n x.2

Full source

@[simp]
theorem isPeriodicPt_prodMap (x : α × β) :
    IsPeriodicPtIsPeriodicPt (Prod.map f g) n x ↔ IsPeriodicPt f n x.1 ∧ IsPeriodicPt g n x.2 := by
  simp [IsPeriodicPt]

Periodic Point Characterization for Product Map

Informal description

For any pair $x = (x_1, x_2) \in \alpha \times \beta$, the point $x$ is a periodic point of the product map $\text{Prod.map}\,f\,g$ with period $n$ if and only if $x_1$ is a periodic point of $f$ with period $n$ and $x_2$ is a periodic point of $g$ with period $n$. In other words, $(f \times g)^n(x) = x$ if and only if $f^n(x_1) = x_1$ and $g^n(x_2) = x_2$.

Function.IsPeriodicPt.prodMap theorem

(ha : IsPeriodicPt f n a) (hb : IsPeriodicPt g n b) : IsPeriodicPt (Prod.map f g) n (a, b)

Full source

theorem IsPeriodicPt.prodMap (ha : IsPeriodicPt f n a) (hb : IsPeriodicPt g n b) :
    IsPeriodicPt (Prod.map f g) n (a, b) :=
  (isPeriodicPt_prodMap _).mpr ⟨ha, hb⟩

Periodic Points of Product Map from Component Periodic Points

Informal description

Given functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, if $a \in \alpha$ is a periodic point of $f$ with period $n$ and $b \in \beta$ is a periodic point of $g$ with period $n$, then the pair $(a, b) \in \alpha \times \beta$ is a periodic point of the product map $f \times g$ with period $n$.

MulAction.period definition

(m : M) (a : α) : ℕ

Full source

/--
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.
-/
@[to_additive "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."]
noncomputable def period (m : M) (a : α) : ℕ := minimalPeriod (fun x => m • x) a

Period of a multiplicative action

Informal description

The period of a multiplicative action of an element $ m $ on a point $ a $ is the smallest positive integer $ n $ such that $ m^n \cdot a = a $, where $ \cdot $ denotes the action. If no such $ n $ exists, the period is defined to be zero.

MulAction.period_eq_minimalPeriod theorem

{m : M} {a : α} : MulAction.period m a = minimalPeriod (fun x => m • x) a

Full source

/-- `MulAction.period m a` is definitionally equal to `Function.minimalPeriod (m • ·) a`. -/
@[to_additive "`AddAction.period m a` is definitionally equal to
`Function.minimalPeriod (m +ᵥ ·) a`"]
theorem period_eq_minimalPeriod {m : M} {a : α} :
    MulAction.period m a = minimalPeriod (fun x => m • x) a := rfl

Period Equals Minimal Period for Multiplicative Action

Informal description

For any element $m$ in a multiplicative monoid $M$ and any point $a$ in a set $\alpha$ with a multiplicative action of $M$, the period of $a$ under the action of $m$ is equal to the minimal period of $a$ under the function $x \mapsto m \cdot x$.

MulAction.pow_period_smul theorem

(m : M) (a : α) : m ^ (period m a) • a = a

Full source

/-- `m ^ (period m a)` fixes `a`. -/
@[to_additive (attr := simp) "`(period m a) • m` fixes `a`."]
theorem pow_period_smul (m : M) (a : α) : m ^ (period m a) • a = a := by
  rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]

Periodic Action Identity: $m^{\text{period}(m,a)} \cdot a = a$

Informal description

For any element $m$ in a multiplicative monoid $M$ and any point $a$ in a set $\alpha$ with a multiplicative action of $M$, the action of $m$ raised to the power of its period at $a$ fixes $a$, i.e., $m^{\text{period}(m,a)} \cdot a = a$.

MulAction.isPeriodicPt_smul_iff theorem

{m : M} {a : α} {n : ℕ} : IsPeriodicPt (m • ·) n a ↔ m ^ n • a = a

Full source

@[to_additive]
lemma isPeriodicPt_smul_iff {m : M} {a : α} {n : ℕ} :
    IsPeriodicPtIsPeriodicPt (m • ·) n a ↔ m ^ n • a = a := by
  rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]

Periodic Point Condition for Multiplicative Action: $m^n \cdot a = a$ iff $a$ is periodic with period $n$ under $m$

Informal description

For a multiplicative action of an element $m$ on a point $a$ in a type $\alpha$, the point $a$ is periodic with period $n$ under the action of $m$ if and only if the $n$-th power of $m$ acting on $a$ returns $a$, i.e., $m^n \cdot a = a$.

MulAction.pow_smul_eq_iff_period_dvd theorem

{n : ℕ} {m : M} {a : α} : m ^ n • a = a ↔ period m a ∣ n

Full source

@[to_additive]
theorem pow_smul_eq_iff_period_dvd {n : ℕ} {m : M} {a : α} :
    m ^ n • a = a ↔ period m a ∣ n := by
  rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]

Period Divisibility Condition for Multiplicative Action: $m^n \cdot a = a$ iff $\text{period}(m,a) \mid n$

Informal description

For any natural number $n$, element $m$ in a multiplicative monoid $M$, and point $a$ in a set $\alpha$ with a multiplicative action of $M$, the action of $m^n$ on $a$ fixes $a$ (i.e., $m^n \cdot a = a$) if and only if the period of $m$ at $a$ divides $n$.

MulAction.zpow_smul_eq_iff_period_dvd theorem

{j : ℤ} {g : G} {a : α} : g ^ j • a = a ↔ (period g a : ℤ) ∣ j

Full source

@[to_additive]
theorem zpow_smul_eq_iff_period_dvd {j : ℤ} {g : G} {a : α} :
    g ^ j • a = a ↔ (period g a : ℤ) ∣ j := by
  match j with
  | (n : ℕ) => rw [zpow_natCast, Int.natCast_dvd_natCast, pow_smul_eq_iff_period_dvd]
  | -(n + 1 : ℕ) =>
    rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]

Period Divisibility Condition for Integer Powers in Multiplicative Action: $g^j \cdot a = a$ iff $\text{period}(g,a) \mid j$

Informal description

For any integer $j$, element $g$ in a group $G$, and point $a$ in a set $\alpha$ with a multiplicative action of $G$, the action of $g^j$ on $a$ fixes $a$ (i.e., $g^j \cdot a = a$) if and only if the period of $g$ at $a$ divides $j$ (considered as an integer).

MulAction.pow_mod_period_smul theorem

(n : ℕ) {m : M} {a : α} : m ^ (n % period m a) • a = m ^ n • a

Full source

@[to_additive (attr := simp)]
theorem pow_mod_period_smul (n : ℕ) {m : M} {a : α} :
    m ^ (n % period m a) • a = m ^ n • a := by
  conv_rhs => rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Periodic Action Modulo Period: $m^{n \bmod \text{period}(m,a)} \cdot a = m^n \cdot a$

Informal description

For any natural number $n$, element $m$ in a multiplicative monoid $M$, and point $a$ in a set $\alpha$ with a multiplicative action of $M$, the action of $m^{n \bmod \text{period}(m,a)}$ on $a$ is equal to the action of $m^n$ on $a$, i.e., $$ m^{n \bmod \text{period}(m,a)} \cdot a = m^n \cdot a. $$

MulAction.zpow_mod_period_smul theorem

(j : ℤ) {g : G} {a : α} : g ^ (j % (period g a : ℤ)) • a = g ^ j • a

Full source

@[to_additive (attr := simp)]
theorem zpow_mod_period_smul (j : ℤ) {g : G} {a : α} :
    g ^ (j % (period g a : ℤ)) • a = g ^ j • a := by
  conv_rhs => rw [← Int.emod_add_ediv j (period g a), zpow_add, mul_smul,
    zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Periodic Action Modulo Period for Integer Powers: $g^{j \bmod \text{period}(g,a)} \cdot a = g^j \cdot a$

Informal description

For any integer $j$, element $g$ in a group $G$, and point $a$ in a set $\alpha$ with a multiplicative action of $G$, the action of $g^{j \bmod \text{period}(g,a)}$ on $a$ is equal to the action of $g^j$ on $a$, i.e., $$ g^{j \bmod \text{period}(g,a)} \cdot a = g^j \cdot a. $$

MulAction.pow_add_period_smul theorem

(n : ℕ) (m : M) (a : α) : m ^ (n + period m a) • a = m ^ n • a

Full source

@[to_additive (attr := simp)]
theorem pow_add_period_smul (n : ℕ) (m : M) (a : α) :
    m ^ (n + period m a) • a = m ^ n • a := by
  rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]

Periodicity of Multiplicative Action: $m^{n + \text{period}(m,a)} \cdot a = m^n \cdot a$

Informal description

For any natural number $n$, element $m$ in a multiplicative monoid $M$, and point $a$ in a set $\alpha$ with a multiplicative action of $M$, the action of $m^{n + \text{period}(m,a)}$ on $a$ is equal to the action of $m^n$ on $a$, i.e., $$ m^{n + \text{period}(m,a)} \cdot a = m^n \cdot a. $$

MulAction.pow_period_add_smul theorem

(n : ℕ) (m : M) (a : α) : m ^ (period m a + n) • a = m ^ n • a

Full source

@[to_additive (attr := simp)]
theorem pow_period_add_smul (n : ℕ) (m : M) (a : α) :
    m ^ (period m a + n) • a = m ^ n • a := by
  rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]

Periodic Action Addition Identity: $m^{\text{period}(m,a) + n} \cdot a = m^n \cdot a$

Informal description

For any natural number $n$, element $m$ in a multiplicative monoid $M$, and point $a$ in a set $\alpha$ with a multiplicative action of $M$, the action of $m^{\text{period}(m,a) + n}$ on $a$ is equal to the action of $m^n$ on $a$, i.e., $$ m^{\text{period}(m,a) + n} \cdot a = m^n \cdot a. $$

MulAction.zpow_add_period_smul theorem

(i : ℤ) (g : G) (a : α) : g ^ (i + period g a) • a = g ^ i • a

Full source

@[to_additive (attr := simp)]
theorem zpow_add_period_smul (i : ℤ) (g : G) (a : α) :
    g ^ (i + period g a) • a = g ^ i • a := by
  rw [← zpow_mod_period_smul, Int.add_emod_right, zpow_mod_period_smul]

Periodicity of Multiplicative Action for Integer Powers: $g^{i + \text{period}(g,a)} \cdot a = g^i \cdot a$

Informal description

For any integer $i$, element $g$ in a group $G$, and point $a$ in a set $\alpha$ with a multiplicative action of $G$, the action of $g^{i + \text{period}(g,a)}$ on $a$ is equal to the action of $g^i$ on $a$, i.e., $$ g^{i + \text{period}(g,a)} \cdot a = g^i \cdot a. $$

MulAction.zpow_period_add_smul theorem

(i : ℤ) (g : G) (a : α) : g ^ (period g a + i) • a = g ^ i • a

Full source

@[to_additive (attr := simp)]
theorem zpow_period_add_smul (i : ℤ) (g : G) (a : α) :
    g ^ (period g a + i) • a = g ^ i • a := by
  rw [← zpow_mod_period_smul, Int.add_emod_left, zpow_mod_period_smul]

Periodic Action Addition Identity for Integer Powers: $g^{\text{period}(g,a) + i} \cdot a = g^i \cdot a$

Informal description

For any integer $i$, element $g$ in a group $G$, and point $a$ in a set $\alpha$ with a multiplicative action of $G$, the action of $g^{\text{period}(g,a) + i}$ on $a$ is equal to the action of $g^i$ on $a$, i.e., $$ g^{\text{period}(g,a) + i} \cdot a = g^i \cdot a. $$

MulAction.pow_smul_eq_iff_minimalPeriod_dvd theorem

{n : ℕ} : a ^ n • b = b ↔ minimalPeriod (a • ·) b ∣ n

Full source

@[to_additive]
theorem pow_smul_eq_iff_minimalPeriod_dvd {n : ℕ} :
    a ^ n • b = b ↔ minimalPeriod (a • ·) b ∣ n := by
  rw [← period_eq_minimalPeriod, pow_smul_eq_iff_period_dvd]

Minimal Period Divisibility Condition for Multiplicative Action: $a^n \cdot b = b$ iff $\text{minimalPeriod}(a \cdot \cdot, b) \mid n$

Informal description

For any natural number $n$, element $a$ in a multiplicative monoid $G$, and point $b$ in a set $\alpha$ with a multiplicative action of $G$, the action of $a^n$ on $b$ fixes $b$ (i.e., $a^n \cdot b = b$) if and only if the minimal period of $b$ under the action of $a$ divides $n$.

MulAction.zpow_smul_eq_iff_minimalPeriod_dvd theorem

{n : ℤ} : a ^ n • b = b ↔ (minimalPeriod (a • ·) b : ℤ) ∣ n

Full source

@[to_additive]
theorem zpow_smul_eq_iff_minimalPeriod_dvd {n : ℤ} :
    a ^ n • b = b ↔ (minimalPeriod (a • ·) b : ℤ) ∣ n := by
  rw [← period_eq_minimalPeriod, zpow_smul_eq_iff_period_dvd]

Minimal Period Divisibility Condition for Integer Powers in Multiplicative Action: $a^n \cdot b = b$ iff $\text{minimalPeriod}(a \cdot \cdot, b) \mid n$

Informal description

For any integer $n$, element $a$ in a multiplicative monoid $G$, and point $b$ in a set $\alpha$ with a multiplicative action of $G$, the action of $a^n$ on $b$ fixes $b$ (i.e., $a^n \cdot b = b$) if and only if the minimal period of $b$ under the action of $a$ divides $n$ (considered as an integer).

MulAction.pow_smul_mod_minimalPeriod theorem

(n : ℕ) : a ^ (n % minimalPeriod (a • ·) b) • b = a ^ n • b

Full source

@[to_additive (attr := simp)]
theorem pow_smul_mod_minimalPeriod (n : ℕ) :
    a ^ (n % minimalPeriod (a • ·) b) • b = a ^ n • b := by
  rw [← period_eq_minimalPeriod, pow_mod_period_smul]

Periodic Action Modulo Minimal Period: $a^{n \bmod \text{minimalPeriod}} \cdot b = a^n \cdot b$

Informal description

For any natural number $n$, element $a$ in a multiplicative monoid $G$, and point $b$ in a set $\alpha$ with a multiplicative action of $G$, the action of $a^{n \bmod \text{minimalPeriod}(a \cdot \cdot, b)}$ on $b$ is equal to the action of $a^n$ on $b$, i.e., $$ a^{n \bmod \text{minimalPeriod}(a \cdot \cdot, b)} \cdot b = a^n \cdot b. $$

MulAction.zpow_smul_mod_minimalPeriod theorem

(n : ℤ) : a ^ (n % (minimalPeriod (a • ·) b : ℤ)) • b = a ^ n • b

Full source

@[to_additive (attr := simp)]
theorem zpow_smul_mod_minimalPeriod (n : ℤ) :
    a ^ (n % (minimalPeriod (a • ·) b : ℤ)) • b = a ^ n • b := by
  rw [← period_eq_minimalPeriod, zpow_mod_period_smul]

Periodic Action Modulo Minimal Period for Integer Powers: $a^{n \bmod \text{minimalPeriod}} \cdot b = a^n \cdot b$

Informal description

For any integer $n$, element $a$ in a multiplicative monoid $G$, and point $b$ in a set $\alpha$ with a multiplicative action of $G$, the action of $a^{n \bmod \text{minimalPeriod}(a \cdot \cdot, b)}$ on $b$ is equal to the action of $a^n$ on $b$, i.e., $$ a^{n \bmod \text{minimalPeriod}(a \cdot \cdot, b)} \cdot b = a^n \cdot b. $$

Mathlib.Dynamics.PeriodicPts.Defs

Main definitions

Main statements

References