VC dimension of a finite Bool-valued function family #
Every finite family of Bool-valued functions A : Finset (α → Bool)
determines a Finset family of accepting sets, one per function. The VC
dimension of the function family is then defined as the Finset.vcDim
of its accepting-set image. This is the entry point from function-class
view to Mathlib's combinatorial VC machinery.
def
Finset.boolFamilyToFinsetFamily
{α : Type u_1}
[Fintype α]
[DecidableEq α]
(A : Finset (α → Bool))
:
Accepting-set image: map each Bool-valued function to its accepting set
{h | f h = true}.
Equations
- A.boolFamilyToFinsetFamily = Finset.image (fun (f : α → Bool) => {h : α | f h = true}) A
Instances For
noncomputable def
Finset.boolVCDim
{α : Type u_1}
[Fintype α]
[DecidableEq α]
(A : Finset (α → Bool))
:
VC dimension of a finite Bool-valued family, computed via the accepting-set
image and Mathlib's Finset.vcDim.