Bounded-error quantum polynomial time (BQP)
TheoremBQP is contained in PP#●ready to prove
MetaMathlibExt.Complexity.KeyTheorems.BQPSubsetPP.bqp_subset_pp
Every decision problem in BQP lies in PP.
public theorem_wanted bqp_subset_pp :
BQP ⊆ PPdef BQP : DecisionComplexityClass :=
{L | ∃ a s : Polynomial ℕ, ∃ gates : List Bool → List QGate,
IsPolyTime gates ∧
(∀ x, (gates x).length ≤ s.eval x.length) ∧
(∀ x, ∀ g ∈ gates x, QGateWellFormed (x.length + a.eval x.length) g) ∧
∀ x,
(L x = true →
2 / 3 ≤ acceptProb
(applyCircuit (x.length + a.eval x.length) (gates x)
(bqpInitState x (a.eval x.length)))) ∧
(L x = false → acceptProb
(applyCircuit (x.length + a.eval x.length) (gates x)
⋯CSLibExt/Computability/Complexity/Classes.lean:893
def PP : 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 →
2 * 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:211
Sources
Sources
- E. Bernstein and U. Vazirani, "Quantum complexity theory", SIAM Journal on Computing 26 (1997), 1411-1473 (BQP ⊆ PP); L. Adleman, J. DeMarrais, and M.-D. Huang, "Quantum computability", SIAM Journal on Computing 26 (1997), 1524-1540; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 10.2.
Uses 4
Statement usesBQP · Probabilistic polynomial time with unbounded error · Complexity classes · Decision problems
TheoremBQP is contained in PSPACE#●ready to prove
MetaMathlibExt.Complexity.KeyTheorems.BQPSubsetPSPACE.bqp_subset_pspace
Every decision problem in BQP, the class of bounded-error quantum polynomial-time decision problems, lies in PSPACE, the class of decision problems decidable in polynomial space.
public theorem_wanted bqp_subset_pspace :
BQP ⊆ PSPACEdef BQP : DecisionComplexityClass :=
{L | ∃ a s : Polynomial ℕ, ∃ gates : List Bool → List QGate,
IsPolyTime gates ∧
(∀ x, (gates x).length ≤ s.eval x.length) ∧
(∀ x, ∀ g ∈ gates x, QGateWellFormed (x.length + a.eval x.length) g) ∧
∀ x,
(L x = true →
2 / 3 ≤ acceptProb
(applyCircuit (x.length + a.eval x.length) (gates x)
(bqpInitState x (a.eval x.length)))) ∧
(L x = false → acceptProb
(applyCircuit (x.length + a.eval x.length) (gates x)
⋯CSLibExt/Computability/Complexity/Classes.lean:893
def PSPACE : DecisionComplexityClass :=
{L | langOf L ∈ Cslib.Turing.MultiTapeTM.Classes.PSPACE}CSLibExt/Computability/Complexity/Classes.lean:117
Sources
Sources
- E. Bernstein and U. Vazirani, "Quantum complexity theory", SIAM Journal on Computing 26 (1997), 1411-1473 (BQP ⊆ PSPACE); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Theorem 10.2.
Uses 4
Statement usesBQP · Polynomial space for decision problems · Complexity classes · Decision problems
2 ready to prove
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.