IMO 2024 Q3

Let $a_1, a_2, a_3, \ldots$ be an infinite sequence of positive integers, and let $N$ be a positive integer. Suppose that, for each $n > N$, $a_n$ is equal to the number of times $a_{n-1}$ appears in the list $a_1, a_2, \ldots, a_{n-1}$.

Prove that at least one of the sequences $a_1, a_3, a_5, \ldots$ and $a_2, a_4, a_6, \ldots$ is eventually periodic.

We follow Solution 1 from the official solutions. We show that the positive integers up to some positive integer $k$ (referred to as small numbers) all appear infinitely often in the given sequence while all larger positive integers appear only finitely often and then that the sequence eventually alternates between small numbers and larger integers. A further detailed analysis of the eventual behavior of the sequence ends up showing that the sequence of small numbers is eventually periodic with period at most $k$ (in fact exactly $k$).

def Imo2024Q3.Condition (a : ℕ → ℕ) (N : ℕ) : Prop

The condition of the problem. Following usual Lean conventions, this is expressed with indices starting from 0, rather than from 1 as in the informal statment (but N remains as the index of the last term for which a n is not defined in terms of previous terms).

Equations

• Imo2024Q3.Condition a N = ((∀ (i : ℕ), 0 < a i) ∧ ∀ (n : ℕ), N < n → a n = (Finset.filter (fun (i : ℕ) => a i = a (n - 1)) (Finset.range n)).card)

def Imo2024Q3.EventuallyPeriodic (b : ℕ → ℕ) : Prop

The property of a sequence being eventually periodic.

Equations

• Imo2024Q3.EventuallyPeriodic b = ∃ (p : ℕ) (M : ℕ), 0 < p ∧ ∀ (m : ℕ), M ≤ m → b (m + p) = b m

Definitions and lemmas about the sequence that do not actually need the condition of

the problem

def Imo2024Q3.M (a : ℕ → ℕ) (N : ℕ) : ℕ

A number greater than any of the initial terms a 0 through a N (otherwise arbitrary).

Equations

• Imo2024Q3.M a N = (Finset.range (N + 1)).sup a + 1

theorem Imo2024Q3.M_pos (a : ℕ → ℕ) (N : ℕ) : 0 < M a N

theorem Imo2024Q3.one_le_M (a : ℕ → ℕ) (N : ℕ) : 1 ≤ M a N

theorem Imo2024Q3.apply_lt_M_of_le_N (a : ℕ → ℕ) {N i : ℕ} (h : i ≤ N) : a i < M a N

theorem Imo2024Q3.N_lt_of_M_le_apply {a : ℕ → ℕ} {N i : ℕ} (h : M a N ≤ a i) : N < i

theorem Imo2024Q3.ne_zero_of_M_le_apply {a : ℕ → ℕ} {N i : ℕ} (h : M a N ≤ a i) : i ≠ 0

theorem Imo2024Q3.apply_lt_of_M_le_apply {a : ℕ → ℕ} {N i j : ℕ} (hi : M a N ≤ a i) (hj : j ≤ N) : a j < a i

theorem Imo2024Q3.apply_ne_of_M_le_apply {a : ℕ → ℕ} {N i j : ℕ} (hi : M a N ≤ a i) (hj : j ≤ N) : a j ≠ a i

theorem Imo2024Q3.toFinset_card_pos {a : ℕ → ℕ} {i : ℕ} (hf : {j : ℕ | a j = a i}.Finite) : 0 < hf.toFinset.card

theorem Imo2024Q3.apply_nth_zero (a : ℕ → ℕ) (i : ℕ) : a (Nat.nth (fun (x : ℕ) => a x = a i) 0) = a i

