Skip to content

A Formalization of the Sauer-Shelah Lemma using Isabelle/HOL

Notifications You must be signed in to change notification settings

ata-keskin/sauer-shelah-lemma

Repository files navigation

Abstract

The Sauer-Shelah Lemma is a fundamental result in extremal set theory and combinatorics. It guarantees the existence of a set $T$ of size $k$ that is shattered by a family of sets $\mathcal{F}$, if the cardinality of the family is greater than some bound dependent on $k$. A set $T$ is said to be shattered by a family $\mathcal{F}$ if every subset of $T$ can be obtained as an intersection of $T$ with some set $S \in \mathcal{F}$.

The Sauer-Shelah Lemma has found use in diverse fields such as computational geometry, approximation algorithms and machine learning. In this entry we formalize the notion of shattering and prove a general version of the Sauer-Shelah Lemma, from which the standard one follows.

About

A Formalization of the Sauer-Shelah Lemma using Isabelle/HOL

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published