FrobeniusPeriodCount.lean

1 import Mathlib.NumberTheory.ArithmeticFunction.Moebius
2 import Mathlib.Dynamics.PeriodicPts.Lemmas
3 import Mathlib.Data.ZMod.QuotientGroup
4 import Mathlib.Tactic
5 
6 /-! Exact-period counting for finite dynamical systems.  The count is the
7 cardinality of an actual subtype, not a recurrence defined to force inversion. -/
8 set_option autoImplicit false
9 namespace PaperXI.FrobeniusPeriodCount
10 open Function Finset
11 open scoped Classical
12 
13 variable {X : Type*} [Finite X]
14 
15 noncomputable def exactCount (f : X → X) (n : ℕ) : ℕ :=
16   Nat.card {x : X // minimalPeriod f x = n}
17 
18 noncomputable def fixedCount (f : X → X) (n : ℕ) : ℕ :=
19   Nat.card {x : X // IsPeriodicPt f n x}
20 
21 omit [Finite X] in
22 lemma exactCount_eq_filter (f : X → X) (n : ℕ) [Fintype X] :
23     exactCount f n = (univ.filter (fun x => minimalPeriod f x = n)).card := by
24   classical
25   simp [exactCount, Nat.card_eq_fintype_card, Fintype.card_subtype]
26 
27 omit [Finite X] in
28 lemma fixedCount_eq_filter (f : X → X) (n : ℕ) [Fintype X] :
29     fixedCount f n = (univ.filter (fun x => IsPeriodicPt f n x)).card := by
30   classical
31   simp [fixedCount, Nat.card_eq_fintype_card, Fintype.card_subtype]
32 
33 /-- Partition points fixed by the nth iterate by their genuine minimal period. -/
34 theorem sum_exactCount (f : X → X) (n : ℕ) (hn : 0 < n) :
35     ∑ d ∈ n.divisors, exactCount f d = fixedCount f n := by
36   classical
37   let := Fintype.ofFinite X
38   let S := univ.filter (fun x : X => IsPeriodicPt f n x)
39   have hm : ∀ x ∈ S, minimalPeriod f x ∈ n.divisors := by
40     intro x hx
41     exact Nat.mem_divisors.mpr ⟨(mem_filter.mp hx).2.minimalPeriod_dvd, hn.ne'⟩
42   have hs := sum_fiberwise_of_maps_to hm (fun _ => (1 : ℕ))
43   simp only [sum_const, smul_eq_mul, mul_one] at hs
44   rw [fixedCount_eq_filter]
45   change ∑ d ∈ n.divisors, exactCount f d = S.card
46   rw [← hs]
47   apply sum_congr rfl
48   intro d hd
49   rw [exactCount_eq_filter]
50   congr 1
51   ext x
52   simp only [S, mem_filter, mem_univ, true_and]
53   constructor
54   · intro hx
55     exact ⟨isPeriodicPt_iff_minimalPeriod_dvd.mpr (hx ▸ (Nat.mem_divisors.mp hd).1), hx⟩
56   · exact fun hx => hx.2
57 
58 /-- Möbius inversion for actual exact-period points of a finite map. -/
59 theorem moebius_exactCount (f : X → X) (n : ℕ) (hn : 0 < n) :
60     (exactCount f n : ℤ) =
61       ∑ d ∈ n.divisors, ArithmeticFunction.moebius d * (fixedCount f (n / d) : ℤ) := by
62   have hsum : ∀ k > 0, ∑ d ∈ k.divisors, (exactCount f d : ℤ) = (fixedCount f k : ℤ) := by
63     intro k hk
64     exact_mod_cast sum_exactCount f k hk
65   have h := ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq.mp hsum n hn
66   calc
67     (exactCount f n : ℤ) =
68         ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * (fixedCount f x.2 : ℤ) := by
69       simpa only [Int.cast_id] using h.symm
70     _ = _ := Nat.sum_divisorsAntidiagonal
71       (fun d k => ArithmeticFunction.moebius d * (fixedCount f k : ℤ))
72 
73 
74 /-- The permutation restricted to points of exact period n. -/
75 noncomputable def regularPerm (e : Equiv.Perm X) (n : ℕ) :
76     Equiv.Perm {x : X // minimalPeriod e x = n} :=
77   e.subtypePerm (fun x => by rw [minimalPeriod_apply (e.injective.mem_periodicPts x)])
78 
79 /-- Number of genuine orbits on exact-period points. -/
80 noncomputable def orbitCount (e : Equiv.Perm X) (n : ℕ) : ℕ :=
81   Nat.card (MulAction.orbitRel.Quotient (Subgroup.zpowers (regularPerm e n))
82     {x : X // minimalPeriod e x = n})
83 
84 theorem regularPerm_minimalPeriod (e : Equiv.Perm X) (n : ℕ)
85     (x : {x : X // minimalPeriod e x = n}) :
86     minimalPeriod (regularPerm e n) x = n := by
87   have hs : Semiconj Subtype.val (regularPerm e n) e := fun _ => rfl
88   have hp : minimalPeriod (regularPerm e n) x = minimalPeriod e x.val := by
89     apply minimalPeriod_eq_minimalPeriod_iff.mpr
90     intro k
91     change ((regularPerm e n)^[k] x = x) ↔ e^[k] x.val = x.val
92     rw [← Subtype.val_inj, hs.iterate_right k x]
93   exact hp.trans x.property
94 
95 /-- Every exact-period orbit has n elements, including the n=1 fixed-point case. -/
96 theorem exactCount_eq_orbitCount_mul (e : Equiv.Perm X) (n : ℕ) :
97     exactCount e n = orbitCount e n * n := by
98   classical
99   let Y := {x : X // minimalPeriod e x = n}
100   let e' := regularPerm e n
101   let G := Subgroup.zpowers e'
102   let Q := MulAction.orbitRel.Quotient G Y
103   let := Fintype.ofFinite Y
104   let := Fintype.ofFinite Q
105   let (y : Y) : Fintype (MulAction.orbit G y) := Fintype.ofFinite _
106   have hc (y : Y) : Fintype.card (MulAction.orbit G y) = n := by
107     calc
108       _ = minimalPeriod e' y := (MulAction.minimalPeriod_eq_card e' y).symm
109       _ = n := regularPerm_minimalPeriod e n y
110   calc
111     exactCount e n = Fintype.card Y := Nat.card_eq_fintype_card
112     _ = Fintype.card ((w : Q) × MulAction.orbit G (Quotient.out w)) :=
113       Fintype.card_congr (MulAction.selfEquivSigmaOrbits G Y)
114     _ = ∑ w : Q, Fintype.card (MulAction.orbit G (Quotient.out w)) := Fintype.card_sigma
115     _ = Fintype.card Q * n := by simp only [hc, sum_const, card_univ, smul_eq_mul]
116     _ = orbitCount e n * n := by rw [orbitCount, Nat.card_eq_fintype_card]
117 
118 /-- Integer divisibility follows from orbit cardinality, not from rounding a sum. -/
119 theorem period_dvd_exactCount (e : Equiv.Perm X) (n : ℕ) :
120     n ∣ exactCount e n := by
121   rw [exactCount_eq_orbitCount_mul]
122   exact dvd_mul_left n _
123 
124 end PaperXI.FrobeniusPeriodCount
125 

Back to source controls