Probability · Prove2Me

Completed

Operations Research Statistics·Captain: mikedeng1

Residual Life Time at Great Age 5: If |c − ((1 − F)/F′)′| ≤ ε for t ≥ t₀, the Residual Life Normed by (1 − F(t))/F′(t) Is Within ε of Π_{0,c} for t ≥ t₀Research Paper

Motivation

The residual life time of a lifetime $X$ at age $t$ is the excess $X - t$ given survival, $X > t$ . How it behaves at great ages is a question in reliability (remaining life of an item that has already lasted long), in insurance and demography (remaining life at old age), and in the peaks-over-threshold method of extreme value statistics, where exceedances over a high threshold are modelled by a generalized Pareto law.

Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974) 792–804) determined every possible limit law of the suitably normed residual life as $t \to \infty$ , and their domains of attraction. For continuous limits, the classical sufficient conditions are von Mises' conditions (1936) on the derivative of $(1 - F)/F'$ . Section 4 of the paper goes further: it gives inequalities that hold at every finite age $t \ge t_0$ , not only in the limit. This mission formalizes that finite- $t$ result, the Corollary to Theorem 7.

Timeline: von Mises (1936) gives sufficient conditions for domains of attraction of extreme value laws; Balkema and de Haan (1974) prove the limit theorems for residual life and the finite- $t$ bounds formalized here; Pickands (1975, Ann. Statist. 3, 119–131) proves the corresponding approximation by the generalized Pareto law for excesses, the result now known as the Pickands–Balkema–de Haan theorem.

Setting

Let $X$ be a real random variable with distribution function $F$ . The residual life distribution function at age $t$ is

F_t(x) = P\{X - t \le x \mid X > t\}.

Assume $F$ has a positive, differentiable density $F'$ for $t \ge t_0$ , and define the norming function

a(t) = \frac{1 - F(t)}{F'(t)} \qquad (t \ge t_0),

the reciprocal of the hazard rate. The normed residual life is $(X - t)/a(t)$ given $X > t$ , with distribution function $P\{(X - t)/a(t) \le x \mid X > t\} = F_t(x\,a(t))$ .

The comparison laws are the distribution functions $\Pi_{0,c}$ , $c \in \mathbb R$ , all vanishing for $x < 0$ :

for $c > 0$ , $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $x \ge 0$ (a generalized Pareto law);
for $c = 0$ , $\Pi_{0,0}(x) = \Pi(x) = 1 - e^{-x}$ for $x \ge 0$ (the exponential law);
for $c < 0$ , $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $0 \le x \le |c|^{-1}$ , and $1$ beyond (bounded support).

Formalization targets

Goal: the Corollary to Theorem 7

If $c \ge 0$ and $\varepsilon \ge 0$ satisfy $|c - a'(t)| \le \varepsilon$ for $t \ge t_0$ , then

\left|\Pi_{0,c}(x) - P\left\{\frac{X - t}{a(t)} \le x \,\middle|\, X > t\right\}\right| \le \varepsilon \qquad \text{for all } x \text{ and all } t \ge t_0 .

Milestones

The bounds (13): if $c_1 \le a' \le c_2$ on $[t_0, \infty)$ , then $1 + c_1 x \le a(t + x a(t))/a(t) \le 1 + c_2 x$ for $t \ge t_0$ , $x \ge 0$ .
The exponential representation

P\left\{\frac{X - t}{a(t)} > x \,\middle|\, X > t\right\} = \frac{1 - F(t + x a(t))}{1 - F(t)} = \exp\left(-\int_0^x \frac{a(t)}{a(t + s a(t))}\, ds\right).

Theorem 7: if $c_1 \le a'(t) \le c_2$ for $t \ge t_0$ , then

\Pi_{0,c_2}(x) \le P\left\{\frac{X - t}{a(t)} \le x \,\middle|\, X > t\right\} \le \Pi_{0,c_1}(x) \qquad (t \ge t_0,\ x \in \mathbb R).

$\sigma(u) = u^{-2}(e^{-u} - 1 + u) = \int_0^1\int_0^t e^{-us}\,ds\,dt$ is positive and decreasing.
Lemma 4: $0 \le -(\partial/\partial c)\Pi_{0,c}(x) < 1$ for $c > -1$ , $x \ne 0$ , $cx \ne -1$ .
$|\Pi_{0,c}(x) - \Pi_{0,c_0}(x)| \le |c - c_0|$ for $c \ge 0$ and all real $c_0$ , $x$ .

The goal is the Corollary because it is the paper's final statement of Section 4: a single parameter $c$ and a single error $\varepsilon$ , with no limit taken. Theorem 7 is the stronger two-parameter sandwich it rests on.

Significance

The result. Theorem 7 and its Corollary are a quantitative, non-asymptotic form of the von Mises condition $\frac{d}{dt}\frac{1-F(t)}{F'(t)} \to c$ . If the derivative of the reciprocal hazard stays within $\varepsilon$ of $c$ from age $t_0$ on, then at every such age the normed excess distribution is uniformly within $\varepsilon$ of the generalized Pareto (or exponential) law $\Pi_{0,c}$ . Letting $\varepsilon \to 0$ along $t_0 \to \infty$ recovers convergence to $\Pi_{0,c}$ , and the bound itself quantifies the error of the generalized Pareto approximation used in threshold-exceedance modelling.

Formalizing it. The result is proved in the paper (1974), with short proofs. To our knowledge no part of it has a machine-checked proof. The mission produces checked versions of the theorem, the corollary and the elementary lemmas about the family $\Pi_{0,c}$ : its monotonicity and Lipschitz dependence on the parameter $c$ , including across the case change at $c = 0$ . Those facts about the generalized Pareto family are reusable in any formal development of extreme value statistics.

Difficulty

The analytic content is elementary, but several steps hide case analysis. The Lipschitz bound in $c$ requires the derivative of $\Pi_{0,c}(x)$ in $c$ across $c = 0$ , where the formula changes from $1 - (1+cx)^{-1/c}$ to $1 - e^{-x}$ , and across the boundary $cx = -1$ of the support when $c < 0$ , where the function is not differentiable. The bound $-\partial_c \Pi_{0,c} < 1$ is not a crude estimate: it reduces to the comparison $\sigma(u) < \sigma(-\psi)$ for the function $\sigma(u) = u^{-2}(e^{-u} - 1 + u)$ , which needs its strict monotonicity on all of $\mathbb R$ , including $u = 0$ where the closed form is undefined. In Theorem 7 the lower bound $1 + c_1 x$ in (13) becomes negative for $c_1 < 0$ and large $x$ ; this is exactly where the comparison law $\Pi_{0,c_1}$ reaches $1$ , and the argument must handle it. The orientation is easy to get wrong: the upper bound $c_2$ on the derivative gives the lower bound $\Pi_{0,c_2}$ , since $\Pi_{0,c}(x)$ decreases in $c$ .

Formalization scope

The source is the published Annals of Probability article (DOI 10.1214/aop/1176996548); page numbers are the journal's.

The law of $X$ is a probability measure μ on ℝ, $F$ is Mathlib's cdf μ, and $F_t(x) = \mu((t, t+x]) / \mu((t, \infty))$ . The normed probability $P\{(X-t)/a(t) \le x \mid X > t\}$ is $F_t(x\,a(t))$ .
"Positive, differentiable density for $t \ge t_0$ " is: for $t \ge t_0$ , cdf μ has derivative $f(t) > 0$ and $f$ has derivative $f'(t)$ , both within $[t_0, \infty)$ ; nothing is assumed to the left of $t_0$ .
The derivative $\frac{d}{dt}a(t)$ is a named function $a'$ with HasDerivWithinAt on $[t_0, \infty)$ ; it is the derivative the density hypothesis already provides, so this adds no assumption. Bare deriv is not used.
Completion of $\Pi_{0,c}$ for $c < 0$ . The paper (p. 801) prints the formula only for $0 \le x \le |c|^{-1}$ . The formalization sets $\Pi_{0,c}(x) = 1$ for $x > |c|^{-1}$ , as "distribution function" requires and as the proof of Lemma 4 uses (" $\Pi_{0,c}(x)$ is constant on both components of $\{c > -1\}\setminus R$ "). The formula gives $1$ at $x = |c|^{-1}$ , so the completion is continuous.
$\Pi_{0,0}$ is a separate branch ( $1 - e^{-x}$ ), not the formula with $1/0$ .
$\sigma$ is defined as $\int_0^1\int_0^t e^{-us}\,ds\,dt$ , and the closed form $u^{-2}(e^{-u} - 1 + u)$ for $u \ne 0$ is part of milestone 4. "Decreasing" is stated as strictly decreasing, which is what the proof of Lemma 4 uses ( $\sigma(u) < \sigma(-\psi)$ ).
Lemma 4 states the differentiability of $c \mapsto \Pi_{0,c}(x)$ at $c$ together with the bound $0 \le -d < 1$ on its derivative $d$ .
The bounds (13) are stated in both printed forms.
No sign condition is added on $c_1, c_2$ in Theorem 7; $c_1$ may be any real number, and $c - \varepsilon$ in the Corollary may be negative.

A trivializing formalization is ruled out: the conclusion is a bound at every real $x$ and every $t \ge t_0$ with $a(t) > 0$ , the conditional probability divides by $\mu((t,\infty)) > 0$ (which the density hypothesis implies), and the hypotheses are satisfied by, for example, the exponential law ( $a \equiv 1$ , $c = 0$ ) and the Pareto law $1 - (1+x)^{-\alpha}$ ( $a(t) = (1+t)/\alpha$ , $c = 1/\alpha$ ).

A complete development needs the fundamental theorem of calculus with one-sided derivatives, a change of variables in interval integrals, and calculus of Real.rpow in the exponent parameter. The lemmas on $\Pi_{0,c}$ and $\sigma$ are reusable beyond this mission; proofs of any milestone are welcome independently.

Selected references

A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
R. von Mises, La distribution de la plus grande de n valeurs, Revue Mathématique de l'Union Interbalkanique 1 (1936), 141–160.
J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), no. 1, 119–131. https://doi.org/10.1214/aos/1176343003
L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

10 thms3 active usersReviewed

Dynamic Programming Machine Learning Operations Research+1·Captain: mikedeng1

Stable Function Approximation in Dynamic Programming II: In a Nondiscounted MDP with All Policies Proper, Value Iteration Through a Self-Weighted Averager ConvergesResearch Paper

Motivation

Value iteration solves a Markov decision process by repeatedly applying the Bellman backup to a table of state values. When the state space is too large for a table, the values are stored in a function approximator instead: each backup is followed by a fit, and the fitted function is backed up again. This approximate value iteration is the basis of fitted dynamic programming and of much of reinforcement learning, and it was known in the early 1990s to diverge for common approximators such as linear regression and neural networks (Boyan and Moore, 1995, cited in the report as [BM95]).

Gordon's technical report (Stable Function Approximation in Dynamic Programming, CMU-CS-95-103, 1995; conference version at ICML 1995) identified a class of approximators, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a grid), for which the combination is stable. For discounted problems stability follows from a norm argument. For nondiscounted problems, where the backup contracts only in a weighted norm, that argument fails, and the report proves convergence by a different route: approximate value iteration is exact value iteration on a derived MDP. This mission formalizes that route and its conclusion, Corollary 4.1 (p. 11).

Setting

A finite nondiscounted Markov decision process $M$ has non-goal states $x=1,\dots,n$ , a finite nonempty action set $U(x)$ at each state, an expected one-step cost $c_{xa}$ , and transition probabilities $p_{axy}\ge 0$ with $\sum_y p_{axy}\le 1$ . The missing mass $1-\sum_y p_{axy}$ is the probability of moving to a cost-free absorbing goal state, which the paper calls state $1$ . A value function is a vector $V\in\mathbb R^n$ ; the goal's value is $0$ . The parallel value backup is

(T_M V)(x)=\min_{a\in U(x)}\Bigl[c_{xa}+\sum_y p_{axy}V(y)\Bigr],

and with a discount factor $\gamma$ the sum is multiplied by $\gamma$ . A policy $\mu$ chooses an admissible action at each state; it is proper if, from every starting state, the probability of having reached the goal after $t$ steps tends to $1$ .

An averager $A$ consists of constants $k_y$ , nonnegative weights $\beta_y$ and nonnegative weights $\beta_{yz}$ ( $z$ ranging over all states, the goal included) with $\beta_y+\sum_z\beta_{yz}=1$ . Its mapping is $M_A(V)(y)=\beta_yk_y+\sum_z\beta_{yz}V(z)$ . Two operators $M_F$ and $T$ are compatible if $(M_F\circ T)^k(V_0)$ converges from every initial guess $V_0$ .

The derived MDP $M'$ has the same states and actions, transition probabilities $p'_{axz}=\sum_y p_{axy}\beta_{yz}$ to non-goal states $z$ , the rest of the mass going to the goal, and costs $c'_{xa}=c_{xa}+\gamma\sum_{y}p_{axy}\beta_yk_y$ .

The states are layered by distance from the goal: $S_1=\{1\}$ , $U_k=\bigcup_{j<k}S_j$ , and $S_k$ is the set of states outside $U_k$ from which every action reaches $U_k$ with positive probability. Write $k(x)$ for the index of the layer containing $x$ . The averager is self-weighted for $M$ if for every state $y$ either $\beta_y>0$ or $\beta_{yx}>0$ for some state $x$ with $k(x)\le k(y)$ .

Formalization targets

Goal: Corollary 4.1 (p. 11)

If every policy of $M$ is proper and $A$ is self-weighted for $M$ , then for every initial guess $V_0$ both

(M_A\circ T_M)^k(V_0)\quad\text{and}\quad(T_M\circ M_A)^k(V_0)

converge as $k\to\infty$ . The first is the page's " $T_M$ and $M_A$ are compatible", the second its "approximate value iteration … will converge".

Milestones

Theorem 4.1 (Derived MDP, p. 7): $T_{M'}=T_M\circ M_A$ , for every discount factor and for the nondiscounted backup.
Exhaustiveness (p. 10, after [BT89]): if all policies of $M$ are proper, every state lies in some layer $S_k$ .
$M'$ terminates (p. 10): if all policies of $M$ are proper and $A$ is self-weighted, there is $m>0$ such that under every policy of $M'$ and from every state the goal is reached within $m$ steps with positive probability; in particular every policy of $M'$ is proper.
Theorem 2.3 (p. 4), in its all-policies-terminate case: value iteration converges from any initial guess. This is the published, proved item BertsekasDP.ssp_main_theorem.

A further item, Theorem 6.1 (p. 12), says the limit is $V^*$ when the optimal value function is a fixed point of $M_A$ , under self-weighting or under positive costs with $k\ge 0$ .

Significance

The corollary gives a checkable, purely combinatorial condition on the approximator and the transition graph under which fitted value iteration on a stochastic shortest path problem cannot diverge. Weight decay ( $\beta_y>0$ everywhere) and any averager that only ever averages a state's value with values no farther from the goal satisfy it. The derived-MDP identity, Theorem 4.1, is the tool the rest of the report builds on (§5, §6.1, Appendix A): it reduces questions about approximate dynamic programming with averagers (convergence, the limit's error, the online Q-learning variant) to questions about an ordinary MDP.

The results are proved in the report, in prose. They have no machine-checked version. The formal development needed here is a finite stochastic shortest path theory (proper policies, the layer partition, termination bounds) on top of the published model BertsekasSSPModel and the proved BertsekasDP.ssp_main_theorem.

Difficulty

The obvious argument fails. If all policies of $M$ are proper, $T_M$ contracts in some weighted max norm, and $M_A$ is a nonexpansion in the unweighted max norm, but $M_A$ can expand the weighted norm, so the composition need not contract. Figure 4 of the report gives a three-state chain and an averager, replacing $V(2)$ by $V(3)$ , for which approximate value iteration diverges. The proof therefore has to go through $M'$ and show that self-weighting makes $M'$ terminate under every policy. That is a probabilistic statement about all, possibly nonstationary, policies of a new process, derived from a layer structure of the old one. Exhaustiveness of the layers itself needs a policy-construction argument.

Formalization scope

The MDP is the published BertsekasSSPModel n C: non-goal states Fin n, a finite action type C with admissible sets M.U i, costs M.g, and transition probabilities M.p whose deficit is the probability of termination. Gordon's state 1 is this implicit termination state: its value is $0$ by construction, and where the partition and the averager's goal weight need to name it, it is none : Option (Fin n). This realises the page's two "without loss of generality" steps (state 1 cost-free and absorbing; $\beta_1=1$ , $k_1=0$ ). The nondiscounted backup is BertsekasSSPBellmanOp M, the discounted one BertsekasDiscountedBellmanOp M γ.

The averager acts on whole value functions over the state set. An approximator that fits only a sample $X_0$ of states is the special case $\beta_{yx}=0$ for $x\notin X_0$ . "All policies proper" quantifies over stationary policies μ : Fin n → C with admissible actions, as on p. 3. Self-weightedness is stated through layer membership, which agrees with the page's $k(x)$ whenever the partition is exhaustive (milestone 2). Theorem 6.1 takes $V^*$ as a real fixed point of the backup; under either of its cases such a fixed point is unique and optimal. Convergence is in $\mathbb R^n$ , which is the same as convergence in max norm.

The goal's hypotheses concern $M$ and $A$ only. A formalization that assumed properness of the derived MDP, dropped the "every action" quantifier in the layers (making the partition and self-weighting weaker notions), or dropped $k(x)\le k(y)$ (making every averager with a positive weight self-weighted) would be a different theorem.

Reusable beyond this mission: the layer partition and its exhaustiveness, and the termination bound for the derived model, are general finite stochastic shortest path facts. Contributions to any milestone are welcome, and so are proofs of the definitions-level lemmas they rely on.

Selected references

G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995. Conference version in Proceedings of the 12th International Conference on Machine Learning (ICML), 1995. https://doi.org/10.1016/B978-1-55860-377-6.50040-2
D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. ([BT89] in the report.)
D. P. Bertsekas and J. N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research 16(3), 1991. https://doi.org/10.1287/moor.16.3.580
J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, Morgan Kaufmann, 1995. ([BM95] in the report.)

8 thms3 active usersReviewed

Completed

Analysis Harmonic Analysis·Captain: mikedeng1

Distribution Function Inequalities for Martingales 2: Gundy's Decomposition of an L¹-Bounded Martingale, with One Stopping TimeResearch Paper

Motivation

Many operators of harmonic analysis are bounded on $L^2$ by an orthogonality argument but fail to be bounded on $L^1$ ; what survives at $p=1$ is a weak-type estimate $\lambda\,P(|Tf|>\lambda)\le c\,\|f\|_1$ . For singular integrals the standard route to such an estimate is the Calderón–Zygmund decomposition, which splits a function at height $\lambda$ into a bounded part and a part supported on a small set. Martingale theory has the same need: square functions, martingale transforms and maximal operators of martingales are bounded on $L^2$ for orthogonality reasons, and their behaviour on $L^1$ -bounded martingales is the delicate endpoint.

R. F. Gundy (1968) supplied the martingale analogue: an $L^1$ -bounded martingale can be written as the sum of three martingales, one bounded in $L^2$ , one whose differences are absolutely summable in $L^1$ , and one that is non-zero only on an event of small probability (Gundy 1968). Gundy's construction used several stopping times. In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder gave a simplified version of the decomposition in which only one stopping time is used, with explicit constants $2$ , $4$ and $1$ . This mission formalizes that version, Theorem 4.1 of the lectures, together with the facts its proof rests on.

Timeline:

1953. J. L. Doob's Stochastic Processes establishes almost-everywhere convergence of $L^1$ -bounded martingales and the maximal inequality.
1966. D. G. Austin proves that the integral of $S^2(f)$ over $\{f^*\le\lambda\}$ is finite for an $L^1$ -bounded martingale (Austin 1966).
1968. Gundy proves the decomposition theorem for $L^1$ -bounded martingales, with applications to weak-type estimates.
1973. Burkholder's Lemma 2.1, a refinement of Austin's theorem, yields a one-stopping-time proof of Gundy's decomposition with explicit constants.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $\mathcal A_0\subseteq\mathcal A_1\subseteq\cdots$ a nondecreasing sequence of sub- $\sigma$ -fields of $\mathcal A$ . A martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ is a sequence $f=(f_1,f_2,\dots)$ of integrable random variables with $f_n$ $\mathcal A_n$ -measurable and $E(f_{n+1}\mid\mathcal A_n)=f_n$ . Its difference sequence is $d=(d_1,d_2,\dots)$ with $f_n=\sum_{k=1}^n d_k$ , i.e. $d_1=f_1$ , $d_k=f_k-f_{k-1}$ (the convention is $f_0=0$ ).

The maximal function is $f^*=\sup_{n\ge1}|f_n|$ , the square function is $S(f)=\big[\sum_{k\ge1}d_k^2\big]^{1/2}$ , and $S_n(f)$ is its $n$ -th partial version. For $0<p<\infty$ ,

\|f\|_p=\sup_{n\ge1}\|f_n\|_p,\qquad \|f_n\|_p=(E|f_n|^p)^{1/p},

and $f$ is $L^p$ -bounded when $\|f\|_p<\infty$ . For $\lambda>0$ , the exit time $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ (with $\inf\emptyset=\infty$ ) is the first index at which $|f_n|$ exceeds $\lambda$ ; $f_\mu$ , $f_{\mu-1}$ , $S_{\mu-1}(f)$ denote evaluation at the random index, with $f_\infty=\lim_n f_n$ .

The Lean development names these objects dseq ( $d$ ), sqFnN/sqFn ( $S_n(f)$ , $S(f)$ ), maxFnN/maxFn ( $f_n^*$ , $f^*$ ), pNorm ( $\|f\|_p$ ), exitTime ( $\mu$ ) and valAt/sqFnAt (evaluation at an index in $\{0,1,\dots,\infty\}$ ), all in the namespace BurkholderDFI.Gundy.

Formalization targets

Goal: Theorem 4.1 (p. 23)

For every $L^1$ -bounded martingale $f$ and every $\lambda>0$ there are martingales $X,Y,Z$ relative to the same $\sigma$ -fields, with difference sequences $x,y,z$ , such that

f=X+Y+Z,\qquad \|X\|_2^2\le2\lambda\|f\|_1,\qquad \Big\|\sum_{k=1}^\infty|y_k|\Big\|_1\le4\|f\|_1,\qquad P(Z^*>0)\le\|f\|_1/\lambda.

The three bounds hold together; each alone is trivial ( $f=0+0+f$ satisfies the first two, $f=0+f+0$ the first and last).

Milestones

Doob's facts (cited, §1, p. 20). An $L^1$ -bounded martingale or nonnegative submartingale converges almost everywhere, and $\|f_\mu\|_1\le\|f\|_1$ for every stopping time $\mu$ .
(1.5) (p. 20). $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$ .
Lemma 2.1 (p. 21). For the exit time $\mu$ above $\lambda$ ,

\|S_{\mu-1}(f)\|_2^2+\|f_{\mu-1}\|_2^2\le2Ef_\mu f_{\mu-1}\le2\lambda\|f\|_1,

with equality on the left for martingales.

Significance

The result. The decomposition is the standard device for passing from $L^2$ to weak-type $(1,1)$ estimates for martingale operators: an operator that is bounded on $L^2$ , controlled by total variation on the second piece, and local in the sense that it vanishes where the third piece vanishes, is of weak type $(1,1)$ . Applications of the decomposition are given in Gundy's papers of 1968 and 1969 (On the class $L\log L$ , martingales, and singular integrals, Studia Math. 33), which the lectures cite for this purpose. The explicit constants $2$ , $4$ , $1$ make every such weak-type constant explicit.

Formalizing it. The theorem is classical and proved; the remaining work is its formalization. As far as is known, no machine-checked proof of Gundy's decomposition, of Lemma 2.1, or of the weak-type maximal inequality in the form (1.5) for real martingales exists in Mathlib or on this platform. Mathlib provides almost-everywhere convergence of $L^1$ -bounded submartingales and Doob's maximal inequality for nonnegative submartingales; the stopped-value bound for unbounded stopping times, the square-function identity of Lemma 2.1 and the decomposition itself are new. The milestones are shared with other missions of this series (Lemma 2.1 is also used for Burkholder's weak-type square function inequality and his exponential estimates), so each proof is reused.

Difficulty

The obvious attempt imitates the Calderón–Zygmund cut directly: truncate $f$ at height $\lambda$ , or stop it when it first exceeds $\lambda$ . Neither produces the required pieces. Truncation destroys the martingale property, and whatever restores it adds terms that must themselves be controlled in the right norm. Stopping at the exit time produces a martingale bounded by $\lambda$ only up to the overshoot at the exit, which is not bounded and lives on an event that is small only in probability. The $L^2$ estimate (4.2) is therefore not a consequence of boundedness; it needs a quantitative square-function bound for the martingale up to the exit, which is the content of Lemma 2.1, and that lemma in turn needs the limit $f_\infty$ and the stopped values $f_\mu$ on $\{\mu=\infty\}$ — so Doob's convergence theorem cannot be avoided.

Formalization scope

Processes are functions f : ℕ → Ω → ℝ with a Mathlib Filtration ℕ and Mathlib's Martingale/Submartingale. The paper indexes from $1$ ; Lean's index $0$ is never read by any quantity in the statements, which use the paper's convention $f_0=0$ . Mathlib's martingale definition additionally constrains $f_0=E(f_1\mid\mathcal A_0)$ ; this is no restriction, since every martingale indexed from $1$ extends this way. The goal asserts that $X,Y,Z$ are Mathlib martingales for the same filtration as $f$ , and the identity $f_n=X_n+Y_n+Z_n$ is required for $n\ge1$ .

Further committed conventions:

$S(f)$ , $f^*$ , $Z^*$ , $\|\cdot\|_p$ and all expectations of nonnegative quantities take values in $[0,\infty]$ (lower Lebesgue integral), so no infinite value is silently replaced by $0$ .
$\|X\|_2=\sup_{n\ge1}\|X_n\|_2$ , not the norm of a limit; $Z^*=\sup_{n\ge1}|Z_n|$ ; $\|\sum_k|y_k|\|_1$ is the integral of the series with $y_1=Y_1$ .
The exit time takes values in $\mathbb N\cup\{\infty\}$ and $\mu-1$ is truncated, with $\infty-1=\infty$ ; the a.e. limit $f_\infty$ is a function supplied with its convergence hypothesis (Lemma 2.1) or asserted to exist (Doob's facts).
"Nonnegative submartingale" means $f_n\ge0$ almost surely for $n\ge1$ .
$\Omega$ is an arbitrary measurable space with a probability measure.

A formalization in which the existential could choose its own filtration, or in which the norms were Bochner integrals (which vanish on non-integrable functions), would trivialize the goal; both are excluded by the statement above.

Infrastructure needed: stopped values at unbounded stopping times and their $L^1$ bound; square-function identities for stopped martingales (orthogonality of martingale differences up to a stopping time); conditional-expectation compensators of predictable truncations. The definitions file is shared with the other eight missions of this series and is reusable for any work on discrete-time square and maximal functions. Proofs of the milestones, alternative arguments, and sharper constants are all welcome.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, The Annals of Probability 1(1), 19–42, 1973. https://doi.org/10.1214/aop/1176997023
R. F. Gundy, A decomposition for L¹-bounded martingales, The Annals of Mathematical Statistics 39(1), 134–138, 1968. https://doi.org/10.1214/aoms/1177698510
D. G. Austin, A sample function property of martingales, The Annals of Mathematical Statistics 37(5), 1396–1397, 1966. https://doi.org/10.1214/aoms/1177699283
J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

5 thms3 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 3: With One Markdown or Markup Allowed, Thresholds x_n < z_n Give the Optimal PolicyResearch Paper

Motivation

Retailers of seasonal goods, home builders selling out a development, and airlines and cruise lines selling promotional fares all face the same operational question: inventory is fixed, the selling season is finite, and the price can be changed only rarely. Menu costs, advertising commitments and customer goodwill often restrict a seller to a single price change. The question is then when to change the price, and, if both a lower and a higher price are available, in which direction.

Feng and Gallego (Management Science 41(8), 1995) answered this for Poisson demand. Their §4 treats a single markdown (Theorem 1) and a single markup (Theorem 2). This mission formalizes their §5, the markup-or-markdown problem: the seller starts at a middle price and has one opportunity to move either down or up. The paper shows that the optimal policy is again described by time thresholds that depend only on the remaining stock, now two per stock level. The paper builds on the deterministic and fluid analysis of Gallego and van Ryzin (1994), where arbitrarily many price changes are allowed, and is the starting point of a literature on limited-price-change revenue management surveyed by Bitran and Caldentey (2003).

Setting

There are three prices $p_1 < p < p_2$ . At price $p_i$ demand is a Poisson process of intensity $\lambda_i$ , and at $p$ of intensity $\lambda$ , with

\lambda_1 > \lambda > \lambda_2, \qquad r_1 > r > r_2, \qquad r_i = p_i\lambda_i,\ r = p\lambda,

all prices and intensities positive. Lowering the price raises both the sales rate and the revenue rate. Salvage value is zero. Note that in this section $p_1$ is the lower price; the initial price is $p$ .

A seller with $n$ units and time-to-go $t$ sells at $p$ and may switch once, to $p_1$ or to $p_2$ . Write $N(\cdot)$ for the demand process at $p$ and $N_i(\cdot)$ for that at $p_i$ .

$J^i(n,t;s) = (p - p_i)E\min(n,N(s)) + p_iE\min(n, N(s) + N_i(t-s))$ is the expected revenue of switching to $p_i$ after $s$ time units.
$J(n,t;0) = \max\{J^1(n,t;0), J^2(n,t;0)\}$ is the revenue of switching at once to the better alternative, and $J(n,t;t) = pE\min(n,N(t))$ the revenue of never switching.
The optimal revenue is

J(n,t) = \sup_{\tau \in \mathcal T} E\bigl[p\min(n,N(\tau)) + J(n - N(\tau), t - \tau; 0)\bigr],

where $\mathcal T$ is the set of stopping times of the history of $N$ with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.

$G^i(n,t) = r - r_i - p_i(\lambda - \lambda_i)P(N_i(t) \ge n)$ .
$\Delta^i(n,t) = J(n,t;t) - J^i(n,t;0)$ and $\Delta(n,t) = J^1(n,t;0) - J^2(n,t;0)$ , with first positive zeros $t^i_n$ and $t_n$ .

Formalization targets

Goal: Theorem 3 (pp. 1385–1386)

Under the paper's assumption $t^1_n < t_n < t^2_n$ for every $n$ , there are strictly increasing sequences $(x_n)$ , $(z_n)$ with

x_n < t^1_n < t_n < t^2_n < z_n

such that $J(n,t) = V(n,t)$ , where $V(n,t) = J(n,t;0) + F(n,t)$ for $x_n \le t \le z_n$ and $V(n,t) = J(n,t;0)$ otherwise. The excess $F(n,\cdot)$ equals $H^1(n,\cdot)$ on $[x_n,t_n]$ and $H^2(n,\cdot)$ on $[t_n,z_n]$ . Each $H^i$ solves

\frac{\partial H}{\partial t} = -\lambda H + L^i(n,t), \qquad L^i(n,t) = G^i(n,t) + \lambda\bigl[V(n-1,t) - J^i(n-1,t;0)\bigr],

with $H^1(n,x_n) = 0$ and $H^2(n,t_n) = H^1(n,t_n)$ . The thresholds are $x_n = \inf\{t \ge 0 : L^1(n,t) = 0\}$ and $z_n = \inf\{t \ge t_n : H^2(n,t) \le 0\}$ .

Milestones

(16), p. 1385: $\partial J^i(n,t;0)/\partial t = r - \lambda[J^i(n,t;0) - J^i(n-1,t;0)] - G^i(n,t)$ .
Lemma 2, p. 1379, in both cases: the zeros of $G(n,\cdot)$ increase strictly in $n$ , and $G(n,\cdot)$ changes sign exactly once.
Lemma 3, p. 1382, in both cases: $J(n,t;t) - J(n,t;0)$ changes sign exactly once at a strictly increasing sequence $t_n$ , and is monotone beyond it.
Lemma 1, p. 1378: a verification criterion identifying $J(n,t)$ as the solution of a system of differential equations and inequalities.

Significance

Theorem 3 says that the two-directional problem has the same simple structure as the one-directional ones. With $m$ units left and time-to-go $u$ , the seller marks down at once when $u$ falls below $x_m$ , marks up at once when $u$ exceeds $z_m$ , and otherwise keeps the price. Because the thresholds increase with the stock, the policy reduces to a table of $2n$ numbers, which the paper computes for a housing example (Table 5). The theorem also quantifies the value of flexibility: in that example, allowing either direction adds about $1,500 over the markdown-only policy and about $7,000 over the markup-only policy.

Lemma 3 and the verification Lemma 1 are reusable beyond this mission. Lemma 3 is a sign-change property of differences of Poisson tail sums, of the kind that drives threshold results in revenue management. Lemma 1 is a sufficient condition for the value of an optimal stopping problem driven by a Poisson process. The paper's results are proved with pen and paper only; none of them has a machine-checked proof. The formalization adds a precise statement of Lemma 1, whose printed hypotheses are insufficient (see the scope section), and an explicit record of which threshold facts Theorem 3 depends on.

Difficulty

The value $J(n,t)$ is the supremum over stopping times of a continuous-time process, and the obvious approach, dynamic programming over the stock, needs the value one stock level down. The thresholds at stock $n+1$ are defined through $V(n,\cdot)$ , so the structure must be propagated from one stock level to the next, and several properties have to propagate together. One must know that $L^1(n+1,\cdot)$ again has a single sign change, which requires $V(n,\cdot) - J^1(n,\cdot;0)$ to be increasing beyond $x_n$ . One must also know that $H^2(n+1,\cdot)$ is positive up to $t^2_{n+1}$ and eventually negative, so that $z_{n+1}$ is finite, and that $z_n < z_{n+1}$ . These facts concern three different price pairs at once: $(p,p_1)$ , $(p,p_2)$ and $(p_1,p_2)$ . A direct comparison of $V$ with the two one-directional value functions fails, because the optimal direction itself depends on the stock and the time-to-go. The verification step needs a pathwise fundamental theorem of calculus for the Poisson-driven process, which is where the regularity hypothesis on $V$ matters.

Formalization scope

Model. Demand at $p$ is the counting process of i.i.d. exponential interarrival times from the published definition QueueingFundamentals_Foundations_ArrivalProcess. The rate enters through the hypothesis IsExpInterarrivals P lam T, and $N_i(t-s)$ enters only through its law: the sum $N(s) + N_i(t-s)$ is written through its Poisson $(\lambda s + \lambda_i(t-s))$ law. $\mathcal T$ is the class of real-valued stopping times $\tau$ of the σ-algebras generated by the counts $N(u)$ , $0 \le u \le s$ , with $0 \le \tau \le t$ and $N(\tau) \le n$ almost surely.
Conventions. Time is time-to-go, $t \ge 0$ ; ODEs are imposed at every $t > 0$ through HasDerivAt. Threshold sequences are indexed from $n = 1$ . Every infimum is a real sInf paired with the nonemptiness of its set. $F$ , $H^1$ , $H^2$ , $V$ and the thresholds are existentially quantified and tied together by the theorem's equations, so the existential determines the paper's objects. The page's assumption $t^1_n < t_n < t^2_n$ is a hypothesis of the goal, as on the page.
Added hypotheses. Prices and intensities are positive, the paper's standing convention. Lemma 1 as printed is false. It is stated with the boundary condition $V(n,0) = J(n,0;0)$ , the zero-stock condition $V(0,t) = 0$ , the obstacle condition $V \ge J(\cdot;0)$ , and local Lipschitz continuity of $V$ in place of "continuous and almost everywhere differentiable". The page's proof uses all four. Lemma 2's printed "bounded" is corrected to "bounded away from zero", since $y_n \to \infty$ .
No trivialization. No statement assumes the optimality identity, the verification conditions, the derivative identity (16), or any sign-change fact as a hypothesis. A goal that defined $V$ and assumed $J = V$ , or that left the thresholds unrelated to $L^1$ and $H^2$ , would not be Theorem 3.
Infrastructure needed. Poisson tail calculus (differentiation of $E\min(n, N(t))$ in $t$ ), variation-diminishing properties of the kernel $e^{-\lambda(t-u)}$ , linear first-order ODEs, and a martingale decomposition for Poisson counting processes evaluated at bounded stopping times. Contributions of any of these, or of proofs of the milestones, are welcome.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8):1371–1391, 1995. https://doi.org/10.1287/mnsc.41.8.1371
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer, 1981. https://doi.org/10.1007/978-1-4684-9477-8
S. Karlin, Total Positivity, Vol. 1, Stanford University Press, 1968.
G. Bitran and R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003. https://doi.org/10.1287/msom.5.3.203.16031

10 thms3 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 2: Markup Is Optimal Once Time-to-Go Exceeds an Increasing Threshold z_nResearch Paper

Why a promotional fare needs a switching rule

An airline may offer a low promotional fare while seats remain available, then raise the fare as departure approaches. The choice is dynamic: a sale changes both the number of seats left and the benefit of waiting. The same decision appears for hotel rooms and theater seats. Feng and Gallego study a policy with two fixed prices and at most one price change, while allowing the switching time to depend on actual sales rather than a calendar date chosen in advance. Their 1995 paper proves that this adaptive problem has an inventory-dependent threshold rule. This mission isolates the markup case, in which the second price is higher than the first.

The two-price restriction has a practical role. A seller may know the fare classes it can offer while still needing to decide when to close the promotional class. The result identifies a sequence of time thresholds that can be computed for the chosen price pair. It is therefore a structural claim about an optimal policy, not a choice of numerical prices or a claim that two prices optimize over every possible price menu.

Demand, inventory, and admissible decisions

There are $n\ge1$ items and $t\ge0$ units of time-to-go. At price $p_i$ , sales requests follow a Poisson counting process $N_i$ with rate $\lambda_i$ . Each request sells one item while stock remains. The paper assumes that demand falls as price rises and that the lower price has the higher revenue rate. Thus the markup case has

0<p_1<p_2,\qquad 0<\lambda_2<\lambda_1,\qquad p_2\lambda_2<p_1\lambda_1.

The salvage value at the end of the horizon is zero. A fixed switch at time $s\in[0,t]$ charges $p_1$ first and $p_2$ afterwards. Its expected revenue, denoted $J(n,t;s)$ , is

J(n,t;s)=(p_1-p_2)\sum_{j=1}^n\Pr\{N_1(s)\ge j\} +p_2\sum_{j=1}^n\Pr\{N_1(s)+N_2(t-s)\ge j\}.

The two counts in the last term are independent, so their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$ . This is the expression in §3 of the paper. In particular, $J(n,t;0)$ is the revenue from increasing the price immediately.

An admissible switching time $\tau$ uses only the history of sales at $p_1$ ; it lies between zero and $t$ and cannot wait past stock exhaustion. The optimal value $J(n,t)$ is the supremum of expected revenue over these stopping times. The stopping decision may react to sales before the change, but it cannot anticipate future requests. This distinction matters because a deterministic switch time generally has less information than an adaptive one.

Formalization targets

The goal is Theorem 2 on pp. 1382–1383. Define the switching function

G(n,t)=p_1\lambda_1-p_2\lambda_2 -p_2(\lambda_1-\lambda_2)\Pr\{N_2(t)\ge n\}, \qquad y_n=\inf\{u\ge0:G(n,u)=0\}.

There are thresholds $x_n,z_n$ with $y_n\le x_n<z_n$ , and $(z_n)_{n\ge1}$ is increasing. A continuation premium $F$ gives the value

J(n,t)=\begin{cases} J(n,t;0)+F(n,t),&t<z_n,\\ J(n,t;0),&t\ge z_n. \end{cases}

For $n\ge1$ , $F(n,t)=H(n,t)$ below $z_n$ and is zero at or above it; $F(0,t)=0$ . The function $H$ satisfies $H(n,0)=0$ and the differential equation $\partial_tH(n,t)=-\lambda_1H(n,t)+L(n,t)$ , where $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ . The remaining thresholds are the first nonnegative zero of $L(n,\cdot)$ and the first positive zero of $H(n,\cdot)$ :

x_n=\inf\{u\ge0:L(n,u)=0\},\qquad z_n=\inf\{u>0:H(n,u)=0\}.

The milestones reproduce equation (17), the markup half of Lemma 2, and Lemma 1. Together they identify the Poisson derivative identity, the sign change of $G$ , and the verification criterion used to relate a candidate value to optimal stopping. The paper proves the mathematical result; the mission asks for machine-checked proofs of these formal statements.

What the result supplies

The threshold sequence tells a seller when increasing the price immediately is optimal, conditional on the stock still available. The value formula also gives the benefit of continuing at the promotional price when time-to-go lies below the threshold. The statement preserves the paper's weaker word “increasing” for $z_n$ : it asserts monotonicity and does not require strict monotonicity of either sequence. The full theorem includes the recursive equations for $F$ and $H$ , so a proof of a threshold-shaped region alone would leave part of the source result unformalized.

Formalization would add a reusable optimal-stopping model built from a Poisson arrival process, a fixed-switch revenue function, and a verification lemma. The arrival process already has a published definition; the switching model and the theorem statements here are new drafts. The theorem is established in the 1995 article, while its Lean proof remains to be supplied.

Where the difficulty lies

The immediate-switch comparison $G(n,t)$ has a single sign change, but the optimal decision also depends on revenue already earned and on the value of unsold stock after each possible sale. For $n>1$ , the relevant forcing term is $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ , so the sign of $G$ alone does not locate the optimal switching threshold. A direct fixed-time comparison likewise does not establish optimality among stopping times that react to observed sales. These are the main obstacles the formal proof must address.

Formalization scope

The Lean model uses natural-number stock, nonnegative real time, positive real prices and rates, and an imported counting process built from independent exponential interarrival times. A rate is attached to each price. The history of the first process defines the stopping-time class; the second process enters through its Poisson law after a switch. The supremum ranges over admissible stopping times, and the payoff is bounded and measurable under the stated process law. The definition writes sales before switching as $\min(n,N_1(\tau))$ , equal almost surely to $N_1(\tau)$ for admissible times. The probability-measure assumption is explicit, though the exponential interarrival law entails it.

Lean assigns a default value to an empty real infimum. The theorem explicitly asserts that each defining zero set for $y_n$ , $x_n$ , and $z_n$ is nonempty; it also keeps $u>0$ in the definition of $z_n$ , since $H(n,0)=0$ . Continuity of $H(n,\cdot)$ at zero connects its boundary value to its differential equation. Lemma 1 includes its missing initial, zero-stock, obstacle, and local-Lipschitz assumptions, all required by its printed proof. The paper's word “bounded” in Lemma 2 is retained in the milestone quotation but replaced by the positive lower bound it uses; $y_n$ is unbounded as stock grows. These choices are recorded for review in the moderation notes.

The goal derives optimality from the demand and price assumptions. It does not assume the verification conditions, the sign change, or the revenue identity as premises. Contributions to the Poisson tail calculus, stopping-time measurability and boundedness, threshold zero sets, and verification argument are within scope and can be reused in related finite-inventory pricing models.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

6 thms3 active usersReviewed

Convex Optimization Information Theory Optimization+1·Captain: mikedeng1

I-Divergence Geometry of Probability Distributions and Minimization Problems 2: Under Moment Constraints the I-Projection Exists at Every Interior Point and Has Exponential-Family DensityResearch Paper

Minimum discrimination information under moment constraints

Given a reference probability distribution $R$ and a set $\mathcal E$ of probability distributions, the minimum discrimination information problem asks for the member of $\mathcal E$ closest to $R$ in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations $\int f_i\,dP = a_i$ , and the classical answer is that the minimizer is an exponential family member, with density $c\exp\sum_i t_i f_i$ with respect to $R$ .

That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the $f_i$ .

Timeline:

1959: Kullback formulates the minimum discrimination information theorem: an element of $\mathcal E$ of exponential form is the minimizer (a sufficient condition).
1966: Kullback and Khairat (Ann. Math. Statist. 37, 1966) refine the sufficient condition.
1972: Čencov proves existence of exponential-form minimizers under general conditions (Statistical Decision Rules and Optimal Inference, Theorem 23.1).
1975: Csiszár proves Theorem 3.3 by the minimizing-sequence method of his Theorem 2.1; a first version of the paper assumed $T_R = E^k$ , weakened to " $T_R$ open" after Čencov's work.

Setting

All distributions (PD's) live on one measurable space $(X,\mathcal X)$ . The I-divergence of $P$ from $Q$ is

I(P\|Q)=\int \log p_Q\,dP\ \text{ if } P\ll Q,\qquad I(P\|Q)=+\infty\ \text{ otherwise},

where $p_Q$ is the density of $P$ with respect to $Q$ ; it takes values in $[0,\infty]$ and vanishes only for $P=Q$ . The variation distance is $|P-Q|=\int|p_R-q_R|\,dR$ for any PD $R$ dominating both. If $\mathcal E$ is a convex set of PD's containing some $P$ with $I(P\|R)<\infty$ , a $Q\in\mathcal E$ with

I(Q\|R)=\min_{P\in\mathcal E} I(P\|R)

is the I-projection of $R$ on $\mathcal E$ .

Fix real-valued measurable functions $f_1,\dots,f_k$ on $X$ . For $a=(a_1,\dots,a_k)\in E^k$ (Euclidean $k$ -space) the moment set $\mathcal E(a)$ is the set of PD's $P$ with $\int f_i\,dP=a_i$ , $i=1,\dots,k$ . Further:

$A_R$ is the set of $a\in E^k$ for which $\mathcal E(a)$ contains some $P$ with $I(P\|R)<\infty$ ;
$T_R=\{t\in E^k:\ \exp\sum_i t_i f_i \text{ is } R\text{-integrable}\}$ , (3.16);
$F(a)=\inf_{P\in\mathcal E(a)} I(P\|R)$ , (3.18), the optimal value as a function of the constraint levels.

Formalization targets

Goal: Theorem 3.3

If $T_R$ is open in $E^k$ , then for every point $a$ of the interior of $A_R$ the I-projection $Q$ of $R$ on $\mathcal E(a)$ exists and

q_R(x)=c\exp\sum_{i=1}^k t_i f_i(x)\qquad R\text{-a.e.},

for some constant $c$ and some $t\in E^k$ .

Milestones

(2.2), the parallelogram identity: $I(P_m\|R)+I(P_n\|R)=2I(\tfrac{P_m+P_n}2\|R)+I(P_m\|\tfrac{P_m+P_n}2)+I(P_n\|\tfrac{P_m+P_n}2)$ .
(2.4): a minimizing sequence $P_n$ in a convex set converges in variation to a PD $Q\ll R$ (closedness of the set is not used).
Lemma 3.1: if $e^{tf}$ is $Q$ -integrable for small $|t|$ , then $I(P_n\|Q)\to0$ implies $\int f\,dP_n\to\int f\,dQ$ .
(3.18): $A_R$ is convex and $F$ is finite and convex on $A_R$ .
(3.19): at an interior point $a$ of $A_R$ there is $t$ with $F(b)\ge F(a)+\sum_i t_i(b_i-a_i)$ for all $b\in A_R$ .
Remark, p. 158: $F$ is differentiable at interior points of $A_R$ , and $\operatorname{grad}F(a)=t$ , the parameter vector of the I-projection.

Significance

Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.

The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).

Difficulty

The obvious argument fails at the first step: the moment set $\mathcal E(a)$ is convex but not closed in variation when the $f_i$ are unbounded, since $\int f_i\,dP$ is not continuous in variation. A minimizing sequence therefore converges in variation to some $Q$ (as in Theorem 2.1), but nothing places $Q$ in $\mathcal E(a)$ : mass can escape to where $|f_i|$ is large. Ruling this out needs quantitative control of $I(P_n\|Q)$ , which in turn requires knowing the form of $Q$ before knowing $Q$ is feasible; the interplay with the convexity of $F$ and the openness of $T_R$ is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.

Formalization scope

Probability distributions are Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions $\log 0=-\infty$ , $\log\frac a0=+\infty$ , $0\cdot(\pm\infty)=0$ .
The variation distance uses $P+Q$ as dominating measure (the page allows any dominating PD; the value is the same).
The I-projection carries $I(Q\|R)<\infty$ explicitly: the page defines it only when $\mathcal E$ meets $\{P: I(P\|R)<\infty\}$ .
$\mathcal E(a)$ requires $P$ -integrability of every $f_i$ , so the constraint integrals are genuine. $E^k$ is Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. $k=0$ is allowed.
$F$ is an infimum in $[0,\infty]$ (equal to $\infty$ outside $A_R$ ); statements use its real value only on $A_R$ , where it is finite. (3.18) prints $I(P\|Q)$ ; the reference measure is $R$ , as the definition of $A_R$ and the proof show. (3.16) prints $(t_1,\dots,t_n)$ for $(t_1,\dots,t_k)$ .
Densities are Radon–Nikodym derivatives and the form (3.2) is an $R$ -almost-everywhere identity with no exceptional set of positive measure.
Lemma 3.1 asserts that $f$ is $P_n$ -integrable for large $n$ as well as the convergence, so that $\int f\,dP_n$ is not a default value.
Trivializing readings are excluded: the goal asserts existence of the I-projection rather than assuming it, $T_R$ is an integrability set (not a set where a junk integral is finite), and the infimum is never a real sInf over a possibly empty set.

A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) $I(P\|R)-I(P\|Q)=\int\log q_R\,dP$ ), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.

