Stochastic Systems

Motivation

Many Markov processes that arise as solutions of stochastic partial differential equations, stochastic delay equations, or other infinite-dimensional models are not strong Feller: their transition probabilities from two nearby starting points can be mutually singular. For such processes convergence to equilibrium cannot hold in total variation, and the classical Harris theorem (a Lyapunov function plus a minorization on a small set) does not apply. Hairer, Mattingly and Scheutzow ([23], 2011) replaced total variation by a coupling distance $W_d$ built from a suitable distance-like function $d$, and proved a weak Harris theorem: contraction of $W_d$ on the whole space, $d$-smallness of the level sets of a Lyapunov function, and the Lyapunov drift together give a unique invariant measure and a rate of convergence. Butkovsky ([6], 2014) extended it to subgeometric rates, and Kulik's monograph ([25], 2017) gives a systematic account.

The remaining difficulty is to verify the contraction hypothesis for a concrete model. Butkovsky, Kulik and Scheutzow (arXiv:1806.00395, Ann. Appl. Probab. 2020) show that it suffices to build a generalized coupling: a pair of processes whose first component has the correct law, whose second component is only close in law to the process started at the other point, and whose components approach each other. Their abstract theorem of §2 is the input to the paper's applications to stochastic functional differential equations and to the 2D Navier–Stokes, Euler-type and Boussinesq SPDEs of §4.

Setting

Let $(E,\rho)$ be a Polish space with Borel $\sigma$-field $\mathcal E$, and let $\{P_t\}_{t\ge0}$ be a Markov transition function: Markov kernels with $P_0(x,\cdot)=\delta_x$ and the Chapman–Kolmogorov identity. Write $P_tf(x)=\int f(y)\,P_t(x,dy)$. The semigroup is Feller if $P_t$ maps bounded continuous functions to continuous functions.

A distance-like function $d:E\times E\to\mathbb R_+$ is symmetric, lower semicontinuous and vanishes exactly on the diagonal. A premetric $\theta$ is lower semicontinuous and vanishes exactly on the diagonal, but need not be symmetric. For probability measures $\mu,\nu$, $\mathcal C(\mu,\nu)$ is the set of couplings and

$d_{TV}(\mu,\nu)=\sup_{A}|\mu(A)-\nu(A)|$ is the total variation distance.

A measurable $V\ge0$ satisfies the Lyapunov condition if, for a concave differentiable $\varphi:\mathbb R_+\to\mathbb R_+$ increasing to infinity with $\varphi(0)=0$ and a constant $K>0$,

Put $H_\varphi(x)=\int_1^x du/\varphi(u)$ for $x\ge1$.

Assumption A asks for a non-increasing $r$ with $r(t)\to0$, a locally bounded $L$, and for every $x,y$ a pair of processes $(X^{x,y},Y^{x,y})$ with $\mathrm{Law}(X^{x,y})=\mathsf P_x$,

Assumption B1 for a set $B$ and $t_0>0$: for every $\varepsilon>0$ there is a set $D$ with $\inf_{x\in B}P_{t_0}(x,D)>0$ and $\sup_{x,y\in D}\theta(x,y)\le\varepsilon$. Assumption B2 is a generalized-coupling version of B1 on a set $B$. The paper's auxiliary distance is $d_N=N\theta(x,y)\wedge N\theta(y,x)\wedge1$.

Formalization targets

Goal: Theorem 2.5

Assume $P$ is Feller, $V$ satisfies the Lyapunov condition, $\rho\wedge1\le\theta$, Assumption A holds, and there is $t_0>0$ such that B1 holds for every level set $\{V\le M\}$ and $t_0$. Then $(P_t)$ has a unique invariant probability measure $\pi$, and for every $\delta\in(0,1)$ there are $C_1,C_2>0$ with

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

Companion: Theorem 2.6

In the exponential case $\varphi(x)=\gamma x$, hypothesis B1 on all level sets may be replaced by B2 on the single level set $\{V\le4K/\gamma\}$; the same bound then holds and is exponential in $t$.

Milestones

In attack order: $d_N$ is distance-like (2.6); the coupling lemma, the gluing lemma and the reimbursement bound used inside the proof of Theorem 2.3(i); Theorem 2.3(i) (contractivity of $d_N$ under A) and (ii) ($d_N$-smallness under B1); the remark after Definition 2.2 that contractivity and smallness give (2.3)–(2.4); the non-expansion step of the proof of Theorem 2.5; Proposition 2.1 (cited weak Harris theorem); and, for the companion, Theorem 2.3(iii), Proposition 2.2 (cited) and Theorem 2.6.

Significance

Theorem 2.5 turns the verification of the weak Harris theorem into two checks that can be carried out model by model: construct a controlled process that is close in law to the true one (Assumption A), and check a support condition on level sets (B1). It covers subexponential rates, given by the function $\varphi$ of the Lyapunov drift, and the Wasserstein distance it controls metrizes weak convergence. Theorem 2.6 is the abstract result behind the exponential ergodicity statements for SPDEs in §4 of the paper.

The results are proved in the paper; none of them, nor the weak Harris theorems of [6] and [23] they rely on, has a machine-checked proof. Mathlib has Markov kernels, their composition and invariant measures, but no coupling distances for lower semicontinuous costs, no maximal coupling or gluing lemma on Polish spaces, and no weak Harris theorem. Propositions 2.1 and 2.2 are cited by the paper, not proved there; formalizing them is part of the mission.

Difficulty

