Documentation

Mathlib.Combinatorics.SetFamily.Shatter

Shattering families #

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

Main declarations #

TODO #

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

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
    Instances For
      Equations
        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}
        theorem Finset.Shatters.mono_left {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : 𝒜 ) (h𝒜 : 𝒜.Shatters s) :
        .Shatters s
        theorem Finset.Shatters.mono_right {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s t : Finset α} (h : t s) (hs : 𝒜.Shatters s) :
        𝒜.Shatters t
        theorem Finset.Shatters.exists_superset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : 𝒜.Shatters s) :
        t𝒜, s t
        theorem Finset.shatters_of_forall_subset {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : ts, t 𝒜) :
        𝒜.Shatters s
        theorem Finset.Shatters.nonempty {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (h : 𝒜.Shatters s) :
        @[simp]
        theorem Finset.shatters_empty {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} :
        theorem Finset.Shatters.subset_iff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s t : Finset α} (h : 𝒜.Shatters s) :
        t s u𝒜, s u = t
        theorem Finset.shatters_iff {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :
        𝒜.Shatters s image (fun (t : Finset α) => s t) 𝒜 = s.powerset
        theorem Finset.univ_shatters {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] :
        @[simp]
        theorem Finset.shatters_univ {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} [Fintype α] :
        𝒜.Shatters univ 𝒜 = univ
        def Finset.shatterer {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) :

        The set family of sets that are shattered by 𝒜.

        Equations
          Instances For
            @[simp]
            theorem Finset.mem_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :
            s 𝒜.shatterer 𝒜.Shatters s
            theorem Finset.shatterer_mono {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} (h : 𝒜 ) :
            theorem Finset.subset_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} (h : IsLowerSet 𝒜) :
            𝒜 𝒜.shatterer
            @[simp]
            theorem Finset.isLowerSet_shatterer {α : Type u_1} [DecidableEq α] (𝒜 : Finset (Finset α)) :
            @[simp]
            theorem Finset.shatterer_eq {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} :
            𝒜.shatterer = 𝒜 IsLowerSet 𝒜
            @[simp]
            theorem Finset.shatterer_idem {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} :
            @[simp]
            theorem Finset.shatters_shatterer {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} :
            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.

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

            Pajor's variant of the Sauer-Shelah lemma.

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

            Vapnik-Chervonenkis dimension #

            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
              Instances For
                theorem Finset.vcDim_mono {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} (h𝒜ℬ : 𝒜 ) :
                𝒜.vcDim .vcDim
                theorem Finset.Shatters.card_le_vcDim {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} (hs : 𝒜.Shatters s) :
                s.card 𝒜.vcDim
                theorem Finset.vcDim_compress_le {α : Type u_1} [DecidableEq α] (a : α) (𝒜 : Finset (Finset α)) :

                Down-compressing decreases the VC-dimension.

                theorem Finset.card_shatterer_le_sum_vcDim {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} [Fintype α] :
                𝒜.shatterer.card kIic 𝒜.vcDim, (Fintype.card α).choose k

                The Sauer-Shelah lemma.