The OR Formalization Drive

Motivation

Multiechelon inventory theory studies supply systems in which stock is held at several levels: here, a depot that orders from an outside supplier and a retail outlet that is replenished from the depot and faces random customer demand. The question is how much to order and ship in each period so as to minimize expected holding, shortage and ordering costs over an infinite horizon. Clark and Scarf (Management Science, 1960) showed that the finite-horizon problem of a serial system decomposes into single-location problems linked by an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) extended the decomposition to the infinite horizon under discounted and average costs, and then asked what it costs to compute an optimal policy.

In the reduced single-location problem the only nonlinear part of the one-period cost is the expected induced penalty $P^L$. Any algorithm for the reduced problem (Veinott–Wagner type policy computations, for instance) evaluates $P^L$ many times. In general each evaluation is a numerical integral. Section 4 of the paper shows that when demand is normal, $P^L$ has a closed form in the univariate and bivariate standard normal distribution functions. This mission formalizes that closed form, eq. (13) on p. 830.

Setting

Time is discrete. One-period demand is $u\sim N(\mu,\sigma^2)$ with $\sigma>0$, independent across periods. For $i\ge1$, $u^{(i)}$ is the total demand over $i$ periods. It is normal with mean $\mu^{(i)}=i\mu$ and standard deviation $\sigma^{(i)}=i^{1/2}\sigma$, density $f^{(i)}$ and cdf $F^{(i)}$. The shipment lead time from depot to outlet is $l\ge0$ and the order lead time from the supplier is $L\ge1$. The cost factors are a system-wide holding cost $h^d>0$, a retailer holding cost $h^r>0$ and a retailer shortage penalty $p^r>0$. Write $p^s=h^d+p^r$. Costs are average costs, so the discount factor is $\alpha=1$ throughout.

The retailer's one-period cost (p. 822) is

$$R(x)=-h^d(x-\mu^{(l)})+p^rE[u^{(l+1)}-x]^++(h^d+h^r)E[x-u^{(l+1)}]^+ .$$

The critical number $x^{r*}$ is a global minimizer of $R$ (property (b), p. 824). The induced penalty cost is $P(x)=0$ for $x\ge x^{r*}$ and $P(x)=R(x)-R(x^{r*})$ for $x<x^{r*}$. Its expectation over the order lead time is

$$P^L(x)=E\,P[x-u^{(L)}]\qquad\text{(eq. (10))}.$$

Let $\Phi$ and $\phi$ be the standard normal cdf and density, $\Theta(z)=z\Phi(z)+\phi(z)$, and $\Phi(\xi_1,\xi_2;\rho)$ the cdf of a bivariate normal pair with standard normal marginals and correlation $\rho$. The paper defines (p. 830)

$$\tau_1(x)=-\frac{x-(x^{r*}+\mu^{(L)})}{\sigma^{(L)}},\quad \tau_2(x)=\frac{x-\mu^{(L+l+1)}}{\sigma^{(L+l+1)}},\quad \nu^{r*}=\frac{x^{r*}-\mu^{(l+1)}}{\sigma^{(l+1)}},$$ $$\tau_3(x)=-\frac{x-(x^{r*}+\mu^{(L)})-[\sigma^{(L)}/\sigma^{(l+1)}]^2[x^{r*}-\mu^{(l+1)}]}{\sigma^{(L)}\sigma^{(L+l+1)}/\sigma^{(l+1)}},$$ $$\epsilon_1(x)=\frac{\Phi[\tau_3(x)]\phi[\tau_2(x)]}{\sigma^{(L+l+1)}},\qquad \epsilon_2(x)=\frac{\Phi(\nu^{r*})\phi[\tau_1(x)]}{\sigma^{(L)}},\qquad \iota(x)=\sigma^{(L)}\Theta[\tau_1(x)],$$ $$\kappa(x)=\sigma^{(l+1)}\Theta(\nu^{r*})\Phi[\tau_1(x)]-\{[\sigma^{(L+l+1)}]^2\epsilon_1(x)-[\sigma^{(L)}]^2\epsilon_2(x)\}-[x-\mu^{(L+l+1)}]\,\Phi[\tau_1(x),\tau_2(x);\rho],$$

with $\rho=-\sigma^{(L)}/\sigma^{(L+l+1)}$.

Formalization targets

Goal: eq. (13)

For every real $x$,

$$P^L(x)=p^s\,\iota(x)-(p^s+h^r)\,\kappa(x).$$

This is an exact identity for every admissible parameter value. It holds with no constants left free.

Milestones

The milestones follow the paper's outline of the derivation on pp. 829–831:

1. eq. (11), $R(x)=p^s[\mu^{(l+1)}-x]+(p^s+h^r)\int_{-\infty}^xF^{(l+1)}(t)\,dt-h^d\mu$;
2. eq. (12), $P^L(x)=\int_{x-x^{r*}}^\infty[R(x-t)-R(x^{r*})]f^{(L)}(t)\,dt$;
3. eq. (14), $P^{L\prime}(x)=-p^s\Phi[\tau_1(x)]+(p^s+h^r)\int_{x-x^{r*}}^\infty F^{(l+1)}(x-t)f^{(L)}(t)\,dt$;
4. eq. (15), the same derivative with the integral replaced by $\Phi[\tau_1(x),\tau_2(x);\rho]$;
5. $P^L(x)\to0$ as $x\to\infty$, hence $P^L(x)=-\int_x^\infty P^{L\prime}(t)\,dt$;
6. $\iota'(x)=-\Phi[\tau_1(x)]$ and $\iota(x)\to0$;
7. the two conditional-normal identities, which give $\Phi[\tau_3(x)]$ and $\Phi(\nu^{r*})$;
8. $\frac{d}{dx}\Phi[\tau_1(x),\tau_2(x);\rho]=\epsilon_1(x)-\epsilon_2(x)$;
9. and 10. the formulas for $\epsilon_1'$ and $\epsilon_2'$;
10. $\kappa'(x)=-\Phi[\tau_1(x),\tau_2(x);\rho]$ and $\kappa(x)\to0$.

Two side remarks of p. 830 are also included: $\Theta'=\Phi$, and the simplified form of $\tau_3$.

Significance

The result. Under normal demand, (13) replaces the numerical integral (12) with a few evaluations of $\Phi$, $\phi$ and the bivariate normal cdf, all available in standard numerical libraries. Together with the decomposition results of Sections 1–3 of the paper, it makes the policy computation for the two-echelon system with normal demand no harder than a single-location computation with an explicit cost function. The same functions reappear in the paper's Section 5 for several retail outlets, after a reinterpretation of $\sigma^{(l+1)}$.

Formalizing it. The paper proves (13) only in outline: it calls the derivation "an elementary integration problem, but … sufficiently involved to warrant an outline" and leaves "tedious algebra" and "more algebra" to the reader. A machine-checked proof turns that outline into a complete argument, including the analytic steps the outline passes over: differentiation under the integral sign, the limits at $+\infty$, and the identification of an integral of normal densities with a bivariate normal probability. To our knowledge no formal proof of (13) exists, and no bivariate normal distribution function is on the platform yet.

Difficulty

The obvious approach is to substitute (11) into (12) and integrate. The result is a double integral of normal densities over a region bounded by a line, and it does not reduce to univariate functions. The paper's route is to differentiate first, identify the derivative (14) as a probability for the correlated pair $(u^{(L)},u^{(L)}+u^{(l+1)})$, and then recover $P^L$ by integrating from $+\infty$. That route needs three things: justification for differentiating under the integral in (12), whose integrand has a kink at $t=x-x^{r*}$; control of the limits at $+\infty$; and the conditional-normal identities, which involve conditioning on a null event and so must be handled through densities. The verification of $\kappa'$ is a long computation with $\Theta$, $\epsilon_1$ and $\epsilon_2$, in which every constant matters.

Formalization scope

Everything lives in the namespace FZEchelon.NormalDemand. The model data form the structure Data (fields $\mu,\sigma,h^d,h^r,p^r,l,L,x^{r*}$). The law of $u^{(i)}$ is the platform's normal demand law InventoryControl.newsboyDemand with mean $i\mu$ and standard deviation $\sqrt i\,\sigma$. Expectations are Bochner integrals, and improper integrals are set integrals over Set.Ioi/Set.Iic. $\Phi$ is cdf (gaussianReal 0 1). The bivariate cdf is the iterated integral of the explicit bivariate density over a lower-left quadrant (meaningful for $|\rho|<1$; here $\rho\in(-1,0)$). Derivatives are HasDerivAt and limits are Tendsto … atTop (𝓝 0).

Standing hypotheses of every theorem: $\sigma>0$; $h^d,h^r,p^r>0$ (p. 821); $L\ge1$; and $x^{r*}$ minimizes $R$. Two of these are added to the page and disclosed. $\sigma>0$ is needed because every $\tau$ divides by some $\sigma^{(i)}$. $L\ge1$ is needed because $\sigma^{(0)}=0$, and the paper treats zero order lead time separately (p. 819). Demand is exactly normal, as in §4, which acknowledges that this violates $u\ge0$ and ignores the objection. No nonnegativity, truncation or approximation enters. The goal fixes $\alpha=1$, the average-cost case the section restricts to. The discounted analogue is not part of this mission.

A trivializing formalization is ruled out: every Bochner integral in the statements has an integrable integrand, since integrands grow at most linearly and the normal law has all moments. No division by a zero standard deviation can occur under the hypotheses. A sorry-free check in the workspace shows that all hypotheses hold together, with a minimizer $x^{r*}$ of $R$ proved to exist.

Needed infrastructure: properties of gaussianReal (moments, convolution of independent normals), differentiation of parametric integrals, and a bivariate normal distribution function with its partial derivatives. A reusable treatment of the bivariate normal cdf, linking the density form used here to Mathlib's multivariateGaussian, would be a contribution of independent value. Proofs of individual milestones are welcome in any order.

Selected references

• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525

Motivation

Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.

Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).

Timeline:

• 1960: Clark and Scarf, finite-horizon decomposition, with a nonstationary penalty $\hat P_n$ built from the outlet's optimal cost functions.
• 1963: Iglehart (Management Science 9) proved, for the single-location discounted problem, that the finite-horizon value functions converge uniformly and that an $(s,S)$ policy is optimal.
• 1984: Federgruen and Zipkin combine the two results and prove that a stationary policy built from the decomposition is optimal for the infinite-horizon discounted and average-cost problems.

Setting

Time is discrete. The cost data are a fixed order cost $K$, an order cost rate $c^d$, a shipment cost rate $c^r$, a holding cost rate $h^d$ on all system stock, an extra holding cost rate $h^r$ at the outlet, and a backorder penalty rate $p^r$; all are positive. The discount factor $\alpha$ satisfies $0 \le \alpha < 1$, shipments take $l$ periods and orders take $L$ periods. One-period demands are independent copies of a nonnegative continuous random variable $u$ with mean $\mu < \infty$, and $u^{(i)}$ denotes the sum of $i$ copies.

The state is $(\hat y, v^d, x^r)$:

• $\hat y = (y^1, \dots, y^L)$ lists the outstanding orders, $y^i$ placed $i$ periods ago;
• $v^d$ is the depot's echelon inventory (its own stock plus $x^r$);
• $x^r$ is the outlet's stock plus shipments in transit.

An action is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$. With demand $u$, the next state is $((y, y^1, \dots, y^{L-1}), v^d + y^L - u, x^r + z - u)$. The one-period cost is

$$c^d(y) + h^d(v^d + y^L) + c^r z + R(x^r + z),$$

where $c^d(y) = K + c^d y$ for $y > 0$, $c^d(0) = 0$, and

$$R(x) = \alpha^l\{-h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r)E[x - u^{(l+1)}]^+\}.$$

$B^\alpha(s \mid \pi)$ is the expected total discounted cost of a policy $\pi$ from state $s$.

The critical number $x^{r*}$ minimizes $(1-\alpha)c^r x + R(x)$. The stationary induced penalty is $P(x) = 0$ for $x \ge x^{r*}$ and $P(x) = (1-\alpha)c^r(x - x^{r*}) + R(x) - R(x^{r*})$ otherwise. The depot problem $IH^d_\alpha$ has state $(\hat y, v^d)$, action $y \ge 0$ and one-period cost $c^d(y) + h^d(v^d + y^L) + P(v^d + y^L)$. The policy $\pi_\alpha^*$ orders by an optimal stationary policy $\sigma^d$ of $IH^d_\alpha$ and ships $z = \max\{0, \min\{x^{r*}, v^d + y^L\} - x^r\}$: up to the critical number when the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 1 (p. 827)

Assume $\alpha^l p^r \ge (1-\alpha^l)h^d$. For every state with $\hat y \ge 0$ and $x^r \le v^d$, and every admissible policy $\pi$,

$$B^\alpha(\hat y, v^d, x^r \mid \pi_\alpha^*) \le B^\alpha(\hat y, v^d, x^r \mid \pi).$$

The goal leaves the form of $\sigma^d$ open: any optimal stationary depot policy will do, and no $(s,S)$ structure is assumed.

Milestones

The milestones follow the paper's own route. Write $\hat g_n$, $g_n^r$, $\hat g_n^d$, $g_n^d$ for the $n$-period optimal costs of the system, of the outlet, of the depot with penalties $\hat P_n$, and of the depot with penalty $P$.

• Eq. (4): $\hat g_n = \hat g_n^d + g_n^r$.
• Property (e): $g_n^r \to g^r = B^{r\alpha}$.
• §2 claim (Iglehart): $g_n^r \to g^r$ uniformly on $(-\infty, x^{r*}]$.
• Lemma 1: $\hat P_n \to P$ uniformly on $\mathbb R$.
• Lemma 2: $\hat g_n^d - g_n^d \to 0$ uniformly.
• Lemma 3: $\hat g_n \to g^d + g^r$.
• Lemma 4: $g$ satisfies the optimality equation (8), and $\pi_\alpha^*$ attains it.

Significance

The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty $P$ that is written in terms of $R$ alone. Computing $P$ does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate $P$ in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.

The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.

Difficulty

The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties $\hat P_n$, built from the outlet's optimal costs $g_{n-1}^r$, and its value functions are not those of any stationary problem. The comparison of $\hat P_n$ with $P$ needs uniform control over the whole real line. The first few $\hat P_n - P$ are in fact unbounded, since $g_0^r = 0$ has the wrong slope. The uniform control therefore holds only for large $n$, and the error has to be propagated through the depot recursion.

The second obstacle is that the one-period costs are unbounded in both directions: $h^d v$ is negative for negative $v$. Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation $\alpha^l p^r \ge (1-\alpha^l)h^d$, and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.

Formalization scope

Everything lives in the namespace FZEchelon.Discounted.

• Model. The data form a structure Model. The pipeline $\hat y$ is a vector indexed by $\{0, \dots, L-1\}$, whose index $k$ is the paper's $y^{k+1}$. For $L = 0$ the current order arrives at once.
• Policies and cost. Time runs forward with weight $\alpha^k$; the paper counts periods remaining. Policies are measurable, non-anticipative, deterministic and history dependent, and they must be feasible along every demand path. $B^\alpha$ is an extended real: the expectation of the positive part of the discounted cost sum minus that of the negative part, under the product law of the demands.
• Finite-horizon programs. These are real infima over the feasible actions.
• Hypotheses. Statements quantify over the physical states $\hat y \ge 0$, $x^r \le v^d$. The standing assumptions of §1 are bundled in StandingAssumptions: positive costs, $0 \le \alpha \le 1$, demand nonnegative, atomless and of finite mean. The §2 statements add $\alpha < 1$ and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers $x^{r*}$ and $x_n^{r*}$ enter as minimizers. The depot policy $\sigma^d$ enters as a measurable, nonnegative stationary policy that is optimal for $IH_\alpha^d$; that is the paper's definition of $\pi_\alpha^*$, and its existence is Iglehart's.
• Ruled out. Comparing $\pi_\alpha^*$ only against stationary policies, or reading $B^\alpha$ as a bare series or a truncated sum, would trivialize or change the theorem. The comparison class is all admissible history-dependent policies.
• Corrections. Where the paper says "bounded" for every $n$ (§2 claim, Lemmas 1 and 2), the statements claim boundedness only where it holds: $n \ge 1$, $n \ge 2$, and eventually, respectively. The moderation notes give the counterexample at $n = 1$. Lemma 2 also carries the standing assumption of p. 821 that never ordering is not optimal. The statement is false without it.
• Infrastructure. A complete development needs the convexity theory of the single-location newsvendor function $R$, value iteration for discounted models with costs bounded below, and the Markov property for the product measure on demand sequences. The control-system file is reusable for other inventory and queueing missions. Formalizations of Iglehart's theorem and of Bertsekas–Shreve Propositions 9.12 and 9.16 are welcome.

Selected references

• A. Federgruen, P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark, H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

Large call centers route several types of customers to a common pool of agents. When the pool is large and highly utilized, the relevant asymptotic regime is the quality-and-efficiency-driven (QED) or Halfin–Whitt regime (Halfin & Whitt 1981). The number of servers $n$ grows while the offered load stays within $O(\sqrt n)$ of $n$. Waiting is then neither negligible nor overwhelming (Gans, Koole & Mandelbaum 2003).

Which class should a freed agent serve next? Exact optimization of a multi-class many-server queue with abandonment is intractable. The standard route is to solve a limiting diffusion control problem and translate its optimal control back into a policy for the queue. Atar, Mandelbaum and Reiman (Ann. Appl. Probab. 2004) carried this out for $k$ customer classes, exponential service and abandonment, general renewal arrivals and general convex-type holding costs. They proved that the translated policy is asymptotically optimal. This mission formalizes that result for the preemptive policy.

Context:

• Harrison & Zeevi (2004) studied the same multi-class many-server problem.
• Bell & Williams (2001) proved asymptotic optimality of a threshold policy for a two-server system in conventional heavy traffic.
• The present paper is the first to cover the QED regime with general costs and abandonment.

Setting

There are $k\ge1$ customer classes and $n$ identical servers.

Primitives.

• Arrivals. Class-$i$ customers arrive according to a renewal process $A^n_i$ with interarrival times $\check U_i(j)/\lambda^n_i$. Here the $\check U_i(j)$ are i.i.d., positive, of mean one and squared coefficient of variation $C^2_{U,i}$.
• Service. Service times are exponential with rate $\mu^n_i$, represented by Poisson processes $S^n_i$.
• Abandonment. Waiting customers abandon at rate $\theta^n_i\ge0$, represented by Poisson processes $R^n_i$.

State. $X^n_i(t)$ is the number of class-$i$ customers in the system, $\Psi^n_i(t)$ the number in service and $\Phi^n_i=X^n_i-\Psi^n_i$ the number waiting. The dynamics are

$$X^n_i(t)=X^{0,n}_i+A^n_i(t)-R^n_i\Big(\int_0^t\Phi^n_i\Big)-S^n_i\Big(\int_0^t\Psi^n_i\Big),\qquad \Psi^n,\Phi^n\in\mathbb Z^k_+,\quad \textstyle\sum_i\Psi^n_i\le n .$$

Policies.

• A scheduling control policy (SCP) is the process $\Psi^n$.
• It is admissible if it does not anticipate the future beyond the time of the next arrival: past information is independent of future primitive increments.
• It is work-conserving if no server idles while customers wait: $(\mathbb 1\cdot X^n-n)^+=\mathbb 1\cdot\Phi^n$.

Scaling and cost. In the QED scaling $n^{-1}\lambda^n_i\to\lambda_i$ with $\sum_i\lambda_i/\mu_i=1$. With $\rho_i=\lambda_i/\mu_i$ the centred processes are $\hat X^n=n^{-1/2}(X^n-\rho n)$, $\hat\Phi^n=n^{-1/2}\Phi^n$ and $\hat\Psi^n=n^{-1/2}(\Psi^n-\rho n)$. The cost is

$$C^n=E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n(t),\hat\Psi^n(t))\,dt .$$

The limiting control problem. It controls

$$X(t)=x+rW(t)+\int_0^t b(X(s),u(s))\,ds,\qquad b(x,u)=\ell+(\mu-\theta)(\mathbb 1\cdot x)^+u-\mu x,$$

where the control $u$ takes values in the simplex $\mathbb S^k$ and $W$ is a $k$-dimensional Brownian motion. The data are $r_i=(\lambda_iC^2_{U,i}+\lambda_i)^{1/2}$ and $\ell_i=\hat\lambda_i-\rho_i\hat\mu_i$. Its value $V(x)$ is the infimum of $E\int_0^\infty e^{-\gamma t}L(X,u)\,dt$, with $L(x,u)=\tilde L((\mathbb 1\cdot x)^+u,x-(\mathbb 1\cdot x)^+u)$.

HJB equation and the proposed policy. The HJB equation is $\tfrac12\sum_ir_i^2\partial_{ii}f+H(x,Df)-\gamma f=0$ with $H(x,p)=\inf_{u\in\mathbb S^k}[b(x,u)\cdot p+L(x,u)]$. Let $h$ be a measurable selection of its minimizers. The proposed preemptive policy (P-SCP) sets the queue vector to $\Theta[(\mathbb 1\cdot X^n-n)^+h(\hat X^n)]$, an integer rounding, and falls back to a static priority rule when that is infeasible.

Formalization targets

Goal: Theorem 2(i)

For a $C^2_{\mathrm{pol}}$ solution $f$ of the HJB equation, a measurable minimizer selection $h$, and initial states with $\hat X^{0,n}\to x$:

$$\lim_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^{n,*}_t,\hat\Psi^{n,*}_t)\,dt\;\le\;\liminf_{n\to\infty}E\int_0^\infty e^{-\gamma t}\tilde L(\hat\Phi^n_t,\hat\Psi^n_t)\,dt$$

This holds for every sequence of work-conserving admissible SCPs, and the left-hand limit exists and is finite. No constants are hard-coded.

Milestones

The milestones follow the proof:

• on the diffusion side, Proposition 2 (well-posedness), Proposition 4 (stability and moment bounds), Proposition 5(i)–(ii) (growth and continuity of $V$) and Theorem 3 ($V$ is the unique $C^2_{\mathrm{pol}}$ HJB solution, and an optimal Markov policy exists);
• on the queueing side, Proposition 1 (feedback rules give admissible SCPs), Lemmas 2–3 (moment bounds), Lemma 4(i)–(ii) (FCLT for the primitives and the fluid limit $(\bar\Psi^n,\bar\Phi^n)\Rightarrow(\rho,0)$), and Theorem 4(i)–(ii): $\liminf\ge V(x)$ always, and $\limsup\le V(x)$ under condition (49).

Significance

The result. Theorem 2(i) justifies using the diffusion control problem as a design tool for multi-class many-server systems. The policy is explicit given $h$, and it is optimal in the limit against all non-anticipating work-conserving policies, including those that use the full history and the time of the next arrival. The proof also identifies the limit cost with $V(x)$.

Formalizing it. The result is proved on paper, with some steps (Proposition 1, the principle of optimality, the time-change and martingale limit theorems) given as sketches or citations. No part of it is machine-checked. A formalization requires:

• a counting-process model of the queue;
• a careful definition of non-anticipation;
• a pathwise controlled SDE;
• classical solvability of a semilinear elliptic HJB equation on $\mathbb R^k$;
• a weak-convergence argument in Skorokhod space.

Each of these is reusable well beyond this paper.

Difficulty

The obvious argument would show that $\hat X^n$ converges to the controlled diffusion and pass the costs to the limit. This fails for two reasons:

• the comparison class contains arbitrary non-Markov, history-dependent policies, so the queue does not converge to a single controlled diffusion;
• the optimal selector $h$ is in general discontinuous (for linear costs it is), so the proposed policy is not a continuous function of the state.

The proof instead compares every policy with the HJB solution through Itô's formula on the prelimit processes. This needs:

• uniform moment bounds;
• tightness of the integral processes;
• the convergence of stochastic integrals of Kurtz and Protter;
• and, for the proposed policy, the fact that the rounding $\Theta$ and the priority fallback perturb the minimizer by $O(n^{-1/2})$.

Existence of a classical HJB solution on all of $\mathbb R^k$, with only Hölder-continuous costs and polynomial growth, rests on a bounded-domain existence theorem for fully nonlinear elliptic equations.

Formalization scope

The Lean development commits to the following conventions.

• Indexing and norms. Classes are Fin k with $k\ge1$; paper class $i$ is index $i-1$, so "class $k$" (highest priority, rounding remainder of $\Theta$) is the last index. Vectors are Fin k → ℝ and $\|\cdot\|$ is the paper's $\ell^1$ norm; the paper's $|\cdot|$ on vectors is read the same way.
• Probability space and paths. All systems share one complete probability space. Time is real and every condition is for $t\ge0$. The paper's "without loss" path regularity (finite arrival counts, Poisson paths $\mathbb Z_+$-valued, nondecreasing and càdlàg) holds for every $\omega$.
• Poisson processes are defined by independent Poisson increments; rate $0$ gives the zero process.
• Policies. A policy is a pair of real processes $(\Psi^n,X^n)$ with integer values. Admissibility is Definition 2 verbatim, with the future $\sigma$-field built from the next arrival time $\tau^n_i(t)$. Work conservation is (18).
• Costs and value are lower Lebesgue integrals in $[0,\infty]$, and $\lim$/$\liminf$ are taken there. The integrands are nonnegative under work conservation.
• Admissible systems range over sample spaces Ω : Type (universe 0). "Complete filtered probability space" means $P$ complete with all null sets in $\mathcal F_0$. Brownian motion is Mathlib's IsBrownianReal per coordinate, with independence and the $(\mathcal F_t)$-Brownian property stated explicitly. $V$ is the infimum over systems and their controlled processes.
• Discount rate. $\gamma>0$ is a hypothesis; the paper leaves it implicit.
• Initial states are integer vectors $X^{0,n}\in\mathbb Z^k_+$ with $n^{-1/2}(X^{0,n}-\rho n)\to x$. The literal "$\hat X^{0,n}\in n^{-1/2}\mathbb Z^k$" would require $\rho_in\in\mathbb Z$. Assumption 1(ii) is not imposed: each policy chooses its own initial split.
• Lemma 3 is stated for all $n$ beyond a threshold that depends on the sequence, with constants $c,\bar m$ chosen before $x$ and the sequence. The printed all-$n$ bound with $c$ independent of $x$ fails when the early terms $\hat X^{0,n}$ are large.
• Weak convergence to a continuous limit uses the coupling form CouplingConverges of the published BellWilliams2001.ThresholdPolicy.Paths; convergence to a deterministic limit is UocInProb.

The goal hypothesizes $f$ and $h$ with the pointwise identity $b(x,h(x))\cdot Df(x)+L(x,h(x))=H(x,Df(x))$ for all $x$. An arbitrary "optimal Markov control policy" may differ from a minimizer selection on the Lebesgue-null lattice where $\hat X^n$ lives, and that formalization would make the goal false. Restricting the comparators to feedback, Markov or nonpreemptive policies, fixing $k$, dropping abandonment, specializing to Poisson arrivals or linear costs, or imposing a common initial split would each trivialize or weaken the statement and is ruled out.

Not formalized:

• Lemma 4(iii) (tightness);
• Lemma 5 (Kurtz–Protter, which needs semimartingale theory absent from Mathlib);
• Lemma 6 (convergence of Stieltjes integrals at limit points);
• Proposition 5(iii);
• the nonpreemptive results, Theorem 2(ii)–(iii).

Contributions are welcome on any milestone, and especially on infrastructure: Poisson and renewal processes, functional central limit theorems in Skorokhod space, classical solvability of elliptic HJB equations, and measurable selection of minimizers.

Selected references

• R. Atar, A. Mandelbaum, M. I. Reiman, Scheduling a multi class queue with many exponential servers: asymptotic optimality in heavy traffic, Ann. Appl. Probab. 14(3), 2004. https://arxiv.org/abs/math/0407058
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone call centers: tutorial, review, and research prospects, Manuf. Serv. Oper. Manag. 5(2), 2003. https://doi.org/10.1287/msom.5.2.79.16071
• J. M. Harrison, A. Zeevi, Dynamic scheduling of a multiclass queue in the Halfin–Whitt heavy traffic regime, Oper. Res. 52(2), 2004. https://doi.org/10.1287/opre.1040.0109
• S. L. Bell, R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Ann. Appl. Probab. 11(3), 2001. https://doi.org/10.1214/aoap/1015345343
• T. G. Kurtz, P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19(3), 1991. https://doi.org/10.1214/aop/1176990334

Motivation

Most stochastic programs of practical size, such as two-stage recourse models in energy, finance or supply-chain planning, cannot be solved exactly: the expectation in the objective is a high-dimensional integral. The standard remedy is sample average approximation (SAA): replace the expectation by an average over a Monte Carlo sample and solve the resulting deterministic problem. This produces a candidate solution $\hat x$ but says nothing about how good it is. A decision maker needs a statistical certificate: an interval that contains the candidate's optimality gap with a prescribed probability.

Mak, Morton and Wood (Oper. Res. Lett. 24, 1999) built such a certificate from $n_g\ge 30$ independent SAA replications, which requires solving at least 30 optimization problems. Bayraksan and Morton (preprint January 2005, published in Math. Program. 108, 2006) showed that a single replication suffices asymptotically, and gave two variants that use two replications. This mission formalizes their validity theorems.

Setting

Let $\tilde\xi$ be a random vector with distribution $\mu$ on a measurable space $\Xi$, let $X\subseteq\mathbb R^d$ be a set of decisions, and let $f:\mathbb R^d\times\Xi\to\mathbb R$ be a cost. The stochastic program is

$$z^*=\min_{x\in X} Ef(x,\tilde\xi). \qquad\text{(SP)}$$

Its optimal set is $X^*$, and the optimality gap of a candidate $\hat x\in X$ is $\mu_{\hat x}=Ef(\hat x,\tilde\xi)-z^*\ge 0$. The paper assumes throughout:

• (A1) $f(\cdot,\tilde\xi)$ is continuous on $X$, with probability one;
• (A2) $E\sup_{x\in X} f^2(x,\tilde\xi)<\infty$;
• (A3) $X$ is nonempty and compact.

Let $\tilde\xi^1,\tilde\xi^2,\dots$ be i.i.d. copies of $\tilde\xi$, and write $\bar f_n(x)=\frac1n\sum_{i=1}^n f(x,\tilde\xi^i)$. The SAA problem is $z_n^*=\min_{x\in X}\bar f_n(x)$ (SP$_n$), with an optimal solution $x_n^*$. The gap estimator is $G_n(\hat x)=\bar f_n(\hat x)-z_n^*$ (display (2)), and the sample variance of the differences $f(\hat x,\tilde\xi^i)-f(x,\tilde\xi^i)$ is

$$s_n^2(x)=\frac1{n-1}\sum_{i=1}^n\Big[\big(f(\hat x,\tilde\xi^i)-f(x,\tilde\xi^i)\big)-\big(\bar f_n(\hat x)-\bar f_n(x)\big)\Big]^2,$$

with population counterpart $\sigma^2_{\hat x}(x)=\operatorname{var}[f(\hat x,\tilde\xi)-f(x,\tilde\xi)]$. Finally $z_\alpha$ is defined by $P(N(0,1)\le z_\alpha)=1-\alpha$.

The single replication procedure (SRP) solves (SP$_n$) once and reports the one-sided interval $\big[0,\ G_n(\hat x)+z_\alpha s_n(x_n^*)/\sqrt n\big]$ (display (5)). The I2RP takes the variance from a second, independent sample $\tilde\xi^{n+1},\dots,\tilde\xi^{2n}$ and its own minimizer $x_n^{2*}$. The A2RP runs the SRP on both halves of a sample of size $2n$, averages the gaps and the variances as in (10), and scales by $\sqrt{2n}$.

Formalization targets

Goal: Theorem 2 (p. 7)

Under (A1)–(A3), for $\hat x\in X$ and $0<\alpha<1$, provided $\alpha\le1/2$ or $\sigma^2_{\hat x}(x^*_{\max})>0$ (see Formalization scope),

$$\liminf_{n\to\infty}P\left(\mu_{\hat x}\le G_n(\hat x)+\frac{z_\alpha s_n(x_n^*)}{\sqrt n}\right)\ge 1-\alpha. \qquad(6)$$

Consistency (Proposition 1, p. 6)

The milestones follow the paper's own proof:

1. the uniform strong law $\sup_{x\in X}|\bar f_n(x)-Ef(x,\tilde\xi)|\to 0$ w.p.1;
2. (i) $z_n^*\to z^*$ w.p.1;
3. (ii) every limit point of $\{x_n^*\}$ lies in $X^*$ w.p.1;
4. the uniform convergence $s_n^2\to\sigma^2_{\hat x}$ on $X$ w.p.1;
5. (iii) $\sigma^2_{\hat x}(x^*_{\min})\le\liminf_n s_n^2(x_n^*)\le\limsup_n s_n^2(x_n^*)\le\sigma^2_{\hat x}(x^*_{\max})$ w.p.1, where $x^*_{\min}$ and $x^*_{\max}$ minimize and maximize $\sigma^2_{\hat x}$ over $X^*$;
6. the $\varepsilon$-bound of the proof of Theorem 2: if $\alpha\le 1/2$ and $\sigma^2_{\hat x}(x^*_{\min})>0$, then for $0<\varepsilon<1$ the liminf in (6) is at least $\Phi((1-\varepsilon)z_\alpha)$.

Companions

Theorem 3 (p. 9) and Theorem 4 (p. 10) are the same coverage statement for the I2RP and the A2RP. Three further statements are included: the negative bias $Ez_n^*\le z^*$ of display (1), the pathwise bound $G_n(\hat x)\ge\bar f_n(\hat x)-\bar f_n(x)$ for $x\in X$, and the consistency $\liminf_n s_n'^2\ge\sigma^2_{\hat x}(x^*_{\min})$ of the pooled variance.

Significance

Theorem 2 makes a single SAA solve enough for an asymptotically valid upper confidence bound on the optimality gap. It cuts the computational cost of the multiple-replication procedure by a factor of about thirty, and it needs no asymptotic normality of $G_n(\hat x)$, which typically fails when (SP) has several optimal solutions. The two-replication variants lessen the small-sample under-coverage of the SRP. The single- and two-replication estimators were later reused in sequential sampling procedures for SAA.

As far as is known, none of these results has been machine-checked. A complete formalization needs a uniform strong law of large numbers over a compact parameter set, which is a reusable result in its own right, together with the SAA consistency theory and a central-limit argument for a statistic that is not itself asymptotically normal.

Difficulty

The obvious route would be to show that $G_n(\hat x)$ is asymptotically normal and apply a standard confidence-interval argument. That fails: $z_n^*$ is a minimum of sample averages, and when $X^*$ is not a singleton its limit law is the law of a minimum of correlated Gaussians, not a Gaussian. The paper's argument has to bound the coverage from below without that limit law. It also needs to control the sample variance at a random, non-convergent minimizer $x_n^*$, which only accumulates on $X^*$. The uniform strong law (Rubinstein–Shapiro, Lemma A1) on which both consistency statements rest is not in Mathlib.

Formalization scope

The Lean development uses these conventions:

• Decisions live in EuclideanSpace ℝ (Fin d). The paper's $\mathbb R^n$ is renamed $\mathbb R^d$ because $n$ is the sample size.
• $\mu$ is a probability measure on $\Xi$ (the law of $\tilde\xi$), and $Ef(x,\tilde\xi)$ is the Bochner integral $\int f(x,\cdot)\,d\mu$.
• The sample is one infinite i.i.d. sequence ξ : ℕ → Ω → Ξ on a probability space $(\Omega,P)$, 0-based: $\tilde\xi^i$ is ξ (i-1). The second sample of Theorems 3–4 is ξ n, …, ξ (2n-1), exactly as printed, and the A2RP's "random" partition is this fixed one, which has the same joint law.
• Estimators are functions of a sample path. $z^*$ and $z_n^*$ are infima of images of $X$, and $X^*$ is an argmin set.
• Probabilities are ℝ≥0∞-valued, so the liminf in (6) is genuine. Proposition 1 (iii) is stated in its equivalent $\varepsilon$-form, which avoids real liminf/limsup junk values.
• $z_\alpha$ is any real with cdf (gaussianReal 0 1) zα = 1 - α.

