Tight weighted paging with delay via mirror descent
Julian Born, Yann Disser, Linda Thelen
cs.DS
Oct 17, 2026 · v2
TL;DR
The main competitive-ratio theorem is formalized in Lean 4, assuming only the BBN07 online rounding, with a public repository; the Lean code was written by Claude Opus under author guidance.
Abstract
We give an O(log k)-competitive randomized algorithm for weighted paging with delay. This improves upon the O(log k log n)-competitive algorithm of Gupta, Kumar, and Panigrahi (STOC 2020, SICOMP 2022) by removing the dependence on the number n of pages. Without delay, the optimal competitive ratio of randomized algorithms is Theta(log k), and since the lower bound carries over, our bound is tight. Our algorithm is fractional and combines mirror descent, used by Bubeck et al. (STOC 2018) for weighted paging without delay, with preemptive service, introduced by Azar et al. (STOC 2017) for online service with delay: when a request is served, an increase in the mirror descent potential is offset by preemptive service to other pending requests, with a budget derived from the mirror descent path. To obtain a randomized algorithm, we use the online rounding of Bansal, Buchbinder, and Naor (FOCS 2007) from classical paging.
Problem
Weighted paging with delay previously had an O(log k log n)-competitive randomized algorithm. This leaves a gap to the Theta(log k) lower bound inherited from classical weighted paging.
Approach
The algorithm, Preemptive Mirror Descent (PMD), is fractional. It combines mirror descent with preemptive service: when a request is served, the increase in the mirror descent potential is offset by serving other pending requests, using budgets derived from the mirror descent path. The analysis uses a Bregman divergence potential and charging arguments against Opt. The fractional algorithm is made randomized via the online rounding of Bansal, Buchbinder, and Naor. The main theorem is verified in Lean 4 with exact constants; the formalization was written by Claude Opus and the authors checked the Lean model.
Results
The algorithm is O(log k)-competitive for weighted paging with delay, which is tight, independent of n, and also applies to deadlines. The Lean verification assumes only the BBN07 rounding procedure.
