A.2 Combinatorial dimensions

Listing A.3: Shattering and VC dimension (Complexity/VCDimension.lean)

def Shatters (X : Type u) (C : ConceptClass X Bool) (S : Finset X) : Prop :=
  forall f : S -> Bool, exists c (*@$\in$@*) C, forall x : S, c (x : X) = f x

noncomputable def VCDim (X : Type u) (C : ConceptClass X Bool) : WithTop N :=
  iSup (S : Finset X) (_ : Shatters X C S), (S.card : WithTop N)

Listing A.4: Littlestone dimension (Complexity/GameInfra.lean)

noncomputable def LittlestoneDim (X : Type) (C : ConceptClass X Bool) :
    WithBot (WithTop N) :=
  iSup (n : N) (_ : exists T : LTree X n, T.isShattered C),
    ((n : WithTop N) : WithBot (WithTop N))