IMO 2001 Q4

Let $n > 1$ be an odd integer and let $c_1, c_2, \dots, c_n$ be integers. For each permutation $a = (a_1, a_2, \dots, a_n)$ of $\{1, 2, \dots, n\}$, define $S(a) = \sum_{i=1}^n c_i a_i$. Prove that there exist two permutations $a ≠ b$ of $\{1, 2, \dots, n\}$ such that $n!$ is a divisor of $S(a) - S(b)$.

Solution

Suppose for contradiction that all the $S(a)$ have distinct residues modulo $n!$, then $$\sum_{i=0}^{n!-1} i ≡ \sum_a S(a) = \sum_i c_i \sum_a a_i = (n-1)! \frac{n(n+1)}2 \sum_i c_i$$ $$= n! \frac{n+1}2 \sum_i c_i ≡ 0 \bmod n$$ where the last equality relies on $n$ being odd. But $\sum_{i=0}^{n!-1} i = \frac{n!(n!-1)}2$ is not divisible by $n!$, since the quotient is $\frac{n!-1}2$ and $n!$ is even when $n > 1$.

def Imo2001Q4.S {n : ℕ} (c : Fin n → ℤ) (a : Equiv.Perm (Fin n)) : ℤ

The function S in the problem. As implemented here it accepts a permutation of Fin n rather than Icc 1 n, and as such contains + 1 to compensate.

Equations

• Imo2001Q4.S c a = ∑ i : Fin n, c i * (↑↑(a i) + 1)

theorem Imo2001Q4.sum_range_modEq_sum_of_contra {n : ℕ} {c : Fin n → ℤ} (hS : ¬∃ (a : Equiv.Perm (Fin n)) (b : Equiv.Perm (Fin n)), a ≠ b ∧ ↑n.factorial ∣ S c a - S c b) : ↑n.factorial * (↑n.factorial - 1) / 2 ≡ ∑ a : Equiv.Perm (Fin n), S c a [ZMOD ↑n.factorial]

Assuming the opposite of what is to be proved, the sum of S over all permutations is congruent to the sum of all residues modulo n!, i.e. n! * (n! - 1) / 2.

theorem Imo2001Q4.sum_perm_add_one {n : ℕ} {i : Fin n} (hn : 1 ≤ n) : ∑ a : Equiv.Perm (Fin n), (↑(a i) + 1) = (n - 1).factorial * (n * (n + 1) / 2)

The sum over all permutations of Icc 1 n of the entry at any fixed position is (n - 1)! * (n * (n + 1) / 2).

theorem Imo2001Q4.sum_modEq_zero_of_odd {n : ℕ} {c : Fin n → ℤ} (hn : Odd n) : ∑ a : Equiv.Perm (Fin n), S c a ≡ 0 [ZMOD ↑n.factorial]

For odd n, the sum of S over all permutations is divisible by n!.

theorem Imo2001Q4.result {n : ℕ} {c : Fin n → ℤ} (hn : Odd n ∧ 1 < n) : ∃ (a : Equiv.Perm (Fin n)) (b : Equiv.Perm (Fin n)), a ≠ b ∧ ↑n.factorial ∣ S c a - S c b