Mathlib.Dynamics.PeriodicPts.Lemmas

Function.directed_ptsOfPeriod_pnat theorem

(f : α → α) : Directed (· ⊆ ·) fun n : ℕ+ => ptsOfPeriod f n

Full source

theorem directed_ptsOfPeriod_pnat (f : α → α) : Directed (· ⊆ ·) fun n : ℕ+ => ptsOfPeriod f n :=
  fun m n => ⟨m * n, fun _ hx => hx.mul_const n, fun _ hx => hx.const_mul m⟩

Directedness of Periodic Points with Respect to Subset Inclusion

Informal description

For any function $f \colon \alpha \to \alpha$, the family of sets $\{\text{ptsOfPeriod}\, f\, n \mid n \in \mathbb{N}^+\}$ is directed with respect to the subset relation $\subseteq$. That is, for any two positive integers $n_1, n_2 \in \mathbb{N}^+$, there exists a positive integer $n \in \mathbb{N}^+$ such that $\text{ptsOfPeriod}\, f\, n_1 \subseteq \text{ptsOfPeriod}\, f\, n$ and $\text{ptsOfPeriod}\, f\, n_2 \subseteq \text{ptsOfPeriod}\, f\, n$.

Function.bijOn_periodicPts theorem

: BijOn f (periodicPts f) (periodicPts f)

Full source

theorem bijOn_periodicPts : BijOn f (periodicPts f) (periodicPts f) :=
  iUnion_pnat_ptsOfPeriod f ▸
    bijOn_iUnion_of_directed (directed_ptsOfPeriod_pnat f) fun i => bijOn_ptsOfPeriod f i.pos

Bijectivity of Function on Its Periodic Points

Informal description

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

Function.minimalPeriod_eq_prime_iff theorem

{p : ℕ} [hp : Fact p.Prime] : minimalPeriod f x = p ↔ IsPeriodicPt f p x ∧ ¬IsFixedPt f x

Full source

theorem minimalPeriod_eq_prime_iff {p : ℕ} [hp : Fact p.Prime] :
    minimalPeriodminimalPeriod f x = p ↔ IsPeriodicPt f p x ∧ ¬IsFixedPt f x := by
  rw [Function.isPeriodicPt_iff_minimalPeriod_dvd, Nat.dvd_prime hp.out,
    ← minimalPeriod_eq_one_iff_isFixedPt.not, or_and_right, and_not_self_iff, false_or,
    iff_self_and]
  exact fun h ↦ ne_of_eq_of_ne h hp.out.ne_one

Characterization of Minimal Period as Prime Number

Informal description

For a function $f \colon \alpha \to \alpha$, a point $x \in \alpha$, and a prime number $p$, the minimal period of $x$ under $f$ equals $p$ if and only if $x$ is a periodic point of $f$ with period $p$ but not a fixed point of $f$.

Function.minimalPeriod_eq_prime theorem

{p : ℕ} [hp : Fact p.Prime] (hper : IsPeriodicPt f p x) (hfix : ¬IsFixedPt f x) : minimalPeriod f x = p

Full source

/-- The backward direction of `minimalPeriod_eq_prime_iff`. -/
theorem minimalPeriod_eq_prime {p : ℕ} [hp : Fact p.Prime] (hper : IsPeriodicPt f p x)
    (hfix : ¬IsFixedPt f x) : minimalPeriod f x = p :=
  minimalPeriod_eq_prime_iff.mpr ⟨hper, hfix⟩

Minimal Period Equals Prime for Non-Fixed Periodic Points

Informal description

Let $f \colon \alpha \to \alpha$ be a function, $x \in \alpha$ a point, and $p$ a prime number. If $x$ is a periodic point of $f$ with period $p$ but not a fixed point of $f$, then the minimal period of $x$ under $f$ is equal to $p$.

Function.minimalPeriod_eq_prime_pow theorem

 {p k : ℕ} [hp : Fact p.Prime] (hk : ¬IsPeriodicPt f (p ^ k) x) (hk1 : IsPeriodicPt f (p ^ (k + 1)) x) :
  minimalPeriod f x = p ^ (k + 1)

Full source

theorem minimalPeriod_eq_prime_pow {p k : ℕ} [hp : Fact p.Prime] (hk : ¬IsPeriodicPt f (p ^ k) x)
    (hk1 : IsPeriodicPt f (p ^ (k + 1)) x) : minimalPeriod f x = p ^ (k + 1) := by
  apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out <;>
    rwa [← isPeriodicPt_iff_minimalPeriod_dvd]

Minimal Period Equals Prime Power When Periodicity First Occurs

Informal description

Let $f \colon \alpha \to \alpha$ be a function, $x \in \alpha$ a point, and $p$ a prime number. For any natural number $k$, if $x$ is not a periodic point of $f$ with period $p^k$ but is a periodic point with period $p^{k+1}$, then the minimal period of $x$ under $f$ is exactly $p^{k+1}$.

Function.Commute.minimalPeriod_of_comp_dvd_mul theorem

