Stochastic Systems

Motivation

The (s, S) policy is the standard control rule for a single item reviewed periodically: when the inventory position reaches or drops below a reorder level $s$, order enough to bring it up to the order-up-to level $S$. Under a fixed ordering cost and fairly general holding and shortage costs, some (s, S) policy minimizes the long-run average cost among all policies (Veinott 1966). That makes computing the best (s, S) pair a routine subproblem in inventory software, in multi-echelon heuristics, and in textbooks.

Before 1991 the available methods searched a box of candidate pairs. Veinott and Wagner (1965) bounded the optimal $s$ and $S$ and compared policies within the bounds. Later methods (Johnson, Management Science 15, 1968; Bell, SIAM J. Applied Mathematics 18, 1970; Federgruen and Zipkin 1984) used policy iteration or partial enumeration. Zheng and Federgruen (1991) gave an exact search that walks a monotone staircase path through the $(s,S)$ grid, and showed it costs about as much as evaluating a single policy. The procedure is the one presented in standard inventory texts such as Zipkin's Foundations of Inventory Management (2000).

Setting

One-period demands $D$ are i.i.d. and integer valued, with $p_j=\Pr\{D=j\}$, $j\ge0$, and $p_0<1$. An order costs $K>0$. $G(y)$ is the one-period expected cost when a period starts at inventory position $y\in\mathbb Z$. The paper assumes only:

• $-G$ is unimodal: for some integer $m$, $G$ is nonincreasing on $y\le m$ and nondecreasing on $y\ge m$;
• $\lim_{|y|\to\infty}G(y)>\min_yG(y)+K$.

Write $y_1^*$ and $y_2^*$ for the smallest and largest minimizers of $G$. The renewal density $m$ and renewal function $M$ are

$$m(0)=(1-p_0)^{-1},\quad m(j)=\sum_{l=0}^{j}p_l\,m(j-l)\ (j\ge1),\qquad M(0)=0,\quad M(j)=M(j-1)+m(j-1).$$

For integers $s<S$, the long-run average cost of the (s, S) policy is

$$c(s,S)=\frac{K+\sum_{j=0}^{S-s-1}m(j)\,G(S-j)}{M(S-s)}.$$

