IMO 2009 N5

Let $S$ be a set and $T : S → S$ be a function. Prove that there does not exist a non-constant polynomial $P ∈ ℤ[X]$ such that for every positive integer $n$, $$ \#\{x ∈ ℤ : T^n(x) = x\} = P(n). $$

Solution

We follow a variant of Solution 2 of the official solution. Namely, $p$ does not have to be prime; we have $P(0) ≡ P(n) \pmod{q}$ for any $n > 0$.

Extra lemma

theorem IMOSL.IMO2009N5.periodicOrbit_eq_iff_mem_periodicOrbit {α✝ : Type u_1} {T : α✝ → α✝} {a₀ a : α✝} (ha₀ : a₀ ∈ Function.periodicPts T) : Function.periodicOrbit T a = Function.periodicOrbit T a₀ ↔ a ∈ Function.periodicOrbit T a₀

If a₀ is T-periodic, then a has the same T-orbit as a₀ if and only if a is in the T-orbit of a₀.

Start of the problem

structure IMOSL.IMO2009N5.NiceFun (α : Type u_1) : Type u_1

We say that a function T : α → α is nice if T^n has finitely many fixed points for every positive integer n.

• toFun : α → α
• nth_fixed_pts (n : ℕ) : Finset α

  Fixed points of $T^n$, except we set the set to be empty at $0$ for convenience.

• nth_fixed_pts_zero : self.nth_fixed_pts 0 = ∅
• nth_fixed_pts_spec' (n : ℕ) (hn : n > 0) (a : α) : a ∈ self.nth_fixed_pts n ↔ Function.IsPeriodicPt self.toFun n a

instance IMOSL.IMO2009N5.NiceFun.instFunLike {α : Type u_1} : FunLike (NiceFun α) α α

Equations

