Bounded-error probabilistic classes RP and BPP

TheoremBPP is contained in PSPACE#●ready to prove

Every decision problem in BPP lies in PSPACE.

public theorem_wanted bpp_subset_pspace :
    BPP ⊆ PSPACE

def BPP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 * 2 ^ (p.eval x.length)) ∧
      (L x = false →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≤
          2 ^ (p.eval x.length))}

CSLibExt/Computability/Complexity/Classes.lean:199

def PSPACE : DecisionComplexityClass :=
  {L | langOf L ∈ Cslib.Turing.MultiTapeTM.Classes.PSPACE}

CSLibExt/Computability/Complexity/Classes.lean:117

Sources

S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009 (BPP ⊆ PSPACE).

Uses 4

Statement usesBPP · Polynomial space for decision problems · Complexity classes · Decision problems

TheoremRP is contained in BPP#●ready to prove

Every decision problem in the class \(\mathsf{RP}\) of one-sided-error randomized polynomial-time decision problems also belongs to the class \(\mathsf{BPP}\) of bounded-error probabilistic polynomial-time decision problems.

public theorem_wanted rp_subset_bpp :
    RP ⊆ BPP

def RP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        2 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 ^ (p.eval x.length)) ∧
      (L x = false →
        Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} = 0)}

CSLibExt/Computability/Complexity/Classes.lean:594

def BPP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 * 2 ^ (p.eval x.length)) ∧
      (L x = false →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≤
          2 ^ (p.eval x.length))}

CSLibExt/Computability/Complexity/Classes.lean:199

Sources

S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 7 (error reduction for RP); M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Theorem 10.13 (RP ⊆ BPP via amplification).

Uses 4

Statement usesBPP · The class RP · Complexity classes · Decision problems

TheoremRP is contained in NP#●ready to prove

Every decision problem in the class \(\mathsf{RP}\) of one-sided-error randomized polynomial-time decision problems also belongs to the class \(\mathsf{NP}\).

public theorem_wanted rp_subset_np :
    RP ⊆ NP

def RP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        2 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 ^ (p.eval x.length)) ∧
      (L x = false →
        Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} = 0)}

CSLibExt/Computability/Complexity/Classes.lean:594

def NP : DecisionComplexityClass :=
  { L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
      IsPolyTime R ∧
      ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }

MathlibExt/Computability/Complexity.lean:200

Sources

S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 7.3 (RP ⊆ NP); M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Theorem 10.13.

Uses 4

Statement usesThe class RP · Complexity classes · Decision problems · The complexity class NP

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.