Shattering families #
This file defines the shattering property and VC-dimension of set families.
Main declarations #
Finset.Shatters
: The shattering property.Finset.shatterer
: The set family of sets shattered by a set family.Finset.vcDim
: The Vapnik-Chervonenkis dimension.
TODO #
- Order-shattering
- Strong shattering
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 𝒜
.
Instances For
instance
Finset.instDecidablePredShatters
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
:
DecidablePred 𝒜.Shatters
Equations
- Finset.instDecidablePredShatters _s = Finset.decidableForallOfDecidableSubsets
theorem
Finset.Shatters.exists_inter_eq_singleton
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{s : Finset α}
{a : α}
(hs : 𝒜.Shatters s)
(ha : a ∈ s)
:
theorem
Finset.Shatters.mono_left
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{ℬ : Finset (Finset α)}
{s : Finset α}
(h : 𝒜 ⊆ ℬ)
(h𝒜 : 𝒜.Shatters s)
:
ℬ.Shatters s
theorem
Finset.Shatters.mono_right
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{s : Finset α}
{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 : ∀ t ⊆ s, t ∈ 𝒜)
:
𝒜.Shatters s
theorem
Finset.Shatters.nonempty
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{s : Finset α}
(h : 𝒜.Shatters s)
:
𝒜.Nonempty
@[simp]
theorem
Finset.shatters_iff
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{s : Finset α}
:
𝒜.Shatters s ↔ Finset.image (fun (t : Finset α) => s ∩ t) 𝒜 = s.powerset
theorem
Finset.univ_shatters
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
[Fintype α]
:
Finset.univ.Shatters s
@[simp]
The set family of sets that are shattered by 𝒜
.
Equations
- 𝒜.shatterer = Finset.filter (fun (s : Finset α) => 𝒜.Shatters s) (𝒜.biUnion Finset.powerset)
Instances For
@[simp]
theorem
Finset.mem_shatterer
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{s : Finset α}
:
theorem
Finset.shatterer_mono
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{ℬ : Finset (Finset α)}
(h : 𝒜 ⊆ ℬ)
:
𝒜.shatterer ⊆ ℬ.shatterer
theorem
Finset.subset_shatterer
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
(h : IsLowerSet ↑𝒜)
:
𝒜 ⊆ 𝒜.shatterer
@[simp]
theorem
Finset.isLowerSet_shatterer
{α : Type u_1}
[DecidableEq α]
(𝒜 : Finset (Finset α))
:
IsLowerSet ↑𝒜.shatterer
@[simp]
theorem
Finset.shatterer_eq
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
:
𝒜.shatterer = 𝒜 ↔ IsLowerSet ↑𝒜
@[simp]
theorem
Finset.shatterer_idem
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
:
𝒜.shatterer.shatterer = 𝒜.shatterer
@[simp]
theorem
Finset.shatters_shatterer
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{s : Finset α}
:
𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s
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 α))
:
𝒜.card ≤ 𝒜.shatterer.card
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
theorem
Finset.shatterer_compress_subset_shatterer
{α : Type u_1}
[DecidableEq α]
(a : α)
(𝒜 : Finset (Finset α))
:
(Down.compression a 𝒜).shatterer ⊆ 𝒜.shatterer
Vapnik-Chervonenkis dimension #
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
theorem
Finset.vcDim_mono
{α : Type u_1}
[DecidableEq α]
{𝒜 : Finset (Finset α)}
{ℬ : 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.compression a 𝒜).vcDim ≤ 𝒜.vcDim
Down-compressing decreases the VC-dimension.
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.