Selected references

I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probab. 3(1), 146–158, 1975. https://doi.org/10.1214/aop/1176996454
S. Kullback, Information Theory and Statistics, Wiley, 1959.
S. Kullback and M. A. Khairat, A note on minimum discrimination information, Ann. Math. Statist. 37, 279–280, 1966.
E. T. Jaynes, Information theory and statistical mechanics, Phys. Rev. 106, 620–630, 1957. https://doi.org/10.1103/PhysRev.106.620
N. N. Čencov, Statistical Decision Rules and Optimal Inference (Russian), Nauka, 1972; English translation, American Mathematical Society, 1982.
I. N. Sanov, On the probability of large deviations of random variables (Russian), Mat. Sbornik 42, 11–44, 1957.

10 thms3 active usersReviewed

Complexity Theory Quantum Information Theoretical Computer Science·Captain: mikedeng1

Strengths and Weaknesses of Quantum Computing I: Relative to a Random Oracle, a Quantum Algorithm Needs Ω(2^{n/2}) Queries to Decide Whether 1ⁿ Has a PreimageResearch Paper

Motivation

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs $\Omega(2^{n/2})$ queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).

Timeline:

1996: Grover's algorithm searches $N$ items with $O(\sqrt N)$ queries.
1997: the paper proves $\mathbf{BQTime}(o(2^{n/2})) \not\supseteq \mathbf{NP}$ relative to a random oracle with probability 1 (Theorem 3.5), and the $\Omega(2^{n/3})$ bound for random permutations (Theorem 3.6).
1998: Boyer, Brassard, Høyer and Tapp give tight bounds for quantum searching.
1999: Zalka shows Grover's algorithm is exactly optimal.

Setting

A $T$ -query algorithm acts on vectors $\varphi \in \mathbb{C}^{(X \cup \{\bot\}) \times R \times W}$ , where $X$ is the set of query strings, $R$ the set of answers (an additive group) and $W$ a finite workspace. A basis configuration $(x, z, w)$ with $x \in X$ is querying $x$ ; $(\bot, z, w)$ is not querying. For an oracle $f : X \to R$ the oracle operator is

