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.

@[reducible, inline]

abbrev Imo1998Q2.JudgePair (J : Type u_3) : Type u_3

An ordered pair of judges.

Equations

• Imo1998Q2.JudgePair J = (J × J)

@[reducible, inline]

abbrev Imo1998Q2.AgreedTriple (C : Type u_3) (J : Type u_4) : Type (max u_3 u_4)

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

Equations

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

@[reducible, inline]

abbrev Imo1998Q2.JudgePair.judge₁ {J : Type u_2} : Imo1998Q2.JudgePair J → J

The first judge from an ordered pair of judges.

Equations

• Imo1998Q2.JudgePair.judge₁ = Prod.fst

@[reducible, inline]

abbrev Imo1998Q2.JudgePair.judge₂ {J : Type u_2} : Imo1998Q2.JudgePair J → J

The second judge from an ordered pair of judges.

Equations

• Imo1998Q2.JudgePair.judge₂ = Prod.snd

@[reducible, inline]

abbrev Imo1998Q2.JudgePair.Distinct {J : Type u_2} (p : Imo1998Q2.JudgePair J) : Prop

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

Equations

• p.Distinct = (p.judge₁ ≠ p.judge₂)

@[reducible, inline]

abbrev Imo1998Q2.JudgePair.Agree {C : Type u_1} {J : Type u_2} (r : C → J → Prop) (p : Imo1998Q2.JudgePair J) (c : C) : Prop

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₂)

@[reducible, inline]

abbrev Imo1998Q2.AgreedTriple.contestant {C : Type u_1} {J : Type u_2} : Imo1998Q2.AgreedTriple C J → C

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

Equations

• Imo1998Q2.AgreedTriple.contestant = Prod.fst

@[reducible, inline]

abbrev Imo1998Q2.AgreedTriple.judgePair {C : Type u_1} {J : Type u_2} : Imo1998Q2.AgreedTriple C J → Imo1998Q2.JudgePair J

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

Equations

• Imo1998Q2.AgreedTriple.judgePair = Prod.snd

@[simp]

theorem Imo1998Q2.JudgePair.agree_iff_same_rating {C : Type u_1} {J : Type u_2} (r : C → J → Prop) (p : Imo1998Q2.JudgePair J) (c : C) : Imo1998Q2.JudgePair.Agree r p c ↔ (r c p.judge₁ ↔ r c p.judge₂)

def Imo1998Q2.agreedContestants {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype C] (p : Imo1998Q2.JudgePair J) : Finset C

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

def Imo1998Q2.A {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] : Finset (Imo1998Q2.AgreedTriple C J)

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

theorem Imo1998Q2.A_maps_to_offDiag_judgePair {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] (a : Imo1998Q2.AgreedTriple C J) : a ∈ Imo1998Q2.A r → a.judgePair ∈ Finset.univ.offDiag

theorem Imo1998Q2.A_fibre_over_contestant {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] (c : C) : Finset.filter (fun (p : Imo1998Q2.JudgePair J) => Imo1998Q2.JudgePair.Agree r p c ∧ p.Distinct) Finset.univ = Finset.image Prod.snd (Finset.filter (fun (a : Imo1998Q2.AgreedTriple C J) => a.contestant = c) (Imo1998Q2.A r))

theorem Imo1998Q2.A_fibre_over_contestant_card {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] (c : C) : (Finset.filter (fun (p : Imo1998Q2.JudgePair J) => Imo1998Q2.JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card = (Finset.filter (fun (a : Imo1998Q2.AgreedTriple C J) => a.contestant = c) (Imo1998Q2.A r)).card

theorem Imo1998Q2.A_fibre_over_judgePair {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] {p : Imo1998Q2.JudgePair J} (h : p.Distinct) : Imo1998Q2.agreedContestants r p = Finset.image Imo1998Q2.AgreedTriple.contestant (Finset.filter (fun (a : Imo1998Q2.AgreedTriple C J) => a.judgePair = p) (Imo1998Q2.A r))

theorem Imo1998Q2.A_fibre_over_judgePair_card {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] {p : Imo1998Q2.JudgePair J} (h : p.Distinct) : (Imo1998Q2.agreedContestants r p).card = (Finset.filter (fun (a : Imo1998Q2.AgreedTriple C J) => a.judgePair = p) (Imo1998Q2.A r)).card

theorem Imo1998Q2.A_card_upper_bound {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] {k : ℕ} (hk : ∀ (p : Imo1998Q2.JudgePair J), p.Distinct → (Imo1998Q2.agreedContestants r p).card ≤ k) : (Imo1998Q2.A r).card ≤ k * (Fintype.card J * Fintype.card J - Fintype.card J)

theorem Imo1998Q2.add_sq_add_sq_sub {α : Type u_3} [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_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) : 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun (p : Imo1998Q2.JudgePair J) => Imo1998Q2.JudgePair.Agree r p c) Finset.univ).card

theorem Imo1998Q2.distinct_judge_pairs_card_lower_bound {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) (c : C) : 2 * z * z ≤ (Finset.filter (fun (p : Imo1998Q2.JudgePair J) => Imo1998Q2.JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card

theorem Imo1998Q2.A_card_lower_bound {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] {z : ℕ} (hJ : Fintype.card J = 2 * z + 1) : 2 * z * z * Fintype.card C ≤ (Imo1998Q2.A r).card

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_1} {J : Type u_2} (r : C → J → Prop) [Fintype J] [Fintype C] (a b k : ℕ) (hC : Fintype.card C = a) (hJ : Fintype.card J = b) (ha : 0 < a) (hb : Odd b) (hk : ∀ (p : Imo1998Q2.JudgePair J), p.Distinct → (Imo1998Q2.agreedContestants r p).card ≤ k) : (↑b - 1) / (2 * ↑b) ≤ ↑k / ↑a