Catalog/Sparsity/IterativeBipartiteRamsey/Full.lean
| 1 | import Catalog.Sparsity.BipartiteRamsey.Full |
| 2 | import Catalog.Sparsity.ShallowTopologicalMinor.Full |
| 3 | |
| 4 | namespace Catalog.Sparsity.IterativeBipartiteRamsey |
| 5 | |
| 6 | open Catalog.Sparsity.BipartiteRamsey |
| 7 | open Catalog.Sparsity.ShallowTopologicalMinor |
| 8 | |
| 9 | /-- Recursive bound for the iterative bipartite Ramsey lemma. -/ |
| 10 | private noncomputable def R_star : ℕ → ℕ → ℕ → ℕ |
| 11 | | 0, t, _ => t |
| 12 | | s + 1, t, m => (bipartiteRamsey m t (R_star s t m)).choose |
| 13 | |
| 14 | private noncomputable def topologicalMinorModel_of_subgraph |
| 15 | {V W : Type} {H : SimpleGraph W} {G G' : SimpleGraph V} {d : ℕ} |
| 16 | (M : ShallowTopologicalMinorModel H G d) |
| 17 | (hsub : ∀ {u v}, G.Adj u v → G'.Adj u v) : |
| 18 | ShallowTopologicalMinorModel H G' d := |
| 19 | { branchVertex := M.branchVertex |
| 20 | edgeTail := M.edgeTail |
| 21 | edgeTail_mem := M.edgeTail_mem |
| 22 | edgePath := fun e => by |
| 23 | let p := M.edgePath e |
| 24 | have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by |
| 25 | intro e' he' |
| 26 | have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he' |
| 27 | revert hmem |
| 28 | refine e'.ind ?_ |
| 29 | intro a b hab |
| 30 | exact show G'.Adj a b by exact hsub hab |
| 31 | exact p.transfer G' hedge |
| 32 | edgePath_isPath := by |
| 33 | intro e |
| 34 | let p := M.edgePath e |
| 35 | have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by |
| 36 | intro e' he' |
| 37 | have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he' |
| 38 | revert hmem |
| 39 | refine e'.ind ?_ |
| 40 | intro a b hab |
| 41 | exact show G'.Adj a b by exact hsub hab |
| 42 | simpa [p] using (M.edgePath_isPath e).transfer hedge |
| 43 | edgePath_length := by |
| 44 | intro e |
| 45 | let p := M.edgePath e |
| 46 | have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by |
| 47 | intro e' he' |
| 48 | have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he' |
| 49 | revert hmem |
| 50 | refine e'.ind ?_ |
| 51 | intro a b hab |
| 52 | exact show G'.Adj a b by exact hsub hab |
| 53 | rw [show ((p.transfer G' hedge)).length = p.length by |
| 54 | rw [SimpleGraph.Walk.length_transfer]] |
| 55 | exact M.edgePath_length e |
| 56 | edgePath_interior_avoids_branch := by |
| 57 | intro e x hx htail hhead w |
| 58 | let p := M.edgePath e |
| 59 | have hedge : ∀ e' ∈ p.edges, e' ∈ G'.edgeSet := by |
| 60 | intro e' he' |
| 61 | have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he' |
| 62 | revert hmem |
| 63 | refine e'.ind ?_ |
| 64 | intro a b hab |
| 65 | exact show G'.Adj a b by exact hsub hab |
| 66 | rw [show (p.transfer G' hedge).support = p.support by |
| 67 | rw [SimpleGraph.Walk.support_transfer]] at hx |
| 68 | exact M.edgePath_interior_avoids_branch e hx htail hhead w |
| 69 | edgePath_interior_disjoint := by |
| 70 | intro e e' x hne hx hx' htail hhead htail' hhead' |
| 71 | let p := M.edgePath e |
| 72 | let p' := M.edgePath e' |
| 73 | have hedge : ∀ e'' ∈ p.edges, e'' ∈ G'.edgeSet := by |
| 74 | intro e'' he'' |
| 75 | have hmem := SimpleGraph.Walk.edges_subset_edgeSet p he'' |
| 76 | revert hmem |
| 77 | refine e''.ind ?_ |
| 78 | intro a b hab |
| 79 | exact show G'.Adj a b by exact hsub hab |
| 80 | have hedge' : ∀ e'' ∈ p'.edges, e'' ∈ G'.edgeSet := by |
| 81 | intro e'' he'' |
| 82 | have hmem := SimpleGraph.Walk.edges_subset_edgeSet p' he'' |
| 83 | revert hmem |
| 84 | refine e''.ind ?_ |
| 85 | intro a b hab |
| 86 | exact show G'.Adj a b by exact hsub hab |
| 87 | rw [show (p.transfer G' hedge).support = p.support by |
| 88 | rw [SimpleGraph.Walk.support_transfer]] at hx |
| 89 | rw [show (p'.transfer G' hedge').support = p'.support by |
| 90 | rw [SimpleGraph.Walk.support_transfer]] at hx' |
| 91 | exact M.edgePath_interior_disjoint e e' hne hx hx' htail hhead htail' hhead' } |
| 92 | |
| 93 | /-- Core induction: with `s` steps remaining and `collected` vertices already |
| 94 | gathered (each adjacent to all of `A_cur`), produce one of the three |
| 95 | outcomes of Lemma 3.10. -/ |
| 96 | private theorem iterStep (m t : ℕ) : |
| 97 | ∀ (s : ℕ), ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 98 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 99 | (A B A_cur collected : Finset V), |
| 100 | Disjoint A B → |
| 101 | (∀ u v, G.Adj u v → (u ∈ A ∧ v ∈ B) ∨ (u ∈ B ∧ v ∈ A)) → |
| 102 | A_cur ⊆ A → collected ⊆ B → |
| 103 | R_star s t m ≤ A_cur.card → |
| 104 | collected.card + s = t → |
| 105 | (∀ v ∈ collected, ∀ u ∈ A_cur, G.Adj u v) → |
| 106 | (∃ (A' S : Finset V), |
| 107 | A' ⊆ A ∧ S ⊆ B ∧ m ≤ A'.card ∧ S.card < t ∧ |
| 108 | (↑A' : Set V).Pairwise (fun u v => |
| 109 | ∀ w, w ∉ (S : Set V) → ¬(G.Adj u w ∧ G.Adj v w))) ∨ |
| 110 | (∃ M : ShallowTopologicalMinorModel |
| 111 | (SimpleGraph.completeGraph (Fin t)) G 1, |
| 112 | Set.range M.branchVertex ⊆ ↑A) ∨ |
| 113 | (∃ (X Y : Finset V), |
| 114 | X ⊆ A ∧ Y ⊆ B ∧ t ≤ X.card ∧ t ≤ Y.card ∧ |
| 115 | ∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) := by |
| 116 | intro s |
| 117 | induction s with |
| 118 | | zero => |
| 119 | -- Base case: collected has t elements, |A_cur| ≥ t → build K_{t,t} |
| 120 | intro V _ _ G _ A B A_cur collected _ _ hAcur hCsub hCard hSum hAllAdj |
| 121 | right; right |
| 122 | obtain ⟨X, hXsub, hXcard⟩ := Finset.exists_subset_card_eq (show t ≤ A_cur.card from hCard) |
| 123 | exact ⟨X, collected, hXsub.trans hAcur, hCsub, hXcard.ge, |
| 124 | (show collected.card = t by omega).ge, |
| 125 | fun x hx y hy => hAllAdj y hy x (hXsub hx)⟩ |
| 126 | | succ s ih => |
| 127 | intro V _ _ G _ A B A_cur collected hAB hBip hAcur hCsub hCard hSum hAllAdj |
| 128 | -- Restrict G to edges within A_cur ∪ (B \ collected) for bipartiteness |
| 129 | let B_cur : Finset V := B \ collected |
| 130 | let Sbip : Finset V := A_cur ∪ B_cur |
| 131 | let G' : SimpleGraph V := |
| 132 | { Adj := fun u v => G.Adj u v ∧ u ∈ Sbip ∧ v ∈ Sbip |
| 133 | symm := fun _ _ h => ⟨G.symm h.1, h.2.2, h.2.1⟩ |
| 134 | loopless := ⟨fun u h => G.loopless.irrefl u h.1⟩ } |
| 135 | haveI : DecidableRel G'.Adj := fun u v => inferInstance |
| 136 | have hDisj' : Disjoint A_cur B_cur := by |
| 137 | rw [Finset.disjoint_left]; intro x hx1 hx2 |
| 138 | exact Finset.disjoint_left.mp hAB (hAcur hx1) (Finset.mem_sdiff.mp hx2).1 |
| 139 | have hBip' : ∀ u v, G'.Adj u v → |
| 140 | (u ∈ A_cur ∧ v ∈ B_cur) ∨ (u ∈ B_cur ∧ v ∈ A_cur) := by |
| 141 | intro u v ⟨hAdj, huS, hvS⟩ |
| 142 | rcases hBip u v hAdj with ⟨huA, hvB⟩ | ⟨huB, hvA⟩ |
| 143 | · left; constructor |
| 144 | · rcases Finset.mem_union.mp huS with h | h |
| 145 | · exact h |
| 146 | · exact absurd (Finset.mem_sdiff.mp h).1 (Finset.disjoint_left.mp hAB huA) |
| 147 | · rcases Finset.mem_union.mp hvS with h | h |
| 148 | · exact absurd hvB (Finset.disjoint_left.mp hAB (hAcur h)) |
| 149 | · exact h |
| 150 | · right; constructor |
| 151 | · rcases Finset.mem_union.mp huS with h | h |
| 152 | · exact absurd huB (Finset.disjoint_left.mp hAB (hAcur h)) |
| 153 | · exact h |
| 154 | · rcases Finset.mem_union.mp hvS with h | h |
| 155 | · exact h |
| 156 | · exact absurd (Finset.mem_sdiff.mp h).1 (Finset.disjoint_left.mp hAB hvA) |
| 157 | -- Apply BipartiteRamsey to G' with A_cur, B_cur |
| 158 | rcases (bipartiteRamsey m t (R_star s t m)).choose_spec |
| 159 | G' A_cur B_cur hDisj' hBip' hCard with |
| 160 | ⟨A', hA'sub, hA'card, hA'pair⟩ | ⟨M, hMrange⟩ | ⟨v, hvBcur, hvdeg⟩ |
| 161 | · -- Outcome (a): no common G'-neighbor → (a) with S = collected |
| 162 | left |
| 163 | refine ⟨A', collected, hA'sub.trans hAcur, hCsub, hA'card, by omega, ?_⟩ |
| 164 | intro u hu v hv huv w hw ⟨huw, hvw⟩ |
| 165 | have huAcur : u ∈ A_cur := hA'sub hu |
| 166 | have hvAcur : v ∈ A_cur := hA'sub hv |
| 167 | have hwB : w ∈ B := by |
| 168 | rcases hBip u w huw with ⟨_, h⟩ | ⟨h, _⟩ |
| 169 | · exact h |
| 170 | · exact absurd h (Finset.disjoint_left.mp hAB (hAcur huAcur)) |
| 171 | have hwBcur : w ∈ B_cur := |
| 172 | Finset.mem_sdiff.mpr ⟨hwB, fun h => hw (Finset.mem_coe.mpr h)⟩ |
| 173 | exact hA'pair hu hv huv w |
| 174 | ⟨⟨huw, Finset.mem_union.mpr (Or.inl huAcur), Finset.mem_union.mpr (Or.inr hwBcur)⟩, |
| 175 | ⟨hvw, Finset.mem_union.mpr (Or.inl hvAcur), Finset.mem_union.mpr (Or.inr hwBcur)⟩⟩ |
| 176 | · -- Outcome (b): pass the topological minor through unchanged |
| 177 | right; left |
| 178 | exact ⟨topologicalMinorModel_of_subgraph M (fun {u v} h => h.1), |
| 179 | hMrange.trans (Finset.coe_subset.mpr hAcur)⟩ |
| 180 | · -- Outcome (c): high-degree vertex in B_cur → iterate |
| 181 | have hvB := (Finset.mem_sdiff.mp hvBcur).1 |
| 182 | have hvNotColl := (Finset.mem_sdiff.mp hvBcur).2 |
| 183 | let A_next := A_cur.filter (G.Adj v ·) |
| 184 | have hAnextCard : R_star s t m ≤ A_next.card := by |
| 185 | apply le_trans hvdeg |
| 186 | apply Finset.card_le_card |
| 187 | intro w hw |
| 188 | rw [Finset.mem_inter] at hw |
| 189 | rw [Finset.mem_filter] |
| 190 | exact ⟨hw.2, (G'.mem_neighborFinset v w |>.mp hw.1).1⟩ |
| 191 | exact ih G A B A_next (insert v collected) |
| 192 | hAB hBip |
| 193 | ((Finset.filter_subset _ _).trans hAcur) |
| 194 | (Finset.insert_subset_iff.mpr ⟨hvB, hCsub⟩) |
| 195 | hAnextCard |
| 196 | (by rw [Finset.card_insert_of_notMem hvNotColl]; omega) |
| 197 | (fun w hw u hu => by |
| 198 | rcases Finset.mem_insert.mp hw with rfl | hw' |
| 199 | · exact G.symm (Finset.mem_filter.mp hu).2 |
| 200 | · exact hAllAdj w hw' u (Finset.filter_subset _ _ hu)) |
| 201 | |
| 202 | /-- Lemma 3.10: iterative version of bipartite Ramsey. In a bipartite graph with |
| 203 | sides `A` and `B`, if `|A|` is large enough, then at least one of: |
| 204 | (a) `A` contains `m` vertices and `B` contains a small separator `S` of size |
| 205 | `< t` such that no two vertices of `A'` have a common neighbor outside `S`, |
| 206 | (b) `G` contains a `1`-subdivision of `K_t` with principal vertices in `A`, |
| 207 | (c) `G` contains a complete bipartite subgraph `K_{t,t}`. -/ |
| 208 | theorem iterativeBipartiteRamsey (m t : ℕ) : |
| 209 | ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 210 | (G : SimpleGraph V) [DecidableRel G.Adj] |
| 211 | (A B : Finset V), |
| 212 | Disjoint A B → |
| 213 | (∀ u v, G.Adj u v → (u ∈ A ∧ v ∈ B) ∨ (u ∈ B ∧ v ∈ A)) → |
| 214 | N ≤ A.card → |
| 215 | (∃ (A' : Finset V) (S : Finset V), |
| 216 | A' ⊆ A ∧ S ⊆ B ∧ m ≤ A'.card ∧ S.card < t ∧ |
| 217 | (↑A' : Set V).Pairwise (fun u v => |
| 218 | ∀ w, w ∉ (S : Set V) → ¬(G.Adj u w ∧ G.Adj v w))) ∨ |
| 219 | (∃ M : ShallowTopologicalMinorModel |
| 220 | (SimpleGraph.completeGraph (Fin t)) G 1, |
| 221 | Set.range M.branchVertex ⊆ ↑A) ∨ |
| 222 | (∃ (X : Finset V) (Y : Finset V), |
| 223 | X ⊆ A ∧ Y ⊆ B ∧ t ≤ X.card ∧ t ≤ Y.card ∧ |
| 224 | ∀ x ∈ X, ∀ y ∈ Y, G.Adj x y) := by |
| 225 | exact ⟨R_star t t m, fun {V} [_] [_] G [_] A B hAB hBip hCard => |
| 226 | iterStep m t t G A B A ∅ hAB hBip Finset.Subset.rfl (Finset.empty_subset _) |
| 227 | hCard (by simp) (fun _ h => absurd h (Finset.notMem_empty _))⟩ |
| 228 | |
| 229 | end Catalog.Sparsity.IterativeBipartiteRamsey |
| 230 |