Prove2Me

§4.1, p. 560 — with π(t)=(et/C−1)/(e−1)\pi(t)=(e^{t/C}-1)/(e-1) the expected wait cost is within e/(e−1)e/(e-1) of min⁡(τ,C)\min(\tau,C)

Proved
NonuniformCompetitive.SpinBlock.blockCDF_ratio

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

competitive-analysisp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1spin-block

Let C>0C>0 and let

π(t)={et/C−1e−1,0≤t≤C,1,t>C.\pi(t)=\begin{cases}\dfrac{e^{t/C}-1}{e-1}, & 0\le t\le C,\\[1ex] 1, & t>C.\end{cases}

The optimal off-line cost of a single lock released at time τ\tau is Copt(στ)=τC_{opt}(\sigma_\tau)=\tau for 0≤τ≤C0\le\tau\le C and CC for τ>C\tau>C, that is min⁡(τ,C)\min(\tau,C). Then for every τ≥0\tau\ge0,

π(τ)⋅C+∫0τ(1−π(t)) dt  ≤  ee−1 min⁡(τ,C).\pi(\tau)\cdot C+\int_0^\tau\big(1-\pi(t)\big)\,dt\;\le\;\frac{e}{e-1}\,\min(\tau,C).

Combined with the expected-cost identity, this is the paper's statement that the randomized algorithm with blocking distribution π\pi "is competitive within factor e/(e−1)e/(e-1)" on every single lock wait.

Formalization Note The integral is the real interval integral; its integrand 1−π1-\pi is continuous on [0,τ][0,\tau], so it is a genuine integral. The inequality holds in fact with equality for every τ≥0\tau\ge0; the statement keeps the paper's "within factor" form.

Preamble
import Mathlib
import Definitions.Def_NonuniformCompetitive_SpinBlock_blockCDF
Formal statement
namespace NonuniformCompetitive.SpinBlock

/-- §4.1, p. 560: substituting the paper's `π` into `E C_A(σ_τ) = π(τ) · C + ∫₀^τ (1 − π(t)) dt`
gives at most `e/(e − 1)` times the off-line cost `C_opt(σ_τ) = min(τ, C)`, for every release
time `τ ≥ 0`. -/
theorem blockCDF_ratio (C : ℝ) (hC : 0 < C) (τ : ℝ) (hτ : 0 ≤ τ) :
    blockCDF C τ * C + ∫ t in (0 : ℝ)..τ, (1 - blockCDF C t) ≤
      Real.exp 1 / (Real.exp 1 - 1) * min τ C := by sorry

end NonuniformCompetitive.SpinBlock
Source
Karlin, Manasse, McGeoch, Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), p. 560, §4.1, proof of Theorem 10, display for C_opt(σ_τ) and the sentence following it
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph