Lemma 7 — Pr[max_{i∈I^hi} T_i > b + 1 + α] ≤ 2^(2−α)/(α − 2) for α > 2

Proved

StochLoadBal.Makespan.lemma_7

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

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-schedulingtail-boundunion-bound

Under the hypotheses of Observation 3 (sizes $X_{ij}\ge0$ measurable, integrable, jobs independent; $y$ feasible for the LP (5)–(9) with parameter $b$ ; $\sigma$ an assignment with (13)–(14)), let $I^{hi}$ be the set of machines of class at least $3$ and $T_i=\sum_{j\in J_i}X'_{ij}$ the truncated load of machine $i$ . Then for every $\alpha>2$ ,

\Pr\Big[\max_{i\in I^{hi}}T_i\ >\ b+1+\alpha\Big]\ \le\ \frac{2^{2-\alpha}}{\alpha-2}.

Integrating this tail bound gives $\mathbb E[\max_{i\in I^{hi}}T_i]\le b+5$ , the first term of the bound $4b+10$ in Lemma 6.

Formalization Note The event is written as "some machine of class at least $3$ has $T_i>b+1+\alpha$ ", which is the event $\max_{i\in I^{hi}}T_i>b+1+\alpha$ and is empty when $I^{hi}=\emptyset$ .

Preamble

import Mathlib
import Definitions.Def_StochLoadBal_Makespan_Rounding

Formal statement

namespace StochLoadBal.Makespan

open MeasureTheory ProbabilityTheory

/-- Lemma 7 (p. 13): for a feasible LP solution `y`, an assignment `σ` with (13)–(14), and
`α > 2`, the probability that some machine `i ∈ I^hi` (class `≥ 3`) has truncated load
`T_i = Σ_{j ∈ J_i} X'_{ij} > b + 1 + α` is at most `2^{2-α}/(α - 2)`. -/
theorem lemma_7 {m n : ℕ} (hm : 1 ≤ m) {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (X : Fin m → Fin n → Ω → ℝ)
    (hmeas : ∀ i j, Measurable (X i j)) (hnn : ∀ i j ω, 0 ≤ X i j ω)
    (hint : ∀ i j, Integrable (X i j) P) (hind : iIndepFun (fun j ω i => X i j ω) P)
    (b : ℝ) (y : Fin m → Fin n → ℝ) (hy : LPFeasible P X b y)
    (σ : Fin n → Fin m) (hσ : IsRoundingOutput P X b y σ) (α : ℝ) (hα : 2 < α) :
    (P {ω | ∃ i, 3 ≤ machineClass P X b y i ∧
        b + 1 + α < ∑ j ∈ Finset.univ.filter (fun j => σ j = i), trunc (X i j ω)}).toReal
      ≤ (2 : ℝ) ^ (2 - α) / (α - 2) := by sorry

end StochLoadBal.Makespan

Source

Gupta, Kumar, Nagarajan & Shen, Stochastic Load Balancing on Unrelated Machines, arXiv:1904.07271v1, p. 13, Lemma 7 (I^hi and T_i defined in the proof of Lemma 6, p. 12)

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