Lax12.ShallowMinorDensity

Edge density of shallow minors

concepts/Lax12/ShallowMinorDensity.lean · lax-12

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A graph G has depth-r density at most d if every depth-r minor H of G has at most d · |V(H)| edges — the standard "grad" bound on how dense the shallow minors of a sparse graph can be. A graph class has subpolynomial density if for every depth r and every ε > 0 there is a constant c such that every depth-r minor H of a member, on m vertices, has at most c · m^(1+ε) edges: shallow-minor edge counts m^(1+o(1)).

Definition 2.4 of Chapter 1 of the source lecture notes (2019/20 edition) defines the grad ∇r(G) as the supremum of |E(H)|/|V(H)| over the depth-r minors H of G, so the per-graph predicate here says ∇r(G) ≤ d.

Lean source view on GitHub

1	import Lax12.NowhereDenseClasses
2	import Mathlib.Data.Set.Card
3	import Mathlib.Analysis.SpecialFunctions.Pow.Real
4
5	/-!
6	---
7	title: Edge density of shallow minors
8	type: definition
9	---
10	A graph G has depth-r density at most d if every depth-r minor
11	H of G has at most d · \|V(H)\| edges — the standard "grad" bound on
12	how dense the shallow minors of a sparse graph can be. A graph class has
13	subpolynomial density if for every depth r and every ε > 0 there is a
14	constant c such that every depth-r minor H of a member, on m
15	vertices, has at most c · m^(1+ε) edges: shallow-minor edge counts
16	m^(1+o(1)).
17
18	Definition 2.4 of Chapter 1 of the source lecture notes (2019/20
19	edition) defines the grad ∇_r(G) as the supremum of \|E(H)\|/\|V(H)\|
20	over the depth-r minors H of G, so the per-graph predicate here
21	says ∇_r(G) ≤ d.
22
23	# Formalization notes
24
25	Both predicates are stated over the shallow-minor relation of the
26	nowhere dense concept, so one notion of depth-r minor serves the whole
27	submission. Minors range over the canonical carriers `Fin m`: every
28	finite graph is isomorphic to one of those and the shallow-minor
29	relation is invariant under isomorphism, so nothing is lost.
30
31	Edges are counted as the natural cardinality (`Set.ncard`) of
32	`edgeSet`, which needs no decidability instance and is the exact count
33	on the finite carriers used here. `HasDensityAtMost` counts edges rather
34	than twice the edges, matching the usual `\|E(H)\| ≤ d · \|V(H)\|` form (the
35	greatest reduced average density is then at most `2 · d`).
36
37	No numeric density parameter is introduced. Every statement of this
38	submission either supplies a concrete bound `d` or concludes the
39	class-level predicate, so a `sInf`-defined grad would be review surface
40	that no claim consumes. The class-level bound carries a multiplicative
41	constant instead of the size threshold used in the literature proof; the
42	two agree because a graph on m vertices has at most m² edges, and
43	the constant form matches the subpolynomial bound of the coloring-number
44	concept.
45	-/
46
47	namespace Lax12.ShallowMinorDensity
48
49	open Lax12.GraphClasses Lax12.NowhereDenseClasses
50
51	/-- Every depth-`r` minor of `G`, on `m` vertices, has at most `d · m`
52	edges. -/
53	def HasDensityAtMost {n : ℕ} (G : SimpleGraph (Fin n)) (r d : ℕ) : Prop :=
54	∀ (m : ℕ) (H : SimpleGraph (Fin m)), HasShallowMinor G r H →
55	H.edgeSet.ncard ≤ d * m
56
57	/-- Every depth-`r` minor of every member of the class, on `m` vertices,
58	has at most `c · m^(1+ε)` edges, where `c` depends only on the depth `r`
59	and on `ε > 0`: shallow-minor edge counts `m^(1+o(1))`. -/
60	def HasSubpolynomialDensity (C : GraphClass) : Prop :=
61	∀ (r : ℕ) (ε : ℝ), 0 < ε → ∃ c : ℝ,
62	∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G →
63	∀ (m : ℕ) (H : SimpleGraph (Fin m)), HasShallowMinor G r H →
64	(H.edgeSet.ncard : ℝ) ≤ c * (m : ℝ) ^ (1 + ε)
65
66	end Lax12.ShallowMinorDensity
67

Formalization notes

Both predicates are stated over the shallow-minor relation of the nowhere dense concept, so one notion of depth-r minor serves the whole submission. Minors range over the canonical carriers $Fin m$ : every finite graph is isomorphic to one of those and the shallow-minor relation is invariant under isomorphism, so nothing is lost.

Edges are counted as the natural cardinality ( $Set.ncard$ ) of $edgeSet$ , which needs no decidability instance and is the exact count on the finite carriers used here. $HasDensityAtMost$ counts edges rather than twice the edges, matching the usual $|E(H)| ≤ d · |V(H)|$ form (the greatest reduced average density is then at most $2 · d$ ).

No numeric density parameter is introduced. Every statement of this submission either supplies a concrete bound $d$ or concludes the class-level predicate, so a $sInf$ -defined grad would be review surface that no claim consumes. The class-level bound carries a multiplicative constant instead of the size threshold used in the literature proof; the two agree because a graph on m vertices has at most m² edges, and the constant form matches the subpolynomial bound of the coloring-number concept.

Builds on

Lax12.NowhereDenseClasses

Used by

Lax12.NowhereDenseDensity

From Mathlib

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

Edge density of shallow minors

Flags

Flag this concept