Lax Lean Archive

Approximate and optimal solutions

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

    For r≥1r\ge1, an rr-approximate solution is feasible and has value at most r OPTr\,\mathrm{OPT} for minimization, or at least OPT/r\mathrm{OPT}/r for maximization. Comparison with every feasible solution avoids division by zero and does not require an attained optimum.

    An optimal value, when needed, is the value of an attained optimum.

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

    Lean source view on GitHub

    1import Lax213208.OptimizationProblem
    2
    3/-!
    4---
    5title: Approximate and optimal solutions
    6type: definition
    7---
    8For r≥1r\ge1, an rr-approximate solution is feasible and has value at most
    9r OPTr\,\mathrm{OPT} for minimization, or at least OPT/r\mathrm{OPT}/r for
    10maximization. Comparison with every feasible solution avoids division by
    11zero and does not require an attained optimum.
    12
    13An optimal value, when needed, is the value of an attained optimum.
    14-/
    15
    16namespace Lax213208.Approximation
    17
    18open OptimizationProblem
    19
    20variable {Instance Solution : Type*}
    21
    22def IsApproximation (problem : Problem Instance Solution)
    23 (r : ℝ) (x : Instance) (y : Solution) : Prop :=
    24 1 ≤ r ∧ problem.feasible x y ∧ ∀ z, problem.feasible x z →
    25 match problem.direction with
    26 | .minimize => (problem.value x y : ℝ) ≤ r * problem.value x z
    27 | .maximize => (problem.value x z : ℝ) ≤ r * problem.value x y
    28
    29def IsOptimalValue (problem : Problem Instance Solution)
    30 (x : Instance) (value : ℝ) : Prop :=
    31 ∃ y, IsApproximation problem 1 x y ∧ (problem.value x y : ℝ) = value
    32
    33end Lax213208.Approximation
    34
    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…