mathlib3 documentation

mathlib-archive / imo.imo1998_q2

IMO 1998 Q2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.

source
@[reducible]
def imo1998_q2.judge_pair (J : Type u_1) :
Type u_1

An ordered pair of judges.

source
@[reducible]
def imo1998_q2.agreed_triple (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.

source
@[reducible]
def imo1998_q2.judge_pair.judge₁ {J : Type u_2} :
imo1998_q2.judge_pair J → J

The first judge from an ordered pair of judges.

source
@[reducible]
def imo1998_q2.judge_pair.judge₂ {J : Type u_2} :
imo1998_q2.judge_pair J → J

The second judge from an ordered pair of judges.

source
@[reducible]
def imo1998_q2.judge_pair.distinct {J : Type u_2} (p : imo1998_q2.judge_pair J) :
Prop

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

source
@[reducible]
def imo1998_q2.judge_pair.agree {C : Type u_1} {J : Type u_2} (r : C → J → Prop) (p : imo1998_q2.judge_pair J) (c : C) :
Prop

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

source
@[reducible]
def imo1998_q2.agreed_triple.contestant {C : Type u_1} {J : Type u_2} :
imo1998_q2.agreed_triple C J → C

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

source
@[reducible]
def imo1998_q2.agreed_triple.judge_pair {C : Type u_1} {J : Type u_2} :
imo1998_q2.agreed_triple C J → imo1998_q2.judge_pair J

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

source
@[simp]
theorem imo1998_q2.judge_pair.agree_iff_same_rating {C : Type u_1} {J : Type u_2} (r : C → J → Prop) (p : imo1998_q2.judge_pair J) (c : C) :
imo1998_q2.judge_pair.agree r p c ↔ (r c p.judge₁ ↔ r c p.judge₂)
source
noncomputable def imo1998_q2.agreed_contestants {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [fintype C] (p : imo1998_q2.judge_pair J) :
finset C

The set of contestants on which two judges agree.

Equations
source
noncomputable def imo1998_q2.A {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [fintype J] [fintype C] :
finset (imo1998_q2.agreed_triple C J)

All incidences of agreement.

Equations
source
theorem imo1998_q2.A_maps_to_off_diag_judge_pair {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [fintype J] [fintype C] (a : imo1998_q2.agreed_triple C J) :
a ∈ imo1998_q2.A r → a.judge_pair ∈ finset.univ.off_diag
source
theorem imo1998_q2.A_fibre_over_contestant {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [fintype J] [fintype C] (c : C) :
finset.filter (λ (p : imo1998_q2.judge_pair J), imo1998_q2.judge_pair.agree r p c ∧ p.distinct) finset.univ = finset.image prod.snd (finset.filter (λ (a : imo1998_q2.agreed_triple C J), a.contestant = c) (imo1998_q2.A r))
source
theorem imo1998_q2.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 (λ (p : imo1998_q2.judge_pair J), imo1998_q2.judge_pair.agree r p c ∧ p.distinct) finset.univ).card = (finset.filter (λ (a : imo1998_q2.agreed_triple C J), a.contestant = c) (imo1998_q2.A r)).card
source
theorem imo1998_q2.A_fibre_over_judge_pair {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [fintype J] [fintype C] {p : imo1998_q2.judge_pair J} (h : p.distinct) :
imo1998_q2.agreed_contestants r p = finset.image imo1998_q2.agreed_triple.contestant (finset.filter (λ (a : imo1998_q2.agreed_triple C J), a.judge_pair = p) (imo1998_q2.A r))
source
theorem imo1998_q2.A_fibre_over_judge_pair_card {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [fintype J] [fintype C] {p : imo1998_q2.judge_pair J} (h : p.distinct) :
(imo1998_q2.agreed_contestants r p).card = (finset.filter (λ (a : imo1998_q2.agreed_triple C J), a.judge_pair = p) (imo1998_q2.A r)).card
source
theorem imo1998_q2.A_card_upper_bound {C : Type u_1} {J : Type u_2} (r : C → J → Prop) [fintype J] [fintype C] {k : ℕ} (hk : ∀ (p : imo1998_q2.judge_pair J), p.distinct → (imo1998_q2.agreed_contestants r p).card ≤ k) :
(imo1998_q2.A r).card ≤ k * (fintype.card J * fintype.card J - fintype.card J)
source
theorem imo1998_q2.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
source
theorem imo1998_q2.norm_bound_of_odd_sum {x y z : ℤ} (h : x + y = 2 * z + 1) :
2 * z * z + 2 * z + 1 ≤ x * x + y * y
source
theorem imo1998_q2.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 (λ (p : imo1998_q2.judge_pair J), imo1998_q2.judge_pair.agree r p c) finset.univ).card
source
theorem imo1998_q2.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 (λ (p : imo1998_q2.judge_pair J), imo1998_q2.judge_pair.agree r p c ∧ p.distinct) finset.univ).card
source
theorem imo1998_q2.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 ≤ (imo1998_q2.A r).card
source
theorem imo1998_q2.clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
(↑b - 1) / (2 * ↑b) ≤ ↑k / ↑a ↔ (b - 1) * a ≤ k * (2 * b)
source
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 : imo1998_q2.judge_pair J), p.distinct → (imo1998_q2.agreed_contestants r p).card ≤ k) :
(↑b - 1) / (2 * ↑b) ≤ ↑k / ↑a