Lax Lean Archive

The complexity class BPP

Lax666725.RandomizedPolynomialTime · concepts/Lax666725/RandomizedPolynomialTime.lean · lax-666725

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A binary language belongs to BPP\mathrm{BPP} if a probabilistic Turing machine, running in polynomial time on every branch, answers correctly with probability at least 2/32/3 on every input. Both false acceptance and false rejection are allowed, each with probability at most 1/31/3 on the corresponding inputs. Languages are exactly those of Lax434930.PolynomialTime.LanguageLax434930.PolynomialTime.Language.

    Concept map
    3 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax666725.ProbabilisticMachines
    2
    3/-!
    4---
    5title: The complexity class BPP
    6type: definition
    7---
    8A binary language belongs to BPP\mathrm{BPP} if a probabilistic Turing
    9machine, running in polynomial time on every branch, answers correctly
    10with probability at least 2/32/3 on every input. Both false acceptance and
    11false rejection are allowed, each with probability at most 1/31/3 on the
    12corresponding inputs. Languages are exactly those of
    13`Lax434930.PolynomialTime.Language`.
    14-/
    15
    16namespace Lax666725.RandomizedPolynomialTime
    17
    18open Lax434930.PolynomialTime ProbabilisticMachines
    19
    20def BPP : Set Language :=
    21 {L | ∃ A : Procedure Bool, ∀ x, (2 / 3 : ℚ) ≤ A.probability x (Correct L x)}
    22
    23end Lax666725.RandomizedPolynomialTime
    24
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…