Control Theory Dynamic Programming Operations Research+2·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case IX: Imperfect State Information — Reduction to a Perfect-Information Model through a Statistic Sufficient for ControlTextbook

Motivation

In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.

For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.

Setting

The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space $S$ , control space $C$ and observation space $Z$ ; a discount factor $\alpha>0$ ; a lower semianalytic cost $g:SC\to R^*=[-\infty,\infty]$ ; a Borel state transition kernel $t(dx'\mid x,u)$ ; Borel observation kernels $s_0(dz\mid x)$ and $s(dz\mid u,x)$ ; and a horizon $N$ . The initial state $x_0$ has distribution $p\in P(S)$ , $z_0\sim s_0(\cdot\mid x_0)$ , and then $x_{k+1}\sim t(\cdot\mid x_k,u_k)$ , $z_{k+1}\sim s(\cdot\mid u_k,x_{k+1})$ . The controller knows the information vector $i_k=(z_0,u_0,\dots,u_{k-1},z_k)\in I_k$ and must choose $u_k\in U_k(i_k)$ , where the constraint set $\Gamma_k=\{(i_k,u)\mid u\in U_k(i_k)\}$ is analytic.

A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ consists of universally measurable stochastic kernels $\mu_k(du_k\mid p;i_k)$ that respect the constraints (Definition 10.4). Together with $p$ it determines probability measures $P_k(\pi,p)$ on the histories $(x_0,z_0,u_0,\dots,x_k,z_k,u_k)$ , the cost

J_{N,\pi}(p)=\int\Big[\sum_{k=0}^{N-1}\alpha^k g(x_k,u_k)\Big]dP_{N-1}(\pi,p),

and the optimal cost $J^*_N(p)=\inf_\pi J_{N,\pi}(p)$ (Definition 10.5). Assumption $(F^+)$ asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; $(F^-)$ asks the same of the positive part.

A statistic is a sequence of Borel maps $\eta_k:P(S)I_k\to Y_k$ into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, $\Gamma_k=\{(i_k,u)\mid(\eta_k(p;i_k),u)\in\hat\Gamma_k\}$ with $\hat\Gamma_k$ analytic; (b) the conditional law of $\eta_{k+1}$ given $(\eta_k,u_k)$ is a Borel kernel $\hat t_k(dy_{k+1}\mid y_k,u_k)$ , for every $p$ and every policy; and (c) the conditional expectation of $g(x_k,u_k)$ given $(\eta_k,u_k)$ is a lower semianalytic function $\hat g_k(y_k,u_k)$ . The perfect state information model (PSI) of Definition 10.7 has states $y_k\in Y_k$ , constraints $\hat U_k(y_k)=(\hat\Gamma_k)_{y_k}$ , costs $\hat g_k$ and transitions $\hat t_k$ ; its cost and optimal cost at $y\in Y_0$ are $\hat J_{N,\hat\pi}(y)$ and $\hat J^*_N(y)$ . The initial distribution of $y_0$ is

\varphi(p)(\underline Y_0)=\int_S s_0(\{z_0\mid\eta_0(p;z_0)\in\underline Y_0\}\mid x_0)\,p(dx_0).

A Markov (PSI) policy $\hat\mu_k(du\mid y_k)$ acts in (ISI) through $\mu_k(du\mid p;i_k)=\hat\mu_k(du\mid\eta_k(p;i_k))$ .

Formalization targets

Goal: Proposition 10.3

Under $(F^+,\hat F^+)$ or $(F^-,\hat F^-)$ ,

J^*_N(p)=\int_{Y_0}\hat J^*_N(y_0)\,\varphi(p)(dy_0)\qquad\forall p\in P(S),

and a Markov (PSI) policy that is optimal, $\varphi(p)$ -optimal or weakly $\varphi(p)$ - $\varepsilon$ -optimal for (PSI) is respectively optimal, optimal at $p$ , or $\varepsilon$ -optimal at $p$ for (ISI); under $(F^+,\hat F^+)$ an $\varepsilon$ -optimal (PSI) policy is $\varepsilon$ -optimal for (ISI). Here $\hat\pi$ is weakly $q$ - $\varepsilon$ -optimal if $\int\hat J_{N,\hat\pi}\,dq\le\int\hat J^*_N\,dq+\varepsilon$ when $\int\hat J^*_N\,dq>-\infty$ and $\int\hat J_{N,\hat\pi}\,dq\le-1/\varepsilon$ otherwise, and $q$ -optimal if $q(\{y_0\mid\hat J_{N,\hat\pi}(y_0)=\hat J^*_N(y_0)\})=1$ (Definition 10.8).

Milestones

Lemma 10.1: the process $(\eta_0,u_0,\dots,\eta_k,u_k)$ generated in (ISI) by a Markov (PSI) policy has the law $\hat P_k[\hat\pi,\varphi(p)]$ .
Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$ .
Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$ .
Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
Proposition 10.4: $\varepsilon$ -optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$ .
Proposition 10.6: the identity maps on $P(S)I_k$ form a statistic sufficient for control.

Significance

Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the $\varphi(p)$ -average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of $\varepsilon$ -optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.

These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.

Difficulty

The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair $(p,\pi)$ , while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values $\pm\infty$ , so interchanging sums and integrals requires the finiteness assumptions $(F^\pm)$ and $(\hat F^\pm)$ ; and the inequality $J^*_N\ge\int\hat J^*_N\,d\varphi(p)$ requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.

Formalization scope

Horizon. Only finite horizons $N\ge1$ are covered, hence only the cases $(F^+,\hat F^+)$ and $(F^-,\hat F^-)$ of the book's statements; the infinite-horizon cases $(P,\hat P)$ , $(N,\hat N)$ , $(D,\hat D)$ are out of scope.
Extended reals. Costs live in EReal with the book's convention $\infty-\infty=+\infty$ written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction ( $\top-\top=\bot$ ) is never used where both terms can be infinite.
Spaces and measures. $S$ , $C$ , $Z$ , $Y_k$ are Borel spaces in the sense of Definition 7.7 with their Borel $\sigma$ -algebras; $P(S)$ carries the weak topology and the Giry $\sigma$ -algebra. Policies are families of maps into ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of $\mathbb N$ ; only stages $k<N$ are constrained.
Conditional statements. Conditions (22) and (23) are stated through the defining relations of conditional probability and expectation, for every $p$ and every policy, with (23) required when $g(x_k,u_k)$ is quasi-integrable.
Policies in Proposition 10.3. The (PSI) policies in the optimality transfers are Markov, as in Proposition 10.2.
No trivialization. Definition 10.6 is the full definition: analytic $\hat\Gamma_k$ with full projection, Borel kernels $\hat t_k$ satisfying (22) for every $p$ and policy, and lower semianalytic $\hat g_k$ satisfying (23); a weaker notion would make Proposition 10.6 empty.

Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10 (1965) 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
C. Striebel, Sufficient statistics in the optimum control of stochastic systems, Journal of Mathematical Analysis and Applications 12 (1965) 576–592. https://doi.org/10.1016/0022-247X(65)90027-2
N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9

12 thms2 active usersReviewed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case VII: The Finite-Horizon Borel Model — over Universally Measurable Policies J*_K = T^K(J_0)Textbook

Motivation

Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.

Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).

Setting

A finite horizon stochastic optimal control model is a nine-tuple $(S,C,U,W,p,f,\alpha,g,N)$ . The state space $S$ , control space $C$ and disturbance space $W$ are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint $U(x)\subseteq C$ is nonempty and $\Gamma=\{(x,u)\mid u\in U(x)\}$ is analytic in $S\times C$ . Disturbances are drawn from a Borel stochastic kernel $p(dw\mid x,u)$ , the system moves by $x_{k+1}=f(x_k,u_k,w_k)$ with $f$ Borel, the discount factor $\alpha$ is a positive real, the one-stage cost $g:\Gamma\to[-\infty,\infty]$ is lower semianalytic ( $\{g<c\}$ is analytic for every real $c$ ), and $N\ge1$ is the horizon. The state transition kernel is $t(B\mid x,u)=p(\{w\mid f(x,u,w)\in B\}\mid x,u)$ .

A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ chooses $u_k$ from a universally measurable stochastic kernel $\mu_k(du_k\mid x_0,u_0,\dots,x_k)$ concentrated on $U(x_k)$ ; it is Markov if $\mu_k$ depends on $x_k$ only, and nonrandomized if every $\mu_k(\cdot\mid\cdot)$ is a point mass. $\Pi'$ denotes all policies and $\Pi$ the Markov ones. A policy and an initial distribution $p$ determine a probability measure $r_N(\pi,p)$ on state–control paths, and the $K$ -stage cost and optimal cost are

J_{K,\pi}(x)=\int\Big[\sum_{k=0}^{K-1}\alpha^k g(x_k,u_k)\Big]dr_N(\pi,p_x),\qquad J^*_K(x)=\inf_{\pi\in\Pi'}J_{K,\pi}(x).

Assumption (F⁺) requires $\int g^-\,dq_k(\pi,p_x)<\infty$ , and (F⁻) requires $\int g^+\,dq_k(\pi,p_x)<\infty$ , for every policy, initial state and stage, where $q_k$ is the marginal of $r_N$ on the $k$ -th pair. The DP operators are

T_\mu(J)(x)=\int_C\Big[g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big]\mu(du\mid x),\qquad T(J)(x)=\inf_{u\in U(x)}\Big\{g(x,u)+\alpha\!\int_S J\,dt(\cdot\mid x,u)\Big\}.

Formalization targets

Goal: Proposition 8.2

J^*_K=T^K(J_0),\qquad K=1,\dots,N,

under (F⁺) or (F⁻), where $J_0\equiv0$ . The goal leaves the horizon, the discount factor and the sign of $g$ unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.

Milestones

In attack order: Lemma 8.1 (the cost of a Markov policy equals $T_{\mu_0}\cdots T_{\mu_{K-1}}(J_0)$ ), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of $T$ ), Lemma 8.3 (under (F⁺), $T^K(J_0)>-\infty$ ), Lemma 8.4 (monotone and bounded convergence for $T_\mu$ ). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ( $J^*_K$ is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).

Significance

Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.

All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention $\infty-\infty=\infty$ .

Difficulty

The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on $K$ , choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and $T(J)$ is generally not Borel even when $J$ and $g$ are; Borel policies are too few for $\varepsilon$ -optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.

Formalization scope

Lean conventions:

Spaces carry [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.
Extended reals are EReal. Addition inside costs and integrands uses the book's convention $-\infty+\infty=+\infty$ (badd), not Mathlib's, which gives $\bot+\top=\bot$ . Integrals are $\int f^+-\int f^-$ with $\infty-\infty=\infty$ (extInt).
The universal σ-algebra is the intersection of all completions (universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).
The integral against $r_N(\pi,p)$ is the iterated integral of Eq. (4) of Chapter 8 (pathInt).
Stages are indexed $0,\dots,N-1$ , and a history is $k$ state–control pairs plus the current state.
$g$ is stored on $S\times C$ , but only its values on $\Gamma$ are constrained or used.

A trivializing formalization is excluded by construction. $J^*_K$ is the infimum over all policies in $\Pi'$ , not over Markov or nonrandomized ones. $J_{K,\pi}$ is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.

A complete development needs:

the analytic-set and universal-measurability theory of §7.6–7.7: closure of analytic sets under projections and sections, measurability of integrals against universally measurable kernels (Proposition 7.46), and the selection theorem (Proposition 7.50);
extended-real integration lemmas in the style of Lemma 7.11.

This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Chapter 8. https://web.mit.edu/dimitrib/www/soc.html
D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Ann. Probab. 2 (1974), 926–941. https://doi.org/10.1214/aop/1176996558
S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Math. Oper. Res. 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15

14 thms2 active usersReviewed

Completed

Combinatorics Markov Chain Operations Research+1·Captain: mikedeng1

Reversibility and Stochastic Networks VI: The Ewens Sampling Distribution Is Consistent Under Sampling Without ReplacementTextbook

Motivation

The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.

Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.

Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.

Setting

A population consists of $M\ge2$ individuals, each carrying an allelic type. Its description is $\mathbf M=(M_1,\dots,M_M)$ , where $M_i$ is the number of allelic types carried by exactly $i$ individuals, so that

\sum_{i=1}^{M} iM_i=M. \qquad (7.3)

For a real parameter $\nu>0$ , the Ewens distribution on descriptions is

\pi_M(\mathbf M)=\binom{\nu+M-1}{M}^{-1}\prod_{i=1}^{M}\Big(\frac{\nu}{i}\Big)^{M_i}\frac{1}{M_i!}, \qquad (7.6)

where $\binom{x}{k}=x(x-1)\cdots(x-k+1)/k!$ is the binomial coefficient for real $x$ . In the infinite alleles model, individuals die at rate $\mu$ , each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability $u$ ; then (7.6) is the equilibrium distribution with $\nu=(M-1)u/(1-u)$ (7.5).

A random sample of size $1\le m\le M$ without replacement is a uniformly random $m$ -element subset of the $M$ labelled individuals, each of the $\binom Mm$ subsets being equally likely; the sample has a description in the same sense.

The number $j$ of individuals carrying one given allele performs a random walk on $\{0,\dots,M\}$ with intensities

q(j,j-1)=\mu\frac jM\Big(\frac{M-j}{M-1}+\frac{j-1}{M-1}u\Big),\qquad q(j,j+1)=\mu\frac{M-j}{M}\frac{j}{M-1}(1-u). \qquad (7.8)

An allele is quasi-fixed when it is the only allele present ( $j=M$ ).

Formalization targets

Goal: consistency under sampling (Theorem 7.1)

If $M\ge2$ and the population description is distributed as $\pi_M$ , then a random sample of size $1\le m\le M$ drawn without replacement has description $\mathbf m$ with probability $\pi_m(\mathbf m)$ , the same $\nu$ being used for both sizes:

\sum_{\mathbf M}\pi_M(\mathbf M)\,P\big(\text{sample has description }\mathbf m\mid\text{population has description }\mathbf M\big)=\pi_m(\mathbf m).

Milestones

(7.6) is a distribution: $\pi_M(\mathbf M)>0$ and $\sum_{\mathbf M}\pi_M(\mathbf M)=1$ (Exercise 7.1.3).
Theorem 7.1 for $m=M-1$ , the case the book's proof establishes first.
Corollary 7.5, the identity of its proof: the probability that a uniformly chosen individual's allele is carried by exactly $i$ individuals is

\sum_{\mathbf M}\frac{iM_i}{M}\pi_M(\mathbf M)=\frac{\nu}{M}\binom{\nu+M-1}{i}^{-1}\binom Mi. \qquad (7.9)

Theorem 7.9: the probability $Q$ that the walk (7.8) started at $1$ reaches $M$ before $0$ satisfies

Q^{-1}=\sum_{i=0}^{M-1}\binom{M-1}{i}^{-1}\binom{\nu+M-1}{i}.

Significance

The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on $\nu$ . Kelly deduces from it the sufficiency of the number of alleles in a sample for $\nu$ and the heterozygosity $\nu/(\nu+1)$ (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).

Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.

Difficulty

The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between $M-1$ and $M$ , a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives $\pi_{M-1}$ and $\pi_M$ . Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of $m$ -subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.

Formalization scope

Descriptions of $n$ individuals are integer partitions Nat.Partition n, with $M_i$ the multiplicity of the part $i$ ; the product in (7.6) runs over $i=1,\dots,n$ . The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.
The population is Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is $\binom Mm^{-1}$ times the number of $m$ -subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.
The goal and Corollary 7.5 quantify over an arbitrary choice of labelling for each population description. They assume $M\ge2$ , as required by the chapter's rule that a parent is chosen among the other $M-1$ individuals; the goal also assumes $1\le m\le M$ . Because $\pi_M>0$ , this forces the conditional sampling law to depend on the population only through its description. Types are natural numbers, so every description is realized and the hypothesis is never vacuous.
The quasi-fixation probability is defined through the jump chain of (7.8): the limit of the probabilities of reaching $M$ within $n$ jumps without reaching $0$ . The theorem assumes $M\ge2$ , $\mu>0$ , $0<u<1$ and $\nu=(M-1)u/(1-u)$ .
Corollary 7.5 is formalized as the identity of its proof. The identification of the oldest allele's frequency with that of a randomly chosen individual uses allele ages and the reversibility of the labelled process (Theorem 7.2) and is not formalized. Theorem 7.2 itself, whose state space orders the allele labels within each class, and the allele-age results (Corollaries 7.3, 7.4, 7.7, 7.8, Theorem 7.6, Corollary 7.10, Theorem 7.11) are not part of the mission.

Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity $(1-x)^{-\nu}=\prod_j e^{\nu x^j/j}$ ) are reusable beyond this mission.

Selected references

F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 7. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
W. J. Ewens, The sampling theory of selectively neutral alleles, Theoretical Population Biology 3 (1972), 87–112. https://doi.org/10.1016/0040-5809(72)90035-4
J. F. C. Kingman, The representation of partition structures, Journal of the London Mathematical Society (2) 18 (1978), 374–380. https://doi.org/10.1112/jlms/s2-18.2.374
M. Kimura and J. F. Crow, The number of alleles that can be maintained in a finite population, Genetics 49 (1964), 725–738. https://doi.org/10.1093/genetics/49.4.725

9 thms2 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Stochastic Inventory Control Models 1: The Dual-Balancing Policy Costs at Most Twice the OptimumResearch Paper

Motivation

Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.

Setting

There are $T$ periods $t = 1, \dots, T$ and a known lead time $L \ge 0$ : an order placed in period $t$ arrives in period $t + L$ . Period $t$ has a per-unit holding cost $h_t \ge 0$ and a per-unit backlogging penalty $p_t \ge 0$ . Ordering costs are zero ( $c_t = 0$ ), which is the standing assumption of the paper's §4. The initial data are the net inventory $ni_0$ and the pipeline orders $q_{1-L}, \dots, q_0 \ge 0$ .

Demands $D_1, \dots, D_T$ are nonnegative random variables on a probability space with a filtration $(\mathcal F_t)$ ; $\mathcal F_t$ is the information at the beginning of period $t$ , and $D_t$ is $\mathcal F_{t+1}$ -measurable. A feasible policy $P$ places orders $Q^P_t \ge 0$ that are $\mathcal F_t$ -measurable. Write $D_{[s,t]} = \sum_{j=s}^t D_j$ (with $D_j = 0$ for $j \le 0$ ), $X_t = ni_0 + \sum_{j=1-L}^{t-1} Q_j - D_{[1,t-1]}$ for the inventory position before ordering and $Y_t = X_t + Q_t$ after ordering.

The marginal holding cost of period $t$ is the holding cost that the units ordered in $t$ incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:

H^P_t = \sum_{j=t+L}^{T} h_j\,\bigl(Q^P_t - (D_{[t,j]} - X^P_t)^+\bigr)^+, \qquad \Pi^P_t = p_{t+L}\,\bigl(D_{[t,t+L]} - Y^P_t\bigr)^+ .

The cost of $P$ is $\mathcal C(P) = \sum_{t=1}^{T-L}(H^P_t + \Pi^P_t)$ ; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.

A dual-balancing policy $B$ orders nothing after period $T - L$ , and in each period $t \le T - L$ orders the quantity that balances the two conditional expected marginal costs:

E\bigl[H^B_t \mid \mathcal F_t\bigr] = E\bigl[\Pi^B_t \mid \mathcal F_t\bigr] \quad\text{almost surely.}

Formalization targets

Goal: Theorem 4.1

For every dual-balancing policy $B$ and every feasible policy $P$ ,

E[\mathcal C(B)] \;\le\; 2\,E[\mathcal C(P)] .

The paper writes $P = OPT$ ; quantifying over all feasible $P$ is the same statement whenever an optimum exists and needs no existence assumption.

Milestones

Lemma 4.1. $E[\mathcal C(B)] = 2\sum_{t=1}^{T-L}E[Z_t]$ with $Z_t = E[H^B_t \mid \mathcal F_t]$ .
Lemma 4.2. With $\mathcal T_H = \{t : Y^B_t < Y^P_t\}$ , $\sum_{t\in\mathcal T_H} H^B_t \le \sum_{t=1}^{T-L} H^P_t$ on every realization.
Lemma 4.3. With $\mathcal T_\Pi = \{t : Y^B_t \ge Y^P_t\}$ , $\sum_{t\in\mathcal T_\Pi} \Pi^B_t \le \sum_{t=1}^{T-L} \Pi^P_t$ on every realization.

Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals $\sum_{t=1-L}^{0}\Pi_t + H_{(-\infty,0]} + \sum_{t=1}^{T-L}(H_t + \Pi_t)$ , which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when $h_T > 0$ and the demands are integrable, so the goal is not about an empty class.

Significance

The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.

Difficulty

The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets $\mathcal T_H$ and $\mathcal T_\Pi$ to be determined by the information of period $t$ , so that conditioning on $\mathcal F_t$ commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.

Formalization scope

Periods are integers (ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods $1, \dots, T$ are read, and the pipeline $q_t$ is substituted for $t \le 0$ .
Ordering costs are $c_t = 0$ and there is no discounting, as in the paper's §4; the reduction of §4.6 from general instances is not formalized. The lead time $L$ is general.
Information is an arbitrary Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.
Expected costs are lower Lebesgue integrals in $[0,\infty]$ , so an infinite expected cost is never read as $0$ .
The balancing condition carries integrability of $H^B_t$ and $\Pi^B_t$ , so a conditional expectation of a non-integrable cost (which Mathlib sets to $0$ ) cannot satisfy it vacuously. The existence item rules out an empty policy class.
Lemmas 4.2 and 4.3 are pathwise and do not use the balancing rule. The comparator totals are the marginal totals of Eq. (4), which is the stronger reading.
Eq. (2) prints $X_{t+L}$ and its restatement on p. 292 prints $p_t$ ; both are typos, and the formalization uses $X_t$ and $p_{t+L}$ .

A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded $\mathcal F_t$ -measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.

Selected references

R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. doi:10.1287/moor.1060.0205
D. C. Heath, P. L. Jackson, Modeling the evolution of demand forecasts with application to safety stock analysis in production/distribution systems, IIE Transactions 26(3):17–30, 1994. doi:10.1080/07408179408966604
P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000. ISBN 978-0-256-11379-7.

6 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information 2: Without Shared Demand Information the Bullwhip Bound Is MultiplicativeResearch Paper

Motivation

The bullwhip effect is the observation that the variability of orders grows as one moves up a supply chain, from the retailer to the wholesaler, the distributor and the factory, even when customer demand is stable. It was documented in industry practice by Lee, Padmanabhan and Whang (Management Science, 1997), who identified demand forecasting as one of its main causes. Amplified order variability raises the safety stock, capacity and transportation costs of every upstream firm, so the question of how large the effect is, and what reduces it, is central to supply chain management.

Chen, Drezner, Ryan and Simchi-Levi (Management Science 46(3), 2000) quantified the effect for a retailer that forecasts with a moving average and follows an order-up-to policy. Their §3 asks whether sharing customer demand information with every stage removes the effect. Theorem 3.1 (the companion mission of this series) shows that it does not; Theorem 3.2, the goal of this mission, gives the lower bound for the chain in which no demand information is shared.

Setting

Time is indexed by the integers $t \in \mathbb Z$ . The retailer faces i.i.d. demand

D_t = \mu + \epsilon_t,

where the error terms $\epsilon_t$ are independent and identically distributed from a symmetric distribution with mean $0$ and variance $\sigma^2 > 0$ .

Single-stage policy (§2). With $p \ge 1$ observations, a lead time $L$ , a safety factor $z$ and a constant $C_{L,\rho}$ , the retailer forms the moving-average estimates

\hat D^L_t = L\,\frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat\sigma^L_{et} = C_{L,\rho}\sqrt{\frac{\sum_{i=1}^p e_{t-i}^2}{p}}, \qquad e_t = D_t - \hat D^1_t,

raises its inventory position to the order-up-to point $y_t = \hat D^L_t + z\hat\sigma^L_{et}$ , and so orders $q_t = y_t - y_{t-1} + D_{t-1}$ . Orders may be negative: excess inventory is returned without cost.

Decentralized chain (§3). Stages $k = 1, 2, \dots$ form a serial chain; stage 1 is the retailer, and $L_k$ is the lead time between stages $k$ and $k+1$ . No stage sees customer demand except the retailer. Stage $k$ forecasts from the orders it receives,

\hat D^{(1)}_t = \frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat D^{(k)}_t = \frac{\sum_{j=0}^{p-1} q^{k-1}_{t-j}}{p} \quad (k \ge 2),

uses the order-up-to point $y^k_t = L_k\hat D^{(k)}_t$ , and orders

q^1_t = y^1_t - y^1_{t-1} + D_{t-1}, \qquad q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t \quad (k \ge 2).

Formalization targets

Goal: Theorem 3.2 (Eq. (7))

For every stage $k \ge 1$ and every period $t$ ,

\frac{\operatorname{Var}(q^k_t)}{\operatorname{Var}(D_t)} \;\ge\; \prod_{i=1}^{k}\left(1 + \frac{2L_i}{p} + \frac{2L_i^2}{p^2}\right).

The bound is the paper's, with its explicit constants. The paper asserts no tightness for this theorem, and none is claimed.

Milestone: Eq. (6)

For the single-stage policy with any safety factor $z$ and any constant $C_{L,\rho}$ ,

\frac{\operatorname{Var}(q_t)}{\operatorname{Var}(D_t)} \;\ge\; 1 + \frac{2L}{p} + \frac{2L^2}{p^2}.

This is the i.i.d. case $\rho = 0$ of the paper's Theorem 2.2. With $z = 0$ and $L = L_1$ the single-stage orders are the stage-1 orders of the chain, so Eq. (6) contains the case $k = 1$ of the goal.

Significance

The result. Theorem 3.2 is half of the paper's comparison between centralized and decentralized information. When demand information is shared, the amplification from the retailer to stage $k$ in the i.i.d. case equals $1 + 2(\sum_{i\le k}L_i)/p + 2(\sum_{i\le k}L_i)^2/p^2$ (Eq. (8)), which grows additively in the lead times. Without sharing, the lower bound (7) is a product over stages and grows multiplicatively. The paper concludes that centralizing demand information "can significantly reduce the bullwhip effect", and that the gap widens as one moves up the chain. Eq. (6) is the single-stage statement that forecasting with a moving average alone already amplifies variability, by a factor depending only on the ratio $L/p$ .

Formalizing it. The paper gives no proof of Theorem 3.2; it refers to Ryan (1997, PhD thesis) and to Chen et al. (1998). A machine-checked proof would therefore supply the first self-contained, verified argument for the multiplicative bound. The Gaussian special case of Eq. (6) is already formalized on Prove2Me, in the Snyder–Shen chapter on the bullwhip effect (SupplyChainTheory.bullwhip_signal_processing at $\rho = 0$ ); that statement assumes Gaussian errors, whereas this mission assumes only symmetry, mean $0$ and variance $\sigma^2$ . Neither the multistage bound nor the symmetric-error version of Eq. (6) has a formal proof.

Difficulty

The natural first idea is induction on the stage: treat the orders of stage $k-1$ as the demand of stage $k$ and apply the single-stage bound. That step fails, because the single-stage bound is a statement about i.i.d. demand, and the orders reaching stage $k \ge 2$ are not i.i.d.: they are autocorrelated, and stage $k$ 's moving average of those orders interacts with the correlation in a way that can raise or lower the variance. Whether the product bound survives depends on controlling that interaction at every stage. For Eq. (6), the safety-stock term $z\hat\sigma^L_{et}$ is a nonlinear function of the demands, and only symmetry of the errors, not normality, is available to control its interaction with the linear part of the order.

Formalization scope

All objects live in the namespace ChenBullwhip.Decentralized.

IIDDemand P is the demand model on a probability space $(\Omega, P)$ : a constant mu, sigma > 0, and errors eps : ℤ → Ω → ℝ that are measurable, mutually independent (iIndepFun), identically distributed, symmetric (eps t and -eps t have the same law), in $L^2$ , with mean $0$ and variance sigma ^ 2. Demand is D t = mu + eps t. Variances are Mathlib's ProbabilityTheory.variance.
SingleStage defines $\hat D^L_t$ , $e_t$ , $\hat\sigma^L_{et}$ , $y_t$ and $q_t$ of §2; $C_{L,\rho}$ is a free real parameter, as the paper does not fix it.
Chain defines the forecasts $\hat D^{(k)}_t$ and the orders $q^k_t$ by recursion on the stage, with the convention $q^0_t = D_{t-1}$ , so that stage 1 orders $y^1_t - y^1_{t-1} + D_{t-1}$ . The recursion $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$ is not printed in the paper; it is the §2.2 order identity applied to a stage whose incoming demand is $q^{k-1}_t$ , as the sequence of events on p. 440 describes.

Disclosed hypotheses not on the page: $p \ge 1$ (a moving average needs an observation), $\sigma > 0$ (the paper divides by $\operatorname{Var}(D) = \sigma^2$ ), and square-integrable errors (Mathlib's variance is $0$ off $L^2$ ). The paper's model (1) asks $\mu \ge 0$ ; since $\mu$ affects no variance, no sign condition is imposed. Lead times are natural numbers. The statements hold in every period $t$ , with no stationarity hypothesis.

Trivializing formalizations are excluded: the orders are computed from the demands, not posited processes with a given covariance; the variances are genuine because every random variable involved is square integrable; and the ratio's denominator is $\sigma^2 > 0$ .

A complete development needs variance and covariance calculus for finite linear combinations of independent $L^2$ variables, and, for Eq. (6), the vanishing of the covariance between an odd and an even function of a symmetric random vector. Both are reusable well beyond this mission. Proofs of either target, and general lemmas on variances of linear filters of i.i.d. sequences, are welcome.

Selected references

F. Chen, Z. Drezner, J. K. Ryan, D. Simchi-Levi, Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information, Management Science 46(3):436–443, 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
H. L. Lee, V. Padmanabhan, S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546
J. K. Ryan, Analysis of Inventory Models with Limited Demand Information, Ph.D. dissertation, Department of Industrial Engineering and Management Science, Northwestern University, 1997.
L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13 (formalized on Prove2Me as SupplyChainTheory.*).

5 thms2 active usersReviewed

Markov Chain Operations Research Probability·Captain: mikedeng1

On the Stochastic Matrices Associated with Certain Queuing Processes 1: The M/G/1 Imbedded Chain Is Ergodic iff ρ < 1 and Recurrent iff ρ ≤ 1Research Paper

Motivation

Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?

F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on $\{0,1,2,\dots\}$ , stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.

Timeline:

1951–1953, Kendall. Introduces the imbedded chains of M/G/1 and GI/M/1 and obtains most of their classification by direct methods.
1953, Foster. Derives the classification from general criteria: Theorem 2 (ergodicity), Theorems 4–6 (transience and recurrence).
1950s onward. The criteria become the standard tools (Feller's text; later the drift conditions of Meyn and Tweedie).

Setting

A Markov chain on the states $\{0,1,2,\dots\}$ is given by a transition matrix $P=[p_{ij}]$ : $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every row $i$ . Write $f_{ij}^{(n)}$ for the probability that the chain started in $i$ first reaches $j$ (for $i=j$ , first returns to $j$ ) at step $n\ge1$ . The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor $1$ . A state $j$ is recurrent if $f_{jj}=\sum_n f_{jj}^{(n)}=1$ and transient if $f_{jj}<1$ ; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time $\sum_n n f_{jj}^{(n)}$ is finite. The mean first-passage time from $i$ to $j$ is $\mu_{ij}=\sum_{n\ge1} n f_{ij}^{(n)}\in[0,\infty]$ .

The M/G/1 matrix is built from a sequence $k_0,k_1,\dots$ of positive numbers summing to one ( $k_n$ is the probability of $n$ arrivals during one service):

[p_{ij}] = \begin{bmatrix} k_0 & k_1 & k_2 & \cdots \\ k_0 & k_1 & k_2 & \cdots \\ 0 & k_0 & k_1 & \cdots \\ 0 & 0 & k_0 & \cdots \\ \vdots & \vdots & \vdots & \end{bmatrix},

that is, $p_{0j}=k_j$ and, for $i\ge1$ , $p_{ij}=k_{j-i+1}$ when $j\ge i-1$ and $0$ otherwise. The traffic intensity is

\rho=\sum_{n=1}^{\infty}n\,k_n\in[0,\infty],

the mean number of arrivals per service.

Formalization targets

Goal: the M/G/1 classification (§3, p. 358)

\text{the chain is ergodic}\iff\rho<1,\qquad\text{the chain is recurrent}\iff\rho\le1 .

The goal leaves $k$ arbitrary apart from positivity and normalization; in particular $\rho=\infty$ is allowed and falls in the transient case.

Milestones (the paper's general theorems and the step of §3 they feed)

Theorem 2 (drift criterion): a nonnegative solution of $\sum_j p_{ij}y_j\le y_i-1$ ( $i\ne0$ ) with $\sum_j p_{0j}y_j<\infty$ makes the system ergodic. Already posed on the platform and referenced here.
Theorem 3: in an ergodic system the mean first-passage times $d_j=\mu_{j0}$ are finite and satisfy $\sum_{j\ge1}p_{ij}d_j=d_i-1$ ( $i\ne0$ ), $\sum_{j\ge1}p_{0j}d_j<\infty$ .
§3 display: for the ergodic M/G/1 chain, $\mu_{i,i-1}=\mu_{10}$ and $\mu_{i0}=i\mu_{10}$ ( $i\ne0$ ).
Theorem 5: a solution of $\sum_j p_{ij}y_j\le y_i$ ( $i\ne0$ ) with $y_i\to\infty$ makes the system recurrent.
Theorem 7: for a probability distribution $\{p_n\}$ with $p_0>0$ , $\sum_n z^np_n=z$ has a root in $(0,1)$ iff $\sum_{n\ge1}np_n>1$ .
Theorem 4: the system is transient iff $\sum_j p_{ij}y_j=y_i$ ( $i\ne0$ ) has a bounded nonconstant solution.

Significance

The result. The classification is the stability theorem for the M/G/1 queue: for $\rho<1$ the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for $\rho=1$ the queue empties infinitely often but has no steady state; for $\rho>1$ it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.

Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.

Difficulty

The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the $n$ -step probabilities $p_{ij}^{(n)}$ and of hitting probabilities of state $0$ , none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic $\Rightarrow\rho<1$ , recurrent $\Rightarrow\rho\le1$ ) need exact identities for mean first-passage times, not just bounds, and these must be handled in $[0,\infty]$ because the means may be infinite. And the boundary case $\rho=1$ (null recurrence) separates the two equivalences: an argument that only compares the mean drift $\rho-1$ with $0$ , such as a law of large numbers for the increments, cannot tell recurrence from transience there.

Formalization scope

The chain is the published QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to $1$ as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.
States are indexed from $0$ , as in the paper; " $i\ne0$ " is i ≠ 0.
The M/G/1 matrix is a function mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for $k_i=2^{-(i+1)}$ ).
$\sum_n k_n=1$ is added as the meaning of "stochastic matrix"; §3 writes only $k_i>0$ .
$\rho$ and all mean first-passage times are extended nonnegative reals ( $[0,\infty]$ ), so divergent means are $\infty$ , never $0$ . Theorem 7's mean is also taken in $[0,\infty]$ .
Recurrent means $f_{jj}=1$ for every state $j$ ; transient means $f_{jj}<1$ for every state. For irreducible chains these are complementary, which is a theorem, not a definition.
The general Theorems 3, 4 and 5 assume irreducibility and aperiodicity, the paper's standing assumption of §1. The goal does not assume them: they follow from $k_i>0$ .
Every series in a hypothesis carries its convergence (Summable or HasSum); Theorem 3's equation (6) is written as $d_i=1+\sum_{j\ge1}p_{ij}d_j$ in $[0,\infty]$ together with finiteness of the $d_j$ , $j\ne0$ .
Theorem 7's distribution is renamed $q$ in Lean to avoid a clash with $p_{ij}$ . Theorem 1 of the paper (§2) and Theorem 6 are not targets of this mission.

Ruled out: $\rho$ as a real tsum (which is $0$ for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix $P$ that need not exist.

Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem $p_{ij}^{(n)}\to\pi_j$ for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.

Selected references

F. G. Foster, On the stochastic matrices associated with certain queuing processes, The Annals of Mathematical Statistics 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
D. G. Kendall, Some problems in the theory of queues, Journal of the Royal Statistical Society B 13(2), 151–185, 1951. https://doi.org/10.1111/j.2517-6161.1951.tb00093.x
D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, The Annals of Mathematical Statistics 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, Wiley, 1950.
S. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511626630

9 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Dimensioning Large Call Centers IV: Asymptotically Optimal Staffing under a Waiting-Cost ConstraintResearch Paper

Motivation

A call center has to decide how many agents to staff. In practice the decision is often posed as a service-level constraint rather than a cost trade-off: use the fewest agents for which the expected waiting cost, or the fraction of customers who wait, stays below a target. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; journal version in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) treat this constraint problem in Section 8 of their paper, alongside the cost-minimization problem of Sections 5–7, and show that a simple square-root staffing rule solves it asymptotically as the arrival rate grows.

The rule matters because it is what practitioners use. Under the classical Erlang-C model, the exact optimum requires evaluating the Erlang-C formula over many staffing levels. The asymptotic rule replaces this with a single equation in the Halfin–Whitt function $P$ : when the target is a delay probability $\varepsilon$ (Example 8.5 of the paper), it reduces to staffing $\lambda/\mu + P^{-1}(\varepsilon)\sqrt{\lambda/\mu}$ servers.

Timeline. Erlang's formula for the M/M/N delay probability dates from 1917. Halfin and Whitt (Operations Research 29, 1981) identified the limit $P(x)$ of the delay probability under square-root staffing $N = \lambda/\mu + x\sqrt{\lambda/\mu}$ with integer $N$ . Jagers and Van Doorn (Operations Research Letters 5, 1986; SIAM Review 33, 1991) studied the continued Erlang loss and delay functions at non-integer numbers of servers, including their convexity, which is what lets the staffing problem be relaxed to a continuous one. Borst, Mandelbaum and Reiman (2000/2004) used these to prove asymptotic optimality of square-root rules for both the cost and the constraint formulations.

Setting

Customers arrive at rate $\lambda$ to $N$ identical servers, each with service rate $\mu > 0$ ; $\mu$ is fixed while $\lambda \to \infty$ . Stability requires $N > \lambda/\mu$ . A customer who waits $t$ time units costs $D_\lambda(t)$ , where $D_\lambda(0) = 0$ , $D_\lambda$ is strictly increasing on $[0,\infty)$ and $\int_0^\infty D_\lambda(t)e^{-\theta t}\,dt < \infty$ for all $\theta > 0$ .

The Erlang-C probability of waiting is

\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Big\}^{-1},

and the conditional waiting cost is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$ . The waiting cost per unit time with $N$ servers is

K(N,\lambda) = \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda).

Given a target $M_\lambda > 0$ , the optimal staffing level is the least integer $N > \lambda/\mu$ with $K(N,\lambda) \le M_\lambda$ ; call it $N^*_\lambda$ .

In the continuous parametrization $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ , define $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$ , the continuous Erlang-C function $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$ , and $K_\lambda(x) = \pi_\lambda(x)G_\lambda(x)$ . The Halfin–Whitt function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. A staffing function $x_\lambda > 0$ is judged by the rounding gap

T_\lambda(x) = \min\big\{|K(\lfloor N_\lambda(x)\rfloor,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - K(N^*_\lambda,\lambda)|\big\}.

It is asymptotically optimal when $T_\lambda(x_\lambda)/M_\lambda \to 0$ as $\lambda\to\infty$ .

Formalization targets

Goal: Theorem 8.2 (rationalized regime)

Suppose that for some $\kappa > 0$ and $\gamma \in (0,\infty)$ , $G_\lambda(\kappa)/M_\lambda \to \gamma$ , i.e. the waiting cost is comparable to the target. Let $y^*_\lambda > 0$ solve $P(y)G_\lambda(y) = M_\lambda$ . Then

\lim_{\lambda\to\infty}\frac{T_\lambda(y^*_\lambda)}{M_\lambda} = 0.

Supporting milestones

Lemma C.1: $G_\lambda$ is strictly convex and decreasing on $(0,\infty)$ .
Section 3: $\pi_\lambda(x) = \pi(N_\lambda(x),\lambda/\mu)$ when $N_\lambda(x)$ is an integer.
Lemma 8.1: if $z^*_\lambda > 0$ solves $\hat\pi_\lambda(z)\hat G_\lambda(z) = M_\lambda$ and $K_\lambda(z^*_\lambda)/(\hat\pi_\lambda\hat G_\lambda)(z^*_\lambda) \to 1$ , then $T_\lambda(z^*_\lambda)/M_\lambda \to 0$ .
Lemma B.1: $P$ is strictly convex and decreasing on $(0,\infty)$ .
Eq. (17): $\limsup a_\lambda/b = \infty$ implies $\liminf P(a_\lambda)/P(b) = 0$ and $\liminf \pi_\lambda(a_\lambda)/\pi_\lambda(b) = 0$ .
Lemma 4.1 (Halfin–Whitt): for bounded $x_\lambda > 0$ , $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$ ; with $x_\lambda \to x$ , $\pi_\lambda(x_\lambda)/P(x)\to 1$ .

Further target: Theorem 8.6 (efficiency-driven regime)

If $G_\lambda(\kappa)/M_\lambda \to 0$ for every $\kappa > 0$ and $y^*_\lambda > 0$ solves $G_\lambda(y) = M_\lambda$ , then $T_\lambda(y^*_\lambda)/M_\lambda \to 0$ .

Significance

The theorem certifies the staffing rule used in workforce-management practice: the excess staffing is determined by one scalar equation involving the Gaussian function $P$ and the scaled waiting cost, and rounding the resulting staffing level misses the constraint by a vanishing fraction of the target. Lemma 8.1 is a reusable framework: any approximation $\hat\pi_\lambda\hat G_\lambda$ that is asymptotically exact at the proposed staffing level yields an asymptotically optimal rule, and the paper instantiates it in three regimes (Theorems 8.2, 8.6, 8.9).

The results are proved on paper. To the best of current knowledge none of them, nor the Halfin–Whitt limit for the continuous Erlang-C extension, has a machine-checked proof. A formalization would produce the first verified heavy-traffic limit of the Erlang-C delay probability, a verified continuous Erlang-C extension with its integer identity, and the convexity facts about $P$ and $G_\lambda$ that many staffing papers cite without proof.

Difficulty

The obvious argument is to quote Halfin and Whitt: the delay probability converges to $P(x)$ under square-root staffing, so $P$ can replace the Erlang-C formula. That limit, as published in 1981, is about integer server counts along sequences with a convergent excess-staffing parameter. The paper needs it for the continuous function $H$ at non-integer server counts and for staffing functions that are merely bounded, and it also needs the identity $H(N,\nu) = \pi(N,\nu)$ at integers and the monotonicity of $\pi_\lambda$ in $x$ , both cited from Jagers and Van Doorn rather than proved. None of these is in Mathlib. A second obstacle is that the staffing function $y^*_\lambda$ is defined only implicitly by an equation involving $G_\lambda$ , which depends on the arbitrary cost functions $D_\lambda$ ; nothing a priori prevents it from escaping to infinity, outside the range where the Halfin–Whitt approximation applies. Finally, $T_\lambda$ compares integer-level costs given by the Erlang-C formula with a continuous approximation, so both representations of the delay probability are in play at once.

Formalization scope

The queue itself is not formalized: there is no Markov chain and no waiting-time distribution. Every statement is about the closed-form waiting cost $K(N,\lambda)$ with $\pi$ given by the Erlang-C formula, exactly as the paper's analysis is. Conventions, all in the namespace DimCallCenters.Constraint:

lam : ℝ is the arrival rate (λ is a Lean keyword); limits are Filter.atTop in lam, with μ fixed. Objects indexed by λ ( $M_\lambda$ , $N^*_\lambda$ , $y^*_\lambda$ ) are functions of lam constrained only for lam > 0.
WaitModel packages μ > 0 and $D_\lambda$ with $D_\lambda(0) = 0$ , strict monotonicity on $[0,\infty)$ , and integrability of $D_\lambda(t)e^{-\theta t}$ on $(0,\infty)$ for θ > 0 (the paper's finiteness of $G$ ; integrability is required because Lean's integral of a non-integrable function is 0).
$N^*_\lambda$ is a function Nstar : ℝ → ℕ given with its two defining properties (feasible; below every feasible integer level above λ/μ). $y^*_\lambda$ and $z^*_\lambda$ are any positive solutions of their equations; existence and uniqueness are not hypotheses.
In $T_\lambda$ the round-down term is dropped when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ (an unstable level where $K$ is undefined). This can only enlarge $T_\lambda$ .
Asymptotic relations are limits of ratios. $\limsup = \infty$ and $\liminf = 0$ are stated with ∃ᶠ ("frequently"), $\limsup < \infty$ as eventual boundedness.
$P$ is defined through explicit $\phi$ , $\Phi$ , $h$ ; the formula also gives $P(0) = 1$ , used in Lemma 4.1(2) at $x = 0$ .
No hypothesis $\lim_{N\downarrow\lambda/\mu}G(N,\lambda) = \infty$ is added: it is not needed for the statements here.

A trivializing formalization is ruled out: $T_\lambda$ keeps all of the paper's terms and is never replaced by a smaller quantity, and the hypotheses are jointly satisfiable — $D_\lambda(t) = a\sqrt{\lambda/\mu}\,t$ with $M_\lambda = M\lambda$ satisfies (33) for every $\kappa$ with $\gamma = a/(\mu\kappa M)$ .

Infrastructure needed: the continuous Erlang-C function and its integer identity; the Halfin–Whitt limit (a Gaussian approximation of Poisson/gamma tails); calculus facts about the normal hazard rate. These are reusable beyond this mission, notably by the sibling missions on the cost-minimization problem. Example 8.5 (delay-probability target with $D_\lambda = 1_{t>0}$ ) motivates the rule but violates the strict monotonicity of $D_\lambda$ , so it is not an instance of the theorem as stated. Contributions on any milestone, and on Theorem 8.9 (quality-driven regime, which needs Lemma 4.2), are welcome.

Selected references

S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
A. A. Jagers, E. A. Van Doorn, On the Continued Erlang Loss Function, Operations Research Letters 5:43–46, 1986.
A. A. Jagers, E. A. Van Doorn, Convexity of Functions which are Generalizations of the Erlang Loss Function and the Erlang Delay Function, SIAM Review 33:281–282, 1991.

18 thms2 active usersReviewed

Algorithmic Game Theory Control Theory Operations Research·Captain: mikedeng1

Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications 2: An Explicit Family of Nash Equilibria for the Linear Impulse GameResearch Paper

Motivation

Impulse control models an agent who acts on a random system through discrete interventions, each with a fixed cost: inventory replenishment, cash management, exchange-rate interventions by a central bank. With two agents whose objectives conflict, the problem becomes a nonzero-sum stochastic differential game with impulse controls. Before the work of Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; preprint arXiv:1605.00039), such games had no general verification theorem and few explicit equilibria; the paper supplies both. Its main application, formalized in this mission, is a game between two central banks with different targets for an exchange rate, a two-player version of the exchange-rate control models of Bertola, Runggaldier and Yasuda and of Cadenillas and Zapatero (references [10], [12] of the paper). The paper proves that this game has an explicit one-parameter family of Nash equilibria of threshold type, with closed-form payoffs.

