Missions · Prove2Me

Probability Statistics·Captain: mikedeng1

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality I: P(√n sup(F − F̂ₙ) > λ) ≤ exp(−2λ²) for λ ≥ min(√(log 2/2), 1.0841 n^(−1/6))Research Paper

Motivation

The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every $n$ , not just in the limit.

Timeline.

1933–1944. Kolmogorov and Smirnov introduce the statistics, prove that their laws do not depend on the continuous distribution, and find the limit laws, e.g. $\lim_n P(D_n^->\lambda)=\exp(-2\lambda^2)$ . Smirnov (1944) also gives the exact law of the one-sided statistic and the expansion $P(D_n^->\lambda)=\exp(-2\lambda^2)\bigl(1-\frac{2\lambda}{3\sqrt n}+O(n^{-1})\bigr)$ .
1956. Dvoretzky, Kiefer and Wolfowitz prove $P(D_n^->\lambda)\le C\exp(-2\lambda^2)$ for every $n$ , with an unspecified constant $C$ (Ann. Math. Statist. 27).
1958. Birnbaum and McCarty conjecture that $C=1$ is admissible.
1979–1985. Explicit constants: $C\le306$ (Devroye and Wise), $C\le29$ (Shorack and Wellner), $C\le2\sqrt2$ (Hu).
1990. Massart proves the conjecture under a mild lower bound on $\lambda$ , and deduces the two-sided bound with the optimal constant $2$ (Ann. Probab. 18).

Setting

Let $x_1,\dots,x_n$ ( $n\ge1$ ) be independent, identically distributed real random variables with a continuous distribution function $F$ . The empirical distribution function is

\hat F_n(x)=\frac1n\sum_{i=1}^n\mathbb 1_{(x_i\le x)},

and the centred, normalised empirical process is $Z_n=\sqrt n(\hat F_n-F)$ . The statistics are

D_n^+=\sup_{x\in\mathbb R}Z_n(x),\qquad D_n^-=\sup_{x\in\mathbb R}\bigl(-Z_n(x)\bigr),\qquad D_n=\sup_{x\in\mathbb R}|Z_n(x)|.

In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), $F$ is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter $\lambda$ is written l.

The proof works with Smirnov's point probabilities $p_{\lambda,n}(j)=\lambda\sqrt n\,(j+\lambda\sqrt n)^{j-1}(n-j-\lambda\sqrt n)^{n-j}n^{-n}\binom nj$ , whose sum over $0\le j<n-\lambda\sqrt n$ is $P(D_n^->\lambda)$ , with Csáki's density $f_\lambda(s)=\frac{\lambda}{\sqrt{2\pi}}s^{-3/2}(1-s)^{-1/2}\exp\bigl(-\frac{\lambda^2}{2s(1-s)}\bigr)$ of the first passage of a Brownian bridge at level $\lambda$ , and with the ratio $C_{\lambda,n}=\exp(2\lambda^2)P(D_n^->\lambda)$ .

Formalization targets

Goal: Theorem 1

For every $n\ge1$ and every $\lambda\ge\sqrt{\log(2)/2}\wedge\gamma n^{-1/6}$ , with $\gamma=1.0841$ ,

P(D_n^->\lambda)\le\exp(-2\lambda^2).

Here $\wedge$ is the minimum. The constant $1$ in front of the exponential is the point of the theorem; the threshold on $\lambda$ is the paper's.

Milestones

The milestones follow the proof in the paper's order of attack:

the reduction to the uniform law, and Smirnov's exact formula (2.3);
the identity $\int_0^1f_\lambda=\exp(-2\lambda^2)$ (2.4);
the local comparison of $p_{\lambda,n}(j)$ with $f_\lambda$ : (2.7), Lemma 2, Claims 1–3, and Proposition 1;
the midpoint bound for log-convex integrands (Lemma 3) and the closed forms of Lemma 4;
the nonasymptotic expansion (2.11), the negativity of its right side $\eta_n$ , and with them Theorem 1 for $n\ge39$ , $\lambda\le\sqrt n/2$ ;
Proposition 2 on the slope of $C_{\lambda,n}$ , the crude bounds (2.13)–(2.14), and the finite grid check (2.15) for $n\le38$ .

Companions

The equality in law of $D_n^+$ and $D_n^-$ , Comment 1 ((1.4) whenever $\exp(-2\lambda^2)\le1/2$ ), the reduction $P(D_n>\lambda)\le2P(D_n^->\lambda)$ , and Corollary 1:

P(D_n>\lambda)\le2\exp(-2\lambda^2)\qquad(\lambda>0).

Significance

The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, $1$ and $2$ , which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.

Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified $C$ . The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, $\eta_{39}$ ); turning those into checked certificates is part of the work.

Difficulty

The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison $P(\tau_n=t)\le\frac1nf_\lambda(t-\varepsilon/3)$ is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time $t$ is close to $\varepsilon=\lambda/\sqrt n$ . Controlling that factor uniformly in $j$ while keeping the leading constant exactly $1$ is what forces the delicate constants ( $\theta=0.4833$ , $\beta=0.826$ , $\mu=0.4345$ , $\gamma=1.0841$ ). For small $n$ the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on $\lambda\mapsto C_{\lambda,n}$ plus a finite numerical check over a grid; neither half suffices alone.

Formalization scope

Conventions:

$n\ge1$ ; the sample is indexed by Fin n; $F$ is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.
Probabilities are measures of events in $[0,\infty]$ and are compared with ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in $[-1,1]$ , hence a genuine real supremum.
$p_{\lambda,n}(j)$ uses an integer power at $j-1$ , so that $p_{\lambda,n}(0)=(1-\varepsilon)^n$ . $C_{\lambda,n}$ is defined from the exact formula (2.3); it equals $\exp(2\lambda^2)P(D_n^->\lambda)$ by the (2.3) milestone, so the analytic milestones carry no probability.
Statements that the page gives through derivatives of $C_{\lambda,n}$ (Proposition 2(i), (iii)) are stated as monotonicity and as an increment bound, because $C_{\lambda,n}$ has kinks.

Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of $j$ ), (2.8) (swapped numerators) and Proposition 2(i) (" $\ge0$ " for nonincreasing) are corrected; Claim 2 carries the hypothesis $\varepsilon\le3s'$ , without which the corrected claim is false; Lemma 3 uses strict inequalities $\delta<s<1-\delta$ ; Comment 1 makes the implicit $\lambda>0$ explicit; (2.14) carries Proposition 2's standing range $n\ge2$ , $0<\lambda<\sqrt n$ .

The goal does not mention $p_{\lambda,n}$ , $f_\lambda$ , $C_{\lambda,n}$ , the case split at $n=39$ , or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.

Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on $]0,1[$ ; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.

Selected references

P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Ann. Probab. 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
A. Dvoretzky, J. Kiefer, J. Wolfowitz, Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator, Ann. Math. Statist. 27:642–669, 1956. https://doi.org/10.1214/aoms/1177728174
Z. W. Birnbaum, R. C. McCarty, A distribution-free upper confidence bound for P(Y<X), based on independent samples of X and Y, Ann. Math. Statist. 29:558–562, 1958.
N. V. Smirnov, Approximate laws of distribution of random variables from empirical data, Uspekhi Mat. Nauk 10:179–206, 1944.
E. Csáki, Investigations concerning the empirical distribution function, Magyar Tud. Akad. Mat. Fiz. Oszt. Közl. 23:239–327, 1974; English translation in Selected Transl. Math. Statist. Probab. 15:229–317, 1981.
G. R. Shorack, J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986.

23 thms3 active usersReviewed

Combinatorics Discrete Geometry Linear Optimization·Captain: mikedeng1

The d-Step Conjecture for Polyhedra of Dimension d < 6 1: The Bounded 5-Step Conjecture Holds, Every 5-Polytope with 10 Facets Has Diameter at Most 5, i.e. Δb(5, 10) = 5Research Paper

Motivation

The simplex method and every other edge-following linear programming algorithm moves from vertex to vertex of the feasible region along its edges. The number of steps such an algorithm needs in the worst case is at least the combinatorial diameter of the feasible polyhedron: the largest distance, counted in edges, between two of its vertices. Klee and Walkup introduced the two functions that measure this worst case, $\Delta(d,n)$ for polyhedra and $\Delta_b(d,n)$ for bounded polyhedra of dimension $d$ with $n$ facets, and wrote that $\Delta(d,n)$ "represents, in a sense, the number of iterations required to solve the 'worst' linear program of $n$ inequalities in $d$ variables using the 'best' edge-following algorithm" (Klee and Walkup 1967, p. 54).

The Hirsch conjecture, reported by Dantzig in 1963, asserted $\Delta(d,n)\le n-d$ . Its diagonal cases $\Delta(d,2d)\le d$ and $\Delta_b(d,2d)\le d$ are the general and the bounded $d$ -step conjectures.

Timeline.

1957–1963: W. M. Hirsch's conjecture, reported in Dantzig's Linear Programming and Extensions (1963, pp. 160, 168), with the claim that it holds for $m\le 4$ .
Before 1967: Klee determines $\Delta(3,n)=n-3$ and $\Delta_b(3,n)=\lfloor 2n/3\rfloor-1$ and settles $\Delta_b(d,n)$ for $n\le d+4$ (Canad. J. Math. 16 and the papers cited as [9], [12], [13] by Klee and Walkup, p. 55).
1967: Klee and Walkup (Acta Math. 117) prove $\Delta_b(5,10)=5$ , show that $\Delta_b(d,2d)\le d$ for all $d$ is equivalent to the bounded Hirsch conjecture, and disprove the unbounded conjecture with $\Delta(4,8)=5$ .
2012: Santos disproves the bounded Hirsch conjecture with a 43-dimensional polytope with 86 facets (Ann. Math. 176). The bounded $d$ -step conjecture therefore fails for some $d$ , and the smallest failing $d$ is unknown; it is at least 6.

Setting

A polyhedron in $\mathbb R^d$ is a nonempty set $P=\{x:\langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}$ ; a polytope is a bounded polyhedron. $P$ is a $d$ -polyhedron with $n$ facets when it has nonempty interior and none of the $n$ inequalities is redundant; then the rows are in bijection with the facets, and row $i$ is tight at $v$ exactly when $v$ lies on the $i$ -th facet. The vertices of $P$ are its extreme points. Two vertices $u\ne v$ span an edge when the segment $[u,v]$ is an extreme subset of $P$ . A path of length $l$ is a sequence of $l$ edges $[x_0,x_1],\dots,[x_{l-1},x_l]$ , and $\delta_P(x,y)$ is the least length of a path from $x$ to $y$ . Then

\Delta_b(d,n)=\max\{\delta_P(x,y): P\text{ a }d\text{-polytope with }n\text{ facets},\ x,y\text{ vertices of }P\}.

$P$ is simple when every vertex lies on exactly $d$ facets. A face is $P$ itself or the intersection of $P$ with a supporting hyperplane, never $\emptyset$ ; its dimension is that of its affine hull. A $(k_1,\dots,k_r)$ -path from $x$ to $y$ is a sequence of faces $K_1,\dots,K_r$ with $x\in K_1$ , $y\in K_r$ , $\dim K_i=k_i$ and $K_i\cap K_{i+1}\ne\emptyset$ . A $d$ -dimensional Dantzig figure $(P,x,y)$ is a $d$ -polyhedron $P$ with $2d$ facets and two vertices $x,y$ such that exactly $d$ facets are incident to $x$ and the other $d$ to $y$ . A $d$ -polytope $Q$ has property A when it has between $2d$ and $2d+2$ facets and the following holds: if its facets are split into two classes $\mathfrak X,\mathfrak Y$ of at most $d+1$ facets each, and both sets $X$ , $Y$ of vertices all of whose facets lie in $\mathfrak X$ , respectively $\mathfrak Y$ , are nonempty, then some vertex of $X$ is joined to some vertex of $Y$ by a path of length at most $d$ .

Formalization targets

Goal: 4.3 THEOREM

\Delta_b(5,10)=5.

In two halves: every $5$ -polytope with $10$ facets satisfies $\delta_P(x,y)\le 5$ for all vertices $x,y$ , and some $5$ -polytope with $10$ facets has two vertices with $\delta_P(x,y)>4$ .

Milestones, in the order the proof uses them

2.8 THEOREM (bounded part): $\Delta_b(d,n)$ is attained by two vertices of a simple $d$ -polytope with $n$ facets, and for $n\ge 2d$ by two vertices on no common facet. For $n=2d$ this is a bounded simple Dantzig figure.
3.4 PROPOSITION (a): every simple Dantzig figure admits a $(k_1,1,k_3)$ -path for positive $k_1+1+k_3=d$ .
3.1 PROPOSITION: (a) facial paths in all $d$ -dimensional simple Dantzig figures, (b) facet-avoiding facial paths in simple $d$ -polytopes with $2d+1$ facets, and (c) facet-avoiding $(1,k_1,\dots,k_r)$ -paths in bounded $(d+1)$ -dimensional figures are equivalent.
3.4 PROPOSITION (b): every bounded simple Dantzig figure admits a $(1,k_2,1,k_4)$ -path for positive $1+k_2+1+k_4=d$ .
Remark after 3.4: adjacent terms of a facial path in a simple figure merge into their sum.
Remark after 3.4, p. 68: bounded simple Dantzig figures of dimension $d\ge 2$ admit $(1,d-2,1)$ -paths.
4.1 PROPOSITION: if the middle face $Q$ of a $(1,d-2,1)$ -path $([x,x'],Q,[y',y])$ has property A, then $\delta_P(x,y)\le d$ .
4.2 LEMMA: every simple $3$ -polytope with $6$ , $7$ or $8$ facets has property A.

Significance

The result. By the paper's reductions, $\Delta_b(d,2d)\le d$ for a given $d$ is equivalent to the bounded Hirsch bound $\Delta_b(d',d'+d)\le d$ for every $d'$ . So 4.3 gives $\Delta_b(d,n)\le n-d$ for all $n\le d+5$ , which is the column $n-d=5$ of the paper's Fig. 2. Since Santos's counterexample, the smallest $d$ with $\Delta_b(d,2d)>d$ is a well-defined open number. This theorem was the first to show it is at least $6$ ; later computer-assisted work treated further small cases, including the bounded $6$ -step case (Bremner and Schewe 2011). Santos's construction starts from exactly the reduction to Dantzig figures (the "strong $d$ -step theorem" for spindles) that this paper uses.

Formalizing it. The result has been proved since 1967; no machine-checked proof of $\Delta_b(5,10)=5$ exists. The platform has the Hirsch bound in dimension $\le 3$ (Hirsch.dimension_three_bound, Hirsch.klee_three_dimensional_bound), the Klee–Walkup wedge reduction at the level of inequality descriptions (Hirsch.balanced_hpoly_transfer), products (Hirsch.diamLE_prod) and Santos's counterexample. The mission adds the facial-path calculus of §3 and the property-A argument of §4. Both are reusable in any later formal treatment of small $d$ -step cases.

Difficulty

The obvious approach, a direct case analysis of $5$ -polytopes with $10$ facets, is out of reach: there are far too many combinatorial types, and nothing bounds the search. The paper first reduces to simple polytopes, and the reduction itself (2.8) rests on a perturbation lemma (2.6) whose proof is deferred to a separate paper by Walkup: simplicity must be gained without shrinking any distance. The facial-path results then pass between bounded and unbounded figures through truncation and the wedge (3.1), and a statement about all unbounded $d$ -dimensional figures is what yields one about bounded $(d+1)$ -dimensional ones. Finally the $(d-2)$ -face $Q$ must be shown to have property A. That property fails for some simple polytopes of classes $(4,10)$ and $(5,11)$ (p. 69), so 4.2 depends on the dimension being $3$ and on the facet count being at most $8$ . Its proof uses Euler's relation and Balinski's theorem that the graph of a $3$ -polytope is $3$ -connected (posed on the platform as Balinski61.Connectivity.disjoint_paths_between_vertices).

Formalization scope

Polyhedra are Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d); edges and walks are Hirsch.Adj and Hirsch.Reach from the published Hirsch_model and Hirsch_walk. The conventions are:

" $d$ -polyhedron with $n$ facets" is a facet presentation: nonempty interior and no redundant row. The rows are exactly the facets; a statement over arbitrary inequality systems would count redundant rows as facets and is not the paper's.
$\delta_P(x,y)\le L$ is Hirsch.Reach P L x y, a walk of $L$ steps that may stand still. $\Delta_b(5,10)=5$ is an upper bound for every polytope plus a witness, never a supremum of reals. A version proving only the upper bound, or only the lower bound, is not the goal.
Simple means pointed with exactly $d$ tight rows at every vertex. On a facet presentation this is equivalent to the paper's "exactly $d$ edges at each vertex".
Faces are nonempty sets $\{x\in P:\langle a_i,x\rangle=b_i,\ i\in I\}$ , and dimension is the dimension of the affine span. A Dantzig figure has Fin (2 * d) rows.
Property A is defined for a bounded face $Q$ of dimension $m$ : its facets are the $(m-1)$ -faces of $P$ inside $Q$ , and the path runs in $Q$ . This keeps 4.1, where $Q$ is a $(d-2)$ -face of a polytope in $\mathbb R^d$ , and 4.2, where $Q=P$ , under one notion. Facet counts use Set.encard.
Explicit readings: 2.8's " $\Delta_b$ can be realized as the distance … of a simple polytope" is stated polytope by polytope ( $\delta_P(u,v)\le\delta_{P'}(x,y)$ ). Only the $\Delta_b$ sentences of 2.8 are stated. 3.4's joint hypothesis on $k_1,\dots,k_4$ is split by part. The merging remark carries the needed hypothesis $k_i+k_{i+1}\le d$ . The printed "3.5 implies" on p. 67 is read as 3.4.

