Missions · Prove2Me

Completed

Analysis Control Theory Operations Research·Captain: mikedeng1

On Minimizing the Ruin Probability by Investment and Reinsurance II: Equation (5) for g = f′ Has a Unique Strictly Decreasing Solution on [0, ∞)Research Paper

Motivation

An insurance company whose surplus falls below zero is ruined. The probability of ruin is the classical measure of solvency risk in actuarial mathematics. A company can lower it in two ways: it can invest part of its surplus in a risky asset, and it can pass part of each claim to a reinsurer in exchange for part of the premium. Which mix of investment and reinsurance minimises the probability of ruin is a stochastic control problem. It is studied in risk theory and in applied probability, and it is a model case for control problems with jumps.

Hipp and Plum (2000) solved the problem with investment alone. They wrote down the Hamilton–Jacobi–Bellman (HJB) equation and showed that it has a smooth solution. H. Schmidli (2002) added proportional reinsurance. He proved a verification theorem (his Theorem 1) and an existence theorem (his Theorem 2) for the combined problem. This mission formalizes the existence theorem and the analytic statements it rests on.

Setting

Claims arrive as a Poisson process with rate $\lambda>0$ . The claim sizes $Y$ are independent with distribution function $G$ , where $G(0)=0$ and $G$ is continuous. The insurer collects premiums at rate $c>0$ . A risky asset follows a geometric Brownian motion with drift $\mu>0$ and volatility $\sigma>0$ . Under proportional reinsurance with retention level $b\in[0,1]$ , the insurer pays the fraction $bY$ of each claim and pays the reinsurer a premium at rate $c(b)$ . The function $c(b)$ is decreasing and continuous, $c(1)=0$ , $\liminf_{b\uparrow1}c(b)/(1-b)>0$ , and there is $\underline b>0$ with $c(b)>c$ for $b<\underline b$ and $c(b)\le c$ for $b\ge\underline b$ . In particular, full reinsurance costs more than the premium income.

Write $f$ for an unnormalised survival probability, with $f(u)=0$ for $u<0$ . The HJB equation (1) of the problem is

