Lax Lean Archive

Efficient polynomial-time approximation schemes

Lax213208.EPTAS · concepts/Lax213208/EPTAS.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

    An EPTAS has ratio 1+ε1+\varepsilon, with ε=1/k\varepsilon=1/k, in time f(k)(n+2)df(k)(n+2)^d, where ff is computable and the exponent dd is independent of precision.

    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
    3import Mathlib.Computability.Partrec
    4
    5/-!
    6---
    7title: Efficient polynomial-time approximation schemes
    8type: definition
    9---
    10An EPTAS has ratio 1+ε1+\varepsilon, with ε=1/k\varepsilon=1/k, in time
    11f(k)(n+2)df(k)(n+2)^d, where ff is computable and the exponent dd is
    12independent of precision.
    13-/
    14
    15namespace Lax213208.EPTAS
    16
    17open OptimizationProblem Programs RApproximation RunningTime
    18
    19variable {Instance Solution : Type*} {problem : Problem Instance Solution}
    20
    21def EPTAS (alg : Program) (inputs : Set Instance) : Prop :=
    22 ∃ f : ℕ → ℕ, Computable f ∧ (∀ k > 0, 0 < f k) ∧
    23 ∃ d : ℕ, 0 < d ∧ ∀ k : ℕ, 0 < k →
    24 let ε : ℝ := 1 / k
    25 Approximates (problem := problem) alg inputs (1 + ε) (some k) ∧
    26 RunsInTime (problem := problem) alg inputs
    27 (fun n => f k * (n + 2) ^ d) (some k)
    28
    29end Lax213208.EPTAS
    30
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…