|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Jeremy Tan. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Jeremy Tan |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise |
| 7 | +import Mathlib.Algebra.Group.Action.Defs |
| 8 | +import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 9 | +import Mathlib.Data.Fintype.Prod |
| 10 | +import Mathlib.Tactic.NormNum.Ineq |
| 11 | + |
| 12 | +/-! |
| 13 | +# IMO 2001 Q3 |
| 14 | +
|
| 15 | +Twenty-one girls and twenty-one boys took part in a mathematical competition. It turned out that |
| 16 | +
|
| 17 | +1. each contestant solved at most six problems, and |
| 18 | +2. for each pair of a girl and a boy, there was at least one problem that was solved by |
| 19 | +both the girl and the boy. |
| 20 | +
|
| 21 | +Show that there is a problem that was solved by at least three girls and at least three boys. |
| 22 | +
|
| 23 | +# Solution |
| 24 | +
|
| 25 | +Note that not all of the problems a girl $g$ solves can be "hard" for boys, in the sense that |
| 26 | +at most two boys solved it. If that was true, by condition 1 at most $6 × 2 = 12$ boys solved |
| 27 | +some problem $g$ solved, but by condition 2 that property holds for all 21 boys, which is a |
| 28 | +contradiction. |
| 29 | +
|
| 30 | +Hence there are at most 5 problems $g$ solved that are hard for boys, and the number of girl-boy |
| 31 | +pairs who solved some problem in common that was hard for boys is at most $5 × 2 × 21 = 210$. |
| 32 | +By the same reasoning this bound holds when "girls" and "boys" are swapped throughout, but there |
| 33 | +are $21^2$ girl-boy pairs in all and $21^2 > 210 + 210$, so some girl-boy pairs solved only problems |
| 34 | +in common that were not hard for girls or boys. By condition 2 the result follows. |
| 35 | +-/ |
| 36 | + |
| 37 | +namespace Imo2001Q3 |
| 38 | + |
| 39 | +open Finset |
| 40 | + |
| 41 | +/-- The conditions on the problems the girls and boys solved, represented as functions from `Fin 21` |
| 42 | +(index in cohort) to the finset of problems they solved (numbered arbitrarily). -/ |
| 43 | +structure Condition (G B : Fin 21 → Finset ℕ) where |
| 44 | + /-- Every girl solved at most six problems. -/ |
| 45 | + G_le_6 (i) : #(G i) ≤ 6 |
| 46 | + /-- Every boy solved at most six problems. -/ |
| 47 | + B_le_6 (j) : #(B j) ≤ 6 |
| 48 | + /-- Every girl-boy pair solved at least one problem in common. -/ |
| 49 | + G_inter_B (i j) : ¬Disjoint (G i) (B j) |
| 50 | + |
| 51 | +/-- A problem is easy for a cohort (boys or girls) if at least three of its members solved it. -/ |
| 52 | +def Easy (F : Fin 21 → Finset ℕ) (p : ℕ) : Prop := 3 ≤ #{i | p ∈ F i} |
| 53 | + |
| 54 | +variable {G B : Fin 21 → Finset ℕ} |
| 55 | + |
| 56 | +open Classical in |
| 57 | +/-- Every contestant solved at most five problems that were not easy for the other cohort. -/ |
| 58 | +lemma card_not_easy_le_five {i : Fin 21} (hG : #(G i) ≤ 6) (hB : ∀ j, ¬Disjoint (G i) (B j)) : |
| 59 | + #{p ∈ G i | ¬Easy B p} ≤ 5 := by |
| 60 | + by_contra! h |
| 61 | + replace h := le_antisymm (card_filter_le ..) (hG.trans h) |
| 62 | + simp_rw [card_filter_eq_iff, Easy, not_le] at h |
| 63 | + suffices 21 ≤ 12 by norm_num at this |
| 64 | + calc |
| 65 | + _ = #{j | ¬Disjoint (G i) (B j)} := by simp [filter_true_of_mem fun j _ ↦ hB j] |
| 66 | + _ = #((G i).biUnion fun p ↦ {j | p ∈ B j}) := by congr 1; ext j; simp [not_disjoint_iff] |
| 67 | + _ ≤ ∑ p ∈ G i, #{j | p ∈ B j} := card_biUnion_le |
| 68 | + _ ≤ ∑ p ∈ G i, 2 := sum_le_sum fun p mp ↦ Nat.le_of_lt_succ (h p mp) |
| 69 | + _ ≤ _ := by rw [sum_const, smul_eq_mul]; omega |
| 70 | + |
| 71 | +open Classical in |
| 72 | +/-- There are at most 210 girl-boy pairs who solved some problem in common that was not easy for |
| 73 | +a fixed cohort. -/ |
| 74 | +lemma card_not_easy_le_210 (hG : ∀ i, #(G i) ≤ 6) (hB : ∀ i j, ¬Disjoint (G i) (B j)) : |
| 75 | + #{ij : Fin 21 × Fin 21 | ∃ p, ¬Easy B p ∧ p ∈ G ij.1 ∩ B ij.2} ≤ 210 := |
| 76 | + calc |
| 77 | + _ = ∑ i, #{j | ∃ p, ¬Easy B p ∧ p ∈ G i ∩ B j} := by |
| 78 | + simp_rw [card_filter, ← univ_product_univ, sum_product] |
| 79 | + _ = ∑ i, #({p ∈ G i | ¬Easy B p}.biUnion fun p ↦ {j | p ∈ B j}) := by |
| 80 | + congr!; ext |
| 81 | + simp_rw [mem_biUnion, mem_inter, mem_filter, mem_univ, true_and] |
| 82 | + congr! 2; tauto |
| 83 | + _ ≤ ∑ i, ∑ p ∈ G i with ¬Easy B p, #{j | p ∈ B j} := sum_le_sum fun _ _ ↦ card_biUnion_le |
| 84 | + _ ≤ ∑ i, ∑ p ∈ G i with ¬Easy B p, 2 := by |
| 85 | + gcongr with i _ p mp |
| 86 | + rw [mem_filter, Easy, not_le] at mp |
| 87 | + exact Nat.le_of_lt_succ mp.2 |
| 88 | + _ ≤ ∑ i : Fin 21, 5 * 2 := by |
| 89 | + gcongr with i |
| 90 | + rw [sum_const, smul_eq_mul] |
| 91 | + exact mul_le_mul_right' (card_not_easy_le_five (hG _) (hB _)) _ |
| 92 | + _ = _ := by norm_num |
| 93 | + |
| 94 | +theorem result (h : Condition G B) : ∃ p, Easy G p ∧ Easy B p := by |
| 95 | + obtain ⟨G_le_6, B_le_6, G_inter_B⟩ := h |
| 96 | + have B_inter_G : ∀ i j, ¬Disjoint (B i) (G j) := fun i j ↦ by |
| 97 | + rw [disjoint_comm]; exact G_inter_B j i |
| 98 | + have cB := card_not_easy_le_210 G_le_6 G_inter_B |
| 99 | + have cG := card_not_easy_le_210 B_le_6 B_inter_G |
| 100 | + rw [← card_map ⟨_, Prod.swap_injective⟩] at cG |
| 101 | + have key := (card_union_le _ _).trans (add_le_add cB cG) |>.trans_lt |
| 102 | + (show _ < #(@univ (Fin 21 × Fin 21) _) by simp) |
| 103 | + obtain ⟨⟨i, j⟩, -, hij⟩ := exists_mem_notMem_of_card_lt_card key |
| 104 | + simp_rw [mem_union, mem_map, mem_filter, mem_univ, Function.Embedding.coeFn_mk, Prod.exists, |
| 105 | + Prod.swap_prod_mk, Prod.mk.injEq, existsAndEq, true_and, and_true, not_or, not_exists, |
| 106 | + not_and', not_not, mem_inter, and_imp] at hij |
| 107 | + obtain ⟨p, pG, pB⟩ := not_disjoint_iff.mp (G_inter_B i j) |
| 108 | + use p, hij.2 _ pB pG, hij.1 _ pG pB |
| 109 | + |
| 110 | +end Imo2001Q3 |
0 commit comments