Setting

The state is a real process. Without interventions it is $x+\sigma W_s$ , where $W$ is a standard real Brownian motion and $\sigma>0$ . Player 1 may shift it up by impulses $\delta\in Z_1=[0,\infty[$ , player 2 down by impulses $\delta\in Z_2=]-\infty,0]$ :

X_s=x+\sigma W_s+\sum_{k:\tau_{1,k}\le s}\delta_{1,k}+\sum_{k:\tau_{2,k}\le s}\delta_{2,k}.

Player 1 earns the running payoff $f_1(X_s)=X_s-s_1$ , player 2 earns $f_2(X_s)=s_2-X_s$ , with $s_1<s_2$ . An impulse $\delta$ costs its author $c+\lambda|\delta|$ and pays the opponent $\tilde c+\tilde\lambda|\delta|$ . Payoffs are discounted at rate $\rho>0$ . The standing assumptions are $c\ge\tilde c\ge0$ , $\lambda\ge\tilde\lambda\ge0$ , $(c,\lambda)\ne(\tilde c,\tilde\lambda)$ and $1-\lambda\rho>0$ .

A strategy of player $i$ is a pair $\varphi_i=(\mathcal C_i,\xi_i)$ : an open continuation region $\mathcal C_i\subseteq\mathbb R$ and a continuous impulse map $\xi_i:\mathbb R\to Z_i$ . Player $i$ intervenes when the state leaves $\mathcal C_i$ , applying the impulse $\xi_i(\text{state})$ ; player 1 has priority when both want to act. This rule defines the controlled process $X^{x;\varphi_1,\varphi_2}$ and the interventions $(\tau_{i,k},\delta_{i,k})$ inductively. Player $i$ 's payoff is

J^i(x;\varphi_1,\varphi_2)=\mathbb E_x\Big[\int_0^\infty e^{-\rho s}f_i(X_s)\,ds-\sum_{k}e^{-\rho\tau_{i,k}}(c+\lambda|\delta_{i,k}|)+\sum_{k}e^{-\rho\tau_{j,k}}(\tilde c+\tilde\lambda|\delta_{j,k}|)\Big].

A pair is $x$ -admissible, $(\varphi_1,\varphi_2)\in\Phi_x$ , when these random variables are integrable, $\sup_t|X_t|$ has all moments, and neither player's interventions accumulate in finite time. A Nash equilibrium is an admissible pair from which no player gains by deviating to any strategy that keeps the pair admissible.

The explicit objects are $\theta=\sqrt{2\rho/\sigma^2}$ , $\eta=(1-\lambda\rho)/\rho$ and

F(y)=2y+\theta c-\eta\log\frac{\eta+y}{\eta-y},\qquad 0<y<\eta .

From the zero $\xi$ of $F$ and a free parameter $\tilde s\in\mathbb R$ , the formulas (4.20)–(4.21) give thresholds $\bar x_1<\bar x_2$ , targets $x_1^*,x_2^*\in]\bar x_1,\bar x_2[$ , coefficients $A_{ij}$ , the functions $\varphi_i(y)=A_{i1}e^{\theta y}+A_{i2}e^{-\theta y}\pm(y-s_i)/\rho$ and the piecewise candidates $\tilde V_1,\tilde V_2$ of (4.6). These are linear outside $]\bar x_1,\bar x_2[$ and equal $\varphi_i$ inside.

Formalization targets

Goal: Proposition 4.7

For every $\tilde s\in\mathbb R$ and every initial state $x\in\mathbb R$ , the threshold strategies

\varphi_1^*=\big(]\bar x_1,+\infty[,\ y\mapsto\max(x_1^*-y,0)\big),\qquad \varphi_2^*=\big(]-\infty,\bar x_2[,\ y\mapsto\min(x_2^*-y,0)\big)

form an $x$ -admissible Nash equilibrium, and

J^1(x;\varphi_1^*,\varphi_2^*)=\tilde V_1(x),\qquad J^2(x;\varphi_1^*,\varphi_2^*)=\tilde V_2(x).

Milestones

(4.17). $F$ has a unique zero $\xi\in(0,\eta)$ .
Proposition 4.2. For every $\tilde s$ , the explicit 8-uple (4.20) satisfies the order conditions (4.7) and the optimality and pasting conditions (4.8)–(4.9). Moreover, $\varphi_2''$ changes sign exactly once in $]x_2^*,\bar x_2[$ .
Lemma 4.6. The impulses (4.23) maximise $\delta\mapsto\tilde V_i(x+\delta)-c-\lambda|\delta|$ , and the intervention operators satisfy (4.24): $\{\mathcal M_1\tilde V_1-\tilde V_1<0\}=]\bar x_1,\infty[$ and $\{\mathcal M_2\tilde V_2-\tilde V_2<0\}=]-\infty,\bar x_2[$ .
Condition (v). The equilibrium pair is $x$ -admissible for every $x$ . This includes the integrability (4.26) of the discounted intervention costs.

Milestones 1–3 are deterministic real analysis; milestone 4 and the goal are probabilistic.

Significance

The result gives explicit equilibria, with explicit thresholds and payoffs, for a nonzero-sum stochastic game with impulse controls. Such games rarely have closed-form solutions. The equilibria form a continuum indexed by $\tilde s$ : equilibrium payoffs are not unique, and every equilibrium in the family is a translate of a fixed interval policy. The explicit formulas also support the comparative statics of Section 4.4, where the continuation region widens as the fixed cost grows.

Proposition 4.7 is proved in the paper by applying its verification theorem (Theorem 3.3) to $\tilde V_1,\tilde V_2$ . The admissibility estimate (4.26) is written out only for initial states $x\in\{x_1^*,x_2^*\}$ ; the general case is said to be similar. As far as is known, none of these results has a machine-checked proof. A formal proof would check every regularity, pasting and admissibility condition. It would also yield a reusable pathwise construction of impulse-controlled Brownian motion.

Difficulty

The deterministic milestones need careful algebra with nested logarithms and square roots. Proving Lemma 4.6 requires the global shape of $\tilde V_i(y)\pm\lambda y$ , which needs the sign pattern of $\varphi_2''$ from Proposition 4.2, not only local conditions at the thresholds.

The goal is harder. The Nash inequality must hold against every admissible deviation: any open continuation region and any continuous impulse map, not only threshold strategies. Comparing payoffs therefore needs a verification argument, namely Itô's formula for a function that is $C^2$ only piecewise and $C^1$ across the thresholds, applied along a process with an unbounded number of jumps, plus a localisation that uses the moment condition (2.8). Admissibility needs a renewal-type bound on the discounted number of interventions, built from i.i.d. exit times of Brownian motion from an interval.

Formalization scope

The Lean development lives in the namespace ImpulseGames.LinearGame.

The constants and standing assumptions are a structure Model with the proposition Model.Standing. The added hypothesis $c>0$ appears in every statement that uses $\xi$ : with $c=0$ , which the standing assumptions allow, $F$ has no zero in $(0,\eta)$ and the family (4.20) does not exist.
The zero $\xi$ is a parameter, constrained by $\xi\in(0,\eta)$ and $F(\xi)=0$ . Milestone 1 shows that exactly one such $\xi$ exists.
The Brownian motion is Mathlib's IsBrownianReal W P on a probability space, with time in $\mathbb R_{\ge0}$ . Definition 2.2 is formalized pathwise: exit times $\inf\{s>\tilde\tau_{k-1}:\tilde X^{k-1}_s\notin\mathcal C_i\}$ in $[0,\infty]$ with $\inf\emptyset=\infty$ , the tie rule favouring player 1, and $e^{-\rho\cdot\infty}=0$ for the tail of each impulse control. No SDE or stochastic integral appears in any statement; the uncontrolled dynamics are $\zeta+\sigma(W_s-W_t)$ .
Payoffs are Bochner expectations. $\Phi_x$ requires every random variable of (2.7) to be integrable, so no deviation can obtain the default value $0$ of a non-integrable expectation. The moment condition (2.8) is stated with an extended-real supremum, and (2.9) is read almost surely.
The Nash condition quantifies over all strategies of Definition 2.1. A formalization that restricts deviations to threshold strategies would be a different, weaker theorem and is excluded. Likewise, the equilibrium payoffs $\tilde V_i$ are the explicit formulas (4.6), never defined as "the equilibrium value".

Two slips of the page are corrected. First, the paper's impulse maps $\xi_i^*(y)=x_i^*-y$ are not $Z_i$ -valued on all of $\mathbb R$ ; they are replaced by $\max(x_1^*-y,0)$ and $\min(x_2^*-y,0)$ , which agree with them wherever each player acts. Second, in Lemma 4.6 the maximiser (4.23) is not unique when $\lambda=\tilde\lambda$ , in the opponent's intervention region (all impulses tie there). The statement asserts maximality everywhere and uniqueness outside that region.

A complete development needs: elementary real analysis for milestones 1–3; a pathwise theory of piecewise-defined processes; an Itô formula for Brownian motion with $C^1$ , piecewise- $C^2$ functions; and exit-time estimates for Brownian motion. The last two are reusable well beyond this mission. Proofs of the deterministic milestones are welcome independently of the stochastic part.

Selected references

R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-sum stochastic differential games with impulse controls: a verification theorem with applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0989 (accepted manuscript: arXiv:1605.00039v4, https://arxiv.org/abs/1605.00039)
G. Bertola, W. J. Runggaldier, K. Yasuda, On classical and restricted impulse stochastic control for the exchange rate, Applied Mathematics and Optimization 74(2), 423–454, 2016.
A. Cadenillas, F. Zapatero, Classical and impulse stochastic control of the exchange rate using interest rates and reserves, Mathematical Finance 10(2), 141–156, 2000.
B. Øksendal, A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer, 2007.

9 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Dimensioning Large Call Centers III: Asymptotically Optimal Staffing in the Quality-Driven RegimeResearch Paper

Motivation

How many agents should a call center staff? Telephone call centers employ millions of people, and staffing is their largest cost, so the question is asked every half hour of every day (Gans, Koole & Mandelbaum, 2003). The classical model is the M/M/N (Erlang-C) queue: calls arrive at rate $\lambda$ , service times are exponential with mean $1/\mu$ , and $N$ agents serve in parallel. Practitioners use the square-root safety staffing rule $N \approx \lambda/\mu + y\sqrt{\lambda/\mu}$ , which Halfin and Whitt (1981) justified in the regime where the probability of waiting stays bounded away from $0$ and $1$ .

Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published as Operations Research 52(1), 2004) asked when such a rule is actually optimal: given a staffing cost and a waiting cost, which staffing level minimizes total cost as the arrival rate grows? They identified three regimes according to how the two costs compare. This mission formalizes their third case, the quality-driven regime, in which waiting is so expensive relative to staffing that the optimal number of agents exceeds the offered load by more than any fixed multiple of its square root.

Setting

Fix a service rate $\mu > 0$ . For every arrival rate $\lambda > 0$ a waiting-cost function $D_\lambda$ assigns cost $D_\lambda(t)$ to a wait of $t$ time units; it satisfies $D_\lambda(0) = 0$ , is strictly increasing, and $t \mapsto D_\lambda(t)e^{-\theta t}$ is integrable on $(0,\infty)$ for every $\theta > 0$ . A staffing cost $F$ , defined for real $N > 0$ , is convex and strictly increasing.

For an integer $N > \lambda/\mu$ the probability of waiting is the Erlang-C formula

\pi(N,\nu) = \frac{\nu^N}{N!}\Bigl\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Bigr\}^{-1},\qquad \nu = \lambda/\mu,

the expected waiting cost of a delayed customer is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$ , and the total cost per unit time is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$ . An optimal staffing level $N^*_\lambda$ minimizes $C(\cdot,\lambda)$ over the integers $N > \lambda/\mu$ .

Write $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ , and for $x > 0$ put $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$ , $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$ , and $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ , where $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$ extends the Erlang-C formula to real $M$ . The normalized cost is $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$ , and a surrogate cost is $C[z;\hat F,\hat\pi,\hat G] = \hat F(z) + \hat\pi(z)\hat G(z)$ . Rounding is measured by $S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda), C(\lceil N_\lambda(x)\rceil,\lambda)\}$ .

Two special functions appear. The Halfin–Whitt delay function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. The Stirling-type approximation is

Q_\lambda(x) = \frac{\exp\{N_\lambda(x)[1 - r_\lambda(x) + \log r_\lambda(x)]\}}{\sqrt{2\pi N_\lambda(x)}\,(1-r_\lambda(x))},\qquad r_\lambda(x) = \frac{\lambda/\mu}{N_\lambda(x)}.

Asymptotic relations are limits of ratios as $\lambda\to\infty$ : $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ , and $a_\lambda \stackrel{\infty}{\ll} b_\lambda$ means $a_\lambda/b_\lambda \to 0$ .

Formalization targets

Goal: Theorem 7.1

Assume the regime is quality-driven, display (27): $F_\lambda(\kappa) \stackrel{\infty}{\ll} G_\lambda(\kappa)$ for every $\kappa > 0$ . Let $y^*_\lambda$ minimize $F_\lambda(y) + Q_\lambda(y)G_\lambda(y)$ over $y > 0$ . Then

\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.

The statement fixes no constants and no rate; it asserts only that rounding the surrogate optimum loses a vanishing fraction of the excess cost.

Milestones

In attack order: Lemma C.1 ( $G_\lambda$ strictly convex decreasing); the identity $H(N,\nu) = \pi(N,\nu)$ at integer $N$ (Section 3, p. 12); Lemma 3.1 and Lemma 3.2; Corollary 3.3 (the asymptotic optimality criterion); Lemma B.1 ( $P$ strictly convex decreasing); display (15); Lemma 4.1 (Halfin and Whitt); and the first statement of Lemma 4.2, $\pi_\lambda(x_\lambda) \stackrel{\infty}{\approx} Q_\lambda(x_\lambda)$ whenever $x_\lambda\to\infty$ .

Significance

Theorem 7.1 completes the paper's picture of optimal staffing. In the rationalized regime the square-root rule with the Halfin–Whitt function $P$ is optimal; in the efficiency-driven regime staffing barely exceeds the load; in the quality-driven regime the staffing excess outgrows $\sqrt{\lambda/\mu}$ and $P$ must be replaced by the Stirling-type expression $Q_\lambda$ . The theorem gives a one-dimensional minimization whose solution is asymptotically optimal, which turns a discrete optimization over $N$ into a smooth problem, and it marks the boundary of validity of square-root staffing.

The result is proved in the paper; it is not formalized anywhere to our knowledge. A complete development formalizes the Section 3 framework (shared with the other regimes of the same paper), the convexity of $G_\lambda$ and of $P$ , the Halfin–Whitt limit for the continuous extension $\pi_\lambda$ , and the Stirling-type asymptotics of the Erlang-C formula. Each of these is a reusable piece of queueing theory in Lean.

Difficulty

The regime theorem itself is short once the framework is in place; the weight lies in the analytic lemmas. Lemma 4.2 requires uniform asymptotics of $\pi_\lambda$ at a staffing excess $x_\lambda$ that may grow at any rate, from barely faster than a constant to faster than $\sqrt{\lambda}$ , where neither the central-limit picture of Halfin and Whitt nor a single Stirling expansion covers all cases. Lemma 4.1 concerns the continuous extension $\pi_\lambda$ at non-integer server counts, whereas Halfin and Whitt's theorem is about integer ones. The natural first idea, that the goal follows from Corollary 3.3 by plugging in Lemma 4.2, does not apply directly: Lemma 4.2 only covers staffing excesses that tend to infinity, and nothing in the definition of the true optimum $x^*_\lambda$ or the surrogate optimum $y^*_\lambda$ says that they do.

Formalization scope

Lean represents $\lambda$ as a positive real, and $\lambda\to\infty$ is the filter atTop on $\mathbb{R}$ with $\mu$ fixed. The standing assumptions on $\mu$ and $D_\lambda$ are the structure WaitModel; $F$ is a function argument with hypotheses ConvexOn and StrictMonoOn on $(0,\infty)$ . Staffing levels $N$ are natural numbers. Minimizers ( $N^*_\lambda$ , $x^*_\lambda$ , $z^*_\lambda$ , $y^*_\lambda$ ) are function arguments with minimality hypotheses at every $\lambda > 0$ , so every statement holds for every choice among ties. Liminf and limsup relations are stated through Filter.Frequently, avoiding boundedness side conditions.

The queue itself (Poisson arrivals, waiting-time law) is not formalized: the paper's analysis and all its theorems concern the closed-form cost $C(N,\lambda)$ with the Erlang-C formula.

Conventions committed to: (i) the goal adds the hypothesis $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$ , which the paper asserts on p. 12 to show the continuous optimum exists but which does not follow from its standing assumptions (it holds exactly when $D_\lambda$ is unbounded); (ii) in $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ , since the cost is undefined at unstable levels; (iii) the integrability of $D_\lambda(t)e^{-\theta t}$ is explicit, because a Lean integral of a non-integrable function is $0$ ; (iv) $P(0) = 1$ , the value of formula (11) at $0$ ; (v) display (15) is stated for $b > 0$ , since the ratio $a_\lambda/b$ is undefined at $b = 0$ . The instance $\mu = 1$ , $F(N) = cN$ , $D_\lambda(t) = a\sqrt{\lambda}\,t$ (Section 9) satisfies every hypothesis of the goal, so the goal is not vacuous; taking $\pi_\lambda$ or $G_\lambda$ at Lean default values is ruled out by these explicit domain conditions.

Only the first statement of Lemma 4.2 is a milestone: the second, $\pi_\lambda(x_\lambda)\approx Q(x_\lambda)$ under $x_\lambda \stackrel{\sup}{\le} \lambda^{1/6}$ , fails as printed at $x_\lambda = \lambda^{1/6}$ . Contributions on the Erlang-C asymptotics, the normal hazard rate, and Laplace transforms of increasing functions are welcome and reusable beyond this mission.

Selected references