O_f\,|x, z, w\rangle = |x, z + f(x), w\rangle, \qquad O_f\,|\bot, z, w\rangle = |\bot, z, w\rangle .

The algorithm consists of a unit vector $\varphi_0$ , unitaries $U_0, \dots, U_{T-1}$ that do not depend on the oracle, and a set of accepting configurations. With oracle $A$ its states are $\varphi_{i+1} = U_i O_A \varphi_i$ ; the acceptance probability is the squared norm of the accepting part of $\varphi_T$ . The query magnitude of $y$ in $\varphi$ is $q_y(\varphi) = \sum_{z, w} |\varphi(y, z, w)|^2$ (Definition 3.2). The algorithm decides a property if it accepts with probability at least $2/3$ when the property holds and at most $1/3$ when it fails.

In the main theorem $X = R = \{0,1\}^n$ with bitwise addition, and the oracle is a uniformly random function $A : \{0,1\}^n \to \{0,1\}^n$ . The question is whether $1^n$ belongs to $\mathcal{L}_A = \{y : \exists x\ A(x) = y\}$ .

Formalization targets

Goal: Theorem 3.5 (finite form)

\exists\, c > 0\ \exists N\ \forall n \ge N\ \forall M \text{ with } T \le c\, 2^{n/2} \text{ queries}: \quad \Pr_A\bigl[M^A \text{ fails to decide } \exists x\ A(x) = 1^n\bigr] \ge \tfrac18 .

The constant is existential, matching the theorem's hypothesis $T(n) = o(2^{n/2})$ ; $c$ and $N$ do not depend on the workspace or the algorithm.

Milestones

Theorem 3.1: unit vectors at distance $\varepsilon$ have measurement distributions within total variation $4\varepsilon$ .
Theorem 3.3 (corrected): changing oracle answers on time–string pairs of total query magnitude $\le \varepsilon^2/T$ moves the final state by at most $2\varepsilon$ .
Corollary 3.4 (corrected): outside a set of at most $4T^2/\varepsilon^2$ strings, changing the oracle at one string moves the final state by at most $\varepsilon$ .
$\Pr[1^n \text{ has no preimage}] = ((2^n-1)/2^n)^{2^n} \ge 1/4$ .
$\Pr[1^n \text{ has a unique preimage}] = ((2^n-1)/2^n)^{2^n-1} \ge 1/e$ .
Final states within $1/13$ for $A$ and $A_y$ force failure on one of them.
The double counting: failing oracles with a unique preimage are at least half the successful oracles with none.

Significance

The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle $\mathbf{NP} \not\subseteq \mathbf{BQP}$ ; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).

The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.

Difficulty

The obvious argument — each query reveals one bit about where the preimage is, so $\Omega(2^n)$ queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across $T$ unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.

Formalization scope

The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running $T$ steps is a $T$ -query algorithm: oracle answers on lengths other than $n$ are fixed and absorbed into the unitaries, as the proof fixes them, and the input $1^n$ is absorbed into $\varphi_0$ . Queries return the full value $A(x) \in \{0,1\}^n$ ; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with $c$ halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all $(2^n)^{2^n}$ functions; total variation distance is the paper's $\sum_x |\mathcal D(x) - \mathcal D'(x)|$ without the factor $1/2$ .

Corrections: Theorem 3.3 is printed with conclusion $\le \varepsilon$ , which fails (one query string, $T = 1$ , distance $2$ at $\varepsilon = 1$ ; machine-checked); the true bound is $2\varepsilon$ . Corollary 3.4 is printed with $|S| \le 2T^2/\varepsilon^2$ , which fails (16 strings, $T = 1$ , $\varepsilon = 0.45$ ); the true bound is $4T^2/\varepsilon^2$ . The printed constant $T(n) \le 2^{n/2}/20$ in the proof of Theorem 3.5 does not support the step $2^n - \mathrm{card}(S) \ge 2^{n-1}$ even with the paper's own count; the goal states an existential constant, and $c = 1/37$ works with the corrected Corollary 3.4. The closing probability- $1$ argument over countably many machines and the class statement about $\mathbf{BQTime}$ are not formalized.

A formalization in which algorithms query at every step on every branch (no $\bot$ sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.

Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.

Selected references

C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5):1510–1523, 1997. arXiv:quant-ph/9701001
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
M. Boyer, G. Brassard, P. Høyer, A. Tapp, Tight bounds on quantum searching, Fortschr. Phys. 46, 1998. arXiv:quant-ph/9605034
C. Zalka, Grover's quantum searching algorithm is optimal, Phys. Rev. A 60, 1999. arXiv:quant-ph/9711070
R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, Quantum lower bounds by polynomials, J. ACM 48, 2001. arXiv:quant-ph/9802049
A. Ambainis, Quantum lower bounds by quantum arguments, J. Comput. Syst. Sci. 64, 2002. arXiv:quant-ph/0002066

9 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Inventory Control and Price Theory 2: For Style Goods with Uniform Demand Linear in Unit Profit, Expected Profit Is Maximized at P* = ((P₀ − 3L) + √((3L − P₀)² + 16P₀L))/4Research Paper

Pricing and stocking a perishable good

A retailer of style goods — seasonal clothing, newspapers, anything that loses most of its value when the selling period ends — must decide before the season how many units to stock, knowing demand only as a probability distribution. Units left over are liquidated at a loss; units short are sales forgone. This single-period trade-off is the newsvendor problem, and its solution, the critical-fractile rule, is one of the first results of stochastic inventory theory.

In practice the retailer also sets the price, and the price moves the demand distribution. T. M. Whitin's 1955 paper Inventory Control and Price Theory (DOI 10.1287/mnsc.2.1.61) is one of the first to put the two decisions into one model. Its Section 3 restates the critical fractile for a given price, then lets the demand distribution depend on the unit profit and asks for the unit profit and stock that jointly maximize expected profit. For one explicit family of demand laws it solves the problem in closed form. This joint price-setting newsvendor problem later grew into a large literature (Mills 1959, Karlin and Carr 1962, and the survey of Petruzzi and Dada 1999), which cites Whitin's model as its starting point.

Setting

There is one selling period. Stock $x \ge 0$ is on hand at its start. Each unit sold earns the unit profit $P$ ; each unit left over at the close is liquidated at the unit liquidation loss $L > 0$ .

Demand depends on the unit profit through its mean. The mean demand is the linear function

\mu(P) = k\,(P - P_0),

where $P_0 > 0$ is the unit profit at which demand falls to zero and $k$ is the reciprocal of the slope of the line relating unit profit and amount demanded. Demand decreases in $P$ , so $k < 0$ , and the admissible unit profits are $0 < P < P_0$ . At unit profit $P$ , demand $X$ has the rectangular (uniform) distribution on $[0, 2\mu(P)]$ .

The expected marginal profit of the $x$ -th unit is $f(x) = P\,\Pr(X \ge x)$ , the probability that it sells weighted by the unit profit, and the expected marginal loss is $g(x) = L\,\Pr(X < x)$ , the probability that it does not sell weighted by the liquidation loss. The expected profit of stocking $x$ units at unit profit $P$ is the area between them,

E(P, x) = \int_0^x \big[f(t) - g(t)\big]\,dt,

which is the expected profit on sales minus the expected liquidation loss. The equilibrium stock is

x_M(P) = -\frac{2kP(P_0 - P)}{P + L}.

Formalization targets

Goal: the optimal unit profit (Eq. (16))

With

P^* = \frac{(P_0 - 3L) + \sqrt{(3L - P_0)^2 + 16P_0L}}{4},

one has $0 < P^* < P_0$ , and for all $0 < P < P_0$ and all $x \ge 0$

E(P, x) \le E\big(P^*, x_M(P^*)\big),

with equality only at $(P, x) = (P^*, x_M(P^*))$ . The formula for $P^*$ involves only $P_0$ and $L$ : the optimal unit profit is independent of the demand slope $k$ .

Milestones, in the order of the paper

Eq. (8) — for a general demand law, profit is maximized at the stock whose probability of being sold is $L/(G + P + L)$ ( $G$ a goodwill loss per unit short). This is already proved on the platform as SupplyChainTheory.chain_optimal_fractile and enters as a reference.
Eq. (11) — on $0 \le x \le 2\mu(P)$ , $f(x) = \frac{P}{2k(P_0 - P)}x + P$ and $g(x) = \frac{-L}{2k(P_0 - P)}x$ .
Eqs. (10), (13) — on the same range, $E(P, x) = \frac{P + L}{4k(P_0 - P)}x^2 + Px$ .
Eqs. (9), (12) — $x_M(P)$ lies in $(0, 2\mu(P))$ , is the only stock with $f = g$ , and is the unique maximizer of $E(P, \cdot)$ over $x \ge 0$ .
Eq. (14) — $E(P, x_M(P)) = -kP^2(P_0 - P)/(P + L)$ .
Eq. (15) — the derivative of $P \mapsto E(P, x_M(P))$ vanishes exactly when $2P^2 + (3L - P_0)P - 2P_0L = 0$ .
Footnote 7 — the elasticity of mean demand at $P^*$ equals $P^*/(P_0 - P^*)$ , and it tends to $1$ as $P_0 \to \infty$ with $L$ fixed.

Significance

The goal is a complete closed-form solution of a joint pricing-and-stocking problem under uncertainty: one price and one stock level, explicitly, with a proof that no other pair does as well. The independence of the optimal unit profit from $k$ says that, in this family, the scale of the market does not affect the optimal margin; only the ratio of the zero-demand margin to the liquidation loss does. Footnote 7 relates the optimum to the classical monopoly rule (unit elasticity) in the limit of a negligible liquidation loss.

Whitin's derivation is calculus on closed forms and was never stated as a theorem with hypotheses. He calls the stationary point of (15) "the optimal $P$ " without checking that it is a maximum, that it is global, or that the stock beyond the support of demand cannot do better. The formalization fixes all three: the goal is a statement of global, unique optimality over the whole admissible region. No machine-checked proof of this result, of the price-setting newsvendor, or of the uniform-demand newsvendor exists on the platform; the general critical-fractile rule (8) is the only part of Section 3 already proved there.

Difficulty

The expected profit is defined from the demand law, so the closed forms (11) and (13) must be derived from the uniform distribution — probabilities of half-lines under a conditioned Lebesgue measure, and an interval integral of the resulting piecewise-linear functions. They hold only on the support of demand; beyond $2\mu(P)$ the marginal profit is $0$ and the marginal loss is $L$ , and the global statement must cover that region too.

The pricing step is where the paper is loose. Setting the derivative of (14) to zero gives a quadratic with two real roots, and a stationary point of a function on an open interval need not be its maximum. The goal asks for the global maximum over $0 < P < P_0$ and its uniqueness, and asks that it be the global maximum of the joint problem, not only of the reduced function $P \mapsto E(P, x_M(P))$ .

Formalization scope

All quantities are real numbers; stock is continuous, as in the paper's calculus. Mean demand is meanDemand k P₀ P = k * (P - P₀) and the paper's sign convention is kept: $k < 0$ is a hypothesis of every statement, as are $L > 0$ and $0 < P < P_0$ (or $P_0 > 0$ where $P$ is not fixed). The demand law is ProbabilityTheory.cond volume (Set.Icc 0 (2 * μ)); $f$ and $g$ use $\Pr(X \ge x)$ and $\Pr(X < x)$ ; $E$ is an interval integral defined for every $x$ .

The paper's loose phrases are read as follows. "Equation (9) may be solved for $x$ " becomes uniqueness of the root of $f - g$ on $x \ge 0$ ; "the equilibrium value of $x$ " becomes the unique maximizer of $E(P, \cdot)$ over $x \ge 0$ ; "differentiating (14)" becomes a HasDerivAt statement with the explicit derivative for $P \mapsto E(P, x_M(P))$ , together with the equivalence with (15); "solving (15) gives the optimal $P$ " becomes the goal's joint global maximum with equality case; "independent of $k$ " is the shape of the formula for $P^*$ ; "as $P_0$ becomes large relative to $L$ , the optimal elasticity approaches unity" becomes a limit as $P_0 \to \infty$ with $L$ fixed.

Defining $E$ by the closed form (13) instead of from the demand law would make milestones (11) and (13) tautologies and would change the model beyond the support of demand; this formalization rules that out. The paper's goodwill loss $G$ belongs to the fixed-price model of (8) and does not appear in $E$ .

A complete development needs the uniform distribution's tail probabilities, interval integrals of piecewise-linear functions, and one-variable calculus for the quadratic and the cubic $P^2(P_0 - P)/(P + L)$ ; the uniform-law lemmas are reusable for any newsvendor problem with uniform demand. Proofs of the milestones, and alternative arguments for the goal, are welcome.

Selected references

T. M. Whitin, Inventory Control and Price Theory, Management Science 2(1), 61–68, 1955. https://doi.org/10.1287/mnsc.2.1.61
E. S. Mills, Uncertainty and Price Theory, Quarterly Journal of Economics 73(1), 116–130, 1959. https://doi.org/10.2307/1883828
S. Karlin and C. R. Carr, Prices and Optimal Inventory Policy, in Arrow, Karlin and Scarf (eds.), Studies in Applied Probability and Management Science, Stanford University Press, 159–172, 1962.
N. C. Petruzzi and M. Dada, Pricing and the Newsvendor Problem: A Review with Extensions, Operations Research 47(2), 183–194, 1999. https://doi.org/10.1287/opre.47.2.183
L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Eq. (14.8) (the critical fractile, formalized on the platform as SupplyChainTheory.chain_optimal_fractile).

9 thms3 active usersReviewed

Computational Geometry Operations Research·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XII: The Euclidean Traveling Salesman Problem — P(|L_N − M| ≥ t) ≤ K e^{−t²/K} for N Uniform Points in the SquareTextbook

Motivation

The Euclidean traveling salesman problem asks for the shortest closed route through a finite set of points in the plane. Even when the points are placed independently and uniformly in a square, finding an individual shortest route is computationally difficult. A separate probabilistic question is whether the optimal length varies much from one random sample to another. In Chapter 11 of Talagrand's 1995 paper, this question motivates a concentration theorem for the tour length and for other geometric functionals with the same local regularity property.

The result is useful because a bound on fluctuations can be applied without computing the distribution of the optimal tour length. It separates the typical size of the length, which may need other geometric estimates, from the chance of a substantial deviation. The paper develops a more general concentration method for product spaces; the geometric chapter shows how its estimates can control an optimization problem whose response to changing one sample point depends strongly on the local configuration.

Setting

Let $Q=[0,1]^2$ , and let $X_1,\ldots,X_N$ be independent points uniformly distributed in $Q$ , with $N\ge1$ . A configuration is the finite set $F=\{X_1,\ldots,X_N\}$ ; repeated sample locations are represented once in $F$ . For any finite $F\subseteq Q$ , write $T(F)$ for the length of a shortest closed tour visiting every point of $F$ . The tour length of the random sample is $T_N=T(F)$ . The empty set and a singleton have tour length zero.

The main theorem concerns a functional $L$ on all finite subsets of $Q$ . A level $k\ge1$ dyadic square $C$ has side $2^{-k}$ . Say that $L$ has regularity constant $K_0>0$ when, for every finite $F$ and every finite $G\subseteq C$ , if a point of $F$ lies within Euclidean distance $2^{-k+2}$ of $C$ , then

L(F)\le L(F\cup G)\le L(F)+K_0,2^{-k}\sqrt{|G|}.

The first inequality is monotonicity under adding points. The second limits the added cost when the new points lie in a small square near an existing point. Lemma 11.2.1 says that the shortest tour functional $T$ has this property with a universal constant. In particular, the functional in the main theorem is not an arbitrary real function on samples: it must obey this condition for every admissible square and pair of finite sets.

A median $M$ of $L(F)$ is any real number for which both $P(L(F)\le M)$ and $P(L(F)\ge M)$ are at least one half. The theorem applies to every median. This convention avoids selecting one median when the distribution has more than one.

For the intermediate geometric estimates, $k_0$ is the largest integer with $2^{2k_0}\le N$ . Given a deviation parameter $t$ , $k_1$ is the integer selected by the criterion (11.1.9) after the paper sets the auxiliary Poisson intensity to $N/8$ . The number $m_k$ counts level $k$ squares that contain at most $N2^{-2k-6}$ distinct sample points. An isolation weight $\alpha(x)$ records the largest scale between $k_1$ and $k_0$ at which the square containing $x$ contains at most $N2^{-2k-7}$ sample points, and equals $2^{-k_0}$ if no such scale exists.

Formalization targets

Gaussian concentration for regular geometric functionals

For each fixed $K_0>0$ , there is a constant $K>0$ , independent of $N$ and $L$ , such that every measurable $L$ with the regularity property above satisfies, for all $t\ge0$ ,

P\bigl(|L(F)-M|\ge t\bigr)\le K\exp(-t^2/K).

This is Theorem 11.2.2, the goal. Its constant may depend on the fixed regularity constant $K_0$ . Lemma 11.2.1 makes the tour length a direct instance. The milestone list also includes the quantitative sparse-square estimate of Proposition 11.1.4, the isolation-weight bound of Proposition 11.2.3, and the deterministic insertion estimate of Proposition 11.2.5. These retain the paper's specified thresholds and the dependency of their constants.

Significance

For $T_N$ , the result supplies a tail bound whose scale does not grow with the number of sample points. It says that the shortest tour length lies near a median with a Gaussian-form upper bound on the probability of a deviation. It does not identify the median or give an algorithm for finding the optimal tour. The abstract form also covers other finite-set functionals once their local regularity condition is established.

The paper proves these claims in ordinary mathematics. This mission asks for machine-checked proofs of the stated concentration, geometric occupancy, and tour-insertion results. The reusable outputs include a finite-set model of Euclidean tours and a precise interface for local regularity; the dyadic occupancy and isolation-weight definitions can support later sections on other geometric structures. No machine-checked proof of these specific chapter results is claimed here.

Difficulty

A naive bounded-differences estimate treats the effect of changing a sample point as if a single fixed worst-case insertion cost applied everywhere. That loses the paper's uniform fluctuation scale: a point can be unusually isolated, and its insertion cost can be much larger than the cost near a typical dense cluster. The central problem is to keep track of those irregular locations while retaining a bound uniform in $N$ . The chapter's dyadic-square counts and isolation weights make this difficulty explicit in the statements.

Formalization scope

Points are pairs of real coordinates constrained to $[0,1]$ , represented as functions on Fin 2. Their distance is the Euclidean $\ell^2$ distance, defined explicitly; the default norm on a Lean function space would give a different metric. The random sample is a product of coordinatewise uniform probability measures. $F$ is the set of distinct sampled locations, so ties have a defined value. Tour length is the minimum cyclic tour cost over the finite set, using the published generic metric-TSP tour model as its base.

Dyadic squares are closed in the local regularity condition. For the single square assigned to a point in the definition of $\alpha$ , the implementation uses half-open cells, with the right endpoint $1$ assigned to the final cell. This resolves only grid-line ties, which have probability zero under the stated sample law. Counts use distinct locations, as does the paper's set $F$ . All probability inequalities are compared in the extended nonnegative reals. The event bound is written with ENNReal.ofReal; a negative formal lower bound represents the paper's trivial probability lower bound. The main theorem explicitly assumes measurability of the sample functional, following the paper's convention that all relevant functions are measurable. Theorems in Section 11.1 retain $t\ge1$ and $t\le\sqrt N/K$ ; the main theorem covers every $t\ge0$ .

The formalization must not replace the square's uniform law by an arbitrary distribution, use a supremum-norm tour, or place the existential constant after $N$ or $L$ . Contributions toward the goal may develop measure-theoretic facts about the product law, finite Euclidean tours, dyadic occupancy bounds, or the insertion estimate. Those interfaces have uses beyond this chapter.

Selected references

Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.

7 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces VII: Bin Packing — P(|B_N − M| ≥ 1 + u) ≤ 8 exp(−u²/(64 N E X₁²))Textbook

Motivation

Bin packing asks for the minimum number of unit-capacity bins into which a list of items with sizes in $[0,1]$ can be packed. It is one of the basic NP-hard problems of combinatorial optimization and operations research, and its stochastic version, where the item sizes are random, has a large literature (Coffman and Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, 1991). A first question about the random optimum is how strongly it concentrates around its typical value.

A short history of that question, as Talagrand recounts it on p. 151 of the source:

Late 1980s. Martingale methods (Rhee–Talagrand; McDiarmid, On the method of bounded differences, 1989) give $P(|B_N - \mathbb E B_N| \ge t) \le 2\exp(-2t^2/N)$ for $N$ i.i.d. items. The exponent ignores the item sizes.
1994. Since $B_N$ behaves like $\sum_i X_i$ when the items are small, the right exponent should be of order $t^2/(N\operatorname{var} X_1)$ , or at least $t^2/(N\,\mathbb E X_1^2)$ . The second form was proved by W. Rhee (Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385) using non-trivial bin-packing theory.
1995. Talagrand (Publ. Math. IHÉS 81, Chapter 6) derives the $t^2/(N\,\mathbb E X_1^2)$ bound in a few lines from his convex hull distance inequality, using only trivial facts about bin packing.

This mission formalizes that chapter.

Setting

Let $\Omega = [0,1]$ and $N \ge 0$ . A point $x = (x_1,\dots,x_N) \in \Omega^N$ is a list of item sizes. A packing into $k$ bins is a map $\sigma : \{1,\dots,N\} \to \{1,\dots,k\}$ with $\sum_{i:\sigma(i)=j} x_i \le 1$ for every bin $j$ . The bin packing number $B_N(x)$ is the least $k$ for which a packing exists ( $N$ bins always suffice; $B_N = 0$ when $N = 0$ ).

Further notation, as in Lean (TalagrandConc.BinPacking):

$\|x\|_2 = (\sum_{i \le N} x_i^2)^{1/2}$ (l2Norm);
for real $a$ , the level set $A(a) = \{y \in \Omega^N : B_N(y) \le a\}$ (levelSet);
for $A \subseteq \Omega^N$ and $x \in \Omega^N$ , $U_A(x) = \{s \in \{0,1\}^N : \exists y \in A,\ s_i = 0 \Rightarrow x_i = y_i\}$ , its convex hull $V_A(x) \subseteq \mathbb R^N$ , and the convex hull distance $f_c(A,x)$ , the Euclidean distance from $0$ to $V_A(x)$ , valued in $[0,+\infty]$ (U, V, convexDist);
$\mu$ a probability measure on $[0,1]$ , $P = \mu^{\otimes N}$ the product probability on $[0,1]^N$ , whose coordinates $X_1,\dots,X_N$ are i.i.d. items with law $\mu$ , and $\mathbb E X_1^2 = \int \omega^2\,d\mu(\omega)$ (secondMoment);
$M$ is a median of $B_N$ if $P(B_N \le M) \ge 1/2$ and $P(B_N \ge M) \ge 1/2$ (IsMedian).

Formalization targets

Goal: Theorem 6.5 (p. 152)

For every median $M$ of $B_N$ and every $u$ with $0 \le u \le 8\sqrt2\,N\,\mathbb E X_1^2$ ,

P\big(|B_N(X_1,\dots,X_N) - M| \ge 1 + u\big) \le 8\exp\Big(-\frac{u^2}{64\,N\,\mathbb E X_1^2}\Big).

Milestones

Lemma 6.1 (p. 151): $B_N(x_1,\dots,x_N) \le 2\sum_{i\le N} x_i + 1$ .
Lemma 6.2, Eq. (6.2) (p. 151): for $a > 0$ and all $x$ , $B_N(x) \le a + 2\|x\|_2\, f_c(A(a),x) + 1$ .
Lemma 6.3, Eq. (6.3) (p. 152): $P(\|x\|_2 \ge 2\sqrt N(\mathbb E X_1^2)^{1/2}) \le \exp(-2N\,\mathbb E X_1^2)$ .
Proposition 6.4, Eq. (6.4) (p. 152): for all $t > 0$ , $a > 0$ ,

P(B_N \le a)\,P\big(B_N \ge a + 4t\sqrt N(\mathbb E X_1^2)^{1/2} + 1\big) \le e^{-t^2/4} + e^{-2N\,\mathbb E X_1^2}.

The goal keeps the paper's explicit constants $8$ , $64$ and $8\sqrt2$ .

Significance

The result. Theorem 6.5 shows that the random optimum $B_N$ fluctuates on the scale $\sqrt{N\,\mathbb E X_1^2}$ rather than $\sqrt N$ . For small items ( $\mathbb E X_1^2 \to 0$ ) this is much sharper than the martingale bound, and it is the scale of the fluctuations of $\sum_i X_i$ , which is a lower bound on $B_N$ . Chapter 6 is also the first application in Part II of the paper, and its scheme recurs in the later chapters: a deterministic lemma relating the functional to $f_c$ of a level set, a tail bound for an auxiliary factor, and Theorem 4.1.1 to finish.

Formalizing it. The result is proved (Talagrand 1995; Rhee 1994 by another route). No machine-checked proof is known to exist: the platform has no random bin packing statement and no general- $\Omega$ form of Talagrand's convex distance inequality. A complete development gives a checked concentration bound for an NP-hard combinatorial optimum, plus a bin-packing layer (the optimum as a minimum over assignments, Lemma 6.1, monotonicity in the item set) that other formalizations can reuse.

Difficulty

