IMO 2011 A2

Let $N$ be a non-negative integer. Determine all sequences $(x_1, x_2, …, x_{N + 1})$ of positive integers such that for every positive integer $n$, there exists an integer $a$ with $$ x_1^n + 2 x_2^n + … + (N + 1) x_{N + 1}^n = a^{n + 1} + 1. $$

Answer

Those with $x_1 = 1$ and $x_2 = x_3 = … = x_{N + 1} = 2 + 3 + … + (N + 1) = N(N + 3)/2$.

Solution

We follow the official solution. The official solution directly assumes $a$ is positive, which can indeed be assumed. The sign of $a$ does not matter if $n$ is odd, and we must have $a > 0$ if $n$ is even.

Extra lemmas

theorem IMOSL.IMO2011A2.Multiset_sup_mem {α : Type u_1} [LinearOrder α] [OrderBot α] {S : Multiset α} (hS : S ≠ 0) : S.sup ∈ S

The supremum of a non-empty multiset belongs to the multiset.

theorem IMOSL.IMO2011A2.Fin_sum_add_two (N : ℕ) : ∑ i : Fin N, (↑i + 2) = N * (N + 3) / 2

We have the formula ∑_{i < N} (i + 2) = N(N + 3)/2.

Start of the problem

theorem IMOSL.IMO2011A2.two_mul_pow_self_le_succ_pow_self {k : ℕ} (hk : k > 0) : 2 * k ^ k ≤ (k + 1) ^ k

For any k > 0, we have 2k^k ≤ (k + 1)^k.

theorem IMOSL.IMO2011A2.exists_mul_pow_lt_succ_pow (m x : ℕ) : ∃ (N : ℕ), ∀ n ≥ N, m * x ^ n < (x + 1) ^ n

For any m, x : ℕ, there exists N such that mx^n < (x + 1)^n for all n ≥ N.

theorem IMOSL.IMO2011A2.exists_sum_map_pow_lt_pow_of_forall_mem_lt {S : Multiset ℕ} {a : ℕ} (ha : a > 0) (hSa : ∀ x ∈ S, x < a) : ∃ (N : ℕ), ∀ n ≥ N, (Multiset.map (fun (x : ℕ) => x ^ n) S).sum < a ^ n

Let S be a multiset of non-negative integers. Let a > 0 be an integer greater than all elements of S. Then ∑_{x ∈ S} x^n < a^n for n large enough.

theorem IMOSL.IMO2011A2.exists_sum_map_pow_lt_pow_of_sup_lt {S : Multiset ℕ} {a : ℕ} (hSa : S.sup < a) : ∃ (N : ℕ), ∀ n ≥ N, (Multiset.map (fun (x : ℕ) => x ^ n) S).sum < a ^ n

Let S be a multiset of non-negative integers, and let a > sup S. Then ∑_{x ∈ S} x^n < a^n for n large enough.

theorem IMOSL.IMO2011A2.sup_eq_of_infinite_sum_map_pow_eq {S T : Multiset ℕ} (hST : ∀ (N : ℕ), ∃ n ≥ N, (Multiset.map (fun (x : ℕ) => x ^ n) S).sum = (Multiset.map (fun (x : ℕ) => x ^ n) T).sum) : S.sup = T.sup

Let S and T be multisets of non-negative integers such that there exists infinitely many n satisfying ∑_{x ∈ S} x^n = ∑_{x ∈ T} x^n. Then sup S = sup T.

theorem IMOSL.IMO2011A2.eq_of_infinite_sum_map_pow_eq {S T : Multiset ℕ} (hS : 0 ∉ S) (hT : 0 ∉ T) (hST : ∀ (N : ℕ), ∃ n ≥ N, (Multiset.map (fun (x : ℕ) => x ^ n) S).sum = (Multiset.map (fun (x : ℕ) => x ^ n) T).sum) : S = T

Let S and T be multisets of positive integers such that there exists infinitely many n satisfying ∑_{x ∈ S} x^n = ∑_{x ∈ T} x^n. Then S = T.

theorem IMOSL.IMO2011A2.eq_cons_one_replicate_of_sum_map_pow_eq {k : ℕ} {S : Multiset ℕ} (hS : 0 ∉ S) (hS0 : S.card = k + 1) (hS1 : ∀ n > 0, ∃ (a : ℕ), (Multiset.map (fun (x : ℕ) => x ^ n) S).sum = a ^ (n + 1) + 1) : S = 1 ::ₘ Multiset.replicate k k

Suppose that |S| = k + 1, and for every n > 0, there exists a : ℕ such that ∑_{x ∈ S} x^n = a^{n + 1} + 1. Then S = {1, k, …, k} with k repeated k times.

theorem IMOSL.IMO2011A2.sum_eq_cons_one_replicate {N k a : ℕ} {x : Fin (N + 1) → ℕ} (hx : ∑ i : Fin (N + 1), Multiset.replicate (↑i + 1) (x i) = 1 ::ₘ Multiset.replicate k a) : k = N * (N + 3) / 2 ∧ x = fun (i : Fin (N + 1)) => if i = 0 then 1 else a

Suppose that ∑_{i ≤ N} {x_i, …, x_i} = {1, a, …, a}, where each x_i is repeated i + 1 times and a is repeated k times. Then k = N(N + 3)/2, x_0 = 1, and x_i = a for all i > 0.

theorem IMOSL.IMO2011A2.Nat_version {N : ℕ} {x : Fin (N + 1) → ℕ} (hx : ∀ (i : Fin (N + 1)), x i > 0) : (∀ n > 0, ∃ (a : ℕ), ∑ i : Fin (N + 1), (↑i + 1) * x i ^ n = a ^ (n + 1) + 1) ↔ x = fun (i : Fin (N + 1)) => if i = 0 then 1 else N * (N + 3) / 2

Let x_0, x_1, …, x_N : ℕ, and suppose that for every n > 0, there exists a : ℕ such that ∑_{i ≤ N} (i + 1) x_i^n = a^{n + 1} + 1. Then x_0 = 1 and x_1 = … = x_N = N(N + 3)/2.

theorem IMOSL.IMO2011A2.final_solution {N : ℕ} {x : Fin (N + 1) → ℕ} (hx : ∀ (i : Fin (N + 1)), x i > 0) : (∀ n > 0, ∃ (a : ℤ), ↑(∑ i : Fin (N + 1), (↑i + 1) * x i ^ n) = a ^ (n + 1) + 1) ↔ x = fun (i : Fin (N + 1)) => if i = 0 then 1 else N * (N + 3) / 2

Final solution