Formalizing Structural Graph Theory in Lean 4

Matoušek Lemma 5.11: the “easy” \(\varepsilon\)-net bound.

The statement uses Real.log (natural logarithm) to match the source’s \(\ln |\mathcal{S}|\). The Lean contract uses \(|N| \le r \ln |\mathcal{A}| + 1\), where \(|\mathcal{A}|\) is the number of sets in the family.

The source states the cleaner inequality \(|N| \le r \ln |\mathcal{S}|\), but its proof immediately chooses an integer sample size \(s = \lceil r \ln |\mathcal{S}| \rceil\). In Lean, the net is a finite set, so the honest conclusion from that argument is \(|N| \le s \le r \ln |\mathcal{A}| + 1\). The stronger contract without the additive \(1\) is false on small finite examples; for instance, on a two-point ground set with family \(\{\{x\}, \{y\}\}\) and \(r = 2\), every \(\frac{1}{2}\)-net has size \(2 > 2 \ln 2\).

The hypothesis \(|\mathcal{A}| \ge 2\) is added because \(r \ln 1 = 0\) would force the net to be empty, which fails when the single set is heavy. The source omits this edge case. Downstream usage (Theorem 5.12) always applies this lemma to families with \(|\mathcal{A}| \ge 2\).

The proof is a probabilistic (union bound) argument: sample \(\lceil r \ln |\mathcal{A}| \rceil\) points independently from the uniform distribution, and show via \((1 - 1/r)^s < e^{-s/r}\) that some sample hits every heavy set.

The bound depends on \(|\mathcal{A}|\) (number of sets), not on the VC-dimension. The VC-dimension enters only in Catalog.VC.EpsilonNetTheorem, which improves the bound to \(O(r \ln r)\).