S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000 (the version formalized here; every index and page cited in this mission is the report's).
S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
N. Gans, G. Koole, A. Mandelbaum, Telephone Call Centers: Tutorial, Review, and Research Prospects, Manufacturing & Service Operations Management 5(2):79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071

24 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Dimensioning Large Call Centers II: Asymptotically Optimal Staffing in the Efficiency-Driven RegimeResearch Paper

Why staffing large call centers is a mathematical question

A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.

The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.

The Erlang-C cost model

Customers arrive at rate $\lambda>0$ and receive exponential service at rate $\mu>0$ per server. The service rate $\mu$ is fixed as $\lambda$ grows. For an integer number of servers $N>\lambda/\mu$ , the Erlang-C delay probability $\pi(N,\lambda/\mu)$ is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate $N\mu-\lambda$ . Let $D_\lambda(t)$ be the cost of a wait of length $t$ . It is strictly increasing on $t\ge0$ , satisfies $D_\lambda(0)=0$ , and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is

G(N,\lambda)=(N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt.

The staffing cost $F(N)$ is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real $N>0$ . Total cost per unit of time at a stable integer level is

C(N,\lambda)=F(N)+\lambda\pi(N,\lambda/\mu)G(N,\lambda).

Write $N^*_\lambda$ for any minimizing stable integer level. Ties are permitted. For a positive real offset $x$ , define $N_\lambda(x)=\lambda/\mu+x\sqrt{\lambda/\mu}$ , $F_\lambda(x)=F(N_\lambda(x))-F(\lambda/\mu)$ , and $G_\lambda(x)=\lambda G(N_\lambda(x),\lambda)$ . The report extends Erlang-C continuously to $\pi_\lambda(x)$ and writes the incremental continuous objective as $C_\lambda(x)=F_\lambda(x)+\pi_\lambda(x)G_\lambda(x)$ . These definitions and the integer-extension identity are from Section 3, printed pages 11–12.

Formalization targets

The report defines the efficiency-driven regime by

\text{for every }\kappa>0,\qquad \lim_{\lambda\to\infty}\frac{F_\lambda(\kappa)}{G_\lambda(\kappa)}=+\infty.

For each $\lambda>0$ , choose $y^*_\lambda>0$ to minimize $F_\lambda(y)+G_\lambda(y)$ over $y>0$ . Let $S_\lambda(y)$ be the smaller cost of the stable integer levels immediately below and above $N_\lambda(y)$ ; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is

\lim_{\lambda\to\infty} \frac{S_\lambda(y^*_\lambda)-F(\lambda/\mu)} {C(N^*_\lambda,\lambda)-F(\lambda/\mu)}=1.

The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.

What the result gives

The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline $F(\lambda/\mu)$ , which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.

The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.

Where the difficulty lies

The simple objective replaces the delay probability $\pi_\lambda(y)$ by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with $\lambda$ . Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when $N_\lambda(y)$ is just above $\lambda/\mu$ , its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.

Formalization scope and conventions

Lean represents $\lambda$ , $\mu$ , offsets, and costs as real numbers; arrival-rate limits use the real filter at $+\infty$ . Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of $D_\lambda$ on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for $G$ and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on $F$ are convexity and strict increase on positive real staffing levels; $F$ does not depend on $\lambda$ .

The report asserts that $G(N,\lambda)$ diverges as $N$ decreases to $\lambda/\mu$ , although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.

All formulas are total Lean functions. Their values at $\lambda\le0$ , unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of $S_\lambda$ ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.

The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.

Selected references

Sem Borst, Avi Mandelbaum, and Martin I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000. Report PDF. Theorem 6.1, printed p. 19; Corollary 3.3, printed p. 14; Lemma 4.1, printed p. 15; Lemma C.1, printed p. 40.

22 thms2 active usersReviewed

Completed

Markov Chain Operations Research Probability·Captain: mikedeng1

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance I: Quadratic Potential Functions Bound Mean Response Times in Open NetworksResearch Paper

Motivation

Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.

Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).

Timeline:

1980–1988: Coffman and Mitrani, then Federgruen and Groenevelt — the achievable performance vectors of a single-station multiclass queue form a polytope described by conservation laws.
Early 1990s: Kumar (reference [Kuma] of the paper), using a potential-function argument he attributes to Meyn, derives a single lower bound on the mean number in system for re-entrant lines with deterministic routing (described on p. 16 of the paper).
1992–1994: Bertsimas, Paschalidis and Tsitsiklis — parametric families of linear bounds for general open networks with Markovian routing (Theorem 4.1), and the nonparametric polyhedron (Theorems 4.2–4.4), shown to be at least as tight.

Setting

A network has $N$ single-server stations and $R$ job classes. Class $r$ is served at station $\sigma(r)$ , and $C_i$ is the set of classes served at station $i$ . Class- $r$ jobs arrive from outside as a Poisson stream of rate $\lambda_{0r}$ , service times are exponential with rate $\mu_r$ , and after service a class- $r$ job becomes a class- $s$ job with probability $p_{rs}$ or leaves with probability $p_{r0}=1-\sum_s p_{rs}$ . The traffic equations

\lambda_r=\lambda_{0r}+\sum_{r'}\lambda_{r'}p_{r'r}\qquad(15)

have a unique solution $\lambda$ (the network is open), and $\sum_{r\in C_i}\lambda_r/\mu_r<1$ at every station.

The state $\vec n=(n_1,\dots,n_R)$ counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write $B_r$ for the event that station $\sigma(r)$ serves class $r$ , and $B_{0i}$ for the event that station $i$ is idle. Under such a policy $\vec n(t)$ is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution $\pi$ and that $E_\pi[n_r^2]<\infty$ for all $r$ . Let $\bar n_r=E_\pi[n_r]$ , which equals $\lambda_rx_r$ with $x_r$ the mean response time of class $r$ (Little's law), and define

I_{rr'}=E_\pi[1\{B_r\}n_{r'}],\qquad N_{ir'}=E_\pi[1\{B_{0i}\}n_{r'}].

For a set $S$ of classes, f-parameters are reals $f(r)\ge 0$ for $r\in S$ such that $\mu_r\big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))+\sum_{r'\notin S}p_{rr'}f(r)\big]$ is nonnegative and the same for all $r\in C_i\cap S$ ; that common value is $f_i$ , and $f_i=0$ when $C_i\cap S=\emptyset$ (restriction (17)). The sums over $r'\notin S$ include the exit $r'=0$ .

Formalization targets

Goal: Theorem 4.1

For every policy satisfying Assumption A, every $S$ and every f-parameters satisfying (17),

\sum_{r\in S}\lambda_rf(r)x_r\ \ge\ \frac{N'(S)}{D'(S)},

where

N'(S)=\sum_{r\in S}\lambda_{0r}f^2(r)+\sum_{r\notin S}\lambda_r\sum_{r'\in S}p_{rr'}f^2(r')+\sum_{r\in S}\lambda_r\Big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))^2+\sum_{r'\notin S}p_{rr'}f^2(r)\Big],

D'(S)=2\Big[\sum_{i=1}^Nf_i-\sum_{r\in S}\lambda_{0r}f(r)\Big].

The formal goal is the product form $N'(S)\le D'(S)\sum_{r\in S}f(r)\bar n_r$ .

Milestones

The utilization identity $E_\pi[1\{B_r\}]=\lambda_r/\mu_r$ (pp. 16 and 19).
Theorem 4.2: the linear equalities (24), (25) between $\bar n_r$ and $I_{rr'}$ .
Theorem 4.3: $\sum_{r\in C_i}I_{rr'}+N_{ir'}=\bar n_{r'}$ (28).
Theorem 4.4: any nonnegative $(x,I,N)$ satisfying (24), (25), (28), with $\bar n_r=\lambda_rx_r$ in those equalities, satisfies every inequality of Theorem 4.1. This statement is deterministic.

Significance

Theorem 4.1 gives, for each choice of $S$ and $f$ , a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost $\sum_r c_rx_r$ subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables $(\bar n,I,N)$ implies all of these inequalities at once, so the parametric search over $f$ is unnecessary.

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.

Difficulty

Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions ( $n_r$ , $n_rn_{r'}$ ) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending $\sum_n\pi(n)(\mathcal Gg)(n)=0$ to quadratic $g$ needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify $\mu_rE_\pi[1\{B_r\}]$ with $\lambda_r$ . Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because $f\ge0$ on $S$ , $f_i\ge0$ and at most one class per station is in service.

Formalization scope

Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs $\tau_k$ of the paper are not built: the paper notes that its expectations at $\tau_k$ are expectations under the invariant distribution of $\vec n(t)$ .

Conventions fixed in Lean:

$\lambda_rx_r$ appears only as the mean number in system $\bar n_r$ (Little's law, used by the paper on pp. 11 and 20); response times are not formalized.
Sums over $r'\notin S$ include the exit $r'=0$ (p. 15).
f-parameters are nonnegative on $S$ (p. 9).
The network is open: (15) has a unique solution, and $\lambda$ is an input constrained by (15), never defined from the policy.
(18) is stated multiplied by $D'(S)$ , which avoids Lean's $x/0=0$ and is (18) whenever $D'(S)>0$ .

A quotient-form statement of (18) would be trivially true when $D'(S)=0$ , and defining $\lambda_r$ as $\mu_rE_\pi[1\{B_r\}]$ would make the utilization identity hold by definition; both are excluded.

Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.

Selected references

D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan WP #3509-92-MSA, 1992; Ann. Appl. Probab. 4(1), 1994. https://doi.org/10.1214/aoap/1177005200
C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queuing network control, Math. Oper. Res. 24(2), 1999. https://doi.org/10.1287/moor.24.2.293

8 thms2 active usersReviewed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Approximation Algorithms for Stochastic Inventory Control Models 2: The Triple-Balancing Policy Costs at Most Three Times the Optimum for Stochastic Lot-SizingResearch Paper

Motivation

Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of $T$ periods, decides whether to place an order, pays a fixed cost $K$ for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand is random and correlated across periods, and the firm's forecast evolves as information arrives, the optimal policy solves a dynamic program over the whole information state. That program is intractable in general, and in practice firms use heuristics with no performance guarantee.

Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2), 2007) gave policies with worst-case guarantees for these models, using a "marginal cost accounting" scheme that charges each unit's holding cost to the period in which it was ordered. For the model with fixed ordering costs, the stochastic lot-sizing problem, they assume that the demand of each period is known at the beginning of that period (make-to-order systems, or settings where the short-term forecast is accurate), while demand further ahead stays random and arbitrarily correlated. Under this assumption they define the triple-balancing policy and prove it costs at most three times the optimum in expectation.

Timeline:

Scarf (1960) proved that $(s,S)$ policies are optimal for independent demands with fixed costs; with correlated demand the optimal policy is a state-dependent $(s_t(f_t), S_t(f_t))$ rule that is hard to compute.
Levi, Pál, Roundy and Shmoys (2007) gave the dual-balancing 2-approximation for the model without fixed costs (§4) and the triple-balancing 3-approximation for the stochastic lot-sizing problem (§6, Theorem 6.1), both for arbitrarily correlated demand.

Setting

There are periods $t=1,\dots,T$ on a probability space $(\Omega,\mathcal F,\mu)$ with a filtration $(\mathcal F_t)$ : $\mathcal F_t$ is the information available at the beginning of period $t$ . The data are a fixed ordering cost $K\ge0$ , per-unit holding costs $h_t\ge0$ , per-unit backlogging penalties $p_t\ge0$ , an initial inventory level $x_1\in\mathbb R$ , and nonnegative demands $D_t$ . The per-unit ordering cost is zero, the lead time is zero and there is no discounting. The defining assumption is that $D_t$ is $\mathcal F_t$ -measurable: the demand of a period is known when the period begins. For every period $s$ there is a conditional joint distribution $I_s$ of the demands given $\mathcal F_s$ , under which every conditional mean $E[D_t\mid f_s]$ is finite.

A feasible policy is an order process $Q=(Q_t)$ with $Q_t\ge0$ and $Q_t$ determined by $\mathcal F_t$ . Its inventory levels are $x_t=x_1+\sum_{j<t}(Q_j-D_j)$ before ordering and $y_t=x_t+Q_t$ after ordering, and its cost is

\mathcal C(Q)=\sum_{t=1}^T\Bigl(K\,\mathbb 1(Q_t>0)+h_t(y_t-D_t)^++p_t(D_t-y_t)^+\Bigr).

The triple-balancing policy TB uses two rules. Let $s^*$ be the last period before $s$ in which TB ordered ( $s^*=0$ if none). Rule 1: TB orders in period $s$ if and only if, without an order in $s$ , the accumulated backlogging cost over $(s^*,s]$ would exceed $K$ . Rule 2: when it orders in $s<T$ , it orders

q_s^B=\max\{q\ge0:\ E[H_s^B(q)\mid f_s]\le K\},\qquad H_s^B(q)=\sum_{j=s}^T h_j\bigl(q-(D_{[s,j]}-x_s)^+\bigr)^+,

the largest quantity whose expected marginal holding cost over $[s,T]$ is at most $K$ . When it orders in period $T$ , it orders exactly enough to clear the backorders and meet $D_T$ . Let $N$ be the number of orders TB places.

Formalization targets

Goal: Theorem 6.1

For every instance, the triple-balancing policy TB and every feasible policy $P$ satisfy

E[\mathcal C(TB)]\le 3\,E[\mathcal C(P)].

The constant 3 is the paper's. The statement leaves the demand law, the information structure and the cost data unrestricted beyond the standing assumptions above.

Milestones

§6.1, Rule 2 observation. In a period where TB orders, $D_s\le y_s^{TB}$ : no backorders remain at the end of the period.
Lemma 6.1. $K\cdot E[N]\le E[\mathcal C(P)]$ for every feasible $P$ .
Lemma 6.2. $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\cdot E[N]$ for every feasible $P$ .

Two non-milestone theorems show that the setting is not empty. A conditional demand law exists whenever demands are integrable, and a triple-balancing policy exists when $h_T>0$ .

Significance

The theorem gives a policy that can be computed online and comes with a worst-case expected-cost guarantee that does not depend on the demand distribution, the horizon or the cost data. In this setting the optimal policy is not computable in general, and the previously used heuristics have no such bound. The two lemmas separate a lower bound on every policy, in terms of TB's own number of orders, from an upper bound on TB's cost. The authors' subsequent work extends the balancing template to capacitated and multi-echelon models (§7 of the paper).

The result is proved in the paper. As far as we know, no machine-checked version exists of this theorem, of the balancing argument, or of a stochastic inventory model with correlated demand and evolving information. A formalization would check the argument, which is terse in places: the printed proof of Lemma 6.2 indexes its final sum loosely and must handle the event $N=0$ . It would also produce reusable infrastructure for policies adapted to a filtration, for regular conditional distributions of future demand, and for cost accounting over random intervals between orders.

Difficulty

The costs of TB and of an arbitrary policy cannot be compared period by period, because the two policies order at different, random times that depend on the evolving information. Any comparison has to be made over intervals whose endpoints are stopping times determined by TB, conditioned on the information at their start. At such a time the other policy may hold more or less stock than TB, and the bound must hold in both cases. Bounding each policy's cost on its own does not work: the guarantee rests on a coupling between when TB orders and what every other policy must pay over the same random stretch of time. The formal side adds a second difficulty. Rule 2 is defined through a conditional expectation viewed as a function of the order quantity, so it needs a regular conditional distribution and a measurable selection of the maximizer.

Formalization scope

Periods are natural numbers $1,\dots,T$ , demands and orders are real-valued, and data at indices outside $1,\dots,T$ are unused.
Information is a MeasureTheory.Filtration ℕ. A policy is feasible when it is nonnegative and adapted, and " $D_t$ known at the start of period $t$ " means $D_t$ is $\mathcal F_t$ -measurable.
The conditional distributions $I_s$ are model data: Markov kernels to demand paths that are $\mathcal F_s$ -measurable regular conditional distributions of the demand path. At every outcome they make $D_s$ deterministic, demands nonnegative and the conditional means $E[D_t\mid f_s]$ finite.
Expected costs, $E[N]$ and the conditional expectation in Rule 2 are lower Lebesgue integrals in $[0,\infty]$ . Lemma 6.2 is stated additively, $E[\mathcal C(TB)]\le E[\mathcal C(P)]+2K\,E[N]$ , which is the paper's inequality whenever the expectations are finite.
The comparison policy is an arbitrary feasible policy, not an optimal one. The paper's proofs use only feasibility, and this form implies the paper's whenever an optimum exists, without any existence hypothesis.
TB is the predicate "feasible and satisfies Rules 1 and 2 at every period and outcome". The rules determine the policy uniquely. Rule 1 uses a strict "exceeds $K$ ", and the period- $T$ order is $D_T-x_T$ .

Several trivializing formalizations are ruled out. Junk conditional expectations cannot make Rule 2 hold for every $q$ , because it uses kernel integrals in $[0,\infty]$ . Infinite expected costs cannot be read as $0$ . The policy class is not empty, because a separate theorem gives existence under $h_T>0$ (without some positive holding cost on $[s,T]$ the maximum in Rule 2 does not exist).

Contributions welcome: proofs of the existence theorems (measurable selection of $q_s^B$ , versions of regular conditional distributions), the stopping-time decomposition of the cost over TB's order intervals, and Lemmas 6.1 and 6.2.

Selected references

R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2):284–302, 2007. https://doi.org/10.1287/moor.1060.0205
H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.

7 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Open Queueing Networks in Heavy Traffic: Reflected Brownian Motion Limit for the Queue Length ProcessResearch Paper

Motivation

Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.

Timeline:

Iglehart and Whitt (1970a,b) proved heavy-traffic limits for a single multiple-server station and for acyclic networks, in which no customer visits a station twice.
Harrison (1973, 1978) treated tandem queues; the 1978 paper introduced reflected Brownian motion on the nonnegative orthant as the diffusion limit.
Harrison and Reiman (1981a, Ann. Probab. 9:302–308) constructed reflected Brownian motion on the orthant through a continuous reflection mapping. That paper is the source of Lemma 1 here.

(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)

Reiman (1984) proved the limit for general open networks with Markovian routing (Theorem 1). The paper also proves a limit for sojourn times along fixed routes (Theorem 2).

Setting

There are $K$ single-server stations and a nonempty set $\mathcal J\subseteq\{1,\dots,K\}$ of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times $u_k^i>0$ ( $k\in\mathcal J$ ), service times $v_k^i>0$ , and routing indicators $\phi_k^i\in\{0,1,\dots,K\}$ . When the $i$ th customer served at station $k$ finishes, it moves to station $\phi_k^i$ , or leaves if $\phi_k^i=0$ . The parameters are the service rates $\mu_k=(E v_k^1)^{-1}$ , the service-time variances $s_k=\operatorname{var} v_k^1$ , the arrival rates $\lambda_k=(E u_k^1)^{-1}$ (with $\lambda_k=0$ for $k\notin\mathcal J$ ), and the interarrival variances $a_k=\operatorname{var} u_k^1$ . The routing matrix $P=(p_{kj})$ , $p_{kj}=P\{\phi_k^1=j\}$ , has spectral radius strictly less than one, so every customer eventually leaves.

Let $A_k(t)$ be the number of exogenous arrivals to station $k$ by time $t$ , and $S_k(t)$ the number of service completions at $k$ in $t$ units of busy time. Let $\hat S_k(t)=\sum_{i\le S_k(t)}e_{\phi_k^i}-S_k(t)e_k$ , with $e_0=0$ . The queue length $Q(t)\in\mathbb Z_+^K$ and the busy time $B(t)$ are the unique solution of

Q(t)=A(t)+\sum_{k=1}^K\hat S_k(B_k(t)),\qquad B_k(t)=\int_0^t1_{\{Q_k(s)>0\}}\,ds,\qquad B(0)=0 .

A sequence of such networks, indexed by $n$ , shares $K$ , $\mathcal J$ and $P$ . Its parameters $\mu(n),s(n),\lambda(n),a(n)$ converge to finite limits $\mu,s,\lambda,a$ . With $\nu(n)=\lambda(n)+\mu(n)P$ , the heavy-traffic condition is

c_k(n)=\sqrt n\,(\nu_k(n)-\mu_k(n))\to c_k .

Moments of order $2+\epsilon$ of the interarrival and service times are bounded uniformly in $n$ . The scaled queue length is $Z^n(t)=n^{-1/2}Q^n(nt)$ , $0\le t\le1$ .

Formalization targets

Goal: Theorem 1

Let $\xi$ be a Brownian motion with drift $c$ and covariance matrix $\mathcal A$ , where

\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),

\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).

Let $Z=\phi(\xi)$ be its reflection with reflection matrix $I-P$ . Then

Z^n\Rightarrow Z\quad\text{in } D[0,1]\text{ (Skorohod topology)}.

The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).

Milestones

The milestones follow the paper's proof, in order:

the existence and uniqueness claim for (1)–(3);
the representation $Q=\tilde X+Y(I-P)$ (Eq. (13));
the least-element map $f$ (Proposition 1);
the reflection mapping $\phi$ (Lemma 1) and $f=\phi$ on continuous paths (Proposition 2);
the netput limit $\zeta^n\Rightarrow\zeta$ (Proposition 3);
stochastic boundedness of $Z^n$ (Lemma 6);
vanishing scaled idleness $n^{-1}I^n_k(n)\to0$ (Proposition 4);
the centred limit $\tilde\zeta^n\Rightarrow\zeta$ (Proposition 5).

Significance

Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing $Q^n(t)\approx\sqrt n\,Z(t/n)$ reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.

The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:

a formal statement of the network, of its Harrison representation, and of weak convergence in $D$ ;
a formal proof of the reflection-mapping facts (Proposition 1, Lemma 1, Proposition 2), which are deterministic and reusable;
eventually, a formal proof of the full limit theorem.

Difficulty

The obvious route applies a functional central limit theorem to $Q^n$ directly. That fails because $Q^n$ is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time $B_k(t)$ , which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator $Y$ . It then has to show that the random time change $B^n_k(nt)/n$ converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of $D$ but is known to be continuous only at continuous paths.

Formalization scope

The Lean development uses the following conventions:

Stations are Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.
A routing indicator lives in Fin (K+1), with 0 meaning "leaves" and j.succ meaning station $j$ .
The primitives are mutually independent (iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.
"Spectral radius $<1$ " is stated as $P^m\to0$ .
$(Q^n,B^n)$ is any pair solving (1)–(3) almost surely, with measurable paths so that (2) is a Lebesgue integral.
The networks are indexed by ℕ; (25)–(26) are imposed for $n\ge1$ , (22) and (26) over $k\in\mathcal J$ , and $\mathcal J$ is the same for all $n$ .
Brownian motion with drift $c$ and covariance $\mathcal A$ lives on $[0,\infty)$ . It is defined by continuity, $\xi(0)=0$ , independent increments, and the Gaussian characteristic function of increments.
$Z$ is the reflection of $\xi$ in the sense of (14)–(17).
Weak convergence in $D$ is stated in Skorohod-representation form: a coupling with almost-sure J $_1$ convergence on $[0,1]$ . This form accommodates a separate probability space for each $n$ .

Added hypotheses, each implicit on the page:

The existence item assumes $U_k(l),V_k(l)\to\infty$ at the sample point; without it the maxima defining $A_k(t)$ and $S_k(t)$ need not exist.
Solutions of (1)–(3) have measurable paths.

No positivity hypothesis on the limits $\mu_k$ is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.

The statement is not to be weakened. Ruled out are:

convergence of finite-dimensional distributions only;
a single network without the index $n$ ;
uniform convergence used in place of the Skorohod topology without the coupling;
a Brownian motion that is not required to have independent Gaussian increments.

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

the deterministic reflection-map results;
Donsker-type theorems for renewal counting processes in $D$ ;
the random time-change lemma (Billingsley);
the continuous mapping theorem in coupling form.

Selected references

M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3):441–458, 1984. https://doi.org/10.1287/moor.9.3.441
J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9:302–308, 1981 (cited in Reiman 1984 as [6]).
J. M. Harrison, The Diffusion Approximation for Tandem Queues in Heavy Traffic, Advances in Applied Probability 10:886–905, 1978 (Reiman 1984, [5]).
J. M. Harrison, The Heavy Traffic Approximation for Single Server Queues in Series, Journal of Applied Probability 10:613–629, 1973 (Reiman 1984, [4]).
D. L. Iglehart and W. Whitt, Multiple Channel Queues in Heavy Traffic, I and II: Sequences, Networks, and Batches, Advances in Applied Probability 2:150–177 and 355–364, 1970 (Reiman 1984, [8], [9]).
P. Billingsley, Convergence of Probability Measures, Wiley, New York, 1968 (Reiman 1984, [1]).

13 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Dimensioning Large Call Centers I: The Rationalized Staffing Function Is Asymptotically OptimalResearch Paper

Motivation

A call center with $N$ agents facing Poisson arrivals at rate $\lambda$ and exponential service at rate $\mu$ is the M/M/N (Erlang-C) queue. Choosing $N$ trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule $N \approx R + y\sqrt R$ , where $R = \lambda/\mu$ is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor $y$ that makes the rule asymptotically optimal as the arrival rate grows.

Timeline of the asymptotic regime the paper builds on:

1917. Erlang's delay formula $\pi(N,\nu)$ for the M/M/N queue.
1981. Halfin and Whitt (Oper. Res. 29(3)) show that with $N = R + \beta\sqrt R$ servers the probability of waiting converges to a limit $P(\beta) \in (0,1)$ , the quality-and-efficiency-driven regime.
2000/2004. Borst, Mandelbaum and Reiman classify cost structures into a rationalized, an efficiency-driven and a quality-driven regime, and prove asymptotic optimality of an explicit staffing rule in each.

This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.

Setting

The service rate $\mu > 0$ is fixed and the arrival rate $\lambda$ grows. A staffing cost $F$ , defined on $(0,\infty)$ , is convex and strictly increasing; it does not depend on $\lambda$ . For each $\lambda > 0$ a waiting-cost function $D_\lambda$ satisfies $D_\lambda(0)=0$ , is strictly increasing on $[0,\infty)$ , and makes

G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)\,e^{-(N\mu-\lambda)t}\,dt

finite for every $N > \lambda/\mu$ . With the Erlang-C formula

\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{\big(1-\tfrac{\nu}{N}\big)\sum_{n=0}^{N-1}\frac{\nu^n}{n!}+\frac{\nu^N}{N!}\Big\}^{-1},

the expected total cost of staffing $N > \lambda/\mu$ agents is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$ , and $N^*_\lambda$ is any integer $N > \lambda/\mu$ minimizing it (7).

In normalized units $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ the paper defines $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$ , $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$ , the continuous delay probability $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with

H(M,\alpha) = \Big\{\alpha\int_0^\infty e^{-\alpha t}\,t\,(1+t)^{M-1}\,dt\Big\}^{-1},

and $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$ , minimized at $x^*_\lambda$ (8). A surrogate $C[z;\hat F,\hat\pi,\hat G] = \hat F(z)+\hat\pi(z)\hat G(z)$ approximates it. Rounding is measured by

S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda),\,C(\lceil N_\lambda(x)\rceil,\lambda)\}. \tag{10}

The Halfin–Whitt delay function is $P(x) = \big(1 + x/h(-x)\big)^{-1}$ , with $h = \phi/(1-\Phi)$ the standard normal hazard rate (11). Asymptotic equality $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ as $\lambda\to\infty$ .

Formalization targets

Goal: Theorem 5.1

Assume the rationalized condition (18): for some $\kappa > 0$ , $F_\lambda(\kappa)/G_\lambda(\kappa) \to \gamma \in (0,\infty)$ . Let $y^*_\lambda$ minimize $F_\lambda(y) + P(y)G_\lambda(y)$ over $y>0$ (19). Then

\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.

The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.

Milestones

Lemma C.1: $G_\lambda$ is strictly convex and strictly decreasing on $(0,\infty)$ .
Section 3, p. 12: $H(N,\nu) = \pi(N,\nu)$ at integers $N > \nu > 0$ .
Lemma 3.1, Lemma 3.2, Corollary 3.3: the approximation principle. If the surrogate approximates $C_\lambda$ at both $x^*_\lambda$ and its own minimizer $z^*_\lambda$ , then rounding $N_\lambda(z^*_\lambda)$ is asymptotically optimal.
Eqs. (13)–(14): $F_\lambda$ preserves $\limsup$ -separation of ratios.
Lemma 4.1 (Halfin & Whitt): for bounded $x_\lambda$ , $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$ .

Significance

The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost $c$ per agent, linear waiting cost $a$ per unit time) it gives $N^* \approx R + y^*(a/c)\sqrt R$ , with $y^*(r)$ the minimizer of $y + rP(y)/y$ , a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.

The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension $\pi_\lambda$ , is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.

Difficulty

The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of $C_\lambda$ is available, but unimodality rests on convexity of $\pi_\lambda$ , which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while $\pi_\lambda$ is evaluated at non-integer $N_\lambda(x_\lambda)$ ; a proof needs a uniform Laplace-type asymptotic for the integral defining $H$ . A further obstacle is bounding $x^*_\lambda$ : the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).

Formalization scope

All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on $\mathbb R$ with $\mu$ fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost $C(N,\lambda)$ , and so are these. Committed conventions:

The standing assumptions are a structure WaitModel ( $\mu>0$ ; $D_\lambda(0)=0$ ; $D_\lambda$ strictly increasing on $[0,\infty)$ ; $t\mapsto D_\lambda(t)e^{-\theta t}$ integrable on $(0,\infty)$ for every $\theta>0$ , which is the paper's finiteness of $G$ ). $F$ is convex and strictly increasing on $(0,\infty)$ .
Staffing levels in $C(N,\lambda)$ are natural numbers; $G$ and $H$ take real $N$ .
Argmins ( $N^*_\lambda$ , $x^*_\lambda$ , $z^*_\lambda$ , $y^*_\lambda$ ) are hypotheses that a given function is a minimizer, for every $\lambda>0$ ; ties are allowed and the theorems hold for every choice.
In $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ , where $C$ is undefined.
$\limsup$ and $\liminf$ relations are written with ∃ᶠ/∀ᶠ, not Filter.limsup on $\mathbb R$ .
Added hypothesis. The goal assumes $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$ . The paper asserts this limit on p. 12, but it does not follow from its assumptions (it fails for bounded $D_\lambda$ ); it is equivalent to $D_\lambda$ being unbounded and is what makes the continuous optimum exist.

The hypotheses are met by linear staffing and waiting costs ( $F(N)=cN$ , $D_\lambda(t)=at$ ), for which (18) holds with $\gamma = c\kappa^2/a$ , so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every $\lambda>0$ , and $S_\lambda$ never evaluates $C$ at an unstable level.

Needed infrastructure: Laplace asymptotics for $\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt$ , differentiation under the integral sign for $G$ , and convexity of $\pi_\lambda$ . All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].

Selected references

S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917.

21 thms2 active usersReviewed

Completed

Dynamical Systems Operations Research Probability·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 7: Weak Limit Points of the Occupation Measures of a Weak Asymptotic Pseudotrajectory Are InvariantResearch Paper

Motivation

Stochastic approximation algorithms are recursions $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ driven by small steps $\gamma_n$ and noise $U_{n+1}$ ; they include the Robbins–Monro scheme, stochastic gradient methods and learning dynamics in games. The ODE method studies their long-run behaviour by comparing a time-interpolation of the iterates with the trajectories of a deterministic dynamical system. In Benaïm's lecture notes (Benaïm 1999) this comparison is formalized by the notion of an asymptotic pseudotrajectory, introduced in Benaïm and Hirsch (1996): a path that, over every window of fixed length, shadows the deterministic orbit started at its current position with an error that vanishes as time goes to infinity.

The pathwise results of the earlier sections of the notes concern algorithms whose step sizes decrease fast enough, typically $\gamma_n=o(1/\log n)$ or $\gamma_n=O(n^{-\alpha})$ . When the step sizes go to zero more slowly, the limit sets of the process can no longer be characterized precisely: with steps of order $1/\log n$ the process may fail to converge even when the chain recurrent set of the ODE consists of isolated equilibria. Section 10, which is mainly based on work of Benaïm and Schreiber, describes instead the statistical behaviour of such processes in terms of the deterministic dynamics. It introduces a weaker, conditional notion, the weak asymptotic pseudotrajectory, and proves in Theorem 10.1 that the empirical distribution of the time spent by the process in different regions of the state space accumulates only on invariant measures of the deterministic dynamics. This is an ergodic-theoretic counterpart of the limit-set theorems of Section 5.

Setting

A semiflow on a metric space $(M,d)$ is a continuous map $\Phi:\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ for $t,s\ge0$ . Throughout, $M$ is a separable metric space with its Borel $\sigma$ -algebra.

Let $(\Omega,\mathcal F,P)$ be a probability space and $\{\mathcal F_t\}_{t\ge0}$ a nondecreasing family of sub- $\sigma$ -algebras. A process $X:\mathbb R_+\times\Omega\to M$ is a weak asymptotic pseudotrajectory of $\Phi$ if

it is progressively measurable: for every $T>0$ the restriction of $X$ to $[0,T]\times\Omega$ is measurable for the product of the Borel $\sigma$ -field of $[0,T]$ and $\mathcal F_T$ ;
for each $\alpha>0$ and $T>0$ , almost surely

\lim_{t\to\infty}P\Big\{\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)\ge\alpha\ \Big|\ \mathcal F_t\Big\}=0 .

Let $\mathcal P(M)$ be the space of Borel probability measures on $M$ with the topology of weak convergence. A measure $\mu\in\mathcal P(M)$ is $\Phi$ -invariant if $(\Phi_t)_*\mu=\mu$ for every $t\ge0$ ; the set of invariant measures is $\mathcal M(\Phi)$ . The occupation measure of the process at time $t>0$ is the random probability measure

\mu_t(\omega)=\frac1t\int_0^t\delta_{X(s,\omega)}\,ds ,

and $\mathcal M(X,\omega)\subset\mathcal P(M)$ is the set of its weak limit points as $t\to\infty$ .

Formalization targets

Goal: Theorem 10.1

If $X$ is a weak asymptotic pseudotrajectory of $\Phi$ , there is a set $\tilde\Omega\subset\Omega$ with $P(\tilde\Omega)=1$ such that for all $\omega\in\tilde\Omega$

\mathcal M(X,\omega)\subset\mathcal M(\Phi).

No tightness is assumed, so $\mathcal M(X,\omega)$ may be empty; the statement asserts the inclusion, not nonemptiness.

Milestones

Fix a uniformly continuous $f:M\to[0,1]$ and $T>0$ , and set $U_n(f,T)=\int_{(n-1)T}^{nT}f(X(s))\,ds$ for $n\ge1$ . The milestones are the numbered displays of the proof on pp. 62–63:

Eq. (47): $\frac1n\sum_{i=1}^n[U_i(f,T)-E(U_i(f,T)\mid\mathcal F_{(i-1)T})]\to0$ almost surely (stated for every continuous $f$ with values in $[0,1]$ , since the proof also applies it to $f\circ\Phi_T$ );
Eq. (50): the same with $U_{i+1}(f,T)$ conditioned on $\mathcal F_{(i-1)T}$ ;
Eq. (51): $E(U_{i+1}(f,T)-U_i(f\circ\Phi_T,T)\mid\mathcal F_{(i-1)T})\to0$ almost surely;
Eq. (52): $\frac1n\sum_{i=1}^nU_{i+1}(f,T)-\frac1n\sum_{i=1}^nU_i(f\circ\Phi_T,T)\to0$ almost surely;
Eq. (53): for a single measurable path whose occupation measures converge weakly to $\mu$ along $t_j\to\infty$ , the averages $\frac1{n_jT}\sum_{i=0}^{n_j-1}\int_{iT}^{(i+1)T}f(x_s)\,ds$ with $n_j=\lfloor t_j/T\rfloor$ converge to $\int f\,d\mu$ for every bounded continuous $f$ .

Significance

The result. Theorem 10.1 locates the long-run statistics of a stochastic process that only shadows a deterministic semiflow in conditional probability. When the occupation measures are tight, for example when the path has compact closure, $\mathcal M(X,\omega)$ is nonempty, and the theorem restricts where the process spends its time to the supports of invariant measures. Right after the theorem the notes define the minimal center of attraction of the process from the supports of the measures in $\mathcal M(X,\omega)$ ; the conclusion applies to processes, such as slowly decreasing step-size algorithms, for which the pathwise limit-set theorem of Section 5 is not available.

Formalizing it. The theorem has a complete published proof. No machine-checked version of it, of weak asymptotic pseudotrajectories, or of occupation-measure limit theorems for continuous-time processes is known to exist. The mission produces a formal definition of progressively measurable weak asymptotic pseudotrajectories, occupation measures of measurable paths and their weak limit points, and a proof that combines a martingale law of large numbers in discrete time with weak convergence in $\mathcal P(M)$ .

Difficulty

The obvious route is to apply the pathwise argument for asymptotic pseudotrajectories along each path. It fails, because condition 2 controls only conditional probabilities: the deviation events may occur infinitely often along almost every path while their conditional probabilities tend to zero. The proof therefore has to work with averages and conditional expectations instead of with individual paths: a strong law of large numbers for bounded martingale differences transfers conditional statements to time averages, and this must be done for one test function and one horizon at a time. Passing from countably many test functions to invariance requires a countable family of uniformly continuous functions that determines weak convergence on the separable space $M$ , and the a.s. sets must be intersected over that family and over rational horizons. Measurability is a second difficulty: paths are not assumed continuous, so the integrals, suprema and conditional expectations involved must be shown to be well defined from progressive measurability alone.

Formalization scope

Time is $\mathbb R_{\ge0}$ ; the semiflow is Mathlib's Flow ℝ≥0 M; the filtration is a Filtration ℝ≥0; $\mathcal P(M)$ is ProbabilityMeasure M with its topology of weak convergence. $M$ is a separable metric space with its Borel $\sigma$ -algebra; it is not assumed compact, complete or Polish. Progressive measurability is stated literally for every $T>0$ . The conditional probability in condition 2 is the conditional expectation of the indicator of the deviation event, which is required to be measurable (the paper's $P\{\cdot\mid\mathcal F_t\}$ presupposes an event); the supremum over $h\in[0,T]$ is taken in $[0,\infty]$ . Invariance for the semiflow is $(\Phi_t)_*\mu=\mu$ for all $t\ge0$ , the form the proof establishes; for a flow it agrees with the definition $\mu(A)=\mu(\Phi_t(A))$ of Section 8.3. Weak limit points are cluster points of $t\mapsto\mu_t(\omega)$ as $t\to\infty$ ; the occupation measure is a genuine probability measure for every measurable path and $t>0$ .

The following formalizations would trivialize the statement and are excluded by the definitions: an "occupation measure" equal to the zero measure for a non-measurable path; a conditional probability of a non-measurable event, which Lean evaluates to $0$ and which would make condition 2 vacuous; invariance defined through images $\Phi_t(A)$ , which need not be Borel for a semiflow; and a compactness or Polish assumption on $M$ , which the theorem does not make.

A complete development needs: Fubini-type measurability for progressively measurable processes, square-integrable martingale convergence and Kronecker's lemma (both largely in Mathlib), conditional expectations of time integrals, a convergence-determining countable family of uniformly continuous functions on a separable metric space, and the identification of weak convergence with convergence of integrals of bounded continuous functions. The martingale law of large numbers (Eqs. (47), (50)) and Eq. (53) are reusable outside this mission. Proofs of any milestone, and alternative arguments for the goal, are welcome.

Selected references

M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. Section 10, Theorem 10.1, pp. 60–63. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617

10 thms2 active usersReviewed

Completed

Dynamical Systems Operations Research·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 1: Limit Sets of Precompact Asymptotic Pseudotrajectories Are Internally Chain TransitiveResearch Paper

Motivation

A stochastic approximation algorithm updates an estimate by small noisy steps, $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$ , with step sizes $\gamma_n\to0$ and noise $U_n$ . Such recursions underlie stochastic gradient descent, adaptive control, reinforcement learning (Q-learning, temporal-difference methods) and learning in games (fictitious play, reinforcement models). The ODE method compares the long-run behaviour of the algorithm with that of the ordinary differential equation $\dot x=F(x)$ . Classical versions of this comparison (Ljung 1977, Kushner and Clark 1978) assume the ODE has a globally asymptotically stable equilibrium, or a Lyapunov function, and cannot describe algorithms whose ODE has periodic orbits, heteroclinic cycles or chaotic sets.

Benaïm and Hirsch (1996) replaced these special assumptions by a single dynamical statement: the interpolated algorithm is an asymptotic pseudotrajectory of the flow of $F$ , and the limit set of every precompact asymptotic pseudotrajectory is internally chain transitive. This mission formalizes that limit set theorem as it is presented in Michel Benaïm's lecture notes Dynamics of Stochastic Approximation Algorithms (Séminaire de Probabilités XXXIII, 1999).

Timeline. Bowen (1975) and Conley (1978) introduced $(\delta,T)$ -pseudo-orbits and chain recurrence, and Conley proved that the chain recurrent set of a flow on a compact space is internally chain recurrent. Benaïm (1996, SIAM J. Control Optim.) related limit sets of stochastic approximation processes to the chain recurrence of the ODE; Benaïm and Hirsch (1996) introduced asymptotic pseudotrajectories for semiflows on metric spaces and proved the limit set theorem in the form formalized here. The 1999 notes give a self-contained proof through the translation semiflow on a space of curves.

Setting

Let $(M,d)$ be a metric space. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$ , $(t,x)\mapsto\Phi_t(x)$ , with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$ . A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$ ; then $\Phi|A$ denotes the restricted semiflow on $A$ .

A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory of $\Phi$ if

\lim_{t\to\infty}\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)=0\quad\text{for every }T>0,

and it is precompact if $X(\mathbb R_+)$ has compact closure. Its limit set is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$ .

For $\delta>0$ , $T>0$ , a $(\delta,T)$ -pseudo-orbit from $a$ to $b$ consists of $k\ge1$ partial trajectories, given by points $y_0,\dots,y_{k-1}$ (and an endpoint $y_k$ ) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$ , $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$ , and $y_k=b$ . One writes $a\hookrightarrow b$ if such pseudo-orbits exist for all $\delta,T>0$ . A nonempty compact invariant set $\Lambda$ is internally chain transitive if $a\hookrightarrow b$ for the restricted semiflow $\Phi|\Lambda$ for all $a,b\in\Lambda$ , so that all $y_i$ lie in $\Lambda$ ; it is internally chain recurrent if $a\hookrightarrow a$ for $\Phi|\Lambda$ for every $a\in\Lambda$ . An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ such that $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly in $x\in W$ .

Formalization targets

Goal: Theorem 5.7 (i)

For every semiflow $\Phi$ on a metric space $M$ and every precompact asymptotic pseudotrajectory $X$ of $\Phi$ ,

L(X)\ \text{is internally chain transitive.}

Milestones (in the order of the proof)

Lemma 3.1. $X$ is an asymptotic pseudotrajectory iff $d(\Theta^t(X),\hat\Phi\circ\Theta^t(X))\to0$ , where $\Theta$ is the translation semiflow on $C^0(\mathbb R_+,M)$ and $\hat\Phi(Y)=\Phi^{Y(0)}$ .
Theorem 3.2. For precompact continuous $X$ : $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of $\Theta^{t}(X)$ , $t\to\infty$ , is a trajectory of $\Phi$ ; and then $\{\Theta^t(X)\}_{t\ge0}$ is relatively compact.
Lemma 5.2. A nonempty open $U$ with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$ contains an attractor whose basin contains $\overline U$ .
Proposition 5.3. For nonempty $\Lambda$ : internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact, invariant and $\Phi|\Lambda$ has no proper attractor.
Theorem 5.5. On a nonempty compact $M$ , the chain recurrent set $R(\Phi)$ is internally chain recurrent.
Corollary 5.6. If $\overline{\gamma^+(x)}$ is compact, then $\omega(x)$ is internally chain transitive.

Significance

The result. Theorem 5.7 (i) is the bridge between probability and dynamics in the ODE method. Once a stochastic approximation process is shown to be an asymptotic pseudotrajectory (missions 2 to 4 of this series do that under martingale-noise conditions), every statement about its limit points becomes a statement about internally chain transitive sets of the ODE: convergence to equilibria when a Lyapunov function exists (Proposition 6.4), convergence to attractors with positive probability (Theorem 7.3), and the analysis of learning dynamics in games. The theorem is sharp in the sense that every internally chain transitive set is a limit set of some asymptotic pseudotrajectory (Theorem 5.7 (ii), proved in Benaïm and Hirsch 1996 and not part of this mission).

Formalizing it. The result is proved in the literature; it is not formalized. Mathlib has semiflows (Flow), omega limit sets and the compact-open topology, but no pseudo-orbits, chain recurrence, Conley's theory of attractors, or asymptotic pseudotrajectories. This mission produces that layer for semiflows on general metric spaces, which is reusable for any later formalization of the ODE method, of Conley theory, or of learning in games.

Difficulty

The obvious approach follows $X$ from a point $a\in L(X)$ to a point $b\in L(X)$ : $X$ returns near $a$ and near $b$ infinitely often, and on windows of length $T$ it is close to a trajectory, so concatenating windows gives a pseudo-orbit. The pseudo-orbit obtained this way has its points on the curve $X$ , not in $L(X)$ ; this only shows that $L(X)$ is chain transitive for $\Phi$ on $M$ , a strictly weaker property. Producing pseudo-orbits whose points lie in $L(X)$ itself is the central difficulty, and it is where precompactness of $X$ is used. Invariance $\Phi_t(L(X))=L(X)$ , with equality, also needs a compactness argument, since a semiflow is not invertible.

Formalization scope

A semiflow is Mathlib's Flow ℝ≥0 M on a [MetricSpace M]; $M$ is arbitrary, with no compactness, completeness or local compactness. Time is ℝ≥0. Curves are functions ℝ≥0 → M; continuity is part of being an asymptotic pseudotrajectory, and precompactness is IsCompact (closure (Set.range X)). Invariance is equality $\Phi_t(A)=A$ . Internally chain recurrent and internally chain transitive sets are nonempty by definition, and their pseudo-orbits are those of the restricted semiflow on the subtype $\Lambda$ , so every point of the pseudo-orbit lies in $\Lambda$ . Attractors converge uniformly on a neighbourhood. Lemma 3.1 and Theorem 3.2 are stated on $C^0(\mathbb R_+,M)$ (C(ℝ≥0, M), compact-open topology) with the half-line distance; the notes write $C^0(\mathbb R,M)$ , but with the convention $\Phi^p(t)=p$ for $t<0$ that version fails for semiflows (a periodic trajectory is a counterexample), and the notes themselves describe asymptotic pseudotrajectories as points of $C^0(\mathbb R_+,M)$ .

