Lax Lean Archive

Polynomial-time approximation schemes

Lax213208.PTAS · concepts/Lax213208/PTAS.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 PTAS has approximation ratio 1+ε1+\varepsilon and polynomial running time for every fixed ε=1/k\varepsilon=1/k, where kk is a positive integer. One program handles all precisions.

    Concept map
    14 concepts
    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: Polynomial-time approximation schemes
    7type: definition
    8---
    9A PTAS has approximation ratio 1+ε1+\varepsilon and polynomial running
    10time for every fixed ε=1/k\varepsilon=1/k, where kk is a positive integer.
    11One program handles all precisions.
    12-/
    13
    14namespace Lax213208.PTAS
    15
    16open OptimizationProblem Programs RApproximation RunningTime
    17
    18variable {Instance Solution : Type*} {problem : Problem Instance Solution}
    19
    20def PTAS (alg : Program) (inputs : Set Instance) : Prop :=
    21 ∀ k : ℕ, 0 < k →
    22 let ε : ℝ := 1 / k
    23 Approximates (problem := problem) alg inputs (1 + ε) (some k) ∧
    24 PolynomialTime (problem := problem) alg inputs (some k)
    25
    26end Lax213208.PTAS
    27
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…