Lax Lean Archive

Approximation guarantees

Lax213208.RApproximation · concepts/Lax213208/RApproximation.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 program approximates within r≥1r\ge1 if it returns a feasible rr-approximate solution on every instance in the class. This requires termination, with no restriction on running time.

    The optional integer precision selects the scheme input convention. Both ordinary algorithms and schemes use this same predicate.

    Concept map
    12 concepts; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax213208.Approximation
    2import Lax213208.AlgorithmInput
    3import Lax213208.Programs
    4
    5/-!
    6---
    7title: Approximation guarantees
    8type: definition
    9---
    10A program approximates within r≥1r\ge1 if it returns a feasible
    11rr-approximate solution on every instance in the class. This requires
    12termination, with no restriction on running time.
    13
    14The optional integer precision selects the scheme input convention. Both ordinary
    15algorithms and schemes use this same predicate.
    16-/
    17
    18namespace Lax213208.RApproximation
    19
    20open OptimizationProblem Approximation AlgorithmInput Programs
    21
    22variable {Instance Solution : Type*} {problem : Problem Instance Solution}
    23
    24def Approximates (alg : Program) (inputs : Set Instance) (r : ℝ)
    25 (precision : Option ℕ := none) : Prop :=
    26 1 ≤ r ∧ ∀ x ∈ inputs, ∃ y,
    27 Returns alg (inputTape problem precision x) (problem.output y) ∧
    28 IsApproximation problem r x y
    29
    30end Lax213208.RApproximation
    31
    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…