\sup_{b\in[0,1]}\sup_{A\ge0}\Big[\tfrac12\sigma^2A^2f''(u)+\big(c-c(b)+\mu A\big)f'(u)+\lambda\big(\mathbb E[f(u-bY)]-f(u)\big)\Big]=0 ,

where $A$ is the amount invested. Eliminating $A$ and substituting $g=f'$ turns (1) into the integral equation (5):

g(u)=\frac{1}{\dfrac{\mu^2}{2\sigma^2}\displaystyle\int_0^u\frac{dx}{D_g(x)}+\dfrac{c}{\lambda}},

D_g(x)=\inf_{b\in[0,1]}\Big[\lambda\Big(1-G(x/b)+\int_0^x\big(1-G((x-z)/b)\big)g(z)\,dz\Big)-\big(c-c(b)\big)g(x)\Big].

Condition (6) at $u$ is $D_g(u)>0$ . In Lean, ReinsPremium, ClaimLaw, tail, den ( $=D_g$ ), SolvesEq5On, H and SolvesHJB (equation (1)) live in the shared module SchmidliRuin.Verif.Setting; HasBoundedDensity, Cond6, SolvesEq3At and SolvesHJBAtZero live in SchmidliRuin.Exist.Setting.

Formalization targets

Goal: Theorem 2 (p. 900)

If $G$ has a bounded density, then

\exists!\ g:[0,\infty)\to\mathbb R\ \text{strictly decreasing, solving (5) on }[0,\infty).

Lean states this as two conjuncts: existence, and equality on $[0,\infty)$ of any two strictly decreasing solutions.

Milestones, in attack order

Lemma 3 (p. 894). For a solution $f$ of (3) on $[0,\eta)$ , the optimal retention is $b^*(u)=1$ for small $u$ : it is optimal not to reinsure small capital.
Lemma 4 (p. 898). Under a bounded density, (5) has a solution on some $[0,\varepsilon)$ , with $g(u)=\lambda/c-\alpha\sqrt u+o(\sqrt u)$ and $\alpha=\lambda\mu/(\sigma c^{3/2})$ .
Condition (6) near $0$ (pp. 898–899): such a local solution satisfies $D_g(u)>0$ for small $u>0$ .
Lemma 5 (p. 899). A decreasing solution on $[0,u_0)$ with (6) on $(0,u_0)$ extends to $[0,u_0]$ , and (6) holds at $u_0$ .
Continuation (proof of Theorem 2, p. 901). A solution with (6) on $(0,u_0]$ continues to $[0,u_0+\eta)$ with (6).
Theorem 1, second sentence (p. 896). For a decreasing solution $g$ of (5), $f(x)=1+\int_0^xg$ is a strictly increasing solution of (1), twice continuously differentiable on $(0,\infty)$ .
Theorem 1, last sentence (p. 896). There is at most one strictly increasing, twice continuously differentiable solution of (1) with $f(0)=1$ .

Significance

The existence theorem completes the dynamic-programming solution of the problem. By the verification theorem, $f=1+\int_0^\cdot g$ divided by $f(\infty)$ is the maximal survival probability $\delta(u)$ . The maximisers of the HJB equation define the optimal feedback strategy: the investment $A^*(u)=-\mu f'(u)/(\sigma^2f''(u))$ and the retention level $b^*(u)$ . Without Theorem 2 the verification theorem would be a statement about a function that might not exist. Equation (5) is also the basis of the paper's numerical scheme (§5), which iterates (5) to compute $\delta$ and the optimal strategies.

Theorem 2 has a published proof. As far as is known, none of the results above has a machine-checked proof, and nothing on Prove2Me states them. The work is to formalize the published argument. This takes the local existence result of Hipp and Plum, which the paper cites rather than reproves, and a continuation argument for a nonlinear Volterra-type equation whose kernel is an infimum over a control parameter. Milestones 6 and 7 are the purely analytic content of the verification theorem that the uniqueness part of Theorem 2 uses. The paper derives milestone 7 stochastically, and an analytic proof is equally welcome.

Difficulty

The denominator $D_g(x)$ vanishes at $x=0$ : $D_g(0)=\lambda-c\,g(0)=0$ , because $g(0)=\lambda/c$ . The integral in (5) is therefore improper at the origin. A Picard iteration started from a constant does not work, because it does not control $\int_0^u dx/D_g(x)$ . One needs the exact square-root rate $D_g(x)\asymp\sqrt x$ , and Lemma 4 obtains it only through Lemma 3 (no reinsurance near $0$ ) and the Hipp–Plum analysis of the reinsurance-free equation. Lemma 4's proof in the paper is a two-line citation, so a solver must formalize that local existence result.

The second difficulty is continuation. A solution can be continued as long as condition (6) holds, and Lemma 5 has to exclude that (6) degenerates at a finite endpoint. There the infimum over $b$ interacts with the vanishing of $g$ . The paper's argument uses a Gronwall estimate and the shape of $c(b)$ around $\underline b$ , and the minimiser $b$ in $D_g$ need not be unique or continuous.

Formalization scope

Model data. $c,\lambda,\mu,\sigma$ are real parameters, all strictly positive. The claim law is a probability measure $\nu$ on $\mathbb R$ , with $G=$ cdf ν, $\nu((-\infty,0])=0$ and $G$ continuous. "Bounded density" means $\nu$ has a measurable density with values in $[0,C]$ . $\mathbb E[h(u-bY)]$ is $\int h(u-by)\,d\nu(y)$ .
Premium. $c(b)$ is a real function, used on $[0,1]$ . The condition $\liminf_{b\uparrow1}c(b)/(1-b)>0$ is the lower bound $c(b)\ge\kappa(1-b)$ near $1$ , which is equivalent. A real-valued $c$ excludes the case $c(0)=\infty$ that the paper allows when $\mathbb E[Y]<\infty$ .
Conventions.
- $1-G(x/b)$ at $b=0$ is $\mathbb P[0\cdot Y>x]=0$ ; it is computed by tail, never by Lean's $x/0=0$ .
- " $g$ solves (5) at $u$ " includes that the integral exists: $g$ is integrable on $[0,u]$ , $D_g\ne0$ on $(0,u)$ , and $1/D_g$ is integrable on $[0,u]$ .
- Every supremum of the paper is a least upper bound (IsLUB … 0). Lean's sSup would return $0$ on an unbounded family, for example when $f''\ge0$ , and that would make " $f$ solves (1)" true by accident.
- Uniqueness is equality on $[0,\infty)$ . The values of $g$ off $[0,\infty)$ are free, so a unique-existence quantifier over $\mathbb R\to\mathbb R$ would be false.
- "Twice continuously differentiable" is read on $(0,\infty)$ , since $f''(0+)=-\infty$ (p. 895). At $u=0$ , (1) and (3) are taken in the boundary form $\sup_b[(c-c(b))f'(0)+\lambda(\mathbb E f(-bY)-f(0))]=0$ , with the right derivative $f'(0)$ .
- $\lambda$ and $c$ are general. §4 sets $\lambda=c=1$ by a change of units.
Trivialising readings ruled out.
- Encoding (5) with an unguarded $1/D_g$ would let a function with a vanishing denominator "solve" (5).
- Dropping the boundary equation at $u=0$ from Lemma 3 makes it false: a premium flat near $b=0$ admits local solutions with $b^*\equiv0$ .
Infrastructure needed.
- existence of the minimiser in $D_g$ and continuity of $D_g$ in $x$ ;
- a local existence theorem for singular integral equations in the style of Hipp–Plum;
- Gronwall's inequality (Mathlib has versions);
- Banach's fixed-point theorem (ContractingWith).
The continuation and closure lemmas (milestones 3–5) are reusable for other HJB equations of risk theory with a jump term. Contributions that state and prove intermediate claims of the paper's proofs are welcome as sub-results.

Selected references

H. Schmidli, On minimizing the ruin probability by investment and reinsurance, Ann. Appl. Probab. 12(3), 890–907, 2002. https://doi.org/10.1214/aoap/1031863173
C. Hipp and M. Plum, Optimal investment for insurers, Insurance Math. Econom. 27(2), 215–228, 2000. https://doi.org/10.1016/S0167-6687(00)00049-4
H. Schmidli, Optimal proportional reinsurance policies in a dynamic setting, Scand. Actuar. J. 2001(1), 55–68, 2001. https://doi.org/10.1080/034612301750077338
S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

10 thms2 active usersReviewed

Algebra Algebraic Geometry Convex Optimization+1·Captain: mikedeng1

Semidefinite Programming Relaxations for Semialgebraic Problems 1: A Polynomial System Has No Real Solution if and only if Its Degree-d Positivstellensatz SDP Is Feasible for All Large dResearch Paper

Motivation

Deciding whether a system of real polynomial equations, inequations and inequalities has a solution is the basic feasibility question behind nonconvex quadratic programming, polynomial optimization, robustness analysis in control, and combinatorial relaxations. Over the complex numbers, Hilbert's Nullstellensatz turns infeasibility into an algebraic identity whose bounded-degree instances are found by linear algebra. Over the reals this fails: $x^2+1=0$ has no real solution, yet $1$ is not in the ideal generated by $x^2+1$ .

The real substitute is the Positivstellensatz of Stengle (Stengle 1974; see Bochnak–Coste–Roy, Real Algebraic Geometry, Theorem 4.4.2): a real polynomial system is infeasible exactly when an identity $f+g^2+h=0$ holds, with $f$ built from sums of squares and the inequality constraints, $g$ a product of the inequation polynomials and $h$ in the ideal of the equations. Parrilo (2003), building on his thesis (2000), observed that once the degrees are bounded, the search for such an identity is a semidefinite program (SDP), because a polynomial is a sum of squares exactly when it has a positive semidefinite Gram matrix. This yields a hierarchy of SDPs that is sound at every level and complete in the limit, and it is the origin of the sum-of-squares (SOS) method used throughout polynomial optimization.

Timeline:

1974: Stengle proves the Positivstellensatz for semialgebraic sets over real closed fields.
1995: Choi, Lam and Reznick analyze the Gram matrix method for sums of squares.
2000–2003: Parrilo (thesis; Math. Program. Ser. B 96) formulates bounded-degree Positivstellensatz refutations as SDPs (Theorem 5.1); Lasserre (2001) develops the dual moment approach independently.

Setting

Write $\mathbb R[x_1,\dots,x_n]$ for real polynomials in $n$ variables. Fix three finite, possibly empty, families: $f_1,\dots,f_s$ (inequalities), $g_1,\dots,g_t$ (inequations), $h_1,\dots,h_u$ (equations). They define the basic semialgebraic set

K=\{x\in\mathbb R^n \mid f_j(x)\ge 0,\ g_k(x)\ne 0,\ h_\ell(x)=0\ \text{for all } j,k,\ell\}.\qquad(4.4)

A cone of $\mathbb R[x_1,\dots,x_n]$ is a subset closed under addition and multiplication that contains every square $a^2$ ; $P(S)$ is the smallest cone containing $S$ , and $P(\emptyset)$ is the set of sums of squares. $M$ is the multiplicative monoid generated by the $g_k$ (with the empty product $1$ ), and $I$ is the ideal generated by the $h_\ell$ .

For a degree bound $D$ , let $z$ be the vector of all monomials $x^\alpha$ of total degree at most $D$ ; it has $\binom{n+D}{D}$ entries. For a real matrix $Q$ indexed by these monomials, the Gram polynomial is $z^TQz=\sum_{\alpha,\beta}Q_{\alpha\beta}x^\alpha x^\beta$ .

The degree- $d$ Positivstellensatz SDP $\mathrm{SDP}_d$ : with $G=\sum_k\deg g_k$ and $N(d)=d(2G+1)$ , find positive semidefinite matrices $Q_T$ over the monomials of degree at most $N(d)$ , one for each $T\subseteq\{1,\dots,s\}$ , and polynomials $q_\ell$ of degree at most $2N(d)$ , such that

\sum_{T}(z^TQ_Tz)\prod_{j\in T}f_j+\Big(\prod_{k=1}^t g_k^{2d}\Big)^2+\sum_{\ell=1}^u q_\ell h_\ell=0 .

Its unknowns are finitely many real numbers, the constraint is linear in them, and the matrices are constrained to be positive semidefinite.

Formalization targets

Goal: Theorem 5.1

\big(\forall d,\ \mathrm{SDP}_d\ \text{feasible}\Rightarrow K=\emptyset\big)\quad\text{and}\quad\big(K=\emptyset\Rightarrow\exists d_0\ \forall d\ge d_0,\ \mathrm{SDP}_d\ \text{feasible}\big).

The first half says every feasible point is a refutation; the second says the hierarchy is complete once the degree bound is large enough. No bound on $d_0$ is asserted, matching the paper.

Milestones

Theorem 4.6, $2\Rightarrow1$ : an identity $f+g^2+h=0$ with $f\in P$ , $g\in M$ , $h\in I$ forces $K=\emptyset$ .
A positive semidefinite Gram matrix gives a sum of squares (§3.2).
Theorem 4.6, $1\Rightarrow2$ (Stengle's Positivstellensatz): $K=\emptyset$ forces such an identity.
$P(\emptyset)$ is the set of sums of squares and the smallest cone; the finite-generator form $P(S)=\{p+\sum_i q_ib_i\}$ ; the squarefree form $\sum_T p_T\prod_{j\in T}f_j$ of the cone used in the proof of Theorem 5.1.
A sum of squares of degree at most $2d$ has a positive semidefinite Gram matrix over the monomials of degree at most $d$ ; Theorem 3.3 combining both directions with the size $\binom{n+d}{d}$ ; the count $\binom{n+d}{d}$ of the monomial vector.

Significance

Theorem 5.1 is the statement that makes Positivstellensatz certificates computable: it converts an existence theorem of real algebraic geometry into a sequence of convex feasibility problems, each solvable by interior-point methods, and any solution is an exact proof of infeasibility. Lower bounds in polynomial optimization (Example 5.4), the copositivity tests of §7.5, SOS relaxations for MAX-CUT and stable sets, and Lyapunov-function searches in control are all instances of this scheme.

The paper proves only the soundness direction of the Positivstellensatz and cites the converse. A complete formal development therefore contains the first machine-checked statement chain from Stengle's theorem to the SDP hierarchy. To the best of current searches, neither Mathlib nor Prove2Me contains the real Positivstellensatz, the Gram matrix characterization of sums of squares, or the monomial count; Mathlib has sums of squares in rings (IsSumSq), positive semidefinite matrices, and the complex Nullstellensatz.

Difficulty

The soundness half is elementary. Completeness rests on Stengle's Positivstellensatz, whose standard proofs pass through real closed fields, orderings of rings and the Tarski–Seidenberg transfer principle, none of which is available in Mathlib in usable form. A tempting shortcut, proving completeness by reasoning only about $\mathbb R$ -points, does not work: the certificate must be an algebraic identity, and points cannot produce it.

A second, smaller difficulty is degree bookkeeping. Each level of the hierarchy has a fixed shape (the exponent of the $g_k$ and the degree of every multiplier are tied to $d$ ), while a certificate supplied by the Positivstellensatz has arbitrary degrees and exponents. A Gram representation also needs a degree bound on every square in a sum of squares, not only on the sum.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ; $n,s,t,u$ are arbitrary natural numbers, including $0$ ; the families are indexed by Fin s, Fin t, Fin u. The set (4.4) lives in $\mathbb R^n$ = Fin n → ℝ.
$P(S)$ is the smallest set closed under $+$ , $\cdot$ and containing all squares (Definition 4.5), an inductive predicate. Mathlib's RingPreordering is not used: it excludes $-1$ , which an infeasible system's cone typically contains.
Sums of squares are IsSumSq; positive semidefiniteness is Matrix.PosSemidef (symmetric, which is the paper's $Q\in\mathcal S^n$ ); $M$ is Submonoid.closure, $I$ is Ideal.span.
The meta-claim "the search … can be done using semidefinite programming" is the definition of $\mathrm{SDP}_d$ : finitely many PSD Gram matrices indexed by a finite type of monomials, and ideal multipliers of bounded total degree. The degree choices ( $m=d$ in $g=\prod g_k^{2m}$ ; multiplier degree $d_2=2d(2G+1)$ ) fill the freedom the proof leaves and satisfy its printed bounds $d_2\ge d$ , $d_2\ge\deg g$ . "Large enough" is $\exists d_0\,\forall d\ge d_0$ .
A formalization without the degree bounds or with an infinite index type would make $\mathrm{SDP}_d$ equivalent to Theorem 4.6 item 2 and is ruled out; so is a goal stated for a fixed $n$ , for empty families only, or with soundness only at large $d$ .
Needed infrastructure: Stengle's Positivstellensatz over $\mathbb R$ (real closed field theory or a direct proof), the Gram matrix correspondence, and degree lemmas for sums of squares. The Positivstellensatz and the Gram correspondence are reusable far beyond this mission; contributions toward either are welcome.

Selected references

P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Math. Program. Ser. B 96 (2003) 293–320. https://doi.org/10.1007/s10107-003-0387-5
G. Stengle, A Nullstellensatz and a Positivstellensatz in semialgebraic geometry, Math. Ann. 207 (1974) 87–97. https://doi.org/10.1007/BF01362149
J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Theorem 4.4.2. https://doi.org/10.1007/978-3-662-03718-8
M. D. Choi, T. Y. Lam, B. Reznick, Sums of squares of real polynomials, Proc. Sympos. Pure Math. 58 (1995) 103–126. https://doi.org/10.1090/pspum/058.2/1327293
J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11 (2001) 796–817. https://doi.org/10.1137/S1052623400366802

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Centralized and Competitive Inventory Models with Demand Substitution 1: The Competitive Substitution Game Has a Nash Equilibrium, Unique and Globally Stable When Substitution Rates Sum Below OneResearch Paper

Motivation

A retailer that carries several substitutable products, such as brands of the same item or sizes of the same garment, must choose stock levels before demand is known. When a product runs out, some of its customers buy another product instead. Inventory models with this demand substitution go back to McGillivray and Silver (1978, INFOR 16(1)) and Parlar and Goyal (1984). When the products are run by different firms, each firm's stock affects the demand its competitors see, and stocking becomes a game. Parlar (1988) proved existence and uniqueness of the equilibrium for two products; Lippman and McCardle (1997) treated a symmetric version of the game with an arbitrary number of firms.

Netessine and Rudi (SSRN 303779, working paper 2002; journal version in Operations Research 51(2), 2003) treat $n$ products with a general joint demand distribution and general prices and costs, under both centralized and competitive management. This mission formalizes their analysis of the competitive game (§2.2): the first-order characterization of its Nash equilibria (Proposition 3) and the existence, uniqueness and global stability of the equilibrium (Proposition 4).

Setting

There are $n$ products, indexed $i=1,\dots,n$ , sold in a single period. Product $i$ is stocked at $Q_i\ge0$ units at unit cost $c_i$ , sold at unit price $r_i$ , and leftovers are salvaged at $s_i$ , with $r_i>c_i>s_i>0$ . Write $u_i=r_i-c_i$ (underage cost) and $o_i=c_i-s_i$ (overage cost).

The first-choice demand $D=(D_1,\dots,D_n)$ is a random vector with a known continuous joint distribution with positive support. A fraction $a_{ij}\in[0,1]$ of the customers who want product $i$ and find it out of stock buy product $j$ instead, with $a_{ii}=0$ and $\sum_{j}a_{ij}<1$ for every $i$ ; a customer whose second choice is also out of stock is lost. The effective demand for product $i$ is

D^s_i = D_i + \sum_{j\neq i} a_{ji}\,(D_j-Q_j)^+ ,

which depends on the other products' stocks $Q_{-i}$ but not on $Q_i$ .

In the competitive model, firm $i$ chooses $Q_i$ and earns the expected profit

\pi_i(Q_i,Q_{-i}) = E\big[u_iD^s_i - u_i(D^s_i-Q_i)^+ - o_i(Q_i-D^s_i)^+\big]. \tag{9}

A best response of firm $i$ to $Q_{-i}$ is a stock $Q_i\ge0$ maximizing $\pi_i(\cdot,Q_{-i})$ , and a Nash equilibrium is a stock vector from which no firm gains by deviating.

Formalization targets

Goal: Proposition 4

A Nash equilibrium exists, the equilibria are exactly the nonnegative solutions of the first-order conditions

\Pr(D_i<Q_i) - \Pr(D_i<Q_i<D^s_i) = \frac{u_i}{u_i+o_i},\qquad i=1,\dots,n, \tag{10}

and if either $\sum_{i}a_{ij}<1$ for all $j$ or $\sum_{j}a_{ij}<1$ for all $i$ , the equilibrium $Q^d$ is unique and globally stable: every sequence of simultaneous best responses started at any nonnegative stock vector converges to $Q^d$ .

Milestones

The derivative $\partial\pi_i/\partial Q_i = u_i-(u_i+o_i)\Pr(D^s_i<Q_i)$ (p. 8).
Concavity of $\pi_i$ in $Q_i$ (p. 8).
Proposition 3: a nonnegative stock vector is a Nash equilibrium if and only if it satisfies (10) (p. 8).
Each best response is unique and is characterized by (10) (proof of Proposition 4, p. 9).
The best response of firm $i$ is nonincreasing in the rivals' stocks, with slope in $Q_j$ at most $a_{ji}$ in absolute value (p. 9).
The simultaneous best-response map is Lipschitz with constant $\max_j\sum_i a_{ji}$ in the one-norm and $\max_i\sum_j a_{ji}$ in the infinity-norm (p. 9).

Significance

Proposition 4 makes the competitive equilibrium a well-defined object: a single stock vector, characterized by (10), which can be compared with the centralized optimum (the paper's Proposition 6) and which best-response adjustment reaches from any starting point. Without uniqueness, comparative statements about "the" competitive stocking level would be about an arbitrary selection.

The paper's argument has two gaps that this mission makes explicit. The proof asserts that best responses are single-valued because each profit is concave, and differentiates the best response using a density of $D^s_i$ ; the bound on the Jacobian is then stated in derivative form. The formal statements replace the derivative bounds by difference (Lipschitz) bounds, which need no differentiability, and state the positivity of the density on which single-valuedness rests. The paper also proves existence by citation to Lippman and McCardle; here existence is part of the goal. No machine-checked proof of these results is known.

Difficulty

The obvious route differentiates the best response implicitly, as the paper does. That requires $D^s_i$ to have a continuous, positive density at the equilibrium quantile, which is not a consequence of a continuous joint law: $D^s_i$ is a piecewise-linear function of $D$ , and its distribution function may have kinks. A second point is that concavity of $\pi_i$ alone does not make the best response unique: a demand law whose support has a gap gives $\pi_i$ a flat stretch and an interval of maximizers. Global stability must hold for every sequence of best responses, not for the iterates of one selected best-response function. Finally, the probabilities in (10) use strict inequalities, and their identification with $\Pr(D^s_i\le Q_i)$ uses that $D^s_i$ has no atoms, which needs a measure-theoretic argument about $D^s_i=D_i+g(D_{-i})$ under an absolutely continuous law.

Formalization scope

Products are indexed by Fin n (0-based). The model data and the standing assumptions $r_i>c_i>s_i>0$ , $a_{ij}\in[0,1]$ , $a_{ii}=0$ and $\sum_j a_{ij}<1$ are fields of a structure Model n. a i j is the share of $i$ 's unmet demand going to $j$ , so $D^s_i$ uses a j i. The demand law is a probability measure $\mu$ on $\mathbb R^n$ that is absolutely continuous with respect to Lebesgue measure, gives every coordinate a positive value almost surely, and has integrable coordinates; this is the reading of "a known continuous multivariate demand distribution with positive support". Expectations are Bochner integrals and probabilities are μ.real of events, with the strict and weak inequalities as printed.

The stocks range over $[0,\infty)^n$ , with no upper bound. A best response maximizes over $[0,\infty)$ ; a Nash equilibrium is defined by the absence of a profitable deviation, not by (10). Defining equilibria by (10) would make Proposition 3 and half of Proposition 4 true by definition, and is ruled out.

One hypothesis is added beyond the page and disclosed in every statement that uses it: $\mu$ has a Lebesgue density that is strictly positive on the open positive orthant. It is used for single-valued best responses, the slope and contraction bounds, and the goal; the derivative, concavity and Proposition 3 do not use it. In the goal, the second branch of the uniqueness condition, $\sum_j a_{ij}<1$ for all $i$ , coincides with the standing assumption of §2, so uniqueness always applies within the model; the disjunction is kept as printed. The paper's proof attaches the one-norm bound $\max_j\sum_i a_{ji}$ to the first branch, which is a column-sum condition on $a$ ; both branches are true, with the one-norm used for row sums and the infinity-norm for column sums.

A complete development needs: differentiation under the integral sign for piecewise-linear integrands, the absence of atoms of $D_i+g(D_{-i})$ under an absolutely continuous law, quantiles of strictly increasing continuous distribution functions, and the Banach fixed-point theorem on the closed nonnegative orthant (Mathlib's ContractingWith). The first two are reusable for every newsvendor model with substitution. Proofs of the milestones in any order are welcome.

Selected references

S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Simon School Working Paper OP 02-01, University of Rochester, April 2002, SSRN 303779. https://doi.org/10.2139/ssrn.303779
S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Operations Research 51(2):329–335, 2003. https://doi.org/10.1287/opre.51.2.329.12788
S. A. Lippman and K. F. McCardle, The Competitive Newsboy, Operations Research 45(1):54–65, 1997. https://doi.org/10.1287/opre.45.1.54
M. Parlar, Game Theoretic Analysis of the Substitutable Product Inventory Problem with Random Demands, Naval Research Logistics 35(3):397–409, 1988.
A. R. McGillivray and E. A. Silver, Some Concepts for Inventory Control under Substitutable Demand, INFOR 16(1):47–63, 1978.
M. Parlar and S. K. Goyal, Optimal Ordering Decisions for Two Substitutable Products with Stochastic Demand, OPSEARCH 21(1):1–15, 1984.
R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (Theorem 5.6.9).

8 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Centralized and Competitive Inventory Models with Demand Substitution 3: Under Multivariate Normal Demand the Centralized Expected Profit Decreases in Every Demand CorrelationResearch Paper

Motivation

A retailer that carries several substitutable products (brands of the same good, sizes of the same item) faces demands that are linked in two ways: a customer who finds the first-choice product out of stock may buy another one, and the first-choice demands themselves are statistically dependent. Inventory planners routinely assume multivariate normal demand and need to know how the dependence between demands affects what the assortment earns. In the single-product newsvendor and in classical risk-pooling arguments, positive correlation is known to hurt; with substitution it is not obvious, because substitution is itself a form of pooling whose value depends on whether two products run out together.

Netessine and Rudi (SSRN 303779, 2002; journal version in Operations Research 51(2), 2003) settle the question for the centralized model with an arbitrary number of products: under multivariate normal demand, the retailer's expected profit decreases in every demand correlation. The authors note that this effect had been observed numerically by Rajaram and Tang (working paper, UCLA, 1999) and Ernst and Kouvelis (1999) but not proved. They prove the analogous statement for each firm in the competitive model with stocking quantities held fixed.

Setting

There are $n$ products. Product $i$ is stocked in quantity $Q_i\ge 0$ at unit cost $c_i$ , sold at price $r_i$ , and salvaged at value $s_i$ , with $r_i>c_i>s_i>0$ . Write $u_i=r_i-c_i$ (underage cost) and $o_i=c_i-s_i$ (overage cost). The substitution fraction $a_{ij}\in[0,1]$ is the share of the unmet demand for product $i$ that switches to product $j$ ; $a_{ii}=0$ and $\sum_j a_{ij}<1$ .

The first-choice demand is a random vector $D=(D_1,\dots,D_n)$ . The effective demand of product $i$ , after substitution from the other products, is

D^s_i = D_i + \sum_{j\ne i} a_{ji}\,(D_j-Q_j)^+ ,\qquad x^+=\max(0,x).

For one realization, product $k$ earns

\pi_k(D) = u_kD^s_k - u_k(D^s_k-Q_k)^+ - o_k(Q_k-D^s_k)^+ ,

and a single centralized company owning all products earns $\pi(D)=\sum_k\pi_k(D)$ . The expected profits are $\pi(Q)=\mathbb E\,\pi(D)$ (the paper's equation (1)) and $\pi_k(Q)=\mathbb E\,\pi_k(D)$ (equation (9), the profit of firm $k$ when each product is owned by a separate firm).

In this mission $D\sim N(m,\Sigma)$ is multivariate normal with mean $m\in\mathbb R^n$ and positive semidefinite covariance matrix $\Sigma=(\sigma_{ij})$ . The correlation of products $i\ne j$ is $\rho_{ij}=\sigma_{ij}/\sqrt{\sigma_{ii}\sigma_{jj}}$ . Raising $\rho_{ij}$ means passing from $\Sigma^1$ to $\Sigma^2$ where $\sigma^2_{ij}=\sigma^2_{ji}\ge\sigma^1_{ij}=\sigma^1_{ji}$ and every other entry, in particular every variance, is unchanged.

A function $f:\mathbb R^n\to\mathbb R$ is supermodular if $f(x)+f(y)\le f(x\vee y)+f(x\wedge y)$ for the componentwise maximum and minimum, and submodular if $-f$ is supermodular. A random vector $D^1$ is smaller than $D^2$ in the supermodular order, $D^1\le_{sm}D^2$ , if $\mathbb Ef(D^1)\le\mathbb Ef(D^2)$ for every supermodular $f$ whose expectations exist.

Formalization targets

Goal: Proposition 2 (p. 7)

For $\Sigma^2$ obtained from $\Sigma^1$ by raising one covariance $\sigma_{ij}$ , $i\ne j$ ,

\pi^{\Sigma^2}(Q)\le\pi^{\Sigma^1}(Q)\quad\text{for every } Q\ge 0,

and, for every maximizer $Q^1$ of $\pi^{\Sigma^1}$ and every maximizer $Q^2$ of $\pi^{\Sigma^2}$ over $Q\ge0$ ,

\pi^{\Sigma^2}(Q^2)\le\pi^{\Sigma^1}(Q^1).

These are the two readings of "stocking quantities held fixed or adjusted optimally".

Milestones

The effective demand $h(D)=D_i+\sum_{j\ne i}a_{ji}(D_j-Q_j)^+$ is a valuation (both super- and submodular).
$D\mapsto\min(h(D),Q_i)$ is submodular.
The realized profit $\pi(D)=\sum_i[(u_i+o_i)\min(D^s_i,Q_i)-o_iQ_i]$ , and each $\pi_k(D)$ , is submodular in $D$ .
(Müller and Scarsini, quoted on p. 7) If $\sigma^1_{ii}=\sigma^2_{ii}$ and $\sigma^1_{ij}\le\sigma^2_{ij}$ for all $i,j$ , then

N(m,\Sigma^1)\le_{sm}N(m,\Sigma^2).

(Proposition 5, p. 10) For every firm $k$ and every fixed $Q\ge0$ , $\pi_k^{\Sigma^2}(Q)\le\pi_k^{\Sigma^1}(Q)$ .

Significance

The result. Proposition 2 says that, under normal demand, positive dependence between substitutable products is costly to the retailer whatever the substitution pattern, the number of products, and the cost parameters, and that re-optimizing the stocking levels cannot undo this. It turns an empirical regularity of numerical studies into a structural statement, and it gives a reason to prefer assortments of products whose demands are less correlated. Proposition 5 gives the same conclusion for each competing firm when stocking quantities are fixed; the paper does not claim it when firms re-optimize, since equilibrium quantities move in ways that need not favour every firm.

Formalizing it. The result is proved in the paper, partly by citation: the comparison of normal laws in the supermodular order is a theorem of Müller and Scarsini that is quoted, not proved, there. No machine-checked version of that comparison is known on the platform: the existing Slepian and Sudakov–Fernique comparisons concern expected suprema and tail probabilities, not expectations of arbitrary supermodular functions. A formal proof of milestone 4 would therefore be reusable well beyond inventory theory, wherever supermodular functionals of Gaussian vectors are compared (portfolio risk, dependence orderings, stop-loss premiums).

Difficulty

The deterministic steps (milestones 1–3) are elementary lattice arguments. The difficulty is milestone 4. The natural route is Gaussian interpolation: connect the two laws through $N(m,(1-t)\Sigma^1+t\Sigma^2)$ and differentiate $\mathbb Ef$ in $t$ . That argument needs $f$ twice differentiable with controlled growth, while the statement must hold for every supermodular $f$ that is merely integrable under the two endpoint laws, such as the piecewise-linear profits of this model, and for singular covariance matrices. Passing from smooth to general supermodular functions, without assuming integrability along the interpolation path, is where the work lies. The paper's own route to the "adjusted optimally" clause, a total derivative $d\pi/d\rho_{ij}$ along a differentiable optimal path, presumes a smoothness of the optimizer that is not available, since the expected profit need not be concave in $Q$ ; the goal is stated as a comparison of optimal values, which avoids it.

Formalization scope

All declarations live in DemandSubstitution.Correlation. Products are indexed by Fin n, 0-based. The model data and the standing assumptions $r_i>c_i>s_i>0$ , $a_{ij}\in[0,1]$ , $a_{ii}=0$ , $\sum_ja_{ij}<1$ form a structure Model n; $u_i$ and $o_i$ are definitions. The paper's §2 assumption that demand is continuous with positive support is dropped, as the paper drops it: a normal law charges negative demands. $N(m,\Sigma)$ is Mathlib's multivariateGaussian on EuclideanSpace ℝ (Fin n), pushed forward to Fin n → ℝ; every statement assumes both covariance matrices positive semidefinite, because Mathlib's construction returns a Dirac mass otherwise. Correlations are encoded through covariances with fixed variances, which is equivalent to raising $\rho_{ij}$ . "Decreasing" is weak. Expectations are Bochner integrals; the profit integrands are Lipschitz and integrable under every normal law, and this integrability is to be proved, not assumed. Supermodularity and the supermodular order reuse the platform definitions SupermodularOn and SupermodularOrder.

A trivializing formalization is ruled out: the Müller–Scarsini comparison is a milestone theorem, never a hypothesis of the goal or of Proposition 5, and the "adjusted optimally" clause quantifies over every pair of maximizers, not over one chosen optimizer.

Contributions welcome: integrability of Lipschitz functions under multivariateGaussian; Gaussian interpolation for supermodular functions; the supermodular comparison itself, which would be reusable on its own.

Selected references

S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Simon School Working Paper OP 02-01, 2002, SSRN 303779. https://doi.org/10.2139/ssrn.303779 (published in Operations Research 51(2):329–335, 2003, https://doi.org/10.1287/opre.51.2.329.12788)
A. Müller and M. Scarsini, Some remarks on the supermodular order, Journal of Multivariate Analysis 73(1):107–119, 2000. https://doi.org/10.1006/jmva.1999.1867
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
K. Rajaram and C. S. Tang, The impact of product substitution on retail merchandising, working paper, University of California, Los Angeles, 1999 (reference [16] of the source; no stable link).
D. M. Topkis, Minimizing a submodular function on a lattice, Operations Research 26(2):305–321, 1978. https://doi.org/10.1287/opre.26.2.305
R. Ernst and P. Kouvelis, The effects of selling packaged goods on inventory decisions, Management Science 45(8):1142–1155, 1999. https://doi.org/10.1287/mnsc.45.8.1142

9 thms2 active usersReviewed

Control Theory Functional Analysis Numerical Analysis+1·Captain: mikedeng1

The Primal-Dual Active Set Strategy as a Semismooth Newton Method V: Local Superlinear Convergence in L² under a Norm GapResearch Paper

Motivation

Optimal control problems with pointwise bounds on the control, such as

\min_u \tfrac12\|y - z\|_{L^2}^2 + \tfrac{\beta}{2}\|u\|_{L^2}^2 \quad\text{subject to } -\Delta y = u \text{ in } \Omega,\ y = 0 \text{ on } \partial\Omega,\ u \le \psi,

reduce, after eliminating the state, to a quadratic program in $L^2(\Omega)$ with a pointwise upper bound. The primal-dual active set strategy solves such problems by guessing the set where the bound is active, solving one linear system on that guess, and updating the guess from the new primal and dual values. It is used routinely in PDE-constrained optimization because each iteration costs one linear solve and, in practice, very few iterations are needed.

Hintermüller, Ito and Kunisch (SIAM J. Optim. 13 (2002) 865–888; authors' version hal-01660511) showed that this strategy is a semismooth Newton method for a nonsmooth reformulation of the optimality system, built on the notion of slant differentiability of Chen, Nashed and Qi (SIAM J. Numer. Anal. 38 (2000) 1200–1216). In finite dimension this gives local superlinear convergence (missions I–IV of this series). This mission concerns the paper's function-space result, Theorem 4.1: in $L^2(\Omega)$ , under a norm gap on the operator, the method still converges locally superlinearly. Ulbrich (SIAM J. Optim. 13 (2003) 805–841) developed a related semismooth Newton theory for superposition operators in function spaces, which also requires a norm gap.

Setting

Let $(\Omega, \mu)$ be a finite measure space (the paper takes a bounded domain $\Omega \subset \mathbb{R}^n$ with Lebesgue measure) and $L^p = L^p(\Omega)$ the real Lebesgue spaces, with inner product $(\cdot,\cdot)$ on $L^2$ . The paper writes $A$ for an operator and calligraphic $\mathcal{A}$ , $\mathcal{I}$ for active and inactive sets.

Slant differentiability (Definition 1). For Banach spaces $X$ , $Z$ , a map $F : X \to Z$ is slantly differentiable in an open set $U$ if there is $G : U \to \mathcal{L}(X, Z)$ , a slanting function, with

\lim_{h\to 0}\frac{1}{\|h\|}\,\|F(x+h) - F(x) - G(x+h)h\| = 0 \qquad (x \in U). \tag{A}

For $\delta \in \mathbb{R}$ , the candidate slanting function of the pointwise max is $G_m(y)(x) = 1$ if $y(x) > 0$ , $0$ if $y(x) < 0$ , $\delta$ if $y(x) = 0$ (4.1).

The problem. Given $f, \psi \in L^2$ and a self-adjoint $A \in \mathcal{L}(L^2)$ with

(Ay, y) \ge \gamma\|y\|^2 \quad (\gamma > 0), \tag{H1}

minimize $\tfrac12(y, Ay) - (f, y)$ subject to $y \le \psi$ . The solution $y^*$ and its multiplier $\lambda^*$ are the unique solution of

Ay^* + \lambda^* = f, \qquad \lambda^* - \max(0, \lambda^* + c(y^* - \psi)) = 0 \ \text{a.e.}, \tag{4.2}

for any fixed $c > 0$ . The norm gap hypothesis is

A = C + \beta I, \qquad C \in \mathcal{L}(L^2, L^q),\quad \beta > 0,\quad q > 2. \tag{H2}

The algorithm. From $(y^0, \lambda^0) \in L^2 \times L^2$ , set $\mathcal{A}_k = \{x : \lambda^k(x) + c(y^k(x) - \psi(x)) > 0\}$ , $\mathcal{I}_k = \Omega\setminus\mathcal{A}_k$ , and solve

Ay^{k+1} + \lambda^{k+1} = f, \qquad y^{k+1} = \psi \text{ on } \mathcal{A}_k, \qquad \lambda^{k+1} = 0 \text{ on } \mathcal{I}_k.

A sequence obeying this rule for every $k$ is a run. Superlinear convergence of $x^k \to x^*$ means $x^k \to x^*$ and, for every $\eta > 0$ , eventually $\|x^{k+1} - x^*\| \le \eta\|x^k - x^*\|$ .

Formalization targets

Goal: Theorem 4.1 (p. 15)

The page reads: "Assume that (H1), (H2) hold and that ψ and f are in L^q(Ω). Then the primal-dual active set strategy or, equivalently, the semismooth Newton method converge superlinearly if ‖y⁰ − y*‖ is sufficiently small and λ⁰ = β(y⁰ − ψ)." The formalized goal is the statement the proof establishes: with $c = \beta$ , there is $\rho > 0$ such that every run with

\|y^0 - y^*\|_{L^2} < \rho, \qquad \lambda^0 = f - Ay^0

converges superlinearly to $(y^*, \lambda^*)$ in $L^2 \times L^2$ . The initialization differs from the printed one; see Formalization scope.

Milestones

Theorem 1.1 (Chen–Nashed–Qi): slant differentiability near a zero $x^*$ with uniformly bounded $G(x)^{-1}$ gives local superlinear convergence of $x^{k+1} = x^k - G(x^k)^{-1}F(x^k)$ .
Proposition 4.1(ii): for $1 \le p < q \le \infty$ , $\max(0,\cdot) : L^q \to L^p$ is slantly differentiable with slanting function $G_m$ .
(4.9)–(4.10): for $c = \beta$ , (4.2) is equivalent to $\beta y^* - \beta\psi + \max(0, Cy^* - f + \beta\psi) = 0$ and $\lambda^* = f - Cy^* - \beta y^*$ .
Equivalence of the algorithms: along a run with $c = \beta$ and $\lambda^0 = f - Ay^0$ , $\lambda^k + \beta(y^k - \psi) = f - Cy^k - \beta\psi$ for all $k$ , so the active sets are those of the reduced algorithm.
Slant differentiability of the reduced map $F(y) = \beta y - \beta\psi + \max(0, Cy - f + \beta\psi)$ on $L^2$ , with $G_F(y+h) = \beta I + G_m(Cy - f + \beta\psi + Ch)C$ , $\delta = 1$ .
Bounded inverses: $G_F(z)$ is invertible on $L^2$ , with $\|G_F(z)^{-1}\|$ bounded uniformly in $z$ .

Two companion items accompany the goal: existence of a run from every $y^0$ , and Proposition 4.1(i), the paper's counterexamples showing that $G_m$ fails to be a slanting function from $L^p$ to $L^p$ .

Significance

Theorem 4.1 is the infinite-dimensional justification of a method used throughout control-constrained optimal control: it shows that the method converges locally superlinearly for the continuous problem itself, not only for each discretization. Example 1 of the paper shows that distributed control of the Poisson equation, and boundary control with Sobolev embeddings, satisfy (H2). Proposition 4.1 isolates the structural reason: the pointwise max is a Newton-differentiable map only between spaces with a norm gap.

None of these results is known to be machine-checked. A complete development would provide slant differentiability in Banach spaces, the Chen–Nashed–Qi local convergence theorem, the norm-gap differentiability of $\max(0,\cdot)$ between Lebesgue spaces, and invertibility of block operators on $L^2$ of a measurable partition. Each of these is reusable for other semismooth Newton analyses in function space.

Difficulty

The obvious argument fails at the max. In finite dimension, $\max(0,\cdot)$ is slantly differentiable with $G_m$ because a small perturbation does not change the sign of any nonzero component. In $L^2$ , a perturbation $h$ of small norm can flip the sign of $y$ on a set of positive measure, and on that set the error $\max(0, y+h) - \max(0, y) - G_m(y+h)h$ is as large as $|y|$ . Proposition 4.1(i) shows that this error is not $o(\|h\|_{L^p})$ in $L^p$ for any $p$ . Superlinear convergence in $L^2$ therefore needs the argument of the max to be controlled in a stronger norm than the error is measured in, which is what (H2) and $f, \psi \in L^q$ provide. A second difficulty is that the two-variable algorithm is not literally a Newton method for a map of $y$ alone; it must be identified with the reduced algorithm, and that identification depends on the initialization.

Formalization scope

Spaces. $L^p$ is Mathlib's Lp ℝ p μ on an arbitrary finite measure space; $q \in (2, \infty]$ is an extended real with 2 < q. The paper's bounded Lipschitz domain is replaced by a finite measure space: the proofs use only $|\Omega| < \infty$ , and Mathlib has no notion of Lipschitz boundary.
Pointwise statements on $L^p$ classes are almost everywhere statements about representatives. (H2) is stated as $Ay = Cy + \beta y$ a.e. for every $y \in L^2$ , which avoids building the inclusion $L^q \subseteq L^2$ .
Hypotheses kept: self-adjointness of $A$ , (H1) with explicit $\gamma > 0$ , (H2) with $\beta > 0$ and $q > 2$ , $f, \psi \in L^q$ . The solution $(y^*, \lambda^*)$ of (4.2) is a hypothesis; it exists and is unique under (H1), as the paper states on p. 12.
The initialization. The printed $\lambda^0 = \beta(y^0 - \psi)$ does not support the proof, which uses " $\lambda^0 + \beta(y^0 - \psi) = f - Cy^0 - \beta\psi$ " and $c = \beta$ . That identity holds exactly for $\lambda^0 = f - Ay^0$ . The goal uses $\lambda^0 = f - Ay^0$ and $c = \beta$ . With the printed initialization the first active set is $\{y^0 > \psi\}$ , and for $y^0$ slightly below $y^*$ the first iterate solves the unconstrained problem, which can be far from $y^*$ .
Superlinear convergence is stated for the pair $(y^k, \lambda^k)$ in the product norm $\max(\|y\|, \|\lambda\|)$ , without dividing by $\|x^k - x^*\|$ , so finite termination qualifies. "Sufficiently small" is an $\exists\rho > 0$ chosen before the run, on $\|y^0 - y^*\|$ only.
No trivialization. The goal mentions neither the reduced algorithm, nor $G_F$ , nor Proposition 4.1; the norm gap $q > 2$ is not weakened to $C \in \mathcal{L}(L^2)$ , under which Proposition 4.1(i) shows that $G_m$ need not be a slanting function; and the companion run_exists shows that the runs the goal quantifies over exist.
Definitions (PDASNewton.FunSpace.Setting): slanting functions, superlinear convergence, $G_m$ , property (A) for $\max(0,\cdot) : L^q \to L^p$ , system (4.2), one step and runs of the algorithm. These duplicate the finite-dimensional definitions of the other missions of the series in a separate namespace.

Proofs of any milestone are welcome, as are reusable lemmas on Lebesgue spaces (Hölder on sets of small measure, multiplication operators, Lax–Milgram on $L^2$ of a measurable subset).

Selected references

M. Hintermüller, K. Ito, K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3) (2002) 865–888. https://doi.org/10.1137/S1052623401383558 ; authors' version https://hal.science/hal-01660511
X. Chen, Z. Nashed, L. Qi, Smoothing methods and semismooth methods for nondifferentiable operator equations, SIAM J. Numer. Anal. 38 (2000) 1200–1216. https://doi.org/10.1137/S0036142999356719
M. Ulbrich, Semismooth Newton methods for operator equations in function spaces, SIAM J. Optim. 13 (2003) 805–841. https://doi.org/10.1137/S1052623400371569
L. Qi, J. Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275

9 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning II: The Gradient of the Normalized Discounted Value Is the Sum over Actions of ∇π·Q under the Discounted Future State DistributionTextbook

Why the gradient of the value matters

Policy gradient methods search a parameterized family of stochastic policies $\pi(a\mid s,\theta)$ , $\theta\in\mathbb R^k$ , by following the gradient of the policy's performance. They are the standard tool when the state space is too large for tabular dynamic programming and when a compact policy class (a neural network, a linear softmax) is easier to represent than a value function. Every such method rests on one identity: a formula for the gradient of the value with respect to $\theta$ that involves only quantities of the current policy, so that it can be estimated from the policy's own trajectories.

Chapter 4 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), states this identity in two settings, the $T$ -epoch undiscounted setting and the $\gamma$ -discounted setting, both in the thesis's normalized convention, in which values lie in $[0,1]$ . The thesis then uses the formula to analyse how many samples a gradient estimate needs (§4.2.3), and in §5.4.2 rewrites it in terms of advantages to explain why gradient methods can stall far from optimal: the gradient weights advantages by the current policy's state distribution, not by the distribution of an optimal policy.

Timeline:

1992: R. J. Williams introduces the likelihood-ratio (REINFORCE) estimator for episodic tasks.
2000: Sutton, McAllester, Singh and Mansour state the policy gradient theorem with function approximation, for discounted and average-reward criteria (NeurIPS 1999 proceedings, 2000); Konda and Tsitsiklis give actor-critic counterparts.
2001: Baxter and Bartlett analyse biased gradient estimation in the infinite-horizon setting.
2003: Kakade's thesis restates both theorems for normalized values, introduces the future state-time distribution $d_{\pi,s_0}$ for non-stationary $T$ -epoch policies, and draws the "mismeasure" consequence.

Setting

A finite MDP has a finite state set $S$ , a finite nonempty action set $A$ , a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ .

$T$ -epoch case. Epochs are $t\in\{0,\dots,T-1\}$ , $T\ge1$ . A non-stationary policy chooses $a$ at epoch $t$ in state $s$ with probability $\pi(a\mid s,t)$ . Starting from $s_0$ , $\Pr(s_t=s\mid\pi,s_0)$ is the probability of being in $s$ at epoch $t$ . The normalized $t$ -value is

V_{\pi,t}(s)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\,\Big|\,\pi,s_t=s\Big],\qquad V_\pi=V_{\pi,0},

the $t$ state-action value is $Q_{\pi,t}(s,a)=\frac1T r(s,a)+\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_{\pi,t+1}(s')]$ with $V_{\pi,T}=0$ , and the future state-time distribution on $S\times\{0,\dots,T-1\}$ is $d_{\pi,s_0}(s,t)=\frac1T\Pr(s_t=s\mid\pi,s_0)$ .

Discounted case. For a stationary policy $\pi(a\mid s)$ and $0\le\gamma<1$ , the normalized value, state-action value, advantage and discounted future state distribution are

V_{\pi,\gamma}(s)=(1-\gamma)\,\mathbb E\Big[\sum_{\tau\ge0}\gamma^\tau r(s_\tau,a_\tau)\,\Big|\,\pi,s_0=s\Big],\qquad Q_{\pi,\gamma}(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[V_{\pi,\gamma}(s')],

A_\pi(s,a)=Q_{\pi,\gamma}(s,a)-V_{\pi,\gamma}(s),\qquad d_{\pi,s_0,\gamma}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,s_0).

A parameterized policy is a family $\pi(a\mid s,\theta)$ (resp. $\pi(a\mid s,t,\theta)$ ) of policies indexed by $\theta\in\mathbb R^k$ , each entry differentiable in $\theta$ ; $\nabla$ is the gradient in $\theta$ .

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

\nabla V_{\pi,\gamma}(s_0)=\frac1{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\Big[\sum_a\nabla\pi(a\mid s,\theta)\,Q_{\pi,\gamma}(s,a)\Big].

The statement asserts that $\theta\mapsto V_{\pi_\theta,\gamma}(s_0)$ is differentiable at the given parameter and that its derivative is the right-hand side. It is the thesis's version of the Sutton–McAllester–Singh–Mansour theorem, and the result the rest of the thesis's discussion of gradient methods builds on.

Milestones

Value representations (p. 47): $V_\pi(s_0)=\mathbb E_{(s,t)\sim d_{\pi,s_0}}\mathbb E_{a\sim\pi(\cdot\mid s,t)}[r(s,a)]$ and $V_{\pi,\gamma}(s_0)=\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\mathbb E_{a\sim\pi(\cdot\mid s)}[r(s,a)]$ .
Theorem 4.2.3 (p. 48), the $T$ -epoch gradient:

\nabla V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi,s_0}}\Big[\sum_a\nabla\pi(a\mid s,t,\theta)\,Q_{\pi,t}(s,a)\Big].

The advantage form (§5.4.2, p. 66), with $A=|A|$ the number of actions:

\nabla V_\pi(s_0)=\frac{A}{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0}}\,\mathbb E_{a\sim\mathrm{Uniform}}\big[A_\pi(s,a)\,\nabla\pi(a\mid s,\theta)\big].

Significance

The result. The gradient formula contains no derivative of the state distribution: the effect of $\theta$ on which states are visited cancels, and the gradient is an expectation over states drawn from the current policy, weighted by a sum over actions. This is what makes Monte Carlo and actor-critic estimators possible, and it is the reason the thesis's sample-size analysis of §4.2.3 has no dependence on the size of the state space. The advantage form makes the limitation equally explicit: a small gradient certifies small advantages only under $d_{\pi,s_0}$ , while the performance difference lemma (Lemma 5.2.1) shows that closeness to optimal is governed by advantages under $d_{\pi^*,s_0}$ . That gap motivates the conservative policy iteration of Chapter 7.

Formalizing it. The theorems are proved in the thesis and in the cited literature; none of them is machine-checked in this normalized convention. The platform has a proved finite-horizon policy gradient theorem for a scalar parameter, a stationary policy and unnormalized values (policy_gradient_discounted_finite, policy_gradient_finite_horizon), and a posed direct-parameterization gradient for Agarwal et al.'s unnormalized discounted value (PolicyGradTheory.ProjGA.direct_gradient). This mission adds the multi-parameter statements, the non-stationary $T$ -epoch version with its state-time distribution, and the infinite-horizon discounted version, where differentiability of an infinite series must be established rather than computed from a finite recursion.

Difficulty

In the $T$ -epoch case the value is a finite polynomial in the policy entries, and the work is bookkeeping: unrolling the backward recursion for $V_{\pi,t}$ against the forward recursion for $\Pr(s_t=\cdot)$ so that the terms involving $\nabla V_{\pi,t+1}$ telescope. In the discounted case the obvious route, differentiating the recursion $V=(1-\gamma)r_\pi+\gamma P_\pi V$ term by term and recursing forever, presupposes that $\theta\mapsto V_{\pi_\theta,\gamma}(s)$ is differentiable, which the thesis's proof takes for granted. The value is an infinite series in $t$ , so that differentiability is a genuine part of the claim, and the resulting formula must be matched with $d_{\pi,s_0,\gamma}$ and $Q_{\pi,\gamma}$ , which are themselves defined as infinite series.

Formalization scope

Finite $S$ and $A$ (Fintype), $A$ nonempty; transition kernel IsTransitionKernel P; rewards in $[0,1]$ as a standing hypothesis of every statement; $0\le\gamma<1$ ; $T\ge1$ . The thesis's later chapters allow infinite state spaces; this mission is finite.
Normalization exactly as in the thesis: $T$ -epoch values and $d_{\pi,s_0}$ carry $1/T$ , discounted values and $d_{\pi,s_0,\gamma}$ carry $1-\gamma$ . Hence the factors $T$ and $1/(1-\gamma)$ in the gradient formulas.
The discounted layer is the published normalized model ApproxOptRL.Shared.Model (value, qValue, advantage, futureStateDist; $d_{\pi,s_0,\gamma}$ is futureStateDist at the point mass on $s_0$ ). The $T$ -epoch layer is defined in this mission (TEpoch): 0-based epochs, tValue by backward recursion, tQValue, stateDist, stateTimeDist.
Parameters live in EuclideanSpace ℝ (Fin k). Every statement assumes that $\pi(\cdot\mid s,\theta)$ (resp. $\pi(\cdot\mid s,t,\theta)$ for $t<T$ ) is a probability distribution for every $\theta$ , and that each entry is differentiable at the parameter $\theta_0$ ("the derivatives $\nabla\pi$ exist", p. 48). Differentiability of the value is not assumed.
Gradients are stated with HasFDerivAt: the value map has the right-hand side as its Fréchet derivative at $\theta_0$ . A statement with fderiv of the value alone, or with a policy that does not depend on $\theta$ , would reduce to $0=0$ and is ruled out.
Expectations over finite sets are finite sums; the uniform expectation over actions is $\frac1{|A|}\sum_a$ .
Contributions welcome: the forward/backward recursion identity for $T$ -epoch values, summability and differentiability of the discounted series, and the closed form of $V_{\pi,\gamma}$ via $(I-\gamma P_\pi)^{-1}$ ; all are reusable by the other missions of this series.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 229–256, 1992. https://doi.org/10.1007/BF00992696
J. Baxter, P. L. Bartlett, Infinite-Horizon Policy-Gradient Estimation, Journal of Artificial Intelligence Research 15, 319–350, 2001. https://doi.org/10.1613/jair.806
V. R. Konda, J. N. Tsitsiklis, Actor-Critic Algorithms, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/6449f44a102fde848669bdd9eb6b76fa-Abstract.html

9 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Optimization+1·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning I: Approximate Policy Iteration with Max-Norm Evaluation Error ε Is Eventually Within 2ε/(1−γ)² of OptimalTextbook

Motivation

Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.

Setting

A finite discounted Markov decision process consists of a finite set of states $S$ , a finite nonempty set of actions $A$ , a transition kernel $P(s'\mid s,a)$ (for every $(s,a)$ a probability distribution over $S$ ), a deterministic reward $r(s,a)\in[0,1]$ , and a discount factor $0\le\gamma<1$ . A policy $\pi(a\mid s)$ is a probability distribution over actions for every state; a deterministic policy is a map $f:S\to A$ , identified with the policy that plays $f(s)$ with probability one.

Values are normalized: the value of $\pi$ at $s$ is

V_\pi(s)=(1-\gamma)\,\mathbb E\Big[\sum_{t\ge0}\gamma^t r(s_t,a_t)\,\Big|\,\pi,\ s_0=s\Big],

and the state-action value is $Q_\pi(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_\pi(s')]$ . With rewards in $[0,1]$ , every value lies in $[0,1]$ . An optimal policy $\pi^*$ has $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and state $s$ ; write $V^*=V_{\pi^*}$ and $Q^*=Q_{\pi^*}$ . The max norm is $\|x\|_\infty=\max_s|x(s)|$ on state vectors and $\max_{s,a}|x(s,a)|$ on state-action arrays.

The backup operator is $[BJ](s)=\max_a\big((1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[J(s')]\big)$ . A deterministic policy $f$ is greedy with respect to $Q$ if $f(s)\in\arg\max_a Q(s,a)$ for every $s$ .

$\gamma$ -approximate value iteration produces vectors $J_0=0,J_1,J_2,\dots$ with $\|J_t-BJ_{t-1}\|_\infty\le\varepsilon$ , and greedy policies $\pi_t$ for the lookahead $(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[J_t(s')]$ .
$\gamma$ -approximate policy iteration starts from any deterministic $\pi_0$ , forms an estimate $\tilde Q_t$ of $Q_{\pi_t}$ with $\|\tilde Q_t-Q_{\pi_t}\|_\infty\le\varepsilon$ , and takes $\pi_{t+1}$ greedy with respect to $\tilde Q_t$ .

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

\limsup_{t\to\infty}\|V^*-V_{\pi_t}\|_\infty\le\frac{2\varepsilon}{(1-\gamma)^2}.

The policies need not converge; the statement bounds where they end up.

Milestones

Theorem 3.1.1: if $\|\tilde Q-Q^*\|_\infty\le\varepsilon$ and $\pi$ is greedy for $\tilde Q$ , then $V_\pi(s)\ge V^*(s)-\frac{2\varepsilon}{1-\gamma}$ for all $s$ .
Lemma 3.2.3: $\|V^*-V_{\pi_{t+1}}\|_\infty\le\gamma\|V^*-V_{\pi_t}\|_\infty+\frac{2\varepsilon}{1-\gamma}$ .
Rate of approximate policy iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\gamma^t+\frac{2\varepsilon}{(1-\gamma)^2}$ .
Contraction of the backup (p. 26): $\|BJ-BJ'\|_\infty\le\gamma\|J-J'\|_\infty$ .
Approximate value iteration (p. 40): $\|V^*-J_t\|_\infty\le\gamma^t+\frac{\varepsilon}{1-\gamma}$ .
Rate of approximate value iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\frac{2\gamma^t}{1-\gamma}+\frac{2\varepsilon}{(1-\gamma)^2}$ .
Theorem 3.2.1: the same lim sup bound $\frac{2\varepsilon}{(1-\gamma)^2}$ for approximate value iteration.

Significance

The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of $\varepsilon$ in max norm costs at most $2\varepsilon/(1-\gamma)^2$ in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor $2\varepsilon/(1-\gamma)$ of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon $1/(1-\gamma)$ in the limit bound are the reason the thesis turns to other error measures in later chapters.

All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor $\gamma$ to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.

Difficulty

Approximate policy iteration is not monotone: with evaluation errors, $V_{\pi_{t+1}}$ can be worse than $V_{\pi_t}$ at some states, so the argument of exact policy iteration, which uses $V_{\pi_{t+1}}\ge V_{\pi_t}$ everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value $V_\pi$ is defined as an infinite series, so its Bellman equation $V_\pi(s)=Q_\pi(s,\pi(s))$ , the optimality equation $V^*=BV^*$ and the bound $0\le V_\pi\le1$ have to be derived from that definition before any of the recursions can be run.

Formalization scope

The model is the published normalized model ApproxOptRL.Shared.Model: value P r γ π is $V_\pi$ (defined as $(1-\gamma)$ times a tsum), qValue is $Q_\pi$ . $S$ and $A$ are finite types, $A$ nonempty; $P$ satisfies IsTransitionKernel; every statement assumes $0\le r\le1$ and $0\le\gamma<1$ .
The optimal policy is a binder $\pi^*$ with IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.
Policies of the runs are deterministic, S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.
The runs are sequences indexed by ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices $t+1$ and $t$ .
$\|\cdot\|_\infty$ is Mathlib's sup norm on S → ℝ and S → A → ℝ.
The lim sup statements are in $\varepsilon$ – $N$ form: for every $\delta>0$ the bound plus $\delta$ holds eventually.
Ruled out: the accuracy hypothesis is stated against $Q_{\pi_t}$ , the value of the current policy, not against $Q^*$ , and the greedy relation genuinely constrains $\pi_{t+1}$ ; with either changed, the hypotheses would be unsatisfiable or the policies unconstrained and the theorem empty.
Infrastructure needed and reusable beyond this mission: the Bellman equation of the normalized value for indicator policies, $V^*=BV^*$ , monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound $0\le V_\pi\le1$ . Contributions of these lemmas are welcome.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996. ISBN 1-886529-10-8.
S. P. Singh and R. C. Yee, An upper bound on the loss from approximate optimal-value functions, Machine Learning 16 (1994), 227–233. https://doi.org/10.1007/BF00993104
S. M. Kakade and J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005

13 thms2 active usersReviewed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion 2: With Random Objective, Z(x) = Z_D(x) = Z_DD(x) and Moment-Matching Distributions Attain Z(x) AsymptoticallyResearch Paper

Motivation

Two-stage stochastic linear programming chooses a first-stage decision $x$ before a random parameter is revealed and pays an optimal second-stage (recourse) cost afterwards. The classical model fixes the distribution of the random parameter. In practice it is rarely known beyond a few moments, and a decision maker who is averse to risk does not evaluate the recourse cost by its plain expectation. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) take both points seriously: the distribution is only known to belong to the class of all distributions with given mean and second-moment matrix, the cost is passed through a convex piecewise-linear disutility, and the decision is evaluated against the worst distribution in the class.

Moment-based worst-case bounds go back to Scarf's newsvendor and to the Chebyshev-type bounds of the moment problem (Isii 1962; Bertsimas and Popescu 2005). Delage and Ye (Oper. Res. 58(3), 2010) showed that a broad class of such minimax problems is solvable in polynomial time by the ellipsoid method. For the case in which the uncertainty sits in the objective of the second-stage linear program, this paper gives a single semidefinite program (its Theorem 2.1, the subject of a companion mission) and, in §2.2, identifies the distributions that come arbitrarily close to the worst case. This mission is about the second result.

Setting

The first-stage region is $X=\{x\in\mathbb R^n : Ax=b,\ x\ge0\}$ . For $x\in X$ the recourse set is $X(x)=\{w\in\mathbb R^d : Ww=h-Tx,\ w\ge0\}$ and the second-stage cost of an objective vector $q\in\mathbb R^d$ is

\mathcal Q(q,x)=\min_{w\in X(x)} q'w .

The disutility is $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge0$ . The moment class $\mathcal P$ consists of the distributions $P$ of a random vector $\tilde q\in\mathbb R^d$ with $\mathbb E_P[\tilde q]=\mu$ and $\mathbb E_P[\tilde q\tilde q']=Q$ . The worst-case value at $x$ is

Z(x)=\sup_{P\in\mathcal P}\mathbb E_P\big[\mathbb U(\mathcal Q(\tilde q,x))\big].

Its dual (6) is

Z_D(x)=\min_{Y,y,y_0}\ Q\cdot Y+\mu'y+y_0\quad\text{s.t.}\quad q'Yq+q'y+y_0\ge\mathbb U(\mathcal Q(q,x))\ \ \forall q\in\mathbb R^d ,

with $Y$ symmetric and $Q\cdot Y=\sum_{ij}Q_{ij}Y_{ij}$ . Its semidefinite reformulation (8) has the dual (9):

Z_{DD}(x)=\max\ \sum_{k=1}^K (h-Tx)'p_k+\beta_kv_{k0}\quad\text{s.t.}\quad \sum_{k=1}^K\begin{pmatrix}V_k&v_k\\ v_k'&v_{k0}\end{pmatrix}=\begin{pmatrix}Q&\mu\\ \mu'&1\end{pmatrix},\ \begin{pmatrix}V_k&v_k\\ v_k'&v_{k0}\end{pmatrix}\succeq0,\ W'p_k\le\alpha_kv_k .

Its variables are scaled conditional moments: $v_{k0}$ is the probability that the $k$ th piece of $\mathbb U$ is active, and $v_k$ , $V_k$ are the first and second moments of $\tilde q$ on that event, multiplied by $v_{k0}$ .

The standing assumptions are Assumption 3, $\{p\in\mathbb R^r : W'p\le q\}\ne\emptyset$ for every $q$ , so that $\mathcal Q(q,x)$ is finite, and Assumption 4, $Q-\mu\mu'\succ0$ . Recourse sets are assumed nonempty.

Formalization targets

Goal: Theorem 2.2

For every $x\in X$ there is a sequence $P_j\in\mathcal P$ with $\mathbb E_{P_j}[\mathbb U(\mathcal Q(\tilde q,x))]\to Z(x)$ , and

Z(x)=Z_D(x)=Z_{DD}(x),

where all three are finite optimal values: a supremum over a nonempty bounded-above set, an infimum over a nonempty bounded-below set, and a supremum over a nonempty bounded-above set.

Milestones

Lemma 2.1: $Z_{DD}(x)\ge Z(x)$ , in the form "each $P\in\mathcal P$ gives a feasible point of (9) whose objective equals $\mathbb E_P[\mathbb U(\mathcal Q)]$ ".
(9) has an optimal solution.
$\mathcal Q(\cdot,x)$ is positively homogeneous and superadditive.
If $W'p\le\alpha v$ with $\alpha\ge0$ then $\alpha\mathcal Q(v,x)\ge(h-Tx)'p$ .
Jensen: $\mathbb E[\mathcal Q(\tilde r,x)]\le\mathcal Q(\mathbb E\tilde r,x)$ , with $\mathcal Q(\tilde r,x)$ integrable.
An optimal solution of (9) can be chosen so that every block has $v_{k0}>0$ or vanishes.
Strong duality $Z(x)=Z_D(x)$ (§2.1).

Significance

Theorem 2.2 says that the semidefinite bound is tight and that the worst case is approached by explicit mixtures. With probability $v_{k0}$ the cost vector sits at the conditional mean $v_k/v_{k0}$ , and with a small probability it is perturbed by a large Gaussian. The construction tells which scenarios a minimax solution guards against. The paper's numerical section uses it to stress-test solutions computed under other distributional assumptions. For the risk-neutral case ( $K=1$ ) the bound collapses to Jensen's bound $\min_{w\in X(x)}\mu'w$ . For $K>1$ it is a combination of Jensen bounds, one per piece of the disutility.

Theorem 2.2 is proved in the paper; no part of it, nor the strong duality of the moment problem that it relies on, is formalized on the platform or, to our knowledge, elsewhere. The mission asks for machine-checked proofs of the identity $Z=Z_D=Z_{DD}$ and of the steps of the extremal construction. Several of these are reusable beyond this paper: weak and strong duality of moment problems, the existence of optimal solutions of moment-type semidefinite programs, and Jensen's inequality for the value function of a linear program.

Difficulty

Most of the argument is linear programming and bookkeeping. The step $Z(x)=Z_D(x)$ is a strong-duality theorem for an infinite-dimensional linear program over measures. The paper cites it from Isii's theory of the moment problem, and none of that theory exists in Mathlib. The construction of near-extremal distributions also needs care. A single distribution in $\mathcal P$ generally cannot attain $Z(x)$ , so the bound is reached only along a family whose second moments are matched by rare, large perturbations. Lemma 2.1 needs measurable selections of an active piece of $\mathbb U$ and of a dual optimal solution of the second-stage program as functions of $q$ . When the optimal solution of (9) has zero-weight blocks, the mixture is undefined until the solution is first rearranged.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and distributions are probability measures on Fin d → ℝ with square-integrable coordinates. They are not densities as in the paper's (5). The moment class uses the published MomentDRO.Conf definitions, and $\mathbb E[\tilde q\tilde q']$ is the uncentred second moment. The paper writes $p$ both for the dimension of $q$ and for dual vectors. Here the dimension is $d$ and dual vectors are named π. Indices $k$ are zero-based. Bordered matrices are Matrix.fromBlocks on Fin d ⊕ Fin 1 and $\succeq0$ is Matrix.PosSemidef. $\mathcal Q$ is a real infimum and the optimal values are real sSup/sInf of value sets. Every statement that uses an optimal value also asserts IsLUB/IsGLB, so junk values cannot make a statement true.

As printed, Assumption 2 (complete recourse) and Assumption 3 for all $q$ contradict each other whenever $W$ has a row. The formalization keeps Assumption 3 for all $q$ and replaces complete recourse by nonemptiness of $X(x)$ , which is what §2's proofs use. Assumption 1 is not used and is omitted. The hypotheses are jointly satisfiable, for example by $W=I$ , $T=0$ , $h=0$ , $\mu=0$ and $Q=I$ .

The sequence clause of Theorem 2.2 alone holds for every finite supremum, so it does not capture the theorem. The goal therefore also asserts the equalities $Z=Z_D=Z_{DD}$ , with all three values genuine, and these carry the content. A formalization that drops them, or states them only through junk values, is ruled out.

A complete development needs the duality theory of the moment problem, Jensen's inequality for concave functions on $\mathbb R^d$ , compactness arguments for semidefinite feasible sets, and multivariate Gaussian mixtures (ProbabilityTheory.multivariateGaussian in Mathlib). Proofs of individual milestones are welcome. So is a general moment-problem duality theorem from which strong_duality follows.

Selected references

D. Bertsimas, X. V. Doan, K. Natarajan, C.-P. Teo, Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion, Mathematics of Operations Research 35(3):580–602, 2010. https://doi.org/10.1287/moor.1100.0445
E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903

11 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Inventory Management of a Fast-Fashion Retail Network 2: The Tangent-Envelope Approximation of Expected Sales Is an Upper BoundResearch Paper

Motivation

Zara ships inventory from a central warehouse to each of its stores every week, and for a short-lived fashion item the warehouse holds a limited amount of each size. Deciding how many units of each size to ship to each store is therefore a constrained allocation problem whose objective is the expected sales a store will realize from a given inventory. Caro and Gallien (working paper, 2007; published in Operations Research, 2010) built such a model, embedded it in a weekly shipment optimization, and tested it in a field experiment in Zara's store network. The store-level sales model has one unusual feature, taken from Zara's practice: as soon as one of the major sizes of an item runs out, the whole item is removed from display, so stock-outs of different sizes interact.

The expected sales under that policy have no closed form usable inside a mixed integer program. The paper replaces them by an explicit piecewise-linear function and asserts that this replacement is an upper bound. This mission formalizes that claim, the chain of identities and inequalities that lead to it, and the paper's statement that its shipment program represents the approximation exactly.

Setting

A reference is offered in a finite set of sizes $\mathcal S = \mathcal S^+ \cup \mathcal S^-$ , with major sizes $\mathcal S^+$ and minor sizes $\mathcal S^- = \mathcal S \setminus \mathcal S^+$ . Sale opportunities for size $s$ follow a Poisson process $N_s(t)$ with rate $\lambda_s > 0$ , independent across sizes, where $t$ is the time since the last replenishment and $T > 0$ is the time between replenishments.

Given an inventory vector $q \in \mathbb N^{\mathcal S}$ , the virtual stockout time of size $s$ is $\tau_s(q_s) = \inf\{t \ge 0 : N_s(t) = q_s\}$ , and $\tau_{\mathcal A} = \min_{s \in \mathcal A}\tau_s(q_s)$ for a set of sizes $\mathcal A$ . Writing $a \wedge b = \min(a,b)$ , the number of sales in one period is

G(q) = \sum_{s \in \mathcal S^+} N_s(\tau_{\mathcal S^+} \wedge T) + \sum_{s \in \mathcal S^-} N_s(\tau_{\mathcal S^+ \cup \{s\}} \wedge T),

since every size stops selling when the first major size runs out, and a minor size also stops when it runs out itself. The expected sales function is $g_\lambda(q) = \mathbb E[G(q)]$ .

For the approximation, let $\gamma(a,b) = \int_0^b v^{a-1}e^{-v}\,dv$ be the lower incomplete Gamma function, and define the tangent coefficients

a_k(\lambda) = \frac{\gamma(k+1, \lambda T)}{\lambda\, k!}, \qquad b_i(\lambda) = \sum_{k=0}^{i-1} a_k(\lambda),

with the tangent at $i = \infty$ equal to the constant $T$ . For each size choose a nonempty finite set $\mathcal N(\lambda_s) \subseteq \mathbb N \cup \{\infty\}$ of tangent indices. The approximate expected sales function is

\tilde g_\lambda(q) = \lambda_{\mathcal S^+} \min_{s \in \mathcal S^+} \min_{i \in \mathcal N(\lambda_s)} \{a_i(\lambda_s)(q_s - i) + b_i(\lambda_s)\} + \sum_{s \in \mathcal S^-} \lambda_s \min_{s' \in \mathcal S^+ \cup \{s\}} \min_{i \in \mathcal N(\lambda_{s'})} \{a_i(\lambda_{s'})(q_{s'} - i) + b_i(\lambda_{s'})\},

with $\lambda_{\mathcal S^+} = \sum_{s\in\mathcal S^+}\lambda_s$ . In Lean the objects are expectedSales, hA ( $\mathbb E[\tau_{\mathcal A}\wedge T]$ ), a, b, tangent and gTilde in the namespace FastFashion.Approx.

Formalization targets

Goal: the approximation is an upper bound

For every independent Poisson family with positive rates, every $T > 0$ , every nonempty $\mathcal S^+$ , every choice of nonempty finite tangent sets, and every $q \in \mathbb N^{\mathcal S}$ ,

g_\lambda(q) \le \tilde g_\lambda(q).

The statement fixes no tangent set, so it covers the paper's numerical choice (7) and every refinement of it.

Milestones

Eq. (2): $g_\lambda(q) = \lambda_{\mathcal S^+}\mathbb E[\tau_{\mathcal S^+}\wedge T] + \sum_{s\in\mathcal S^-}\lambda_s\mathbb E[\tau_{\mathcal S^+\cup\{s\}}\wedge T]$ .
Eq. (3): $\mathbb E[\tau_{\mathcal D}\wedge T] \le \min_{s\in\mathcal D}\mathbb E[\tau_s\wedge T]$ for nonempty $\mathcal D$ .
Eqs. (4)–(5): $\mathbb E[\tau_s\wedge T] = \frac1{\lambda_s}\sum_{k=1}^{q_s}\mathbb P(N_s(T)\ge k) = \sum_{k=1}^{q_s}\frac{\gamma(k,\lambda_sT)}{\lambda_s\Gamma(k)}$ .
The terms $a_k(\lambda)$ are positive and strictly decreasing in $k$ .
Eq. (6): $\mathbb E[\tau_s\wedge T] = \min_{i\in\mathbb N\cup\{\infty\}}\{a_i(\lambda_s)(q_s-i)+b_i(\lambda_s)\}$ , the minimum attained.

Further result: the MIP represents the approximation

In the shipment program (MIP) (13)–(19) of §3.2, with positive prices, every optimal solution has $z_j = \tilde g_{\lambda_j}(x_j + I_j)$ at every store $j$ .

Significance

The upper bound is what makes the paper's optimization coherent: the MIP maximizes $\sum_j P_j \tilde g_{\lambda_j}$ , and the bound guarantees that this objective never underestimates the expected revenue of a shipment plan, with an error controlled by the number of tangents. Identity (6) exhibits $\mathbb E[\tau_s \wedge T]$ as a concave function of $q_s$ with explicit Erlang-type slopes; (2) is a standard optional-sampling identity for compensated Poisson processes stopped at a bounded stopping time; and the MIP statement is the step that turns a minimum of affine functions into linear constraints.

The paper proves none of these in detail: (2), (4) and (5) are justified by a reference to the optional sampling theorem, (6) by a sentence on discrete concavity, and the upper bound and the MIP claim by one sentence each. None of the statements has a machine-checked proof. A formalization produces a checked chain from the Poisson model to the deterministic program, fixes the indexing error in the printed coefficients of (6), and isolates the exact hypotheses (nonempty major sizes, nonempty tangent sets, positive prices) under which the claims hold.

Difficulty

The deterministic parts — (3) given pathwise monotonicity, the envelope inequality given concavity, and the MIP argument — are short. The probabilistic identities are not. Equation (2) needs the optional sampling theorem for the compensated process $N_s(t) - \lambda_s t$ in continuous time, applied at $\tau_{\mathcal A} \wedge T$ (the paper cites Karatzas and Shreve 1991), which requires showing that $\tau_{\mathcal A}$ is a stopping time for the joint filtration of the family and that $N_s$ is still a martingale with respect to that larger filtration; this is where independence across sizes enters. Equation (4) needs the distribution of $\tau_s(q_s)$ , the $q_s$ -th arrival time, which is Erlang; the statement in the model is about first hitting times of a counting process, not about sums of exponential inter-arrival times, so the link between the two descriptions has to be built. Equation (5) needs the identity $\mathbb P(N(T) \ge k) = \gamma(k, \lambda T)/\Gamma(k)$ between Poisson tails and the incomplete Gamma function.

A tempting shortcut is to define $g_\lambda$ directly by formula (2), or $\mathbb E[\tau_s\wedge T]$ by formula (4); both make the corresponding milestones definitional and the goal a statement about formulas rather than about sales. The formalization defines $g_\lambda$ from $G$ and $h^{\mathcal A}$ from the stopping times.

Formalization scope

Model. Sizes form a finite type; the major sizes are a Finset and the minor sizes its complement. The demand is a structure IsPoissonFamily λ N P: each $N_s$ is a counting process with $N_s(0)=0$ , non-decreasing right-continuous paths with unit jumps, Poisson increments of mean $\lambda_s(t-u)$ , independent increments, and the processes are independent across sizes. $P$ is a probability measure.
Stockout times take values in $\mathbb R \cup \{+\infty\}$ (WithTop ℝ), so the infimum of an empty set is $+\infty$ , never $0$ ; $\tau_{\mathcal A}\wedge T$ is a real number in $[0,T]$ .
Expectations are Bochner integrals. They are not junk: $0 \le G(q) \le \sum_s N_s(T)$ , which is integrable, and $\tau_{\mathcal A}\wedge T \in [0,T]$ .
Corrected coefficients. As printed, $a_k = \gamma(k,\lambda T)/(\lambda\Gamma(k))$ and $b_1 = a_0$ involves $\Gamma(0)$ ; the formalization uses $a_k = \gamma(k+1,\lambda T)/(\lambda\,k!)$ , matching the paper's description of $a_k$ as the probability that the $(k+1)$ -th unit sells.
Tangent sets. The rule (7), " $b_i(\lambda_s) \approx 0, 0.3T, 0.6T, 0.8T, 0.9T, T$ ", is approximate and is replaced by an arbitrary nonempty finite set $\mathcal N(\lambda_s) \subseteq \mathbb N\cup\{\infty\}$ .
Added hypotheses. $\mathcal S^+ \ne \emptyset$ (for (8) and the goal), nonempty $\mathcal D$ in (3), and $P_j > 0$ in the MIP statement.
MIP. Optimality is defined as feasibility plus an objective at least that of every feasible point; existence of an optimum is not asserted.

The paper's further remark that $\tilde g_\lambda$ inherits the qualitative properties of Proposition 1, and the multicolor extension of Appendix §5.2, are not included. Contributions of general infrastructure are welcome: optional sampling for continuous-time counting processes, Erlang hitting-time laws for Poisson processes, and the Poisson-tail/incomplete-Gamma identity are all reusable well beyond this mission.

Selected references

F. Caro, J. Gallien, Inventory Management of a Fast-Fashion Retail Network, working paper (August 2, 2007); published in Operations Research 58(2), 2010. https://doi.org/10.1287/opre.1090.0698
I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2

10 thms2 active usersReviewed

Analysis Control Theory Dynamical Systems·Captain: mikedeng1

Small Gain Theorems for Large Scale Systems and Construction of ISS Lyapunov Functions 2: Under the Small Gain Condition Γ_μ ≱ id, an Ω-Path ExistsResearch Paper

Why paths in the positive orthant matter for networks

A large control system is often built from many subsystems $\Sigma_1,\dots,\Sigma_n$ , each of which is input-to-state stable (ISS) with respect to the states of the others. Whether the interconnection is again ISS is decided by a small gain condition on the matrix of interconnection gains. For two subsystems this goes back to Jiang, Teel and Praly (1994) and to the Lyapunov version of Jiang, Mareels and Wang (1996). For $n$ subsystems, Dashkovskiy, Rüffer and Wirth formulated the condition as a property $\Gamma_\mu\not\ge\mathrm{id}$ of a monotone operator on $\mathbb R^n_+$ (2007). Rüffer's thesis (2007) and the paper on which this mission is based (arXiv:0901.1842, SIAM J. Control Optim. 2010) turned it into a Lyapunov construction.

The construction needs a geometric object: a path $\sigma$ in the positive orthant, unbounded in every coordinate, along which the gain operator strictly decreases every component. For a linear gain matrix this is a Perron vector. For nonlinear gains, its existence is the first of the paper's two main results (Theorem 5.2). This mission formalizes that theorem and the lemmas of §8 that prove it. The companion mission formalizes the second main result, the Lyapunov function built from such a path.

Setting

Write $\mathbb R_+=[0,\infty)$ . Vectors in $\mathbb R^n_+$ are compared componentwise: $v\le w$ means $v_i\le w_i$ for all $i$ , and $v<w$ means $v_i<w_i$ for all $i$ . A function $\gamma:\mathbb R_+\to\mathbb R_+$ is of class $\mathcal K$ if it is continuous, strictly increasing and $\gamma(0)=0$ , and of class $\mathcal K_\infty$ if it is moreover unbounded.

A gain matrix is $\Gamma=(\gamma_{ij})_{i,j=1}^n$ with $\gamma_{ij}\in\mathcal K\cup\{0\}$ and $\gamma_{ii}\equiv0$ . A monotone aggregation function (MAF) is a continuous $\mu:\mathbb R^n_+\to\mathbb R_+$ with $\mu(s)>0$ for $s\ne0$ , $\mu(x)<\mu(y)$ whenever $x<y$ , and $\mu(x)\to\infty$ as $\|x\|\to\infty$ . Typical examples are sums and maxima. Given MAFs $\mu_1,\dots,\mu_n$ , the gain operator is

\Gamma_\mu(s)_i=\mu_i\big(\gamma_{i1}(s_1),\dots,\gamma_{in}(s_n)\big),\qquad s\in\mathbb R^n_+ .

The paper assumes from p. 8 on that $\mu_i$ , restricted to the coordinates of the nonzero entries of row $i$ , still has the strict monotonicity (Remark 2.6). The small gain condition (SGC) is $\Gamma_\mu\not\ge\mathrm{id}$ : for every $s\ne0$ , at least one component of $\Gamma_\mu(s)$ is strictly smaller than the corresponding component of $s$ . The set

\Omega(\Gamma_\mu)=\{s\in\mathbb R^n_+:\Gamma_\mu(s)<s\}

collects the points that every component of $\Gamma_\mu$ strictly decreases.

An $\Omega$ -path (Definition 5.1) is a continuous $\sigma:\mathbb R_+\to\mathbb R^n_+$ with every component $\sigma_i\in\mathcal K_\infty$ such that (i) each $\sigma_i^{-1}$ is locally Lipschitz on $(0,\infty)$ ; (ii) on every compact $K\subset(0,\infty)$ the derivatives of all $\sigma_i^{-1}$ , where they exist, lie in $[c,C]$ for constants $0<c<C$ depending on $K$ only; and (iii) $\sigma(r)\in\Omega(\Gamma_\mu)$ for all $r>0$ .

Formalization targets

Goal: Theorem 5.2

Let $\Gamma$ be a gain matrix and $\mu$ a compatible vector of MAFs. Assume one of: (i) $\Gamma_\mu$ is linear with spectral radius less than one; (ii) $\Gamma$ is irreducible and $\Gamma_\mu\not\ge\mathrm{id}$ ; (iii) $\mu=\max$ and $\Gamma_\mu\not\ge\mathrm{id}$ ; (iv) the entries of $\Gamma$ are bounded and $\Gamma_\mu\not\ge\mathrm{id}$ . Then

\exists\,\sigma\ \text{an }\Omega\text{-path with}\quad\Gamma_\mu(\sigma(r))<\sigma(r)\quad\forall r>0 .

In cases (i)–(iii) the entries are in $\mathcal K_\infty\cup\{0\}$ , and in case (iv) they are in $(\mathcal K\setminus\mathcal K_\infty)\cup\{0\}$ .

Milestones

The milestones follow §8 in the order the proof uses them.

Bounded gains: Lemmas 8.1–8.3, where iterates of a point of $\Omega$ tend to $0$ and the polygon through them stays in $\Omega$ ; and Proposition 8.4, which is case (iv).
Technical lemmas: Lemmas 8.5–8.7 on diagonal operators $\mathrm{diag}(\rho)$ and the decay set $\Psi=\{s:\Gamma_\mu(s)\le s\}$ .
Topological statements: Proposition 8.8, path-connectedness of $\Psi$ ; Proposition 8.10, where $\Omega$ meets every simplex $S_r=\{s:\sum s_i=r\}$ ; and Proposition 8.9, where $\Psi_\infty=\bigcap_k\Gamma_\mu^k(\Psi)$ is unbounded.
Irreducible case: the scaling step quoted from Rüffer's earlier work, and Theorem 8.11, which is case (ii).
Maximum case: Theorem 8.14, case (iii) in its cycle-condition form.
Linear case: the Perron step of §8.5, case (i).

Significance

An $\Omega$ -path turns a small gain condition into a Lyapunov function. If each $V_i$ is an ISS Lyapunov function of $\Sigma_i$ , then $V(x)=\max_i\sigma_i^{-1}(V_i(x_i))$ is one for the network (Theorem 5.3). So Theorem 5.2 is the step that makes the small gain condition a certificate of network stability, and the corollaries of §5–§7 (sums, maxima, neural networks) all pass through it.

The results are published and proved on paper. None is machine-checked: no proof assistant library contains MAFs, gain operators, the sets $\Omega$ and $\Psi$ , or $\Omega$ -paths. The paper cites three ingredients without proof: Lemma 8.6, Proposition 8.9 and the scaling step of Theorem 8.11. It also gives Theorem 8.14 only as a sketch. Formalizing them closes those gaps in one place.

Difficulty

For bounded gains the problem is easy: far out, every point of a large ray lies in $\Omega$ , and the only work is the descent to the origin. With $\mathcal K_\infty$ entries, $\Gamma_\mu$ is unbounded and no ray need stay in $\Omega$ . Following the image of a single point fails, because forward iterates go to $0$ , not to infinity. The paper instead uses backward orbits inside $\Psi_\infty$ . That this set is nonempty and unbounded is a fixed-point argument of Knaster–Kuratowski–Mazurkiewicz type (Propositions 8.9 and 8.10), not a monotonicity argument. A second obstacle is strictness. A backward orbit is only $\le$ -increasing, while Definition 5.1 needs strictly increasing components with derivative bounds. This is where the diagonal scalings of Lemmas 8.6–8.7 enter.

Formalization scope

$\mathbb R_+$ is ℝ≥0 and $\mathbb R^n_+$ is Fin n → ℝ≥0, with subsystems indexed from $0$ . The strict order $<$ is a named predicate (SLt), never Lean's < on functions, which means " $\le$ and $\ne$ ". The small gain condition is ∀ s ≠ 0, ¬ s ≤ T s. The inverses $\sigma_i^{-1}$ are carried as explicit two-sided inverses, and derivatives are ordinary real derivatives at points $r>0$ where they exist. Compatibility (Remark 2.6) and $\gamma_{ii}\equiv0$ are hypotheses of every statement about $\Gamma_\mu$ . Irreducibility is the matrix-power form of p. 12, which Mathlib's Matrix.isIrreducible_iff_exists_pow_pos connects to Matrix.IsIrreducible. The spectral-radius hypothesis says that every complex eigenvalue has modulus $<1$ . The 1-norm defines $S_r$ .

Hypotheses made explicit or corrected:

Theorem 5.2's header types $\Gamma$ in $\mathcal K_\infty\cup\{0\}$ while (iv) needs bounded entries, so each case carries its own entry class.
Case (iv) is stated as printed, without "no zero rows".
Proposition 8.10 prints " $T(s)\not\ge s$ for all $s\in\mathbb R^n_+$ ". No map satisfies this at $s=0$ , so it is stated for $s\ne0$ .
Propositions 8.9 and 8.10 assume $n\ge1$ .

A path with $\Gamma_\mu(\sigma(r))\le\sigma(r)$ , or with Lean's < on functions, is not an $\Omega$ -path. Such a reading would make the goal follow from the origin alone, and it is ruled out.

Needed infrastructure: comparison-function calculus (inverses and compositions of $\mathcal K_\infty$ functions), piecewise linear interpolation in $\mathbb R^n_+$ with Lipschitz inverse bounds, and a KKM-type argument on the simplex. The first two are reusable well beyond this mission. Contributions of any milestone, proofs of the cited ingredients (Lemma 8.6, Proposition 8.9, Proposition 8.10, the scaling step of Theorem 8.11) and a full proof of Theorem 8.14 are welcome.

Selected references

S. N. Dashkovskiy, B. S. Rüffer, F. R. Wirth, Small Gain Theorems for Large Scale Systems and Construction of ISS Lyapunov Functions, arXiv:0901.1842v2, 2009; SIAM J. Control Optim. 48(6), 2010. https://arxiv.org/abs/0901.1842 , https://doi.org/10.1137/090746483
S. Dashkovskiy, B. S. Rüffer, F. R. Wirth, An ISS small gain theorem for general networks, Math. Control Signals Systems 19 (2007), pp. 93–122.
B. S. Rüffer, Monotone dynamical systems, graphs, and stability of large-scale interconnected systems, PhD thesis, Universität Bremen, 2007. http://nbn-resolving.de/urn:nbn:de:gbv:46-diss000109058
B. S. Rüffer, Monotone inequalities, dynamical systems, and paths in the positive orthant of Euclidean n-space, Positivity, 2009/2010. https://doi.org/10.1007/s11117-009-0016-5
Z.-P. Jiang, I. M. Y. Mareels, Y. Wang, A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems, Automatica 32 (1996), pp. 1211–1215.

18 thms2 active usersReviewed

Completed

Algorithmic Game Theory Dynamical Systems Linear algebra·Captain: mikedeng1

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 2: Near Jordan's Three-Player Game Γ₀ of Section III, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

A central question of the theory of learning in games is whether simple adaptive behavior leads players to a Nash equilibrium. Many natural dynamics — fictitious play, best-reply dynamics, replicator dynamics — fail to converge in some games, and the failures are usually exhibited one dynamic at a time. Hart and Mas-Colell (AER 2003) asked a structural question instead: is there any continuous-time dynamic, satisfying one informational restriction, that converges to Nash equilibrium for all games in a reasonable family? The restriction is uncoupledness: each player's adjustment may depend on the current strategy profile and on that player's own payoff function, but not on the payoff functions of the others. This is the situation of players who do not know the opponents' preferences.

Their answer is negative, and the paper proves it with two examples. This mission formalizes the second, built on a three-player game introduced by James Jordan (GEB 1993) in his study of learning mixed-strategy equilibria. A companion mission formalizes the first example, a two-player game on the unit disk.

Setting

Three players each choose between two pure strategies, $0$ and $1$ . A game $\Gamma$ is identified with its payoff functions $(u^1,u^2,u^3)$ , $u^i:\{0,1\}^3\to\mathbb R$ . A state is a mixed profile $x=(x^1,x^2,x^3)\in X=[0,1]^3$ , where $x^i$ is the probability that player $i$ plays $0$ (top row, left column, left matrix). Payoffs extend to $X$ by expectation over independent randomizations, and $\bar x$ is a Nash equilibrium when no player can raise its expected payoff by changing its own coordinate.

Jordan's family $\mathcal U_0$ consists of the games

u^i(s)=\begin{cases}a^i & s^i=0,\ s^{i+1}=1,\\ 1 & s^i=1,\ s^{i+1}=0,\\ 0&\text{otherwise,}\end{cases}

indices modulo 3, with parameters $a^i$ close to $1$ : each player wants to mismatch the next player. Jordan's game $\Gamma_0$ is the member with all $a^i=1$ ; every game of $\mathcal U_0$ has a unique Nash equilibrium $\bar x^i(\Gamma)=a^{i-1}/(a^{i-1}+1)$ , and $\bar x(\Gamma_0)=(1/2,1/2,1/2)$ .

A dynamic for a family $\mathcal U$ is a vector field $\dot x=F(x;\Gamma)$ on $X$ , one for each $\Gamma\in\mathcal U$ . It is uncoupled if $F^i(x;\Gamma)=F^i(x;\Gamma')$ whenever $\Gamma,\Gamma'\in\mathcal U$ give player $i$ the same payoff function. When every game of $\mathcal U$ has a single Nash equilibrium $\bar x(\Gamma)$ , $F$ is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ , $\bar x(\Gamma)$ is a rest point, every solution converges to it, $F(\cdot;\Gamma)$ is $C^1$ , and the Jacobian $J$ of $F(\cdot;\Gamma)$ at $\bar x(\Gamma)$ is hyperbolic and stable: all its eigenvalues have negative real parts.

Formalization targets

Goal: Theorem 1 near Jordan's game

Let $\mathcal U$ have the single-Nash-equilibrium property and contain every game of $\mathcal U_0$ that is close to $\Gamma_0$ . Then

\text{no uncoupled dynamic for }\mathcal U\text{ is Nash-convergent for }\mathcal U .

Milestones

Every game of $\mathcal U_0$ (indeed every $a$ with all $a^i>0$ ) has the unique equilibrium $\bar x^i=a^{i-1}/(a^{i-1}+1)$ ; in particular $\bar x_0=(1/2,1/2,1/2)$ .
If $F$ is uncoupled and Nash-convergent, then $f=F(\cdot;\Gamma_0)$ satisfies $f^i(\bar x_0+(y-\tfrac12)e_i)=0$ for $y$ near $1/2$ , hence the diagonal and the trace of $J=Df(\bar x_0)$ vanish:

\operatorname{tr}J=0.

A real $3\times3$ matrix with zero trace and nonzero determinant has an eigenvalue with positive real part.

Two further items record the paper's observations: uncoupledness forces $J=\begin{pmatrix}0&c&0\\0&0&d\\e&0&0\end{pmatrix}$ , and such a matrix has an eigenvalue with positive real part when $cde\ne0$ and spectrum $\{0\}$ otherwise. A last item shows that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent.

Significance

The theorem says that convergence to Nash equilibrium is not a property that adaptive dynamics can deliver on informational grounds alone: as soon as a family contains the games near $\Gamma_0$ , any rule in which players respond only to their own payoffs fails for some game, even though every game in the family has a unique equilibrium and a coupled rule converges for all of them. The finite example matters because it shows that the obstruction is not an artifact of continuum strategy spaces: it occurs in a $2\times2\times2$ game in mixed strategies. The paper contrasts it (§IV) with the existence of uncoupled dynamics that converge to correlated equilibria: Nash equilibrium cannot be reached in an uncoupled way, while correlated equilibrium, a notion based on coordination, can. Follow-up work extends the impossibility to stochastic uncoupled dynamics (Hart and Mas-Colell, GEB 2006) and surveys the area (Hart, Econometrica 2005).

The result has been proved since 2003; no machine-checked proof of it is known. A formal proof requires an equilibrium computation in a parametric family of finite games, a careful treatment of the derivative of a vector field defined only on a cube, and a spectral fact about real $3\times3$ matrices. The definitions of uncoupled and Nash-convergent dynamics written here are reusable for other impossibility results of the same kind.

Difficulty

The obvious attempt is to analyze a particular dynamic and show that it cycles around $\bar x_0$ . That proves nothing about other dynamics: the statement quantifies over every uncoupled $F$ , so the argument must extract a constraint on $F$ from uncoupledness alone. Uncoupledness only relates the dynamic at different games through single coordinates of $F$ , and Nash-convergence only constrains $F$ at the equilibria of the games in $\mathcal U$ ; neither says anything directly about the Jacobian at $\Gamma_0$ . Formally, the delicate steps are the uniqueness of the equilibrium for all nearby parameters, which requires excluding pure and partially mixed equilibria, and the passage from vanishing along a segment to a vanishing partial derivative.

Formalization scope

Players are indexed $0,1,2$ in Lean (the page's player $i$ is index $i-1$ ), strategies are Fin 2, and a game is Fin 3 → (Fin 3 → Fin 2) → ℝ. The state space is $X=[0,1]^3\subset\mathbb R^3$ ; a dynamic is any map $F:\mathbb R^3\times\text{Game}\to\mathbb R^3$ , whose values outside $X$ never matter. Committed conventions:

Solutions stay in $X$ : a solution is a curve on $[0,\infty)$ with values in $X$ satisfying the ODE (one-sided derivative at $0$ ). Allowing curves that leave $X$ would let the junk values of $F$ outside $X$ falsify convergence for every $F$ and trivialize the goal.
Uncoupledness is required only between games of $\mathcal U$ and only at states of $X$ .
Nash-convergence bundles four clauses for every game of $\mathcal U$ and every Nash equilibrium of it: rest point, $C^1$ on $X$ , all eigenvalues of the Jacobian with negative real part (the published FatkhullinPolyak.Discrete.IsHurwitz), and convergence of every solution. The Jacobian is the derivative within $X$ .
The single-Nash-equilibrium property of $\mathcal U$ is a hypothesis of the goal.
The neighborhood hypothesis. The page assumes that $\mathcal U$ contains a neighborhood of $\Gamma_0$ . The goal assumes less: $\mathcal U$ contains every game of $\mathcal U_0$ in some footnote-7 neighborhood of $\Gamma_0$ . The page's hypothesis implies this one, so the formal goal is at least as strong. The literal hypothesis is not used because it is not known (and not claimed on the page) to be compatible with the single-equilibrium property, and a contradictory pair of hypotheses would make the goal vacuous.
Milestone 1 assumes only $a^i>0$ instead of $|a^i-1|<\varepsilon$ for small $\varepsilon$ ; this covers every such family with $\varepsilon\le1$ .

The family $\mathcal U$ cannot be vacuous: Jordan's games with $|a^i-1|<1/2$ satisfy both hypotheses, and the coupled-dynamic item certifies that Nash-convergence itself can be met, so the goal's force rests on uncoupledness. Contributions welcome include the equilibrium computation for $\mathcal U_0$ , the spectral lemmas (which are independent of game theory), and the calculus step from vanishing along a segment to a vanishing partial derivative within a cube.

Selected references

S. Hart and A. Mas-Colell, Uncoupled Dynamics Do Not Lead to Nash Equilibrium, American Economic Review 93(5):1830–1836, 2003. https://doi.org/10.1257/000282803322655581
J. S. Jordan, Three Problems in Learning Mixed-Strategy Nash Equilibria, Games and Economic Behavior 5(3):368–386, 1993. https://doi.org/10.1006/game.1993.1022
S. Hart and A. Mas-Colell, Stochastic Uncoupled Dynamics and Nash Equilibrium, Games and Economic Behavior 57(2):286–303, 2006. https://doi.org/10.1016/j.geb.2005.09.007
S. Hart, Adaptive Heuristics, Econometrica 73(5):1401–1430, 2005. https://doi.org/10.1111/j.1468-0262.2005.00625.x

6 thms2 active usersReviewed

Discrete Geometry Number Theory Theoretical Computer Science·Captain: mikedeng1

On Lattices, Learning with Errors, Random Linear Codes, and Cryptography 6: The Smoothing Parameter Satisfies η_ε(L) ≥ √(ln(1/ε)/π)/λ₁(L*) ≥ √(ln(1/ε)/π)·λ_n(L)/nResearch Paper

Motivation

The learning with errors (LWE) problem underlies much of post-quantum public-key cryptography, and its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). Every step of that reduction is calibrated by the smoothing parameter $\eta_\epsilon(L)$ of Micciancio and Regev (SIAM J. Comput. 2007): the Gaussian width above which a discrete Gaussian on a lattice behaves like a continuous one. The approximation factors of the reduction are stated in terms of $\eta_\epsilon(L)$ , and they are converted into factors for the standard lattice problems (GapSVP, SIVP) by comparing $\eta_\epsilon(L)$ with the successive minima of $L$ and of its dual.

Upper bounds on $\eta_\epsilon(L)$ (Lemmas 2.11 and 2.12 of the paper, from Micciancio–Regev) say the smoothing parameter is not too large. Claim 2.13 is the matching lower bound: the smoothing parameter cannot be much smaller than $1/\lambda_1(L^*)$ , and hence than $\lambda_n(L)/n$ . The second comparison goes through Banaszczyk's transference theorem (Banaszczyk, Math. Ann. 296 (1993)), $1 \le \lambda_1(L)\lambda_n(L^*) \le n$ , which relates the geometry of a lattice to that of its dual.

This mission formalizes Claim 2.13 from the published J. ACM article (Article 34, 2009), together with the steps of its proof and the transference theorem it cites. The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms; it is outside this series of missions.

Setting

Work in $\mathbb{R}^n$ , $n \ge 1$ , with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$ . A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is

L^* = \{y \in \mathbb{R}^n : \langle x, y\rangle \in \mathbb{Z} \text{ for all } x \in L\},

again a lattice, with $(L^*)^* = L$ .

The successive minima used here are $\lambda_1(L)$ , the length of a shortest nonzero vector of $L$ , and $\lambda_n(L)$ , the least $r$ such that $L$ contains $n$ linearly independent vectors of length at most $r$ .

For $s > 0$ the Gaussian function is $\rho_s(x) = \exp(-\pi\|x/s\|^2)$ (Eq. (4)), and for a countable set $A$ , $\rho_s(A) = \sum_{x\in A}\rho_s(x)$ . In particular $\rho_{1/s}(y) = \exp(-\pi s^2\|y\|^2)$ .

For $\epsilon > 0$ the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s$ such that $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ (Definition 2.10).

Formalization targets

Goal: Claim 2.13 (p. 34:20)

For any lattice $L$ and any $\epsilon > 0$ ,

\eta_\epsilon(L) \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{1}{\lambda_1(L^*)} \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{\lambda_n(L)}{n}.

Both inequalities of the chain are part of the goal. The asymptotic "In particular" sentence of the claim ( $\epsilon(n) = o(1)$ , large enough $n$ ) is not.

Milestones, in attack order

The remark after Definition 2.10 (p. 34:19). The map $s \mapsto \rho_{1/s}(L^*\setminus\{0\})$ is continuous and strictly decreasing on $(0,\infty)$ , tends to $\infty$ as $s \to 0$ and to $0$ as $s \to \infty$ , and $\epsilon \mapsto \eta_\epsilon(L)$ is its inverse; in particular $\rho_{1/\eta_\epsilon(L)}(L^*\setminus\{0\}) = \epsilon$ .
The display of the proof of Claim 2.13 (p. 34:20). For $s = \eta_\epsilon(L)$ and $v \in L^*$ of length $\lambda_1(L^*)$ ,

\epsilon = \rho_{1/s}(L^*\setminus\{0\}) \ge \rho_{1/s}(v) = \exp\bigl(-\pi(s\lambda_1(L^*))^2\bigr).

Lemma 2.3, Banaszczyk's transference theorem (p. 34:18). For any $n$ -dimensional lattice $L$ ,

1 \le \lambda_1(L)\cdot\lambda_n(L^*) \le n .

Significance

The result. Claim 2.13 shows that the smoothing parameter for a negligible $\epsilon$ exceeds every constant multiple of $1/\lambda_1(L^*)$ and of $\lambda_n(L)/n$ . Together with the upper bound $\eta_\epsilon(L) \le \sqrt{\ln(2n(1+1/\epsilon))/\pi}\,\lambda_n(L)$ of Lemma 2.12, it locates $\eta_\epsilon(L)$ within a polynomial factor of $\lambda_n(L)$ . This is what lets the reduction's guarantees, phrased in $\eta_\epsilon(L)$ , be read as approximation factors for SIVP and GapSVP. The transference theorem is used throughout the geometry of numbers and in lattice-based cryptography to pass between a lattice and its dual.

Formalizing it. The claim and its proof are classical and short, but neither is machine-checked. The mission produces formal definitions of the dual lattice, the successive minima $\lambda_1$ , $\lambda_n$ and the smoothing parameter on EuclideanSpace ℝ (Fin n), a proof that Definition 2.10 is well posed, and a statement of Banaszczyk's transference theorem. The upper bound of the transference theorem is a substantial result in its own right (the paper cites it without proof), and a formal proof of it would be reusable well beyond this mission.

Difficulty

The first inequality of the goal is elementary once the smoothing parameter is known to be attained, with $\rho_{1/\eta}(L^*\setminus\{0\}) = \epsilon$ exactly. That step is not a formality: it needs the continuity and strict monotonicity of an infinite lattice sum in the scale parameter, and the fact that a shortest nonzero dual vector exists, both of which rest on the discreteness of $L^*$ .

The second inequality is a single line in the paper, "by Lemma 2.3", but it uses the upper bound of Banaszczyk's theorem, applied to the dual lattice. The easy lower bound $1 \le \lambda_1(L)\lambda_n(L^*)$ does not suffice, and a Minkowski-type argument gives a bound worse than linear in $n$ . Applying the lemma to $L^*$ also needs $L^*$ to be a lattice with dual $L$ .

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n). A lattice is L : Submodule ℤ _ with [DiscreteTopology L] [IsZLattice ℝ L]. The dual is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.
Every theorem assumes $0 < n$ : the paper's lattices are $n$ -dimensional with $n \ge 1$ . This is the only added hypothesis.
Gaussian sums are real tsums. They are summable over discrete subgroups, so no summability hypotheses are added.
$\eta_\epsilon(L)$ , $\lambda_1$ and $\lambda_n$ are infima (sInf). The paper's "smallest" is the attainment proved in milestones 1 and 2, not built into the definition. $\lambda_1$ and $\lambda_n$ are defined for every $\mathbb{Z}$ -submodule, so they apply to $L^*$ without extra instances.
For $\epsilon \ge 1$ the paper's $\sqrt{\ln(1/\epsilon)/\pi}$ is the square root of a non-positive number; Lean's Real.sqrt gives $0$ there and the goal reduces to true statements. No hypothesis $\epsilon < 1$ is added, since the page says "any $\epsilon > 0$ ".
The goal is a conjunction of both inequalities of the chain, not only the outer comparison $\eta_\epsilon(L) \ge \sqrt{\ln(1/\epsilon)/\pi}\,\lambda_n(L)/n$ , which would be weaker. Lemma 2.3 states both bounds; stating only the easy lower bound would leave the goal's second inequality without its milestone.
No printed statement needed correction.

Contributions welcome: the attainment of $\lambda_1$ and $\lambda_n$ for IsZLattice (and for the dual), the identity $(L^*)^* = L$ in this setting, continuity and monotonicity of Gaussian lattice sums, and above all Banaszczyk's transference theorem.

Selected references

O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, J. ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
W. Banaszczyk, New bounds in some transference theorems in the geometry of numbers, Math. Ann. 296, 625–635, 1993. https://doi.org/10.1007/BF01445125
D. Micciancio, O. Regev, Worst-case to average-case reductions based on Gaussian measures, SIAM J. Comput. 37(1), 267–302, 2007. https://doi.org/10.1137/S0097539705447360

7 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Proximal Alternating Minimization and Projection Methods for Nonconvex Problems: An Approach Based on the Kurdyka-Łojasiewicz Inequality: Non-Divergent Iterates Have Finite Length and a Critical LimitResearch Paper

Motivation

Many problems in signal processing, statistics and decision theory have two blocks of variables coupled by a smooth term: matrix factorization, blind deconvolution, feasibility problems for two sets, and models of two agents adjusting their decisions in turn. Minimizing over one block at a time (alternating minimization, or Gauss–Seidel) is the natural method. Without convexity it can oscillate, and its iterates need not converge. Attouch, Bolte, Redont and Soubeyran (Math. Oper. Res. 35(2), 2010; arXiv:0801.1780) regularize each block step by a proximal term. They prove that, when the objective satisfies the Kurdyka–Łojasiewicz (KL) inequality, every sequence of the method that does not run off to infinity has finite length and converges to a critical point.

Timeline:

1963: Łojasiewicz proves the gradient inequality for real-analytic functions, which gives convergence of bounded gradient trajectories.
1998: Kurdyka extends the inequality to differentiable functions definable in an o-minimal structure.
2006–2007: Bolte, Daniilidis, Lewis and Shiota extend it to nonsmooth lower semicontinuous subanalytic and definable functions, with the limiting subdifferential.
2009: Attouch and Bolte use the Łojasiewicz inequality to prove convergence of the proximal point method for nonconvex functions (Math. Program. 116, 2009).
2010: this paper treats the alternating proximal scheme with a general smooth coupling $Q$ .
2014: Bolte, Sabach and Teboulle replace the exact block minimizations by linearized proximal steps (PALM, Math. Program. 146, 2014).

Setting

Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ and $g:\mathbb R^m\to\mathbb R\cup\{+\infty\}$ be proper (never $-\infty$ , finite somewhere) and lower semicontinuous. Let $Q:\mathbb R^n\times\mathbb R^m\to\mathbb R$ be continuously differentiable, with $\nabla Q$ Lipschitz on bounded sets. This is assumption (H) for

L(x,y)=f(x)+Q(x,y)+g(y).

The product $\mathbb R^n\times\mathbb R^m$ carries the Euclidean norm $\|(x,y)\|^2=\|x\|^2+\|y\|^2$ . Write $\nabla Q=(\nabla_xQ,\nabla_yQ)$ .

Given $(x_0,y_0)$ and step sizes $\lambda_k,\mu_k>0$ , the proximal alternating scheme is

x_{k+1}\in\operatorname{argmin}_u\Big\{L(u,y_k)+\tfrac1{2\lambda_k}\|u-x_k\|^2\Big\},\qquad y_{k+1}\in\operatorname{argmin}_v\Big\{L(x_{k+1},v)+\tfrac1{2\mu_k}\|v-y_k\|^2\Big\}.\tag{5–6}

Assumption (H1) asks that $\inf L>-\infty$ , that $L(\cdot,y_0)$ be proper, and that $\lambda_k,\mu_k\in(r_-,r_+)$ for all $k$ , for some $0<r_-<r_+$ .

The Fréchet subdifferential $\hat\partial L(z)$ is the set of $v$ with $\liminf_{w\to z,\,w\ne z}\big(L(w)-L(z)-\langle v,w-z\rangle\big)/\|w-z\|\ge0$ . The limiting subdifferential $\partial L(z)$ collects the limits of $v_j\in\hat\partial L(z_j)$ along $z_j\to z$ with $L(z_j)\to L(z)$ . A point $z$ is critical if $0\in\partial L(z)$ . $L$ has the KL property at $\bar z\in\operatorname{dom}\partial L$ if there are $\eta>0$ , a neighbourhood $U$ of $\bar z$ and a continuous concave $\varphi:[0,\eta)\to\mathbb R_+$ with $\varphi(0)=0$ , $\varphi\in C^1(0,\eta)$ , $\varphi'>0$ , such that

\varphi'\big(L(z)-L(\bar z)\big)\,\operatorname{dist}\big(0,\partial L(z)\big)\ge1\quad\text{whenever }z\in U,\ L(\bar z)<L(z)<L(\bar z)+\eta .

Formalization targets

Goal: Theorem 9 (p. 11)

If $L$ satisfies (H), (H1) and has the KL property at every point of $\operatorname{dom}\partial L$ , then every sequence of (5–6) satisfies

\|(x_k,y_k)\|\to\infty\qquad\text{or}\qquad\Big(\sum_k\|x_{k+1}-x_k\|+\|y_{k+1}-y_k\|<\infty\ \text{ and }\ (x_k,y_k)\to z^\star,\ 0\in\partial L(z^\star)\Big).

Milestones

Proposition 3 (p. 5): $\partial L(x,y)=\{\partial f(x)+\nabla_xQ(x,y)\}\times\{\partial g(y)+\nabla_yQ(x,y)\}=\partial_xL(x,y)\times\partial_yL(x,y)$ on $\operatorname{dom}L$ .
Lemma 5 (p. 6), in four parts: the scheme is well defined; the decrease estimate (7); summability of the squared steps; the explicit subgradient $(x_k^*,y_k^*)\in\partial L(x_k,y_k)$ (8), which tends to $0$ along bounded subsequences.
Proposition 6 (p. 7): limit points are critical, and $L$ is finite and constant on them.
(19)–(20), (24), (25), (26) from the proof of Theorem 8 (pp. 9–11).
Theorem 8 (p. 9): a local convergence result with explicit constants: $M=2r_+(C+1/r_-)$ , the trapping radius (16), and the tail bound (18).

Significance

Theorem 9 makes the KL inequality the single hypothesis behind global convergence of a nonconvex block method. Semi-algebraic, subanalytic and definable data satisfy it, so the theorem covers sparse and low-rank regularizers, indicator functions of semi-algebraic sets, and polynomial couplings. With $f=\delta_C$ , $g=\delta_D$ and $Q(x,y)=\tfrac12\|x-y\|^2$ it yields convergence of an averaged alternating projection method between two closed sets (§3.4 of the paper). The proof pattern of sufficient decrease, a relative-error subgradient bound and the KL inequality was later abstracted for PALM and many other algorithms. A formal proof of this paper's argument therefore covers the template those analyses reuse.

The result has been proved since 2010. To our knowledge it has not been formalized in any proof assistant. Mathlib has the Fréchet derivative and the gradient, but no limiting subdifferential and no KL theory. The published Prove2Me definitions of the limiting subdifferential and of the KL property (from the Li–Pong ADMM series) are reused here, so this mission also tests that infrastructure on a second algorithm.

Difficulty

The decrease estimate (7) gives only $\sum\|z_{k+1}-z_k\|^2<\infty$ . That makes steps vanish and limit points critical (Proposition 6), but it does not give convergence, because square-summable steps can have infinite total length. Turning square summability into summability needs the KL inequality. That inequality holds only near a critical point and only on a sublevel band, so the iterates must first be shown never to leave a ball $B(\bar z,\rho)$ , by an induction that uses the very finite-length estimate it is trying to establish. The constants in (16) are arranged so that this induction closes. A second difficulty is nonsmooth calculus: the subdifferential sum rule for $f(x)+g(y)+Q(x,y)$ and the closedness of the graph of $\partial L$ along sequences with converging function values. Lower semicontinuity alone does not give convergence of the function values; the proximal inequalities do.

Formalization scope

Everything lives in the namespace ProxAltMin.Conv, in Lean 4 with Mathlib. Conventions:

$\mathbb R^n$ , $\mathbb R^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and the product is the $L^2$ product WithLp 2 (… × …), not the sup-norm product.
$\mathbb R\cup\{+\infty\}$ is EReal with "never $-\infty$ " as part of properness.
The argmin steps are inequalities quantified over all competitors, so every selection of minimizers is covered.
Balls are open.
The KL data $(\eta,U,\varphi)$ of Theorem 8 are explicit parameters, with real $\eta>0$ ; this is equivalent to $\eta\in(0,+\infty]$ .
Inside the proof of Theorem 8 the paper normalizes $L(\bar z)=0$ ; the milestones taken from that proof carry $l_i-\bar l$ instead.
Every infinite sum in a conclusion comes with an explicit summability claim.
Theorem 9's "KL property at each point of the domain of $f$ " is read as "at each point of $\operatorname{dom}\partial L$ ", the domain on which Definition 7 places the KL property.

Theorem and page numbers are those of arXiv:0801.1780v3 (22 Jan 2013), which is the version read; the published article has the same content.

A trivializing formalization is ruled out: the run predicate is satisfiable (Lemma 5's existence milestone; for $f=g=Q=0$ any constant sequence is a run), the constants $M$ and $C$ are tied to the data rather than chosen by the prover, and no conclusion is a sum or a distance whose library value is $0$ on bad input.

Needed infrastructure: the subdifferential calculus behind Proposition 3 (a smooth perturbation and a separable sum), the closedness of the limiting subdifferential, existence of proximal minimizers for coercive lower semicontinuous functions on $\mathbb R^n$ , and the elementary but delicate bookkeeping of Theorem 8. The first two are reusable well beyond this mission. Contributions welcome: proofs of any milestone, and general lemmas on limiting subdifferentials stated as separate theorems.

Selected references

H. Attouch, J. Bolte, P. Redont, A. Soubeyran, Proximal alternating minimization and projection methods for nonconvex problems: an approach based on the Kurdyka–Łojasiewicz inequality, Mathematics of Operations Research 35(2):438–457, 2010. https://doi.org/10.1287/moor.1100.0449 (arXiv:0801.1780v3, https://arxiv.org/abs/0801.1780v3)
H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Mathematical Programming 116:5–16, 2009. https://doi.org/10.1007/s10107-007-0133-5
J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4):1205–1223, 2007. https://doi.org/10.1137/050644641
K. Kurdyka, On gradients of functions definable in o-minimal structures, Annales de l'Institut Fourier 48(3):769–783, 1998. https://doi.org/10.5802/aif.1638
J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Mathematical Programming 146:459–494, 2014. https://doi.org/10.1007/s10107-013-0701-9
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

16 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Algorithms for Scheduling Runway Operations Under Constrained Position Shifting 1: Dynamic Programming on the CPS Network Gives the Minimum MakespanResearch Paper

Motivation

A busy runway is the bottleneck of an airport, and the order in which arriving or departing aircraft use it determines how many operations fit into an hour. Consecutive aircraft must be spaced by minimum separations that depend on both aircraft (a light aircraft behind a heavy one needs a long gap because of wake turbulence), so reordering the first-come-first-served (FCFS) queue can raise throughput considerably. Unrestricted reordering is unacceptable in practice: it makes the controllers' job harder and can push one aircraft to the back of the queue indefinitely. Following Dear (1976), constrained position shifting (CPS) allows each aircraft to move at most $k$ positions away from its FCFS position, with $k$ between 1 and 3 in practice.

Earlier algorithms for CPS either exploited a small number of aircraft types and ignored time windows and precedence constraints (Psaraftis 1980), or needed exponentially many parallel processors (Trivizas 1998), and Carr (2004) conjectured that runway scheduling under CPS has exponential complexity in general. Balakrishnan and Chandran (Oper. Res. 58(6), 2010) showed that, for fixed $k$ , the problem with time windows and precedence constraints is solved by dynamic programming on a network whose size is linear in the number of aircraft. This mission formalizes the core of that result: the network, its precedence pruning, and the dynamic program for the minimum makespan.

Setting

There are $n\ge 1$ aircraft, labelled $0,\dots,n-1$ in FCFS order, and the landing positions are also $0,\dots,n-1$ . An instance consists of

the maximum position shift $k\in\mathbb N$ ;
separations $\delta_{ab}\ge 0$ , the minimum time between a leading aircraft $a$ and a trailing aircraft $b$ , satisfying the triangle inequality $\delta_{ac}\le\delta_{ab}+\delta_{bc}$ (which holds for wake-vortex separations in arrivals-only or departures-only operation);
a time window $[e(a),l(a)]$ for each aircraft;
a finite set of precedence pairs $(x,y)$ of distinct aircraft, meaning that $x$ lands before $y$ .

A $k$ -CPS sequence is a bijection $\sigma$ from positions to aircraft with $|\sigma(p)-p|\le k$ for all $p$ . A feasible schedule is such a $\sigma$ with landing times $t_p$ such that $e(\sigma(p))\le t_p\le l(\sigma(p))$ , $\delta_{\sigma(p)\sigma(q)}\le t_q-t_p$ for all positions $p<q$ , and every precedence pair is respected. The makespan is $t_{n-1}$ , the landing time of the last aircraft.

The CPS network has stages $p=1,\dots,n$ . A node of stage $p$ is a list of $\min\{2k+1,p\}$ distinct aircraft occupying the positions that end at $p-1$ , each within $k$ of its FCFS position; its last entry is its final aircraft. An arc joins a stage- $p$ node $i$ to a stage- $(p+1)$ node $j$ when the first $\min\{2k,p\}$ entries of $j$ are the last $\min\{2k,p\}$ entries of $i$ . A source-sink path picks one node per stage, joined by arcs, and its sequence puts the final aircraft of the stage- $(q+1)$ node at position $q$ . The pruned network $G$ deletes the nodes that violate a precedence pair $(x,y)$ : those containing $y$ before $x$ , or $y$ at a position less than $x-k$ , or $x$ at a position greater than $y+k$ .

On $G$ , with $e(j),l(j)$ the window of the final aircraft of $j$ , $\delta_i(j)$ the separation between the final aircraft of $i$ and $j$ , and $P(j)$ the predecessors of $j$ , the dynamic program is $T^*(j)=e(j)$ at stage 1 and

T^*(j)=\max\Big\{e(j),\ \min_{i\in P(j):\,T^*(i)\le l(i)}\big(T^*(i)+\delta_i(j)\big)\Big\}\qquad(1)

with $\min\emptyset=+\infty$ .

Formalization targets

Goal: §4.1, the minimum makespan rule

\exists\ \text{feasible schedule}\iff \exists\, j\in G_n:\ T^*(j)\le l(j),

\min\{\text{makespan of a feasible schedule}\}=\min\{T^*(j): j\in G_n,\ T^*(j)\le l(j)\},

where $G_n$ is stage $n$ of $G$ ; the second identity is stated as " $\tau$ is the least makespan iff $\tau$ is the least admissible $T^*(j)$ " for every real $\tau$ .

Milestones

Theorem 1. $\sigma$ is a $k$ -CPS sequence iff it is the sequence of a source-sink path of the CPS network.
Lemma 1 (Case I). For $a<b$ , a path whose sequence puts $a$ after $b$ has a node containing $b$ before $a$ .
Lemma 2 (Case II). For $a<b$ , in the position-constrained network, a path whose sequence puts $a$ before $b$ has a node containing $a$ before $b$ .
§3.1 conclusion. The source-sink paths of $G$ are exactly the $k$ -CPS sequences respecting all precedence pairs.
Lemma 3. For every node $j$ of $G$ , $T^*(j)$ is the earliest landing time of the final aircraft of $j$ over all partial schedules ending at $j$ , and $+\infty$ exactly when there is none.

Significance

The network turns a search over permutations into a shortest-path-like computation over $O(n(2k+1)^{2k+1})$ nodes, so for the small values of $k$ used in practice the minimum makespan with time windows and precedence constraints is computed in time linear in $n$ . The same network underlies the paper's algorithms for total delay (§5.2) and, in a time-expanded form, for arbitrary separable costs without the triangle inequality (§6).

The paper's proofs are short and informal. A formalization pins down exactly what $T^*(j)$ means (the paper describes it only as "arrival time of the final aircraft of node $i$ in an optimal solution"), makes precise which nodes the precedence pruning removes, and checks the correctness of the stage- $n$ rule. The result has not been machine-checked before.

Difficulty

Two features of the model make the correctness of the network nontrivial. First, a node records only a window of at most $2k+1$ consecutive positions, so nothing local prevents a path from using the same aircraft twice or omitting one; Theorem 1 asserts that the global sequence is nevertheless a permutation, and Lemmas 1 and 2 assert that precedence, a global property of the sequence, is detected inside single nodes. Second, the recursion (1) adds the separation only between consecutive aircraft, while feasibility constrains every pair of aircraft; the triangle inequality is what reconciles the two, and without it Lemma 3 fails.

The obvious reading of §4.1 also fails: taking the least $T^*(j)$ over all stage- $n$ nodes, as the paper prints, can select a node whose final aircraft lands after its latest time. The goal filters stage $n$ by $T^*(j)\le l(j)$ .

Formalization scope

All data are real numbers; aircraft and positions are Fin n, 0-based; stages are 1-based natural numbers; [NeZero n] encodes $n\ge 1$ . Separations are pairwise in the definition of feasibility, never only consecutive. The recursion takes values in WithTop ℝ, with $\top=+\infty$ ; optima are stated with IsLeast over sets of makespans, never with a real infimum. Precedence pairs are a Finset of ordered pairs of distinct aircraft, covering both of the paper's cases.

Explicit readings of loose phrases:

"corresponding source-sink path" (Theorem 1) is the path whose final aircraft, stage by stage, form the sequence, as defined in the proof;
"the values of $T^*(\cdot)$ " (Lemma 3) are earliest landing times over partial schedules ending at the node: paths in $G$ with times satisfying the windows of the earlier aircraft, the earliest time of the last one, and all pairwise separations;
"the minimum makespan is the lowest value of $T^*(\cdot)$ among all nodes in stage $n$ " is corrected to the nodes with $T^*(j)\le l(j)$ , which is the paper's own feasibility check;
the Case II position filter uses the printed rule ( $<b-k$ , $>a+k$ ).

Not formalized: running times (Proposition 1 and the $O(k)$ preprocessing remark), the predecessor pointers and tie-breaking that reconstruct an optimal sequence, the removal of nodes unreachable from the source or the sink (it does not change the set of source-sink paths), asymmetric shifts (§3.2) and disjoint time windows.

A formalization that defines feasibility with consecutive separations only, defines $T^*$ by the recursion and states Lemma 3 as an unfolding, or states Theorem 1 as "some CPS sequence exists iff some path exists" would be trivial; the statements here avoid all three.

The definitions (instance, $k$ -CPS sequences, the CPS network and its pruning) are shared with the two other missions of this series (total delay, discrete time) and may be consolidated later. Proofs of the milestones, and lemmas about the window structure of the network, are welcome.

Selected references

H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
H. N. Psaraftis, A Dynamic Programming Approach for Sequencing Groups of Identical Jobs, Operations Research 28(6), 1347–1359, 1980. https://doi.org/10.1287/opre.28.6.1347
R. G. Dear, The Dynamic Scheduling of Aircraft in the Near Terminal Area, MIT Flight Transportation Laboratory Report R76-9, 1976.
D. A. Trivizas, Optimal Scheduling with Maximum Position Shift (MPS) Constraints: A Runway Scheduling Application, Journal of Navigation 51(2), 250–266, 1998.
F. R. Carr, Robust Decision-Support Tools for Airport Surface Traffic, Ph.D. thesis, Massachusetts Institute of Technology, 2004.

8 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Inventory Management of a Fast-Fashion Retail Network 1: Expected Sales Under the Major-Size Display Policy Are Non-Decreasing, Discretely Concave and SupermodularResearch Paper

Motivation

Fast-fashion retailers such as Zara replenish their stores several times a week from a central warehouse, and the warehouse holds a limited stock of each garment that must be split across hundreds of stores. Caro and Gallien built the store-level sales model behind the shipment-allocation system they developed with Zara and tested in a live pilot (Caro and Gallien, Inventory Management of a Fast-Fashion Retail Network, working paper, August 2, 2007; published in Operations Research 58(2), 2010). One display policy shapes the model. A garment (a reference) comes in several sizes, a few of which are designated major sizes. As soon as one major size runs out in a store, the whole reference is removed from the shop floor, so the remaining stock of the other sizes stops selling.

The allocation optimization only works if expected store sales have the right shape. They must grow with inventory, show decreasing marginal returns, and show complementarity across sizes. Proposition 1 of the paper establishes these properties for the model. The paper also cites the analogous result of Lu and Song (2003) for assemble-to-order systems as the template for its proof.

Setting

Fix a finite set of sizes $\mathcal S$ , split into the major sizes $\mathcal S^+$ and the minor sizes $\mathcal S^- = \mathcal S \setminus \mathcal S^+$ . Time $t \ge 0$ is measured from the last replenishment, and the next replenishment comes at time $T > 0$ .

Demand is random. On a probability space, each size $s$ has a counting process $N_s(t)$ , the number of sale opportunities for $s$ in $[0, t]$ . It is a Poisson process with rate $\lambda_s > 0$ :

$N_s(0) = 0$ ;
its paths are non-decreasing and right-continuous with jumps of size one;
the increment $N_s(t) - N_s(u)$ is Poisson with mean $\lambda_s (t-u)$ ;
increments over disjoint intervals are independent.

The processes of different sizes are mutually independent. In Lean this family is IsPoissonFamily lam N P.

An inventory vector $q = (q_s) \in \mathbb N^{\mathcal S}$ gives the stock of each size right after replenishment. The virtual stockout time of size $s$ is

\tau_s(q_s) = \inf\{t \ge 0 : N_s(t) = q_s\},

the time at which size $s$ would run out if it stayed on display. For a set of sizes $\mathcal A$ , write $\tau_{\mathcal A} = \min_{s \in \mathcal A} \tau_s(q_s)$ and $a \wedge b = \min(a, b)$ . Under the major-size policy, the random sales over one period are

G(q) = \sum_{s \in \mathcal S^+} N_s(\tau_{\mathcal S^+} \wedge T) + \sum_{s \in \mathcal S^-} N_s(\tau_{\mathcal S^+ \cup \{s\}} \wedge T). \tag{1}

The expected sales function is $g(q) = \mathbb E[G(q)]$ (expectedSales). The proof also uses $h^{\mathcal A}(q) = \mathbb E[\tau_{\mathcal A} \wedge T]$ (hA) and the marginal difference $\Delta_s f(q) = f(q + e_s) - f(q)$ (delta), where $e_s$ is the $s$ -th unit vector.

Formalization targets

Goal: Proposition 1

For every $q \in \mathbb N^{\mathcal S}$ and all sizes $s \ne s'$ :

g \text{ is non-decreasing}, \qquad \Delta_s g(q + e_s) \le \Delta_s g(q), \qquad \Delta_s g(q) \le \Delta_s g(q + e_{s'}),

and $g$ is supermodular on the lattice $\mathbb N^{\mathcal S}$ :

g(q) + g(q') \le g(q \vee q') + g(q \wedge q').

The statement is uniform in the rates, the horizon and the choice of major sizes, so it covers every instance of the model.

Milestones (Appendix §5.1 and §3.1.3, in the order the proof uses them)

On every sample path, $q \mapsto G(q)$ is non-decreasing.
Identity (2): $g(q) = \lambda_{\mathcal S^+} h^{\mathcal S^+}(q) + \sum_{s \in \mathcal S^-} \lambda_s h^{\mathcal S^+ \cup \{s\}}(q)$ , where $\lambda_{\mathcal S^+} = \sum_{s \in \mathcal S^+} \lambda_s$ .
For $s \in \mathcal A$ , $\Delta_s h^{\mathcal A}(q)$ equals an integral over $[0, T]$ of Poisson probabilities, and that integral equals $\frac{1}{\lambda_s}\mathbb P(\tau_s(q_s+1) \le \tau_{\mathcal A \setminus \{s\}} \wedge T)$ .
$\Delta_s h^{\mathcal A}$ is non-increasing in $q_s$ and non-decreasing in $q_{s'}$ for $s' \ne s$ .
On every sample path, $q \mapsto \tau_{\mathcal A} \wedge T$ is supermodular.
$h^{\mathcal A}$ is supermodular.

Significance

The result. Proposition 1 justifies treating each store's expected sales as a concave, complementary function of the size profile. The paper's allocation MIP is built on that structure. It approximates $g$ by a lower envelope of tangents and embeds the approximation in a mixed integer program that allocates warehouse stock across stores. The proposition explains why sending a unit of a major size can raise the value of the minor sizes already in a store. It also explains why the marginal value of a size falls as more of it is shipped. Without these properties a greedy or envelope-based allocation would have no structural footing.

Formalizing it. The result is proved on paper, with one error in the printed proof. The last line of the Appendix display gives $\Delta_s h^{\mathcal A}(q)$ as a probability, but the quantity is a time. The correct value carries a factor $1/\lambda_s$ and has $q_s + 1$ in place of $q_s$ . This mission states the corrected identity. As far as is known, no machine-checked proof of any part of the result exists. A complete development would give a verified link from a continuous-time stochastic model to the discrete convexity properties that inventory optimization relies on. It would also produce reusable facts about Poisson processes and their hitting times along the way.

Difficulty

The monotonicity of $g$ is pathwise and elementary. The other properties are not pathwise properties of $G$ . Under the major-size policy, a realisation of $G$ need not have decreasing increments in $q_s$ . The concavity and the complementarity appear only after taking expectations and rewriting $g$ through the stopping times, using identity (2). That identity is an optional-sampling statement for the compensated Poisson processes at the bounded random times $\tau_{\mathcal A} \wedge T$ . These times depend on several independent processes at once, so the relevant filtration is the joint one. Mathlib has optional sampling only in discrete time.

The marginal-difference formula needs three ingredients:

the tail-integral representation of $\mathbb E[\tau_{\mathcal A} \wedge T]$ ;
the factorisation of $\mathbb P(\tau_{\mathcal A} > t)$ through independence across sizes;
the Erlang law of the hitting times $\tau_s(k)$ .

The first idea, proving concavity of $g$ directly from (1) path by path, fails for the reason above.

Formalization scope

All objects live in the namespace FastFashion.Structure:

Sizes: a Fintype with decidable equality. The major sizes are a Finset Sp and the minor sizes are its complement. No nonemptiness assumption is placed on the sizes or on $\mathcal S^+$ ; $\mathcal S^+ = \emptyset$ is allowed, as in the paper.
Inventories: vectors $q : \mathcal S \to \mathbb N$ with the componentwise order and lattice operations. $e_s$ is Pi.single s 1.
Stockout times: $\tau_s(q_s)$ takes values in WithTop ℝ. It is $+\infty$ on paths that never reach $q_s$ , so it is never Lean's junk value $0$ , and $\tau_\emptyset = +\infty$ . The truncation $\tau_{\mathcal A} \wedge T$ (stopMin) is a real number in $[0, T]$ .
Expectations and probabilities: expectations are Bochner integrals. They need no integrability hypothesis, because $0 \le G(q) \le \sum_s N_s(T)$ and $0 \le \tau_{\mathcal A} \wedge T \le T$ . Probabilities are real numbers.
Supermodularity: Topkis's lattice definition, the published platform definition Supermodularity.Monotonicity.SupermodularOn, applied on the whole lattice.
Poisson family: the processes are independent as whole processes. The σ-algebras generated by all times are independent, not only the one-dimensional marginals.

Two formalizations would trivialize the mission, and neither is used. $g$ is defined as the expectation of $G$ from (1), never by formula (2), and $h^{\mathcal A}$ is never defined by a product-of-probabilities integral. Proposition 1 states both readings of "supermodular": the per-coordinate marginal-difference inequalities and the lattice inequality.

Deviations from the printed text:

The last line of the Appendix display is replaced by $\frac{1}{\lambda_s}\mathbb P(\tau_s(q_s+1) \le \tau_{\mathcal A\setminus\{s\}} \wedge T)$ .
"non-decreasing in $x_s$ " in Proposition 1 is read as $q_s$ .

Infrastructure a complete development needs:

hitting times of counting processes and their Erlang laws;
a continuous-time optional sampling theorem for the compensated Poisson process, or a direct computation from independent increments;
the tail formula $\mathbb E[X] = \int_0^\infty \mathbb P(X > t)\,dt$ for bounded non-negative $X$ ;
lattice facts about minima of single-variable increasing functions.

The Poisson-process and hitting-time lemmas are reusable well beyond this mission and are welcome as separate contributions. The companion mission on the paper's tangent-envelope approximation uses the same model layer.

Selected references

F. Caro, J. Gallien, Inventory Management of a Fast-Fashion Retail Network, working paper, August 2, 2007; published in Operations Research 58(2):257–273, 2010. https://doi.org/10.1287/opre.1090.0698
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
Y. Lu, J.-S. Song, Order-Based Cost Optimization in Assemble-to-Order Systems, Operations Research 53(1):151–169, 2005 (working paper 2003). https://doi.org/10.1287/opre.1040.0146
I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Algorithms for Scheduling Runway Operations Under Constrained Position Shifting 2: The Minimum Total Delay Is a Shortest Source-Sink Path in the CPS NetworkResearch Paper

Motivation

Runway capacity is the binding constraint at many busy airports. An aircraft landing or taking off behind another must wait a minimum separation time that depends on the two aircraft's weight classes, because of wake vortices; the US Federal Aviation Administration publishes these spacing requirements. Reordering aircraft changes the sum of the separations incurred and hence the delays, but unrestricted reordering is unacceptable to airlines and controllers: an aircraft that arrived early could be pushed to the end of the queue. Constrained position shifting (CPS), introduced by Psaraftis (1980) and used in the United States and Europe since, allows each aircraft to move at most $k$ positions from its first-come-first-served (FCFS) position.

Balakrishnan and Chandran (Operations Research 58(6), 2010) recast CPS scheduling as dynamic programming on a layered network, the CPS network, whose size is polynomial in the number of aircraft $n$ for fixed $k$ . Their §4 minimizes the makespan (the landing time of the last aircraft). §5.2 minimizes the total delay, equivalently the average delay, which measures passenger and airline cost more directly. This mission formalizes §5.2.

Setting

There are $n$ aircraft labelled $1,\dots,n$ in FCFS order, a maximum position shift $k\in\mathbb N$ , separations $\delta_{ab}\ge 0$ (the minimum time between leading aircraft $a$ and trailing aircraft $b$ ), and a finite set of precedence pairs $(x,y)$ with $x\ne y$ , meaning that $x$ must land before $y$ . The separations satisfy the triangle inequality $\delta_{ac}\le\delta_{ab}+\delta_{bc}$ , as wake-vortex separations do for arrivals-only or departures-only operations.

A $k$ -CPS sequence is a permutation $\sigma$ of the aircraft (position $p$ receives aircraft $\sigma(p)$ ) with $|\sigma(p)-p|\le k$ for every $p$ . A feasible schedule is a $k$ -CPS sequence that places $x$ before $y$ for each precedence pair, together with landing times $t_1,\dots,t_n$ (by position) such that

t_p\ge 0,\qquad t_q-t_p\ge\delta_{\sigma(p)\sigma(q)}\quad(p<q).

There are no time windows. Its total delay is $t_1+\dots+t_n$ , measured from time $0$ , at which all aircraft are available.

The CPS network has stages $1,\dots,n$ . A node of stage $p$ is a sequence of $\min\{2k+1,p\}$ distinct aircraft that can occupy positions $p-\min\{2k+1,p\}+1,\dots,p$ (each within $k$ of its position). Its last aircraft is its final aircraft. An arc joins a stage- $p$ node $i$ to a stage- $(p+1)$ node $j$ when the sequences overlap: the first $\min\{2k,p\}$ aircraft of $j$ are the last $\min\{2k,p\}$ aircraft of $i$ . A source-sink path picks one node per stage, and its sequence assigns position $p$ to the final aircraft of the stage- $p$ node. Precedence is incorporated by deleting every node that places $y$ before $x$ for some pair $(x,y)$ , or that places an aircraft outside the positions a pair allows it (§3.1). The result is the pruned network $G$ . For nodes $i,j$ , $\delta_i(j)$ is the separation between their final aircraft.

For a node $j$ in stage $p$ and times $t_1,\dots,t_p$ along a path to $j$ , the paper uses the partial objective

\theta_j(p)=t_1+\dots+t_{p-1}+(n-p+1)\,t_p .

Formalization targets

Goal: the shortest-path equivalence (§5.2, p. 1656)

Give the arc $(i,j)$ from stage $p-1$ to stage $p$ the distance $(n-p+1)\delta_i(j)$ , and source and sink arcs distance $0$ . Then a feasible schedule exists if and only if $G$ has a source-sink path, and

\min_{(\sigma,t)\ \text{feasible}}\ \sum_{p=1}^{n}t_p\;=\;\min_{v\ \text{source-sink path of }G}\ \sum_{p=2}^{n}(n-p+1)\,\delta_{v_{p-1}}(v_p),

where each minimum exists exactly when the other does.

Milestones

Theorem 1 with Lemmas 1–2 (pp. 1652–1654): the source-sink paths of $G$ are exactly the $k$ -CPS sequences respecting the precedence pairs.
Proposition 2 (p. 1656): in a schedule of minimum total delay, $t_p-t_{p-1}=\delta_{\sigma(p-1)\sigma(p)}$ for every $p\ge 2$ .
Proposition 3 (p. 1656): all paths from the source to a node lying on some source-sink path contain the same set of aircraft.
The recursion of §5.2 (p. 1656): with $\theta^*_j(p)$ the minimum of $\theta_j(p)$ over partial schedules ending at $j$ , $\theta^*_j(1)=0$ and

\theta^*_j(p)=\min_{i\in P(j)}\big(\theta^*_i(p-1)+(n-p+1)\,\delta_i(j)\big),

where $P(j)$ is the set of predecessors of $j$ in $G$ .

Significance

The result turns a sequencing problem over up to $n!$ orders into a shortest-path computation on a directed acyclic graph with $O(n(2k+1)^{2k+1})$ nodes, and it does so while respecting precedence constraints, which earlier CPS algorithms (Psaraftis 1980; Trivizas 1998) could not handle. It is the average-delay counterpart of the makespan algorithm of §4 and shares its network. The same network carries the discrete-time models of §6.

The paper's proof of the equivalence is one sentence ("follows from properties of shortest paths and is omitted here"). Propositions 2 and 3 are proved in a few lines, and Theorem 1 by an argument about windows of $2k+1$ consecutive positions. None of these results has a machine-checked proof. A formal development makes explicit the conventions the prose leaves implicit (the time origin, pairwise separations, which nodes Proposition 3 refers to) and checks that the recursion and the shortest-path value really compute the minimum total delay.

Difficulty

The arc distances weight the separation into stage $p$ by $n-p+1$ , the number of aircraft whose landing it delays. The equivalence needs two directions. A path's length must be the total delay of the schedule that lands each aircraft at its predecessor's time plus the separation, and that schedule must satisfy every pairwise separation, not only the consecutive ones; this is where the triangle inequality enters. Conversely, every feasible schedule must have total delay at least the length of its sequence's path, and every feasible sequence must be a path of $G$ . The last point is Theorem 1 with precedence pruning: a node sees only $2k+1$ consecutive positions, so detecting a violated precedence pair inside one node requires the position filter of §3.1 for pairs that reverse FCFS order. Proposition 3 is false for nodes that lie on no source-sink path, which the printed statement does not exclude.

Formalization scope

Aircraft and positions are Fin n, 0-based, and stages are 0-based natural numbers, so the arc into stage $s$ has distance $(n-s)\delta_i(j)$ . Separations are real, nonnegative and satisfy the triangle inequality; feasibility requires them between every pair of positions. Landing times are real and nonnegative. The paper fixes no time origin, but its path length equals the total delay exactly when delays are measured from $0$ , and without a lower bound on the times the objective has no minimum. Minima are stated with IsLeast on sets of values, never with a real infimum. Feasibility and the existence of a path are stated separately, because the equality of least elements alone does not force them to exist.

The following loose phrases are given explicit readings. "In an optimal solution" (Proposition 2) means a feasible schedule whose total delay is at most that of every feasible schedule. "The CPS network" in Proposition 3 means nodes lying on a source-sink path, stated for the network without precedence pruning, which also covers the pruned one. " $\theta^*$ " means the least element of the set of values of $\theta_j(p)$ over partial schedules ending at $j$ , and the printed $\theta^*_j(s)$ is read as $\theta^*_j(p)$ . The boundary value $\theta^*_j(1)=0$ is not printed and is stated explicitly. Precedence pruning uses the printed Case II rule. Running times (the $O(n(2k+1)^{2k+2})$ bound) are not formalized.

A trivializing formalization would require separations only between consecutive aircraft, define the minimum by the recursion itself, or use a network whose nodes need not be distinct or admissible. Here the minimum is defined directly over feasible schedules, separations are pairwise, and the nodes are checked against the paper's Figure 1 (stage sizes 2, 4, 7, 14, 14, 7 and 13 paths for $n=6$ , $k=1$ ).

The development needs finite sums, permutations of Fin n and lists. The network layer (stages, arcs, precedence pruning, Theorem 1) is shared with the makespan and discrete-time missions of this series and reusable for any CPS objective. Proofs of any milestone, alternative proofs of the goal, and generalizations (asymmetric shifts, §3.2) are welcome.

Selected references

H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
H. N. Psaraftis, A Dynamic Programming Approach for Sequencing Groups of Identical Jobs, Operations Research 28(6), 1347–1359, 1980. https://doi.org/10.1287/opre.28.6.1347
R. G. Dear, Y. S. Sherif, An Algorithm for Computer Assisted Sequencing and Scheduling of Terminal Area Operations, Transportation Research Part A 25(2–3), 129–139, 1991.
D. A. Trivizas, Optimal Scheduling with Maximum Position Shift (MPS) Constraints: A Runway Scheduling Application, Journal of Navigation 51(2), 250–266, 1998.
R. de Neufville, A. Odoni, Airport Systems: Planning, Design, and Management, McGraw-Hill, 2003.

6 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Reliable Facility Location Design Under the Risk of Disruptions 1: With R = J the Compact Level-Assignment Formulation Equals the Scenario-Based Stochastic ProgramResearch Paper

Motivation

Facility location models decide where to open depots, warehouses or service centres and which customers each one serves. Classical models assume that an open facility always works. In practice facilities are disrupted by weather, strikes, power loss or supplier failure, and a network designed for normal operation can become very expensive when its nearest facilities go down. Reliable facility location models place facilities so that the sum of the fixed cost and the expected transportation cost, taken over random facility failures, is minimal.

Cui, Ouyang and Shen (UCTC-FR-2010-02, 2010; published as Oper. Res. 58(4):998–1011) study the case in which each site fails independently with its own probability. The most direct model of this situation is a scenario-based stochastic program: list every pattern of failures, give it its probability, and let each customer be served optimally in each pattern. That program has $2^J$ scenarios for $J$ candidate sites and cannot be written down for realistic $J$ . The paper proposes instead a compact formulation in which each customer receives an ordered list of backup facilities ("levels") and the probability that each level is the one that serves her is carried by a small set of recursive variables. This mission is about the claim that the compact model loses nothing.

The level-assignment technique comes from Snyder and Daskin (Transp. Sci. 39(3):400–416, 2005), who treated the case of one common failure probability for all sites. The uniform-probability model of Snyder and Shen's textbook is on the platform as SupplyChainTheory_disruptions; it is a different model (one $q$ , no cap on the number of levels) and is not reused here.

Setting

There are $I$ customers $i = 0,\dots,I-1$ with demand rates $\lambda_i \ge 0$ and $J$ candidate sites $j = 0,\dots,J-1$ with fixed costs $f_j$ and failure probabilities $0 \le q_j < 1$ . Failures are independent. Shipping one unit from site $j$ to customer $i$ costs $d_{ij}$ , and each unit of missed demand of customer $i$ costs a penalty $\phi_i$ . An emergency facility with index $J$ never fails ( $q_J = 0$ ), costs nothing to open ( $f_J = 0$ ), and "serves" at the penalty cost $d_{iJ} = \phi_i$ .

The compact model (RUFL). Each customer is assigned to facilities at levels $r = 0,\dots,R$ , with $R \ge 1$ ; a level- $r$ facility serves her exactly when all her facilities at levels $0,\dots,r-1$ have failed. The variables are $X_j\in\{0,1\}$ (site $j$ open), $Y_{ijr}\in\{0,1\}$ (facility $j$ is customer $i$ 's level- $r$ facility) and $P_{ijr}$ , the probability that $j$ serves $i$ at level $r$ . Constraints (1b)–(1d) say that each level holds one facility until the emergency facility appears, which happens exactly once, and that only open sites are used, each at most once. Constraints (1e)–(1f) fix $P$ : $P_{ij0} = 1-q_j$ and $P_{ijr} = (1-q_j)\sum_{k<J}\frac{q_k}{1-q_k}P_{i,k,r-1}Y_{i,k,r-1}$ . The objective is

\Phi(X,Y,P) = \sum_{j=0}^{J-1} f_jX_j + \sum_{i=0}^{I-1}\sum_{j=0}^{J}\sum_{r=0}^{R}\lambda_i d_{ij}P_{ijr}Y_{ijr}.

The scenario model (SSP). A scenario is $\omega\in\Omega=\{0,1\}^J$ , with $\delta_{j\omega}=1$ if site $j$ operates in $\omega$ (and $\delta_{J\omega}=1$ always). Its probability is $p_\omega = \prod_{j<J}(1-q_j)^{\delta_{j\omega}}q_j^{1-\delta_{j\omega}}$ . With $Y_{ij\omega}\in\{0,1\}$ (customer $i$ served by $j$ in $\omega$ ), (SSP) minimizes

\Psi(X,Y) = \sum_{j=0}^{J-1} f_jX_j + \sum_{i=0}^{I-1}\sum_{j=0}^{J}\sum_{\omega\in\Omega}\lambda_i d_{ij}p_\omega Y_{ij\omega}

subject to $\sum_{j=0}^{J}Y_{ij\omega}=1$ and $Y_{ij\omega}\le\delta_{j\omega}X_j$ for regular $j$ .

Formalization targets

Goal: Proposition 1 (p. 10)

If $R = J$ , both programs have optimal solutions, and for every optimal $(X,Y,P)$ of (RUFL) and every optimal $(X',Y')$ of (SSP),

\Phi(X,Y,P) = \Psi(X',Y').

The paper states this as "formulation (1a)–(1g) is equivalent to the stochastic programming formulation that covers all failure scenarios"; its proof shows equality of optimal values, and that is the reading formalized.

Milestones (Appendix A.1, pp. 32–34)

Scenario-probability identity. For distinct regular sites $j(0),\dots,j(r-1)$ and a facility $j(r)$ not among them, the scenarios in which $j(0),\dots,j(r-1)$ fail and $j(r)$ operates have total probability

\sum_{\omega\in\Omega(i,r)}p_\omega = (1-q_{j(r)})\prod_{\ell=0}^{r-1}q_{j(\ell)}.

(RUFL) → (SSP). Every (RUFL)-feasible $(X,Y,P)$ has an (SSP)-feasible $(X,Y')$ with $\Psi(X,Y') = \Phi(X,Y,P)$ , for any $R$ .
Normalization. Some optimal solution of (SSP), with the same $X$ , serves every customer in every scenario by her closest operating open facility, ties to the lowest index.
(SSP) → (RUFL). If $R = J$ , every normalized (SSP)-feasible $(X,Y)$ has a (RUFL)-feasible $(X,Y',P')$ with $\Phi(X,Y',P') = \Psi(X,Y)$ .

Significance

The proposition says that, with enough levels, the compact model is exact: its optimal value is the true minimum expected cost over all failure patterns. The compact model has $O(IJR)$ variables and constraints against $O(IJ2^J)$ for (SSP), and after the standard linearization of the products $P_{ijr}Y_{ijr}$ it is an ordinary mixed-integer program to which the paper's Lagrangian relaxation applies. For $R<J$ the paper notes the compact model is in general not equivalent; Proposition 1 is the anchor that says what the parameter $R$ trades away.

The result is proved in the paper; as far as we know it has not been formalized. The work here is to formalize that proof: the product-measure computation behind milestone 1, the two explicit solution maps, and the exchange argument behind the normalization. The probability identity for "first success in an ordered list of independent trials" and the scenario-to-level bookkeeping are reusable for other reliability models built on Snyder–Daskin levels.

Difficulty

The cost identities are routine once the right bookkeeping is in place; the obstacle is that bookkeeping. In direction (RUFL) → (SSP) one must show that the recursion (1e)–(1f), which multiplies by $q_k/(1-q_k)$ and sums over all regular $k$ , collapses to the closed product $(1-q_{j(r)})\prod_{\ell<r}q_{j(\ell)}$ along a customer's assigned list, using that (1b)–(1d) put exactly one facility on each level until the emergency facility and that (1c) forbids repeats. Then the sum over the $2^J$ scenarios must be regrouped by the first operating facility on that list, which needs milestone 1 on a product space.

The converse direction is where $R=J$ enters, and the naive attempt fails: an arbitrary optimal (SSP) solution may serve a customer by different, equally good facilities in different scenarios in ways that no single ordered list reproduces. The normalization step removes this freedom; only after it can one read off a single list per customer, and $R=J$ guarantees that this list (all open sites no farther than the penalty, then $J$ ) fits on the available levels.

Formalization scope

Indices are 0-based; facilities are Fin (J+1) with Fin.last J the emergency facility, and levels are Fin (R+1). The extended data $d_{iJ}=\phi_i$ , $q_J=0$ , and the conventions $\delta_{J\omega}=1$ , $X_J=1$ are definitions, not hypotheses. Scenarios are Fin J → Bool and $p_\omega$ is the explicit finite product; no measure theory is involved, and (17a) is a finite sum. Binary variables are real numbers constrained to $\{0,1\}$ . $R = J$ is expressed by taking the instance type Instance I J J; with the standing $R\ge 1$ this means $J\ge1$ . Demand rates are nonnegative; no sign is assumed on $d$ , $\phi$ or $f$ .

Two printed constraints are corrected, and the formalization commits to the corrections. The first sum in (1b) is printed over the regular sites $j\le J-1$ ; it runs here over all $J+1$ facilities, as the paper's own reading of (1b) requires. Constraint (17c) is printed as $\sum_i Y_{ij\omega}\le\delta_{j\omega}X_j$ , which gives each site a capacity of one customer per scenario and makes Proposition 1 false; it is stated here per customer, $Y_{ij\omega}\le\delta_{j\omega}X_j$ .

The goal asserts existence of optimal solutions of both programs before comparing their values, so it cannot hold vacuously. Contributions welcome: proofs of the milestones, a general lemma on the probability that the first success among independent Bernoulli trials occurs at a given position, and an existence-of-optimum lemma for finite binary programs.

Selected references

X. Cui, Y. Ouyang, Z.-J. M. Shen, Reliable Facility Location Design under the Risk of Disruptions, UCTC-FR-2010-02, University of California Transportation Center, 2010; Operations Research 58(4):998–1011, 2010. https://doi.org/10.1287/opre.1090.0801
L. V. Snyder, M. S. Daskin, Reliability models for facility location: the expected failure cost case, Transportation Science 39(3):400–416, 2005. https://doi.org/10.1287/trsc.1040.0107
H. D. Sherali, A. Alameddine, A new reformulation-linearization technique for bilinear programming problems, Journal of Global Optimization 2(4):379–410, 1992. https://doi.org/10.1007/BF00122429

8 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Reliable Facility Location Design Under the Risk of Disruptions 2: Optimal Solutions Order Each Customer's Assignment Levels by DistanceResearch Paper

Why backup assignments matter

A facility location plan decides which sites to open and which customers each site serves. Real facilities fail: plants are shut by strikes, warehouses by floods, distribution centres by power outages. When a customer's facility is down, she is served by a backup facility, or not served at all at a penalty. Reliable facility location chooses sites and backup assignments together, minimizing fixed costs plus the expected transportation and penalty cost over the random failures.

Snyder and Daskin (2005) introduced the level-assignment formulation in which every customer receives a ranked list of facilities, and they assumed all sites fail with the same probability. Cui, Ouyang and Shen (2010) allow each site its own failure probability $q_j$ , which is the realistic case: a site in a flood plain and a site inland do not fail equally often. Their compact mixed-integer program (RUFL) is the subject of this mission.

Timeline.

Snyder and Daskin (2005), Transportation Science 39(3): level-assignment formulation of the reliability P-median and UFL problems, equal failure probability $q$ ; consecutive assignments are ordered by distance in an optimal solution.
Snyder and Shen, Fundamentals of Supply Chain Theory, Theorem 9.10 (textbook treatment): the same ordering for the reliable fixed-charge location problem with $0<q<1$ and positive demands.
Cui, Ouyang and Shen (2010), UCTC-FR-2010-02 / Operations Research 58(4): site-dependent failure probabilities $q_j$ , a cap $R$ on the number of levels, and Proposition 2, the ordering result for this model.

The model (RUFL)

There are customers $i = 0,\dots,I-1$ with demand rates $\lambda_i$ , and candidate sites $j = 0,\dots,J-1$ with fixed costs $f_j$ and failure probabilities $0 \le q_j < 1$ ; failures are independent. Shipping one unit from $j$ to $i$ costs $d_{ij}$ , and each unserved unit of customer $i$ costs a penalty $\phi_i$ . An emergency facility with index $J$ represents non-service: $f_J = 0$ , $q_J = 0$ and $d_{iJ} = \phi_i$ .

Each customer is assigned at levels $r = 0,\dots,R$ , $R\ge 1$ . Her level- $r$ facility serves her exactly when all her facilities at levels $0,\dots,r-1$ have failed. The variables are $X_j\in\{0,1\}$ (site $j$ open), $Y_{ijr}\in\{0,1\}$ (facility $j$ is customer $i$ 's level- $r$ facility) and $P_{ijr}$ , the probability that $j$ serves $i$ at level $r$ . (RUFL) minimizes

\Phi(X,Y,P) = \sum_{j=0}^{J-1} f_jX_j + \sum_{i=0}^{I-1}\sum_{j=0}^{J}\sum_{r=0}^{R}\lambda_i d_{ij}P_{ijr}Y_{ijr}

subject to: at every level a customer has exactly one facility unless she has already reached the emergency facility (1b); only open sites are used, each at most once (1c); the emergency facility is assigned exactly once (1d); and the probabilities follow the transition equations

P_{ij0} = 1-q_j,\qquad P_{ijr} = (1-q_j)\sum_{k=0}^{J-1}\frac{q_k}{1-q_k}P_{i,k,r-1}Y_{i,k,r-1}\quad (1\le r\le R).

So if a customer's levels are $j_0, j_1, \dots$ , then $P_{i j_r r} = (1-q_{j_r})\,q_{j_0}\cdots q_{j_{r-1}}$ .

Formalization targets

Goal: Proposition 2

Assume $\lambda_i > 0$ for every customer and $q_k > 0$ for every regular site. In every optimal solution $(X,Y,P)$ of (RUFL),

Y_{ijr} = 1,\ Y_{ik,r+1} = 1 \ \Longrightarrow\ d_{ij}\le d_{ik}\qquad (0\le r,\ r+1\le R,\ 0\le j,k\le J),

where $d_{iJ} = \phi_i$ .

Milestones (the proof of Appendix A.2)

Swap identity. If $(X,Y,P)$ is feasible with $Y_{ijr} = Y_{ik,r+1} = 1$ for regular $j,k$ , exchanging $j$ and $k$ and recomputing $P$ gives a feasible solution whose cost changes by

\lambda_i(1-q_k)(d_{ik}-d_{ij})P_{ijr}.

Emergency case. If instead $k = J$ , moving $J$ up to level $r$ and dropping $j$ gives a feasible solution whose cost changes by $\lambda_i P_{ijr}(\phi_i - d_{ij})$ .
Positivity. If every regular $q_k>0$ , an assigned facility has $P_{ijr}>0$ .

Significance

Proposition 2 says that for a given set of facilities assigned to a customer, the optimal order of the levels depends only on the distances, not on the failure probabilities. A solution method may therefore sort each customer's assigned facilities by distance instead of searching over orders. The paper's Lagrangian subproblem (RSP $_i$ ) uses exactly this: "following a similar argument to Proposition 2" (§3.3.1, p. 13), its objective depends only on the set of facilities chosen, which is what makes the set function of Proposition 3 (a separate mission of this series) well defined. The proposition does not say that the $R$ nearest open facilities are the right ones: the paper's Example 1 (p. 11) shows a farther but more reliable facility can be optimal.

The result is proved in the paper; no machine-checked proof exists. The equal-probability special case is published on Prove2Me as SupplyChainTheory.rflp_ordered_assignments (Snyder–Shen Theorem 9.10), in a different model (one $q$ , no level cap). This mission adds the site-dependent case with a level cap, and it makes explicit two hypotheses the printed statement omits.

Difficulty

The exchange argument is short on paper, but its bookkeeping is exactly where a formal proof has to work. The paper's modified $P'$ keeps the old values at unlisted indices, and that array does not satisfy the transition equations, so feasibility of the swapped solution has to be shown with the recomputed probabilities, level by level, including the fact that levels after $r+1$ are unchanged. The emergency case is dismissed in one sentence; its cost change must be computed. Finally, " $<0$ " needs $\lambda_i>0$ and $P_{ijr}>0$ ; the naive reading of the printed proposition, with $q_j = 0$ allowed, is false, because a level-0 facility that never fails leaves all later levels with probability zero and in arbitrary order.

Formalization scope

Indices are 0-based. Facilities are Fin (J+1) with the emergency facility Fin.last J; levels are Fin (R+1); the extended data $d_{iJ}=\phi_i$ , $q_J=0$ are definitions. $X$ , $Y$ , $P$ are real arrays, with (1g) requiring $X$ , $Y$ to be $0$ or $1$ . Constraint (1b) is printed with its first sum ending at $J-1$ ; it is formalized with the sum over all $j \le J$ , the reading the paper's own explanation of (1b) gives. "Optimal" means feasible with objective at most that of every feasible solution; the feasible set is nonempty (send every customer to $J$ at level 0), so the goal is not vacuous. Proposition 2 carries the hypotheses $\lambda_i>0$ and $q_k>0$ ; without them it is false, and a statement that dropped them would be unprovable rather than trivial. The level $r$ ranges over $0\le r\le R-1$ , the range in which level $r+1$ exists.

The development needs only finite sums and a recursion over levels; no measure theory is required. The recomputed probabilities transProb and the two moves swapY, emergencyUpY are reusable for any exchange argument on this formulation. Proofs of the milestones, of the goal, and of the equivalence of the transition equations with the closed product form are welcome.

Selected references

Cui, T., Ouyang, Y., Shen, Z.-J. M., Reliable Facility Location Design under the Risk of Disruptions, UCTC-FR-2010-02, University of California Transportation Center, 2010; published in Operations Research 58(4):998–1011, 2010. https://doi.org/10.1287/opre.1090.0801
Snyder, L. V., Daskin, M. S., Reliability Models for Facility Location: The Expected Failure Cost Case, Transportation Science 39(3):400–416, 2005. https://doi.org/10.1287/trsc.1040.0107
Snyder, L. V., Shen, Z.-J. M., Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, §9.6. https://doi.org/10.1002/9781119584445

6 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

A Combinatorial Algorithm Minimizing Submodular Functions in Strongly Polynomial Time II: Minimizing a Submodular Function over a Ring Family Reduces to Minimizing over All SubsetsResearch Paper

Motivation

A submodular function on a finite set $V$ is a function $f$ on subsets of $V$ with $f(X \cup Y) + f(X \cap Y) \le f(X) + f(Y)$ . Minimizing such a function is one of the central tractable problems of combinatorial optimization: it contains minimum cuts in directed graphs, matroid intersection and polymatroid problems, and many scheduling and facility-location subproblems. Grötschel, Lovász and Schrijver showed in 1981 that it can be done in polynomial time with the ellipsoid method; in 2000, Schrijver (JCTB 80, 346–355) and, simultaneously, Iwata, Fleischer and Fujishige (J. ACM 48, 2001) gave the first combinatorial strongly polynomial algorithms.

In many applications the function is not defined on all subsets of $V$ but only on a ring family: a collection closed under union and intersection, such as the order ideals of a precedence relation in scheduling, or the sets of a closure system. The last section of Schrijver's paper (§6, pp. 353–354) shows that nothing is lost: any algorithm minimizing submodular functions on all subsets of $V$ also minimizes a submodular function given only on a ring family. This mission formalizes that reduction.

Setting

Let $V$ be a finite set. A collection $\mathcal C$ of subsets of $V$ is a ring family if $X \cup Y \in \mathcal C$ and $X \cap Y \in \mathcal C$ whenever $X, Y \in \mathcal C$ . A real function $f$ is submodular on $\mathcal C$ if

f(X \cup Y) + f(X \cap Y) \le f(X) + f(Y) \qquad (X, Y \in \mathcal C).

Following the paper, $\mathcal C$ is normalized: $\emptyset \in \mathcal C$ , $V \in \mathcal C$ , and $M_u \ne M_v$ for all $u \ne v$ , where $M_v$ is the smallest set of $\mathcal C$ containing $v$ . (Elements with the same $M_v$ can be identified.) Under this normalization $\mathcal C$ is the family of lower ideals of a partial order on $V$ .

For $X \subseteq V$ , the closure $\overline X$ is the smallest set of $\mathcal C$ containing $X$ . For $v \in V$ , $L_v$ is the largest set of $\mathcal C$ not containing $v$ . The paper defines weights

c(v) := \max\{0,\ f(L_v) - f(L_v \cup \{v\})\} \qquad (23)

with the modular extension $c(X) := \sum_{v \in X} c(v)$ , and the function on all subsets of $V$

g(X) := f(\overline X) + c(\overline X) \qquad (X \subseteq V). \qquad (26)

In Lean, $V$ is a type with [Fintype V] [DecidableEq V], subsets are Finset V, $\mathcal C$ is C : Set (Finset V), and the objects above are IsRingFamily C, SubmodularOn C f, closure C X, M C v, L C v, cw C f v (for $c(v)$ ), csum C f X (for $c(X)$ ) and g C f X, all in the namespace SchrijverSFM.Ring.

Formalization targets

Goal: the reduction

Under the normalization above, for $f$ submodular on $\mathcal C$ :

g \text{ is submodular on all subsets of } V,

and, if $U \subseteq V$ minimizes $g(U) - c(U)$ over all subsets of $V$ , then $\overline U \in \mathcal C$ and

f(\overline U) \le f(T) \qquad \text{for all } T \in \mathcal C.

Both conjuncts are needed: the second alone follows almost from the definitions, while the first is what makes an all-subsets algorithm applicable to $g - c$ in the first place.

Milestones

$\mathcal C$ is the collection of all lower ideals of some partial order on $V$ (p. 353).
$L_v$ is the largest set in $\mathcal C$ not containing $v$ , equal to the union of the $M_u$ not containing $v$ , and $L_v \cup \{v\} \in \mathcal C$ (p. 353, (23)).
The one-element step (25): $f(X) \le f(Y) + c(v)$ for $X, Y \in \mathcal C$ , $Y = X \cup \{v\}$ , $v \notin X$ .
Monotonicity (24): $f(Y) + c(Y) \ge f(X) + c(X)$ for $X \subseteq Y$ in $\mathcal C$ .
The closure identities $\overline X \cup \overline Y = \overline{X \cup Y}$ and $\overline X \cap \overline Y \supseteq \overline{X \cap Y}$ .
Display (27): $g$ is submodular.
Transfer of minimizers: if $U$ minimizes $g - c$ over $2^V$ , then $\overline U$ minimizes $f$ over $\mathcal C$ .

Significance

The reduction means that a single algorithm for unconstrained submodular minimization serves for every ring family, given only the sets $M_v$ . This is how ring-family constrained problems (for example minimum-cost closures and precedence-constrained scheduling objectives) are routinely handed to general submodular-minimization codes, and it is the standard justification for stating submodular minimization algorithms over $2^V$ only.

On the formal side, the mission produces a small reusable layer on ring families of finite sets (closure operator, the lower-ideal representation, the largest set avoiding an element) together with the monotonization trick (24), which is of independent use whenever a function on a lattice of sets has to be made monotone by a modular correction. The result is classical and its proof in the paper is complete; to our knowledge no machine-checked version exists. Companion mission I of this series formalizes the algorithm of §§2–5 itself; this mission does not depend on it, since the algorithm enters only as the hypothesis that a minimizer $U$ of $g - c$ is given.

Difficulty

Every step is elementary, but two points are easy to get wrong. First, (24) is proved on the page by assuming $Y = X \cup \{v\}$ ; reducing the general case $X \subseteq Y$ to such one-element steps inside $\mathcal C$ requires the normalization $M_u \ne M_v$ : without it a ring family can jump by more than one element (for $\mathcal C = \{\emptyset, V\}$ with $|V| = 2$ the inequality (24) fails for suitable $f$ ). Second, the weights $c(v)$ evaluate $f$ at $L_v \cup \{v\}$ , which belongs to $\mathcal C$ only because of the same normalization; a formalization that drops it lets values of $f$ outside $\mathcal C$ leak into $c$ and $g$ . The submodularity proof (27) also needs the asymmetric closure facts — equality for unions but only containment for intersections — which is exactly why the monotonicity (24) is required.

Formalization scope

$V$ is a finite type with decidable equality; subsets are Finset V; $\mathcal C$ is a Set (Finset V).
$f$ is a real function on all of Finset V; only its values on $\mathcal C$ matter, and under the hypotheses no other value enters $c$ , $g$ or the conclusions. The paper allows any ordered field; the formalization uses $\mathbb R$ .
The normalization of p. 353 is assumed as hypotheses: ∅ ∈ C, Finset.univ ∈ C, and M C u ≠ M C v for u ≠ v. No hypothesis $f(\emptyset) = 0$ is made; §6 does not use it.
The closure is the intersection (Finset.inf) of the sets of $\mathcal C$ containing $X$ , and $L_v$ the union (Finset.sup) of the sets of $\mathcal C$ avoiding $v$ ; their default values on an empty family are never reached under the hypotheses.
$c(X)$ is the modular extension $\sum_{v \in X} c(v)$ ; the $\max\{0, \cdot\}$ in (23) is kept, so $c \ge 0$ .
Submodularity of $g$ on all subsets is the published platform definition NonmonotoneSubmod.Shared.Submodular.
Not formalized: the running-time claims of §6 ("we can find $c$ by $2|V|$ oracle calls", strongly polynomial time) and the oracle model; there is no machine model.
The goal does not assume (24) or (27), and it is not the minimizer-transfer statement alone, which would be near-definitional.

Contributions welcome: proofs of the milestones in the order listed, general lemmas on closure operators of ring families of Finsets, and the lower-ideal representation, which is reusable beyond this mission.

Selected references

A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000), 346–355. https://doi.org/10.1006/jctb.2000.1989
S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001), 761–777. https://doi.org/10.1145/502090.502096
M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981), 169–197. https://doi.org/10.1007/BF02579273

10 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Quantitative Stability in Stochastic Programming: The Method of Probability Metrics 2: Linear Two-Stage Programs Are Lipschitz Stable in the Fortet–Mourier Metric ζ₂Research Paper

Why stability of two-stage programs matters

A linear two-stage stochastic program with fixed recourse chooses a here-and-now decision $x$ before a random vector $\xi$ is observed, and pays a recourse cost afterwards. It is the basic model of stochastic programming, used in capacity planning, energy and supply-chain models. In practice the distribution $\mu$ of $\xi$ is never known exactly: it is estimated from data, replaced by a discrete scenario approximation, or perturbed for robustness. The question is how much the optimal value and the optimal decisions can move when $\mu$ is replaced by a nearby $\nu$ , and in which distance between probability measures "nearby" should be measured.

Rachev and Römisch (Math. Oper. Res. 27(4), 2002, doi:10.1287/moor.27.4.792.304; the mission cites the authors' preprint from edoc.hu-berlin.de) answer this with the method of probability metrics: they derive from the structure of the integrand a canonical distance on measures for each class of models. For linear two-stage programs the canonical distance is the Fortet–Mourier metric of order 2.

Timeline. Robinson and Wets (1987) studied qualitative stability of two-stage programs with respect to weak convergence of measures. Walkup and Wets (1969) had earlier established the piecewise-bilinear structure of the second-stage value function used here. Römisch and Schultz (1991) proved a quantitative stability result for two-stage programs with complete recourse in the Wasserstein metric $W_2$ . The present paper (published 2002) replaces complete recourse by relatively complete recourse plus dual feasibility, and $W_2$ by the metric $\zeta_2$ , which it bounds by a multiple of $W_2$ (p. 13).

Setting

Let $X\subseteq\mathbb R^m$ be a nonempty polyhedron and $\Xi\subseteq\mathbb R^s$ a polyhedron. Fix $c\in\mathbb R^m$ , an $(r,\overline m)$ -matrix $W$ , and data $q(\xi)\in\mathbb R^{\overline m}$ , $h(\xi)\in\mathbb R^r$ and an $(r,m)$ -matrix $T(\xi)$ depending affine linearly on $\xi$ . The second-stage value is

\Phi(u,t)=\inf\{uy:\ Wy=t,\ y\ge0\},

with $\operatorname{pos}W=\{Wy:y\ge0\}$ and $D=\{u:\{z:W'z\le u\}\ne\emptyset\}$ . The integrand is $f_0(\xi,x)=cx+\Phi(q(\xi),h(\xi)-T(\xi)x)$ when $h(\xi)-T(\xi)x\in\operatorname{pos}W$ and $q(\xi)\in D$ , and $+\infty$ otherwise. For a Borel probability measure $\nu$ on $\Xi$ the problem is

\min\Big\{\int_\Xi f_0(\xi,x)\,\nu(d\xi):x\in X\Big\},

with optimal value $v(\nu)$ and solution set $S(\nu)$ . Two assumptions are made: (A1) $h(\xi)-T(\xi)x\in\operatorname{pos}W$ and $q(\xi)\in D$ for all $(\xi,x)\in\Xi\times X$ ; (A2) $\mu$ has a finite second moment.

The Fortet–Mourier metric $\zeta_2$ on $\mathcal P_2(\Xi)$ , the probability measures on $\Xi$ with finite second moment, is

\zeta_2(\mu,\nu)=\sup_{f\in\mathcal F_2(\Xi)}\Big|\int_\Xi f\,d\mu-\int_\Xi f\,d\nu\Big|,\quad \mathcal F_2(\Xi)=\{f:|f(\xi)-f(\tilde\xi)|\le\max\{1,\|\xi\|,\|\tilde\xi\|\}\|\xi-\tilde\xi\|\}.

For an open bounded $\mathcal U\supseteq S(\mu)$ , the growth function is $\psi(\tau)=\inf\{\int_\Xi f_0(\xi,x)\,\mu(d\xi)-v(\mu): d(x,S(\mu))\ge\tau,\ x\in X\cap\operatorname{cl}\mathcal U\}$ , and $\Psi(\eta)=\eta+\psi^{-1}(2\eta)$ with $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$ .

Formalization targets

Goal: Theorem 3.3 (p. 13)

Under (A1), (A2), $S(\mu)\ne\emptyset$ and $\mathcal U$ an open bounded neighbourhood of $S(\mu)$ , there are $L>0$ and $\delta>0$ such that for every $\nu\in\mathcal P_2(\Xi)$ with $\zeta_2(\mu,\nu)<\delta$ :

|v(\mu)-v(\nu)|\le L\,\zeta_2(\mu,\nu),\qquad \emptyset\ne S(\nu)\subseteq S(\mu)+\Psi(L\,\zeta_2(\mu,\nu))\,\mathbb B.

The constants are existential, so the goal does not depend on any particular estimate of them.

Milestones

Lemma 3.1 (p. 11): $\Phi$ is finite and continuous on the polyhedral cone $D\times\operatorname{pos}W$ , piecewise of the form $C_ju\cdot t$ on finitely many polyhedral cones with disjoint interiors, convex in $t$ and concave in $u$ .
Proposition 3.2 (p. 11): $f_0$ is a normal convex integrand, and for $\|x\|\le r$ it satisfies $|f_0(\xi,x)-f_0(\tilde\xi,x)|\le Lr\max\{1,\|\xi\|,\|\tilde\xi\|\}\|\xi-\tilde\xi\|$ , a Lipschitz bound in $x$ with factor $\hat L\max\{1,\|\xi\|^2\}$ , and $|f_0(\xi,x)|\le Kr\max\{1,\|\xi\|^2\}$ .
$\mathcal P_{\mathcal F_{\mathcal U}}\supseteq\mathcal P_2(\Xi)$ (p. 13): every measure with finite second moment satisfies the integrability conditions of the general theory.
Corollary 2.8 (p. 10): the general Lipschitz stability theorem in the metric $\zeta_g$ for convex models whose integrands lie, up to a factor $L$ , in the class $\mathcal F_g$ .

Significance

The theorem says that, under the two natural well-posedness conditions of linear recourse models, optimal values are Lipschitz continuous and solution sets move by at most $\Psi(L\zeta_2)$ , where $\zeta_2$ only sees test functions with the local Lipschitz growth of the integrand. Since $\zeta_2\le(1+\int\|\xi\|^2d\mu+\int\|\xi\|^2d\nu)^{1/2}W_2$ , the result contains the earlier $W_2$ stability theorem.

The results are proved in the paper, except Lemma 3.1, which it cites from Walkup and Wets (1969). None of them is formalized in Mathlib or on Prove2Me. A formalization would provide a checked model of the two-stage recourse function, the Fortet–Mourier metrics, and an end-to-end quantitative stability theorem for stochastic programs, none of which exist in Mathlib.

Difficulty

The obvious argument bounds $|v(\mu)-v(\nu)|$ by $\sup_x|\int f_0(\cdot,x)\,d(\mu-\nu)|$ and then by $L\zeta_2$ . Two steps fail. First, the supremum ranges over all of $X$ , which may be unbounded, while $f_0(\cdot,x)/L$ lies in $\mathcal F_2$ only for $x$ in a bounded set; the argument must localize to $X\cap\operatorname{cl}\mathcal U$ and then show, using convexity, that for $\nu$ close to $\mu$ the localized and global problems coincide. Second, the Lipschitz estimate in $\xi$ for $f_0$ requires the piecewise-bilinear structure of $\Phi$ (Lemma 3.1) and a chaining argument across the polyhedral pieces of $\Xi$ ; the integrand is not differentiable.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The paper never fixes its norm and all its constants are existential, so the Euclidean norm is a faithful instance. Second-stage vectors $u,t,y,z$ are coordinate vectors Fin k → ℝ; index sets are 0-based.
A polyhedron is a finite intersection of closed half-spaces. The standing assumptions are: $X$ a nonempty polyhedron, $\Xi$ a polyhedron, $q,h,T$ affine maps.
A measure in $\mathcal P(\Xi)$ is a Borel probability measure on $\mathbb R^s$ with $\nu(\Xi^c)=0$ ; $\int_\Xi f_0(\xi,x)\,\nu(d\xi)$ is the extended-real integral of the published DupacovaWets.Consistency.expect over $\nu$ restricted to $\Xi$ .
$\Phi$ , $f_0$ , $v$ and $\psi$ are extended-real infima ( $+\infty$ over an empty set); "min" in $\psi$ is read as an infimum. $\zeta_2$ , $\zeta_g$ , $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$ , and the distance to a set is the extended distance ( $+\infty$ to $\emptyset$ ).
To rule out trivializations: every value bound states that $v(\mu)$ , $v(\nu)$ are finite before comparing them, so the extended-real arithmetic $\infty-\infty$ cannot make it vacuous; in $\zeta_2$ a test function that is not integrable for both measures contributes $+\infty$ , never a junk $0$ .
Disclosed readings: Proposition 3.2 leaves its radius $r$ unquantified; it is stated with the constants first and then every $r\ge1$ . Lemma 3.1's " $\operatorname{pos}W\times D$ " is read as $D\times\operatorname{pos}W$ , in the order of $\Phi$ 's arguments. Corollary 2.8 adds $\mu,\nu\in\mathcal P_{\mathcal F_{\mathcal U}}(\Xi)$ , an assumption of Theorem 2.2 that its proof invokes; Theorem 3.3 needs no such addition, because milestone 3 supplies it.
Needed infrastructure: LP duality and the Walkup–Wets decomposition of $\Phi$ ; normal integrands and measurability of their infima; integrability under moment conditions; the general stability theorems (Theorems 2.2–2.3 of the paper) for $d=0$ . The definitions of $\zeta_p$ , $\mathcal F_g$ and normal integrands are reusable well beyond this mission. Contributions toward any milestone, and proofs of the auxiliary facts (for example, that every $f\in\mathcal F_2(\Xi)$ is integrable for $\nu\in\mathcal P_2(\Xi)$ ), are welcome.

Selected references

S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: The method of probability metrics, Mathematics of Operations Research 27(4) (2002) 792–818. https://doi.org/10.1287/moor.27.4.792.304 (cited here from the authors' preprint, edoc.hu-berlin.de)
D. W. Walkup, R. J-B Wets, Lifting projections of convex polyhedra, Pacific Journal of Mathematics 28 (1969) 465–475 (the paper's [55]).
S. M. Robinson, R. J-B Wets, Stability in two-stage stochastic programming, SIAM Journal on Control and Optimization 25 (1987) 1409–1416 (the paper's [37]).
W. Römisch, R. Schultz, Stability analysis for stochastic programs, Annals of Operations Research 30 (1991) 241–266 (the paper's [40]).
R. T. Rockafellar, R. J-B Wets, Variational Analysis, Springer (the paper's [38]; normal integrands, Chapter 14).
S. T. Rachev, Probability Metrics and the Stability of Stochastic Models, Wiley, Chichester 1991 (the paper's [32]).

8 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

Bounded-parameter Markov Decision Processes 1: The Optimistic and Pessimistic Optimal Interval Value Functions Satisfy Bellman-like EquationsResearch Paper

Motivation

A Markov decision process is specified by numbers: transition probabilities and rewards. In practice these numbers are estimated from data, elicited from experts, or produced by aggregating the states of a larger model, and in each case what is actually known is a range for each parameter rather than its value. Givan, Leach and Dean (Artificial Intelligence, 2000) introduced bounded-parameter MDPs (BMDPs) to reason about a whole family of MDPs at once: every transition probability is only known to lie in a closed interval. Their motivation was state-space aggregation, where grouping states with similar but not identical dynamics yields exactly such interval bounds, and the same object later reappeared as the interval or "box" uncertainty set of robust MDPs (Nilim and El Ghaoui, 2005; Iyengar, 2005) and of optimistic exploration in reinforcement learning (Strehl and Littman, 2008).

Over such a family, the value of a policy is no longer a number but an interval, and "optimal" needs a definition. This mission formalizes the paper's answer: two total orders on intervals, the corresponding optimal policies, and the Bellman-like equations their interval value functions satisfy.

Setting

An exact MDP $M=\langle Q,A,F,R\rangle$ has a finite set $Q$ of states, a finite nonempty set $A$ of actions, transition probabilities $F_{pq}(\alpha)\ge 0$ with $\sum_{q}F_{pq}(\alpha)=1$ , a reward $R(q)\in\mathbb R$ for each state and a discount rate $0\le\gamma<1$ . A policy is a map $\pi:Q\to A$ ; $\Pi$ is the set of all policies. The value function $V_{M,\pi}(p)$ is the expected discounted sum of rewards $\sum_{t\ge 0}\gamma^t\,\mathbb E[R(X_t)\mid X_0=p]$ along the Markov chain with transitions $F_{pq}(\pi(p))$ . The operators

VI_{M,\pi}(v)(p)=R(p)+\gamma\sum_{q}F_{pq}(\pi(p))\,v(q),\qquad VI_{M,\alpha}(v)(p)=R(p)+\gamma\sum_{q}F_{pq}(\alpha)\,v(q)

act on value functions $v:Q\to\mathbb R$ . $V_1\le_{\mathrm{dom}}V_2$ is the statewise order.

A BMDP $M_\updownarrow$ gives for each $p,q,\alpha$ an interval $[F_\downarrow{}_{pq}(\alpha),F_\uparrow{}_{pq}(\alpha)]\subseteq[0,1]$ with $\sum_q F_\downarrow{}_{pq}(\alpha)\le 1\le\sum_q F_\uparrow{}_{pq}(\alpha)$ , a reward $R$ and a discount rate $\gamma$ . Its members $M\in M_\updownarrow$ are the exact MDPs with that $R$ and $\gamma$ and with $F^M_{pq}(\alpha)\in[F_\downarrow{}_{pq}(\alpha),F_\uparrow{}_{pq}(\alpha)]$ . The interval value of a policy is

V_\updownarrow{}_\pi(q)=\Big[\min_{M\in M_\updownarrow}V_{M,\pi}(q),\ \max_{M\in M_\updownarrow}V_{M,\pi}(q)\Big]=[V_\downarrow{}_\pi(q),V_\uparrow{}_\pi(q)].

Intervals are compared by the optimistic order, which compares upper bounds first and breaks ties by lower bounds, and the pessimistic order, which compares lower bounds first:

[l_1,u_1]\le_{\mathrm{opt}}[l_2,u_2]\iff u_1<u_2\ \vee\ (u_1=u_2\wedge l_1\le l_2),\qquad [l_1,u_1]\le_{\mathrm{pes}}[l_2,u_2]\iff l_1<l_2\ \vee\ (l_1=l_2\wedge u_1\le u_2).

A policy $\pi_{\mathrm{opt}}$ is optimistically optimal if $V_\updownarrow{}_{\pi_{\mathrm{opt}}}(q)\ge_{\mathrm{opt}}V_\updownarrow{}_\pi(q)$ for all $\pi$ and $q$ ; pessimistically optimal is defined with $\ge_{\mathrm{pes}}$ . The optimal interval value functions are $V_\updownarrow{}_{\mathrm{opt}}=V_\updownarrow{}_{\pi_{\mathrm{opt}}}$ and $V_\updownarrow{}_{\mathrm{pes}}=V_\updownarrow{}_{\pi_{\mathrm{pes}}}$ .

Formalization targets

Goal: Theorem 9, equations (25) and (26)

At every state $p$ ,

V_\updownarrow{}_{\mathrm{opt}}(p)=\max_{\alpha\in A,\ \le_{\mathrm{opt}}}\Big[\min_{M\in M_\updownarrow}VI_{M,\alpha}(V_\downarrow{}_{\mathrm{opt}})(p),\ \max_{M\in M_\updownarrow}VI_{M,\alpha}(V_\uparrow{}_{\mathrm{opt}})(p)\Big],

and the same with $\mathrm{pes}$ in place of $\mathrm{opt}$ . The maximum over actions is for the total order on intervals: attained by some action and an upper bound for every action.

Milestones

In the order the proof uses them: Theorem 3 (second sentence: $V_{M,\pi}$ is the unique fixed point of $VI_{M,\pi}$ ); Theorem 6 (comparison: $u\le_{\mathrm{dom}}VI_{M,\pi}(u)$ implies $u\le_{\mathrm{dom}}V_{M,\pi}$ , and its three variants); Lemma 1 (every member's values and backups are bracketed by finitely many order-maximizing MDPs); Lemma 2 (statewise composition of member MDPs dominates, or is dominated by, both components); Theorem 7 ( $\pi$ -maximizing and $\pi$ -minimizing MDPs exist among the order-maximizing ones); Corollary 1 ( $V_\downarrow{}_\pi$ and $V_\uparrow{}_\pi$ are a minimum and a maximum for $\le_{\mathrm{dom}}$ ); Lemma 3 (statewise composition of policies improves the upper, resp. lower, bounds); Theorem 8 (optimistically and pessimistically optimal policies exist).

Significance

Theorem 9 is the interval analogue of the Bellman optimality equation. It is what makes the optimal interval value functions computable: the paper's interval value iteration algorithms $IVI_\updownarrow{}_{\mathrm{opt}}$ and $IVI_\updownarrow{}_{\mathrm{pes}}$ (Section 5) iterate exactly the right-hand sides of (25) and (26). The lower half of (26) is the max-min equation of robust dynamic programming with rectangular box uncertainty, and the upper half of (25) is the max-max equation behind optimistic planning; Theorem 9 states both, together with the tie-breaking second component, in one model. Theorems 7 and 8 are of independent use: a single member MDP is worst (or best) for a policy at all states at once, and the partial orders on interval value functions nevertheless have maxima over policies.

None of these results has a machine-checked proof. The platform has robust Bellman equations in other models (costs, general rectangular sets, a sup over nature) but nothing on BMDPs, interval value functions, or the orders $\le_{\mathrm{opt}}$ and $\le_{\mathrm{pes}}$ . The mission produces the paper's optimality theory end to end, from the comparison principle for exact MDPs to the two Bellman-like equations, on a model shared with the companion mission on interval policy evaluation.

Difficulty

The orders $\le_{\mathrm{opt}}$ and $\le_{\mathrm{pes}}$ are total on intervals but only partial on interval value functions, and they are lexicographic. The obvious construction of an optimal policy, switching statewise to whichever of two policies has the better interval, fails: the composed policy need not dominate either component in $\le_{\mathrm{opt}}$ , because lower bounds can get worse at states where the upper bounds do not change (the paper says so explicitly, eq. (20)). Existence therefore needs a two-stage argument. A second obstacle is that $V_\downarrow{}_\pi$ and $V_\uparrow{}_\pi$ are defined statewise, as minima over an uncountable family; that one member attains them at every state simultaneously is a theorem (Theorem 7), and the Bellman-like equations rest on it. Finally, the inner minima in (25) act on $V_\downarrow{}_{\mathrm{opt}}$ , the lower bound of an optimistically chosen policy, which is not the componentwise best lower bound over policies; the equation couples the two components through the tie-break.

Formalization scope

$Q$ and $A$ are finite types, $A$ is nonempty; $Q$ may be empty. An exact MDP is a structure with transition function F p α q $=F_{pq}(\alpha)$ , stochastic rows, reward $R:Q\to\mathbb R$ and discount $0\le\gamma<1$ . $V_{M,\pi}$ is defined as the convergent series $\sum_t\gamma^tP_\pi^tR$ , not as a solution of (2). Rewards of the BMDP are tight, as the paper assumes from footnote 3 on; reward intervals are not formalized. Members of $M_\updownarrow$ form a subtype of exact MDPs with the BMDP's $R$ and $\gamma$ . The minima and maxima of Definition 3 and of (25)–(26) are the real infimum and supremum over that subtype, which is nonempty and on which values are bounded, so no junk value enters. Intervals are pairs (lower, upper); the orders (17) are spelled out. Policies are deterministic stationary maps $Q\to A$ , the paper's $\Pi$ . An ordering of $Q$ is a bijection Fin |Q| ≃ Q, and the index $r$ of Definition 1 is the largest index at which expression (9) does not exceed 1 (the page's phrase admits ties; only the largest index keeps the remaining mass inside its interval). Definition 8 is read as $V_\updownarrow{}_{\mathrm{opt}}=V_\updownarrow{}_{\pi_{\mathrm{opt}}}$ for an optimistically optimal $\pi_{\mathrm{opt}}$ , so the goal is quantified over all optimistically (pessimistically) optimal policies; Theorem 8 is the milestone that makes this quantification non-vacuous. Lemma 3 is stated as in the Appendix (p. 36): part (d) concerns $\pi_4=\pi_1\oplus_{\mathrm{pes}}\pi_2$ , where p. 17 misprints $\pi_3$ .

A formalization in which members carry their own discount, rows need not sum to one, the minima range over all functions $Q\to A\to Q\to\mathbb R$ , or $V_\updownarrow{}_{\mathrm{opt}}$ is the componentwise supremum over policies would make several statements false or trivial; each is ruled out above.

Contributions welcome beyond proofs of the milestones: a reusable theory of discounted policy evaluation for finite MDPs (the series representation, the fixed-point characterization, monotonicity of $VI_{M,\pi}$ ), which other missions on finite MDPs can import.

Selected references

R. Givan, S. Leach, T. Dean, Bounded-parameter Markov decision processes, Artificial Intelligence 122 (2000). https://doi.org/10.1016/S0004-3702(00)00047-3
A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
G. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129
A. Strehl, M. Littman, An analysis of model-based interval estimation for Markov decision processes, Journal of Computer and System Sciences 74(8), 2008. https://doi.org/10.1016/j.jcss.2007.08.009
M. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

12 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

The Sample Average Approximation Method for Stochastic Discrete Optimization 1: Under Assumption A, 1 − P(Ŝ^ε_N ⊂ S^ε) Decays Exponentially Fast in the Sample Size NResearch Paper

Motivation

Many decision problems in operations research ask for the best element of a finite set of alternatives when each alternative's cost is random: which projects to fund when resource use is uncertain, which crew pairings to fly when delays are random, which items to pack into a knapsack whose overflow is penalized. The expected cost is rarely available in closed form, because it is a high-dimensional integral over the distribution of the random data. The sample average approximation (SAA) method replaces the expectation by an average over a random sample and solves the resulting deterministic problem with a standard discrete optimization routine. The method is widely used in stochastic programming (see Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming, SIAM 2009, Ch. 5, https://doi.org/10.1137/1.9780898718751).

Kleywegt and Shapiro (preprint; published with Homem-de-Mello as SIAM J. Optim. 12(2):479–502, 2002, https://doi.org/10.1137/S1052623499363220) ask why the method works so well for discrete problems. Their answer is a large-deviations statement: when the feasible set is finite, the probability that the SAA problem returns a wrong answer decays exponentially in the sample size. This mission formalizes that result, Proposition 2.2 of the two-author preprint, together with its consistency companion, Proposition 2.1.

Setting

Let $\mathcal S$ be a nonempty finite set, $W$ a random element of a measurable space $\mathcal W$ , and $G : \mathcal S \times \mathcal W \to \mathbb R$ such that $G(x,\cdot)$ is measurable and $\mathbb E|G(x,W)| < \infty$ for every $x \in \mathcal S$ . The true problem (1.1) is

v^* = \min_{x \in \mathcal S} g(x), \qquad g(x) = \mathbb E\, G(x, W).

Let $W^1, W^2, \dots$ be an independent, identically distributed sample with the law of $W$ . The sample average function and the SAA problem (2.1) are

\hat g_N(x) = \frac1N \sum_{n=1}^N G(x, W^n), \qquad \hat v_N = \min_{x \in \mathcal S} \hat g_N(x).

For $\varepsilon \ge 0$ , the $\varepsilon$ -optimal sets are $\mathcal S^\varepsilon = \{x \in \mathcal S : g(x) \le v^* + \varepsilon\}$ and $\hat{\mathcal S}^\varepsilon_N = \{x \in \mathcal S : \hat g_N(x) \le \hat v_N + \varepsilon\}$ ; at $\varepsilon = 0$ they are the optimal sets $\mathcal S^*$ and $\hat{\mathcal S}_N$ . Two numbers drive the analysis: the maximal deviation $\delta_N = \max_{x \in \mathcal S}|\hat g_N(x) - g(x)|$ of (2.2), and the well-conditioning number

\alpha(\varepsilon) = \min_{x \in \mathcal S \setminus \mathcal S^\varepsilon} g(x) - v^* - \varepsilon

of (2.3), the gap between the $\varepsilon$ -optimal solutions and the rest.

For a real random variable $X$ with moment generating function $M(t) = \mathbb E\, e^{tX}$ and logarithmic moment generating function $\Lambda(t) = \log M(t) \in (-\infty, +\infty]$ , the rate function is $I(z) = \sup_{t \ge 0}\{tz - \Lambda(t)\}$ . Assumption A requires that for every $x \in \mathcal S$ the moment generating function of $G(x, W)$ be finite in a neighbourhood of $t = 0$ .

Formalization targets

Goal: Proposition 2.2

Under Assumption A, for every $\varepsilon \ge 0$ there is $\gamma > 0$ with

\limsup_{N \to \infty} \frac1N \log\Big[1 - P\big(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon\big)\Big] \le -\gamma. \tag{2.5}

The constant $\gamma$ is not specified: it depends on $\alpha(\varepsilon)$ through rate functions and cannot be computed before the problem is solved. The goal asserts only its existence, which is the paper's claim.

Milestones

$\alpha(\varepsilon) > 0$ whenever $\mathcal S \setminus \mathcal S^\varepsilon \ne \emptyset$ (2.3).
$\delta_N < \alpha(\varepsilon)/2$ implies $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ .
The union bound $1 - P(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon) \le \sum_{x \in \mathcal S} P\{|\hat g_N(x) - g(x)| \ge \alpha(\varepsilon)/2\}$ .
The large-deviations upper bound (2.4): $\frac1N \log P(Z_N \ge a) \le -I(a)$ for i.i.d. averages $Z_N$ .
$I(a) > 0$ for $a$ above the mean, when $M$ is finite near $0$ .
Under Assumption A, $P\{|\hat g_N(x) - g(x)| \ge r\} \le e^{-N\gamma_x} + e^{-N\gamma'_x}$ with $\gamma_x, \gamma'_x > 0$ .

Companions

Proposition 2.1 ( $\hat v_N \to v^*$ w.p.1, and $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ w.p.1 for $N$ large enough), the almost-sure convergence $\delta_N \to 0$ of (2.2), the singleton consequence ( $\mathcal S^\varepsilon = \{x^*\}$ implies $\hat{\mathcal S}^\varepsilon_N = \{x^*\}$ eventually), the facts $I(\mu) = 0 = \min I$ , the Example of §3.2 showing that a sample size $N > k/2$ can be required, and the computation $\alpha(0) = \min_i c_i$ on the hypercube with best value $1/k^{1/p}$ (§4).

Significance

Proposition 2.2 explains the practical behaviour of the SAA method on discrete problems: an exact optimal solution of the true problem is obtained with probability approaching one exponentially fast, so a moderate sample often suffices even when the number of feasible solutions is astronomically large. It is the basis of the paper's replication argument (§3.2: the probability of success $p(N)$ of one SAA replication tends to one exponentially fast) and identifies $\alpha(\varepsilon)$ as the quantity that governs the difficulty of a stochastic discrete problem, which the numerical study of §4 then examines. Later sample-size estimates for SAA (Shapiro, Dentcheva and Ruszczyński 2009, §5.3) refine the same argument into explicit, non-asymptotic bounds.

The result is proved in the paper. The mission produces a machine-checked proof of it and of its ingredients, including a Lean statement of the Cramér–Chernoff upper bound with the rate function $I$ in the extended reals and the positivity of $I$ above the mean under a local moment condition. To our knowledge none of these is formalized on the platform or in Mathlib in this form.

Difficulty

The argument is short on paper; the formal difficulty is in the large-deviations step. Mathlib has the Chernoff inequality $P(X \ge a) \le e^{-ta}\,\mathbb E e^{tX}$ and the factorization of moment generating functions of independent sums, but the step from there to $\frac1N \log P(Z_N \ge a) \le -I(a)$ requires passing to a supremum over $t$ in the extended reals, handling $t$ where $M(t) = \infty$ , and the case $P(Z_N \ge a) = 0$ . The positivity $I(a) > 0$ requires $\Lambda'(0) = \mu$ , i.e. differentiating the moment generating function at an interior point of its domain. A naive attempt that works with real logarithms fails at probability zero, where $\log 0$ is not $-\infty$ , and an attempt that bounds $\delta_N$ by Chebyshev's inequality gives only a polynomial rate.

Formalization scope

The feasible set is a Finset of an arbitrary type X, assumed nonempty; minima and maxima over it are Finset.inf' and Finset.sup', so they are attained. The sample is a sequence W : ℕ → Ω → 𝒲 of measurable maps on a probability space, mutually independent (iIndepFun) and identically distributed with W 0; the paper's $W^n$ is W (n - 1), and $g(x)$ is the expectation of $G(x, W^1)$ . Measurability of $G(x,\cdot)$ is Borel measurability. Logarithms of probabilities are ENNReal.log, with $\log 0 = -\infty$ , and the limit superior in (2.5) is taken in the extended reals; this is the paper's convention and it makes the goal correct when $\mathcal S^\varepsilon = \mathcal S$ , where the event is sure. Assumption A is stated as integrability of $e^{tG(x,W)}$ for $t$ near $0$ , not through the value of Mathlib's mgf, which is $0$ where the expectation is infinite. The logarithmic moment generating function is the published definition BellWilliams2001.ThresholdPolicy.logMGF (extended-real valued, $+\infty$ off the domain of $M$ ), and $I$ is the supremum over $t \ge 0$ only, as on p. 3. Wherever $\alpha(\varepsilon)$ appears, the nonemptiness of $\mathcal S \setminus \mathcal S^\varepsilon$ is a hypothesis; the goal does not mention $\alpha$ and needs none.

A trivializing formalization is ruled out: with Real.log the event " $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ is sure" would give $\log 0 = 0$ and make the goal false, and a rate function built from mgf would count infinite moment generating functions as $\Lambda = \log 0 = 0$ ; neither encoding is used.

A complete development needs the Cramér–Chernoff bound for i.i.d. sums with an extended-real rate function, differentiability of the moment generating function at interior points, and the strong law of large numbers applied to finitely many functions. The large-deviations items (milestones 4 and 5, and $I(\mu) = 0$ ) are stated for an arbitrary i.i.d. real sequence and are reusable beyond this mission. Proofs of any item, including the optional examples, are welcome.

Selected references

A. J. Kleywegt and A. Shapiro, The sample average approximation method for stochastic discrete optimization, preprint (two-author version), https://edoc.hu-berlin.de/server/api/core/bitstreams/2dcf2d5b-5fb9-44d1-b36a-5e378c803717/content. Published with T. Homem-de-Mello in SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220
A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

9 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Is Network Traffic Approximated by Stable Lévy Motion or Fractional Brownian Motion? 4: Superposed ON/OFF Input Under Fast Growth Converges in C[0,∞) to Fractional Brownian MotionResearch Paper

Why heavy-tailed input matters

Measurements of Ethernet and Internet traffic in the 1990s showed that cumulative traffic is self-similar and long-range dependent: correlations of the input rate decay so slowly that they are not summable, and fluctuations at large time scales do not average out the way Poisson-type models predict (Leland et al. 1994). A widely accepted explanation is that the lengths of individual transmissions (file sizes, session durations) are heavy tailed, with infinite variance. Queueing and capacity-planning calculations then depend on which stochastic process approximates the cumulative input over long horizons.

Two approximations had been proposed: fractional Brownian motion, a Gaussian self-similar process with dependent increments, and α-stable Lévy motion, a heavy-tailed process with independent increments. Mikosch, Resnick, Rootzén and Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both arise from the same models and that the answer depends on how fast the number of sources grows relative to the time scale. This mission formalizes their Gaussian answer for the superposition of ON/OFF sources: Theorem 4.

1995–1997: Willinger, Taqqu, Sherman and Wilson derive fractional Brownian motion from superposed ON/OFF sources with heavy-tailed periods, as an iterated limit: first the number of sources $M\to\infty$ , then the time scale $T\to\infty$ , and for finite-dimensional distributions only.
1998: Heath, Resnick and Samorodnitsky (Math. Oper. Res. 23) give the exact decay of the covariance of a single stationary ON/OFF source.
2002: Mikosch, Resnick, Rootzén and Stegeman let $M$ and $T$ grow together and show that fast growth gives fractional Brownian motion as a functional limit in $\mathbb C[0,\infty)$ , while slow growth gives stable Lévy motion.

The superposed ON/OFF model

A single ON/OFF source alternates between ON-periods, during which it sends work at rate $1$ , and silent OFF-periods. The ON-periods $X_1,X_2,\dots$ are iid with law $F_{\mathrm{on}}$ and the OFF-periods $Y_{\mathrm{off}},Y_1,Y_2,\dots$ iid with law $F_{\mathrm{off}}$ , both on $[0,\infty)$ , all independent, with means $\mu_{\mathrm{on}}$ , $\mu_{\mathrm{off}}$ and $\mu=\mu_{\mathrm{on}}+\mu_{\mathrm{off}}$ . The tails are regularly varying: for $x>0$ ,

\bar F_{\mathrm{on}}(x)=x^{-\alpha}L_{\mathrm{on}}(x),\qquad \bar F_{\mathrm{off}}(x)=x^{-\alpha_{\mathrm{off}}}L_{\mathrm{off}}(x),\qquad 1<\alpha<\alpha_{\mathrm{off}}<2,

with $L_{\mathrm{on}},L_{\mathrm{off}}$ slowly varying ( $L(cx)/L(x)\to1$ for every $c>0$ ). So both periods have finite mean and infinite variance, and the ON-periods have the heavier tail.

To make the source stationary, a delay $T_0=B(X^{(0)}_{\mathrm{on}}+Y_{\mathrm{off}})+(1-B)Y^{(0)}_{\mathrm{off}}$ is used, where $B$ is Bernoulli with $P(B=1)=\mu_{\mathrm{on}}/\mu$ and $X^{(0)}_{\mathrm{on}},Y^{(0)}_{\mathrm{off}}$ have the integrated-tail laws $F^{(0)}(x)=\mu_F^{-1}\int_0^x\bar F(s)\,ds$ . With $T_n=T_0+\sum_{i=1}^n(X_i+Y_i)$ the source's activity is

W_t=B\,\mathbf 1_{[0,X^{(0)}_{\mathrm{on}})}(t)+\sum_{n\ge0}\mathbf 1_{[T_n,T_n+X_{n+1})}(t),\qquad t\ge0,

a stationary process with $EW_t=\mu_{\mathrm{on}}/\mu$ .

The $T$ -th model superposes $M=M(T)$ independent copies $W^{(1)},\dots,W^{(M)}$ , where $M$ is integer valued, non-decreasing and $M(T)\to\infty$ . The cumulative input is $A(t)=\int_0^t\sum_{m=1}^MW^{(m)}_s\,ds$ . With the quantile $b(t)=(1/\bar F_{\mathrm{on}})^{\leftarrow}(t)$ , the fast growth condition is

\text{Condition 2:}\qquad \lim_{T\to\infty}\frac{b(MT)}{T}=\infty,

equivalently $MT\bar F_{\mathrm{on}}(T)\to\infty$ . The normalisation and limit constants are

d_T=[T^{3-\alpha}L_{\mathrm{on}}(T)M]^{1/2},\qquad \sigma_0^2=\frac{2\mu_{\mathrm{off}}^2\Gamma(2-\alpha)/(\alpha-1)}{\mu^3\Gamma(4-\alpha)},\qquad H=\frac{3-\alpha}{2}\in(\tfrac12,1).

A standard fractional Brownian motion $B_H$ is a mean-zero Gaussian process on $[0,\infty)$ with continuous paths and $\mathrm{Cov}(B_H(t),B_H(s))=\tfrac12(t^{2H}+s^{2H}-|t-s|^{2H})$ .

Formalization targets

Goal: Theorem 4

If Condition 2 holds, then

\frac{A(T\cdot)-TM\mu^{-1}\mu_{\mathrm{on}}(\cdot)}{d_T}\ \xrightarrow{d}\ \sigma_0B_H(\cdot)\qquad\text{weakly in }\mathbb C[0,\infty).

Intermediate targets

In the order of the paper's argument: the mean $EW_t=\mu_{\mathrm{on}}/\mu$ (p. 27); the covariance decay (2.5) $\gamma_W(h)\sim\frac{\mu_{\mathrm{off}}^2}{(\alpha-1)\mu^3}h^{-(\alpha-1)}L_{\mathrm{on}}(h)$ ; Condition 2 $\Leftrightarrow T=o(d_T)$ (p. 61); the variance asymptotic (7.1) $\mathrm{Var}(G_T)\sim\sigma_0^2T^{3-\alpha}L_{\mathrm{on}}(T)$ for $G_T=\int_0^T(W_u-EW_u)\,du$ ; Lemma 13, the one-dimensional limit $d_T^{-1}\sum_mG^{(m)}_{Tt}\to N(0,\sigma_0^2t^{3-\alpha})$ ; the covariance limit (7.4); and the second-moment bound $E|d_T^{-1}\sum_mG^{(m)}_{Tu}|^2\le c\,u^{1+\varepsilon}$ behind tightness (p. 63). (2.5) and (7.1) are cited by the paper from Heath–Resnick–Samorodnitsky and Willinger–Taqqu–Sherman–Wilson; they are stated here as the paper states them.

Significance

Theorem 4 justifies fractional Brownian motion as the model of aggregate traffic from many heavy-tailed sources in a single, simultaneous limit, replacing the iterated limit of earlier work, and it upgrades finite-dimensional convergence to weak convergence of paths. Functionals of the path, such as the supremum of $A(Tt)-ct$ that governs the buffer content of a fluid queue, therefore inherit Gaussian approximations. Together with Theorem 2 it shows that a single growth condition on $M$ decides between Gaussian and stable approximations.

The result is proved in the paper; it is not formalized anywhere. A formalization adds a machine-checked statement of the theorem and reusable developments of regularly varying functions, the stationary alternating renewal process, fractional Brownian motion, and convergence in $\mathbb C[0,\infty)$ .

Difficulty

The obvious route is a central limit theorem for $\sum_{m}G^{(m)}_{Tt}$ , a sum of $M$ iid bounded terms; but the number of terms and their distribution change with $T$ , so one needs a triangular-array limit theorem whose variance condition rests on the exact asymptotic (7.1). That asymptotic in turn needs the covariance decay (2.5) of a single stationary source, which requires renewal theory for the alternating process with infinite-variance periods. Convergence of finite-dimensional distributions alone does not give the theorem: tightness in $\mathbb C[0,K]$ needs a moment bound on increments that is uniform in $T$ for small time lags, which requires Potter-type bounds for the regularly varying function $x\mapsto EG_x^2$ .

Formalization scope

Time and models. $T\to\infty$ along atTop on $\mathbb R$ . Each model $T$ has its own probability space carrying $M(T)$ independent sources; the theorems hold for every such family. Lean's X n, Y n are the paper's $X_{n+1}$ , $Y_{n+1}$ and Lean's sources $0,\dots,M-1$ are the paper's $1,\dots,M$ . Time in the normalised process runs over $\mathbb R_{\ge0}$ .
Standing hypotheses. $F_{\mathrm{on}},F_{\mathrm{off}}$ are probability measures on $[0,\infty)$ (non-negativity is implicit in "lengths"); (2.1) is stated as " $x\mapsto x^{\alpha}\bar F(x)$ is slowly varying"; $1<\alpha<\alpha_{\mathrm{off}}<2$ ; $M$ non-decreasing with $M\to\infty$ (§3.2); Condition 2 where §7 assumes it. No other hypothesis is added.
Junk values ruled out. $b$ is an infimum over $\{x>0:t\bar F_{\mathrm{on}}(x)\le1\}$ , never a division by zero; the series defining $W_t$ has non-negative terms and fails to converge only on a null event; equalities of laws come with measurability. The limit is pinned completely: Gaussian, mean zero, the covariance above with $\sigma_H=1$ and $H=(3-\alpha)/2$ , continuous paths, multiplied by $\sigma_0$ . Fidi convergence in place of the functional limit, a free scale in the limit, or a limit identified only by its marginals would each be a different, weaker theorem.
Weak convergence is stated in coupling form: for every sequence $T_n\to\infty$ there are one probability space, copies $Y_n$ with continuous paths of the laws of the normalised processes at $T_n$ , and a standard fractional Brownian motion $Y'$ such that $Y_n\to\sigma_0Y'$ uniformly on every $[0,K]$ almost surely. On the Polish space $\mathbb C[0,\infty)$ this is equivalent to weak convergence.
Infrastructure needed: Karamata's theorem and Potter bounds; the stationary alternating renewal process and its covariance asymptotics; a triangular-array central limit theorem; existence of fractional Brownian motion; a moment criterion for tightness in $\mathbb C[0,K]$ . The regular-variation and path-space material is reusable well beyond this mission; contributions of any of these pieces, and of any milestone, are welcome.

Selected references

T. Mikosch, S. Resnick, H. Rootzén and A. Stegeman, Is network traffic approximated by stable Lévy motion or fractional Brownian motion?, Ann. Appl. Probab. 12(1) (2002), 23–68. https://doi.org/10.1214/aoap/1015961155
D. Heath, S. Resnick and G. Samorodnitsky, Heavy tails and long range dependence in on/off processes and associated fluid models, Math. Oper. Res. 23 (1998), 145–165. https://doi.org/10.1287/moor.23.1.145
W. Willinger, M. S. Taqqu, R. Sherman and D. V. Wilson, Self-similarity through high-variability: statistical analysis of Ethernet LAN traffic at the source level, IEEE/ACM Trans. Networking 5 (1997), 71–86. https://doi.org/10.1109/90.554723
W. E. Leland, M. S. Taqqu, W. Willinger and D. V. Wilson, On the self-similar nature of Ethernet traffic (extended version), IEEE/ACM Trans. Networking 2 (1994), 1–15. https://doi.org/10.1109/90.282603
N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511721434
P. Billingsley, Convergence of Probability Measures, Wiley, 1968 (Theorem 12.3, moment criterion for tightness).

9 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Designing a Call Center with Impatient Customers II: In the Halfin–Whitt Regime the Scaled Erlang-A Queue Converges to a Diffusion with Piecewise-Linear DriftResearch Paper

Motivation

Telephone call centers are large service systems: hundreds of agents answer callers who wait in a queue and hang up when their patience runs out. Staffing them is a trade-off between the cost of agents and the quality of service, and in large centers both the efficiency (agents busy almost all the time) and the service level (most callers answered almost immediately) can be high at once. Garnett, Mandelbaum and Reiman (M&SOM 4(3), 2002) study the simplest model that captures customer abandonment, the Erlang-A or $M/M/N+M$ queue, and derive approximations for it in the regime where the number of agents is large.

Their Theorem 2 is the process-level justification of these approximations: the queue-length process, centred at the number of agents and scaled by its square root, converges to a one-dimensional diffusion. The steady-state performance formulas of the paper (delay probability, abandonment probability, waiting times) are computed from this diffusion and its stationary law.

Timeline.

Halfin and Whitt (1981) proved the corresponding limit for the $M/M/N$ queue without abandonment, in the regime $\sqrt N(1-\rho_N) \to \beta$ with $\beta > 0$ (Oper. Res. 29(3)). The limit is a diffusion with drift $-\mu(\beta + x)$ below $0$ and constant drift $-\mu\beta$ above.
Fleming, Stolyar and Simon (1994) conjectured the limit with abandonment, with a slightly different centering, and proved the weak limit of the stationary distributions.
Garnett, Mandelbaum and Reiman (2002) state the process limit for $0 < \theta < \infty$ as Theorem 2, with the extensions $\theta = 0$ and $\theta = \infty$ as Theorem 2* in Appendix C.

Setting

Fix a service rate $\mu > 0$ . For each $N \ge 1$ the $N$ -th system has $N$ statistically identical agents, Poisson arrivals of rate $\lambda_N > 0$ , exponential service times of rate $\mu$ , an unlimited waiting room served first come, first served, and exponential patience of rate $\theta_N > 0$ for every caller. A caller whose wait in queue reaches their patience abandons and does not return. The number of callers in the system, $Q_N(t)$ , is a birth–death process on $\{0, 1, 2, \dots\}$ with birth rate $\lambda_N$ and death rate $\min(k, N)\mu + (k-N)^+\theta_N$ in state $k$ . Its initial value $Q_N(0)$ is an arbitrary random variable.

The traffic intensity is $\rho_N = \lambda_N/(N\mu)$ . The centred and scaled process is

q_N(t) = \frac{Q_N(t) - N}{\sqrt N}, \qquad t \ge 0 .

When $q_N \ge 0$ it counts waiting callers and when $q_N \le 0$ it counts idle agents, both in units of $\sqrt N$ .

For $\beta \in \mathbb R$ and $\theta > 0$ , the drift is the piecewise-linear function

f(x) = \begin{cases} -\mu(\beta + x), & x \le 0,\\ -(\mu\beta + \theta x), & x > 0,\end{cases}

and the limit diffusion $q$ solves $dq(t) = f(q(t))\,dt + \sqrt{2\mu}\,db(t)$ , where $b$ is a standard Brownian motion independent of $q(0)$ . The noise is additive, so this means: $q$ has continuous paths and $q(t) = q(0) + \int_0^t f(q(s))\,ds + \sqrt{2\mu}\,b(t)$ for all $t \ge 0$ . Below $0$ it behaves like an Ornstein–Uhlenbeck process with restraining force $\mu$ , above $0$ like one with restraining force $\theta$ .

Formalization targets

Goal: Theorem 2 (p. 216)

Assume

\lim_{N\to\infty}\sqrt N(1-\rho_N) = \beta \in (-\infty,\infty), \qquad \lim_{N\to\infty}\theta_N = \theta \in (0,\infty),

and $q_N(0) \Rightarrow \nu$ for a probability law $\nu$ on $\mathbb R$ . Then

q_N \Rightarrow q \quad\text{in } D[0,\infty),

where $q$ is the solution of $dq = f(q)\,dt + \sqrt{2\mu}\,db$ with $q(0) \sim \nu$ , and this solution is unique in law.

Milestone: the limit equation is well posed (Theorem 2, p. 216)

On every probability space with a standard Brownian motion $b$ and an independent initial value $X_0$ , the equation has a solution adapted to $\sigma(X_0, b(s): s \le t)$ , and any two solutions with the same $b$ and initial value are indistinguishable.

Milestone: infinitesimal moments (Appendix C, p. 224)

The infinitesimal expectation $\mu_N(x)$ and variance $\sigma_N^2(x)$ of $q_N$ at the point $x$ , as displayed on p. 224, satisfy

\lim_{N\to\infty}\mu_N(x) = f(x), \qquad \lim_{N\to\infty}\sigma_N^2(x) = 2\mu \qquad (x \in \mathbb R).

Significance

The result. Theorem 2 is the basis for the paper's QED (quality- and efficiency-driven) approximations $Q_N \approx N + q\sqrt N$ , which give explicit formulas for the probability of delay, the probability of abandonment and the waiting-time distribution in terms of $\beta$ , $\mu$ and $\theta$ . Unlike the $M/M/N$ case, $\beta$ may be of either sign: abandonment keeps the system stable even when the offered load exceeds the number of agents. The resulting square-root staffing rule $N = R + \beta\sqrt R$ , with $R = \lambda/\mu$ , is used in call-center practice.

Formalizing it. The result is proved in the paper by Stone's criteria for birth–death processes, with uniqueness of the limit equation delegated to the literature. No many-server process limit exists on Prove2Me or in Mathlib. A formal proof would give the first machine-checked heavy-traffic process limit for a many-server queue, and the infrastructure (Poisson time-change representation of a birth–death process, path-space weak convergence to a continuous diffusion, well-posedness of a Lipschitz additive-noise SDE) would serve every other diffusion limit in queueing theory.

Difficulty

The infinitesimal-moment computation is elementary; it identifies the limit but does not prove convergence. The hard step is the passage from generator convergence to weak convergence of processes on $D[0,\infty)$ : tightness of $\{q_N\}$ in the Skorokhod space, which needs control of the jumps (of size $1/\sqrt N$ ) and of the unbounded state space, and identification of every limit point as a solution of the equation, which needs uniqueness of the limit. A pointwise limit of the drifts at each fixed $x$ is not enough: the convergence has to be controlled locally uniformly along the paths. A finite-dimensional limit at fixed times is weaker than the theorem.

Formalization scope

Queue. $Q_N$ is realized by the time-change representation of Mandelbaum, Massey and Reiman (1998), cited by the paper: $Q_N(t) = Q_N(0) + A(\lambda_N t) - S(\mu\int_0^t \min(Q_N(s), N)\,ds) - R(\theta_N \int_0^t (Q_N(s)-N)^+\,ds)$ , with $A, S, R$ independent unit-rate Poisson processes independent of $Q_N(0)$ . This has the birth–death law above.
Time. Paths are functions on $\mathbb R$ ; every condition is imposed for $t \ge 0$ only. Brownian time is $\mathbb R_{\ge 0}$ .
Indexing. $N$ is both the index and the number of agents; every hypothesis on the $N$ -th system is imposed for $N \ge 1$ . $\lambda_N$ , $\theta_N$ are real sequences and $\mu$ is fixed.
Weak convergence. All $Q_N$ live on one probability space, which is no loss since only their laws matter. $q_N(0) \Rightarrow \nu$ is convergence of $E\,g(q_N(0))$ for every bounded continuous $g$ . $q_N \Rightarrow q$ is stated in coupling form (Skorokhod representation with almost-sure uniform convergence on compact time intervals), which is equivalent to $J_1$ weak convergence when the limit is continuous.
Limit. The SDE is pathwise (Lebesgue integral, no Itô integral). Brownian motion is Mathlib's IsBrownianReal with every path continuous and every coordinate measurable. $q(0)$ is independent of $b$ , which is implicit in the paper. The goal asserts existence of a solution with $q_N \Rightarrow q$ and uniqueness of its law; dropping the uniqueness clause, fixing $\nu$ to a point mass, restricting to $\beta > 0$ , $\mu = 1$ , $\theta = \mu$ , or the stationary case is a different theorem.
Infinitesimal moments. Defined exactly as displayed, with $\lfloor\cdot\rfloor$ the integer part. The display is printed for $\theta = 0$ ; the milestone is its $0 < \theta < \infty$ instance with the limit $f$ of Theorem 2, pointwise in $x$ .
Not covered. The cases $\theta = 0$ and $\theta = \infty$ of Theorem 2* and the interchange of limits (Part 2).

Contributions welcome: a Poisson time-change existence theorem, tightness criteria in $D[0,\infty)$ , well-posedness of Lipschitz SDEs with additive noise, and the martingale-problem approach to identifying limits.

Selected references

O. Garnett, A. Mandelbaum, M. Reiman, Designing a Call Center with Impatient Customers, Manufacturing & Service Operations Management 4(3):208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753
S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
P. J. Fleming, A. Stolyar, B. Simon, Heavy Traffic Limit for a Mobile Phone System Loss Model, Proc. 2nd Int. Conf. on Telecommunication Systems Modeling and Analysis, 1994.
A. Mandelbaum, W. A. Massey, M. I. Reiman, Strong Approximations for Markovian Service Networks, Queueing Systems 30:149–201, 1998. https://doi.org/10.1023/A:1019112920622
S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

9 thms2 active usersReviewed

Completed

Combinatorics Probability Theoretical Computer Science·Captain: mikedeng1

On Lattices, Learning with Errors, Random Linear Codes, and Cryptography 4: A Random Subset Sum of l Uniform Elements of a Finite Abelian Group Is on Average Within √(|G|/2^l) of UniformResearch Paper

Motivation

Regev's On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324) introduced the Learning with Errors (LWE) problem and built a public-key cryptosystem on it. The source for this mission is that published J. ACM article. The paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series; this mission formalizes a self-contained piece of finite combinatorics from §5.

In the cryptosystem the public key is a list of $m$ LWE samples, and a bit is encrypted by adding up a uniformly random subset of them. Semantic security rests on one fact: if the public key were truly uniform, the sum of a random subset of it would be close to uniform, so the ciphertext would carry no information about the bit. Claim 5.3 (p. 34:36) makes this precise for an arbitrary finite abelian group $G$ . It is a special case of the leftover hash lemma of Impagliazzo and Zuckerman (1989), in which the family of functions $b \mapsto \sum_i b_i g_i$ indexed by $g \in G^l$ is a universal hash family. Variants of the same statement appear in the security proofs of most lattice-based encryption schemes that use random subset sums, including the dual-Regev and GPV-style constructions.

Setting

Let $G$ be a finite abelian group, written additively, with $|G|$ elements, and let $l \ge 0$ be an integer. For $g = (g_1, \dots, g_l) \in G^l$ and $b = (b_1, \dots, b_l) \in \{0,1\}^l$ the subset sum $\sum_i b_i g_i$ is the sum of the $g_i$ with $b_i = 1$ (the empty subset gives $0$ ). The distribution of the sum of a uniformly random subset of $g_1, \dots, g_l$ is

P_g(h) = \frac{1}{2^l}\,\bigl|\{\, b \in \{0,1\}^l \mid \textstyle\sum_i b_i g_i = h \,\}\bigr|, \qquad h \in G.

The paper defines the statistical distance of two densities as $\int |\varphi_1 - \varphi_2|$ , with range $[0,2]$ , and notes that the same definition applies to discrete random variables (p. 34:14). The distance of $P_g$ from the uniform distribution on $G$ is therefore

\Delta(g) = \sum_{h \in G} \Bigl| P_g(h) - \frac{1}{|G|} \Bigr|,

with no factor $\tfrac12$ . Expectations and probabilities over $g$ refer to a uniform choice of $g_1, \dots, g_l \in G$ , that is, the uniform distribution on all $|G|^l$ tuples, repetitions allowed: $\mathrm{Exp}_g[F(g)] = |G|^{-l}\sum_{g \in G^l} F(g)$ .

In Lean these objects are RegevLWE.SubsetSum.subsetSum, P, statDistUniform and expectG.

Formalization targets

Goal: Claim 5.3

\mathop{\mathrm{Exp}}_g\bigl[\Delta(g)\bigr] \le \sqrt{\frac{|G|}{2^l}} \qquad\text{and}\qquad \Pr_g\Bigl[\Delta(g) > \sqrt[4]{|G|/2^l}\Bigr] \le \sqrt[4]{\frac{|G|}{2^l}}.

Both sentences of the claim are in the goal. The second is what the security proof (Lemma 5.4, p. 34:37) uses: for all but a $\sqrt[4]{|G|/2^l}$ fraction of public keys, the random subset sum is within $\sqrt[4]{|G|/2^l}$ of uniform. The constants are exactly as printed.

Milestones

The $\ell_2$ norm as a collision probability (p. 34:36). For every $g$ , with $b, b'$ independent and uniform in $\{0,1\}^l$ ,

\sum_{h} P_g(h)^2 = \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i\Bigr] \le \frac{1}{2^l} + \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i \Bigm| b \neq b'\Bigr].

Collisions of distinct subsets (p. 34:37). For any $b \neq b'$ , $\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G|$ .
Expected $\ell_2$ norm (p. 34:37). $\mathrm{Exp}_g[\sum_h P_g(h)^2] \le 1/2^l + 1/|G|$ .
Cauchy–Schwarz and the $\ell_2$ identity (p. 34:37), pointwise in $g$ :

\sum_h \Bigl|P_g(h) - \frac{1}{|G|}\Bigr| \le |G|^{1/2}\Bigl(\sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2\Bigr)^{1/2}, \qquad \sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2 = \sum_h P_g(h)^2 - \frac{1}{|G|}.

Significance

The result. Claim 5.3 is the step in the security proof of Regev's cryptosystem that removes the public key from the picture: once the key is replaced by uniform samples (by the LWE assumption), the claim shows that an encryption is statistically close to uniform, independently of the encrypted bit. The parameter choice $m \ge (1+\epsilon)(n+1)\log p$ of Lemma 5.4 is exactly what makes $|G|/2^m$ negligible for $G = \mathbb{Z}_p^n \times \mathbb{Z}_p$ . Without the claim the cryptosystem would have a hardness assumption but no reduction from it.

Formalizing it. The claim is proved, with a complete argument in the paper; nothing here is open. To our knowledge no machine-checked proof of this statement, or of the leftover hash lemma for subset-sum hash families over a general finite abelian group, exists in Mathlib or on the platform. A formal proof gives a reusable, constant-exact statement of the subset-sum leftover hash lemma with the paper's normalization of statistical distance. The four milestones are standard facts about finite averages and collision probabilities that recur in many cryptographic security proofs.

Difficulty

There is no deep step; the work is in organizing finite counting arguments without loss. Two points need care. The collision fact $\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G|$ holds for every pair $b \neq b'$ only because the coefficients $b_i - b'_i$ lie in $\{-1, 0, 1\}$ : for a general linear form over a group with torsion, a nonzero coefficient vector need not give a uniformly distributed sum, so an argument that treats the coefficients as arbitrary integers fails. And passing from the $\ell_2$ bound to the expected $\ell_1$ distance requires the exchange of expectation and square root in the right direction (concavity), which is easy to misapply. The bound must hold for every finite abelian group and every $l$ , including $l = 0$ and $|G| = 1$ , with no asymptotic slack.

Formalization scope

$G$ is any type with [AddCommGroup G] [Fintype G] [DecidableEq G]; $l : ℕ$ , and $l = 0$ is allowed (then $P_g$ is the point mass at $0$ and the claim holds). No hypothesis is added to the paper's statement: $|G| \ge 1$ holds for every group.
$\{0,1\}^l$ is encoded as Fin l → Bool; $g$ ranges over all functions Fin l → G, so the uniform choice of $g$ is over all $|G|^l$ tuples with repetition, not over $l$ -element subsets of $G$ .
Every expectation and probability is an exact finite average with real values: $\mathrm{Exp}_g[F] = |G|^{-l}\sum_g F(g)$ , and $\Pr_g[E]$ is the number of tuples satisfying $E$ divided by $|G|^l$ . Probabilities over $(b, b')$ are counts over the $(2^l)^2$ pairs; the conditional probability given $b \neq b'$ divides by $(2^l)^2 - 2^l$ . At $l = 0$ the paper's conditional probability is undefined; Lean's convention $0/0 = 0$ makes milestone 1 read $1 \le 1$ there, which is consistent with the paper.
The statistical distance is $\sum_h |P_g(h) - 1/|G||$ , without $\tfrac12$ . A formalization with the $\tfrac12$ -normalized total variation distance would state a weaker result (half the bound) and is excluded. "More than" in the second sentence is strict, "at most" is $\le$ . The fourth root is Real.sqrt (Real.sqrt x).
Milestone 4 states only the first two steps of the paper's final chain (the Cauchy–Schwarz inequality and the identity), pointwise in $g$ ; the remaining two steps (Jensen for the square root and the substitution of milestone 3) are part of the goal. Its milestone text quotes the whole chain for context.
No definitions beyond the four above are needed, and no measure theory. Proofs of the milestones, and alternative proofs of the goal (for instance via Fourier analysis on $G$ ), are welcome.

Selected references

O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. doi:10.1145/1568318.1568324
R. Impagliazzo and D. Zuckerman, How to Recycle Random Bits, Proc. 30th IEEE FOCS, 248–253, 1989. doi:10.1109/SFCS.1989.63486
J. Håstad, R. Impagliazzo, L. A. Levin and M. Luby, A Pseudorandom Generator from any One-way Function, SIAM Journal on Computing 28(4), 1364–1396, 1999. doi:10.1137/S0097539793244708

6 thms2 active usersReviewed

All missions

On Minimizing the Ruin Probability by Investment and Reinsurance II: Equation (5) for g = f′ Has a Unique Strictly Decreasing Solution on [0, ∞)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 900)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Semidefinite Programming Relaxations for Semialgebraic Problems 1: A Polynomial System Has No Real Solution if and only if Its Degree-d Positivstellensatz SDP Is Feasible for All Large dResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Centralized and Competitive Inventory Models with Demand Substitution 1: The Competitive Substitution Game Has a Nash Equilibrium, Unique and Globally Stable When Substitution Rates Sum Below OneResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Centralized and Competitive Inventory Models with Demand Substitution 3: Under Multivariate Normal Demand the Centralized Expected Profit Decreases in Every Demand CorrelationResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 7)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Primal-Dual Active Set Strategy as a Semismooth Newton Method V: Local Superlinear Convergence in L² under a Norm GapResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (p. 15)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning II: The Gradient of the Normalized Discounted Value Is the Sum over Actions of ∇π·Q under the Discounted Future State DistributionTextbook

Why the gradient of the value matters

Setting

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning I: Approximate Policy Iteration with Max-Norm Evaluation Error ε Is Eventually Within 2ε/(1−γ)² of OptimalTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion 2: With Random Objective, Z(x) = Z_D(x) = Z_DD(x) and Moment-Matching Distributions Attain Z(x) AsymptoticallyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.2

Milestones

Significance

Difficulty

Formalization scope