Catalog.Sparsity.Densification
Lemma
Let \(\preccurlyeq_d\) be as in Definition ShallowMinor.
For every \(\varepsilon \in (0, \frac{2}{3}]\) there exists \(M(\varepsilon) \in \mathbb{N}\), with \(M(\cdot)\) non-increasing, such that: if \(G\) is a graph on \(n \geq M(\varepsilon)\) vertices with minimum degree at least \(n^\varepsilon\), then either
- \(G\) contains \(K_t\) as a depth-\(1\) minor for some \(t \geq \log n\), or
- there is a depth-\(1\) minor \(G'\) of \(G\) with \(n' \geq n^{1-\varepsilon}\) vertices and at least \((n')^{1 + \varepsilon + \varepsilon^2}\) edges.
Review notes
The proof uses a probabilistic argument (Chernoff’s bound) to find a random subset \(A\) with good properties, then a greedy contraction process. The key output is that either a large clique minor is found, or edge density is amplified from \(n^\varepsilon\) (minimum degree) to \((n')^{\varepsilon + \varepsilon^2}\) in a depth-1 minor \(G'\). The exponent increase from \(\varepsilon\) to \(\varepsilon + \varepsilon^2\) is what drives the iteration in the proof of Theorem 3.1.
Lean encoding.
- Minimum degree is encoded pointwise:
\(\forall v,\; n^\varepsilon \leq \texttt{G.degree}\;v\),
comparing \(\mathbb{R}\)-valued
rpowagainst a cast of the natural-number degree. - \(\log n\) uses
Real.log(natural logarithm). The source does not specify the base; the constant \(M\) absorbs any base choice. - The non-increasing property of \(M(\varepsilon)\) is not encoded; it is not needed downstream.
- The existential over \(G'\) quantifies over a new vertex type \(W\) with
all necessary instances (
DecidableEq,Fintype,DecidableRel).
Catalog/Sparsity/Densification/Contract.lean (full)
| 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 |