Observation 1 — the class loop classifies every machine within m iterations, and at most ℓ machines have class at most ℓ

Proved

StochLoadBal.Makespan.observation_1

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

linear-programmingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1roundingstochastic-scheduling

Let $m\ge1$ and let $y$ be a feasible solution of the LP (5)–(9) with parameter $b$ . Run the class loop of §3.2 on $y$ . Then

the loop terminates within $m$ iterations, so every machine $i$ receives a class $\ell_i$ with $1\le \ell_i\le m$ ;
for every $\ell$ ,

\#\{i\in[m]:\ \ell_i\le \ell\}\ \le\ \ell .

The second part is the counting fact behind the union bound of Lemma 7: few machines have a small class, and machines of a large class $\ell$ have a tail probability $\ell^{-\alpha}$ .

Formalization Note "Terminates in at most $m$ iterations" is stated as: the loop, run with fuel $m$ , leaves no machine with the junk class $0$ . The second part is stated for every natural number $\ell$ ; it says nothing new for $\ell>m$ and, for $\ell=0$ , repeats that every machine is classified.

Preamble

import Mathlib
import Definitions.Def_StochLoadBal_Makespan_Rounding

Formal statement

namespace StochLoadBal.Makespan

open MeasureTheory ProbabilityTheory

/-- Observation 1 (p. 11): for a feasible LP solution `y`, the class loop classifies every
machine within its `m` iterations (every class lies in `1, …, m`), and for every `ℓ` at most
`ℓ` machines have class at most `ℓ`. -/
theorem observation_1 {m n : ℕ} (hm : 1 ≤ m) {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω)
    (X : Fin m → Fin n → Ω → ℝ) (b : ℝ) (y : Fin m → Fin n → ℝ)
    (hy : LPFeasible P X b y) :
    (∀ i, 1 ≤ machineClass P X b y i ∧ machineClass P X b y i ≤ m) ∧
    ∀ ℓ : ℕ, (Finset.univ.filter (fun i => machineClass P X b y i ≤ ℓ)).card ≤ ℓ := by sorry

end StochLoadBal.Makespan

Source

Gupta, Kumar, Nagarajan & Shen, Stochastic Load Balancing on Unrelated Machines, arXiv:1904.07271v1, p. 11, Observation 1

Human review

Endorsed by Shuze Chen · Oct 20, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 20, 2026
Confirmed by the mission captain (proposal self-audit).

View graph