def Shatters {α : Type u_1} [SemilatticeInf α] (𝒜 : Set α) (A : α) : Prop

A set family 𝒜 shatters a set A if all subsets of A can be obtained as the intersection of A with some element of the set family. We also say that A is traced by 𝒜.

Equations

• Shatters 𝒜 A = ∀ ⦃B : α⦄, B ≤ A → ∃ C ∈ 𝒜, A ⊓ C = B

theorem Shatters.mono {α : Type u_1} [SemilatticeInf α] {𝒜 ℬ : Set α} {A : α} (h : 𝒜 ⊆ ℬ) (h𝒜 : Shatters 𝒜 A) : Shatters ℬ A

theorem Shatters.anti {α : Type u_1} [SemilatticeInf α] {𝒜 : Set α} {A B : α} (h : A ≤ B) (hB : Shatters 𝒜 B) : Shatters 𝒜 A

def IsNIPWith {α : Type u_1} (d : ℕ) (𝒜 : Set (Set α)) : Prop

A set family 𝒜 is d-NIP if it has VC dimension at most d, namely if all the sets it shatters have size at most d.

Equations

• IsNIPWith d 𝒜 = ∀ ⦃A : Finset α⦄, Shatters 𝒜 ↑A → A.card ≤ d

theorem IsNIPWith.anti {α : Type u_1} {d : ℕ} {𝒜 ℬ : Set (Set α)} (hℬ𝒜 : ℬ ⊆ 𝒜) (h𝒜 : IsNIPWith d 𝒜) : IsNIPWith d ℬ

theorem IsNIPWith.mono {α : Type u_1} {d₁ d₂ : ℕ} {𝒜 : Set (Set α)} (hd : d₁ ≤ d₂) (hd₁ : IsNIPWith d₁ 𝒜) : IsNIPWith d₂ 𝒜