# IMO 1998 Q2 #

In a competition, there are `a`

contestants and `b`

judges, where `b ≥ 3`

is an odd integer. Each
judge rates each contestant as either "pass" or "fail". Suppose `k`

is a number such that, for any
two judges, their ratings coincide for at most `k`

contestants. Prove that `k / a ≥ (b - 1) / (2b)`

.

## Solution #

The problem asks us to think about triples consisting of a contestant and two judges whose ratings
agree for that contestant. We thus consider the subset `A ⊆ C × JJ`

of all such incidences of
agreement, where `C`

and `J`

are the sets of contestants and judges, and `JJ = J × J - {(j, j)}`

. We
have natural maps: `left : A → C`

and `right: A → JJ`

. We count the elements of `A`

in two ways: as
the sum of the cardinalities of the fibres of `left`

and as the sum of the cardinalities of the
fibres of `right`

. We obtain an upper bound on the cardinality of `A`

from the count for `right`

,
and a lower bound from the count for `left`

. These two bounds combine to the required result.

First consider the map `right : A → JJ`

. Since the size of any fibre over a point in JJ is bounded
by `k`

and since `|JJ| = b^2 - b`

, we obtain the upper bound: `|A| ≤ k(b^2-b)`

.

Now consider the map `left : A → C`

. The fibre over a given contestant `c ∈ C`

is the set of
ordered pairs of (distinct) judges who agree about `c`

. We seek to bound the cardinality of this
fibre from below. Minimum agreement for a contestant occurs when the judges' ratings are split as
evenly as possible. Since `b`

is odd, this occurs when they are divided into groups of size
`(b-1)/2`

and `(b+1)/2`

. This corresponds to a fibre of cardinality `(b-1)^2/2`

and so we obtain
the lower bound: `a(b-1)^2/2 ≤ |A|`

.

Rearranging gives the result.

An ordered pair of judges.

## Equations

- Imo1998Q2.JudgePair J = (J × J)

## Instances For

A triple consisting of contestant together with an ordered pair of judges.

## Equations

- Imo1998Q2.AgreedTriple C J = (C × Imo1998Q2.JudgePair J)

## Instances For

The first judge from an ordered pair of judges.

## Equations

- Imo1998Q2.JudgePair.judge₁ = Prod.fst

## Instances For

The second judge from an ordered pair of judges.

## Equations

- Imo1998Q2.JudgePair.judge₂ = Prod.snd

## Instances For

The proposition that the judges in an ordered pair are distinct.

## Instances For

The proposition that the judges in an ordered pair agree about a contestant's rating.

## Equations

- Imo1998Q2.JudgePair.Agree r p c = (r c p.judge₁ ↔ r c p.judge₂)

## Instances For

The contestant from the triple consisting of a contestant and an ordered pair of judges.

## Equations

- Imo1998Q2.AgreedTriple.contestant = Prod.fst

## Instances For

The ordered pair of judges from the triple consisting of a contestant and an ordered pair of judges.

## Equations

- Imo1998Q2.AgreedTriple.judgePair = Prod.snd

## Instances For

The set of contestants on which two judges agree.

## Equations

- Imo1998Q2.agreedContestants r p = Finset.filter (fun (c : C) => Imo1998Q2.JudgePair.Agree r p c) Finset.univ

## Instances For

All incidences of agreement.

## Equations

- Imo1998Q2.A r = Finset.filter (fun (a : Imo1998Q2.AgreedTriple C J) => Imo1998Q2.JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