VC dimension

vcDimdef

The Vapnik–Chervonenkis dimension of a binary concept class is the largest size of a set it Shatters. It is the combinatorial quantity that controls how much data is needed to learn the class.

noncomputable def vcDim {α : Type*} (C : ConceptClass α Bool) : ENat :=
  ⨆ W ∈ {W : Finset α | Shatters C (W : Set α)}, (W.card : ENat)

Builds on

Shattering

Used by

Problem CX-003 — the sample complexity of PAC learning

From Mathlib

Data.Finset.Card
Data.ENat.Lattice

import Conjectura.Defs.ComputerScience.Learning.VCDimension · maintainer — open · raw source

Adapted for Conjectura from cslib, split into one concept per module. Released by its authors under Apache 2.0.

Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger

Full credits