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.

source

theorem imo1994_q1.tedious (m : ℕ) (k : fin (m + 1)) :

m - (m + (m + 1 - ↑k)) % (m + 1) = ↑k

source

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)