Edge density of shallow minors
Lax199508.ShallowMinorDensity · concepts/Lax199508/ShallowMinorDensity.lean · lax-199508
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
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.
Concept map
Lean source view on GitHub
| 1 | import Lax199508.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 Lax199508.ShallowMinorDensity |
| 48 | |
| 49 | open Lax199508.GraphClasses Lax199508.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 Lax199508.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 : 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 () of , which needs no decidability instance and is the exact count on the finite carriers used here. counts edges rather than twice the edges, matching the usual form (the greatest reduced average density is then at most ).
No numeric density parameter is introduced. Every statement of this submission either supplies a concrete bound or concludes the class-level predicate, so a -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.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments