# Extra lemmas about periodic points #

source
theorem Function.directed_ptsOfPeriod_pnat {α : Type u_1} (f : α → α) :
Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (n : ℕ+) => ptsOfPeriod f ↑n
source
@[deprecated Function.directed_ptsOfPeriod_pnat (since := "2025-04-27")]
theorem Function.directed_ptsOfPeriod_pNat {α : Type u_1} (f : α → α) :
Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (n : ℕ+) => ptsOfPeriod f ↑n

Alias of `Function.directed_ptsOfPeriod_pnat`.

source
theorem Function.bijOn_periodicPts {α : Type u_1} (f : α → α) :
Set.BijOn f (periodicPts f) (periodicPts f)
source
theorem Function.minimalPeriod_eq_prime_iff {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)] :
minimalPeriod f x = p ↔ IsPeriodicPt f p x ∧ ¬IsFixedPt f x
source
theorem Function.minimalPeriod_eq_prime {α : Type u_1} {f : α → α} {x : α} {p : ℕ} [hp : Fact (Nat.Prime p)] (hper : IsPeriodicPt f p x) (hfix : ¬IsFixedPt f x) :
minimalPeriod f x = p

The backward direction of `minimalPeriod_eq_prime_iff`.

source
theorem Function.minimalPeriod_eq_prime_pow {α : Type u_1} {f : α → α} {x : α} {p k : ℕ} [hp : Fact (Nat.Prime p)] (hk : ¬IsPeriodicPt f (p ^ k) x) (hk1 : IsPeriodicPt f (p ^ (k + 1)) x) :
minimalPeriod f x = p ^ (k + 1)
source
theorem Function.Commute.minimalPeriod_of_comp_dvd_mul {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : Function.Commute f g) :
minimalPeriod (f ∘ g) x ∣ minimalPeriod f x * minimalPeriod g x
source
theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime {α : Type u_1} {f : α → α} {x : α} {g : α → α} (h : Function.Commute f g) (hco : (minimalPeriod f x).Coprime (minimalPeriod g x)) :
minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x
source
theorem Function.minimalPeriod_le_card {α : Type u_1} {f : α → α} {x : α} [Fintype α] :
minimalPeriod f x ≤ Fintype.card α
source
theorem Function.isPeriodicPt_factorial_card_of_mem_periodicPts {α : Type u_1} {f : α → α} {x : α} [Fintype α] (h : x ∈ periodicPts f) :
IsPeriodicPt f (Fintype.card α).factorial x
source
theorem Function.mem_periodicPts_iff_isPeriodicPt_factorial_card {α : Type u_1} {f : α → α} {x : α} [Fintype α] :
x ∈ periodicPts f ↔ IsPeriodicPt f (Fintype.card α).factorial x
source
theorem Function.Injective.mem_periodicPts {α : Type u_1} {f : α → α} [Finite α] (h : Injective f) (x : α) :
x ∈ periodicPts f
source
@[deprecated Function.Injective.mem_periodicPts (since := "2025-04-27")]
theorem Function.mem_periodicPts_of_injective {α : Type u_1} {f : α → α} [Finite α] (h : Injective f) (x : α) :
x ∈ periodicPts f

Alias of `Function.Injective.mem_periodicPts`.

source
theorem Function.injective_iff_periodicPts_eq_univ {α : Type u_1} {f : α → α} [Finite α] :
Injective f ↔ periodicPts f = Set.univ
source
@[deprecated Function.injective_iff_periodicPts_eq_univ (since := "2025-04-27")]
theorem Function.injective_iff_forall_mem_periodicPts {α : Type u_1} {f : α → α} [Finite α] :
Injective f ↔ periodicPts f = Set.univ

Alias of `Function.injective_iff_periodicPts_eq_univ`.

source
theorem Function.injective_iff_iterate_factorial_card_eq_id {α : Type u_1} {f : α → α} [Fintype α] :
Injective f ↔ f^[(Fintype.card α).factorial] = id
source
theorem Function.minimalPeriod_prodMap {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (x : α × β) :
minimalPeriod (Prod.map f g) x = (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
source
theorem Function.minimalPeriod_fst_dvd {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} :
minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x
source
theorem Function.minimalPeriod_snd_dvd {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} :
minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x