A pair $(s,S)$ is an optimal policy if $c(s,S)\le c(s',S')$ for all integers $s'<S'$. The optimal cost $c^*$ is the value of any optimal policy. For fixed $S$, $s$ is an optimal reorder level if $c(s,S)\le c(s',S)$ for all $s'<S$.

The algorithm (§3, p. 659) starts at any minimizer $y^*$ of $G$.

• Step 0. Decrease $s$ from $y^*$ until $c(s,y^*)\le G(s)$. Set $S^0:=y^*$, $c^0:=c(s,S^0)$ and $S:=y^*+1$.
• Step 1. While $G(S)\le c^0$: if $c(s,S)<c^0$, set $S^0:=S$, increase $s$ while $c(s,S^0)\le G(s+1)$, and set $c^0:=c(s,S^0)$. In either case, $S:=S+1$.

Formalization targets

Goal: Theorem 1(a)

For every demand law with $p_0<1$, every $K>0$, every $G$ satisfying the two assumptions, and every minimizer $y^*$ of $G$, the algorithm terminates. On termination, with final values $s,S^0,c^0$,

$$c(s,S^0)\le c(s',S')\ \text{ for all integers } s'<S',\qquad c^0=c(s,S^0)=c^*.$$

Milestones

The milestones are the results the paper's justification of the algorithm (p. 659) rests on, in the order it uses them:

1. the weighted-average identity (6), $c(s-1,S)=\alpha_nc(s,S)+(1-\alpha_n)G(s)$ with $\alpha_n=M(n)/M(n+1)$ and $n=S-s$, and Lemma 0 on the comparisons it implies;
2. Lemma 1(a): a reorder level $s^0<y_1^*$ with $G(s^0)\ge c(s^0,S)\ge G(s^0+1)$ (condition (7)) is optimal for $S$;
3. Corollary 1, the stopping rule of Step 0;
4. Lemma 2(a)–(c), the bounds $y_2^*\le S^*$ and $S^*\le\bar S^*=\max\{y\ge y_2^*:G(y)\le c^*\}$, which give the stopping rule of Step 1;
5. Lemma 3(a), the single-comparison test for improvement, and Corollary 2(b) with Lemma 3(b), which justify the inner loop.

Significance

The result. Theorem 1(a) makes the exact optimum of the (s, S) problem as cheap to compute as the cost of one policy, for any $G$ with $-G$ unimodal. No convexity is needed, and lead times, random lead times of the Zipkin type, and linear purchase costs are allowed. Its bounds (Lemma 2) and the monotone staircase structure of the search also underlie later work on continuous review, discounting and approximation.

Formalizing it. The theorem is proved on paper. As far as we know, none of the results in this mission has a machine-checked proof: the platform's Veinott–Wagner items concern a different (discounted, convex) model. Formalizing it produces a verified correctness proof of a widely implemented algorithm, and checks the paper's lemmas at their edge cases. Two of the printed statements need repair: Lemma 1(b) and Lemma 3(a) (see the scope section).

Difficulty

Optimality is claimed over all pairs $s'<S'$, an infinite set, but the algorithm visits only a monotone path. The proof therefore has to show that every pair it skips is no better. For a fixed $S$, the skipped reorder levels are handled by the unimodality of $c(\cdot,S)$ (Lemma 1). The skipped order-up-to levels are handled by the one-comparison test of Lemma 3(a), and those above the stopping point by the bound of Lemma 2(b). An argument from joint convexity or joint unimodality of $c$ in $(s,S)$ is not available. The paper uses no structure of $c$ beyond what Lemmas 0–3 state, and these hold only under the side conditions written in them.

Lemma 2(b)'s printed proof leaves the class of (s, S) policies (it uses a randomized order-up-to level). The limit at $-\infty$ may be finite, so $\min_{s<S}c(s,S)$ need not be attained for every $S$. Lattice demands, for which $m$ vanishes somewhere, create ties between adjacent reorder levels. Each of these breaks a naive transcription of the paper's argument.

Formalization scope

• Levels $s,S,y$ are integers. Demand values are natural numbers, and the demand law is the published VeinottWagnerSS.RenewalCost.DemandDist with the extra hypothesis $p_0<1$. All costs are real.
• The cost is the ratio above. Equation (1) on p. 655 is misprinted as $M(S-s)K+\sum\cdots$, and the ratio is the form fixed by (3) and (5). The Lean value $c(s,S)$ for $s\ge S$ is a junk $0$, so every quantifier over reorder levels carries $s<S$.
• $m$ is defined by the solved recursion $m(j)=(1-p_0)^{-1}\sum_{l=1}^{j}p_l\,m(j-l)$ (p. 660), and $M(j)=\sum_{i<j}m(i)$.
• The growth assumption is encoded as: $G$ has a minimizer $y_0$ and $G(y)>G(y_0)+K$ for all but finitely many $y$. Under unimodality this is equivalent to the page's limit condition. It is not strengthened to $G\to+\infty$.
• Optimality is among (s, S) policies. That an (s, S) policy is optimal among all policies is Veinott (1966) and is neither stated nor used. $c^*$, $c^*(S)$, $y_i^*$, $\bar S^*$, $\bar S_c$ and $s'$ are never real infima: they are the cost of a given optimal pair, $\exists$-statements, or binders characterised as least or greatest elements.
• The algorithm is a step function on the state $(s,S,S^0,c^0,\text{phase})$ that keeps the paper's order of tests and its weak and strict inequalities. The run with $n$ steps returns an output only if the algorithm has terminated.
• Ruled out as trivializing: comparing only with the pairs the algorithm visits or with a bounded box; assuming termination, or a budget that returns the current state; assuming $G\to+\infty$; leaving $c(s,S)$ unguarded for $s\ge S$.
• Repaired statements. Lemma 3(a) is stated with condition (7) at $S^0$ as an extra hypothesis. With $s^0$ merely optimal it fails when $m$ has a zero: for $p=(1/5,0,1/5,3/5)$, $m(1)=0$ and adjacent reorder levels tie. The algorithm always has (7). Lemma 1(b), "an optimal reorder level satisfying (7) exists for every $S$", is false when $\lim_{y\to-\infty}G(y)$ is finite. An example is $D\equiv2$, $K=1$, $G(0)=5$, $G(y)=10-0.1\cdot2^{-|y|}$ ($y\neq0$), $S=1$, where no optimal reorder level exists. It is not posed here, and the goal does not depend on it.
• Not formalized: Theorem 1(b)–(c), the operation counts, which depend on a bookkeeping model described in words; Corollary 3, which the paper notes is not needed for the algorithm; and the variant for a general starting level $S_0$.
• Welcome contributions: general facts about the discrete renewal density ($m\ge0$, $M>0$), the identity (6), and lemmas on $c(\cdot,S)$ that are reusable for related (s, S) and (r, Q) work.

Selected references

• Y.-S. Zheng and A. Federgruen, Finding Optimal (s, S) Policies Is About As Simple As Evaluating a Single Policy, Operations Research 39(4):654–665, 1991. https://doi.org/10.1287/opre.39.4.654
• 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
• A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM J. Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• A. Federgruen and P. Zipkin, An Efficient Algorithm for Computing Optimal (s, S) Policies, Operations Research 32(6):1268–1285, 1984. https://doi.org/10.1287/opre.32.6.1268
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Why arrival averages and time averages agree

Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.

Before 1982 the property had been proved under strong extra structure:

• Strauch (1970) proved an instantaneous version, at a fixed time point, which does not by itself give limit theorems.
• Wolff (1970) proved a limit theorem for a stationary observed process, using particular properties of its interaction with the Poisson stream.
• Stidham (1972) proved a limit theorem for regenerative processes, under restrictions on how regeneration points relate to the arrivals.
• Wolff (1982), the source of this mission, proved the limit theorem with no stationarity, regeneration or ergodicity at all. The only link assumed between system and arrivals is that the system does not anticipate future arrivals. The proof uses Watanabe's (1964) martingale characterization of the Poisson process.
• Melamed and Whitt (1990) recast the result as one instance of a general "arrivals see time averages" (ASTA) principle for arbitrary point processes.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. On it live a process $N=\{N(t),t\ge0\}$, the state of a system, with values in an arbitrary measurable space, and a Poisson process $A=\{A(t),t\ge0\}$ at rate $\lambda>0$, counting customer arrivals in $(0,t]$. The interaction between $A$ and $N$ is unspecified: arrivals may change the state.

Fix a set $B$ of states with $\{N(t)\in B\}\in\mathcal F$ for every $t\ge0$, and define

$$U(t)=\mathbf 1\{N(t)\in B\},\qquad V(t)=t^{-1}\int_0^tU(s)\,ds,\qquad Y(t)=\int_0^tU(s)\,dA(s),\qquad Z(t)=\frac{Y(t)}{A(t)}.$$

$V(t)$ is the fraction of time in $[0,t]$ that $N$ is in $B$. $Y(t)$ is the number of arrivals up to $t$ who find $N$ in $B$, and $Z(t)$ is the fraction of arrivals who do.

The paths of $U$ are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. $U$ is assumed jointly measurable in $(\omega,t)\in\Omega\times[0,\infty)$. The single structural assumption is the Lack of Anticipation Assumption (LAA):

for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ and $\{U(s),0\le s\le t\}$ are independent.

The paper's proof of (6) uses this independence for every event of $\mathcal F_t$, the σ-field generated by $\{A(s),U(s);0\le s\le t\}$. The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to $\mathcal F_t$: for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ is independent of $\mathcal F_t$. This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of $A$ and from the past of $U$ is not independence from their joint past.

Formalization targets

Goal: Theorem 1 (p. 225)

Under lack of anticipation (with respect to $\mathcal F_t$, see above), for every random variable $V(\infty)$,

$$V(t)\to V(\infty)\ \text{w.p. 1}\quad\Longleftrightarrow\quad Z(t)\to V(\infty)\ \text{w.p. 1},\qquad t\to\infty.$$

The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.

Milestones

The proof in §2 passes through the following statements, which form the milestone list:

1. (2), (3): $E\{Y(t)\}=\lambda tE\{V(t)\}=\lambda E\{\int_0^tU(s)\,ds\}$.
2. (6): $E\{Y(t+h)-Y(t)\mid\mathcal F_t\}=\lambda E\{\int_t^{t+h}U(s)\,ds\mid\mathcal F_t\}$.
3. Lemma 1: $R(t)=Y(t)-\lambda tV(t)$ is a martingale.
4. (7): the second-moment bound $E\{R^2(t)\}\le\lambda t+2\lambda^2t^2$.
5. (10): the grid strong law $R(nh)/n\to0$ w.p. 1.
6. (11): the pathwise interpolation bound between grid points.
7. Lemma 2: $R(t)/t\to0$ w.p. 1.
8. The strong law $A(t)/t\to\lambda$ for the Poisson process.

Companion: Theorem 2 (p. 228)

For a Poisson process with bounded, integrable rate $\lambda(t)$ and $\Lambda(t)/t\to\bar\lambda\in(0,\infty)$, where $\Lambda(t)=\int_0^t\lambda(s)\,ds$, the same equivalence holds with $V(t)$ replaced by the rate-weighted average $\bar V(t)=\Lambda(t)^{-1}\int_0^tU(s)\lambda(s)\,ds$. Display (12), $E\{Y(t)\}=\int_0^tE\{U(s)\}\lambda(s)\,ds$, is its analogue of (3).

Significance

Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).