{g : α → α} (h : Commute f g) : minimalPeriod (f ∘ g) x ∣ minimalPeriod f x * minimalPeriod g x

Full source

theorem Commute.minimalPeriod_of_comp_dvd_mul {g : α → α} (h : Commute f g) :
    minimalPeriodminimalPeriod (f ∘ g) x ∣ minimalPeriod f x * minimalPeriod g x :=
  dvd_trans h.minimalPeriod_of_comp_dvd_lcm (lcm_dvd_mul _ _)

Minimal Period of Composition Divides Product 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 product of the minimal periods of $x$ under $f$ and under $g$. In other words, $$\text{minimalPeriod}(f \circ g, x) \mid \text{minimalPeriod}(f, x) \cdot \text{minimalPeriod}(g, x).$$

Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime theorem

 {g : α → α} (h : Commute f g) (hco : Coprime (minimalPeriod f x) (minimalPeriod g x)) :
  minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

Full source

theorem Commute.minimalPeriod_of_comp_eq_mul_of_coprime {g : α → α} (h : Commute f g)
    (hco : Coprime (minimalPeriod f x) (minimalPeriod g x)) :
    minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x := by
  apply h.minimalPeriod_of_comp_dvd_mul.antisymm
  suffices
    ∀ {f g : α → α},
      Commute f g →
        Coprime (minimalPeriod f x) (minimalPeriod g x) →
          minimalPeriodminimalPeriod f x ∣ minimalPeriod (f ∘ g) x from
    hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
  intro f g h hco
  refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd
  · exact (isPeriodicPt_minimalPeriod _ _).const_mul _
  · exact (isPeriodicPt_minimalPeriod _ _).mul_const _

Minimal Period of Composition Equals Product of Minimal Periods for Commuting Functions with Coprime Periods

Informal description

Let $f, g \colon \alpha \to \alpha$ be commuting functions (i.e., $f \circ g = g \circ f$). If the minimal periods of $x$ under $f$ and $g$ are coprime, then the minimal period of $x$ under the composition $f \circ g$ is equal to the product of the minimal periods under $f$ and $g$. That is, $$\text{minimalPeriod}(f \circ g, x) = \text{minimalPeriod}(f, x) \cdot \text{minimalPeriod}(g, x).$$

Function.minimalPeriod_le_card theorem

[Fintype α] : minimalPeriod f x ≤ card α

Full source

theorem minimalPeriod_le_card [Fintype α] : minimalPeriod f x ≤ card α := by
  rw [← periodicOrbit_length]
  exact List.Nodup.length_le_card nodup_periodicOrbit

Minimal Period Bound by Cardinality of Finite Type

Informal description

For any endomorphism $f \colon \alpha \to \alpha$ on a finite type $\alpha$ and any point $x \in \alpha$, the minimal period of $x$ under $f$ is at most the cardinality of $\alpha$. That is, $\text{minimalPeriod}(f, x) \leq \text{card}(\alpha)$.

Function.isPeriodicPt_factorial_card_of_mem_periodicPts theorem

[Fintype α] (h : x ∈ periodicPts f) : IsPeriodicPt f (card α)! x

Full source

theorem isPeriodicPt_factorial_card_of_mem_periodicPts [Fintype α] (h : x ∈ periodicPts f) :
    IsPeriodicPt f (card α)! x :=
  isPeriodicPt_iff_minimalPeriod_dvd.mpr
    (Nat.dvd_factorial (minimalPeriod_pos_of_mem_periodicPts h) minimalPeriod_le_card)

Periodic Points Have Factorial-of-Cardinality Period in Finite Types

Informal description

For a finite type $\alpha$, if a point $x$ is a periodic point of a function $f \colon \alpha \to \alpha$, then $x$ is a periodic point of $f$ with period $n!$, where $n$ is the cardinality of $\alpha$. In other words, $f^{[n!]}(x) = x$.

Function.mem_periodicPts_iff_isPeriodicPt_factorial_card theorem

[Fintype α] : x ∈ periodicPts f ↔ IsPeriodicPt f (card α)! x

Full source

theorem mem_periodicPts_iff_isPeriodicPt_factorial_card [Fintype α] :
    x ∈ periodicPts fx ∈ periodicPts f ↔ IsPeriodicPt f (card α)! x where
  mp := isPeriodicPt_factorial_card_of_mem_periodicPts
  mpr h := minimalPeriod_pos_iff_mem_periodicPts.mp
    (IsPeriodicPt.minimalPeriod_pos (Nat.factorial_pos _) h)

Periodic Point Criterion via Factorial of Cardinality in Finite Types

Informal description

For a finite type $\alpha$, a point $x$ is a periodic point of a function $f \colon \alpha \to \alpha$ if and only if the $(n!)$-th iterate of $f$ at $x$ equals $x$, where $n$ is the cardinality of $\alpha$. In other words: \[ x \in \text{periodicPts}(f) \leftrightarrow f^{[n!]}(x) = x \]

Function.Injective.mem_periodicPts theorem

[Finite α] (h : Injective f) (x : α) : x ∈ periodicPts f

