Documentation

Mathlib.Combinatorics.SetFamily.Shatter

Shattering families #

This file defines the shattering property and VC-dimension of set families.

Main declarations #

TODO #

source
def Finset.Shatters {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) (s : Finset α) :
Prop

A set family 𝒜 shatters a set s if all subsets of s can be obtained as the intersection of s and some element of the set family, and we denote this 𝒜.Shatters s. We also say that s is traced by 𝒜.

Equations
  • 𝒜.Shatters s = ∀ ⦃t : Finset α⦄, t ⊆ s → ∃ u ∈ 𝒜, s ∩ u = t
Instances For
    source
    instance Finset.instDecidablePredShatters {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} :
    DecidablePred 𝒜.Shatters
    Equations
    source
    theorem Finset.Shatters.exists_inter_eq_singleton {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α} (hs : 𝒜.Shatters s) (ha : a ∈ s) :
    ∃ t ∈ 𝒜, s ∩ t = {a}
    source
    theorem Finset.Shatters.mono_left {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} {s : Finset α} (h : 𝒜 ⊆ ℬ) (h𝒜 : 𝒜.Shatters s) :
    ℬ.Shatters s
    source
    theorem Finset.Shatters.mono_right {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {t : Finset α} (h : t ⊆ s) (hs : 𝒜.Shatters s) :
    𝒜.Shatters t
    source
    theorem Finset.Shatters.exists_superset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : 𝒜.Shatters s) :
    ∃ t ∈ 𝒜, s ⊆ t
    source
    theorem Finset.shatters_of_forall_subset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : ∀ t ⊆ s, t ∈ 𝒜) :
    𝒜.Shatters s
    source
    theorem Finset.Shatters.nonempty {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : 𝒜.Shatters s) :
    𝒜.Nonempty
    source
    @[simp]
    theorem Finset.shatters_empty {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} :
    𝒜.Shatters ∅ ↔ 𝒜.Nonempty
    source
    theorem Finset.Shatters.subset_iff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {t : Finset α} (h : 𝒜.Shatters s) :
    t ⊆ s ↔ ∃ u ∈ 𝒜, s ∩ u = t
    source
    theorem Finset.shatters_iff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :
    𝒜.Shatters s ↔ Finset.image (fun (t : Finset α) => s ∩ t) 𝒜 = s.powerset
    source
    theorem Finset.univ_shatters {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] :
    Finset.univ.Shatters s
    source
    @[simp]
    theorem Finset.shatters_univ {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} [Fintype α] :
    𝒜.Shatters Finset.univ ↔ 𝒜 = Finset.univ
    source
    def Finset.shatterer {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) :
    Finset (Finset α)

    The set family of sets that are shattered by 𝒜.

    Equations
    • 𝒜.shatterer = Finset.filter 𝒜.Shatters (𝒜.biUnion Finset.powerset)
    Instances For
      source
      @[simp]
      theorem Finset.mem_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :
      s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s
      source
      theorem Finset.shatterer_mono {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} (h : 𝒜 ⊆ ℬ) :
      𝒜.shatterer ⊆ ℬ.shatterer
      source
      theorem Finset.subset_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} (h : IsLowerSet ↑𝒜) :
      𝒜 ⊆ 𝒜.shatterer
      source
      @[simp]
      theorem Finset.isLowerSet_shatterer {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) :
      IsLowerSet ↑𝒜.shatterer
      source
      @[simp]
      theorem Finset.shatterer_eq {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} :
      𝒜.shatterer = 𝒜 ↔ IsLowerSet ↑𝒜
      source
      @[simp]
      theorem Finset.shatterer_idem {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} :
      𝒜.shatterer.shatterer = 𝒜.shatterer
      source
      @[simp]
      theorem Finset.shatters_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :
      𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s
      source
      theorem Finset.Shatters.shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :
      𝒜.Shatters s → 𝒜.shatterer.Shatters s

      Alias of the reverse direction of Finset.shatters_shatterer.

      source
      theorem Finset.card_le_card_shatterer {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) :
      𝒜.card ≤ 𝒜.shatterer.card

      Pajor's variant of the Sauer-Shelah lemma.

      source
      theorem Finset.Shatters.of_compression {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α} (hs : (Down.compression a 𝒜).Shatters s) :
      𝒜.Shatters s
      source
      theorem Finset.shatterer_compress_subset_shatterer {α : Type u_1} [DecidableEq α] (a : α) (𝒜 : Finset (Finset α)) :
      (Down.compression a 𝒜).shatterer ⊆ 𝒜.shatterer

      Vapnik-Chervonenkis dimension #

      source
      def Finset.vcDim {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) :
      ℕ

      The Vapnik-Chervonenkis dimension of a set family is the maximal size of a set it shatters.

      Equations
      • 𝒜.vcDim = 𝒜.shatterer.sup Finset.card
      Instances For
        source
        theorem Finset.Shatters.card_le_vcDim {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (hs : 𝒜.Shatters s) :
        s.card ≤ 𝒜.vcDim
        source
        theorem Finset.vcDim_compress_le {α : Type u_1} [DecidableEq α] (a : α) (𝒜 : Finset (Finset α)) :
        (Down.compression a 𝒜).vcDim ≤ 𝒜.vcDim

        Down-compressing decreases the VC-dimension.

        source
        theorem Finset.card_shatterer_le_sum_vcDim {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} [Fintype α] :
        𝒜.shatterer.card ≤ ∑ k ∈ Finset.Iic 𝒜.vcDim, (Fintype.card α).choose k

        The Sauer-Shelah lemma.