Catalog/Sparsity/StrongColoringBoundByAdm/TreeCounting.lean
| 1 | import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 2 | import Mathlib.Data.Finset.Basic |
| 3 | import Mathlib.Data.Finset.Card |
| 4 | import Mathlib.Order.Defs.PartialOrder |
| 5 | import Mathlib.Tactic |
| 6 | |
| 7 | namespace Catalog.Sparsity.StrongColoringBoundByAdm |
| 8 | |
| 9 | variable {α : Type*} [DecidableEq α] |
| 10 | |
| 11 | /-- Children of `a` in the tree: elements of `S` whose parent is `a`, |
| 12 | excluding `a` itself. -/ |
| 13 | def treeChildren (S : Finset α) (parent : α → α) (a : α) : Finset α := |
| 14 | S.filter fun b => parent b = a ∧ b ≠ a |
| 15 | |
| 16 | /-- Non-root leaves of the tree: elements of `S` distinct from `root` |
| 17 | that have no proper children. The root is excluded because when it |
| 18 | has no children, counting it would break the `k ^ r` bound for `r ≥ 1`. -/ |
| 19 | def treeLeaves (S : Finset α) (parent : α → α) (root : α) : Finset α := |
| 20 | S.filter fun a => a ≠ root ∧ (treeChildren S parent a).card = 0 |
| 21 | |
| 22 | /-- In a rooted tree represented by a parent function on a finset, if every |
| 23 | vertex has depth at most `r` and at most `k` children, then the number of |
| 24 | non-root leaves is at most `k ^ r`. -/ |
| 25 | theorem card_treeLeaves_le_pow |
| 26 | (S : Finset α) (root : α) (parent : α → α) (depth : α → ℕ) (r k : ℕ) |
| 27 | (hroot : root ∈ S) |
| 28 | (hparent_root : parent root = root) |
| 29 | (hparent_mem : ∀ a ∈ S, parent a ∈ S) |
| 30 | (hparent_depth : ∀ a ∈ S, a ≠ root → depth (parent a) + 1 = depth a) |
| 31 | (hdepth_root : depth root = 0) |
| 32 | (hdepth_le : ∀ a ∈ S, depth a ≤ r) |
| 33 | (hbranch : ∀ a ∈ S, (treeChildren S parent a).card ≤ k) : |
| 34 | (treeLeaves S parent root).card ≤ k ^ r := by |
| 35 | classical |
| 36 | induction r generalizing S root parent depth k with |
| 37 | | zero => |
| 38 | have hleaf_empty : treeLeaves S parent root = ∅ := by |
| 39 | ext a |
| 40 | constructor |
| 41 | · intro ha |
| 42 | rcases Finset.mem_filter.mp ha with ⟨haS, haLeaf⟩ |
| 43 | rcases haLeaf with ⟨ha_root, _⟩ |
| 44 | have hdepth_eq := hparent_depth a haS ha_root |
| 45 | have hdepth_bound := hdepth_le a haS |
| 46 | omega |
| 47 | · intro ha |
| 48 | simp at ha |
| 49 | simp [hleaf_empty] |
| 50 | | succ r ih => |
| 51 | set children : Finset α := treeChildren S parent root with hchildren |
| 52 | set subtree : α → Finset α := fun c => |
| 53 | S.filter fun a => ∃ n, (parent^[n]) a = c with hsubtree |
| 54 | set parent' : α → α → α := fun c a => if a = c then c else parent a with hparent' |
| 55 | set branch : α → Finset α := fun c => |
| 56 | (treeLeaves S parent root).filter fun a => a ∈ subtree c with hbranchDef |
| 57 | have hchildren_card : children.card ≤ k := by |
| 58 | simpa [hchildren] using hbranch root hroot |
| 59 | have hiterate_mem : ∀ n {a : α}, a ∈ S → (parent^[n]) a ∈ S := by |
| 60 | intro n |
| 61 | induction n with |
| 62 | | zero => |
| 63 | intro a ha |
| 64 | simpa using ha |
| 65 | | succ n ihn => |
| 66 | intro a ha |
| 67 | rw [Function.iterate_succ_apply] |
| 68 | exact ihn (hparent_mem a ha) |
| 69 | have hroot_iter : ∀ n, (parent^[n]) root = root := by |
| 70 | intro n |
| 71 | induction n with |
| 72 | | zero => rfl |
| 73 | | succ n ihn => |
| 74 | rw [Function.iterate_succ_apply] |
| 75 | simpa [hparent_root] using ihn |
| 76 | have hsubtree_ne_root : |
| 77 | ∀ {c a : α}, c ∈ children → a ∈ subtree c → a ≠ root := by |
| 78 | intro c a hc haSub |
| 79 | rcases Finset.mem_filter.mp hc with ⟨_, hpredc⟩ |
| 80 | rcases hpredc with ⟨_, hc_root⟩ |
| 81 | rw [hsubtree] at haSub |
| 82 | rcases Finset.mem_filter.mp haSub with ⟨_, ⟨n, hn⟩⟩ |
| 83 | intro ha_root |
| 84 | subst a |
| 85 | have : root = c := by |
| 86 | simpa [hroot_iter n] using hn |
| 87 | exact hc_root this.symm |
| 88 | have hsubtree_children_subset : |
| 89 | ∀ c a, treeChildren (subtree c) (parent' c) a ⊆ treeChildren S parent a := by |
| 90 | intro c a b hb |
| 91 | rw [treeChildren] at hb ⊢ |
| 92 | rcases Finset.mem_filter.mp hb with ⟨hbSub, hpredb⟩ |
| 93 | rcases hpredb with ⟨hparb, hbne⟩ |
| 94 | rw [hsubtree] at hbSub |
| 95 | rcases Finset.mem_filter.mp hbSub with ⟨hbS, _⟩ |
| 96 | have hb_ne_c : b ≠ c := by |
| 97 | intro hbc |
| 98 | subst b |
| 99 | have : c = a := by |
| 100 | simpa [hparent'] using hparb |
| 101 | exact hbne this |
| 102 | have hpar : parent b = a := by |
| 103 | simpa [hparent', hb_ne_c] using hparb |
| 104 | exact Finset.mem_filter.mpr ⟨hbS, ⟨hpar, hbne⟩⟩ |
| 105 | have hsubtree_root_has_child : |
| 106 | ∀ {c a : α}, c ∈ children → a ∈ subtree c → a ≠ c → |
| 107 | (treeChildren (subtree c) (parent' c) c).card ≠ 0 := by |
| 108 | intro c a hc haSub ha_ne_c |
| 109 | rcases Finset.mem_filter.mp hc with ⟨_, hpredc⟩ |
| 110 | rcases hpredc with ⟨hparc, hc_root⟩ |
| 111 | rw [hsubtree] at haSub |
| 112 | rcases Finset.mem_filter.mp haSub with ⟨haS, ⟨n, hn⟩⟩ |
| 113 | have hn_ne_zero : n ≠ 0 := by |
| 114 | intro hn0 |
| 115 | subst n |
| 116 | simp only [Function.iterate_zero, id_eq] at hn |
| 117 | exact ha_ne_c hn |
| 118 | rcases Nat.exists_eq_succ_of_ne_zero hn_ne_zero with ⟨m, rfl⟩ |
| 119 | let b := (parent^[m]) a |
| 120 | have hpb : parent b = c := by |
| 121 | dsimp [b] |
| 122 | simpa [Function.iterate_succ_apply'] using hn |
| 123 | have hb_mem_sub : b ∈ subtree c := by |
| 124 | rw [hsubtree] |
| 125 | refine Finset.mem_filter.mpr ?_ |
| 126 | refine ⟨hiterate_mem m haS, ⟨1, ?_⟩⟩ |
| 127 | simp [b, hpb] |
| 128 | have hb_ne_c : b ≠ c := by |
| 129 | intro hbc |
| 130 | have : root = c := by |
| 131 | simpa [hparc, b, hbc] using hpb |
| 132 | exact hc_root this.symm |
| 133 | have hb_child : b ∈ treeChildren (subtree c) (parent' c) c := by |
| 134 | rw [treeChildren] |
| 135 | refine Finset.mem_filter.mpr ?_ |
| 136 | refine ⟨hb_mem_sub, ?_⟩ |
| 137 | constructor |
| 138 | · simpa [hparent', hb_ne_c] using hpb |
| 139 | · exact hb_ne_c |
| 140 | exact Finset.card_ne_zero.mpr ⟨b, hb_child⟩ |
| 141 | have hdesc_child : |
| 142 | ∀ n a, depth a = n → a ∈ S → a ≠ root → ∃ c ∈ children, a ∈ subtree c := by |
| 143 | intro n |
| 144 | induction n with |
| 145 | | zero => |
| 146 | intro a hdeptha haS ha_root |
| 147 | have hdepth_eq := hparent_depth a haS ha_root |
| 148 | omega |
| 149 | | succ n ihn => |
| 150 | intro a hdeptha haS ha_root |
| 151 | by_cases hpar : parent a = root |
| 152 | · refine ⟨a, ?_, ?_⟩ |
| 153 | · rw [hchildren, treeChildren] |
| 154 | exact Finset.mem_filter.mpr ⟨haS, ⟨hpar, ha_root⟩⟩ |
| 155 | · rw [hsubtree] |
| 156 | exact Finset.mem_filter.mpr ⟨haS, by refine ⟨0, ?_⟩; simp⟩ |
| 157 | · have hparentS : parent a ∈ S := hparent_mem a haS |
| 158 | have hdepth_parent : depth (parent a) = n := by |
| 159 | have hdepth_eq := hparent_depth a haS ha_root |
| 160 | omega |
| 161 | rcases ihn (parent a) hdepth_parent hparentS hpar with ⟨c, hc, hparentSub⟩ |
| 162 | refine ⟨c, hc, ?_⟩ |
| 163 | rw [hsubtree] at hparentSub ⊢ |
| 164 | rcases Finset.mem_filter.mp hparentSub with ⟨_, ⟨m, hm⟩⟩ |
| 165 | refine Finset.mem_filter.mpr ⟨haS, ⟨m.succ, ?_⟩⟩ |
| 166 | simpa [Function.iterate_succ_apply] using hm |
| 167 | have hsubtree_bound : |
| 168 | ∀ c ∈ children, (treeLeaves (subtree c) (parent' c) c).card ≤ k ^ r := by |
| 169 | intro c hc |
| 170 | rcases Finset.mem_filter.mp hc with ⟨hcS, hpredc⟩ |
| 171 | rcases hpredc with ⟨hparc, hc_root⟩ |
| 172 | have hc_sub : c ∈ subtree c := by |
| 173 | rw [hsubtree] |
| 174 | exact Finset.mem_filter.mpr ⟨hcS, by refine ⟨0, ?_⟩; simp⟩ |
| 175 | have hdepth_c : depth c = 1 := by |
| 176 | have hdepth_eq := hparent_depth c hcS hc_root |
| 177 | rw [hparc, hdepth_root] at hdepth_eq |
| 178 | omega |
| 179 | have hparent_mem_sub : |
| 180 | ∀ a ∈ subtree c, parent' c a ∈ subtree c := by |
| 181 | intro a haSub |
| 182 | by_cases hac : a = c |
| 183 | · subst a |
| 184 | simpa [hparent'] using hc_sub |
| 185 | · rw [hsubtree] at haSub |
| 186 | rcases Finset.mem_filter.mp haSub with ⟨haS, ⟨n, hn⟩⟩ |
| 187 | have hn_ne_zero : n ≠ 0 := by |
| 188 | intro hn0 |
| 189 | subst n |
| 190 | simp only [Function.iterate_zero, id_eq] at hn |
| 191 | exact hac hn |
| 192 | rcases Nat.exists_eq_succ_of_ne_zero hn_ne_zero with ⟨m, rfl⟩ |
| 193 | rw [hsubtree] |
| 194 | refine Finset.mem_filter.mpr ?_ |
| 195 | refine ⟨by simpa [hparent', hac] using hparent_mem a haS, ⟨m, ?_⟩⟩ |
| 196 | simpa [hparent', hac, Function.iterate_succ_apply] using hn |
| 197 | have hparent_depth_sub : |
| 198 | ∀ a ∈ subtree c, a ≠ c → (depth (parent' c a) - 1) + 1 = depth a - 1 := by |
| 199 | intro a haSub ha_ne_c |
| 200 | rw [hsubtree] at haSub |
| 201 | rcases Finset.mem_filter.mp haSub with ⟨haS, _⟩ |
| 202 | have ha_root : a ≠ root := hsubtree_ne_root hc (by simpa [hsubtree] using haSub) |
| 203 | have hdepth_eq := hparent_depth a haS ha_root |
| 204 | have hparent_sub : parent a ∈ subtree c := by |
| 205 | have : parent' c a ∈ subtree c := |
| 206 | hparent_mem_sub a (by simpa [hsubtree] using haSub) |
| 207 | simpa [hparent', ha_ne_c] using this |
| 208 | have hparent_root : parent a ≠ root := hsubtree_ne_root hc hparent_sub |
| 209 | have hparent_depth_eq := hparent_depth (parent a) (hparent_mem a haS) hparent_root |
| 210 | have : parent' c a = parent a := by |
| 211 | simp [hparent', ha_ne_c] |
| 212 | rw [this] |
| 213 | omega |
| 214 | have hdepth_le_sub : |
| 215 | ∀ a ∈ subtree c, depth a - 1 ≤ r := by |
| 216 | intro a haSub |
| 217 | rw [hsubtree] at haSub |
| 218 | rcases Finset.mem_filter.mp haSub with ⟨haS, _⟩ |
| 219 | have hdepth_bound := hdepth_le a haS |
| 220 | by_cases hac : a = c |
| 221 | · subst a |
| 222 | omega |
| 223 | · have ha_root : a ≠ root := hsubtree_ne_root hc (by simpa [hsubtree] using haSub) |
| 224 | have hdepth_eq := hparent_depth a haS ha_root |
| 225 | omega |
| 226 | have hbranch_sub : |
| 227 | ∀ a ∈ subtree c, (treeChildren (subtree c) (parent' c) a).card ≤ k := by |
| 228 | intro a haSub |
| 229 | exact le_trans (Finset.card_le_card (hsubtree_children_subset c a)) |
| 230 | (hbranch a (by |
| 231 | rw [hsubtree] at haSub |
| 232 | exact (Finset.mem_filter.mp haSub).1)) |
| 233 | exact ih (subtree c) c (parent' c) (fun a => depth a - 1) k |
| 234 | hc_sub |
| 235 | (by simp [hparent']) |
| 236 | hparent_mem_sub |
| 237 | hparent_depth_sub |
| 238 | (by simp [hdepth_c]) |
| 239 | hdepth_le_sub |
| 240 | hbranch_sub |
| 241 | have hbranch_card : |
| 242 | ∀ c ∈ children, (branch c).card ≤ k ^ r := by |
| 243 | intro c hc |
| 244 | by_cases hcleaf : (treeChildren S parent c).card = 0 |
| 245 | · have hsingle : branch c ⊆ ({c} : Finset α) := by |
| 246 | intro a ha |
| 247 | rw [hbranchDef] at ha |
| 248 | rcases Finset.mem_filter.mp ha with ⟨haLeaf, haSub⟩ |
| 249 | by_cases hac : a = c |
| 250 | · simp [hac] |
| 251 | · have hnonzero := |
| 252 | hsubtree_root_has_child hc haSub hac |
| 253 | have hsubset := |
| 254 | hsubtree_children_subset c c |
| 255 | have : (treeChildren S parent c).card ≠ 0 := by |
| 256 | intro hzero |
| 257 | have hle0 : (treeChildren (subtree c) (parent' c) c).card ≤ 0 := by |
| 258 | exact le_trans (Finset.card_le_card hsubset) (by simp [hzero]) |
| 259 | exact hnonzero (Nat.eq_zero_of_le_zero hle0) |
| 260 | exact (this hcleaf).elim |
| 261 | have hk_pos : 0 < k := by |
| 262 | have : 1 ≤ children.card := Finset.one_le_card.mpr ⟨c, hc⟩ |
| 263 | have hk_one : 1 ≤ k := le_trans this hchildren_card |
| 264 | omega |
| 265 | calc |
| 266 | (branch c).card ≤ ({c} : Finset α).card := Finset.card_le_card hsingle |
| 267 | _ = 1 := by simp |
| 268 | _ ≤ k ^ r := Nat.one_le_pow _ _ hk_pos |
| 269 | · have hsubset_branch : |
| 270 | branch c ⊆ treeLeaves (subtree c) (parent' c) c := by |
| 271 | intro a ha |
| 272 | rw [hbranchDef] at ha |
| 273 | rcases Finset.mem_filter.mp ha with ⟨haLeaf, haSub⟩ |
| 274 | rcases Finset.mem_filter.mp haLeaf with ⟨haS, hleafPred⟩ |
| 275 | rcases hleafPred with ⟨ha_root, hleaf_card⟩ |
| 276 | have ha_ne_c : a ≠ c := by |
| 277 | intro hac |
| 278 | subst a |
| 279 | exact hcleaf hleaf_card |
| 280 | have hleaf_sub : |
| 281 | (treeChildren (subtree c) (parent' c) a).card = 0 := by |
| 282 | apply Nat.eq_zero_of_le_zero |
| 283 | refine le_trans (Finset.card_le_card (hsubtree_children_subset c a)) ?_ |
| 284 | simp [hleaf_card] |
| 285 | rw [treeLeaves] |
| 286 | exact Finset.mem_filter.mpr ⟨haSub, ⟨ha_ne_c, hleaf_sub⟩⟩ |
| 287 | exact le_trans (Finset.card_le_card hsubset_branch) (hsubtree_bound c hc) |
| 288 | have hleaf_subset : |
| 289 | treeLeaves S parent root ⊆ children.biUnion branch := by |
| 290 | intro a haLeaf |
| 291 | rcases Finset.mem_filter.mp haLeaf with ⟨haS, hleafPred⟩ |
| 292 | rcases hleafPred with ⟨ha_root, _⟩ |
| 293 | have hdeptha := hdepth_le a haS |
| 294 | rcases hdesc_child (depth a) a rfl haS ha_root with ⟨c, hc, haSub⟩ |
| 295 | rw [Finset.mem_biUnion] |
| 296 | exact ⟨c, hc, by |
| 297 | rw [hbranchDef] |
| 298 | exact Finset.mem_filter.mpr ⟨haLeaf, haSub⟩⟩ |
| 299 | calc |
| 300 | (treeLeaves S parent root).card ≤ (children.biUnion branch).card := |
| 301 | Finset.card_le_card hleaf_subset |
| 302 | _ ≤ ∑ c ∈ children, (branch c).card := Finset.card_biUnion_le |
| 303 | _ ≤ ∑ c ∈ children, k ^ r := by |
| 304 | gcongr with c hc |
| 305 | exact hbranch_card c hc |
| 306 | _ = children.card * k ^ r := by simp |
| 307 | _ ≤ k * k ^ r := by gcongr |
| 308 | _ = k ^ (Nat.succ r) := by simp [Nat.pow_succ, Nat.mul_comm] |
| 309 | |
| 310 | end Catalog.Sparsity.StrongColoringBoundByAdm |
| 311 |