Theorem 20.6: the VC dimension of H_{V,E,sign} is O(|E| log |E|); explicitly VCdim ≤ 2|E| log₂(16|E|)

Proved

UnderstandingML.vcDim_sign_net

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

neural-networkssample-complexityvc-dimension

Theorem 20.6. The VC dimension of $H_{V,E,\operatorname{sign}}$ is $O(|E|\log(|E|))$ .

Formally, with explicit constants: for a layered graph of depth $\ge 1$ with a single output neuron, every $m \le \operatorname{VCdim}(H_{V,E,\operatorname{sign}})$ satisfies $m \le 2|E|\log_2(16|E|)$ (from $2^m \le (em)^{|E|}$ for a shattered set of size $m$ ); in particular the VC dimension is finite.

Preamble

import Definitions.Def_UnderstandingML_NeuralNetworks

open MeasureTheory

Formal statement

namespace UnderstandingML

/-- **Theorem 20.6** (p. 274). The VC dimension of `H_{V,E,sign}` is `O(|E| log(|E|))`.
Explicitly, with the constants the proof gives (`2^m ≤ (em)^{|E|}` for a shattered set of size
`m`): `VCdim(H_{V,E,sign}) ≤ 2|E| log₂(16|E|)`, for a network of depth at least `1` with a
single output neuron. -/
theorem vcDim_sign_net (n : ℕ) (G : LayeredGraph) (hd : 1 ≤ G.depth) (m : ℕ)
    (hm : (m : ℕ∞) ≤ vcDim (signNetClass n G)) :
    (m : ℝ) ≤ 2 * G.numEdges * Real.logb 2 (16 * G.numEdges) := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §20.4 pp. 274-275, Theorem 20.6 with its proof

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph