Error reduction for BPP

The error 1 / 3 in the definition of BPP (Cslib.Complexity.BPP) can be made exponentially small Arora and Barak, Section 7.4.1. Cut the random string into 2 r(n) blocks of p(n) bits, where n is the length of the encoded instance, run the bounded-error decider on every block and accept when a strict majority, more than r(n), of the runs accept (Cslib.Complexity.repeatMajority). The answer is wrong only when at most half of the runs are right, which happens on at most an (8 / 9) ^ r(n) fraction of the random strings (Cslib.card_filter_card_filter_le_le, an exponential-moment bound). Since 2 * 8 ^ 6 < 9 ^ 6, r = 6 q runs make the error at most 2 ^ (-q(n)).

The condition Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent enc q p V Q says that V errs on at most a 2 ^ (-q(n)) fraction of the random strings on every instance in the promise of Q; for a decision problem it is Cslib.Complexity.DecidesWithErrorExponent. Error reduction is proved once, for promise problems: a promise problem is in PromiseBPP exactly when it is solved in polynomial time with error at most 2 ^ (-q(n)) for every polynomial q (Cslib.Complexity.mem_PromiseBPP_iff_forall_solvesWithErrorExponent), and the statement for BPP is its instance at PromiseProblem.ofSet A. The one-sided version for RP is Cslib.Complexity.mem_PromiseRP_iff_forall_solvesWithOneSidedErrorExponent.

Main definitions

• Cslib.Complexity.ErrorExponentAt: the per-instance condition that a verifier errs from a specified Boolean answer on at most a 2 ^ (-q(n)) fraction of random strings.
• Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent: error at most 2 ^ (-q(n)).
• Cslib.Complexity.DecidesWithErrorExponent: its specialization to a decision problem.
• Cslib.Complexity.BPP.booleanSubalgebra: BPP as a Boolean subalgebra of Set α.

Main results

• Cslib.Complexity.errorExponentAt_true_iff, Cslib.Complexity.errorExponentAt_false_iff: per-instance error-exponent bounds as bounds on Cslib.Complexity.acceptCount.
• Cslib.Complexity.ErrorExponentAt.congr: extensionality for per-instance error-exponent bounds.
• Cslib.Complexity.BoundedErrorAt.repeatMajority, Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.repeatMajority: 12 q(n) majority votes reduce the error to 2 ^ (-q(n)).
• Cslib.Complexity.ErrorExponentAt.boundedErrorAt, Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent.solvesWithBoundedError: error at most 2 ^ (-q(n)) ≤ 1 / 4 is bounded error.
• Cslib.Complexity.mem_PromiseBPP_iff_forall_solvesWithErrorExponent, Cslib.Complexity.mem_BPP_iff_forall_decidesWithErrorExponent: error reduction for PromiseBPP and BPP.
• Cslib.Complexity.inter_mem_BPP, Cslib.Complexity.union_mem_BPP, Cslib.Complexity.diff_mem_BPP, Cslib.Complexity.symmDiff_mem_BPP: Boolean closure of BPP.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

@[reducible, inline]

abbrev Cslib.Complexity.ErrorExponentAt {α : Type} (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) (a : α) (b : Bool) : Prop

V gives the answer b with error at most 2 ^ (-q(n)) on the instance a, using random strings whose length is p evaluated at the length n of the encoded instance: the random strings r of length p n with V (a, r) = !b make up at most a 2 ^ (-q n) fraction.

theorem Cslib.Complexity.errorExponentAt_true_iff {α : Type} {enc : α ↪ List Bool} {q p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} : ErrorExponentAt enc q p V a true ↔ 2 ^ Polynomial.eval (enc a).length q * (2 ^ Polynomial.eval (enc a).length p - acceptCount V a (Polynomial.eval (enc a).length p)) ≤ 2 ^ Polynomial.eval (enc a).length p

Error at most 2 ^ (-q(n)) from true is rejection of at most a 2 ^ (-q(n)) fraction of the random strings.

theorem Cslib.Complexity.errorExponentAt_false_iff {α : Type} {enc : α ↪ List Bool} {q p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} : ErrorExponentAt enc q p V a false ↔ 2 ^ Polynomial.eval (enc a).length q * acceptCount V a (Polynomial.eval (enc a).length p) ≤ 2 ^ Polynomial.eval (enc a).length p

Error at most 2 ^ (-q(n)) from false is acceptance of at most a 2 ^ (-q(n)) fraction of the random strings.

theorem Cslib.Complexity.ErrorExponentAt.congr {α : Type} {enc : α ↪ List Bool} {q p : Polynomial ℕ} {V W : α × List Bool → Bool} {a : α} {b : Bool} (h : ErrorExponentAt enc q p V a b) (hVW : ∀ (r : Fin (Polynomial.eval (enc a).length p) → Bool), V (a, List.ofFn r) = W (a, List.ofFn r)) : ErrorExponentAt enc q p W a b

An error-exponent bound at an instance depends only on the verifier's values on strings of length p(|a|).

theorem Cslib.Complexity.BoundedErrorAt.repeatMajority {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {b : Bool} (h : BoundedErrorAt enc p V a b) (q : Polynomial ℕ) : ErrorExponentAt enc q (12 * q * p) (Complexity.repeatMajority enc (6 * q) p V) a b

Per-instance error reduction for bounded error: the strict majority of 12 q(n) runs of a verifier on independent blocks of random bits errs from b on at most a 2 ^ (-q(n)) fraction of the random strings whenever a single run produces b on at least two thirds of them.

theorem Cslib.Complexity.ErrorExponentAt.boundedErrorAt {α : Type} {enc : α ↪ List Bool} {q p : Polynomial ℕ} {V : α × List Bool → Bool} {a : α} {b : Bool} (h : ErrorExponentAt enc q p V a b) (hq : 2 ≤ Polynomial.eval (enc a).length q) : BoundedErrorAt enc p V a b

Error at most 2 ^ (-q(n)) ≤ 1 / 4 on an instance is bounded error on that instance.

def Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent {α : Type} (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) (Q : PromiseProblem α) : Prop

V solves the promise problem Q with error at most 2 ^ (-q(n)), using random strings whose length is p evaluated at the length n of the encoded instance: for every yes-instance the rejected random strings, and for every no-instance the accepted ones, make up at most a 2 ^ (-q(n)) fraction. Nothing is required on instances outside the promise.

theorem Cslib.Complexity.PromiseProblem.SolvesWithBoundedError.repeatMajority {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} {p : Polynomial ℕ} {V : α × List Bool → Bool} (h : SolvesWithBoundedError enc p V Q) (q : Polynomial ℕ) : SolvesWithErrorExponent enc q (12 * q * p) (Complexity.repeatMajority enc (6 * q) p V) Q

Error reduction for bounded error: the majority-vote argument of Arora and Barak, Section 7.4.1, which the book states for languages, applied to promise problems. The strict majority of 12 q(n) runs of a bounded-error solver, on independent blocks of random bits, errs on at most a 2 ^ (-q(n)) fraction of the random strings.

theorem Cslib.Complexity.PromiseProblem.SolvesWithErrorExponent.solvesWithBoundedError {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} {q p : Polynomial ℕ} {V : α × List Bool → Bool} (h : SolvesWithErrorExponent enc q p V Q) (hq : ∀ (n : ℕ), 2 ≤ Polynomial.eval n q) : SolvesWithBoundedError enc p V Q

Error at most 2 ^ (-q(n)) ≤ 1 / 4 is bounded error.

def Cslib.Complexity.DecidesWithErrorExponent {α : Type} (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool) (A : Set α) : Prop

V decides A with error at most 2 ^ (-q(n)), using random strings whose length is p evaluated at the length n of the encoded instance: it solves ofSet A with that error. For every instance a, the random strings r giving the wrong answer, V (a, r) = false for members of A and V (a, r) = true for the others, make up at most a 2 ^ (-q(n)) fraction.

theorem Cslib.Complexity.mem_PromiseBPP_iff_forall_solvesWithErrorExponent {α : Type} {enc : α ↪ List Bool} {Q : PromiseProblem α} : Q ∈ PromiseBPP enc ↔ ∀ (q : Polynomial ℕ), ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ PromiseProblem.SolvesWithErrorExponent enc q p V Q

Error reduction for PromiseBPP, the promise-problem form of the BPP error reduction of Arora and Barak, Section 7.4.1: a promise problem is in PromiseBPP exactly when, for every polynomial q, it is solved in polynomial time with error at most 2 ^ (-q(n)).

theorem Cslib.Complexity.mem_BPP_iff_forall_decidesWithErrorExponent {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ BPP enc ↔ ∀ (q : Polynomial ℕ), ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ DecidesWithErrorExponent enc q p V A

Error reduction for BPP Arora and Barak, Section 7.4.1: a problem is in BPP exactly when, for every polynomial q, it is decided in polynomial time with error at most 2 ^ (-q(n)).

Boolean closure of BPP

theorem Cslib.Complexity.inter_mem_BPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ BPP enc) (hB : B ∈ BPP enc) : A ∩ B ∈ BPP enc

BPP is closed under intersection: reduce the error of both deciders to 2 ^ (-3) = 1 / 8, and accept when both accept on disjoint parts of the random string.

def Cslib.Complexity.BPP.booleanSubalgebra {α : Type} (enc : α ↪ List Bool) : BooleanSubalgebra (Set α)

BPP as a Boolean subalgebra of Set α.

@[simp]

theorem Cslib.Complexity.BPP.coe_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} : ↑(booleanSubalgebra enc) = BPP enc

@[simp]

theorem Cslib.Complexity.BPP.mem_booleanSubalgebra {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ booleanSubalgebra enc ↔ A ∈ BPP enc

theorem Cslib.Complexity.union_mem_BPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ BPP enc) (hB : B ∈ BPP enc) : A ∪ B ∈ BPP enc

BPP is closed under union.

theorem Cslib.Complexity.diff_mem_BPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ BPP enc) (hB : B ∈ BPP enc) : A \ B ∈ BPP enc

BPP is closed under set difference.

theorem Cslib.Complexity.symmDiff_mem_BPP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ BPP enc) (hB : B ∈ BPP enc) : symmDiff A B ∈ BPP enc

BPP is closed under symmetric difference.