Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/NDSubpolynomialWcol/Full.lean
1import Catalog.Sparsity.Preliminaries.Full
2import Catalog.Sparsity.ColoringNumbers.Full
3import Catalog.Sparsity.Admissibility.Full
4import Catalog.Sparsity.NowhereDense.Full
5import Catalog.Sparsity.NDSubpolynomialDensity.Full
6import Catalog.Sparsity.AdmBoundByTopGrad.Full
7import Catalog.Sparsity.ColoringNumberEquivalence.Full
8import Catalog.Sparsity.ShallowMinor.Full
9import Catalog.Sparsity.ShallowMinorComposition.Full
10import Catalog.Sparsity.ShallowTopologicalMinor.Full
11import Mathlib.Analysis.SpecialFunctions.Pow.Real
12
13open Catalog.Sparsity.ColoringNumbers
14open Catalog.Sparsity.Admissibility
15open Catalog.Sparsity.NowhereDense
16open Catalog.Sparsity.Preliminaries
17open Catalog.Sparsity.ShallowMinor
18open Catalog.Sparsity.ShallowMinorComposition
19open Catalog.Sparsity.ShallowTopologicalMinor
20
21namespace Catalog.Sparsity.NDSubpolynomialWcol
22
23/-! ## Helper lemmas -/
24
25/-- Edge count of a simple graph is at most |V|². -/
26private lemma edgeFinset_card_le_card_mul_card {W : Type} [DecidableEq W] [Fintype W]
27 (H : SimpleGraph W) [DecidableRel H.Adj] :
28 H.edgeFinset.card ≤ Fintype.card W * Fintype.card W := by
29 calc H.edgeFinset.card
30 ≤ (Fintype.card W).choose 2 := SimpleGraph.card_edgeFinset_le_card_choose_two
31 _ = Fintype.card W * (Fintype.card W - 1) / 2 := Nat.choose_two_right _
32 _ ≤ Fintype.card W * (Fintype.card W - 1) := Nat.div_le_self _ 2
33 _ ≤ Fintype.card W * Fintype.card W :=
34 Nat.mul_le_mul_left _ (Nat.sub_le _ 1)
35
36/-- Topological minors have at most as many vertices as the host. -/
37private lemma card_le_of_isShallowTopologicalMinor {V W : Type}
38 [DecidableEq W] [Fintype W] [Fintype V]
39 {H : SimpleGraph W} {G : SimpleGraph V} {d : ℕ}
40 (h : IsShallowTopologicalMinor H G d) :
41 Fintype.card W ≤ Fintype.card V := by
42 obtain ⟨m⟩ := h
43 exact Fintype.card_le_of_injective m.branchVertex m.branchVertex.injective
44
45/-- Theorem 3.4/ch2: Nowhere dense classes have subpolynomial wcol. -/
46theorem nd_subpolynomial_wcol (C : GraphClass) (hC : IsNowhereDense C)
47 (r : ℕ) (ε : ℝ) (hε : 0 < ε) :
48 ∃ f : ℝ, 0 < f ∧ ∀ {V : Type} [DecidableEq V] [Fintype V]
49 (G : SimpleGraph V),
50 C G → ∃ (ord : LinearOrder V),
51 letI := ord; (↑(wcol G r) : ℝ) ≤ f * (Fintype.card V : ℝ) ^ ε := by
52 -- Choose ε₁ for the density bound, ensuring 3·r²·ε₁ < ε
53 set ε₁ := ε / (3 * ↑(r ^ 2) + 1) with hε₁_def
54 have hε₁_pos : 0 < ε₁ := div_pos hε (by positivity)
55 -- Get N from subpolynomial density (for depth r-1 shallow reducts)
56 obtain ⟨N, hN⟩ := Catalog.Sparsity.NDSubpolynomialDensity.nd_subpolynomial_density
57 C hC (r - 1) ε₁ hε₁_pos
58 -- Define constant K = r · (6r)^{r²} · (N+2)^{3r²} and set f = K + 1
59 set K : ℕ := r * (6 * r) ^ (r ^ 2) * (N + 2) ^ (3 * r ^ 2) with hK_def
60 refine ⟨↑K + 1, by positivity, ?_⟩
61 -- For each graph G in C
62 intro V _ _ G hCG
63 set n := Fintype.card V with hn_def
64 -- Define d = ⌈n^{ε₁}⌉₊ + N
65 set d := ⌈(↑n : ℝ) ^ ε₁⌉₊ + N with hd_def
66 -- Prove edge bound hypothesis for adm_le_of_topGrad_bound
67 have hd_bound : ∀ {W : Type} [DecidableEq W] [Fintype W]
68 (H : SimpleGraph W) [DecidableRel H.Adj],
69 IsShallowTopologicalMinor H G (r - 1) →
70 H.edgeFinset.card ≤ d * Fintype.card W := by
71 intro W _ _ H _ hMinor
72 set m := Fintype.card W with hm_def
73 -- Case split on whether m ≥ N (large) or m < N (small)
74 by_cases hm_large : N ≤ m
75 · -- Large case: use density bound
76 -- H is a topological minor → shallow minor → in ShallowReduct C (r-1)
77 have hSM : IsShallowMinor H G (r - 1) :=
78 shallowTopologicalMinor_toShallowMinor hMinor
79 have hReduct : ShallowReduct C (r - 1) H :=
80 ⟨V, inferInstance, inferInstance, G, hCG, hSM⟩
81 have hDensity := hN H hReduct hm_large
82 -- hDensity : (↑(H.edgeFinset.card) : ℝ) < (↑m : ℝ) ^ (1 + ε₁)
83 -- |V(H)| ≤ |V(G)| = n
84 have hm_le_n : m ≤ n := card_le_of_isShallowTopologicalMinor hMinor
85 -- Chain: edge_count < m^{1+ε₁} = m · m^{ε₁} ≤ m · n^{ε₁} ≤ m · ⌈n^{ε₁}⌉ ≤ m · d
86 by_cases hm0 : m = 0
87 · have h := edgeFinset_card_le_card_mul_card H
88 simp only [← hm_def, hm0, Nat.mul_zero, Nat.le_zero] at h ⊢
89 exact h
90 · have hm_pos : (0 : ℝ) < ↑m := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hm0)
91 have h1 : (↑m : ℝ) ^ (1 + ε₁) = ↑m * (↑m : ℝ) ^ ε₁ := by
92 rw [Real.rpow_add hm_pos, Real.rpow_one]
93 have h2 : (↑m : ℝ) ^ ε₁ ≤ (↑n : ℝ) ^ ε₁ :=
94 Real.rpow_le_rpow (Nat.cast_nonneg _) (Nat.cast_le.mpr hm_le_n) hε₁_pos.le
95 have h3 : (↑n : ℝ) ^ ε₁ ≤ ↑d := by
96 calc (↑n : ℝ) ^ ε₁ ≤ ↑⌈(↑n : ℝ) ^ ε₁⌉₊ := Nat.le_ceil _
97 _ ≤ ↑d := by exact_mod_cast Nat.le_add_right _ N
98 have key : (↑(H.edgeFinset.card) : ℝ) < ↑d * ↑m := calc
99 (↑(H.edgeFinset.card) : ℝ) < (↑m : ℝ) ^ (1 + ε₁) := hDensity
100 _ = ↑m * (↑m : ℝ) ^ ε₁ := h1
101 _ ≤ ↑m * ↑d := mul_le_mul_of_nonneg_left (h2.trans h3) hm_pos.le
102 _ = ↑d * ↑m := mul_comm _ _
103 exact_mod_cast key.le
104 · -- Small case: m < N, so edge_count ≤ m² ≤ m · N ≤ m · d
105 push_neg at hm_large
106 calc H.edgeFinset.card
107 ≤ m * m := edgeFinset_card_le_card_mul_card H
108 _ ≤ m * N := Nat.mul_le_mul_left m (Nat.le_of_lt hm_large)
109 _ ≤ m * d := Nat.mul_le_mul_left m (Nat.le_add_left N _)
110 _ = d * m := Nat.mul_comm m d
111 -- Get ordering from admissibility bound
112 obtain ⟨ord, hadm⟩ :=
113 Catalog.Sparsity.AdmBoundByTopGrad.adm_le_of_topGrad_bound G r d hd_bound
114 refine ⟨ord, ?_⟩
115 letI := ord
116 -- Chain: wcol ≤ 1 + r·(adm-1)^{r²} ≤ 1 + r·(6r·d³)^{r²}
117 have hwcol := Catalog.Sparsity.ColoringNumberEquivalence.wcol_le_of_adm G r
118 have hadm_sub : adm G r - 1 ≤ 6 * r * d ^ 3 := by omega
119 have hnat_bound : wcol G r ≤ 1 + r * (6 * r * d ^ 3) ^ (r ^ 2) := by
120 calc wcol G r
121 ≤ 1 + r * (adm G r - 1) ^ (r ^ 2) := hwcol
122 _ ≤ 1 + r * (6 * r * d ^ 3) ^ (r ^ 2) := by
123 apply Nat.add_le_add_left
124 apply Nat.mul_le_mul_left
125 exact Nat.pow_le_pow_left hadm_sub _
126 -- Convert to real: ↑(wcol G r) ≤ (↑K + 1) · (↑n)^ε
127 by_cases hn0 : n = 0
128 · -- V is empty, wcol = 0
129 have : IsEmpty V := Fintype.card_eq_zero_iff.mp hn0
130 simp only [show wcol G r = 0 from by simp [wcol, Finset.univ_eq_empty],
131 Nat.cast_zero, show (↑n : ℝ) = 0 from by exact_mod_cast hn0,
132 Real.zero_rpow (ne_of_gt hε), mul_zero, le_refl]
133 · -- n ≥ 1
134 have hn_pos : 0 < n := Nat.pos_of_ne_zero hn0
135 have hn1 : (1 : ℝ) ≤ ↑n := Nat.one_le_cast.mpr hn_pos
136 have hne1 : (1 : ℝ) ≤ (↑n : ℝ) ^ ε₁ := Real.one_le_rpow hn1 hε₁_pos.le
137 have hnε : (1 : ℝ) ≤ (↑n : ℝ) ^ ε := Real.one_le_rpow hn1 hε.le
138 -- d ≤ (N+2) · n^{ε₁}
139 have hd_le : (↑d : ℝ) ≤ (↑N + 2) * (↑n : ℝ) ^ ε₁ := by
140 have hceil := le_of_lt (Nat.ceil_lt_add_one
141 (Real.rpow_nonneg (Nat.cast_nonneg n) ε₁))
142 have h1 : (↑d : ℝ) ≤ (↑n : ℝ) ^ ε₁ + ((↑N : ℝ) + 1) := by
143 push_cast [hd_def]; linarith
144 have h2 : (↑N : ℝ) + 1 ≤ ((↑N : ℝ) + 1) * (↑n : ℝ) ^ ε₁ :=
145 le_mul_of_one_le_right (by positivity) hne1
146 nlinarith
147 -- 3r²ε₁ ≤ ε
148 have hexp : ε₁ * (3 * (↑r : ℝ) ^ 2) ≤ ε := by
149 have h : (0 : ℝ) < 3 * ↑(r ^ 2) + 1 := by positivity
150 have h2 : (3 : ℝ) * (↑r : ℝ) ^ 2 ≤ 3 * ↑(r ^ 2) + 1 := by push_cast; linarith
151 calc ε₁ * (3 * (↑r : ℝ) ^ 2)
152 ≤ ε₁ * (3 * ↑(r ^ 2) + 1) := mul_le_mul_of_nonneg_left h2 hε₁_pos.le
153 _ = ε := by rw [hε₁_def, div_mul_cancel₀ _ (ne_of_gt h)]
154 -- d^{3r²} ≤ (N+2)^{3r²} · (n^{ε₁})^{3r²}
155 have hd_pow : (↑d : ℝ) ^ (3 * r ^ 2) ≤
156 ((↑N : ℝ) + 2) ^ (3 * r ^ 2) * ((↑n : ℝ) ^ ε₁) ^ (3 * r ^ 2) := by
157 rw [← mul_pow]
158 exact pow_le_pow_left₀ (Nat.cast_nonneg _)
159 (by linarith) _
160 -- (n^{ε₁})^{3r²} ≤ n^ε
161 have hrpow_le : ((↑n : ℝ) ^ ε₁) ^ (3 * r ^ 2) ≤ (↑n : ℝ) ^ ε := by
162 rw [← Real.rpow_natCast ((↑n : ℝ) ^ ε₁) (3 * r ^ 2),
163 ← Real.rpow_mul (Nat.cast_nonneg n)]
164 apply Real.rpow_le_rpow_of_exponent_le hn1
165 convert hexp using 1; push_cast; ring
166 -- Main chain
167 have hstep1 : (↑(wcol G r) : ℝ) ≤
168 1 + (↑r : ℝ) * (6 * (↑r : ℝ)) ^ (r ^ 2) * (↑d : ℝ) ^ (3 * r ^ 2) := by
169 have h := Nat.cast_le (α := ℝ).mpr hnat_bound
170 push_cast at h; rw [mul_pow, ← pow_mul] at h; linarith
171 calc (↑(wcol G r) : ℝ)
172 ≤ 1 + (↑r : ℝ) * (6 * ↑r) ^ (r ^ 2) * (↑d : ℝ) ^ (3 * r ^ 2) := hstep1
173 _ ≤ 1 + (↑r : ℝ) * (6 * ↑r) ^ (r ^ 2) *
174 (((↑N : ℝ) + 2) ^ (3 * r ^ 2) * ((↑n : ℝ) ^ ε₁) ^ (3 * r ^ 2)) := by
175 gcongr
176 _ = 1 + (↑K : ℝ) * ((↑n : ℝ) ^ ε₁) ^ (3 * r ^ 2) := by
177 simp only [hK_def]; push_cast; ring
178 _ ≤ 1 + (↑K : ℝ) * (↑n : ℝ) ^ ε := by gcongr
179 _ ≤ (↑n : ℝ) ^ ε + (↑K : ℝ) * (↑n : ℝ) ^ ε := by linarith
180 _ = (↑K + 1) * (↑n : ℝ) ^ ε := by ring
181
182end Catalog.Sparsity.NDSubpolynomialWcol
183