Prove2Me

Proof of Theorem 8.3 — the extreme points of P1 are the n! vectors v(π), and P1 is their convex hull

Proved
MulticlassQNet.SingleStation.proof_8_3_extreme_points

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

extreme-pointsp2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1polymatroidqueueing-network

Consider the multiclass single-server queue with classes E={1,…,n}E=\{1,\dots,n\}, arrival rates λi>0\lambda_i>0, service rates μi>0\mu_i>0 and load ∑i∈Eλi/μi<1\sum_{i\in E}\lambda_i/\mu_i<1. Let P1⊆R+n\mathrm{P1}\subseteq\mathbb R_+^n be the polyhedron of Theorem 8.3,

∑i∈Sniμi ≥ ∑i∈Sρi/μi1−∑i∈Sρi(S⊂E),∑i∈Eniμi=∑i∈Eρi/μi1−∑i∈Eρi,\sum_{i\in S}\frac{n_i}{\mu_i}\ \ge\ \frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i}\quad(S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=\frac{\sum_{i\in E}\rho_i/\mu_i}{1-\sum_{i\in E}\rho_i},

with ρi=λi/μi\rho_i=\lambda_i/\mu_i, and for each permutation π\pi of EE let v(π)v(\pi) be the solution of the system (58), ∑j≤kxπj/μπj=b({π1,…,πk})\sum_{j\le k}x_{\pi_j}/\mu_{\pi_j}=b(\{\pi_1,\dots,\pi_k\}) for k=1,…,nk=1,\dots,n. Then

  1. the extreme points of P1 are exactly the vectors v(π)v(\pi), π\pi ranging over the n!n! permutations of EE;
  2. P1 is the convex hull of these vectors:
ext⁡P1={v(π):π∈SE},P1=conv⁡{v(π):π∈SE}.\operatorname{ext}\mathrm{P1}=\{v(\pi):\pi\in\mathfrak S_E\},\qquad \mathrm{P1}=\operatorname{conv}\{v(\pi):\pi\in\mathfrak S_E\}.

This is the polyhedral content of the paper's argument that P1 is an (extended) polymatroid base: it identifies the vertices with the performance vectors of the n!n! preemptive priority rules and makes linear optimization over P1 a greedy computation (the cμc\mu rule).

Formalization Note The statement concerns only the explicit vectors v(π)v(\pi); the paper's further claims that v(π)v(\pi) is the performance of a priority rule and that P1 is the achievable region are not formalized (no policy appears). "Having n!n! extreme points" is stated as the equality of the extreme-point set with the range of π↦v(π)\pi\mapsto v(\pi), without a cardinality claim (different permutations could in principle give equal vectors). Conventions are those of the definition MulticlassQNet.SingleStation.Polyhedra.

Preamble
import Mathlib
import Definitions.Def_MulticlassQNet_SingleStation_Polyhedra
Formal statement
namespace MulticlassQNet.SingleStation

/-- Proof of Theorem 8.3 (p. 37): P1 is an (extended) polymatroid base whose extreme points are
exactly the vectors `v(π)` of (58), one per permutation `π` of the classes, and every point of P1
is a convex combination of them. -/
theorem proof_8_3_extreme_points {n : ℕ} (lam mu : Fin n → ℝ)
    (hlam : ∀ i, 0 < lam i) (hmu : ∀ i, 0 < mu i) (hload : ∑ i, lam i / mu i < 1) :
    Set.extremePoints ℝ (P1 lam mu) = Set.range (v lam mu) ∧
      P1 lam mu = convexHull ℝ (Set.range (v lam mu)) := by sorry

end MulticlassQNet.SingleStation
Source
Bertsimas, Paschalidis, Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan WP #3509-92-MSA (Dec. 1992), p. 37, §8.2, proof of Theorem 8.3, third paragraph; Eq. (58) p. 33
Human review

  • Endorsed by Shuze Chen · Oct 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 4, 2026

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

View graph