The obvious route is a bounded-differences argument: changing one item changes $B_N$ by at most one. That route yields only the exponent $t^2/N$ , because it cannot see that small items change little. Replacing the Hamming geometry by one weighted by item sizes is the point. The weights $x_i$ depend on the point $x$ itself, so no fixed weighted Hamming distance works. The convex hull distance $f_c$ controls every weighting at once, and the resulting factor $\|x\|_2$ is random and must be controlled separately (Lemma 6.3). In Lean, the further difficulty is the probabilistic input: Theorem 4.1.1 / Eq. (4.1.2) for a general (non-finite) $\Omega = [0,1]$ is not available, and the convex-hull minimax step (Lemma 4.1.2) behind Lemma 6.2 must be formalized too.

Formalization scope

$\Omega = [0,1]$ is Mathlib's unitInterval. Coordinates are Fin N (0-based). $P$ is Measure.pi (fun _ : Fin N => μ) for μ : Measure unitInterval with IsProbabilityMeasure μ. No density is assumed.
$B_N$ is sInf {k : ℕ | IsPacking x k}, an exact minimum over assignments Fin N → Fin k, not a heuristic such as First Fit. Zero-size items are allowed, as in the paper.
$f_c$ is an infimum in ℝ≥0∞ with the Euclidean norm written out ( $+\infty$ for an empty set; Mathlib's default norm on Fin N → ℝ is the sup norm). Lemma 6.2 is stated in ℝ≥0∞.
Probabilities are ℝ≥0∞-valued. Every event in the statements ( $\{B_N \le a\}$ , $\{\|x\|_2 \ge c\}$ ) is Borel. The paper's measurability convention matters only inside the proofs.
Theorem 6.5 makes the paper's implicit $u \ge 0$ explicit, and it is stated for every median, not for a chosen one. Lean's $u^2/0 = 0$ matters only in the degenerate case $N\,\mathbb E X_1^2 = 0$ , which forces $u = 0$ . There the bound is $8$ .
Not admissible: weakening the range of $u$ (the bound fails for large $u$ when $\mathbb E X_1^2$ is small), replacing $\mathbb E X_1^2$ by $1$ , or defining $B_N$ through a heuristic or a real-valued sInf.
Infrastructure needed: Talagrand's inequality (4.1.2) on a general product probability space (posed on the platform only in a finite-alphabet form) and Lemma 4.1.2. Both are welcome as separate contributions. A Chebyshev/exponential-moment bound gives Lemma 6.3.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 6, pp. 151–152. https://doi.org/10.1007/BF02699376
W. Rhee, Inequalities for the Bin Packing Problem III, Optimization 29 (1994), 381–385.
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, LMS Lecture Note Series 141, Cambridge Univ. Press, 148–188. https://doi.org/10.1017/CBO9781107359949.008
E. G. Coffman Jr., G. S. Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, Wiley, 1991.

6 thms3 active usersReviewed

Bandit Algorithms Operations Research Statistics·Captain: mikedeng1

Some Aspects of the Sequential Design of Experiments II: Staying on Heads and Switching on Tails Loses at Most 3 − 2√2 per Toss in the Long RunResearch Paper

Motivation

In 1952 Herbert Robbins asked how a statistician should draw a sample sequentially from two populations when the goal is the largest possible expected total, not a test or an estimate after the fact (Robbins 1952). This is the problem now called the two-armed bandit, and Robbins' paper is the usual starting point of the multi-armed bandit literature that underlies clinical-trial allocation, adaptive experimentation and online recommendation (Lattimore and Szepesvári 2020).

Robbins illustrated the problem with two coins. His first concrete rule, "stay on heads, switch on tails" (later known as win-stay, lose-shift or play the winner), uses only the outcome of the last toss, yet its long-run loss relative to an observer who knows the better coin is at most $3-2^{3/2}\approx 0.172$ per toss, against $1/2$ for a rule that ignores the outcomes. The same rule was studied again in clinical-trial design as "play the winner" (Zelen 1969).

Timeline. 1952: Robbins computes the operating characteristics of the stay-or-switch rule $R_1$ and of the outcome-blind rule $R_0$ for two coins, and shows that a greedy rule with sparse forced sampling attains $\max(\alpha,\beta)$ for arbitrary populations with finite means (Section 2). 1969: Zelen proposes the play-the-winner rule for clinical trials. 1985: Lai and Robbins give the logarithmic lower bound on regret and rules that attain it (Lai and Robbins 1985).

Setting

Two coins $A$ and $B$ have unknown head probabilities $\alpha$ and $\beta$ , with $0\le\alpha,\beta\le1$ . A head pays $\$ 1 $, a tail pays nothing. If$ x_i\in{0,1} $is the payoff of the$ i $-th toss,$ S_n=x_1+\dots+x_n $is the total received after$ n $tosses. In the formal development the pair of coins is a **two-armed stochastic bandit**: arm$ 0 $is coin$ A $, with payoff law$ (1-\alpha)\delta_0+\alpha\delta_1 $, and arm$ 1 $is coin$ B $, with payoff law$ (1-\beta)\delta_0+\beta\delta_1$.

A sampling rule chooses the coin for each toss from the outcomes of the earlier tosses. Two rules are studied.

Rule $R_1$ . For the first toss choose $A$ or $B$ at random. Then, for $i=1,2,\dots$ , if the $i$ -th toss results in heads, use the same coin for the $(i+1)$ -th toss; if it results in tails, switch to the other coin.
Rule $R_0$ . Choose one of the two coins at random and then use it for every toss.

Write $p_i$ for the probability of heads on the $i$ -th toss under the rule in use, and $\mathrm E(S_n/n)$ for the expected average payoff of the first $n$ tosses. The paper's two parameters are

\gamma=\frac{\alpha+\beta}{2},\qquad \delta=\frac{|\alpha-\beta|}{2},

so that $\max(\alpha,\beta)=\gamma+\delta$ is the expected payoff per toss of an observer who knows the better coin. Following the paper, $\alpha$ and $\beta$ are assumed not both $0$ and not both $1$ ; then $|\alpha+\beta-1|<1$ .

Formalization targets

Goal: the asymptotic loss of $R_1$ and its maximum

Under $R_1$ ,

\lim_{n\to\infty}\mathrm E\!\left(\frac{S_n}{n}\right)=\gamma+\frac{\delta^2}{1-\gamma}, \qquad L(A,B,R_1)=\lim_{n\to\infty}\left[\max(\alpha,\beta)-\mathrm E\!\left(\frac{S_n}{n}\right)\right]=\delta\left[1-\frac{\delta}{1-\gamma}\right],

and for every admissible pair of coins

0\le L(A,B,R_1)\le M_1=3-2^{3/2},

with equality at $\alpha=0,\ \beta=2-2^{1/2}$ and at $\alpha=2-2^{1/2},\ \beta=0$ (Eqs. (6), (8) and the text after (8), p. 531).

Milestones, in the order of the argument

Eq. (2): $p_{i+1}=(\alpha+\beta-1)p_i+(\alpha+\beta-2\alpha\beta)$ for $i\ge1$ .
Eq. (3): the closed form $p_i=(\alpha+\beta-1)^{i-1}\bigl[p_1-c\bigr]+c$ with $c=(\alpha+\beta-2\alpha\beta)/(2-(\alpha+\beta))$ .
Eqs. (4)–(5): $\lim_i p_i=c=\gamma+\delta^2/(1-\gamma)$ .
Eq. (6): both $\mathrm E(S_n/n)$ and $(p_1+\dots+p_n)/n$ have the stated limit.
Eqs. (7)–(8) and $M_1$ : $\max(\alpha,\beta)=\gamma+\delta$ and $0\le\delta[1-\delta/(1-\gamma)]\le 3-2^{3/2}$ , with the two maximizers.
Rule $R_0$ : $L(A,B,R_0)=\delta$ , whose maximum over the admissible pairs is $M_0=1/2$ , at $(0,1)$ and $(1,0)$ .

Significance

The result. The goal quantifies how much an extremely simple adaptive rule recovers. A rule blind to outcomes loses up to half a dollar per toss; one bit of memory cuts the worst case to about $0.172$ . Robbins used this comparison to argue that the sequential design problem has nontrivial, computable answers, and to motivate the forced-sampling rule $\bar R$ of the same section, whose loss tends to $0$ . The closed forms (3)–(6) are the exact operating characteristics of the four-state Markov chain $(\text{coin},\text{outcome})$ that $R_1$ generates.

Formalizing it. The results are classical and elementary on paper, but none of them has a machine-checked proof. The mission produces a verified chain from the canonical bandit measure to an explicit long-run payoff: the head probability of a fixed toss is computed from the law of the whole trajectory, the recursion is derived from the rule's kernels, and the Cesàro limit closes the argument. The same pattern applies to any finite-memory bandit rule, and the coin bandit and the two rules are reusable test cases for the platform's bandit library. No platform theorem states $R_1$ , its recursion or its loss; other two-state models on the platform (a Markov-renewal gain rate, an MDP gadget) are different objects.

Difficulty

The recursion (2) is a statement about the trajectory law, not about a Markov chain given in advance: the chain $(\text{coin}_i,x_i)$ has to be extracted from the Ionescu–Tulcea construction of the bandit measure, where the coin of toss $i+1$ is a deterministic function of toss $i$ and the payoff is drawn from the chosen coin's law. The head probability alone is not a Markov chain: $p_{i+1}$ depends on the joint law of coin and outcome at toss $i$ , so a naive one-step argument on $p_i$ does not apply, and the affine form of (2) is a property of this particular rule. The maximization in (8) is over a two-dimensional region whose maximizers lie on the boundary $\alpha=0$ or $\beta=0$ , and the excluded corners are exactly where the formula $\delta/(1-\gamma)$ breaks down.

Formalization scope

The bandit is the published BanditAlgorithm.StochasticBandit 2; the rules are policies of the published type BanditPolicy 2, and probabilities and expectations are taken under the published infinite-horizon measure banditTrajMeasure, whose coordinate $t$ is toss $t+1$ . Head probabilities are elements of unitInterval. The conventions committed to are:

"At random" for the first coin of $R_1$ and $R_0$ is the fair choice, probability $1/2$ each.
Heads is the payoff value $1$ ; $p_i$ is defined for $i\ge1$ and every statement quantifies over $i\ge1$ or $n\ge1$ .
"Not both $0$ or both $1$ " is the hypothesis $\neg(\alpha=0\wedge\beta=0)\wedge\neg(\alpha=1\wedge\beta=1)$ , never $0<\alpha$ or $\alpha<1$ , which would remove the maximizer $\alpha=0$ . Robbins states it immediately before Eq. (2), and the Lean carries it through the probability and loss results.
The paper's " $\lim E(S_n/n)=\lim (p_1+\dots+p_n)/n$ " is stated as convergence of both sequences to the same value.
" $L(A,B,R_1)$ has its maximum value $M_1$ when …" is read as: $L\le M_1$ for every admissible $(\alpha,\beta)$ , and $L=M_1$ at both named points ("or vice versa").
$2^{3/2}$ is written $2\sqrt2$ . The numerical asides ( $\approx .172$ , $\approx .586$ , "17.2 cents") are not formalized, nor is the "tossing the two coins alternately" variant of $R_0$ .

The asymptotic loss is stated as the limit of $\max(\alpha,\beta)-\mathrm E(S_n/n)$ ; defining $L$ by its closed form would make the goal a tautology. Likewise, the head probabilities are computed from the law of the rule on the coins: positing a sequence that satisfies (2) would drop the probabilistic content.

A complete development needs: the one-dimensional marginals of banditTrajMeasure (the law of coordinate $t+1$ given the prefix), the joint law of (coin, payoff) at each toss, linearity of expectation for bounded payoffs, a Cesàro-mean lemma, and a short two-variable optimization. The trajectory-marginal lemmas are reusable for every bandit mission on the platform; contributions that prove them in general are welcome.

Selected references

H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58(5) (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
M. Zelen, Play the winner rule and the controlled clinical trial, J. Amer. Statist. Assoc. 64 (1969), 131–146. https://doi.org/10.1080/01621459.1969.10500959
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6 (1985), 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

12 thms3 active usersReviewed

Completed

Markov Chain Operations Research Stochastic Systems·Captain: mikedeng1

Stochastic Processes Occurring in the Theory of Queues and their Analysis by the Method of the Imbedded Markov Chain: In GI/M/s, a Positive Wait Is Exponential and a Positive Queue GeometricResearch Paper

Motivation

A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).

Timeline:

Erlang (1908–1929) treated M/M/s, where the queue length is itself Markovian.
Kendall (1951) treated M/G/1 by a chain imbedded at departure epochs.
W. L. Smith (Kendall's ref. [19]) observed that for a single server, under restrictions on the input law, exponential service gives an exponential waiting time apart from an atom at zero.
Kendall (1953), this paper, treated GI/M/s for every input law and every number of servers $s$ , and showed that Smith's restrictions are unnecessary.
Foster (1953) gave the criterion for ergodicity of a denumerable chain through a summable invariant vector, which is the step Kendall's argument relies on.

Setting

Customers arrive with independent inter-arrival times of law $A$ on $[0,\infty)$ and mean $a$ , $0<a<\infty$ . There are $s\ge 1$ servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean $b$ , $0<b<\infty$ . The relative traffic intensity is $\rho=b/(sa)$ .

The state of the imbedded chain at an arrival epoch is the number $i\in\{0,1,2,\dots\}$ of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix $P=[p_{ij}]$ of eq. (8) is given in three blocks, written with the death-process probabilities $[n\mid m]=\int_0^\infty\binom{m}{n}(1-e^{-u/b})^n e^{-(m-n)u/b}\,dA(u)$ of (9)–(10), the probabilities $\{n\mid s;m\}$ of (11)–(12), and the Poisson probabilities $(n\mid s)=\int_0^\infty e^{-su/b}(su/b)^n/n!\,dA(u)$ of (13)–(14):

p_{ij}=\begin{cases}(i+1-j\mid s) & j\ge s,\ j\le i+1,\\ [\,i+1-j\mid i+1\,] & i<s,\ j<s,\ j\le i+1,\\ \{s-j\mid s;\,i-s+1\} & i\ge s,\ j<s,\\ 0 & j>i+1.\end{cases}

The key function is

F(\lambda)=\int_0^\infty e^{-(1-\lambda)su/b}\,dA(u).

The queue size met by an arrival is $Q=\max(i-s,0)$ . The waiting time $w$ is, given $i$ , the sum of $k=\max(i-s+1,0)$ independent exponential variables of mean $b/s$ .

Formalization targets

Goal: Theorem IV (p. 350)

When $\rho<1$ the chain has a limiting distribution $\pi$ , and with $\lambda$ the root of $F(\lambda)=\lambda$ in $(0,1)$ and $c=b/(s(1-\lambda))$ ,

\Pr(Q=n\mid Q>0)=(1-\lambda)\lambda^{n-1}\ (n\ge1),\qquad \Pr(w>t\mid w>0)=e^{-t/c}\ (t\ge0),

with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: $\lambda$ and $c$ are determined by $A$ , $b$ and $s$ .

Milestones

The matrix is stochastic (p. 349), and the chain is irreducible and aperiodic (p. 347).
The coefficients $(n\mid s)$ are positive, sum to one and have mean $1/\rho$ ; $F(\lambda)=\sum_n (n\mid s)\lambda^n$ ; for $\rho<1$ the equation $F(\lambda)=\lambda$ has a unique root in $(0,1)$ (p. 348–349).
For the trial vector $x=[\mu_0,\dots,\mu_{s-2},1,\lambda,\lambda^2,\dots]$ (15): the invariance equations for $j\ge s$ are equivalent to $F(\lambda)=\lambda$ ; those for $1\le j\le s-1$ determine the $\mu$ 's; the one for $j=0$ follows from the row sums (pp. 348–349).
A nonnull absolutely summable invariant vector makes the chain ergodic, and normalized it is the limiting distribution (p. 348).
Theorem I: for $\rho<1$ the chain is irreducible and ergodic, and $\pi_j=C\lambda^{j-(s-1)}$ for $j\ge s-1$ .
Theorem II: $\Pr(Q=0)=\alpha=\dfrac{\sum\mu+1+\lambda}{\sum\mu+1/(1-\lambda)}$ and $\Pr(w=0)=\beta=\dfrac{\sum\mu+1}{\sum\mu+1/(1-\lambda)}$ .
Theorem III: $E(Q)=(1-\alpha)/(1-\lambda)$ and $E(w)/b=(1-\beta)/(s(1-\lambda))$ .
Eq. (27): for M/M/s the root is $\lambda=\rho$ .

Significance

Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number $\lambda$ . All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing $\lambda$ from a one-dimensional equation and the finitely many $\mu$ 's from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.

The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of $Q$ and $w$ from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover $s\ge2$ .

Difficulty

The obvious route is to guess the geometric tail and check it against the balance equations. For $j\ge s$ this works, but the rows $i\ge s$ of the block $\mathbf B$ involve the convolution integral (11), and the equations for $j<s$ couple the geometric tail to the boundary terms $\mu_0,\dots,\mu_{s-2}$ . Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give $p^n_{ij}\to\pi_j$ . That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.

Formalization scope

The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and $w$ by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are $0$ -based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all $i,j$ , not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by $[0,\infty)$ , integrable, mean $a$ ), and $(n\mid s)$ is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.

Trivializing formalizations are ruled out: $\lambda$ is tied to $F(\lambda)=\lambda$ on $(0,1)$ rather than free; $\pi$ is the limiting distribution of $P$ , asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the $\mu$ 's of Theorems II–III are characterized by the invariance equations, never defined from $\pi$ .

A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block $\mathbf B$ , and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.

Selected references

D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950, ch. 15.
W. L. Smith, On the distribution of queueing times, Proc. Cambridge Philos. Soc. 49, 449–461, 1953 (cited by Kendall as "to be published", ref. [19]).
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.

22 thms3 active usersReviewed

Analysis Operations Research·Captain: mikedeng1

The Data-Driven Newsvendor Problem: New Bounds and Insights II: Every Log-Concave Demand Has Weighted Mean Spread at Least min(b,h)/(b+h)Research Paper

Motivation

The newsvendor problem is the basic single-period inventory model: a decision maker orders $q$ units before a random demand $D$ is observed, pays $b>0$ per unit of unmet demand and $h>0$ per unit left over, and minimizes the expected cost $C(q)=E[b(D-q)^+ + h(q-D)^+]$ . When the distribution of $D$ is known, the optimal order is the $b/(b+h)$ quantile of $D$ . In practice the distribution is unknown and only a sample of past demands is available; the standard data-driven order is the sample average approximation (SAA), the $b/(b+h)$ quantile of the empirical distribution.

R. Levi, G. Perakis and J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights (Operations Research 63(6), 2015), ask how many samples guarantee that the SAA order is $\epsilon$ -optimal with high probability. Levi, Roundy and Shmoys (2007) gave a distribution-free bound. Levi, Perakis and Uichanco show that, asymptotically in $\epsilon$ , the right measure of difficulty is a single scalar of the demand law, the weighted mean spread at the critical quantile, and that for the class of log-concave demand distributions (normal, uniform, exponential, logistic, Laplace and many others used in inventory theory) this scalar is bounded below by $\min(b,h)/(b+h)$ . That uniform bound turns a distribution-dependent sample-size guarantee into one that holds for every log-concave demand, and is markedly tighter than the distribution-free one.

This mission formalizes the bound (Proposition 2) and the chain of lemmas the paper uses to prove it. The source is the authors' accepted manuscript of the paper (MIT DSpace), cited by its own page numbers.

Setting

Fix costs $b>0$ , $h>0$ and the critical ratio $\beta=b/(b+h)\in(0,1)$ . A demand law is given by a probability density $f:\mathbb R\to\mathbb R$ : measurable, nonnegative, with $\int f=1$ . Its cdf is $F(t)=\int_{(-\infty,t]}f$ , and its $\beta$ quantile is

q^*=\inf\{q : F(q)\ge \beta\}.

The absolute mean spread (AMS, Definition 1) at $t$ is the gap between the conditional means above and below $t$ ,

\Delta(t)=E(D\mid D\ge t)-E(D\mid D\le t)=\frac{\int_{[t,\infty)}x f(x)\,dx}{1-F(t)}-\frac{\int_{(-\infty,t]}x f(x)\,dx}{F(t)},

and the weighted mean spread (WMS, Definition 2) is $\Delta(q^*)f(q^*)$ .

A density is log-concave (Definition 3) if $\log f$ is concave on its support. Equivalently, $f(x)^a f(y)^{1-a}\le f(ax+(1-a)y)$ for all $x,y$ and $a\in[0,1]$ ; this form allows $f$ to vanish outside an interval.

For a log-concave $f$ and a point $t$ with $f(t)>0$ , the number $\gamma_1$ is a supergradient of $\log f$ at $t$ , written $\gamma_1\in\partial\log f(t)$ , if $\log f(x)\le\log f(t)+\gamma_1(x-t)$ for all $x$ with $f(x)>0$ . The paper splits the class $\mathbb L$ of log-concave densities into the subclasses $\mathbb L_{q^*,\gamma_0,\gamma_1}$ of densities with quantile $q^*$ , $f(q^*)=\gamma_0$ and $\gamma_1\in\partial\log f(q^*)$ , and minimizes the AMS over each subclass (problem (11)). The minimizer is the truncated exponential density

\tilde f(x)=\gamma_0e^{\gamma_1(x-q^*)}\ \text{ on }[\underline x,\overline x],\qquad \underline x=q^*+\tfrac1{\gamma_1}\log\!\big(1-\tfrac{\gamma_1}{\gamma_0}\beta\big),\quad \overline x=q^*+\tfrac1{\gamma_1}\log\!\big(1+\tfrac{\gamma_1}{\gamma_0}(1-\beta)\big),

and zero elsewhere (display (12)), with AMS $z^*_{q^*,\gamma_0,\gamma_1}$ in closed form.

The Lean development uses the names IsPdf, cdfOf, quantileOf, ams, IsLogSupergradient, tildeF and zStar for these objects, in the namespace DataDrivenNV.WMS.

Formalization targets

Goal: Proposition 2

For every log-concave density $f$ ,

\Delta(q^*)\,f(q^*)\ \ge\ \frac{\min(b,h)}{b+h}.

The statement has no further hypothesis: no moment condition, no continuity, no restriction on $\gamma_0,\gamma_1$ .

Milestones, in the order of the paper's proof

Lemma 1: at the quantile, $-\frac{b+h}{h}\le\frac{\gamma_1}{\gamma_0}\le\frac{b+h}{b}$ .
Lemma 2: $f(x)\le\gamma_0e^{\gamma_1(x-t)}$ for every $x$ .
Lemma 3 (Domination Lemma): a density dominated on the support of another, with the same mass left of $t$ , has the larger AMS at $t$ .
Proposition 1: $\tilde f$ belongs to $\mathbb L_{q,\gamma_0,\gamma_1}$ and minimizes the AMS there.
The closed form: $\Delta_{\tilde f}(q)=z^*_{q,\gamma_0,\gamma_1}=\frac{\gamma_0}{\gamma_1^2}\big[(\frac{b+h}{h}+\frac{\gamma_1}{\gamma_0})\log(1+\frac{\gamma_1}{\gamma_0}\frac{h}{b+h})+(\frac{b+h}{b}-\frac{\gamma_1}{\gamma_0})\log(1-\frac{\gamma_1}{\gamma_0}\frac{b}{b+h})\big]$ .
Lemma 4: three elementary inequalities in $\beta\in(0,1)$ and $\eta\in(-\frac1{1-\beta},\frac1\beta)$ .

Significance

The proposition is what makes the paper's log-concave sample-size bound (Theorem 4) parameter-free: the probability that the biased SAA order is $\epsilon$ -optimal is, asymptotically, at least $1-2\exp(-\frac14N\epsilon\,\Delta(q^*)f(q^*))$ (Theorem 3), and Proposition 2 replaces the unknown $\Delta(q^*)f(q^*)$ by $\min(b,h)/(b+h)$ . A manager who only knows that demand is log-concave can then size a sample without estimating any parameter of the law.

The result is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. Formalizing it produces a checked lower bound for an inventory-theory quantity together with reusable facts about log-concave densities on the line: exponential envelopes from a supergradient, the quantile-and-slope constraints of Lemma 1, and the comparison of conditional means behind the Domination Lemma.

Difficulty

The definitions are elementary, but the proof passes through an infinite-dimensional optimization problem over a class of densities. The obvious first step, "the AMS is minimized by the most concentrated density", has no direct meaning without fixing the density value and the slope of $\log f$ at the quantile; after fixing them, one needs the envelope of Lemma 2, a stochastic comparison (Lemma 3) and an explicit integral of a truncated exponential. The Domination Lemma as printed is false (a density whose support has a gap to the right of $t$ is a counterexample), so it is formalized under the hypothesis that the dominating density is positive exactly on an interval around $t$ , which is how Proposition 1 uses it. The case $\gamma_1=0$ (uniform minimizer) and the two boundary values of $\gamma_1/\gamma_0$ (one-sided exponential minimizers) are not covered by the closed form (12) and must be handled separately in a proof of the goal. Finally, Lemma 1 rests on the monotonicity of the failure rate $f/(1-F)$ and the reversed hazard rate $f/F$ of log-concave laws, which must be proved from log-concavity.

Formalization scope

Densities are functions ℝ → ℝ with IsPdf f (measurable, nonnegative everywhere, integrable, total integral 1); the law of $D$ is never introduced separately. Log-concavity is the published definition ConvexOptimization.LogConcaveOn Set.univ f (power form, zeros allowed). Concavity of Real.log ∘ f is not used, because Real.log 0 = 0 would treat $\log f$ as $0$ off the support. The quantile is an sInf; for $\beta\in(0,1)$ its defining set is nonempty and bounded below. The AMS is the difference of two ratios of integrals. At the quantile both denominators are positive, and the goal and Proposition 1 assume no integrability of $xf(x)$ , since log-concave densities have exponential tails. The value $f(q^*)$ is taken pointwise; $q^*$ lies in the interior of the support, where a log-concave density is continuous.

Conventions and disclosed departures from the page:

" $\gamma_1\in\partial\log f$ , the set of all subgradients" is read as the superdifferential of the concave $\log f$ on $\{f>0\}$ .
Lemma 3 carries three added hypotheses: $f_2$ vanishes outside some $[l,u]\ni t$ and is positive on $(l,u)$ ; $0<F_1(t)<1$ ; and $xf_1(x)$ , $xf_2(x)$ are integrable. The first repairs the printed statement; the other two are the conditions under which Definition 1 makes sense for general densities.
Proposition 1 and the closed form of $z^*$ are stated for $\gamma_1\neq0$ and $\gamma_1/\gamma_0$ strictly inside the interval of Lemma 1, where (12) is a finite interval.
The goal has no such restriction.

Assumption 1 of the paper (monotonicity of $f$ beyond $q^*$ ) and the continuity assumption of §3 are hypotheses of Theorems 3–4 only and are not used here. A formalization in which $f(q^*)$ or $\Delta(q^*)$ takes a junk value (a non-integrable $xf(x)$ , a zero denominator) would make the goal trivially true or false; the hypotheses above exclude this, and no statement assumes the conclusion of another.

Contributions welcome: proofs of the milestones in any order; general lemmas on log-concave densities on $\mathbb R$ (exponential tails, integrability of moments, monotone hazard rates, continuity in the interior of the support); and the boundary cases of problem (11).

Selected references

R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6):1294–1306, 2015. Authors' accepted manuscript, MIT DSpace. https://doi.org/10.1287/opre.2015.1422
R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4):821–839, 2007. https://doi.org/10.1287/moor.1070.0272

