Prove2Me

§5, pp. 565–566 — every feasible point of the 1-d-d phase LP has α≥(e2d−1+1/4d)/((e2d−1−1)+1/2d)\alpha\ge(e_{2d-1}+1/4d)/((e_{2d-1}-1)+1/2d)

Proved
NonuniformCompetitive.Isosceles.lp_lower_bound

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

competitive-analysislinear-programmingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let d≥1d\ge1 be an integer, let π1,…,π2d−1\pi_1,\dots,\pi_{2d-1} be arbitrary real numbers and let α\alpha be a real number. Suppose the phase constraints of the two-server problem on the 11-dd-dd isosceles triangle hold:

(πk) 2d+∑i=1k(1−πi)≤α⋅k(1≤k<2d),(\pi_k)\,2d+\sum_{i=1}^{k}(1-\pi_i)\le\alpha\cdot k\qquad(1\le k<2d), 2d+∑i=12d−1(1−πi)+12≤α⋅2d.2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot 2d.

Then

α≥e2d−1+1/4d(e2d−1−1)+1/2d,e2d−1=(2d2d−1)2d−1.\alpha\ge\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.

In the paper, πk\pi_k is the probability that a phase-based on-line algorithm covers both aa and bb after the kk-th request of a phase of alternating requests to aa and bb; the left-hand sides are its expected costs on the phase σk\sigma_k (the kk alternating requests, then a request at cc and possibly one more at aa or bb), and kk, resp. 2d2d, is the optimal off-line cost of that phase. The statement says that no choice of the πk\pi_k gives an LP bound below the ratio of Theorem 12; together with the paper's Theorem 3 this is the lower-bound half of Theorem 12.

Formalization Note The πk\pi_k are free real variables, as in the paper ("we permit the πk\pi_k to be free variables"); no constraint 0≤πk≤10\le\pi_k\le1 is imposed, which makes the statement stronger. π\pi is a function N→R\mathbb N\to\mathbb R whose values at 00 and at indices ≥2d\ge 2d are unused.

Preamble
import Mathlib
import Definitions.Def_NonuniformCompetitive_Isosceles_isoscelesRatio
Formal statement
namespace NonuniformCompetitive.Isosceles

/-- §5, pp. 565–566 (Karlin–Manasse–McGeoch–Owicki 1994): the phase LP for the two-server problem
on the `1`-`d`-`d` isosceles triangle. For `1 ≤ d`, any real numbers `π 1, …, π (2d-1)` (free,
not restricted to `[0,1]`) and any `α` satisfying the `2d` phase constraints
* `2d · π_k + ∑_{i=1}^{k} (1 - π_i) ≤ α · k` for `1 ≤ k < 2d`, and
* `2d + ∑_{i=1}^{2d-1} (1 - π_i) + 1/2 ≤ α · 2d`,
have `α ≥ (e_{2d-1} + 1/(4d)) / ((e_{2d-1} - 1) + 1/(2d))`.
The values of `π` at `0` and at indices `≥ 2d` are unused. -/
theorem lp_lower_bound (d : ℕ) (hd : 1 ≤ d) (π : ℕ → ℝ) (α : ℝ)
    (hlt : ∀ k : ℕ, 1 ≤ k → k < 2 * d →
      π k * (2 * d : ℝ) + ∑ i ∈ Finset.Icc 1 k, (1 - π i) ≤ α * (k : ℝ))
    (hge : (2 * d : ℝ) + ∑ i ∈ Finset.Icc 1 (2 * d - 1), (1 - π i) + 1 / 2 ≤ α * (2 * d : ℝ)) :
    isoscelesRatio d ≤ α := by sorry

end NonuniformCompetitive.Isosceles
Source
Karlin, Manasse, McGeoch, Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), DOI 10.1007/BF01189993, pp. 565–566, §5, proof of Theorem 12: the constraint system on p. 565 and the displayed bound for α\alpha on p. 566
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