The obvious route to contraction is a true coupling of $P_t(x,\cdot)$ and $P_t(y,\cdot)$ whose components meet or approach. For processes without the strong Feller property, such a coupling is generally not available explicitly; the generalized coupling only gives the second marginal up to a total variation error. Turning the error-in-law bound into a statement about $W_{d_N}$ needs a maximal coupling of two laws on a Polish space and a gluing of two couplings along a common marginal, both of which rest on disintegration of measures. The cited Proposition 2.1 is itself a substantial result: existence of an invariant measure needs tightness from the Lyapunov drift and the Feller property, and the subexponential rate needs a careful interpolation between the drift and the contraction.

Formalization scope

The state space is any type with MetricSpace, CompleteSpace, SeparableSpace and the Borel σ-algebra; $\rho$ is dist. Time is ℝ≥0 and $P$ is a map ℝ≥0 → Kernel E E with Markov kernels, $P_0=\mathrm{id}$, Chapman–Kolmogorov, and measurability of $s\mapsto P_s(x,A)$, which the time integral in (2.2) presupposes. Expectations, $P_tV$ and $W_d$ are lower Lebesgue integrals in $[0,\infty]$, and (2.2) is stated without subtraction ($P_tV+\int_0^tP_s(\varphi\circ V)\,ds\le V+Kt$), which is equivalent. A pair of processes is represented by its joint law on path space; $\mathrm{Law}(X^{x,y})=\mathsf P_x$ is read through the one-dimensional marginals $\mathrm{Law}(X^{x,y}_t)=P_t(x,\cdot)$, a weaker hypothesis. Total variation is the published MarkovChainCLT.tvDist, without a factor 2. "Unique invariant measure" means unique among probability measures, with invariance $\int P_t(x,\cdot)\,\pi(dx)=\pi$ for every $t$. $H_\varphi^{-1}(C_2t)$ is encoded by quantifying over every $u\ge1$ with $H_\varphi(u)=C_2t$; such a $u$ exists and is unique under the Lyapunov condition. In Proposition 2.1 condition 2 is stated as $\rho\wedge1\le d$, which is Proposition 2.1 for the equivalent complete metric $\rho\wedge1$ and is the form the proof of Theorem 2.5 uses.

No statement relies on a junk value: no Bochner integral of a possibly non-integrable function, no real-valued infimum over a possibly empty or unbounded set, no Measure.map along a non-measurable map, no default-valued inverse of $H_\varphi$ (which would make the bound read $W\le0$), and "invariant" is never used without "probability".

A complete development needs: Kantorovich-type coupling distances for lower semicontinuous costs, maximal couplings and gluing on Polish spaces, the transfer of $W_d$-bounds through Markov kernels, and the weak Harris theorem with subexponential rates. All of these are reusable well beyond this mission. Contributions to any milestone, including the cited Propositions 2.1 and 2.2, are welcome.

Selected references

• O. Butkovsky, A. Kulik, M. Scheutzow, Generalized couplings and ergodic rates for SPDEs and other Markov models, Ann. Appl. Probab. 30(1), 2020. arXiv:1806.00395, doi:10.1214/19-AAP1485
• M. Hairer, J. C. Mattingly, M. Scheutzow, Asymptotic coupling and a general form of Harris' theorem with applications to stochastic delay equations, Probab. Theory Related Fields 149, 2011. arXiv:0902.4495
• O. Butkovsky, Subgeometric rates of convergence of Markov processes in the Wasserstein metric, Ann. Appl. Probab. 24(2), 2014. arXiv:1211.4273
• A. Kulik, Ergodic Behavior of Markov Processes, De Gruyter, Berlin, 2017. doi:10.1515/9783110458930
• C. Villani, Optimal Transport: Old and New, Springer, 2009 (coupling lemma, Theorem 4.1; gluing, p. 23). doi:10.1007/978-3-540-71050-9

Why lost-sales inventory with lead times matters

In many retail and spare-parts settings, demand that cannot be met from stock is lost rather than backlogged, and replenishment orders arrive only after a positive lead time. The resulting lost-sales inventory model is a basic model of inventory theory. Its optimal policy depends on the whole pipeline of outstanding orders, so dynamic programming over that state becomes intractable as the lead time grows. This is why the model is often replaced by its backlogged counterpart, even when that approximation is poor (Bijvank and Vis, 2011).

Simple heuristics are therefore of practical interest. The simplest is the constant-order policy, which orders the same amount in every period regardless of the state. Reiman (2004, unpublished manuscript) showed that the best constant-order policy sometimes outperforms the base-stock policy, and Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante (arXiv:1211.4063, Math. Oper. Res. 2016) proved that it is asymptotically optimal as the lead time grows, with a gap that decays polynomially in the lead time. Xin and Goldberg (arXiv:1409.1499v2, Oper. Res. 2016) proved that for the infinite-horizon average-cost problem the gap actually decays exponentially, with an explicit rate and explicit constants. This mission formalizes that result.

Timeline:

• 1958: Karlin and Scarf introduce the lost-sales model with a positive lead time; convexity results follow in Karlin and Scarf (1958) and Morton (1969).
• 1962: Kingman bounds how fast the expected waiting time of an initially empty GI/G/1 queue approaches its steady-state value (doi).
• 2004: Reiman finds that the best constant-order policy can outperform the base-stock policy.
• 2009: Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 55(3)) prove base-stock policies asymptotically optimal as the lost-sales penalty grows.
• 2011: Huh, Janakiraman and Nagarajan (Operations Research 59(1)) give the existence of stationary optimal policies used by the paper.
• 2015–2016: Goldberg et al. prove asymptotic optimality of constant-order policies as the lead time grows; Xin and Goldberg prove exponential decay of the gap.

The setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with law $\mathcal D$, finite mean $\mathbb E[D]$ and strictly positive variance. The lead time $L\ge1$ is an integer, $h>0$ is the unit holding cost and $p>0$ the unit lost-sales penalty. At the start of period $t$ there is on-hand inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of orders placed but not yet delivered. In each period, $x_{1,t}$ arrives, a new order is placed (it enters the end of the pipeline), demand $D_t$ is realized, and the period cost

is incurred; then $I_{t+1}=(I_t+x_{1,t}-D_t)^+$. The system starts empty. A policy $\pi$ chooses orders from the information available, and its long-run average cost is $C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$. The optimal cost is $\mathrm{OPT}(L)=\inf_\pi C(\pi)$.

The constant-order policy $\pi_r$ orders $r$ in every period. Its cost is governed by the random walk $jr-\sum_{i=1}^jD_i$ through

the steady-state and $L$-th waiting times of a single-server queue with interarrival law $\mathcal D$ and constant service time $r$. The best constant order $r_\infty$ is the least minimizer of $C(\pi_r)$ over $0\le r\le\mathbb E[D]$. The rate and constants are

with $\vartheta$ the largest minimizer in the definition of $\gamma$ ($\vartheta=\infty$ if the infimum is not attained, and $1/\infty=0$).

Formalization targets

Goal: Theorem 1 (p. 8)

The quantities $r_\infty,\gamma,\vartheta,g$ depend on $\mathcal D,h,p$ but not on $L$.

Milestones, in the order the proof uses them

