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.

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

An ordered pair of judges.

Equations
Instances For
    @[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
    Instances For
      @[reducible, inline]

      The first judge from an ordered pair of judges.

      Equations
      • Imo1998Q2.JudgePair.judge₁ = Prod.fst
      Instances For
        @[reducible, inline]

        The second judge from an ordered pair of judges.

        Equations
        • Imo1998Q2.JudgePair.judge₂ = Prod.snd
        Instances For
          @[reducible, inline]

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

          Equations
          • p.Distinct = (p.judge₁ p.judge₂)
          Instances For
            @[reducible, inline]
            abbrev Imo1998Q2.JudgePair.Agree {C : Type u_1} {J : Type u_2} (r : CJProp) (p : Imo1998Q2.JudgePair J) (c : C) :

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

            Equations
            Instances For
              @[reducible, inline]

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

              Equations
              • Imo1998Q2.AgreedTriple.contestant = Prod.fst
              Instances For
                @[reducible, inline]

                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
                  @[simp]
                  theorem Imo1998Q2.JudgePair.agree_iff_same_rating {C : Type u_1} {J : Type u_2} (r : CJProp) (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 : CJProp) [Fintype C] (p : Imo1998Q2.JudgePair J) :

                  The set of contestants on which two judges agree.

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

                    All incidences of agreement.

                    Equations
                    Instances For
                      theorem Imo1998Q2.A_maps_to_offDiag_judgePair {C : Type u_1} {J : Type u_2} (r : CJProp) [Fintype J] [Fintype C] (a : Imo1998Q2.AgreedTriple C J) :
                      a Imo1998Q2.A ra.judgePair Finset.univ.offDiag
                      theorem Imo1998Q2.A_fibre_over_contestant {C : Type u_1} {J : Type u_2} (r : CJProp) [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 : CJProp) [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 : CJProp) [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 : CJProp) [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 : CJProp) [Fintype J] [Fintype C] {k : } (hk : ∀ (p : Imo1998Q2.JudgePair J), p.Distinct(Imo1998Q2.agreedContestants r p).card k) :
                      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 : CJProp) [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 : CJProp) [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 : CJProp) [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 : CJProp) [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