Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/ShallowMinorComposition/Full.lean
1import Catalog.Sparsity.Preliminaries.Full
2import Catalog.Sparsity.ShallowMinor.Full
3import Catalog.Sparsity.NowhereDense.Full
4import Mathlib.Tactic
5
6open Catalog.Sparsity.ShallowMinor
7open Catalog.Sparsity.NowhereDense
8open Catalog.Sparsity.Preliminaries
9
10namespace Catalog.Sparsity.ShallowMinorComposition
11
12private def composedBranchSet {U V W : Type}
13 {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ}
14 (mJH : ShallowMinorModel J H b) (mHG : ShallowMinorModel H G a) (u : U) : Set V :=
15 {x | ∃ v, v ∈ mJH.branchSet u ∧ x ∈ mHG.branchSet v}
16
17private def composedCenter {U V W : Type}
18 {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ}
19 (mJH : ShallowMinorModel J H b) (mHG : ShallowMinorModel H G a) (u : U) : V :=
20 mHG.center (mJH.center u)
21
22private theorem composedCenter_mem {U V W : Type}
23 {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ}
24 (mJH : ShallowMinorModel J H b) (mHG : ShallowMinorModel H G a) (u : U) :
25 composedCenter mJH mHG u ∈ composedBranchSet mJH mHG u := by
26 refine ⟨mJH.center u, mJH.center_mem u, mHG.center_mem _⟩
27
28private theorem composedBranchSet_disjoint {U V W : Type}
29 {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ}
30 (mJH : ShallowMinorModel J H b) (mHG : ShallowMinorModel H G a)
31 {u v : U} (huv : u ≠ v) :
32 Disjoint (composedBranchSet mJH mHG u) (composedBranchSet mJH mHG v) := by
33 refine Set.disjoint_left.mpr ?_
34 intro x hxU hxV
35 rcases hxU with ⟨u', hu', hxu'⟩
36 rcases hxV with ⟨v', hv', hxv'⟩
37 by_cases huv' : u' = v'
38 · subst huv'
39 exact Set.disjoint_left.mp (mJH.branchDisjoint u v huv) hu' hv'
40 · exact Set.disjoint_left.mp (mHG.branchDisjoint u' v' huv') hxu' hxv'
41
42private theorem lift_center_walk {U V W : Type}
43 {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ}
44 (mJH : ShallowMinorModel J H b) (mHG : ShallowMinorModel H G a)
45 (u : U) {s t : W} (p : H.Walk s t)
46 (hp : ∀ z ∈ p.support, z ∈ mJH.branchSet u) :
47 ∃ q : G.Walk (mHG.center s) (mHG.center t),
48 q.length ≤ (2 * a + 1) * p.length ∧
49 ∀ w ∈ q.support, w ∈ composedBranchSet mJH mHG u := by
50 induction p with
51 | @nil s =>
52 refine ⟨SimpleGraph.Walk.nil, by simp, ?_⟩
53 intro w hw
54 simp at hw
55 subst w
56 exact ⟨s, hp s (by simp), mHG.center_mem s⟩
57 | @cons s s' t h p ih =>
58 have hs : s ∈ mJH.branchSet u := hp s (by simp)
59 have hs' : s' ∈ mJH.branchSet u := hp s' (by simp)
60 have hp' : ∀ z ∈ p.support, z ∈ mJH.branchSet u := by
61 intro z hz
62 exact hp z (by simp [hz])
63 rcases ih hp' with ⟨q, hq_len, hq_support⟩
64 rcases mHG.branchEdge s s' h with ⟨xs, hxs, ys, hys, hxy⟩
65 rcases mHG.branchRadius s xs hxs with ⟨ps, _, hps_len, hps_support⟩
66 rcases mHG.branchRadius s' ys hys with ⟨pt, _, hpt_len, hpt_support⟩
67 let step : G.Walk (mHG.center s) (mHG.center s') :=
68 ps.append (hxy.toWalk.append pt.reverse)
69 have hstep_len : step.length ≤ 2 * a + 1 := by
70 dsimp [step]
71 rw [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons,
72 SimpleGraph.Walk.length_reverse]
73 omega
74 have hstep_support_right :
75 ∀ w ∈ (hxy.toWalk.append pt.reverse).support, w ∈ composedBranchSet mJH mHG u := by
76 intro w hw
77 rw [SimpleGraph.Walk.mem_support_append_iff] at hw
78 rcases hw with hw | hw
79 · have hw' : w = xs ∨ w = ys := by
80 simpa using hw
81 rcases hw' with rfl | rfl
82 · exact ⟨s, hs, hxs⟩
83 · exact ⟨s', hs', hys⟩
84 · exact ⟨s', hs', hpt_support w (by simpa [SimpleGraph.Walk.support_reverse] using hw)⟩
85 have hstep_support_left : ∀ w ∈ ps.support, w ∈ composedBranchSet mJH mHG u := by
86 intro w hw
87 exact ⟨s, hs, hps_support w hw⟩
88 have hstep_support : ∀ w ∈ step.support, w ∈ composedBranchSet mJH mHG u := by
89 intro w hw
90 dsimp [step] at hw
91 rw [SimpleGraph.Walk.mem_support_append_iff] at hw
92 rcases hw with hw | hw
93 · exact hstep_support_left w hw
94 · exact hstep_support_right w hw
95 refine ⟨step.append q, ?_, ?_⟩
96 · have hsum : step.length + q.length ≤ (2 * a + 1) + (2 * a + 1) * p.length := by
97 exact add_le_add hstep_len hq_len
98 simpa [SimpleGraph.Walk.length_cons, Nat.mul_add, Nat.add_comm, Nat.add_left_comm,
99 Nat.add_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using hsum
100 · intro w hw
101 rw [SimpleGraph.Walk.mem_support_append_iff] at hw
102 rcases hw with hw | hw
103 · exact hstep_support w hw
104 · exact hq_support w hw
105
106private theorem composedBranchSet_radius {U V W : Type}
107 {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ}
108 (mJH : ShallowMinorModel J H b) (mHG : ShallowMinorModel H G a)
109 (u : U) (x : V) (hx : x ∈ composedBranchSet mJH mHG u) :
110 ∃ p : G.Walk (composedCenter mJH mHG u) x, p.IsPath ∧ p.length ≤ 2 * a * b + a + b ∧
111 ∀ w ∈ p.support, w ∈ composedBranchSet mJH mHG u := by
112 classical
113 rcases hx with ⟨v, hv, hxv⟩
114 rcases mJH.branchRadius u v hv with ⟨pH, _, hpH_len, hpH_support⟩
115 rcases lift_center_walk mJH mHG u pH hpH_support with ⟨q, hq_len, hq_support⟩
116 rcases mHG.branchRadius v x hxv with ⟨px, _, hpx_len, hpx_support⟩
117 let raw : G.Walk (composedCenter mJH mHG u) x := q.append px
118 refine ⟨raw.bypass, raw.bypass_isPath, ?_, ?_⟩
119 · have hq_len' : q.length ≤ (2 * a + 1) * b := by
120 exact le_trans hq_len (Nat.mul_le_mul_left (2 * a + 1) hpH_len)
121 have hraw_len : raw.length ≤ (2 * a + 1) * b + a := by
122 have hraw_eq : raw.length = q.length + px.length := by
123 dsimp [raw]
124 exact SimpleGraph.Walk.length_append q px
125 rw [hraw_eq]
126 exact add_le_add hq_len' hpx_len
127 have hrewrite : (2 * a + 1) * b + a = 2 * a * b + a + b := by
128 ring
129 exact le_trans raw.length_bypass_le (hrewrite ▸ hraw_len)
130 · intro w hw
131 have hw' : w ∈ raw.support := raw.support_bypass_subset hw
132 dsimp [raw] at hw'
133 have hw'' : w ∈ q.support ∨ w ∈ px.support :=
134 (SimpleGraph.Walk.mem_support_append_iff q px).mp hw'
135 rcases hw'' with hw'' | hw''
136 · exact hq_support w hw''
137 · exact ⟨v, hv, hpx_support w hw''⟩
138
139private theorem composedBranchSet_edge {U V W : Type}
140 {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V} {a b : ℕ}
141 (mJH : ShallowMinorModel J H b) (mHG : ShallowMinorModel H G a)
142 {u v : U} (huv : J.Adj u v) :
143 ∃ x ∈ composedBranchSet mJH mHG u, ∃ y ∈ composedBranchSet mJH mHG v, G.Adj x y := by
144 rcases mJH.branchEdge u v huv with ⟨u', hu', v', hv', hu'v'⟩
145 rcases mHG.branchEdge u' v' hu'v' with ⟨x, hx, y, hy, hxy⟩
146 exact ⟨x, ⟨u', hu', hx⟩, y, ⟨v', hv', hy⟩, hxy⟩
147
148/-- The depth-`d` reduct of a graph class `C`: the class of all graphs
149 that are depth-`d` shallow minors of some graph in `C`. (Def 2.13) -/
150def ShallowReduct (C : GraphClass) (d : ℕ) : GraphClass :=
151 fun {V : Type} [DecidableEq V] [Fintype V] (H : SimpleGraph V) =>
152 ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (G : SimpleGraph W),
153 C G ∧ IsShallowMinor H G d
154
155/-- Lemma 2.12: Composition of shallow minors. -/
156theorem shallowMinor_trans
157 {V W U : Type} {J : SimpleGraph U} {H : SimpleGraph W} {G : SimpleGraph V}
158 {a b : ℕ} :
159 IsShallowMinor J H b → IsShallowMinor H G a →
160 IsShallowMinor J G (2 * a * b + a + b) := by
161 intro hJH hHG
162 rcases hJH with ⟨mJH⟩
163 rcases hHG with ⟨mHG⟩
164 refine ⟨{
165 branchSet := composedBranchSet mJH mHG
166 center := composedCenter mJH mHG
167 center_mem := composedCenter_mem mJH mHG
168 branchDisjoint := fun u v huv => composedBranchSet_disjoint mJH mHG huv
169 branchRadius := fun u x hx => composedBranchSet_radius mJH mHG u x hx
170 branchEdge := fun u v huv => composedBranchSet_edge mJH mHG huv
171 }⟩
172
173/-- Corollary 2.14: If C is nowhere dense, then C ∇ d is nowhere dense. -/
174theorem nowhereDense_shallowReduct (C : GraphClass) (d : ℕ) :
175 IsNowhereDense C → IsNowhereDense (ShallowReduct C d) := by
176 intro hC d'
177 obtain ⟨t, ht⟩ := hC (2 * d * d' + d + d')
178 refine ⟨t, ?_⟩
179 intro V hV _ H hH hminor
180 rcases hH with ⟨W, _, _, G, hCG, hHG⟩
181 exact ht G hCG (shallowMinor_trans hminor hHG)
182
183end Catalog.Sparsity.ShallowMinorComposition
184