9 thms3 active usersReviewed

Completed

Algorithmic Game Theory Functional Analysis·Captain: mikedeng1

Existence of Correlated Equilibria III: A Game with Compact Hausdorff Strategy Spaces and Continuous Payoffs Has a Countably Additive Correlated EquilibriumResearch Paper

Motivation

A correlated equilibrium (Aumann 1974) describes play in a game where a mediator draws a profile of recommended actions from a joint distribution and tells each player only that player's own recommendation; the distribution is an equilibrium when no player gains, on average, by departing from the recommendation. Correlated equilibria are the natural outcome of regret-minimizing learning dynamics and the solution concept underlying much of algorithmic game theory, so it matters in which games they are guaranteed to exist.

For finite games existence follows from Nash's theorem, since every Nash equilibrium is a correlated one. Hart and Schmeidler (1989) gave a direct proof based on linear duality, with no fixed-point theorem, and then extended it beyond finite games. This mission formalizes the last and most general of their three existence theorems: games with arbitrarily many players whose strategy spaces are compact Hausdorff spaces.

Timeline.

1952: Fan and Glicksberg prove fixed-point theorems that yield Nash equilibria, hence correlated equilibria, for continuous games on compact strategy spaces.
1969: Peleg proves existence of Nash equilibria for games with infinitely many players, finite strategy sets and continuous payoffs.
1974: Aumann introduces correlated equilibria (J. Math. Econ. 1).
1987: Aumann characterizes correlated equilibrium as Bayesian rationality (Econometrica 55).
1989: Hart and Schmeidler prove existence of correlated equilibria by a separation argument: Theorem 1 for finite games, Theorem 2 for infinitely many players with finite strategy sets, Theorem 3 for compact Hausdorff strategy spaces (Math. Oper. Res. 14).

Setting

A game consists of a nonempty set $N$ of players, possibly uncountable; for each player $i\in N$ a nonempty set $S^i$ of pure strategies; and for each player a payoff function $h^i:S\to\mathbb R$ on the set of strategy profiles $S=\prod_{j\in N}S^j$ . For a profile $s$ and a strategy $t^i\in S^i$ , $(s^{-i},t^i)$ denotes the profile obtained from $s$ by replacing player $i$ 's coordinate with $t^i$ ; thus $h^i(s)=h^i(s^{-i},s^i)$ .

In this mission each $S^i$ is a compact Hausdorff space with its Borel σ-algebra $\Sigma^i$ , the profile space $S$ carries the product topology, and $\Sigma$ is the Borel σ-algebra of $S$ . The product σ-algebra $\Sigma_0$ generated by the $\Sigma^i$ is contained in $\Sigma$ , and the inclusion may be strict when $S$ is not metrizable (the paper's footnote 13).

Let $p$ be a probability measure on $(S,\Sigma)$ . Think of $p$ as the mediator's distribution; player $i$ learns the coordinate $s^i$ of the drawn profile. A deviation of player $i$ is a $\Sigma^i$ -measurable map $\zeta^i:S^i\to S^i$ that replaces each recommendation by an action. The measure $p$ is a correlated equilibrium with respect to $\{\Sigma^i\}_{i\in N}$ and $\Sigma$ when, for every player $i$ and every deviation $\zeta^i$ ,

\int_S\bigl[h^i(s^{-i},s^i)-h^i\bigl(s^{-i},\zeta^i(s^i)\bigr)\bigr]\,dp(s)\ \ge\ 0 . \tag{4}

The left side is the expected gain from obeying the recommendation instead of following $\zeta^i$ .

Formalization targets

Goal: Theorem 3

If every $S^i$ is compact Hausdorff and every $h^i$ is continuous on $S$ with the product topology, then

\exists\, p\ \text{probability measure on } (S,\Sigma)\ \text{such that (4) holds for all } i\in N \text{ and all } \Sigma^i\text{-measurable } \zeta^i .

"Countably additive" in the paper's statement is automatic: $p$ is a measure.

Milestones, in the order of the proof

Every f-set game has a correlated equilibrium. An f-set is a product $T=\prod_iT^i$ of finite nonempty sets $T^i\subseteq S^i$ with $T^i$ a singleton for all but finitely many $i$ ; the game $\Gamma_T$ restricts each player to $T^i$ , and its correlated equilibrium $q_T$ is a finitely supported probability on $S$ .
On a compact Hausdorff space, every net of probability measures has a regular probability measure as a cluster point for the topology induced by the continuous functions.
For a regular probability $p$ on $S$ and a Borel set $R^i\subseteq S^i$ , there are a closed $F^i\subseteq R^i$ and an open $G^i\supseteq R^i$ with $p\bigl((G^i\setminus F^i)\times S^{-i}\bigr)<\varepsilon$ : the marginal of a regular measure is regular.
The special case. A regular cluster point $p$ of the $q_T$ satisfies (4) for every deviation that equals a fixed $t^i$ on a Borel set $R^i$ and the identity elsewhere.
For continuous $h^i$ and $\varepsilon>0$ , $S^i$ has a finite Borel partition $A_1,\dots,A_K$ with $|h^i(s^{-i},a)-h^i(s^{-i},b)|<\varepsilon$ for $a,b$ in the same piece and every $s^{-i}$ .
The general case. If (4) holds for all deviations of the special form, it holds for every Borel deviation.

An optional milestone records the remark on p. 23 that, for a finite strategy set $S^i$ , condition (4) for player $i$ is equivalent to the earlier condition (3), one inequality per recommendation $r^i$ and alternative $t^i$ .

Significance

The result. Theorem 3 guarantees correlated equilibria, with a genuine (countably additive) probability measure, in every continuous game on compact strategy spaces, however many players there are. It also justifies taking $\Sigma$ to be the full Borel σ-algebra rather than the smaller product σ-algebra, so that every Borel-measurable deviation rule is allowed. Nash existence under the same hypotheses (Fan 1952, Glicksberg 1952) implies existence of correlated equilibria too, but through a fixed-point theorem; the proof here uses only finite-dimensional duality and compactness.

Formalizing it. The theorem is classical and its proof is published; nothing here is open. To our knowledge no machine-checked proof of Theorem 3, or of any existence result for correlated equilibria in infinite games, exists. Finite-game existence results are on the platform (AGT.nash_existence; the correlated-equilibrium encodings of Aumann 1987 and Foster and Vohra 1997, and AGT.swap_regret_correlated_equilibrium). The formalization would add reusable measure-theoretic tools on compact products: the regular cluster point of a net of probability measures, the regularity of marginals, and uniform partitions for continuous functions on a product.

Difficulty

The obvious argument is the one that proves Theorem 2: approximate the game by finite games $\Gamma_T$ , take correlated equilibria $q_T$ , extract a weak-* cluster point $p$ , and pass the inequalities of $\Gamma_T$ to the limit. Passing to the limit works only for integrands that are continuous in $s$ , because $p$ is a cluster point against continuous functions only. The integrand of (4) is $h^i(s)-h^i(s^{-i},\zeta^i(s^i))$ , and $\zeta^i$ is merely Borel measurable, so this integrand need not be continuous and the limit step fails. Restricting to continuous deviations would avoid the difficulty but would prove a weaker theorem. Two further points need care: on a non-metrizable product the Borel σ-algebra is larger than the product σ-algebra, and the f-sets ordered by inclusion are not a directed set.

Formalization scope

The profile space is a type synonym Profile S of ∀ i, S i carrying the product topology and the instance borel (Profile S), so measures on $S$ live on the Borel σ-algebra $\Sigma$ and not on Mathlib's product σ-algebra MeasurableSpace.pi ( $=\Sigma_0$ ). The pair $(s^{-i},t^i)$ is Function.update s i t. Players form a type ι with Nonempty ι; each S i is nonempty, compact and Hausdorff with BorelSpace (S i); payoffs are h : ι → Profile S → ℝ with each h i continuous. Deviations are all maps ζ : S i → S i with Measurable ζ.

The predicate IsCorrelatedEq h μ requires IsProbabilityMeasure μ and, for each player and measurable deviation, both integrability of the integrand and nonnegativity of its integral. The integrability clause prevents a trivializing reading in which a non-integrable integrand, whose Lean integral is $0$ , satisfies (4) vacuously; restricting deviations to continuous maps, or using the product σ-algebra, would also change the theorem and is ruled out.

The f-set net is indexed by the f-sets containing a fixed profile $\hat s$ , which are directed; the paper's "ordered by inclusion of the sets $T$ " over all f-sets is not directed, and anchoring repairs this without affecting any statement of the paper. A correlated equilibrium $q_T$ of $\Gamma_T$ is encoded by its finite support and weights (IsFSetCE). The special case is stated for a regular cluster point of the $q_T$ given by these constructed objects, not for an arbitrary measure.

A complete development needs Banach–Alaoglu or the compactness of probability measures on a compact space, the Riesz–Markov–Kakutani representation (RealRMK), regularity of measures (Measure.Regular), Urysohn's lemma, and uniform continuity on compact spaces, all available in Mathlib in some form. Proofs of any milestone, including the general-purpose milestones 2, 3 and 5, are welcome.

Selected references

S. Hart and D. Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14(1), 18–25, 1989. https://doi.org/10.1287/moor.14.1.18
R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1, 67–96, 1974. https://doi.org/10.1016/0304-4068(74)90037-8
R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55(1), 1–18, 1987. https://doi.org/10.2307/1911154
B. Peleg, Equilibrium Points for Games with Infinitely Many Players, Journal of the London Mathematical Society s1-44, 292–294, 1969. https://doi.org/10.1112/jlms/s1-44.1.292
I. L. Glicksberg, A Further Generalization of the Kakutani Fixed Point Theorem, with Application to Nash Equilibrium Points, Proceedings of the AMS 3, 170–174, 1952. https://doi.org/10.1090/S0002-9939-1952-0046638-5
K. Fan, Fixed-Point and Minimax Theorems in Locally Convex Topological Linear Spaces, PNAS 38, 121–126, 1952. https://doi.org/10.1073/pnas.38.2.121
N. Dunford and J. T. Schwartz, Linear Operators, Part I, Interscience, 1958.

9 thms3 active usersReviewed

Completed

Markov Chain Operations Research Stochastic Systems·Captain: mikedeng1

Contact Interactions on a Lattice I: A Contact Process with (2d − 1)λₖ < kμ Dies Out from Every Finite Initial SetResearch Paper

Motivation

The contact process is the basic model of an infection spreading on a lattice: each infected site recovers at a constant rate, and each healthy site becomes infected at a rate that depends on how many of its neighbours are infected. It was introduced by T. E. Harris in Contact Interactions on a Lattice (Ann. Probab. 2, 1974), and it became one of the central examples of interacting particle systems, alongside the voter model and the stochastic Ising model (Liggett, Interacting Particle Systems, 1985, Ch. VI). Its main question is whether a finite infection dies out with probability one or survives forever with positive probability, and how that answer depends on the rates.

Harris's paper gives the first answers. It shows that, under natural conditions on the rates, the probability of survival is monotone, subadditive and submodular as a function of the initial set, and it uses these properties to prove a condition for certain extinction: Theorem 7.1. For the linear contact process (recovery rate $1$ , infection rate $\lambda$ per infected neighbour) the condition is $(2d-1)\lambda<1$ . Holley obtained Theorem 7.1 by different methods at about the same time (footnote 4, p. 981); Holley and Liggett (Ann. Probab. 3, 1975) later developed the duality theory of such processes.

Setting

Let $Z_d$ be the $d$ -dimensional integer lattice, $d\ge1$ . Sites $x,y$ are neighbours, $x\sim y$ , if $\sum_i|x^i-y^i|=1$ ; $N_x$ is the set of the $2d$ neighbours of $x$ . A configuration is a finite set $\xi\subset Z_d$ of infected sites; $\Xi_0$ is the set of all of them, $\xi(N_x)=|\xi\cap N_x|$ , and $x\sim\xi$ means $x\notin\xi$ and $x$ has a neighbour in $\xi$ .

The parameters are a recovery rate $\mu\ge0$ and infection rates $\lambda_0=0,\lambda_1,\dots,\lambda_{2d}\ge0$ . The contact process $\{\xi_t\}$ started from a finite set is the continuous-time Markov chain on $\Xi_0$ that leaves $\xi$ at rate

q_\xi=\mu|\xi|+\sum_{x\sim\xi}\lambda_{\xi(N_x)}\qquad(4.4)

and jumps to $\xi\setminus x$ ( $x\in\xi$ ) at rate $\mu$ and to $\xi\cup x$ ( $x\sim\xi$ ) at rate $\lambda_{\xi(N_x)}$ (4.5). The empty set is absorbing. Write $P_t(\xi,\eta)$ for its transition function, $r(\xi,\eta)=q_{\xi\eta}/q_\xi$ for the transition matrix of its imbedded jump chain, and

p_t(\xi)=P_\xi\{\xi_t\neq\varnothing\},\qquad p_\infty(\xi)=\lim_{t\to\infty}p_t(\xi),\qquad m_t(\xi)=\mathscr E_\xi|\xi_t| .

The process is increasing, subadditive or submodular if, for all $\xi,\eta$ and $t\ge0$ , respectively $p_t(\xi)\le p_t(\xi\cup\eta)$ , $p_t(\xi\cup\eta)\le p_t(\xi)+p_t(\eta)$ , or $p_t(\xi\cup\eta)+p_t(\xi\cap\eta)\le p_t(\xi)+p_t(\eta)$ ((5.2)–(5.4)).

Formalization targets

Goal: Theorem 7.1 (p. 981)

If

(2d-1)\lambda_k<k\mu,\qquad k=1,\dots,2d,

then

p_\infty(\xi)=0\qquad\text{for every finite }\xi\subset Z_d .

Milestones, in the order of the paper

Theorem 4.3 (p. 975): from a finite set the process has finitely many jumps on every $[0,t]$ ; equivalently $\sum_\eta P_t(\xi,\eta)=1$ .
(5.1) (p. 976): $p_t(\xi)$ is non-increasing in $t$ , so $p_\infty(\xi)$ is a limit.
Theorem 5.6(a) (p. 977): if $\lambda_k\uparrow$ , the process is increasing.
Theorem 5.6(b) (p. 977): if moreover $\lambda_k/k\downarrow$ , it is subadditive.
Lemma 5.8 (p. 978): if $\lambda_k\le\min_{j\ge k}\lambda'_j$ , then $p_t\le p'_t$ and $m_t\le m'_t$ .
Theorem 6.2 (p. 979): if $\{\lambda_i\}$ is concave and non-decreasing with $\lambda_0=0$ , the process is submodular.
Change of time scale (p. 981): multiplying all rates by $c>0$ replaces $P_t$ by $P_{ct}$ and leaves $p_\infty$ unchanged.
First-step display (p. 981): for a subadditive process, a singleton $\{x\}$ , and $n\ge1$ , $p_\infty(\{x\})=\sum_\eta r^{(n)}(\{x\},\eta)p_\infty(\eta)\le p_\infty(\{x\})\,\mathscr E_x|\xi_{(n)}|$ .
(7.2) (p. 981): for $\mu=1$ , $\lambda_k=k\lambda$ : $\pi_1=\frac{2d\lambda}{1+2d\lambda}\pi_2$ , where $\pi_1,\pi_2$ are $p_\infty$ of a site and of a pair of neighbours.
(7.3)–(7.4) (p. 981): $\pi_2-\pi_1=(1+(2d-1)\lambda)\sum'r(\xi,\xi\cup x)(p_\infty(\xi\cup x)-\pi_2)\le(\pi_2-\pi_1)(2d-1)\lambda$ .
Conclusion of the proof (p. 981): for $\mu=1$ , $\lambda_k=k\lambda$ , $\pi_1>0$ implies $(2d-1)\lambda\ge1$ .

Significance

Theorem 7.1 gives a computable sufficient condition for extinction that holds in every dimension and for every non-linear infection law satisfying it. For the linear process it gives the lower bound $\lambda_c\ge1/(2d-1)$ on the critical infection rate; the paper's §9 shows conversely that the process survives for large $\lambda_k/\mu$ , so the critical rate is non-trivial. The monotonicity, subadditivity and submodularity theorems of §§5–6 are the comparison tools on which much of the later theory of attractive spin systems was built, and Lemma 5.8 is the prototype of comparison between processes with ordered rates.

The results are proved in the paper, and the proof of Theorem 7.1 is half a page once §§5–6 are available. No machine-checked version of the contact process, of its comparison theorems, or of Theorem 7.1 is known to exist. A formalization produces a continuous-time Markov chain with unbounded rates and an absorbing state on a countable state space, its minimal transition function, a non-explosion criterion, first-step analysis for absorption probabilities, and coupling arguments for monotone comparison. The companion mission Contact Interactions on a Lattice II treats Theorem 7.6, the integrability of the expected size, on the same model.

Difficulty

The obvious argument is first-step analysis on singletons and pairs, (7.2) and (7.3). It fails as it stands because (7.3) involves $p_\infty$ of every three-point set $\xi\cup x$ , and no finite system of first-step equations closes; some inequality between survival probabilities of nested sets is needed, and the milestones record the one the paper uses. Submodularity, subadditivity and monotonicity are not consequences of the rates by direct computation: the paper proves each by building several contact processes on one probability space (Tables 1–4), which in a formal development means constructing couplings of chains with unbounded rates and checking that each marginal has the right law. The reduction from general $\lambda_k$ to the linear case also needs the comparison Lemma 5.8, another coupling. Finally the rates grow linearly in $|\xi|$ , so uniformization does not apply and non-explosion (Theorem 4.3) must be proved before transition probabilities are known to sum to one.

Formalization scope

The process is the countable-state chain of §4, not the Feller process on all subsets of $Z_d$ of §2: sites are Fin d → ℤ, configurations are Finsets, and $P_t$ is the minimal transition function of the rates (4.4)–(4.5), defined as the increasing limit of Feller's backward recursion. There is no measure-theoretic process object; $P_\xi$ and $\mathscr E_\xi$ enter only through $P_t$ . Consequently Theorem 4.1 ( $\Xi_0$ is stochastically closed) is built in, and every statement is made for finite initial sets, including those the page makes for arbitrary $\xi\in\Xi$ ((5.2)–(5.4), Lemma 5.8); for infinite $\xi$ the page itself notes $p_t(\xi)=1$ .

The committed conventions:

$P_t$ , $p_t$ , $p_\infty$ and $m_t$ take values in $[0,\infty]$ ; $p_t(\xi)=1-P_t(\xi,\varnothing)$ and $p_\infty(\xi)=\inf_{t\ge0}p_t(\xi)$ , so $p_\infty=0$ means absorption at $\varnothing$ and cannot be produced by loss of mass to explosion.
The rates are real; every theorem assumes $d\ge1$ , $\mu\ge0$ , $\lambda_0=0$ and $\lambda_k\ge0$ for $k\le2d$ . Conditions on $\{\lambda_k\}$ range over $k=1,\dots,2d$ (or $0,\dots,2d$ ), never over all natural numbers.
$2d-1$ is the real number $2d-1$ .
In the linear case the scalar rate is written $l$ ( $\lambda$ is reserved in Lean), $\mu=1$ and $\lambda_k=kl$ .

Trivializing formalizations are ruled out: the survival probability is not taken from an arbitrary semigroup or a uniformization (the rates are unbounded); $p_\infty$ is not a real infimum or limUnder, whose junk value $0$ would make the goal free; $\lambda$ is indexed by the number of infected, not vacant, neighbours, and $\lambda_0=0$ forbids spontaneous infection; and (7.2) is stated for every site and every neighbour, not for one fixed pair.

A complete development needs: non-explosion for chains with linearly growing rates; the Chapman–Kolmogorov and strong Markov properties of the minimal chain at jump times; lattice symmetries (translations and coordinate reflections) acting on the chain; and couplings of several contact processes realised as one chain on a product type space. The chain infrastructure and the coupling lemmas are reusable beyond this mission, in particular by its companion. Contributions to any milestone are welcome, including proofs of the milestones under the paper's hypotheses by methods other than Harris's.

Selected references

T. E. Harris, Contact interactions on a lattice, The Annals of Probability 2(6), 969–988, 1974. https://doi.org/10.1214/aop/1176996493
R. Holley and T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, The Annals of Probability 3(4), 643–663, 1975. https://doi.org/10.1214/aop/1176996306
T. M. Liggett, Interacting Particle Systems, Grundlehren 276, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
W. Feller, On the integro-differential equations of purely discontinuous Markoff processes, Transactions of the AMS 48, 488–515, 1940. https://doi.org/10.1090/S0002-9947-1940-0002697-3
J. R. Norris, Markov Chains, Cambridge University Press, 1997, §2.8. https://doi.org/10.1017/CBO9780511810633

13 thms3 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Heavy-Traffic Limits for Queues with Many Exponential Servers: The Scaled Stationary M/M/n Queue Length Converges to a Hybrid Exponential–Normal LawResearch Paper

Why many-server queues in heavy traffic

Telephone exchanges, call centers, hospital wards and cloud server pools are queues with a large number $s$ of parallel servers. For such systems two classical approximations pull in opposite directions. Holding $s$ fixed and letting the traffic intensity $\rho \to 1$ gives the conventional heavy-traffic limit, in which almost every customer waits. Letting $s$ grow with $\rho$ fixed below one gives a limit in which almost nobody waits. Real systems sit in between: a positive fraction of customers wait, and waits are short. Halfin and Whitt (Operations Research 29 (1981) 567–588) identified the scaling that produces this middle regime and the limit laws it yields. The scaling is now called the Halfin–Whitt or quality-and-efficiency-driven (QED) regime, and it underlies square-root staffing: run $n \approx R + \beta\sqrt R$ servers for an offered load of $R$ Erlangs. Borst, Mandelbaum and Reiman (Operations Research 52 (2004) 17–34) built staffing rules for large call centers on it.

Timeline. Erlang (1917) gave the delay probability of the M/M/s queue. Iglehart (1965) proved diffusion limits for M/M/s queues with the number of servers growing and the traffic intensity fixed. Halfin and Whitt (1981) proved that the delay probability has a limit strictly between 0 and 1 exactly when $(1-\rho_n)\sqrt n$ converges to a positive constant (their Proposition 1), derived the limit of the stationary queue length (Theorem 1), and extended the process-level limit to GI/M/s queues. Later work extended the regime to many-server queues with general service times and abandonment.

Setting

An M/M/s queue has Poisson arrivals at rate $\lambda > 0$ , $s \ge 1$ servers, and exponential service times with rate $\mu > 0$ . Its traffic intensity is $\rho = \lambda/(s\mu)$ . The number $Q(t)$ of customers in the system (waiting or in service) is a birth–death process on $\{0,1,2,\dots\}$ with birth rate $\lambda$ and death rate $\min(k,s)\mu$ in state $k$ . When $\rho < 1$ , $Q(t)$ converges in distribution to $Q(\infty)$ , whose law $p_k = P(Q(\infty) = k)$ is the unique probability distribution solving the balance equations of this chain. The probability of delay $\alpha = P(Q(\infty) \ge s)$ is the Erlang-C formula.

The mission studies a sequence of such queues: queue $n \ge 1$ has $s_n = n$ servers, the fixed service rate $\mu$ , and arrival rate $\lambda_n$ with $\rho_n = \lambda_n/(n\mu) < 1$ and $\lambda_n \to \infty$ . Its stationary queue length is $Q_n(\infty)$ , and the scaled queue length is

X_n = \frac{Q_n(\infty) - n}{\sqrt n}.

Throughout, $\Phi$ and $\varphi$ denote the standard normal distribution function and density, and for $\beta > 0$

\alpha(\beta) = \big[1 + \sqrt{2\pi}\,\beta\,\Phi(\beta)\,e^{\beta^2/2}\big]^{-1} = \frac{\varphi(\beta)}{\varphi(\beta) + \beta\Phi(\beta)} \in (0,1).

The standing assumption of the paper's Section 2 is the heavy-traffic condition

\lim_{n\to\infty} (1-\rho_n)\sqrt n = \beta, \qquad \beta > 0. \tag{2.2}

Formalization targets

Goal: Theorem 1

Under (2.2), with $\alpha = \alpha(\beta)$ ,

X_n \Rightarrow X, \qquad P(X \ge 0) = \alpha,\quad P(X > x \mid X \ge 0) = e^{-x\beta}\ (x \ge 0),\quad P(X \le x \mid X \le 0) = \frac{\Phi(\beta + x)}{\Phi(\beta)}\ (x \le 0).

The limit is exponential with rate $\beta$ above zero and a normal law truncated at zero below it, with masses $\alpha$ and $1-\alpha$ .

Milestones, in the order the paper proves them

The stationary law (1.1)–(1.3) of one M/M/s queue, and the identification (1.2) of $P(Q(\infty) \ge s)$ with the Erlang-C formula.
Lemma 1: recursions expressing the partial moments $\sum_{k<s} k^m p_k$ and $\sum_{k \ge s} k^m p_k$ through lower ones and $\alpha$ .
Proposition 1: $P(Q_n(\infty) \ge n) \to \alpha \in (0,1)$ if and only if (2.2) holds, and then $\alpha = \alpha(\beta)$ .
Proposition 2: for $\delta > 0$ and $(n - \delta_n)/\sqrt n \to \delta$ with $\delta_n \le n$ ,

P(Q_n(\infty) \le \delta_n \mid Q_n(\infty) \le n) \to \frac{\Phi(\beta-\delta)}{\Phi(\beta)},\qquad \sqrt n\,P(Q_n(\infty) = [\delta_n] \mid Q_n(\infty) \le n) \to \frac{\varphi(\beta-\delta)}{\Phi(\beta)},

and for $(\delta_n - n)/\sqrt n \to \delta$ with $\delta_n \ge n$ ,

P(Q_n(\infty) \ge \delta_n \mid Q_n(\infty) \ge n) \to e^{-\delta\beta},\qquad \sqrt n\,P(Q_n(\infty) = [\delta_n] \mid Q_n(\infty) \ge n) \to \beta e^{-\delta\beta}.

Corollary 1: the first four moments and the variance of $X_n$ converge to explicit functions of $\alpha$ and $\beta$ , for example $E X_n \to -\beta + \alpha/\beta$ .

Significance

Theorem 1 is the stationary half of the Halfin–Whitt regime. It turns the Erlang-C formula, a ratio of sums with $n$ terms that is opaque for large $n$ , into a two-parameter description of congestion: $\alpha$ is the fraction of customers who wait, $\beta$ is the scaled safety margin of servers, and the conditional laws above give the distribution of the number waiting and of the number of idle servers. Proposition 1 and Theorem 1 are what square-root staffing rules evaluate; Corollary 1 supplies the mean and variance used in the paper's numerical approximations.

All results of this mission are proved in the paper, by direct calculation from (1.1)–(1.3), Stirling's formula and the central limit theorem for Poisson variables. None has a machine-checked proof. Proposition 1 and the two Section 1 facts are posed on the platform as open theorems from the Gross et al. queueing textbook series; this mission adds the conditional and local limits, the weak-convergence theorem and the moment results on the same definitions, so that a closed development would give a fully checked derivation of the Halfin–Whitt limit from the balance equations.

Difficulty

The stationary law is explicit, so nothing here needs a stochastic process. The difficulty is analytic and uniform: each statement is a limit of ratios of sums of $n$ or infinitely many terms, $(n\rho_n)^k/k!$ below $n$ and a geometric tail above $n$ , in which $\rho_n \to 1$ and $n \to \infty$ at linked rates. The lower half needs a central limit theorem for Poisson laws whose parameter $n\rho_n$ moves with $n$ and is evaluated at a moving point; the local limits (2.10) and (2.12) need Stirling's formula with explicit control of $\log \rho_n$ to second order. Weak convergence then needs tightness, or a direct argument from the conditional limits, and the moment limits need uniform integrability, which the fixed- $s$ moment recursions do not give by themselves. Holding $\rho$ fixed, or taking limits in $n$ and $\rho$ one after the other, gives degenerate answers ( $\alpha = 0$ or $\alpha = 1$ ); the two limits must be taken together.

Formalization scope

The Lean development lives in the namespace HalfinWhitt81.Stationary. The law of $Q_n(\infty)$ is a sequence p n : ℕ → ℝ satisfying IsSteadyState (fun _ => lam n) (mmcDeath μ n) (p n) of the referenced definition QueueingFundamentals.BirthDeath.Balance (nonnegative, summing to one, solving the balance equations of the M/M/n chain); the Erlang-C formula and $\alpha(\beta)$ are erlangC and halfinWhittAlpha of QueueingFundamentals.BirthDeath.Erlang, and $\Phi$ , $\varphi$ are Mathlib's cdf (gaussianReal 0 1) and gaussianPDFReal 0 1. These, and the three open theorems for (1.1)–(1.3), (1.2) and Proposition 1, come from the Gross et al. (2008) series and are referenced, not restated. The related Borst–Mandelbaum–Reiman items (DimCallCenters.*.lemma_4_1, for the continuous extension of Erlang-C) state a different result and are not used.

Conventions committed to:

hypotheses on queue $n$ (rates, steady state, $\delta_n \le n$ or $\delta_n \ge n$ ) are imposed for $n \ge 1$ , and only limits are asserted; $\lambda_n \to \infty$ is kept as a hypothesis although it follows from (2.2);
the standing assumption "(2.1) or, equivalently, (2.2)" is the hypothesis (2.2) with $\beta > 0$ , and $\alpha$ is written as $\alpha(\beta)$ , equal to the limit in (2.1) by Proposition 1;
probabilities of $Q_n(\infty)$ are sums of p n (probLE, probGE, probEqInt); a conditional probability $P(A \mid B)$ with $A \subseteq B$ is the ratio $P(A)/P(B)$ ; $[x]$ is Int.floor, with $P(Q = m) = 0$ for $m < 0$ ;
$X_n$ uses $n^{-1/2}$ : the page's (2.13) prints $n^{1/2}$ , a misprint; (2.12) prints the limit $\beta e^{-\beta}$ , a misprint for $\beta e^{-\delta\beta}$ , which is what is formalized;
" $X_n \Rightarrow X$ " is stated as: there is a Borel probability measure $\nu$ on $\mathbb R$ with the three properties of Theorem 1 such that $\sum_k p_n(k)\,g((k-n)/\sqrt n) \to \int g\,d\nu$ for every bounded continuous $g$ ; the exponential clause is for $x \ge 0$ and the normal clause for $x \le 0$ ;
infinite sums whose convergence is not implied by the hypotheses (the moment series of Lemma 1 and Corollary 1) have their convergence in the conclusion.

The goal cannot be met trivially: the law of $Q_n(\infty)$ is the M/M/n steady state, not a free sequence; the limit measure is asserted to exist together with its three properties and the convergence, so no vacuous "for every $\nu$ " reading is possible; and the statement $P(X_n \ge 0) \to \alpha$ alone is Proposition 1, already posed.

A complete development needs: the closed form of the M/M/n steady state, Poisson central limit and local limit theorems with a moving parameter, Stirling's formula with error terms, a criterion for weak convergence from convergence of distribution functions, and uniform integrability for the moments. The Poisson limit theorems and the weak-convergence criterion are reusable beyond this mission. Proofs of the referenced open theorems, of individual milestones, and alternative routes to Theorem 1 (moment convergence, or the process-level limit) are all welcome.

Selected references

S. Halfin and W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3) (1981) 567–588. https://doi.org/10.1287/opre.29.3.567
R. B. Cooper, Introduction to Queueing Theory, Macmillan, 1972 (the source cited for (1.1)–(1.3)).
D. L. Iglehart, Limiting Diffusion Approximations for the Many Server Queue and the Repairman Problem, Journal of Applied Probability 2(2) (1965) 429–441.
S. Borst, A. Mandelbaum and M. I. Reiman, Dimensioning Large Call Centers, Operations Research 52(1) (2004) 17–34. https://doi.org/10.1287/opre.1030.0081
D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008 (§2.4: the Erlang-C formula and the Halfin–Whitt limit).

