Randomness does not help polynomial-size circuits

Let F be a Boolean function of n + p variables, read as F (x ++ r) for an input x and a random string r. If, for every x, at least two thirds of the random strings give the answer g x, then g has circuits of size O(n (C(F) + n)), where C(F) is the circuit complexity of F (Adleman's theorem in circuit form, Arora and Barak, Theorem 7.14): take 12 (n + 1) random strings that make the majority right for all 2 ^ n inputs at once (Cslib.exists_forall_lt_card_filter_mem), and hardwire them. For one-sided error, n + 1 random strings and their disjunction suffice. Applied at every length, bounded-error randomness over a family of polynomial-size circuits stays in P/poly.

Main results

• Cslib.Circuits.Boolean.complexity_le_of_boundedError, Cslib.Circuits.Boolean.complexity_le_of_oneSidedError: one input length.
• Cslib.Circuits.Boolean.PPoly.of_boundedError, Cslib.Circuits.Boolean.PPoly.of_oneSidedError: all input lengths.
• Cslib.Circuits.Boolean.PPoly.exists_of_boundedError, Cslib.Circuits.Boolean.PPoly.exists_of_oneSidedError: the same with a promise, on chosen sets of inputs, as needed for problems with an arbitrary encoding.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 7.5
• L. Adleman, Two theorems on random polynomial time

theorem Cslib.Circuits.Boolean.complexity_le_of_eq_threshold {n p m j : ℕ} (F : BooleanFunction (n + p)) (g : BooleanFunction n) (ω : Fin m → Fin p → Bool) (h : ∀ (x : BitString n), g x = threshold m j fun (i : Fin m) => F (Fin.append x (ω i))) : complexity interpretation (single g) ≤ m * (complexity interpretation (single F) + 2) + (2 + m * (2 * (m + 2)))

If g is a threshold of copies of F with hardwired random strings, its complexity is at most that of the copies and of the threshold.

theorem Cslib.Circuits.Boolean.exists_complexity_le_of_boundedError {n p : ℕ} (S : Set (Fin n → Bool)) (F : BooleanFunction (n + p)) (g : BooleanFunction n) (h : ∀ x ∈ S, 2 * 2 ^ p ≤ 3 * {r : Fin p → Bool | F (Fin.append x r) = g x}.card) : ∃ (g' : BooleanFunction n), (∀ x ∈ S, g' x = g x) ∧ complexity interpretation (single g') ≤ (12 * n + 12) * (complexity interpretation (single F) + 2) + (2 + (12 * n + 12) * (2 * (12 * n + 12 + 2)))

Adleman's theorem, for one input length, on a set of inputs. If, for every x ∈ S, at least two thirds of the random strings r have F (x ++ r) = g x, then some function agreeing with g on S has circuits of size O(n (C(F) + n)).

theorem Cslib.Circuits.Boolean.complexity_le_of_boundedError {n p : ℕ} (F : BooleanFunction (n + p)) (g : BooleanFunction n) (h : ∀ (x : Fin n → Bool), 2 * 2 ^ p ≤ 3 * {r : Fin p → Bool | F (Fin.append x r) = g x}.card) : complexity interpretation (single g) ≤ (12 * n + 12) * (complexity interpretation (single F) + 2) + (2 + (12 * n + 12) * (2 * (12 * n + 12 + 2)))

Adleman's theorem, for one input length. If, for every x, at least two thirds of the random strings r have F (x ++ r) = g x, then g has circuits of size O(n (C(F) + n)).

theorem Cslib.Circuits.Boolean.exists_complexity_le_of_oneSidedError {n p : ℕ} (S : Set (Fin n → Bool)) (F : BooleanFunction (n + p)) (g : BooleanFunction n) (h₁ : ∀ x ∈ S, g x = true → 2 ^ p ≤ 2 * {r : Fin p → Bool | F (Fin.append x r) = true}.card) (h₂ : ∀ x ∈ S, g x = false → ∀ (r : Fin p → Bool), F (Fin.append x r) = false) : ∃ (g' : BooleanFunction n), (∀ x ∈ S, g' x = g x) ∧ complexity interpretation (single g') ≤ (n + 1) * (complexity interpretation (single F) + 2) + (2 + (n + 1) * (2 * (n + 1 + 2)))

Adleman's theorem for one-sided error, for one input length, on a set of inputs. If, for every x ∈ S with g x = true, at least half of the random strings r have F (x ++ r) = true, and for every x ∈ S with g x = false none has, then some function agreeing with g on S has circuits of size O(n (C(F) + n)).

theorem Cslib.Circuits.Boolean.complexity_le_of_oneSidedError {n p : ℕ} (F : BooleanFunction (n + p)) (g : BooleanFunction n) (h₁ : ∀ (x : BitString n), g x = true → 2 ^ p ≤ 2 * {r : Fin p → Bool | F (Fin.append x r) = true}.card) (h₂ : ∀ (x : BitString n), g x = false → ∀ (r : Fin p → Bool), F (Fin.append x r) = false) : complexity interpretation (single g) ≤ (n + 1) * (complexity interpretation (single F) + 2) + (2 + (n + 1) * (2 * (n + 1 + 2)))

Adleman's theorem for one-sided error, for one input length. If, for every x with g x = true, at least half of the random strings r have F (x ++ r) = true, and for every x with g x = false none has, then g has circuits of size O(n (C(F) + n)).

theorem Cslib.Circuits.Boolean.PPoly.exists_of_boundedError {p : ℕ → ℕ} (F : (n : ℕ) → BooleanFunction (n + p n)) (hF : PolynomiallyBounded fun (n : ℕ) => complexity interpretation (single (F n))) (S : (n : ℕ) → Set (Fin n → Bool)) (g : (n : ℕ) → BooleanFunction n) (h : ∀ (n : ℕ), ∀ x ∈ S n, 2 * 2 ^ p n ≤ 3 * {r : Fin (p n) → Bool | F n (Fin.append x r) = g n x}.card) : ∃ L ∈ PPoly, ∀ (n : ℕ), ∀ x ∈ S n, L.slice n x = g n x

Adleman's theorem, on sets of inputs. If F n is a family of functions of n + p n variables with circuits of polynomial size, and for every input x ∈ S n at least two thirds of the random strings r have F n (x ++ r) = g n x, then some language in P/poly agrees with g on the sets S n.

theorem Cslib.Circuits.Boolean.PPoly.of_boundedError {A : Language Bool} {p : ℕ → ℕ} (F : (n : ℕ) → BooleanFunction (n + p n)) (hF : PolynomiallyBounded fun (n : ℕ) => complexity interpretation (single (F n))) (h : ∀ (n : ℕ) (x : Fin n → Bool), 2 * 2 ^ p n ≤ 3 * {r : Fin (p n) → Bool | F n (Fin.append x r) = A.slice n x}.card) : A ∈ PPoly

Adleman's theorem. If F n is a family of functions of n + p n variables with circuits of polynomial size, and for every input x of every length n at least two thirds of the random strings r have F n (x ++ r) = A.slice n x, then A ∈ P/poly.

theorem Cslib.Circuits.Boolean.PPoly.exists_of_oneSidedError {p : ℕ → ℕ} (F : (n : ℕ) → BooleanFunction (n + p n)) (hF : PolynomiallyBounded fun (n : ℕ) => complexity interpretation (single (F n))) (S : (n : ℕ) → Set (Fin n → Bool)) (g : (n : ℕ) → BooleanFunction n) (h₁ : ∀ (n : ℕ), ∀ x ∈ S n, g n x = true → 2 ^ p n ≤ 2 * {r : Fin (p n) → Bool | F n (Fin.append x r) = true}.card) (h₂ : ∀ (n : ℕ), ∀ x ∈ S n, g n x = false → ∀ (r : Fin (p n) → Bool), F n (Fin.append x r) = false) : ∃ L ∈ PPoly, ∀ (n : ℕ), ∀ x ∈ S n, L.slice n x = g n x

Adleman's theorem for one-sided error, on sets of inputs.

theorem Cslib.Circuits.Boolean.PPoly.of_oneSidedError {A : Language Bool} {p : ℕ → ℕ} (F : (n : ℕ) → BooleanFunction (n + p n)) (hF : PolynomiallyBounded fun (n : ℕ) => complexity interpretation (single (F n))) (h₁ : ∀ (n : ℕ) (x : Fin n → Bool), A.slice n x = true → 2 ^ p n ≤ 2 * {r : Fin (p n) → Bool | F n (Fin.append x r) = true}.card) (h₂ : ∀ (n : ℕ) (x : Fin n → Bool), A.slice n x = false → ∀ (r : Fin (p n) → Bool), F n (Fin.append x r) = false) : A ∈ PPoly

Adleman's theorem for one-sided error. If F n is a family of functions of n + p n variables with circuits of polynomial size, every input x ∈ A has F n (x ++ r) = true for at least half of the random strings r, and no x ∉ A has it for any r, then A ∈ P/poly.