The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:

• the strong law for the Poisson process;
• a strong law for square-integrable martingale differences;
• Stieltjes integration against a counting path.

Difficulty

The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of $A$ are independent of the past of $U$. The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.

On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, $U(t)=\mathbf 1\{A \text{ jumps at } t\}$ satisfies LAA with $V\equiv0$ but $Z\equiv1$. The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.

Formalization scope

• Time and paths. Time is $\mathbb R$, and every hypothesis concerns $t\ge0$ only. Processes are maps $\mathbb R\to\Omega\to(\cdot)$. A Poisson process with intensity function $\lambda(\cdot)$ is a counting process $A:\mathbb R\to\Omega\to\mathbb N$ with $A(0)=0$, every path non-decreasing and right-continuous, Poisson-distributed increments with mean $\int_s^t\lambda$, and independent increments over any finite increasing sequence of times. The constant-rate case is Theorem 1's setting.
• The averages. $Y(t)$ is encoded as $\sum_{k=1}^{A(t)}U(T_k)$ over the arrival epochs $T_k=\inf\{s\ge0:A(s)\ge k\}$, which is the Lebesgue–Stieltjes integral $\int_{(0,t]}U\,dA$ with multiplicities. $Z(t)=0$ when $A(t)=0$, and $V(0)=0$; limits do not see these values.
• The standing hypotheses. These are carried as binders of the goal: measurability of $\{N(t)\in B\}$ for $t\ge0$, path regularity w.p. 1 (left continuity at $t>0$, right limits at $t\ge0$), joint measurability on $\Omega\times[0,\infty)$, and lack of anticipation as independence of the σ-field of future increments of $A$ from $\mathcal F_t$. The milestones (2), (3), (7) and (11) need less: (2) and (3) are stated under the printed LAA, and (7) and (11) under no independence assumption at all.
• The limit and the expectations. $V(\infty)$ is an arbitrary function $\Omega\to\mathbb R$, shared by both sides of the equivalence. Expectations in the milestones come with integrability conclusions, or are lower integrals in $[0,\infty]$, so that no identity holds through Lean's junk value $0$ for non-integrable functions.
• Ruled out. A formalization in which $V(\infty)$ is quantified separately on each side, which loses "to the same limit". A goal that assumes Lemma 2, (3) or the strong law $A(t)/t\to\lambda$ as a hypothesis. A definition of $Y$ that counts distinct jump times and not arrivals.

Welcome contributions:

• a reusable Poisson-process library: the strong law, square moments, independence of increments from a past σ-field;
• a martingale strong law of Feller's type;
• Stieltjes sums against counting paths.

All of these are useful well beyond this mission.

Selected references

• R. W. Wolff, Poisson Arrivals See Time Averages, Operations Research 30(2):223–231, 1982. https://doi.org/10.1287/opre.30.2.223
• S. Watanabe, On discontinuous additive functionals and Lévy measures of a Markov process, Japanese Journal of Mathematics 34:53–70, 1964. https://doi.org/10.4099/jjm1924.34.0_53
• B. Melamed and W. Whitt, On arrivals that see time averages, Operations Research 38(1):156–172, 1990. https://doi.org/10.1287/opre.38.1.156
• P. Brémaud and J. Jacod, Processus ponctuels et martingales: résultats récents sur la modélisation et le filtrage, Advances in Applied Probability 9(2):362–416, 1977. https://doi.org/10.2307/1426091
• S. Stidham, Regenerative processes in the theory of queues, with applications to the alternating-priority queue, Advances in Applied Probability 4(3):542–577, 1972.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

Many iterative algorithms update only part of a vector at a time. In a parallel implementation, one processor may read a value written several rounds earlier by another processor. Random observations also perturb each update. John N. Tsitsiklis's 1994 paper gives conditions under which such an asynchronous stochastic iteration still converges. The paper develops the result to analyze Q-learning, where state-action values are revised from sampled costs and successor states. Its general theorem also applies to iterative fixed-point calculations beyond that application.

The central issue is that a processor can choose which component to update after seeing the past, and its input can be stale. A convergence theorem that presumes a fixed update schedule or current data would miss both features. The paper's Assumptions 1–3 describe when delays, sampling noise, and random step sizes remain compatible with almost-sure convergence. Assumption 5 gives a weighted maximum norm contraction for the iteration map. Theorem 3 combines these conditions into the target of this mission.

Setting

Fix a positive integer $n$ and write $x(t)\in\mathbb R^n$ for the vector after round $t\ge0$. Let $F:\mathbb R^n\to\mathbb R^n$ be the map whose fixed point the iteration seeks. For component $i$, the step size $\alpha_i(t)$ lies in $[0,1]$, the noise is $w_i(t)$, and $\tau^i_j(t)\le t$ is the time from which component $j$ was read. Thus $x^i(t)$ has coordinates $x_j(\tau^i_j(t))$. With $\alpha_i(t)=0$ when component $i$ is idle, all rounds obey the single update equation

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr).$$

All quantities live on a probability space with law $\mathsf P$. The increasing filtration $\mathcal F(t)$ represents information available when the step sizes and delays are selected, before the round's noise is observed. Assumption 1 says every timestamp $\tau^i_j(t)$ tends to infinity almost surely: no fixed old value remains in use forever. Assumption 2 makes the initial state, chosen step sizes, delays, and noise measurable at the specified times; the noise has conditional mean zero, and its conditional second moment is bounded by a deterministic affine function of the largest squared iterate seen so far. Assumption 3 requires, for each component, divergent total step size and a square-summable step-size sequence, with a deterministic bound on all squared partial sums.

For a vector $v$ with strictly positive coordinates, the weighted maximum norm is $\|z\|_v=\max_i |z_i|/v_i$. Assumption 5 provides $x^*\in\mathbb R^n$ and $\beta\in[0,1)$ such that $\|F(x)-x^*\|_v\le\beta\|x-x^*\|_v$ for every $x$. Assumption 6, used in the boundedness milestone, requires the related growth bound $\|F(x)\|_v\le\beta\|x\|_v+D$ for some real $D$. The weighted norm permits different component scales.

Formalization targets

Boundedness under a weighted growth bound

Theorem 1 is the main intermediate target. Under Assumptions 1, 2, 3, and 6, it asserts

$$\mathsf P\!\left(\exists M\in\mathbb R\;\forall t,i,\ |x_i(t)|\le M\right)=1.$$

The bound $M$ may depend on the sample path. Lemmas 1–3 of the paper are milestones in its analysis: a scalar noisy recursion converges, its tails become uniformly small, and the pathwise bounds in the contradiction step hold.

Almost-sure convergence under a weighted contraction

The goal is Theorem 3, under Assumptions 1, 2, 3, and 5:

$$\mathsf P\!\left(\lim_{t\to\infty}x(t)=x^*\right)=1.$$

This theorem does not assume bounded iterates or Assumption 6 separately. Its proof uses Theorem 1 after deriving the needed growth bound from the contraction condition. Lemma 8 is the remaining milestone, comparing the coordinate iterates to an auxiliary deterministic recursion and a noise tail.

Significance

The result gives a fixed-point convergence guarantee when coordinates update at different times, delays can vary, and update choices can depend on past observations. In the paper's Q-learning application, these features describe exploratory sampling and possible parallel computation with old state-action values. For discounted problems, the associated Q-learning map contracts in the maximum norm, so Theorem 3 supplies the convergence step once the stochastic assumptions are checked (Tsitsiklis 1994, §7).

The mathematical results were proved in 1994; this mission asks for machine-checked proofs of their formal statements. Its reusable output would include a model of asynchronous noisy iteration, a scalar martingale-noise convergence lemma with random conditional variance bounds, and a precise interface between weighted contractions and pathwise convergence. The goal and milestone theorem files are currently statements with proof holes, while the definition file compiles without one.

Difficulty

A coordinate's next value depends on a vector assembled from observations at several earlier times. A direct estimate against the current error therefore does not close: the stale coordinates can reflect larger past errors. The noise condition is also tied to the largest iterate seen so far, so a deterministic global variance bound is unavailable before boundedness has been established. These two dependencies make the ordinary synchronous contraction argument insufficient. The scalar noise result and the pathwise comparison lemmas isolate the conditions needed for the boundedness and convergence statements.

Formalization scope

Vectors are functions Fin n → ℝ, with $n>0$; the source labels coordinates $1,\ldots,n$, while Fin n starts at zero. Function order is componentwise. The model sets $\alpha_i(t)=0$ on idle rounds and uses the paper's unified update equation. It does not store the sets of update times separately. The delay values on idle rounds are left arbitrary because they do not affect the update; the source chooses the current time there. All step sizes lie in $[0,1]$, and all delays are at most the current time, on every sample path.

The probability law is a probability measure. The filtration consists of increasing sub-σ-algebras. The iterate sequence is explicitly assumed adapted in the main theorems, matching the paper's use of $x(t)$ and its running maximum as $\mathcal F(t)$-measurable random variables. Conditional moment assumptions use integral inequalities over measurable sets, allowing generalized conditional expectations when the noise need not have a finite unconditional second moment. The conditional upper bound is required nonnegative almost surely, as the original inequality entails. Divergence and square summability use partial sums, so a non-summable series cannot receive a default value.

The maximum norm is the finite supremum of coordinate absolute values, and the weighted norm divides by the strictly positive coordinates of $v$. Almost-sure boundedness means a path-dependent finite bound on every coordinate and time. Pathwise Lemmas 3 and 8 are stated on a retained sample path, with the auxiliary quantities and hypotheses established at their locations in the paper; Lemma 8 uses the proof's translated and rescaled coordinates. These conventions rule out an empty coordinate type, junk integrals, and a vacuous boundedness claim. Contributions to the stated lemmas, their probabilistic infrastructure, and the final convergence proof are within scope.

Selected references

• John N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. DOI: 10.1023/A:1022689125041.

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

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

Many approximation results in probability and operations research take the form of a sequence of discrete or jump-driven systems converging to a diffusion or another limit process. When the approximating systems are written as stochastic integral equations, $X_n(t) = X_n(0) + \int_0^t \sigma(X_n(s-))\,dY_n(s)$, the key step is to show that the stochastic integrals converge whenever the integrands and the integrators converge. That this is not automatic was known from the work of Wong and Zakai (1965): smooth approximations of Brownian motion produce a Stratonovich, not an Itô, limit. Kurtz and Protter (1991) give a condition on the integrators under which convergence in distribution of the pair (integrand, integrator) in the Skorohod topology implies convergence in distribution of the triple (integrand, integrator, integral). The result is essentially the theorem of Jakubowski, Mémin and Pagès (1989), with a formulation and proof that avoid the general theory of semimartingale characteristics. It underlies diffusion approximations for queueing and storage networks, approximation schemes for stochastic differential equations, and limit theorems for statistics and filters that are written as stochastic integrals.

Setting

Time is $[0,\infty)$. A path $x:[0,\infty)\to E$ in a metric space $E$ is cadlag if it is right-continuous and has a left limit $x(t-)$ at every $t>0$; $D_E[0,\infty)$ is the set of cadlag paths, and $x(0-)=x(0)$. Let $\Lambda$ be the set of continuous, strictly increasing maps of $[0,\infty)$ onto itself. Cadlag paths $x_n$ converge to $x$ in the Skorohod (J1) topology if there are $\lambda_n\in\Lambda$ with $x_n\circ\lambda_n(t)\to x(t)$ and $\lambda_n(t)\to t$ uniformly on bounded intervals. For a product space $E_1\times E_2$ the pair $(x_n,y_n)$ converges if one sequence $\lambda_n$ serves both components; this is strictly stronger than convergence of each component.

Let $\mathbb M^{km}$ be the real $k\times m$ matrices. For a $\mathbb M^{km}$-valued process $X$ and an $\mathbb R^m$-valued process $Y$, the stochastic integral (1.7) is

$$\int_0^t X(s-)\,dY(s)=\lim\sum_i X(t_i)\big(Y(t_{i+1})-Y(t_i)\big),$$

the limit in probability along partitions $\{t_i\}$ of $[0,t]$ whose mesh tends to zero. Throughout, $\int X\,dY$ means $\int X(s-)\,dY(s)$. An $\{\mathcal F_t\}$-adapted cadlag process $Y$ is a semimartingale if $Y=M+A$ with $M$ an $\{\mathcal F_t\}$-local martingale and $A$ of finite variation on bounded intervals, with total variation $T_t(A)$ on $[0,t]$. $[M]$ denotes the quadratic variation.

For $\delta\in(0,\infty]$ let $h_\delta(r)=(1-\delta/r)^+$ and

$$J_\delta(x)(t)=\sum_{s\le t}h_\delta\big(|x(s)-x(s-)|\big)\big(x(s)-x(s-)\big),$$

which collects the part of the jumps larger than $\delta$; $Y^\delta=Y-J_\delta(Y)$ then has jumps of size at most $\delta$. Condition C2.2(i) on a sequence $Y_n$ asks for decompositions $Y_n^\delta=M_n^\delta+A_n^\delta$ such that for each $\alpha>0$ there are stopping times $\tau_n^\alpha$ with $P\{\tau_n^\alpha\le\alpha\}\le1/\alpha$ and $\sup_nE\big[[M_n^\delta]_{t\wedge\tau_n^\alpha}+T_{t\wedge\tau_n^\alpha}(A_n^\delta)\big]<\infty$. $\Rightarrow$ denotes convergence in distribution.

