Prove2Me

§4.1, p. 560 — expected cost of a lock wait: π(τ)C+∫0τ(1−π(t)) dt\pi(\tau)C+\int_0^\tau(1-\pi(t))\,dt

Proved
NonuniformCompetitive.SpinBlock.expected_wait_cost

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

competitive-analysislayer-cakep2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1spin-block

Let C>0C>0 be the context-switch cost, and let the blocking time b∈[0,∞]b\in[0,\infty] of an algorithm be random with law ν\nu, a probability measure on [0,∞][0,\infty]. Write π(t)=ν{b<t}\pi(t)=\nu\{b<t\} for the probability that the algorithm blocks before time tt. For a lock released at time τ≥0\tau\ge0, the expected cost of the wait is

E waitCostC(b,τ)=π(τ)⋅C+∫0τ(1−π(t)) dt,\mathbf{E}\,\mathrm{waitCost}_C(b,\tau)=\pi(\tau)\cdot C+\int_0^\tau\big(1-\pi(t)\big)\,dt ,

where 1−π(t)=ν{b≥t}1-\pi(t)=\nu\{b\ge t\} is the probability that the process is still spinning at time tt. The first term is the expected cost of blocking and the second the expected cost of spinning.

The identity reduces the competitive analysis of a randomized spin-block algorithm on a single lock wait to a one-dimensional computation with its distribution function; the paper applies it to its particular distribution π\pi.

Formalization Note The identity is stated for every blocking law ν\nu, not only the paper's π\pi, exactly as the paper's explanation of its two terms applies. Both sides are in [0,∞][0,\infty]; the integral is a lower Lebesgue integral over (0,τ](0,\tau], so no integrability hypothesis is needed. The convention that a tie b=τb=\tau costs τ\tau is what makes π(τ)=ν{b<τ}\pi(\tau)=\nu\{b<\tau\} (strict) and 1−π(t)=ν{b≥t}1-\pi(t)=\nu\{b\ge t\} the right sets.

Preamble
import Mathlib
import Definitions.Def_NonuniformCompetitive_SpinBlock_Model

open scoped NNReal ENNReal
open MeasureTheory
Formal statement
namespace NonuniformCompetitive.SpinBlock

/-- §4.1, p. 560, the expected-cost display: if the blocking time `b` of an algorithm has law `ν`
(a probability measure on `[0, ∞]`) and the lock is released at time `τ`, the expected cost is
`π(τ) · C + ∫₀^τ (1 − π(t)) dt`, where `π(τ) = ν{b < τ}` is the probability of blocking before `τ`
and `1 − π(t) = ν{b ≥ t}` is the probability of still spinning at time `t`. -/
theorem expected_wait_cost (C : ℝ) (hC : 0 < C) (ν : Measure ℝ≥0∞) [IsProbabilityMeasure ν]
    (τ : ℝ≥0) :
    ∫⁻ b, waitCost C b τ ∂ν =
      ν (Set.Iio (τ : ℝ≥0∞)) * ENNReal.ofReal C +
        ∫⁻ t in Set.Ioc (0 : ℝ) τ, ν (Set.Ici (ENNReal.ofReal t)) := 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 E C_A(σ_τ)
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