Probability

Motivation

Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating $x \leftarrow x + \alpha\,(F(x) - x + w)$ with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).

Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping $F$: a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.

Setting

A mapping $F:\mathbb R^n\to\mathbb R^n$ with components $F_1,\dots,F_n$ is given, and the goal is to solve $F(x)=x$. Time is discrete, $t=0,1,2,\dots$. The iterate $x(t)\in\mathbb R^n$ evolves by

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr),\qquad x^i(t)=\bigl(x_1(\tau^i_1(t)),\dots,x_n(\tau^i_n(t))\bigr),$$

where $\alpha_i(t)\in[0,1]$ is a stepsize ($\alpha_i(t)=0$ when component $i$ is not updated), $w_i(t)$ is noise, and $0\le\tau^i_j(t)\le t$ are delays: the update of component $i$ may read component $j$ as it was at an earlier time. All quantities are random variables on a probability space $(\Omega,\mathcal F,P)$ with an increasing sequence of σ-fields $\{\mathcal F(t)\}$, the history up to the choice of the stepsizes at time $t$.

Vector inequalities are componentwise and $e$ is the vector of ones. The paper's assumptions are:

• Assumption 1: every delay index $\tau^i_j(t)$ tends to infinity, with probability 1.
• Assumption 2: $x(0)$, $\alpha_i(t)$, $\tau^i_j(t)$ are $\mathcal F(t)$-measurable and $w_i(t)$ is $\mathcal F(t+1)$-measurable; $E[w_i(t)\mid\mathcal F(t)]=0$; and $E[w_i^2(t)\mid\mathcal F(t)]\le A+B\max_j\max_{\tau\le t}|x_j(\tau)|^2$ for deterministic constants $A,B$.
• Assumption 3: $\sum_t\alpha_i(t)=\infty$ and $\sum_t\alpha_i^2(t)\le C$ with probability 1, for a deterministic $C$.
• Assumption 4: $F$ is monotone ($x\le y\Rightarrow F(x)\le F(y)$), continuous, has a unique fixed point $x^*$, and $F(x)-re\le F(x-re)\le F(x+re)\le F(x)+re$ for all $x$ and all $r>0$.

In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.

Formalization targets

Goal: Theorem 2 (p. 189)

Under Assumptions 1–4, if $x(t)$ is bounded with probability 1, then

$$\lim_{t\to\infty}x(t)=x^*\qquad\text{with probability 1.}$$

Boundedness is a hypothesis, not a conclusion: for monotone $F$ it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.

Milestones

1. Lemma 1 (p. 190): for a scalar recursion $W(t+1)=(1-\alpha(t))W(t)+\alpha(t)w(t)$ with martingale-difference noise whose conditional variance is bounded by an a.s. bounded $B(t)$, and stepsizes with $\sum\alpha=\infty$, $\sum\alpha^2\le C$, $W(t)\to0$ with probability 1.
2. Lemma 4 (p. 193): the sequences $U^{k+1}=(U^k+F(U^k))/2$, $U^0=x^*+re$, and $L^{k+1}=(L^k+F(L^k))/2$, $L^0=x^*-re$, satisfy $F(U^k)\le U^{k+1}\le U^k$ and $F(L^k)\ge L^{k+1}\ge L^k$.
3. Lemma 5 (p. 193): $U^k\to x^*$ and $L^k\to x^*$.
4. Lemma 6 (p. 194): on a sample path where $L^k\le x(t)\le U^k$ from time $t_k$ on and all delays exceed $t_k$ from time $t'_k$ on, $x_i(t)\le X_i(t)+W_i(t;t'_k)$, where $X_i$ relaxes from $U^k_i$ towards $F_i(U^k)$ and $W_i(t;t'_k)$ accumulates the noise from $t'_k$.
5. Lemma 7 (p. 195): under the choices of $\delta_k$ and $t''_k$ made on pp. 194–195, $x_i(t)\le U^{k+1}_i$ for all $t\ge t''_k$.

Significance

Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.

The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.

Difficulty

The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes $U^k,L^k$ to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.

Formalization scope

• Components are Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. $re$ is r • 1.
• The update is stated in the paper's unified form for every $t$, with $\alpha_i(t)=0$ off the update times; the update sets $T^i$ are not represented. The paper sets $\tau^i_j(t)=t$ off $T^i$; the formalization leaves $\tau^i_j(t)$ free there, which is more general. $\alpha_i(t)\in[0,1]$ and $\tau^i_j(t)\le t$ hold on every sample path.
• Conditional expectations are generalized, written with set integrals (CondMeanZero, CondSqLe): $\int_S w\,dP=0$ for every $\mathcal F(t)$-set $S$ on which $w$ is integrable, and $\int_S w^2\,dP\le\int_S g^+\,dP$ in $[0,\infty]$. Mathlib's condExp is not used: it is $0$ for non-integrable functions and would make the noise assumptions vacuous.
• Series conditions use partial sums (divergence to $+\infty$; every partial sum at most $C$), never tsum, which is $0$ for non-summable sequences. The constants $A,B,C$ are chosen before the almost-sure quantifier; the bound on $x(t)$ is chosen after it.
• The paper treats $x(t)$ as determined by $\mathcal F(t)$ and uses this implicitly; Theorem 2 assumes it explicitly (Adapted).
• Lemma 1 leaves $W(0)$ unconstrained, as on the page. Lemmas 4 and 5 hold for every $r>0$. Lemmas 6 and 7 are pathwise: they fix one sample path and take the induction's objects ($k$, $t_k$, $t'_k$, $t''_k$, $X$, $\delta_k$) as given with exactly the properties the paper has established for them; they are not existential statements about these times.
• A trivializing formalization (junk conditional expectations, tsum for the series, a deterministic bound on $x(t)$, or a second unrelated $x^*$) is ruled out by the choices above.

Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version $W(t;t_0)$), and lemmas on monotone maps satisfying (7).

Selected references

• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994) 185–202. https://doi.org/10.1023/A:1022689125041
• C. J. C. H. Watkins and P. Dayan, Q-learning, Machine Learning 8 (1992) 279–292. https://doi.org/10.1007/BF00992698
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994) 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://hdl.handle.net/1721.1/3719
• B. T. Poljak and Ya. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automation and Remote Control 34 (1973) 377–397.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.

Timeline.

• 1989: Watkins' thesis introduces Q-learning and sketches a convergence argument.
• 1992: Watkins and Dayan publish the proof via the action-replay process, for bounded rewards, discount $0<\gamma<1$ and learning rates satisfying condition (3) at every state–action pair.
• 1994: Jaakkola, Jordan and Singh (Neural Computation 6) and Tsitsiklis (Machine Learning 16) give proofs through stochastic approximation for asynchronous iterations, with predictable random choices of state, action and step.
• Later work (Szepesvári 1997; Even-Dar and Mansour 2003) quantifies the convergence rate.

Setting

A finite controlled Markov process has a finite state set $X$, a finite nonempty action set $\mathfrak A$ (the same in every state), mean rewards $\mathcal R_x(a)$ and transition probabilities $P_{xy}[a]$. Rewards received $s$ steps later are discounted by $\gamma^s$ with $0<\gamma<1$. The optimal action-value function $Q^*$ is the unique solution of the Bellman optimality equation

$$Q^*(x,a)=\mathcal R_x(a)+\gamma\sum_y P_{xy}[a]\max_b Q^*(y,b).$$

In the $n$-th episode the agent observes a state $x_n$, performs an action $a_n$, observes the next state $y_n$ and a reward $r_n$ of mean $\mathcal R_{x_n}(a_n)$, and updates its table with a learning rate $\alpha_n$:

$$Q_n(x,a)=\begin{cases}(1-\alpha_n)Q_{n-1}(x,a)+\alpha_n\bigl[r_n+\gamma\max_b Q_{n-1}(y_n,b)\bigr]&(x,a)=(x_n,a_n),\\ Q_{n-1}(x,a)&\text{otherwise,}\end{cases}$$

from given initial values $Q_0$. Episodes need not form a single trajectory. Writing $n^i(x,a)$ for the episode of the $i$-th visit to $(x,a)$, the learning-rate condition is

$$\sum_{i=1}^\infty\alpha_{n^i(x,a)}=\infty,\qquad\sum_{i=1}^\infty\bigl[\alpha_{n^i(x,a)}\bigr]^2<\infty\qquad\forall x,a.\tag{3}$$

The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states $\langle x,n\rangle$ (a real state and a level $n$), in which taking $a$ at $\langle x,n\rangle$ replays a randomly chosen earlier episode that tried $a$ in $x$, emitting its reward and dropping to the level below that episode. Its expected one-step reward is $\mathcal R^{(n)}_x(a)$ and its aggregated transition probabilities are $P^{(n)}_{xy}[a]$.

Formalization targets

Goal: the Theorem (p. 282)

Given bounded rewards $|r_n|\le\mathcal R$, learning rates $0\le\alpha_n<1$ and (3),

$$Q_n(x,a)\to Q^*(x,a)\quad\text{as }n\to\infty,\ \forall x,a,\ \text{with probability }1.$$

Milestones (the paper's appendix, in attack order)

• Lemma A (p. 288): $Q_n(x,a)=Q^*_{\mathrm{ARP}}(\langle x,n\rangle,a)$ for all $a,x$ and $n\ge0$.
• Lemma B.1 (p. 289): the values of $s$ actions with and without a continuation policy differ by at most $\gamma^s\mathcal R/(1-\gamma)$.
• Lemma B.2 (p. 289): started high enough, the ARP strays below any level $l$ within $s$ actions with arbitrarily small probability.
• The stochastic-convergence theorem quoted in the proof of B.3 (p. 290): $X_{n+1}=X_n+\beta_n(\xi_n-X_n)$ with $\sum\beta_n=\infty$, $\sum\beta_n^2<\infty$ and bounded $\xi_n$ of mean $\Xi$ converges to $\Xi$ almost surely.
• Lemma B.3 (p. 290): almost surely $P^{(n)}_{xy}[a]\to P_{xy}[a]$ and $\mathcal R^{(n)}_x(a)\to\mathcal R_x(a)$.
• Lemma B.4 (p. 291): rewards within $\eta$ and transition rows within $\eta/\mathcal R$ give values of $s$ actions within $\eta s(s+1)/2$.

A further item states that the optimality equation has exactly one solution for $0\le\gamma<1$.

Significance

The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD($\lambda$), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.

Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.

Difficulty

The update touches one table entry at a time, at random times chosen by the agent, and its target $r_n+\gamma\max_b Q_{n-1}(y_n,b)$ depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize $Q_n$ as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.

Formalization scope

Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:

• $X$ and $\mathfrak A$ are Fintypes with decidable equality, $\mathfrak A$ is nonempty, and $\max_b$ is Finset.sup'. The process is a structure with R x a $=\mathcal R_x(a)$ and P x a y $=P_{xy}[a]$, rows nonnegative and summing to $1$.
• $Q^*$ enters the goal through the predicate IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.
• Lean index $n$ is the paper's episode $n\ge1$; index $0$ of the episode data is unused and qIter … 0 $=Q_0$.
• Condition (3) is written over episodes: the learning rate charged to $(x,a)$ at episode $n$ is $\alpha_n$ if $(x_n,a_n)=(x,a)$ and $0$ otherwise; its partial sums tend to $+\infty$ and its squares are summable. This equals (3) and forces infinitely many visits.
• Probability model (pinned). The paper describes it in words only. On a filtered probability space, $x_n,a_n,\alpha_n$ are $\mathcal F_{n-1}$-measurable, $y_n,r_n$ are $\mathcal F_n$-measurable, $\Pr[y_n=y\mid\mathcal F_{n-1}]=P_{x_ny}[a_n]$, $\mathbb E[r_n\mid\mathcal F_{n-1}]=\mathcal R_{x_n}(a_n)$, $|r_n|\le\mathcal R$, $0\le\alpha_n<1$, and (3) holds almost surely. Fixed episode schedules with independent outcomes are a special case.
• The ARP deck at level $n$ includes card $n$ (as in the card game and Lemma A's proof); $P^{(n)}$ keeps the printed range of levels $1,\dots,n-1$; ARP optimality is over deterministic Markov policies of the ARP. Finite action sequences are lists of actions with $0$ terminal reward.
• Corrections disclosed in the items. B.1 is stated with $\le$ (the page's strict inequalities fail for a constant reward). B.4 assumes closeness of transition rows in $\ell^1$ and $s\ge1$: with the page's entrywise closeness the printed constant is false once $|X|\ge4$. The stochastic-convergence theorem is read with conditional mean $\Xi$ and adapted steps.

Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.

The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.

Selected references

• C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292. https://doi.org/10.1023/A:1022676722315
• C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989.
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994), 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. https://doi.org/10.1007/BF00993306
• H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8

Motivation

An assembly system must coordinate the production of components that meet at a common downstream item. A shortage of any required component can delay the finished product, while producing a component too early incurs holding cost. In Rosling's 1989 study, the central question is whether optimal decisions for such a tree can be understood using the simpler theory of a pure series inventory system. The paper proves an equivalence when the initial inventory positions are in a condition it calls long-run balance. That equivalence gives a precise route from an assembly network to serial inventory control without discarding its lead times or its discounted costs.

Setting

There are items $1,\ldots,N$ in a tree rooted at end item $1$. Every item $i>1$ has one immediate successor $s(i)<i$; one unit of each component is needed for an end unit. Let $l_i$ be the production or delivery lead time of item $i$. The total lead time $M_i$ is the sum of lead times on the path from $i$ to the end item, with $M_0=0$, and the equivalent lead time is $L_i=M_i-M_{i-1}$. Items are indexed so that $M_i$ is nondecreasing. These definitions and indexing conditions are in §§1–2 of the paper.

At the beginning of each period $t$, outstanding orders arrive, the controller chooses the post-order echelon position $Y_{it}$, and then demand $\xi_t$ for the end item occurs. The pre-order position is $X_{it}$, while $X^l_{kt}$ is the position of predecessor $k$ from orders old enough to arrive after its lead time. A decision is feasible when $X_{it}\le Y_{it}\le X^l_{kt}$ for every immediate predecessor $k$ of $i$. Decisions depend only on demands already observed. The demands are independent and identically distributed, nonnegative, and have a density and a finite positive mean.

The discounted Problem P charges echelon holding cost $h_i$ for item $i$ and a shortage coefficient $p+H_1$ for the end item. Its discount factor is $\alpha$. The objective is the expectation of the sum over periods of the holding charges and the expected end-item shortfall over $l_1+1$ demands, with a constant independent of the policy. The paper's Assumption requires every $h_i>0$ and $\sum_i h_i\alpha^{-M_{s(i)}}<p+H_1$. The system is in long-run balance in period $t$ when positions of adjacent items, compared at the same age relative to total lead time, satisfy equation (5):

$$X^{M_i-\mu}_{it}\le X^{M_{i+1}-\mu}_{i+1,t} \quad(1\le i<N,\ 0\le\mu<M_i).$$

Formalization targets

Equivalent series optimal policies

The equivalent series system has successor $i-1$, lead time $L_i$, the same demand law and shortage coefficient, and holding coefficient $h_i\alpha^{l_i-L_i}$. Theorem 2 states that its optimal policies and those of the assembly system agree when the assembly system is initially in long-run balance. In the formal statement, the first inclusion is unconditional; the reverse inclusion is conditional on Problem P attaining an optimum:

$$\operatorname{Opt}(P)\subseteq\operatorname{Opt}(P_{\mathrm{series}}), \qquad \operatorname{Opt}(P)\ne\varnothing \Longrightarrow \operatorname{Opt}(P_{\mathrm{series}})\subseteq\operatorname{Opt}(P).$$

The target includes Lemmas 1 and 2, Theorem 1, Corollary 1, and the cost identity displayed in the proof of Theorem 2. Lemma 1 limits excess production, Lemma 2 gives a production lower bound, Theorem 1 describes when long-run balance is reached and preserved, and Corollary 1 uses the adjacent series position in that result. Each is stated at the strength given on pp. 568–569 of the paper.

Significance

Theorem 2 identifies the same policy choices in a tree assembly problem and a series problem whose stages have modified lead times and holding coefficients. It makes the serial interpretation exact for initially balanced systems and supports the paper's later discussion of series-system calculations. The statement is an equivalence of optimal policies, rather than just an equality of numerical values, so both the feasible-policy comparison and the cost comparison matter.

The theorem and its supporting results are proved in the 1989 paper; they have not been machine-checked in this development. A complete formalization would supply a reusable account of finite-history inventory policies, random demand histories, echelon positions, and extended-real discounted objectives. The published serial model SupplyChainTheory_multiechelon represents a different stage-indexed system; the assembly tree, its initial pipeline, and Problem P still need their own definitions. The paper's order-up-to Corollary 2 relies on an extension of earlier serial results and is outside this target.

Difficulty

The first natural comparison is to replace the tree's predecessor constraints with adjacent-item constraints. Those feasible sets are not equal for arbitrary states: positions at different total lead times can cross, and initial orders placed before period 1 affect the earliest periods. Long-run balance controls the necessary position comparisons, but equation (5) is empty for an item with $M_i=0$. The printed proof also uses a middle inequality outside the range covered by equation (5) when an equivalent lead time vanishes. A faithful statement must account for these boundary cases without defining the series problem through the assembly problem's optimal policies.

Formalization scope

Items use the paper's indices $1,\ldots,N$, with $N\ge1$ and $s(1)=0$. Lean period $k$ is paper period $t=k+1$; the policy sees exactly $k$ earlier demands. The common demand law $\nu$ is a probability measure on the reals, concentrated on nonnegative values, absolutely continuous with respect to Lebesgue measure, integrable, and of positive mean. The law of demand over $l_1+1$ periods is the pushforward of a finite product law under summation. Feasibility and the optimal-policy bounds are almost-sure statements, so changes on null histories do not alter them. Pathwise balance results quantify over one nonnegative demand path.

Initial positions include the orders placed before period 1. Their ages are monotone and obey the predecessor constraints inherited from that past. In addition to the paper's initial long-run balance, a separate boundary condition carries the missing comparison when $M_i=0$. Discounting is restricted to $0<\alpha<1$: at $\alpha=1$ the paper specifies average cost through a separate limiting prescription. The formal cost lies in the extended reals and is computed from its positive and negative parts; under the Assumption, feasible policies have a finite negative part. The policy-independent constant of equation (2) is omitted from both systems. “Optimal” means feasible and no more costly than every feasible policy, never a default value of an empty infimum.

The series system is built as a second instance of the same model, using the paper's successor, lead-time, and holding-coefficient transformations. Its cost and constraint (3) are then computed by the shared definitions. Contributions toward the lead-time identities, almost-sure policy comparisons, finite-time balance theorem, and extended-real cost identity are all part of the scope.

Selected references

• Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. DOI: 10.1287/opre.37.4.565.

Motivation

Spare-parts provisioning for repairable ("recoverable") items is a classical inventory problem: aircraft components fail, are sent to repair, and a stock of spares covers the units in the repair pipeline. Sherbrooke's METRIC model (Sherbrooke 1968), developed at RAND for the U.S. Air Force, measures the performance of a stock level by the expected number of backorders, the average number of unfilled demands outstanding at a random time. Every allocation computed by METRIC is driven by this quantity, and in particular by how it depends on the mean demand of each item.

For a new item that mean is not known. Air Force practice at the time produced a single engineering estimate of mean demand and computed backorders from it as if it were exact. In the section Demand Prediction (pp. 138–139) Sherbrooke argues that this practice is biased in one direction: under Poisson demand and any positive spare stock, the point estimate always understates expected backorders whenever the true mean is genuinely uncertain. This is his reason why a Bayesian treatment of demand is "of fundamental importance for all items, not merely low-demand items". The mission formalizes that claim and the computation behind it.

Setting

Fix one item. Its spare stock $s \in \{0, 1, 2, \dots\}$ is stock on hand plus on order plus in repair, minus backorders; under one-for-one replenishment it is constant. Let the number of units in resupply at a random time be Poisson distributed with mean $\lambda > 0$:

$$p(x \mid \lambda) = e^{-\lambda}\frac{\lambda^x}{x!}, \qquad x = 0, 1, 2, \dots$$

The expected backorders at spare stock $s$ are, by the paper's eq. (2),

$$B(s \mid \lambda) = \sum_{x=s+1}^{\infty} (x - s)\, p(x \mid \lambda).$$

In eq. (2) the mean is $\lambda T$ (customer rate times mean resupply time); on p. 138 it is the mean demand over a unit time interval. Only the mean enters, so it is written as one parameter $\lambda$. In Lean this is SherbrookeMetric.PointEstimate.backorders s lam, built on the published Poisson probabilities ServiceParts.StockLevels.poissonPmf.

Uncertain mean demand. The true mean takes the values $\lambda_k > 0$, $k \in K$ ($K$ finite), with probabilities $w_k \ge 0$, $\sum_k w_k = 1$. The point estimate is the mean of this distribution, $\bar\lambda = \sum_k w_k \lambda_k$, and the expected backorders accounting for the uncertainty are $\sum_k w_k B(s \mid \lambda_k)$. The paper's example (p. 138) takes $\lambda \in \{0.5, 1.5\}$ with probability $0.5$ each, so $\bar\lambda = 1$; its procedure (p. 139) discretizes a gamma prior to five to ten values.

Formalization targets

Goal: the point estimate understates backorders (pp. 138–139)

If two distinct values $\lambda_k \ne \lambda_{k'}$ both carry positive probability, then for every spare stock $s \ge 1$

$$B(s \mid \bar\lambda) < \sum_k w_k\, B(s \mid \lambda_k),$$

and for $s = 0$ the two sides are equal for every prior. The goal fixes no constants and no particular prior.

Milestones

1. Eq. (10), p. 139: for $\lambda > 0$, $B(s \mid \cdot)$ is twice differentiable at $\lambda$ with

$$\frac{\partial^2 B(s \mid \lambda)}{\partial\lambda^2} = \frac{e^{-\lambda}\lambda^{s-1}}{(s-1)!} > 0 \quad (s \ge 1),$$

and second derivative $0$ for $s = 0$. 2. Strict convexity, p. 139: for $s \ge 1$, $\lambda \mapsto B(s \mid \lambda)$ is strictly convex on $(0, \infty)$. 3. The worked example, p. 138 (off the goal's path): $B(2 \mid 1) = 3e^{-1} - 1 \approx 0.1036$ and $0.5\,B(2 \mid 0.5) + 0.5\,B(2 \mid 1.5) \approx 0.1486$.

Significance

The result. Expected backorders are the objective METRIC minimizes, item by item, subject to a budget. If the objective is evaluated at a point estimate, every item with uncertain demand looks better stocked than it is, and since the size of the error varies by item, the marginal comparisons that drive the allocation are distorted. The inequality is the quantitative statement behind the paper's recommendation to compute backorders as a posterior mixture over possible mean demands. It also says that an underestimate of demand costs more than an overestimate of the same size when backorders are the objective. For $s = 0$ the bias vanishes because $B(0 \mid \lambda) = \lambda$ is linear.

Formalizing it. The paper proves the statement in one line ("it is easy to show") by differentiating twice. No machine-checked version exists. A formal proof needs termwise differentiation of the Poisson backorder series, a closed form for its second derivative, and the passage from a positive second derivative to strict convexity and then to a strict finite Jensen inequality under a nondegenerate prior. The resulting facts about $\lambda \mapsto B(s \mid \lambda)$ are reusable in any Poisson inventory model (base-stock, $(s-1, s)$ policies, METRIC and VARI-METRIC). Convexity of $B$ in the stock level $s$, the paper's eq. (3), is a different statement; it is already posed on the platform as ServiceParts.StockLevels.backorder_differences (compound Poisson demand) and is not repeated here. The definition of the Poisson probabilities is the published ServiceParts.StockLevels.Basic (Muckstadt 2005).

Difficulty

Each step is classical, but none is a one-liner in Lean. The series $B(s \mid \lambda)$ is an infinite sum whose terms depend on $\lambda$ both through $e^{-\lambda}$ and through $\lambda^x$, so differentiating it twice under the summation sign requires a uniform summability bound for the derivative series on a neighbourhood of $\lambda$. The tempting shortcut of reasoning with deriv alone fails: deriv returns $0$ at points of non-differentiability, so a formula for deriv (deriv B) says nothing about smoothness, and the milestone is stated with HasDerivAt for this reason. The strict inequality further needs strict convexity, not just convexity, and a hypothesis that the prior is not concentrated on one value: with a one-point prior both sides coincide.

Formalization scope

• $B(s \mid \lambda)$ is a real-valued tsum over $x \in \mathbb N$ of $(x - s)\,p(x \mid \lambda)$ for $x > s$ and $0$ otherwise. The family is summable for every real $\lambda$; no statement relies on the tsum junk value.
• Spare stock is a natural number; mean demand is real. Convexity and the second-derivative formula are stated for $\lambda > 0$, the paper's "for any positive $\lambda$".
• Explicit readings of the paper's phrases: "backorders computed from a point estimate" is $B(s \mid \bar\lambda)$ with $\bar\lambda$ the prior mean (the paper assumes "the initial estimate is the mean of the true mean demand distribution"); "the correct value" is the prior expectation $\sum_k w_k B(s \mid \lambda_k)$; "mean demand can assume more than one value" means two distinct values each of positive probability; "positive spare stock" means $s \ge 1$; "understate" is strict.
• The prior is a finite distribution with positive support points. This covers the paper's two-point example and its five-to-ten-point discretization of a gamma prior; a general prior on $(0, \infty)$ would need integrability hypotheses and is not part of the mission.
• The printed value $B^*(2) = 0.1485$ is a rounding slip; the exact value is $0.14864\ldots$, and the worked example states $0.1486$.
• A formalization that fixes $s$, uses $\le$ in place of $<$, drops the nondegeneracy hypothesis (making the strict statement false), or states the second derivative with deriv alone (vacuous at non-differentiable points) does not meet the target.
• Not formalized: the remark that the understatement "is also true for probability distributions like the negative binomial, though difficult to prove analytically" (unproved on the page), the gamma prior and Bayes updating (a procedure), and the comment that the resulting allocation "will produce inferior results" (not a mathematical statement).
• Contributions welcome: termwise differentiation lemmas for Poisson-weighted series, the closed form $B(s \mid \lambda) = \lambda - s + \sum_{x<s}(s - x)p(x \mid \lambda)$, and a strict finite Jensen inequality in the form used here.

Selected references

• C. C. Sherbrooke, METRIC: A Multi-Echelon Technique for Recoverable Item Control, Operations Research 16(1) (1968), 122–141. https://doi.org/10.1287/opre.16.1.122
• G. J. Feeney and C. C. Sherbrooke, The (s−1, s) Inventory Policy under Compound Poisson Demand, Management Science 12(5) (1966), 391–411. https://doi.org/10.1287/mnsc.12.5.391
• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005. https://doi.org/10.1007/0-387-27288-8

Motivation

The logarithm of a share price is commonly modelled as a Brownian motion with drift, $X_t=\sigma B_t+ct$. The Black–Scholes option pricing formula needs the volatility $\sigma$ but not the drift $c$, so a practitioner must estimate $\sigma^2$ from data. Observing the whole path would give $\sigma^2$ exactly through its quadratic variation, but a real observer sees far less. The most readily available daily information is the opening and closing prices together with the day's high and low.

Parkinson (1980) proposed an estimator from the high–low range, and Garman and Klass (1980) found the minimum-variance estimator among a class of quadratic functions of high, low and close. Both were derived assuming zero drift, $c=0$, and the Garman–Klass estimator is biased when $c\neq0$. Rogers and Satchell (Ann. Appl. Probab. 1 (1991) 504–512) proposed the estimator

$$\hat\sigma^2\equiv S_1(S_1-X_1)+I_1(I_1-X_1),$$

which is unbiased for every drift. Their estimator is now a standard tool in empirical finance for range-based volatility measurement.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ carrying a standard Brownian motion $B=(B_t)_{t\ge0}$: $B_0=0$, its increments over disjoint intervals are independent and Gaussian with variance equal to the length of the interval, and every sample path $t\mapsto B_t(\omega)$ is continuous. Fix a drift $c\in\mathbb R$ and a volatility $\sigma\ge0$. The log-price is

$$X_t=\sigma B_t+ct,\qquad t\ge0,$$

and, for a trading period $[0,t]$, the running maximum and running minimum are

$$S_t=\sup_{0\le u\le t}X_u,\qquad I_t=\inf_{0\le u\le t}X_u.$$

Thus $S_t$, $I_t$ and $X_t$ are the high, the low and the close of the log-price (with the open normalized to $X_0=0$). In Lean these are logPrice σ c B t ω, runMax σ c B t ω and runMin σ c B t ω in the namespace RogersSatchell.Unbiased.

The proof in the paper passes through an exponential time: a random variable $T$ with $P(T>x)=e^{-\lambda x}$ (rate $\lambda>0$, mean $\lambda^{-1}$), independent of the whole path $B$. For $\sigma>0$ the rates

$$\alpha=\frac{\sqrt{c^2+2\lambda\sigma^2}-c}{\sigma^2},\qquad \beta=\frac{\sqrt{c^2+2\lambda\sigma^2}+c}{\sigma^2}$$

appear, in Lean alpha σ c lam and beta σ c lam.

Formalization targets

Goal: display (3)

For every $c\in\mathbb R$, every $\sigma\ge0$ and every $t\ge0$, $S_t(S_t-X_t)+I_t(I_t-X_t)$ is integrable and

$$E\big[S_t(S_t-X_t)+I_t(I_t-X_t)\big]=\sigma^2t.$$

At $t=1$ this is the unbiasedness of $\hat\sigma^2$ of display (2). The statement quantifies over all drifts; the absence of $c$ on the right-hand side is the content.

Milestones (Section 2, pp. 505–506)

1. At an independent exponential time $T$ of rate $\lambda$: $S_T\sim\operatorname{Exp}(\alpha)$ and $-I_T\sim\operatorname{Exp}(\beta)$.
2. The Wiener–Hopf splitting: $S_T$ and $S_T-X_T$ are independent, and $S_T-X_T$ has the law of $-I_T$.
3. $E[S_T(S_T-X_T)]=1/(\alpha\beta)=\sigma^2/2\lambda$.
4. $E[S_T(S_T-X_T)]=\int_0^\infty\lambda e^{-\lambda t}\,E[S_t(S_t-X_t)]\,dt$.
5. $E[S_t(S_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
6. $E[I_t(I_t-X_t)]=\sigma^2t/2$ for every $t\ge0$.
7. (off the goal's path) With $Y_1=S_1(S_1-X_1)$, $Y_2=I_1(I_1-X_1)$: $E Y_1^2=EY_2^2=\sigma^4/2$, $E(Y_1+Y_2)^2\le2\sigma^4$ and $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, for every drift $c$.

Significance

The goal certifies a drift-free unbiased volatility estimator built from four numbers per trading day. Because only $\sigma^2$ enters the Black–Scholes formula, an estimator whose mean does not depend on the nuisance parameter $c$ is exactly what is needed. Milestone 7 complements this with a drift-uniform bound on its variance, $\operatorname{var}(\hat\sigma^2)\le\sigma^4$, while the exact value $0.331\sigma^4$ quoted in the paper is only available at $c=0$.

On the formalization side, the results are classical and proved; none is machine-checked as far as the platform's catalog shows. A complete development would give the first formal treatment of the joint law of the running maximum of drifted Brownian motion at an exponential time, of the Wiener–Hopf splitting at the maximum, and of a Laplace-inversion argument for a moment function of the time horizon. All three are reusable well beyond volatility estimation: in ruin theory, queueing (reflected Brownian motion), and the pricing of lookback and barrier options.

Difficulty

The obvious approach, computing $E[S_t(S_t-X_t)]$ directly from the joint density of $(S_t,X_t)$ for drifted Brownian motion, requires the reflection principle combined with a Girsanov change of measure, followed by a double integral involving Gaussian tails, done separately for each sign of $c$. The cancellation that makes the drift disappear is not visible in that computation, and a statement specialized to $c=0$ (where the reflection principle alone suffices) does not carry over. Every step of the milestone list rests on path properties of Brownian motion (the strong Markov property, the law of the running maximum, splitting at the maximum) that Mathlib does not yet provide for IsBrownianReal, and the passage from milestone 4 to milestone 5 needs uniqueness of the Laplace transform.

Formalization scope

• Brownian motion is Mathlib's ProbabilityTheory.IsBrownianReal B P with B : ℝ≥0 → Ω → ℝ, plus the hypothesis that every sample path is continuous (the standard choice of a continuous version). Time is ℝ≥0.
• $S_t$ and $I_t$ are the real sSup/sInf of the path over the interval $[0,t]$; with continuous paths they are attained. The supremum is never taken over all times or in extended reals.
• "$E$" is the Bochner integral, and every expectation identity also asserts integrability, so no identity can hold through Lean's convention that a non-integrable function integrates to $0$.
• "$T$ exponential with mean $\lambda^{-1}$" is HasLaw T (expMeasure λ) P; "parameter $\alpha$" is read as rate $\alpha$. "Independent of $B$" is independence from the path-valued random variable with the product σ-algebra. $S_T$ is evaluated at $T$ truncated to $[0,\infty)$.
• "Has the same law as" is equality of image measures, together with the almost-everywhere measurability of both maps.
• "Inversion of the Laplace transform gives" becomes the fixed-time identity for every $t\ge0$ (milestones 5 and 6), separate from the Laplace identity (milestone 4).
• Milestones 1 and 3 assume $\sigma>0$ because $\alpha,\beta$ divide by $\sigma^2$; the Wiener–Hopf splitting, the goal, and milestones 4–7 allow $\sigma\ge0$.

A formalization that specializes to $c=0$, takes the supremum over all of $[0,\infty)$, or omits the integrability conjuncts is not the statement of this mission.

Infrastructure that a complete development needs: the reflection principle or the strong Markov property for Brownian motion, the exponential-time law of the running maximum of a Lévy process, and uniqueness of Laplace transforms for continuous functions. All of these are reusable; contributions of any of them are welcome. Related platform items cover other objects and are credited here: running maxima and exit problems for spectrally negative Lévy processes (Avram2004.Exit.reflected), a drifted Brownian motion in characteristic-function form in a queueing-network setting (Reiman84.QueueLength.Paths), and a GI/G/1 Wiener–Hopf transform identity (QueueingFundamentals.GG1.wiener_hopf_transform).

Selected references

• L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4), 1991, 504–512. https://doi.org/10.1214/aoap/1177005835
• M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1), 1980, 67–78. https://doi.org/10.1086/296072
• M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1), 1980, 61–65. https://doi.org/10.1086/296071
• P. Greenwood and J. Pitman, Fluctuation identities for Lévy processes and splitting at the maximum, Advances in Applied Probability 12(4), 1980, 893–902. https://doi.org/10.2307/1426747

Motivation

Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility $\sigma$ than the close alone. Rogers and Satchell (1991) propose an estimator, $S_1(S_1-X_1)+I_1(I_1-X_1)$, that is unbiased for $\sigma^2$ whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.

Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at $N$ times. The sampled maximum $S$ falls short of the true maximum $S_1$ by an amount $\Delta = S_1 - S \ge 0$, and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model $\Delta$ by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,

$$a=\sqrt{2\pi}\Big[\tfrac14-\tfrac{\sqrt2-1}{6}\Big],\qquad b=\frac{1+3\pi/4}{12},$$

enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.

Setting

Fix a volatility $\sigma>0$ and a sampling mesh $h>0$ (in the paper $h=1/N$). For a level $\alpha\ge0$ define

$$G_{\sigma,h}(\alpha)=\int_0^h e^{-2\alpha^2/(u\sigma^2)}\,\frac{du}{(4uh)^{1/2}} .$$

The factor $e^{-2\alpha^2/(u\sigma^2)}$ is the probability that a Brownian bridge of duration $u$ and volatility $\sigma$ climbs above level $\alpha$. The factor $(4uh)^{-1/2}$ is a probability density on $(0,h]$. Since $G_{\sigma,h}(0)=1$ and $G_{\sigma,h}$ decreases continuously to $0$, it is the survival function of a law on $(0,\infty)$. This law is the paper's display (9).

A real random variable $Z$ has distribution (9) if it is measurable and $P(Z>\alpha)=G_{\sigma,h}(\alpha)$ for every $\alpha\ge0$. In the paper, $Z$ is the overshoot of the continuous maximum over the sampled maximum $x$ in the sampling interval to the left of the time $t$ at which $x$ is attained, and $Z'$ is the overshoot in the interval to the right. The paper then assumes (p. 508) that $Z$ and $Z'$ are independent, each with distribution (9), and approximates $\Delta$ by $Z\vee Z'=\max(Z,Z')$. Write $Z\wedge Z'=\min(Z,Z')$.

In Lean, overshootSurvival σ h α is $G_{\sigma,h}(\alpha)$, HasOvershootLaw P σ h Z is "$Z$ has distribution (9) under $P$", and constA, constB are $a$ and $b$.

Formalization targets

Goal: the two moments of $Z\vee Z'$ (Eq. (11), p. 508, and the display on p. 509)

For $\sigma,h>0$ and $Z,Z'$ independent with distribution (9), the variables $Z\vee Z'$ and $(Z\vee Z')^2$ are integrable, and

$$E(Z\vee Z')=a\,\sigma\sqrt h,\qquad E\big[(Z\vee Z')^2\big]=b\,\sigma^2h .$$

Milestones, in the order the paper uses them

1. (9), p. 507. The two integral forms of the survival function agree:

$$\int_0^h e^{-2\alpha^2/(u\sigma^2)}\frac{du}{(4uh)^{1/2}}=\int_{h^{-1}}^\infty e^{-2\alpha^2s/\sigma^2}\frac{ds}{(4hs^3)^{1/2}} .$$

2. (10), p. 508. $EZ=\sigma(2\pi h)^{1/2}/8$.
3. Display before (11), p. 508. $E(Z\wedge Z')=\sqrt{2\pi h}\,(\sqrt2-1)\,\sigma/6$.
4. (12), p. 508. $EZ^2=\sigma^2h/6$.
5. (13), p. 509. $E[(Z\wedge Z')^2]=\frac{\sigma^2h}{4}\big(1-\frac\pi4\big)$.

The goal combines milestones 2–5 through $Z\vee Z'=Z+Z'-Z\wedge Z'$, which the paper uses in (11).

Significance

The result. The two identities are the coefficients of the corrected estimator (5): replacing $\Delta$ and $\Delta^2$ by $a\sigma\sqrt h$ and $b\sigma^2h$ turns the high–low estimator into an equation whose positive root $\hat\sigma_h$ largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for $a$ and $b$ the correction has no concrete form.

Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes $\Delta$). To our knowledge none of these identities has been formalized before.

Difficulty

The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights $(4hs^3)^{-1/2}$ on an unbounded domain. The minimum of $Z$ and $Z'$ couples two such integrals, and the resulting kernels $(s+u)^{-1/2}$ and $\sqrt{st}/(s+t)$ have to be integrated in closed form over the unit square. Matching $\sqrt2-1$ and $1-\pi/4$ exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is $0$.

Formalization scope

• Model. Random variables live on an arbitrary probability space (Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels $\alpha\ge0$: the formula is even in $\alpha$, and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. $Z\vee Z'$ and $Z\wedge Z'$ are max and min.
• Parameters. $\sigma>0$ and $h>0$ only. The paper's $h=1/N\le1$ is not needed and not imposed.
• Explicit readings. "E" is the Bochner integral, and every expectation identity carries its integrability (Integrable, or MemLp … 2 for second moments). The conditioning "$\mid t-h<H_x<t,\ X_t=x$" in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's "$E(Z\wedge Z')^2$" in (13) is read as $E[(Z\wedge Z')^2]$, as its first line shows. The integrals in (9) run over $(0,h]$ and $[h^{-1},\infty)$.
• Not formalized. The approximate statements $E\Delta\doteq a\sigma\sqrt h$ and $E\Delta^2\doteq b\sigma^2h$, the densities (6) and (7), and the independence remark of p. 508 are modelling approximations about the random walk, not theorems. The estimators (5) and $\hat\sigma^2_{GK,h}$ are definitions with no claim attached. The Brownian-bridge maximum (8) is not stated (its print also has a slip: $1-2/u$ for $1-s/u$). Section 4 (simulations) is out of scope.
• Non-triviality. The hypotheses are satisfiable for every $\sigma,h>0$: a probability measure on $\mathbb R$ with survival function $G_{\sigma,h}$ exists, and the two coordinates under its product measure are independent copies. A formalization that stated the survival condition for all $\alpha\in\mathbb R$ would be vacuous and is ruled out. So is one without the integrability conjuncts, which could hold with both sides $0$.
• Related items. The platform's generic identity survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.
• Welcome contributions. Closed forms for $\int_0^1\!\int_0^1(s+t)^{-1/2}\,ds\,dt$ and $\int_0^1\!\int_0^1\sqrt{st}/(s+t)\,ds\,dt$, which are reusable lemmas, and a general "moments of $\max$ and $\min$ of independent variables from their survival functions" lemma.

Selected references

• L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4) (1991), 504–512. https://doi.org/10.1214/aoap/1177005835
• M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1) (1980), 67–78. https://doi.org/10.1086/296072
• M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1) (1980), 61–65. https://doi.org/10.1086/296071
• S. Beckers, Variances of security price returns based on high, low and closing prices, Journal of Business 56(1) (1983), 97–112.

Motivation

Demand for many products does not arrive at a constant rate. It moves with an underlying environment: the economy, the season, a product's life-cycle stage, the state of a customer's own operations. Song and Zipkin (Oper. Res. 41(2):351–370, 1993) modelled this environment as a continuous-time Markov chain, the world, whose current state sets the Poisson demand rate, and showed that a basestock policy whose level depends on the current world state is optimal under linear order costs. Missions I and II of this series formalize those optimality results.

A practitioner who uses such a policy wants to know how the levels depend on the world. If a higher world state means more demand now and more demand later, a higher level should be kept. That is what intuition says, but the optimal level depends on the whole future of the world chain, not only on the current demand rate. §4 of the paper answers it for a world with an arbitrary partial order, which covers several independent demand drivers at once.

Setting

The world $A$ is a continuous-time Markov chain on a countable set $\mathbf I$ with generator $Q = (q_{ij})$, $q_i = -q_{ii}$, and bounded rates $q^* = \sup_i q_i$, $\lambda^* = \sup_i \lambda_i$. While $A = i$, unit demands arrive at rate $\lambda_i$, all demand is backlogged, and orders arrive after a random lead time $L$ that is independent of the world and the demand. Costs are discounted at rate $\alpha > 0$. With the unit order cost $\bar c$, holding rate $h$ and penalty rate $p$, set $c = \bar c\,E[e^{-\alpha L}]$ and

$$\hat C(x) = \max\{-px,\ hx\}, \qquad C(i,y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big],$$

where $D^i_L$ is the demand during a lead time when the world starts in $i$. Uniformizing at a rate $\mu \ge q^* + \lambda^*$ with $\beta = 1/(\mu+\alpha)$ and $\gamma = \beta\mu$, the myopic cost is $G^+(i,y) = (1-\gamma)cy + \beta C(i,y)$. The linear-cost model ($K = 0$) is solved by value iteration from $W_0 \equiv 0$:

$$G_n(i,y) = G^+(i,y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i,y-1) + \sum_{j\ne i} q_{ij}W_{n-1}(j,y) + (\mu-\lambda_i-q_i)W_{n-1}(i,y)\Big\},$$

$W_n(i,x) = \min_{y\ge x} G_n(i,y)$, with limits $G_\infty$ and $W_\infty$. The myopic level $y^+(i)$, the finite-horizon levels $y^*_n(i)$ and the optimal level $y^*(i)$ are the smallest minimizers of $G^+(i,\cdot)$, $G_n(i,\cdot)$ and $G_\infty(i,\cdot)$, and $y^*_\infty(i) = \lim_n y^*_n(i)$. Throughout, $\alpha\bar c < p$ (Assumption 1).

The world states carry a partial order $\preceq$. The chain is stochastically partial-monotone (display (14)) if for every $i \preceq j$ there is a probability space carrying copies of $A$ started at $i$ and at $j$ whose paths satisfy $A(t) \preceq A'(t)$ for all $t \ge 0$ almost surely. Condition 1 requires this together with $\lambda_i$ nondecreasing in $i$.

Formalization targets

Goal: Theorem 8

Under Condition 1, the three families of levels exist and are nondecreasing along $\preceq$:

$$i \preceq j \ \Longrightarrow\ y^+(i) \le y^+(j),\qquad y^*(i) \le y^*(j),\qquad y^*_\infty(i) \le y^*_\infty(j).$$

Milestones

• Lemma 8, with its fixed-lead-time form from the proof: $D(l)$ given $A(0)=i$ is stochastically smaller than given $A(0)=j$ for each $l \ge 0$, and $D^i_L \le_{st} D^j_L$.
• Lemma 9: $\Delta C(i,y) \ge \Delta C(j,y)$ for $i \preceq j$.
• Theorem 7: for all $n \ge 1$ and fixed $x$, $\Delta W_{n-1}(i,x)$ and $\Delta G_n(i,x)$ are nonincreasing in $i$, and $y^*_n(i)$ is nondecreasing in $i$.
• Theorem 9 (companion): if $q_{ij} \ne 0$ only for $j \succeq i$, then $y^*(i) = y^+(i)$, so the myopic policy is optimal.
• Theorem 10 (companion): with a fixed order cost $K > 0$, the bounds $S^+(i)$, $r^+(i)$, $r^-(i)$, $r^{--}(i)$ on the optimal $(r,S)$ parameters are nondecreasing in $i$.

Significance

Theorem 8 turns an optimal policy into a structured one. A world-dependent basestock policy has one level per world state; monotonicity says the levels follow the order of the states, which reduces search, makes the levels interpretable, and gives sanity checks for computed solutions. Theorem 9 identifies when nothing beyond the one-step cost needs to be computed at all. Theorem 10 is the paper's substitute for an open question: the authors could not show that the optimal $(r,S)$ parameters are monotone, and instead bound them between monotone functions.

All of these results are proved in the paper. None of them has been machine-checked. The formalization requires a value-iteration argument for a model with unbounded one-period costs, a coupling argument for Markov-modulated Poisson demand, and the passage to the limit in the levels. These are the ingredients of most monotone-policy results in inventory theory with Markov-modulated demand.

Difficulty

The obvious argument fails at the generator. For a single scalar world, stochastic monotonicity is equivalent to the expectation inequality (15) for nondecreasing functions, and the inductive step of Theorem 7 only needs that. For a partial order, the expectation inequality is strictly weaker than the coupling (14) (Massey 1987). The induction must also handle the cross term $\sum_j q_{ij}\Delta W_{n-1}(j,x)$, which requires an embedded discrete-time chain whose one-step kernel preserves the order. The paper's Lemma 7 asserts that the embedded chain $P = I + Q/\nu$ is monotone for every $\nu \ge q^*$. As printed, this is false at $\nu = q^*$: for two states with $q_{01} = q_{10} = 1$, $P$ swaps the states. A complete proof cannot rely on that lemma as printed.

