Approximation ratio
HasApproximationRatiodef
An algorithm achieves approximation ratio ρ when, on every instance, the cost of its output is within a factor ρ of the optimum. Whether a given problem admits a given ratio is often open even when the problem itself is well understood.
def HasApproximationRatio {I S : Type*}
(alg : I → S) (cost : I → S → ℝ) (opt : I → ℝ) (ρ : ℝ) : Prop :=
∀ i : I, cost i (alg i) ≤ ρ * opt iFrom Mathlib
import Conjectura.Defs.ComputerScience.Algorithms.ApproximationRatio · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors