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

Theorem 4 on Kathleen Romanik's testing dimension.

theorem fixBits {V : Type u_1} [DecidableEq V] [Fintype V] (C : Finset V) (D : Finset V) (hD : D ⊆ C) : (Finset.filter (fun (H : Finset V) => C ∩ H = D) Finset.univ).card = (Finset.univ \ C).powerset.card

theorem four {V : Type u_1} [DecidableEq V] [Fintype V] (c : ℕ) (m : ℕ) (hm : m ≤ Fintype.card V) : (∀ (𝓗 : Finset (Finset V)), 𝓗.card > c → dimTest 𝓗 ≥ m) ↔ c ≥ 2 ^ Fintype.card V - 2 ^ (Fintype.card V - m)

Theorem 4 from "VC-dimensions".

theorem towards_lowerbound₀ {V : Type u_1} [DecidableEq V] [Fintype V] (c : ℕ) (m : ℕ) : 2 ^ (Fintype.card V - m) ≥ 2 ^ Fintype.card V - c → c ≥ 2 ^ Fintype.card V - 2 ^ (Fintype.card V - m)

theorem towards_lowerbound₁ {V : Type u_1} [DecidableEq V] [Fintype V] (c : ℕ) (m : ℕ) : Fintype.card V - m ≥ Nat.clog 2 (2 ^ Fintype.card V - c) → 2 ^ (Fintype.card V - m) ≥ 2 ^ Nat.clog 2 (2 ^ Fintype.card V - c)

theorem towards_lowerbound₂ {V : Type u_1} [DecidableEq V] [Fintype V] (c : ℕ) : 2 ^ Nat.clog 2 (2 ^ Fintype.card V - c) ≥ 2 ^ Fintype.card V - c

theorem towards_lowerbound₃ {V : Type u_1} [DecidableEq V] [Fintype V] (c : ℕ) (m : ℕ) : Fintype.card V - m ≥ Nat.clog 2 (2 ^ Fintype.card V - c) → 2 ^ (Fintype.card V - m) ≥ 2 ^ Fintype.card V - c