Standing assumptions and pins. Every goal-level statement carries (A1)–(A3) and the i.i.d. hypothesis. Three hypotheses are made explicit that the paper leaves implicit:

1. $f(x,\cdot)$ is measurable for each $x$ ("$f(x,\tilde\xi)$ is a random variable");
2. $x_n^*$ is a measurable map that, almost surely, lies in $X$ and minimizes $\bar f_n$ over $X$ on the same sample;
3. (A2) is read as "$\sup_{x\in X}f^2(x,\cdot)$ has an integrable majorant", which avoids proving that the supremum is measurable.

At $n\le 1$ the factors $1/n$, $1/(n-1)$ and $1/\sqrt n$ evaluate to Lean's $0$; every coverage statement is a liminf and ignores them.

Several encodings would trivialize the statement, and all are ruled out. The minimizer $x_n^*$ must minimize the SAA problem of its own sample: a free $x_n^*$, or one fitted to the other sample, would change the theorem. The second sample must not be replaced by an independent sequence. The quantile must not be pinned through an sInf. Positivity of $\sigma^2_{\hat x}(x^*_{\min})$ is a hypothesis only of the $\varepsilon$-bound, as on p. 8.

One correction of the paper. Theorems 2 and 4 are stated for every $0<\alpha<1$, but for $\alpha>1/2$ the paper's argument (replace $x^*_{\min}$ by $x^*_{\max}$) needs $\sigma^2_{\hat x}(x^*_{\max})>0$, and without it both statements are false: for $X=[-1,1]$, $f(x,\xi)=x^2-2x\xi$, $\tilde\xi\sim N(0,1)$, $\hat x=0$ and $\alpha=0.9$, the SRP coverage tends to about $0.010$ and the A2RP coverage to $e^{-2z_\alpha^2}\approx0.037$, both below $0.1$. The Lean goal and Theorem 4 therefore carry the hypothesis "$\alpha\le1/2$, or $\sigma^2_{\hat x}(x)>0$ for some $x\in X^*$". Theorem 3 is stated as printed.

Contributions are welcome at every level. The most reusable one is the uniform strong law of large numbers for Carathéodory integrands on a compact set with an integrable envelope, which also serves other SAA consistency results.

Selected references

• G. Bayraksan, D. P. Morton, Assessing Solution Quality in Stochastic Programs, preprint (January 26, 2005); published in Math. Program. 108 (2006). https://doi.org/10.1007/s10107-006-0720-x
• W. K. Mak, D. P. Morton, R. K. Wood, Monte Carlo bounding techniques for determining solution quality in stochastic programs, Oper. Res. Lett. 24 (1999) 47–56. https://doi.org/10.1016/S0167-6377(98)00054-6
• R. Y. Rubinstein, A. Shapiro, Discrete Event Systems: Sensitivity Analysis and Stochastic Optimization by the Score Function Method, Wiley, 1993 (Lemma A1, p. 67; Theorem A1, p. 69).
• A. Shapiro, Monte Carlo sampling methods, in: Handbooks in OR & MS 10, Stochastic Programming, Elsevier, 2003, 353–425. https://doi.org/10.1016/S0927-0507(03)10006-0

Motivation

A firm holds a fixed stock of a perishable or seasonal product: airline seats, hotel rooms, fashion goods, tickets. It must sell the stock over a finite season, and whatever is left at the end is worth nothing. The firm can change its price at any time, and demand responds to the price at random. Should it adjust its price continually as sales occur and time runs out, or is one well-chosen price nearly as good?

Gallego and van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), set up this question as a continuous-time stochastic control problem and answered it. The source for this mission is the published 1994 article. Its answer is quantitative: the expected revenue of a single fixed price is within a factor $1-1/(2\sqrt{\min\{n,\lambda^*t\}})$ of the best possible dynamic policy. The paper is one of the founding results of dynamic pricing in revenue management. The deterministic (fluid) upper bound it introduced became the standard benchmark of the field, and later work on re-solving heuristics, network revenue management and learning-while-pricing builds on it.

Setting

Demand. The firm chooses a demand intensity $\lambda$ from an interval $\Lambda\ni 0$ of allowable rates, and the market charges the inverse-demand price $p(\lambda)$. On nonzero rates, $p$ is strictly decreasing and nonnegative; rate $0$ corresponds to the null price $p_\infty$, at which nothing sells. The revenue rate is $r(\lambda)=\lambda p(\lambda)$. It has $r(0)=0$, and it is continuous, concave and bounded on $\Lambda$. $\lambda^*$ denotes its least maximizer, and $p^*=p(\lambda^*)$, $r^*=r(\lambda^*)$. Such data form a regular demand function (§2.1).

The stochastic problem. At time $0$ the firm holds $n$ items and has a horizon $[0,t]$. A non-anticipating pricing policy $u$ chooses the intensity $\lambda_s\in\Lambda$ at each elapsed time $s$ as a function of the sales history so far. Sales follow a Poisson process with this controlled intensity, and at most $n$ items can be sold. A sale at time $s$ earns the current price $p_s$. The expected revenue is $J_u(n,t)=E_u[\int_0^t p_s\,dN_s]$, where $N_s$ counts the sales, and the optimal expected revenue is $J^*(n,t)=\sup_u J_u(n,t)$.

The deterministic problem. Replacing random sales by their rates gives

$$J^D(x,t)=\sup\Big\{\int_0^t r(\lambda(s))\,ds:\ \lambda(s)\in\Lambda,\ \int_0^t\lambda(s)\,ds\le x\Big\}.$$

It is solved by the constant rate $\lambda^D=\min\{\lambda^*,x/t\}$ (Proposition 2).

Fixed-price heuristics. $J^{FP}(n,t)$ is the expected revenue of charging $p^D=p(\lambda^D)$ for the whole horizon. $J^{OFP}(n,t)$ is the expected revenue of the best constant price.

Formalization targets

