IMO 1982 Q1

The function f is defined for all positive integers n and takes on non-negative integer values. Also, for all m, n

f (m + n) - f(m) - f(n) = 0 or 1 f 2 = 0, f 3 > 0, and f 9999 = 3333.

Determine f 1982.

The solution is based on the one at the Art of Problem Solving website.

We prove the helper lemmas:

1. f m + f n ≤ f(m + n) superadditive.
2. n * f(m) ≤ f(m * n) superhomogeneous.
3. a * f a + c * f d ≤ f (a * b + c * d) superlinear, (derived from 1. and 2.).

So we can establish on the one hand that f 1980 ≤ 660, by observing that 660 * 1 = 660 * f3 ≤ f 1980 = f (660 * 3).

On the other hand, we establish that f 1980 ≥ 660 from 5 * f 1980 + 33 * f 3 ≤ f (5 * 1980 + 33 * 1) = f 9999 = 3333.

We then conclude f 1980 = 660 and then eventually determine that either f 1982 = 660 or f 1982 = 661.

In the latter case we derive a contradiction, because if f 1982 = 661 then 3334 = 5 * f 1982 + 29 * f(3) + f(2) ≤ f (5 * 1982 + 29 * 3 + 2) = f 9999 = 3333.

structure Imo1982Q1.IsGood (f : ℕ+ → ℕ) : Prop

• rel (m n : ℕ+) : f (m + n) = f m + f n ∨ f (m + n) = f m + f n + 1

  The function satisfies the functional relation.

• f₂ : f 2 = 0
• hf₃ : 0 < f 3
• f_9999 : f 9999 = 3333

theorem Imo1982Q1.IsGood.f₁ {f : ℕ+ → ℕ} (hf : IsGood f) : f 1 = 0

theorem Imo1982Q1.IsGood.f₃ {f : ℕ+ → ℕ} (hf : IsGood f) : f 3 = 1

theorem Imo1982Q1.IsGood.superadditive {f : ℕ+ → ℕ} (hf : IsGood f) {m n : ℕ+} : f m + f n ≤ f (m + n)

theorem Imo1982Q1.IsGood.superhomogeneous {f : ℕ+ → ℕ} (hf : IsGood f) {m n : ℕ+} : ↑n * f m ≤ f (n * m)

theorem Imo1982Q1.IsGood.superlinear {f : ℕ+ → ℕ} (hf : IsGood f) {a b c d : ℕ+} : ↑a * f b + ↑c * f d ≤ f (a * b + c * d)

theorem Imo1982Q1.IsGood.le_mul_three_apply {f : ℕ+ → ℕ} (hf : IsGood f) (n : ℕ+) : ↑n ≤ f (3 * n)

theorem Imo1982Q1.IsGood.part_1 {f : ℕ+ → ℕ} (hf : IsGood f) : 660 ≤ f 1980

theorem Imo1982Q1.IsGood.part_2 {f : ℕ+ → ℕ} (hf : IsGood f) : f 1980 ≤ 660

theorem imo1982_q1 {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) : f 1982 = 660