Shattering families

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

Main declarations

• Finset.StronglyShatters:
• Finset.OrderShatters:

TODO

• Order-shattering
• Strong shattering

Strong shattering

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

Equations

• 𝒜.StronglyShatters s = ∃ (t : Finset α), ∀ ⦃u : Finset α⦄, u ⊆ s → ∃ v ∈ 𝒜, s ∩ v = u ∧ v \ s = t

Order shattering

def Finset.OrderShatters {α : Type u_1} [DecidableEq α] [LinearOrder α] : Finset (Finset α) → List α → Prop

Equations

• One or more equations did not get rendered due to their size.
• x✝.OrderShatters [] = x✝.Nonempty

@[implicit_reducible]

instance Finset.instDecidableRel {α : Type u_1} [DecidableEq α] [LinearOrder α] : DecidableRel OrderShatters

Equations

• One or more equations did not get rendered due to their size.

def Finset.orderShatterser {α : Type u_1} [DecidableEq α] [LinearOrder α] (𝒜 : Finset (Finset α)) : Finset (Finset α)

Equations

• 𝒜.orderShatterser = {s ∈ 𝒜.biUnion Finset.powerset | 𝒜.OrderShatters (s.sort fun (x1 x2 : α) => x1 ≤ x2)}