Formalizing Structural Graph Theory in Lean 4

Catalog/Sparsity/NDSubpolynomialDensity/Full.lean
1import Catalog.Sparsity.Preliminaries.Full
2import Catalog.Sparsity.ShallowMinor.Full
3import Catalog.Sparsity.NowhereDense.Full
4import Catalog.Sparsity.ShallowMinorComposition.Full
5import Catalog.Sparsity.Densification.Full
6import Mathlib.Combinatorics.SimpleGraph.Finite
7import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
8import Mathlib.Analysis.SpecialFunctions.Exp
9import Mathlib.Analysis.SpecialFunctions.Pow.Real
10import Mathlib.Tactic
11
12open Catalog.Sparsity.ShallowMinor
13open Catalog.Sparsity.NowhereDense
14open Catalog.Sparsity.Preliminaries
15open Catalog.Sparsity.ShallowMinorComposition
16open Classical
17
18namespace Catalog.Sparsity.NDSubpolynomialDensity
19
20noncomputable section
21
22private structure MinimumDegreeWitness {V : Type} [DecidableEq V] [Fintype V] [Nonempty V]
23 (G : SimpleGraph V) (d : ℕ) where
24 W : Type
25 instDecEqW : DecidableEq W
26 instFintypeW : Fintype W
27 instNonemptyW : Nonempty W
28 f : W ↪ V
29 s : Set V
30 hs : s = Set.range f
31 hcard : Fintype.card W = s.toFinset.card
32 hsdeg : d ≤ (SimpleGraph.comap f G).minDegree
33 hsedge : G.edgeFinset.card ≤ (SimpleGraph.comap f G).edgeFinset.card +
34 (d - 1) * (Fintype.card V - Fintype.card W)
35
36attribute [instance] MinimumDegreeWitness.instDecEqW
37attribute [instance] MinimumDegreeWitness.instFintypeW
38attribute [instance] MinimumDegreeWitness.instNonemptyW
39
40private def embeddingRangeEquiv {V W : Type} (f : W ↪ V) : W ≃ Set.range f :=
41 { toFun := fun w => ⟨f w, ⟨w, rfl⟩⟩
42 invFun := fun v => Classical.choose v.2
43 left_inv := by
44 intro w
45 apply f.injective
46 simpa using (Classical.choose_spec (p := fun u : W => f u = f w) ⟨w, rfl⟩)
47 right_inv := by
48 intro v
49 apply Subtype.ext
50 simpa using (Classical.choose_spec (p := fun u : W => f u = v.1) v.2) }
51
52private def comapIsoInduceRange {V W : Type} (G : SimpleGraph V) (f : W ↪ V) :
53 SimpleGraph.comap f G ≃g G.induce (Set.range f) :=
54 { toEquiv := embeddingRangeEquiv f
55 map_rel_iff' := by
56 intro a b
57 constructor <;> intro hab <;> simpa using hab }
58
59private def minimumDegreeWitnessAux (n : ℕ) :
60 ∀ {V : Type} [DecidableEq V] [Fintype V] [Nonempty V],
61 Fintype.card V = n →
62 ∀ (G : SimpleGraph V) (d : ℕ),
63 d * Fintype.card V ≤ G.edgeFinset.card →
64 MinimumDegreeWitness G d := by
65 induction n with
66 | zero =>
67 intro V _ _ _ hcard G d hEdges
68 exfalso
69 have : 0 < Fintype.card V := Fintype.card_pos
70 rw [hcard] at this
71 omega
72 | succ n ih =>
73 intro V _ _ _ hcard G d hEdges
74 letI : DecidableRel G.Adj := Classical.decRel _
75 by_cases hd : d ≤ G.minDegree
76 · refine
77 { W := V
78 instDecEqW := inferInstance
79 instFintypeW := inferInstance
80 instNonemptyW := inferInstance
81 f := Function.Embedding.refl V
82 s := Set.univ
83 hs := by
84 ext v
85 simp
86 hcard := by
87 simp
88 hsdeg := ?_
89 hsedge := ?_ }
90 · change d ≤ G.minDegree
91 exact hd
92 · change G.edgeFinset.card ≤ G.edgeFinset.card +
93 (d - 1) * (Fintype.card V - Fintype.card V)
94 simp
95 · let x : V := Classical.choose G.exists_minimal_degree_vertex
96 have hx : G.minDegree = G.degree x := Classical.choose_spec G.exists_minimal_degree_vertex
97 have hdeglt : G.degree x < d := by
98 have hminlt : G.minDegree < d := lt_of_not_ge hd
99 simpa [hx] using hminlt
100 cases n with
101 | zero =>
102 have hcard1 : Fintype.card V = 1 := hcard
103 have hdpos : 0 < d := by omega
104 have hedgele : G.edgeFinset.card ≤ 0 := by
105 calc
106 G.edgeFinset.card ≤ (Fintype.card V).choose 2 := G.card_edgeFinset_le_card_choose_two
107 _ = 0 := by rw [hcard1]; decide
108 have : d * 1 ≤ 0 := by simpa [hcard1] using le_trans hEdges hedgele
109 omega
110 | succ n' =>
111 let s0 : Set V := { y : V | y ≠ x }
112 have hcard_s0_raw : Fintype.card s0 = Fintype.card V - 1 := by
113 simpa [s0] using (Set.card_ne_eq x)
114 have hcard_s0 : Fintype.card s0 = n' + 1 := by
115 rw [hcard_s0_raw, hcard]
116 omega
117 haveI : Nonempty s0 := Fintype.card_pos_iff.mp (by rw [hcard_s0]; exact Nat.succ_pos _)
118 have hEdges_s0 : d * Fintype.card s0 ≤ (G.induce s0).edgeFinset.card := by
119 have hdeg_le : G.degree x ≤ d := Nat.le_of_lt hdeglt
120 have hedge : (G.induce s0).edgeFinset.card = G.edgeFinset.card - G.degree x := by
121 have hs0 : s0 = ({x}ᶜ : Set V) := by
122 ext y
123 simp [s0]
124 simpa [hs0] using
125 (show (G.induce ({x}ᶜ : Set V)).edgeFinset.card = G.edgeFinset.card - G.degree x by
126 rw [G.card_edgeFinset_induce_compl_singleton x, G.card_edgeFinset_deleteIncidenceSet x])
127 calc
128 d * Fintype.card s0 = d * (Fintype.card V - 1) := by rw [hcard_s0_raw]
129 _ = d * Fintype.card V - d := by rw [Nat.mul_sub, Nat.mul_one]
130 _ ≤ G.edgeFinset.card - d := Nat.sub_le_sub_right hEdges d
131 _ ≤ G.edgeFinset.card - G.degree x := by omega
132 _ = (G.induce s0).edgeFinset.card := hedge.symm
133 let w : MinimumDegreeWitness (G.induce s0) d :=
134 ih hcard_s0 (G.induce s0) d hEdges_s0
135 let f0 : w.W ↪ V :=
136 { toFun := fun v => (w.f v).1
137 inj' := by
138 intro a b h
139 apply w.f.injective
140 exact Subtype.ext h }
141 have hsdeg0 : d ≤ (SimpleGraph.comap f0 G).minDegree := by
142 change d ≤ (SimpleGraph.comap w.f (G.induce s0)).minDegree
143 exact w.hsdeg
144 have hdeg_loss : G.degree x ≤ d - 1 := by omega
145 have hedge : (G.induce s0).edgeFinset.card = G.edgeFinset.card - G.degree x := by
146 have hs0 : s0 = ({x}ᶜ : Set V) := by
147 ext y
148 simp [s0]
149 simpa [hs0] using
150 (show (G.induce ({x}ᶜ : Set V)).edgeFinset.card = G.edgeFinset.card - G.degree x by
151 rw [G.card_edgeFinset_induce_compl_singleton x, G.card_edgeFinset_deleteIncidenceSet x])
152 have hcard_W_le_s0 : Fintype.card w.W ≤ Fintype.card s0 := by
153 exact Fintype.card_le_of_embedding w.f
154 have hcard_s0_succ : Fintype.card s0 + 1 = Fintype.card V := by
155 have hone_le : 1 ≤ Fintype.card V := by
156 rw [hcard]
157 omega
158 rw [hcard_s0_raw]
159 simpa using (Nat.sub_add_cancel hone_le)
160 have hcard_diff :
161 Fintype.card s0 - Fintype.card w.W + 1 = Fintype.card V - Fintype.card w.W := by
162 calc
163 Fintype.card s0 - Fintype.card w.W + 1 = Fintype.card s0 + 1 - Fintype.card w.W := by
164 simpa [Nat.add_comm] using
165 (Nat.sub_add_comm (n := Fintype.card s0) (m := 1)
166 (k := Fintype.card w.W) hcard_W_le_s0).symm
167 _ = Fintype.card V - Fintype.card w.W := by rw [hcard_s0_succ]
168 have hsedge0 :
169 G.edgeFinset.card ≤ (SimpleGraph.comap f0 G).edgeFinset.card +
170 (d - 1) * (Fintype.card V - Fintype.card w.W) := by
171 change G.edgeFinset.card ≤
172 (SimpleGraph.comap w.f (G.induce s0)).edgeFinset.card +
173 (d - 1) * (Fintype.card V - Fintype.card w.W)
174 calc
175 G.edgeFinset.card = (G.induce s0).edgeFinset.card + G.degree x := by
176 rw [hedge, Nat.sub_add_cancel]
177 exact G.degree_le_card_edgeFinset x
178 _ ≤ (SimpleGraph.comap w.f (G.induce s0)).edgeFinset.card +
179 (d - 1) * (Fintype.card s0 - Fintype.card w.W) + (d - 1) := by
180 exact add_le_add w.hsedge hdeg_loss
181 _ = (SimpleGraph.comap w.f (G.induce s0)).edgeFinset.card +
182 (d - 1) * ((Fintype.card s0 - Fintype.card w.W) + 1) := by
183 rw [Nat.mul_add, Nat.mul_one]
184 ac_rfl
185 _ = (SimpleGraph.comap w.f (G.induce s0)).edgeFinset.card +
186 (d - 1) * (Fintype.card V - Fintype.card w.W) := by
187 rw [hcard_diff]
188 exact
189 { W := w.W
190 instDecEqW := w.instDecEqW
191 instFintypeW := w.instFintypeW
192 instNonemptyW := w.instNonemptyW
193 f := f0
194 s := Set.range f0
195 hs := rfl
196 hcard := by
197 rw [Set.toFinset_range]
198 symm
199 simpa using Finset.card_image_of_injective Finset.univ f0.injective
200 hsdeg := hsdeg0
201 hsedge := hsedge0 }
202
203private theorem exists_inducedSubgraph_minDegree_sq_card
204 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V] (G : SimpleGraph V) (d : ℕ)
205 (hEdges : d * Fintype.card V ≤ G.edgeFinset.card) :
206 ∃ s : Set V, d ≤ (G.induce s).minDegree ∧ Fintype.card V ≤ (Fintype.card s) ^ 2 := by
207 letI : DecidableRel G.Adj := Classical.decRel _
208 let P : Set V → Prop := fun s =>
209 d ≤ (G.induce s).minDegree ∧ Fintype.card V ≤ (Fintype.card s) ^ 2
210 change ∃ s : Set V, P s
211 by_cases hd0 : d = 0
212 · subst d
213 refine ⟨Set.univ, by simp, ?_⟩
214 have hpos : 0 < Fintype.card V := Fintype.card_pos
215 have hpow : Fintype.card V ≤ (Fintype.card V) ^ 2 := by
216 calc
217 Fintype.card V = 1 * Fintype.card V := by simp
218 _ ≤ Fintype.card V * Fintype.card V := by
219 exact Nat.mul_le_mul_right _ (Nat.succ_le_of_lt hpos)
220 _ = (Fintype.card V) ^ 2 := by simp [pow_two]
221 rw [Fintype.card_setUniv]; exact hpow
222 · let w : MinimumDegreeWitness G d :=
223 minimumDegreeWitnessAux (Fintype.card V) rfl G d hEdges
224 have hcard_s : Fintype.card w.W = Fintype.card w.s := by
225 calc
226 Fintype.card w.W = w.s.toFinset.card := w.hcard
227 _ = Fintype.card w.s := by
228 rw [Set.toFinset_card]
229 let iso : SimpleGraph.comap w.f G ≃g G.induce w.s := by
230 rw [w.hs]
231 exact comapIsoInduceRange G w.f
232 have hsdeg : d ≤ (G.induce w.s).minDegree := by
233 exact iso.minDegree_eq ▸ w.hsdeg
234 have hsedge :
235 G.edgeFinset.card ≤ (G.induce w.s).edgeFinset.card +
236 (d - 1) * (Fintype.card V - Fintype.card w.s) := by
237 calc
238 G.edgeFinset.card ≤ (SimpleGraph.comap w.f G).edgeFinset.card +
239 (d - 1) * (Fintype.card V - Fintype.card w.W) := w.hsedge
240 _ = (G.induce w.s).edgeFinset.card +
241 (d - 1) * (Fintype.card V - Fintype.card w.s) := by
242 rw [iso.card_edgeFinset_eq, hcard_s]
243 have hsize : Fintype.card V ≤ (Fintype.card w.s) ^ 2 := by
244 by_contra hsbad
245 have hslt : (Fintype.card w.s) ^ 2 < Fintype.card V := lt_of_not_ge hsbad
246 have hedge_small : (G.induce w.s).edgeFinset.card < Fintype.card V := by
247 calc
248 (G.induce w.s).edgeFinset.card ≤ (Fintype.card w.s).choose 2 :=
249 (G.induce w.s).card_edgeFinset_le_card_choose_two
250 _ ≤ (Fintype.card w.s) ^ 2 := Nat.choose_le_pow _ 2
251 _ < Fintype.card V := hslt
252 have hdpos : 0 < d := Nat.pos_of_ne_zero hd0
253 have hcontra : G.edgeFinset.card < d * Fintype.card V := by
254 have hsucc : 1 + (d - 1) = d := by
255 simpa [Nat.add_comm] using (Nat.succ_pred_eq_of_pos hdpos)
256 calc
257 G.edgeFinset.card ≤ (G.induce w.s).edgeFinset.card +
258 (d - 1) * (Fintype.card V - Fintype.card w.s) := hsedge
259 _ < Fintype.card V + (d - 1) * (Fintype.card V - Fintype.card w.s) := by
260 exact Nat.add_lt_add_right hedge_small _
261 _ ≤ Fintype.card V + (d - 1) * Fintype.card V := by
262 exact Nat.add_le_add_left (Nat.mul_le_mul_left _ (Nat.sub_le _ _)) _
263 _ = d * Fintype.card V := by
264 calc
265 Fintype.card V + (d - 1) * Fintype.card V = (1 + (d - 1)) * Fintype.card V := by
266 rw [Nat.add_mul, Nat.one_mul]
267 _ = d * Fintype.card V := by rw [hsucc]
268 exact (not_lt_of_ge hEdges) hcontra
269 exact ⟨w.s, hsdeg, hsize⟩
270
271private theorem isShallowMinor_zero_of_embedding {V W : Type}
272 {G : SimpleGraph V} {H : SimpleGraph W} (f : H ↪g G) :
273 IsShallowMinor H G 0 := by
274 refine ⟨{
275 branchSet := fun w => {f w}
276 center := fun w => f w
277 center_mem := ?_
278 branchDisjoint := ?_
279 branchRadius := ?_
280 branchEdge := ?_ }⟩
281 · intro w
282 simp
283 · intro u v huv
284 refine Set.disjoint_left.2 ?_
285 intro x hxU hxV
286 simp only [Set.mem_singleton_iff] at hxU hxV
287 exact huv (f.injective (hxU.symm.trans hxV))
288 · intro v x hx
289 rw [Set.mem_singleton_iff] at hx
290 subst x
291 refine ⟨SimpleGraph.Walk.nil, SimpleGraph.Walk.IsPath.nil, by simp, ?_⟩
292 intro w hw
293 simp at hw
294 simp [hw]
295 · intro u v huv
296 exact ⟨f u, by simp, f v, by simp, f.map_rel_iff.mpr huv⟩
297
298private theorem isShallowMinor_mono {V W : Type}
299 {H : SimpleGraph W} {G : SimpleGraph V} {d d' : ℕ}
300 (hMinor : IsShallowMinor H G d) (hdd' : d ≤ d') :
301 IsShallowMinor H G d' := by
302 rcases hMinor with ⟨m⟩
303 refine ⟨{
304 branchSet := m.branchSet
305 center := m.center
306 center_mem := m.center_mem
307 branchDisjoint := m.branchDisjoint
308 branchRadius := ?_
309 branchEdge := m.branchEdge }⟩
310 intro v x hx
311 rcases m.branchRadius v x hx with ⟨p, hpPath, hpLen, hpSupp⟩
312 exact ⟨p, hpPath, le_trans hpLen hdd', hpSupp⟩
313
314private theorem induced_isShallowMinor_zero {V : Type} [DecidableEq V] [Fintype V]
315 (G : SimpleGraph V) (s : Set V) :
316 IsShallowMinor (G.induce s) G 0 := by
317 simpa using
318 (isShallowMinor_zero_of_embedding
319 (SimpleGraph.Embedding.comap (Function.Embedding.subtype s) G))
320
321private def completeGraphEmbeddingOfLE {m n : ℕ} (hmn : m ≤ n) :
322 SimpleGraph.completeGraph (Fin m) ↪g SimpleGraph.completeGraph (Fin n) :=
323 SimpleGraph.Embedding.completeGraph (Fin.castLEEmb hmn)
324
325private theorem clique_minor_of_large_card
326 {V : Type} [DecidableEq V] [Fintype V] {G : SimpleGraph V} {t q : ℕ}
327 (htCard : Nat.ceil (Real.exp t) ≤ Fintype.card V)
328 (hqLog : Real.log ↑(Fintype.card V) ≤ q)
329 (hMinor : IsShallowMinor (SimpleGraph.completeGraph (Fin (q + 1))) G 1) :
330 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G 1 := by
331 have hExpLe : Real.exp t ≤ Fintype.card V := by
332 calc
333 Real.exp t ≤ Nat.ceil (Real.exp t) := by exact_mod_cast Nat.le_ceil (Real.exp t)
334 _ ≤ Fintype.card V := by exact_mod_cast htCard
335 have htLog : (t : ℝ) ≤ Real.log ↑(Fintype.card V) := by
336 have hCardPos : 0 < (Fintype.card V : ℝ) := lt_of_lt_of_le (Real.exp_pos t) hExpLe
337 simpa using Real.log_le_log (Real.exp_pos t) hExpLe
338 have htq_real : (t : ℝ) ≤ q := le_trans htLog hqLog
339 have htq : t ≤ q := by exact_mod_cast htq_real
340 exact shallowMinor_trans
341 (isShallowMinor_zero_of_embedding
342 (completeGraphEmbeddingOfLE (Nat.succ_le_succ htq)))
343 hMinor
344
345private theorem not_boostedMinor_of_large_parameter
346 {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {ε : ℝ}
347 (hWpos : 0 < (Fintype.card W : ℝ)) (hε58 : (5 : ℝ) / 8 ≤ ε)
348 (hEdges : (Fintype.card W : ℝ) ^ (1 + ε + ε ^ (2 : ℕ)) ≤ (H.edgeFinset.card : ℝ)) :
349 False := by
350 let m : ℝ := Fintype.card W
351 have hm_pos : 0 < m := hWpos
352 have hm_one_le : 1 ≤ m := by
353 have hcard_pos : 0 < Fintype.card W := by
354 exact_mod_cast hWpos
355 change (1 : ℝ) ≤ (Fintype.card W : ℝ)
356 exact_mod_cast (Nat.succ_le_of_lt hcard_pos)
357 have hcardUpper : (H.edgeFinset.card : ℝ) ≤ m ^ (2 : ℕ) := by
358 calc
359 (H.edgeFinset.card : ℝ) ≤ ((Fintype.card W).choose 2 : ℝ) := by
360 exact_mod_cast H.card_edgeFinset_le_card_choose_two
361 _ ≤ ((Fintype.card W) ^ 2 : ℕ) := by exact_mod_cast Nat.choose_le_pow _ 2
362 _ = m ^ (2 : ℕ) := by simp [m]
363 have hExpLarge : (2 : ℝ) < 1 + ε + ε ^ (2 : ℕ) := by
364 nlinarith [sq_nonneg (ε - (3 : ℝ) / 8)]
365 have hLower : m ^ (2 : ℝ) < m ^ (1 + ε + ε ^ (2 : ℕ)) := by
366 have hm_one_lt : 1 < m := by
367 by_contra hmNotLt
368 have hm_le_one : m ≤ 1 := le_of_not_gt hmNotLt
369 have hcard_pos : 0 < Fintype.card W := by
370 have hm_pos' : 0 < (Fintype.card W : ℝ) := by simpa [m] using hm_pos
371 exact_mod_cast hm_pos'
372 have hcard_le_one : Fintype.card W ≤ 1 := by
373 change (Fintype.card W : ℝ) ≤ 1 at hm_le_one
374 exact_mod_cast hm_le_one
375 have hcard : Fintype.card W = 1 := by omega
376 have hEdgesZero : (H.edgeFinset.card : ℝ) = 0 := by
377 have hle0 : (H.edgeFinset.card : ℝ) ≤ 0 := by
378 calc
379 (H.edgeFinset.card : ℝ) ≤ ((Fintype.card W).choose 2 : ℝ) := by
380 exact_mod_cast H.card_edgeFinset_le_card_choose_two
381 _ = 0 := by rw [hcard]; norm_num
382 linarith
383 have : ¬ ((1 : ℝ) ^ (1 + ε + ε ^ (2 : ℕ)) ≤ (H.edgeFinset.card : ℝ)) := by
384 simp [hEdgesZero]
385 have hEdgesOne : (1 : ℝ) ^ (1 + ε + ε ^ (2 : ℕ)) ≤ (H.edgeFinset.card : ℝ) := by
386 simpa [m, hcard] using hEdges
387 exact this hEdgesOne
388 have := Real.rpow_lt_rpow_of_exponent_lt hm_one_lt hExpLarge
389 simpa [Real.rpow_natCast] using this
390 have hcardUpper' : (H.edgeFinset.card : ℝ) ≤ m ^ (2 : ℝ) := by
391 simpa [Real.rpow_natCast] using hcardUpper
392 exact (not_lt_of_ge hcardUpper') (hLower.trans_le hEdges)
393
394private theorem card_le_pow_three_of_boost
395 {V W : Type} [Fintype V] [Fintype W] {ε : ℝ}
396 (hVpos : 0 < (Fintype.card V : ℝ)) (hε : ε ≤ (2 : ℝ) / 3)
397 (hWlo : (Fintype.card V : ℝ) ^ (1 - ε) ≤ (Fintype.card W : ℝ)) :
398 (Fintype.card V : ℝ) ≤ (Fintype.card W : ℝ) ^ (3 : ℕ) := by
399 let n : ℝ := Fintype.card V
400 let m : ℝ := Fintype.card W
401 have hExp : (1 : ℝ) / 3 ≤ 1 - ε := by linarith
402 have hcalc : n ^ ((1 : ℝ) / 3) ≤ m := by
403 calc
404 n ^ ((1 : ℝ) / 3) ≤ n ^ (1 - ε) := by
405 have hn_one : 1 ≤ n := by
406 change (1 : ℝ) ≤ (Fintype.card V : ℝ)
407 exact_mod_cast (Nat.succ_le_of_lt (show 0 < Fintype.card V by exact_mod_cast hVpos))
408 exact Real.rpow_le_rpow_of_exponent_le hn_one hExp
409 _ ≤ m := hWlo
410 have hpow := Real.rpow_le_rpow (by positivity : 0 ≤ n ^ ((1 : ℝ) / 3)) hcalc
411 (by positivity : (0 : ℝ) ≤ (3 : ℝ))
412 have hn_eq : (n ^ ((1 : ℝ) / 3)) ^ (3 : ℝ) = n := by
413 calc
414 (n ^ ((1 : ℝ) / 3)) ^ (3 : ℝ) = n ^ (((1 : ℝ) / 3) * 3) := by
415 rw [Real.rpow_mul (by positivity : 0 ≤ n)]
416 _ = n ^ (1 : ℕ) := by simp
417 _ = n := by simp
418 calc
419 n = (n ^ ((1 : ℝ) / 3)) ^ (3 : ℝ) := hn_eq.symm
420 _ ≤ m ^ (3 : ℝ) := hpow
421 _ = m ^ (3 : ℕ) := by simp
422
423private theorem le_floor_double {x : ℝ} (hx : 1 ≤ x) :
424 x ≤ Nat.floor (2 * x) := by
425 have hlt : 2 * x < Nat.floor (2 * x) + 1 := Nat.lt_floor_add_one (2 * x)
426 have hx2 : x ≤ 2 * x - 1 := by linarith
427 have hle : 2 * x - 1 < Nat.floor (2 * x) := by linarith
428 linarith
429
430private theorem rpow_le_floor_rpow_add
431 {n a δ : ℝ} (hn : 0 < n) (hn1 : 1 ≤ n) (ha : 0 ≤ a) (hgap : 2 ≤ n ^ δ) :
432 n ^ a ≤ Nat.floor (n ^ (a + δ)) := by
433 have hxa : 1 ≤ n ^ a := Real.one_le_rpow hn1 ha
434 have hdouble : 2 * n ^ a ≤ n ^ (a + δ) := by
435 calc
436 2 * n ^ a ≤ n ^ δ * n ^ a := by gcongr
437 _ = n ^ (a + δ) := by
438 rw [mul_comm, ← Real.rpow_add hn]
439 have hfloorMono : (Nat.floor (2 * n ^ a) : ℝ) ≤ Nat.floor (n ^ (a + δ)) := by
440 exact_mod_cast Nat.floor_mono hdouble
441 exact le_trans (le_floor_double hxa) hfloorMono
442
443private theorem le_of_sq_le_sq {m n : ℕ} (h : m ^ 2 ≤ n ^ 2) :
444 m ≤ n := by
445 exact (Nat.pow_le_pow_iff_left (show (2 : ℕ) ≠ 0 by decide)).1 h
446
447private theorem le_of_pow_six_le_pow_six {m n : ℕ} (h : m ^ 6 ≤ n ^ 6) :
448 m ≤ n := by
449 exact (Nat.pow_le_pow_iff_left (show (6 : ℕ) ≠ 0 by decide)).1 h
450
451private def iterationDepth : ℕ → ℕ
452 | 0 => 0
453 | k + 1 => 3 * iterationDepth k + 1
454
455private theorem iterationDepth_monotone : Monotone iterationDepth := by
456 intro i j hij
457 induction hij with
458 | refl =>
459 rfl
460 | @step j hij ih =>
461 have hsucc : iterationDepth j ≤ iterationDepth (j + 1) := by
462 simp [iterationDepth]
463 omega
464 exact le_trans ih hsucc
465
466private def sizeSeq (B : ℕ) : ℕ → ℕ
467 | 0 => B
468 | j + 1 => (sizeSeq B j) ^ 6
469
470private theorem sizeSeq_base_le {B : ℕ} (hB : 1 ≤ B) :
471 ∀ j : ℕ, B ≤ sizeSeq B j := by
472 intro j
473 induction j with
474 | zero =>
475 simp [sizeSeq]
476 | succ j ih =>
477 simp [sizeSeq]
478 calc
479 B ≤ sizeSeq B j := ih
480 _ ≤ (sizeSeq B j) ^ 6 := by
481 have hpos : 0 < sizeSeq B j := lt_of_lt_of_le (by decide : 0 < 1) (le_trans hB ih)
482 simpa using
483 (Nat.pow_le_pow_right hpos (show 1 ≤ 6 by decide) :
484 (sizeSeq B j) ^ 1 ≤ (sizeSeq B j) ^ 6)
485
486private theorem step_or_clique
487 {V : Type} [DecidableEq V] [Fintype V] [Nonempty V]
488 (G : SimpleGraph V) (M : ℕ)
489 {a δ : ℝ} (ha0 : 0 < a) (ha23 : a ≤ (2 : ℝ) / 3)
490 (_hδ : 0 < δ) (hδa : 2 * δ ≤ a ^ (2 : ℕ))
491 (hDensify :
492 ∀ {W : Type} [DecidableEq W] [Fintype W]
493 (H : SimpleGraph W) [DecidableRel H.Adj],
494 M ≤ Fintype.card W →
495 (∀ v : W, (Fintype.card W : ℝ) ^ a ≤ ↑(H.degree v)) →
496 (∃ t : ℕ, Real.log ↑(Fintype.card W) ≤ ↑t ∧
497 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) H 1) ∨
498 (∃ (U : Type) (_ : DecidableEq U) (_ : Fintype U)
499 (H' : SimpleGraph U) (_ : DecidableRel H'.Adj),
500 IsShallowMinor H' H 1 ∧
501 (Fintype.card W : ℝ) ^ (1 - a) ≤ ↑(Fintype.card U) ∧
502 (Fintype.card U : ℝ) ^ (1 + a + a ^ 2) ≤ ↑(H'.edgeFinset.card)))
503 {t0 : ℕ}
504 (hMBound : M ^ 2 ≤ Fintype.card V)
505 (hCliqueBound : (Nat.ceil (Real.exp t0)) ^ 2 ≤ Fintype.card V)
506 (hRound : 2 ≤ (Fintype.card V : ℝ) ^ δ)
507 (hDense : (Fintype.card V : ℝ) ^ (1 + a + δ) ≤ (G.edgeFinset.card : ℝ)) :
508 IsShallowMinor (SimpleGraph.completeGraph (Fin (t0 + 1))) G 1 ∨
509 ((a < (5 : ℝ) / 8) ∧
510 ∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W)
511 (H : SimpleGraph W) (_ : DecidableRel H.Adj),
512 IsShallowMinor H G 1 ∧
513 ((Fintype.card V : ℝ) ≤ (Fintype.card W : ℝ) ^ (6 : ℕ)) ∧
514 ((Fintype.card W : ℝ) ^ (1 + a + 2 * δ) ≤ (H.edgeFinset.card : ℝ))) := by
515 letI : DecidableRel G.Adj := Classical.decRel _
516 let n : ℝ := Fintype.card V
517 let d : ℕ := Nat.floor (n ^ (a + δ))
518 have hn_pos : 0 < n := by
519 change (0 : ℝ) < (Fintype.card V : ℝ)
520 exact_mod_cast Fintype.card_pos
521 have hn_one : 1 ≤ n := by
522 change (1 : ℝ) ≤ (Fintype.card V : ℝ)
523 exact_mod_cast (Nat.succ_le_of_lt Fintype.card_pos)
524 have hdEdgesNat : d * Fintype.card V ≤ G.edgeFinset.card := by
525 have hdEdges : (d : ℝ) * n ≤ (G.edgeFinset.card : ℝ) := by
526 calc
527 (d : ℝ) * n ≤ (n ^ (a + δ)) * n := by
528 gcongr
529 exact Nat.floor_le (by positivity : 0 ≤ n ^ (a + δ))
530 _ = n ^ (1 + a + δ) := by
531 calc
532 (n ^ (a + δ)) * n = (n ^ (a + δ)) * (n ^ (1 : ℝ)) := by rw [Real.rpow_one]
533 _ = n ^ ((a + δ) + 1) := by rw [← Real.rpow_add hn_pos]
534 _ = n ^ (1 + a + δ) := by congr 1; ring
535 _ ≤ (G.edgeFinset.card : ℝ) := hDense
536 have hdEdges' : (d * Fintype.card V : ℝ) ≤ (G.edgeFinset.card : ℝ) := by
537 simpa [n] using hdEdges
538 exact_mod_cast hdEdges'
539 rcases exists_inducedSubgraph_minDegree_sq_card G d hdEdgesNat with ⟨s, hsdeg, hsize⟩
540 let S : SimpleGraph s := G.induce s
541 have hsCardLe : Fintype.card s ≤ Fintype.card V := by
542 exact Fintype.card_le_of_embedding (Function.Embedding.subtype s)
543 have hsdegReal : (Fintype.card s : ℝ) ^ a ≤ (S.minDegree : ℝ) := by
544 calc
545 (Fintype.card s : ℝ) ^ a ≤ n ^ a := by
546 exact Real.rpow_le_rpow (by positivity : 0 ≤ (Fintype.card s : ℝ))
547 (by
548 change (Fintype.card s : ℝ) ≤ (Fintype.card V : ℝ)
549 exact_mod_cast hsCardLe) ha0.le
550 _ ≤ d := rpow_le_floor_rpow_add hn_pos hn_one ha0.le hRound
551 _ ≤ (S.minDegree : ℝ) := by
552 change (d : ℝ) ≤ ↑((G.induce s).minDegree)
553 exact_mod_cast hsdeg
554 have hMcard : M ≤ Fintype.card s := by
555 apply le_of_sq_le_sq
556 calc
557 M ^ 2 ≤ Fintype.card V := hMBound
558 _ ≤ (Fintype.card s) ^ 2 := hsize
559 have hCliqueCard : Nat.ceil (Real.exp t0) ≤ Fintype.card s := by
560 apply le_of_sq_le_sq
561 exact le_trans hCliqueBound hsize
562 have hStep := hDensify S hMcard (by
563 intro v
564 have hminle : (S.minDegree : ℝ) ≤ (S.degree v : ℝ) := by
565 exact_mod_cast S.minDegree_le_degree v
566 exact hsdegReal.trans hminle)
567 rcases hStep with ⟨q, hqLog, hqMinor⟩ | ⟨W, hWDec, hWFint, H, hHDec, hMinor, hWlo, hHedges⟩
568 · exact Or.inl <|
569 shallowMinor_trans
570 (clique_minor_of_large_card hCliqueCard hqLog hqMinor)
571 (induced_isShallowMinor_zero G s)
572 · have hs_pos : 0 < (Fintype.card s : ℝ) := by
573 have hs_nat_pos : 0 < Fintype.card s := by
574 have hceil_pos : 0 < Nat.ceil (Real.exp t0) := by
575 exact Nat.ceil_pos.mpr (Real.exp_pos t0)
576 exact lt_of_lt_of_le hceil_pos hCliqueCard
577 exact_mod_cast hs_nat_pos
578 by_cases hLarge : (5 : ℝ) / 8 ≤ a
579 · exfalso
580 exact not_boostedMinor_of_large_parameter H (show 0 < (Fintype.card W : ℝ) by
581 have hWlo_pos : 0 < (Fintype.card s : ℝ) ^ (1 - a) := Real.rpow_pos_of_pos hs_pos _
582 linarith) hLarge hHedges
583 · have hSmall : a < (5 : ℝ) / 8 := by linarith
584 refine Or.inr ⟨hSmall, W, hWDec, hWFint, H, hHDec, ?_, ?_, ?_⟩
585 · exact shallowMinor_trans hMinor (induced_isShallowMinor_zero G s)
586 · have hs_le : (Fintype.card s : ℝ) ≤ (Fintype.card W : ℝ) ^ (3 : ℕ) :=
587 card_le_pow_three_of_boost (V := s) (W := W) hs_pos ha23 hWlo
588 calc
589 (Fintype.card V : ℝ) ≤ (Fintype.card s : ℝ) ^ (2 : ℕ) := by exact_mod_cast hsize
590 _ ≤ ((Fintype.card W : ℝ) ^ (3 : ℕ)) ^ (2 : ℕ) := by gcongr
591 _ = (Fintype.card W : ℝ) ^ (6 : ℕ) := by rw [← pow_mul]
592 · have hWone : 1 ≤ (Fintype.card W : ℝ) := by
593 have hWlo_pos : 0 < (Fintype.card s : ℝ) ^ (1 - a) := Real.rpow_pos_of_pos hs_pos _
594 have hWpos : 0 < (Fintype.card W : ℝ) := lt_of_lt_of_le hWlo_pos hWlo
595 have hWnatpos : 0 < Fintype.card W := by
596 exact_mod_cast hWpos
597 exact_mod_cast (Nat.succ_le_of_lt hWnatpos)
598 have hExpLe : 1 + a + 2 * δ ≤ 1 + a + a ^ (2 : ℕ) := by linarith
599 exact le_trans (Real.rpow_le_rpow_of_exponent_le hWone hExpLe) hHedges
600
601set_option maxHeartbeats 1000000 in
602private theorem nd_subpolynomial_density_depthZero (C : GraphClass) (hC : IsNowhereDense C)
603 (ε : ℝ) (hε : 0 < ε) :
604 ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V]
605 (G : SimpleGraph V) [DecidableRel G.Adj],
606 C G →
607 N ≤ Fintype.card V →
608 (G.edgeFinset.card : ℝ) < (Fintype.card V : ℝ) ^ (1 + ε) := by
609 by_cases hε1 : 1 ≤ ε
610 · refine ⟨2, ?_⟩
611 intro V _ _ G _ hG hN
612 let n : ℝ := Fintype.card V
613 have hcard_two : 2 ≤ Fintype.card V := hN
614 have hcard_pos : 0 < Fintype.card V := by omega
615 have hn_pos : 0 < n := by
616 change (0 : ℝ) < (Fintype.card V : ℝ)
617 exact_mod_cast hcard_pos
618 have hn_one : 1 ≤ n := by
619 change (1 : ℝ) ≤ (Fintype.card V : ℝ)
620 exact_mod_cast (Nat.succ_le_of_lt hcard_pos)
621 have hEdgesQuad : (G.edgeFinset.card : ℝ) < n ^ (2 : ℝ) := by
622 have hchoose : (Fintype.card V).choose 2 < (Fintype.card V) ^ 2 := by
623 rw [Nat.choose_two_right]
624 have hdiv :
625 Fintype.card V * (Fintype.card V - 1) / 2 < Fintype.card V * (Fintype.card V - 1) := by
626 have hsub_pos : 0 < Fintype.card V - 1 := by
627 omega
628 apply Nat.div_lt_self
629 · exact Nat.mul_pos hcard_pos hsub_pos
630 · decide
631 have hmul :
632 Fintype.card V * (Fintype.card V - 1) < (Fintype.card V) ^ 2 := by
633 rw [pow_two]
634 exact Nat.mul_lt_mul_of_pos_left (by omega) hcard_pos
635 exact lt_trans hdiv hmul
636 calc
637 (G.edgeFinset.card : ℝ) ≤ ((Fintype.card V).choose 2 : ℝ) := by
638 exact_mod_cast G.card_edgeFinset_le_card_choose_two
639 _ < ((Fintype.card V) ^ 2 : ℕ) := by
640 exact_mod_cast hchoose
641 _ = n ^ (2 : ℝ) := by simp [n]
642 have hPow : n ^ (2 : ℝ) ≤ n ^ (1 + ε) := by
643 have hExp : (2 : ℝ) ≤ 1 + ε := by linarith
644 exact Real.rpow_le_rpow_of_exponent_le hn_one hExp
645 exact lt_of_lt_of_le hEdgesQuad hPow
646 · have hε_lt_one : ε < 1 := lt_of_not_ge hε1
647 let a0 : ℝ := ε / 2
648 let δ : ℝ := ε ^ (2 : ℕ) / 32
649 have ha0_pos : 0 < a0 := by
650 positivity
651 have ha0_lt_23 : a0 < (2 : ℝ) / 3 := by
652 dsimp [a0]
653 nlinarith
654 have hδ_pos : 0 < δ := by
655 positivity
656 have hδa0 : 2 * δ ≤ a0 ^ (2 : ℕ) := by
657 dsimp [a0, δ]
658 ring_nf
659 nlinarith [sq_nonneg ε]
660 have ha0δ_le_ε : a0 + δ ≤ ε := by
661 dsimp [a0, δ]
662 nlinarith
663 have ha0_lt_58 : a0 < (5 : ℝ) / 8 := by
664 dsimp [a0]
665 nlinarith
666 have hδ_lt : δ < (1 : ℝ) / 24 := by
667 dsimp [δ]
668 nlinarith
669 have hkExists : ∃ k : ℕ, (5 : ℝ) / 8 ≤ a0 + k * δ := by
670 obtain ⟨k, hk⟩ := exists_nat_ge (((5 : ℝ) / 8 - a0) / δ)
671 refine ⟨k, ?_⟩
672 have hk' : (((5 : ℝ) / 8 - a0) / δ) ≤ (k : ℝ) := by
673 exact_mod_cast hk
674 have hk'' : (5 : ℝ) / 8 - a0 ≤ (k : ℝ) * δ := (div_le_iff₀ hδ_pos).1 hk'
675 linarith
676 let k : ℕ := Nat.find hkExists
677 have hk_lower : (5 : ℝ) / 8 ≤ a0 + k * δ := Nat.find_spec hkExists
678 have hk_pos : 0 < k := by
679 refine Nat.pos_iff_ne_zero.mpr ?_
680 intro hk0
681 have : (5 : ℝ) / 8 ≤ a0 := by
682 simpa [k, hk0] using hk_lower
683 exact (not_le_of_gt ha0_lt_58) this
684 have hk_eq : (k - 1) + 1 = k := by
685 omega
686 have hk_pred_cast : ((k - 1 : ℕ) : ℝ) = (k : ℝ) - 1 := by
687 have hk_cast : ((k - 1 : ℕ) : ℝ) + 1 = (k : ℝ) := by
688 exact_mod_cast hk_eq
689 linarith
690 let a : ℕ → ℝ := fun m => a0 + ((k - m : ℕ) : ℝ) * δ
691 have ha_final_large : (5 : ℝ) / 8 ≤ a 0 := by
692 simpa [a] using hk_lower
693 have ha_final_lt : a 0 < (2 : ℝ) / 3 := by
694 have hnot : ¬ ((5 : ℝ) / 8 ≤ a0 + ((k - 1 : ℕ) : ℝ) * δ) := by
695 simpa [k] using (Nat.find_min hkExists (Nat.pred_lt (Nat.ne_of_gt hk_pos)))
696 have hnot' : ¬ ((5 : ℝ) / 8 ≤ a0 + ((k : ℝ) - 1) * δ) := by
697 simpa [hk_pred_cast] using hnot
698 have hprev : a0 + ((k : ℝ) - 1) * δ < (5 : ℝ) / 8 := by
699 linarith
700 have hshift : a 0 = a0 + ((k : ℝ) - 1) * δ + δ := by
701 calc
702 a 0 = a0 + (k : ℝ) * δ := by simp [a]
703 _ = a0 + (((k : ℝ) - 1) + 1) * δ := by ring
704 _ = a0 + ((k : ℝ) - 1) * δ + δ := by ring
705 linarith
706 have ha_ge_a0 : ∀ m : ℕ, a0 ≤ a m := by
707 intro m
708 dsimp [a]
709 have hnonneg : 0 ≤ (((k - m : ℕ) : ℝ) * δ) := by positivity
710 linarith
711 have ha_pos : ∀ m : ℕ, 0 < a m := by
712 intro m
713 exact lt_of_lt_of_le ha0_pos (ha_ge_a0 m)
714 have ha_le_final : ∀ {m : ℕ}, m ≤ k → a m ≤ a 0 := by
715 intro m hm
716 calc
717 a m = a0 + (((k - m : ℕ) : ℝ) * δ) := by simp [a]
718 _ ≤ a0 + (k : ℝ) * δ := by
719 gcongr
720 exact_mod_cast (Nat.sub_le _ _)
721 _ = a 0 := by simp [a]
722 have ha_lt_23 : ∀ {m : ℕ}, m ≤ k → a m < (2 : ℝ) / 3 := by
723 intro m hm
724 exact lt_of_le_of_lt (ha_le_final hm) ha_final_lt
725 have hδa : ∀ {m : ℕ}, m ≤ k → 2 * δ ≤ (a m) ^ (2 : ℕ) := by
726 intro m hm
727 have hsq : a0 ^ (2 : ℕ) ≤ (a m) ^ (2 : ℕ) := by
728 nlinarith [ha_ge_a0 m, ha0_pos, ha_pos m]
729 exact le_trans hδa0 hsq
730 have ha_step : ∀ {m : ℕ}, m + 1 ≤ k → a m = a (m + 1) + δ := by
731 intro m hm
732 have hnat : k - m = (k - (m + 1)) + 1 := by
733 omega
734 have hnat_cast : ((k - m : ℕ) : ℝ) = ((k - (m + 1) : ℕ) : ℝ) + 1 := by
735 exact_mod_cast hnat
736 calc
737 a m = a0 + ((k - m : ℕ) : ℝ) * δ := by simp [a]
738 _ = a0 + ((((k - (m + 1) : ℕ) : ℝ) + 1) * δ) := by rw [hnat_cast]
739 _ = a (m + 1) + δ := by
740 simp [a]
741 ring
742 let MSeq : ℕ → ℕ := fun m =>
743 if hm : m ≤ k then
744 Classical.choose (Densification.densification (a m) (ha_pos m) (ha_lt_23 hm).le)
745 else
746 1
747 have hDensifySeq :
748 ∀ {m : ℕ}, m ≤ k →
749 ∀ {W : Type} [DecidableEq W] [Fintype W]
750 (H : SimpleGraph W) [DecidableRel H.Adj],
751 MSeq m ≤ Fintype.card W →
752 (∀ v : W, (Fintype.card W : ℝ) ^ a m ≤ ↑(H.degree v)) →
753 (∃ t : ℕ, Real.log ↑(Fintype.card W) ≤ ↑t ∧
754 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) H 1) ∨
755 (∃ (U : Type) (_ : DecidableEq U) (_ : Fintype U)
756 (H' : SimpleGraph U) (_ : DecidableRel H'.Adj),
757 IsShallowMinor H' H 1 ∧
758 (Fintype.card W : ℝ) ^ (1 - a m) ≤ ↑(Fintype.card U) ∧
759 (Fintype.card U : ℝ) ^ (1 + a m + a m ^ 2) ≤ ↑(H'.edgeFinset.card)) := by
760 intro m hm W _ _ H _ hM hdeg
761 have hM' :
762 Classical.choose (Densification.densification (a m) (ha_pos m) (ha_lt_23 hm).le) ≤
763 Fintype.card W := by
764 simpa [MSeq, hm] using hM
765 exact (Classical.choose_spec
766 (Densification.densification (a m) (ha_pos m) (ha_lt_23 hm).le)) H hM' hdeg
767 obtain ⟨t, htClique⟩ := hC (iterationDepth (k + 1))
768 obtain ⟨Bround, hBround_spec⟩ : ∃ Bround : ℕ, (2 : ℝ) ^ (1 / δ) ≤ Bround := by
769 exact exists_nat_ge ((2 : ℝ) ^ (1 / δ))
770 let Bcore : ℕ :=
771 (Finset.range (k + 1)).sup fun m => (MSeq m) ^ 2
772 let B : ℕ :=
773 max (max (((Nat.ceil (Real.exp t)) ^ 2)) Bround) Bcore
774 let N : ℕ := sizeSeq B k
775 have hB_M : ∀ {m : ℕ}, m ≤ k → (MSeq m) ^ 2 ≤ B := by
776 intro m hm
777 have hm_mem : m ∈ Finset.range (k + 1) := Finset.mem_range.mpr (Nat.lt_succ_iff.mpr hm)
778 have hsup : (MSeq m) ^ 2 ≤ Bcore := by
779 simpa [Bcore] using
780 (Finset.le_sup (s := Finset.range (k + 1)) (f := fun j => (MSeq j) ^ 2) hm_mem)
781 exact le_trans hsup (le_max_right _ _)
782 have hB_clique : (Nat.ceil (Real.exp t)) ^ 2 ≤ B := by
783 exact le_trans (le_max_left _ _) (le_max_left _ _)
784 have hB_round : Bround ≤ B := by
785 exact le_trans (le_max_right _ _) (le_max_left _ _)
786 have hB_one : 1 ≤ B := by
787 have hposClique : 0 < (Nat.ceil (Real.exp t)) ^ 2 := by
788 have hceil_pos : 0 < Nat.ceil (Real.exp t) := Nat.ceil_pos.mpr (Real.exp_pos _)
789 exact pow_pos hceil_pos 2
790 exact le_trans (Nat.succ_le_of_lt hposClique) hB_clique
791 have hSizeBase : ∀ m : ℕ, B ≤ sizeSeq B m := sizeSeq_base_le hB_one
792 have hBround_pow : 2 ≤ (Bround : ℝ) ^ δ := by
793 have hround_real : (2 : ℝ) ^ (1 / δ) ≤ (Bround : ℝ) := by
794 exact_mod_cast hBround_spec
795 have htwo : ((2 : ℝ) ^ (1 / δ)) ^ δ = 2 := by
796 simpa [one_div] using
797 (Real.rpow_inv_rpow (x := (2 : ℝ)) (y := δ) (by positivity) (ne_of_gt hδ_pos))
798 calc
799 2 = ((2 : ℝ) ^ (1 / δ)) ^ δ := htwo.symm
800 _ ≤ (Bround : ℝ) ^ δ := by
801 exact Real.rpow_le_rpow
802 (by positivity : 0 ≤ (2 : ℝ) ^ (1 / δ)) hround_real hδ_pos.le
803 refine ⟨N, ?_⟩
804 intro V _ _ G _ hG hN
805 let n : ℝ := Fintype.card V
806 have hN_one : 1 ≤ N := by
807 exact le_trans hB_one (by simpa [N] using hSizeBase k)
808 have hcard_pos : 0 < Fintype.card V := lt_of_lt_of_le (by decide : 0 < 1) (le_trans hN_one hN)
809 have hn_pos : 0 < n := by
810 change (0 : ℝ) < (Fintype.card V : ℝ)
811 exact_mod_cast hcard_pos
812 have hn_one : 1 ≤ n := by
813 change (1 : ℝ) ≤ (Fintype.card V : ℝ)
814 exact_mod_cast (Nat.succ_le_of_lt hcard_pos)
815 have hCliqueImpossible :
816 ∀ m : ℕ, m ≤ k →
817 ∀ {W : Type} [DecidableEq W] [Fintype W] (H : SimpleGraph W),
818 IsShallowMinor H G (iterationDepth (k - m)) →
819 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) H 1 →
820 False := by
821 intro m hm W _ _ H hMinor hClique
822 have hComp0 :
823 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G
824 (2 * iterationDepth (k - m) * 1 + iterationDepth (k - m) + 1) :=
825 shallowMinor_trans hClique hMinor
826 have hDepthEq :
827 2 * iterationDepth (k - m) * 1 + iterationDepth (k - m) + 1 =
828 iterationDepth ((k - m) + 1) := by
829 simp [iterationDepth, two_mul]
830 omega
831 have hComp :
832 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G
833 (iterationDepth ((k - m) + 1)) := hDepthEq ▸ hComp0
834 have hComp' :
835 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G
836 (iterationDepth (k + 1)) := by
837 apply isShallowMinor_mono hComp
838 exact iterationDepth_monotone (by omega)
839 exact htClique G hG hComp'
840 set_option maxHeartbeats 1000000 in
841 have hIter :
842 ∀ m : ℕ, m ≤ k →
843 ∀ {W : Type} [DecidableEq W] [Fintype W] (H : SimpleGraph W),
844 IsShallowMinor H G (iterationDepth (k - m)) →
845 sizeSeq B m ≤ Fintype.card W →
846 ((Fintype.card W : ℝ) ^ (1 + a m + δ) ≤ (H.edgeFinset.card : ℝ)) →
847 False := by
848 intro m
849 induction m with
850 | zero =>
851 intro hm W _ _ H hMinor hCard hEdge
852 have hCardBase : B ≤ Fintype.card W := by
853 simpa [sizeSeq] using hCard
854 have hcard_pos_nat : 0 < Fintype.card W := lt_of_lt_of_le (by decide : 0 < 1)
855 (le_trans hB_one hCardBase)
856 letI : Nonempty W := Fintype.card_pos_iff.mp hcard_pos_nat
857 have hRound : 2 ≤ (Fintype.card W : ℝ) ^ δ := by
858 have hBround_card : Bround ≤ Fintype.card W := le_trans hB_round hCardBase
859 calc
860 2 ≤ (Bround : ℝ) ^ δ := hBround_pow
861 _ ≤ (Fintype.card W : ℝ) ^ δ := by gcongr
862 have hDensifyNow :
863 ∀ {U : Type} [DecidableEq U] [Fintype U]
864 (H' : SimpleGraph U) [DecidableRel H'.Adj],
865 MSeq 0 ≤ Fintype.card U →
866 (∀ v : U, (Fintype.card U : ℝ) ^ a 0 ≤ ↑(H'.degree v)) →
867 (∃ t : ℕ, Real.log ↑(Fintype.card U) ≤ ↑t ∧
868 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) H' 1) ∨
869 (∃ (U' : Type) (_ : DecidableEq U') (_ : Fintype U')
870 (H'' : SimpleGraph U') (_ : DecidableRel H''.Adj),
871 IsShallowMinor H'' H' 1 ∧
872 (Fintype.card U : ℝ) ^ (1 - a 0) ≤ ↑(Fintype.card U') ∧
873 (Fintype.card U' : ℝ) ^ (1 + a 0 + a 0 ^ 2) ≤ ↑(H''.edgeFinset.card)) := by
874 intro U _ _ H' _ hM hdeg
875 exact hDensifySeq (m := 0) hm H' hM hdeg
876 have hStep := step_or_clique H (MSeq 0)
877 (ha_pos 0) (ha_lt_23 hm).le hδ_pos (hδa hm)
878 (le_trans (hB_M hm) hCardBase) (le_trans hB_clique hCardBase) hRound hEdge
879 (hDensify := hDensifyNow)
880 rcases hStep with hClique | hBoost
881 · exact hCliqueImpossible 0 hm H hMinor hClique
882 · rcases hBoost with ⟨hSmall, W', hWDec, hWFint, H', hHDec, hMinorStep, hCardStep, hEdgeStep⟩
883 exact (not_lt_of_ge ha_final_large) (by simpa [a] using hSmall)
884 | succ m ih =>
885 intro hm W _ _ H hMinor hCard hEdge
886 have hm' : m ≤ k := Nat.le_of_succ_le hm
887 have hCardBase : B ≤ Fintype.card W := by
888 exact le_trans (hSizeBase (m + 1)) hCard
889 have hcard_pos_nat : 0 < Fintype.card W := lt_of_lt_of_le (by decide : 0 < 1)
890 (le_trans hB_one hCardBase)
891 letI : Nonempty W := Fintype.card_pos_iff.mp hcard_pos_nat
892 have hRound : 2 ≤ (Fintype.card W : ℝ) ^ δ := by
893 have hBround_card : Bround ≤ Fintype.card W := le_trans hB_round hCardBase
894 calc
895 2 ≤ (Bround : ℝ) ^ δ := hBround_pow
896 _ ≤ (Fintype.card W : ℝ) ^ δ := by gcongr
897 have hDensifyNow :
898 ∀ {U : Type} [DecidableEq U] [Fintype U]
899 (H' : SimpleGraph U) [DecidableRel H'.Adj],
900 MSeq (m + 1) ≤ Fintype.card U →
901 (∀ v : U, (Fintype.card U : ℝ) ^ a (m + 1) ≤ ↑(H'.degree v)) →
902 (∃ t : ℕ, Real.log ↑(Fintype.card U) ≤ ↑t ∧
903 IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) H' 1) ∨
904 (∃ (U' : Type) (_ : DecidableEq U') (_ : Fintype U')
905 (H'' : SimpleGraph U') (_ : DecidableRel H''.Adj),
906 IsShallowMinor H'' H' 1 ∧
907 (Fintype.card U : ℝ) ^ (1 - a (m + 1)) ≤ ↑(Fintype.card U') ∧
908 (Fintype.card U' : ℝ) ^ (1 + a (m + 1) + a (m + 1) ^ 2) ≤
909 ↑(H''.edgeFinset.card)) := by
910 intro U _ _ H' _ hM hdeg
911 exact hDensifySeq (m := m + 1) hm H' hM hdeg
912 have hStep := step_or_clique H (MSeq (m + 1))
913 (ha_pos (m + 1)) (ha_lt_23 hm).le hδ_pos (hδa hm)
914 (le_trans (hB_M hm) hCardBase) (le_trans hB_clique hCardBase) hRound hEdge
915 (hDensify := hDensifyNow)
916 rcases hStep with hClique | hBoost
917 · exact hCliqueImpossible (m + 1) hm H hMinor hClique
918 · rcases hBoost with ⟨hSmall, W', hWDec, hWFint, H', hHDec, hMinorStep, hCardStep, hEdgeStep⟩
919 have hCardStepNat : Fintype.card W ≤ (Fintype.card W') ^ 6 := by
920 exact_mod_cast hCardStep
921 have hCard' : sizeSeq B m ≤ Fintype.card W' := by
922 have hPow : (sizeSeq B m) ^ 6 ≤ (Fintype.card W') ^ 6 := by
923 calc
924 (sizeSeq B m) ^ 6 = sizeSeq B (m + 1) := by simp [sizeSeq]
925 _ ≤ Fintype.card W := hCard
926 _ ≤ (Fintype.card W') ^ 6 := hCardStepNat
927 exact le_of_pow_six_le_pow_six hPow
928 have hMinor' : IsShallowMinor H' G (iterationDepth (k - m)) := by
929 have hkm : k - m = (k - (m + 1)) + 1 := by
930 omega
931 have hComp0 :
932 IsShallowMinor H' G
933 (2 * iterationDepth (k - (m + 1)) * 1 + iterationDepth (k - (m + 1)) + 1) :=
934 shallowMinor_trans hMinorStep hMinor
935 have hDepthEq :
936 2 * iterationDepth (k - (m + 1)) * 1 + iterationDepth (k - (m + 1)) + 1 =
937 iterationDepth (k - m) := by
938 rw [hkm]
939 simp [iterationDepth, two_mul]
940 omega
941 exact hDepthEq ▸ hComp0
942 have hEdge' :
943 (Fintype.card W' : ℝ) ^ (1 + a m + δ) ≤ (H'.edgeFinset.card : ℝ) := by
944 have haeq : a m = a (m + 1) + δ := ha_step hm
945 calc
946 (Fintype.card W' : ℝ) ^ (1 + a m + δ)
947 = (Fintype.card W' : ℝ) ^ (1 + a (m + 1) + 2 * δ) := by
948 rw [haeq]
949 congr 1
950 ring
951 _ ≤ (H'.edgeFinset.card : ℝ) := hEdgeStep
952 exact ih hm' H' hMinor' hCard' (by convert hEdge')
953 by_contra hDense
954 have hInitDense : n ^ (1 + a k + δ) ≤ (G.edgeFinset.card : ℝ) := by
955 have hExp : 1 + a k + δ ≤ 1 + ε := by
956 simpa [a, add_assoc] using ha0δ_le_ε
957 exact le_trans (Real.rpow_le_rpow_of_exponent_le hn_one hExp) (not_lt.mp hDense)
958 have hMinor0 : IsShallowMinor G G (iterationDepth (k - k)) := by
959 simpa [iterationDepth] using
960 (isShallowMinor_zero_of_embedding (SimpleGraph.Embedding.refl (G := G)))
961 exact hIter k le_rfl G hMinor0 hN (by convert hInitDense)
962
963/-- Theorem 3.1/ch1: Nowhere dense classes have subpolynomial edge density. -/
964theorem nd_subpolynomial_density (C : GraphClass) (hC : IsNowhereDense C)
965 (r : ℕ) (ε : ℝ) (hε : 0 < ε) :
966 ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V]
967 (H : SimpleGraph V) [DecidableRel H.Adj],
968 (∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (G : SimpleGraph W),
969 C G ∧ IsShallowMinor H G r) →
970 N ≤ Fintype.card V →
971 (H.edgeFinset.card : ℝ) < (Fintype.card V : ℝ) ^ (1 + ε) := by
972 obtain ⟨N, hN⟩ := nd_subpolynomial_density_depthZero
973 (ShallowReduct C r) (nowhereDense_shallowReduct C r hC) ε hε
974 refine ⟨N, ?_⟩
975 intro V _ _ H _ hHr hCard
976 exact hN H hHr hCard
977
978end
979
980end Catalog.Sparsity.NDSubpolynomialDensity
981