Lax Lean Archive

Quasipolynomial-time approximation schemes

Lax213208.QPTAS · concepts/Lax213208/QPTAS.lean · lax-213208

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 QPTAS has approximation ratio 1+ε1+\varepsilon and quasipolynomial running time for every fixed ε=1/k\varepsilon=1/k, where kk is a positive integer.

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

    Lean source view on GitHub

    1import Lax213208.RApproximation
    2import Lax213208.RunningTime
    3
    4/-!
    5---
    6title: Quasipolynomial-time approximation schemes
    7type: definition
    8---
    9A QPTAS has approximation ratio 1+ε1+\varepsilon and quasipolynomial
    10running time for every fixed ε=1/k\varepsilon=1/k, where kk is a positive integer.
    11-/
    12
    13namespace Lax213208.QPTAS
    14
    15open OptimizationProblem Programs RApproximation RunningTime
    16
    17variable {Instance Solution : Type*} {problem : Problem Instance Solution}
    18
    19def QPTAS (alg : Program) (inputs : Set Instance) : Prop :=
    20 ∀ k : ℕ, 0 < k →
    21 let ε : ℝ := 1 / k
    22 Approximates (problem := problem) alg inputs (1 + ε) (some k) ∧
    23 QuasipolynomialTime (problem := problem) alg inputs (some k)
    24
    25end Lax213208.QPTAS
    26
    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…