• Eq. (3): $C(\pi_r)=h\,\mathbb E[I^r_\infty]+p\,\mathbb E[D]-pr$ for $r\in[0,\mathbb E[D])$.
• Sec. 2.2: the best constant exists and $r_\infty<\mathbb E[D]$; Sec. 2.3: $\vartheta>0$, $\gamma\in[0,1)$, $g>0$ and $\mathrm{OPT}(L)\ge g$.
• Observation 1 (convexity of $\mathfrak f_{\mathbf d}$ and a Jensen bound) and Lemma 2: $\mathrm{OPT}(L)\ge C_L(r_L)$ and the decomposition (5) of $C(\pi_{r_\infty})-\mathrm{OPT}(L)$.
• Lemma 3 (Kingman's series and the tail bound), Lemma 4 ($r_\infty\le r_L$), Lemma 5 ($\sum_n\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\ge p/h$), the Chernoff step $\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\le\gamma^n$, and the bound on the term (6).
• Further: Lemma 1 (monotonicity of $\gamma$ in $p/h$) and Corollary 1 (the closed form for exponential demand).

Significance

The theorem shows that a lead time of order $\log(\epsilon^{-1})$ suffices for the constant-order policy to be within a factor $1+\epsilon$ of optimal, whereas the earlier bounds of Goldberg et al. needed a lead time polynomial in $\epsilon^{-1}$. The constants are explicit and computable from the demand law: for exponential demand with $p=h$ and $L=1$ the bound is already about $3.36$, and it approaches $1$ quickly as $L$ grows (Table 1 of the paper). Lemma 1 adds that the rate $\gamma$ worsens as $p/h$ grows, the regime opposite to the one in which base-stock policies are known to be nearly optimal.

The result is proved on paper; no machine-checked proof is known to exist. A formalization would produce a checked infinite-horizon lost-sales model and a checked statement of Kingman's random-walk identities for this queue. It would also produce checked comparisons of an arbitrary history-dependent policy with constant-order policies through convexity. The statement here is taken over a policy class at least as large as the paper's, so a proof also extends the result to randomized history-dependent policies.

Difficulty

The cost of the constant-order policy is the expected supremum of a random walk, while the optimal policy has no closed form and may not even induce a stationary distribution. The paper avoids the steady state of the optimal policy by constructing a random vector with the needed stationarity properties (Theorem 2). That construction is not part of this mission. Here, the lower bound on $\mathrm{OPT}(L)$ in Lemma 2 instead goes through the published, proved lower certificate for the full policy class. The second obstacle is quantitative: the exponential rate comes from comparing the minimizers $r_\infty$ and $r_L$ of two different convex functions (Lemma 4) and from a first-order optimality condition involving a non-differentiable expectation (Lemma 5). Neither follows from the observation that one function dominates the other.

Formalization scope

The model is the published CappedBaseStock model: zero-based time, an empty initial state, demand laws on $[0,\infty)$ with finite positive mean, and costs and long-run averages in $[0,\infty]$. $\mathrm{OPT}(L)$ is the infimum over all measurable, history-dependent, possibly randomized policies. That class contains the paper's Markov deterministic class $\Pi$, so every statement involving $\mathrm{OPT}(L)$ is at least as strong as printed. "Strictly positive variance" is encoded as "the demand law is not a point mass". It is a hypothesis wherever the paper's argument needs it; the Chernoff step, eq. (3) and Corollary 1 do not need it.

$C(\pi_r)$ is the model's long-run cost of the constant policy, not formula (3), and $\mathbb E[I^r_\infty]$ is a lower integral in $[0,\infty]$, so that eq. (3) and Lemma 3 are not true by definition. $r_\infty$ and $r_L$ are infima of the argmin sets, whose nonemptiness is a milestone. $1/\vartheta$ is encoded with the paper's convention $1/\infty=0$. Lemma 3's tail bound is stated additively in $[0,\infty]$, and the series in Lemmas 3 and 5 are extended-real series indexed from $0$. The goal's ratio is taken in $[0,\infty]$, where $x/0=\infty$ for $x\neq0$. None of $\gamma<1$, $g>0$ or $r_\infty<\mathbb E[D]$ is assumed: all three are milestones. A formalization that defines $\mathrm{OPT}$ over constant-order policies only, fixes $r$ instead of $r_\infty$, treats $\gamma,\vartheta,g$ as free parameters, or takes the ratio in $\mathbb R$ after truncating infinite costs would make the goal trivial and is ruled out. The objects are defined from the full parameter record, which includes $L$. That they do not depend on $L$ follows from eq. (3) and the existence milestone.

No statement corrects a printed slip. Theorem 2 (existence of the stationary vector) and eq. (2) (bounded stationary optimal policies) are not stated; Observation 1 instead takes Theorem 2's properties (i)–(iii) as hypotheses on an arbitrary law. The source is arXiv:1409.1499v2, whose printed page numbers equal the PDF's. Useful infrastructure: Lindley-type random-walk suprema, Spitzer–Kingman identities, Chernoff bounds for i.i.d. sums (Mathlib's measure_le_le_exp_mul_mgf), and Cesàro limits of expected costs. All of it is reusable for other queueing and inventory missions. Proofs of any milestone are welcome, and the Chernoff step is the natural entry point.

Selected references

• L. Xin, D. A. Goldberg, Optimality gap of constant-order policies decays exponentially in the lead time for lost sales models, Operations Research 64(6), 2016; preprint arXiv:1409.1499v2. https://arxiv.org/abs/1409.1499v2
• D. A. Goldberg, D. A. Katz-Rogozhnikov, Y. Lu, M. Sharma, M. S. Squillante, Asymptotic optimality of constant-order policies for lost sales inventory models with large lead times, Mathematics of Operations Research, 2016; preprint arXiv:1211.4063. https://arxiv.org/abs/1211.4063
• J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49, 1962. https://doi.org/10.1093/biomet/49.3-4.315
• M. Bijvank, I. F. A. Vis, Lost-sales inventory theory: a review, European Journal of Operational Research 215(1), 2011. https://doi.org/10.1016/j.ejor.2011.02.004
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

Why expected recourse is a counting question

A two-stage stochastic program chooses a first action before uncertainty is observed and then takes a recourse action after the observation. Evaluating the expected optimal recourse value can be difficult even when the recourse problem for each fixed observation is a small linear program. This mission isolates the example in Section 3 of Hanasusanto, Kuhn and Wiesemann's preprint: the second-stage program has no first-stage decision at all, yet sufficiently accurate expected values determine how many ways a finite partial order can be arranged into a total order.

The counting connection has a specific history. Brightwell and Winkler (1991) established the complexity of counting linear extensions and related their number to an order-polytope volume. Hanasusanto, Kuhn and Wiesemann use that relation in their October 2015 preprint to establish Theorem 3's strong #P-hardness claim for approximate expected recourse with random recourse coefficients. The mission addresses the exact mathematical relation and the error threshold that support that claim. The complexity-class and encoding parts are outside its Lean statement.

Finite orders, volumes, and program (10)

Let $P$ be a finite partially ordered set with $k=|P|$. A linear extension lists its elements in a total order that respects the partial order. The number of these lists is $N(P)$. The unit cube is $C=[0,1]^P$. Its order polytope is

Write $V(P)$ for the Lebesgue volume of $O(P)$. The paper writes $S=\{1,\ldots,k\}$ and $P(S;\preceq)$ for this polytope; changing the names of the elements does not change either the count or the volume.

For a realization $\xi\in C$, define $q_P(\xi)$ as the optimal objective value of the paper's random-recourse program (10). It maximizes a scalar $z$, subject to $0\le z\le1$, nonnegative variables $y_{ij}$, and

The sum includes reflexive pairs, for which the summand is zero. The expected recourse value is $Q(P)=\int_C q_P(\xi)\,d\xi$. Lebesgue measure of $C$ is one, so this integral is the expectation under the uniform distribution on the cube. The program is feasible for every $\xi$: $y=0$ and $z=0$ are allowed. Its objective is bounded by one because $z\le1$. These details give the value a genuine finite meaning at every realization.

Formalization targets

The first target is the exact value of the second stage for every $\xi\in C$:

Consequently, the expected recourse value satisfies the displayed identity in the proof of Theorem 3:

The counting target quoted in the proof of Lemma 3 is

Lemma 3's rounding step concerns an approximation $\vartheta$ of $V(P)$. If $|\vartheta-V(P)|\le\varepsilon$ and $0\le\varepsilon<1/(2k!)$, then $|k!\vartheta-N(P)|<1/2$. The mission's main goal uses an approximation of $Q(P)$, as in Theorem 3. Under the same strict error threshold,

The target leaves no independent dimension parameter or unspecified oracle value: $k$ is the cardinality of the very poset used in program (10), and $\vartheta$ must approximate that program's expected value. The strict half-unit bound makes $N(P)$ the unique nearest integer to $k!(1-\vartheta)$.

What the result provides

The theorem shows that an accurate numerical answer to the expected-recourse question contains an exact combinatorial count. This explains why a routine second-stage linear optimization problem can lead to a difficult expectation problem: the expectation records the volume of a polytope whose geometry encodes all linear extensions. The page's threshold specifies precisely how much accuracy is needed to recover the count; a coarser estimate does not support the same rounding conclusion. The original paper also explains why its instance yields strong #P-hardness: the coefficients needed for its random-recourse representation are only $-1$, $0$, and $1$ in the continuation of Theorem 3's proof.

Formalizing the reduction's mathematical claims produces reusable interfaces for order-polytopes, their volumes, and the expectation of this recourse program. It also poses the factorial volume identity as a theorem rather than treating it as a free assumption. The published Prove2Me definition FCP.Order.LinearExtensions already represents the same linear-extension object and is reused here. The five theorem statements in this proposal are open proof obligations; the existence of the published definition is not a claim that these results already have machine-checked proofs. Proofs of the pointwise value, the expectation identity, the volume identity, and the rounding consequences are welcome.

Where the difficulty lies

For a fixed realization, the program's $y_{ij}$ variables have no upper bounds. That feature makes its value jump between zero and one according to whether the order inequalities hold. The pointwise characterization does not by itself settle the expectation: the set where the value changes must be represented measurably, and the integral is over the unit cube with its normalized mass. The factorial relation is a separate geometric statement about the order polytope. Simply counting its defining inequalities gives neither its volume nor the number of linear extensions. These are the substantive steps behind the short rounding calculation.

Formalization scope and conventions

Lean uses a finite type with a PartialOrder in place of the paper's labeled set $S=\{1,\ldots,k\}$. The published FCP.Order.LinearExtensions definition counts order-preserving bijections from this type to the positions $0,\ldots,k-1$. It has exactly the paper's meaning of a compatible permutation. The cube and order polytope are sets of real-valued functions on that finite type. Volume is volume converted to a real number; expected recourse is the Lebesgue integral over the cube. The cube has mass one, including when $P$ is empty, and the results include that edge case.

The reusable cube, order polytope, volume, and linear-extension count form a separate definition module. The paper's second-stage program imports that module and defines only its own feasible levels, optimal value, and expected recourse.

The second-stage program is encoded through its feasible objective levels and their real supremum. Since zero is feasible and every feasible level is at most one, the supremum cannot use Lean's default value for an empty or unbounded real set. Classical decidability selects the comparable pairs in the finite sum. Accuracy means an absolute-error inequality with a nonnegative $\varepsilon$ and a strict threshold $\varepsilon<1/(2k!)$. These choices preserve both the page's feasibility and its rounding margin.

The main goal is the correctness of the reduction in Theorem 3. It does not formalize #P, strong #P-hardness, pseudo-polynomial running time, unary encodings, or bit lengths. A formulation that assumes $Q(P)=1-V(P)$ or $N(P)=k!V(P)$ in the goal would erase the result's content; those are separate milestone theorems. Reusable work includes the finite-order volume identity and measure-theoretic handling of the indicator on the cube. The preprint's Section 3 supplies every object and convention used here.

Selected references

• G. A. Hanasusanto, D. Kuhn, and W. Wiesemann, A comment on “computational complexity of stochastic programming problems”, Optimization Online preprint 2015/03/4825, version of October 6, 2015, pp. 10–12. Preprint.
• G. Brightwell and P. Winkler, Counting linear extensions, Order 8(3), 225–242, 1991. DOI.

Motivation

The lost-sales inventory model with a positive lead time is one of the basic models of inventory theory. A retailer reviews stock once per period, places an order that arrives $L$ periods later, and loses (rather than backlogs) any demand that cannot be met from stock on hand. Lost sales are the norm in retail, where a customer facing an empty shelf buys elsewhere. The optimal policy is the solution of a dynamic program whose state is the on-hand inventory together with the whole pipeline of $L$ outstanding orders. The state dimension therefore grows with the lead time, and computing the optimal policy is intractable beyond small $L$: for a lead time of four and geometric demand the dynamic program already has 228,581 states (Zipkin 2008a, Operations Research 56(5), 1256–1263).

Heuristics (base-stock, myopic, cost-balancing) have been studied at length. Reiman (2004) analyzed an open-loop policy that orders one unit at fixed intervals in a continuous-review lost-sales model with Poisson demand. Zipkin (2008a) observed numerically that ordering the same constant amount every period performs well already at lead time four. Huh, Janakiraman, Muckstadt and Rusmevichientong (2009) proved that order-up-to policies are asymptotically optimal as the lost-sales penalty grows. Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante proved that a constant-order policy is asymptotically optimal as the lead time grows, with an explicit threshold. This mission formalizes that result, Theorem 1 of their paper.

Setting

Fix a holding cost $h>0$ per unit left over at the end of a period, a lost-demand penalty $c>0$ per unit of unmet demand, a lead time $L\ge1$, and a horizon $T>L$. Demands $D_1,D_2,\dots$ are i.i.d. with a law $\mathcal D$ on $[0,\infty)$ that has a finite third moment and is not deterministic. At the start of period $t$ the system holds inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of outstanding orders. First $x_{1,t}$ arrives; then an order is placed and joins the end of the pipeline; then $D_t$ is realized, and

The system starts empty. A policy chooses each order from the information available before the period's demand, possibly with randomization. Problem (1) is

For $r\ge0$ let $I^r_\infty=\sup_{k\ge0}\big(kr-\sum_{i=1}^kD_i\big)$, the steady-state waiting time of a GI/D/1 queue. For $r<\mathbb E[D]$ the constant-order policy $\pi_r$ orders the random amount $I^r_\infty+r$ (drawn independently of the demands) in the first period and $r$ in every later period. The best constant is $z=\arg\min_{v\ge0}(h\mathbb E[I^v_\infty]-cv)$ (the smallest minimizer). With $Q$ the $c/(c+h)$ quantile of $\mathcal D$, $g=h\mathbb E[(Q-D)^+]+c\mathbb E[(D-Q)^+]$, $\sigma$ the standard deviation and $\zeta$ the skewness of $D$, set $m=\lceil(26(3\zeta+c(h\sigma)^{-1}\mathbb E[D]+1))^2\rceil$ and

Formalization targets

Goal: Theorem 1

For all $\epsilon\in(0,1)$, $L\ge y(\epsilon)$ and $T\ge(1+3\epsilon^{-1})L$,

Milestones

The milestones follow the paper's argument in its order:

• the cost of $L$ consecutive periods from a given state (Lemma 3) and under $\pi_r$ (Lemma 4);
• a bounded optimal policy (Lemma 5) and the existence of a most favourable state $(\mathbf x^*,\mathcal I^*)$ (§5);
• lower bounds on the optimal cost over $L$ periods (Lemmas 6, 7);
• random-walk estimates ((26) and Lemma 9) and the per-window gap of $\pi_{r^*}$, $r^*=L^{-1}\sum_ix^*_i$ (Theorem 8);
• an explicit Lipschitz CLT rate (Theorem 11), the separation $\mathbb E[D]-r^*\ge\frac12\sigma m^{-1/2}$ (Lemma 10), and the resulting explicit gap (Corollary 12);
• the newsvendor bound $\mathbb E[C^\pi_t]\ge g$ (§3.1) and the stationary cost of $\pi_r$, (25).

Significance

The theorem says that the policy which ignores the state entirely, ordering the same amount every period after a single randomized first order, loses at most a factor $1+\epsilon$ against the optimal policy once the lead time exceeds an explicit threshold. The threshold depends only on $h$, $c$ and the demand law. Optimal policies are out of computational reach precisely when $L$ is large, so this is the first guarantee of near-optimality whose computation does not grow with the lead time. The paper's Corollary 2 (the ratio tends to $1$ as $L\to\infty$) follows directly.

The result is proved in the paper (up to the correction below); this platform holds no formalization of it or of its lemmas. A formalization would produce reusable statements about suprema of random walks with negative drift (Lemma 9, (26)), a quantitative central limit theorem for Lipschitz test functions (Theorem 11), and the finite-horizon lost-sales problem built on the published model of this platform.

Difficulty

The obvious comparison fails. An optimal policy may vary its orders arbitrarily over time, so its pipeline need not look like a constant stream. Comparing it period by period with $\pi_r$ gives nothing, because the inventory of $\pi_r$ is driven by an unbounded random-walk supremum.

The paper instead bounds the optimal cost over any $L$ consecutive periods by the cost from the most favourable state. It then has to show that the average $r^*$ of that state's pipeline stays bounded away from $\mathbb E[D]$ uniformly in $L$. This last step is the crux. The components of $\mathbf x^*$ may vary considerably over the window, and a qualitative central limit theorem is not enough: the argument needs an explicit rate (Theorem 11) with constants that survive summation over $L$ windows. On the probabilistic side, the expectations of random indices $i^r_k$ at which random walks attain their maxima are not adapted to the demand filtration. They are controlled only through the distributional identity of Lemma 9 and the geometric tail (26).

Formalization scope

The model is the published CappedBaseStock_Model. Its parameter record supplies $L\ge1$, $h>0$ and the penalty $c>0$ (field p; the record is called prm). Its demand law supplies a probability law on $[0,\infty)$ with finite positive mean. The finite third moment and non-determinism are explicit hypotheses. $Q$ and $g$ are the published newsvendorLevel and backorderCost. The conventions:

• Time is zero-based: Lean period $t$ is the paper's period $t+1$, and a window starting at Lean $t_0$ is the paper's $\tau=t_0+1$. Pipeline slot $i$ is $x_{i+1}$.
• Costs, OPT and expectations of nonnegative quantities are lower integrals in $[0,\infty]$, and $I^r_\infty$ is valued in $[0,\infty]$. Real expectations appear only for integrable quantities.
• OPT is the infimum over the model's admissible policies: measurable functions of past demands and a private uniform seed. This class contains the paper's policy class, so OPT is at most the paper's and the goal is at least as strong as the page.
• "Conditional on $\mathbf x^\pi_\tau=\mathbf x$, $I^\pi_\tau=\mathcal I$" is rendered by running the system from that state. Lemma 3 states that this integrates back to the policy's cost.
• Lemmas 6–7, Theorem 8 and Corollary 12 are stated for every policy that almost surely never orders more than $Q$, which includes the paper's optimal $\bar\pi$; their proofs use only that bound.
• $\pi_r$ draws its first order as the quantile function of $I^r_\infty$ at the policy's uniform seed.
• The ratio of Theorem 1 is stated multiplicatively. A ratio would read $0$ at $\mathrm{OPT}=0$, whereas $\mathrm{OPT}(L,T)\ge Tg>0$.

A correction. As printed, the second term of $y(\epsilon)$ (p. 5) and of Corollary 12 (p. 14) lack a factor $\mathbb E[D]$. The proof of Corollary 12 establishes $\mathcal I^*\le(\lceil(2ch^{-1}L)^{1/2}\rceil+2)\mathbb E[D]$, and the printed bounds are not invariant under rescaling the demand. Both are stated here with the factor restored, and each item's note says so.

Neither a long-run average cost nor a restricted comparator (stationary, Markov, or bounded-order) may replace the finite-horizon OPT. The demand law may not be specialized, and $\pi_r$ may not order $r$ in its first period: each change makes the goal a different, easier theorem.

A complete development needs Lindley-type recursions and the stationarity of the GI/D/1 waiting time, Chernoff and moment bounds for random-walk maxima, a Stein-method CLT rate, and the existence of optimal policies for a finite-horizon problem with a continuous state. The random-walk and CLT parts are independent of inventory theory and reusable. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• D. A. Goldberg, D. A. Katz-Rogozhnikov, Y. Lu, M. Sharma, M. S. Squillante, Asymptotic Optimality of Constant-Order Policies for Lost Sales Inventory Models with Large Lead Times, Mathematics of Operations Research, 2016; preprint arXiv:1211.4063v2 (cited version). https://arxiv.org/abs/1211.4063
• P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5), 1256–1263, 2008.
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4), 937–944, 2008.
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 404–420, 2009.
• M. Reiman, A New and Simple Policy for a Continuous Review Lost-Sales Inventory Model, unpublished manuscript, 2004.
• L. H. Y. Chen, Q.-M. Shao, Stein's Method for Normal Approximation, in An Introduction to Stein's Method, 1–59, 2005.
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003.

