VC-dimensions of nondeterministic finite automata for words of equal length

Part 1: Define VC dimension and VC index and prove
`dimVC = indexVC - 1` (even in the case of the empty family)

def shatters_some {V : Type u_1} [DecidableEq V] (𝓕 : Finset (Finset V)) (d : ℕ) : Prop

To make this computable, restrict A ⊆ ⋃ 𝓕

Equations

• shatters_some 𝓕 d = ∃ (A : Finset V), A.card = d ∧ ∀ B ⊆ A, ∃ C ∈ 𝓕, A ∩ C = B

def shatters_all {V : Type u_1} [DecidableEq V] (𝓕 : Finset (Finset V)) (d : ℕ) : Prop

Perhaps more natural to say: there is such a set, and 𝓕 shatters them all.

Equations

• shatters_all 𝓕 d = ∀ (A : Finset V), A.card = d → ∀ B ⊆ A, ∃ C ∈ 𝓕, A ∩ C = B

instance instDecidableEqFinsetInter_acmoi {V : Type u_1} [DecidableEq V] (A : Finset V) (B : Finset V) (C : Finset V) : Decidable (A ∩ C = B)

Equations

• instDecidableEqFinsetInter_acmoi A B C = decEq (A ∩ C) B

instance instDecidableEqFinset_acmoi {V : Type u_1} [DecidableEq V] (𝓕 : Finset (Finset V)) (𝓖 : Finset (Finset V)) : Decidable (𝓕 = 𝓖)

Equations

• instDecidableEqFinset_acmoi 𝓕 𝓖 = decEq 𝓕 𝓖

instance instDecidableExistsFinsetAndMemEqInter_acmoi {V : Type u_1} [DecidableEq V] (A : Finset V) (B : Finset V) (𝓕 : Finset (Finset V)) : Decidable (∃ C ∈ 𝓕, A ∩ C = B)

Equations

• instDecidableExistsFinsetAndMemEqInter_acmoi A B 𝓕 = Multiset.decidableExistsMultiset

instance instDecidableForallForallSubsetFinsetExistsAndMemEqInter_acmoi {V : Type u_1} [DecidableEq V] [Fintype V] (A : Finset V) (𝓕 : Finset (Finset V)) : Decidable (∀ B ⊆ A, ∃ C ∈ 𝓕, A ∩ C = B)

Equations

• instDecidableForallForallSubsetFinsetExistsAndMemEqInter_acmoi A 𝓕 = Fintype.decidableForallFintype

instance instDecidableAndEqNatCardForallForallSubsetFinsetExistsMemInter_acmoi {V : Type u_1} [DecidableEq V] [Fintype V] (A : Finset V) (𝓕 : Finset (Finset V)) (d : ℕ) : Decidable (A.card = d ∧ ∀ B ⊆ A, ∃ C ∈ 𝓕, A ∩ C = B)

Equations

• instDecidableAndEqNatCardForallForallSubsetFinsetExistsMemInter_acmoi A 𝓕 d = instDecidableAnd

instance instDecidableShatters_some {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (d : ℕ) : Decidable (shatters_some 𝓕 d)

Equations

• instDecidableShatters_some 𝓕 d = id Fintype.decidableExistsFintype

instance instDecidableShatters_all {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (d : ℕ) : Decidable (shatters_all 𝓕 d)

Equations

• instDecidableShatters_all 𝓕 d = id Fintype.decidableForallFintype

theorem empty_does_not_shatter {V : Type u_1} [DecidableEq V] (k : ℕ) : ¬shatters_some ∅ k

theorem nonempty_shatters {V : Type u_1} [DecidableEq V] (𝓕 : Finset (Finset V)) {A : Finset V} (hA : A ∈ 𝓕) : shatters_some 𝓕 0

theorem shatters_some₀ {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) : F ≠ ∅ ↔ shatters_some F 0

Shattering some set of size 0 or 1 is equivalent to having cardinality at least 2^0 or 2^1, respectively.

theorem shatters_some₁ {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : (∃ A ∈ 𝓕, ∃ B ∈ 𝓕, A ≠ B) ↔ shatters_some 𝓕 1

Shattering some set of size 0 or 1 is equivalent to having cardinality at least 2^0 or 2^1, respectively.

def dimVC {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : ℕ

The VC dimension of a finite set family.

Equations

• dimVC 𝓕 = if H : 𝓕 = ∅ then 0 else (Finset.filter (shatters_some 𝓕) (Finset.range (Finset.univ.card + 1))).max' ⋯

theorem subset_of_size {α : Type u_1} {s : Finset α} (a : ℕ) (b : ℕ) (h_card : s.card = b) (h_le : a ≤ b) : ∃ t ⊆ s, t.card = a

Obtain a smaller subset of a given set.

theorem not_shatters_all_empty {V : Type u_1} [DecidableEq V] [Fintype V] (k : ℕ) (hk : k ≤ Fintype.card V) : ¬shatters_all ∅ k

theorem not_shatters_all_emp {V : Type u_1} [DecidableEq V] [Fintype V] : ¬shatters_all ∅ 0

theorem shatters_all₀ {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) : F ≠ ∅ ↔ shatters_all F 0

theorem shatters_monotone {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (k : ℕ) (l : ℕ) (h : k ≤ l) (h₀ : shatters_some 𝓕 l) : shatters_some 𝓕 k

A family can also shatter a smaller set.

theorem le_max'_iff (S : Finset ℕ) (h : S.Nonempty) (k : ℕ) : k ≤ S.max' h ↔ ∃ y ∈ S, k ≤ y

theorem shattering_skolem {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) (k : ℕ) (h : shatters_some F k) : ∃ (A : Finset V), A.card = k ∧ ∃ (φ : { B : Finset V // B ⊆ A } → { C : Finset V // C ∈ F }), ∀ (B : { B : Finset V // B ⊆ A }), A ∩ ↑(φ B) = ↑B

theorem VC_injective_function {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) (A : Finset V) (φ : { B : Finset V // B ⊆ A } → { C : Finset V // C ∈ F }) (h : ∀ (B : { B : Finset V // B ⊆ A }), A ∩ ↑(φ B) = ↑B) : Function.Injective φ

theorem card_of_injective {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) (A : Finset V) (φ : { B : Finset V // B ⊆ A } → { C : Finset V // C ∈ F }) (h : Function.Injective φ) : A.powerset.card ≤ F.card

Lean 3 version thanks to Adam Topaz.

theorem pow_le_of_shatters {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) (k : ℕ) (h : shatters_some F k) : 2 ^ k ≤ F.card

theorem pow_le_of_shatters₂ {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) (k : ℕ) (h : shatters_some F k) : k ≤ Nat.log 2 F.card

theorem pow_le (m : ℕ) : m < 2 ^ m

theorem dimVC_def {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (h𝓕 : ∃ (f : Finset V), f ∈ 𝓕) (k : ℕ) : k ≤ dimVC 𝓕 ↔ shatters_some 𝓕 k

theorem pow_le_of_shatters₃! {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (h𝓕 : ∃ (f : Finset V), f ∈ 𝓕) : dimVC 𝓕 ≤ Nat.log 2 𝓕.card

The VC dimension is bounded by the logarithm of the cardinality. This is one of the bounds listed in Wikipedia.

theorem indexVC_as_min'_defined {V : Type u_1} [DecidableEq V] [Fintype V] {𝓕 : Finset (Finset V)} : (Finset.filter (fun (k : ℕ) => ¬shatters_some 𝓕 k) (Finset.range (Finset.univ.card + 2))).Nonempty

theorem not_shatter_ {V : Type u_1} [DecidableEq V] [Fintype V] {𝓕 : Finset (Finset V)} : (Finset.filter (fun (k : ℕ) => ¬shatters_some 𝓕 k) (Finset.range (𝓕.card + 1))).Nonempty

def indexVC {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : ℕ

The VC index is the VC dimension +1 for nonempty finite families, but can be defined for families of all cardinalities.

Equations

• indexVC 𝓕 = if H : shatters_some 𝓕 Finset.univ.card then Finset.univ.card + 1 else (Finset.filter (fun (k : ℕ) => ¬shatters_some 𝓕 k) (Finset.range (Finset.univ.card + 1))).min' ⋯

def indexVC_as_min' {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : ℕ

Equations

• indexVC_as_min' 𝓕 = (Finset.filter (fun (k : ℕ) => ¬shatters_some 𝓕 k) (Finset.range (Finset.univ.card + 2))).min' ⋯

theorem too_big_to_shatter {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : ¬shatters_some 𝓕 (Fintype.card V + 1)

theorem shatters_some_mono {k : ℕ} {l : ℕ} (h₀ : k ≤ l) {V : Type u_1} [DecidableEq V] [Fintype V] {𝓕 : Finset (Finset V)} (h : shatters_some 𝓕 l) : shatters_some 𝓕 k

theorem indexVC_as_min'_eq_indexVC {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : indexVC_as_min' 𝓕 = indexVC 𝓕

theorem indexVC_as_min'_emp {V : Type u_1} [DecidableEq V] [Fintype V] : indexVC_as_min' ∅ = 0

theorem dimVC_emp {V : Type u_1} [DecidableEq V] [Fintype V] : dimVC ∅ = 0

theorem dim_index_VC {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : dimVC 𝓕 = indexVC 𝓕 - 1

Obtain dimVC from indexVC. Since dimVC ∅ = 0 and indexVC ∅ x= 0, this relies on 0 - 1 = 0.

theorem VC_mono {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (𝓖 : Finset (Finset V)) (h : 𝓕 ⊆ 𝓖) : dimVC 𝓕 ≤ dimVC 𝓖

theorem VC_trivBound {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (h𝓕 : ∃ (f : Finset V), f ∈ 𝓕) : dimVC 𝓕 ≤ Finset.univ.card

def indexTest {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : ℕ

Kathleen Romanik's testing dimension, index version.

Equations

• indexTest 𝓕 = if hf : ∃ (B : Finset V), B ∉ 𝓕 then (Finset.filter (fun (k : ℕ) => ¬shatters_all 𝓕 k) (Finset.range (Finset.univ.card + 1))).min' ⋯ else Finset.univ.card + 1

def dimTest {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : ℕ

Kathleen Romanik's testing dimension, Source: Definition 2 of "VC-dimensions of nondeterministic finite automata for words of equal length".

Equations

• dimTest 𝓕 = if H : 𝓕 = ∅ then 0 else let_fun this := ⋯; (Finset.filter (fun (k : ℕ) => shatters_all 𝓕 k) (Finset.range (Finset.univ.card + 1))).max' ⋯

theorem dimTest_le_dimVC {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : dimTest 𝓕 ≤ dimVC 𝓕

theorem shatters_all_mono {V : Type u_1} [DecidableEq V] [Fintype V] {𝓕 : Finset (Finset V)} {k : ℕ} {l : ℕ} (h : shatters_all 𝓕 l) (h₀ : k ≤ l) (h₁ : l ≤ Finset.univ.card) : shatters_all 𝓕 k

theorem please_nemp {V : Type u_1} [DecidableEq V] [Fintype V] {𝓕 : Finset (Finset V)} (G : ∃ (B : Finset V), B ∉ 𝓕) : (Finset.filter (fun (k : ℕ) => ¬shatters_all 𝓕 k) (Finset.range (Fintype.card V + 1))).Nonempty

theorem indexTest_le_indexVC {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : indexTest 𝓕 ≤ indexVC 𝓕

theorem dim_index_test {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : dimTest 𝓕 = indexTest 𝓕 - 1

theorem dimVC_powerset {V : Type u_1} [DecidableEq V] [Fintype V] : dimVC Finset.univ = Finset.univ.card

The VC dimension of the powerset is the cardinality of the underlying set. Note that this does not require [Nonempty V].

theorem dimVC_eq {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (h𝓕 : ∃ (f : Finset V), f ∈ 𝓕) (k : ℕ) : shatters_some 𝓕 k ∧ ¬shatters_some 𝓕 (k + 1) → dimVC 𝓕 = k

theorem summarize {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) : dimTest 𝓕 ≤ dimVC 𝓕 ∧ dimVC 𝓕 ≤ indexVC 𝓕 ∧ dimTest 𝓕 ≤ indexTest 𝓕 ∧ indexTest 𝓕 ≤ indexVC 𝓕

A diamond:

indexVC

dimVC indexTest dimTest

theorem counter₁ : ∃ (V : Type) (x : DecidableEq V) (x_1 : Fintype V) (𝓕 : Finset (Finset V)), dimVC 𝓕 < indexTest 𝓕

theorem counter₂ : ∃ (V : Type) (x : DecidableEq V) (x_1 : Fintype V) (𝓕 : Finset (Finset V)), dimVC 𝓕 > indexTest 𝓕