# Documentation

Archive.Imo.Imo1998Q2

# 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.

@[inline, reducible]
abbrev Imo1998Q2.JudgePair (J : Type u_1) :
Type u_1

An ordered pair of judges.

Instances For
@[inline, reducible]
abbrev Imo1998Q2.AgreedTriple (C : Type u_1) (J : Type u_2) :
Type (max u_1 u_2)

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

Instances For
@[inline, reducible]

The first judge from an ordered pair of judges.

Instances For
@[inline, reducible]

The second judge from an ordered pair of judges.

Instances For
@[inline, reducible]
abbrev Imo1998Q2.JudgePair.Distinct {J : Type u_1} (p : ) :

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

Instances For
@[inline, reducible]
abbrev Imo1998Q2.JudgePair.Agree {C : Type u_1} {J : Type u_2} (r : CJProp) (p : ) (c : C) :

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

Instances For
@[inline, reducible]
abbrev Imo1998Q2.AgreedTriple.contestant {C : Type u_1} {J : Type u_2} :
C

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

Instances For
@[inline, reducible]
abbrev Imo1998Q2.AgreedTriple.judgePair {C : Type u_1} {J : Type u_2} :

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

Instances For
@[simp]
theorem Imo1998Q2.JudgePair.agree_iff_same_rating {C : Type u_2} {J : Type u_1} (r : CJProp) (p : ) (c : C) :
( )
def Imo1998Q2.agreedContestants {C : Type u_1} {J : Type u_2} (r : CJProp) [] (p : ) :

The set of contestants on which two judges agree.

Instances For
def Imo1998Q2.A {C : Type u_1} {J : Type u_2} (r : CJProp) [] [] :

All incidences of agreement.

Instances For
theorem Imo1998Q2.A_maps_to_offDiag_judgePair {C : Type u_1} {J : Type u_2} (r : CJProp) [] [] (a : ) :
a Finset.offDiag Finset.univ
theorem Imo1998Q2.A_fibre_over_contestant {C : Type u_2} {J : Type u_1} (r : CJProp) [] [] (c : C) :
Finset.filter (fun p => ) Finset.univ = Finset.image Prod.snd (Finset.filter (fun a => ) ())
theorem Imo1998Q2.A_fibre_over_contestant_card {C : Type u_2} {J : Type u_1} (r : CJProp) [] [] (c : C) :
Finset.card (Finset.filter (fun p => ) Finset.univ) = Finset.card (Finset.filter (fun a => ) ())
theorem Imo1998Q2.A_fibre_over_judgePair {C : Type u_2} {J : Type u_1} (r : CJProp) [] [] {p : } (h : ) :
= Finset.image Imo1998Q2.AgreedTriple.contestant (Finset.filter (fun a => ) ())
theorem Imo1998Q2.A_fibre_over_judgePair_card {C : Type u_2} {J : Type u_1} (r : CJProp) [] [] {p : } (h : ) :
= Finset.card (Finset.filter (fun a => ) ())
theorem Imo1998Q2.A_card_upper_bound {C : Type u_2} {J : Type u_1} (r : CJProp) [] [] {k : } (hk : ∀ (p : ), ) :
k * ()
theorem Imo1998Q2.add_sq_add_sq_sub {α : Type u_1} [Ring α] (x : α) (y : α) :
(x + y) * (x + y) + (x - y) * (x - y) = 2 * x * x + 2 * y * y
theorem Imo1998Q2.norm_bound_of_odd_sum {x : } {y : } {z : } (h : x + y = 2 * z + 1) :
2 * z * z + 2 * z + 1 x * x + y * y
theorem Imo1998Q2.judge_pairs_card_lower_bound {C : Type u_2} {J : Type u_1} (r : CJProp) [] {z : } (hJ : = 2 * z + 1) (c : C) :
2 * z * z + 2 * z + 1 Finset.card (Finset.filter (fun p => ) Finset.univ)
theorem Imo1998Q2.distinct_judge_pairs_card_lower_bound {C : Type u_2} {J : Type u_1} (r : CJProp) [] {z : } (hJ : = 2 * z + 1) (c : C) :
2 * z * z Finset.card (Finset.filter (fun p => ) Finset.univ)
theorem Imo1998Q2.A_card_lower_bound {C : Type u_1} {J : Type u_2} (r : CJProp) [] [] {z : } (hJ : = 2 * z + 1) :
2 * z * z *
theorem Imo1998Q2.clear_denominators {a : } {b : } {k : } (ha : 0 < a) (hb : 0 < b) :
(b - 1) / (2 * b) k / a (b - 1) * a k * (2 * b)
theorem imo1998_q2 {C : Type u_2} {J : Type u_1} (r : CJProp) [] [] (a : ) (b : ) (k : ) (hC : ) (hJ : ) (ha : 0 < a) (hb : Odd b) (hk : ∀ (p : ), ) :
(b - 1) / (2 * b) k / a