Catalog/Sparsity/StrongColoringBoundByAdm/Full.lean
| 1 | import Mathlib.Tactic |
| 2 | import Catalog.Sparsity.Admissibility.Full |
| 3 | import Catalog.Sparsity.ColoringNumbers.Full |
| 4 | import Catalog.Sparsity.StrongColoringBoundByAdm.TreeCounting |
| 5 | |
| 6 | open Classical |
| 7 | |
| 8 | namespace Catalog.Sparsity.StrongColoringBoundByAdm |
| 9 | |
| 10 | noncomputable section |
| 11 | |
| 12 | variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V] |
| 13 | |
| 14 | open Catalog.Sparsity.Admissibility |
| 15 | open Catalog.Sparsity.ColoringNumbers |
| 16 | |
| 17 | /-- Every vertex is in its own strong r-reachability set. -/ |
| 18 | private theorem self_mem_sreach (G : SimpleGraph V) (r : ℕ) (v : V) : |
| 19 | v ∈ SReach G r v := by |
| 20 | simp [SReach] |
| 21 | |
| 22 | /-- Per-vertex admissibility is at most the global admissibility. -/ |
| 23 | private theorem admVertex_le_adm (G : SimpleGraph V) (r : ℕ) (v : V) : |
| 24 | admVertex G r v ≤ adm G r := by |
| 25 | unfold adm |
| 26 | exact Finset.le_sup (f := fun w => admVertex G r w) (by simp) |
| 27 | |
| 28 | private theorem sreach_predecessor (G : SimpleGraph V) (r : ℕ) (v u : V) |
| 29 | (hu : u ∈ SReach G r v) (hne : u ≠ v) : |
| 30 | u < v ∧ ∃ (u' : V) (p : G.Walk v u'), |
| 31 | v ≤ u' ∧ G.Adj u' u ∧ |
| 32 | (∀ x ∈ p.support, v ≤ x) ∧ p.length + 1 ≤ r := by |
| 33 | rcases hu with ⟨hu_le, p, hp_path, hp_len, hp_internal⟩ |
| 34 | have hu_lt : u < v := lt_of_le_of_ne hu_le hne |
| 35 | have hp_not_nil : ¬ p.Nil := by |
| 36 | rw [SimpleGraph.Walk.nil_iff_length_eq] |
| 37 | intro hp_zero |
| 38 | apply hne |
| 39 | have huv : v = u := by |
| 40 | have hv : v = p.getVert p.length := by |
| 41 | simpa [hp_zero] using p.getVert_zero.symm |
| 42 | exact hv.trans p.getVert_length |
| 43 | exact huv.symm |
| 44 | refine ⟨hu_lt, p.penultimate, p.dropLast, ?_⟩ |
| 45 | refine ⟨?_, p.adj_penultimate hp_not_nil, ?_, ?_⟩ |
| 46 | · by_cases hlen : p.length = 1 |
| 47 | · simp [SimpleGraph.Walk.penultimate, hlen] |
| 48 | · have hpos : 0 < p.length := Nat.pos_of_ne_zero fun hzero => |
| 49 | hp_not_nil (SimpleGraph.Walk.nil_iff_length_eq.mpr hzero) |
| 50 | have hlt : p.length - 1 < p.length := Nat.sub_lt hpos (by decide) |
| 51 | exact le_of_lt (hp_internal (p.length - 1) (by omega) hlt) |
| 52 | · intro x hx |
| 53 | rcases (SimpleGraph.Walk.mem_support_iff_exists_getVert.mp hx) with ⟨n, rfl, hnle⟩ |
| 54 | have hdrop_len : p.dropLast.length = p.length - 1 := by |
| 55 | simp [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_length] |
| 56 | have htake : p.dropLast.getVert n = p.getVert n := by |
| 57 | rw [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_getVert] |
| 58 | simp [hdrop_len] at hnle |
| 59 | simp [Nat.min_eq_right hnle] |
| 60 | rw [htake] |
| 61 | by_cases hn : n = 0 |
| 62 | · simp [hn] |
| 63 | · have hdrop_len' : n ≤ p.length - 1 := by |
| 64 | simpa [hdrop_len] using hnle |
| 65 | have hlt : n < p.length := by omega |
| 66 | exact le_of_lt (hp_internal n (Nat.pos_of_ne_zero hn) hlt) |
| 67 | · have hlen_drop : p.dropLast.length = p.length - 1 := by |
| 68 | simp [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_length] |
| 69 | have hpos : 0 < p.length := Nat.pos_of_ne_zero fun hzero => |
| 70 | hp_not_nil (SimpleGraph.Walk.nil_iff_length_eq.mpr hzero) |
| 71 | rw [hlen_drop] |
| 72 | have hsub : p.length - 1 + 1 = p.length := by |
| 73 | omega |
| 74 | rw [hsub] |
| 75 | exact hp_len |
| 76 | |
| 77 | private theorem iterate_root_eq {α : Type*} (par : α → α) {v : α} (hpar_root : par v = v) : |
| 78 | ∀ m, par^[m] v = v := by |
| 79 | intro m |
| 80 | induction m with |
| 81 | | zero => rfl |
| 82 | | succ m ihm => |
| 83 | rw [Function.iterate_succ_apply] |
| 84 | simp [hpar_root, ihm] |
| 85 | |
| 86 | private theorem above_v_bfs_data (G : SimpleGraph V) (r : ℕ) (v : V) : |
| 87 | ∃ (d : V → ℕ) (bp : V → V), |
| 88 | d v = 0 ∧ bp v = v ∧ |
| 89 | (∀ w, v ≤ w → d w ≤ r → w ≠ v → |
| 90 | v ≤ bp w ∧ G.Adj (bp w) w ∧ d (bp w) + 1 = d w) ∧ |
| 91 | (∀ w (p : G.Walk v w), (∀ x ∈ p.support, v ≤ x) → p.length ≤ r → |
| 92 | d w ≤ p.length) ∧ |
| 93 | (∀ w, v ≤ w → d w ≤ r → |
| 94 | ∃ p : G.Walk v w, (∀ x ∈ p.support, v ≤ x) ∧ p.length = d w) := by |
| 95 | let Good : V → ℕ → Prop := fun w n => |
| 96 | ∃ p : G.Walk v w, (∀ x ∈ p.support, v ≤ x) ∧ p.length = n |
| 97 | let d : V → ℕ := fun w => |
| 98 | if h : ∃ n, n ≤ r ∧ Good w n then Nat.find h else r + 1 |
| 99 | have hd_lower : ∀ w (p : G.Walk v w), (∀ x ∈ p.support, v ≤ x) → p.length ≤ r → |
| 100 | d w ≤ p.length := by |
| 101 | intro w p hp_support hp_len |
| 102 | have hgood : ∃ n, n ≤ r ∧ Good w n := ⟨p.length, hp_len, p, hp_support, rfl⟩ |
| 103 | change (if h : ∃ n, n ≤ r ∧ Good w n then Nat.find h else r + 1) ≤ p.length |
| 104 | rw [dif_pos hgood] |
| 105 | exact Nat.find_min' hgood ⟨hp_len, p, hp_support, rfl⟩ |
| 106 | have hd_achieve : ∀ w, v ≤ w → d w ≤ r → |
| 107 | ∃ p : G.Walk v w, (∀ x ∈ p.support, v ≤ x) ∧ p.length = d w := by |
| 108 | intro w hwv hdwr |
| 109 | by_cases hgood : ∃ n, n ≤ r ∧ Good w n |
| 110 | · have hspec := Nat.find_spec hgood |
| 111 | rcases hspec with ⟨_, p, hp_support, hp_len⟩ |
| 112 | refine ⟨p, hp_support, ?_⟩ |
| 113 | simpa [d, hgood] using hp_len |
| 114 | · exfalso |
| 115 | have : r + 1 ≤ r := by |
| 116 | simp [d, hgood] at hdwr |
| 117 | omega |
| 118 | have hd_v : d v = 0 := by |
| 119 | have hgood : ∃ n, n ≤ r ∧ Good v n := |
| 120 | ⟨0, Nat.zero_le _, SimpleGraph.Walk.nil, by simp, rfl⟩ |
| 121 | have hmin : Nat.find hgood ≤ 0 := |
| 122 | Nat.find_min' hgood ⟨Nat.zero_le _, SimpleGraph.Walk.nil, by simp, rfl⟩ |
| 123 | change (if h : ∃ n, n ≤ r ∧ Good v n then Nat.find h else r + 1) = 0 |
| 124 | rw [dif_pos hgood] |
| 125 | exact le_antisymm hmin (Nat.zero_le _) |
| 126 | let bp : V → V := fun w => |
| 127 | if hw : v ≤ w ∧ d w ≤ r ∧ w ≠ v then |
| 128 | let p := Classical.choose (hd_achieve w hw.1 hw.2.1) |
| 129 | p.penultimate |
| 130 | else v |
| 131 | refine ⟨d, bp, hd_v, ?_, ?_, hd_lower, hd_achieve⟩ |
| 132 | · simp [bp, hd_v] |
| 133 | · intro w hwv hdwr hwne |
| 134 | let p : G.Walk v w := Classical.choose (hd_achieve w hwv hdwr) |
| 135 | have hp_support : ∀ x ∈ p.support, v ≤ x := |
| 136 | (Classical.choose_spec (hd_achieve w hwv hdwr)).1 |
| 137 | have hp_len : p.length = d w := |
| 138 | (Classical.choose_spec (hd_achieve w hwv hdwr)).2 |
| 139 | have hp_not_nil : ¬ p.Nil := by |
| 140 | rw [SimpleGraph.Walk.nil_iff_length_eq] |
| 141 | intro hp_zero |
| 142 | apply hwne |
| 143 | have hvw : v = w := by |
| 144 | have hv : v = p.getVert p.length := by |
| 145 | simpa [hp_zero] using p.getVert_zero.symm |
| 146 | exact hv.trans p.getVert_length |
| 147 | exact hvw.symm |
| 148 | have hbp_eq : bp w = p.penultimate := by |
| 149 | simp [bp, hwv, hdwr, hwne, p] |
| 150 | have hbp_ge : v ≤ bp w := by |
| 151 | rw [hbp_eq] |
| 152 | exact hp_support _ (p.getVert_mem_support (p.length - 1)) |
| 153 | have hbp_adj : G.Adj (bp w) w := by |
| 154 | rw [hbp_eq] |
| 155 | exact p.adj_penultimate hp_not_nil |
| 156 | have hdrop_support : ∀ x ∈ p.dropLast.support, v ≤ x := by |
| 157 | intro x hx |
| 158 | have hx' : x ∈ p.support := by |
| 159 | rw [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_support_eq_support_take_succ] at hx |
| 160 | exact List.mem_of_mem_take hx |
| 161 | exact hp_support x hx' |
| 162 | have hdrop_len : p.dropLast.length = d w - 1 := by |
| 163 | rw [SimpleGraph.Walk.dropLast, SimpleGraph.Walk.take_length, hp_len, |
| 164 | Nat.min_eq_left (Nat.sub_le _ _)] |
| 165 | have hdw_pos : 0 < d w := by |
| 166 | rw [← hp_len] |
| 167 | exact Nat.pos_of_ne_zero fun hzero => |
| 168 | hp_not_nil (SimpleGraph.Walk.nil_iff_length_eq.mpr hzero) |
| 169 | have hd_pred_len : d p.penultimate ≤ p.dropLast.length := by |
| 170 | exact hd_lower (w := p.penultimate) (p := p.dropLast) hdrop_support |
| 171 | (by |
| 172 | rw [hdrop_len] |
| 173 | exact le_trans (Nat.sub_le _ _) hdwr) |
| 174 | have hd_pred_le : d (bp w) ≤ d w - 1 := by |
| 175 | rw [hbp_eq] |
| 176 | rw [hdrop_len] at hd_pred_len |
| 177 | exact hd_pred_len |
| 178 | have hd_pred_succ_le : d (bp w) + 1 ≤ d w := by |
| 179 | omega |
| 180 | have hd_pred_le_r : d (bp w) ≤ r := by |
| 181 | exact le_trans (Nat.le_of_lt (Nat.lt_of_succ_le hd_pred_succ_le)) hdwr |
| 182 | obtain ⟨q, hq_support, hq_len⟩ := hd_achieve (bp w) hbp_ge hd_pred_le_r |
| 183 | have hconcat_support : ∀ x ∈ (q.concat hbp_adj).support, v ≤ x := by |
| 184 | intro x hx |
| 185 | have hx' : x ∈ q.support ∨ x = w := by |
| 186 | simpa [SimpleGraph.Walk.support_concat] using hx |
| 187 | rcases hx' with hxq | rfl |
| 188 | · exact hq_support x hxq |
| 189 | · exact hwv |
| 190 | have hdw_len : d w ≤ (q.concat hbp_adj).length := by |
| 191 | have hq_concat_len : (q.concat hbp_adj).length ≤ r := by |
| 192 | rw [SimpleGraph.Walk.length_concat, hq_len] |
| 193 | exact le_trans hd_pred_succ_le hdwr |
| 194 | exact hd_lower (w := w) (p := q.concat hbp_adj) hconcat_support hq_concat_len |
| 195 | have hdw_le : d w ≤ d (bp w) + 1 := by |
| 196 | simpa [SimpleGraph.Walk.length_concat, hq_len] using hdw_len |
| 197 | refine ⟨hbp_ge, hbp_adj, ?_⟩ |
| 198 | exact le_antisymm hd_pred_succ_le hdw_le |
| 199 | |
| 200 | private theorem exists_walk_to_descendant |
| 201 | (G : SimpleGraph V) (v : V) |
| 202 | (S : Finset V) (par : V → V) (dep : V → ℕ) |
| 203 | (hpar_root : par v = v) |
| 204 | (hpar_mem : ∀ a ∈ S, par a ∈ S) |
| 205 | (hpar_dep : ∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a) |
| 206 | (hadj : ∀ a ∈ S, a ≠ v → G.Adj (par a) a) |
| 207 | {a x : V} (haS : a ∈ S) (ha_ne_v : a ≠ v) (hxS : x ∈ S) {n : ℕ} |
| 208 | (hiter : par^[n] x = a) : |
| 209 | ∃ q : G.Walk a x, |
| 210 | q.length = n ∧ |
| 211 | dep a + n = dep x ∧ |
| 212 | ∀ y ∈ q.support, y ∈ S ∧ ∃ m, par^[m] y = a := by |
| 213 | induction n generalizing x with |
| 214 | | zero => |
| 215 | simp only [Function.iterate_zero, id_eq] at hiter |
| 216 | subst x |
| 217 | refine ⟨SimpleGraph.Walk.nil, rfl, by simp, ?_⟩ |
| 218 | intro y hy |
| 219 | simp at hy |
| 220 | subst y |
| 221 | exact ⟨haS, ⟨0, by simp⟩⟩ |
| 222 | | succ n ih => |
| 223 | have hx_ne_v : x ≠ v := by |
| 224 | intro hxv |
| 225 | subst x |
| 226 | have : a = v := by |
| 227 | calc |
| 228 | a = par^[n.succ] v := hiter.symm |
| 229 | _ = v := iterate_root_eq par hpar_root _ |
| 230 | exact ha_ne_v this |
| 231 | have hparxS : par x ∈ S := hpar_mem x hxS |
| 232 | have hiter' : par^[n] (par x) = a := by |
| 233 | simpa [Function.iterate_succ_apply] using hiter |
| 234 | obtain ⟨q, hq_len, hq_dep, hq_support⟩ := |
| 235 | ih hparxS hiter' |
| 236 | have hadjx : G.Adj (par x) x := hadj x hxS hx_ne_v |
| 237 | have hdep_x : dep (par x) + 1 = dep x := hpar_dep x hxS hx_ne_v |
| 238 | refine ⟨q.concat hadjx, by simp [hq_len], ?_, ?_⟩ |
| 239 | · omega |
| 240 | · intro y hy |
| 241 | have hy' : y ∈ q.support ∨ y = x := by |
| 242 | simpa [SimpleGraph.Walk.support_concat] using hy |
| 243 | rcases hy' with hyq | rfl |
| 244 | · exact hq_support y hyq |
| 245 | · exact ⟨hxS, ⟨n.succ, hiter⟩⟩ |
| 246 | |
| 247 | private theorem exists_child_leaf_walk |
| 248 | (G : SimpleGraph V) (r : ℕ) (v : V) |
| 249 | (S : Finset V) (par : V → V) (dep : V → ℕ) |
| 250 | (hpar_root : par v = v) |
| 251 | (hpar_mem : ∀ a ∈ S, par a ∈ S) |
| 252 | (hpar_dep : ∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a) |
| 253 | (hdep_le : ∀ a ∈ S, dep a ≤ r) |
| 254 | (hadj : ∀ a ∈ S, a ≠ v → G.Adj (par a) a) |
| 255 | (w c u : V) |
| 256 | (hc : c ∈ treeChildren S par w) |
| 257 | (huS : u ∈ S) |
| 258 | (hdesc : ∃ n, par^[n] u = c) : |
| 259 | ∃ q : G.Walk w u, |
| 260 | q.length ≤ r ∧ |
| 261 | ∀ y ∈ q.support, y = w ∨ y ∈ S ∧ ∃ m, par^[m] y = c := by |
| 262 | rcases Finset.mem_filter.mp hc with ⟨hcS, hchild⟩ |
| 263 | rcases hchild with ⟨hparc, hc_ne_w⟩ |
| 264 | have hc_ne_v : c ≠ v := by |
| 265 | intro hcv |
| 266 | subst c |
| 267 | exact hc_ne_w (hpar_root.symm.trans hparc) |
| 268 | obtain ⟨n, hn⟩ := hdesc |
| 269 | obtain ⟨q, hq_len, hq_dep, hq_support⟩ := |
| 270 | exists_walk_to_descendant G v S par dep hpar_root hpar_mem hpar_dep hadj |
| 271 | hcS hc_ne_v huS hn |
| 272 | have hwc : G.Adj w c := by |
| 273 | simpa [hparc] using hadj c hcS hc_ne_v |
| 274 | have hdep_c : dep w + 1 = dep c := by |
| 275 | simpa [hparc] using hpar_dep c hcS hc_ne_v |
| 276 | refine ⟨SimpleGraph.Walk.cons hwc q, ?_, ?_⟩ |
| 277 | · have hdep_u := hdep_le u huS |
| 278 | simp [hq_len] |
| 279 | omega |
| 280 | · intro y hy |
| 281 | have hy' : y = w ∨ y ∈ q.support := by |
| 282 | simpa [SimpleGraph.Walk.support_cons] using hy |
| 283 | rcases hy' with rfl | hyq |
| 284 | · exact Or.inl rfl |
| 285 | · exact Or.inr (hq_support y hyq) |
| 286 | |
| 287 | set_option linter.unusedSectionVars false in |
| 288 | private theorem iterate_depth_eq |
| 289 | (S : Finset V) (par : V → V) (dep : V → ℕ) (v : V) |
| 290 | (hpar_root : par v = v) |
| 291 | (hpar_mem : ∀ a ∈ S, par a ∈ S) |
| 292 | (hpar_dep : ∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a) |
| 293 | {a x : V} (_haS : a ∈ S) (ha_ne_v : a ≠ v) (hxS : x ∈ S) {n : ℕ} |
| 294 | (hiter : par^[n] x = a) : |
| 295 | dep a + n = dep x := by |
| 296 | induction n generalizing x with |
| 297 | | zero => |
| 298 | simp only [Function.iterate_zero, id_eq] at hiter |
| 299 | subst x |
| 300 | omega |
| 301 | | succ n ih => |
| 302 | have hx_ne_v : x ≠ v := by |
| 303 | intro hxv |
| 304 | subst x |
| 305 | have : a = v := by |
| 306 | calc |
| 307 | a = par^[n.succ] v := hiter.symm |
| 308 | _ = v := iterate_root_eq par hpar_root _ |
| 309 | exact ha_ne_v this |
| 310 | have hparxS : par x ∈ S := hpar_mem x hxS |
| 311 | have hiter' : par^[n] (par x) = a := by |
| 312 | simpa [Function.iterate_succ_apply] using hiter |
| 313 | have hdep_x : dep (par x) + 1 = dep x := hpar_dep x hxS hx_ne_v |
| 314 | have hrec := ih hparxS hiter' |
| 315 | omega |
| 316 | |
| 317 | private theorem descendants_of_distinct_children_disjoint |
| 318 | (S : Finset V) (par : V → V) (dep : V → ℕ) (v : V) |
| 319 | (hpar_root : par v = v) |
| 320 | (hpar_mem : ∀ a ∈ S, par a ∈ S) |
| 321 | (hpar_dep : ∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a) : |
| 322 | ∀ a ∈ S, ∀ c₁ ∈ treeChildren S par a, ∀ c₂ ∈ treeChildren S par a, |
| 323 | c₁ ≠ c₂ → ∀ x ∈ S, (∃ n, par^[n] x = c₁) → ¬∃ m, par^[m] x = c₂ := by |
| 324 | intro a haS c₁ hc₁ c₂ hc₂ hc_ne x hxS hx₁ hx₂ |
| 325 | rcases hx₁ with ⟨n, hn⟩ |
| 326 | rcases hx₂ with ⟨m, hm⟩ |
| 327 | have hc₁S : c₁ ∈ S := (Finset.mem_filter.mp hc₁).1 |
| 328 | have hc₂S : c₂ ∈ S := (Finset.mem_filter.mp hc₂).1 |
| 329 | have hpar₁ : par c₁ = a := (Finset.mem_filter.mp hc₁).2.1 |
| 330 | have hpar₂ : par c₂ = a := (Finset.mem_filter.mp hc₂).2.1 |
| 331 | have hc₁_ne_v : c₁ ≠ v := by |
| 332 | intro hc₁v |
| 333 | have : c₁ = a := by |
| 334 | calc |
| 335 | c₁ = v := hc₁v |
| 336 | _ = par v := hpar_root.symm |
| 337 | _ = a := by simpa [hc₁v] using hpar₁ |
| 338 | exact (Finset.mem_filter.mp hc₁).2.2 this |
| 339 | have hc₂_ne_v : c₂ ≠ v := by |
| 340 | intro hc₂v |
| 341 | have : c₂ = a := by |
| 342 | calc |
| 343 | c₂ = v := hc₂v |
| 344 | _ = par v := hpar_root.symm |
| 345 | _ = a := by simpa [hc₂v] using hpar₂ |
| 346 | exact (Finset.mem_filter.mp hc₂).2.2 this |
| 347 | have hdep₁ : dep a + 1 = dep c₁ := by |
| 348 | simpa [hpar₁] using hpar_dep c₁ hc₁S hc₁_ne_v |
| 349 | have hdep₂ : dep a + 1 = dep c₂ := by |
| 350 | simpa [hpar₂] using hpar_dep c₂ hc₂S hc₂_ne_v |
| 351 | have hdepth₁ := |
| 352 | iterate_depth_eq S par dep v hpar_root hpar_mem hpar_dep hc₁S hc₁_ne_v hxS hn |
| 353 | have hdepth₂ := |
| 354 | iterate_depth_eq S par dep v hpar_root hpar_mem hpar_dep hc₂S hc₂_ne_v hxS hm |
| 355 | have hnm : n = m := by omega |
| 356 | subst hnm |
| 357 | exact hc_ne (hn.symm.trans hm) |
| 358 | |
| 359 | private theorem succ_card_treeChildren_le_admVertex |
| 360 | (G : SimpleGraph V) (r : ℕ) (v : V) |
| 361 | (S : Finset V) (par : V → V) (dep : V → ℕ) |
| 362 | (hpar_root : par v = v) |
| 363 | (hpar_mem : ∀ a ∈ S, par a ∈ S) |
| 364 | (hpar_dep : ∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a) |
| 365 | (hdep_le : ∀ a ∈ S, dep a ≤ r) |
| 366 | (habove : ∀ a ∈ S, a ∉ (SReach G r v \ {v}).toFinset → v ≤ a) |
| 367 | (hadj : ∀ a ∈ S, a ≠ v → G.Adj (par a) a) |
| 368 | (hreach : ∀ a ∈ S, a ≠ v → |
| 369 | ∃ u ∈ (SReach G r v \ {v}).toFinset, u ∈ S ∧ ∃ n, par^[n] u = a) |
| 370 | (hleaf : ∀ u ∈ (SReach G r v \ {v}).toFinset, u ∈ S → |
| 371 | ∀ b ∈ S, par b ≠ u ∨ b = u) |
| 372 | (hdisjoint : ∀ a ∈ S, ∀ c₁ ∈ treeChildren S par a, ∀ c₂ ∈ treeChildren S par a, |
| 373 | c₁ ≠ c₂ → ∀ x ∈ S, (∃ n, par^[n] x = c₁) → ¬∃ m, par^[m] x = c₂) |
| 374 | (w : V) (hw : w ∈ S) : |
| 375 | (treeChildren S par w).card + 1 ≤ admVertex G r w := by |
| 376 | classical |
| 377 | let children : Finset V := treeChildren S par w |
| 378 | let child : Fin children.card → V := fun i => (children.equivFin.symm i).1 |
| 379 | have hchild_mem : ∀ i, child i ∈ children := by |
| 380 | intro i |
| 381 | exact (children.equivFin.symm i).2 |
| 382 | have hchild_data : ∀ i, child i ∈ S ∧ par (child i) = w ∧ child i ≠ w := by |
| 383 | intro i |
| 384 | rcases Finset.mem_filter.mp (hchild_mem i) with ⟨hS, hpred⟩ |
| 385 | exact ⟨hS, hpred.1, hpred.2⟩ |
| 386 | have hchild_ne_v : ∀ i, child i ≠ v := by |
| 387 | intro i |
| 388 | rcases hchild_data i with ⟨hcS, hparc, hc_ne_w⟩ |
| 389 | intro hcv |
| 390 | have hcw : child i = w := by |
| 391 | calc |
| 392 | child i = v := hcv |
| 393 | _ = par v := hpar_root.symm |
| 394 | _ = w := by simpa [hcv] using hparc |
| 395 | exact hc_ne_w hcw |
| 396 | have hleaf_data : ∀ i : Fin children.card, |
| 397 | ∃ u : V, u ∈ (SReach G r v \ {v}).toFinset ∧ u ∈ S ∧ ∃ n, par^[n] u = child i := by |
| 398 | intro i |
| 399 | rcases hchild_data i with ⟨hcS, _, _⟩ |
| 400 | exact hreach (child i) hcS (hchild_ne_v i) |
| 401 | let leaf : Fin children.card → V := fun i => Classical.choose (hleaf_data i) |
| 402 | have hleaf_mem : ∀ i, leaf i ∈ (SReach G r v \ {v}).toFinset := by |
| 403 | intro i |
| 404 | exact (Classical.choose_spec (hleaf_data i)).1 |
| 405 | have hleaf_S : ∀ i, leaf i ∈ S := by |
| 406 | intro i |
| 407 | exact (Classical.choose_spec (hleaf_data i)).2.1 |
| 408 | have hleaf_desc : ∀ i, ∃ n, par^[n] (leaf i) = child i := by |
| 409 | intro i |
| 410 | exact (Classical.choose_spec (hleaf_data i)).2.2 |
| 411 | have hraw_data : ∀ i, ∃ q : G.Walk w (leaf i), |
| 412 | q.length ≤ r ∧ |
| 413 | ∀ y ∈ q.support, y = w ∨ y ∈ S ∧ ∃ m, par^[m] y = child i := by |
| 414 | intro i |
| 415 | exact exists_child_leaf_walk G r v S par dep hpar_root hpar_mem hpar_dep |
| 416 | hdep_le hadj w (child i) (leaf i) (hchild_mem i) (hleaf_S i) (hleaf_desc i) |
| 417 | let raw : ∀ i, G.Walk w (leaf i) := fun i => Classical.choose (hraw_data i) |
| 418 | have hraw_len : ∀ i, (raw i).length ≤ r := by |
| 419 | intro i |
| 420 | exact (Classical.choose_spec (hraw_data i)).1 |
| 421 | have hraw_support : ∀ i y, y ∈ (raw i).support → y = w ∨ y ∈ S ∧ ∃ m, par^[m] y = child i := by |
| 422 | intro i y hy |
| 423 | exact (Classical.choose_spec (hraw_data i)).2 y hy |
| 424 | let paths : Fin children.card → (u : V) × G.Walk w u := |
| 425 | fun i => ⟨leaf i, (raw i).bypass⟩ |
| 426 | have hpaths : IsAdmFamily G r w paths := by |
| 427 | refine ⟨?_, ?_, ?_, ?_⟩ |
| 428 | · intro i |
| 429 | have hleaf_set : leaf i ∈ SReach G r v \ {v} := by |
| 430 | simpa using hleaf_mem i |
| 431 | simp only [Set.mem_diff, Set.mem_singleton_iff] at hleaf_set |
| 432 | have hleaf_lt_v : leaf i < v := lt_of_le_of_ne hleaf_set.1.1 hleaf_set.2 |
| 433 | have hw_not_sreach : w ∉ (SReach G r v \ {v}).toFinset := by |
| 434 | intro hw_sreach |
| 435 | rcases hchild_data i with ⟨hcS, hparc, hc_ne_w⟩ |
| 436 | rcases hleaf w hw_sreach hw (child i) hcS with hpar_ne | hcw |
| 437 | · exact hpar_ne hparc |
| 438 | · exact hc_ne_w hcw |
| 439 | have hvw : v ≤ w := habove w hw hw_not_sreach |
| 440 | exact lt_of_lt_of_le hleaf_lt_v hvw |
| 441 | · intro i |
| 442 | simpa [paths] using (raw i).bypass_isPath |
| 443 | · intro i |
| 444 | exact le_trans (SimpleGraph.Walk.length_bypass_le (raw i)) (hraw_len i) |
| 445 | · intro i j hij x hxi hxj |
| 446 | by_cases hxw : x = w |
| 447 | · exact hxw |
| 448 | · have hxi_raw : x ∈ (raw i).support := by |
| 449 | exact SimpleGraph.Walk.support_bypass_subset (raw i) (by simpa [paths] using hxi) |
| 450 | have hxj_raw : x ∈ (raw j).support := by |
| 451 | exact SimpleGraph.Walk.support_bypass_subset (raw j) (by simpa [paths] using hxj) |
| 452 | have hxi_desc : x ∈ S ∧ ∃ n, par^[n] x = child i := by |
| 453 | rcases hraw_support i x hxi_raw with rfl | hx |
| 454 | · exact (hxw rfl).elim |
| 455 | · exact hx |
| 456 | have hxj_desc : x ∈ S ∧ ∃ n, par^[n] x = child j := by |
| 457 | rcases hraw_support j x hxj_raw with rfl | hx |
| 458 | · exact (hxw rfl).elim |
| 459 | · exact hx |
| 460 | have hchild_ne : child i ≠ child j := by |
| 461 | intro hEq |
| 462 | apply hij |
| 463 | apply children.equivFin.symm.injective |
| 464 | exact Subtype.ext hEq |
| 465 | exact False.elim <| |
| 466 | (hdisjoint w hw (child i) (hchild_mem i) (child j) (hchild_mem j) |
| 467 | hchild_ne x hxi_desc.1 hxi_desc.2) hxj_desc.2 |
| 468 | have hw_not_child : w ∉ children := by |
| 469 | intro hw_child |
| 470 | rcases Finset.mem_filter.mp hw_child with ⟨_, hpred⟩ |
| 471 | exact hpred.2 rfl |
| 472 | have hcard_lt : children.card < Fintype.card V := by |
| 473 | simpa [children] using |
| 474 | (Fintype.card_subtype_lt (p := fun x : V => x ∈ children) (x := w) hw_not_child) |
| 475 | unfold admVertex |
| 476 | have hsup : children.card ≤ |
| 477 | Finset.sup (Finset.range (Fintype.card V)) (fun k => |
| 478 | if ∃ paths : Fin k → (u : V) × G.Walk w u, IsAdmFamily G r w paths |
| 479 | then k else 0) := by |
| 480 | have hfamily : ∃ ps : Fin children.card → (u : V) × G.Walk w u, IsAdmFamily G r w ps := |
| 481 | ⟨paths, hpaths⟩ |
| 482 | have hmem : children.card ∈ Finset.range (Fintype.card V) := |
| 483 | Finset.mem_range.mpr hcard_lt |
| 484 | simpa [if_pos hfamily] using |
| 485 | (Finset.le_sup (f := fun k => |
| 486 | if ∃ paths : Fin k → (u : V) × G.Walk w u, IsAdmFamily G r w paths |
| 487 | then k else 0) hmem) |
| 488 | have hsup' : (treeChildren S par w).card ≤ |
| 489 | Finset.sup (Finset.range (Fintype.card V)) (fun k => |
| 490 | if ∃ paths : Fin k → (u : V) × G.Walk w u, IsAdmFamily G r w paths |
| 491 | then k else 0) := by |
| 492 | simpa [children] using hsup |
| 493 | omega |
| 494 | |
| 495 | private theorem tree_branching_le_adm |
| 496 | (G : SimpleGraph V) (r : ℕ) (v : V) (k : ℕ) |
| 497 | (hk : adm G r = k + 1) |
| 498 | (S : Finset V) (par : V → V) (dep : V → ℕ) |
| 499 | (hpar_root : par v = v) |
| 500 | (hpar_mem : ∀ a ∈ S, par a ∈ S) |
| 501 | (hpar_dep : ∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a) |
| 502 | (hdep_le : ∀ a ∈ S, dep a ≤ r) |
| 503 | (habove : ∀ a ∈ S, a ∉ (SReach G r v \ {v}).toFinset → v ≤ a) |
| 504 | (hadj : ∀ a ∈ S, a ≠ v → G.Adj (par a) a) |
| 505 | (hreach : ∀ a ∈ S, a ≠ v → |
| 506 | ∃ u ∈ (SReach G r v \ {v}).toFinset, u ∈ S ∧ ∃ n, par^[n] u = a) |
| 507 | (hleaf : ∀ u ∈ (SReach G r v \ {v}).toFinset, u ∈ S → |
| 508 | ∀ b ∈ S, par b ≠ u ∨ b = u) |
| 509 | (hdisjoint : ∀ a ∈ S, ∀ c₁ ∈ treeChildren S par a, ∀ c₂ ∈ treeChildren S par a, |
| 510 | c₁ ≠ c₂ → ∀ x ∈ S, (∃ n, par^[n] x = c₁) → ¬∃ m, par^[m] x = c₂) |
| 511 | (w : V) (hw : w ∈ S) : |
| 512 | (treeChildren S par w).card ≤ k := by |
| 513 | have hlocal : (treeChildren S par w).card + 1 ≤ admVertex G r w := |
| 514 | succ_card_treeChildren_le_admVertex G r v S par dep hpar_root |
| 515 | hpar_mem hpar_dep hdep_le habove hadj hreach hleaf |
| 516 | hdisjoint w hw |
| 517 | have hglobal : admVertex G r w ≤ k + 1 := by |
| 518 | simpa [hk] using admVertex_le_adm G r w |
| 519 | omega |
| 520 | |
| 521 | private theorem exists_tree_covering_sreach (G : SimpleGraph V) (r : ℕ) (v : V) : |
| 522 | ∃ (S : Finset V) (par : V → V) (dep : V → ℕ), |
| 523 | v ∈ S ∧ |
| 524 | par v = v ∧ |
| 525 | (∀ a ∈ S, par a ∈ S) ∧ |
| 526 | (∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a) ∧ |
| 527 | dep v = 0 ∧ |
| 528 | (∀ a ∈ S, dep a ≤ r) ∧ |
| 529 | (∀ a ∈ S, (treeChildren S par a).card ≤ adm G r - 1) ∧ |
| 530 | (SReach G r v \ {v}).toFinset ⊆ treeLeaves S par v := by |
| 531 | classical |
| 532 | obtain ⟨d, bp, hd_v, hbp_v, hbp_step, hd_lower, _⟩ := above_v_bfs_data G r v |
| 533 | let SR : Finset V := (SReach G r v \ {v}).toFinset |
| 534 | have hSR_lt_mem : ∀ {u}, u ∈ SR → u < v ∧ u ∈ SReach G r v := by |
| 535 | intro u hu |
| 536 | have hu_set : u ∈ SReach G r v \ ({v} : Set V) := by |
| 537 | simpa [SR] using hu |
| 538 | have hu_diff : u ∈ SReach G r v ∧ u ≠ v := by |
| 539 | simpa [Set.mem_diff, Set.mem_singleton_iff] using hu_set |
| 540 | have hu_le : u ≤ v := by |
| 541 | exact (show u ≤ v ∧ ∃ p : G.Walk v u, p.IsPath ∧ p.length ≤ r ∧ |
| 542 | ∀ i : ℕ, 0 < i → i < p.length → v < p.getVert i from by |
| 543 | simpa [SReach] using hu_diff.1).1 |
| 544 | exact ⟨lt_of_le_of_ne hu_le hu_diff.2, hu_diff.1⟩ |
| 545 | have hnot_SR_of_ge : ∀ {a}, v ≤ a → a ∉ SR := by |
| 546 | intro a ha_ge haSR |
| 547 | exact (not_lt_of_ge ha_ge) (hSR_lt_mem haSR).1 |
| 548 | have hpred_exists : ∀ u, u ∈ SR → ∃ u', v ≤ u' ∧ G.Adj u' u ∧ d u' + 1 ≤ r := by |
| 549 | intro u hu |
| 550 | have hu_mem : u ∈ SReach G r v := (hSR_lt_mem hu).2 |
| 551 | have hu_ne : u ≠ v := (hSR_lt_mem hu).1.ne |
| 552 | rcases sreach_predecessor G r v u hu_mem hu_ne with |
| 553 | ⟨_, u', p, hu'_ge, hu'_adj, hp_support, hp_len⟩ |
| 554 | have hd_u' : d u' ≤ p.length := hd_lower u' p hp_support (by omega) |
| 555 | refine ⟨u', hu'_ge, hu'_adj, ?_⟩ |
| 556 | omega |
| 557 | let pred : V → V := fun u => |
| 558 | if hu : u ∈ SR then Classical.choose (hpred_exists u hu) else v |
| 559 | have hpred_spec : ∀ {u}, u ∈ SR → v ≤ pred u ∧ G.Adj (pred u) u ∧ d (pred u) + 1 ≤ r := by |
| 560 | intro u hu |
| 561 | simp [pred, hu] |
| 562 | exact Classical.choose_spec (hpred_exists u hu) |
| 563 | let Useful : V → Prop := fun a => |
| 564 | a = v ∨ ∃ u ∈ SR, ∃ n, bp^[n] (pred u) = a |
| 565 | let S : Finset V := (Finset.univ.filter Useful) ∪ SR |
| 566 | let par : V → V := fun a => if a ∈ SR then pred a else bp a |
| 567 | let dep : V → ℕ := fun a => if a ∈ SR then d (pred a) + 1 else d a |
| 568 | have huseful_memS : ∀ {a}, Useful a → a ∈ S := by |
| 569 | intro a ha |
| 570 | exact Finset.mem_union.mpr <| Or.inl <| Finset.mem_filter.mpr ⟨by simp, ha⟩ |
| 571 | have hSR_memS : ∀ {u}, u ∈ SR → u ∈ S := by |
| 572 | intro u hu |
| 573 | exact Finset.mem_union.mpr <| Or.inr hu |
| 574 | have huseful_of_memS_notSR : ∀ {a}, a ∈ S → a ∉ SR → Useful a := by |
| 575 | intro a haS ha_notSR |
| 576 | rcases Finset.mem_union.mp haS with haU | haSR |
| 577 | · exact (Finset.mem_filter.mp haU).2 |
| 578 | · exact False.elim (ha_notSR haSR) |
| 579 | have hpar_eq_bp_of_ge : ∀ {a}, v ≤ a → par a = bp a := by |
| 580 | intro a ha_ge |
| 581 | simp [par, hnot_SR_of_ge ha_ge] |
| 582 | have hdep_eq_d_of_ge : ∀ {a}, v ≤ a → dep a = d a := by |
| 583 | intro a ha_ge |
| 584 | simp [dep, hnot_SR_of_ge ha_ge] |
| 585 | have hpred_useful : ∀ {u}, u ∈ SR → Useful (pred u) := by |
| 586 | intro u hu |
| 587 | right |
| 588 | exact ⟨u, hu, 0, rfl⟩ |
| 589 | have hbp_preserves_bounds : ∀ {a}, v ≤ a → d a ≤ r → v ≤ bp a ∧ d (bp a) ≤ r := by |
| 590 | intro a ha_ge hda |
| 591 | by_cases ha_v : a = v |
| 592 | · subst a |
| 593 | simp [hbp_v, hd_v] |
| 594 | · rcases hbp_step a ha_ge hda ha_v with ⟨hbp_ge, _, hbp_dep⟩ |
| 595 | refine ⟨hbp_ge, ?_⟩ |
| 596 | omega |
| 597 | have hbp_iter_bounds : ∀ {u}, u ∈ SR → ∀ n, v ≤ bp^[n] (pred u) ∧ d (bp^[n] (pred u)) ≤ r := by |
| 598 | intro u hu n |
| 599 | induction n with |
| 600 | | zero => |
| 601 | rcases hpred_spec hu with ⟨hpred_ge, _, hpred_bound⟩ |
| 602 | refine ⟨by simpa using hpred_ge, ?_⟩ |
| 603 | have hd_pred : d (pred u) ≤ r := by |
| 604 | omega |
| 605 | simpa using hd_pred |
| 606 | | succ n ih => |
| 607 | simpa [Function.iterate_succ_apply'] using hbp_preserves_bounds ih.1 ih.2 |
| 608 | have huseful_bounds : ∀ {a}, Useful a → v ≤ a ∧ d a ≤ r := by |
| 609 | intro a ha |
| 610 | rcases ha with rfl | ⟨u, hu, n, rfl⟩ |
| 611 | · simp [hd_v] |
| 612 | · exact hbp_iter_bounds hu n |
| 613 | have huseful_bp : ∀ {a}, Useful a → Useful (bp a) := by |
| 614 | intro a ha |
| 615 | rcases ha with rfl | ⟨u, hu, n, rfl⟩ |
| 616 | · left |
| 617 | simp [hbp_v] |
| 618 | · right |
| 619 | refine ⟨u, hu, n.succ, ?_⟩ |
| 620 | simp [Function.iterate_succ_apply'] |
| 621 | have hroot_mem : v ∈ S := huseful_memS <| Or.inl rfl |
| 622 | have hv_not_SR : v ∉ SR := hnot_SR_of_ge le_rfl |
| 623 | have hpar_root : par v = v := by |
| 624 | simp [par, hv_not_SR, hbp_v] |
| 625 | have hpar_mem : ∀ a ∈ S, par a ∈ S := by |
| 626 | intro a haS |
| 627 | by_cases haSR : a ∈ SR |
| 628 | · simpa [par, haSR] using huseful_memS (hpred_useful haSR) |
| 629 | · have haUseful : Useful a := huseful_of_memS_notSR haS haSR |
| 630 | have hbpUseful : Useful (bp a) := huseful_bp haUseful |
| 631 | simpa [par, haSR] using huseful_memS hbpUseful |
| 632 | have hpar_dep : ∀ a ∈ S, a ≠ v → dep (par a) + 1 = dep a := by |
| 633 | intro a haS ha_ne_v |
| 634 | by_cases haSR : a ∈ SR |
| 635 | · have hpred_ge : v ≤ pred a := (hpred_spec haSR).1 |
| 636 | have hpred_notSR : pred a ∉ SR := hnot_SR_of_ge hpred_ge |
| 637 | simp [par, dep, haSR, hpred_notSR] |
| 638 | · have haUseful : Useful a := huseful_of_memS_notSR haS haSR |
| 639 | have ha_bounds := huseful_bounds haUseful |
| 640 | rcases hbp_step a ha_bounds.1 ha_bounds.2 ha_ne_v with ⟨hbp_ge, _, hbp_dep⟩ |
| 641 | have hbp_notSR : bp a ∉ SR := hnot_SR_of_ge hbp_ge |
| 642 | simp [par, dep, haSR, hbp_notSR, hbp_dep] |
| 643 | have hdep_root : dep v = 0 := by |
| 644 | simp [dep, hv_not_SR, hd_v] |
| 645 | have hdep_le : ∀ a ∈ S, dep a ≤ r := by |
| 646 | intro a haS |
| 647 | by_cases haSR : a ∈ SR |
| 648 | · simpa [dep, haSR] using (hpred_spec haSR).2.2 |
| 649 | · have haUseful : Useful a := huseful_of_memS_notSR haS haSR |
| 650 | simpa [dep, haSR] using (huseful_bounds haUseful).2 |
| 651 | have habove : ∀ a ∈ S, a ∉ SR → v ≤ a := by |
| 652 | intro a haS ha_notSR |
| 653 | exact (huseful_bounds (huseful_of_memS_notSR haS ha_notSR)).1 |
| 654 | have hadj : ∀ a ∈ S, a ≠ v → G.Adj (par a) a := by |
| 655 | intro a haS ha_ne_v |
| 656 | by_cases haSR : a ∈ SR |
| 657 | · simpa [par, haSR] using (hpred_spec haSR).2.1 |
| 658 | · have haUseful : Useful a := huseful_of_memS_notSR haS haSR |
| 659 | have ha_bounds := huseful_bounds haUseful |
| 660 | rcases hbp_step a ha_bounds.1 ha_bounds.2 ha_ne_v with ⟨_, hbp_adj, _⟩ |
| 661 | simpa [par, haSR] using hbp_adj |
| 662 | have hpar_above : ∀ {a}, a ∈ S → v ≤ par a := by |
| 663 | intro a haS |
| 664 | by_cases haSR : a ∈ SR |
| 665 | · simpa [par, haSR] using (hpred_spec haSR).1 |
| 666 | · have haUseful : Useful a := huseful_of_memS_notSR haS haSR |
| 667 | have hbpUseful : Useful (bp a) := huseful_bp haUseful |
| 668 | simpa [par, haSR] using (huseful_bounds hbpUseful).1 |
| 669 | have hpar_iter_pred : ∀ {u}, u ∈ SR → ∀ n, par^[n.succ] u = bp^[n] (pred u) := by |
| 670 | intro u hu n |
| 671 | induction n with |
| 672 | | zero => |
| 673 | simp [par, hu] |
| 674 | | succ n ih => |
| 675 | have hge : v ≤ bp^[n] (pred u) := (hbp_iter_bounds hu n).1 |
| 676 | calc |
| 677 | par^[n.succ.succ] u = par (par^[n.succ] u) := by |
| 678 | rw [Function.iterate_succ_apply'] |
| 679 | _ = par (bp^[n] (pred u)) := by |
| 680 | rw [ih] |
| 681 | _ = bp (bp^[n] (pred u)) := by |
| 682 | simpa using (hpar_eq_bp_of_ge hge) |
| 683 | _ = bp^[n.succ] (pred u) := by |
| 684 | rw [Function.iterate_succ_apply'] |
| 685 | have hreach : ∀ a ∈ S, a ≠ v → |
| 686 | ∃ u ∈ SR, u ∈ S ∧ ∃ n, par^[n] u = a := by |
| 687 | intro a haS ha_ne_v |
| 688 | by_cases haSR : a ∈ SR |
| 689 | · refine ⟨a, haSR, hSR_memS haSR, 0, by simp⟩ |
| 690 | · have haUseful : Useful a := huseful_of_memS_notSR haS haSR |
| 691 | rcases haUseful with hEq | ⟨u, hu, n, hn⟩ |
| 692 | · exact False.elim (ha_ne_v hEq) |
| 693 | · refine ⟨u, hu, hSR_memS hu, n.succ, ?_⟩ |
| 694 | exact (hpar_iter_pred hu n).trans hn |
| 695 | have hleaf : ∀ u ∈ SR, u ∈ S → |
| 696 | ∀ b ∈ S, par b ≠ u ∨ b = u := by |
| 697 | intro u hu _ b hbS |
| 698 | left |
| 699 | intro hparb |
| 700 | have : v ≤ u := by |
| 701 | simpa [hparb] using hpar_above hbS |
| 702 | exact (not_lt_of_ge this) (hSR_lt_mem hu).1 |
| 703 | have hdisjoint : |
| 704 | ∀ a ∈ S, ∀ c₁ ∈ treeChildren S par a, ∀ c₂ ∈ treeChildren S par a, |
| 705 | c₁ ≠ c₂ → ∀ x ∈ S, (∃ n, par^[n] x = c₁) → ¬∃ m, par^[m] x = c₂ := |
| 706 | descendants_of_distinct_children_disjoint S par dep v hpar_root hpar_mem hpar_dep |
| 707 | have hadm_ge : 1 ≤ adm G r := by |
| 708 | calc |
| 709 | 1 ≤ admVertex G r v := by |
| 710 | unfold admVertex |
| 711 | omega |
| 712 | _ ≤ adm G r := admVertex_le_adm G r v |
| 713 | have hk : adm G r = (adm G r - 1) + 1 := by |
| 714 | omega |
| 715 | have hbranch : ∀ a ∈ S, (treeChildren S par a).card ≤ adm G r - 1 := by |
| 716 | intro a haS |
| 717 | exact tree_branching_le_adm G r v (adm G r - 1) hk S par dep hpar_root |
| 718 | hpar_mem hpar_dep hdep_le habove hadj hreach hleaf hdisjoint a haS |
| 719 | have hleaf_cover : SR ⊆ treeLeaves S par v := by |
| 720 | intro u hu |
| 721 | have huS : u ∈ S := hSR_memS hu |
| 722 | have hu_ne_v : u ≠ v := (hSR_lt_mem hu).1.ne |
| 723 | have hchild_empty : treeChildren S par u = ∅ := by |
| 724 | ext b |
| 725 | constructor |
| 726 | · intro hb |
| 727 | rcases Finset.mem_filter.mp hb with ⟨hbS, hchild⟩ |
| 728 | rcases hleaf u hu huS b hbS with hpar_ne | hbu |
| 729 | · exact (hpar_ne hchild.1).elim |
| 730 | · exact (hchild.2 hbu).elim |
| 731 | · intro hb |
| 732 | simp at hb |
| 733 | rw [treeLeaves] |
| 734 | exact Finset.mem_filter.mpr ⟨huS, ⟨hu_ne_v, by simp [hchild_empty]⟩⟩ |
| 735 | refine ⟨S, par, dep, hroot_mem, hpar_root, hpar_mem, hpar_dep, hdep_root, |
| 736 | hdep_le, hbranch, ?_⟩ |
| 737 | simpa [SR] using hleaf_cover |
| 738 | |
| 739 | private theorem ncard_sreach_sdiff_le_pow (G : SimpleGraph V) (r : ℕ) (v : V) : |
| 740 | (SReach G r v \ {v}).ncard ≤ (adm G r - 1) ^ r := by |
| 741 | obtain ⟨S, par, dep, hroot_mem, hpar_root, hpar_mem, hpar_dep, |
| 742 | hdep_root, hdep_le, hbranch, hleaf_cover⟩ := |
| 743 | exists_tree_covering_sreach G r v |
| 744 | have hbound := card_treeLeaves_le_pow S v par dep r (adm G r - 1) |
| 745 | hroot_mem hpar_root hpar_mem hpar_dep hdep_root hdep_le hbranch |
| 746 | calc (SReach G r v \ {v}).ncard |
| 747 | = (SReach G r v \ {v}).toFinset.card := Set.ncard_eq_toFinset_card' _ |
| 748 | _ ≤ (treeLeaves S par v).card := Finset.card_le_card hleaf_cover |
| 749 | _ ≤ (adm G r - 1) ^ r := hbound |
| 750 | |
| 751 | end |
| 752 | |
| 753 | noncomputable section |
| 754 | |
| 755 | variable {V : Type*} [Fintype V] [LinearOrder V] |
| 756 | |
| 757 | /-- Lemma 2.5: the strong r-coloring number is bounded by a power of the |
| 758 | r-admissibility. -/ |
| 759 | theorem scol_le_one_add_adm_sub_one_pow (G : SimpleGraph V) (r : ℕ) : |
| 760 | Catalog.Sparsity.ColoringNumbers.scol G r ≤ |
| 761 | 1 + (Catalog.Sparsity.Admissibility.adm G r - 1) ^ r := by |
| 762 | classical |
| 763 | unfold Catalog.Sparsity.ColoringNumbers.scol |
| 764 | apply Finset.sup_le |
| 765 | intro v _ |
| 766 | have h1 := Set.ncard_diff_singleton_add_one (self_mem_sreach G r v) (Set.toFinite _) |
| 767 | have h2 := ncard_sreach_sdiff_le_pow G r v |
| 768 | omega |
| 769 | |
| 770 | end |
| 771 | |
| 772 | end Catalog.Sparsity.StrongColoringBoundByAdm |
| 773 |