Counting accepted strings

Cslib.Complexity.acceptCount V a n is the number of strings w of length n with V (a, w) = true, for any Boolean predicate V : α × List Bool → Bool. No efficiency of V is assumed. It counts the certificates of a verifier in the counting classes (Cslib.Complexity.SharpP), the random strings accepted by a bounded-error or majority verifier, and the choice strings accepted by a fair-coin machine (Turing.MultiTapePTM.acceptCount).

Main definitions

• Cslib.Complexity.acceptCount: the number of accepted strings of a given length.

Main results

• Cslib.Complexity.acceptCount_le_two_pow, Cslib.Complexity.acceptCount_pos_iff, Cslib.Complexity.acceptCount_eq_zero_iff: the range and support of the count.
• Cslib.Complexity.acceptCount_add: counting accepted strings by their prefixes.
• Cslib.Complexity.acceptCount_zero, Cslib.Complexity.acceptCount_add_acceptCount_not, Cslib.Complexity.acceptCount_not: counts of trivial and negated verifiers.

def Cslib.Complexity.acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ

The number of strings w of length n with V (a, w) = true.

theorem Cslib.Complexity.acceptCount_le_two_pow {α : Type} {V : α × List Bool → Bool} {a : α} {n : ℕ} : acceptCount V a n ≤ 2 ^ n

At most all 2 ^ n strings are accepted.

theorem Cslib.Complexity.acceptCount_pos_iff {α : Type} {V : α × List Bool → Bool} {a : α} {n : ℕ} : 0 < acceptCount V a n ↔ ∃ (w : List Bool), w.length = n ∧ V (a, w) = true

Some string of length n is accepted exactly when the count is positive.

theorem Cslib.Complexity.acceptCount_eq_zero_iff {α : Type} {V : α × List Bool → Bool} {a : α} {n : ℕ} : acceptCount V a n = 0 ↔ ∀ (w : Fin n → Bool), V (a, List.ofFn w) = false

No string of length n is accepted exactly when the count is zero.

theorem Cslib.Complexity.acceptCount_add_card_filter_eq_false {α : Type} {V : α × List Bool → Bool} {a : α} {n : ℕ} : acceptCount V a n + {w : Fin n → Bool | V (a, List.ofFn w) = false}.card = 2 ^ n

The strings that V accepts together with a and those it rejects are all the strings.

theorem Cslib.Complexity.acceptCount_add {α : Type} (V : α × List Bool → Bool) (a : α) (m n : ℕ) : acceptCount V a (m + n) = ∑ u : Fin m → Bool, acceptCount (fun (x : α × List Bool) => V (x.1, List.ofFn u ++ x.2)) a n

Counting strings by their prefixes: the strings of length m + n accepted by V are the strings u ++ w, with u of length m and w of length n accepted with the prefix u.

theorem Cslib.Complexity.acceptCount_congr {α : Type} {V : α × List Bool → Bool} {a : α} {W : α × List Bool → Bool} (h : ∀ (w : List Bool), V (a, w) = W (a, w)) (n : ℕ) : acceptCount V a n = acceptCount W a n

Verifiers that agree on an instance accept the same strings with it.

theorem Cslib.Complexity.acceptCount_zero {α : Type} (V : α × List Bool → Bool) (a : α) : acceptCount V a 0 = if V (a, []) = true then 1 else 0

With no bits there is one string, the empty one.

@[simp]

theorem Cslib.Complexity.acceptCount_true {α : Type} (a : α) (n : ℕ) : acceptCount (fun (x : α × List Bool) => true) a n = 2 ^ n

The verifier accepting everything accepts all 2 ^ n strings of length n.

@[simp]

theorem Cslib.Complexity.acceptCount_false {α : Type} (a : α) (n : ℕ) : acceptCount (fun (x : α × List Bool) => false) a n = 0

The verifier rejecting everything accepts no string.

theorem Cslib.Complexity.acceptCount_add_acceptCount_not {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : acceptCount V a n + acceptCount (fun (x : α × List Bool) => !V x) a n = 2 ^ n

A verifier and its negation together accept every string once.

theorem Cslib.Complexity.acceptCount_not {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : acceptCount (fun (x : α × List Bool) => !V x) a n = 2 ^ n - acceptCount V a n

The negation of a verifier accepts the strings that it rejects.