Ruled out: pseudo-orbits with no trajectory piece ( $k=0$ ), pseudo-orbits allowed to leave $L(X)$ , invariance as mere inclusion $\Phi_t(A)\subset A$ , and any compactness assumption on $M$ . Each of these makes the goal weaker than the theorem of the notes.

A complete development needs: elementary properties of pseudo-orbits (concatenation, continuity estimates), Arzelà–Ascoli on C(ℝ≥0, M), Conley's attractor construction, and the conjugacy between $\Phi$ and the translation semiflow on $S_\Phi$ . Proofs of the milestones, alternative direct proofs of the goal (Benaïm 1996), and reusable lemmas about chain recurrence for Flow are all welcome.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

12 thms2 active usersReviewed

Completed

Dynamical Systems Operations Research·Captain: mikedeng1

Dynamics of Stochastic Approximation Algorithms 2: Under A1 and A2 the Interpolated Process Is an Asymptotic Pseudotrajectory of the Flow of FResearch Paper

Motivation

A stochastic approximation algorithm is a recursion

x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)

in $\mathbb R^d$ , driven by a vector field $F$ , decreasing step sizes $\gamma_n$ and perturbations $U_n$ . Robbins–Monro root finding, stochastic gradient descent, adaptive filters, learning dynamics in games (fictitious play, reinforcement learning) and urn models all have this form. The ODE method, introduced by Ljung (1977) and developed by Kushner and Clark (1978), Métivier and Priouret (1987) and Kushner and Yin (1997), studies such a recursion by comparing it with the differential equation $\dot x=F(x)$ .

Benaïm and Hirsch (1996) gave the comparison a dynamical form: the continuous-time interpolation of $\{x_n\}$ is an asymptotic pseudotrajectory of the flow of $F$ . Proposition 4.1 of Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) states that deterministic comparison theorem under two assumptions: a noise condition (A1) and either bounded iterates (A2) or a Lipschitz, bounded vector field near the iterates (A2′). The notes then verify A1 almost surely for martingale noise (Propositions 4.2 and 4.4) and use the asymptotic pseudotrajectory property to describe limit sets, attractors and nonconvergence.

Setting

Let $F:\mathbb R^d\to\mathbb R^d$ be continuous. It is globally integrable if through every point there is exactly one integral curve $y:\mathbb R\to\mathbb R^d$ , $\dot y=F(y)$ ; the flow $\Phi_t(p)$ is the value at time $t$ of the integral curve through $p$ .

The step sizes satisfy $\gamma_n\ge0$ , $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ . Set $\tau_0=0$ , $\tau_n=\sum_{i=1}^n\gamma_i$ , and $m(t)=\sup\{k\ge0:\tau_k\le t\}$ . The affine interpolated process $X:\mathbb R_+\to\mathbb R^d$ and the piecewise constant processes $\overline X,\overline U,\bar\gamma$ are, for $0\le s<\gamma_{n+1}$ ,

X(\tau_n+s)=x_n+s\,\frac{x_{n+1}-x_n}{\gamma_{n+1}},\qquad \overline X(\tau_n+s)=x_n,\quad \overline U(\tau_n+s)=U_{n+1},\quad \bar\gamma(\tau_n+s)=\gamma_{n+1}.

The noise enters through

\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\overline U(s)\,ds\Big\| .

A1: for every $T>0$ , $\sup\{\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\|:n<k\le m(\tau_n+T)\}\to0$ as $n\to\infty$ ; equivalently $\Delta(t,T)\to0$ as $t\to\infty$ .
A2: $\sup_n\|x_n\|<\infty$ .
A2′: $F$ is Lipschitz and bounded on a neighbourhood of $\{x_n\}$ .

A continuous $X:\mathbb R_+\to\mathbb R^d$ is an asymptotic pseudotrajectory of $\Phi$ if for every $T>0$

\lim_{t\to\infty}\sup_{0\le h\le T}\big\|X(t+h)-\Phi_h(X(t))\big\|=0 .

Formalization targets

Goal: Proposition 4.1

F\ \text{continuous, globally integrable},\quad \text{A1},\quad \text{A2 or A2}'\quad\Longrightarrow\quad X\ \text{is an asymptotic pseudotrajectory of}\ \Phi .

No rate and no constant appear; the statement holds under either alternative.

Milestones

Eq. (9): $X(t)-X(0)=\int_0^t[F(\overline X(s))+\overline U(s)]\,ds$ .
A1: the discrete and the continuous forms of A1 are equivalent, for each $T>0$ .
Theorem 3.2: for a flow on a metric space and a continuous $X$ with relatively compact image, $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of the translates $\Theta^t(X)$ in $C^0(\mathbb R,M)$ is a trajectory of the flow; both imply that $\{\Theta^t(X)\}$ is relatively compact.
Comparison of $X$ and $\overline X$ (p. 13): if $\|F(x_n)\|\le K$ , then for $t$ large, $\sup_{t\le u\le t+T}\|X(u)-\overline X(u)\|\le2\Delta(t-1,T+1)+\sup_{t\le u\le t+T}K\bar\gamma(u)$ .
Estimate (11): under A1 and A2′, for $t$ large,

\sup_{0\le h\le T}\|X(t+h)-\Phi_h(X(t))\|\le C(T)\Big[\Delta(t-1,T+1)+\sup_{t\le s\le t+T}\bar\gamma(s)\Big],

with $C(T)$ depending only on $T$ and on $F$ (through its Lipschitz constant and bound on the neighbourhood).

Significance

Proposition 4.1 separates the dynamics of a stochastic approximation algorithm from its noise. Any noise condition implying A1 almost surely (Propositions 4.2 and 4.4 of the notes for $L^q$ -bounded and subgaussian martingale differences) combines with it to give: almost every sample path, after interpolation, is an asymptotic pseudotrajectory of $\dot x=F(x)$ . The limit set theorem (Theorem 5.7: limit sets are internally chain transitive), the Lyapunov-function criterion (Proposition 6.4) and the attractor results (Section 7) then apply path by path. Estimate (11) gives the quantitative version used for rates.

The result is proved in the notes, building on Benaïm and Hirsch (1996). No machine-checked proof of it, or of the asymptotic pseudotrajectory framework, is known to exist. A formal proof would supply a checked bridge between discrete recursions with step sizes and flows of vector fields, which every ODE-method convergence proof crosses.

Difficulty

The obvious argument compares $X$ directly with the flow by Gronwall's inequality. It needs $F$ Lipschitz along both the interpolated path and the flow line, which holds under A2′ but not under A2, where $F$ is only continuous and solutions are unique without any Lipschitz bound. Under A2 the comparison must go through compactness instead: equicontinuity of the translates, identification of every limit point as an integral curve, and uniqueness of integral curves. The last step is where global integrability is used, and it cannot be replaced by a quantitative estimate.

Under A2′ the iterates may be unbounded, so no compactness is available, and the path and the flow line must be kept inside the region where $F$ is controlled for the whole window $[t,t+T]$ .

Formalization scope

Space $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); time is ℝ≥0 for the pseudotrajectory and ℝ inside integrals. Sequences are ℕ → · with the paper's indices; $\gamma_0$ and $U_0$ are unused.
$m(t)$ is the largest $k$ with $\tau_k\le t$ , so the divisor $\gamma_{m(t)+1}$ is positive even when some steps vanish.
Limits are written with $\varepsilon$ ; the suprema that remain ( $\Delta$ , $\sup\bar\gamma$ ) are over bounded nonempty sets, and $\overline U$ is a step function with finitely many pieces on bounded intervals, so no integral or supremum takes a default value.
The flow of $F$ is a function satisfying the integral-curve property, together with global integrability (existence and uniqueness of integral curves on $\mathbb R$ ); continuity of the flow is not assumed.
A2′ is read with a uniform neighbourhood: $F$ is Lipschitz and bounded on $\{y:\operatorname{dist}(y,\{x_n\})<r\}$ for some $r>0$ . Under the reading "some open set containing $\{x_n\}$ " the proposition fails for unbounded iterates.
Theorem 3.2 is stated for flows on $C^0(\mathbb R,M)$ (compact-open topology); for semiflows with the convention $\Phi^p(t)=p$ for $t<0$ , the implication (i)⇒(ii) is false as printed.

Trivializing formalizations are ruled out: the goal keeps both alternatives A2 and A2′ (neither a global Lipschitz condition nor bounded iterates is assumed in place of the disjunction), $X$ is the explicit piecewise affine interpolation rather than any curve with the desired property, and the constant in (11) is fixed before the sequences, so it cannot depend on the run.

A complete development needs Gronwall's inequality (in Mathlib), Arzelà–Ascoli on $C^0(\mathbb R,M)$ , continuous dependence of solutions on initial data under uniqueness (Kamke's theorem, not in Mathlib), and interval integrals of step functions. The asymptotic pseudotrajectory definitions and Theorem 3.2 are reusable for the other missions on these notes. Proofs of individual milestones are welcome; Eq. (9) and the comparison of $X$ and $\overline X$ are the natural entry points.

Selected references

M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probab. Theory Related Fields 74 (1987), 403–428. https://doi.org/10.1007/BF00699098
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
L. Ljung, Analysis of recursive stochastic algorithms, IEEE Trans. Automat. Control 22 (1977), 551–575. https://doi.org/10.1109/TAC.1977.1101561

9 thms2 active usersReviewed

Control Theory Mechanism Design Operations Research·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 2: The Producer's First-Best Value in Closed FormResearch Paper

Motivation

Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.

The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.

The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.

Setting

Fix integers $N,d\ge0$ (usages for the mean effort and for the volatility effort), cost parameters $\mu\in(0,\infty)^N$ , $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $0<\varepsilon\le1$ , risk aversions $r,p>0$ , a marginal volatility cost $h>0$ , slopes $\kappa,\theta\in\mathbb R$ , a horizon $T>0$ , an initial consumption $X_0\in\mathbb R$ and a reservation utility $R_0<0$ .

The consumer chooses a mean effort $\alpha$ with values in $A=\prod_i[0,\mu_iA_{\max}]$ and a responsiveness effort $\beta$ with values in $B=[\varepsilon,1]^d$ , at cost

c(\alpha,\beta)=c_1(\alpha)+\tfrac12c_2(\beta),\qquad c_1(a)=\tfrac12\sum_i\frac{a_i^2}{\mu_i},\qquad c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}\big(b_j^{-1}-1\big).

The consumption $X$ follows $X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s$ with $\sigma(b)=(\sigma_1\sqrt{b_1},\dots,\sigma_d\sqrt{b_d})$ , in the weak sense: $X$ is the canonical process on $C([0,T],\mathbb R)$ , and an admissible pair $(\nu,\mathbb P)$ is a progressively measurable control $\nu=(\alpha,\beta)$ with a probability measure under which $X$ starts at $X_0$ and solves the associated martingale problem.

The consumer values consumption by $f(x)=\kappa x$ and the producer bears the generation cost $g(x)=\theta x$ ; write $\delta=\kappa-\theta$ . For a payment $\xi$ made at time $T$ , the consumer's and the producer's criteria are

J_A=\mathbb E^{\mathbb P}\Big[-e^{-r\left(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds\right)}\Big],\qquad J_P=\mathbb E^{\mathbb P}\Big[-e^{-p\left(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T\right)}\Big].

A contract is an $\mathcal F_T$ -measurable $\xi$ with uniform exponential moments (2.5). The first-best value is

V^{FB}=\sup\big\{J_P(\xi,\nu,\mathbb P):\ \xi\text{ a contract},\ (\nu,\mathbb P)\text{ admissible},\ J_A(\xi,\nu,\mathbb P)\ge R_0\big\}.

The consumer's Hamiltonians are $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ . Finally $\rho=\frac{rp}{r+p}$ , $L_0=-\frac1r\log(-R_0)$ , $U(x)=-e^{-px}$ , $\bar\mu=\sum_i\mu_i$ and $x^-=\max(0,-x)$ .

Formalization targets

Goal: Proposition 3.1 (i)

Assume $\delta^-T\le A_{\max}$ . Then

V^{FB}=U\big(\bar v(0,X_0)-L_0\big),\quad \bar v(0,X_0)=\delta TX_0+\int_0^T\Big(\tfrac12\bar\mu(\delta^-)^2(T-t)^2+H_v\big(-h-\rho\delta^2(T-t)^2\big)\Big)dt.

Milestones

Proposition 2.1. The best responses $\hat a(z)$ , $\hat b(\gamma)$ attain the infima defining $H_m$ , $H_v$ , and these Hamiltonians have explicit closed forms.
(A.5). The auxiliary value $\bar V=\sup_{(\nu,\mathbb P)}\mathbb E^{\mathbb P}\big[-e^{-\rho(\int_0^T(\delta X_t-c(\nu_t))dt-\frac h2\langle X\rangle_T)}\big]$ is finite and negative, and $V^{FB}=R_0(\bar V/R_0)^{1+p/r}$ .
Proposition A.3 (i), with the explicit solution of p. 28.

\bar V=-e^{-\rho\left(\delta TX_0+\int_0^T\bar m(t)dt\right)},\qquad \bar m(t)=H_m(\delta(T-t))+H_v\big(-h-\rho\delta^2(T-t)^2\big).

Significance

The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy $\delta$ through the mean-effort term, on the volatility cost $h$ and the effective risk aversion $\rho$ through the volatility Hamiltonian, and on the reservation utility only through the shift by $L_0$ . It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.

The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.

Difficulty

The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of $\bar V$ into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on $\langle X\rangle_T$ ; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on $\bar V$ must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.

Formalization scope

The canonical space is $C([0,T],\mathbb R)$ with the coordinate σ-algebra and the canonical filtration; processes are indexed by $[0,T]$ . Admissible pairs are given by a martingale problem: $X_0=X_0$ almost surely, and both $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are martingales. In the criteria, $\langle X\rangle_T$ is replaced by its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ ; a contract remains any $\mathcal F_T$ -measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in $[-\infty,0]$ , and every value is an extended-real supremum with $\sup\emptyset=-\infty$ . $B$ is read as $[\varepsilon,1]^d$ , with indices in Fin N and Fin d.

The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: $\varepsilon\le1$ (so $B\ne\emptyset$ ), $R_0<0$ (so $L_0$ is defined), and, for the goal only, $\delta^-T\le A_{\max}$ , without which the printed $\frac12\bar\mu(\delta^-)^2(T-t)^2$ exceeds $H_m(\delta(T-t))$ and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of $H_m$ in Proposition 2.1 is false for $z^->A_{\max}$ and is replaced by $\bar\mu(m z^--m^2/2)$ with $m=z^-\wedge A_{\max}$ ; the index range of $\hat b$ is $j=1,\dots,d$ ; on p. 28, $\int_0^t\bar m$ is $\int_t^T\bar m$ and "(A.11)" is (A.6).

The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal electricity demand response contracting with responsiveness incentives, arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022. https://arxiv.org/abs/1810.09063
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance Stoch. 22, 2018. https://arxiv.org/abs/1510.07111
B. Holmström, P. Milgrom, Aggregation and linearity in the provision of intertemporal incentives, Econometrica 55, 1987. https://doi.org/10.2307/1913238
Y. Sannikov, A continuous-time version of the principal–agent problem, Rev. Econ. Stud. 75, 2008. https://doi.org/10.1111/j.1467-937X.2007.00463.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §5.4 (martingale problems and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Control Theory Mechanism Design Operations Research·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 1: The Producer's Second-Best Value in Closed FormResearch Paper

Motivation

Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.

Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.

Setting

Fix integers $N,d\ge0$ , cost parameters $\mu\in(0,\infty)^N$ and $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $\varepsilon\in(0,1]$ , risk aversions $r,p>0$ , a marginal cost of volatility $h>0$ , marginal energy value $\kappa$ and cost $\theta$ with $\delta:=\kappa-\theta$ , a horizon $T>0$ , an initial consumption $X_0$ and a reservation utility $R_0<0$ . Write $\bar\mu:=\sum_i\mu_i$ and $x^-:=\max(0,-x)$ .

Consumption. $X$ is the canonical process on $\Omega=C([0,T],\mathbb R)$ with its natural filtration $\mathbb F$ . A control $\nu=(\alpha,\beta)$ is progressively measurable, with $\alpha_t\in A:=\prod_i[0,\mu_iA_{\max}]$ (effort to reduce consumption) and $\beta_t\in B:=[\varepsilon,1]^d$ (effort to reduce volatility). Under $\nu$ the consumption follows, in the weak sense,

X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s,\qquad |\sigma(b)|^2=\sum_j\sigma_j^2b_j .

Effort costs $c(\nu)=c_1(\alpha)+\frac12c_2(\beta)$ per unit time, with $c_1(a)=\frac12\sum_ia_i^2/\mu_i$ and $c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}(b_j^{-1}-1)$ .

Criteria. For a payment $\xi$ at time $T$ , the consumer's criterion is $J_A=\mathbb E[-e^{-r(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds)}]$ and the producer's is $J_P=\mathbb E[U(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T)]$ with $U(x)=-e^{-px}$ . Contracts $\mathcal C$ are the $\mathcal F_T$ -measurable $\xi$ with exponential moments of order $m>1$ uniformly over the consumer's responses (2.5). The consumer's value is $V_A(\xi)=\sup J_A$ , and $\mathcal P^\star(\xi)$ is the set of his optimal responses.

Second best. The producer offers $\xi$ , the consumer responds optimally, ties are broken in the producer's favour, and participation requires $V_A(\xi)\ge R_0$ :

V^{SB}:=\sup_{\xi\in\mathcal C,\ V_A(\xi)\ge R_0}\ \sup_{\mathcal P^\star(\xi)}J_P(\xi,\cdot),\qquad\sup\emptyset=-\infty .

Hamiltonians. $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ .

Formalization targets

Goal: Proposition 3.2 (i)

Assume $\delta^-T\le A_{\max}$ . With $q_t(z)=h+rz^2+p(z-\delta(T-t))^2$ , $L_0=-\frac1r\log(-R_0)$ ,

m_{SB}(t)=\frac12\bar\mu\delta^2(T-t)^2-\frac12\inf_{z\in\mathbb R}\Big\{\bar\mu\big(z^-+\delta(T-t)\big)^2-2H_v\big(-q_t(z)\big)\Big\},

V^{SB}=U\big(v(0,X_0)-L_0\big),\qquad v(0,X_0)=\delta TX_0+\int_0^Tm_{SB}(s)\,ds .

Milestones

Proposition 2.1. The consumer's best responses $\hat a_i(z)=\mu_i(z^-\wedge A_{\max})$ and $\hat b_j(\gamma)=(1\wedge(\lambda_j\gamma^-)^{-1/2})\vee\varepsilon$ attain the infima defining $H_m$ and $H_v$ , and

H_m(z)=\bar\mu\big(m z^--\tfrac{m^2}2\big),\ m=z^-\wedge A_{\max};\qquad H_v(\gamma)=-\tfrac12\big(\hat c_2(\gamma)-\gamma|\hat\sigma(\gamma)|^2\big).

Lemma A.1. With $f_0(q,\gamma)=q|\hat\sigma(\gamma)|^2+\hat c_2(\gamma)$ , $F_0(q):=\inf_{\gamma\le0}f_0(q,\gamma)=f_0(q,-q)=-2H_v(-q)$ , and $F_0$ is non-decreasing.
Proposition A.4 (ii). A minimiser of $z\mapsto F_0(h-k+rz^2+p(z-y)^2)+\bar\mu(z^-+y)^2$ is $\frac p{r+p}y$ when $y\ge0$ , and lies in $[y,\frac p{r+p}y]$ when $y\le0$ .

A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates $z_{SB}(t)=\frac p{r+p}\delta(T-t)$ and $\gamma_{SB}(t)=-h-\frac{rp}{r+p}\delta^2(T-t)^2$ when $\delta\ge0$ .

Significance

The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.

The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.

Difficulty

The deterministic milestones are calculus on boxes. The goal is not. The upper bound $V^{SB}\le U(v(0,X_0)-L_0)$ must hold for every $\mathcal F_T$ -measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every $\xi\in\mathcal C$ inducing an optimal response can be written as $Y_T^{y_0,Z,\Gamma}$ , an integral against $dX$ and $d\langle X\rangle$ driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.

Formalization scope

All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:

Weak formulation. An admissible pair $(\nu,\mathbb P)$ is a control and a probability measure on $C([0,T],\mathbb R)$ with $X_0=X_0$ a.s., under which $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are $\mathbb F$ -martingales. This is the martingale problem equivalent to weak solutions of (2.1); the paper deliberately leaves weak solutions informal (footnote 2). The pair, not the law alone, is the admissible object, because the cost depends on $\nu$ .
Quadratic variation. $\langle X\rangle_T$ in $J_P$ is its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ .
Values. Expected utilities are negated lower Lebesgue integrals, in $[-\infty,0]$ ; all suprema are in the extended reals, so the empty supremum is $-\infty$ , as on p. 9.
Hamiltonians are defined by their infima, not by the closed forms of Proposition 2.1.
Indices are Fin N, Fin d; $N=0$ , $d=0$ are allowed. $\hat b_j(\gamma)=1$ when $\lambda_j\gamma^-\le1$ (the paper's $0^{-1/2}=+\infty$ ).
Added hypotheses. $\varepsilon\le1$ ( $B\neq\emptyset$ ), $R_0<0$ ( $\log(-R_0)$ defined), and for the goal $\delta^-T\le A_{\max}$ . The paper's closed form is computed with the effort cap removed (" $\eta_A\to0$ as $A\nearrow\infty$ ", p. 30), and with the capped effort of the model it is correct exactly under this hypothesis.
Corrected misprints. $-2H_m(-q(z))$ in $m_{SB}$ is read as $-2H_v(-q(z))$ ; with $H_m$ the infimum is $-\infty$ . The printed $H_m(z)=\frac12\bar\mu(z^-\wedge A_{\max})^2$ is false for $z^->A_{\max}$ and is corrected. " $j=1,\dots,N$ " for $\hat b$ means $j=1,\dots,d$ . In Proposition A.4 (ii) the open interval becomes closed, and "for large $A$ " is read as $\eta_A\equiv0$ .

The goal is an equality of extended reals between $V^{SB}$ , defined from the model, and an explicit real number. A formalization that defines $V^{SB}$ over a restricted class of contracts, or with a real-valued supremum that returns $0$ on unbounded sets, would trivialize or change it and is not the goal.

Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal Electricity Demand Response Contracting with Responsiveness Incentives, arXiv:1810.09063v3, 2019; Mathematics of Operations Research 47 (2022). https://arxiv.org/abs/1810.09063v3
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance and Stochastics 22 (2018) 1–37. https://doi.org/10.1007/s00780-017-0344-4
B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987) 303–328. https://doi.org/10.2307/1913238
Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008) 957–984. https://doi.org/10.1111/j.1467-937X.2008.00486.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer 1991, §5.4 (martingale problem and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Completed

Markov Chain Numerical Analysis Operations Research+1·Captain: mikedeng1

Fundamentals of Queueing Theory X: Uniformization of Continuous-Time Markov ChainsTextbook

Motivation

Most Markovian queueing models have no closed-form transient solution. The M/M/1 queue already needs modified Bessel functions (Chapter 2 of the book), and a finite-capacity or multi-class model with state-dependent rates has no closed form at all. What an analyst can always write down is the system of forward equations $p'(t)=p(t)Q$ for the state probabilities. Chapter 8 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), presents two numerical techniques that turn such models into numbers: the randomization (or uniformization) method for the transient distribution of a finite continuous-time Markov chain, and the Fourier-series method for inverting a Laplace transform, as needed for the M/G/1 waiting-time transform (5.33) and the busy-period transform (5.37).

Uniformization goes back to Jensen (1953) and is the standard transient solver in performance-evaluation and reliability tools. Its appeal is that it replaces a matrix exponential, which is numerically delicate, by powers of a stochastic matrix weighted by Poisson probabilities, with an error bound that can be fixed before the computation starts (Grassmann 1977; Gross and Miller 1984). The Fourier-series method with Euler summation is due to Abate and Whitt (Abate and Whitt 1992; Abate, Choudhury and Whitt 1999).

Setting

A continuous-time Markov chain $X(t)$ on the states $\{0,1,\dots,N\}$ is described by its infinitesimal generator $Q=(q_{ij})$ : for $i\ne j$ , $q_{ij}\ge0$ is the rate of jumps from $i$ to $j$ , and the diagonal entry is $-q_i$ with

q_i=\sum_{j\ne i}q_{ij},\qquad i=0,1,\dots,N.

The transient state-probability vector $p(t)=(p_0(t),\dots,p_N(t))$ , $p_n(t)=\Pr\{X(t)=n\}$ , is the solution of the forward equations

p'(t)=p(t)Q\quad(t\ge0),

started from a given probability vector $p(0)$ . Fix a constant $\Lambda>0$ with $\Lambda\ge q_i$ for every $i$ (the book takes $\Lambda=\max_i q_i$ ) and define the uniformized matrix

\tilde P=\frac{Q}{\Lambda}+I,\qquad \tilde p_{in}=\begin{cases}q_{in}/\Lambda&(i\ne n),\\1-q_i/\Lambda&(i=n).\end{cases}

It is the transition matrix of a discrete-time chain $Y_k$ : the state of $X$ after the $k$ -th event of a Poisson process of rate $\Lambda$ that has been thinned. Write $\phi^{(k)}=p(0)\tilde P^{k}$ for its distribution after $k$ steps.

For the second half of the chapter, the Laplace transform of a real function $f$ on $[0,\infty)$ is $\bar f(s)=\int_0^\infty e^{-st}f(t)\,dt$ , and the Fourier-series approximant with parameter $A$ is

f_{A,n}(t)=\frac{e^{A/2}}{2t}\Big[\bar f\Big(\frac{A}{2t}\Big)+2\sum_{k=1}^{n}(-1)^k\,\mathrm{Re}\,\bar f\Big(\frac{A+2k\pi i}{2t}\Big)\Big],

with $f_A(t)=\lim_{n\to\infty}f_{A,n}(t)$ .

Formalization targets

Goal: the randomization formula with its truncation bound (Eqs. (8.9)–(8.12))

The forward equations have a solution, and every solution satisfies, for all $t\ge0$ ,

p(t)=\sum_{k=0}^{\infty}p(0)\tilde P^{(k)}\,\frac{e^{-\Lambda t}(\Lambda t)^k}{k!},

and whenever $\sum_{k=0}^{T}e^{-\Lambda t}(\Lambda t)^k/k!>1-\epsilon$ , every component of the sum truncated at $k=T$ is within $\epsilon$ of $p_n(t)$ .

Milestones

Eq. (8.12): $\tilde P$ has the entries above and is a stochastic matrix.
Eqs. (8.13)–(8.14): $\phi^{(k)}=\phi^{(k-1)}\tilde P$ and each $\phi^{(k)}$ is a probability vector.
p.385: $\phi=\phi\tilde P\iff0=\phi Q$ .
Eqs. (8.27)–(8.28): for bounded Lipschitz $f$ , $A>0$ and $t>0$ ,

f_A(t)-f(t)=\sum_{k=1}^{\infty}e^{-kA}f\big((2k+1)t\big),\qquad |f_A(t)-f(t)|\le\frac{Ce^{-A}}{1-e^{-A}}\ \text{ if } |f(x)|\le C \text{ for } x>3t.

The mission also contains Eqs. (8.7)–(8.8) as a further theorem, outside the milestone list: the transition probabilities satisfy $p_{in}(t)=\sum_k\tilde p^{(k)}_{in}e^{-\Lambda t}(\Lambda t)^k/k!$ , and $p_n(t)=\sum_i p_i(0)p_{in}(t)$ .

Significance

The randomization formula reduces the transient analysis of any finite Markovian queue (finite-buffer, multi-server, with balking, reneging or state-dependent rates) to repeated vector–matrix products with a sparse stochastic matrix. The truncation point is chosen from a Poisson tail alone, independently of $Q$ . Milestone 3 shows that the same matrix gives the stationary equations, so one iteration serves both transient and steady-state computation. The discretization identity (8.27) is what justifies the parameter choice in Algorithm 8.1: the error decays like $e^{-A}$ .

All of these results are classical and proved in the literature. None of them is formalized in Lean or Mathlib as far as a search of the platform and Mathlib shows. Mathlib has the matrix exponential and Poisson summation under decay hypotheses, but no continuous-time Markov chain generators, no uniformization, and no Laplace transform. This mission would add the finite-state link between generators, stochastic matrices and matrix exponentials that later chapters of queueing and reliability theory use, and a verified error formula for a numerical inversion method in wide use.

Difficulty

The book's derivation is probabilistic: it conditions on the number of events of the Poisson( $\Lambda$ ) process and thins them. A formal statement cannot rest on that picture, because $p(t)$ is defined analytically, by the forward equations. The goal therefore contains a uniqueness statement for a linear ODE on $[0,\infty)$ with one-sided derivative at $0$ , which the book never mentions. The componentwise bound then needs $\tilde P$ to be stochastic, so that every $\phi^{(k)}_n$ lies in $[0,1]$ . That is exactly where $\Lambda\ge\max_i q_i$ is used; with a smaller $\Lambda$ the matrix $\tilde P$ has negative diagonal entries and the bound fails.

For (8.27), the book gives no proof. The identity is an aliasing (Poisson-summation) formula for a periodic function assembled from the values of $f$ at all odd multiples of $t$ . The convergence of the conditionally summed series (8.24) is the delicate point: continuity of $f$ at $t$ , the book's only hypothesis, does not guarantee convergence of a Fourier series. Mathlib's Poisson summation theorems require decay of the Fourier transform that the damped, reflected function built from $f$ does not have.

Formalization scope

States are Fin (N+1); a row vector is Fin (N+1) → ℝ; $pQ$ is vecMul. A generator is a real matrix with nonnegative off-diagonal entries and diagonal $-\sum_{j\ne i}q_{ij}$ .
$p(t)$ is not defined as the series. It is any function with $p(0)=p_0$ and one-sided derivative $p(t)Q$ within $[0,\infty)$ at every $t\ge0$ . The goal also asserts that such a function exists, so it cannot hold vacuously, and it asserts the series identity for every solution. Defining $p(t)$ as the series (8.9) would make the goal a tautology and is ruled out.
$\Lambda$ is any real with $\Lambda>0$ and $\Lambda\ge q_i$ for all $i$ (the book takes equality with $\max_i q_i$ ).
The truncation bound is stated componentwise, as on p.384 ("an error bound on $p_n(t)$ of $\epsilon$ "), for an arbitrary real $\epsilon$ and truncation point $T$ .
The series (8.8), (8.9) are stated with HasSum, so convergence is part of the claim.
The Laplace transform is the Lebesgue integral over $(0,\infty)$ at a complex argument. $f_A(t)$ is the limit of the partial sums $f_{A,n}(t)$ , and the convergence is part of milestone 4.
Strengthened hypotheses in milestone 4: $f$ bounded and Lipschitz on $[0,\infty)$ replaces " $t$ is a continuity point of $f$ ", which is not sufficient for convergence.
Corrected misprints: $e^{-\lambda t}$ in (8.9) is $e^{-\Lambda t}$ ; $q_{ij}/\Lambda$ in (8.12) is $q_{in}/\Lambda$ ; $\phi(Q/\Lambda-I)$ on p.385 is $\phi(Q/\Lambda+I)$ .
Not formalized: Theorem 8.1 (Bromwich inversion) and the real form (8.21), which the book states without hypotheses on $f$ ; the limit claim $\lim_k\phi^{(k)}=\lim_t p(t)$ on p.385, which fails when $\tilde P$ is periodic; the Euler-summation approximation (8.26) and the round-off discussion, which are stated with "≈".

Useful infrastructure: the matrix exponential and its derivative (Matrix, NormedSpace.exp), uniqueness for linear ODEs (Grönwall), Fourier series on the circle, and a reusable Laplace transform file. Contributions of general lemmas on generators and stochastic matrices are welcome, as they apply to every finite Markovian model in the series.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§8.1.2–8.2. https://doi.org/10.1002/9781118625651
A. Jensen, "Markoff chains as an aid in the study of Markoff processes", Skandinavisk Aktuarietidskrift 36 (1953) 87–91.
W. K. Grassmann, "Transient solutions in Markovian queueing systems", Computers & Operations Research 4 (1977) 47–53.
D. Gross, D. R. Miller, "The randomization technique as a modeling tool and solution procedure for transient Markov processes", Operations Research 32 (1984) 343–361. https://doi.org/10.1287/opre.32.2.343
J. Abate, W. Whitt, "The Fourier-series method for inverting transforms of probability distributions", Queueing Systems 10 (1992) 5–87. https://doi.org/10.1007/BF01158520
J. Abate, G. L. Choudhury, W. Whitt, "An introduction to numerical transform inversion and its application to probability models", in W. Grassmann (ed.), Computational Probability, Kluwer, 1999, 257–323.

8 thms2 active usersReviewed

Markov Chain Operations Research Probability·Captain: mikedeng1

Fundamentals of Queueing Theory I: Foster's Criterion for Positive RecurrenceTextbook

Motivation

Almost every model in queueing theory is analysed through a Markov chain. The number of customers in an M/M/c queue is a continuous-time birth–death chain; the number left behind by departing customers of an M/G/1 queue is a discrete-parameter chain on $\{0,1,2,\dots\}$ (the imbedded Markov chain); networks of queues are chains on vectors of queue lengths. Before any steady-state formula (Erlang's formulas, the Pollaczek–Khintchine formula, product forms) can be used, one has to know that the chain has a steady state at all: that it is positive recurrent, so that a stationary distribution exists and equals the limiting distribution.

Chapter 1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), collects the two ingredients the rest of the book stands on: the Poisson process with its exponential interarrival times (§§1.7–1.8), and the classification theory of discrete-parameter Markov chains (§1.9), ending with Foster's criterion (Theorem 1.2), a sufficient condition for positive recurrence in terms of a drift inequality. The criterion goes back to F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953) (DOI 10.1214/aoms/1177728976), and is the ancestor of the Foster–Lyapunov method used for stability of queueing networks and stochastic systems.

This mission is the first of a series formalizing the book chapter by chapter.

Setting

A homogeneous discrete-parameter Markov chain on $\{0,1,2,\dots\}$ is given by a transition matrix $P=\{p_{ij}\}$ with $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every $i$ . The $m$ -step transition probabilities $p_{ij}^{(m)}$ are the entries of $P^m$ .

The first-passage probability $f_{ij}^{(n)}$ is the probability that the chain started in $i$ enters $j$ for the first time at step $n\ge1$ ; for $i=j$ it is the probability of first return at step $n$ . The return probability is $f_{jj}=\sum_{n\ge1}f_{jj}^{(n)}$ and the mean recurrence time is $m_{jj}=\sum_{n\ge1}n f_{jj}^{(n)}\in[0,\infty]$ . A state is positive recurrent if $f_{jj}=1$ and $m_{jj}<\infty$ ; the chain is positive recurrent if every state is.

The chain is irreducible if for every pair of states $(i,j)$ some $p_{ij}^{(n)}$ is positive, and aperiodic if for every state $k$ the greatest common divisor of $\{n\ge1:p_{kk}^{(n)}>0\}$ is $1$ . A stationary distribution is a probability vector $\pi$ with $\pi=\pi P$ , i.e. $\pi_j=\sum_i\pi_i p_{ij}$ for every $j$ .

For the Poisson part, $T_0,T_1,\dots$ are independent interarrival times, each exponentially distributed with rate $\lambda>0$ ; the arrival epochs are $S_n=T_0+\dots+T_{n-1}$ , and $N(t)=\#\{n\ge1:S_n\le t\}$ counts the arrivals in $[0,t]$ .

Formalization targets

Goal: Theorem 1.2 (Foster's criterion)

An irreducible, aperiodic chain is positive recurrent if there exist $x_j\ge0$ with

\sum_{j=0}^\infty p_{ij}x_j\le x_i-1\quad(i\ne0),\qquad\sum_{j=0}^\infty p_{0j}x_j<\infty .

Milestones: the Markov chain theorems

Theorem 1.1(a). In an irreducible, positive recurrent chain, $\pi_j=1/m_{jj}$ is a stationary distribution, and it is the only one.
Theorem 1.1(c). If moreover the chain is aperiodic and all moments of $\pi$ are finite, then $\lim_{m\to\infty}p_{ij}^{(m)}=\pi_j$ for all $i,j$ .

Milestones: the Poisson process and the exponential distribution

Eqs. (1.11)–(1.14). The unique solution of $p_0'=-\lambda p_0$ , $p_n'=-\lambda p_n+\lambda p_{n-1}$ with $p_0(0)=1$ , $p_n(0)=0$ is $p_n(t)=(\lambda t)^n e^{-\lambda t}/n!$ .
Eq. (1.15). With exponential interarrival times,

\Pr\{N(t)\le n\}=\int_t^\infty\frac{\lambda(\lambda x)^n}{n!}e^{-\lambda x}dx=\sum_{i=0}^n\frac{(\lambda t)^ie^{-\lambda t}}{i!}.

Eq. (1.16). Given $N(L)=k$ , the arrival epochs have density $k!/L^k$ on $\{0<t_1<\dots<t_k<L\}$ .
Eq. (1.17) and its converse (p.21). The exponential law satisfies $\Pr\{T\le t_1\mid T\ge t_0\}=\Pr\{0\le T\le t_1-t_0\}$ , and it is the only continuous distribution on $[0,\infty)$ that does.
Nonhomogeneous Poisson law (p.22). With a continuous rate $\lambda(t)$ the forward equations have the unique solution $p_n(t)=e^{-m(t)}m(t)^n/n!$ , $m(t)=\int_0^t\lambda(s)\,ds$ .

Significance

Foster's criterion reduces positive recurrence, a statement about return times, to exhibiting one test function $x$ with negative drift outside a single state. In the book it is the tool that establishes the existence of steady state for imbedded chains of the M/G/1 and G/M/1 queues (Chapter 5); its generalizations are the standard stability proofs for queueing networks. Theorem 1.1 then supplies what positive recurrence buys: the stationary distribution exists, is unique, equals $1/m_{jj}$ , and is the limit of the transition probabilities. The Poisson results justify the "Markovian" arrivals and services of Chapters 2–4.

All of these results are classical and proved in the literature; the book states Theorems 1.1 and 1.2 without proof. The Prove2Me platform already holds machine-checked versions of related Markov chain theorems in other missions (Levin–Peres–Wilmer's and Durrett's countable-chain convergence theorems), stated with different definitions and hypotheses. What this mission adds is a formal development in the book's own terms — first-passage probabilities $f_{jj}^{(n)}$ , mean recurrence times $m_{jj}$ , gcd periodicity — on which the later missions of the series (imbedded chains, birth–death processes) can build, together with a formal proof of Foster's criterion, which is not on the platform.

Difficulty

For Foster's criterion the natural first step, taking expectations of the drift inequality along the chain, only shows that the expected value of $x$ decreases while the chain stays away from $0$ . Turning that into a bound on the expected return time to $0$ requires an optional-stopping or telescoping argument over a random time, with the value $x$ possibly unbounded, and a separate argument that positive recurrence of state $0$ propagates to all states of an irreducible chain. The book's hypotheses include aperiodicity, which the argument does not use.

For Theorem 1.1, identifying the stationary distribution with $1/m_{jj}$ requires relating the matrix powers $P^n$ to the first-passage probabilities (a renewal decomposition), and uniqueness over countably many states needs care with infinite sums. For the Poisson results, the difficulty is measure-theoretic: the distribution of the sum of $n+1$ exponential variables, and conditioning on the event $\{N(L)=k\}$ for the order-statistics property.

Formalization scope

States are natural numbers; the transition matrix is a real function $p:\mathbb N\times\mathbb N\to\mathbb R$ with nonnegative entries and rows summing to one (as a convergent series). The return probability and the mean recurrence time are valued in $[0,\infty]$ , so null recurrence ( $m_{jj}=\infty$ ) is representable. Irreducibility is the per-pair notion. Stationary equations are stated componentwise with convergent series.

In Foster's criterion the series $\sum_j p_{ij}x_j$ are required to converge for every $i$ , which is the book's condition $\sum_j p_{0j}x_j<\infty$ together with the finiteness implicit in the inequalities for $i\ne0$ ; $x$ is real-valued and nonnegative. Dropping the convergence requirement would let a divergent row series (whose Lean sum is $0$ ) satisfy the inequality vacuously; allowing $x_j=\infty$ would make the hypothesis trivially satisfiable. Neither is permitted.

The closed forms stated explicitly are: $\pi_j=1/m_{jj}$ (Theorem 1.1(a), with both existence and uniqueness), the Poisson probabilities $(\lambda t)^ne^{-\lambda t}/n!$ (1.14), the Erlang tail integral and the Poisson CDF (1.15), the density $k!/L^k$ (1.16), and $e^{-m(t)}m(t)^n/n!$ for the nonhomogeneous law. Equations (1.14) and the nonhomogeneous law are stated as "solves the equations with the initial conditions if and only if equals the closed form", so both existence and uniqueness are asserted.

The Poisson results use random variables on a probability space, with Mathlib's expMeasure for the exponential law and cond for conditional probability. The derivation of the forward equations from the $o(\Delta t)$ axioms of §1.7 is not formalized; the Poisson law is reached from the equations and, separately, from exponential interarrival times.

Not formalized: Theorem 1.1(b) and the word "ergodic" in 1.1(c), which rest on the book's informal notion of ergodicity; Theorem 1.3, whose phrase "for Theorem 1.1 to be valid" for a continuous-time chain is not pinned down.

The Markov chain definitions are reusable by every later mission that studies an imbedded chain. Contributions welcome: proofs of the milestones, and supporting lemmas (Chapman–Kolmogorov, renewal decomposition of $p_{jj}^{(n)}$ , class properties of recurrence).

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976

11 thms2 active usersReviewed

Dynamic Programming Markov Chain Operations Research+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VII: The (BOR) Assumptions and Positive Recurrence of Optimal PoliciesTextbook

Motivation

Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.

Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.

According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).

Setting

A Markov decision chain consists of a countable state space $S$ , finite nonempty action sets $A_i$ , nonnegative finite costs $C(i,a)$ and transition probabilities $P_{ij}(a)$ . A policy $\theta$ may use the whole history and randomize. For $\alpha\in(0,1)$ the discount value function is $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$ , the infimum of $\sum_t\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i]$ ; the average cost of $\theta$ is $J_\theta(i)=\limsup_n\frac1nE_\theta[\sum_{t<n}C(X_t,A_t)\mid X_0=i]$ and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)$ . All of these lie in $[0,\infty]$ .

