Approximation ratio

Conjectura.Defs.ComputerScience.Algorithms.ApproximationRatio

/-
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
-/
import Mathlib.Analysis.SpecialFunctions.Pow.Real

/-! # Approximation ratio -/

namespace Conjectura.Algorithms

/-- 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 i

end Conjectura.Algorithms