Eq. (3.1) — the mean busy time is the average of the $\alpha$ -points

Proved

SingleMachineSched.AlphaSched.eq_3_1

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

alpha-pointsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let $n$ jobs have integral processing times $p_j > 0$ , integral release dates $r_j \ge 0$ and weights $w_j > 0$ , indexed by nonincreasing $w_j/p_j$ . For every job $j$ , the mean busy time of $j$ in the LP schedule is the average over $\alpha \in (0,1]$ of its $\alpha$ -points in the LP schedule:

M^{LP}_j = \int_0^1 t_j(\alpha)\, d\alpha .

This identity turns bounds on completion times stated in terms of $\alpha$ -points into bounds in terms of $M^{LP}_j$ , and hence of the LP value.

Formalization Note The integral is the Lebesgue integral over $(0, 1]$ . Since $M^{LP}_j \ge r_j + p_j/2 > 0$ , the identity cannot hold through the convention that a non-integrable function has integral $0$ . The weights and the sortedness are the paper's standing assumptions; the identity itself concerns only the LP schedule.

Preamble

import Mathlib
import Definitions.Def_SingleMachineSched_AlphaSched_AlphaPoints

Formal statement

namespace SingleMachineSched.AlphaSched

open MeasureTheory

/-- Eq. (3.1) (Goemans et al. 2002, p. 176): the mean busy time of job `j` in the LP schedule is
the average of its `α`-points, `M^LP_j = ∫_0^1 t_j(α) dα`. -/
theorem eq_3_1 {n : ℕ} (p r : Fin n → ℕ) (w : Fin n → ℝ)
    (hp : ∀ j, 0 < p j) (hw : ∀ j, 0 < w j)
    (hsort : ∀ j k : Fin n, j ≤ k → w k / p k ≤ w j / p j) (j : Fin n) :
    mLP p r j = ∫ a in Set.Ioc (0 : ℝ) 1, alphaPoint p (lpSet p r) j a := by sorry

end SingleMachineSched.AlphaSched

Source

Goemans, Queyranne, Schulz, Skutella & Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2) (2002), p. 176, Eq. (3.1)

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

Eq. (3.1) — the mean busy time is the average of the α\alphaα-points

Eq. (3.1) — the mean busy time is the average of the $\alpha$ -points