Extra lemmas about periodic points #
theorem
Function.directed_ptsOfPeriod_pNat
{α : Type u_1}
(f : α → α)
:
Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (n : ℕ+) => Function.ptsOfPeriod f ↑n
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_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 : (Function.minimalPeriod f x).Coprime (Function.minimalPeriod g x))
:
Function.minimalPeriod (f ∘ g) x = Function.minimalPeriod f x * Function.minimalPeriod g x
theorem
Function.minimalPeriod_prod_map
{α : Type u_1}
{β : Type u_2}
(f : α → α)
(g : β → β)
(x : α × β)
:
Function.minimalPeriod (Prod.map f g) x = (Function.minimalPeriod f x.1).lcm (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