Motivation

Escape to infinity can be arbitrarily slow for a general stochastic process. The source asks whether independent uniformly elliptic lattice environments force a positive deterministic speed whenever a direction is transient. The source is OpenAI's September 2026 manuscript.

Setting

Uniform ellipticity provides one positive lower bound for all step probabilities, almost surely at every site. Directional transience means the position projected onto a fixed unit vector tends to positive infinity almost surely under the law averaging environment and walk.

Formalization targets

The theorem (admitted, not proved here) states that, for every dimension d ≥ 2 and every Borel probability measure ν on the set of transition rows (a row is a probability vector p over the 2d nearest-neighbour directions ±e_i of ℤ^d, with entries nonnegative and summing to 1), the following holds. Suppose ν is uniformly elliptic, meaning there is κ > 0 with p(e) ≥ κ for every direction e, for ν-almost every row p. Let ℓ be a unit vector in ℝ^d (ℓ·ℓ = 1), and suppose the walk is directionally transient in direction ℓ. Here the environment assigns to each site of ℤ^d an independent ν-distributed row, the walk starts at the origin and at each step moves from its current site x in direction e with probability given by the row at x, and the annealed law averages over the environment and the walk. Directional transience means that, almost surely under this annealed law, the inner product of the walk position X_n with ℓ tends to +∞ as n → ∞. The conclusion is that there exists a vector v ∈ ℝ^d with v·ℓ > 0 such that the walk has asymptotic velocity v, that is, X_n/n → v as n → ∞ almost surely under the annealed law. In other words, directional transience of an i.i.d. uniformly elliptic random walk in random environment in dimension at least two implies ballisticity with a nonzero velocity having positive component along ℓ.

