Documentation

Archive.Imo.Imo1982Q1

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.

source
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
Instances For
    source
    theorem Imo1982Q1.IsGood.f₁ {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) :
    f 1 = 0
    source
    theorem Imo1982Q1.IsGood.f₃ {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) :
    f 3 = 1
    source
    theorem Imo1982Q1.IsGood.superadditive {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) {m n : ℕ+} :
    f m + f n ≤ f (m + n)
    source
    theorem Imo1982Q1.IsGood.superhomogeneous {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) {m n : ℕ+} :
    ↑n * f m ≤ f (n * m)
    source
    theorem Imo1982Q1.IsGood.superlinear {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) {a b c d : ℕ+} :
    ↑a * f b + ↑c * f d ≤ f (a * b + c * d)
    source
    theorem Imo1982Q1.IsGood.le_mul_three_apply {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) (n : ℕ+) :
    ↑n ≤ f (3 * n)
    source
    theorem Imo1982Q1.IsGood.part_1 {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) :
    660 ≤ f 1980
    source
    theorem Imo1982Q1.IsGood.part_2 {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) :
    f 1980 ≤ 660
    source
    theorem imo1982_q1 {f : ℕ+ → ℕ} (hf : Imo1982Q1.IsGood f) :
    f 1982 = 660