Goal: Theorem 3

For $\lambda^*>0$, $n\ge1$ and $t>0$, $J^*(n,t)$ is finite and positive, and

$$\frac{J^{OFP}(n,t)}{J^*(n,t)}\ \ge\ \frac{J^{FP}(n,t)}{J^*(n,t)}\ \ge\ 1-\frac{1}{2\sqrt{\min\{n,\lambda^*t\}}}.$$

Milestones

1. Proposition 2: $\lambda^D$ solves (11), and $J^D(x,t)=t\,r(\lambda^D)$.
2. Eqs. (13)–(14): $E_u[N_t]=E_u[\int_0^t\lambda_s ds]\le n$ and $J_u(n,t)=E_u[\int_0^t r(\lambda_s)ds]$ for every policy.
3. Eq. (15) and Lemma 1: $J_u(n,t)\le J_u(n,t,\mu)\le J^D(n,t,\mu)$ for all $\mu\ge0$.
4. The zero duality gap: $J^D(n,t)=\min_{\mu\ge0}J^D(n,t,\mu)$.
5. Theorem 2: $J^*(n,t)\le J^D(n,t)$ for all $n\ge 0$, $t\ge0$.
6. Eq. (17): a fixed price $p$ earns $p\,E[\min\{n,N_{\lambda(p)t}\}]$, with $N$ Poisson.
7. Inequality (18), Gallego's bound $E[(N-n)^+]\le(\sqrt{\sigma^2+(n-\mu)^2}-(n-\mu))/2$, already on the platform.
8. The two case bounds of the proof of Theorem 3, including (19), and the exact fixed-price revenue of the Remark.

Significance

The result. Theorem 2 says that uncertainty can only cost revenue. The deterministic value is a computable upper bound for every policy, so any heuristic can be judged against it. Theorem 3 turns this into a guarantee: with 400 items and scarce stock, a single price earns at least 97.5% of the optimum. The loss vanishes as the expected sales volume grows. This is the justification for the stable, rarely changed prices seen in practice, and the template for the asymptotic-optimality analyses that followed: fluid bounds, re-solving, bid prices.

Formalizing it. The results are proved on paper, and none is formalized. The platform has a discrete-time Bernoulli analogue of Theorem 2 (Talluri–van Ryzin, RevenueManagement.deterministic_upper_bound) and Bitran–Caldentey's periodic-review version as open items. Neither is this continuous-time model. A formalization would add a controlled Poisson sales process with a policy-dependent intensity, the compensator identities (13)–(14) for it, and a Lagrangian-duality argument over measurable rate paths. These are reusable for every continuous-time revenue-management model on the platform. Gallego's moment bound (18) is already proved there.

Difficulty

The deterministic side (Proposition 2, the duality gap) is convex analysis on one concave function. The fixed-price bounds reduce to a Poisson computation and (18). The obstacle is Theorem 2's stochastic step. The revenue is collected at random jump times chosen by an adaptive policy, and comparing it with a deterministic integral requires the compensator identity $E_u[\int p_s\,dN_s]=E_u[\int r(\lambda_s)\,ds]$ for an arbitrary non-anticipating intensity. The paper cites Brémaud's martingale theory for this, which Mathlib does not have. A first idea is to apply Jensen's inequality to $J_u$ directly. It fails because the stock constraint holds only pathwise, through $N_t\le n$, and not in expectation for a rate path. Restricting to Markovian policies does not remove the need for the identity.

Formalization scope

• Model. Rates are real numbers, and $\Lambda\subseteq[0,\infty)$ is an interval containing $0$. $p$ is a real function, strictly decreasing and nonnegative on $\Lambda\setminus\{0\}$. $r(\lambda)=\lambda p(\lambda)$ is continuous, concave and bounded above on $\Lambda$, and $\lambda^*$ is its least maximizer. $p(0)$ is never used, since the null price may be $+\infty$.
• Policies depend on elapsed time and the past sale times (the internal history); randomized policies are not included. Intensities are jointly measurable and locally integrable.
• The sales process is built from i.i.d. $\mathrm{Exp}(1)$ clocks, one per item. A sale occurs when the intensity integrated since the last sale reaches the next clock, so at most $n$ items are sold. Constraint (2) is part of the construction, not a hypothesis.
• Values. Expected revenues and $J^*$ are in $[0,\infty]$, as lower Lebesgue integrals and suprema. $J^D$ is a real supremum over measurable, integrable rate paths, nonempty and bounded for $x,t\ge0$. $J^{FP}$ and $J^{OFP}$ are expected revenues of constant-price policies of this process, and the goal also asserts $0<J^*<\infty$. Defining $J_u$ by the right side of (14), $J^*$ by the HJB equation, or $J^{FP}$ by formula (17) would trivialize the mission, and is ruled out.
• Added hypotheses. Theorem 3 assumes $n\ge1$, $t>0$ and $\lambda^*>0$, which the page leaves implicit: the ratios divide by $J^*$, which vanishes otherwise. Eqs. (13)–(14) are stated for every policy, without Proposition 1's bound $\lambda_s\le\lambda^*$, and without the reduction to Markovian policies.
• Corrected slips. (12) prints $J^D(x,t)=t\min\{r^*,r^0\}$, which is false for $x>\lambda^*t$ (exponential demand with $x=at$ gives $r^0=0$). The statement uses $t\,r(\lambda^D)$, and the printed form where $x\le\lambda^*t$. The Remark's "$E(N_n-n)^+=n(1-P\{N_n=n\})$" should read $E[\min\{N_n,n\}]$; its displayed $J^{FP}$ formula is right. Proposition 2's "the optimal solution" is stated as optimality, since uniqueness fails without strict concavity.
• Welcome contributions. Infrastructure for counting processes with stochastic intensity (the clock construction, the compensator identity), Jensen and Lagrangian duality for concave integral functionals on rate paths, and Poisson truncated-mean computations.

Selected references

• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11:55–60, 1992 (cited in the paper's references, p. 1019).
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer-Verlag, New York, 1980 (as cited in the paper).
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004 (Chapter 5; on the platform as RevenueManagement.*).
• G. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003 (on the platform as PricingRM.DetHeuristic.*).