Competitive ratio

Conjectura.Defs.ComputerScience.Algorithms.CompetitiveRatio

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

/-! # Competitive ratio -/

namespace Conjectura.Algorithms

/-- An online algorithm is **c-competitive** when its cost on every request sequence is within
a factor `c` of the best offline cost, up to an additive constant. The online analogue of
`HasApproximationRatio`, with the constant absorbing start-up effects. -/
def IsCompetitive {R S : Type*}
    (alg : R → S) (cost : R → S → ℝ) (offlineOpt : R → ℝ) (c : ℝ) : Prop :=
  ∃ b : ℝ, ∀ r : R, cost r (alg r) ≤ c * offlineOpt r + b

end Conjectura.Algorithms