Lax Lean Archive

Fully polynomial-time approximation schemes

Lax213208.FPTAS · concepts/Lax213208/FPTAS.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 FPTAS has ratio 1+ε1+\varepsilon, with ε=1/k\varepsilon=1/k, in time polynomial in both instance size and kk. The constants and exponents are independent of the instance and 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
    3
    4/-!
    5---
    6title: Fully polynomial-time approximation schemes
    7type: definition
    8---
    9An FPTAS has ratio 1+ε1+\varepsilon, with ε=1/k\varepsilon=1/k, in time
    10polynomial in both instance size and kk. The constants and exponents
    11are independent of the instance and precision.
    12-/
    13
    14namespace Lax213208.FPTAS
    15
    16open OptimizationProblem Programs RApproximation RunningTime
    17
    18variable {Instance Solution : Type*} {problem : Problem Instance Solution}
    19
    20def FPTAS (alg : Program) (inputs : Set Instance) : Prop :=
    21 ∃ c d e : ℕ, 0 < c ∧ 0 < d ∧ 0 < e ∧
    22 ∀ k : ℕ, 0 < k →
    23 let ε : ℝ := 1 / k
    24 Approximates (problem := problem) alg inputs (1 + ε) (some k) ∧
    25 RunsInTime (problem := problem) alg inputs
    26 (fun n => c * (n + 2) ^ d * (k + 1) ^ e) (some k)
    27
    28end Lax213208.FPTAS
    29
    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…