13 thms3 active usersReviewed

Completed

Dynamical Systems Operations Research Stochastic Systems·Captain: mikedeng1

Subadditive Ergodic Theory 1: Kingman's Theorem — x₀ₜ/t Converges with Probability One and in Mean to a Finite ξ with E(ξ) = γResearch Paper

Motivation

Many stochastic systems have an accumulated cost or passage time that grows with the length of an observation window. Splitting a window at an intermediate time gives an upper bound on the total, even when it does not give an equality. First-passage percolation and products of random matrices are examples discussed by Kingman (1973). A central question is whether the cost per unit time settles to a long-run rate on almost every sample path.

Hammersley and Welsh introduced subadditive stochastic processes in 1965. Kingman's 1968 theorem established the almost-sure limit for the stationary process considered here. His 1973 paper restated the result, identified the limit's expectation, and set out the process model and related formulations used in later applications. The 1973 article explicitly attributes the proof of Theorem 1, its maximal inequality, and its decomposition to the 1968 work; this mission formalizes the statements as presented in the 1973 paper.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ . For integers $0\le s<t$ , let $x_{st}:\Omega\to\mathbb R$ be a measurable random variable. Think of $x_{st}$ as the accumulated quantity over the interval from $s$ to $t$ . Condition S₁ is subadditivity: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$ . The stronger equality defines an additive process.

Condition S₂ says that shifting every interval one time unit forward leaves the joint distribution of the whole family unchanged. It concerns the law of $(x_{s+1,t+1})_{s<t}$ as a single countable path. The one-dimensional statement that each $x_{st}$ has a distribution depending only on $t-s$ is called S₂′ in the paper; it does not replace S₂. Condition S₃ says that every positive-time variable $x_{0t}$ is integrable and that, for some real $A$ , its mean $g_t=E_P(x_{0t})$ satisfies $g_t\ge-At$ for all $t\ge1$ . A subadditive process satisfies S₁, S₂, and S₃.

The associated mean growth rate is $\gamma(x)=\inf_{t\ge1}g_t/t$ . The time index starts at one in this infimum because division by zero would introduce an unrelated value. S₃ gives a finite lower bound; the subadditive mean relation makes this infimum the limit of $g_t/t$ . Kingman also considers the invariant σ-field $\mathcal I$ : events determined by the entire path and unchanged by the shift $(x_{st})\mapsto(x_{s+1,t+1})$ . It records the part of the process that can remain random in the limiting rate. Source: §§1.1–1.2, pp. 883–885.

Formalization targets

Theorem 1: finite long-run rate

For every subadditive process there is an integrable real random variable $\xi$ such that

\frac{x_{0t}(\omega)}{t}\longrightarrow\xi(\omega) \quad\text{for }P\text{-almost every }\omega, \qquad \int_\Omega\left|\frac{x_{0t}}{t}-\xi\right|\,dP\longrightarrow0, \qquad E_P(\xi)=\gamma(x).

These are three distinct claims: almost-sure convergence, convergence in mean, and an identity for the limit's expectation. The limit need not be a constant. The milestone list also covers the convergence of the means, the maximal inequality (1.2.5), the decomposition (1.2.6), the measure-preserving formulation (1.3.4)–(1.3.5), and the representation through $\mathcal I$ in (1.2.4). Each statement comes from the 1973 paper, §§1.1–1.3.

Measure-preserving formulation

For a measure-preserving map $\theta:\Omega\to\Omega$ , condition Sᴱ concerns integrable functions $f_n$ with $f_{m+n}(\omega)\le f_m(\omega)+f_n(\theta^m\omega)$ for $m,n\ge1$ and a linear lower bound on their expectations. It yields an integrable $\xi$ with $f_n/n\to\xi$ almost surely and in mean. Neither invertibility nor ergodicity of $\theta$ is assumed. Source: §1.3, p. 886.

Significance

The theorem assigns a finite sample-path growth rate to an entire class of stationary subadditive systems. It also ties the average of that rate to the infimum of the normalized expected values. The equality is useful when a system's finite-window means are easier to estimate than its individual long-run paths. The invariant σ-field statement explains why a stationary system can have different rates on different paths without contradicting the mean identity. Kingman's examples show how the same framework reaches percolation and matrix products.

The result is mathematically proved, as the 1973 article states. The remaining work here is a machine-checked development of its process model and the displayed results. A published Prove2Me item, PalmQueueing.Ergodic.kingman_subadditive, is open and concerns an ergodic bijective flow with a constant possibly infinite limit; it does not supply this nonergodic finite-limit theorem or convergence in mean. The draft statements in this mission compile with proof placeholders. No machine-checked proof of these new statements is claimed.

Difficulty

Subadditivity gives bounds when intervals are joined, but it does not express $x_{0t}$ as a sum of identically distributed increments. The ordinary additive ergodic theorem therefore does not immediately give convergence for $x_{0t}/t$ . Nor does convergence of the expectations $g_t/t$ alone force convergence on individual paths or in mean. The process may also have a nonconstant limit: stationarity is a joint-law condition, not an ergodicity assumption that erases invariant information. These are the gaps the formalization must close without strengthening the hypotheses. Source: §§1.1–1.3.

Formalization scope

Lean represents $x$ as a function of two natural-number indices and a sample point, but every condition and conclusion uses only $s<t$ . S₁ and the Sᴱ cocycle inequality follow the paper's pointwise displays; random-variable equality in the decomposition is stated almost surely at each valid index pair. Measurability of each valid coordinate is explicit. S₂ compares two probability measures on the full countable path space, so equality of individual marginals cannot satisfy it. The probability measure is normalized, and S₃ requires Bochner integrability to keep every mean finite. The constant $\gamma$ is a real infimum over positive times, used only under S₃. The goal's limit is real and integrable; Kingman's separate Theorem 2 treats a possible value of $-\infty$ and belongs to another mission.

The invariant σ-field is the pullback of the path-space shift-invariant σ-field. Its measurability claim is made through an almost-everywhere equal version, since almost-sure limits are insensitive to changes on null sets. Conditional expectation uses this explicit sub-σ-field. All limits in this mission take positive integer time to infinity. The Sᴱ definition requires measure preservation but no inverse and no ergodicity. Thus neither a marginal-law substitution for S₂ nor an ergodic constant-limit specialization can trivialize the target.

A complete proof can reuse Mathlib's measure theory, conditional expectation, product measurable spaces, measure-preserving maps, and subadditive-sequence results. The two process definitions, the invariant σ-field interface, and auxiliary statements are useful to later formalizations of stationary growth models. Contributions that prove the stated results or develop general-purpose lemmas for these objects fit the mission.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, The Annals of Probability 1(6), 883–899, 1973. DOI: 10.1214/aop/1176996798.

8 thms3 active usersReviewed

Completed

Statistics·Captain: mikedeng1

On Tail Probabilities for Martingales 3: If E exp[−e(λ)W] ≤ e^{−λa} and E exp[−f(λ)W] ≥ e^{−λ(a+1)} for All λ ≥ 0, Then P{W < b} > ½ exp[−(½ + 2δ)a²/b]Research Paper

Motivation

Freedman's inequality bounds the probability that a martingale with increments bounded above by $1$ reaches a level $a$ before its accumulated conditional variance exceeds $b$ : the bound is $\exp[-a^2/2(a+b)]$ (D. A. Freedman, On Tail Probabilities for Martingales, Ann. Probab. 3 (1975) 100–118, Theorem (4.1), doi:10.1214/aop/1176996452). It is the standard tool for concentration of martingales whose variance is random, and it is used throughout online learning, bandit theory and the analysis of randomized algorithms.

The same paper shows that the exponent $a^2/2b$ cannot be improved in general. For a martingale with increments bounded by $1$ in absolute value, Freedman's estimate (1.10) bounds from below the probability that level $a$ is crossed while the conditional variance used is still below $b$ . The analytic core of that lower bound is isolated in the paper as Proposition (4.10), p. 109: a statement about a single nonnegative random variable whose Laplace transform is controlled from both sides. The paper calls its proof "disappointingly hard". This mission formalizes Proposition (4.10) and the steps of its proof.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. For real $\lambda$ put (Definition (1.2), p. 101)

e(\lambda)=e^{\lambda}-1-\lambda,\qquad f(\lambda)=e^{-\lambda}-1+\lambda .

Both are nonnegative and equal $\lambda^2/2+O(\lambda^3)$ near $0$ . Fix $a>0$ and a nonnegative random variable $W$ . The two Laplace-transform bounds are, for every $\lambda\ge0$ ,

\text{(4.11a)}\quad E\{\exp[-e(\lambda)W]\}\le\exp(-\lambda a),\qquad \text{(4.11b)}\quad E\{\exp[-f(\lambda)W]\}\ge\exp(-\lambda(a+1)).

In the paper $W=W_a$ is the conditional variance $\sum_{i\le\tau_a}\operatorname{Var}\{X_i\mid\mathcal F_{i-1}\}$ accumulated up to the first time $\tau_a$ the martingale reaches $a$ ; for that variable (4.11a) and (4.11b) are Theorems (1.12) and (1.8). Here $W$ is abstract. The hypotheses are consistent: the first-passage time of standard Brownian motion to level $a$ has $E e^{-sW}=e^{-a\sqrt{2s}}$ , and since $f(\lambda)\le\lambda^2/2\le e(\lambda)$ for $\lambda\ge0$ , it satisfies both bounds.

The parameter conditions (4.12) on positive reals $\delta,a,b$ are

\delta<\tfrac13,\qquad \frac ba>\frac{9}{\delta^2},\qquad \frac{a^2}{b}>\frac{16}{\delta^2}\log\frac{64}{\delta^2}.

The proof uses the notation (4.14): $\varphi(\lambda)=\lambda^2/2-\lambda^3/6$ , $\lambda=(1+\delta)a/b$ , $k=a^2/b$ , $N=2/\delta^2$ , the five intervals $I_1=[0,Na]$ , $I_2=(Na,(1-2\delta)b]$ , $I_3=(b,2b]$ , $I_4=(2b,\infty)$ , $I_5=((1-2\delta)b,b]$ , and the terms

\eta_i=\varphi(\lambda)\int_{I_i}P\{W<x\}\,e^{-\varphi(\lambda)x}\,dx .

In Lean these objects are FreedmanTail.LowerTail.e, f, LaplaceUpper, LaplaceLower, ParamConditions, phi, lamStar, kStar, NStar, I1–I5 and eta.

Formalization targets

Goal: Proposition (4.10)

Under (4.11a)–(4.11b) for all $\lambda\ge0$ and (4.12a)–(4.12c),

P\{W<b\}>\tfrac12\exp\!\left[-\left(\tfrac12+2\delta\right)\frac{a^2}{b}\right].\qquad(4.13)

Milestones

In the order of the proof:

Lemma (4.9): $\alpha>0$ , $x>2\log\alpha$ imply $e^x>\alpha x$ .
(4.17): $\exp(-\delta^2k/8)<1/(8k)$ under (4.12).
(4.18): under (4.11a), $P\{W<x\}<\exp[-a^2/(2(a+x))]$ for $x\ge0$ .
(4.15): under (4.11b) and (4.12), $\varphi(\lambda)\int_0^\infty P\{W<x\}e^{-\varphi(\lambda)x}\,dx>\exp[-\lambda(a+1)]$ .
(4.19), with its exponent corrected: $P\{W<x\}<(\tfrac18-\tfrac1{50})\exp[-(1+\delta)k]$ for $0\le x\le Na$ .
(4.16:1)–(4.16:4): $\eta_1<(\tfrac18-\tfrac1{50})e^{-(1+\delta)k}$ and $\eta_i<\tfrac18e^{-(1+\delta)k}$ for $i=2,3,4$ .
(4.16:5): $\eta_5<P\{W<b\}\cdot\exp[(-\tfrac12+2\delta^2)k]$ .

Significance

The result. Proposition (4.10) converts two-sided control of a Laplace transform into a lower bound for a left tail, with an explicit constant and an explicit range of validity. Applied to the crossing variance $W_a$ it gives Freedman's lower bound (1.10) for $P\{W_a<b\}$ , which matches the exponent $a^2/(2b)$ of the upper bound of Theorem (4.1) up to the term $2\delta a^2/b$ . That is the statement that Freedman's inequality is sharp in the regime $a^2/b\to\infty$ , $b/a\to\infty$ .

Formalizing it. The proposition is proved in the 1975 paper; no machine-checked proof is known. Mathlib contains Chernoff-type upper bounds and the layer-cake formula, but no lower tail bound derived from two-sided Laplace-transform control. The mission produces a self-contained, constant-explicit Tauberian-type lemma for nonnegative random variables, usable without any martingale structure. The companion missions of this series formalize Theorem (4.1) and the Laplace bound (1.8); together they would give the sharpness statement for martingales.

Difficulty

The obvious route is to invert the Laplace-transform bounds directly. A lower bound on $E\{e^{-sW}\}$ does not by itself bound $P\{W<b\}$ from below: the mass that makes the Laplace transform large could sit at small values of $W$ or be spread over a wide range. Without (4.11a) the conclusion fails, and with it every contribution from values of $W$ away from $b$ must be shown negligible at a precision of order $e^{-(1+\delta)k}$ , where $k=a^2/b$ is large. The main term is smaller than the total by the factor $e^{-k/2}$ , so every error term must be estimated with constants explicit enough to stay below it. The thresholds (4.12b)–(4.12c) are what make all of these comparisons hold at once.

Formalization scope

The probability space is a measurable space Ω with a measure P and [IsProbabilityMeasure P]. $W$ is a measurable function Ω → ℝ with W ω ≥ 0 for every ω. The expectations in (4.11) are Bochner integrals of $\exp[-e(\lambda)W]$ and $\exp[-f(\lambda)W]$ ; for $\lambda\ge0$ these integrands lie in $(0,1]$ , so they are integrable and the integrals are genuine expectations. Probabilities are P.real {ω | W ω < x}, with the strict event as on the page. The integrals in $x$ are Lebesgue integrals over $[0,\infty)$ and over the intervals $I_i$ ; the integrand is a nondecreasing function of $x$ times $e^{-\varphi(\lambda)x}$ , hence measurable and, as $\varphi(\lambda)>0$ , integrable.

Conventions and corrections, each also disclosed in the items:

The page says "for each $a>0$ , let $W_a$ be a nonnegative random variable"; only the one variable at the one level $a$ of (4.12) enters, so the statement is made for a fixed $a$ and a single $W$ .
(4.14) prints $\varphi(\lambda)=\lambda^2/2>\lambda^3/6$ ; this is read as $\varphi(\lambda)=\lambda^2/2-\lambda^3/6$ , as the rest of the proof requires.
(4.19) prints $\theta=(\tfrac18-\tfrac1{50})\exp[-(1+\delta)]$ ; the milestone states $\theta=(\tfrac18-\tfrac1{50})\exp[-(1+\delta)k]$ , which is what the page's argument proves and what (4.16:1) needs.
(4.18) is stated for every $x\ge0$ , the range on which it is used.
The proof of (4.16:5) ends "This settles (3.16:5)", a misprint for (4.16:5).

A trivializing formalization is ruled out: the hypotheses are satisfied by the Brownian first-passage time above, the parameter conditions hold for instance at $\delta=0.3$ , $a=10^6$ , $b=2\cdot10^8$ , and no integral in a hypothesis or conclusion can take a default value $0$ .

Needed infrastructure: Markov's inequality and the layer-cake formula (both in Mathlib), the identity $E\{e^{-sW}\}=s\int_0^\infty P\{W<x\}e^{-sx}\,dx$ for $W\ge0$ , and elementary estimates of $e^x$ and of the convex function $\theta(x)=\tfrac{\lambda^2}2x+\tfrac{N}{N+1}\tfrac{a^2}{2x}$ of (4.21). The layer-cake identity and the left-tail bound (4.18) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the unnumbered steps (4.20)–(4.30).

The source is the published article in The Annals of Probability (a scanned copy); page numbers are the journal's.

Selected references

D. A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1) (1975) 100–118. doi:10.1214/aop/1176996452

14 thms3 active usersReviewed

Completed

Statistics·Captain: mikedeng1

On Tail Probabilities for Martingales 1: If X_n ≤ 1 and E{X_n | ℱ_{n−1}} ≤ 0, Then P{S_n ≥ a and T_n ≤ b for Some n} ≤ (b/(a+b))^{a+b} e^a ≤ exp[−a²/2(a+b)]Research Paper

Motivation

For sums of independent bounded random variables, the inequalities of Bernstein and Bennett bound the probability of a large deviation by an exponential in the deviation and the variance (Bennett 1962; Hoeffding 1963). Many processes met in probability, statistics and learning theory are not sums of independent terms but martingales or supermartingales: sequential estimators, stochastic approximation iterates, the regret of an online algorithm. For them the relevant scale is not a fixed variance but the conditional variance accumulated along the path, which is itself random.

David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) extended the Bernstein–Bennett inequality to this dependent case, with the conditional variance in place of the variance and with a bound that holds simultaneously for all times. The result, now called Freedman's inequality, is the standard tool for martingale concentration with variance-sensitive rates and is used throughout bandit and reinforcement-learning analyses, random-graph arguments and stochastic optimization. This mission formalizes that theorem, (4.1) of the paper, together with the chain of lemmas the paper uses to prove it.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal F_0\subset\mathcal F_1\subset\mathcal F_2\subset\cdots$ an increasing sequence of sub- $\sigma$ -fields of $\mathcal F$ (a filtration). Let $X_1,X_2,\dots$ be real random variables with $X_n$ measurable with respect to $\mathcal F_n$ . Define

the partial sums $S_n=X_1+\cdots+X_n$ , with $S_0=0$ ;
the conditional variances $V_n=\operatorname{Var}\{X_n\mid\mathcal F_{n-1}\}$ ;
the intrinsic time $T_n=V_1+\cdots+V_n$ , with $T_0=0$ .

Freedman treats $T_n$ as an intrinsic clock: read at time $T_n$ rather than $n$ , the process $S_n$ resembles Brownian motion. The paper's condition (3.4) is

X_n\le1\ \text{a.e.}\qquad\text{and}\qquad E\{X_n\mid\mathcal F_{n-1}\}\le0\ \text{a.e.}\qquad\text{for all }n\ge1,

