Operations Research

Motivation

A steady-state simulation produces a single long output path $Y=\{Y(t):t\ge0\}$, and the quantity of interest is its long-run mean $\mu$. The central difficulty of simulation output analysis is that the observations are correlated, so the classical confidence interval $\bar Y_n(1)\pm z\,\hat\sigma/\sqrt n$ needs a consistent estimate of the time-average variance constant $\sigma^2$, which is hard to obtain. The method of standardized time series (STS), introduced by Schruben (1983) and put on a general footing by Glynn and Iglehart (Math. Oper. Res. 15 (1990)), avoids estimating $\sigma$: it divides the centred sample mean by a functional $g$ of the whole sample path that scales like $\sigma$, so that $\sigma$ cancels in the limit. Batch means, the area estimator and other procedures used in simulation software are all instances of this construction.

Cancelling $\sigma$ has a price. Glynn and Iglehart show (their Corollary 4.16) that every STS interval has asymptotic expected length at least $2\sigma\Phi^{-1}(1-\delta/2)/\sqrt n$, the length of the interval that knows $\sigma$, and (4.23) that this bound is the infimum over all admissible $g$. This mission formalizes the next question the paper asks and answers: is the infimum attained? Proposition 4.26 says it is not, and the companion results quantify the residual randomness of the interval length.

Setting

$C[0,1]$ is the space of continuous real functions on $[0,1]$ with the uniform metric $\rho(x,y)=\sup_t|x(t)-y(t)|$ and its Borel $\sigma$-algebra; $k(t)=t$, and $C_0[0,1]=\{x\in C[0,1]:x(0)=0\}$. For $g:C[0,1]\to\mathbb R$, $D(g)$ is the set of points at which $g$ is not continuous. On a probability space $(\Omega,\mathcal F,P)$, $B$ is a standard Brownian motion, viewed as a random element of $C[0,1]$.

Assumption (2.1). There are finite constants $\mu$ and $\sigma>0$ such that $X_n\Rightarrow\sigma B$ in $C[0,1]$, where

$$X_n(t)=n^{1/2}\big(\bar Y_n(t)-\mu t\big),\qquad \bar Y_n(t)=\frac1n\int_0^{nt}Y(s)\,ds,\quad 0\le t\le1 .$$

The class $\mathcal M$ (2.3) consists of the measurable $g:C[0,1]\to\mathbb R$ with

1. $g(ax)=a\,g(x)$ for $a>0$;
2. $g(x-\beta k)=g(x)$ for $\beta\in\mathbb R$;
3. $P\{g(B)>0\}=1$;
4. $P\{B\in D(g)\}=0$.

With $H(x)=P\{B(1)/g(B)\le x\}$ and $\alpha,\beta$ chosen so that $H(\beta)-H(\alpha)=1-\delta$, the interval $[\bar Y_n(1)-g(\bar Y_n)\beta,\ \bar Y_n(1)-g(\bar Y_n)\alpha]$ (2.10) is an asymptotic $100(1-\delta)\%$ confidence interval for $\mu$, of width $L_n=g(\bar Y_n)(\beta-\alpha)$.

Formalization targets

Goal: Proposition 4.26

For every $\sigma>0$ there is no $g\in\mathcal M$ such that, for some $\alpha>0$,

$$P\{g(\sigma B)=\alpha\sigma\}=1. \qquad (4.25)$$

By the paper's discussion before (4.25), attaining the lower bound of Corollary 4.16 with some $g\in\mathcal M$ requires (4.25); the goal therefore says that the bound is attained by no $g\in\mathcal M$. The goal is stated in terms of (4.25) and not of the limit (4.24), so it does not depend on the expected-length machinery of Corollary 4.16.

Milestones (the steps of the proof, pp. 13–14)

1. For $|z|<\eta$: $P\{|B(t)-z|<\eta,\ \max_{0\le s\le t}|B(s)|<2\eta\}>0$.
2. (4.27): $P\{\rho(\sigma B,x)<\varepsilon\}>0$ for every $x\in C_0[0,1]$ and $\varepsilon>0$.
3. If the range of $g$ over every $\varepsilon$-neighbourhood of $x$ contains $\{\alpha\sigma:\sigma>0\}$, then $x\in D(g)$.
4. Under (2.3i) and (4.25), $C_0[0,1]\subseteq D(g)$.

Companions

• $g(B)$ is nondegenerate for every $g\in\mathcal M$ (p. 14).
• Proposition 4.32: if $\{g^2(X_n)\}$ is uniformly integrable, then

$$\lim_{n\to\infty}nE(L_n-EL_n)^2=\sigma^2E\big(g(B)-Eg(B)\big)^2(\beta-\alpha)^2>0 .$$

Significance

The result closes the expected-length analysis of STS intervals: the bound $2\sigma\Phi^{-1}(1-\delta/2)$ is the exact infimum over $\mathcal M$ but no single standardization reaches it, so every STS procedure is strictly worse, in expected length, than the interval with known $\sigma$. The companion results explain why: $g(B)$ is never degenerate, so $n^{1/2}L_n$ converges to a nondegenerate random limit and the interval length fluctuates at order $n^{-1/2}$, while intervals built on a consistent estimator of $\sigma$ (the regenerative method, Proposition 4.34) fluctuate only at order $n^{-1}$. This is the quantitative trade-off a practitioner faces when choosing between STS and variance-estimation methods.

The paper's results are proved; none of them is formalized. The mission produces machine-checked versions of a support property of Wiener measure on $C[0,1]$ (every path started at $0$ is in the support), which is reusable well beyond simulation, and of the deterministic step that turns such a support property into everywhere-discontinuity of a functional.

Difficulty

The goal's statement is elementary, but its proof needs a quantitative fact about Brownian paths: the law of $\sigma B$ charges every uniform ball around every path in $C_0[0,1]$. The natural first attempt, using that $g$ is continuous $P$-almost everywhere and constant almost surely on $\sigma B$, fails without this fact, because almost-sure statements say nothing about any particular path $x$. Mathlib provides Brownian finite-dimensional laws and independent increments, but no small-ball or support estimate for Brownian motion in the uniform metric, so (4.27) has to be built from scratch. A second subtlety is that (4.25) is given for one $\sigma$ only; the homogeneity (2.3i) is what upgrades it to all scales, and that upgrade is what makes the range of $g$ near $x$ unbounded.

Proposition 4.32 needs, in addition, the passage from weak convergence of $g(X_n)$ to convergence of second moments under uniform integrability, in the space $C[0,1]$.

Formalization scope

• $C[0,1]$ is C(unitInterval, ℝ) with its sup norm; $\rho$ is dist. Mathlib has no measurable structure on it at this commit, so the Borel $\sigma$-algebra is declared in the mission's definitions file.
• $B$ is a measurable map $\Omega\to C[0,1]$ whose coordinates agree, for every $\omega$, with a process satisfying Mathlib's IsBrownianReal. "Measurable" in $\mathcal M$ means Borel measurable.
• $D(g)$ is the set where $g$ is not continuous; $P\{B\in D(g)\}$ is the outer measure of the preimage, so no measurability of $D(g)$ is assumed.
• Assumption (2.1) is a structure: joint measurability of $Y$, local integrability of its paths (the implicit condition that makes $\bar Y_n$ defined), $\bar Y_n$ pinned pointwise by its integral formula, $\sigma>0$, and convergence in distribution of $X_n$ to $\sigma B$. The index $n$ ranges over $\mathbb N$.
• $P\{\cdot\}=1$ is "almost surely". $0<\delta<1$ is added where the confidence level appears.
• The paper writes "$D(g)=C_0[0,1]$" at the end of the proof of Proposition 4.26; its argument proves only $C_0[0,1]\subseteq D(g)$, which is what milestone 4 states.
• Proposition 4.32 uses Bochner integrals; its uniform-integrability hypothesis makes every integral there finite.

The goal is a negation of an existence statement, so it would be trivially true if $\mathcal M$ were empty or if the Brownian hypothesis were unsatisfiable. Neither holds: $\mathcal M$ contains the batch-means functionals of the paper's Example 3.1 (p. 5), and the goal assumes nothing about small balls, (4.27) or continuity of $g$. Those appear only as milestones.

Contributions welcome: the support theorem for Brownian motion in $C[0,1]$ (milestones 1–2), any of the deterministic steps, and the moment-convergence argument of Proposition 4.32.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. https://doi.org/10.1287/moor.15.1.1
• L. Schruben, Confidence interval estimation using standardized time series, Operations Research 31(6):1090–1108, 1983. https://doi.org/10.1287/opre.31.6.1090
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968. https://doi.org/10.1002/9780470316962

Motivation

A retailer with limited shelf or screen space must choose which subset of its products to show each arriving customer. Which assortment earns the most depends on customer preferences, and those are unknown at first: the seller learns them from the purchases it observes. This is dynamic assortment selection, and it is a standard model in online retail and revenue management. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 67(5), 2019; preprint arXiv:1706.03880v2) study it under the multinomial logit (MNL) choice model as the MNL-Bandit problem. They propose an epoch-based upper-confidence-bound policy (Algorithm 1) that needs no prior knowledge of the parameters.

Their worst-case guarantee (Theorem 1) is regret of order $\sqrt{NT\log NT}$. Many instances are easier than the worst case: the best assortment beats every other feasible assortment by a fixed margin. For such well-separated instances, earlier policies obtained logarithmic regret, but only when told a lower bound on that margin:

• Rusmevichientong, Shen and Shmoys (2010), $O(N^2\log^2 T)$;
• Sauré and Zeevi (2013), $O(N\log T)$ for fixed cardinality.

This mission formalizes the paper's §6.1, which shows that the same parameter-free Algorithm 1 adapts to the separation.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$ and unknown attraction parameters $v_i\ge0$. The no-purchase option has weight $v_0=1$. Offered an assortment $S$, a customer buys $i\in S$ with probability $v_i/(1+\sum_{j\in S}v_j)$ and buys nothing with probability $1/(1+\sum_{j\in S}v_j)$ (2.1). The expected revenue of $S$ is

$$R(S,\mathbf v)=\frac{\sum_{i\in S}r_iv_i}{1+\sum_{j\in S}v_j}\quad(2.2).$$

Feasible assortments form a family $\mathcal S$ defined by totally unimodular constraints $A\,x(S)\le b$ (2.3). Assumption 4.1 asks that $v_i\le v_0=1$ for all $i$ and that $\mathcal S$ be closed under taking subsets.

A policy chooses $S_t\in\mathcal S$ from the past choices. The regret after $T$ customers is $\mathrm{Reg}_\pi(T,\mathbf v)=T\,R(S^*,\mathbf v)-\mathbb E_\pi\sum_{t=1}^TR(S_t,\mathbf v)$, where $S^*$ maximizes $R(\cdot,\mathbf v)$ over $\mathcal S$ (2.6).

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ until a customer buys nothing. It keeps three statistics for each product $i$:

• $T_i(\ell)$, the number of epochs up to $\ell$ that offered $i$;
• $\bar v_{i,\ell}$, the average number of purchases of $i$ per such epoch;
• the upper confidence bound $v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,48\log(\sqrt N\ell+1)/T_i(\ell)}+48\log(\sqrt N\ell+1)/T_i(\ell)$.

The next epoch offers an assortment maximizing the MNL revenue computed with $v^{\mathrm{UCB}}$ in place of $\mathbf v$.

The separation of an instance is the gap between the optimal and the second-best expected revenue among feasible assortments,

$$\Delta(\mathbf v)=\min_{S\in\mathcal S:\,R(S,\mathbf v)\neq R(S^*,\mathbf v)}\big(R(S^*,\mathbf v)-R(S,\mathbf v)\big)\quad(6.1).$$

The analysis uses the threshold $\tau=4NC\log NT/\Delta^2(\mathbf v)$ (6.2), with $C=\max\{C_1^2,C_2\}$, $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$. It also uses good epochs: those in which every $v^{\mathrm{UCB}}_{i,\ell}$ lies above $v_i$ and within the confidence width of Lemma 4.1.

Formalization targets

Goal: Theorem 3 (p. 20)

There are absolute constants $B_1,B_2$ such that for every instance satisfying Assumption 4.1 with $r_i\in[0,1]$, every tie-breaking rule and every $T$,

$$\mathrm{Reg}_\pi(T,\mathbf v)\le B_1\,\frac{N^2\log T}{\Delta(\mathbf v)}+B_2.$$

The constants are not fixed, so the goal survives any improvement of them.

Milestones

• Lemma 4.1 (p. 13): $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability $\ge1-6/(N\ell)$, and $v^{\mathrm{UCB}}_{i,\ell}-v_i\le C_1\sqrt{v_i\log(\sqrt N\ell+1)/T_i(\ell)}+C_2\log(\sqrt N\ell+1)/T_i(\ell)$ with probability $\ge1-7/(N\ell)$.
• Lemma 4.3 (p. 14): $(1+\sum_{j\in S}v_j)(\tilde R(S)-R(S,\mathbf v))$ is at most the sum of these widths over the offered set, with probability $\ge1-13/\ell$.
• Lemma 6.1 (p. 20): in a good epoch, if every offered product has $T_i(\ell)\ge\tau$, the offered assortment is optimal.
• Lemma 6.2 (p. 20): at most $N\tau$ good epochs offer a sub-optimal assortment.
• Corollary C.1 (p. 48): at most $N\log NT$ epochs offer a product with $T_i(\ell)<\log NT$.
• (C.5) (p. 48): the regret is at most $\mathbb E_\pi\sum_{\ell\le L}(1+V(S_\ell))(R(S^*,\mathbf v)-R(S_\ell,\mathbf v))$.

Companion: Corollary 6.1 (p. 21)

Under the cardinality constraint $|S|\le K$: $\mathrm{Reg}_\pi(T,\mathbf v)\le B_1\,NK\log NT/\Delta(\mathbf v)+B_2$.

Significance

The result. Theorem 3 shows that one policy is simultaneously near-optimal in the worst case (Theorem 1, $\tilde O(\sqrt{NT})$, matched by the lower bound of Theorem 2 up to logarithms) and logarithmic on separated instances. It does so without being told $\Delta(\mathbf v)$, which the separation-based policies of Rusmevichientong et al. and Sauré–Zeevi require. Under a cardinality constraint, Corollary 6.1 matches the order of Sauré–Zeevi's bound.

Formalizing it. The theorem is proved in the paper (Appendix C), and no machine-checked version exists. A formal proof has to make several things precise:

• Algorithm 1 as a function of the observed history;
• the epoch structure of a finite horizon;
• the pathwise counting arguments of Lemmas 6.1–6.2 and Corollary C.1;
• the probabilistic estimates inherited from the worst-case analysis.

Two printed details need care, and the formal statements fix them: Appendix C defines good epochs with "or" where both inequalities are meant, and Lemma 6.2's proof skips one case.

Difficulty

The counting part looks routine but depends on indexing. The bounds that are good at the end of epoch $\ell$ select the assortment of epoch $\ell+1$, so "a good epoch offering a sub-optimal set" pairs two consecutive epochs. A per-product count of under-sampled epochs is then off by one per product, so the printed bound $N\tau$ does not follow from the statement of Lemma 6.1 by counting alone.

The probabilistic part is the harder one. The per-epoch purchase counts are geometric with mean $v_i$ only conditionally on adaptively chosen assortments. The confidence statements must hold uniformly over a random number of samples, and the regret must be converted from customers to epochs, whose lengths are random and truncated at $T$. A union bound over all epochs costs a factor $\log T$, and that factor has to stay within the claimed $N^2\log T/\Delta$.

Formalization scope

Products are Fin N (0-based), and choices are Option (Fin N) with none the no-purchase option. A policy maps the past choices to an assortment. The law of a length-$T$ history is the product of MNL probabilities, so every expectation is a finite sum. Revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1, and $R(S^*,\mathbf v)$ is a Finset.sup' over the nonempty family $\mathcal S$. Algorithm 1 is defined as an explicit state machine and never reads $\mathbf v$. Ties in its argmax are broken by an arbitrary selector, and every statement quantifies over all selectors.

Standing assumptions carried by every statement:

• $0\le v_i\le1$;
• $r_i\in[0,1]$;
• the totally unimodular form of $\mathcal S$;
• closure under subsets;
• nonemptiness of $\mathcal S$ (needed for $S^*$ to exist).

Disclosed conventions:

• UCB before sampling. $v^{\mathrm{UCB}}_{i,\ell}=1$ while $T_i(\ell)=0$.
• Degenerate separation. $\Delta(\mathbf v)=1$ when every feasible assortment is optimal; the regret is then $0$.
• Lemma 4.1 constants. $C_1,C_2$ take the values established in the proof of Lemma 4.1.
• Probabilistic lemmas. They are stated for every horizon $T$ as probabilities that epoch $\ell$ is completed and the bound fails.
• Lemma 4.3. The printed free index $i$ is read as the sum over the offered set, and $\tilde R$ uses the bounds of the preceding epoch.
• (C.5). It is stated as "$\le$", since the last epoch is truncated at $T$.

The constants $B_1,B_2$ are quantified before every other object. A constant depending on $N$, $\mathbf v$ or $\Delta$ would make the theorem say only that regret is finite. The policy is pinned to Algorithm 1, not to any optimistic rule.

Contributions are welcome at every level:

• the pathwise lemmas (6.1, 6.2, C.1), which need no probability;
• the epoch rewriting (C.5);
• the concentration Lemmas 4.1 and 4.3, shared with the companion mission on Theorem 1;
• reusable infrastructure: MNL choice probabilities and finite-horizon history laws for adaptive policies.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019. https://doi.org/10.1287/opre.2018.1832 ; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880v2
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6):1666–1680, 2010. https://doi.org/10.1287/opre.1100.0866
• D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3):387–404, 2013. https://doi.org/10.1287/msom.2013.0429
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147

Why the lost-sales state space matters

The lost-sales inventory system with a positive lead time is one of the basic models of inventory theory. Demand that cannot be met from stock is lost rather than backlogged, and orders arrive a fixed number $L$ of periods after they are placed. Unlike the backlog system, where the inventory position is a sufficient one-dimensional state and a base-stock policy is optimal, the lost-sales system needs the whole pipeline of outstanding orders as its state, and its optimal policy has no simple form. Computing optimal policies by dynamic programming therefore runs into the size of an $L$-dimensional state space.

Paul Zipkin's paper Old and New Methods for Lost-Sales Inventory Systems (Operations Research 56(5), 2008, doi:10.1287/opre.1070.0471) revisits this model, compares classical and new heuristics against optimal policies, and prepares the computation with a state-reduction result. Morton (1969, SIAM Review 11, Equation (83)) showed that under an optimal policy the state remains in a bounded set; Zipkin's §4 extends the argument to every policy in a class $Z(s)$ that contains the usual heuristics. This mission formalizes that section: the reduced state space $X(s)$, the policy class $Z(s)$, and Claim 1, which says that states outside $X(s)$ are transient.

Setting

Fix the lead time $L\ge 1$. The state is the $L$-vector $x=(x_0,\dots,x_{L-1})$: $x_0$ is the stock on hand after this period's delivery, and $x_l$ ($1\le l\le L-1$) is the order that arrives $l$ periods later, so $x_{L-1}$ is the most recent order. Given the state $x$, an order $z\ge 0$ and a demand $d\ge 0$, the next state is

$$x_+ = \bigl([x_0-d]^+ + x_1,\ x_2,\ \dots,\ x_{L-1},\ z\bigr),\qquad [a]^+=\max(a,0).$$

Demands in successive periods are independent with a common law $D$ on $[0,\infty)$.

The pipeline partial sums are $v_l=\sum_{m=l}^{L-1}x_m$ for $l=0,\dots,L-1$ and $v_L=0$; $v_0$ is the inventory position and $v_{L-1}=x_{L-1}$ the most recent order. A level vector is $s=(s_0,\dots,s_L)$ with $s_0\ge s_1\ge\dots\ge s_L\ge 0$. For a level vector $s$,

$$X(s)=\{x\ge 0:\ v_l\le s_l,\ l=0,\dots,L-1\},$$

and $Z(s)$ is the set of stationary policies $z$ (an order $z(x)\ge 0$ in each state $x\ge 0$) with $z(x)=0$ for $x\notin X(s)$ and $v_l+z(x)\le s_l$ for $l=0,\dots,L$ and $x\in X(s)$. The vector base-stock policy with parameter $s$ is

$$z_s(x)=\bigl[\min\{s_l-v_l,\ l=0,\dots,L\}\bigr]^+,$$

equation (5) of the paper with a general $s$ in place of Morton's $\bar s$. Under a stationary policy $z$, from an initial state $x$ and along a demand path $(d_t)$, the state process is $x_0=x$, $x_{t+1}=(x_t)_+$ with order $z(x_t)$ and demand $d_t$. In Lean these are next, v, IsLevelVector, Xs, Zs, vectorBaseStock and traj in the namespace LostSalesOldNew.StateReduction.

Formalization targets

Goal: Claim 1 (p. 1259)

For a level vector $s$, a policy $z\in Z(s)$, i.i.d. demands with law $D$ on $[0,\infty)$ and $P(d>0)>0$, and any initial state $x\ge 0$, almost surely

$$\exists\,T\ \forall\,t\ge T:\quad x_t\in X(s).$$

The paper's word is "transient"; the statement above says that every state outside $X(s)$, indeed the whole complement, is visited only finitely often.

Milestones

1. (5) and §4: for every level vector $s$, $z_s\in Z(s)$.
2. Invariance (proof of Claim 1): $x\in X(s)$, $z\in Z(s)$, $d\ge 0$ imply $x_+\in X(s)$.
3. Entrance (proof of Claim 1): along a demand path with $d_t\ge 0$ and $\sum_{t<n}d_t\to\infty$, the process started at any $x\ge 0$ visits $X(s)$.

A further item records the paper's remark that $X(s)$ and $Z(s)$ are increasing in $s$.

Significance

Claim 1 lets the dynamic program be solved on the compact set $X(\bar s)$ with policies restricted to $Z(\bar s)$, which is what makes the paper's exact computations (lead times up to four, §6) feasible. Since $Z(s)$ contains the vector base-stock policies and, for $s$ large enough, any policy that stops ordering in large states, the claim also says that every plausible policy eventually confines the state to a bounded set.

The result has a short proof in the paper and no machine-checked version. Formalizing it produces a reusable encoding of the lost-sales pipeline with general stationary policies, and makes explicit two points the paper leaves implicit: the probabilistic reading of "transient", and the demand condition under which the process must leave the complement of $X(s)$. Related platform material treats the backlog analogue (VeinottBaseStock.base_stock_level_absorbing, a base-stock level set is absorbing) and lost-sales dynamics under other conventions (CappedBaseStock_Model, from an empty initial state under capped base-stock policies with average cost); those formulations use another state convention and cost criterion and are not imported here.

Difficulty

The invariance step is algebra on partial sums. The content of the claim is the entrance step: outside $X(s)$ the policy orders nothing, so the process can only reach $X(s)$ through demand draining the stock and the pipeline. That requires the cumulative demand to diverge, which fails pathwise (demand identically zero leaves a state with $x_0>s_0$ fixed forever) and holds only almost surely, from independence and $P(d>0)>0$. The naive reading of "transient" as invariance alone, or as the pathwise statement with divergent demand assumed, misses this step.

Formalization scope

• States are Fin L → ℝ with $L\ge 1$ in the goal; theorems quantify over nonnegative states. The vector $(x,z)$ is Fin.snoc x z; $v$ takes a natural-number index and vanishes at $l\ge L$, so $v_L=0$.
• Level vectors are Fin (L+1) → ℝ, antitone with nonnegative last entry. $X(s)$ constrains $v_0,\dots,v_{L-1}$; $Z(s)$ constrains $v_l+z(x)$ for $l=0,\dots,L$.
• Policies are deterministic stationary functions of the state, with no measurability required. The zero condition and the sign condition of $Z(s)$ range over states $x\ge 0$ (the paper's state space); over all of $\mathbb R^L$ the vector base-stock policy would not be in $Z(s)$.
• Demand is a probability measure $D$ on $\mathbb R$ with $D((-\infty,0))=0$; the demand sequence is the coordinate process under Measure.infinitePi (fun _ : ℕ => D). The hypothesis $D((0,\infty))>0$ is added to the paper's assumptions; without it the claim is false.
• "Transient" is read as: almost surely the state lies in $X(s)$ from some period on.
• Ruled out: the goal is neither the invariance statement alone, which says nothing about states outside $X(s)$, nor the pathwise entrance statement with divergent cumulative demand assumed, which drops the probabilistic content.

A complete development needs the partial-sum algebra of the pipeline, the second Borel–Cantelli lemma or the strong law for i.i.d. nonnegative sequences under Measure.infinitePi, and induction along traj. The pipeline encoding is shared with the second mission of this series (lead-time monotonicity). Proofs of any milestone and of the goal are welcome.

Selected references

• P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5):1256–1263, 2008. https://doi.org/10.1287/opre.1070.0471
• T. Morton, Bounds on the Solution of the Lagged Optimal Inventory Equation with No Demand Backlogging and Proportional Costs, SIAM Review 11:572–576, 1969 (as cited in Zipkin 2008).
• T. Morton, The Near-Myopic Nature of the Lagged-Proportional-Cost Inventory Problem with Lost Sales, Operations Research 19(7):1708–1716, 1971. https://doi.org/10.1287/opre.19.7.1708
• R. Levi, G. Janakiraman, M. Nagarajan, Provably Near-Optimal Balancing Policies for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research, 2008 (forthcoming at the time of Zipkin 2008).

Motivation

The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an $L$-dimensional vector, and no simple policy is optimal.

Its structure has a long history:

• Karlin and Scarf (1958) formulated the model and showed, for lead time one and continuous demand, that the optimal order decreases in on-hand inventory with slope bounded by one.
• Morton (1969) extended these qualitative properties to general lead times, again by differentiating the optimal cost function, which required smooth demand distributions.
• Zipkin (2008), the paper formalized here, recovered and unified both results with a change of state variables and a single structural property, L♮-convexity, from discrete convex analysis (Murota 2003). The argument needs no smoothness and works for discrete as well as continuous demand.

Setting

Time is discrete. In each period the order due arrives, a new order $z\ge0$ is placed, demand $d\ge0$ occurs, and a holding or penalty cost is charged. The lead time $L\ge1$ is an integer. The original state $x=(x_0,\dots,x_{L-1})$ records on-hand inventory $x_0$ followed by the orders in transit. Demands are independent with a common law $\mu$. The costs are linear and stationary: unit procurement cost $c$, unit holding cost $\hat h$, unit lost-sales penalty $p$, and discount factor $\gamma$.

The transformed state is the vector of partial sums $v_l=\sum_{k=l}^{L-1}x_k$, $0\le l<L$, with the convention $v_L=0$. It ranges over the cone

$$V=\{v\in\mathbb R^L : v_0\ge v_1\ge\dots\ge v_{L-1}\ge 0\}.$$

The transformed order is $\zeta=-z\le0$. With $e$ the all-ones vector, the state moves to

$$v_+=\big([v_0-v_1-d]^+ + v_1,\ v_2,\ \dots,\ v_{L-1},\ 0\big)-\zeta e .$$

The one-period cost is $\hat q(u)=\hat hu^+ + pu^-$ on $u=y-d$, where $y=v_0-v_1$ is the on-hand stock, and $\hat q^0(y)=E[\hat q(y-d)]$. With $k$ periods to go, the optimal cost functions are

$$\bar f_0\equiv0,\qquad \bar g_k(v,\zeta)=-\gamma^Lc\zeta+\hat q^0(v_0-v_1)+\gamma E\big[\bar f_k(v_+)\big],\qquad \bar f_{k+1}(v)=\inf_{\zeta\le0}\bar g_k(v,\zeta).$$

A function $\varphi$ is submodular on a set $S\subseteq\mathbb R^n$ if $\varphi(x\vee y)+\varphi(x\wedge y)\le\varphi(x)+\varphi(y)$ for all $x,y\in S$, with $\vee,\wedge$ the componentwise maximum and minimum. A function $f:V\to\mathbb R$ is L♮-convex if $\psi(v,\zeta)=f(v-\zeta e)$ is submodular on $V\times\Re^-$. A function $g(v,\zeta)$ on $V\times\Re^-$ is L♮-convex if $g\big((v,\zeta)-\xi(e,1)\big)$ is submodular in $(v,\zeta,\xi)$ over $v\in V$, $\zeta\le\xi\le0$.

Formalization targets

Goal: Theorem 4 (p. 939)

For every number of periods to go $k$,

$$\bar f_k \text{ is L♮-convex on } V \quad\text{and}\quad \bar g_k \text{ is L♮-convex on } V\times\Re^- .$$

The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.

Milestones, in the order the proof uses them

1. Lemma 1 (p. 938): if $f(v)$ is L♮-convex, so is $\psi(v,\zeta)=f(v-\zeta e)$.
2. Lemma 2 (p. 939): if $g(v,\zeta)$ is L♮-convex, so is $f(v)=\min_{\zeta\le0}g(v,\zeta)$.
3. Optimal filling (proof of Theorem 4): in the end-of-period program (3), filling as much demand as possible is optimal ($a=\min\{d,v_0-v_1\}$). Consequently $\bar\kappa_t(v,\zeta\mid d)=\hat q(v_0-v_1-d)+\gamma\bar f_{t+1}(v_+)$.
4. $\psi_t$ is L♮-convex: the objective $\psi_t(v_+,v,\zeta)=\hat h(v_+-v_1)+p(v_+-v_0+d)+\gamma\bar f_{t+1}[(v_+,v_2,\dots,v_{L-1},0)-\zeta e]$ of program (4) is L♮-convex on its constraint set.
5. $\bar\kappa_t$ is L♮-convex: the end-of-period cost $\bar\kappa_t(v,\zeta\mid d)$ is L♮-convex in $(v,\zeta)$ for each $d$.
6. $\bar g_t$ is L♮-convex: if $\bar f_{t+1}$ is L♮-convex, so is $\bar g_t=-\gamma^Lc\zeta+E_d[\bar\kappa_t]$, by (5).

Significance

The result. L♮-convexity of $\bar f_t$ implies that $\bar f_t$ is submodular and convex in the transformed state. L♮-convexity of $\bar g_t$ yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order $\bar z_t(v)$ is nonincreasing in $v$ and changes by at most $\omega$ when every component of $v$ increases by $\omega$. These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:

• a formal L♮-convexity theory on real cones (the shift characterization, its preservation under partial minimization, and its preservation under expectation);
• a checked version of the induction behind Theorem 4;
• a verified model of the lost-sales recursion in the transformed state, which missions on Corollary 5 and the later sections can import.

Difficulty

The obvious argument works with ordinary convexity and submodularity in the original state $x$. It stalls: the lost-sales transition $[x_0-d]^+$ is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in $x$. The paper's structure appears only in the partial sums $v$. Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over $\zeta$ (Lemma 2). Proving plain submodularity of $\bar f_t$ on $V$ therefore does not close the induction.

A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.

A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of $d\mapsto\bar f_k(v_+)$, and these come from the model rather than from the definitions.

Formalization scope

• Representation. States are functions Fin L → ℝ, indexed $0,\dots,L-1$ as in the paper. A helper returns $v_l$ for $l<L$ and $0$ at $l=L$. A function $g(v,\zeta)$ is encoded on Fin (L+1) → ℝ with $\zeta$ last. The objective $\psi_t$ of (4) is encoded on Fin (L+2) → ℝ with coordinates $(v_+,v_0,\dots,v_{L-1},\zeta)$. The order is componentwise.
• L♮-convexity on a domain $D$: $(x,\xi)\mapsto f(x-\xi e)$ is submodular on $\{\xi\le0,\ x\in D,\ x-\xi e\in D\}$, with $e$ the all-ones vector on every coordinate. For $D=V$ this is the paper's definition verbatim. This is the paper's definition, not Murota's translation-submodularity form, and it is stated on real vectors. The platform's discrete-convexity library (DiscreteConvex.LConvexFunctions.*) works on $\mathbb Z^V$ with values in $\mathbb R\cup\{+\infty\}$, a different domain and definition, and is not reused.
• Time. Data are stationary, so the paper's $\bar f_t$ depends on $t$ only through the number of periods to go $k=T+L+1-t$, and "for all $t$" is "for all $k$". The minimum over $z\ge0$ is taken in every period, as printed in (1).
• Explicit readings of the paper's phrases.
  • "min" (over $\zeta\le0$, over $v_+$, over $(a,w)$) is an infimum over the constraint set. In the model every cost is nonnegative, so the infimum is genuine. The generic Lemma 2 assumes the values bounded below, and the generic milestone 5 assumes the continuation nonnegative on $V$.
  • "the $d_t$ are independent and nonnegative": one law $\mu$ with $\mu(-\infty,0)=0$, since data are stationary.
  • "unit cost", "discount rate": $c,\hat h,p\ge0$ and $0<\gamma\le1$.
  • Finite mean demand is added: without it $\hat q^0$ is infinite.
  • "the optimal $a=\min\{d,v_0-v_1\}$": stated as the equality of the infimum of program (4) with its value at $v_+=\max(v_0-d,v_1)$.
• Ruled out. A statement that holds because a value function is the junk constant $0$ (constants are L♮-convex), plain submodularity on $V$ in place of the shift condition, quantification over all of $\mathbb R^L$ instead of $V$, and a goal about an arbitrary function assumed to satisfy the recursion. None of these is the paper's theorem; the goal is stated for the recursion itself.
• Not in scope. "L♮-convex implies convex" for a generic function, which is false without regularity (a non-measurable additive function is L♮-convex in this sense); Lemma 3 and Corollary 5, for a follow-up mission that references Theorem 4; the smooth-case Hessian discussion; the infinite-horizon remarks.
• Welcome contributions. Reusable lemmas on submodularity over sublattices of $\mathbb R^n$ (partial minimization, Topkis 2.7.6), on preservation of submodularity under integration, and on measurability of the value functions.

Selected references

• P. Zipkin, On the structure of lost-sales inventory models, Operations Research 56(4) (2008) 937–944. https://doi.org/10.1287/opre.1070.0482
• S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• T. E. Morton, Bounds on the solution of the lagged optimal inventory equation with no demand backlogging and proportional costs, SIAM Review 11(4) (1969) 572–596. https://doi.org/10.1137/1011090
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998.

Motivation

Queueing models often represent work arriving to and leaving a server by a real-valued input path. The resulting workload cannot fall below a barrier. Functional limit theorems describe what happens to such paths under scaling, but a limit for the input path is useful only when it can be carried through the workload transformation. Ward Whitt’s 1980 paper studies several path transformations that occur in stochastic-process limits and states conditions under which their limits can be computed in Skorohod topologies. Section 6 treats the running supremum and a reflecting barrier, including paths with a linear drift that changes with the scaling index. This mission formalizes the three-regime reflection result, Theorem 6.4, and the source results on its dependency path. Whitt (1980)

The result is already proved in the paper. Its formal Lean statement remains an open proof target here. The mission is therefore concerned with formalizing the known theorem, including its exact jump conditions and convergence modes, rather than proposing a new queueing claim. Whitt (1980), pp. 80–81

Setting

A càdlàg path on a real interval $T$ is right-continuous and has a limit from the left wherever $T$ approaches a time from the left. The collection of such real-valued paths is $D(T,\mathbb R)$. For a compact interval $[a,b]$, the $J_1$ distance between $x$ and $y$ allows an increasing homeomorphism $\lambda$ of time and measures the larger of its distance from the identity and the uniform distance between $x$ and $y\circ\lambda$. On a general interval, $J_1$ convergence is specified by restrictions to compact subintervals whose endpoints are continuity points of the limit or endpoints of $T$. The paper uses complete separable metric spaces for general path-space results; Section 6 specializes to real-valued paths and intervals with $0$ as a closed left endpoint. Whitt (1980), pp. 70, 80

For $x\in D(T,\mathbb R)$ and $t\in T$, define the running supremum $x^{\uparrow}(t)=\sup_{0\le s\le t}x(s)$ and running infimum $x^{\downarrow}(t)=\inf_{0\le s\le t}x(s)$. The reflecting-barrier map is $f(x)(t)=x(t)-x^{\downarrow}(t)$. This is the paper’s definition: it subtracts the full running infimum. The identity path is $e(t)=t$, and $\theta$ denotes the zero path. A path has no positive jumps if $x(t)\le x(t-)$ for each $t>0$ in $T$; no negative jumps reverses that inequality. Whitt (1980), pp. 80–81

Formalization targets

The goal is Theorem 6.4. Suppose $x_n-c_ne\to x$ in $J_1$ and $x(0)=0$. Its three conclusions are

$$\begin{aligned} c_n\to c &\implies f(x_n)\to f(x+ce) &&(J_1),\\ c_n\to+\infty &\implies f(x_n)-c_ne\to x &&(J_1),\\ c_n\to-\infty\ \text{and }x\text{ has no positive jumps} &\implies f(x_n)\to\theta &&(U). \end{aligned}$$

Here $U$ means uniform convergence on every compact subinterval. The goal keeps all three drift regimes together, as the printed theorem does. Its milestones are the finite-partition fact cited from Billingsley, the interval-splitting Lemma 2.2, continuity of addition at limits without shared discontinuities in Theorem 4.1, the running-supremum inequality in Theorem 6.1, the three-regime supremum theorem 6.2, and the paper’s explicit claim that $f$ is $J_1$-continuous. Whitt (1980), pp. 71, 79–81

Significance

The theorem specifies which output path appears after reflection as the linear centering changes. Finite drift leaves a reflected limit with drift included; large positive drift leaves the centered input limit; large negative drift drives the reflected path uniformly to zero when upward jumps of the limit are excluded. The distinction between $J_1$ and the stronger compact-uniform mode in the last case is part of the result. These statements make the paper’s barrier transformation usable when an input-process limit is already known. Whitt (1980), Theorem 6.4

A completed formal development would establish reusable path-space components: a precise $J_1$ convergence interface for real intervals, a theorem about addition with disjoint discontinuities, and continuity properties of running extrema and reflection. The present Lean items state these results and compile with proof placeholders. No machine-checked proof of these mission theorems is claimed here. The milestone list follows the claims Whitt states or cites, so later proofs can be attached to the same mathematical targets. Whitt (1980), §§2, 4, 6

Difficulty

A uniform estimate alone does not establish a $J_1$ limit: separate paths may converge using different changes of time, and addition can fail when the limiting paths jump together. Whitt’s Theorem 4.1 gives continuity precisely at pairs with disjoint discontinuity sets. In the reflection theorem, a linearly growing drift also changes which extrema matter, and the sign of a jump decides whether the large-drift conclusion can hold. The negative-drift conclusion asks for compact-uniform convergence, which is stronger than merely retaining $J_1$ convergence. These are real constraints on the statement; dropping a jump condition or replacing $U$ by $J_1$ changes the theorem. Whitt (1980), pp. 78–81

Formalization scope

Paths are total functions $\mathbb R\to S$, but only their values on the stated interval count. The Lean definitions require càdlàg membership of both prelimit and limit paths in each $J_1$ convergence claim. A time change on $[a,b]$ is strictly increasing, continuous, and onto; this represents the paper’s increasing homeomorphism. Uniform and $J_1$ distances take values in the extended nonnegative reals, so an unbounded supremum cannot silently become zero. Continuity points use continuity within $T$, and the discontinuity set likewise contains only points of $T$. Sequential convergence is used because the paper’s $J_1$ spaces are metrizable. These choices encode the paper’s path-space conventions rather than imposing conditions on values outside $T$. Whitt (1980), §§2, 4, 6

The compact form of Theorem 6.1 uses metric (2.1); the noncompact metric (2.2) is outside this mission’s definition layer. Theorem 4.1 retains the paper’s complete separable metric-space setting and metric compatibility of addition. Its measurability clause is omitted: this mission does not construct the Borel measurable space of $D(T,S)$, and a product measurable structure on all total functions would express a different claim. The source’s $f(x)=x-x^{\downarrow}$ is used on both prelimit and limit paths; it is not replaced by a clipped running infimum. Whitt (1980), pp. 70, 78–81

The definition layer, the addition theorem, the running-extremum results, and the barrier continuity statement are welcome proof targets. The theorem’s centered-path hypothesis remains a genuine $J_1$ convergence assertion, and the jump conditions apply to the limit path only. A vacuous convergence predicate or an independently assumed conclusion would not represent this mission’s goal.

Selected references

• Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, pp. 67–85. DOI: 10.1287/moor.5.1.67

Why processor speed changes the scheduling problem

A processor can save energy by running slowly when work is light, but a deadline may force it to run faster. Yao, Demers, and Shenker formulated this tradeoff as an offline and online scheduling problem for a variable-speed processor in their 1995 FOCS paper. Their Average Rate Heuristic (AVR) uses only each job's arrival, deadline, and required work to set speed. This mission formalizes their quadratic-power analysis: AVR's worst-case energy is at least four and at most eight times the minimum possible energy. The authors prove these bounds in Theorem 2, rather than an exact value.