A second difficulty is that the one-period cost is unbounded. The classical theorems that ordered differences survive value iteration (Denardo, Lovejoy) assume bounded costs, so the induction has to be carried out by hand, and the limits $G_\infty$, $y^*_\infty$ must be justified by Lemma 4's uniform bounds.

Formalization scope

The Lean development lives in the namespace SongZipkinFluct.Monotone. World states form a countable nonempty type with a PartialOrder instance; no linear order is assumed. Inventory positions are integers. The demand-count law $f_i(d\mid l)$ and the world transition function $P(t)$ are defined by uniformization at the model's rate $\mu$, the paper's own device. The lead-time law is a probability measure on $[0,\infty)$, and $C(i,y)$ is the series $\sum_d g_i(d\mid\alpha)\hat C(y-d)$ of display (16). $W_n$ uses an infimum over integers $y \ge x$, and $W_\infty$, $G_\infty$ are suprema over $n$, which equal the limits because the sequences are nondecreasing and bounded. Monotonicity in $i$ is Monotone/Antitone with respect to $\preceq$. Smallest minimizers, maxima and minima are IsLeast/IsGreatest characterizations, never sInf on $\mathbb Z$.

Condition 1(a) is encoded as the coupling (14) itself, with one probability space per pair $i \preceq j$ and copies identified by their finite-dimensional distributions. Replacing it by the expectation inequality (15), or the partial order by a total order, would change the theorem and is ruled out. Every goal statement asserts the existence of the levels it constrains before constraining them, so no conclusion holds vacuously. The standing hypotheses together with Condition 1 are satisfiable: a one-state instance is checked in Lean.

Lemma 7 is not included because it is false as printed. A guarded version (for instance with $\nu \ge 2q^*$) would be a welcome contribution. Reusable parts include the uniformized Markov-modulated Poisson process, the coupling definition of stochastic monotonicity for a countable partially ordered state space, and the usual stochastic order on $\mathbb N$. Proofs of Lemma 9 and Theorem 7 that avoid Lemma 7 are particularly welcome.

Selected references

• J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• W. A. Massey, Stochastic orderings for Markov processes on partially ordered spaces, Mathematics of Operations Research 12(2):350–367, 1987. https://doi.org/10.1287/moor.12.2.350
• J. Keilson and A. Kester, Monotone matrices and monotone Markov processes, Stochastic Processes and their Applications 5(3):231–241, 1977. https://doi.org/10.1016/0304-4149(77)90033-3
• A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• W. S. Lovejoy, Ordered solutions for dynamic programs, Mathematics of Operations Research 12(2):269–276, 1987. https://doi.org/10.1287/moor.12.2.269