vcDim — Mathlib

English

The VC-dimension of a set family is the size of the largest shattered set.

Русский

VC-размерность семейства множеств равна максимальному размеру множества, которое оно шаттерит.

LaTeX

$$$\\mathrm{vcDim}(\\mathcal{A}) = \\mathcal{A}.shatterer.\\sup \\mathrm{card}$$$

Lean4

/-- The Vapnik-Chervonenkis dimension of a set family is the maximal size of a set it shatters. -/
def vcDim (𝒜 : Finset (Finset α)) : ℕ :=
  𝒜.shatterer.sup card

Похожие утверждения