Formalizing Structural Graph Theory in Lean 4

Matoušek Theorem 5.12: the \(\varepsilon\)-net theorem.

The constant \(C\) is quantified before the type \(\alpha\), ensuring it depends only on the VC-dimension bound \(d\).

The source states this for a general probability measure \(\mu\). We use the uniform distribution on a finite type. The general measure case reduces to this by padding \(X\) with dummy points (see proof sketch below), so no generality is lost at the theorem level.

The Lean contract now makes the nonemptiness of the ground type explicit via [Nonempty α]. This is not extra mathematical content: a probability measure already forces the underlying space to be nonempty in the source setting. In the finite-uniform encoding, omitting this assumption makes the statement false on the empty type. Concretely, for \(\mathcal{A} = \{\emptyset\}\) on \(\alpha = \emptyset\), the current predicate Catalog.VC.EpsilonNet.IsEpsilonNet treats \(\emptyset\) as heavy because both sides of the density test are zero, but no finite set can intersect it nontrivially.

Proof outline. Pad \(X\) with dummy points to \(X'\) of size \(2^k\). By Catalog.VC.EpsilonApproximationBound: obtain a \(\frac{1}{4r}\)-approximation \(Y \subseteq X'\) of size \(O(r^2 \log r)\). Apply Catalog.VC.EasyEpsilonNetLemma to \((Y, \mathcal{S}|_Y)\): yields a \(\frac{1}{2r}\)-net \(N\) of size \(O(r \ln \pi(|Y|)) = O(r \ln r)\). Since \(Y\) is a \(\frac{1}{4r}\)-approximation, \(N\) is a \(\frac{1}{r}\)-net for \(X\).