# mathlib3documentation

mathlib-archive / imo.imo1994_q1

# IMO 1994 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let m and n be two positive integers. Let a₁, a₂, ..., aₘ be m different numbers from the set {1, 2, ..., n} such that for any two indices i and j with 1 ≤ i ≤ j ≤ m and aᵢ + aⱼ ≤ n, there exists an index k such that aᵢ + aⱼ = aₖ. Show that (a₁+a₂+...+aₘ)/m ≥ (n+1)/2

# Sketch of solution #

We can order the numbers so that a₁ ≤ a₂ ≤ ... ≤ aₘ. The key idea is to pair the numbers in the sum and show that aᵢ + aₘ₊₁₋ᵢ ≥ n+1. Indeed, if we had aᵢ + aₘ₊₁₋ᵢ ≤ n, then a₁ + aₘ₊₁₋ᵢ, a₂ + aₘ₊₁₋ᵢ, ..., aᵢ + aₘ₊₁₋ᵢ would be m elements of the set of aᵢ's all larger than aₘ₊₁₋ᵢ, which is impossible.

theorem imo1994_q1.tedious (m : ) (k : fin (m + 1)) :
m - (m + (m + 1 - k)) % (m + 1) = k
theorem imo1994_q1 (n m : ) (A : finset ) (hm : A.card = m + 1) (hrange : (a : ), a A 0 < a a n) (hadd : (a : ), a A (b : ), b A a + b n a + b A) :
(m + 1) * (n + 1) 2 * A.sum (λ (x : ), x)