Formalization targets

Goal: Theorem 2.2 (distributional part)

For each $n$, let $(X_n,Y_n)$ be $\{\mathcal F^n_t\}$-adapted with paths in $D_{\mathbb M^{km}\times\mathbb R^m}[0,\infty)$, $Y_n$ an $\{\mathcal F^n_t\}$-semimartingale satisfying C2.2(i) for some $\delta\in(0,\infty]$. If $(X_n,Y_n)\Rightarrow(X,Y)$ in the Skorohod topology on $D_{\mathbb M^{km}\times\mathbb R^m}[0,\infty)$, then $Y$ is a semimartingale with respect to a filtration to which $X$ and $Y$ are adapted, and

$$\Big(X_n,\,Y_n,\,\int X_n\,dY_n\Big)\Rightarrow\Big(X,\,Y,\,\int X\,dY\Big)\quad\text{in }D_{\mathbb M^{km}\times\mathbb R^m\times\mathbb R^k}[0,\infty).$$

Milestones, in the order the proof uses them

• Lemma 2.1: time-change-equivariant maps that are continuous for local uniform convergence are Skorohod-continuous, jointly with their argument.
• Continuity of $J_\delta$ (after (2.1)): $(x_n,J_\delta(x_n))\to(x,J_\delta(x))$ and $(x_n,x_n-J_\delta(x_n))\to(x,x-J_\delta(x))$.
• Lemma 6.2: a sequential characterization of Skorohod convergence.
• The step approximation $I_\varepsilon$ of §6, with $r(z(t),I_\varepsilon(z)(t))\le\varepsilon$.
• Lemma 6.1: $z_n\to z$ implies $(z_n,I_\varepsilon(z_n))\to(z,I_\varepsilon(z))$ almost surely in the random thresholds.
• (1.12)–(1.13): integrals against step functions with uniformly bounded jump counts converge, jointly with integrand and integrator.
• (2.2): $\int x_n(s-)\,dJ_\delta(y_n)(s)\to\int x(s-)\,dJ_\delta(y)(s)$.
• (2.7): $E\big[\sup_{s\le t\wedge\tau}|R(s)|\big]\le\varepsilon\big(2E[[M]_{t\wedge\tau}]^{1/2}+E[T_{t\wedge\tau}(A)]\big)$ for $R=\int H\,d(M+A)$ with $|H|\le\varepsilon$.
• Remark 2.4: the limit $Y$ is a semimartingale.

Significance

The result. Theorem 2.2 reduces convergence of stochastic integrals to two checks: joint convergence of integrand and integrator, and the uniform control C2.2(i) on the integrators. Remarks 2.3 and 2.5 give simple sufficient conditions (stochastic boundedness of $T_t(A_n^\delta)$ plus a second-moment bound; relative compactness for a fixed integrator), and Section 5 of the paper derives from it weak limit theorems for stochastic differential equations driven by semimartingales, including Wong–Zakai-type corrections. Without the theorem, each diffusion approximation that passes through an integral equation needs its own ad hoc argument.

Formalizing it. The theorem is proved and classical; nothing here is open. Lean's Mathlib has no Skorohod space, no stochastic integral against a semimartingale and no semimartingale, so the mission produces the first machine-checked definitions of J1 convergence on $D_E[0,\infty)$, of the left-point stochastic integral (1.7), and of convergence in distribution of cadlag processes, together with the deterministic facts about them that a proof of Theorem 2.2 needs. The definitions are meant to be reused by later missions on weak convergence of processes and on stochastic differential equations (the paper's Theorem 5.4 is planned as a follow-up that references them).

Difficulty

The obvious argument — the integral is a continuous function of the pair (integrand, integrator), so the continuous mapping theorem applies — fails in two ways. First, the map $(x,y)\mapsto\int x(s-)\,dy(s)$ is not continuous in the Skorohod topology, and for a general semimartingale integrator it is not even defined path by path. Example 1.1 makes the failure concrete: with $X=Y=X_n=\chi_{[1,\infty)}$ and $Y_n=\chi_{[1+1/n,\infty)}$, each component converges, yet $\int_0^tX_n\,dY_n=1$ for $t>1+1/n$ while $\int_0^tX\,dY=0$, because the jumps of integrand and integrator coalesce in the wrong order; joint convergence of the pair excludes this. Second, Example 1.2 shows that joint convergence is still not enough: integrators whose variation grows without bound (piecewise linear interpolations of Brownian motion) produce an extra drift $\tfrac12t$ in the limit. C2.2(i) is the condition that excludes this, and the identification of the limit integral also requires knowing that the limit $Y$ is a semimartingale, which is not given.

Formalization scope

Time is ℝ≥0; a process is a map ℝ≥0 → Ω → E. $\mathbb R^m$ is Fin m → ℝ and $\mathbb M^{km}$ is Fin k → Fin m → ℝ, with the sup metric; products carry the max metric (J1 convergence does not depend on the product metric). The conventions the formal statements commit to:

• "$x_n\to x$ in the Skorohod topology" is the sequential definition of pp. 1037–1038 with one time change sequence; "uniformly for $t$ in bounded intervals" is uniformly on $[0,T]$ for every $T$. For a pair or a triple the time change is shared by all components.
• "$\Rightarrow$" is convergence in distribution in coupling form: a probability space carrying copies of the processes and of the limit, with almost sure Skorohod convergence. Laws are taken on the product σ-algebra of path space; for the finite-dimensional state spaces here this is equivalent to weak convergence of the laws on $D_E[0,\infty)$.
• The coupling relation is defined for Polish state spaces with their Borel σ-algebras. Every state space in the probabilistic milestones is a finite-dimensional real product and satisfies this requirement.
• $\int X\,dY$ is the in-probability limit of left-point Riemann sums (1.7) over all partition sequences with mesh tending to zero, with cadlag paths. The prelimit integrals are given processes with this property; the limit integral is produced in the conclusion.
• The semimartingale conclusion of Theorem 2.2 is stated for a copy of $(X,Y)$ on a space that may carry extra randomness, with a filtration making both adapted.
• In C2.2(i) the free $t$ is universally quantified ("for every $t\ge0$") and the stopping times are chosen before $t$; expectations of nonnegative quantities are taken in $[0,\infty]$; $t\wedge\tau=t$ when $\tau=\infty$.
• $[M]=\sum_j[M_j]$ with $[M](0)=0$; since C2.2(i) asks for some decomposition, this agrees with Protter's convention $[M](0)=M(0)^2$.
• In (2.1), $|x|=\sum_i|x_i|$ (the paper's convention for vectors, p. 1049); in (2.7), Euclidean norms for $R$ and $T(A)$ and the Frobenius norm for the integrand.
• "a.s." in Lemma 6.1 refers to the law of the thresholds $\theta_k$, i.i.d. uniform on $[\frac12,1]$, and the null set may depend on the convergent sequence.
• $\delta$ ranges over $(0,\infty]$, with $J_\infty=0$.

The theorem has trivializing formalizations, all excluded here: componentwise convergence of $(X_n,Y_n)$ in place of joint convergence; an integral not pinned to (1.7) (any process would do); and assuming the limit integral, or the semimartingale property of $Y$, as a hypothesis.

Local martingales and cross variations reuse the published Ethier–Kurtz definitions EthierKurtz_IsSourceLocalMartingale and EthierKurtz_HasCrossVariation. A complete development needs the Skorohod space and its tightness theory, the stochastic integral against semimartingales (existence and the Burkholder–Davis–Gundy/Doob estimates), and the quasimartingale criterion of Meyer and Zheng. Contributions to any of these layers are welcome; the deterministic milestones (Lemma 2.1, Lemma 6.2, the continuity of $J_\delta$, (1.12)–(1.13), Lemma 6.1) are independent of the probabilistic ones and reusable for any work on the J1 topology.

Selected references

• T. G. Kurtz and P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19 (1991), 1035–1070. https://doi.org/10.1214/aop/1176990334
• A. Jakubowski, J. Mémin and G. Pagès, Convergence en loi des suites d'intégrales stochastiques sur l'espace D¹ de Skorokhod, Probab. Theory Related Fields 81 (1989), 111–137. https://doi.org/10.1007/BF00343739
• S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658
• P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. https://doi.org/10.1007/978-3-662-02619-9
• E. Wong and M. Zakai, On the convergence of ordinary integrals to stochastic integrals, Ann. Math. Statist. 36 (1965), 1560–1564. https://doi.org/10.1214/aoms/1177699916
• P. A. Meyer and W. A. Zheng, Tightness criteria for laws of semimartingales, Ann. Inst. H. Poincaré Probab. Statist. 20 (1984), 353–372. http://www.numdam.org/item/AIHPB_1984__20_4_353_0/