Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Bounded-error randomized approximation of the clique number

Lax253009.RandomizedApproximation · concepts/Lax253009/RandomizedApproximation.lean · lax-253009

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 randomized polynomial-time approximation has a polynomial-length tape of independent fair bits and a deterministic polynomial-time evaluator in the registered stack-machine model. On every nonempty graph it returns an integer satisfying both approximation inequalities with probability at least 2/32/3. Its answer on the remaining tapes is unrestricted.

    The input to the evaluator is the registered pairing of the graph encoding and the random tape. Both the machine and the polynomial are uniform and chosen before the input graph. The tape has polynomial length in the graph encoding, so the total runtime is polynomial in that encoding. Integer outputs are binary words on the output stack and need not have bounded size.

    Concept map
    6 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax253009.Approximation
    2import Lax253009.FiniteProbability
    3import Lax434930.Certificates
    4
    5/-!
    6---
    7title: Bounded-error randomized approximation of the clique number
    8type: definition
    9---
    10A randomized polynomial-time approximation has a polynomial-length tape of
    11independent fair bits and a deterministic polynomial-time evaluator in the
    12registered stack-machine model. On every nonempty graph it returns an
    13integer satisfying both approximation inequalities with probability at least
    142/32/3. Its answer on the remaining tapes is unrestricted.
    15
    16The input to the evaluator is the registered pairing of the graph encoding
    17and the random tape. Both the machine and the polynomial are uniform and
    18chosen before the input graph. The tape has polynomial length in the graph
    19encoding, so the total runtime is polynomial in that encoding. Integer
    20outputs are binary words on the output stack and need not have bounded size.
    21-/
    22
    23namespace Lax253009.RandomizedApproximation
    24
    25open Graphs FiniteProbability Lax434930.PolynomialTime
    26
    27def Good {n : ℕ} (ε : ℝ) (G : Graph n) (a : ℕ) : Prop :=
    28 a ≤ G.cliqueNumber ∧
    29 (G.cliqueNumber : ℝ) ≤ Real.rpow (n : ℝ) (1 - ε) * (a : ℝ)
    30
    31def Approximable (ε : ℝ) : Prop :=
    32 ∃ (coins : Polynomial ℕ) (estimate : Word → ℕ),
    33 Nonempty (Turing.TM2ComputableInPolyTime id Computability.encodeNat estimate) ∧
    34 ∀ (n : ℕ), 0 < n → ∀ G : Graph n,
    35 (2 / 3 : ℝ) ≤ probability (fun r : Fin (coins.eval G.encode.length) → Bool ↦
    36 Good ε G (estimate (Lax434930.Certificates.pair G.encode (List.ofFn r))))
    37
    38end Lax253009.RandomizedApproximation
    39
    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…