Lax12.NowhereDenseDensity

Nowhere dense classes have subpolynomial shallow-minor density

concepts/Lax12/NowhereDenseDensity.lean · lax-12

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax12.NowhereDenseDensity

⊢Lax12Proofs.NowhereDenseDensity.hasSubpolynomialDensity_of_nowhereDense

Theorem

Every nowhere dense graph class has subpolynomial density: for every depth r and every ε > 0 there is a constant c such that every depth-r minor of a member, on m vertices, has at most c · m^(1+ε) edges. Together with the reverse implication — which is immediate, since a large clique as a shallow minor forces quadratically many edges — this is the density characterization of nowhere denseness.

The source lecture notes state the implication as Theorem 3.1 of Chapter 1 (2019/20 edition), in the threshold form "G has fewer than n^(1+ε) edges once n ≥ N(r, ε)", and credit the proof they present to Zdeněk Dvořák.

Lean source view on GitHub

1	import Lax12.NowhereDenseClasses
2	import Lax12.ShallowMinorDensity
3
4	/-!
5	---
6	title: Nowhere dense classes have subpolynomial shallow-minor density
7	type: theorem
8	---
9	Every nowhere dense graph class has subpolynomial density: for every
10	depth r and every ε > 0 there is a constant c such that every
11	depth-r minor of a member, on m vertices, has at most
12	c · m^(1+ε) edges. Together with the reverse implication — which is
13	immediate, since a large clique as a shallow minor forces quadratically
14	many edges — this is the density characterization of nowhere denseness.
15
16	The source lecture notes state the implication as Theorem 3.1 of
17	Chapter 1 (2019/20 edition), in the threshold form "G has fewer than
18	n^(1+ε) edges once n ≥ N(r, ε)", and credit the proof they
19	present to Zdeněk Dvořák.
20
21	# Formalization notes
22
23	Both hypothesis and conclusion are the shared predicates of the imported
24	definition concepts. The bound is uniform over all members of the class
25	and all their depth-r minors, with the constant depending only on the
26	depth and on ε; that uniformity is what the coloring-number chain
27	downstream consumes. The multiplicative form used here is the one the
28	notes themselves record as equivalent to their threshold form,
29	immediately after the theorem: a graph on m vertices has at most m²
30	edges, so the finitely many sizes below the threshold are absorbed into
31	the constant. Only the stated direction is claimed: the easy converse is
32	a separate statement and is not conjoined here.
33	-/
34
35	namespace Lax12.NowhereDenseDensity
36
37	open Lax12.GraphClasses Lax12.NowhereDenseClasses Lax12.ShallowMinorDensity
38
39	/-- Nowhere dense graph classes have subpolynomial shallow-minor
40	density. -/
41	axiom hasSubpolynomialDensity_of_nowhereDense
42	(C : GraphClass) (h : NowhereDense C) :
43	HasSubpolynomialDensity C
44
45	end Lax12.NowhereDenseDensity
46

Show Proof

Formalization notes

Both hypothesis and conclusion are the shared predicates of the imported definition concepts. The bound is uniform over all members of the class and all their depth-r minors, with the constant depending only on the depth and on ε; that uniformity is what the coloring-number chain downstream consumes. The multiplicative form used here is the one the notes themselves record as equivalent to their threshold form, immediately after the theorem: a graph on m vertices has at most m² edges, so the finitely many sizes below the threshold are absorbed into the constant. Only the stated direction is claimed: the easy converse is a separate statement and is not conjoined here.

Builds on

Used by

none

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive