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

Definition 10, Lemma 11, and Lemma 12 from the paper.
(Bonus material for ac-exercises)

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

To make this computable, restrict A ⊆ ⋃ 𝓕

Equations

• shatters_card 𝓕 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_card {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : Finset (Finset V)) (d : ℕ) : Decidable (shatters_card 𝓕 d)

Equations

• instDecidableShatters_card 𝓕 d = id Fintype.decidableExistsFintype

theorem empty_does_not_shatter {V : Type u_1} [DecidableEq V] [Fintype V] : ¬shatters_card ∅ 0

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

theorem filter_condition {V : Type u_1} (𝓕 : Finset (Finset V)) (condition : Finset (Finset V) → ℕ → Prop) [DecidablePred (condition 𝓕)] (h₀ : 0 < 𝓕.card) (h₁ : condition 𝓕 0) : 0 ∈ Finset.filter (fun (k : ℕ) => condition 𝓕 k) (Finset.range 𝓕.card)

theorem equivVC {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) : 0 < F.card ↔ shatters_card F 0

theorem VC_filter {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) (h₀ : 0 < F.card) : 0 ∈ Finset.filter (fun (k : ℕ) => shatters_card F k) (Finset.range F.card)

TODO: Simplify since the two assumptions are equivalent.

def dimVC {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : { 𝓕 : Finset (Finset V) // ∃ (f : Finset V), f ∈ 𝓕 }) : ℕ

The VC dimension of a finite set family.

Equations

• dimVC 𝓕 = (Finset.filter (shatters_card ↑𝓕) (Finset.range (↑𝓕).card)).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 of_size_subset (V : Type u_1) [Fintype V] (S : Finset V) (k : ℕ) (l : ℕ) (h₀ : k ≤ l) (h : S.card = l) : ∃ (T : Finset V), T.card = k ∧ T ⊆ S

theorem shatters_monotone {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : { 𝓕 : Finset (Finset V) // ∃ (f : Finset V), f ∈ 𝓕 }) (k : ℕ) (l : ℕ) (h : k ≤ l) (h₀ : shatters_card (↑𝓕) l) : shatters_card (↑𝓕) k

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

theorem VC_as_a_function {V : Type u_1} [DecidableEq V] [Fintype V] (F : Finset (Finset V)) (k : ℕ) (h : shatters_card 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_card F k) : 2 ^ k ≤ F.card

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

theorem VC_works {V : Type u_1} [DecidableEq V] [Fintype V] (𝓕 : { 𝓕 : Finset (Finset V) // ∃ (f : Finset V), f ∈ 𝓕 }) (k : ℕ) : k ≤ dimVC 𝓕 ↔ shatters_card (↑𝓕) k

Dec 21 2024 with just a little ChatGPT help.

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

theorem rescue_lemma_12 {m : ℕ} : (2 * m.succ).succ < 2 ^ Nat.clog 2 (2 * m.succ).succ

def ν₂ (n : ℕ) : ℕ

ν₂ is called t in the paper.

Equations

• ν₂ = padicValNat 2

theorem ν₂_odd (n : ℕ) : ν₂ (2 * n + 1) = 0

theorem ν₂_2 (n : ℕ) (h : 0 < n) : ν₂ (2 * n) = ν₂ n + 1

theorem bits_odd {n : ℕ} : (2 * n + 1).bits = true :: n.bits

theorem bits_even {n : ℕ} (h : n ≠ 0) : (2 * n).bits = false :: n.bits

theorem length_map_sum (l : List Bool) : (List.map Bool.toNat l).sum ≤ l.length

def hammingBits (n : ℕ) : ℕ

Equations

• hammingBits n = (List.map Bool.toNat n.bits).sum

theorem hammingBits_2 (n : ℕ) : hammingBits (2 * n) = hammingBits n

theorem hammingBits_odd (n : ℕ) : hammingBits (2 * n + 1) = hammingBits n + 1

theorem mentioned_in_lemma_12 {n : ℕ} {s : ℕ} (h : n < 2 ^ s) : hammingBits n ≤ s

theorem andhence {m : ℕ} : hammingBits (2 * m.succ) < Nat.clog 2 (2 * m.succ).succ

theorem ν₂_hammingBits (n : ℕ) : ν₂ (n + 1) + hammingBits (n + 1) = hammingBits n + 1

def arndt : ℕ → ℕ

This function is called a at https://oeis.org/A005187 and we name it in honor of Jörg Arndt.

Equations

• arndt 0 = 0
• arndt k.succ = arndt k + 1 + ν₂ (k + 1)

theorem lemma11 (m : ℕ) : arndt m + hammingBits (2 * m) = 2 * m

Jörg Arndt (2019) claimed this without proof as a resolution of a conjecture of Benoit Cloitre (2003). Cloitre is a coauthor of Shallit (2023) and Jean-Paul Allouche.

theorem lemma12 (n : ℕ) : arndt n + Nat.clog 2 n.succ ≥ 2 * n