The paper cites two inputs without proving them: Lemma 2.6 (Walkup's simple perturbation) and Balinski's theorem. A complete development needs face lattices of H-polyhedra, wedges and truncations, and the planar-graph arguments of 4.2. The face and facial-path layer is reusable for the companion mission on $\Delta(4,8)=5$ and for other diameter problems. Contributions are welcome at every milestone, including proofs of 2.6.

Selected references

V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Mathematica 117 (1967), 53–78. https://doi.org/10.1007/BF02395040
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963.
V. Klee, Diameters of polyhedral graphs, Canadian Journal of Mathematics 16 (1964), 602–614. https://doi.org/10.4153/CJM-1964-058-5
M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific Journal of Mathematics 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176 (2012), 383–412. https://doi.org/10.4007/annals.2012.176.1.7
D. Bremner and L. Schewe, Edge-graph diameter bounds for convex polytopes with few facets, Experimental Mathematics 20 (2011), 229–237. https://doi.org/10.1080/10586458.2011.564966

12 thms3 active usersReviewed

Completed

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

Some Monotonicity Results for Partially Observed Markov Decision Processes: MLR-Monotone Optimal Values and the Myopic Policy as a Lower Bound on the Optimal PolicyResearch Paper

Motivation

A partially observed Markov decision process (POMDP) models a controller that cannot see the state of the system it controls. It sees only noisy observations, and so it acts on a belief: a probability vector over the hidden states. Machine maintenance, medical screening, quality control and search problems all have this form. The dynamic program of a POMDP lives on the simplex of beliefs, a continuum, so computing exact optimal policies is expensive even when the state, action and observation sets are small. Structural results reduce that cost. A value function that is monotone in the belief, or a policy known to dominate a cheap reference policy, shrinks the space a computation must search. Such results also explain the model: they say when one belief is "better" than another.

W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes (Operations Research 35(5):736–743, 1987), provides such results by ordering beliefs with the monotone likelihood ratio (MLR) order instead of first-order stochastic dominance.

Timeline. Smallwood and Sondik (1973) set out the finite POMDP and its piecewise-linear value functions. White (1979, 1980) obtained monotone policies and values for machine replacement, for single-stage problems, and for the completely observed and completely unobserved extremes, all under first-order stochastic dominance. Albright (1979) treated the two-state case, where the usual orders coincide. Whitt (1979, 1982) developed the likelihood-ratio orders and showed that they are preserved by Bayesian updating. Lovejoy (1987) combined these into general monotonicity results for finite POMDPs, and the MLR order has since become the standard tool for structural results in POMDPs.

Setting

Let $S=\{1,\dots,n\}$ (states) and $O=\{1,\dots,m\}$ (observations) carry their natural orders, and let $A$ be a finite, completely ordered action set. For a finite chain $X$ , $\Pi(X)$ is the set of probability vectors on $X$ . For $\pi,\pi'\in\Pi(X)$ , $\pi\ge_s\pi'$ (first-order stochastic dominance) means $\sum_{i\ge q}\pi_i\ge\sum_{i\ge q}\pi'_i$ for every $q$ . $\pi\ge_r\pi'$ (MLR order) means $\pi_i\pi'_{i'}\ge\pi_{i'}\pi'_i$ whenever $i\ge i'$ . For matrices $f,g$ on $X\times Y$ , $f\ge_{tp}g$ means $f(x\vee x',y\vee y')\,g(x\wedge x',y\wedge y')\ge f(x,y)\,g(x',y')$ for all pairs, and $f$ is TP₂ if $f\ge_{tp}f$ .

In each period the decision maker in state $s_t=i$ chooses $a\in A$ and receives the reward $g(i,a)$ . The state moves to $j$ with probability $p^a_{ij}$ (matrix $P^a$ ), and an observation $k$ arrives with probability $r^a_{jk}$ (matrix $R^a$ , with row $r^a(j)\in\Pi(O)$ ), generated by the new state $j$ and the action $a$ . The paper assumes $r^a_{jk}>0$ throughout. The discount factor is $\beta\ge 0$ . From a belief $\pi$ , the observation $k$ has probability $\sigma(k;\pi,a)=\sum_{i,j}\pi_i p^a_{ij}r^a_{jk}$ , and the posterior is the Bayes update $T_j(\pi,a,k)=\sum_i\pi_ip^a_{ij}r^a_{jk}/\sigma(k;\pi,a)$ . With

h(\pi,a,V)=\sum_{i}\pi_i g(i,a)+\beta\sum_{k}\sigma(k;\pi,a)\,V(T(\pi,a,k)),

a finite horizon $N$ with salvage value $g_s$ gives the optimal values $V^*_{N+1}(\pi)=\sum_i\pi_ig_s(i)$ and $V^*_t(\pi)=\max_a h(\pi,a,V^*_{t+1})$ . For $N=\infty$ and $0<\beta<1$ , $V^*$ is the bounded solution of $V^*(\pi)=\max_a h(\pi,a,V^*)$ . The myopic actions are $\alpha(\pi)=\operatorname{argmax}_a\sum_i\pi_ig(i,a)$ .

Formalization targets

Goal: Proposition 2 (myopic lower bound)

Under (a) $g_s$ nondecreasing, (b) $g(\cdot,a)$ nondecreasing, (c) $P^a\ge_{tp}P^{a'}$ for $a\ge a'$ , (d) $r^a(j)\ge_r r^a(j')$ for $j\ge j'$ , (e) $r^a(j)\ge_s r^{a'}(j)$ for $a\ge a'$ , and (f) $r^a_{jk}r^{a'}_{j'k}\ge r^{a'}_{jk}r^a_{j'k}$ for $a\ge a'$ , $j\ge j'$ : for every $t\le N$ (finite horizon), or for the infinite horizon with $0<\beta<1$ , and every $\pi\in\Pi(S)$ ,

\forall\,\delta^*(\pi)\ \exists\,\alpha(\pi)\le\delta^*(\pi),\qquad \forall\,\alpha(\pi)\ \exists\,\delta^*(\pi)\ge\alpha(\pi),

where $\delta^*(\pi)$ ranges over the maximizers of $a\mapsto h(\pi,a,V^*_{t+1})$ (resp. $h(\pi,a,V^*)$ ).

Milestone: Proposition 1 (MLR-monotone values)

Under (a)–(d) with every $P^a$ TP₂: $\pi\ge_r\pi'$ in $\Pi(S)$ implies $V^*_t(\pi)\ge V^*_t(\pi')$ for $t=1,\dots,N+1$ , and, without (a), $V^*(\pi)\ge V^*(\pi')$ for $N=\infty$ .

Supporting milestones

The ordering facts behind both propositions: MLR implies stochastic dominance (§1), Lemma 1.1 (characterization of $\ge_s$ ), Lemma 1.3 (TP₂ prediction preserves $\ge_r$ ), Lemma 1.2 (the Bayes update is MLR-monotone in the observation, the prior and the action), the stochastic monotonicity of $\sigma$ in the belief (proof of Proposition 1) and in the action (Lemma 2.3), the comparison of $h$ -increments with myopic increments (proof of Proposition 2), and Lemma 2.2 (dominated increments order maximizer sets).

Significance

The result. Proposition 2 makes the myopic policy, which solves a one-stage problem, a lower bound on an optimal policy for every belief and every period. In a search over policies, actions below $\alpha(\pi)$ can be discarded. When $g$ also has isotone differences, $\alpha$ is nondecreasing, and the optimal policy is bounded below by a monotone function that is easy to compute. Proposition 1 gives MLR-monotone value functions, the input to many later structural results for POMDPs. Lemma 1.2 records the fact behind it: Bayesian updating respects the MLR order, while first-order stochastic dominance does not survive conditioning.

Formalizing it. These results are proved on paper. This mission produces machine-checked proofs, together with a reusable finite-POMDP layer (belief update, observation probabilities, Bellman operator, finite- and infinite-horizon values) and a library of the stochastic orders on finite chains. One statement in the paper is wrong: the printed "only if" direction of Lemma 1.2(1) is false. The mission states only the direction that is true and used.

Difficulty

The obvious induction on $t$ for Proposition 1 needs $k\mapsto V(T(\pi,a,k))$ to be nondecreasing and $\sigma(\pi,a)$ to increase with $\pi$ . Both need a belief order that conditioning preserves. Under first-order stochastic dominance the posterior is not monotone in the prior, and the paper's counterexample (p. 740) shows that the induction then fails. The MLR order repairs this, but proving that the prediction step preserves it (Lemma 1.3) requires a total-positivity composition argument (Karlin–Rinott, Theorem 2.4) on product lattices. For Proposition 2 the difficulty is to compare continuation values across actions: the observation distribution and the posterior both change with the action, and two separate orderings (Lemma 2.3 and Lemma 1.2(3)) must be combined before the maximizer comparison applies. The infinite-horizon parts additionally need the Bellman fixed point characterized well enough to pass monotonicity to the limit.

Formalization scope

Everything is finite, so all probabilities and expectations are finite sums and no measure theory is involved. States, observations and actions are finite nonempty types with a LinearOrder (any finite chain is isomorphic to $\{1,\dots,n\}$ ). $\Pi(X)$ is Mathlib's stdSimplex ℝ X. The orders $\ge_s,\ge_r,\ge_{tp}$ are plain relations (StochGE, MLRGE, TPGE) with the larger argument first, and every statement assumes simplex membership explicitly. The standing assumptions (stochastic rows of $P^a$ and $R^a$ , $r^a_{jk}>0$ , $\beta\ge0$ ) are fields of the structure POMDP. $V^*_t$ is computed by recursion (3) counted in steps to go, Vstar gs N t = valueToGo gs (N+1-t). The infinite-horizon $V^*$ is any function bounded on $\Pi(S)$ that solves the Bellman equation there. For $0<\beta<1$ such a function exists and is unique on $\Pi(S)$ , by contraction. The equivalence between recursion (3) and the optimum over history-dependent strategies is cited by the paper from the literature and is not part of this mission. Maximizer sets (argmaxSet) carry the "for all $\delta^*$ / there exists $\alpha$ " quantifiers. Both halves of each part of Proposition 2 are $\forall\exists$ statements.

The goal is not to be read with $V^*_{t+1}$ or $V^*$ replaced by an arbitrary, or an arbitrary nondecreasing, value function. That reading would reduce Proposition 2 to Lemma 2.2 plus a hypothesis. The goal quantifies only over the value functions of recursion (3) and over bounded Bellman solutions.

A complete development needs finite total-positivity composition (Mathlib's four functions theorem is the natural starting point), Abel summation for Lemma 1.1, and a contraction argument for the infinite horizon. The order library and the finite POMDP layer are reusable beyond this paper. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1.3.

Selected references

W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes, Operations Research 35(5):736–743, 1987. https://doi.org/10.1287/opre.35.5.736
R. D. Smallwood and E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
W. Whitt, A Note on the Influence of the Sample on the Posterior Distribution, Journal of the American Statistical Association 74:424–426, 1979.
W. Whitt, Multivariate Monotone Likelihood Ratio and Uniform Conditional Stochastic Order, Journal of Applied Probability 19:695–701, 1982.
S. Karlin and Y. Rinott, Classes of Orderings of Measures and Related Correlation Inequalities. I. Multivariate Totally Positive Distributions, Journal of Multivariate Analysis 10(4):467–498, 1980. https://doi.org/10.1016/0047-259X(80)90065-2
C. White, Optimal Control-limit Strategies for a Partially Observed Replacement Problem, International Journal of Systems Science 10:321–331, 1979 (the machine-replacement model of §5).
S. C. Albright, Structural Results for Partially Observable Markov Decision Processes, Operations Research 27(5):1041–1053, 1979. https://doi.org/10.1287/opre.27.5.1041

16 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Job Matching, Coalition Formation, and Gross Substitutes 1: Under Gross Substitutes the Salary-Adjustment Process Reaches a Discrete Core Allocation in Finitely Many RoundsResearch Paper

Motivation

Labor markets match workers to firms, and the terms of each match (the salary) are negotiated along with the match itself. A firm's output depends on the whole team it hires, so a firm cares about sets of workers, not individual workers one at a time. Kelso and Crawford (1982) asked when such a market has a stable outcome, the core, in which no firm and group of workers can agree on terms that all of them prefer, and when a simple decentralized auction finds one.

Their answer is the gross-substitutes condition: raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. Under it, an ascending process in which firms make offers and workers reject all but their favorite reaches a core allocation. This condition became the standard hypothesis for the existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti 1999), it is the hypothesis behind matching with contracts (Hatfield and Milgrom 2005), and the process is the ancestor of ascending auction designs.

Timeline.

1962: Gale and Shapley, deferred acceptance for one-to-one and many-to-one matching without money.
1971: Shapley and Shubik, the assignment game: one-to-one matching with transferable utility; the core is nonempty and is the set of solutions of a dual linear program.
1981: Crawford and Knoer, a salary-adjustment process for one-to-one matching with money, converging to the core.
1982: Kelso and Crawford, many-to-one matching with money and production complementarities; existence of the core under gross substitutes via the salary-adjustment process (Theorem 1, the target of this mission).

Setting

There are finitely many workers $i \in W$ and firms $j \in F$ , with at least one firm. Worker $i$ 's utility of working for firm $j$ at salary $s$ is $u^i(j; s)$ , strictly increasing and continuous in $s$ . Firm $j$ 's gross product from hiring the set $C \subseteq W$ is $y^j(C)$ , and its profit at the salary vector $s^j = (s_{1j},\dots,s_{mj})$ is

\pi^j(C; s^j) = y^j(C) - \sum_{i \in C} s_{ij}.

$M^j(s^j)$ is the set of profit-maximizing $C$ . Each pair has a starting salary $\sigma_{ij}$ . The assumptions (p. 1486) are (MP) $y^j(C \cup \{i\}) - y^j(C) - \sigma_{ij} \ge 0$ for $i \notin C$ ; (NFL) $y^j(\emptyset) = 0$ ; and (GS): if $C \in M^j(s^j)$ and $\tilde s^j \ge s^j$ , some $\tilde C \in M^j(\tilde s^j)$ contains $\{i \in C : \tilde s_{ij} = s_{ij}\}$ .

In the discrete market with unit $\delta > 0$ , firm $j$ may pay worker $i$ only $\sigma_{ij} + k\delta$ , $k = 0, 1, 2, \dots$ . An allocation sends each worker $i$ to a firm $f(i)$ at a salary $s_{if(i)}$ ; it is individually rational (D1) if $s_{if(i)} \ge \sigma_{if(i)}$ and every firm's profit is nonnegative. It is a (discrete) core allocation (D3) if it is individually rational, pays permitted salaries, and no firm $j$ , set $C$ and permitted salaries $r^j$ satisfy $u^i(j; r_{ij}) > u^i(f(i); s_{if(i)})$ for all $i \in C$ and $\pi^j(C; r^j) > \pi^j(C^j; s^j)$ .

The salary-adjustment process (pp. 1488–1489), verbatim:

R1. Firms begin facing a set of permitted salaries $s_{ij}(0) = \sigma_{ij}$ . Permitted salaries at round $t$ , $s_{ij}(t)$ , remain constant, except as noted below. In round zero, each firm makes offers to all workers; this is costless by (MP).

R2. On each round, each firm makes offers to the members of one of its favorite sets of workers, given the schedule of permitted salaries $s^j(t) \equiv [s_{1j}(t), \dots, s_{mj}(t)]$ . That is, firm $j$ makes offers to the members of $C^j[s^j(t)]$ , where $C^j[s^j(t)]$ maximizes $\pi^j[C; s^j(t)]$ . Firms may break ties between sets of workers however they like, with the following exception: Any offer made by firm $j$ in round $t - 1$ that was not rejected must be repeated in round $t$ . By (GS), the firm sacrifices no profits in doing this, since (by R4) other workers' permitted salaries cannot have fallen, and the salary of a worker who did not reject an offer remains constant.

R3. Each worker who receives one or more offers rejects all but his or her favorite (taking salaries into account), which he or she tentatively accepts. Workers may break ties at any time however they like.

R4. Offers not rejected in previous periods remain in force. If worker $i$ rejected an offer from firm $j$ in round $t - 1$ , $s_{ij}(t) = s_{ij}(t - 1) + 1$ ; otherwise $s_{ij}(t) = s_{ij}(t - 1)$ . Firms continue to make offers to their favorite sets of workers, taking into account their permitted salaries.

R5. The process stops when no rejections are issued in some period. Workers then accept the offers that remain in force from the firms they have not rejected.

Formalization targets

Goal: Theorem 1 (p. 1489)

"The salary-adjustment process R1–R5 converges in finite time to a discrete core allocation in the discrete market for which it is defined." Formally, under the assumptions above:

\Big(\exists \text{ a run}\Big)\ \wedge\ \forall \rho \text{ run}:\ \Big(\exists T:\ \rho \text{ issues no rejections in round } T\Big)\ \wedge\ \Big(\forall T \text{ such rounds},\ \text{outcome}_\rho(T) \text{ is a discrete core allocation}\Big).

Milestones, in the paper's order

R2 is well defined: a run exists (each firm has a favorite set containing its unrejected offers).
Lemma 1: every worker has at least one offer in every period.
Lemma 2: after finitely many rounds every worker has exactly one offer and the process stops.
Lemma 3: the allocation at a stopping round is individually rational.
Lemma 4: the allocation at a stopping round is a discrete core allocation.

Significance

Theorem 1 gives the existence of a core allocation in every discrete market satisfying (MP), (NFL) and (GS), with no convexity of production and arbitrary complementarity within the limits of (GS). It is the step from which the paper derives the existence of a strict core allocation of the continuous market (Theorem 2, by letting the unit shrink), and with additional no-ties assumptions the firm-optimality of the process's outcome (Theorem 4) and the comparative statics of entry and exit (Theorem 5).

The result is proved in the paper and has been reproved in more general settings; it has no machine-checked proof known to us. Nothing of this paper was on Prove2Me before this series. Related platform work, credited but not reused: the Gale–Shapley deferred-acceptance development (GS62CollegeAdmissions.*, proved), the no-money ancestor of this process; and the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core the process approximates when production is additively separable. Neither states anything about this process. This mission is mission 1 of a series of seven on the paper: 2 (strict core of the continuous market), 3 (one-sided coalition formation), 4 (firm-optimality), 5 (comparative statics), 6 (gross substitutes and decreasing returns), 7 (a market without a core). Each states its own model.

Difficulty

The process is quantified over all tie-breakings, so no single computation settles it; the statements are about every sequence of rounds consistent with R1–R5. Two points carry the content. First, R2 imposes a constraint that may not be satisfiable: a firm must repeat its unrejected offers and choose a profit-maximizing set. Without (GS) no such set need exist and the process is not defined. Second, the core property at the stopping round compares the outcome with coalitions using salaries the process never reached; the comparison is with salaries on the discrete grid only, and it is false if coalitions may use salaries below $\sigma_{ij}$ or off the grid. Termination is not automatic either: the process may continue after a round without rejections, salaries are real numbers, and no bound on the number of rounds is given.

Formalization scope

Lean representation, in namespace KelsoCrawford.Process:

Market W F carries u, y, σ; workers and firms are finite types, with [Nonempty F] (the paper's $n \ge 1$ ; with no firms and some worker no run exists).
Allocation assigns every worker to a firm (no unemployment, as in the paper's $f$ ).
(GS) is GrossSubstitutesOn (M.y j) (M.gridVectors δ j) for each firm: the discrete (GS), since the paper notes that a discrete market may satisfy (GS) while its continuous version does not.
The core is D3 with permitted salaries M.grid δ $= \{\sigma_{ij} + k\delta : k \in \mathbb N\}$ .
A Run records salaries, offers and tentative choices per round; IsRun is R1–R4, Stopped is R5's "no rejections", outcome is R5's allocation.

Explicit readings of the paper's phrases:

"converges in finite time" = every run has a round without rejections; no bound on that round is claimed;
"to a discrete core allocation" = at every round without rejections, the allocation read off is in the discrete core;
the unit $1$ of R4 is a parameter $\delta > 0$ (same theorem in rescaled units);
$\sigma_{ij}$ is data; its defining relation $u^i(j;\sigma_{ij}) = u^i(0;0)$ is not assumed (a more general statement).

The existence of a run is part of the goal: without it, statements about all runs would be vacuous. Fixing a tie-breaking rule would turn the statements into claims about a single run and is ruled out; so are the strict core D2 (false here because of ties at the grid) and an integer grid below $\sigma_{ij}$ (false for improving coalitions). Proofs of the milestones and reusable infrastructure for ascending processes are welcome.

Selected references

A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1913320
D. Gale and L. S. Shapley, College admissions and the stability of marriage, American Mathematical Monthly 69(1), 1962, 9–15. https://doi.org/10.2307/2312726
L. S. Shapley and M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
F. Gul and E. Stacchetti, Walrasian equilibrium with gross substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531
J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466

8 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·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

Completed

Operations Research Optimization·Captain: mikedeng1

The Fritz John Necessary Optimality Conditions in the Presence of Equality and Inequality Constraints: Every Minimizer of a C¹ Program Admits Multipliers (ū₀, ū, v̄) ≠ 0 with ū ≥ 0Research Paper

Motivation

For problems with inequality constraints only, F. John (1948) showed that every minimizer admits nonnegative multipliers $(\bar u_0, \bar u_1, \dots, \bar u_m) \ne 0$ , one of which belongs to the objective. The Kuhn–Tucker conditions (1951) are the stronger statement in which the objective's multiplier can be taken equal to one; they need a constraint qualification.

Problems arising in practice mix equalities and inequalities. Fritz John's theorem does not cover them, and the obvious reduction, writing each equality $h_j(x) = 0$ as the two inequalities $h_j(x) \le 0$ and $-h_j(x) \le 0$ , destroys the content of the conditions: every feasible point then satisfies them with $\bar u_0 = 0$ . O. L. Mangasarian and S. Fromovitz (1967) proved a version of Fritz John's conditions that treats equalities directly and stays informative, and from it derived the constraint qualification now known as the Mangasarian–Fromovitz constraint qualification (MFCQ). MFCQ is the standard regularity assumption in the convergence theory of sequential quadratic programming, interior-point and augmented-Lagrangian methods, and in the stability theory of parametric programs.

Timeline.

1939, W. Karush (master's thesis) and 1951, H. W. Kuhn and A. W. Tucker: multiplier conditions with $\bar u_0 = 1$ for inequality constraints, under a constraint qualification.
1948, F. John: the multiplier rule with $\bar u_0 \ge 0$ for inequality constraints, no qualification needed.
1967, Mangasarian and Fromovitz (this paper): the multiplier rule for equalities and inequalities together, and the qualification (3.4)–(3.6).

Setting

Let $E^n$ be $n$ -dimensional Euclidean space, and let $\theta, g_1, \dots, g_m, h_1, \dots, h_k : E^n \to \mathbb R$ be functions with continuous first partial derivatives on $E^n$ . The program is

\text{minimize } \theta(x) \quad \text{subject to} \quad g_i(x) \le 0,\ i \in M = \{1,\dots,m\}, \qquad h_j(x) = 0,\ j \in K = \{1,\dots,k\}. \tag{1.1}

The feasible set is $S = \{x \in E^n : g_i(x) \le 0,\ i \in M,\ h_j(x) = 0,\ j \in K\}$ . A point $\bar x$ is a solution of (1.1) if $\bar x \in S$ and $\theta(\bar x) \le \theta(x)$ for all $x \in S$ . The active set at $\bar x$ is $\bar M = \{i \in M : g_i(\bar x) = 0\}$ . The gradient of $f$ at $\bar x$ is $\nabla f(\bar x)$ , and $y'z$ denotes the inner product.

The generalized Fritz John conditions hold at $\bar x$ if there are $\bar u = (\bar u_0, \bar u_1, \dots, \bar u_m)$ and $\bar v = (\bar v_1, \dots, \bar v_k)$ with

\bar u_0 \nabla\theta(\bar x) + \sum_{i=1}^m \bar u_i \nabla g_i(\bar x) + \sum_{j=1}^k \bar v_j \nabla h_j(\bar x) = 0, \qquad \sum_{i=1}^m \bar u_i g_i(\bar x) = 0, \qquad \bar u \ge 0, \qquad (\bar u, \bar v) \ne 0 .

The Kuhn–Tucker conditions are the same system with $\bar u_0 = 1$ and no nontriviality requirement.

Formalization targets

Goal: the generalized Fritz John necessary conditions (p. 41)

If $\bar x$ is a solution of (1.1), then there exist $\bar u \in E^{m+1}$ and $\bar v \in E^k$ with

\bar u_0 \nabla\theta(\bar x) + \sum_{i=1}^m \bar u_i \nabla g_i(\bar x) + \sum_{j=1}^k \bar v_j \nabla h_j(\bar x) = 0, \quad \sum_{i=1}^m \bar u_i g_i(\bar x) = 0, \quad \bar u \ge 0, \quad (\bar u, \bar v) \ne 0. \tag{2.9–2.12}

No regularity of the constraints is assumed. The nontriviality requirement covers $\bar u_0$ , the $\bar u_i$ and the $\bar v_j$ together.

Milestones

Motzkin's transposition theorem (p. 39): for real matrices $A, B, C$ with $A$ nonempty, exactly one of $y'A < 0,\ y'B \le 0,\ y'C = 0$ and $Az_1 + Bz_2 + Cz_3 = 0,\ z_1 \ge 0,\ z_1 \ne 0,\ z_2 \ge 0$ is solvable.
Lemma 1 (pp. 39–40): if $f_i(\bar x) = 0$ , $h_j(\bar x) = 0$ at some $\bar x$ in an open set $D$ , no $x \in D$ has $f_i(x) < 0$ for all $i$ and $h_j(x) = 0$ for all $j$ , and the $\nabla h_j(\bar x)$ are linearly independent, then no $y$ has $y'\nabla f_i(\bar x) < 0$ and $y'\nabla h_j(\bar x) = 0$ .
Lemma 2 (p. 40): under the same assumptions, without independence, there are $\bar r \ge 0$ and $\bar s$ , not both zero, with $\sum \bar r_i \nabla f_i(\bar x) + \sum \bar s_j \nabla h_j(\bar x) = 0$ .
$D$ is open (p. 41): $D = \{x : g_i(x) < 0,\ i \in M \setminus \bar M\}$ is open.
The reduction (pp. 41–42): at a solution $\bar x$ of (1.1), $\bar x \in D$ and the system $\theta(x) - \theta(\bar x) < 0$ , $g_i(x) < 0$ ( $i \in \bar M$ ), $h_j(x) = 0$ has no solution in $D$ .

Companion results

Corollary (p. 43): the generalized Fritz John conditions hold at any feasible point satisfying (2.27) or (2.28).
The generalized constraint qualification (pp. 43–44): at a solution, $\bar y'\nabla g_i(\bar x) < 0$ ( $i \in \bar M$ ), $\bar y'\nabla h_j(\bar x) = 0$ and independent $\nabla h_j(\bar x)$ imply the Kuhn–Tucker conditions.
The splitting remark (p. 38): after splitting equalities, every feasible point satisfies Fritz John's original conditions.

Significance

The theorem is a multiplier rule for smooth programs with both kinds of constraints and no assumption on the constraints. It has two direct consequences in the paper. First, it yields MFCQ, the condition (3.4)–(3.6) under which the Kuhn–Tucker conditions hold at every solution. MFCQ is weaker than linear independence of all active gradients (LICQ), and it is equivalent to boundedness of the Kuhn–Tucker multiplier set (Gauvin, 1977). Second, the corollary identifies feasible non-minimizers at which the conditions hold anyway.

The result is classical and its proof is in every nonlinear-programming textbook. Mathlib has the equality-constrained Lagrange multiplier rule for a local extremum (IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt) and the implicit function theorem, and Prove2Me has a formalized Fritz John theorem for inequality constraints only. To our knowledge no machine-checked proof of the mixed equality–inequality Fritz John rule, of MFCQ, or of Motzkin's transposition theorem in this form exists. The formalization would provide the standard multiplier rule and qualification on which a formal theory of nonlinear programming builds.

Difficulty

With inequalities alone, John's theorem follows from the observation that if $\bar x$ is a minimizer, no direction $y$ strictly decreases $\theta$ and every active $g_i$ to first order; Motzkin's (or Gordan's) theorem then produces the multipliers. With equalities the first step fails: a direction with $y'\nabla h_j(\bar x) = 0$ is tangent to the equality manifold but generally leaves it, so a first-order descent direction does not yield a feasible point with smaller objective. Lemma 1 is precisely the claim that it does when the $\nabla h_j(\bar x)$ are independent, and it needs a curve inside $\{h = 0\}$ along which the strict inequalities persist: the implicit function theorem, applied on an open set, with care that the curve stays in $D$ . The linearly dependent case must be handled separately, and it is the only place the multipliers $\bar v$ can be nonzero with $\bar u = 0$ .

Formalization scope

$E^n$ is EuclideanSpace ℝ (Fin n), the inner product $y'z$ is inner ℝ y z, and $\nabla f(\bar x)$ is Mathlib's gradient f xbar. "Continuous first partial derivatives on $E^n$ ", the standing assumption of §1, is ContDiff ℝ 1 (equivalent in finite dimension) and is a hypothesis of the goal, the corollary and the constraint qualification; Lemma 1 and Lemma 2 use ContDiffOn ℝ 1 · D on an open set $D$ , as on the page. Indices $i \in M$ and $j \in K$ are Fin m and Fin k, 0-based; $m = 0$ and $k = 0$ are allowed. The multiplier vector $\bar u \in E^{m+1}$ is split into u0 : ℝ and u : Fin m → ℝ, and $(\bar u, \bar v) \ne 0$ is "u0 ≠ 0, or some u i ≠ 0, or some v j ≠ 0". A solution of (1.1) is a global minimizer over $S$ , as the proof on p. 42 uses. In Motzkin's theorem a matrix is the family of its columns, and "either … or …, but never both" is Xor. In Lemma 2, "the assumptions of Lemma 1" exclude the proviso (2.5) of linear independence, which the proof of Lemma 2 treats separately.

The goal does not assume linear independence of the $\nabla h_j(\bar x)$ , does not mention $D$ or Lemma 1, and requires $(\bar u, \bar v) \ne 0$ with $\bar u_0$ included; a formalization that drops $\bar u_0$ from the nontriviality condition is false at $m = k = 0$ , and one that requires $\bar u_0 \ne 0$ is the Kuhn–Tucker statement, false without a qualification.

A complete development needs Motzkin's (or Gordan's) theorem of the alternative, which is reusable well beyond this mission, and the implicit function theorem on open sets in Euclidean space with a $C^1$ curve argument. Proofs of any milestone are welcome, as is a proof of the goal by another route.

Selected references

O. L. Mangasarian and S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, J. Math. Anal. Appl. 17 (1967), 37–47. https://doi.org/10.1016/0022-247X(67)90163-1
F. John, Extremum problems with inequalities as subsidiary conditions, in Studies and Essays Presented to R. Courant on his 60th Birthday, Interscience, New York, 1948, 187–204.
H. W. Kuhn and A. W. Tucker, Nonlinear programming, Proc. Second Berkeley Symposium on Mathematical Statistics and Probability, University of California Press, 1951, 481–492.
J. Gauvin, A necessary and sufficient regularity condition to have bounded multipliers in nonconvex programming, Math. Programming 12 (1977), 136–138. https://doi.org/10.1007/BF01593777
O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969; reprinted SIAM Classics in Applied Mathematics 10, 1994. https://doi.org/10.1137/1.9781611971255

7 thms3 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

The Data-Driven Newsvendor Problem: New Bounds and Insights I: The SAA Order Is ε-Optimal with Probability at Least 1 − 2exp(−Nε²min(b,h)/((18 + 8ε)(b + h)))Research Paper

Motivation

The newsvendor problem is the basic model of stocking under uncertain demand: an order quantity is fixed before a random demand is observed, and every unit short or left over is penalized. Its solution is a quantile of the demand distribution. In practice that distribution is unknown and only a sample of past demands is available. The standard remedy, sample average approximation (SAA), replaces the expectation by the empirical average over the sample and orders the corresponding sample quantile. The practical question is how many observations make the SAA order nearly as good as the true optimum, without assuming anything about the demand distribution.

Levi, Roundy and Shmoys (Math. Oper. Res. 32(4), 2007) gave the first distribution-free answer, using Hoeffding's inequality. Levi, Perakis and Uichanco (Oper. Res. 63(6), 2015) improved it with Bernstein's inequality. The improvement matters most when the service level is high, which is the typical case in inventory practice. This mission formalizes that improved bound, Theorem 2 of the 2015 paper.

Setting

A retailer orders $q\in\mathbb R$ units before a real demand $D$ with law $\mu$ and cdf $F(q)=\Pr(D\le q)$ is realized. Unmet demand costs $b>0$ per unit (underage cost) and unsold stock costs $h>0$ per unit (overage cost). The expected cost is

C(q)=\mathbb E\big[b(D-q)^+ + h(q-D)^+\big],

which is finite when $\mathbb E|D|<\infty$ . The critical quantile is $q^*=\inf\{q:F(q)\ge b/(b+h)\}$ , and it minimizes $C$ .

An order $q$ is $\epsilon$ -optimal when its relative regret $(C(q)-C(q^*))/C(q^*)$ is at most $\epsilon$ , i.e. $C(q)\le(1+\epsilon)C(q^*)$ . The set of such orders is $S_\epsilon$ . The function $C$ is convex with one-sided derivatives

\partial_+C(q)=-b+(b+h)F(q),\qquad \partial_-C(q)=-b+(b+h)\Pr(D<q).

The LRS interval is

S^{LRS}_\epsilon=\Big\{q:\partial_-C(q)\le\tfrac\epsilon3\min(b,h)\ \text{and}\ \partial_+C(q)\ge-\tfrac\epsilon3\min(b,h)\Big\}.

Given an i.i.d. sample $D^1,\dots,D^N$ from $\mu$ , the empirical cdf is $\hat F_N(q)=\frac1N\sum_k\mathbf 1[D^k\le q]$ , and the SAA solution is the sample quantile

\hat Q_N=\inf\{q:\hat F_N(q)\ge b/(b+h)\}.

It is a random variable through the sample.

Formalization targets

Goal: Theorem 2 (improved LRS bound)

For every demand law with $\mathbb E|D|<\infty$ , every $N\ge1$ and every $0<\epsilon\le1$ ,

\Pr\big(\hat Q_N\notin S_\epsilon\big)\le 2\exp\Big(-\frac{N\epsilon^2}{18+8\epsilon}\cdot\frac{\min\{b,h\}}{b+h}\Big).

Milestones, in the order of the paper's proof

(§2, p. 7) $C$ is convex, and its one-sided derivatives are the two formulas above.
(Theorem EC.1) Bernstein's inequality for i.i.d. bounded variables: $\Pr\big(\frac1N\sum_iX^i-\mathbb E X^1\ge t\big)\le\exp\big(-Nt^2/(2\sigma^2+2tc/3)\big)$ .
(Proposition EC.1) For every $\gamma>0$ , $\Pr\big(\partial_-C(\hat Q_N)\le\gamma\text{ and }\partial_+C(\hat Q_N)\ge-\gamma\big)\ge1-2\exp\big(-3N\gamma^2/(6bh+8\gamma(b+h))\big)$ .
(Display (3)) For $0<\epsilon\le1$ , $S^{LRS}_\epsilon\subseteq S_\epsilon$ .

Significance

The earlier LRS bound has the exponent $-\frac29N\epsilon^2\big(\min\{b,h\}/(b+h)\big)^2$ . Theorem 2 replaces the square by the first power. When the critical ratio $b/(b+h)$ approaches $1$ (high service levels), $\min\{b,h\}/(b+h)$ is small, and the required sample size drops accordingly. Raising the service level from 95% to 99% multiplies the sample size the LRS bound requires by 25, but the sample size Theorem 2 requires only by 5 (p. 9). The bound holds for every demand distribution, with no density, continuity or support assumption.

The milestones are reusable on their own. One is the one-sided derivative formula for the expected newsvendor cost. Another is Bernstein's inequality for i.i.d. bounded variables, which Mathlib does not have; it has Hoeffding's inequality. The third is a distribution-free concentration statement for sample quantiles. The result is proved in the paper. To our knowledge none of these statements is formalized; this mission produces machine-checked versions.

Difficulty

A Hoeffding-type argument yields only the squared dependence on $\min\{b,h\}/(b+h)$ . The improvement needs the variance $F(1-F)$ of the indicator $\mathbf 1[D\le q]$ , which is small near extreme quantiles. Bernstein's inequality applies at a fixed point $q$ . The sample quantile, however, is random, and $F$ can jump. The event that $\hat Q_N$ falls left of the target quantile therefore has to be reduced to deviations of $\hat F_N$ at deterministic points, with care at atoms of $D$ , where $\partial_+C$ and $\partial_-C$ differ. The final step from the derivatives to the relative regret requires convexity of $C$ and a lower bound on $C(q^*)$ that holds for every distribution.

Formalization scope

Model. The demand law is a probability measure μ on ℝ, with no sign restriction (the page's $q\ge0$ plays no role here). $F$ is Mathlib's cdf μ, and $\Pr(D<q)$ is μ (Set.Iio q). The realized cost is the published InventoryControl.newsboyLoss h b q d, and $C$ is a Bochner integral. Every statement that evaluates $C$ assumes Integrable id μ ( $\mathbb E|D|<\infty$ ). This is the standing assumption under which $C$ is an expectation. It also rules out the trivializing formalization in which a non-integrable cost integrates to $0$ and every order is $\epsilon$ -optimal.
Quantiles. $q^*$ and $\hat Q_N$ are infima (sInf) of sets that are nonempty and bounded below under the hypotheses, never argmins or choice functions. The sample is x : Fin N → ℝ under the product measure Measure.pi (fun _ => μ), with $N\ge1$ ; the indices are 0-based.
Probabilities. "With probability at least $1-p$ " is stated as an upper bound $p$ on the outer measure of the failure set.
$\epsilon$ -optimality is the multiplicative form $C(q)\le(1+\epsilon)C(q^*)$ , which avoids dividing by $C(q^*)$ .
Pinned hypotheses.
- The goal and milestone 4 are stated for $0<\epsilon\le1$ . The paper says "for any $\epsilon>0$ ", but both statements fail for large $\epsilon$ . Take $b=h=1$ , $N=1$ and $D\in\{0,M\}$ with $\Pr(D=M)=0.005$ . Then $q^*=0$ , and the order $M$ has relative regret $198$ , yet at $\epsilon=150$ the bound promises a failure probability of about $1.9\cdot10^{-4}$ .
- In Theorem EC.1, the centred bound $|X^1-\mathbb EX^1|\le c$ is added to the printed $|X^1|\le c$ . It holds for the indicators to which the paper applies the inequality.

A complete development needs the following:

the one-sided derivatives of a convex integral functional;
Bernstein's inequality for product measures;
the quantile-to-cdf reduction for the empirical and the true cdf;
the convexity estimate behind (3).

The Bernstein inequality and the sample-quantile concentration are useful beyond this mission. Contributions to any milestone are welcome.

Selected references

R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6), 2015. https://doi.org/10.1287/opre.2015.1422. Statements are cited from the authors' accepted manuscript (MIT DSpace), body pp. 7–9 and e-companion pp. ec5–ec6.
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), 2007. https://doi.org/10.1287/moor.1070.0272
S. N. Bernstein, Theory of Probability, Moscow, 1927.
P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.

7 thms3 active usersReviewed

Completed

Linear algebra Number Theory·Captain: mikedeng1

Factoring Polynomials with Rational Coefficients I: A Reduced Lattice Basis Satisfies |b_j|² ≤ 2^{n−1}·max|x_i|² for Any t Linearly Independent Lattice VectorsResearch Paper

Motivation

A lattice in $\mathbb R^n$ is the set of integer combinations of $n$ linearly independent vectors. Many problems in algorithmic number theory, cryptography and integer programming reduce to finding a short nonzero vector of a lattice, or a few short independent ones. Finding the shortest vector exactly is hard, but in 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász introduced a notion of reduced basis that can be computed in polynomial time and whose vectors are provably short up to a factor depending only on the dimension (Lenstra, Lenstra, Lovász 1982). Their paper used it to factor polynomials in $\mathbb Q[X]$ in polynomial time; the same reduction (now called LLL) became a standard tool for simultaneous Diophantine approximation (the paper's own (1.39)), for H. W. Lenstra's integer programming algorithm in fixed dimension (Lenstra 1983), and for cryptanalysis of knapsack and RSA variants.

What makes a reduced basis useful is a set of explicit inequalities proved in Section 1 of the paper, before any algorithm appears. They compare the lengths of the basis vectors with the lattice determinant and with arbitrary lattice vectors, with constants such as $2^{n-1}$ and $2^{n(n-1)/4}$ . This mission formalizes those inequalities.

Setting

Let $n\ge1$ and let $(\,\cdot\,,\,\cdot\,)$ and $|\cdot|$ be the ordinary inner product and Euclidean length on $\mathbb R^n$ . Vectors $b_1,\ldots,b_n\in\mathbb R^n$ form a basis for a lattice $L$ when they are linearly independent over $\mathbb R$ and $L=\sum_{i=1}^n\mathbb Z b_i$ . The determinant of $L$ is

d(L)=|\det(b_1,b_2,\ldots,b_n)|,

the $b_i$ written as columns (1.1). The Gram–Schmidt vectors $b_i^*$ and coefficients $\mu_{ij}$ ( $1\le j<i\le n$ ) are defined inductively by

b_i^*=b_i-\sum_{j=1}^{i-1}\mu_{ij}b_j^*,\qquad \mu_{ij}=\frac{(b_i,b_j^*)}{(b_j^*,b_j^*)}\qquad(1.2),(1.3);

the $b_i^*$ are pairwise orthogonal and not normalised. The basis is reduced if

|\mu_{ij}|\le\tfrac12\quad(1\le j<i\le n)\qquad(1.4)

and

|b_i^*+\mu_{i\,i-1}b_{i-1}^*|^2\ge\tfrac34|b_{i-1}^*|^2\quad(1<i\le n)\qquad(1.5).

The first condition is a size condition on the coefficients; the second (the Lovász condition) says that swapping $b_{i-1}$ and $b_i$ would not shrink the $(i-1)$ -th Gram–Schmidt length by more than the factor $\frac34$ (pp. 516–517).

Formalization targets

Goal: Proposition (1.12), p. 518

Let $b_1,\ldots,b_n$ be a reduced basis for $L$ and let $x_1,\ldots,x_t\in L$ be linearly independent. Then

|b_j|^2\le 2^{n-1}\cdot\max\{|x_1|^2,|x_2|^2,\ldots,|x_t|^2\}\qquad (j=1,\ldots,t).

The statement quantifies over every reduced basis and every independent family of lattice vectors. Its case $t=1$ is Proposition (1.11).

Milestones

In the order of the paper's proofs (pp. 517–518):

$|b_i^*|^2\ge(\frac34-\mu_{i\,i-1}^2)|b_{i-1}^*|^2\ge\frac12|b_{i-1}^*|^2$ for $1<i\le n$ (proof of (1.6));
$|b_j^*|^2\le 2^{i-j}|b_i^*|^2$ for $1\le j\le i\le n$ (proof of (1.6));
$|b_i|^2=|b_i^*|^2+\sum_{j<i}\mu_{ij}^2|b_j^*|^2\le 2^{i-1}|b_i^*|^2$ (proof of (1.6));
(1.7): $|b_j|^2\le 2^{i-1}|b_i^*|^2$ for $1\le j\le i\le n$ ;
if $x=\sum_l r_lb_l$ with $r_l\in\mathbb Z$ and $i$ is the largest index with $r_i\ne0$ , then $|x|^2\ge|b_i^*|^2$ (proof of (1.11), reused as (1.13));
(1.11): $|b_1|^2\le 2^{n-1}|x|^2$ for every nonzero $x\in L$ .

Companion statements

The rest of Proposition (1.6) and the remark after it: $d(L)=\prod_i|b_i^*|$ (proof of (1.6)); (1.8) $d(L)\le\prod_i|b_i|\le 2^{n(n-1)/4}d(L)$ ; (1.9) $|b_1|\le 2^{(n-1)/4}d(L)^{1/n}$ ; and Hadamard's inequality (1.10) $d(L)\le\prod_i|b_i|$ for an arbitrary basis.

Significance

Proposition (1.11) says the first vector of a reduced basis approximates a shortest nonzero lattice vector within the factor $2^{(n-1)/2}$ ; (1.12) extends this to all of the first $t$ basis vectors, so that $|b_j|^2$ is within $2^{n-1}$ of the $j$ -th successive minimum of $L$ (the remark after (1.12)). These are the guarantees on which the paper's factoring algorithm rests: in Section 2 a reduced basis of a lattice built from a $p$ -adic factor yields, through (1.11) and (1.12), an irreducible factor of the polynomial. Inequality (1.9) gives simultaneous Diophantine approximation in polynomial time, and (1.8) bounds how far a reduced basis is from orthogonal.

All of these results are proved in the paper and in textbooks. Verified LLL developments exist in Isabelle/HOL (Bottesch et al., A verified LLL algorithm, AFP 2018), but Mathlib, the library this platform builds on, has neither the reduced-basis predicate of (1.4)–(1.5) nor these bounds. A Lean development produces a reusable definition layer for lattices with the paper's conventions, Gram–Schmidt length estimates, and Hadamard's inequality in determinant form, which the other missions of this series (the reduction algorithm and the factoring application) build on.

Difficulty

The estimates on Gram–Schmidt lengths are single-variable inductions once (1.5) has been rewritten using orthogonality. The step that does not follow from a direct estimate is (1.12): the vectors $x_1,\ldots,x_t$ are arbitrary independent lattice vectors with no relation to the basis order, so a bound on each $|x_j|$ by a single Gram–Schmidt length does not by itself say which $b_j$ it controls. A naive argument that pairs $x_j$ with $b_j$ fails. The determinant statements need the link between Mathlib's matrix determinant of the columns $b_i$ and the Gram–Schmidt lengths, which Mathlib does not state in this form.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (abbreviated Vec n), a basis is a family b : Fin n → Vec n, the lattice is Submodule.span ℤ (Set.range b), and "basis for $L$ " is linear independence over $\mathbb R$ together with equality of that span with $L$ . The vectors $b_i^*$ are Mathlib's unnormalised InnerProductSpace.gramSchmidt, and $\mu_{ij}$ is (1.3) verbatim. $d(L)$ is the absolute determinant of the column matrix; it is not defined as $\prod|b_i^*|$ , which would make the first companion statement true by definition. Section 1 begins "Let $n$ be a positive integer", so every statement carries $0<n$ .

Lean indices run from $0$ to $n-1$ : the paper's $b_i$ is Lean's b ⟨i-1, _⟩, an exponent $2^{i-1}$ at paper index $i$ is $2^i$ at Lean index $i$ , and the pair $(i-1,i)$ of (1.5) is $(i,i+1)$ . Exponents $n(n-1)/4$ , $(n-1)/4$ and $1/n$ are real powers. The maximum in (1.12) is a Finset.sup' over the nonempty index set of the $x_j$ , and the statement is empty at $t=0$ , as on the page.

Every statement about a reduced basis also assumes linear independence: the reducedness inequalities alone hold for degenerate dependent families, whose Gram–Schmidt vectors vanish, and would make the targets trivial. The goal does not assume (1.7), (1.13) or any ordering of the $x_j$ ; those appear only as milestones. Proofs of the milestones and companions, and general lemmas on Gram–Schmidt and determinants that would belong in Mathlib, are welcome.

Selected references

A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261, 515–534, 1982. https://doi.org/10.1007/BF01457454
H. W. Lenstra, Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4), 538–548, 1983. https://doi.org/10.1287/moor.8.4.538
R. Bottesch, J. Divasón, M. Haslbeck, S. Joosten, R. Thiemann, A. Yamada, A verified LLL algorithm, Archive of Formal Proofs, 2018. https://www.isa-afp.org/entries/LLL_Basis_Reduction.html

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Functional Analysis Probability·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 Probability+1·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 Probability 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

Combinatorics Operations Research·Captain: mikedeng1

Sequencing Jobs to Minimize Total Weighted Completion Time Subject to Precedence Constraints 1: The Series-Parallel Algorithm Returns an Optimal SequenceResearch Paper

Motivation

Sequencing jobs on one machine to minimize the total weighted completion time $\sum_j w_jC_j$ is one of the basic problems of scheduling theory. Without precedence constraints it is solved by Smith's ratio rule (1956): sequence the jobs in nonincreasing order of $w_j/p_j$ . With arbitrary precedence constraints the problem is NP-hard, as Lawler shows in the same report. Between these two extremes lies the class of series parallel precedence constraints, which covers chains, rooted trees and their nested combinations, and which is exactly the class that can be assembled from single jobs by "all of this before all of that" and "this independently of that".

Lawler's report (IRIA-LABORIA No. 205, 1976; Annals of Discrete Mathematics 2, 1978) gives an $O(n\log n)$ algorithm for this class, once a decomposition of the constraints is known. It is the standard reference for the polynomial case of $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ .

Timeline.

1956, Smith: the ratio rule, no precedence constraints.
1964, Conway, Maxwell and Miller: parallel chains with unit weights.
1971–1973, Baker, Horn, Adolphson and Hu: rooted trees, in $O(n\log n)$ .
1975, Sidney: job modules and $\rho$ -maximal initial sets, for arbitrary precedence constraints, without an efficient method to find them.
1976/1978, Lawler: series parallel constraints in $O(n\log n)$ ; NP-completeness for arbitrary constraints.

Setting

There are $n$ jobs, forming a finite set $N$ , to be processed by a single machine. Precedence constraints are given by an acyclic digraph $G=(N,A)$ : job $i$ must precede job $j$ if there is a directed path from $i$ to $j$ . Job $j$ has a processing time $p_j>0$ and a real weight $w_j$ (of either sign). A feasible sequence lists every job once and never puts a job before one that must precede it. The machine starts at time $0$ without idle time, so the completion time $C_j$ of job $j$ is the sum of the processing times of $j$ and the jobs before it. The cost of a sequence is $\sum_{j\in N} w_jC_j$ , and an optimal sequence is a feasible sequence of minimum cost.

A transitive series parallel digraph is built from single nodes by series composition $(N_1\cup N_2,\ A_1\cup A_2\cup N_1\times N_2)$ and parallel composition $(N_1\cup N_2,\ A_1\cup A_2)$ of digraphs on disjoint node sets. $G$ is series parallel if its transitive closure is transitive series parallel. A decomposition tree records such a construction: its leaves are the jobs, and its internal nodes are marked $S$ (left son before right son) or $P$ .

Sidney's theory works with three notions. A nonempty $M\subseteq N$ is a module if every job outside $M$ must precede all of $M$ , must follow all of $M$ , or is unconstrained with respect to all of $M$ . A subset $I\subseteq M$ is an initial set of $M$ if it contains, with each of its jobs, every job of $M$ that must precede it. With

\rho(I)=\frac{\sum_{j\in I}w_j}{\sum_{j\in I}p_j},

an initial set $I^*$ is $\rho$ -maximal if $\rho(I^*)\ge\rho(I)$ for every initial set $I$ of $M$ .

A composite job is a sequence of jobs treated as one job whose weight and processing time are the sums over its jobs. Lawler's algorithm works bottom-up on the decomposition tree and represents an optimal sequence for each node's module as a set of composite jobs: a leaf gives its job, a $P$ -node the union of its sons' sets, and an $S$ -node the output of the series procedure (Steps 1–3, p. 11), which absorbs elements of $M_1$ and $M_2$ into a composite job $k=(i,k)$ or $k=(k,j)$ until the ratios separate.

Formalization targets

Goal: the algorithm is correct

For a decomposition tree $T$ of $G$ and any run of the algorithm on $T$ producing the set $F$ of composite jobs, every arrangement $L$ of $F$ in nonincreasing ratio order, with each composite job expanded into its sequence, is an optimal sequence:

\operatorname{flatten}(L)\ \text{is an optimal sequence for } N .

Ties, both in the algorithm's choice of minimal and maximal elements and in the final sort, may be broken arbitrarily.

Milestones

Subtrees are modules (p. 7): the leaves of any subtree of a decomposition tree form a module.
Theorem 1 (p. 7): an optimal sequence for a module extends to an optimal sequence for $N$ in which the module's jobs keep their order.
Existence (Definition 3, p. 8): every module has a $\rho$ -maximal initial set.
Theorem 2 (p. 8): for a $\rho$ -maximal initial set $I$ of a module $M$ , some optimal sequence for $N$ runs $I$ consecutively, before all other jobs of $M$ .
Ratio order (p. 10): composite jobs in nonincreasing ratio order cost no more than in any other order.
Parallel composition (p. 10): the union of two representing sets represents the parallel composition.
Series composition, separated ratios (p. 10): if every ratio in $M_1$ exceeds every ratio in $M_2$ , the union represents the series composition.
Series composition, Steps 1–3 (pp. 10–11): the output of the series procedure represents the series composition.

A companion theorem states that the algorithm always has a run.

Significance

The result places $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ with series parallel constraints in polynomial time. Sidney's module and $\rho$ -maximal initial set machinery, which it uses, is the decomposition later used in approximation algorithms for general precedence constraints; Theorems 1 and 2 hold for arbitrary acyclic constraints.

The algorithm and Sidney's theorems are proved in the literature; none of them has a machine-checked proof. The report proves Theorems 1 and 2 by citation to Sidney's 25 lemmas and argues the algorithm's correctness informally in a few paragraphs. A formal development supplies the missing invariants (what exactly is preserved at each node of the tree) and checks that arbitrary tie-breaking is harmless.

Difficulty

The algorithm's correctness rests on an invariant the page states only in passing: that composite jobs behave as single jobs. Read literally, "nonincreasing ratio order is optimal for $M_1$ and for $M_2$ " does not imply the same for their parallel composition. A composite job of two unconstrained jobs can be optimal on its own module yet blocks a better interleaving once another module is added. The invariant that makes the induction go through is that every composite job is a $\rho$ -maximal initial set of itself, and the series procedure must be shown to preserve it while merging. The second difficulty is Theorems 1 and 2 themselves: exchange arguments over sequences of a whole module, with real weights of either sign, under arbitrary acyclic constraints.

Formalization scope

Jobs have a type $\iota$ with decidable equality; $N$ is a Finset ι; the arcs are a relation G : ι → ι → Prop with endpoints in $N$ , acyclic in the sense that no job reaches itself by a path, and "must precede" is Relation.TransGen G. Processing times are positive on $N$ , weights are arbitrary reals. The objective and optimality are the published SingleMachinePrec.Biclique.WeightedCompletion; feasibility is checked against the arcs of $G$ , which for a sequence listing each job once is the same as against its paths. "Optimal for $M$ " uses the job set $M$ .

The decomposition tree is an inductive SPTree with leaves, $S$ -nodes and $P$ -nodes. It is tied to $G$ by three hypotheses: its leaves are distinct, they are exactly $N$ , and on $N$ the transitive closure of $G$ equals the arc relation of the transitive series parallel digraph the tree builds. Composite jobs are lists of jobs, sets of composite jobs are lists of lists, and their ratio is $\sum w/\sum p$ over the list. The algorithm is an inductive relation (Run, SeriesMerge, SeriesLoop), so every tie-breaking is a run. The dummies of ratio $\pm\infty$ in Step 1 become vacuous conditions on empty sets.

Committed conventions and disclosed deviations:

Lean evaluates $0/0=0$ , so $\rho(\emptyset)=0$ ; $\rho$ -maximality compares nonempty initial sets only and requires the maximal set to be nonempty, and composite jobs are nonempty.
Modules use the disjunction of (4.1)–(4.3); for acyclic $G$ and nonempty $M$ this is the page's "exactly one".
"Represents an optimal sequence" includes the composite invariant (every nonempty proper prefix has ratio at most the whole). Without it the parallel and series milestones are false.
In the parallel and series milestones, $M_1$ , $M_2$ and $M_1\cup M_2$ are assumed to be modules, as on the page (the sons of a node of the decomposition tree and the node itself). Without this, a path through a job outside $M_1\cup M_2$ could constrain two of its jobs while feasibility on $M_1\cup M_2$ does not see it, and the series milestone would be false.
The introduction's "nondecreasing order of the ratios" (p. 1) is a slip for the nonincreasing order used in §5; the formalization uses nonincreasing.

The goal assumes nothing about modules, Theorem 2 or subtrees, only the tree, the data and a run, and the companion theorem shows that runs exist, so the goal is neither trivial nor vacuous.

Needed infrastructure: exchange arguments for $\sum w_jC_j$ on lists, restriction of sequences to modules, induction over decomposition trees. Theorems 1 and 2 and the ratio-order lemma are reusable in any $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ development. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

E. L. Lawler, Sequencing jobs to minimize total weighted completion time subject to precedence constraints, IRIA-LABORIA Rapport de Recherche No. 205, December 1976. https://hal.science/hal-04716371v1. Journal version: Annals of Discrete Mathematics 2 (1978), 75–90. https://doi.org/10.1016/S0167-5060(08)70323-6
J. B. Sidney, Decomposition algorithms for single-machine sequencing with precedence relations and deferral costs, Operations Research 23 (1975), 283–298. https://doi.org/10.1287/opre.23.2.283
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956), 59–66. https://doi.org/10.1002/nav.3800030106
J. Valdes, R. E. Tarjan, E. L. Lawler, The recognition of series parallel digraphs, SIAM Journal on Computing 11 (1982), 298–313. https://doi.org/10.1137/0211023

11 thms3 active usersReviewed

Completed

Dynamical Systems Operations Research Probability+1·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

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 2: The 3-Partition Flow Shop on Three Machines Has a Preemptive Schedule of Finish Time 2tB Iff a 3-Partition ExistsResearch Paper

Motivation

A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in which a task may be interrupted and resumed later on the same machine. For two machines the optimal finish time is computed by Johnson's rule, and preemption does not help. The paper shows that with three machines the preemptive problem is already NP-complete, and its second result, Theorem 2, strengthens this to NP-completeness in the strong sense: the problem stays hard even when the task times are written in unary.

Strong NP-completeness matters because it rules out a pseudo-polynomial algorithm, one whose running time is polynomial in the sum of the task lengths. The preemptive three-machine flow shop ( $F3\mid pmtn\mid C_{\max}$ in later notation) is a standard entry in complexity classifications of scheduling problems, and Theorem 2 is the reference for its status. The paper notes that Garey and Johnson obtained a proof independently.

Timeline. Johnson (1954) solved the two-machine flow shop. Garey, Johnson and Sethi (1976) proved the non-preemptive three-machine flow shop NP-complete in the strong sense. Gonzalez and Sahni (1978) treated the preemptive case: Theorem 1 (ordinary NP-completeness via Partition) and Theorem 2 (strong NP-completeness via 3-Partition), the subject of this mission.

Setting

A flow shop has $m\ge 1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ runs on $P_j$ and takes time $t_{j,i}\ge 0$ ; zero times are allowed. For each job, task $j\ge 2$ can begin only after task $j-1$ has been completed, and schedules start at time $0$ .

A preemptive schedule is given, as in the paper's footnote on p. 40, by finitely many pieces $(s,f)$ per task: the task is processed on its processor during $[s,f)$ . Pieces have $0\le s<f$ , pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$ , and a piece of task $j'$ starts only after every piece of every earlier task $j<j'$ of the same job has ended. A task has no preemption when it is processed in at most one piece; a non-preemptive schedule has no preemption anywhere. The completion time of job $i$ is $f_i(S)$ , the end of its last piece, and the finish time is $FT(S)=\max_i f_i(S)$ .

3-Partition. An instance $C=(a_1,\dots,a_s,B)$ , $s=3t$ , consists of a positive integer $B$ and nonnegative integers $a_i$ with $\sum_i a_i=tB$ and $B/4<a_i<B/2$ . It has a 3-partition if $\{1,\dots,s\}$ splits into $t$ disjoint sets $L_1,\dots,L_t$ , each of three elements with $\sum_{j\in L_k}a_j=B$ .

The instance FS. From $C$ the proof of Lemma 4 builds a three-processor flow shop with $s+t+2$ jobs:

jobs $1,\dots,s$ : times $(a_i,\,0,\,a_i)$ on $(P_1,P_2,P_3)$ ;
job $s+1$ : $(0,\,2B,\,B)$ ;
jobs $s+i+1$ , $1\le i\le t-2$ : $(B,\,2B,\,B)$ ;
job $s+t$ : $(B,\,2B,\,0)$ ;
job $s+t+1$ : $(0,\,0,\,B)$ ;
job $s+t+2$ : $(B,\,0,\,0)$ .

Each processor carries total work exactly $2tB$ , and the threshold is $\tau=2tB$ .

Formalization targets

Goal: Theorem 2, as Lemma 4's equivalence

For every 3-Partition instance $C$ with $t\ge 2$ ,

\exists\,S \text{ preemptive schedule of } FS:\ FT(S)\le 2tB \quad\Longleftrightarrow\quad C \text{ has a 3-partition},

and every task time of $FS$ satisfies $t_{j,i}\le 2B$ . The second clause records that the instance's numbers are bounded by those of $C$ , the reduction's contribution to "the problem size being measured as the sum of the length of the tasks".

Milestones

Lemma 3 (p. 40). For a flow shop with $m\ge 1$ processors, every preemptive schedule $S$ can be replaced by a schedule $S'$ with no preemptions on $P_1$ and on $P_m$ and $FT(S')=FT(S)$ .
Lemma 4(a) (p. 41). If $C$ has a 3-partition, $FS$ has a non-preemptive schedule with $FT\le 2tB$ .
First step of Lemma 4(b) (pp. 41–42). In every preemptive schedule of $FS$ with $FT\le 2tB$ , the jobs among $1,\dots,s$ whose $P_1$ task is completed by time $2B$ have $\sum t_{1,i}=B$ .
Lemma 4(b) (pp. 41–42). If $C$ has no 3-partition, every preemptive schedule of $FS$ has $FT>2tB$ .

Significance

The result. Theorem 2 places the preemptive three-machine flow shop among the strongly NP-hard scheduling problems, so no algorithm polynomial in the number of jobs and the total processing time exists unless P = NP. It also shows that allowing preemption, which makes several single-stage problems (such as $P\mid pmtn\mid C_{\max}$ ) easy, does not help for three-stage flow shops. Lemma 3, that preemptions on the first and last machines can be removed without changing the finish time, holds for any number of machines and is a reusable structural fact about flow-shop schedules.

Formalizing it. The result is proved on paper, and its proof of the "only if" direction is an informal busy-processor argument repeated window by window. As far as is known, no part of it has a machine-checked proof. A formal development has to make the interval accounting rigorous: why each processor is busy throughout $[0,2tB]$ , why exactly $B$ units of element jobs end on $P_1$ by $2B$ , and how the argument restarts on $[2B,2tB]$ . Lemma 3 needs an exchange argument on piece representations. Both are new for the platform.

Difficulty

The direction "3-partition $\Rightarrow$ schedule" is a direct construction. The hard direction is the converse. Preemption lets any task be split across many intervals, so the usual non-preemptive arguments, which reason about the order in which whole tasks run, do not apply directly. The paper's argument that the window $[0,2B]$ must contain exactly three element jobs of total $B$ on $P_1$ depends on every processor being continuously busy, and turning "otherwise there is idle time" into a precise statement requires a careful account of which jobs are available to each processor at each moment. The induction on windows is then not a literal restriction of the schedule to a smaller instance, because pieces may cross the boundary at $2B$ .

Formalization scope

Times are real numbers; the 3-Partition data are natural numbers cast to $\mathbb R$ . Processors are Fin m with $P_1=$ 0; in $FS$ , $P_1,P_2,P_3$ are 0, 1, 2.
The 3-Partition instance is the published ResourceScheduling.Chain.ThreePartition (0-based indices, t parts, b $=B$ , Valid, HasSolution), whose definition is the paper's p. 37 problem.
Preemptive schedules are finite sets of pieces per task; precedence is required between every pair of tasks $j<j'$ of a job, so a zero task occupies no time and does not break the job's order. Finish time is a maximum over jobs with baseline $0$ , never an unattained supremum.
"No preemptions on $P_j$ " means at most one piece per task on $P_j$ .
Not formalized: "NP-complete", the reduction symbol $\propto$ , "the problem size being measured as the sum of the length of the tasks", and Lemma 2 (membership in NP). The goal states the equivalence Lemma 4 proves for the constructed instance, plus the bound $t_{j,i}\le 2B$ on its task times.
Added hypothesis: $t\ge 2$ . For $t<2$ the paper's job indices $s+1$ and $s+t$ coincide with conflicting times, so the construction is undefined there.
The first step of Lemma 4(b) is read as: the sum of $t_{1,i}$ over element jobs whose $P_1$ task has completed by time $2B$ equals $B$ .
A trivializing formalization is ruled out: the schedules quantified over are all preemptive schedules of the specific instance $FS(C)$ , the threshold $2tB$ is explicit, and the validity conditions $B/4<a_i<B/2$ are kept, so the schedule side cannot match the weaker "partition into $t$ groups of sum $B$ ".

Contributions welcome: the interval-accounting lemmas (busy processors, work available before a time), Lemma 3's exchange argument, and the schedule of Figure 2.

Selected references

T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1):36–52, 1978. https://doi.org/10.1287/opre.26.1.36
M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, "Strong" NP-Completeness Results: Motivation, Examples, and Implications, Journal of the ACM 25(3):499–508, 1978. https://doi.org/10.1145/322077.322090

8 thms3 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

On the Generalized “Birth-and-Death” Process 1: For Rates λ(t), μ(t) ≥ 0 the Population Size Is Geometric with a Modified Zero Term, ξ_t = 1 − e^{−ρ}/W, η_t = 1 − 1/WResearch Paper

Motivation

Population models often allow each individual to produce a new individual or die at rates that change over time. Seasonal conditions, exposure to an epidemic, and changing conditions in a laboratory population all make a constant rate a restrictive assumption. In Kendall's 1948 paper, the question is how the entire distribution of the population size evolves when the per-individual birth and death rates are prescribed functions of time. The distribution matters even when its mean is known: a population can have a stable expected size while still having a substantial chance of extinction. Kendall presents the varying-rate model as a generalization of the constant-rate process discussed by Feller in 1939 (Kendall 1948, §1).

This mission concerns Kendall's solution for a population descended from one ancestor. It includes the explicit distribution, the forward equations that connect it to the birth and death model, and the formulas for its mean, variance, and chance of eventual extinction. The paper has no numbered theorems; its results are identified here by its equation numbers and printed pages.

Setting

At time $t\ge0$ , let $n_t$ be the number of individuals. Each individual gives birth at instantaneous rate $\lambda(t)$ and dies at rate $\mu(t)$ , so a population of size $n$ moves to $n+1$ at rate $n\lambda(t)$ and to $n-1$ at rate $n\mu(t)$ . Both rates are nonnegative. The initial state is $n_0=1$ . Write $P_n(t)$ for the probability that $n_t=n$ . The forward equations in §2, (2)–(4), p. 2 are

P_0'(t)=\mu(t)P_1(t),\qquad P_n'(t)=(n+1)\mu(t)P_{n+1}(t)+(n-1)\lambda(t)P_{n-1}(t) -n(\lambda(t)+\mu(t))P_n(t)\quad(n\ge1).

The formula for $P_0'$ reflects that a population already at zero cannot reproduce. The $n-1$ term vanishes at $n=1$ , as it must. The model is expressed through these real-valued probability functions; it does not require a sample-space construction of a stochastic process.

Define the integrated rate difference $\rho(t)$ and the function $W(t)$ by §2, (10a)–(11), p. 4:

\rho(t)=\int_0^t(\mu(\tau)-\lambda(\tau))\,d\tau,\qquad W(t)=e^{-\rho(t)}\left(1+\int_0^t e^{\rho(\tau)}\mu(\tau)\,d\tau\right).

Set $\xi_t=1-e^{-\rho(t)}/W(t)$ and $\eta_t=1-1/W(t)$ . Kendall's modified-zero geometric law is $P_0(t)=\xi_t$ and $P_n(t)=(1-\xi_t)(1-\eta_t)\eta_t^{n-1}$ for $n\ge1$ . The zero state has its own mass; the positive states form a geometric tail. For the nonnegative rates in this mission, $W(t)\ge1$ and $0\le\eta_t<1$ on $t\ge0$ , so the displayed formulas have their ordinary probabilistic meaning.

Formalization targets

The geometric transient law

The goal is the full claim of §2, (8), (10a)–(12), pp. 3–4: the explicit $P_n(t)$ starts from one ancestor, is nonnegative and sums to one for every $t\ge0$ , and satisfies the forward equations above. In symbols, the distribution part is

P_0(t)=\xi_t,\qquad P_n(t)=(1-\xi_t)(1-\eta_t)\eta_t^{n-1}\ (n\ge1),\qquad \sum_{n=0}^{\infty}P_n(t)=1.

The milestones record the paper's intermediate statements in reading order: the rational generating function $\phi(z,t)$ in (9); the pair of equations for $\xi$ and $\eta$ obtained from the generating-function equation (6); the equations for $U=1-\xi$ and $V=1-\eta$ ; the differential equation and integral representation of $W$ ; the alternate formulas (10b)–(10c); and the explicit expressions (12). Each is a statement made in the source, with the page and equation displayed beside its milestone.

Extinction and moments

The companion target from §3, (18)–(19), p. 6 writes $J(t)=\int_0^t e^{\rho(\tau)}\mu(\tau)\,d\tau$ and states

P_0(t)=\frac{J(t)}{1+J(t)},\qquad P_0(t)\longrightarrow1\ \Longleftrightarrow\ J(t)\longrightarrow+\infty.

When $J(t)$ has finite limit $I$ , the limiting extinction chance is $I/(1+I)$ . Companion statements also retain the mean $\bar n_t=e^{-\rho(t)}$ , all three expressions for the variance in (14c), the criterion that extinction has zero chance exactly when $\mu$ vanishes identically, and the necessary divergence of $\int_0^\infty\mu$ for almost-sure extinction (Kendall 1948, pp. 4, 6–7).

Significance

The geometric law supplies every finite-time population probability from the rate functions. Its zero mass yields an extinction probability without taking limits of an unspecified process, while its first two moments quantify expected growth and fluctuations. The extinction criterion distinguishes a population that dies out with probability one from one that retains a positive chance of survival even when its eventual mean behavior is simple. The variance formulas give later sections of Kendall's paper a way to compare rate schedules with the same expected population (§§3, 6).

The result was proved in the 1948 paper. The work here is to state its model and conclusions precisely in Lean, preserving the initial condition, normalization, boundary state, and time-dependent rate conventions. The current files are theorem statements with proof placeholders; a successful build checks their syntax and types, not the mathematical proofs. Once proved, the definitions and the moment and extinction statements can also support formal work on time-dependent branching and population models.

Difficulty

Knowing the expected population is insufficient to determine the distribution. The forward equation for each $P_n$ couples it to both neighboring states, producing an infinite system. A direct finite truncation would change the birth rate at its upper boundary and would therefore no longer be Kendall's model. The zero state also behaves differently from positive states: a purely geometric law on all $n\ge0$ does not capture its mass. The generating function has a rational form, but its time dependence must still agree with the forward system for every state and with a normalized probability law. The extinction statement adds an improper integral, whose finite and divergent regimes require distinct limits.

Formalization scope

Lean represents $\lambda,\mu:\mathbb R\to\mathbb R$ as continuous functions that are nonnegative for $t\ge0$ . The paper calls the rates specified functions and assumes their nonnegativity; global continuity is an explicit convenience for the two-sided derivatives and interval integrals. Only nonnegative time appears in the probabilistic statements. The oriented intervalIntegral from zero to $t$ represents every finite integral. HasDerivAt expresses each derivative, and HasSum expresses both normalization and the moment and generating-function series. The law lives on natural-number states, with $P_0$ handled separately. The coefficient at state $n=1$ is the real number $n-1$ , not an implicit extension to a negative state.

The positivity of $W$ on nonnegative time must follow from the rates. The definitions are total Lean real functions, so a result that relies on a division states the hypotheses that keep its denominator nonzero. The limit $J(t)\to+\infty$ expresses divergence of the paper's improper integral. No uniqueness of solutions to the forward equations is included, because the cited passage does not establish that claim. The goal requires the explicit law to solve the forward equations and to be a probability law; merely expanding its generating function would leave the population model unformalized. Contributions that prove the formulas, establish the required positivity and convergence facts, or develop reusable lemmas for time-dependent linear birth and death equations all fit the scope.

Selected references

D. G. Kendall, On the generalized “birth-and-death” process, Annals of Mathematical Statistics 19(1), 1–15, 1948. DOI: 10.1214/aoms/1177730285.

8 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 1: The Spanning-Tree Interchange Tour ψ* Is a Minimal Cost TourResearch Paper

Motivation

The traveling salesman problem is NP-hard in general, so special cost structures under which it can be solved exactly in polynomial time are of lasting interest in combinatorial optimization and scheduling. One of the earliest and most cited such cases comes from sequencing on a machine whose condition is described by a single real number: a furnace temperature, a knife setting, a fill level. Each job must start at a prescribed state and leaves the machine in another, and changing the state between consecutive jobs costs money or time. Finding the cheapest cyclic order of the jobs is a traveling salesman problem with asymmetric costs.

P. C. Gilmore and R. E. Gomory solved this problem exactly in 1964 (Oper. Res. 12(5), 655–679) with an algorithm of $O(N^2)$ simple steps. Their construction became the standard example of a solvable TSP case: it is the starting point of the survey literature on polynomially solvable TSPs (Gilmore, Lawler and Shmoys 1985; Burkard, Deineko, van Dal, van der Veen and Woeginger 1998), and it appears in the no-wait flow shop literature, where two-machine no-wait scheduling reduces to exactly this cost structure.

Setting

There are $N$ jobs $J_1,\dots,J_N$ . Job $i$ must be started when the state of the machine is $A_i$ and leaves the machine in state $B_i$ ; the jobs are numbered so that $j>i$ implies $B_j\ge B_i$ . Two cost densities $f,g:\mathbb R\to\mathbb R$ satisfy $f(x)+g(x)\ge0$ : raising the state through $x$ costs $f(x)$ per unit, lowering it costs $g(x)$ per unit. The changeover cost of having job $j$ follow job $i$ is

c_{ij}=\begin{cases}\int_{B_i}^{A_j}f(x)\,dx & \text{if } A_j\ge B_i,\\ \int_{A_j}^{B_i}g(x)\,dx & \text{if } B_i>A_j.\end{cases}

A permutation $\psi$ of the jobs assigns to each job $i$ its successor $\psi(i)$ and has cost $c(\psi)=\sum_i c_{i\psi(i)}$ . It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if it is a single cycle through all jobs.

A permutation $\varphi$ ranks the $A$ if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$ . The interchange $\alpha_{ij}$ swaps $i$ and $j$ ; applying it to $\psi$ gives $\psi\alpha_{ij}$ (first $\alpha_{ij}$ , then $\psi$ ), which exchanges the successors of $i$ and $j$ , at cost $c_\psi(\alpha_{ij})=c(\psi\alpha_{ij})-c(\psi)$ . The graph $G_\varphi$ links $i$ and $\varphi(i)$ for every $i$ ; a spanning tree of $G_\varphi$ is a minimal set of additional arcs $R_{ij}$ that makes it connected, with cost $\sum c_\varphi(\alpha_{ij})$ . Node $q$ is of type 1 if $B_q\le A_{\varphi(q)}$ and of type 2 otherwise.

Given a minimal cost spanning tree $\tau$ of $G_\varphi$ made of arcs $R_{q,q+1}$ , the tour $\psi^*$ is obtained from $\varphi$ by executing the interchanges $\alpha_{q,q+1}$ , $R_{q,q+1}\in\tau$ , first those of type 1 in decreasing order of $q$ , then those of type 2 in increasing order of $q$ .

Formalization targets

Goal: Theorem 5

\psi^*\ \text{is a tour, and}\quad c(\psi^*)\le c(\psi)\ \text{ for every tour }\psi.

This is the paper's main theorem. It fixes no constant and no special form of $f,g$ ; it asserts that the specific tour produced by the algorithm is optimal among all tours.

Milestones

In the order the proof uses them:

Theorem 1: $c(\varphi)=\min_\psi c(\psi)$ over all permutations.
Eq. (11): under $B_j\ge B_i$ , $A_{\psi(j)}\ge A_{\psi(i)}$ , the cost of $\alpha_{ij}$ is $\int_{[B_i,B_j]\cap[A_{\psi(i)},A_{\psi(j)}]}(f+g)$ .
Lemma 1: an interchange between two different cycles merges them.
Theorem 2: the interchanges of a spanning tree, in any order, turn $\psi$ into a tour.
Lemma 2: some minimal cost spanning tree of $G_\varphi$ uses only arcs $R_{i,i+1}$ .
Lemma 5: adjacent interchanges executed on $\varphi$ in the stated order have additive cost.
Theorem 3: $\psi^*$ is a tour of cost $c(\varphi)+c_\varphi(\tau)$ .
Theorem 4: $c(\psi)\ge c(\varphi)+c^*(\psi)$ for every permutation, with the underestimate $c^*$ of (17).
Lemma 7: for a tour $\psi$ the graph $G_\psi^*$ is connected.
Lemma 8: conditions (22a) and (22b) hold for equally many indices.
Eq. (28): $c^*(\psi)\ge c_\varphi(\tau)$ for every tour $\psi$ .

Off the goal's path: Theorem 7, a minimal tour for $(f,g)$ is minimal for $(f+g,0)$ .

Significance

The theorem shows that a traveling salesman problem whose costs come from a one-dimensional state is solved by three polynomial steps: sorting (an optimal assignment), a minimum spanning tree over $N-1$ candidate arcs, and a prescribed sequence of interchanges. It is the base case for a family of later results on solvable TSPs and for the two-machine no-wait flow shop, where it gives an exact polynomial algorithm.

The result has been proved since 1964. No machine-checked proof of it is known to exist. The proof in the paper argues largely from figures ("evident geometrically"), and its statement of Theorem 3 lists the interchanges in an order that contradicts its own proof: executed in the printed order, the paper's numerical example yields a tour of cost 39 instead of the optimum 34. A formal proof settles which order is correct and fills in the geometric steps. Partial contributions are useful: the permutation facts (Lemmas 1, 8 and Theorem 2) are independent of the cost model and reusable.

Difficulty

The obvious argument fails at two points. First, interchanges do not commute in cost: once one interchange is executed, the cost of the next one depends on the new successors, so the cost of $\psi^*$ is not simply $c(\varphi)$ plus the tree cost for an arbitrary execution order. Showing that the specific order of Lemma 5 avoids all interference requires tracking how type-1 and type-2 nodes behave as interchanges are applied. Second, optimality is not a local statement: an arbitrary tour is not reachable from $\varphi$ by tree interchanges, so the lower bound needs the separate underestimate $c^*$ and a counting argument relating every tour to a spanning tree of $G_\varphi$ . Neither step follows from general minimum spanning tree theory.

Formalization scope

Jobs are Fin (n + 1) ( $N=n+1\ge1$ ), so the paper's job $i$ is index $i-1$ ; the adjacent arc $R_{q,q+1}$ is indexed by q : Fin n and joins q.castSucc and q.succ. Permutations are Equiv.Perm (Fin (n + 1)), and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j (Mathlib's composition, "first $\alpha_{ij}$ , then $\psi$ "). Costs are real; (1) uses oriented interval integrals and (17) set integrals.

Explicit readings of the paper's loose phrases:

"any integrable functions $f,g$ " is read as local integrability on $\mathbb R$ , with $f+g\ge0$ the only sign condition;
"proper subsets $s$ " in (4) are nonempty proper subsets;
"a minimal set of additional arcs that connect" is minimal under inclusion; "minimal cost spanning tree" is minimal in cost among spanning trees made of adjacent arcs (by Lemma 2 the same minimum as over all trees);
"minimal cost tour" means cost at most that of every tour, i.e. every permutation that is a single cycle;
"obtained by executing the $\alpha$ 's in a particular order" (Lemma 5) is the explicit order of its proof;
ties among the $A$ leave $\varphi$ non-unique; every statement holds for every ranking $\varphi$ .

The order of $\psi^*$ is that of the proof of Lemma 5 and of steps T2–T4 (p. 673), not the order printed in Theorem 3.

Trivializing formalizations are ruled out: the goal quantifies over all tours, not over permutations (that is Theorem 1) nor over tours reachable from $\varphi$ ; $\psi^*$ is constructed from $\varphi$ and $\tau$ , not taken as an arbitrary tour of the right cost; $\tau$ is both inclusion-minimal and cost-minimal; and the costs keep both branches of (1) with general densities, not $c_{ij}=|A_j-B_i|$ . The TSP items already on the platform concern symmetric or metric distances with tours as visiting orders, a different model, and are not reused.

Needed infrastructure: cycle structure of permutations under transpositions (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, interval integrals of locally integrable functions. Contributions to any milestone are welcome; the purely combinatorial ones (Lemmas 1, 8, Theorem 2, Lemma 7) are independent of the integrals.

Selected references

P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5), 1964, 655–679. https://doi.org/10.1287/opre.12.5.655
P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in The Traveling Salesman Problem (Lawler, Lenstra, Rinnooy Kan, Shmoys, eds.), Wiley, 1985, 87–143. ISBN 978-0-471-90413-7
R. E. Burkard, V. G. Deineko, R. van Dal, J. A. A. van der Veen and G. J. Woeginger, Well-solvable special cases of the traveling salesman problem: a survey, SIAM Review 40(3), 1998, 496–546. https://doi.org/10.1137/S0036144596297514
J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proc. AMS 7(1), 1956, 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7

15 thms3 active usersReviewed

Completed

Probability 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

Convex Optimization Functional Analysis Optimization·Captain: mikedeng1

A Dual Algorithm for the Solution of Nonlinear Variational Problems via Finite Element Approximation 1: For 0 < ρ < 2r, the Modified Dual Algorithm Converges Strongly to (v, Av)Research Paper

Motivation

Many problems in mechanics and optimal control are posed as the minimization of a convex functional of the form $f(Av)-\langle b,v\rangle$ , where $A$ is a differential operator and $f$ is non-smooth: an obstacle, a friction term, a plasticity threshold. Splitting the variable, $y=Av$ , separates the linear operator from the non-smooth function, and a Lagrange multiplier for the constraint $Av-y=0$ turns the problem into a sequence of two simpler ones: a linear system in $v$ and a pointwise nonlinear problem in $y$ . The scheme that alternates between the two and then updates the multiplier is now called the alternating direction method of multipliers (ADMM). It is one of the standard algorithms of large-scale convex optimization, statistics and imaging (Boyd, Parikh, Chu, Peleato and Eckstein, 2011).

Gabay and Mercier (IRIA report RR-126, 1975; Comput. Math. Appl., 1976) gave a convergence proof of this method in Hilbert space, for a stepsize $\rho$ anywhere in $(0,2r)$ , where $r$ is the penalty parameter of the augmented Lagrangian.

Timeline.

1969: Hestenes and Powell introduce the augmented Lagrangian (method of multipliers).
1975: Glowinski and Marrocco propose the alternating scheme for nonlinear Dirichlet problems.
1975–76: Gabay and Mercier prove strong convergence of the primal iterates for $0<\rho<2r$ under strong monotonicity of $f_1'$ (this mission).
1983: Gabay identifies ADMM with Douglas–Rachford splitting applied to the dual.
1992: Eckstein and Bertsekas extend convergence to maximal monotone operators, without strong monotonicity, for $\rho=r$ .

Setting

$V$ and $Y$ are real Hilbert spaces; $(\cdot,\cdot)$ and $|\cdot|$ are the inner product and norm of $Y$ , $\|\cdot\|$ the norm of $V$ . $A:V\to Y$ is a continuous linear operator and $b$ is a continuous linear functional on $V$ , with value $\langle b,v\rangle$ at $v$ . The dual of $Y$ is identified with $Y$ . The function $f:Y\to(-\infty,+\infty]$ is a sum $f=f_1+f_2$ where

$f_1:Y\to\mathbb R$ is convex and continuously differentiable, and its gradient is strongly monotone: $(f_1'(y)-f_1'(z),y-z)\ge\gamma|y-z|^2$ for some $\gamma>0$ (2.3);
$f_2$ is proper (never $-\infty$ , somewhere finite), convex and lower semicontinuous;
$|Av|^2\ge\alpha^2\|v\|^2$ for some $\alpha>0$ (2.5);
some $Av_0$ lies in the interior of $\operatorname{dom}f_2=\{y:f_2(y)<+\infty\}$ (qualification).

The problem is

(\mathcal P)\qquad \inf_{v\in V}\ f(Av)-\langle b,v\rangle ,

and a solution $v^*$ is a point where this value is finite and minimal. The Lagrangian and augmented Lagrangian are, for $\lambda\in Y$ and $r>0$ ,

\mathcal L(v,y;\lambda)=f(y)+(\lambda,Av-y)-\langle b,v\rangle,\qquad \mathcal L_r=\mathcal L+\frac r2|Av-y|^2 .

The modified dual algorithm (3.4) starts from any $(y^0,\lambda^0)\in Y\times Y$ and, for $n\ge0$ ,

finds $v^{n+1}$ with $r(Av^{n+1},Aw)=(ry^n-\lambda^n,Aw)+\langle b,w\rangle$ for all $w\in V$ (minimization of $\mathcal L_r$ in $v$ );
finds $y^{n+1}$ with $\lambda^n+rAv^{n+1}-ry^{n+1}-f_1'(y^{n+1})\in\partial f_2(y^{n+1})$ (minimization of $\mathcal L_r$ in $y$ );
sets $\lambda^{n+1}=\lambda^n+\rho(Av^{n+1}-y^{n+1})$ .

$P$ denotes the orthogonal projection of $Y$ onto the range $R(A)$ , which is closed by (2.5).

Formalization targets

Goal: Theorem 3.1

For $r>0$ and every stepsize with

0<\rho<2r,

every run of the algorithm satisfies

\|v^n-v^*\|\to0,\qquad |y^n-Av^*|\to0,\qquad \sup_n|\lambda^n|<\infty,

where $v^*$ is the unique solution of $(\mathcal P)$ . The multipliers need not converge.

Milestones

Proposition 2.1: $(\mathcal P)$ has a unique solution.
Theorem 2.1: a saddle point $(v^*,y^*;\lambda^*)$ of $\mathcal L$ consists of the solution $v^*$ , $y^*=Av^*$ and $\lambda^*\in\partial f(Av^*)$ with $A'\lambda^*=b$ ; and a saddle point exists.
Theorem 2.2: for $r>0$ , $\mathcal L_r$ and $\mathcal L$ have the same saddle points.
(3.8)–(3.10): a saddle point is a fixed point of Steps 1–2.
(3.11)–(3.12): $A(v^{n+1}-v^*)=P(y^n-y^*)-\frac1rP(\lambda^n-\lambda^*)$ .
(3.19)–(3.20): the energy estimate

\gamma|y^{n+1}-y^*|^2+\Bigl(r-\frac\rho2\Bigr)|(I-P)(y^{n+1}-y^*)|^2+\frac r2|P(y^{n+1}-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^{n+1}-\lambda^*)|^2\le\frac r2|P(y^n-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^n-\lambda^*)|^2

and its sum over $n=0,\dots,N$ . 7. $y^n\to y^*$ for $0<\rho\le2r$ . 8. (3.22)–(3.23): a contraction-plus-summable-forcing recursion for $|P(\lambda^n-\lambda^*)|^2$ , and the scalar lemma that such recursions tend to $0$ . 9. $P(\lambda^n-\lambda^*)\to0$ and $v^n\to v^*$ for $0<\rho<2r$ .

Significance

The theorem says that ADMM converges without any step-size tuning beyond $\rho<2r$ , and that the primal iterates converge in norm in infinite dimension, which is what makes the method usable for finite element discretizations of variational problems (the companion mission on internal approximations treats the discretization). It covers obstacle problems, Bingham fluids and elasto-plastic torsion, where $f_2$ is an indicator or a non-differentiable norm.

The result is proved in the 1975 report. To our knowledge it has no machine-checked proof. Formalizing it adds a library-level convergence theorem for ADMM in Hilbert space with $\mathrm{EReal}$ -valued convex functions, a saddle-point existence theorem for linearly constrained convex problems, and the energy estimate (3.19) as a reusable lemma. The formalization also fixes two defects of the printed text (see Formalization scope): a sign in Step 1 and a qualification hypothesis that is too weak.

Difficulty

The energy estimate (3.19) only controls the multiplier through its component in $R(A)^\perp$ , and only the $y$ -error through $\gamma>0$ . The natural first idea, a Lyapunov function in $|\lambda^n-\lambda^*|^2$ alone that decreases at each step, does not work for $\rho\ne r$ : the component $P(\lambda^n-\lambda^*)$ obeys a separate recursion whose contraction factor $|1-\rho/r|$ is below one only for $0<\rho<2r$ , and whose forcing term must be shown summable from the $y$ -estimate. The existence of a multiplier, i.e. of a saddle point, is a separate difficulty: it needs the subdifferential chain rule $\partial(f\circ A)=A'\partial f(A\,\cdot)$ in infinite dimension, under a constraint qualification.

Formalization scope

Lean conventions:

$V$ , $Y$ are InnerProductSpace ℝ with CompleteSpace; multipliers are elements of $Y$ ; $b$ is a StrongDual ℝ V.
$f_1:Y\to\mathbb R$ (a Gateaux-differentiable function is finite), with a gradient f₁' at every point (HasGradientAt) that is continuous; "weakly continuous on finite-dimensional subspaces" is then automatic.
$f_2:Y\to$ EReal, with IsProperFn, IsConvexFn, IsSubgradient from the published InertialFB.IFB.ConvexAnalysis and Mathlib's LowerSemicontinuous. No subtraction in EReal occurs: the variational inequalities (3.6), (3.9) are stated as subgradient inclusions, and the Lagrangians as a real part plus $f_2(y)$ .
A solution of $(\mathcal P)$ has finite value. A run is any triple of sequences indexed by $\mathbb N$ satisfying Steps 1–3 for every $n$ ; the start is arbitrary, and the well-posedness of the steps is not assumed or used.
$P$ is the orthogonal projection onto the closure of $R(A)$ , equal to $R(A)$ under (2.5).
Strong convergence is convergence in norm; "bounded" is Bornology.IsBounded (Set.range λ).

Corrections to the printed text, each explained in the item's statement:

Step 1 (3.5) and (3.8) carry $+\langle b,v\rangle$ . The paper prints $-\langle b,v\rangle$ there and in Remark 1 of p. 15, which is inconsistent with $\mathcal L$ and $(\mathcal P)$ : with the printed sign the iteration solves the problem with $-b$ .
The qualification (2.4), " $\operatorname{int}\operatorname{dom}f_2\ne\emptyset$ ", is strengthened to $\operatorname{int}\operatorname{dom}f_2\cap R(A)\ne\emptyset$ . With (2.4) alone, Theorem 2.1's saddle point need not exist and the multipliers of Theorem 3.1 need not be bounded: $V=\mathbb R$ , $Y=\mathbb R^2$ , $Av=(v,0)$ , $f_1=|\cdot|^2/2$ , $f_2$ the indicator of the disc of centre $(0,1)$ and radius $1$ , $\langle b,v\rangle=v$ .
Proposition 2.1 assumes that $f_2\circ A$ is somewhere finite, which its proof requires.

Ruled out: the solution $v^*$ is a hypothesis of the goal, so the hypotheses must not be contradictory. They are met by $V=Y=\mathbb R$ , $A=\mathrm{id}$ , $f_1(y)=y^2/2$ , $f_2=0$ , $b=0$ , and a proper $f_2$ excludes the degenerate reading in which every point "solves" $(\mathcal P)$ with value $+\infty$ .

A complete development needs: existence of minimizers of coercive convex l.s.c. functions on a Hilbert space; the subdifferential sum and chain rules under a continuity qualification; orthogonal projections onto closed ranges; and elementary facts about summable sequences. The saddle-point theory (Theorems 2.1–2.2) and the scalar lemma (3.23) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal by a different route.

Selected references

D. Gabay and B. Mercier, A dual algorithm for the solution of non linear variational problems via finite element approximation, IRIA Rapport de Recherche 126, 1975. https://hal.science/hal-04716124v1 ; journal version: Computers & Mathematics with Applications 2 (1976) 17–40, https://doi.org/10.1016/0898-1221(76)90003-1
R. Glowinski and A. Marrocco, Sur l'approximation, par éléments finis d'ordre un, et la résolution, par pénalisation-dualité, d'une classe de problèmes de Dirichlet non linéaires, RAIRO Analyse Numérique 9 (1975) 41–76. https://doi.org/10.1051/m2an/197509R200411
M. R. Hestenes, Multiplier and gradient methods, J. Optim. Theory Appl. 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
I. Ekeland and R. Temam, Analyse convexe et problèmes variationnels, Dunod, 1974 (the paper's [E]).
J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Math. Programming 55 (1992) 293–318. https://doi.org/10.1007/BF01581204
S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3 (2011) 1–122. https://doi.org/10.1561/2200000016

16 thms3 active usersReviewed

Completed

Probability 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

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Shock Models and Wear Processes IV: With a Random Threshold, Shock Survival Probabilities Are Submultiplicative for Every Damage Law Iff the Threshold Is NBUResearch Paper

Motivation

Reliability theory classifies life distributions by how they age. A device whose remaining life, once it has survived to age $t$ , is stochastically shorter than the life of a new device is called new better than used (NBU). The NBU class, together with the classes IHR (increasing hazard rate) and IHRA (increasing hazard rate average), organizes much of the theory of maintenance and replacement: Marshall and Proschan showed that the NBU property is what makes certain replacement policies beneficial, and Barlow and Proschan's monographs build the statistical theory of reliability on these classes.

A question that runs through this literature is where such ageing properties come from physically. Esary, Marshall and Proschan (Ann. Probability 1973) answer it for shock models: a device is hit by shocks arriving in time as a Poisson process, each shock adds a random amount of damage, and the device fails when the accumulated damage exceeds its threshold. Section 4 of their paper treats a fixed threshold and shows that the life is IHRA for every damage law. Section 5, the subject of this mission, lets the threshold itself be random, which models the variation between individual items of a production lot. It then asks which ageing properties of the threshold law are inherited by the life distribution, and which are forced if the inheritance is to hold whatever the damage law.

Setting

All distributions are laws of non-negative random variables. For a distribution $F$ on $\mathbb R$ with $F(z) = 0$ for $z < 0$ (a damage law), $F^{(k)}$ denotes the $k$ -fold convolution of $F$ , with $F^{(0)}$ the point mass at $0$ ; thus $F^{(k)}(x) = P\{X_1 + \cdots + X_k \le x\}$ for independent $X_i \sim F$ .

A threshold law is a distribution $G$ with $G(z) = 0$ for $z < 0$ ; write $\bar G = 1 - G$ for its survival function. If the threshold $Y \sim G$ is independent of the damages, the probability of surviving $k$ shocks is

\bar P_k = \int_0^\infty F^{(k)}(x)\, dG(x) = P\{X_1 + \cdots + X_k \le Y\}, \qquad k = 0, 1, \dots \tag{5.1}

If shocks arrive as a Poisson process of rate $\lambda > 0$ , the device's life distribution $H$ has survival function

\bar H(t) = \sum_{k=0}^\infty e^{-\lambda t}\frac{(\lambda t)^k}{k!}\,\bar P_k, \qquad t \ge 0. \tag{5.2}

A survival function $\bar F$ is NBU if $\bar F(t + x) \le \bar F(x)\bar F(t)$ for all $x, t \ge 0$ ; it is IHR if $\bar F(x + t)/\bar F(t)$ is non-increasing in $t$ for each $x > 0$ , and IHRA if $[\bar F(t)]^{1/t}$ is non-increasing in $t > 0$ . The discrete analogue of NBU for the sequence $\bar P_k$ is submultiplicativity, $\bar P_{j+k} \le \bar P_j \bar P_k$ .

Formalization targets

Goal: Theorem 5.3

For a threshold law $G$ with $G(z) = 0$ for $z < 0$ :

\Big(\forall F:\ \bar P_{j+k} \le \bar P_j\,\bar P_k \ \ \forall j,k \ge 0\Big) \iff \bar G \text{ is NBU},

the quantifier ranging over every damage law $F$ ; and if $G$ is NBU, then for every damage law $F$ and every $\lambda > 0$ the life distribution $H$ of (5.2) is NBU.

Milestones

Theorem 3.1 (3.5). For any sequence $1 = \bar P_0 \ge \bar P_1 \ge \cdots \ge 0$ and $\lambda > 0$ : if $\bar P_j \bar P_k \ge \bar P_{j+k}$ for all $j, k$ , then $H$ of (2.1) is NBU.
First display of the proof of Theorem 5.3. If $G$ is NBU, then $\bar P_{j+k} \le \bar P_j \bar P_k$ for each damage law $F$ .
Second display of the proof of Theorem 5.3. If submultiplicativity holds for every $F$ , then $\bar G(s + j x_k) \le \bar G(s)\,\bar G(j x_k)$ for $s > 0$ , $x_k = s/k$ , $j = 0, 1, \dots$ .

Further items (not milestones)

Theorem 5.1 (the life is exponential for every $F$ iff $G$ is exponential) and Theorem 5.2 (b), (c) (an IHR threshold makes $\bar P_k^{1/k}$ non-increasing for every $F$ ; non-increasing $\bar P_k^{1/k}$ for every $F$ forces $G$ to be IHRA) are posed as companion statements from the same section.

Significance

Theorem 5.3 is a characterization: the NBU class is exactly the class of threshold laws for which the cumulative-damage mechanism preserves the discrete NBU property under every damage law. Combined with Theorem 3.1 (3.5), it gives a physical derivation of NBU life distributions: an item with an NBU random strength, subject to Poisson shocks with arbitrary i.i.d. non-negative damage, has an NBU life. Theorems 5.1 and 5.2 place the exponential and the IHR/IHRA classes in the same framework, and the authors record that whether an IHRA threshold suffices in Theorem 5.2 (b) is left unresolved.

The results are proved in the paper. No machine-checked version is known to exist; this mission produces one. A complete development also supplies reusable infrastructure: convolution powers of laws on $[0, \infty)$ as Mathlib measures, Poisson mixtures of a sequence, and the ageing classes of p. 631 as predicates on survival functions.

Difficulty

The equivalence couples a property of one function, $\bar G$ , to a family of inequalities indexed by every damage law, and the left side is about convolutions while the right side is pointwise. Two points make the statement harder than it looks. First, (5.1) as printed is $P\{X_1 + \cdots + X_k \le Y\}$ , whereas the paper's proof works with $E\bar G(X_1 + \cdots + X_k) = P\{X_1 + \cdots + X_k < Y\}$ ; the two agree only when $F^{(k)}$ and $G$ have no common discontinuities, and they can disagree as soon as $F^{(k)}$ has an atom where $G$ has one, a case the left side of the equivalence includes. A formal proof cannot invoke that convention. Second, the second sentence of the theorem passes through a Poisson series (5.2) whose terms involve the whole sequence $\bar P_k$ , so the NBU property of $H$ is a statement about a power series in $t$ , not about any single $\bar P_k$ .

Formalization scope

A distribution is a probability measure on $\mathbb R$ ; " $F(z) = 0$ for $z < 0$ " is mass $0$ on $(-\infty, 0)$ , and " $G(0) = 0$ " (Theorems 5.1, 5.2) is mass $0$ on $(-\infty, 0]$ . $F^{(k)}$ is the $k$ -fold Measure.conv power with $F^{(0)} = \delta_0$ , and $F^{(k)}(x)$ is the mass of $(-\infty, x]$ .
$\bar P_k$ is (5.1) as printed, $\int F^{(k)}(x)\,dG(x)$ over $\mathbb R$ ; since $G$ is carried by $[0, \infty)$ this is $\int_0^\infty$ including an atom of $G$ at $0$ , which Theorem 5.3 allows. The paper's convention that $F^{(k)}$ and $G$ have no common discontinuities is not added as a hypothesis: the statements hold for (5.1) without it. The integrand is monotone with values in $[0,1]$ , so the Bochner integral is a genuine expectation.
"For all $F$ " sits inside the equivalence of Theorem 5.3 and ranges over every probability measure on $[0, \infty)$ . Submultiplicativity for one fixed $F$ is a different, weaker statement.
NBU and IHR are cross-multiplied, agreeing with the paper's ratio form wherever denominators are positive (the paper restricts variables to avoid zero denominators). NBU is on $x, t \ge 0$ exactly as in definition (v). Powers $[\bar G(t)]^{1/t}$ and $\bar P_k^{1/k}$ are real powers. "Decreasing" means non-increasing.
$H$ is the series (2.1) as a function on $\mathbb R$ , equal to $1$ on $(-\infty, 0)$ ; $\lambda > 0$ as in (1.1). In Theorem 3.1 (3.5) the non-negativity $\bar P_k \ge 0$ is stated explicitly.
In Theorem 5.1 "exponential" allows rate $0$ for $H$ (the damage law $\delta_0$ gives $\bar H \equiv 1$ ) and requires a positive rate for $G$ ( $G(0) = 0$ rules out the degenerate case $\bar G = 0$ on $(0,\infty)$ ).
A trivializing formalization is ruled out: the threshold-law quantifier is not restricted to a class where both sides are automatic, the integral cannot collapse to a default value, and the NBU predicate is the paper's on $[0, \infty)$ , not on $(0, \infty)$ or a vacuous domain.

Contributions welcome: proofs of the milestones, a library for Poisson mixtures and convolution powers of laws on $[0,\infty)$ , and the extra items of §5.

Selected references

J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, The Annals of Probability 1(4), 627–649, 1973. https://doi.org/10.1214/aop/1176996891
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965; reprinted SIAM Classics in Applied Mathematics, 1996. https://doi.org/10.1137/1.9781611971194
Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-Out for Components and Systems, The Annals of Mathematical Statistics 37(4), 816–825, 1966. https://doi.org/10.1214/aoms/1177699362

5 thms3 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Ergodic Theorems for Weakly Interacting Infinite Systems and the Voter Model: The Discrete-Time Proximity Process Is Dual to the Branching Process with InterferenceResearch Paper

Motivation

Many models in probability, statistical physics and the theory of stochastic networks are interacting particle systems: infinitely many sites, each in state 0 or 1, each updating at random according to the states of a few other sites. A basic question about such a system is ergodicity: does it have a unique stationary distribution, and does its law converge to it from every initial configuration? For infinite systems the question is hard, because the state space $\{0,1\}^I$ is uncountable and standard Markov chain arguments do not apply.

Holley and Liggett (Ann. Probab. 3 (1975), 643–663) introduced a class of such systems, the proximity processes, which arise from a coupling of more general weakly interacting systems (the settings of Vasershtein (1969), Dobrushin (1971) and Chover (1974)), and showed that each proximity process is dual to a process of finite sets, the branching process with interference. Duality turns a question about an infinite-dimensional process into a question about a process whose states are finite sets. The paper uses it to give short proofs of ergodicity criteria and, in its §5, to study the invariant measures of the voter model. Duality of this kind became one of the main tools of the field; see Liggett, Interacting Particle Systems (Springer, 1985).

This mission formalizes the discrete-time half of the paper: the duality theorem (1.6) and its first applications, Corollary (3.1) and Corollary (4.1).

Setting

Let $I$ be a countable set of sites and $S=\{0,1\}^I$ the set of configurations $\eta:I\to\{0,1\}$ , with the product $\sigma$ -algebra. For $\eta\in S$ , $C(\eta)=\{i\in I:\eta(i)=1\}$ is the set of occupied sites.

The data of the model are, for each site $i$ , a sequence $N_{i,0}=\emptyset,N_{i,1},N_{i,2},\dots$ of finite subsets of $I$ and a probability distribution $f_i$ on $\{0,1,2,\dots\}$ .

The proximity process $\eta_n$ is the Markov chain on $S$ whose transition function is the product measure

Q(\eta,\cdot)=\prod_{i\in I}\nu_{\alpha(i,\eta),i},\qquad \alpha(i,\eta)=\sum_{k:\,N_{i,k}\cap C(\eta)\neq\emptyset}f_i(k),

where $\nu_{\rho,i}$ puts mass $\rho$ on $1$ . In words: each site $i$ independently picks an index $k$ with probability $f_i(k)$ and becomes $1$ exactly when the set $N_{i,k}$ contains an occupied site. $P_\eta(\eta_n\in\cdot)$ denotes the law at time $n$ started from $\eta$ .

The branching process with interference (b.p.i.) $A_n$ is the Markov chain on the collection $\mathcal T$ of finite subsets of $I$ with transition function

\tilde Q(A,B)=\sum{}'\prod_{i\in A}f_i(k_i),

the sum over all sequences $(k_i)_{i\in A}$ with $\bigcup_{i\in A}N_{i,k_i}=B$ : each particle at $i$ splits into particles on $N_{i,k}$ with probability $f_i(k)$ , and particles landing on the same site merge. $P_F$ denotes probabilities for the chain started at $F$ .

For $F\in\mathcal T$ , $B(F)=\{\eta\in S:\eta(i)=0\ \text{for all } i\in F\}$ .

Formalization targets

Goal: Theorem (1.6)

For all $n\ge0$ , $\eta\in S$ and $F\in\mathcal T$ ,

P_\eta(\eta_n\in B(F))=P_F(A_n\cap C(\eta)=\emptyset).

Milestones

The proof is an induction on $n$ whose steps are four displayed identities on p. 647:

(2.3) the one-step law of the proximity process on $B(F)$ : $P_\eta(\eta_1\in B(F))=\sum'\prod_{i\in F}f_i(k_i)$ , the sum over sequences with $N_{i,k_i}\cap C(\eta)=\emptyset$ for all $i\in F$ ;
(2.4) the same expression for $P_F(A_1\cap C(\eta)=\emptyset)$ ;
(2.5) the first-step decomposition $P_F(A_{n+1}\cap C(\eta)=\emptyset)=\sum_{(k_i)}P_{\bigcup_{i\in F}N_{i,k_i}}(A_n\cap C(\eta)=\emptyset)\prod_{i\in F}f_i(k_i)$ ;
(2.8) the last-step decomposition $P_\eta(\eta_{n+1}\in B(F))=\sum_{(k_i)}P_\eta(\eta_n\in B(\bigcup_{i\in F}N_{i,k_i}))\prod_{i\in F}f_i(k_i)$ .

Applications

Corollary (3.1): if $\sum_k|N_{i,k}|f_i(k)\le\lambda<1$ for all $i$ , then

P_\eta(\eta_n\in B(F))\ge1-\lambda^n|F|,

and the point mass on the all-zero configuration is the only stationary distribution; along the way, (3.5): $P_F(A_n\neq\emptyset)\le E_F|A_n|\le\lambda^n|F|$ .

(4.5): for the §4 model on $\mathbb Z$ , $P_{F\cup G}(A_t\neq\emptyset)\le P_F(A_t\neq\emptyset)+P_G(A_t\neq\emptyset)-P_{F\cap G}(A_t\neq\emptyset)$ .
Corollary (4.1): on $I=\mathbb Z$ with $N_{i,1}=\{i-1,i+1\}$ , $f_i(0)=1-\lambda$ , $f_i(1)=\lambda$ , and $h(\lambda)=2\lambda+2\lambda^2-7\lambda^3+5\lambda^4-\lambda^5$ ,

P_\eta(\eta_t\in B(F))\ge1-[h(\lambda)]^{(t-1)/2}|F|\qquad(t\ge1).

Significance

The duality identity expresses every finite-dimensional "all vacant" probability of the proximity process, which determine its law, through a chain on finite sets. Consequences in the paper: a sufficient condition for convergence to the all-zero configuration (Corollary (3.1)), which in the nearest-neighbour example on $\mathbb Z$ gives $\lambda<\tfrac12$ ; the sharper range $h(\lambda)<1$ , i.e. $\lambda<0.6527$ , for that example (Corollary (4.1)), which the interference term makes possible; and, in continuous time, the analysis of the invariant measures of the voter model.

The results are classical and proved; a search of Prove2Me and Mathlib found no machine-checked proof of any of them. A formalization contributes a Lean model of an infinite-product Markov kernel on $\{0,1\}^I$ with its $n$ -step laws, a model of a set-valued branching chain, and the duality between them, which are reusable for other duality arguments (contact process, voter model, coalescing random walks).

Difficulty

The two sides of (1.7) are defined independently and live on different spaces. The left side is the time- $n$ law of a chain on the uncountable space $\{0,1\}^I$ , obtained by iterating an infinite product kernel; the right side comes from a transition matrix on the countable set of finite subsets of $I$ , whose entries are themselves infinite sums over sequences indexed by a finite set. Neither side can be computed in closed form beyond $n=1$ , so no direct evaluation proves the identity for general $n$ .

Two technical points stand in the way of a naive argument. Evaluating a product kernel on a cylinder event and integrating it against a previous law requires the kernel to be measurable in $\eta$ , a statement about cylinder sets of an infinite product that a hand proof passes over. And the natural recursion for $n$ -step probabilities of the b.p.i. adds the new step at the end, while the comparison with the proximity process needs information about the first step; the two orders agree only by a Chapman–Kolmogorov argument over a countable state space with $[0,\infty]$ -valued sums. Corollary (4.1) further needs quantitative estimates of survival probabilities for specific initial sets on $\mathbb Z$ .

Formalization scope

All objects are in the namespace HolleyLiggett.Duality, in one definitions file.

$\{0,1\}$ is Bool (true = 1), $S$ is Config I := I → Bool with the product $\sigma$ -algebra, $\mathcal T$ is Finset I.
Standing assumptions on every theorem: [Countable I], N : I → ℕ → Finset I (finite sets) with N i 0 = ∅, and f : I → PMF ℕ (probability distributions). A finite collection $N_{i,0},\dots,N_{i,m}$ is the case $f_i(k)=0$ for $k>m$ .
The kernel (1.1) is Measure.infinitePi of the two-point measures; the $n$ -step law is proxLaw, iterating Measure.bind from the point mass at $\eta$ . Measurability of the kernel is a true fact that solvers must prove; it is not assumed.
The b.p.i. $n$ -step probabilities bpiProb follow the last-step recursion $P_F(A_{n+1}=B)=\sum_GP_F(A_n=G)\tilde Q(G,B)$ . All probabilities are in ℝ≥0∞, and each $\sum'$ over sequences is an unconditional sum over ↥F → ℕ.
The page's " $\eta(1)=1$ " in (1.2) is read as $\eta(i)=1$ . Corollary (4.1) carries the added hypothesis $t\ge1$ : at $t=0$ the printed bound fails when $h(\lambda)>1$ , and the proof starts at $t=1$ . Inequality (4.5) uses the §4 model on $\mathbb Z$ , with the subtracted term moved across.
The goal relates the two chains defined by (1.1) and (1.4). A statement through the coupling $X_{i,n}$ of the proof, about an arbitrary process with the right one-step behaviour, or for $n=1$ only, is not the theorem.

The continuous-time duality (Theorem (2.12)), Corollaries (3.9) and (4.15) and the voter model of §5 are out of scope. Contributions welcome: the measurability and probability facts for proxStep, Chapman–Kolmogorov for bpiProb, and proofs of the milestones.

Selected references

R. A. Holley and T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, Ann. Probab. 3(4) (1975), 643–663. https://doi.org/10.1214/aop/1176996306
T. M. Liggett, Interacting Particle Systems, Grundlehren der mathematischen Wissenschaften 276, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
R. L. Dobrushin, Markov processes with a large number of locally interacting components (Russian), Problems of Information Transmission 7(2) (1971), 70–87 (as cited by Holley and Liggett).
O. N. Stavskaya and I. I. Pyatetskii-Shapiro, On homogeneous nets of spontaneously active elements, Systems Theory Research 20 (1971), 75–88 (as cited by Holley and Liggett).
L. N. Vasershtein, Processes over denumerable products of spaces, describing large systems, Problems of Information Transmission 3 (1969), 47–52 (as cited by Holley and Liggett).

6 thms3 active usersReviewed

Completed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

Globally Convergent Inexact Newton Methods I: Inexact Newton Backtracking Converges to Every Limit Point Where F′ Is Invertible, That Point Is a Zero of F, and Initial Steps Are Eventually AcceptedResearch Paper

Motivation

Newton's method for a nonlinear system $F(x) = 0$ , with $F:\mathbb R^n\to\mathbb R^n$ , solves the linear system $F'(x_k)s_k = -F(x_k)$ at every step. For large systems that solve is itself iterative (a Krylov method such as GMRES), and it is stopped early. The resulting inexact Newton methods, introduced by Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19 (1982)), accept any step with $\|F(x_k)+F'(x_k)s_k\|\le\eta_k\|F(x_k)\|$ , where the forcing term $\eta_k\in[0,1)$ controls how accurately the linear system is solved. Their theory is local: it applies once the iterates are near a solution with invertible derivative.

Practical solvers (Newton–Krylov codes in large-scale simulation, nonlinear solver libraries such as PETSc's SNES and SUNDIALS' KINSOL) combine such inexact steps with a globalization, most often backtracking along the step. Eisenstat and Walker (SIAM J. Optim. 4 (1994)) gave the global convergence theory for this combination: what can be said about the iterates from an arbitrary starting point, with no assumption that a solution exists or that $F'$ is invertible anywhere.

Timeline. Dembo, Eisenstat and Steihaug (1982) proved local convergence of inexact Newton methods. Dembo and Steihaug (Math. Program. 26 (1983)) studied truncated Newton methods for unconstrained minimization. Brown and Saad (1990) studied globalized Newton–Krylov methods with line searches and model trust regions, under the inner-product norm. Eisenstat and Walker (1994) gave the general framework treated here, for an arbitrary norm. Their 1996 paper (SIAM J. Sci. Comput. 17) proposed the forcing-term choices that are now standard.

Setting

Let $E$ be $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$ , and let $F:E\to E$ be continuously differentiable with derivative $F'(x)$ . A point $x_*$ is a limit point of $(x_k)$ if every ball $N_\delta(x_*)=\{y:\|y-x_*\|<\delta\}$ contains $x_k$ for infinitely many $k$ .

Algorithm GIN (global inexact Newton method). Fix $t\in(0,1)$ . At each $k$ , find a level $\eta_k\in[0,1)$ and a step $s_k$ with

\|F(x_k)+F'(x_k)s_k\|\le\eta_k\|F(x_k)\| \quad (2.1),\qquad \|F(x_k+s_k)\|\le[1-t(1-\eta_k)]\,\|F(x_k)\| \quad (2.2),

and set $x_{k+1}=x_k+s_k$ . Condition (2.1) says that $s_k$ reduces the norm of the local linear model by the factor $\eta_k$ . Condition (2.2) asks that $\|F\|$ itself decrease by a fixed fraction $t$ of that predicted reduction.

Algorithm MR (minimum reduction method). Fix $\eta_{\max}\in[0,1)$ and $0<\theta_{\min}<\theta_{\max}<1$ . At step $k$ , choose $\bar\eta_k\in[0,\eta_{\max}]$ and a curve $\sigma_k$ with $\|F(x_k)+F'(x_k)\sigma_k(\eta)\|\le\eta\|F(x_k)\|$ for $\bar\eta_k\le\eta\le1$ (5.1). Start at $\eta_k=\bar\eta_k$ . While (2.2) fails for $s_k=\sigma_k(\eta_k)$ , replace $\eta_k$ by $1-\theta(1-\eta_k)$ for some $\theta\in[\theta_{\min},\theta_{\max}]$ . Then set $x_{k+1}=x_k+\sigma_k(\eta_k)$ .

Algorithm INB (inexact Newton backtracking). Choose $\bar\eta_k\in[0,\eta_{\max}]$ and an inexact Newton step $\bar s_k$ at level $\bar\eta_k$ . While (2.2) fails, shorten the step, $s_k\leftarrow\theta s_k$ , and raise the level, $\eta_k\leftarrow1-\theta(1-\eta_k)$ . INB is MR with the backtracking curve $\sigma_k(\eta)=\frac{1-\eta}{1-\bar\eta_k}\bar s_k$ (6.1).

An algorithm does not break down if it produces an infinite sequence of iterates, in particular if every while-loop exits.

Formalization targets

Goal: Theorem 6.1 (global convergence of Algorithm INB)

If Algorithm INB does not break down and $x_*$ is a limit point of $(x_k)$ at which $F'(x_*)$ is invertible, then

F(x_*)=0,\qquad x_k\to x_*,\qquad s_k=\bar s_k\ \text{and}\ \eta_k=\bar\eta_k\ \text{for all sufficiently large }k.

The statement assumes no solution, bounded level set, Lipschitz derivative or particular norm. The last clause says that backtracking eventually stops, so the local rate is governed by the forcing terms $\bar\eta_k$ .

Milestones

In attack order:

Lemmas 1.1 and 1.2. Continuity of $y\mapsto F'(y)^{-1}$ at an invertible point, and a uniform linearization error $\|F(z)-F(y)-F'(y)(z-y)\|\le\varepsilon\|z-y\|$ near $x$ .
Theorem 3.3. If $F(x_k)\to0$ , the steps satisfy (2.1) with a fixed $\eta$ , and $\|F(x_k)\|$ is nonincreasing, then an invertible limit point is a zero and the limit.
Theorem 3.4. A GIN run with $\sum_k(1-\eta_k)=\infty$ has $F(x_k)\to0$ , plus the conclusion of Theorem 3.3 at invertible limit points.
Theorem 3.5. A GIN run converges to a limit point near which $\|s_k\|\le\Gamma(1-\eta_k)\|F(x_k)\|$ (3.2).
Lemma 5.1. The while-loop terminates, with $1-\eta_k\ge\min\{1-\bar\eta_k,\theta_{\min}\delta/(\Gamma\|F(x_k)\|)\}$ .
MR runs are GIN runs (§5).
Theorem 5.2 for MR. Under $\|\sigma_k(\eta)\|\le\Gamma(1-\eta)\|F(x_k)\|$ near a limit point $x_*$ (5.6): $F(x_*)=0$ , $x_k\to x_*$ , and $\eta_k=\bar\eta_k$ eventually.
INB runs are MR runs with the curve (6.1), and $s_k=\sigma_k(\eta_k)$ throughout the loop (§6).

Further items, which are not milestones: Corollary 6.2 (exact Newton with backtracking takes full Newton steps eventually), Theorem 5.2 for Algorithm TL, Lemma 3.1 (existence of acceptable GIN steps), and Proposition 2.1 (the Goldstein–Armijo alpha condition implies (2.2) in the Euclidean norm).

Significance

The result. Theorem 6.1 is the global convergence guarantee for the inexact Newton backtracking method that Newton–Krylov solvers implement. It separates three outcomes: the iterates diverge, they accumulate only at points where $F'$ is singular, or they converge to a solution with invertible derivative and eventually take the unmodified inexact Newton steps. In the third case the local theory of Dembo, Eisenstat and Steihaug applies from some iteration on, so the forcing terms alone set the convergence rate. Theorem 5.2 is the template: §§6–8 of the paper derive the convergence of backtracking, equality-curve and dogleg-type methods from it by verifying (5.6).

Formalizing it. The results are proved on paper and none of them has a machine-checked proof that we know of. The mission produces a library of algorithm-run predicates with explicit while-loops for inexact Newton methods. It also checks the paper's reduction chain (INB is a run of MR, MR is a run of GIN) and the global convergence theorems in an arbitrary finite-dimensional norm.

Difficulty

The obvious argument fails at both ends. Sufficient decrease (2.2) alone gives monotonicity of $\|F(x_k)\|$ , but not convergence of the iterates. On the page, $F(x)=x^2-1$ admits sequences satisfying (2.2) with both $\pm1$ as limit points. Convergence of $\|F(x_k)\|$ to $0$ needs $\sum(1-\eta_k)=\infty$ , and nothing in the algorithm states this. In Theorem 5.2 it has to be derived from the exit level of the while-loop, which depends on a neighbourhood of $x_*$ where the linearization error is uniformly controlled. A solver must combine a limit-point argument (only infinitely many iterates are near $x_*$ , not all of them) with the loop's worst-case backtracking factor $\theta_{\min}$ . The invertibility of $F'(x_*)$ enters only through the bound (5.6) for the backtracking curve, which must be established uniformly in $k$ .

Formalization scope

Space and norm. $E$ is a finite-dimensional real normed space ([NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]). This is exactly " $\mathbb R^n$ with an arbitrary norm". Fin n → ℝ (sup norm) and EuclideanSpace would each fix one norm. Only Proposition 2.1 assumes an inner product space, as the page does.
Derivative. $F'$ is fderiv ℝ F, with ContDiff ℝ 1 F (the paper's standing assumption). Invertibility is ContinuousLinearMap.IsInvertible, and $F'(x)^{-1}$ is ContinuousLinearMap.inverse.
Runs. An algorithm that does not break down is a predicate on infinite sequences (IsGINRun, IsMRRun, IsINBRun, plus IsTLRun, IsENBRun). The steps and levels the algorithm says to "find" or "choose" are data constrained only by the stated conditions. A while-loop is recorded by its number of passes $m_k$ and factors $\theta_{k,j}\in[\theta_{\min},\theta_{\max}]$ . Every trial before the last fails the loop's test and the last one passes it. Termination is part of the run.
Limit point is MapClusterPt xstar atTop x. "For all sufficiently large $k$ " is ∀ᶠ k in atTop. The paper's "whenever $x_k$ is sufficiently near $x_*$ [and $k$ is sufficiently large]" is ∃ Γ, ∃ δ > 0, [∃ K,] ∀ k [≥ K], x k ∈ ball xstar δ → …. $\Gamma$ precedes $k$ ("independent of $k$ "), and the " $k$ large" clause appears only in (3.2), where the page has it.
Hypotheses as printed. Theorems 3.5 and 5.2 do not assume $F'(x_*)$ invertible. Theorem 5.2 does not assume $\sum(1-\eta_k)=\infty$ . Lemma 5.1 is stated for one iteration of the loop shared by MR and TL, for every choice of factors.
Trivializing readings ruled out. A run predicate without the "rejected" clause would allow needless backtracking, and one without the "accepted" clause would drop (2.2). Both clauses are present. A sorry-free check (F = id on $\mathbb R$ ) confirms that the INB, GIN and ENB run predicates and the goal's hypotheses are satisfiable, so the goal is not vacuous.
Infrastructure. Continuity of operator inversion and uniform differentiability on neighbourhoods are in Mathlib. The run predicates and trial-level recursions are reusable for any line-search or backtracking analysis. Each milestone is stated independently; contributions in any order are welcome.

Selected references

S. C. Eisenstat and H. F. Walker, Globally Convergent Inexact Newton Methods, SIAM J. Optim. 4(2) (1994) 393–422. https://doi.org/10.1137/0804022
R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton Methods, SIAM J. Numer. Anal. 19(2) (1982) 400–408. https://doi.org/10.1137/0719025
R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Math. Program. 26 (1983) 190–212. https://doi.org/10.1007/BF02592055
P. N. Brown and Y. Saad, Hybrid Krylov Methods for Nonlinear Systems of Equations, SIAM J. Sci. Stat. Comput. 11(3) (1990) 450–481. https://doi.org/10.1137/0911026
S. C. Eisenstat and H. F. Walker, Choosing the Forcing Terms in an Inexact Newton Method, SIAM J. Sci. Comput. 17(1) (1996) 16–32. https://doi.org/10.1137/0917003
J. E. Dennis and R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, SIAM Classics in Applied Mathematics 16 (1996). https://doi.org/10.1137/1.9781611971200

12 thms3 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Shock Models and Wear Processes I: Under Poisson Shocks, Cumulative Nonnegative I.I.D. Damage up to a Fixed Threshold Gives an IHRA Life DistributionResearch Paper

Motivation

Reliability theory classifies life distributions by how they age. The IHRA class (increasing hazard rate average) is the smallest class of life distributions that contains the exponential distributions and is closed under forming coherent systems and taking limits in distribution (Birnbaum, Esary and Marshall 1966). It is therefore the natural class for the lifetime of a system built from components that wear out. A distribution belongs to it when its survival function $\bar F$ satisfies: $[\bar F(t)]^{1/t}$ is decreasing in $t > 0$ .

Esary, Marshall and Proschan (Ann. Probability 1 (1973) 627–649) asked where such ageing comes from physically. Their answer is a shock model: a device receives shocks at the epochs of a Poisson process, each shock does random damage, and the device fails when the accumulated damage exceeds its capacity. The central result of their §4, formalized in this mission, is that this model always produces an IHRA life, whatever the damage distribution. In the authors' words, "the IHRA property has been obtained … as an implication of a natural physical model. The only hypothesis imposed upon $F$ is that it be the distribution of a nonnegative random variable." The paper is a standard reference of reliability theory and the source of the cumulative damage model used across maintenance and insurance applications.

Setting

Shocks arrive according to a Poisson process with rate $\lambda > 0$ . Write $\bar P_k$ for the probability that the device survives the first $k$ shocks; then $1 \ge \bar P_0 \ge \bar P_1 \ge \dots \ge 0$ (display (2.2)). Conditioning on the number of shocks in $[0, t]$ gives the shock survival function (2.1):

\bar H(t) = \sum_{k=0}^{\infty} \bar P_k\, e^{-\lambda t}\frac{(\lambda t)^k}{k!}, \qquad t \ge 0,

with $\bar H(t) = 1$ for $t < 0$ . The weights $K(k,t) = e^{-\lambda t}(\lambda t)^k/k!$ are the Poisson probabilities.

In the cumulative damage model the $i$ th shock causes a damage $X_i \ge 0$ , the damages are independent with common distribution function $F$ (so $F(z) = 0$ for $z < 0$ ), and the device survives $k$ shocks when $X_1 + \dots + X_k \le x$ , for a fixed threshold $x$ . Hence (4.1)

\bar P_k = F^{(k)}(x), \qquad k = 0, 1, \dots,

where $F^{(k)}$ is the $k$ -fold convolution of $F$ and $F^{(0)}$ is degenerate at $0$ . A distribution with survival function $\bar F$ is IHRA if $[\bar F(t)]^{1/t}$ is decreasing in $t > 0$ ; throughout, "decreasing" means non-increasing.

Formalization targets

Goal: Corollary 4.2, display (4.7)

For every distribution $F$ on $[0,\infty)$ , every $\lambda > 0$ and every threshold $x$ ,

\bar H(t) = \sum_{k=0}^\infty e^{-\lambda t}\frac{(\lambda t)^k}{k!} F^{(k)}(x) \quad \text{is IHRA.}

This is the first of the three statements of Corollary 4.2; the second ((4.7a), independent damages $F_i$ that worsen with $i$ ) is an extra item of this mission, and the third ((4.7b), dependent damages satisfying (4.3)–(4.5)) belongs to mission III of this series.

Milestones

(2.6): $\bar H(t) \ge \bar H(0)e^{-\lambda t}$ for $t \ge 0$ .
Theorem 3.1 (3.4) through the three claims of its proof (p. 633): if $1 = \bar P_0 \ge \bar P_1 \ge \dots$ and $\bar P_k^{1/k}$ is decreasing in $k \ge 1$ , then $\bar P_k - \zeta^k$ ( $0 \le \zeta \le 1$ ) has at most one sign change, from $+$ to $-$ ; this property passes to $\bar H(t) - e^{-(1-\zeta)\lambda t}$ on $t \ge 0$ ; hence $\bar H(t) - e^{-\theta t}$ has at most one sign change for every $\theta > 0$ ; and $H$ is IHRA.
Lemma 4.1: for $F$ on $[0,\infty)$ , $[F^{(k)}(x)]^{1/k}$ is decreasing in $k = 1, 2, \dots$ .

Further items

Lemma 4.1a and Corollary 4.2 (4.7a); Theorem 4.4 ( $[F^{(k)}(x)]^{1/k}$ is constant in $k$ iff $F$ has no mass in $(0,x]$ ); Corollary 4.5 ((4.7) is exponential iff $F$ has no mass in $(0,x]$ ); Corollary 4.11 ( $[P\{N(x) \ge k\}]^{1/k}$ is decreasing for the count $N(x)$ of an ordinary renewal process).

Significance

The goal turns a modelling assumption into a theorem: anyone who models failure as accumulated nonnegative damage under Poisson shocks obtains, without further checks, every consequence of IHRA proved in reliability theory, including the closure of the class under the formation of coherent systems. Theorem 3.1 (3.4) is reusable on its own: it reduces the IHRA property of any Poisson mixture to a discrete condition on the $\bar P_k$ , and the same scheme drives the first passage result for wear processes (Theorem 4.10, mission III). Lemma 4.1, applied to renewal processes, gives Corollary 4.11, a statement about renewal counts with no shock model in sight.

All results are proved in the paper; none has a machine-checked proof that we know of. The Mathlib library has the Poisson distribution and the convolution of measures, but no reliability classes, no total positivity and no variation diminishing property. The mission's output is a formal proof of the paper's chain of results and, along the way, reusable statements about Poisson mixtures and convolution powers.

Difficulty

Two steps resist a direct argument. The first is the transfer from sequences to functions: knowing that $\bar P_k - \zeta^k$ changes sign at most once says nothing pointwise about the series $\sum_k(\bar P_k - \zeta^k)K(k,t)$ . The paper invokes the variation diminishing property of the totally positive Poisson kernel (Karlin, Total Positivity, 1968), which is not in Mathlib. The second is Lemma 4.1, an inequality between convolution powers of an arbitrary law: no density, moments or continuity may be assumed, atoms at $0$ and at $x$ are allowed, so any argument through densities or Laplace transforms loses generality. A further subtlety is the passage from "one sign change of $\bar H(t) - e^{-\theta t}$ for every $\theta$ " to the monotonicity of $[\bar H(t)]^{1/t}$ , which needs care where $\bar H$ vanishes.

Formalization scope

A distribution $F$ with $F(z) = 0$ for $z < 0$ is a probability measure $\mu$ on $\mathbb R$ with $\mu(-\infty,0) = 0$ ; nothing else is assumed. $F^{(k)}$ is the $k$ -fold additive convolution of $\mu$ (Mathlib's Measure.conv) starting from the point mass at $0$ , and $F^{(k)}(x)$ is the real number $F^{(k)}(-\infty,x]$ .
$\bar H$ is the series (2.1) as a function on $\mathbb R$ , equal to $1$ on $t < 0$ . It is never defined through a constructed random failure time, and IHRA is never encoded through a condition on the $\bar P_k$ : the goal concludes that $[\bar H(t)]^{1/t}$ is decreasing on $t > 0$ for the series itself. This rules out the trivializing reading in which the goal unfolds to Lemma 4.1.
Powers $[\bar H(t)]^{1/t}$ and $\bar P_k^{1/k}$ are real powers with exponent $1/t$ , $1/k$ in $\mathbb R$ .
Hypotheses the paper leaves implicit and the Lean statements make explicit: $\lambda > 0$ ; $\bar P_k \ge 0$ (the $\bar P_k$ are probabilities); in Corollary 4.5, $x \ge 0$ (the threshold is a capacity), and "exponential" includes the degenerate rate $0$ .
Sign change statements about $\bar H$ hold on $t \ge 0$ , where the series defines it.
The threshold $x$ in the goal ranges over all reals, as printed.
In Corollary 4.11 the renewal process is given by independent measurable interarrival times with common law $\mu$ , and $N(x) = \#\{k \ge 1 : X_1 + \dots + X_k \le x\}$ takes values in $\{0, 1, \dots, \infty\}$ .

A complete development needs: the variation diminishing property of the Poisson kernel (reusable for every Poisson mixture), monotonicity of $[F^{(k)}(x)]^{1/k}$ via convolution integrals, and elementary facts about real powers and sign changes. Proofs of any milestone or extra item, and general total positivity lemmas, are welcome.

Selected references

J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, The Annals of Probability 1(4) (1973) 627–649. https://doi.org/10.1214/aop/1176996891
Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-Out for Components and Systems, The Annals of Mathematical Statistics 37 (1966) 816–825. https://doi.org/10.1214/aoms/1177699362
S. Karlin, Total Positivity, Vol. I, Stanford University Press, 1968.
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965. https://doi.org/10.1137/1.9781611971194

8 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints 1: Under Normality, the E-Model Chance Constraints Are Equivalent to the Convex Program (29)Research Paper

Motivation

Chance-constrained programming replaces a linear program $\max c'x$ subject to $Ax\le b$ by a problem in which some data are random and each constraint only has to hold with a prescribed probability. Charnes and Cooper introduced the idea in 1959 for scheduling heating-oil production against weather-dependent demand, and the formulation is now a standard modelling tool in operations research, finance, energy systems and engineering design (Charnes and Cooper 1959; Prékopa 1995).

A chance-constrained problem is not directly solvable: its constraints are probabilities of events that depend on the decision. The 1963 paper of Charnes and Cooper (doi:10.1287/opre.11.1.18) asks when such a problem has a deterministic equivalent, an ordinary mathematical program with the same feasible decisions and corresponding objective values, and when that equivalent is a convex program. Its first answer, for the expected-value ('E') model under linear decision rules and normality, is the subject of this mission. The resulting constraint form, a mean slack dominating $K_\alpha$ standard deviations, is an early instance of the second-order-cone reformulation of individual normal chance constraints used throughout modern stochastic and robust optimization.

Timeline. 1959: Charnes and Cooper, chance-constrained programming with the heating-oil model. 1963: this paper, deterministic equivalents for the E, V and P models under linear decision rules $x=Db$ . 1965: Miller and Wagner treat joint chance constraints with independent rows (doi:10.1287/opre.13.6.930). 1971: Prékopa's logarithmically concave measures give convexity of joint chance constraints under log-concave laws.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. The data are a constant $m\times n$ matrix $A$ with rows $a_1',\dots,a_m'$ , a random right-hand side $b:\Omega\to\mathbb R^m$ and random objective coefficients $c:\Omega\to\mathbb R^n$ . A linear decision rule is an $n\times m$ real matrix $D$ ; it chooses $x=Db$ after $b$ is observed. Write $\mu_b=Eb$ , $\mu_c=Ec$ and $\hat b=b-\mu_b$ .

The E-model (18) is

\max\ E(c'Db)\quad\text{subject to}\quad P(a_i'Db\le b_i)\ge\alpha_i\qquad(i=1,\dots,m),

with one probability level $\alpha_i$ per row: the constraints are row-wise, as in (3) of the paper, not a single joint constraint.

For $\tfrac12<\alpha<1$ let $K_\alpha=\Phi^{-1}(\alpha)>0$ be the standard normal $\alpha$ -quantile. With the moment functions (30),

\sigma_i^2(D)=E(a_i'Db-b_i)^2,\qquad \mu_i(D)=\mu_{b_i}-a_i'D\mu_b,

the paper's deterministic program (29) in the variables $(D,v)$ , $v\in\mathbb R^m$ , is

\min\ -\mu_c'D\mu_b\quad\text{s.t.}\quad \mu_i(D)-v_i\ge0,\quad -K_{\alpha_i}^2\sigma_i^2(D)+K_{\alpha_i}^2\mu_i^2(D)+v_i^2\ge0,\quad v_i\ge0 .

Formalization targets

Goal: (18) is equivalent to the convex program (29)

Assume every $b_k$ is square integrable, every $c_j$ and $c_jb_k$ integrable, $b$ and $c$ uncorrelated ( $E(c_jb_k)=E c_j\,E b_k$ ), every variate $a_i'Db-b_i$ normal (for every $D$ and $i$ , zero variance allowed), and $\tfrac12<\alpha_i<1$ . Then

\Big(\forall D:\ D\text{ feasible for (18)}\iff\exists v,\ (D,v)\text{ feasible for (29)}\Big)\ \wedge\ \Big(\forall D:\ E(c'Db)=\mu_c'D\mu_b\Big)\ \wedge\ \{(D,v)\ \text{feasible for (29)}\}\ \text{is convex}.

Milestones, in the order of the paper

(19a): $E(c'Db)=(Ec)'D(Eb)$ for uncorrelated $b$ , $c$ .
(22)–(27): with positive variance, $P(a_i'Db\le b_i)\ge\alpha_i\iff(-\mu_{b_i}+a_i'D\mu_b)/\sqrt{E[\hat b_i-a_i'D\hat b]^2}\le-K_{\alpha_i}$ .
(28a)–(28b): (27) holds iff some $v_i$ satisfies $\mu_{b_i}-a_i'D\mu_b\ge v_i\ge K_{\alpha_i}\sqrt{E[\hat b_i-a_i'D\hat b]^2}\ge0$ .
(28c)–(28d): for $v_i\ge0$ , that pair is equivalent to its squared form.
Footnote ‡ to (30): $\sigma_i^2(D)-\mu_i^2(D)=E[\hat b_i-a_i'D\hat b]^2$ .
The convexity paragraph after (30): the feasible set of (29) is convex in $(D,v)$ .
'V Model' (32)–(34): under the same normal chance assumptions and square integrability of each $c_jb_k$ , the chance constraints of (32) are equivalent to (33) for some $v$ ; the pair feasible set and $V(D)=E(c'Db-z^0)^2$ are convex.

Significance

The result. The theorem turns a problem whose constraints are probabilities into a finite-dimensional convex program whose data are the first two moments of $b$ and the means of $c$ . The optimal rules of (18) minimize (29), whose optimal value is the negative of the maximum in (18). The slack variables $v_i$ separate each constraint into a "quality" part (the mean slack $\mu_i(D)$ ) and a "risk" part ( $K_{\alpha_i}$ standard deviations), which is the interpretation the paper develops in (31) and its Appendix. The same constraint set serves the V-model (33), so only the objective changes between the two models.

Formalizing it. The result is classical and its proof is elementary, but the paper's argument is informal in ways that matter for a machine-checked version: it divides by a standard deviation it then allows to vanish, writes $F_i$ for what must be an upper-tail function, and labels a variance as $\sigma_i^2(D)$ while defining $\sigma_i^2(D)$ as a raw second moment. This mission produces a statement in which each of these points is settled, with every hypothesis explicit. No machine-checked version of the result is known to exist.

Difficulty

The chance-constraint step itself is a one-dimensional fact about the normal law, but three points need care. The variance of $a_i'Db-b_i$ may be zero for some $D$ and $i$ ; then the law is a point mass, the quotient in (27) is undefined, and the equivalence must be argued separately, as footnote † of p. 28 indicates. The quadratic constraint of (29) alone, $v_i^2\ge K_{\alpha_i}^2(\sigma_i^2(D)-\mu_i^2(D))$ , describes both nappes of a hyperboloid and is not convex; convexity needs $v_i\ge0$ and the positive semidefiniteness of $D\mapsto\operatorname{Var}(a_i'Db-b_i)$ , which comes from square integrability of $b$ and not from normality. Finally, the identity relating $\sigma_i^2$ , $\mu_i^2$ and the variance requires the integrals to be genuine, so the integrability hypotheses cannot be dropped.

Formalization scope

Everything is in the namespace ChanceDetEquiv.EModel. The probability space is (Ω, P) with [IsProbabilityMeasure P]; A : Matrix (Fin m) (Fin n) ℝ, b : Ω → Fin m → ℝ, c : Ω → Fin n → ℝ, D : Matrix (Fin n) (Fin m) ℝ; $a_i'Db$ is (A *ᵥ (D *ᵥ b ω)) i. Expectations are Bochner integrals and probabilities are P.real. Explicit readings of the paper's phrases:

"deterministic equivalent for (18)" is the conjunction of an iff between feasible sets (with the auxiliary $v$ existentially quantified) and $E(c'Db)=\mu_c'D\mu_b$ for every $D$ ; (29) minimizes the negative of this mean;
"is a convex programming problem" is Convex ℝ of the feasible set of (29) in $(D,v)$ , $v_i\ge0$ included; for the V model it also asserts ConvexOn ℝ of $V$ ;
"normally distributed" is: for every $D$ and $i$ , the law of $a_i'Db-b_i$ is gaussianReal μ s for some $\mu$ and $s\ge0$ ; joint normality of $b$ is not assumed, since it would be a stronger hypothesis;
" $b$ and $c$ are uncorrelated" is $E(c_jb_k)=E c_j\,E b_k$ for all $j,k$ ;
$K_\alpha=\Phi^{-1}(\alpha)$ , using the published definition Cohen2019_Robust_Phi; $F_i$ in (26)–(27) is read as the upper-tail function of $z_i$ , and $\alpha_i<1$ is added so that $K_{\alpha_i}$ is finite;
$\sigma_i^2(D)$ is the raw second moment exactly as printed in (30).

Positive variance is a hypothesis of milestones 2 and 3, where (27) has a denominator. The goal and later milestones admit zero variance. The statements admit no trivializing reading: the normality hypothesis is satisfied by constant and by Gaussian $b$ , the integrability hypotheses rule out the junk value $0$ of non-integrable expectations, and $\alpha_i<1$ rules out the junk value of $\Phi^{-1}(1)$ .

A complete development needs: the normal CDF and quantile, the law of an affine image of a random variable, variance as $E X^2-(EX)^2$ in $L^2$ , and convexity of the epigraph of a seminorm composed with an affine map. The convexity milestones need no probability beyond $L^2$ and are reusable for any second-order-cone representation of individual chance constraints. Proofs of any milestone, and of the goal from the milestones, are welcome.

The related open platform item KallMayer.Chance.chapter2_theorem2_5 (convexity of a single normal chance-feasible set in $x$ ) is credited here and not restated: no item of this mission states the convexity of the set of $D$ feasible for (18). Related published items that are about other models: DRCVRP.RCI.prob_le_iff_valueAtRisk_le (chance constraints and value-at-risk for a general law) and the log-concavity results of NumStochOpt.LogConcave.

Selected references

A. Charnes and W. W. Cooper, Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints, Operations Research 11(1), 1963, 18–39. https://doi.org/10.1287/opre.11.1.18
A. Charnes and W. W. Cooper, Chance-Constrained Programming, Management Science 6(1), 1959, 73–79. https://doi.org/10.1287/mnsc.6.1.73
A. Prékopa, Stochastic Programming, Kluwer, 1995. https://doi.org/10.1007/978-94-017-3087-7
P. Kall and J. Mayer, Stochastic Linear Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4419-7729-8

10 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

On Representatives of Subsets: Two Partitions into m Classes Have a Common System of Representatives When Any k Classes of One Meet at Least k Classes of the OtherResearch Paper

Motivation

Many assignment questions reduce to one combinatorial question: given finitely many sets, can one choose a different element from each? Workers are matched to jobs they are qualified for, rows of a matrix to columns with nonzero entries. The criterion for when this is possible is Hall's marriage theorem, first stated and proved by P. Hall in a five-page note in 1935 (DOI 10.1112/jlms/s1-10.37.26). It underlies bipartite matching, the integrality of the assignment polytope, the Birkhoff–von Neumann theorem on doubly stochastic matrices, and transversal theory in matroids.

Hall's note was written with a second question in view. In 1916 D. König proved, in the language of bipartite graphs, that if a set of $mn$ things is divided into $m$ classes of $n$ things in two ways, then one can choose $m$ things that represent every class of both divisions at once ("Über Graphen und ihre Anwendungen", Math. Annalen 77 (1916), 453). Van der Waerden (1927) and Sperner (1927) gave the set-theoretic form and a short proof. Hall's contribution was a criterion for a common system of representatives of two divisions in which the classes need not have equal sizes, obtained from the marriage theorem in two short steps.

Setting

Let $S$ be any set, finite or infinite, and let

T_1, T_2, \dots, T_m \tag{1}

be a finite system of subsets of $S$ . The sets $T_i$ may be infinite and need not be distinct; when one speaks of $k$ of the sets, $k$ indices are meant, so a repeated set is counted with multiplicity. A complete set of distinct representatives, or C.D.R., of (1) is a choice of pairwise distinct elements $a_1, \dots, a_m$ of $S$ with

a_i \in T_i \qquad (i = 1, \dots, m).

The system satisfies Hall's condition when any $k$ of the sets contain between them at least $k$ elements of $S$ , for $k = 1, \dots, m$ . The meet of all C.D.R.s, written $R$ , is the set of elements of $S$ that occur as a representative in every C.D.R. of (1).

A division of $S$ into classes is a family of pairwise disjoint sets $S_1, S_2, \dots$ whose union is $S$ . The paper writes $A \wedge B$ and $A \vee B$ for intersection and union; this mission writes $A \cap B$ and $A \cup B$ .

In Lean the system is T : ι → Set α over a finite index type, a C.D.R. is an injective a : ι → α with a i ∈ T i (IsCDR), Hall's condition is HallCondition, and the meet of all C.D.R.s is cdrMeet, all in the namespace HallReps.CDR.

Formalization targets

Goal: Theorem 3 (pp. 29–30)

Let $S$ be divided into $m$ classes in two ways, $S = S_1 \cup \dots \cup S_m = S_1' \cup \dots \cup S_m'$ , each a division into pairwise disjoint classes. If, for each $k$ , any $k$ of the classes $S_j'$ contain between them elements from at least $k$ of the classes $S_i$ , then for some permutation $\sigma$ of $\{1, \dots, m\}$ there are elements

a_i \in S_i \cap S'_{\sigma(i)} \qquad (i = 1, \dots, m).

The set $S$ and the classes may be infinite, and no class is assumed non-empty.

Milestones

Lemma (p. 27). If $a$ is a C.D.R. of (1) and $R$ is the meet of all C.D.R.s, the sets $T_i$ whose representative $a_i$ lies in $R$ contain between them exactly the elements of $R$ , and there are $|R|$ of them.
Induction step, p. 28. With (4) the system $T_1, \dots, T_{m-1}$ and $R^*$ the meet of its C.D.R.s: if $T_m \not\subseteq R^*$ , then (1) has a C.D.R.
Induction step, p. 29. If (4) has a C.D.R. and $T_m \subseteq R^*$ , then some $\rho + 1$ of the sets, including $T_m$ , have union exactly $R^*$ , where $\rho = |R^*|$ .
Theorem 1 (p. 27). Hall's condition is sufficient for a C.D.R. of (1).
Theorem 2 (p. 29). If $S$ is divided into any number of classes and any $k$ of the sets $T_i$ contain between them elements from at least $k$ classes, there are $a_i \in T_i$ lying in pairwise different classes.

A companion item states König's theorem (§1, p. 26), which the paper deduces from Theorem 3 on p. 30.

Significance

Theorem 3 gives a necessary and sufficient criterion for two partitions of a set into $m$ classes to admit a common system of representatives. Necessity is immediate, and the paper proves sufficiency. It contains König's theorem, and through it the statement that a regular bipartite multigraph has a perfect matching, as the case of equal class sizes. Hall remarks that R. Rado's generalization of König's theorem (1933) also follows. Theorem 2, the passage from "distinct elements" to "elements of distinct classes", is the form used for transversals of partitions and is the first instance of what later became the theory of common transversals and matroid intersection.

On the formal side, Hall's theorem for finite sets is in Mathlib as Finset.all_card_le_biUnion_card_iff_existsInjective' (in Mathlib/Combinatorics/Hall/Finite.lean), and the platform already has a proved equivalence for arbitrary sets with a finite index type (YogeshwaranDM.sdr_iff, included in this mission as a reference item) as well as finite bipartite-graph forms. For that reason Theorem 1 is a milestone and not the goal. What this mission adds is Hall's own proof structure, namely the meet of all C.D.R.s and the Lemma about it, which has not been formalized; Theorems 2 and 3 for divisions of a possibly infinite set; and König's theorem in its set-partition form. To our knowledge none of these statements has a machine-checked proof on the platform.

Difficulty

Theorem 3 does not follow from Theorem 1 applied to the classes $S_j'$ directly. Theorem 1 produces distinct elements, but the conclusion needs elements in distinct classes $S_i$ , and two distinct elements of $S_j'$ may lie in the same $S_i$ . The paper's route goes through Theorem 2, which allows any number of classes. That route needs Theorem 1 for systems whose sets can be infinite, because a single $T_i$ may meet infinitely many classes, so the finite-set version of Hall's theorem in Mathlib is not enough on its own. In Hall's own proof of Theorem 1, the work lies in the Lemma. It is an exchange statement about all C.D.R.s at once, whose object $R$ is defined by a universal quantifier over C.D.R.s, and it must be established over an arbitrary finite index type with possibly infinite sets.

Formalization scope

The ground set is a type α, with no finiteness or decidability assumed. The system (1) is T : ι → Set α with [Finite ι] (or Fin (m + 1) in the two induction steps, where the paper's $m$ is the Lean m + 1, its last set is T (Fin.last m), and (4) is fun i : Fin m => T i.castSucc).
Cardinalities of unions of the $T_i$ are Set.encard in ℕ∞, so an infinite union counts as infinite. Set.ncard is used only for subsets of Fin m, for the finite set $R^*$ (with its finiteness stated), and in König's theorem.
" $k$ of the sets" is a Finset ι of indices, so repeated sets count with multiplicity.
Divisions into classes are class maps: cls : α → κ in Theorem 2, with κ arbitrary, and p q : α → Fin m in Theorem 3 and König's theorem. A class map makes the classes cover $S$ and be pairwise disjoint by construction. Empty classes are allowed.
In Theorem 3 the permutation is existential and chosen together with the representatives. $a_i \in S_i \cap S'_{\sigma(i)}$ is p (a i) = i ∧ q (a i) = σ i.
Added or dropped hypotheses: the Lemma assumes a C.D.R. exists, as the page does (without one, cdrMeet is all of α). The first induction step omits the page's C.D.R. of (4), because its hypothesis already implies one. König's theorem adds $0 < n$ , which the page presumes and without which the statement is false.
The trivializing formalizations are ruled out. Typing the $T_i$ as Finset α would reduce Theorem 1 to Mathlib and lose the page's "It is not necessary that the sets $T_i$ shall be finite". Measuring unions by ncard would make Hall's condition fail exactly when a union is infinite. An infinite index type would make Theorem 1 and the Lemma false. None of these is used.
Useful contributions include proofs of the Lemma and of the induction steps, a proof of Theorem 1 either from them or from Mathlib's Hall theorem via a reduction to finite sets, and the reductions Theorem 1 → Theorem 2 → Theorem 3 → König.

Selected references

P. Hall, On representatives of subsets, J. London Math. Soc. 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
D. König, Über Graphen und ihre Anwendungen auf Determinantentheorie und Mengenlehre, Math. Annalen 77 (1916), 453–465. https://doi.org/10.1007/BF01456961
B. L. van der Waerden, Ein Satz über Klasseneinteilungen von endlichen Mengen, Abh. Math. Sem. Hamburg 5 (1927), 185–188. https://doi.org/10.1007/BF02952519
R. Rado, Bemerkungen zur Kombinatorik im Anschluss an Untersuchungen von Herrn D. König, Sitzungsber. Berliner Math. Ges. 32 (1933), 60–75.
Mathlib, Mathlib/Combinatorics/Hall/Finite.lean and Mathlib/Combinatorics/Hall/Basic.lean. https://github.com/leanprover-community/mathlib4

8 thms3 active usersReviewed

All missions

The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality I: P(√n sup(F − F̂ₙ) > λ) ≤ exp(−2λ²) for λ ≥ min(√(log 2/2), 1.0841 n^(−1/6))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

The d-Step Conjecture for Polyhedra of Dimension d < 6 1: The Bounded 5-Step Conjecture Holds, Every 5-Polytope with 10 Facets Has Diameter at Most 5, i.e. Δb(5, 10) = 5Research Paper

Motivation

Setting

Formalization targets

Goal: 4.3 THEOREM

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Some Monotonicity Results for Partially Observed Markov Decision Processes: MLR-Monotone Optimal Values and the Myopic Policy as a Lower Bound on the Optimal PolicyResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (myopic lower bound)

Milestone: Proposition 1 (MLR-monotone values)

Supporting milestones

Significance

Difficulty

Formalization scope

Selected references

Job Matching, Coalition Formation, and Gross Substitutes 1: Under Gross Substitutes the Salary-Adjustment Process Reaches a Discrete Core Allocation in Finitely Many RoundsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 1489)

Milestones, in the paper's order

Significance

Difficulty

Formalization scope

Selected references

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

Setting

Formalization targets

Goal: Theorem IV (p. 350)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Fritz John Necessary Optimality Conditions in the Presence of Equality and Inequality Constraints: Every Minimizer of a C¹ Program Admits Multipliers (ū₀, ū, v̄) ≠ 0 with ū ≥ 0Research Paper

Motivation

Setting

Formalization targets

Goal: the generalized Fritz John necessary conditions (p. 41)

Milestones

Companion results

Significance

Difficulty

Formalization scope

Selected references

The Data-Driven Newsvendor Problem: New Bounds and Insights I: The SAA Order Is ε-Optimal with Probability at Least 1 − 2exp(−Nε²min(b,h)/((18 + 8ε)(b + h)))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (improved LRS bound)

Milestones, in the order of the paper's proof

Significance

Difficulty

Formalization scope

Selected references

Factoring Polynomials with Rational Coefficients I: A Reduced Lattice Basis Satisfies |b_j|² ≤ 2^{n−1}·max|x_i|² for Any t Linearly Independent Lattice VectorsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition (1.12), p. 518

Milestones