so $(S_n)$ is a supermartingale whose increments are bounded above by $1$ ; no lower bound is assumed. The auxiliary functions are $e(\lambda)=e^\lambda-1-\lambda$ and $Q_\lambda(v,y)=\exp\{\lambda y-e(\lambda)v\}$ , with time first and position second. A stopping time $\sigma$ takes values in $\{0,1,2,\dots,\infty\}$ with $\{\sigma\le n\}\in\mathcal F_n$ , and $P\{\sigma=\infty\}>0$ is allowed.

In Lean these are FreedmanTail.Bernstein.S, V, T (on Filtration ℕ m, with V given by Mathlib's condVar) and FreedmanTail.Bernstein.e, Q.

Formalization targets

Goal: (4.1) Theorem

Under (3.4), for all $a>0$ and $b>0$ ,

P\{S_n\ge a\ \text{and}\ T_n\le b\ \text{for some } n=1,2,\dots\}\le\Bigl(\frac{b}{a+b}\Bigr)^{a+b}e^{a}\le\exp\Bigl[-\frac{a^{2}}{2(a+b)}\Bigr].

The first bound is of Bennett type, the second of Bernstein type. The event is a union over all times; the bound does not depend on any horizon.

Milestones

In the order the paper's proof uses them:

(3.1) Lemma: $g(0)=\tfrac12$ , $g(x)=(e^x-1-x)/x^2$ for $x\ne0$ , is increasing.
(3.2) Corollary: $\exp(\lambda x)\le1+\lambda x+x^2e(\lambda)$ for $\lambda\ge0$ , $x\le1$ .
(3.5): $E\{\exp(\lambda X)\}\le1+e(\lambda)\operatorname{Var}X\le\exp[e(\lambda)\operatorname{Var}X]$ for $\lambda\ge0$ , $X\le1$ , $E(X)\le0$ .
Proof of (3.3): $\{Q_\lambda(T_n,S_n),\mathcal F_n\}$ is a supermartingale for $\lambda\ge0$ .
(3.3) Proposition: $\int_{\{\sigma<\infty\}}Q_\lambda(T_\sigma,S_\sigma)\,dP\le1$ for every stopping time $\sigma$ and $\lambda\ge0$ .
Proof of (4.1): $P\{A\}\le\exp[-\lambda a+e(\lambda)b]$ for every $\lambda\ge0$ , where $A$ is the event of the goal.
Proof of (4.1): $\lambda_0=\log[(a+b)/b]$ minimizes this bound, with value $(b/(a+b))^{a+b}e^a$ .
Proof of (4.1): $(b/(a+b))^{a+b}e^a\le\exp[-a^2/(2(a+b))]$ .

Significance

The inequality bounds the probability that a supermartingale ever reaches level $a$ before its accumulated conditional variance exceeds $b$ . Since it holds for all times at once, fixed-horizon versions follow immediately, as do versions with stopping times, and with a peeling argument over $b$ it gives the variance-adaptive confidence sequences used in sequential testing and in the analysis of algorithms. Freedman's paper uses it to derive the law of the iterated logarithm for martingales; later work uses it wherever a martingale's conditional variance is much smaller than the square of its increment bound.

The theorem has been proved for fifty years. What this mission adds is a machine-checked statement and proof of the full infinite-horizon form under the one-sided hypothesis (3.4), together with the exponential supermartingale and the optional-stopping bound (3.3) as reusable lemmas. Prove2Me already has fixed-horizon Bernstein-form consequences for martingale differences; the infinite-horizon Bennett form under (3.4) does not appear in Mathlib or on the platform.

Difficulty

The naive route of applying Markov's inequality to $\exp(\lambda S_n)$ at a fixed $n$ gives a bound for one time only and requires a deterministic bound on $T_n$ . Taking a union over all $n$ loses everything. The content of the theorem is that the random clock $T_n$ and the supremum over time can both be absorbed, which requires an exponential process compensated by the random $T_n$ and an optional-stopping bound for stopping times that may be infinite with positive probability. The process need not be uniformly integrable, and the increments have no lower bound. A second, smaller, difficulty is the variance form of (3.5): the bound uses $\operatorname{Var}X$ rather than $E(X^2)$ , which is strictly sharper when $E(X)<0$ and is needed to compensate with conditional variances.

Formalization scope

Lean conventions this mission commits to:

Increments are a sequence X : ℕ → Ω → ℝ used from index $1$ (X 0 is never read), so $S_n$ , $T_n$ and $V_n$ carry the paper's indices. The filtration is Mathlib's Filtration ℕ m, and " $X_n$ is $\mathcal F_n$ -measurable" is StronglyMeasurable[ℱ n] (X n) for $n\ge1$ .
$V_n$ is Mathlib's condVar (ℱ (n - 1)) (X n) P. Mathlib sets a conditional expectation of a non-integrable function to $0$ , so every increment is assumed square integrable (MemLp (X n) 2 P). This is the one hypothesis added to the page. Under (3.4) the page also allows increments of infinite variance, for which its $T_n$ is $+\infty$ ; the formalization narrows the class of processes and leaves every conclusion as printed. Milestone (3.5) likewise assumes $E(X^2)<\infty$ , which is the case the page reduces to.
"Expectation-decreasing martingale" is Mathlib's Supermartingale.
Stopping times are Ω → WithTop ℕ with IsStoppingTime; $\top$ is $\infty$ . In (3.3) the integral over $\{\sigma<\infty\}$ is a lower Lebesgue integral in $[0,\infty]$ , so the bound does not presuppose integrability, and $S_\sigma$ , $T_\sigma$ are read only on $\{\sigma\ne\infty\}$ .
The probability of the event "for some $n$ " is the measure of $\{\omega:\exists n\ge1,\ S_n(\omega)\ge a,\ T_n(\omega)\le b\}$ . $(b/(a+b))^{a+b}$ is a real power.
(3.1) is stated as strict monotonicity, which its proof ( $g'(x)>0$ for $x\ne0$ ) establishes.

A fixed-horizon statement ( $n=N$ , or $n\le N$ ), a martingale hypothesis $E\{X_n\mid\mathcal F_{n-1}\}=0$ , or a two-sided bound $|X_n|\le1$ would each be a strictly weaker theorem than (4.1) and is not an acceptable formalization of the goal.

The development needs exponential supermartingales compensated by conditional variance, optional stopping for stopping times that may be infinite, and elementary real analysis of $e^x$ . The real-analysis milestones (3.1), (3.2) and the two calculus steps are independent and reusable; (3.5) is a self-contained moment-generating-function bound; the supermartingale and (3.3) are reusable for every exponential-supermartingale argument. Contributions to any milestone, and alternative proofs of the goal, are welcome.

Selected references

David A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1) (1975), 100–118. https://doi.org/10.1214/aop/1176996452 (source of this mission; a scanned copy of the published article, cited by printed page)
George Bennett, Probability Inequalities for the Sum of Independent Random Variables, Journal of the American Statistical Association 57 (1962), 33–45. https://doi.org/10.1080/01621459.1962.10482149
Wassily Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963), 13–30. https://doi.org/10.1080/01621459.1963.10500830

11 thms3 active usersReviewed

Operations Research Optimization Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 1: Markdown Is Optimal Once Time-to-Go Falls Below a Strictly Increasing Threshold x_nResearch Paper

Why the timing of a markdown matters

A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.

The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.

Prices, demand, and admissible switches

Let $n\ge1$ be the initial stock and $t\ge0$ the time to go. The seller first charges price $p_1$ and may change once to a lower price $p_2$ . Demands at the two prices are independent Poisson counts with positive rates $\lambda_1$ and $\lambda_2$ . A lower price produces more arrivals, so $p_2<p_1$ and $\lambda_1<\lambda_2$ . Feng and Gallego also assume that lowering the price increases the revenue rate: $p_1\lambda_1<p_2\lambda_2$ . There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.

Write $N_1(s)$ for the observed sales count at the initial price by time $s$ . If the price changes at deterministic time $s\in[0,t]$ , let $J(n,t;s)$ be the expected total revenue. The count after the change is independent of $N_1(s)$ , and their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$ . The optimal value $J(n,t)$ allows the switch time $\tau$ to depend on the counts observed so far. An admissible $\tau$ lies between zero and $t$ , is a stopping time for the history of $N_1$ , and occurs before stock is exhausted almost surely. At $s=0$ , $J(n,t;0)$ is the revenue from charging $p_2$ immediately. The paper defines these quantities in §3, pp. 1377–1379.

Formalization targets

The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence $x_1<x_2<\cdots$ of inventory-dependent thresholds. When $t\le x_n$ , switching immediately earns the optimal value; when $t>x_n$ , a correction $F(n,t)$ is added:

J(n,t)=\begin{cases} J(n,t;0),&t\le x_n,\\ J(n,t;0)+F(n,t),&t>x_n. \end{cases}

The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with $F(0,t)=0$ . For $n\ge1$ , set $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ , where $G$ is the Poisson-tail expression from §4.1. The threshold $x_n$ is the first nonnegative zero of $L(n,\cdot)$ . A function $H(n,\cdot)$ satisfies $\partial_tH=-\lambda_1H+L$ for positive time and $H(n,x_n)=0$ ; $F$ is zero below $x_n$ and equals $H$ at and above it. If $y_n$ is the first zero of $G(n,\cdot)$ , the theorem also gives $x_1=y_1$ and $x_n<y_n$ for $n>1$ .

Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of $G$ in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.

What the result provides

The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.

The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.

Where the mathematics is difficult

The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory $n$ depends on the correction at stock $n-1$ . Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of $G$ , the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.

The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.

Formalization scope

Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.

The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.

For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

6 thms3 active usersReviewed

Completed

Statistics·Captain: mikedeng1

Poisson Approximation for Dependent Trials 2: For φ-Mixing Bernoulli Trials, an Order-λ⁻¹ Bound on |Eh(W) − 𝒫_λh| in Var W − λ + 2(2m+1)Σp_i² and nφ(m+1)Research Paper

Motivation

The number of successes in many rare trials is approximately Poisson. For independent trials the quality of that approximation was quantified by Le Cam in 1960: if $X_1,\dots,X_n$ are independent Bernoulli variables with $P(X_i=1)=p_i$ , $W=\sum_i X_i$ and $\lambda=\sum_i p_i$ , the total variation distance between the law of $W$ and the Poisson law with mean $\lambda$ is bounded by a constant multiple of $\sum_i p_i^2$ , and by a constant multiple of $\lambda^{-1}\sum_i p_i^2$ when $\lambda\ge 1$ . Many applications have dependent trials: occurrences of a pattern in a sequence, exceedances of a high level by a stationary process, failures in a system with local interactions. L. H. Y. Chen's 1975 paper extended Charles Stein's method of normal approximation to the Poisson case and obtained explicit bounds for dependent trials. The approach became known as the Stein–Chen method, and is now the standard tool for Poisson approximation of dependent counts.

Timeline.

1960. Le Cam proves the independent-trial bounds (0.1)–(0.3) of Chen's introduction.
1964. Kerstan extends them to independent nonnegative integer variables and improves the constant in (0.3).
1970. Stein introduces his method of normal approximation for dependent variables.
1975. Chen (Ann. Probab. 3) adapts it to Poisson approximation. He proves Theorems 4.1–4.4 for sequences satisfying Ibragimov's mixing condition, the $m$ -dependent case, and a second-order expansion for independent trials.

This mission formalizes the order- $\lambda^{-1}$ bound of that paper, Theorem 4.2.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and let $X_1,\dots,X_n$ be Bernoulli trials: random variables with values in $\{0,1\}$ and $p_i=P(X_i=1)$ . Following the paper, set $X_i\equiv0$ for $i\le0$ and $i\ge n+1$ . Put

W=\sum_{i=1}^nX_i,\qquad \lambda=\sum_{i=1}^np_i .

For a bounded real function $h$ on the nonnegative integers, the Poisson expectation is

\mathcal P_\lambda h=e^{-\lambda}\sum_{k=0}^\infty h(k)\frac{\lambda^k}{k!},

the mean of $h$ under the Poisson law with parameter $\lambda$ . The quantity of interest is $|Eh(W)-\mathcal P_\lambda h|$ for all $h$ with $|h|\le1$ . Its supremum over such $h$ is twice the total variation distance between the law of $W$ and the Poisson law.

Dependence is measured by Ibragimov's mixing condition (4.1). Let $\mathcal M_{a,b}=\sigma(X_i:a\le i\le b)$ . There must be a non-increasing sequence $\varphi(k)\downarrow0$ such that for all $j,k\ge1$ and every event $B\in\mathcal M_{j+k,\infty}$ ,

|P(B\mid\mathcal M_{1j})-P(B)|\le\varphi(k)\quad\text{almost surely}.

A sequence is $m$ -dependent when $(X_1,\dots,X_r)$ and $(X_{r+k},\dots)$ are independent for all $k>m$ . It then satisfies (4.1) with $\varphi(k)=0$ for $k>m$ .

The proof works with the partial sums $V^{(i)}=\sum_{|k-i|>m}X_k$ , $V^{(i,j)}=\sum_{|k-i|>m,|k-j|>m}X_k$ , $Y_{ij}=V^{(i)}+\sum_{k=i-m}^jX_k$ and $Y'_{ij}=V^{(i)}+\sum_{k=i-m,k\ne i}^jX_k$ . It also uses the Stein solution $S_\lambda h$ , the solution for $w\ge1$ of $wf(w)-\lambda f(w+1)=h(w)-\mathcal P_\lambda h$ .

Formalization targets

Goal: Theorem 4.2, (4.13)

For every $m=0,1,2,\dots$ and every $h$ with $|h|\le1$ ,

|Eh(W)-\mathcal P_\lambda h|\le2\lambda^{-1}\bigl[8m+5+4(n\varphi(m+1))^{1/2}\bigr]\Bigl[\operatorname{Var}(W)-\lambda+2(2m+1)\sum_{i=1}^np_i^2\Bigr]+32\bigl[6m+3+(n\varphi(m+1))^{1/2}\bigr]n\varphi(m+1).

The bound involves only the law of $W$ through $\operatorname{Var}(W)$ , the success probabilities, the window $m$ and the mixing rate. The window $m$ is free, so the statement covers every trade-off between local dependence and mixing.

Consequences (companion items)

Theorem 4.3, (4.21). For $m$ -dependent trials, $|Eh(W)-\mathcal P_\lambda h|\le2(8m+5)\lambda^{-1}\bigl[\sum\sum_{i\ne j}\operatorname{Cov}(X_i,X_j)+(4m+1)\sum p_i^2\bigr]$ .
Corollary 4.1, (4.23). For independent trials, $|Eh(W)-\mathcal P_\lambda h|\le10\lambda^{-1}\sum p_i^2$ . This improves Le Cam's (0.3).
Theorem 4.4. For identically distributed trials with $\varphi(m)=e^{-\alpha m}$ , there are bounds (4.24) and (4.25) whose constants depend only on $\alpha$ .

Milestones

The milestones follow the paper's proof:

the basic identity (2.2), the Stein solution (2.5) and the expansion (2.6);
the bounds on $S_\lambda h$ : Lemmas 3.1–3.3, (3.6) and Lemma 3.5;
the mixing inequalities, Lemmas 4.1–4.3 and 4.6;
the variance bound, Lemma 4.4;
the four displays (4.14) and (4.16)–(4.19) of the proof of Theorem 4.2;
Cauchy–Schwarz (4.10) and Lemma 4.5.

Significance

Theorem 4.2 gives an error of order $\lambda^{-1}$ times the excess variance $\operatorname{Var}(W)-\lambda+O(m\sum p_i^2)$ , plus a mixing remainder. When the trials are nearly uncorrelated, $\operatorname{Var}(W)\approx\lambda$ and the bound is small even though $\lambda$ is large. This is the regime where the companion Theorem 4.1, which carries a factor $\min(\lambda^{-1/2},1)$ , is weaker. The independent case recovers Le Cam's order $\lambda^{-1}\sum p_i^2$ with constant 10. The $m$ -dependent case gives explicit Poisson limit theorems for scan statistics and pattern counts.

All results of the paper are proved there, and the proofs are elementary apart from the measure theory of Lemma 4.1. To our knowledge none of them has a machine-checked proof. Mathlib has the Poisson distribution and conditional expectation, but no Stein–Chen bound and no mixing inequality of Ibragimov's type. A formal proof would give the first checked quantitative Poisson approximation for dependent trials. It would also give reusable covariance inequalities for $\varphi$ -mixing sequences (Lemmas 4.2 and 4.3).

Difficulty

Most of the work is bookkeeping, and it is heavy. Identity (2.2) needs a telescoping over windows $[i-m,j]$ whose ends can fall outside $[1,n]$ . (4.15)–(4.18) need $|Y'_{i,j-1}+1-\lambda|$ to be compared with $|V^{(i,j)}-EV^{(i,j)}|$ with explicit constants.

The genuinely probabilistic step is the decoupling of Lemma 4.2. Condition (4.1) controls conditional probabilities of events. Lemma 4.2 needs a bound on conditional expectations of functions of a whole random vector. Passing from one to the other requires a regular conditional distribution that is uniformly close to the unconditional law on a set of full measure (Lemma 4.1). The naive route, applying (4.1) to each level set of a simple function, loses a factor that grows with the number of levels and does not give the constant $2\|f\|$ .

The bound (4.16) applies Lemma 4.4 to a subsequence of the trials. This uses the fact that dropping variables preserves (4.1) with the same $\varphi$ , because $\varphi$ is non-increasing.

Formalization scope

Trials. The trials are a map $X:\mathbb N\to\Omega\to\mathbb N$ that is measurable, vanishes at index $0$ and above $n$ , and is at most $1$ almost surely. The constant padding adds nothing to any $\sigma$ -algebra, so (4.1), $m$ -dependence and independence of the padded sequence are those of $X_1,\dots,X_n$ .
Probabilities and moments. $p_i$ is defined as $P(X_i=1)$ , not taken as a parameter. $\operatorname{Var}$ and $\operatorname{Cov}$ are Mathlib's. All integrands are almost surely bounded, so no integrability hypotheses are needed.
Norms. Sup norms are replaced by bounds $M$ with $|h|\le M$ . $\|S_\lambda h\|$ ranges over $w\ge1$ .
Mixing condition. In (4.1) the conditional probability is the conditional expectation of the indicator, and lags are $k\ge1$ .
Added hypotheses. The §3 lemmas and (2.6), (4.14) assume $\lambda>0$ , because they divide by $\lambda$ . The goal and the companions do not assume it: at $\lambda=0$ all $p_i$ vanish, $W=0$ almost surely, and both sides are $0$ under Lean's convention $0^{-1}=0$ .
Lemmas 4.2 and 4.3. They are stated for an arbitrary measurable real sequence satisfying (4.1), as on the page. The independent copy $Z'$ is expressed through the law of $Z$ .
Theorem 4.4. Its constants are quantified before the probability space, $n$ and the trials. This is what "depend only on $\alpha$ " means.

A trivializing formalization is ruled out. Measurability of the trials is part of the definition, because otherwise conditional expectations in (4.1) collapse to $0$ . The goal mentions only $W$ , $\lambda$ , $p_i$ , $\operatorname{Var}(W)$ , $\varphi$ , $m$ and $h$ . It does not mention $S_\lambda h$ or any milestone quantity.

A complete development needs the Stein solution and its bounds, a Bernoulli-sum calculus over integer windows, regular conditional distributions on standard Borel spaces, and the mixing covariance inequalities. The last two are reusable beyond this mission. Contributions to any milestone are welcome, as are alternative proofs of Lemma 4.2 through Mathlib's condDistrib.

Selected references

L. H. Y. Chen, Poisson approximation for dependent trials, Annals of Probability 3(3):534–545, 1975. https://doi.org/10.1214/aop/1176996359
L. Le Cam, An approximation theorem for the Poisson binomial distribution, Pacific Journal of Mathematics 10(4):1181–1197, 1960. https://doi.org/10.2140/pjm.1960.10.1181
C. Stein, A bound for the error in the normal approximation to the distribution of a sum of dependent random variables, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2:583–602, 1972. https://projecteuclid.org/euclid.bsmsp/1200514239
I. A. Ibragimov, Some limit theorems for stationary processes, Theory of Probability and its Applications 7(4):349–382, 1962. https://doi.org/10.1137/1107036
A. D. Barbour, L. Holst, S. Janson, Poisson Approximation, Oxford University Press, 1992. ISBN 978-0-19-852235-9

22 thms3 active usersReviewed

Completed

Statistics·Captain: mikedeng1

Poisson Approximation for Dependent Trials 3: For Independent Trials with max p_i ≤ λ/2, |Eh(W) − 𝒫_λh + (Σp_i²)𝒫_λU_λh| ≤ (24 + 96√2)λ⁻¹Σp_i³Research Paper

Motivation

The number of successes in many rare, roughly independent trials is approximately Poisson. This law of small numbers is used for counts of rare events in reliability, insurance, epidemiology, queueing and random combinatorics. A quantitative version says how large the error is. For independent Bernoulli trials with success probabilities $p_1,\dots,p_n$ and $\lambda=\sum p_i$ , Le Cam (1960) showed that the error in total variation is of order $\sum p_i^2$ . When all $p_i$ are small this tends to zero, but it does not say what the leading part of the error is.

L. H. Y. Chen's 1975 paper (Ann. Probab. 3, 534–545) adapted Charles Stein's method for normal approximation to the Poisson case. The result is now called the Stein–Chen method. The paper's §2–§4 give first-order error bounds for dependent (mixing) trials. Its §5, "A refinement", goes one order further for independent trials. It identifies the first-order correction explicitly and shows that what remains is of order $\lambda^{-1}\sum p_i^3$ . Kerstan (1964) had obtained a similar expansion by a different method. Chen's version comes from iterating the basic identity of the Stein–Chen method. This mission formalizes §5.

Timeline:

1953: Prohorov bounds the distance between the binomial and the Poisson law.
1960: Le Cam proves the $\sum p_i^2$ bound for independent, non-identical trials. Hodges and Le Cam give a short proof.
1964: Kerstan gives a refinement of the Prohorov–Le Cam bounds.
1975: Chen introduces the Stein–Chen method. It gives first-order bounds under Ibragimov's mixing condition and the second-order expansion (Theorem 5.1) for independent trials.

Setting

Let $X_1,\dots,X_n$ be independent random variables on a probability space, each taking only the values $0$ and $1$ , with success probabilities $p_i=P(X_i=1)$ . Put

W=\sum_{i=1}^nX_i,\qquad\lambda=\sum_{i=1}^np_i,\qquad W^{(i)}=\sum_{k\ne i}X_k,\qquad\lambda^{(i)}=\sum_{j\ne i}p_j .

For a bounded real function $h$ on the nonnegative integers, the Poisson expectation is

\mathscr P_\lambda h=e^{-\lambda}\sum_{k=0}^\infty h(k)\frac{\lambda^k}{k!},

the mean of $h$ under the Poisson law with parameter $\lambda$ . The Stein equation is $wf(w)-\lambda f(w+1)=h(w)-\mathscr P_\lambda h$ . For $w\ge1$ its solution is

S_\lambda h(w)=-(w-1)!\,\lambda^{-w}\sum_{k=0}^{w-1}\bigl[h(k)-\mathscr P_\lambda h\bigr]\frac{\lambda^k}{k!}.

Write $\Delta f(w)=f(w+1)-f(w)$ and $Lf(w)=f(w+1)$ . Chen's second-order operator is

U_\lambda h(w)=\Delta S_\lambda h(w+1)=S_\lambda h(w+2)-S_\lambda h(w+1),\qquad w\ge0 .

For another parameter $b>0$ , $S_bU_\lambda h$ and $U_bU_\lambda h$ apply the Stein solution and the operator with parameter $b$ to the function $U_\lambda h$ .

In Lean: poissonExp, stein, delta, shiftL, stU, prob, lam, lamExcept, W, Wi, all in the namespace PoissonDepTrials.SecondOrder.

Formalization targets

Goal: Theorem 5.1, (5.7)

If $X_1,\dots,X_n$ are independent, $n\ge2$ and $\bar p=\max_ip_i\le\lambda/2$ , then for every $h$ with $|h|\le1$ ,

\Bigl|Eh(W)-\mathscr P_\lambda h+\Bigl(\sum_{i=1}^np_i^2\Bigr)\mathscr P_\lambda U_\lambda h\Bigr|\le\bigl(24+96\sqrt2\bigr)\lambda^{-1}\sum_{i=1}^np_i^3 .

The paper writes the constant as "an absolute constant $C$ not greater than $24+96(2)^{1/2}$ ". The formal goal fixes $C$ at that value, which is the same statement.

Milestones

In order: the Stein solution (2.3)/(2.5); the difference identity (3.6); Lemmas 3.1, 3.2, 3.3 and 3.5 (bounds on $S_\lambda h$ and $\Delta S_\lambda h$ ); the first-order identity (5.8) $Eh(W)=\mathscr P_\lambda h-\sum_ip_i^2EU_\lambda h(W^{(i)})$ ; Lemmas 5.1 and 5.2 (dependence of Poisson expectations on the parameter); Lemmas 5.3–5.5 (bounds on $\mathscr P_b|L^mU_\lambda h|$ , $S_bU_\lambda h$ and $U_bU_\lambda h$ ); the bound (5.9),

\Bigl|Eh(W)-\mathscr P_\lambda h+\Bigl(\sum p_i^2\Bigr)\mathscr P_\lambda U_\lambda h\Bigr|\le24\lambda^{-1}\sum_ip_i^3+96\lambda^{-1}\sum_i\sum_{j\ne i}\frac{p_i^2p_j^2}{\lambda^{(i)}};