The question matters when an online scheduler must choose speed before seeing later jobs. Deadline feasibility alone does not measure energy: processing the same number of cycles at twice the speed for half as long can cost more when power grows superlinearly. The paper's model isolates that dependence in a power function $P(s)$, so the competitive guarantee measures the energy price of AVR's speed choices. The initial motivation, model, and heuristic are in §§1–4 of the paper.

Jobs, schedules, and the average-rate rule

Fix a nondegenerate time window $[t_0,t_1]$. A finite job instance $J$ assigns each job $j$ an arrival time $a_j$, deadline $b_j>a_j$, and nonnegative required work $R_j$ in CPU cycles. Every job window $[a_j,b_j]$ lies inside $[t_0,t_1]$. A schedule $S=(s,\operatorname{job})$ has nonnegative processor speed $s(t)$ and selects at most one job at each time. Speed and job selection are constant between finitely many breakpoints. The schedule is feasible if each job receives its full work inside its own window:

$$\int_{a_j}^{b_j}s(t)\,\mathbf 1\{\operatorname{job}(t)=j\}\,dt=R_j \qquad\text{for every }j.$$

For a power function $P$, its energy is $E_P(S)=\int_{t_0}^{t_1}P(s(t))\,dt$. An optimal schedule minimizes this quantity among feasible schedules. These definitions follow §2, p. 375. The intensity of an interval $[z,z']$ is the total work of jobs whose full windows it contains, divided by $z'-z$. An interval with maximum intensity is critical; Theorem 1 identifies the processor speed on that interval in an optimal schedule §3, p. 375.

Each job's density is $d_j=R_j/(b_j-a_j)$, extended as a step function equal to $d_j$ on $[a_j,b_j]$ and zero elsewhere. AVR runs at speed $\sum_j d_j(t)$ and chooses the earliest-deadline available job. For quadratic power, its energy is

$$\operatorname{AVR}(J)=\int_{t_0}^{t_1}\left(\sum_jd_j(t)\right)^2dt.$$

The competitive ratio is the least upper bound of $\operatorname{AVR}(J)/\operatorname{OPT}(J)$ over instances, where $\operatorname{OPT}(J)$ is the least feasible energy §4, p. 376, Eq. (2).

Formalization targets

The goal is the paper's Theorem 2, p. 381:

$$4\le r\le 8\qquad(P(s)=s^2).$$

The upper bound compares AVR with every feasible schedule. The lower bound says that every constant strictly below four is exceeded by the AVR-to-feasible-energy ratio on some instance. This formulation does not claim that one finite instance attains four.

The milestone path follows the paper: Theorem 1 characterizes optimal speed; Lemma 5.1 reduces to jobs of type A or B; Eq. (5) splits their costs; Lemma 5.2 and Eq. (7) control the A contribution; Lemmas 5.3–5.6 reduce the analysis to canonical instances; Lemma 5.8 supplies a matrix bound; Lemma 5.7 gives $F_A\le4\operatorname{OPT}_A$ and $F_B\le4\operatorname{OPT}_B$; Example 2 approaches the lower constant. These statements and their order come from §5, pp. 378–381. The paper also states a higher-power result, Theorem 3, for real $p\ge2$:

$$p^p\le r_p\le 2^{p-1}p^p.$$

That result is a companion item. The extended abstract leaves its full proof to a longer paper §6, pp. 381–382.

What the bounds provide

The upper bound guarantees that AVR's energy is controlled by a fixed multiple of the offline optimum for every finite job set, even though AVR sets speed from individual job densities. The lower family rules out a guarantee below four for this heuristic. Together they delimit the performance of AVR under quadratic power; they do not give its exact worst-case ratio. The A/B reductions and the tree-induced matrix estimate are useful mathematical interfaces for later analyses of interval-structured schedules.

The paper proves Theorem 2 in the mathematical sense. This mission supplies machine-checkable statements and definitions, with proofs left open for solvers. Closing it requires formal proofs of the reduction steps, the matrix estimate, and the limiting example, plus an explicit connection from the optimal-schedule analysis to comparison with every feasible schedule. No completed Lean proof is claimed here.

The main difficulty

The simple calculation $\left(\sum_j d_j(t)\right)^2$ exposes overlap between job windows but does not say how that overlap compares with an optimal schedule. An optimal schedule may run jobs in a different order and may preempt them. The paper therefore changes the instance while preserving the optimal speed profile: it first separates cumulative execution into two types, then reduces to single execution intervals and specially aligned, nested windows. The matrix inequality controls the resulting expression. A pointwise comparison of AVR speed with optimal speed cannot replace these reductions, because an optimal schedule can concentrate work on critical intervals while AVR spreads each job's density across its entire window §5, pp. 377–381.

Formalization scope

Jobs use Fin n, allowing the empty instance. The instance requires $t_0<t_1$, $a_j<b_j$, containment in the window, and $R_j\ge0$. A schedule uses real-valued speed and an optional job label; none denotes no assigned job. Its piecewise-constant requirement is witnessed by finitely many increasing breakpoints. Values at breakpoints are unrestricted by the piecewise-constant clauses, and speed comparisons in the theorems are almost-everywhere statements. Job windows are closed, as printed; endpoints do not affect the integrals. A schedule may have positive speed while no job is assigned, since the source does not equate idleness with zero speed.

Every energy expression is a real interval integral. The schedule conditions ensure the integrands in theorem hypotheses are piecewise constant away from finitely many points. Density denominators are positive. An execution-speed quotient for a zero-work job can have zero denominator, in which case Lean returns zero; such a job contributes no executed work. The goal uses quantified comparisons with feasible schedules rather than a real infimum, and Lemma 5.6 uses all upper bounds on a nonempty canonical family rather than a real supremum. The lower bounds quantify over every smaller constant, avoiding a false attainment claim. These choices guard against default values for empty or unbounded extrema.

Theorem 1's printed convexity hypothesis is strengthened to strict convexity and nondecreasing power on nonnegative speeds: its stated speed uniqueness fails for a linear power function, and a decreasing power function rewards idle speed. This repair is explicit in that item's description. Existence of a quadratic optimum is included as a milestone from the algorithm of §3, although it is not a separately numbered theorem. Example 2 includes the variable exponent $e\ge1$, the limiting ratios at $e=1$ and $e=3/2$, and an eventual upper bound of four across the family. The A-job order resolves exact ties by index. For canonical and tree-induced nesting, intervals that meet only at an endpoint count as disjoint; this admits the paper's displayed four-interval matrix.

The development needs Mathlib's real interval integrals, finite sums, measures of intervals, matrix eigenvalues, and real-power limits. The finite schedule model, canonical-instance data, and tree-induced matrix interface can be reused beyond this particular ratio bound. Contributions may establish these interfaces' elementary properties, the paper's milestone theorems, or independent proofs of the goal, provided they preserve the stated job and schedule classes.

Selected references

• Frances Yao, Alan Demers, and Scott Shenker, A Scheduling Model for Reduced CPU Energy, Proceedings of the 36th IEEE Symposium on Foundations of Computer Science, 1995, pp. 374–382. DOI 10.1109/SFCS.1995.492493.

Why time reversal matters

Functional limit theorems describe the behavior of entire time-indexed paths under scaling. In queueing and other stochastic models, a path of departures, workload, or accumulated input may be related to another path by reversing a finite observation window. To carry a limit theorem through that change of viewpoint, one needs to know how reversal acts on the topology of the path space. Ward Whitt's 1980 paper studies composition, reflection, first passage, and time reversal as maps that transfer functional limit theorems to derived processes (Whitt 1980).

The time-reversal result is a precise metric statement. Ordinary reversal preserves the Skorohod $J_1$ distance exactly. A version shifted to begin at the group identity satisfies a bound with constant two. These facts give continuity and, when the random paths satisfy the hypotheses, make reversal available to the continuous mapping theorem. Whitt's introduction explains how deterministic path continuity connects to stochastic-process limits (Whitt 1980, pp. 67–69).

Paths, distances, and reversal

Let $S$ be a complete separable metric group, written additively, with identity $0$ and metric $m$. The metric is translation invariant: moving both points by the same group element leaves their distance unchanged. Let $D$ contain the càdlàg paths $x:[0,1]\to S$, meaning paths that are right continuous and possess left limits. Section 8 additionally requires $x(1)=x(1-)$, so the terminal value agrees with the value approached from earlier times. Let $D_\theta=\{x\in D:x(0)=0\}$. These are the spaces Whitt fixes for time reversal (Whitt 1980, p. 83).

The uniform distance is $\rho(x,y)=\sup_{0\le t\le1}m(x(t),y(t))$. A time change $\lambda\in\Lambda$ is an increasing homeomorphism of $[0,1]$ onto itself; $e(t)=t$ is the identity time change. The $J_1$ distance used in the paper is

$$d(x,y)=\inf_{\lambda\in\Lambda} \max\{\rho(\lambda,e),\rho(x,y\circ\lambda)\}.$$

Two paths may be close when their values can be matched after a small distortion of time. This is the paper's equation (2.1), rather than an unspecified equivalent $J_1$ metric (Whitt 1980, p. 70).

The reverse-time map reads the left limit at the reflected time:

$$R(x)(t)= \begin{cases} x((1-t)-),&0\le t<1,\\ x(0),&t=1, \end{cases} \qquad r(x)(t)=R(x)(t)-x(1).$$

The left limit is essential: the direct value $x(1-t)$ places jumps on the wrong side and generally does not give a right-continuous reverse path. The terminal convention gives $R(x)(0)=x(1)$, so $r(x)(0)=0$. Whitt also uses the reflected time change $(-r)(\lambda)(t)=1-\lambda(1-t)$ in the proof (Whitt 1980, pp. 83–84).

Formalization targets

The goal is Whitt's Theorem 8.1. For every $x,y\in D$,

$$d(Rx,Ry)=d(x,y),\qquad d(rx,ry)\le 2d(x,y).$$

The second inequality also applies when both paths lie in $D_\theta$, since $D_\theta\subseteq D$. The constant is the paper's printed constant, not a parameter to optimize in this mission (Whitt 1980, Theorem 8.1, p. 83).

The milestones record four claims from the theorem's proof: reversal preserves its path spaces and has inverse behavior on its natural domains; reflected time changes stay in $\Lambda$; reversal obeys exact and bounded uniform-distance relations; and reversal interacts with time changes through $(-r)(\lambda)$. Their descriptions reproduce the printed proof sentences. The proof calls the time-change cost a “minimum” once, although equation (2.1) and the displayed calculation use a maximum. The formal target follows equation (2.1) (Whitt 1980, pp. 70, 84).

What the result gives

An isometry preserves every $J_1$ distance, so ordinary reversal preserves convergent and Cauchy sequences in this metric. The bound for $r$ makes shifted reversal Lipschitz and therefore continuous. A functional limit theorem for input paths can then be translated into one for the corresponding reversed paths whenever the path-space hypotheses hold. The result is already proved in Whitt's paper; the open work here is a machine-checked development of its definitions, supporting claims, and metric theorem.

Formalizing the result also creates reusable interfaces for endpoint-constrained càdlàg paths, left-limit reversal, uniform path distance, and reflected time changes. Those interfaces may support later statements about reversed stochastic models. This mission does not assert weak convergence of probability laws or Borel measurability; those would require a separate measurable-space development for $D$.

Mathematical difficulty

The immediate idea $t\mapsto x(1-t)$ does not preserve càdlàg paths at jumps: a right-continuous jump becomes left-continuous. The correction uses left limits, but endpoint behavior then matters. Without $x(1)=x(1-)$, the shifted reverse path need not start at the identity. The $J_1$ assertion also concerns an infimum over all allowed time changes, so a uniform-distance statement alone does not establish the theorem. These are the points at which reflection of the time axis becomes a claim about the precise path-space topology (Whitt 1980, pp. 83–84).

Formalization scope

Lean represents paths as total functions $\mathbb R\to S$; all path conditions, metrics, and equality claims read only $[0,1]$. Càdlàg membership requires right continuity and left limits within the interval, with $x(1)=x(1-)$ included in $D$. Completeness and separability are explicit because the paper calls $S$ a complete separable metric space. The additive metric group is represented by an additive commutative group with an explicit translation-invariance hypothesis. This chooses the commutative reading exemplified by $S=\mathbb R^k$; the paper uses additive notation but does not separately state commutativity.

The paper's $\Lambda$ is encoded by strict increase, continuity, and surjectivity on $[0,1]$, which characterize increasing homeomorphisms there. The paper's $d$ is equation (2.1) on both sides of the goal. Lean uses extended nonnegative distances for $\rho$ and $d$, avoiding the default value a real supremum can assign to an empty or unbounded set. The claims do not become trivial by dropping $D$ membership: it is an explicit hypothesis, and the zero path over $\mathbb R$ satisfies it. A local, sorry-free check confirms that instance. Two easier statements are excluded on purpose: the goal is stated for the $J_1$ distance $d$, not the uniform distance $\rho$, and $R$ reads the left limit $x((1-t)-)$, not the value $x(1-t)$.

The proof's first sentence says the maps are one-to-one and onto. The map $r:D\to D_\theta$ forgets an additive offset and is not injective on all of $D$; the formal milestone expresses involution for $R$ on $D$ and for the restriction of $r$ to $D_\theta$. One identity printed for $r$ with $x\in D_\theta$ also holds for every $x\in D$; the formal milestone uses that broader domain and says so in its item description. Contributions are welcome for the left-limit and time-change infrastructure as well as the four listed statements and the goal.

Selected references

• Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, pp. 67–85. DOI: 10.1287/moor.5.1.67.