Catalog/Sparsity/NDSubpolynomialDensity/Contract.lean
| 1 | import Catalog.Sparsity.Preliminaries.Contract |
| 2 | import Catalog.Sparsity.ShallowMinor.Contract |
| 3 | import Catalog.Sparsity.NowhereDense.Contract |
| 4 | import Mathlib.Combinatorics.SimpleGraph.Finite |
| 5 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 6 | |
| 7 | open Catalog.Sparsity.ShallowMinor |
| 8 | open Catalog.Sparsity.NowhereDense |
| 9 | open Catalog.Sparsity.Preliminaries |
| 10 | |
| 11 | namespace Catalog.Sparsity.NDSubpolynomialDensity |
| 12 | |
| 13 | /-- Theorem 3.1/ch1: Nowhere dense classes have subpolynomial edge density. |
| 14 | |
| 15 | For every ND class C, r ∈ ℕ, ε > 0, every graph H that is a depth-r |
| 16 | shallow minor of some graph in C and has n ≥ N vertices has fewer than |
| 17 | n^{1+ε} edges. -/ |
| 18 | axiom nd_subpolynomial_density (C : GraphClass) (hC : IsNowhereDense C) |
| 19 | (r : ℕ) (ε : ℝ) (hε : 0 < ε) : |
| 20 | ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 21 | (H : SimpleGraph V) [DecidableRel H.Adj], |
| 22 | (∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) (G : SimpleGraph W), |
| 23 | C G ∧ IsShallowMinor H G r) → |
| 24 | N ≤ Fintype.card V → |
| 25 | (H.edgeFinset.card : ℝ) < (Fintype.card V : ℝ) ^ (1 + ε) |
| 26 | |
| 27 | end Catalog.Sparsity.NDSubpolynomialDensity |
| 28 |