and the closing inequality $\lambda^{-1}\sum_ip_i^2\sum_{j\ne i}p_j^2/\lambda^{(i)}\le\sqrt2\,\lambda^{-1}\sum_ip_i^3$ .

Significance

The theorem gives an explicit first correction to the Poisson approximation of a Poisson-binomial law, with a remainder of the next order. When all $p_i$ equal $p$ , the first-order error $\sum p_i^2=\lambda p$ is replaced by the remainder $\lambda^{-1}\sum p_i^3=p^2$ , which is smaller by the factor $\lambda$ . The correction term is a functional of the Poisson law alone, $-(\sum p_i^2)\mathscr P_\lambda U_\lambda h$ . It can be evaluated without knowing the distribution of $W$ . The method of proof applies the basic identity twice. The paper notes that further iteration gives expansions to any order.

On the formal side, Mathlib has the Poisson distribution but no Stein–Chen machinery and no quantitative Poisson approximation. The theorem has, as far as is known, no machine-checked proof. This mission produces the Stein solution and its standard bounds (Lemmas 3.1–3.5), which are reusable by any Stein–Chen argument. It also produces the parameter-perturbation estimates of Lemmas 5.1–5.2 and a complete second-order expansion. Missions 1 and 2 of this series formalize the first-order bounds of §4 under a mixing condition. They share the Stein-solution layer.

Difficulty

The first-order bound needs only that $\Delta S_\lambda h$ is uniformly small (Lemma 3.4). A second-order bound needs more. After the first application of the identity, the error $\sum p_i^2EU_\lambda h(W^{(i)})$ has to be expanded again. That requires control of the iterated operator $U_bU_\lambda h$ with a different parameter $b=\lambda^{(i)}$ , because $W^{(i)}$ is approximately Poisson with mean $\lambda^{(i)}$ , not $\lambda$ . The bound on $U_bU_\lambda h$ (Lemma 5.5) grows linearly in $|w-\lambda|$ . Applying the uniform bounds of §3 throughout loses a factor $\lambda^{1/2}$ and produces an error of order $\lambda^{-1/2}\sum p_i^3$ instead of $\lambda^{-1}\sum p_i^3$ . The linear growth has to be paired with the variance of $W^{(i,j)}$ . The averaging over pairs $(i,j)$ in the final step uses the condition $\bar p\le\lambda/2$ , which keeps every $\lambda^{(i)}$ comparable to $\lambda$ .

Formalization scope

Conventions committed to in Lean:

The trials are a sequence X : ℕ → Ω → ℕ. Each $X_i$ is measurable with values in $\{0,1\}$ almost surely. $X_i\equiv0$ for $i=0$ and $i>n$ , which is the paper's own padding convention (p. 535). Independence is iIndepFun (fun i => X i) P over all of ℕ. Because the padding variables are constants, this is equivalent to independence of $X_1,\dots,X_n$ .
$p_i$ is defined from $X$ , not taken as a parameter.
$\|h\|$ is replaced by an arbitrary bound $M$ with $|h(k)|\le M$ for all $k$ . The norm of $S_\lambda h$ is taken over its domain $w\ge1$ .
$\bar p\le\lambda/2$ is written as $p_i\le\lambda/2$ for every $i\in\{1,\dots,n\}$ .
The goal assumes neither $\lambda>0$ nor integrability. Every function involved is bounded, so every expectation and Poisson sum is genuine. At $\lambda=0$ both sides of (5.7) vanish.

Hypotheses added relative to the page, each disclosed in the item's Formalization Note:

$\lambda>0$ in the §3 and §5 lemmas, in (5.8) and in (5.9). These divide by $\lambda$ , by $b$ or by $\lambda^{(i)}$ .
$b>0$ in Lemmas 5.3–5.5, which is the standing range of §5.
Boundedness of $f$ in Lemma 5.2. The lemma is only applied to bounded functions.

The random indices $I,J$ that the paper introduces to shorten notation in (5.8)–(5.9) are not formalized. The same quantities are written as finite sums over indices.

Ruled out: the second-order term must be the operator $U_\lambda h=\Delta S_\lambda h(\cdot+1)$ built from the Stein solution exactly as on p. 543. A free function, or $U_\lambda h$ evaluated at the junk value $S_\lambda h(0)$ , would empty the theorem.

Welcome contributions include:

the Stein-solution bounds of §3, which are reusable well beyond this paper;
Poisson-sum manipulations (Lemmas 5.1–5.2);
the independence bookkeeping that turns (2.6) into (5.8).

Selected references

L. H. Y. Chen, Poisson approximation for dependent trials, Ann. Probab. 3(3):534–545, 1975. https://doi.org/10.1214/aop/1176996359
L. Le Cam, An approximation theorem for the Poisson binomial distribution, Pacific J. Math. 10:1181–1197, 1960. https://doi.org/10.2140/pjm.1960.10.1181
J. L. Hodges and L. Le Cam, The Poisson approximation to the Poisson binomial distribution, Ann. Math. Statist. 31:737–740, 1960. https://doi.org/10.1214/aoms/1177705799
J. Kerstan, Verallgemeinerung eines Satzes von Prochorow und Le Cam, Z. Wahrscheinlichkeitstheorie verw. Gebiete 2:173–179, 1964. https://doi.org/10.1007/BF00533419
C. Stein, A bound for the error in the normal approximation to the distribution of a sum of dependent random variables, Proc. Sixth Berkeley Symp. Math. Statist. Prob. 2, 1972. https://projecteuclid.org/euclid.bsmsp/1200514239

16 thms3 active usersReviewed

Completed

Statistics·Captain: mikedeng1

Poisson Approximation for Dependent Trials 1: For φ-Mixing Bernoulli Trials, |Eh(W) − 𝒫_λh| ≤ 6 min(λ^{−1/2}, 1)[Var W − λ + 2(2m+1)Σp_i² + 4(λ+1)nφ(m+1)]Research Paper

Motivation

A sum of many rare events is approximately Poisson. For independent Bernoulli trials this is the classical law of small numbers, and its quantitative form goes back to Prohorov (1953) and Le Cam (1960): if $X_1,\dots,X_n$ are independent with $P(X_i=1)=p_i$ , then the law of $W=\sum_i X_i$ is close to the Poisson law with mean $\lambda=\sum_i p_i$ , with an error controlled by $\sum_i p_i^2$ . Many applications need the same conclusion for dependent trials: runs and clusters in sequences, exceedances of a stationary time series, matches in DNA sequences, extremes of mixing processes.

Louis H. Y. Chen's 1975 paper adapted Charles Stein's method for normal approximation (1970, published 1972) to the Poisson case and obtained explicit error bounds for sums of dependent Bernoulli trials under mixing and $m$ -dependence. The technique, now called the Stein–Chen method, became the standard tool for Poisson approximation, through Arratia, Goldstein and Gordon (1989) and Barbour, Holst and Janson, Poisson Approximation (1992).

Timeline:

1953–1960. Prohorov and Le Cam bound the error of the Poisson approximation for independent trials.
1964. Kerstan extends Le Cam's bounds to independent nonnegative integer-valued variables.
1970. Stein introduces his method for normal approximation of dependent sums (Berkeley Symposium, proceedings 1972).
1975. Chen proves Poisson approximation bounds for $\varphi$ -mixing and $m$ -dependent trials (this mission).
1989–1992. Arratia–Goldstein–Gordon and Barbour–Holst–Janson give local-dependence and total-variation versions.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1,\dots,X_n$ Bernoulli random variables, possibly dependent, with success probabilities $p_i=P(X_i=1)$ . Put

W=\sum_{i=1}^n X_i,\qquad \lambda=\sum_{i=1}^n p_i .

For a real function $h$ on the nonnegative integers, the Poisson expectation of $h$ is

\mathcal P_\lambda h=e^{-\lambda}\sum_{k=0}^\infty h(k)\frac{\lambda^k}{k!},

the mean of $h$ under the Poisson distribution with parameter $\lambda$ . The quantity to be bounded is $|Eh(W)-\mathcal P_\lambda h|$ for all $h$ with $|h|\le1$ ; its supremum over such $h$ is twice the total variation distance between the law of $W$ and the Poisson law.

Dependence is measured by Ibragimov's mixing condition. Write $\mathcal M_{a,b}$ for the $\sigma$ -algebra generated by $X_a,\dots,X_b$ and $\mathcal M_{a,\infty}$ for that generated by $X_a,X_{a+1},\dots$ . The sequence satisfies (4.1) with a nonincreasing sequence $\varphi(k)\downarrow0$ if, for all $j,k\ge1$ and every event $B\in\mathcal M_{j+k,\infty}$ ,

\bigl|P(B\mid\mathcal M_{1j})-P(B)\bigr|\le\varphi(k)\quad\text{almost surely}.

Thus $\varphi(k)$ bounds how much knowledge of the first $j$ trials can change the probability of an event determined by trials at distance at least $k$ . A sequence is $m$ -dependent if $(X_1,\dots,X_r)$ and $(X_{r+k},X_{r+k+1},\dots)$ are independent whenever $k>m$ ; then (4.1) holds with $\varphi(k)=0$ for $k>m$ , and independent trials are the case $m=0$ .

Formalization targets

Goal: Theorem 4.1 (p. 541)

For every $m=0,1,2,\dots$ and every $h$ with $|h|\le1$ ,

\bigl|Eh(W)-\mathcal P_\lambda h\bigr|\le6\min(\lambda^{-1/2},1)\Bigl[\operatorname{Var}(W)-\lambda+2(2m+1)\sum_{i=1}^np_i^2+4(\lambda+1)\,n\,\varphi(m+1)\Bigr].

The parameter $m$ is free: it trades the local term $2(2m+1)\sum p_i^2$ against the mixing term $n\varphi(m+1)$ .

Consequences

Theorem 4.3, (4.20). For $m$ -dependent trials the mixing term vanishes:

\bigl|Eh(W)-\mathcal P_\lambda h\bigr|\le6\min(\lambda^{-1/2},1)\Bigl[\sum\sum_{i\ne j}\operatorname{Cov}(X_i,X_j)+(4m+1)\sum_{i=1}^np_i^2\Bigr].

Corollary 4.1 (Le Cam), (4.22). For independent trials, $|Eh(W)-\mathcal P_\lambda h|\le6\min(\lambda^{-1/2},1)\sum_ip_i^2$ .

Milestones

The milestones follow the paper's proof:

the basic identity (2.2) for $E[Wf(W)-\lambda f(W+1)]$ , valid for any dependence;
the solution $S_\lambda h$ of the Stein equation (2.3)–(2.5), and the resulting representation (2.6) of $Eh(W)-\mathcal P_\lambda h$ ;
the bounds on $S_\lambda h$ and $\Delta S_\lambda h$ (Lemmas 3.1–3.4);
the covariance inequalities under mixing (Lemmas 4.1–4.3, 4.6);
the variance identity (4.7), the bound (4.8), the inequality (4.10) and Lemma 4.5.

Significance

The theorem bounds the distance to the Poisson law by quantities a user can compute or estimate: the variance of $W$ , the $p_i$ , and the mixing rate. When the trials are weakly dependent and individually rare, $\operatorname{Var}(W)\approx\lambda$ , $\sum p_i^2$ is small, and the bound is small. It recovers Le Cam's independent-case bound up to the constant and extends it to $m$ -dependent and $\varphi$ -mixing sequences. The expansion (2.6) and the bounds on the Stein solution in §3 are reused throughout the later literature on the Stein–Chen method.

The results of this paper are proved on paper; none of them is formalized in a proof assistant. Mathlib has the Poisson distribution, conditional expectation, independence and regular conditional distributions, but no Stein–Chen identity, no bounds on the Stein solution, and no covariance inequality for $\varphi$ -mixing sequences. This mission produces all three, and the companion missions of this series (Theorem 4.2, an order- $\lambda^{-1}$ bound, and Theorem 5.1, a second-order refinement for independent trials) rely on the same objects.

Difficulty

The identities (2.2), (2.6) and (4.7) are finite manipulations, and the bounds of §3 on $S_\lambda h$ are elementary real analysis. The main difficulty is the transfer of the mixing condition from events to functions. Condition (4.1) bounds conditional probabilities of single events almost surely, with a null set that depends on the event. Lemma 4.2 needs a bound on $E^Yf(Y,Z)-E^Yf(Y,Z')$ for an arbitrary bounded function of a past vector $Y$ and a future vector $Z$ ; this requires a regular conditional distribution of $Z$ given $Y$ and one null set that works for all events at once (Lemma 4.1). That step uses that $\mathbb R^s$ is a standard Borel space, and it fails for an argument that handles one event at a time. Lemma 4.3 then needs care with the independent copy $Z'$ and with the three-block decomposition.

Formalization scope

All objects are defined in PoissonDepTrials.MixSqrt.Setting. The conventions are:

The trials are a sequence $X:\mathbb N\to\Omega\to\mathbb N$ , measurable, with values in $\{0,1\}$ almost surely, and identically zero at index $0$ and at indices above $n$ . The zero padding is the paper's own convention (p. 535), and it changes no $\sigma$ -algebra.
$p_i$ is defined as $P(X_i=1)$ , not taken as a parameter.
$\|h\|$ is replaced by an arbitrary bound $M$ with $|h|\le M$ . $\|S_\lambda h\|$ is taken over $w\ge1$ , the domain of $S_\lambda h$ .
$P(B\mid\mathcal M_{1j})$ is the conditional expectation of the indicator of $B$ . Measurability of every $X_i$ is assumed wherever (4.1) is used.
$m$ -dependence is stated for the tail $\sigma$ -algebra $\mathcal M_{r+k,\infty}$ , which is equivalent to the paper's finite blocks.
$E^Yf(Y,Z')$ , for $Z'$ an independent copy of $Z$ , is written as $\int f(Y,z)\,dP_Z(z)$ , without enlarging $\Omega$ .
In Lemma 4.1, "Borel space" is StandardBorelSpace.

Added hypotheses: $\lambda>0$ in the identity (2.6) and in Lemmas 3.3, 3.4 and (2.5), because $S_\lambda h$ divides by $\lambda^w$ ; $m\ge1$ and $a\ge1$ in Lemmas 4.2 and 4.3, because (4.1) concerns lags $\ge1$ of a sequence starting at $X_1$ . The goal has no hypothesis $\lambda>0$ : at $\lambda=0$ every trial vanishes almost surely and both sides are zero.

The goal does not mention $S_\lambda h$ , $V^{(i)}$ or $Y_{ij}$ ; it is stated only in terms of $W$ , $\lambda$ , the $p_i$ , $\operatorname{Var}(W)$ , $\varphi$ , $m$ and $h$ . The mixing condition is required to hold with a nonincreasing $\varphi$ tending to $0$ , so it cannot be satisfied vacuously.

Reusable infrastructure includes the Stein–Chen identity (2.2), the bounds on the Stein solution (Lemmas 3.3, 3.4), and the covariance inequalities for $\varphi$ -mixing sequences (Lemmas 4.2, 4.3), which apply beyond Poisson approximation. Proofs of any milestone are welcome, as are proofs of the companion results from the goal.

Selected references

L. H. Y. Chen, Poisson approximation for dependent trials, Ann. Probab. 3(3):534–545, 1975. https://doi.org/10.1214/aop/1176996359
C. Stein, A bound for the error in the normal approximation to the distribution of a sum of dependent random variables, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2:583–602, 1972. https://projecteuclid.org/euclid.bsmsp/1200514239
L. Le Cam, An approximation theorem for the Poisson binomial distribution, Pacific J. Math. 10(4):1181–1197, 1960. https://doi.org/10.2140/pjm.1960.10.1181
I. A. Ibragimov, Some limit theorems for stationary processes, Theory Probab. Appl. 7(4):349–382, 1962. https://doi.org/10.1137/1107036
R. Arratia, L. Goldstein, L. Gordon, Two moments suffice for Poisson approximations: the Chen–Stein method, Ann. Probab. 17(1):9–25, 1989. https://doi.org/10.1214/aop/1176991491
A. D. Barbour, L. Holst, S. Janson, Poisson Approximation, Oxford University Press, 1992. https://global.oup.com/academic/product/poisson-approximation-9780198522355

17 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Supply Chain Coordination with Contracts VI: With a Forecast Update, Buy-Back Terms with w₁ − w₂ + λc₂ = λc₁ Give the Retailer λΩ₁(q₁) and a Lower Period-2 Margin w₂ − c₂ < w₁ − c₁Textbook

Motivation

A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.

This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.

Setting

A demand signal $\xi \ge 0$ with density $g$ and distribution function $G$ is observed once before the selling season. Given $\xi$ , demand $D$ has distribution function $F(\cdot\,|\,\xi)$ , continuous and strictly increasing on $[0,\infty)$ . Demand is stochastically increasing in the signal: $F(x\,|\,\xi_h) < F(x\,|\,\xi_l)$ for $\xi_h > \xi_l$ . Expected sales are $S(q\,|\,\xi) = E[\min(q,D)\,|\,\xi]$ . Period 1 is before the signal and period 2 is after it. The retailer's total order is $q_1$ after period 1 and $q_2 \ge q_1$ after period 2. The supplier's unit production cost is $c_i$ in period $i$ , with $c_1 < c_2 < p$ , where $p$ is the retail price. Salvage values and goodwill costs are zero.

The supply chain's period-2 objective is

\Omega_2(q_2\,|\,q_1,\xi) = pS(q_2\,|\,\xi) - c_2 q_2 + c_2 q_1 ,

and $q_2(q_1,\xi)$ maximizes it over $q_2 \ge q_1$ . The supply chain's expected profit is $\Omega_1(q_1) = -c_1 q_1 + E[\Omega_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ .

Under the buy back contract $\{w_1, w_2, b\}$ the retailer pays $w_i$ per unit ordered in period $i$ , and the supplier refunds $b$ per unsold unit. The retailer's period-2 profit is $\pi_2(q_2\,|\,q_1,\xi) = (p-b)S(q_2\,|\,\xi) - (w_2-b)q_2 + w_2 q_1$ , and his period-1 profit is $\pi_1(q_1) = -w_1 q_1 + E[\pi_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ . The supplier's period-2 profit $\Pi_2$ and her period-1 profit $\Pi_1(x\,|\,q_1)$ , as functions of the stock $x$ she holds, are given in the mission's Profits definition.

Formalization targets

Goal: the buy back contract coordinates

For $\lambda \in [0,1]$ with

p - b = \lambda p,\qquad w_2 - b = \lambda c_2,\qquad w_1 - w_2 + \lambda c_2 = \lambda c_1,

the identities

\pi_2(q_2\,|\,q_1,\xi) = \lambda\big(\Omega_2(q_2\,|\,q_1,\xi) - c_2 q_1\big) + w_2 q_1,\qquad \pi_1(q_1) = \lambda\,\Omega_1(q_1)

hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for $\lambda > 0$ ). In addition,

w_2 - c_2 = w_1 - \big(\lambda c_1 + (1-\lambda)c_2\big) < w_1 - c_1 \quad (\lambda < 1).

Milestones

The structure of the period-2 problem, Eqs. (25)–(26): $q_2(\xi)$ solves $F(q_2(\xi)\,|\,\xi) = (p-c_2)/p$ and increases in $\xi$ , and the threshold $\xi(q_1)$ splits the signals into those that trigger a period-2 order and those that do not.
The retailer's period-2 identity (p. 65).
The supplier fills any period-2 order up to $q_2(q_1,\xi)$ , and for $\lambda < 1$ she does not fill a larger one (p. 65).
The retailer's period-1 identity (p. 66).
The first-order condition (27) for $q_1^o$ .
The supplier's period-2 profit increases in her stock below $q_1$ , so she produces at least the period-1 order (p. 66).
The supplier produces exactly the period-1 order (p. 67).
The margin comparison (p. 67).

Significance

The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through $\lambda$ . Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.

These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold $\xi(x)$ .

Difficulty

The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and $\partial \Pi_1(x\,|\,q_1)/\partial x = -c_1 + c_2(1 - G(\xi(x)))$ . The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum $\max(q_1, q_2(\xi))$ has a kink at $\xi = \xi(q_1)$ . The integrand switches between two regimes, and the switch point moves with $q_1$ . The supplier's period-1 profit is not differentiable at $x = q_1$ ; only its right derivative is negative at $q_1^o$ . Turning the page's derivative statements into the global claim that $x = q_1^o$ is her unique optimum needs a monotonicity argument on both sides of $q_1^o$ .

Formalization scope

The conditional law is a measurable family $\xi \mapsto D_\xi$ of probability measures on $\mathbb R$ supported on $[0,\infty)$ , each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on $[0,\infty)$ . The signal has a measurable density $g \ge 0$ with $\int_0^\infty g = 1$ , and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. $0 < c_2 < p$ makes the critical ratio lie in $(0,1)$ . Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).

The optimum $q_2(q_1,\xi)$ is a hypothesis-carried selection maximizing $\Omega_2$ over $q_2 \ge q_1$ . It is never an arbitrary function: a formalization that let $q_2(q_1,\xi)$ be unconstrained would make $\pi_1 = \lambda\Omega_1$ a statement about meaningless orders. The thresholds $\xi(q_1)$ enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over $q_1 \ge 0$ and $q_2 \ge q_1$ . Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).

Three corrections of the print are disclosed in the item notes:

the strict margin inequality fails at $\lambda = 1$ ;
the p. 66 identity for $\Pi_2(x, q_1, q_2, \xi)$ is off by the constant $(1-\lambda)c_2q_1$ ;
"retailer optimal equals chain optimal" needs $\lambda > 0$ in the converse direction.

Contributions are welcome on all milestones. A lemma that differentiates $q \mapsto E[\max_{q_2 \ge q} \Omega_2]$ with a density-driven threshold would be reusable beyond this mission.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. https://doi.org/10.1016/S0927-0507(03)11006-7
K. L. Donohue, Efficient Supply Contracts for Fashion Goods with Forecast Updating and Two Production Modes, Management Science 46(11), 1397–1411, 2000. https://doi.org/10.1287/mnsc.46.11.1397.12088
M. Fisher and A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 87–99, 1996. https://doi.org/10.1287/opre.44.1.87

12 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Supply Chain Coordination with Contracts VII: In the Single-Location Base-Stock Model the Transfers t_I = (1 − λ)h_r, t_B = β_r − λβ Make the Retailer's Cost λc(s_r)Textbook

Motivation

A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.

The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).

Setting

Let $D_r$ denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean $\mu_r=\mathbb E[D_r]$ , distribution function $F_r$ , and density $f_r$ . At inventory level $s\in\mathbb R$ , expected inventory is $I_r(s)=\mathbb E[(s-D_r)^+]$ and expected backorders are $B_r(s)=\mathbb E[(D_r-s)^+]$ , where $x^+=\max(x,0)$ . The section assumes $F_r(0)=0$ and a strictly increasing differentiable $F_r$ on nonnegative levels. These assumptions place the optimum above zero.

The retailer pays holding cost $h_r I_r(s)$ and its own backorder cost $\beta_r B_r(s)$ . The supplier pays a further backorder cost $\beta_s B_r(s)$ . All three cost rates are positive. Thus $c_r(s)=h_r I_r(s)+\beta_r B_r(s)$ and $c_s(s)=\beta_s B_r(s)$ are the firms' costs, while $c(s)=c_r(s)+c_s(s)$ is the channel cost. Write $\beta=\beta_r+\beta_s$ . Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.

The proposed contract pays the retailer $t_I I_r(s)+t_B B_r(s)$ from the supplier, where $t_I$ and $t_B$ are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter $\lambda\in(0,1]$ , the contract sets $t_I=(1-\lambda)h_r$ and $t_B=\beta_r-\lambda\beta$ . The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter $\lambda$ describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.

Formalization targets

The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum $s_r^\circ$ is unique and satisfies

F_r(s_r^\circ)=\frac{\beta}{h_r+\beta};

the uncontracted retailer has its own unique optimum $s_r^*$ with $s_r^*<s_r^\circ$ . Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family ( $t_I\ge0$ , with $t_I>0$ exactly for $\lambda<1$ , and $\{t_B:0<\lambda\le1\}=[-\beta_s,\beta_r)$ ); the decomposition

t_I I_r(y)+t_B B_r(y)=(t_I+t_B)I_r(y)+t_B(\mu_r-y);

and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price $p=h_r+\beta_r$ and wholesale price $w=h_r$ , the newsvendor retailer's profit $pS(q)-wq$ , with expected sales $S(q)=\mathbb E[\min(q,D_r)]$ , equals $-c_r(q)+\beta_r\mu_r$ . The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:

c_r^\lambda(s)=\lambda c(s),\qquad c_s^\lambda(s)=(1-\lambda)c(s) \quad\text{for all }s\in\mathbb R\text{ and }0<\lambda\le1.

Consequently, the retailer's contracted cost has the same unique minimizer $s_r^\circ$ as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in $\lambda$ , which is the page's statement that the retailer's share of the cost increases with $\lambda$ . The result does not prescribe one fixed allocation of cost: each $\lambda$ in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.

Significance

The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to $\beta_r$ , while the channel's stock decision uses $\beta_r+\beta_s$ . Under the contract, the retailer bears the fraction $\lambda$ of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.

The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).

Difficulty

The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as $\lambda c$ would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.

Formalization scope

Lean represents $D_r$ by a probability measure on $\mathbb R$ supported on $[0,\infty)$ , with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on $[0,\infty)$ , equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates $h_r,\beta_r,\beta_s$ are fields of one model, and $I_r,B_r$ are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.

Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that $t_I>0$ for all $\lambda\in(0,1]$ fails at $\lambda=1$ , where $t_I=0$ ; the formal statement asserts $t_I\ge0$ with strict positivity exactly for $\lambda<1$ . The contract range is exactly $0<\lambda\le1$ ; $\lambda=0$ would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.

Selected references

Gérard P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; source used here: author's third draft, January 2003, §6.7. DOI.

12 thms3 active usersReviewed