The goal is OAI.DirectionalTransience.directional_transience_implies_ballisticity. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• positive probability transience velocity hemisphere.

Significance

The chosen central target converts almost-sure transience to a velocity statement in every dimension at least two. The separate dimension-at-least-three statement starts from positive probability and identifies the transient hemisphere. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Transience controls eventual direction but not the time spent in traps. A law of large numbers with positive projected velocity needs quantitative control of these delays.

Formalization scope

The main statement assumes $d\ge2$, a unit direction, and an independent identically distributed uniformly elliptic environment. The supporting hemisphere target assumes $d\ge3$ and a nonzero direction. Their original definition groups stay separate.

The shared definitions are supplied by DirectionalBallisticity, VelocityHemisphere. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Directional transience implies ballisticity, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A telephone call center must decide how many agents $N$ to staff against an offered load $R=\lambda/\mu$ (arrival rate over service rate). Staff too few and callers wait and hang up; staff too many and agents sit idle. For large centers the industry rule of thumb is square-root safety staffing, $N\approx R+\beta\sqrt R$, and the question is what service level such a rule buys.

For the model without abandonment, the $M/M/N$ queue, the answer is the theorem of Halfin and Whitt (Oper. Res. 1981): the probability of waiting has a nondegenerate limit in $(0,1)$ exactly when $\sqrt N(1-\rho_N)\to\beta>0$. Real callers are impatient, and Garnett, Mandelbaum and Reiman (M&SOM 2002) prove the analogue for the Erlang-A queue, where abandonment changes both the limits and the admissible range of $\beta$. Their Theorem 4 is the theoretical basis of the "quality-and-efficiency-driven" (QED) staffing regime used in call-center practice.

