Competitive ratio
IsCompetitivedef
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 + bFrom Mathlib
import Conjectura.Defs.ComputerScience.Algorithms.CompetitiveRatio · 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