For a distinguished state $z$ the relative value is $h_\alpha(i)=V_\alpha(i)-V_\alpha(z)$ . The (SEN) assumptions are: (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded on $(0,1)$ ; (SEN2) $h_\alpha\le M$ for a finite function $M\ge0$ ; (SEN3) $h_\alpha\ge-L$ for a finite constant $L\ge0$ . Under (SEN), $J=\lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ is a finite constant, and a limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some $\beta_n\to1^-$ . The ACOI and ACOE read

J+h(i)\ \ge\ (\text{resp. }=)\ \min_{a\in A_i}\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\qquad i\in S.

For a nonempty set $G$ the first passage time is $T=\min\{n\ge1:X_n\in G\}$ . The class $\Re(i,G)$ consists of the policies that, from $i$ , enter $G$ with probability one in finite expected time $m_{iG}(\theta)$ ; $\Re^*(i,G)$ adds a finite expected first passage cost $c_{iG}(\theta)=E_\theta[\sum_{t<T}C(X_t,A_t)]$ . A (randomized) stationary policy $d$ is $z$ standard if the Markov chain it induces has $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ ; it then has a single positive recurrent class $R_d\ni z$ and a finite constant average cost $J_d$ .

Formalization targets

Goal: Theorem 7.5.6

Assume (BOR): (BOR1) a $z$ standard policy $d$ exists; (BOR2) for some $\varepsilon>0$ the set $D=\{i: C(i,a)\le J_d+\varepsilon\text{ for some }a\}$ is finite; (BOR3) every $i\in D-R_d$ can be reached from $z$ by some $\theta_i\in\Re^*(z,i)$ . Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy $e$ has a positive recurrent state in

D(e)=\{i: C(i,e)\le J+\varepsilon\},

at most $|D(e)|$ positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies $e\in\Re^*(i,D(e)\cap R(e))$ for every $i$ .

Milestones

Lemma 7.4.1: $h_\alpha(i)\le c_{iz}(\theta_i)$ for $\theta_i\in\Re^*(i,z)$ , hence (SEN2).
Lemma 7.4.2: $h(i)\le c_{iG}(\theta)-Jm_{iG}(\theta)+E_\theta[h(X_T)]$ for $\theta\in\Re(i,G)$ under an integrability condition.
Theorem 7.4.3: four sufficient conditions for equality in the ACOI at a state.
Lemma 7.5.2: $J_d=(1-\alpha)\sum_{i\in R}\pi_i(d)V_{d,\alpha}(i)$ for a $z$ standard $d$ .
Proposition 7.5.3: a $z$ standard policy gives (SEN1–2).
Corollary 7.5.4: on $S=\{0,1,\dots\}$ , increasing $V_\alpha$ plus a $0$ standard policy gives (SEN), with nonnegative increasing limit functions.
Proposition 7.5.5: an optimal stationary policy has a positive recurrent state of cost at most $J+\varepsilon$ , reachable from $i$ , when (7.33) holds.
Corollaries 7.5.9 and 7.5.10: the (CAV) and (CAV*) conditions imply (BOR).

Significance

Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.

The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.

Difficulty

The obvious approach to the ACOE is to pass to the limit $\alpha\to1^-$ in the discount optimality equation. Exchanging this limit with $\sum_jP_{ij}(a)h_\alpha(j)$ requires a dominating function, and (SEN2) only gives a pointwise bound $M$ whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy $\Phi$ vanishes along them, which in turn needs finiteness of $c_{iG}$ that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set $D$ is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.

Formalization scope

States form a countable type $S$ ; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, $m_{iG}$ , $c_{iG}$ , $P_\theta(X_T=j)$ , $Q^{(n)}_{ij}$ ) are computed from the history probabilities of the process. $V_\alpha$ , $J_\theta$ , $m_{iG}$ and $c_{iG}$ take values in $[0,\infty]$ ; $m_{iG}=\infty$ when $G$ is missed with positive probability; the first passage time satisfies $T\ge1$ . $h_\alpha$ and $\sum_jP_{ij}(a)h(j)$ are in the extended reals, with the book's convention that a function bounded below has an expectation in $(-\infty,+\infty]$ . Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities $\pi_j=(m_{jj})^{-1}$ are the notions for the chain induced by a (randomized) stationary policy. $J_d$ is the average cost of $d$ from $z$ .

A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which $|D(e)|$ is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.

A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at $T$ ); Abelian limits of $\sum_t\alpha^tP(T=t)$ ; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. doi:10.1002/9780470317037
V. S. Borkar, "On minimum cost per unit time control of Markov chains", SIAM J. Control Optim. 22 (1984), 965–978.
V. S. Borkar, "Control of Markov chains with long-run average cost criterion: the dynamic programming equations", SIAM J. Control Optim. 27 (1989), 642–657.
V. S. Borkar, Topics in Controlled Markov Chains, Pitman Research Notes in Mathematics 240, Longman, 1991.
R. Cavazos-Cadena, "Weak conditions for the existence of optimal stationary policies in average Markov decision chains with unbounded costs", Kybernetika 25 (1989), 145–156.
R. Cavazos-Cadena and L. I. Sennott, "Comparing recent assumptions for the existence of average optimal stationary policies", Oper. Res. Letters 11 (1992), 33–37.
L. I. Sennott, "The average cost optimality equation and critical number policies", Prob. Eng. Inform. Sci. 7 (1993).
L. I. Sennott, "Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs", Operations Research 37 (1989), 626–633. doi:10.1287/opre.37.4.626
K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967.

15 thms2 active usersReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VI: The (SEN) Assumptions and the Average Cost Optimality InequalityTextbook

Motivation

Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.

Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ , for each state $i$ a finite nonempty action set $A_i$ , a nonnegative finite cost $C(i,a)$ , and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$ . A policy $\theta$ chooses the action at time $n$ at random according to a distribution that may depend on the whole history $(X_0, A_0, \dots, X_n)$ ; a stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$ .

For an initial state $i$ , the $n$ -horizon cost is $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t) \mid X_0 = i]$ , the average cost is $J_\theta(i) = \limsup_{n} v_{\theta,n}(i)/n$ , and the minimum average cost is $J(i) = \inf_\theta J_\theta(i)$ over all policies. A policy is average cost optimal if $J_\theta \equiv J$ . For $\alpha \in (0,1)$ the discounted value function is $V_\alpha(i) = \inf_\theta \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i]$ . All these quantities lie in $[0,\infty]$ .

Fix a distinguished state $z$ and put $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ . The (SEN) assumptions are:

(SEN1) $(1-\alpha)V_\alpha(z)$ is bounded for $\alpha \in (0,1)$ ;
(SEN2) there is a nonnegative finite function $M$ with $h_\alpha(i) \le M(i)$ for all $i$ and $\alpha$ ;
(SEN3) there is a nonnegative finite constant $L$ with $-L \le h_\alpha(i)$ for all $i$ and $\alpha$ .

A limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some sequence $\beta_n \to 1^-$ . If $f_\alpha$ is a stationary policy realizing the discount optimality equation $V_\alpha(i) = \min_a \{C(i,a) + \alpha\sum_j P_{ij}(a)V_\alpha(j)\}$ , a limit point $f$ is a stationary policy with $f_{\beta_n}(i) = f(i)$ for large $n$ , for each $i$ , along some $\beta_n \to 1^-$ .

Formalization targets

Goal: Theorem 7.2.3

Under (SEN), there is a finite constant $J = \lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ independent of $i$ ; limit functions exist, satisfy $-L \le h \le M$ and the average cost optimality inequality (ACOI)

J + h(i) \ge \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)h(j)\Big\}, \qquad i \in S;

every stationary policy realizing the minimum is average cost optimal with $J_e \equiv J$ and $E_e[h(X_n)]/n \to 0$ ; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.

Milestones

Proposition 7.1.1: finitely many initial transitions with finite cost do not change $J_\theta$ .
Lemma 7.2.1: a bounded-below solution $(J,h)$ of the ACOI inequality for a stationary $e$ gives $J_e \le J$ .
Proposition B.6: a sequence of functions squeezed between $-L$ and $M$ on a countable set has a pointwise convergent subsequence.
Proposition 7.2.4: (SEN) does not depend on the choice of $z$ .
Proposition 7.7.1: (SEN) $\Rightarrow$ (H*) $\Rightarrow$ (H).
Proposition 7.7.2: the conclusions of Theorem 7.2.3 hold under (H), with a state-dependent lower bound $L(i)$ .

Significance

Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.

The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.

Difficulty

On a finite state space the relative value functions are bounded and the Abelian limit $(1-\alpha)V_\alpha$ can be controlled directly. Here $h_\alpha$ is bounded above only by a function $M$ that may be unbounded, so passing to the limit in the discounted optimality equation $\sum_j P_{ij}(a)h_\alpha(j)$ cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of $E_e[h(X_n)]/n$ for a function $h$ that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.

Formalization scope

The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost $0$ , as the chapter prescribes.

The relative value $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ is computed in EReal, never through a truncated real subtraction: a state with $V_\alpha(i) = \infty$ gives $h_\alpha(i) = +\infty$ , so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces $V_\alpha(z) < \infty$ . Sums $\sum_j P_{ij}(a)h(j)$ and expectations $E[h(X_n)]$ of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to $0$ when not summable. The limit $\alpha \to 1^-$ is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences $\alpha_n \to 1^-$ in $(0,1)$ , and the (SEN), (H), (H*) sets are predicates carrying their witnesses $M$ and $L$ .

A development that bounds only $h_\alpha$ as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in $J(i)$ , proves a different and weaker theorem and does not count.

Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality $\limsup(1-\alpha)\sum\alpha^t c_t \le \limsup \frac1n\sum_{t<n}c_t$ (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Chapter 7 (pp. 127–166) and Appendix B. https://doi.org/10.1002/9780470317037
L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37 (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, The average cost optimality equation and critical number policies, Probability in the Engineering and Informational Sciences 7 (1993). (Cited in the book's bibliography, p. 321.)
L. I. Sennott, Another set of conditions for average optimality in Markov control processes, Systems & Control Letters 24 (1995) 147–151. (Cited in the book's bibliography.)
R. Cavazos-Cadena, A counterexample on the optimality equation in Markov decision chains with the average cost criterion, Systems & Control Letters 16 (1991) 387–392. (Cited in the book's bibliography.)
S. M. Ross, Non-discounted denumerable Markovian decision models, Annals of Mathematical Statistics 39 (1968) 412–423. (Cited in the book's bibliography.)
H. M. Taylor, Markovian sequential replacement processes, Annals of Mathematical Statistics 36 (1965) 1677–1694. (Cited in the book's bibliography.)
E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control; formalized on Prove2Me in the mission of the same name (Borel state spaces, a different model).

12 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains VII: Palm's Theorem for Nonstationary DemandTextbook

Motivation

Spare-parts inventory models for repairable items rest on Palm's theorem: if demands arrive as a Poisson process with constant rate $\lambda$ and each demanded unit spends an independent, identically distributed resupply time with mean $\bar\tau$ in the pipeline, the number of units in resupply is Poisson with mean $\lambda\bar\tau$ in steady state. Stock levels, backorders and fill rates are all computed from that distribution.

Both assumptions fail in practice. Military flying programmes ramp up and down within weeks, repair shops close for periods, and commercial parts distribution centres see demand that varies by day of the week. Chapter 9 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) extends Palm's theorem to a nonstationary Poisson demand process with time-dependent resupply-time distributions, gives the compound (multi-unit order) version, and uses the result to compute, at any time $t$ , the distribution of units in repair at the depot of a two-echelon system.

Timeline: Palm (1938) proved the stationary result for telephone traffic; Feeney and Sherbrooke (1966) extended it to compound Poisson demand; Hillestad and Carrillo (RAND, 1980) and Crawford (RAND, 1981) developed the time-dependent extensions, summarized by Carrillo (RAND, 1989). The chapter presents these results.

Setting

A single item is stocked at one location, and every demand is for one unit.

Demand rate $\lambda(s) \ge 0$ , integrable on bounded intervals, with mean function $m(t) = \int_0^t \lambda(s)\,ds$ .
Demand process: a nonstationary Poisson process with mean function $m$ , with $N(0) = 0$ . $N(t)$ counts demands in $[0,t]$ and $T_0 < T_1 < \cdots$ are the demand epochs.
Resupply times: a unit demanded at time $s$ is resupplied within $w$ time units with probability $G_s(w)$ . Resupply times are nonnegative, have finite expectations, are independent from unit to unit, and are independent of the demand process.
$X(t)$ is the number of units in resupply at time $t$ : demands in $[0,t]$ whose resupply is not complete at $t$ .

The mean of $X(t)$ is

\alpha(t) = \int_0^t \bigl(1 - G_s(t-s)\bigr)\lambda(s)\,ds.

In the compound version (Section 9.2), orders arrive as above and each order is for $Q \ge 1$ units, with a time-stationary law $u_j = P(Q = j)$ . All units of an order share its resupply time, $Y(t)$ counts units demanded in $[0,t]$ , and $u^{(n)}_k$ is the $n$ -fold convolution of $(u_j)$ .

In the two-echelon version (Section 9.3), base $i$ has failure rate $\lambda_i$ . A failure is repaired at the base with probability $r_i$ and at the depot otherwise. Depot repair of a failure occurring at time $u$ takes a deterministic time $D(u)$ with $D(t) + t \ge D(s) + s$ for $s < t$ (no crossing). Write $\tilde t = \inf\{u \ge 0 : D(u) + u > t\}$ .

Formalization targets

Goal: Theorem 13 (p. 216)

For every $t \ge 0$ ,

P\{X(t) = k\} = e^{-\alpha(t)}\frac{\alpha(t)^k}{k!}, \qquad k = 0,1,2,\dots

This is an exact statement at each finite time, not a limit. With constant $\lambda$ and $G_s = G$ it reduces to the finite-time step of Palm's theorem.

Milestones

$E[N(t)] = m(t)$ (Section 9.1, p. 216).
Theorem 12 (p. 216): given $N(t) = n$ , the epochs $T_0, \dots, T_{n-1}$ are distributed as the order statistics of $n$ i.i.d. variables with distribution function $F(x) = m(x)/m(t)$ on $[0,t)$ .
The binomial step of the proof of Theorem 13 (pp. 216–217): $P\{X(t) = k \mid N(t) = n\} = \binom nk p^k(1-p)^{n-k}$ , with $p = \int_0^t (1 - G_s(t-s))\lambda(s)/m(t)\,ds$ .
Section 9.2 (p. 218): $E[Y(t)] = m(t)E[Q]$ and $\operatorname{Var}[Y(t)] = m(t)E[Q^2]$ .
Theorem 14 (p. 218): $P[X(t) = k] = \sum_{n\ge1} u^{(n)}_k e^{-\alpha(t)}\alpha(t)^n/n!$ for $k \ge 1$ , and $e^{-\alpha(t)}$ at $k = 0$ .
Section 9.3.2 (p. 221): $P\{X_0(t) = k\} = e^{-m_0(\tilde t,t)} m_0(\tilde t,t)^k/k!$ with $m_0(\tilde t,t) = \int_{\tilde t}^t \sum_i \lambda_i(u)(1-r_i)\,du$ .

A plain supporting item states that $N(t)$ is Poisson with mean $m(t)$ , the factor the proof of Theorem 13 uses.

Significance

Theorem 13 gives the full distribution of the pipeline at every instant. Time-dependent expected backorders, $\sum_{x > s(t)} (x - s(t)) P\{X(t) = x\}$ , and fill rates $P\{X(t) < s(t)\}$ follow from it, so stock levels can be planned against a surge or a repair outage without a steady-state approximation. Theorem 14 does the same for multi-unit orders. The depot result feeds the base-level convolution of Section 9.3.3, which in turn gives time-dependent performance measures for a two-echelon system.

These results are proved in the literature, and the chapter reproduces the proofs of Theorems 13 and 14. It cites Theorem 12 without proof ("similar to the one given in Chapter 3"). No machine-checked version of any of them is known, and neither Mathlib nor this platform has a Poisson process, stationary or not, a thinning theorem, or an order-statistics theorem. The formal content of this mission therefore includes the construction and the first distributional facts of the nonstationary Poisson process.

Difficulty

The algebra of the proof is a Poisson mixture of binomials and is short. The difficulty is Theorem 12 and its use. The obvious argument treats "the $n$ demands in $[0,t]$ " as $n$ independent draws from $F$ and assigns each an independent resupply time with law $G_{\text{draw}}$ . Making this rigorous requires identifying the conditional joint law of the epochs given $N(t) = n$ . The resupply time of the $j$ -th demand is not independent of its epoch: its law depends on the epoch. So it must be shown that, after conditioning, the marks attached to sorted epochs behave like marks attached to unsorted i.i.d. draws. The book's constant-rate argument (Chapter 3) uses the uniform density $n!/t^n$ on the simplex. Here the density involves $\lambda$ , which may vanish on intervals, and $m$ need not be invertible.

Formalization scope

Demand process. The nonstationary Poisson process is constructed, not postulated. With i.i.d. exponential(1) gaps and unit-rate points $\Gamma_k = A_0 + \cdots + A_k$ , the $k$ -th demand occurs at $T_k = \inf\{s \ge 0 : m(s) \ge \Gamma_k\}$ , and $N(t) = \#\{k : \Gamma_k \le m(t)\}$ .
Resupply times. Resupply times are $\rho(T_k, U_k)$ for a jointly measurable $\rho \ge 0$ and i.i.d. marks $U_k$ independent of the gaps, with $G_s(w) = \nu\{\rho(s,\cdot) \le w\}$ . Every measurable family $G_s$ arises this way, and joint measurability makes $\alpha(t)$ a genuine integral. Independence of resupply times from the demand process is not written in Theorem 12 or 13 but is used in the proof; it is part of the model.
Pinnings and conventions.
- " $\lambda$ integrable" is read as integrable on bounded intervals.
- Time is $t \ge 0$ .
- Theorem 12 assumes $m(t) > 0$ , since $F$ is $0/0$ otherwise, and sets $F = 0$ on $(-\infty,0)$ .
- Conditional probabilities are written as joint probabilities.
- $E[Y(t)]$ is stated in $[0,\infty]$ ; the variance identity assumes $E[Q^2] < \infty$ .
- $\tilde t$ is an infimum over $u \ge 0$ , and $D \ge 0$ .
- Counts are cardinalities, and are $0$ on the null event where they would be infinite.
Corrections. Theorem 14's printed sum starts at $n = 1$ , which gives $P[X(t) = 0] = 0$ . The statement keeps the book's formula for $k \ge 1$ and adds $P[X(t) = 0] = e^{-\alpha(t)}$ . The depot's Poisson demand stream with rate $\sum_i \lambda_i(1-r_i)$ is generated from the bases' processes and independent repair-location choices, not assumed.
Not stated.
- Eqs. (9.1)–(9.2), the FCFS depot backorders owed to base $i$ : the derivation on p. 221 is informal, and (9.1) prints the exponent $s_0(t-1)$ for $s_0(t)-1$ .
- The base analysis of Section 9.3.3.
- The compound law of $Y(t)$ on p. 217, which has the same $n = 0$ omission.
Trivialization ruled out. $X(t)$ is computed from the demand epochs and resupply times, not defined by its law, and resupply times cannot depend on the demand epochs except through the prescribed $G_s$ . Either shortcut would make the goal empty or false.
Infrastructure. The time-changed Poisson construction, its count law, the order-statistics property and marked thinning are reusable well beyond this chapter: in queueing ( $M_t/G_t/\infty$ ), in reliability, and in the stationary Palm mission of this series. Contributions of these general lemmas are welcome.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 9, pp. 215–222. https://doi.org/10.1007/b138879
C. Palm, "Analysis of the Erlang traffic formulae for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
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
R. J. Hillestad and M. J. Carrillo, Models and techniques for recoverable item stockage when demand and the repair processes are nonstationary — Part I: Performance measurement, Report N-1482-AF, RAND Corporation, 1980.
G. B. Crawford, Palm's theorem for nonstationary processes, Report R-2750-RC, RAND Corporation, 1981.
M. J. Carrillo, Generalizations of Palm's theorem and Dyna-METRIC's demand and pipeline variability, Report R-3698-AF, RAND Corporation, 1989.

11 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Elements of Queueing Theory IV: PASTA and the Formulas of Palm CalculusTextbook

PASTA and the Formulas of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.

The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.

The goal

Theorem 3.3.1 (p.211) is the one that says when the two views coincide.

This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the θ_t-framework.

E⁰_A[f(Z(0))] = E[f(Z(0))]                                                            (3.3.1)

for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f, whenever A admits the constant F_t-intensity λ; and, under ergodicity,

lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds .                       (3.3.2)

The "some care" is the word predictable. PASTA is false without it: an arrival that changes the state it then observes does not see the time average, and that is exactly what predictability — measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a — rules out.

The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two are equivalent, but that equivalence is a remark on the page and not part of this theorem.

Why it earns its place: Pollaczek–Khinchin

§3.4 derives formulas from conservation equations. Applying the rate conservation principle of Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula

iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) ,                (3.4.44)

an identity between a stationary expectation and a Palm expectation of the workload just before an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and

E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) ,                                   (3.4.45)

the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.

The rest of the chapter

§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.

§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by thinnings of the entrance processes of two disjoint sets.

§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.

What this mission provides

Nothing here is on the platform or in Mathlib. The nearest platform item, queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the Palm identity for a stationary ergodic marked point process, derived from the inversion formula (1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a pathwise limit. Different framework, different hypotheses, and neither implies the other.

Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.

Formalization scope

PASTA carries both displays. (3.3.1) is an equality in [0, ∞] for every non-negative measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one common limit, so both limits exist. Predictability is measurability for the predictable σ-field P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis, because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity, E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".
Takács (3.4.44) and Pollaczek–Khinchin (3.4.45) are stated for every real u, and for u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for {W(t−)}, and it asserts that its denominator is non-zero.
Lemma 3.2.1 asserts both closed forms of E_α R. The chain is irreducible, F is non-empty, and hitting times are counted from time 0.
Theorem 3.2.1 asserts the equality in (3.2.43), the convergence to 1, and E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.
Lemmas 3.5.1 and 3.5.2 are stated for the full on-off model of §3.5.3. The on-off point processes are independent, their on periods, off periods and fluid functions are i.i.d. and independent, P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞]. Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.

A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.

14 thms2 active usersReviewed

Stochastic Systems

Missions

Stochastic Optimal Control: The Discrete-Time Case IX: Imperfect State Information — Reduction to a Perfect-Information Model through a Statistic Sufficient for ControlTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 10.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Optimal Control: The Discrete-Time Case VII: The Finite-Horizon Borel Model — over Universally Measurable Policies J*_K = T^K(J_0)Textbook

Motivation

Setting

Formalization targets

Goal: Proposition 8.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Reversibility and Stochastic Networks VI: The Ewens Sampling Distribution Is Consistent Under Sampling Without ReplacementTextbook

Motivation

Setting

Formalization targets

Goal: consistency under sampling (Theorem 7.1)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Approximation Algorithms for Stochastic Inventory Control Models 1: The Dual-Balancing Policy Costs at Most Twice the OptimumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information 2: Without Shared Demand Information the Bullwhip Bound Is MultiplicativeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 (Eq. (7))

Milestone: Eq. (6)

Significance

Difficulty

Formalization scope

Selected references

On the Stochastic Matrices Associated with Certain Queuing Processes 1: The M/G/1 Imbedded Chain Is Ergodic iff ρ < 1 and Recurrent iff ρ ≤ 1Research Paper

Motivation

Setting

Formalization targets

Goal: the M/G/1 classification (§3, p. 358)

Milestones (the paper's general theorems and the step of §3 they feed)

Significance

Difficulty

Formalization scope

Selected references

Dimensioning Large Call Centers IV: Asymptotically Optimal Staffing under a Waiting-Cost ConstraintResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.2 (rationalized regime)

Supporting milestones

Further target: Theorem 8.6 (efficiency-driven regime)

Significance

Difficulty

Formalization scope

Selected references

Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications 2: An Explicit Family of Nash Equilibria for the Linear Impulse GameResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4.7

Milestones

Significance