Timeline. Palm (1943) introduced exponential patience; Riordan (1962) computed the conditional mean wait of the model; Jagerman (1974) gave the asymptotics of the Erlang-B formula; Halfin and Whitt (1981) proved the square-root law for $M/M/N$ ($\beta>0$ only); Fleming, Stolyar and Simon (1994) found the limiting stationary law of the scaled Erlang-A queue; Garnett, Mandelbaum and Reiman (2002) proved the three-way equivalence below, for $\beta$ of either sign.

Setting

The Erlang-A queue ($M/M/N+M$) has Poisson arrivals of rate $\lambda>0$, $N\ge1$ identical agents with exponential service of rate $\mu>0$, an unlimited waiting room served in order of arrival, and independent exponential patience times of rate $\theta>0$: a caller whose wait exceeds their patience abandons. The number in system is a birth–death process with birth rate $\lambda$ and death rate $\min(k,N)\mu+(k-N)^+\theta$; its stationary law is

The three performance measures are:

• the delay probability $P_N\{W>0\}=\sum_{k\ge N}\pi_k$, the chance an arriving caller must wait;
• the abandonment probability $P_N\{Ab\}=\sum_{n\ge0}\pi_{N+n}\,\frac{(n+1)\theta}{N\mu+(n+1)\theta}=\frac{\theta}{\lambda}\sum_{k>N}(k-N)\pi_k$;
• the Erlang-B blocking probability $P_N\{Bl\}=E(\lambda/\mu,N)$ of the loss system $M/M/N/N$.

Write $\varphi,\Phi$ for the standard normal density and distribution function, $h(x)=\varphi(x)/[1-\Phi(x)]$ for its hazard rate, and

In the asymptotic statements the $N$-th system has $N$ agents, arrival rate $\lambda_N$, the fixed service rate $\mu$, patience rate $\theta_N$, and traffic intensity $\rho_N=\lambda_N/(N\mu)$.

Formalization targets

Goal: Theorem 4 (p. 219)

With $\theta_N\equiv\theta\in(0,\infty)$, the following are equivalent:

in which case $\alpha=w(-\beta,\sqrt{\mu/\theta})$ and $\Delta=[\sqrt{\theta/\mu}\,h(\beta\sqrt{\mu/\theta})-\beta]\,\alpha$.

Milestones

1. The weak limit of the scaled stationary queue $(Q_N(\infty)-N)/\sqrt N$ (proof of Theorem 2*, Part 2, p. 225).
2. Lemma 1: $P_N\{W>0\}\to w(-\beta,\sqrt{\mu/\theta})$.
3. Three exact finite-$N$ identities for $P_N\{Ab\}$ (Riordan, Palm, and the final form in $P_N\{W>0\}$ and $P_N\{Bl\}$), p. 226.
4. The Erlang-B asymptotic $\sqrt N\,P_N\{Bl\}\to h(-\beta)$.
5. Lemma 2: $\sqrt N\,P_N\{Ab\}\to[\sqrt{\theta/\mu}\,h(\beta\sqrt{\mu/\theta})-\beta]\,w(-\beta,\sqrt{\mu/\theta})$.
6. The Remark on the extremes: $\beta=-\infty$ iff $\alpha=1$ iff $\Delta=\infty$, and $\beta=+\infty$ iff $\alpha=0$ iff $\Delta=0$.

Lemmas 1 and 2 and the stationary limit are stated with $\theta_N\to\theta\in(0,\infty)$, the paper's setting for them.

Significance

The result. Theorem 4 states that a single parameter, the scaled staffing gap $\beta$, determines both service measures in the limit, and that no other staffing sequence gives a nondegenerate delay probability or abandonment of order $1/\sqrt N$. Because $\beta$ may be negative, a call center with impatient callers can be staffed below the offered load and still keep abandonment at order $1/\sqrt N$, which is impossible without abandonment. The explicit $\alpha(\beta)$ and $\Delta(\beta)$ turn a target delay probability or abandonment level into a value of $\beta$, which is the staffing rule of Table 4 of the paper.

Formalizing it. The theorem is proved in the paper, partly by citation (Fleming et al. for the stationary limit, Jagerman for Erlang-B, Riordan and Palm for exact formulas); none of it has been machine-checked. A formalization supplies the cited inputs, the exact identities, and the converse directions, which the paper treats briefly. The $\theta=0$ counterpart, the Halfin–Whitt theorem, is posed separately on the platform (QueueingFundamentals.BirthDeath.halfin_whitt, HalfinWhitt81.Stationary.theorem_1) and is not a target here.

Difficulty

Every quantity is an explicit series, but its limit is a local-limit problem. The $N$ terms below $N$ form a Poisson-type sum whose normalized tail must be shown to converge to a Gaussian integral uniformly enough to pass through the normalization. The terms above $N$ form a product whose logarithm must be expanded to second order in $(k-N)/\sqrt N$. The two pieces enter with comparable weight, so neither can be dropped. Termwise convergence alone does not suffice: the series need tail bounds uniform in $N$. The converse directions require monotonicity of $\alpha$ and $\Delta$ in $\beta$ and the extreme regimes, not only the limits at finite $\beta$.

Formalization scope

• Model. All objects are explicit functions of $(N,\lambda,\mu,\theta)$ defined in ErlangA.Staffing.Model; the stationary law is the explicit normalized sequence, not an arbitrary steady state. The sequences are $\lambda,\theta:\mathbb N\to\mathbb R$ with $\lambda_N,\theta_N>0$ for $N\ge1$, and $\mu>0$ is fixed.
• Delay. $P_N\{W>0\}=\sum_{k\ge N}\pi_k$ (arrivals finding all agents busy). The paper's proof writes $P\{Q_N(\infty)>N\}$, which differs by $\pi_N\to0$.
• Abandonment. $P_N\{Ab\}$ is the arrival form above. It equals the balance form $(\theta/\lambda)\sum_{k>N}(k-N)\pi_k$ of equation (2).
• Limits. Every limit is Filter.Tendsto … atTop of the $N$-th quantity; $\pm\infty$ limits use atTop/atBot. The ranges $\beta\in\mathbb R$, $\alpha\in(0,1)$, $\Delta\in(0,\infty)$ are part of the goal: without them the equivalence is false (the delay probability also converges, to $1$, when $\sqrt N(1-\rho_N)\to-\infty$).
• Goal shape. A conjunction of List.TFAE of the three existential conditions with the "in which case" clause. Neither part may be dropped, and the equivalence may not be weakened to one direction or to $\beta>0$.
• Misprints. Two printed formulas are corrected: the Riordan term $(\lambda_N\theta)$ is read as $(\lambda_N/\theta)$, and a parenthesis is restored in the density $f$ on p. 225.
• Infrastructure. Needed: tail bounds for Poisson-type series, a local central limit estimate for the Poisson distribution near its mean, Gaussian tail asymptotics $h(t)\sim t$, and the incomplete gamma function. The Erlang-B asymptotic and the Gaussian facts are reusable for every many-server queue. Solutions to any milestone, and to auxiliary lemmas such as summability of the stationary weights, are welcome.

Selected references

• O. Garnett, A. Mandelbaum, M. Reiman, Designing a call center with impatient customers, Manufacturing & Service Operations Management 4(3), 208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753
• S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 567–587, 1981. https://doi.org/10.1287/opre.29.3.567
• D. L. Jagerman, Some properties of the Erlang loss function, Bell System Technical Journal 53, 1974 (as cited in the paper's reference list).
• P. J. Fleming, A. Stolyar, B. Simon, Heavy traffic limit for a mobile phone system loss model, Proc. 2nd Int. Conf. Telecommunication Systems, Modeling and Analysis, Nashville, 158–176, 1994.