Finite VC dimension

HasFiniteVCDimdef

A class has finite VC dimension when some n bounds the size of every set it Shatters. By the fundamental theorem of statistical learning this is equivalent to being PAC learnable in the binary agnostic setting.

def HasFiniteVCDim {α : Type*} (C : ConceptClass α Bool) : Prop :=
  ∃ n : ℕ, ∀ W : Finset α, Shatters C (W : Set α) → W.card ≤ n

Builds on

Shattering

Used by

Problem CX-001 — the fundamental theorem of statistical learning
Problem CX-003 — the sample complexity of PAC learning

From Mathlib

Data.Finset.Card

import Conjectura.Defs.ComputerScience.Learning.HasFiniteVCDim · 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