Potential function with sharp $(k+1)$ upper bound and work-function step bound (coalesced start, finite metric)

Open

KServer.potential_coalesced_k_ge3_finite

by jackjburleson · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

competitive-analysisfinite-metrick-serverwork-function

Let $k\ge 3$ , let $M$ be a finite metric space, and place all $k$ servers initially at the single point $p$ (coalesced start). Then there exists a potential function $\Phi$ on request prefixes and a constant $c\ge 0$ with $\Phi([])\le 0$ such that:

Upper bound: for every finite request sequence $\sigma$ , $\Phi(\sigma) \le (k+1)\,\mathrm{OPT}(p^k,\sigma) + c$ , where $\mathrm{OPT}$ is the offline cost (offlineCost).
Step bound: for every prefix $l$ , request $r$ , and injective terminal configuration $Y$ , the unordered work function increment satisfies

\widehat w_{p^k}(l\,\!+\!\!+[r])(Y) - \widehat w_{p^k}(l)(Y) \le \Phi(l\,\!+\!\!+[r]) - \Phi(l).

This is the key missing ingredient for the sharp coalesced growth bound KServer.workFnU_growth_sharp_coalesced_finite: together with the telescoping reduction (KServer.growth_of_potential_coalesced), it yields majorants $u_t$ with $\sum_t u_t \le (k+1)\,\mathrm{OPT}$ and no additive constant. It generalizes KServer.workFnU_sharp_potential_known_cases (which covers $k\le 2$ or $|M|\le k+2$ ) to the remaining cases, which are exactly the open ones in E. Koutsoupias, The k-server problem (2009), Section 3.4, and Y. Emek, P. Fraigniaud, A. Korman, A. Rosen, On the Additive Constant of the k-server Work Function Algorithm (2009), Section 3.

Preamble

import Definitions.Def_KServer_workfunctionU
open KServer

Formal statement

theorem KServer.potential_coalesced_k_ge3_finite
    (k : ℕ) (hk : 3 ≤ k) (M : Type) [MetricSpace M] [Fintype M]
    (p : M) :
    ∃ Φ : List M → ℝ, ∃ c : ℝ,
      (∀ σ : List M, Φ σ ≤ ((k : ℝ) + 1) * offlineCost (fun _ : Fin k => p) σ + c) ∧
      (∀ (l : List M) (r : M) (Y : Config k M), Function.Injective Y →
        workFnU (fun _ => p) (l ++ [r]) Y - workFnU (fun _ => p) l Y ≤
          Φ (l ++ [r]) - Φ l) ∧
      (0 ≤ c ∧ Φ [] ≤ 0) := by sorry

Source

Proposed potential-form of the open sharp extended-cost criterion in E. Koutsoupias, The k-server problem (2009), Section 3.4, https://users.cs.fiu.edu/~giri/teach/6936/S10/K-Server_CSReviews_09.pdf, equation (6); cf. Y. Emek, P. Fraigniaud, A. Korman and A. Rosen, On the Additive Constant of the k-server Work Function Algorithm (2009), Section 3, https://arxiv.org/pdf/0902.1378.

View graph

Potential function with sharp (k+1)(k+1)(k+1) upper bound and work-function step bound (coalesced start, finite metric)

Potential function with sharp $(k+1)$ upper bound and work-function step bound (coalesced start, finite metric)