Finite VC dimension

Conjectura.Defs.ComputerScience.Learning.HasFiniteVCDim

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

/-! # Finite 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

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

end Conjectura.Learning