theorem Imo2024Q3.map_add_one_range (p : ℕ → Prop) [DecidablePred p] (n : ℕ) (h0 : ¬p 0) : Finset.map { toFun := fun (x : ℕ) => x + 1, inj' := ⋯ } (Finset.filter (fun (x : ℕ) => p (x + 1)) (Finset.range n)) = Finset.filter (fun (x : ℕ) => p x) (Finset.range (n + 1))

The basic structure of the sequence, eventually alternating small and large numbers

theorem Imo2024Q3.Condition.pos {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) : 0 < a n

@[simp]

theorem Imo2024Q3.Condition.apply_ne_zero {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) : a n ≠ 0

theorem Imo2024Q3.Condition.one_le_apply {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) : 1 ≤ a n

theorem Imo2024Q3.Condition.apply_eq_card {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (h : N < n) : a n = (Finset.filter (fun (i : ℕ) => a i = a (n - 1)) (Finset.range n)).card

theorem Imo2024Q3.Condition.apply_add_one_eq_card {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (h : N ≤ n) : a (n + 1) = (Finset.filter (fun (i : ℕ) => a i = a n) (Finset.range (n + 1))).card

@[simp]

theorem Imo2024Q3.Condition.nth_apply_eq_zero {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) : Nat.nth (fun (x : ℕ) => a x = 0) n = 0

theorem Imo2024Q3.Condition.nth_apply_add_one_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (h : N ≤ n) : Nat.nth (fun (x : ℕ) => a x = a n) (a (n + 1) - 1) = n

theorem Imo2024Q3.Condition.apply_nth_add_one_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {m n : ℕ} (hfc : ∀ (hf : {i : ℕ | a i = m}.Finite), n < hf.toFinset.card) (hn : N ≤ Nat.nth (fun (x : ℕ) => a x = m) n) : a (Nat.nth (fun (x : ℕ) => a x = m) n + 1) = n + 1

theorem Imo2024Q3.Condition.apply_nth_add_one_eq_of_infinite {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {m n : ℕ} (hi : {i : ℕ | a i = m}.Infinite) (hn : N ≤ Nat.nth (fun (x : ℕ) => a x = m) n) : a (Nat.nth (fun (x : ℕ) => a x = m) n + 1) = n + 1

theorem Imo2024Q3.Condition.apply_nth_add_one_eq_of_lt {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {m n : ℕ} (hn : N < Nat.nth (fun (x : ℕ) => a x = m) n) : a (Nat.nth (fun (x : ℕ) => a x = m) n + 1) = n + 1

theorem Imo2024Q3.Condition.lt_toFinset_card {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : M a N ≤ a (j + 1)) (hf : {i : ℕ | a i = a j}.Finite) : M a N - 1 < hf.toFinset.card

theorem Imo2024Q3.Condition.nth_ne_zero_of_M_le_of_lt {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i k : ℕ} (hi : M a N ≤ a i) (hk : k < a (i + 1)) : Nat.nth (fun (x : ℕ) => a x = a i) k ≠ 0

theorem Imo2024Q3.Condition.apply_add_one_lt_of_apply_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hi : N ≤ i) (hij : i < j) (ha : a i = a j) : a (i + 1) < a (j + 1)

theorem Imo2024Q3.Condition.apply_add_one_ne_of_apply_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hi : N ≤ i) (hj : N ≤ j) (hij : i ≠ j) (ha : a i = a j) : a (i + 1) ≠ a (j + 1)

theorem Imo2024Q3.Condition.exists_infinite_setOf_apply_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : ∃ (m : ℕ), {i : ℕ | a i = m}.Infinite

theorem Imo2024Q3.Condition.nonempty_setOf_infinite_setOf_apply_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : {m : ℕ | {i : ℕ | a i = m}.Infinite}.Nonempty

theorem Imo2024Q3.Condition.injOn_setOf_apply_add_one_eq_of_M_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (h : M a N ≤ n) : Set.InjOn a {i : ℕ | a (i + 1) = n}

theorem Imo2024Q3.Condition.empty_consecutive_apply_ge_M {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : {i : ℕ | M a N ≤ a i ∧ M a N ≤ a (i + 1)} = ∅

theorem Imo2024Q3.Condition.card_lt_M_of_M_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (h : M a N ≤ n) : ∃ (hf : {i : ℕ | a i = n}.Finite), hf.toFinset.card < M a N

theorem Imo2024Q3.Condition.bddAbove_setOf_infinite_setOf_apply_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : BddAbove {m : ℕ | {i : ℕ | a i = m}.Infinite}

theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_anti {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j k : ℕ} (hj : 0 < j) (hk : {i : ℕ | a i = k}.Infinite) (hjk : j ≤ k) : {i : ℕ | a i = j}.Infinite

The definitions of small, medium and big numbers and the eventual alternation

noncomputable def Imo2024Q3.Condition.k (a : ℕ → ℕ) : ℕ

The largest number to appear infinitely often.

Equations

• Imo2024Q3.Condition.k a = sSup {m : ℕ | {i : ℕ | a i = m}.Infinite}

def Imo2024Q3.Condition.Small (a : ℕ → ℕ) (j : ℕ) : Prop

Small numbers are those that are at most k (that is, those that appear infinitely often).

Equations

• Imo2024Q3.Condition.Small a j = (j ≤ Imo2024Q3.Condition.k a)

theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_k {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : {i : ℕ | a i = k a}.Infinite

theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_iff_small {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (hj : 0 < j) : {i : ℕ | a i = j}.Infinite ↔ Small a j

theorem Imo2024Q3.Condition.finite_setOf_apply_eq_iff_not_small {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (hj : 0 < j) : {i : ℕ | a i = j}.Finite ↔ ¬Small a j

theorem Imo2024Q3.Condition.finite_setOf_apply_eq_k_add_one {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : {i : ℕ | a i = k a + 1}.Finite

theorem Imo2024Q3.Condition.finite_setOf_k_lt_card {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : {m : ℕ | ∀ (hf : {i : ℕ | a i = m}.Finite), k a < hf.toFinset.card}.Finite

There are only finitely many m that appear more than k times.

theorem Imo2024Q3.Condition.bddAbove_setOf_k_lt_card {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : BddAbove {m : ℕ | ∀ (hf : {i : ℕ | a i = m}.Finite), k a < hf.toFinset.card}

theorem Imo2024Q3.Condition.k_pos {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : 0 < k a

theorem Imo2024Q3.Condition.small_one {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : Small a 1

theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_one {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : {i : ℕ | a i = 1}.Infinite

noncomputable def Imo2024Q3.Condition.l (a : ℕ → ℕ) : ℕ

The largest number to appear more than k times.

Equations

• Imo2024Q3.Condition.l a = sSup {m : ℕ | ∀ (hf : {i : ℕ | a i = m}.Finite), Imo2024Q3.Condition.k a < hf.toFinset.card}

def Imo2024Q3.Condition.Medium (a : ℕ → ℕ) (j : ℕ) : Prop

Medium numbers are those that are more than k but at most l (and include all numbers appearing finitely often but more than k times).

Equations

• Imo2024Q3.Condition.Medium a j = (Imo2024Q3.Condition.k a < j ∧ j ≤ Imo2024Q3.Condition.l a)

def Imo2024Q3.Condition.Big (a : ℕ → ℕ) (j : ℕ) : Prop

Big numbers are those greater than l (thus, appear at most k times).

Equations

• Imo2024Q3.Condition.Big a j = (Imo2024Q3.Condition.l a < j)

theorem Imo2024Q3.Condition.k_le_l {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : k a ≤ l a

theorem Imo2024Q3.Condition.k_lt_of_big {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : Big a j) : k a < j

theorem Imo2024Q3.Condition.pos_of_big {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : Big a j) : 0 < j

theorem Imo2024Q3.Condition.not_small_of_big {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : Big a j) : ¬Small a j

theorem Imo2024Q3.Condition.exists_card_le_of_big {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : Big a j) : ∃ (hf : {i : ℕ | a i = j}.Finite), hf.toFinset.card ≤ k a

noncomputable def Imo2024Q3.Condition.N'aux (a : ℕ → ℕ) (N : ℕ) : ℕ

N'aux is such that, by position N'aux, every medium number has made all its appearances and every small number has appeared more than max(k, N+1) times.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Imo2024Q3.Condition.N' (a : ℕ → ℕ) (N : ℕ) : ℕ

N' is such that, by position N', every medium number has made all its appearances and every small number has appeared more than max(k, N+1) times; furthermore, a N' is small (which means that every subsequent big number is preceded by a small number).

Equations

• Imo2024Q3.Condition.N' a N = Imo2024Q3.Condition.N'aux a N + if Imo2024Q3.Condition.Small a (a (Imo2024Q3.Condition.N'aux a N + 1)) then 1 else 2

theorem Imo2024Q3.Condition.not_medium_of_N'aux_lt {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : N'aux a N < j) : ¬Medium a (a j)

theorem Imo2024Q3.Condition.small_or_big_of_N'aux_lt {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : N'aux a N < j) : Small a (a j) ∨ Big a (a j)

theorem Imo2024Q3.Condition.small_or_big_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : N' a N ≤ j) : Small a (a j) ∨ Big a (a j)

theorem Imo2024Q3.Condition.nth_sup_k_N_add_one_le_N'aux_of_small {a : ℕ → ℕ} {N j : ℕ} (h : Small a j) : Nat.nth (fun (x : ℕ) => a x = j) (k a ⊔ (N + 1)) ≤ N'aux a N

theorem Imo2024Q3.Condition.nth_sup_k_le_N'aux_of_small {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : Small a j) : Nat.nth (fun (x : ℕ) => a x = j) (k a) ≤ N'aux a N

theorem Imo2024Q3.Condition.nth_sup_N_add_one_le_N'aux_of_small {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {j : ℕ} (h : Small a j) : Nat.nth (fun (x : ℕ) => a x = j) (N + 1) ≤ N'aux a N

theorem Imo2024Q3.Condition.N_lt_N'aux {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : N < N'aux a N

theorem Imo2024Q3.Condition.N_lt_N' {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : N < N' a N

N is less than N'.

theorem Imo2024Q3.Condition.lt_card_filter_eq_of_small_nth_lt {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j t : ℕ} (hj0 : 0 < j) (h : Small a j) (ht : Nat.nth (fun (x : ℕ) => a x = j) t < i) : t < (Finset.filter (fun (m : ℕ) => a m = j) (Finset.range i)).card

theorem Imo2024Q3.Condition.k_lt_card_filter_eq_of_small_of_N'aux_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hj0 : 0 < j) (h : Small a j) (hN'aux : N'aux a N < i) : k a < (Finset.filter (fun (m : ℕ) => a m = j) (Finset.range i)).card

theorem Imo2024Q3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'aux_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hj0 : 0 < j) (h : Small a j) (hN'aux : N'aux a N < i) : N + 1 < (Finset.filter (fun (m : ℕ) => a m = j) (Finset.range i)).card

theorem Imo2024Q3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hj0 : 0 < j) (h : Small a j) (hN' : N' a N < i) : N + 1 < (Finset.filter (fun (m : ℕ) => a m = j) (Finset.range i)).card

theorem Imo2024Q3.Condition.apply_add_one_big_of_apply_small_of_N'aux_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Small a (a i)) (hN'aux : N'aux a N ≤ i) : Big a (a (i + 1))

theorem Imo2024Q3.Condition.apply_add_one_big_of_apply_small_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Small a (a i)) (hN' : N' a N ≤ i) : Big a (a (i + 1))

theorem Imo2024Q3.Condition.apply_add_one_small_of_apply_big_of_N'aux_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Big a (a i)) (hN'aux : N'aux a N ≤ i) : Small a (a (i + 1))

theorem Imo2024Q3.Condition.apply_add_one_small_of_apply_big_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Big a (a i)) (hN' : N' a N ≤ i) : Small a (a (i + 1))

theorem Imo2024Q3.Condition.apply_add_two_small_of_apply_small_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Small a (a i)) (hN' : N' a N ≤ i) : Small a (a (i + 2))

theorem Imo2024Q3.Condition.small_apply_N' {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) : Small a (a (N' a N))

a (N' a N) is a small number.

theorem Imo2024Q3.Condition.small_apply_N'_add_iff_even {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} : Small a (a (N' a N + n)) ↔ Even n

theorem Imo2024Q3.Condition.small_apply_add_two_mul_iff_small {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (m : ℕ) (hN' : N' a N ≤ n) : Small a (a (n + 2 * m)) ↔ Small a (a n)

theorem Imo2024Q3.Condition.apply_sub_one_small_of_apply_big_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Big a (a i)) (hN' : N' a N ≤ i) : Small a (a (i - 1))

theorem Imo2024Q3.Condition.apply_sub_one_big_of_apply_small_of_N'_lt {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Small a (a i)) (hN' : N' a N < i) : Big a (a (i - 1))

theorem Imo2024Q3.Condition.apply_sub_two_small_of_apply_small_of_N'_lt {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Small a (a i)) (hN' : N' a N < i) : Small a (a (i - 2))

theorem Imo2024Q3.Condition.N_add_one_lt_apply_of_apply_big_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Big a (a i)) (hN' : N' a N ≤ i) : N + 1 < a i

theorem Imo2024Q3.Condition.setOf_apply_eq_of_apply_big_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (h : Big a (a i)) (hN' : N' a N ≤ i) : {j : ℕ | a j = a i} = {j : ℕ | N < j ∧ Small a (a (j - 1)) ∧ a i = (Finset.filter (fun (t : ℕ) => a t = a (j - 1)) (Finset.range j)).card}

theorem Imo2024Q3.Condition.N_lt_of_apply_eq_of_apply_big_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hj : a j = a i) (h : Big a (a i)) (hN' : N' a N ≤ i) : N < j

theorem Imo2024Q3.Condition.small_apply_sub_one_of_apply_eq_of_apply_big_of_N'_le {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hj : a j = a i) (h : Big a (a i)) (hN' : N' a N ≤ i) : Small a (a (j - 1))

The main lemmas leading to the required result

theorem Imo2024Q3.Condition.apply_add_one_eq_card_small_le_card_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (hi : N' a N < i) (hib : Big a (a i)) : a (i + 1) = (Finset.filter (fun (m : ℕ) => a i ≤ (Finset.filter (fun (j : ℕ) => a j = m) (Finset.range i)).card) (Finset.range (k a + 1))).card

Lemma 1 from the informal solution.

theorem Imo2024Q3.Condition.apply_eq_card_small_le_card_eq_of_small {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i : ℕ} (hi : N' a N + 1 < i) (his : Small a (a i)) : a i = (Finset.filter (fun (m : ℕ) => a (i - 1) ≤ (Finset.filter (fun (j : ℕ) => a j = m) (Finset.range i)).card) (Finset.range (k a + 1))).card

Similar to Lemma 1 from the informal solution, but with a Small hypothesis instead of Big and considering a range one larger (the form needed for Lemma 2).

theorem Imo2024Q3.Condition.exists_apply_sub_two_eq_of_apply_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {i j : ℕ} (hi : N' a N + 2 < i) (hijlt : i < j) (his : Small a (a i)) (hijeq : a i = a j) (hij1 : ∀ (t : ℕ), Small a t → (Finset.filter (fun (x : ℕ) => a x = t) (Finset.Ico i j)).card ≤ 1) : ∃ t ∈ Finset.Ico i j, a (i - 2) = a t

Lemma 2 from the informal solution.

def Imo2024Q3.Condition.pSet (a : ℕ → ℕ) (n : ℕ) : Set ℕ

The indices, minus n, of small numbers appearing for the second or subsequent time at or after a n.

Equations

• Imo2024Q3.Condition.pSet a n = {t : ℕ | ∃ i ∈ Finset.Ico n (n + t), Imo2024Q3.Condition.Small a (a i) ∧ a (n + t) = a i}

noncomputable def Imo2024Q3.Condition.p (a : ℕ → ℕ) (n : ℕ) : ℕ

The index, minus n, of the second appearance of the first small number to appear twice at or after a n. This is only used for small a n with N' a N + 2 < n.

Equations

• Imo2024Q3.Condition.p a n = sInf (Imo2024Q3.Condition.pSet a n)

theorem Imo2024Q3.Condition.nonempty_pSet {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) : (pSet a n).Nonempty

theorem Imo2024Q3.Condition.exists_mem_Ico_small_and_apply_add_p_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) : ∃ i ∈ Finset.Ico n (n + p a n), Small a (a i) ∧ a (n + p a n) = a i

theorem Imo2024Q3.Condition.p_pos {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) : 0 < p a n

theorem Imo2024Q3.Condition.card_filter_apply_eq_Ico_add_p_le_one {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) (n : ℕ) {j : ℕ} (hjs : Small a j) : (Finset.filter (fun (i : ℕ) => a i = j) (Finset.Ico n (n + p a n))).card ≤ 1

theorem Imo2024Q3.Condition.apply_add_p_eq {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (hn : N' a N + 2 < n) (hs : Small a (a n)) : a (n + p a n) = a n

theorem Imo2024Q3.Condition.even_p {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (hn : N' a N + 2 < n) (hs : Small a (a n)) : Even (p a n)

theorem Imo2024Q3.Condition.p_le_two_mul_k {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (hn : N' a N + 2 < n) (hs : Small a (a n)) : p a n ≤ 2 * k a

theorem Imo2024Q3.Condition.p_apply_sub_two_le_p_apply {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (hn : N' a N + 4 < n) (hs : Small a (a n)) : p a (n - 2) ≤ p a n

theorem Imo2024Q3.Condition.p_apply_le_p_apply_add_two {a : ℕ → ℕ} {N : ℕ} (hc : Condition a N) {n : ℕ} (hn : N' a N + 2 < n) (hs : Small a (a n)) : p a n ≤ p a (n + 2)

theorem Imo2024Q3.Condition.exists_p_eq (a : ℕ → ℕ) (N : ℕ) (hc : Condition a N) : ∃ (b : ℕ) (c : ℕ), ∀ (n : ℕ), b < n → p a (N' a N + 2 * n) = c

theorem Imo2024Q3.Condition.exists_a_apply_add_eq (a : ℕ → ℕ) (N : ℕ) (hc : Condition a N) : ∃ (b : ℕ) (c : ℕ), 0 < c ∧ ∀ (n : ℕ), b < n → a (N' a N + 2 * n + 2 * c) = a (N' a N + 2 * n)

theorem Imo2024Q3.result {a : ℕ → ℕ} {N : ℕ} (h : Condition a N) : (EventuallyPeriodic fun (i : ℕ) => a (2 * i)) ∨ EventuallyPeriodic fun (i : ℕ) => a (2 * i + 1)