Catalog/Sparsity/Densification/Contract.lean
| 1 | import Catalog.Sparsity.ShallowMinor.Contract |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Finite |
| 3 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 4 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 5 | |
| 6 | open Catalog.Sparsity.ShallowMinor |
| 7 | |
| 8 | namespace Catalog.Sparsity.Densification |
| 9 | |
| 10 | /-- Lemma 3.4/ch1: Densification lemma. |
| 11 | |
| 12 | For every ε ∈ (0, 2/3], there exists a threshold M such that every graph G |
| 13 | on n ≥ M vertices with minimum degree ≥ n^ε either: |
| 14 | (1) contains K_t as a depth-1 minor for some t ≥ log n, or |
| 15 | (2) has a depth-1 minor G' with n' ≥ n^{1-ε} vertices and |
| 16 | ≥ (n')^{1+ε+ε²} edges. -/ |
| 17 | axiom densification (ε : ℝ) (hε_pos : 0 < ε) (hε_le : ε ≤ 2 / 3) : |
| 18 | ∃ M : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] |
| 19 | (G : SimpleGraph V) [DecidableRel G.Adj], |
| 20 | M ≤ Fintype.card V → |
| 21 | (∀ v : V, (Fintype.card V : ℝ) ^ ε ≤ ↑(G.degree v)) → |
| 22 | (∃ t : ℕ, Real.log ↑(Fintype.card V) ≤ ↑t ∧ |
| 23 | IsShallowMinor (SimpleGraph.completeGraph (Fin (t + 1))) G 1) ∨ |
| 24 | (∃ (W : Type) (_ : DecidableEq W) (_ : Fintype W) |
| 25 | (G' : SimpleGraph W) (_ : DecidableRel G'.Adj), |
| 26 | IsShallowMinor G' G 1 ∧ |
| 27 | (Fintype.card V : ℝ) ^ (1 - ε) ≤ ↑(Fintype.card W) ∧ |
| 28 | (Fintype.card W : ℝ) ^ (1 + ε + ε ^ 2) ≤ ↑(G'.edgeFinset.card)) |
| 29 | |
| 30 | end Catalog.Sparsity.Densification |
| 31 |