• IMOSL.IMO2009N5.NiceFun.instFunLike = { coe := IMOSL.IMO2009N5.NiceFun.toFun, coe_injective' := ⋯ }

theorem IMOSL.IMO2009N5.NiceFun.nth_fixed_pts_spec {α : Type u_1} (T : NiceFun α) {n : ℕ} {a : α} (hn : n > 0) : a ∈ T.nth_fixed_pts n ↔ Function.IsPeriodicPt (⇑T) n a

nth_fixed_pts n consists of points a such that T^n(a) = a.

noncomputable def IMOSL.IMO2009N5.NiceFun.period_n_pts {α : Type u_1} (T : NiceFun α) (n : ℕ) : Finset α

The finite set of points of T-period exactly n.

Equations

• T.period_n_pts n = {a ∈ T.nth_fixed_pts n | Function.minimalPeriod (⇑T) a = n}

theorem IMOSL.IMO2009N5.NiceFun.period_zero_pts {α : Type u_1} (T : NiceFun α) : T.period_n_pts 0 = ∅

period_n_pts 0 = ∅.

theorem IMOSL.IMO2009N5.NiceFun.period_n_pts_spec {α : Type u_1} (T : NiceFun α) {n : ℕ} {a : α} (hn : n > 0) : a ∈ T.period_n_pts n ↔ Function.minimalPeriod (⇑T) a = n

The finite set period_n_pts is indeed the set of T-period n points if n > 0.

theorem IMOSL.IMO2009N5.NiceFun.period_n_pts_spec2 {α : Type u_1} (T : NiceFun α) {n : ℕ} {a : α} : a ∈ T.period_n_pts n ↔ n > 0 ∧ Function.minimalPeriod (⇑T) a = n

An alternate version of period_n_pts_spec that, in addition, says that there are no "T-period 0 points".

theorem IMOSL.IMO2009N5.NiceFun.mem_periodicPts_of_mem_period_n_pts {α : Type u_1} (T : NiceFun α) {n : ℕ} {a : α} (ha : a ∈ T.period_n_pts n) : a ∈ Function.periodicPts ⇑T

Any member of period_n_pts is a member of periodicPts T.

theorem IMOSL.IMO2009N5.NiceFun.pos_of_mem_period_n_pts {α : Type u_1} (T : NiceFun α) {n : ℕ} {a : α} (ha : a ∈ T.period_n_pts n) : n > 0

If T.period_n_pts n has an element, then n > 0.

theorem IMOSL.IMO2009N5.NiceFun.iterate_apply_mem_period_n_pts {α : Type u_1} (T : NiceFun α) {n : ℕ} {a : α} (ha : a ∈ T.period_n_pts n) (k : ℕ) : (⇑T)^[k] a ∈ T.period_n_pts n

If a has T-period n, then T^k(a) has T-period n.

Summation formula for the number of fixed points

theorem IMOSL.IMO2009N5.NiceFun.mem_nth_fixed_pts_iff_mem_period_n_pts_divisors {α : Type u_1} (T : NiceFun α) {a : α} (n : ℕ) : a ∈ T.nth_fixed_pts n ↔ ∃ d ∈ n.divisors, a ∈ T.period_n_pts d

T^n(a) = a if and only if a has T-period dividing n. Note: Due to the formulation of nth_fixed_pts and Nat.divisors, the implemented formulation works even if n = 0.

theorem IMOSL.IMO2009N5.NiceFun.period_n_pts_PairwiseDisjoint {α : Type u_1} (T : NiceFun α) (S : Set ℕ) : S.PairwiseDisjoint T.period_n_pts

The sets of points with T-period n are pairwise disjoint across all n.

theorem IMOSL.IMO2009N5.NiceFun.nth_fixed_pts_eq_disjiUnion_divisors_period_n_pts {α : Type u_1} (T : NiceFun α) (n : ℕ) : T.nth_fixed_pts n = n.divisors.disjiUnion T.period_n_pts ⋯

The set of nth fixed points is the union, over all d ∣ n, of the set of elements of T-period d.

theorem IMOSL.IMO2009N5.NiceFun.card_nth_fixed_pts_eq_sum_card_period_n_pts {α : Type u_1} (T : NiceFun α) (n : ℕ) : (T.nth_fixed_pts n).card = ∑ d ∈ n.divisors, (T.period_n_pts d).card

Summation formula for the number of points a such that T^n(a) = a. Note: This is one of the key observations used in the solution.

The number of points of period n is divisible by n.

theorem IMOSL.IMO2009N5.NiceFun.periodicOrbit_length_of_mem_period_n_pts {α : Type u_1} {n : ℕ} {a : α} (T : NiceFun α) (ha : a ∈ T.period_n_pts n) : (Function.periodicOrbit (⇑T) a).length = n

The "periodic orbit" of the points of T-period n has size n.

theorem IMOSL.IMO2009N5.NiceFun.card_period_n_pts_eq_n_mul_card_periodicOrbits {α : Type u_1} [DecidableEq α] (T : NiceFun α) (n : ℕ) : (T.period_n_pts n).card = n * (Finset.image (Function.periodicOrbit ⇑T) (T.period_n_pts n)).card

The size of period_n_pts is n times the number of corresponding orbits.

theorem IMOSL.IMO2009N5.NiceFun.n_dvd_card_period_n_pts {α : Type u_1} [DecidableEq α] (T : NiceFun α) (n : ℕ) : n ∣ (T.period_n_pts n).card

The set of points with T-period n has size divisible by n. Note: This is one of the key observations used in the solution.

theorem IMOSL.IMO2009N5.NiceFun.card_nth_fixed_pts_modeq_prime {α : Type u_1} [DecidableEq α] (T : NiceFun α) {q : ℕ} (hq : Nat.Prime q) (n : ℕ) : (T.nth_fixed_pts (n * q)).card ≡ (T.nth_fixed_pts n).card [MOD q]

For any n and for any prime q, the number of fixed points of T^n and T^{nq} are congruent modulo q.

theorem IMOSL.IMO2009N5.final_solution {α : Type u_1} [DecidableEq α] {T : NiceFun α} (h : ∃ (P : Polynomial ℤ), ∀ n > 0, ↑(T.nth_fixed_pts n).card = Polynomial.eval (↑n) P) : ∃ (N : ℕ), ∀ n > 0, (T.nth_fixed_pts n).card = N

Final solution