Catalog/Sparsity/BipartiteRamsey/Full.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Clique |
| 2 | import Mathlib.Data.Finset.Powerset |
| 3 | import Mathlib.Data.Fintype.EquivFin |
| 4 | import Mathlib.Data.Nat.Choose.Basic |
| 5 | import Catalog.Sparsity.MulticolorRamsey.Full |
| 6 | import Catalog.Sparsity.ShallowTopologicalMinor.Full |
| 7 | |
| 8 | namespace Catalog.Sparsity.BipartiteRamsey |
| 9 | |
| 10 | open Catalog.Sparsity.ShallowTopologicalMinor |
| 11 | |
| 12 | private noncomputable def localNeighborPair |
| 13 | {V : Type} [DecidableEq V] [Fintype V] |
| 14 | (G : SimpleGraph V) [DecidableRel G.Adj] (A : Finset V) |
| 15 | (b u v : V) (huA : u ∈ A) (hvA : v ∈ A) |
| 16 | (hub : G.Adj b u) (hvb : G.Adj b v) (huv : u ≠ v) : |
| 17 | (SimpleGraph.completeGraph ↑(((G.neighborFinset b ∩ A : Finset V) : Set V))).edgeSet := by |
| 18 | refine ⟨s(⟨u, by simp [huA, hub]⟩, ⟨v, by simp [hvA, hvb]⟩), ?_⟩ |
| 19 | rw [SimpleGraph.mem_edgeSet, SimpleGraph.top_adj] |
| 20 | intro h |
| 21 | apply huv |
| 22 | exact Subtype.ext_iff.mp h |
| 23 | |
| 24 | private theorem localPairCodeBound |
| 25 | {V : Type} [DecidableEq V] [Fintype V] |
| 26 | (G : SimpleGraph V) [DecidableRel G.Adj] (A : Finset V) (d : ℕ) |
| 27 | {b : V} (hdeg : (G.neighborFinset b ∩ A).card < d) : |
| 28 | Fintype.card |
| 29 | ((SimpleGraph.completeGraph ↑(((G.neighborFinset b ∩ A : Finset V) : Set V))).edgeSet) ≤ |
| 30 | Nat.choose (d - 1) 2 := by |
| 31 | have hcard_eq : |
| 32 | Fintype.card |
| 33 | ((SimpleGraph.completeGraph ↑(((G.neighborFinset b ∩ A : Finset V) : Set V))).edgeSet) = |
| 34 | (G.neighborFinset b ∩ A).card.choose 2 := by |
| 35 | have hfilter : {a ∈ A | G.Adj b a} = G.neighborFinset b ∩ A := by |
| 36 | ext x |
| 37 | simp [and_comm] |
| 38 | have hfilter_card : {a ∈ A | G.Adj b a}.card = (G.neighborFinset b ∩ A).card := by |
| 39 | rw [hfilter] |
| 40 | calc |
| 41 | Fintype.card |
| 42 | ((SimpleGraph.completeGraph ↑(((G.neighborFinset b ∩ A : Finset V) : Set V))).edgeSet) = |
| 43 | {a ∈ A | G.Adj b a}.card.choose 2 := by |
| 44 | rw [SimpleGraph.card_edgeSet] |
| 45 | simpa [Fintype.card_of_finset' (G.neighborFinset b ∩ A) (fun x => Iff.rfl)] using |
| 46 | (SimpleGraph.card_edgeFinset_top_eq_card_choose_two |
| 47 | (V := ↑(((G.neighborFinset b ∩ A : Finset V) : Set V)))) |
| 48 | _ = (G.neighborFinset b ∩ A).card.choose 2 := by rw [hfilter_card] |
| 49 | have hle : (G.neighborFinset b ∩ A).card ≤ d - 1 := by |
| 50 | omega |
| 51 | calc |
| 52 | Fintype.card |
| 53 | ((SimpleGraph.completeGraph ↑(((G.neighborFinset b ∩ A : Finset V) : Set V))).edgeSet) = |
| 54 | (G.neighborFinset b ∩ A).card.choose 2 := hcard_eq |
| 55 | _ ≤ Nat.choose (d - 1) 2 := Nat.choose_le_choose 2 hle |
| 56 | |
| 57 | private noncomputable def localPairCode |
| 58 | {V : Type} [DecidableEq V] [Fintype V] |
| 59 | (G : SimpleGraph V) [DecidableRel G.Adj] (A : Finset V) (d : ℕ) |
| 60 | (b u v : V) (huA : u ∈ A) (hvA : v ∈ A) |
| 61 | (hub : G.Adj b u) (hvb : G.Adj b v) (huv : u ≠ v) |
| 62 | (hdeg : (G.neighborFinset b ∩ A).card < d) : |
| 63 | Fin (Nat.choose (d - 1) 2) := |
| 64 | Fin.castLE (localPairCodeBound G A d hdeg) |
| 65 | ((Fintype.equivFin |
| 66 | ((SimpleGraph.completeGraph ↑(((G.neighborFinset b ∩ A : Finset V) : Set V))).edgeSet)) |
| 67 | (localNeighborPair G A b u v huA hvA hub hvb huv)) |
| 68 | |
| 69 | private theorem localNeighborPair_symm |
| 70 | {V : Type} [DecidableEq V] [Fintype V] |
| 71 | (G : SimpleGraph V) [DecidableRel G.Adj] (A : Finset V) |
| 72 | (b u v : V) (huA : u ∈ A) (hvA : v ∈ A) |
| 73 | (hub : G.Adj b u) (hvb : G.Adj b v) (huv : u ≠ v) : |
| 74 | localNeighborPair G A b u v huA hvA hub hvb huv = |
| 75 | localNeighborPair G A b v u hvA huA hvb hub huv.symm := by |
| 76 | apply Subtype.ext |
| 77 | simp [localNeighborPair, Sym2.eq_swap] |
| 78 | |
| 79 | private theorem localPairCode_symm |
| 80 | {V : Type} [DecidableEq V] [Fintype V] |
| 81 | (G : SimpleGraph V) [DecidableRel G.Adj] (A : Finset V) (d : ℕ) |
| 82 | {b u v : V} (huA : u ∈ A) (hvA : v ∈ A) |
| 83 | (hub : G.Adj b u) (hvb : G.Adj b v) (huv : u ≠ v) |
| 84 | (hdeg : (G.neighborFinset b ∩ A).card < d) : |
| 85 | localPairCode G A d b u v huA hvA hub hvb huv hdeg = |
| 86 | localPairCode G A d b v u hvA huA hvb hub huv.symm hdeg := by |
| 87 | dsimp [localPairCode] |
| 88 | rw [localNeighborPair_symm G A b u v huA hvA hub hvb huv] |
| 89 | |
| 90 | private theorem localPairCode_injective |
| 91 | {V : Type} [DecidableEq V] [Fintype V] |
| 92 | (G : SimpleGraph V) [DecidableRel G.Adj] (A : Finset V) (d : ℕ) |
| 93 | {b u₁ v₁ u₂ v₂ : V} |
| 94 | (hu₁A : u₁ ∈ A) (hv₁A : v₁ ∈ A) (hu₂A : u₂ ∈ A) (hv₂A : v₂ ∈ A) |
| 95 | (hu₁b : G.Adj b u₁) (hv₁b : G.Adj b v₁) |
| 96 | (hu₂b : G.Adj b u₂) (hv₂b : G.Adj b v₂) |
| 97 | (huv₁ : u₁ ≠ v₁) (huv₂ : u₂ ≠ v₂) |
| 98 | (hdeg : (G.neighborFinset b ∩ A).card < d) |
| 99 | (hcode : |
| 100 | localPairCode G A d b u₁ v₁ hu₁A hv₁A hu₁b hv₁b huv₁ hdeg = |
| 101 | localPairCode G A d b u₂ v₂ hu₂A hv₂A hu₂b hv₂b huv₂ hdeg) : |
| 102 | s(u₁, v₁) = s(u₂, v₂) := by |
| 103 | dsimp [localPairCode] at hcode |
| 104 | have hpair_eq : |
| 105 | localNeighborPair G A b u₁ v₁ hu₁A hv₁A hu₁b hv₁b huv₁ = |
| 106 | localNeighborPair G A b u₂ v₂ hu₂A hv₂A hu₂b hv₂b huv₂ := by |
| 107 | apply (Fintype.equivFin |
| 108 | ((SimpleGraph.completeGraph ↑(((G.neighborFinset b ∩ A : Finset V) : Set V))).edgeSet)).injective |
| 109 | exact Fin.castLE_injective (localPairCodeBound G A d hdeg) hcode |
| 110 | simpa [localNeighborPair] using congrArg Subtype.val hpair_eq |
| 111 | |
| 112 | private noncomputable def commonNeighborCodes |
| 113 | {V : Type} [DecidableEq V] [Fintype V] |
| 114 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 115 | (A B : Finset V) (d : ℕ) |
| 116 | (hdeg : ∀ b : ↑B, (G.neighborFinset b.1 ∩ A).card < d) |
| 117 | (u v : ↑(A : Set V)) : |
| 118 | Finset (Fin (Nat.choose (d - 1) 2)) := |
| 119 | (B.attach).biUnion fun bw => |
| 120 | if huv : u.1 ≠ v.1 ∧ G.Adj bw.1 u.1 ∧ G.Adj bw.1 v.1 then |
| 121 | {localPairCode G A d bw.1 u.1 v.1 u.2 v.2 huv.2.1 huv.2.2 huv.1 (hdeg bw)} |
| 122 | else |
| 123 | ∅ |
| 124 | |
| 125 | private theorem mem_commonNeighborCodes |
| 126 | {V : Type} [DecidableEq V] [Fintype V] |
| 127 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 128 | (A B : Finset V) (d : ℕ) |
| 129 | (hdeg : ∀ b : ↑B, (G.neighborFinset b.1 ∩ A).card < d) |
| 130 | (u v : ↑(A : Set V)) (x : Fin (Nat.choose (d - 1) 2)) : |
| 131 | x ∈ commonNeighborCodes G A B d hdeg u v ↔ |
| 132 | ∃ (b : V) (hb : b ∈ B) (huv : u.1 ≠ v.1) (hub : G.Adj b u.1) (hvb : G.Adj b v.1), |
| 133 | localPairCode G A d b u.1 v.1 u.2 v.2 hub hvb huv (hdeg ⟨b, hb⟩) = x := by |
| 134 | classical |
| 135 | unfold commonNeighborCodes |
| 136 | simp only [Finset.mem_biUnion] |
| 137 | constructor |
| 138 | · rintro ⟨b, -, hmem⟩ |
| 139 | by_cases huv : u.1 ≠ v.1 ∧ G.Adj b.1 u.1 ∧ G.Adj b.1 v.1 |
| 140 | · refine ⟨b.1, b.2, huv.1, huv.2.1, huv.2.2, ?_⟩ |
| 141 | have hx : x = localPairCode G A d b.1 u.1 v.1 u.2 v.2 |
| 142 | huv.2.1 huv.2.2 huv.1 (hdeg b) := by |
| 143 | simpa [huv] using hmem |
| 144 | exact hx.symm |
| 145 | · have hfalse : ¬(¬u = v ∧ G.Adj b.1 u.1 ∧ G.Adj b.1 v.1) := by |
| 146 | simpa using huv |
| 147 | simp [hfalse] at hmem |
| 148 | · rintro ⟨b, hb, huv, hub, hvb, hx⟩ |
| 149 | refine ⟨⟨b, hb⟩, by simp, ?_⟩ |
| 150 | simpa [huv, hub, hvb] using hx.symm |
| 151 | |
| 152 | private theorem commonNeighborCodes_symm |
| 153 | {V : Type} [DecidableEq V] [Fintype V] |
| 154 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 155 | (A B : Finset V) (d : ℕ) |
| 156 | (hdeg : ∀ b : ↑B, (G.neighborFinset b.1 ∩ A).card < d) |
| 157 | (u v : ↑(A : Set V)) : |
| 158 | commonNeighborCodes G A B d hdeg u v = |
| 159 | commonNeighborCodes G A B d hdeg v u := by |
| 160 | classical |
| 161 | ext x |
| 162 | constructor |
| 163 | · intro hx |
| 164 | rcases (mem_commonNeighborCodes G A B d hdeg u v x).1 hx with |
| 165 | ⟨b, hb, huv, hub, hvb, hcode⟩ |
| 166 | refine (mem_commonNeighborCodes G A B d hdeg v u x).2 ?_ |
| 167 | refine ⟨b, hb, huv.symm, hvb, hub, ?_⟩ |
| 168 | exact (localPairCode_symm G A d u.2 v.2 hub hvb huv (hdeg ⟨b, hb⟩)).symm.trans hcode |
| 169 | · intro hx |
| 170 | rcases (mem_commonNeighborCodes G A B d hdeg v u x).1 hx with |
| 171 | ⟨b, hb, huv, hub, hvb, hcode⟩ |
| 172 | refine (mem_commonNeighborCodes G A B d hdeg u v x).2 ?_ |
| 173 | refine ⟨b, hb, huv.symm, hvb, hub, ?_⟩ |
| 174 | exact (localPairCode_symm G A d u.2 v.2 hvb hub huv.symm (hdeg ⟨b, hb⟩)).trans hcode |
| 175 | |
| 176 | private noncomputable def edgeColor |
| 177 | {V : Type} [DecidableEq V] [Fintype V] |
| 178 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 179 | (A B : Finset V) (d : ℕ) |
| 180 | (hdeg : ∀ b : ↑B, (G.neighborFinset b.1 ∩ A).card < d) |
| 181 | (u v : ↑(A : Set V)) : |
| 182 | Fin (Nat.choose (d - 1) 2 + 1) := |
| 183 | if hcodes : (commonNeighborCodes G A B d hdeg u v).Nonempty then |
| 184 | Fin.castLE (Nat.le_succ _) ((commonNeighborCodes G A B d hdeg u v).min' hcodes) |
| 185 | else |
| 186 | Fin.last _ |
| 187 | |
| 188 | private theorem edgeColor_symm |
| 189 | {V : Type} [DecidableEq V] [Fintype V] |
| 190 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 191 | (A B : Finset V) (d : ℕ) |
| 192 | (hdeg : ∀ b : ↑B, (G.neighborFinset b.1 ∩ A).card < d) |
| 193 | (u v : ↑(A : Set V)) : |
| 194 | edgeColor G A B d hdeg u v = edgeColor G A B d hdeg v u := by |
| 195 | classical |
| 196 | simp [edgeColor, commonNeighborCodes_symm] |
| 197 | |
| 198 | private theorem exists_commonNeighbor_of_edgeColor_eq |
| 199 | {V : Type} [DecidableEq V] [Fintype V] |
| 200 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 201 | (A B : Finset V) (d : ℕ) |
| 202 | (hdeg : ∀ b : ↑B, (G.neighborFinset b.1 ∩ A).card < d) |
| 203 | {u v : ↑(A : Set V)} (huv : u ≠ v) {j : Fin (Nat.choose (d - 1) 2)} |
| 204 | (hcolor : edgeColor G A B d hdeg u v = Fin.castLE (Nat.le_succ _) j) : |
| 205 | ∃ (b : V) (hb : b ∈ B) (hub : G.Adj b u.1) (hvb : G.Adj b v.1), |
| 206 | localPairCode G A d b u.1 v.1 u.2 v.2 |
| 207 | hub hvb (fun h => huv (Subtype.ext h)) (hdeg ⟨b, hb⟩) = j := by |
| 208 | classical |
| 209 | let codes := commonNeighborCodes G A B d hdeg u v |
| 210 | by_cases hcodes : codes.Nonempty |
| 211 | · have hmin : |
| 212 | Fin.castLE (Nat.le_succ _) (codes.min' hcodes) = |
| 213 | Fin.castLE (Nat.le_succ _) j := by |
| 214 | simpa [edgeColor, codes, hcodes] using hcolor |
| 215 | have hmin_eq : codes.min' hcodes = j := Fin.castLE_injective _ hmin |
| 216 | have hmem : j ∈ codes := by |
| 217 | rw [← hmin_eq] |
| 218 | exact Finset.min'_mem codes hcodes |
| 219 | rcases (mem_commonNeighborCodes G A B d hdeg u v j).1 hmem with |
| 220 | ⟨b, hb, _, hub, hvb, hcode⟩ |
| 221 | exact ⟨b, hb, hub, hvb, hcode⟩ |
| 222 | · have hlast : |
| 223 | edgeColor G A B d hdeg u v = Fin.last (Nat.choose (d - 1) 2) := by |
| 224 | simp [edgeColor, codes, hcodes] |
| 225 | have hne : |
| 226 | Fin.castLE (Nat.le_succ _) j ≠ Fin.last (Nat.choose (d - 1) 2) := by |
| 227 | intro h |
| 228 | have hval := congrArg Fin.val h |
| 229 | exact Nat.ne_of_lt j.isLt hval |
| 230 | exact (hne (hcolor.symm.trans hlast)).elim |
| 231 | |
| 232 | /-- Lemma 3.9: in a bipartite graph with sides `A` and `B`, if `|A|` is large |
| 233 | enough (as a function of `m`, `t`, `d`), then at least one of the following |
| 234 | holds: |
| 235 | (a) `A` contains `m` vertices with no common neighbor, |
| 236 | (b) `G` contains a `1`-subdivision of `K_t` with principal vertices in `A`, |
| 237 | (c) `B` contains a vertex of degree at least `d`. -/ |
| 238 | theorem bipartiteRamsey (m t d : ℕ) : |
| 239 | ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 240 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 241 | (A B : Finset V), |
| 242 | Disjoint A B → |
| 243 | (∀ u v, G.Adj u v → (u ∈ A ∧ v ∈ B) ∨ (u ∈ B ∧ v ∈ A)) → |
| 244 | N ≤ A.card → |
| 245 | (∃ A' : Finset V, A' ⊆ A ∧ m ≤ A'.card ∧ |
| 246 | (↑A' : Set V).Pairwise (fun u v => |
| 247 | ∀ w, ¬(G.Adj u w ∧ G.Adj v w))) ∨ |
| 248 | (∃ M : ShallowTopologicalMinorModel |
| 249 | (SimpleGraph.completeGraph (Fin t)) G 1, |
| 250 | Set.range M.branchVertex ⊆ ↑A) ∨ |
| 251 | (∃ v ∈ B, d ≤ (G.neighborFinset v ∩ A).card) := by |
| 252 | classical |
| 253 | let k := Nat.choose (d - 1) 2 |
| 254 | let sizes : List ℕ := List.replicate k t ++ [m] |
| 255 | obtain ⟨N, hN⟩ := Catalog.Sparsity.MulticolorRamsey.multicolorRamsey sizes (by |
| 256 | simp [sizes]) |
| 257 | refine ⟨N, ?_⟩ |
| 258 | intro V _ _ G _ A B hAB hBip hAcard |
| 259 | by_cases hbig : ∃ v ∈ B, d ≤ (G.neighborFinset v ∩ A).card |
| 260 | · exact Or.inr (Or.inr hbig) |
| 261 | · have hdeg : ∀ b : ↑B, (G.neighborFinset b.1 ∩ A).card < d := by |
| 262 | intro b |
| 263 | exact lt_of_not_ge (fun hge => hbig ⟨b.1, b.2, hge⟩) |
| 264 | have hcA : N ≤ Fintype.card ↑(A : Set V) := by |
| 265 | rw [Fintype.card_of_finset' A (fun x => Iff.rfl)] |
| 266 | exact hAcard |
| 267 | let c0 : Sym2 ↑(A : Set V) → Fin (k + 1) := |
| 268 | Sym2.lift ⟨edgeColor G A B d hdeg, edgeColor_symm G A B d hdeg⟩ |
| 269 | let c : Sym2 ↑(A : Set V) → Fin sizes.length := |
| 270 | fun e => Fin.cast (by simp [sizes]) (c0 e) |
| 271 | obtain ⟨i, S, hsize, hpair⟩ := hN (V := ↑(A : Set V)) hcA c |
| 272 | by_cases hiLast : i.1 = k |
| 273 | · let lastColor : Fin sizes.length := ⟨k, by simp [sizes]⟩ |
| 274 | have hi_eq_last : i = lastColor := by |
| 275 | apply Fin.ext |
| 276 | simp [lastColor, hiLast] |
| 277 | refine Or.inl ⟨S.map ⟨Subtype.val, Subtype.val_injective⟩, ?_, ?_, ?_⟩ |
| 278 | · intro x hx |
| 279 | rcases Finset.mem_map.mp hx with ⟨u, hu, rfl⟩ |
| 280 | exact u.2 |
| 281 | · have hmle : m ≤ S.card := by |
| 282 | simpa [sizes, hiLast] using hsize |
| 283 | simpa using hmle |
| 284 | · intro u hu v hv huv w huw |
| 285 | rcases Finset.mem_map.mp hu with ⟨u', hu', rfl⟩ |
| 286 | rcases Finset.mem_map.mp hv with ⟨v', hv', rfl⟩ |
| 287 | have huv' : u' ≠ v' := by |
| 288 | intro h |
| 289 | apply huv |
| 290 | exact congrArg Subtype.val h |
| 291 | have hcolor : c s(u', v') = lastColor := by |
| 292 | exact (hpair hu' hv' huv').trans hi_eq_last |
| 293 | have hwB : w ∈ B := by |
| 294 | rcases hBip u'.1 w huw.1 with ⟨huA, hwB⟩ | ⟨huB, hwA⟩ |
| 295 | · exact hwB |
| 296 | · exact (Finset.disjoint_left.mp hAB u'.2 huB).elim |
| 297 | have hcodes_nonempty : |
| 298 | (commonNeighborCodes G A B d hdeg u' v').Nonempty := by |
| 299 | refine ⟨localPairCode G A d w u'.1 v'.1 u'.2 v'.2 |
| 300 | (G.symm huw.1) (G.symm huw.2) (fun h => huv' (Subtype.ext h)) (hdeg ⟨w, hwB⟩), ?_⟩ |
| 301 | exact (mem_commonNeighborCodes G A B d hdeg u' v' |
| 302 | (localPairCode G A d w u'.1 v'.1 u'.2 v'.2 |
| 303 | (G.symm huw.1) (G.symm huw.2) (fun h => huv' (Subtype.ext h)) (hdeg ⟨w, hwB⟩))).2 |
| 304 | ⟨w, hwB, fun h => huv' (Subtype.ext h), G.symm huw.1, G.symm huw.2, rfl⟩ |
| 305 | have hcolor0 : edgeColor G A B d hdeg u' v' = Fin.last k := by |
| 306 | have hcolor' : c0 s(u', v') = Fin.last k := by |
| 307 | apply Fin.ext |
| 308 | simpa [c, sizes, lastColor] using congrArg Fin.val hcolor |
| 309 | simpa [c0] using hcolor' |
| 310 | have hnotlast : |
| 311 | edgeColor G A B d hdeg u' v' ≠ Fin.last k := by |
| 312 | have hbase : |
| 313 | Fin.castLE (Nat.le_succ k) ((commonNeighborCodes G A B d hdeg u' v').min' hcodes_nonempty) ≠ |
| 314 | Fin.last k := by |
| 315 | intro h |
| 316 | have hval := congrArg Fin.val h |
| 317 | exact Nat.ne_of_lt ((commonNeighborCodes G A B d hdeg u' v').min' hcodes_nonempty).isLt hval |
| 318 | simpa [edgeColor, hcodes_nonempty] using hbase |
| 319 | exact hnotlast hcolor0 |
| 320 | · have hik1 : i.1 < k + 1 := by |
| 321 | simpa [sizes] using i.isLt |
| 322 | have hj : i.1 < k := by |
| 323 | omega |
| 324 | let j : Fin k := ⟨i.1, hj⟩ |
| 325 | have htle : t ≤ S.card := by |
| 326 | simpa [sizes, List.get_eq_getElem, hj] using hsize |
| 327 | obtain ⟨T, hTS, hTcard⟩ : ∃ T : Finset ↑(A : Set V), T ⊆ S ∧ T.card = t := by |
| 328 | obtain ⟨T, hT⟩ := Finset.powersetCard_nonempty.2 htle |
| 329 | exact ⟨T, (Finset.mem_powersetCard.mp hT).1, (Finset.mem_powersetCard.mp hT).2⟩ |
| 330 | let f0 : Fin t ↪ ↑(T : Set ↑(A : Set V)) := |
| 331 | (Fintype.equivFinOfCardEq |
| 332 | (α := ↑(T : Set ↑(A : Set V))) |
| 333 | (by rw [Fintype.card_of_finset' T (fun x => Iff.rfl), hTcard])).symm.toEmbedding |
| 334 | let f : Fin t ↪ V := { |
| 335 | toFun x := (f0 x).1.1 |
| 336 | inj' := by |
| 337 | intro a b hab |
| 338 | apply f0.inj' |
| 339 | apply Subtype.ext |
| 340 | apply Subtype.ext |
| 341 | exact hab |
| 342 | } |
| 343 | have hfA : Set.range f ⊆ ↑A := by |
| 344 | intro x hx |
| 345 | rcases hx with ⟨a, rfl⟩ |
| 346 | exact (f0 a).1.2 |
| 347 | have hcolor_edge : |
| 348 | ∀ a b : Fin t, a ≠ b → |
| 349 | edgeColor G A B d hdeg ((f0 a).1) ((f0 b).1) = Fin.castLE (Nat.le_succ k) j := by |
| 350 | intro a b hab |
| 351 | have hab' : (f0 a).1 ≠ (f0 b).1 := by |
| 352 | intro h |
| 353 | apply hab |
| 354 | exact f0.inj' (Subtype.ext h) |
| 355 | have haS : (f0 a).1 ∈ S := hTS (f0 a).2 |
| 356 | have hbS : (f0 b).1 ∈ S := hTS (f0 b).2 |
| 357 | have hpair' : c s((f0 a).1, (f0 b).1) = i := hpair haS hbS hab' |
| 358 | apply Fin.ext |
| 359 | simpa [c, c0, sizes, j] using congrArg Fin.val hpair' |
| 360 | have hmid : |
| 361 | ∀ a b : Fin t, ∀ hab : a ≠ b, |
| 362 | ∃ (w : V) (hwB : w ∈ B) (hwa : G.Adj w (f a)) (hwb : G.Adj w (f b)), |
| 363 | localPairCode G A d w (f a) (f b) |
| 364 | ((f0 a).1).2 ((f0 b).1).2 |
| 365 | hwa hwb |
| 366 | (fun h => hab (f.injective h)) (hdeg ⟨w, hwB⟩) = j := by |
| 367 | intro a b hab |
| 368 | simpa [f] using |
| 369 | exists_commonNeighbor_of_edgeColor_eq G A B d hdeg |
| 370 | (u := ((f0 a).1)) (v := ((f0 b).1)) |
| 371 | (fun h => hab (f0.inj' (Subtype.ext h))) (hcolor_edge a b hab) |
| 372 | let edgeTail : (SimpleGraph.completeGraph (Fin t)).edgeSet → Fin t := fun e => e.1.out.1 |
| 373 | have hedgeTail_mem : ∀ e : (SimpleGraph.completeGraph (Fin t)).edgeSet, |
| 374 | edgeTail e ∈ (e : Sym2 (Fin t)) := by |
| 375 | intro e |
| 376 | exact Sym2.out_fst_mem (e : Sym2 (Fin t)) |
| 377 | let edgeHead : (SimpleGraph.completeGraph (Fin t)).edgeSet → Fin t := |
| 378 | fun e => Sym2.Mem.other (hedgeTail_mem e) |
| 379 | have hedge_ne : ∀ e : (SimpleGraph.completeGraph (Fin t)).edgeSet, edgeTail e ≠ edgeHead e := by |
| 380 | intro e |
| 381 | have heMem : s(edgeTail e, edgeHead e) ∈ (SimpleGraph.completeGraph (Fin t)).edgeSet := by |
| 382 | rw [Sym2.other_spec (hedgeTail_mem e)] |
| 383 | exact e.2 |
| 384 | have heAdj : (SimpleGraph.completeGraph (Fin t)).Adj (edgeTail e) (edgeHead e) := by |
| 385 | rw [SimpleGraph.mem_edgeSet] at heMem |
| 386 | exact heMem |
| 387 | exact (SimpleGraph.top_adj _ _).mp heAdj |
| 388 | let edgeMid : (SimpleGraph.completeGraph (Fin t)).edgeSet → V := |
| 389 | fun e => (hmid (edgeTail e) (edgeHead e) (hedge_ne e)).choose |
| 390 | have hedgeMid_memB : ∀ e : (SimpleGraph.completeGraph (Fin t)).edgeSet, edgeMid e ∈ B := by |
| 391 | intro e |
| 392 | exact (hmid (edgeTail e) (edgeHead e) (hedge_ne e)).choose_spec.1 |
| 393 | have hedgeMid_adj_tail : |
| 394 | ∀ e : (SimpleGraph.completeGraph (Fin t)).edgeSet, G.Adj (edgeMid e) (f (edgeTail e)) := by |
| 395 | intro e |
| 396 | exact (hmid (edgeTail e) (edgeHead e) (hedge_ne e)).choose_spec.2.1 |
| 397 | have hedgeMid_adj_head : |
| 398 | ∀ e : (SimpleGraph.completeGraph (Fin t)).edgeSet, G.Adj (edgeMid e) (f (edgeHead e)) := by |
| 399 | intro e |
| 400 | exact (hmid (edgeTail e) (edgeHead e) (hedge_ne e)).choose_spec.2.2.1 |
| 401 | have hedgeMid_code : |
| 402 | ∀ e : (SimpleGraph.completeGraph (Fin t)).edgeSet, |
| 403 | localPairCode G A d (edgeMid e) (f (edgeTail e)) (f (edgeHead e)) |
| 404 | ((f0 (edgeTail e)).1).2 ((f0 (edgeHead e)).1).2 |
| 405 | (hedgeMid_adj_tail e) (hedgeMid_adj_head e) |
| 406 | (fun h => hedge_ne e (f.injective h)) (hdeg ⟨edgeMid e, hedgeMid_memB e⟩) = j := by |
| 407 | intro e |
| 408 | exact (hmid (edgeTail e) (edgeHead e) (hedge_ne e)).choose_spec.2.2.2 |
| 409 | refine Or.inr (Or.inl ⟨{ |
| 410 | branchVertex := f |
| 411 | edgeTail := edgeTail |
| 412 | edgeTail_mem := hedgeTail_mem |
| 413 | edgePath := fun e => |
| 414 | SimpleGraph.Walk.cons (G.symm (hedgeMid_adj_tail e)) |
| 415 | (SimpleGraph.Walk.cons (hedgeMid_adj_head e) SimpleGraph.Walk.nil) |
| 416 | edgePath_isPath := by |
| 417 | intro e |
| 418 | have hfw : f (edgeTail e) ≠ edgeMid e := by |
| 419 | intro hEq |
| 420 | exact Finset.disjoint_left.mp hAB (hfA ⟨edgeTail e, rfl⟩) (hEq ▸ hedgeMid_memB e) |
| 421 | have hff : f (edgeTail e) ≠ f (edgeHead e) := by |
| 422 | exact fun h => hedge_ne e (f.injective h) |
| 423 | exact SimpleGraph.Walk.IsPath.cons |
| 424 | (SimpleGraph.Walk.IsPath.of_adj (hedgeMid_adj_head e)) |
| 425 | (by simp [hfw, hff]) |
| 426 | edgePath_length := by |
| 427 | intro e |
| 428 | simp |
| 429 | edgePath_interior_avoids_branch := by |
| 430 | intro e x hx htail hhead w |
| 431 | have hxmid : x = edgeMid e := by |
| 432 | have hx' : x = edgeMid e ∨ x = f (edgeHead e) := by |
| 433 | simpa [htail] using hx |
| 434 | rcases hx' with hx' | hx' |
| 435 | · exact hx' |
| 436 | · exact (hhead hx').elim |
| 437 | intro hEq |
| 438 | have hbranchA : f w ∈ A := hfA ⟨w, rfl⟩ |
| 439 | have hmidB : edgeMid e ∈ B := hedgeMid_memB e |
| 440 | have hEq' : edgeMid e = f w := hxmid.symm.trans hEq |
| 441 | exact Finset.disjoint_left.mp hAB hbranchA (hEq' ▸ hmidB) |
| 442 | edgePath_interior_disjoint := by |
| 443 | intro e e' x hne hx hx' htail hhead htail' hhead' |
| 444 | have hxmid : x = edgeMid e := by |
| 445 | have hx'' : x = edgeMid e ∨ x = f (edgeHead e) := by |
| 446 | simpa [htail] using hx |
| 447 | rcases hx'' with hx'' | hx'' |
| 448 | · exact hx'' |
| 449 | · exact (hhead hx'').elim |
| 450 | have hxmid' : x = edgeMid e' := by |
| 451 | have hx'' : x = edgeMid e' ∨ x = f (edgeHead e') := by |
| 452 | simpa [htail'] using hx' |
| 453 | rcases hx'' with hx'' | hx'' |
| 454 | · exact hx'' |
| 455 | · exact (hhead' hx'').elim |
| 456 | have hmidEq : edgeMid e = edgeMid e' := hxmid.symm.trans hxmid' |
| 457 | let bmid := edgeMid e |
| 458 | have hbmidB : bmid ∈ B := hedgeMid_memB e |
| 459 | have htail'_adj : G.Adj bmid (f (edgeTail e')) := by |
| 460 | simpa [bmid, hmidEq] using hedgeMid_adj_tail e' |
| 461 | have hhead'_adj : G.Adj bmid (f (edgeHead e')) := by |
| 462 | simpa [bmid, hmidEq] using hedgeMid_adj_head e' |
| 463 | have hcodeEq : |
| 464 | localPairCode G A d bmid (f (edgeTail e)) (f (edgeHead e)) |
| 465 | ((f0 (edgeTail e)).1).2 ((f0 (edgeHead e)).1).2 |
| 466 | (hedgeMid_adj_tail e) (hedgeMid_adj_head e) |
| 467 | (fun h => hedge_ne e (f.injective h)) (hdeg ⟨bmid, hbmidB⟩) = |
| 468 | localPairCode G A d bmid (f (edgeTail e')) (f (edgeHead e')) |
| 469 | ((f0 (edgeTail e')).1).2 ((f0 (edgeHead e')).1).2 |
| 470 | htail'_adj hhead'_adj |
| 471 | (fun h => hedge_ne e' (f.injective h)) (hdeg ⟨bmid, hbmidB⟩) := by |
| 472 | calc |
| 473 | localPairCode G A d bmid (f (edgeTail e)) (f (edgeHead e)) |
| 474 | ((f0 (edgeTail e)).1).2 ((f0 (edgeHead e)).1).2 |
| 475 | (hedgeMid_adj_tail e) (hedgeMid_adj_head e) |
| 476 | (fun h => hedge_ne e (f.injective h)) (hdeg ⟨bmid, hbmidB⟩) = j := by |
| 477 | exact hedgeMid_code e |
| 478 | _ = localPairCode G A d bmid (f (edgeTail e')) (f (edgeHead e')) |
| 479 | ((f0 (edgeTail e')).1).2 ((f0 (edgeHead e')).1).2 |
| 480 | htail'_adj hhead'_adj |
| 481 | (fun h => hedge_ne e' (f.injective h)) (hdeg ⟨bmid, hbmidB⟩) := by |
| 482 | simpa [bmid, hmidEq] using (hedgeMid_code e').symm |
| 483 | have hpairV : |
| 484 | s(f (edgeTail e), f (edgeHead e)) = s(f (edgeTail e'), f (edgeHead e')) := by |
| 485 | exact localPairCode_injective G A d |
| 486 | ((f0 (edgeTail e)).1).2 ((f0 (edgeHead e)).1).2 |
| 487 | ((f0 (edgeTail e')).1).2 ((f0 (edgeHead e')).1).2 |
| 488 | (hedgeMid_adj_tail e) (hedgeMid_adj_head e) |
| 489 | htail'_adj hhead'_adj |
| 490 | (fun h => hedge_ne e (f.injective h)) |
| 491 | (fun h => hedge_ne e' (f.injective h)) |
| 492 | (hdeg ⟨bmid, hbmidB⟩) hcodeEq |
| 493 | have hpairFin : |
| 494 | s(edgeTail e, edgeHead e) = s(edgeTail e', edgeHead e') := by |
| 495 | apply (Sym2.map.injective f.injective) |
| 496 | simpa using hpairV |
| 497 | have heq : e = e' := by |
| 498 | apply Subtype.ext |
| 499 | calc |
| 500 | (e : Sym2 (Fin t)) = s(edgeTail e, edgeHead e) := by |
| 501 | symm |
| 502 | exact Sym2.other_spec (hedgeTail_mem e) |
| 503 | _ = s(edgeTail e', edgeHead e') := hpairFin |
| 504 | _ = (e' : Sym2 (Fin t)) := by |
| 505 | exact Sym2.other_spec (hedgeTail_mem e') |
| 506 | exact hne heq |
| 507 | }, hfA⟩) |
| 508 | |
| 509 | end Catalog.Sparsity.BipartiteRamsey |
| 510 |