IMO 2015 Q6

The sequence $a_1, a_2, \dots$ of integers satisfies the conditions

1. $1 ≤ a_j ≤ 2015$ for all $j ≥ 1$,
2. $k + a_k ≠ l + a_l$ for all $1 ≤ k < l$.

Prove that there exist two positive integers $b$ and $N$ for which $$\left|\sum_{j=m+1}^n (a_j-b)\right| ≤ 1007^2$$ for all integers $m,n$ such that $N ≤ m < n$.

Solution

We follow solution 2 ("juggling") from https://web.evanchen.cc/exams/IMO-2015-notes.pdf.

Consider a collection of balls at different integer heights that starts out empty at time 0 and is modified at each succeeding integer time t as follows:

• If there is a ball at height 0 it is removed (caught)
• Then a ball is added at height $a_t$
• Then all balls have their height decreased by 1

Condition 1 ensures that all heights stay in [0, 2014]. Condition 2 ensures that the heights at any point in time are distinct, so we can model the collection as a finset of heights of monotonically increasing, bounded cardinality. So there is a time where the cardinality reaches a maximum; we take N to be that time and b to be that maximum cardinality. $1 ≤ b ≤ 2015$.

Let $S_t$ be the sum of heights at time $t$. The key observation is that for all $t ≥ N$ $$S_{t+1} = S_t + a_{t+1} - b$$ because 0 must be in the set of heights at time $t$ (otherwise the cardinality will increase); this height is replaced by $a_{t+1}$ and then all $b$ balls have their height decreased by 1. Thus $$\left|\sum_{j=m+1}^n (a_j-b)\right| = |S_n - S_m|.$$ Now for all $t ≥ N$, $$\sum_{i=0}^{b-1} i ≤ S_t ≤ 0 + \sum_{i=0}^{b-2} (2014-i),$$ so the absolute difference is upper-bounded by $$\sum_{i=0}^{b-2} (2014-i) - (b-1) - \sum_{i=0}^{b-2} (b-2-i) = (b-1)(2015-b) ≤ 1007^2.$$

def Imo2015Q6.Condition (a : ℕ → ℤ) : Prop

The conditions on a in the problem. We reindex a to start from 0 rather than 1; N then only has to be nonnegative rather than positive, and the sum in the problem statement is over Ico m n rather than Ioc m n.

Equations

• Imo2015Q6.Condition a = ((∀ (i : ℕ), a i ∈ Finset.Icc 1 2015) ∧ Function.Injective fun (i : ℕ) => ↑i + a i)

def Imo2015Q6.pool (a : ℕ → ℤ) : ℕ → Finset ℤ

The collection of ball heights in the solution.

Equations

• Imo2015Q6.pool a 0 = ∅
• Imo2015Q6.pool a t.succ = Finset.map (Equiv.subRight 1).toEmbedding (insert (a t) ((Imo2015Q6.pool a t).erase 0))

theorem Imo2015Q6.exists_add_eq_of_mem_pool {a : ℕ → ℤ} {t : ℕ} {z : ℤ} (hz : z ∈ pool a t) : ∃ u < t, ↑u + a u = ↑t + z

theorem Imo2015Q6.pool_subset_Icc {a : ℕ → ℤ} (ha : Condition a) {t : ℕ} : pool a t ⊆ Finset.Icc 0 2014

The ball heights are always within [0, 2014].

theorem Imo2015Q6.not_mem_pool_self {a : ℕ → ℤ} (ha : Condition a) {t : ℕ} : a t ∉ pool a t

theorem Imo2015Q6.card_pool_succ {a : ℕ → ℤ} (ha : Condition a) {t : ℕ} : (pool a (t + 1)).card = (pool a t).card + if 0 ∈ pool a t then 0 else 1

The number of balls stays unchanged if there is a ball with height 0 and increases by 1 otherwise.

theorem Imo2015Q6.monotone_card_pool {a : ℕ → ℤ} (ha : Condition a) : Monotone fun (t : ℕ) => (pool a t).card

theorem Imo2015Q6.exists_max_card_pool {a : ℕ → ℤ} (ha : Condition a) : ∃ (b : ℕ) (N : ℕ), ∀ t ≥ N, (pool a t).card = b

There exists a point where the number of balls reaches a maximum (which follows from its monotonicity and boundedness). We take its coordinates for the problem's b and N.

theorem Imo2015Q6.b_pos {a : ℕ → ℤ} (ha : Condition a) {b N : ℕ} (hbN : ∀ t ≥ N, (pool a t).card = b) : 0 < b

theorem Imo2015Q6.zero_mem_pool {a : ℕ → ℤ} (ha : Condition a) {t b N : ℕ} (hbN : ∀ t ≥ N, (pool a t).card = b) (ht : t ≥ N) : 0 ∈ pool a t

theorem Imo2015Q6.sum_sub_sum_eq_sub {a : ℕ → ℤ} (ha : Condition a) {t b N : ℕ} (hbN : ∀ t ≥ N, (pool a t).card = b) (ht : t ≥ N) : ∑ x ∈ pool a (t + 1), x - ∑ x ∈ pool a t, x = a t - ↑b

The key observation, one term of the telescoping sum for the problem's expression.

theorem Imo2015Q6.sum_telescope {a : ℕ → ℤ} (ha : Condition a) {b N : ℕ} (hbN : ∀ t ≥ N, (pool a t).card = b) {m n : ℕ} (hm : N ≤ m) (hn : m < n) : ∑ j ∈ Finset.Ico m n, (a j - ↑b) = ∑ x ∈ pool a n, x - ∑ x ∈ pool a m, x

The telescoping sum giving the part of the problem's expression within the modulus signs.

theorem Imo2015Q6.le_sum_pool {a : ℕ → ℤ} (ha : Condition a) {t b N : ℕ} (hbN : ∀ t ≥ N, (pool a t).card = b) (ht : t ≥ N) : ∑ i ∈ Finset.range b, ↑i ≤ ∑ x ∈ pool a t, x

theorem Imo2015Q6.sum_pool_le {a : ℕ → ℤ} (ha : Condition a) {t b N : ℕ} (hbN : ∀ t ≥ N, (pool a t).card = b) (ht : t ≥ N) : ∑ x ∈ pool a t, x ≤ ∑ i ∈ Finset.range (b - 1), (2014 - ↑i)

theorem Imo2015Q6.result {a : ℕ → ℤ} (ha : Condition a) : ∃ b > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n > m, |∑ j ∈ Finset.Ico m n, (a j - b)| ≤ 1007 ^ 2