Full source

theorem Injective.mem_periodicPts [Finite α] (h : Injective f) (x : α) : x ∈ periodicPts f := by
  obtain ⟨m, n, heq, hne⟩ : ∃ m n, f^[m] x = f^[n] x ∧ m ≠ n := by
    simpa [Injective] using not_injective_infinite_finite (f^[·] x)
  rcases lt_or_gt_of_ne hne with hlt | hlt
  · exact mk_mem_periodicPts (by omega) (iterate_cancel h heq.symm)
  · exact mk_mem_periodicPts (by omega) (iterate_cancel h heq)

All Points are Periodic for Injective Functions on Finite Types

Informal description

Let $\alpha$ be a finite type and $f : \alpha \to \alpha$ be an injective function. Then every element $x \in \alpha$ is a periodic point of $f$, i.e., $x$ belongs to the set of periodic points of $f$.

Function.injective_iff_periodicPts_eq_univ theorem

[Finite α] : Injective f ↔ periodicPts f = univ

Full source

theorem injective_iff_periodicPts_eq_univ [Finite α] : InjectiveInjective f ↔ periodicPts f = univ := by
  refine ⟨fun h ↦ eq_univ_iff_forall.mpr h.mem_periodicPts, fun h ↦ ?_⟩
  rw [Finite.injective_iff_surjective, ← range_eq_univ, ← univ_subset_iff, ← h]
  apply periodicPts_subset_range

Injectivity Equivalence via Periodic Points in Finite Types

Informal description

For a finite type $\alpha$ and a function $f : \alpha \to \alpha$, the following are equivalent: 1. The function $f$ is injective. 2. The set of periodic points of $f$ is equal to the entire type $\alpha$, i.e., $\text{periodicPts}(f) = \text{univ}$.

Function.injective_iff_iterate_factorial_card_eq_id theorem

[Fintype α] : Injective f ↔ f^[(card α)!] = id

Full source

theorem injective_iff_iterate_factorial_card_eq_id [Fintype α] :
    InjectiveInjective f ↔ f^[(card α)!] = id := by
  simp only [injective_iff_periodicPts_eq_univ, mem_periodicPts_iff_isPeriodicPt_factorial_card,
    funext_iff, eq_univ_iff_forall, IsPeriodicPt, id, IsFixedPt]

Injectivity Equivalence via Iteration of Factorial Order in Finite Types

Informal description

For a finite type $\alpha$ with a function $f : \alpha \to \alpha$, the following are equivalent: 1. The function $f$ is injective. 2. The iterate of $f$ composed $(|\alpha|)!$ times equals the identity function on $\alpha$, i.e., $f^{[|\alpha|!]} = \text{id}$.

Function.minimalPeriod_prodMap theorem

 (f : α → α) (g : β → β) (x : α × β) : minimalPeriod (Prod.map f g) x = (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Full source

theorem minimalPeriod_prodMap (f : α → α) (g : β → β) (x : α × β) :
    minimalPeriod (Prod.map f g) x = (minimalPeriod f x.1).lcm (minimalPeriod g x.2) :=
  eq_of_forall_dvd <| by cases x; simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]

Minimal Period of Product Map Equals LCM of Component Minimal Periods

Informal description

For functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, and a point $x = (x_1, x_2) \in \alpha \times \beta$, the minimal period of $x$ under the product map $(f \times g)$ is equal to the least common multiple of the minimal periods of $x_1$ under $f$ and $x_2$ under $g$. That is, $$\text{minimalPeriod}(f \times g, (x_1, x_2)) = \text{lcm}(\text{minimalPeriod}(f, x_1), \text{minimalPeriod}(g, x_2)).$$

Function.minimalPeriod_fst_dvd theorem

: minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x

Full source

theorem minimalPeriod_fst_dvd : minimalPeriodminimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x := by
  rw [minimalPeriod_prodMap]; exact Nat.dvd_lcm_left _ _

Minimal Period of First Component Divides Minimal Period of Product Map

Informal description

For functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, and a point $x = (x_1, x_2) \in \alpha \times \beta$, the minimal period of $x_1$ under $f$ divides the minimal period of $x$ under the product map $(f \times g)$. That is, $$\text{minimalPeriod}(f, x_1) \mid \text{minimalPeriod}(f \times g, x).$$

Function.minimalPeriod_snd_dvd theorem

: minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x

Full source

theorem minimalPeriod_snd_dvd : minimalPeriodminimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x := by
  rw [minimalPeriod_prodMap]; exact Nat.dvd_lcm_right _ _

Minimal Period of Second Component Divides Minimal Period of Product Map

Informal description

For functions $f : \alpha \to \alpha$ and $g : \beta \to \beta$, and a point $x = (x_1, x_2) \in \alpha \times \beta$, the minimal period of $x_2$ under $g$ divides the minimal period of $x$ under the product map $(f \times g)$. That is, $$\text{minimalPeriod}(g, x_2) \mid \text{minimalPeriod}(f \times g, (x_1, x_2)).$$