VC dimension

Conjectura.Defs.ComputerScience.Learning.VCDimension

/-
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/
import Conjectura.Defs.ComputerScience.Learning.Shatters
import Mathlib.Data.Finset.Card
import Mathlib.Data.ENat.Lattice

/-! # VC dimension

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Learning

/-- 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)

end Conjectura.Learning