Lax5.AlmostLinearNC
Monadically dependent classes have almost linear neighborhood complexity
concepts/Lax5/AlmostLinearNC.lean · Lax5
Theorem
Every monadically dependent graph class has almost linear neighborhood complexity: for every ε > 0 there is a constant c such that every member G and every nonempty vertex subset A satisfy |{N(v) ∩ A : v ∈ V(G)}| ≤ c · |A|^(1+ε).
This is Theorem 2 of Dreier, Mählmann, McCarty, Pilipczuk, Toruńczyk, Neighborhood Complexity and Radius-1 Merge-Width in Monadically Dependent Graph Classes (2026).
Lean source view on GitHub
| 1 | import Lax5.MonadicDependence |
| 2 | import Lax5.NeighborhoodComplexity |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Monadically dependent classes have almost linear neighborhood complexity |
| 7 | type: theorem |
| 8 | --- |
| 9 | Every monadically dependent graph class has almost linear neighborhood |
| 10 | complexity: for every ε > 0 there is a constant *c* such that every |
| 11 | member *G* and every nonempty vertex subset *A* satisfy |
| 12 | |{N(v) ∩ A : v ∈ V(G)}| ≤ *c* · |A|^(1+ε). |
| 13 | |
| 14 | This is Theorem 2 of Dreier, Mählmann, McCarty, Pilipczuk, Toruńczyk, |
| 15 | *Neighborhood Complexity and Radius-1 Merge-Width in Monadically |
| 16 | Dependent Graph Classes* (2026). |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | The hypothesis is the transduction-based definition of monadic |
| 21 | dependence; the conclusion is the shared predicate `HasAlmostLinearNC` |
| 22 | of the neighborhood complexity concept, so this statement and the |
| 23 | nowhere dense counting statement read uniformly. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax5.AlmostLinearNC |
| 27 | |
| 28 | open Lax5.GraphClasses Lax5.MonadicDependence Lax5.NeighborhoodComplexity |
| 29 | |
| 30 | /-- Monadically dependent graph classes have almost linear neighborhood |
| 31 | complexity. -/ |
| 32 | axiom hasAlmostLinearNC_of_monadicallyDependent |
| 33 | (C : GraphClass) (h : MonadicallyDependent C) : |
| 34 | HasAlmostLinearNC C |
| 35 | |
| 36 | end Lax5.AlmostLinearNC |
| 37 |
Formalization notes
The hypothesis is the transduction-based definition of monadic
dependence; the conclusion is the shared predicate HasAlmostLinearNC
of the neighborhood complexity concept, so this statement and the
nowhere dense counting statement read uniformly.
Imported by
none
Mathlib imports
none