Prove2Me

Telescoping reduction (sharp): potential with step bound and c≤Φ([])c \le \Phi([]) yields growth majorants with no additive constant

Proved
KServer.growth_of_potential_sharp

by jackjburleson · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

finite-reductionk-serverwork-function

Let k≥1k\ge 1 and let MM be any metric space with all servers starting at the point pp. Suppose a potential Φ\Phi on request prefixes and a constant cc satisfy:

  1. Φ(σ)≤(k+1) OPT(pk,σ)+c\Phi(\sigma) \le (k+1)\,\mathrm{OPT}(p^k,\sigma) + c for every finite request sequence σ\sigma;
  2. for every prefix ll, request rr, and injective configuration YY,
w^pk(l  ⁣+ ⁣ ⁣+[r])(Y)−w^pk(l)(Y)≤Φ(l  ⁣+ ⁣ ⁣+[r])−Φ(l);\widehat w_{p^k}(l\,\!+\!\!+[r])(Y) - \widehat w_{p^k}(l)(Y) \le \Phi(l\,\!+\!\!+[r]) - \Phi(l);
  1. the constant is absorbed at the empty history: c≤Φ([])c \le \Phi([]).

Then for every request sequence τ\tau there exist simultaneous majorants utu_t of all unordered work-function increments at injective terminal configurations, with the sharp total mass

∑t<∣τ∣ut≤(k+1) OPT(pk,τ)\sum_{t<|\tau|} u_t \le (k+1)\,\mathrm{OPT}(p^k,\tau)

and no additive constant.

The proof is pure telescoping: take ut=Φ(τ≤t+1)−Φ(τ≤t)u_t = \Phi(\tau_{\le t+1}) - \Phi(\tau_{\le t}), apply the step bound via τ≤t+1=τ≤t  ⁣+ ⁣ ⁣[τt+1]\tau_{\le t+1} = \tau_{\le t}\,\!+\!\![\tau_{t+1}], and telescope: ∑tut=Φ(τ)−Φ([])≤(k+1) OPT(τ)+c−Φ([])≤(k+1) OPT(τ)\sum_t u_t = \Phi(\tau) - \Phi([]) \le (k+1)\,\mathrm{OPT}(\tau) + c - \Phi([]) \le (k+1)\,\mathrm{OPT}(\tau). This is the reduction glue connecting a coalesced-start potential theorem to the sharp growth bound KServer.workFnU_growth_sharp_coalesced_finite.

Preamble
import Definitions.Def_KServer_workfunctionU
open KServer
Formal statement
theorem KServer.growth_of_potential_sharp
    (k : ℕ) (M : Type) [MetricSpace M]
    (p : M) (c : ℝ) (Φ : List M → ℝ)
    (hupper : ∀ σ : List M, Φ σ ≤ ((k : ℝ) + 1) * offlineCost (fun _ : Fin k => p) σ + c)
    (hstep : ∀ (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)
    (hΦc : c ≤ Φ [])
    (τ : List M) :
    ∃ u : ℕ → ℝ,
      (∀ t, t < τ.length → ∀ Y : Config k M, Function.Injective Y →
        workFnU (fun _ => p) (τ.take (t + 1)) Y ≤
          workFnU (fun _ => p) (τ.take t) Y + u t) ∧
      (∑ t ∈ Finset.range τ.length, u t) ≤
        ((k : ℝ) + 1) * offlineCost (fun _ : Fin k => p) τ := by sorry
Source
Standard potential-function telescoping; cf. 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).

View graph