Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Linear algebra Numerical Analysis Optimization·Captain: mikedeng1

The Primal-Dual Active Set Strategy as a Semismooth Newton Method II: Global Convergence and Monotonicity for M-MatricesResearch Paper

Motivation

Obstacle problems, contact problems and box-constrained quadratic programs share one finite-dimensional core: the linear complementarity problem "find $y \le \psi$ and $\lambda \ge 0$ with $Ay + \lambda = f$ and $\lambda_i(y_i - \psi_i) = 0$ ". After discretization by finite differences or piecewise linear finite elements, the matrix $A$ is typically an M-matrix, which is why this class sits at the centre of the numerical analysis of variational inequalities.

The primal-dual active set strategy solves such problems by guessing which constraints are active, solving one linear system on that guess, and updating the guess from the new primal and dual values. 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 problem. Local superlinear convergence then follows from Newton theory. This mission concerns the paper's global result: for M-matrices the method converges from every starting point, and its primal iterates decrease monotonically. A related global result for a purely primal active set method appears in Hoppe's 1987 analysis of multigrid methods for obstacle problems, which the paper cites as [H].

Setting

Fix $n \ge 0$ , a matrix $A \in \mathbb{R}^{n\times n}$ , vectors $f, \psi \in \mathbb{R}^n$ and a constant $c > 0$ . Vectors are compared componentwise. The paper writes $A$ for the matrix and calligraphic $\mathcal{A}$ , $\mathcal{I}$ for index sets; Lean uses A for the matrix and activeSet for $\mathcal{A}$ .

Problem (3.1). Find $(y, \lambda) \in \mathbb{R}^n \times \mathbb{R}^n$ with

Ay + \lambda = f, \qquad \lambda - \max(0, \lambda + c(y - \psi)) = 0,

the maximum taken componentwise. For $c > 0$ the second equation says exactly $y \le \psi$ , $\lambda \ge 0$ and $\lambda_i (y_i - \psi_i) = 0$ for every $i$ .

M-matrix. $A$ is an M-matrix if it is nonsingular, its off-diagonal entries satisfy $a_{ij} \le 0$ for $i \ne j$ , and its inverse is entrywise nonnegative, $A^{-1} \ge 0$ .

Blocks. For an index set $\mathcal{I}$ with complement $\mathcal{A}$ , $A_{\mathcal{I}}$ is the principal submatrix with rows and columns in $\mathcal{I}$ , and $A_{\mathcal{I}\mathcal{A}}$ the submatrix with rows in $\mathcal{I}$ and columns in $\mathcal{A}$ .

The algorithm. Start from arbitrary $(y^0, \lambda^0)$ . Given $(y^k, \lambda^k)$ , let

\mathcal{A}_k = \{ i : \lambda^k_i + c(y^k - \psi)_i > 0\}, \qquad \mathcal{I}_k = \{ i : \lambda^k_i + c(y^k - \psi)_i \le 0\},

and let $(y^{k+1}, \lambda^{k+1})$ 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. The solution of (3.1) is written $x^* = (y^*, \lambda^*)$ and the iterates $x^k = (y^k, \lambda^k)$ .

Formalization targets

Goal: Theorem 3.2 (p. 7)

If $A$ is an M-matrix, then for arbitrary initial data

x^k \to x^*, \qquad y^* \le y^{k+1} \le y^k \ \text{ for all } k \ge 1, \qquad y^k \le \psi \ \text{ for all } k \ge 2.

Milestones (Appendix A, p. 20)

For every partition $\mathcal{I}, \mathcal{A}$ : $A_{\mathcal{I}}$ is regular, $A_{\mathcal{I}}^{-1} \ge 0$ and $A_{\mathcal{I}}^{-1} A_{\mathcal{I}\mathcal{A}} \le 0$ .
Complementarity (A.1): $\lambda^k_i = 0$ or $y^k_i = \psi_i$ , for all $i$ and $k \ge 1$ , for every run and every matrix.
Monotonicity: $y^{k+1} \le y^k$ for $k \ge 1$ .
Primal feasibility: $y^k \le \psi$ for $k \ge 2$ .
Lower bound: $y^* \le y^k$ for $k \ge 1$ .
Remark A.1 and dual feasibility: if $\lambda^{\bar k}_i < 0$ with $\bar k \ge 1$ , then $\lambda^k_i = 0$ and $y^k_i \le \psi_i$ for all $k \ge \bar k + 1$ ; and $\lambda^k \ge 0$ for all $k$ beyond some $k_o$ .

A companion item states that a run exists from every initial pair when $A$ is an M-matrix.

Significance

The result. Theorem 3.2 makes the active set strategy a globally convergent method for the discretized obstacle problem, with no line search, no merit function and no damping. The monotonicity statement says more: from the second iterate on, every primal iterate is feasible and lies above the solution, and the iterates descend to it. Combined with the paper's observation (p. 7) that convergent iterates of the method converge in finitely many steps, it gives finite termination from every starting point. The theorem is the model for later global results on the method under weaker hypotheses, two of which (a norm condition and small perturbations of M-matrices) appear in the same paper as Theorems 3.3 and 3.4.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires the classical sign facts on principal blocks of M-matrices, which Mathlib does not contain, and a careful treatment of the iteration as a relation on pairs of vectors. The M-matrix block lemma is reusable well beyond this mission, for instance in comparison principles for discretized elliptic problems.

Difficulty

The obvious argument would bound a merit function or a contraction factor; neither is available, because the iteration map is discontinuous and the active sets change from step to step. The paper's argument is instead an order argument. Its central step is the monotonicity $y^{k+1} \le y^k$ : it requires the complementarity (A.1) of the previous iterate, which holds only from $k = 1$ on, and the sign structure of the blocks $A_{\mathcal{I}_k}^{-1}$ and $A_{\mathcal{I}_k}^{-1} A_{\mathcal{I}_k \mathcal{A}_k}$ for every possible active set. The index bounds are sharp in the sense that the statements fail at $k = 0$ (respectively $k = 1$ for feasibility), because the initial data are arbitrary. Convergence of the multipliers is a separate step: negative multiplier coordinates must be shown to vanish permanently after one more iteration.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the product is A *ᵥ y, and $\le$ on vectors is componentwise. Convergence of $x^k$ is in the product topology on $\mathbb{R}^n \times \mathbb{R}^n$ .
Nonsingularity of an M-matrix is IsUnit A.det. Lean's inverse of a singular matrix is the zero matrix, so without this clause every singular matrix with nonpositive off-diagonal entries would count as an M-matrix; the M-matrix definition is the page's, not an equivalent characterization.
The solution is a hypothesis IsSolution A f ψ c ystar lamstar. The paper speaks of "the unique solution"; for an M-matrix it exists and is unique by Berman–Plemmons, so the hypothesis assumes nothing the paper does not have. The uniqueness fact is not restated.
The algorithm is a relation. One step is IsStep, a run is IsRun with free initial data y 0, lam 0. The stopping option of step (iv) is not modelled. Because a universally quantified statement over runs would be empty if no run existed, the companion item run_exists states existence of a run from every initial pair.
The constant $c > 0$ is a binder of every statement that needs it; (A.1) needs neither $c > 0$ nor any hypothesis on $A$ , and has none.
Remark A.1 is printed without " $\bar k \ge 1$ "; its proof assumes it and the statement is false at $\bar k = 0$ , so the bound is kept.
A trivializing formalization is ruled out: no statement assumes monotonicity, feasibility or convergence of the iterates, and the M-matrix hypothesis cannot be met by a singular matrix.
Needed infrastructure: principal submatrices of M-matrices (Berman–Plemmons, Ch. 6), and inverse-nonnegativity arguments for block systems. Proofs of the block lemma, of (A.1) and of the order lemmas are welcome independently of the goal.

The printed closing step of the proof writes $\lambda^k = Ay^k + f$ ; step (iii) gives $\lambda^k = f - Ay^k$ . No item quotes or depends on that line.

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):865–888, 2002. https://doi.org/10.1137/S1052623401383558 (authors' version: https://hal.science/hal-01660511)
A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, Academic Press, 1979; reprinted as SIAM Classics in Applied Mathematics 9, 1994. https://doi.org/10.1137/1.9781611971262
R. H. W. Hoppe, Multigrid algorithms for variational inequalities, SIAM J. Numer. Anal. 24(5):1046–1065, 1987. https://doi.org/10.1137/0724069
L. Qi, J. Sun, A nonsmooth version of Newton's method, Math. Program. 58:353–367, 1993. https://doi.org/10.1007/BF01581275

9 thms2 active usersReviewed

Dynamic Programming Machine Learning Optimization+1·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

Motivation

Policy iteration replaces the current policy by the greedy policy with respect to its state-action values. With exact values this improves the policy at every state. When the improvement step is only approximate, or is restricted to a class of policies, a greedy replacement can make the policy worse, and the resulting error bounds are stated in max norm over all states, a quantity that sampling cannot control in large state spaces.

Conservative policy iteration (CPI), introduced by Kakade and Langford (ICML 2002) and developed in Chapter 7 of Kakade's PhD thesis (UCL, 2003), takes a different route. Instead of switching to a new policy, it mixes the current policy with a small amount of a better one, and it measures progress by an average over states visited under the current policy rather than by a maximum over all states. The thesis proves that the exact form of the algorithm improves its objective at every step, halts after a number of updates polynomial in the horizon and the accuracy, and returns a policy whose average advantages against an entire policy class are small. The approach underlies later trust-region and conservative update methods in reinforcement learning.

Setting

A finite Markov decision process has a finite state set $S$ , a finite action set $A$ , transition probabilities $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ . A stationary policy $\pi$ chooses action $a$ in state $s$ with probability $\pi(a\mid s)$ . For a discount factor $0\le\gamma<1$ the normalized value of $\pi$ 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],

which lies in $[0,1]$ . 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')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$ . The horizon time is $H=1/(1-\gamma)$ .

Fix a reset distribution $\mu$ on $S$ . The value of $\mu$ is $V_\pi(\mu)=\mathbb E_{s\sim\mu}V_\pi(s)$ . The discounted future state distribution is

d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,\ s_0\sim\mu),

and $d_{\pi,s_0}$ is the case where $\mu$ is the point mass at $s_0$ . For another policy $h$ :

the advantage under a distribution $\nu$ is $A_\pi(\nu,h)=\mathbb E_{s\sim\nu}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$ ;
the future state-action value is $\mathbb Q_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}Q_\pi(s,a)$ ;
the future advantage is $\mathbb A_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$ .

The conservative update with mixing weight $\alpha\in[0,1]$ is $\pi_{\rm new}=(1-\alpha)\pi+\alpha\pi'$ .

Exact CPI (Algorithm 11) works with a class $\Pi$ of stationary policies and an accuracy $\varepsilon>0$ . Starting from any stationary policy, it repeats three steps:

The ExactPolicyChooser returns $\pi'\in\arg\max_{h\in\Pi}\mathbb Q_\pi(\mu,h)$ .
If $\mathbb A_\pi(\mu,\pi')>\varepsilon/H$ , the algorithm sets $\alpha=\mathbb A_\pi(\mu,\pi')/(4H)$ and replaces $\pi$ by $(1-\alpha)\pi+\alpha\pi'$ .
Otherwise it halts and returns $\pi$ .

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

Every run $\pi_0,\pi_1,\dots$ of Exact CPI has a halting round $K$ with

K<\frac{8H^2}{\varepsilon^2},\qquad V_{\pi_{k+1}}(\mu)-V_{\pi_k}(\mu)>\frac{\varepsilon^2}{8H^2}\ \ (k<K),\qquad \mathbb A_{\pi_K}(\mu,h)\le\frac{\varepsilon}{H}\ \ (h\in\Pi).

The returned $\pi_K$ is a stationary policy. The thesis states the halting bound as $O(H^2/\varepsilon^2)$ calls to the chooser. The constant $8$ is the one the thesis's own Corollary 7.2.3 supplies, and the mission states it explicitly.

Milestones

Lemma 7.2.2. For every $\alpha\in[0,1]$ , with $\epsilon_\infty=\max_s|\mathbb E_{a\sim\pi'(\cdot\mid s)}A_\pi(s,a)|$ ,

V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A_\pi(\mu,\pi')-\frac{2\gamma\alpha}{1-\gamma(1-\alpha)}\epsilon_\infty\Big).

Corollary 7.2.3. If $\mathbb A_\pi(\mu,\pi')\ge0$ , the step $\alpha=\frac{1-\gamma}{4}\mathbb A_\pi(\mu,\pi')$ gives $V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\mathbb A_\pi(\mu,\pi')^2/8$ .
Domination of the start distribution (p. 88): $d_{\pi,\mu}\ge\mu/H$ .
Lemma 5.2.1, discounted half: $V_{\pi'}(s_0)-V_\pi(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d_{\pi',s_0}}\mathbb E_{a\sim\pi'(\cdot\mid s)}A_\pi(s,a)$ .
Theorem 7.3.1. If $A_\pi(\nu,h)\le\varepsilon/H$ for all $h\in\Pi$ , then for every $\pi'\in\Pi$ and every state $s_0$ ,

V_\pi(s_0)\ge V_{\pi'}(s_0)-\varepsilon-H\|d_{\pi',s_0}-\nu\|_1.

Example 7.4.1. A two-state MDP on which the bound of Lemma 7.2.2 holds with equality for all $\alpha$ and $\gamma$ .

Milestones 1, 2 and 4 are already stated on the platform from Kakade–Langford (2002), in the same normalized model. They are included here as references and are not posed again.

Significance

The result. Theorem 7.3.2 is the exact-oracle core of CPI's sample-complexity analysis: the sample-based version later in the chapter replaces the exact chooser and the exact future advantage by estimates. The guarantee is stated through future advantages, so it does not depend on a max-norm accuracy over all states. Through Theorem 7.3.1 it translates into a value guarantee against every policy of the class whose future state distribution is close to the measure the algorithm was trained on. The output need not lie in $\Pi$ : even for a deterministic class the returned policy is in general stochastic.

Formalizing it. All results here are proved in the thesis, and the three referenced statements are proved on the platform. None of the new statements has a machine-checked proof. The mission adds a fully specified Exact CPI run as a Lean object, an explicit constant in place of the $O(\cdot)$ , and checked versions of the μ-optimality bound and of the tightness example. Its layer is shared with the Kakade–Langford missions, so later work on sample-based CPI can build on it directly.

Difficulty

The halting bound needs two ingredients that are easy to separate and easy to get wrong. The improvement guarantee of Corollary 7.2.3 holds only for a policy and a mixture weight in $[0,1]$ , so every iterate of the run must be shown to remain a policy and every step size to stay in range. The count of updates then rests on the normalized values being bounded in $[0,1]$ , a property of the model rather than of the algorithm. The output condition is stated for every $h\in\Pi$ , while the algorithm only tests the one policy the chooser returned, and the chooser maximizes future state-action values rather than future advantages.

A tempting shortcut is the thesis's remark on p. 88 that $\mathbb A_\pi(\mu,h)\le\varepsilon/H$ implies $A_\pi(\mu,h)\le\varepsilon$ . This is false in general: it would need $\mathbb E_{a\sim h}A_\pi(s,a)\ge0$ at every state. The mission formalizes only the true ingredient, $d_{\pi,\mu}\ge\mu/H$ .

Formalization scope

The layer is the published normalized model ApproxOptRL.Shared.Model: value, qValue, advantage, futureStateDist, and eta for $V_\pi(\mu)$ . The future advantage is ApproxOptRL.CPI.policyAdvantage and the conservative update is ApproxOptRL.CPI.mixPolicy. The model makes these commitments:

$S$ and $A$ are finite nonempty types.
Policies are maps $\pi:S\to A\to\mathbb R$ with IsPolicy, and deterministic policies are indicator policies.
Values carry the factor $1-\gamma$ , so all constants are the thesis's normalized ones. The thesis's statements for infinite state spaces are taken for finite $S$ , where $\|\cdot\|_1$ is a finite sum.
In Lean the policy class is called Pi because Π is reserved.

The run is the explicit predicate IsExactCPIRun: up to the round where the algorithm halts, the chooser output lies in $\Pi$ and maximizes $\mathbb Q_{\pi_k}(\mu,\cdot)$ over $\Pi$ , and the update uses exactly $\alpha_k=\mathbb A/(4H)$ . The halting round is part of the conclusion, never a hypothesis. A formalization in which the halting test or the step size is a free variable, or in which $\Pi$ is empty, would make "halts" an assumption or the run hypothesis unsatisfiable; the goal fixes both and requires $\Pi$ nonempty. The chooser's argmax is assumed to be attained, as in the thesis.

Contributions that would help: bounds $0\le V_\pi\le1$ and $|A_\pi|\le1$ for the normalized model, summability facts for futureStateDist, and a proof that a mixture of policies is a policy. These are reusable across every mission built on the same model.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003, Chapter 7. https://discovery.ucl.ac.uk/id/eprint/10100726/
S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002, pp. 267–274. https://dl.acm.org/doi/10.5555/645531.656005

12 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

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion 3: With Random Right-Hand Side and Known Dual Extreme Points, the Problem Equals the Semidefinite Program (14)Research Paper

Motivation

Two-stage stochastic linear programs model a decision $x$ taken before uncertainty is revealed, followed by a corrective recourse action once it is. The classical model needs the full probability distribution of the uncertain data, which in practice is rarely known; often only estimates of the mean and the second moments are available, and the computed plan can be sensitive to the distribution assumed. The minimax (distributionally robust) approach replaces the single distribution by the class of all distributions with given first and second moments and optimizes against the worst member of that class. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) combine this with risk aversion, through a piecewise-linear disutility of the second-stage cost, and determine which instances can be solved as semidefinite programs.

When the randomness sits in the right-hand side of the second stage, the paper shows that the problem is NP-hard in general (Theorem 3.1). This mission concerns the tractable special case that follows (§3.2): if the extreme points of the dual feasible region of the recourse problem are known, the whole minimax problem is one semidefinite program.

Setting

A first-stage decision $x\in\mathbb R^n$ is feasible if $x\in X=\{x : Ax=b,\ x\ge 0\}$ and costs $c'x$ . Given a recourse matrix $W\in\mathbb R^{r\times d}$ , a technology matrix $T\in\mathbb R^{r\times n}$ , a constant cost vector $q\in\mathbb R^d$ and a realized right-hand side $h\in\mathbb R^r$ , the second-stage cost is written as the optimal value of the dual of the recourse linear program,

\mathcal Q(h,x)=\max_{p}\ (h-Tx)'p\quad\text{s.t.}\quad W'p\le q .

Risk aversion enters through the disutility $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge 0$ . The right-hand side $\tilde h$ is random, and its distribution is only known to lie in the moment class

\mathcal P=\{P : \mathbb E_P[\tilde h]=\mu,\ \mathbb E_P[\tilde h\tilde h']=Q\}.

The worst-case expected disutility is $\hat Z(x)=\sup_{P\in\mathcal P}\mathbb E_P[\mathbb U(\mathcal Q(\tilde h,x))]$ , and the problem is

Z=\min_{x\in X}\big(c'x+\hat Z(x)\big).

The moment problem defining $\hat Z(x)$ has the dual (12): minimize $Q\cdot Y+\mu'y+y_0$ over symmetric $Y$ , $y\in\mathbb R^r$ , $y_0\in\mathbb R$ with $h'Yh+y'h+y_0\ge\mathbb U(\mathcal Q(h,x))$ for every $h$ , where $Q\cdot Y=\sum_{i,j}Q_{ij}Y_{ij}$ .

The standing assumptions are: $X$ nonempty and bounded (Assumption 1); complete recourse, $\{Ww : w\ge 0\}=\mathbb R^r$ (Assumption 2); a nonempty dual polyhedron $\{p : W'p\le q\}$ (Assumption 3); $Q\succ\mu\mu'$ (Assumption 4); and the extreme points $p_1,\dots,p_N$ of $\{p : W'p\le q\}$ are known (Assumption 5).

Formalization targets

Goal: Theorem 3.2 (p. 589)

The problem is equivalent to the semidefinite program

\hat Z_{\rm SDP}=\min_{x,Y,y,y_0}\ c'x+Q\cdot Y+\mu'y+y_0\ \ \text{s.t.}\ \begin{pmatrix}Y & \tfrac12(y-\alpha_k p_i)\\ \tfrac12(y-\alpha_k p_i)' & y_0+\alpha_k p_i'Tx-\beta_k\end{pmatrix}\succeq 0\ \ \forall k,i,\quad Ax=b,\ x\ge 0, \tag{14}

in the sense that $\hat Z(x)$ equals the value of the per- $x$ program (15) for every $x\in X$ , and $Z=\hat Z_{\rm SDP}$ , both being genuine finite infima.

Milestones (§3.1 and the proof of Theorem 3.2, pp. 588–590)

Strong duality for (11)/(12): $\hat Z(x)=\hat Z_D(x)$ .
The constraints of (12) are equivalent to $h'Yh+(y-\alpha_kp)'h+y_0+\alpha_kp'Tx-\beta_k\ge 0$ for all $h$ , all $p$ with $W'p\le q$ and all $k$ .
Every feasible $Y$ of (12) is positive semidefinite.
$\mathcal Q(h,x)=\max_{i=1,\dots,N}(h-Tx)'p_i$ .
A quadratic $h'Yh+2v'h+c$ is nonnegative on $\mathbb R^r$ iff the bordered matrix $\begin{pmatrix}Y&v\\v'&c\end{pmatrix}$ is positive semidefinite (already proved on the platform).
The feasible sets of (12) and (15) coincide, so $\hat Z_D(x)$ is the value of (15).

Significance

The result. Theorem 3.2 turns a two-level problem — a minimum over $x$ of a supremum over an infinite-dimensional set of distributions — into one convex program of polynomial size in $n$ , $r$ , $K$ and $N$ , jointly in the first-stage decision and the dual multipliers. The first-stage decision enters the linear matrix inequalities only through the corner entry $y_0+\alpha_kp_i'Tx-\beta_k$ , which is affine in $x$ ; this is what keeps the joint program convex. Together with the NP-hardness of the general case (Theorem 3.1), it locates the source of intractability in the enumeration of dual vertices. The same program (15) is the starting point of the construction of an extremal distribution (Theorem 3.3), which the paper uses to stress-test first-stage solutions.

Formalizing it. The result is proved in the paper, with strong duality for the moment problem cited from the literature. Nothing in this chain is formalized: neither the moment-problem duality under the interior condition $Q\succ\mu\mu'$ , nor the vertex representation of a bounded linear program over a pointed polyhedron given by its extreme points. The lemma that a nonnegative quadratic corresponds to a positive semidefinite bordered matrix is already proved on the platform and is reused.

Difficulty

The reduction from (12) to (15) is elementary once $\mathcal Q(h,x)=\max_i(h-Tx)'p_i$ is available, but that identity is a genuine statement about polyhedra: the dual region $\{p : W'p\le q\}$ is unbounded, so compactness arguments such as Krein–Milman do not apply, and one needs both that the polyhedron is pointed (here a consequence of complete recourse, which forces $W$ to have full row rank) and that a bounded linear objective attains its maximum at a vertex. The other substantial step is strong duality between the moment problem over measures and the semi-infinite dual (12), which requires the moment vector $(\mu,Q)$ to lie in the interior of the moment cone; without $Q\succ\mu\mu'$ a duality gap or an empty class $\mathcal P$ can occur. Finally, the equality $Z=\hat Z_{\rm SDP}$ requires exchanging an infimum over $x$ with the infimum over the dual variables, which needs each per- $x$ program to be feasible and bounded.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and pieces and extreme points are indexed by Fin K and Fin N (zero-based). The paper's letter $p$ is both the dimension of $q$ and the dual variable; in Lean the dimension is $d$ and the dual vector is π. The class $\mathcal P$ consists of probability measures on $\mathbb R^r$ with square-integrable coordinates, mean $\mu$ and uncentred second-moment matrix $Q$ , built on the published MomentDRO.Conf.Setting; the paper's densities are replaced by measures. $\mathcal Q(h,x)$ is the real supremum over the dual polyhedron. Every printed min/max is a real infimum/supremum of a set of objective values, and the statements assert with IsLUB/IsGLB that these are genuine finite bounds; attainment of the minima is not claimed. $Y$ is required symmetric throughout. The bordered matrix is the published WorstCaseVaR.KnownMoments.bordered and $\succeq 0$ is Matrix.PosSemidef.

Readings of the source:

As printed, Assumption 2 (complete recourse) and Assumption 3 ("for all $q$ ") contradict each other when $r\ge 1$ . The section-wise reading is used: complete recourse together with dual feasibility at the single constant $q$ of §3.
"Assumption i" in Theorem 3.2 and in its proof is read as Assumption 5.
"The strong duality condition" is read as Assumption 4.
Assumption 5 is the hypothesis that the list $p_1,\dots,p_N$ is exactly the set of extreme points of the dual region; "explicitly known" has no further mathematical content.
(11) integrates over $\mathbb R^p$ where $\mathbb R^r$ is meant.

A formalization in which $\hat Z_{\rm SDP}$ is defined through $\hat Z_D(x)$ , or in which positive semidefiniteness is replaced by a hand-written quadratic condition, would make the goal a restatement of strong duality; (14) is stated as a single program in $(x,Y,y,y_0)$ with Matrix.PosSemidef constraints. The hypotheses of the goal are satisfiable ( $r=1$ , $W=[1,-1]$ , $q=(1,1)$ , $\mu=0$ , $Q=1$ , $X=\{1\}$ ).

Contributions welcome: the vertex representation of bounded linear programs over pointed polyhedra, and duality for moment problems with first and second moments, are both reusable well beyond this mission.

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
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
A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001, pp. 135–165. https://doi.org/10.1007/978-1-4757-3403-4_7
L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: a conic programming approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101

10 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

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Designing a Call Center with Impatient Customers III: Square-Root Staffing Is Equivalent to a Nondegenerate Delay Probability and to Abandonment of Order 1/√NResearch Paper

Motivation

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

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

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

Setting

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

\pi_k\propto\frac{(\lambda/\mu)^k}{k!}\ (k\le N),\qquad \pi_k\propto\prod_{j=N+1}^{k}\frac{\lambda}{N\mu+(j-N)\theta}\cdot\frac{(\lambda/\mu)^N}{N!}\ (k>N).

The three performance measures are:

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

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

w(x,y)=\Bigl[1+\frac{h(-xy)}{y\,h(x)}\Bigr]^{-1}.

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

Formalization targets

Goal: Theorem 4 (p. 219)

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

\lim_{N\to\infty}\sqrt N(1-\rho_N)=\beta\in\mathbb R,\qquad \lim_{N\to\infty}P_N\{W>0\}=\alpha\in(0,1),\qquad \lim_{N\to\infty}\sqrt N\,P_N\{Ab\}=\Delta\in(0,\infty),

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

13 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

The Sample Average Approximation Method for Stochastic Discrete Optimization 2: √N(v̂_N − v) Converges in Distribution to the Minimum over S of a Centered Gaussian VectorResearch Paper

Motivation

Many decision problems in operations research have a finite set of alternatives and an objective that is an expectation: choose a configuration, a route or a stocking level $x$ from a finite set $\mathcal S$ to minimize the expected cost $\mathbb E\,G(x, W)$ , where $W$ is random. When the expectation cannot be computed in closed form, the sample average approximation (SAA) method draws an i.i.d. sample $W^1, \dots, W^N$ , replaces the expectation by the sample average, and solves the resulting deterministic problem. Its optimal value $\hat v_N$ is used in practice as an estimate of the true optimal value $v^*$ , and statistical bounds on the quality of a candidate solution are built from replications of $\hat v_N$ (Mak, Morton and Wood, 1999). Confidence statements of that kind need the distribution of $\hat v_N$ , at least asymptotically.

Kleywegt and Shapiro (preprint, two-author version; published with Homem-de-Mello in SIAM J. Optim. 12 (2002)) gave the asymptotic distribution of $\hat v_N$ for discrete problems in their Proposition 2.3. The analogous result for problems with continuous decision variables is due to Shapiro (1991); the discrete statement needs neither compactness nor Lipschitz continuity in $x$ , and requires finite variances only at the optimal solutions.

Setting

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

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

and its set of optimal solutions is $\mathcal S^* = \{x \in \mathcal S : g(x) = v^*\}$ . Given an i.i.d. sample $W^1, W^2, \dots$ 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),

with optimal set $\hat{\mathcal S}_N$ . Because $\mathcal S$ is finite, all minima are attained. For $x \in \mathcal S$ the variance $\sigma^2(x) = \operatorname{Var}\{G(x, W)\}$ of (2.7) may or may not exist; when the variances exist on a subset $T \subseteq \mathcal S$ , the autocovariance of $G$ on $T$ is the matrix $\big(\operatorname{Cov}(G(x, W), G(x', W))\big)_{x, x' \in T}$ . Convergence in distribution is written $\Rightarrow$ .

Formalization targets

Goal: Proposition 2.3, (2.8)

If the variances $\sigma^2(x)$ exist for every $x \in \mathcal S^*$ , then

\sqrt N\,(\hat v_N - v^*) \;\Rightarrow\; \min_{x \in \mathcal S^*} Y(x),

where $(Y(x))_{x \in \mathcal S^*}$ is a Gaussian vector with zero mean and $\operatorname{Cov}(Y(x), Y(x')) = \operatorname{Cov}(G(x, W), G(x', W))$ . The statement is general in the number of optimal solutions: when $\mathcal S^*$ has more than one point, the limit is the minimum of a correlated Gaussian vector, which is not normal and has negative mean.

Milestones (in the order of the paper's argument)

Almost surely, $\hat v_N - \min_{x \in \mathcal S^*} \hat g_N(x) = 0$ for all $N$ large enough.
(2.6): $\sqrt N\,[\hat v_N - \min_{x \in \mathcal S^*} \hat g_N(x)] \to 0$ almost surely and in probability.
$\sqrt N\,[\min_{x \in \mathcal S^*} \hat g_N(x) - v^*] = \min_{x \in \mathcal S^*} \{\sqrt N\,[\hat g_N(x) - g(x)]\}$ .
The joint central limit theorem: for $T \subseteq \mathcal S$ with finite variances,

\Big(\sqrt N\,[\hat g_N(x) - g(x)]\Big)_{x \in T} \;\Rightarrow\; (Y(x))_{x \in T}.

Companions

(2.9): if $\mathcal S^* = \{x^*\}$ , then $\sqrt N\,(\hat v_N - v^*) \Rightarrow N(0, \sigma^2(x^*))$ .
Negative bias (pp. 4–5): for every $N \ge 1$ , $\mathbb E[\hat v_N] \le v^*$ .

Significance

The result. Proposition 2.3 identifies the first-order fluctuations of the SAA optimal value. It shows that $\hat v_N$ is $\sqrt N$ -consistent, that it is asymptotically normal when the true optimum is unique, and that its asymptotic bias is of order $N^{-1/2}$ and equal to $\mathbb E[\min_{x \in \mathcal S^*} Y(x)] < 0$ when several solutions are optimal and their costs are not perfectly correlated. Confidence intervals and stopping rules for SAA, and the statistical lower bounds used to assess candidate solutions, rest on this description.

Formalizing it. The result is classical and proved on paper; it has not been machine-checked. A formal proof requires a multivariate central limit theorem, which this Mathlib does not contain (only the one-dimensional CLT is available), together with the transfer of convergence in distribution through the continuous map $y \mapsto \min_x y(x)$ and through perturbations that vanish in probability. These components are general probability results whose use extends well beyond stochastic programming. The negative-bias inequality and the singleton case (2.9) are included as companion targets.

Difficulty

The argument on the page is short, and each step names a standard theorem. The formal difficulty is that two of those theorems are not available in the needed form. The central limit theorem is used for a random vector indexed by $\mathcal S^*$ , with an arbitrary, possibly singular, covariance matrix; a coordinatewise application of the one-dimensional CLT gives only the marginal limits, which do not determine the law of the minimum. The step from (2.6) to (2.8) combines convergence in distribution with a term that tends to zero in probability, which requires a Slutsky-type lemma on the real line. The tempting simplification of assuming a unique optimal solution removes exactly the case in which the limit is not normal, and is therefore not the goal.

Formalization scope

The feasible set is a Finset of an arbitrary type X, assumed nonempty; minima over it and over $\mathcal S^*$ are Finset.inf', so they are attained. $\mathcal S^*$ is the Finset of minimizers of $g$ . 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. "The variance exists" is square integrability (MemLp … 2), assumed in the goal only on $\mathcal S^*$ , exactly as in the Proposition. Convergence in distribution is Mathlib's TendstoInDistribution; the limit is any random vector $Y$ , on any probability space, whose law is multivariateGaussian 0 Σ on the Euclidean space $\mathbb R^{\mathcal S^*}$ , with $\Sigma$ the autocovariance matrix of $G$ on $\mathcal S^*$ . That matrix is positive semidefinite under the variance hypothesis, so the Gaussian law is genuine (Mathlib's multivariateGaussian degenerates to a point mass only for a matrix that is not positive semidefinite). The milestone CLT is stated jointly, for every subfamily $T \subseteq \mathcal S$ with finite variances; the page states it for $T = \mathcal S$ in terms of marginals plus covariances.

A trivializing formalization is ruled out: the limit is indexed by $\mathcal S^*$ and not by $\mathcal S$ , its covariance is the autocovariance of $G$ and not a free matrix, square integrability is assumed wherever a covariance is used, and the negative-bias statement asserts integrability of $\hat v_N$ so that the Bochner integral is not its junk value $0$ .

A complete development needs the multivariate central limit theorem for i.i.d. square-integrable vectors (for instance through characteristic functions or the Cramér–Wold device), the continuous mapping theorem, a Slutsky lemma, and the strong law of large numbers applied to finitely many functions. The multivariate CLT and the Slutsky lemma are reusable beyond this mission. Contributions to any of these, and proofs of any item, 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. Shapiro, Asymptotic analysis of stochastic programs, Annals of Operations Research 30:169–186, 1991. https://doi.org/10.1007/BF02204815
W. K. Mak, D. P. Morton and R. K. Wood, Monte Carlo bounding techniques for determining solution quality in stochastic programs, Operations Research Letters 24:47–56, 1999. https://doi.org/10.1016/S0167-6377(98)00054-6
A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

7 thms2 active usersReviewed

Algorithmic Game Theory Dynamical Systems Linear algebra·Captain: mikedeng1

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 1: Near the Two-Player Unit-Disk Game Γ₀ of Section II, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

Learning in games asks whether players who adjust their strategies over time, by simple rules, end up at a Nash equilibrium. Many adaptive dynamics share one informational feature: each player's adjustment depends on the current play and on that player's own payoff function, but not on the payoffs of the others. Hart and Mas-Colell (AER 2003) call such dynamics uncoupled, and show that this feature alone rules out guaranteed convergence to Nash equilibrium, even for families of games in which every game has exactly one equilibrium. Earlier non-convergence results, such as Shapley's example for fictitious play and the cycling examples of Jordan (1993) and Foster and Young (1998), concern particular dynamics; this one applies to the whole class of uncoupled dynamics. It is one reason the learning literature turned to weaker targets such as correlated equilibrium, which regret-based uncoupled procedures do reach (Hart and Mas-Colell, Econometrica 2000).

The paper proves its theorem in two settings: a two-player game with a continuum of strategies (§II and the Appendix) and a three-player game with two strategies each (§III). This mission formalizes the first setting.

Setting

There are two players, $i=1,2$ , and $j=3-i$ denotes the other player. Each player's strategy set is the closed unit disk $D=\{z\in\mathbb R^2:\|z\|\le1\}$ , and a profile is $x=(x^1,x^2)\in X:=D\times D$ . A game $\Gamma=(u^1,u^2)$ is a pair of payoff functions on $X$ . A profile $\bar x$ is a (pure) Nash equilibrium if no player gains by changing only their own strategy. A dynamic for a family $\mathcal U$ of games is a vector field $F(x;\Gamma)$ on $X$ for each $\Gamma\in\mathcal U$ , read $\dot x=F(x;\Gamma)$ . It is uncoupled if $F^i$ depends on the game only through $u^i$ : two games of $\mathcal U$ in which player $i$ has the same payoff function give the same $F^i(x;\cdot)$ at every $x\in X$ .

A dynamic is Nash-convergent for $\mathcal U$ if, for every $\Gamma\in\mathcal U$ with its Nash equilibrium $\bar x(\Gamma)$ :

$F(\cdot\,;\Gamma)$ is $C^1$ on $X$ ;
$F(\bar x(\Gamma);\Gamma)=0$ ;
all eigenvalues of the $4\times4$ Jacobian matrix of $F(\cdot\,;\Gamma)$ at $\bar x(\Gamma)$ have negative real parts;
every solution $x(t)$ converges to $\bar x(\Gamma)$ as $t\to\infty$ , from any initial condition.

The game $\Gamma_0$ has payoffs $u_0^i(x^i,x^j)=-\|x^i-\varphi(x^j)\|^2$ . Here $\varphi:D\to D$ is continuous, $\varphi(z)=2z$ for $\|z\|\le\frac13$ , $\varphi$ rotates the unit circle by $\pi/4$ , and $\varphi$ is affine on rays in between. The family $\mathcal U_0$ consists of the games $u^i(x^i,x^j)=-\|x^i-\xi^i(x^j)\|^2$ with continuous $\xi^i:D\to D$ such that $\xi^i(\xi^j(x^i))=x^i$ has a unique solution. Every such game has a unique Nash equilibrium, and $\Gamma_0\in\mathcal U_0$ has the equilibrium $(0,0)$ .

Formalization targets

Goal: THEOREM 1 for the game $\Gamma_0$ of §II

Let $\mathcal U$ be a family in which each game has a single Nash equilibrium and which contains every game of $\mathcal U_0$ within some $\eta>0$ of $\Gamma_0$ . Then

F\ \text{uncoupled for}\ \mathcal U\ \Longrightarrow\ F\ \text{is not Nash-convergent for}\ \mathcal U.

Milestones

the explicit $\varphi$ has the two required properties, and rotates by an angle in $[0,\pi/4]$ (fn. 21);
every game of $\mathcal U_0$ has a unique Nash equilibrium, and that of $\Gamma_0$ is $(0,0)$ ;
Lemma 2: for an uncoupled Nash-convergent dynamic on $\mathcal U_0$ , at a unique best reply $F^i=0$ and the own-strategy Jacobian block $J^i$ has eigenvalues with negative real parts;
the derivative identity, giving the Jacobian at $\Gamma_0$ the block form

J=\begin{bmatrix}J^1&-2J^1\\-2J^2&J^2\end{bmatrix};

the coefficient $a_3=3\det(J^1)\operatorname{tr}(J^2)+3\det(J^2)\operatorname{tr}(J^1)$ of $\lambda$ in $\det(J-\lambda I)$ , and Lemma 3: if $J^1,J^2$ are stable, then $J$ has an eigenvalue with positive real part;
the main-text result: no uncoupled dynamic is Nash-convergent for $\mathcal U_0$ ;
the Appendix: the functions $\psi_a$ satisfy conditions (1)–(4), and the conclusions of Lemma 2 at $\Gamma_0$ already follow from the games of $\mathcal U_0$ near $\Gamma_0$ .

A companion statement, that the coupled dynamic $\dot x=\bar x(\Gamma)-x$ is Nash-convergent, shows that the notion of Nash-convergence can be met.

Significance

The theorem identifies an informational obstruction rather than a computational one. Convergence to Nash equilibrium is easy if the dynamic may use the whole game, as the coupled dynamic $\dot x=\bar x(\Gamma)-x$ shows. It fails once each player may react only to their own payoff function, and the failure persists on an arbitrarily small neighborhood of a single game. It explains why no natural adaptive procedure has been found that converges to Nash equilibrium in general, and it motivates the stochastic, finite-memory and correlated-equilibrium variants studied afterwards (for example Hart and Mas-Colell, GEB 2006).

The result is proved in the paper. As far as the curators know, it has no machine-checked proof. A formalization fixes the model precisely. That matters here, because the conclusion depends on details the prose treats lightly: which perturbations the family must contain, what the Jacobian is at boundary points, and which solutions count.

Difficulty

The obvious argument fails because an uncoupled dynamic is a different vector field for each game, and nothing forces the fields to fit together except the uncoupledness constraint. The proof extracts information about $F(\cdot\,;\Gamma_0)$ from auxiliary games that share one player's payoff with $\Gamma_0$ , and in which that player's best reply is constant. Making those auxiliary games lie in the family is the delicate part: in $\mathcal U_0$ they are immediate, but near $\Gamma_0$ they require the functions $\psi_a$ of the Appendix, whose fixed-point conditions (3) and (4) rest on an angle argument. The linear-algebra step is exact: the stability of $J^1$ and $J^2$ must be shown to force instability of the coupled $4\times4$ matrix through the sign of one coefficient of its characteristic polynomial.

Formalization scope

$\mathbb R^2$ is modelled as $\mathbb C$ , and rotation by $\theta$ is multiplication by $e^{i\theta}$ . Players are Fin 2, 0-based, and the other player is i + 1. A game is a pair of real functions on $\mathbb C^2$ , but every definition looks only at its values on $X=D\times D$ . Nash equilibria are pure equilibria in $X$ (fn. 9 notes there are no mixed ones). Derivatives are Fréchet derivatives within $X$ . Eigenvalue conditions use the published predicate FatkhullinPolyak.Discrete.IsHurwitz, with the $4\times4$ Jacobian indexed in player-major order. The $C^1$ and Jacobian conditions, which the paper imposes on every dynamic it considers, are part of NashConvergent. The single-Nash-equilibrium property is a hypothesis of the goal.

Two encodings are deliberate:

The neighborhood. " $\mathcal U$ contains a neighborhood of $\Gamma_0$ " is read as the Appendix reads it: $\mathcal U$ contains every game of $\mathcal U_0$ close to $\Gamma_0$ in the sense of fn. 7. This is implied by the literal hypothesis, so the formal theorem is at least as strong. A full neighborhood contains games with several equilibria, so together with the single-equilibrium hypothesis it would make the theorem vacuous.
Solutions. Solutions are curves that stay in $X$ . If curves were allowed to leave $X$ , they would follow values of $F$ that no game constrains, and Nash-convergence would fail for every $F$ , which makes the goal trivial. The goal must also not be met through an empty family: the hypotheses are jointly satisfiable, for instance by $\{\Gamma\in\mathcal U_0:\Gamma\text{ within }1\text{ of }\Gamma_0\}$ .

The development needs:

calculus of $C^1$ maps on a product of disks;
spectra of real matrices viewed over $\mathbb C$ and the characteristic polynomial of a $4\times4$ block matrix;
elementary planar geometry of rotations and radial interpolation.

The linear-algebra milestones (block Jacobian, $a_3$ , Lemma 3) are independent of game theory and reusable. Contributions are welcome on any milestone, in any order.

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
S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68(5), 1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153
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
D. P. Foster and H. P. Young, On the Nonconvergence of Fictitious Play in Coordination Games, Games and Economic Behavior 25(1), 79–96, 1998. https://doi.org/10.1006/game.1997.0615
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

14 thms2 active usersReviewed

Numerical Analysis Optimization·Captain: mikedeng1

The Primal-Dual Active Set Strategy as a Semismooth Newton Method I: Local Superlinear Convergence for P-Matrix Complementarity ProblemsResearch Paper

Motivation

Many problems in optimization and in the discretization of partial differential equations reduce to a linear complementarity problem with an obstacle: find $y, \lambda \in \mathbb{R}^n$ with

Ay + \lambda = f, \qquad y \le \psi, \quad \lambda \ge 0, \quad (\lambda, y - \psi) = 0,

for a matrix $A$ and vectors $f, \psi$ . When $A$ is symmetric positive definite this is the optimality system of the quadratic program $\min \tfrac12 (y, Ay) - (f, y)$ subject to $y \le \psi$ . Finite-difference and finite-element discretizations of obstacle problems and of control-constrained optimal control problems lead to systems of exactly this form, with $n$ in the thousands or millions.

The primal-dual active set strategy solves such systems by guessing, at every iteration, which constraints are active and solving one linear system for that guess. It was introduced as a special case of generalized Moreau–Yosida approximations by Ito and Kunisch, and was observed to converge in a few iterations, typically without a line search. M. Hintermüller, K. Ito and K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3):865–888, 2002 (DOI 10.1137/S1052623401383558; authors' version HAL hal-01660511) explained that behaviour: the strategy is a semismooth Newton method for a nonsmooth reformulation of the problem, and therefore inherits local superlinear convergence. This mission formalizes that local theory, the first of a five-part series on the paper.

Setting

Fix $n \ge 0$ , $A \in \mathbb{R}^{n\times n}$ , $f, \psi \in \mathbb{R}^n$ and $c > 0$ . Vectors are ordered componentwise. The complementarity conditions are equivalent to one nonsmooth equation, so the problem becomes

Ay + \lambda = f, \qquad \lambda - \max(0, \lambda + c(y - \psi)) = 0, \tag{3.1}

with the maximum taken componentwise. The paper writes $A$ for the matrix and calligraphic $\mathcal{A}$ , $\mathcal{I}$ for index sets; the two are unrelated.

Primal-dual active set algorithm. Given an iterate $(y^k, \lambda^k)$ , the active set is $\mathcal{A}_k = \{i : \lambda^k_i + c(y^k - \psi)_i > 0\}$ and the inactive set is $\mathcal{I}_k = \{i : \lambda^k_i + c(y^k - \psi)_i \le 0\}$ . The next iterate solves

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 run is a sequence of iterates, from arbitrary initial data $(y^0, \lambda^0)$ , in which every pair follows its predecessor in this way.

A P-matrix is a square matrix all of whose principal minors are positive. For a P-matrix every principal block $A_{\mathcal{I}}$ is invertible, so every step is uniquely solvable, and (3.1) has exactly one solution $(y^*, \lambda^*)$ .

Slant differentiability. Let $X, Z$ be Banach spaces and $F : X \to Z$ . A map $G$ from $X$ to the bounded linear operators $\mathcal{L}(X, Z)$ is a slanting function for $F$ in an open set $U$ if for every $x \in U$

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

The derivative is evaluated at the perturbed point $x + h$ , not at $x$ ; this is what lets a nonsmooth map such as $\max(0,\cdot)$ qualify. A sequence $x^k$ converges superlinearly to $x^*$ if $x^k \to x^*$ and for every $\eta > 0$ , eventually $\|x^{k+1} - x^*\| \le \eta\,\|x^k - x^*\|$ .

For (3.1) put $F(y, \lambda) = \bigl(Ay + \lambda - f,\ \lambda - \max(0, \lambda + c(y-\psi))\bigr)$ . For $\delta \in \mathbb{R}^n$ let $G_m(y)$ be the diagonal matrix with entries $0$ where $y_i < 0$ , $1$ where $y_i > 0$ and $\delta_i$ where $y_i = 0$ . The paper's $G_F(x)$ is the block matrix (2.4) obtained by using $G_m$ with $\delta = 0$ for the max-term of $F$ .

Formalization targets

Goal: Theorem 3.1

For a P-matrix $A$ , $c > 0$ and the solution $x^* = (y^*, \lambda^*)$ of (3.1), there is $\rho > 0$ such that every run with $\|x^0 - x^*\| < \rho$ satisfies

x^k \to x^*, \qquad \forall \eta > 0:\ \|x^{k+1} - x^*\| \le \eta\,\|x^k - x^*\| \text{ for all large } k.

The radius depends on the data and the solution, not on the run. The goal speaks about the active set algorithm itself; its identification with a semismooth Newton method is a milestone.

Milestones

Theorem 1.1 (cited from Chen, Nashed and Qi): if $F(x^*) = 0$ , $G$ is a slanting function for $F$ on an open neighbourhood $U$ of $x^*$ , and $G(x)$ is invertible for $x \in U$ with $\{\|G(x)^{-1}\|\}$ bounded, then the Newton iteration $x^{k+1} = x^k - G(x^k)^{-1}F(x^k)$ converges superlinearly to $x^*$ from every $x^0$ close enough to $x^*$ .
Lemma 3.1: $y \mapsto \max(0, y)$ on $\mathbb{R}^n$ is slantly differentiable with slanting function $G_m$ , for every $\delta$ .
§3, p. 7: $F$ is slantly differentiable on $\mathbb{R}^n \times \mathbb{R}^n$ with slanting function $G_F$ .
§2, (2.7)–(2.8): for a P-matrix, every $G_F(x)$ is invertible and the inverses are uniformly bounded.
§2, (2.4)–(2.6): $G_F(x^k)(x^{k+1} - x^k) = -F(x^k)$ holds exactly when $x^{k+1}$ follows $x^k$ by one active set step.

Three companion statements accompany the goal: a run exists from every initial pair; a run that converges to $x^*$ reaches it after finitely many steps (§3, p. 7); and if $y^* < \psi$ and $\lambda^0 + c(y^0 - \psi) \le 0$ , the run equals $x^*$ from the first iterate on (Remark 3.4 (iii)).

Significance

The result. Theorem 3.1 explains why the primal-dual active set strategy converges fast in practice, and it does so through a notion, slant differentiability, that carries over to function spaces, where Clarke's generalized Jacobian is not available. The paper's later sections (missions II–V of this series) use the same framework for global convergence under M-matrix, diagonal-dominance and perturbation hypotheses, and for superlinear convergence in $L^2(\Omega)$ . Theorem 1.1 itself is an abstract local convergence result for nonsmooth Newton methods that applies far beyond complementarity problems.

Formalizing it. The results are proved on paper; none of them is machine-checked. Mathlib has the Fréchet derivative and Newton-type fixed-point arguments, but no slant differentiability, no semismooth Newton method and no theory of the primal-dual active set strategy. A completed mission gives a reusable Lean statement and proof of the Chen–Nashed–Qi theorem in Banach spaces, slant differentiability of the componentwise maximum, and a verified bridge between a combinatorial active set iteration and a Newton iteration.

Difficulty

The map $\max(0, \cdot)$ is not differentiable at $0$ , so the classical Newton convergence theorem does not apply to $F$ . The obvious substitute is a condition with the derivative at the base point, $\|F(x) - F(x-h) - G(x)h\| = o(\|h\|)$ ; the paper notes (p. 3) that with it Theorem 1.1 would need an additional uniformity assumption in $x \in U$ when $X$ is infinite dimensional. Statements and proofs therefore have to work with the derivative at the perturbed point, which is the point at which the Newton iteration evaluates it. A second difficulty is bookkeeping: the identification of the Newton step with the active set step is a block computation over index sets that change with $k$ , and the bound on $\|G_F(x)^{-1}\|$ must hold uniformly over all $2^n$ active sets, using only that principal blocks of a P-matrix are invertible.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and the order is componentwise. Pairs $(y, \lambda)$ live in (Fin n → ℝ) × (Fin n → ℝ) with the max of the two sup norms; in finite dimension every norm gives the same notion of superlinear convergence. Property (A) is stated as a little-o relation, so nothing is divided by $\|h\|$ ; boundedness of $\{G(x)\}$ , required in the original Chen–Nashed–Qi definition, is deliberately not part of it, as in the paper. $F$ and $G$ are total maps; the paper's domain $D \supseteq U$ plays no role.

Standing assumptions: $c > 0$ in every statement; $A$ is a P-matrix wherever the paper uses it (the goal, the inverse bound, the existence of runs, finite termination, Remark 3.4 (iii)), via the published definition RobinsonSR.Schur.IsPMatrix. The solution $(y^*, \lambda^*)$ of (3.1) is a hypothesis; for a P-matrix it exists and is unique, which is a separate classical theorem not restated here. A step of the algorithm is a relation and a run is an infinite sequence of steps; the "Stop" option of the algorithm is not modelled. Nonsingularity in Theorem 1.1 means a two-sided bounded linear inverse, and the Newton iteration is written as the linear equation $G(x^k)(x^{k+1} - x^k) = -F(x^k)$ .

The radius $\rho$ in Theorem 1.1 and Theorem 3.1 is quantified before the sequence; a formalization in which $\rho$ may depend on the run, or in which superlinear convergence drops either the convergence or the rate condition, does not state the theorem. A companion item shows runs exist, so the goal is not vacuous.

Contributions welcome: proofs of Theorem 1.1 in Banach spaces (reusable for missions II–V), of Lemma 3.1, of the block identities, and of the uniform inverse bound over all active sets.

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):865–888, 2002. doi:10.1137/S1052623401383558; authors' version hal-01660511v1.
X. Chen, Z. Nashed, L. Qi, Smoothing methods and semismooth methods for nondifferentiable operator equations, SIAM J. Numer. Anal. 38(4):1200–1216, 2000. doi:10.1137/S0036142999356719
L. Qi, J. Sun, A nonsmooth version of Newton's method, Math. Program. 58:353–367, 1993. doi:10.1007/BF01581275
A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM Classics in Applied Mathematics 9, 1994. doi:10.1137/1.9781611971262

8 thms2 active usersReviewed

Discrete Geometry Harmonic Analysis Probability·Captain: mikedeng1

On Lattices, Learning with Errors, Random Linear Codes, and Cryptography 2: For r ≥ √2·η_ε(L), ε ≤ 1/10, a Discrete Gaussian Sample Lies Outside Any Proper Subspace with Probability ≥ 1/10Research Paper

Motivation

Regev's paper (J. ACM 56(6), Article 34, 2009) introduces the learning with errors (LWE) problem and shows that solving it is at least as hard, for quantum algorithms, as approximating standard worst-case lattice problems such as the shortest independent vectors problem (SIVP) and GapSVP. LWE is the basis of most lattice-based public-key cryptography, including the post-quantum schemes standardized since.

The reduction runs through a sampling problem: produce samples of the discrete Gaussian distribution $D_{L,r}$ on a lattice $L$ . The last step converts such a sampler into a solver for SIVP, which asks for $n$ short linearly independent lattice vectors. That conversion rests on one geometric fact about $D_{L,r}$ , Lemma 3.15 of the paper (p. 34:31): when the width $r$ is at least $\sqrt2$ times the smoothing parameter of $L$ , a sample is not trapped in any proper subspace. The lemma first appeared, with only a proof sketch, in the preliminary version of Micciancio and Regev's work on worst-case to average-case reductions (SIAM J. Comput. 2007); Regev's article gives the full proof. This mission formalizes that lemma. The paper's main theorem, a quantum reduction (Theorem 3.1), is outside this series.

Setting

Work in $\mathbb{R}^n$ , $n \ge 1$ , with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ .

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}\ \forall x \in L\}$ , and $\det(L)$ is the volume of a fundamental domain; $\det(L^*) = 1/\det(L)$ .
The Gaussian function of width $s > 0$ is $\rho_s(x) = \exp(-\pi\|x\|^2/s^2)$ (Eq. (4)); for a countable set $A$ , $\rho_s(A) = \sum_{x \in A}\rho_s(x)$ .
The discrete Gaussian $D_{L,r}$ is the probability distribution on $L$ with mass $D_{L,r}(x) = \rho_r(x)/\rho_r(L)$ (Eq. (6)).
For $\epsilon > 0$ , the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s > 0$ with $\rho_{1/s}(L^* \setminus \{0\}) \le \epsilon$ (Definition 2.10, p. 34:19).
A subspace $H$ is a real linear subspace of $\mathbb{R}^n$ ; "dimension at most $n-1$ " means $H$ is proper.

Formalization targets

Goal: Lemma 3.15 (p. 34:31)

For an $n$ -dimensional lattice $L$ , $0 < \epsilon \le \tfrac1{10}$ , $r \ge \sqrt2\,\eta_\epsilon(L)$ and every subspace $H$ with $\dim H \le n - 1$ ,

\Pr_{x \sim D_{L,r}}[x \notin H] = \sum_{x \in L \setminus H} \frac{\rho_r(x)}{\rho_r(L)} \;\ge\; \frac{1}{10}.

The constants $\sqrt2$ , $\tfrac1{10}$ and $\tfrac1{10}$ are the printed ones.

Milestones, in attack order

Lemma 2.14 (Poisson summation, p. 34:20), already proved on the platform: $f(L) = \det(L^*)\hat f(L^*)$ , with $\hat f(w) = \int f(x)e^{-2\pi i\langle x, w\rangle}dx$ .
The remark after Definition 2.10 (p. 34:19): $s \mapsto \rho_{1/s}(L^* \setminus \{0\})$ is continuous and strictly decreasing on $(0,\infty)$ , tends to $\infty$ at $0$ and to $0$ at $\infty$ , and $\epsilon \mapsto \eta_\epsilon(L)$ is its inverse.
The expectation chain (proof of Lemma 3.15, p. 34:31): for a unit vector $w$ ,

\mathop{\mathrm{Exp}}_{x\sim D_{L,r}}\bigl[e^{-\pi\langle w,x\rangle^2/r^2}\bigr] = \frac{\det(L^*)r^n}{\sqrt2\,\rho_r(L)}\sum_{y\in L^*}e^{-\pi r^2(\|y\|^2 - \langle w,y\rangle^2/2)} \le \frac{\det(L^*)r^n}{\sqrt2\,\rho_r(L)}\rho_{\sqrt2/r}(L^*) \le \frac{\det(L^*)r^n}{\sqrt2\,\rho_r(L)}(1+\epsilon).

The normalization bound (p. 34:31): $\rho_r(L) = \det(L^*)r^n\rho_{1/r}(L^*) \ge \det(L^*)r^n$ for every $r > 0$ .
The conclusion of the proof (p. 34:31): the expectation is at most $\tfrac1{\sqrt2}(1+\epsilon) < 0.9$ .

Significance

The result. Lemma 3.15 gives Corollary 3.16: $n^2$ independent samples of $D_{L,r}$ contain $n$ linearly independent vectors except with exponentially small probability. Since samples of $D_{L,r}$ have norm at most about $\sqrt n\, r$ with high probability, a sampler at width $r \approx \sqrt2\,\eta_\epsilon(L)$ therefore yields short independent vectors, which is how Regev's reduction reaches SIVP (§3.3). The same property is used in later work wherever discrete Gaussian samples must generate a full-rank set of lattice vectors.

Formalizing it. The lemma is proved in the paper; it has no machine-checked proof that we know of. The work this mission asks for is the formalization of the known proof: the Gaussian-sum analysis of a discrete Gaussian on a general lattice in Mathlib's ZLattice framework, built on the platform's proved Poisson summation formula for lattices. The remark after Definition 2.10 (well-definedness of the smoothing parameter) and the normalization bound $\rho_r(L) \ge \det(L^*)r^n$ are used across the whole paper (Lemmas 3.2, 3.12, Claims 3.8, 3.9) and are reusable beyond this mission.

Difficulty

The obvious argument fails at the first step: there is no direct way to bound the mass of $D_{L,r}$ on a hyperplane, because a lattice can place many short vectors in one hyperplane and the normalization $\rho_r(L)$ is not known in closed form. The paper's route replaces the indicator of $H$ by a Gaussian in the direction orthogonal to $H$ and moves to the dual lattice, where the smoothing hypothesis controls the sum. Formally this requires Poisson summation for an anisotropic Gaussian (a Gaussian with a non-scalar covariance), i.e. the Fourier transform of $x \mapsto \exp(-\pi(\|x\|^2 + \langle w,x\rangle^2)/r^2)$ , which is not a stated Mathlib lemma, together with summability of Gaussian sums over lattices and the identification of the dual lattice used by the Poisson formula with the one in the paper. The smoothing remark needs continuity and strict monotonicity of a lattice theta series and its limits at $0$ and $\infty$ .

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure. A lattice is L : Submodule ℤ (EuclideanSpace ℝ (Fin n)) with [DiscreteTopology L] [IsZLattice ℝ L] (discrete, full rank), the same shape as the referenced Poisson summation item. $L^*$ is LinearMap.BilinForm.dualSubmodule (innerₗ _) L; $\det(L^*)$ is written $(\texttt{ZLattice.covolume } L)^{-1}$ .
All Gaussian sums are real tsums over the lattice or its dual; they are summable, so the values are the true sums. $D_{L,r}$ is a mass function on the points of $L$ , and the probability of $x \notin H$ is the sum of the masses of the lattice points outside $H$ .
$\eta_\epsilon(L)$ is the real infimum of $\{s > 0 : \rho_{1/s}(L^* \setminus \{0\}) \le \epsilon\}$ ; that it is attained is milestone 2, not a definitional shortcut.
Added hypotheses, all disclosed in the items: $n \ge 1$ in the goal (at $n = 0$ the natural-number subtraction $n - 1$ is $0$ , the only subspace of dimension $0$ is the whole space $\mathbb{R}^0$ , and the probability is $0$ ); $\epsilon > 0$ (Definition 2.10 is for $\epsilon > 0$ ; for $\epsilon \le 0$ the Lean infimum is over the empty set, equals $0$ , and the hypothesis $r \ge \sqrt2\,\eta_\epsilon(L)$ would be vacuous); $r > 0$ (a Gaussian width; for $n \ge 1$ it follows from the other hypotheses).
Rotation. The proof's "assume without loss of generality that $(1,0,\dots,0)$ is orthogonal to $H$ " is formalized coordinate-free: milestones 3 and 5 are stated for an arbitrary unit vector $w$ , with $x_1$ replaced by $\langle w, x\rangle$ .
Lemma 2.14 is printed "for any function $f$ ", the technical conditions omitted (p. 34:20). The referenced platform item states it for Schwartz functions $f$ , in translated form; every function the proof applies it to is a Gaussian, hence Schwartz.
Not a trivializing formalization: the probability is not stated through a Bochner integral or an unconstrained tsum, the smoothing hypothesis is not vacuous ( $\epsilon > 0$ ), and the goal is the probability bound, not the expectation bound of milestone 3.
Contributions welcome: Fourier transforms of anisotropic Gaussians on EuclideanSpace, summability and monotonicity of lattice theta series, and the smoothing remark, each reusable in the sibling missions of this series.

Selected references

O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
D. Micciancio and O. Regev, Worst-Case to Average-Case Reductions Based on Gaussian Measures, SIAM Journal on Computing 37(1), 2007. https://doi.org/10.1137/S0097539705447360

9 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

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion 1: With Random Objective, the Risk-Averse Minimax Problem Equals the Semidefinite Program (7)Research Paper

Motivation

Two-stage stochastic linear programs choose a first-stage decision $x$ before a random parameter is revealed and a recourse decision $w$ afterwards. The classical model assumes the distribution of the random data is known. In practice it is estimated, and often only its first two moments are trusted. The minimax (distributionally robust) approach hedges against this ambiguity by minimizing the worst-case expected cost over all distributions consistent with the known information; it goes back to Žáčková (1966) and Dupačová (1987). A second concern is risk: a decision maker who is not risk neutral evaluates the random second-stage cost through a nondecreasing convex disutility, not through its mean.

Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) combine both: the distribution of the second-stage data is known only through its mean and second-moment matrix, and the second-stage cost is passed through a piecewise-linear convex disutility. For the case where the randomness is in the objective of the second-stage problem, they show that the resulting minimax problem is exactly a single semidefinite program of polynomial size. This mission formalizes that result, Theorem 2.1 of the paper, and the steps of its proof.

Setting

The first-stage feasible region is $X=\{x\in\mathbb R^n : Ax=b,\ x\ge 0\}$ for $A\in\mathbb R^{m_1\times n}$ , $b\in\mathbb R^{m_1}$ , with first-stage cost vector $c\in\mathbb R^n$ . Given a recourse matrix $W\in\mathbb R^{r\times d}$ , a technology matrix $T\in\mathbb R^{r\times n}$ and $h\in\mathbb R^r$ , the recourse set of $x$ is $X(x)=\{w\in\mathbb R^d : Ww=h-Tx,\ w\ge 0\}$ . For an objective vector $q\in\mathbb R^d$ , the second-stage cost is the value of a linear program,

\mathcal Q(q,x)=\min_{w}\ q'w\quad\text{s.t.}\quad Ww=h-Tx,\ w\ge 0 .

The disutility is $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge 0$ , a nondecreasing convex piecewise-linear function; $K=1$ , $\alpha_1=1$ , $\beta_1=0$ is the risk-neutral case.

The objective $\tilde q$ of the second stage is random, the right-hand side $h$ is constant. The moment class $\mathcal P$ consists of all probability distributions of $\tilde q$ on $\mathbb R^d$ with $\mathbb E_P[\tilde q]=\mu$ and $\mathbb E_P[\tilde q\tilde q']=Q$ . The problem studied is

Z=\min_{x\in X}\Big(c'x+Z(x)\Big),\qquad Z(x)=\sup_{P\in\mathcal P}\mathbb E_P\big[\mathbb U(\mathcal Q(\tilde q,x))\big]. \tag{2}

The inner supremum is an infinite-dimensional linear program over distributions (the paper's (5)). Its dual (6) is the semi-infinite program

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,

over symmetric $Y$ , where $Q\cdot Y=\sum_{i,j}Q_{ij}Y_{ij}$ . The paper's standing assumptions are: $X$ is nonempty and bounded (Assumption 1); complete recourse (Assumption 2); $\{\pi\in\mathbb R^r : W'\pi\le q\}\neq\emptyset$ for all $q$ (Assumption 3); and $Q-\mu\mu'\succ 0$ (Assumption 4).

Formalization targets

Goal: Theorem 2.1

Under the assumptions, with $M_k=\begin{pmatrix}Y&\frac12(y-\alpha_k w_k)\\ \frac12(y-\alpha_k w_k)'&y_0-\beta_k\end{pmatrix}$ ,

Z=Z_{\mathrm{SDP}}=\min_{x,Y,y,y_0,w_k}\ c'x+Q\cdot Y+\mu'y+y_0\ \ \text{s.t.}\ \ M_k\succeq 0,\ Ww_k+Tx=h,\ w_k\ge0\ (k=1,\dots,K),\ Ax=b,\ x\ge 0, \tag{7}

and, for every $x\in X$ , $Z(x)$ equals the value of the program (8) obtained from (7) by fixing $x$ . The Lean goal also asserts that both $Z$ and $Z_{\mathrm{SDP}}$ are genuine greatest lower bounds of their sets of objective values.

Milestones, in the order the proof uses them

Weak duality $Z(x)\le Z_D(x)$ (§2.1, p. 583).
Strong duality $Z(x)=Z_D(x)$ under Assumption 4 (§2.1, p. 583, citing Isii).
Any $(Y,y,y_0)$ satisfying the $k$ -th constraint $(\mathcal C_k)$ of (6) has $Y\succeq 0$ .
Under Assumption 3, $X(x)$ is bounded and convex.
The minimax exchange $\inf_q\max_{w\in X(x)}=\max_{w\in X(x)}\inf_q$ for $q'Yq+q'y+y_0-\alpha_kq'w-\beta_k$ .
$(\mathcal C_k)$ holds iff a single $w_k\in X(x)$ satisfies the inequality for every $q$ .
The matrix inequality form: a quadratic $[q;1]'M[q;1]$ is nonnegative for all $q$ iff $M\succeq 0$ (a published, proved theorem, referenced).
The dual (6) and the semidefinite program (8) have the same objective values (p. 584).

Significance

Theorem 2.1 turns a minimax problem over an infinite-dimensional set of distributions, with a nonlinear risk measure applied to an LP value function, into one semidefinite program whose size is polynomial in $n$ , $d$ , $r$ and $K$ . Off-the-shelf interior-point solvers then compute the risk-averse minimax decision, and the dual of (8) yields an explicit worst-case distribution (Theorem 2.2, formalized in the companion mission). The paper contrasts this with Delage and Ye's ellipsoid-method result, which covers a larger class of functions but gives no single compact program, and with the random right-hand-side case, which it shows to be NP-hard.

The result is proved in the paper; nothing here is open mathematics. As far as a search of the platform shows, none of it is formalized: no moment-problem duality theorem, no reformulation of a distributionally robust two-stage program, and no instance of the S-lemma-type step " $\forall q\ \exists w$ becomes $\exists w\ \forall q$ " exist in machine-checked form. A complete development would provide the moment-problem strong duality for a specific continuous integrand with linear growth, which other distributionally robust optimization results reuse.

Difficulty

The obvious argument dualizes the moment problem and then substitutes the formula for $\mathcal Q$ . Two steps resist this. First, strong duality for the moment problem is not a finite-dimensional LP fact: it needs the moment vector $(\mu,Q)$ to lie in the interior of the moment cone, and passing from that to "no duality gap" requires a separation argument in an infinite-dimensional space together with integrability of the integrand under every distribution with finite second moments. Second, constraint (6) is a "for every $q$ there is a $w$ " statement, because $\mathcal Q(q,x)$ is a minimum over $w$ . Replacing it with one $w_k$ that works for all $q$ is not a formal manipulation: it needs $Y\succeq 0$ , which is not a constraint of (6) but a consequence of it, then a minimax theorem with the compact side $X(x)$ , then attainment of the outer maximum. Both the boundedness of $X(x)$ and the convexity in $q$ are derived, not assumed.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ; indices $k$ run over Fin K with $K\ge 1$ . The paper's letter $p$ denotes both the dimension of $q$ and the LP dual vector; here the dimension is $d$ and dual vectors are $\pi$ . Distributions are probability measures with square-integrable coordinates (the platform's MomentDRO.Conf moment objects), not the densities written in (5). Every printed min/max is a real infimum/supremum of the set of objective values; attainment is not claimed except where a statement says so. $\mathcal Q(q,x)$ is a real infimum and is only used where $X(x)\neq\emptyset$ and Assumption 3 hold, which make it finite. Positive semidefiniteness is Matrix.PosSemidef on matrices indexed by Fin d ⊕ Fin 1. The minimax exchange is stated in EReal, since $\inf_q$ can be $-\infty$ .

As printed, Assumptions 2 and 3 contradict each other whenever $r\ge1$ : complete recourse produces a nonzero $u\ge0$ with $Wu=0$ , and Assumption 3 at $q=-u$ is then infeasible. A statement assuming both would be vacuous. The formalization therefore uses what the proof of Theorem 2.1 uses: Assumption 3 for all $q$ , and $X(x)\neq\emptyset$ for every $x\in X$ in place of Assumption 2. The hypotheses of the goal are satisfiable (e.g. $W=1$ , $T=0$ , $h=0$ , $X=\{0\}$ , $\mu=0$ , $Q=1$ ). Program (7) is defined as one joint program over $(x,Y,y,y_0,w_1,\dots,w_K)$ , never through $Z_D(x)$ , so the goal is not strong duality plus unfolding.

Needed infrastructure: integrability of LP value functions under second-moment distributions, the moment-problem strong duality, Sion's minimax theorem (available in Mathlib and on the platform), and the bordered-matrix characterization of nonnegative quadratics (already proved on the platform). Proofs of any milestone, and reusable lemmas about LP value functions, are welcome.

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
K. Isii, On the sharpness of Chebyshev-type inequalities, Annals of the Institute of Statistical Mathematics, 185–197, 1963 (reference [15] of the paper; volume as printed there). https://doi.org/10.1287/moor.1100.0445
M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
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
J. Dupačová, The minimax approach to stochastic programming and an illustrative application, Stochastics 20(1):73–88, 1987. https://doi.org/10.1080/17442508708833436

12 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

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

Dynamical Systems Operations Research Stochastic Systems+1·Captain: mikedeng1

The Power of Two Choices in Randomized Load Balancing I: In the Limiting Supermarket System the Expected Time Converges to T_d(λ) = Σ λ^((d^i−d)/(d−1))Research Paper

Motivation

Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at $n$ servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is $1/(1-\lambda)$ at load $\lambda$ . With two choices it is exponentially smaller as $\lambda \to 1^-$ . This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.

Timeline:

1994/1999. Azar, Broder, Karlin and Upfal proved the static version, balanced allocations: throwing $n$ balls into $n$ bins with $d \ge 2$ choices per ball gives a maximum load of $\log\log n/\log d + O(1)$ w.h.p., against $\Theta(\log n/\log\log n)$ for one choice (SIAM J. Comput. 1999).
1996. Vvedenskaya, Dobrushin and Karpelevich derived the dynamic limiting equations for $d = 2$ and showed convergence of their trajectories to the fixed point, without a rate (Problems of Information Transmission 32(1), 1996).
1996/2001. Mitzenmacher, independently, introduced the limiting system for general $d$ , proved doubly exponential tails along every trajectory and exponential convergence to the fixed point in a weighted $L_1$ potential, and derived the limiting expected time $T_d(\lambda)$ (IEEE TPDS 2001). This mission formalizes Section 2 of that paper.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$ , $0<\lambda<1$ , at $n$ FIFO servers. Each customer chooses $d$ servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean $1$ . Let $s_i(t)$ be the fraction of servers holding at least $i$ customers at time $t$ .

A state is a sequence $s = (s_0, s_1, s_2, \dots)$ of reals with $s_0 = 1$ , $s_i \ge 0$ and $s_0 \ge s_1 \ge s_2 \ge \cdots$ . The empty state has $s_0 = 1$ and $s_i = 0$ for $i \ge 1$ . As $n \to \infty$ the tails follow the limiting system

\frac{ds_i}{dt} = \lambda\,(s_{i-1}^d - s_i^d) - (s_i - s_{i+1}) \quad (i \ge 1), \qquad s_0 = 1. \tag{1}

A trajectory is a map $t \mapsto s(t)$ , $t \ge 0$ , whose values are states and whose coordinates satisfy (1) (from the right at $t = 0$ ). Throughout, $d \ge 2$ is an integer.

The fixed point is $\pi_i = \lambda^{(d^i - 1)/(d - 1)}$ , so $\pi_0 = 1$ , $\pi_1 = \lambda$ , $\pi_2 = \lambda^{1+d}$ . A customer arriving in state $s$ becomes the $i$ -th customer of its queue with probability $s_{i-1}^d - s_i^d$ and then waits for $i$ services, so the expected time it spends in the system is

E(s) = \sum_{i=1}^{\infty} i\,(s_{i-1}^d - s_i^d).

The target constant is

T_d(\lambda) = \sum_{i=1}^{\infty} \lambda^{\frac{d^i - d}{d-1}}.

Formalization targets

Goal: Corollary 2

For $d \ge 2$ and $0 < \lambda < 1$ , $T_d(\lambda) < \infty$ , and:

\text{if } s_j(0) = 0 \text{ for some } j, \text{ then } E(s(t)) \xrightarrow[t\to\infty]{} T_d(\lambda);\qquad \text{if } s(0) \text{ is empty, then } E(s(t)) \le T_d(\lambda) \ \ \forall t \ge 0.

The hypothesis $s_j(0) = 0$ holds for every initial state that comes from a finite system.

Milestones, in the order the proof uses them

Lemma 2. $\pi$ is the unique fixed point of (1) with $\sum_{i\ge1} s_i < \infty$ .
Theorem 2. If $s_j(0) = 0$ for some $j$ , there are constants $N \ge 1$ , $0<\alpha<1$ , $\beta>1$ , $\gamma>0$ , independent of $t$ , with $s_i(t) \le \gamma\,\alpha^{\beta^i}$ for all $i \ge N$ , $t \ge 0$ . From the empty state, $s_i(t) \le \pi_i$ for all $i$ and $t \ge 0$ .
Theorem 3. There are weights $w_i \ge 1$ such that $\Phi(t) = \sum_{i\ge1} w_i |s_i(t) - \pi_i|$ satisfies $\Phi(t) \le c_0 e^{-\delta t}$ ( $\delta > 0$ ) whenever $\Phi(0) < \infty$ , and in particular whenever $s_j(0) = 0$ for some $j$ .
Corollary 1. Under the conditions of Theorem 3 (weights $w_i \ge 1$ fixed before the trajectory, with $\Phi(0) < \infty$ , or $s_j(0) = 0$ for some $j$ ), $\sum_{i\ge1} |s_i(t) - \pi_i| \le c_0 e^{-\delta t}$ .
Proof of Corollary 2, display. $\sum_{i\ge1} i(s_{i-1}^d - s_i^d) = \sum_{i\ge0} s_i^d$ for a state with $s_i \to 0$ .
Lemma 4. The drift of (1) is Lipschitz in $\ell^1$ on states, with constant $2 + 2d\lambda$ .

Significance

The comparison $T_1(\lambda) = 1/(1-\lambda)$ against $T_d(\lambda)$ is the quantitative content of the power of two choices: the companion mission shows $T_d(\lambda)/\log T_1(\lambda) \to 1/\log d$ as $\lambda \to 1^-$ , an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.

All results are proved in the paper (Theorem 3's proof is written out for $d = 2$ with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all $d \ge 2$ , including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of $|\epsilon_i|$ in Theorem 3.

Difficulty

The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for $\ell^\infty$ -bounded countable systems. The plain $L_1$ distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights $w_i$ must be built so that every coordinate's contribution to $d\Phi/dt$ is dominated by $-\delta w_i |\epsilon_i|$ , while staying geometrically bounded so that $\Phi(0) < \infty$ under the doubly exponential tails of Theorem 2. Exchanging $t \to \infty$ with the infinite sum defining $E$ needs uniform tail control, which is again Theorem 2.

Formalization scope

Namespace PowerTwoChoices.Limit; λ is lam : ℝ, $d : ℕ$ with $2 \le d$ , $0 < \lambda < 1$ in every theorem.
A state is x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every $t \ge 0$ , with HasDerivWithinAt on Set.Ici 0 for each coordinate $i \ge 1$ : right derivative at $t = 0$ , two-sided for $t > 0$ .
Exponents are natural numbers: $\pi_i = \lambda^{\sum_{k<i} d^k}$ , and $T_d$ 's $i$ -th term is $\lambda^{\sum_{1\le k<i} d^k}$ .
$\Phi$ , the $L_1$ distance, $E$ and $T_d$ are sums in $[0,\infty]$ , so a divergent series is $\infty$ , never a default $0$ . "Converges exponentially" (Definition 2) means $\Phi(t) \le c_0 e^{-\delta t}$ for all $t \ge 0$ with real $c_0$ and $\delta > 0$ ; $\delta$ may depend on the trajectory. The paper's $d(t)$ is renamed l1Dist.
Time is real and $t \to \infty$ is Filter.atTop.
Every theorem quantifies over trajectories; existence of a trajectory from a given state (Picard iteration, cited by the paper) is not part of the mission. The class is nonempty: the constant trajectory at $\pi$ is one.
Ruled out: summing $E$ or $T_d$ as a real tsum (a divergent series would make the upper bound free and the limit attainable by a junk $0$ ), dropping the summability condition in Lemma 2 ( $(1,1,\dots)$ is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for $d = 2$ only.
Needed infrastructure: comparison principles for quasimonotone countable ODE systems, Dini-derivative Grönwall estimates, and interchange of limits and $\ell^1$ sums. All of these are reusable beyond this mission, and contributions of such lemmas as separate theorems are welcome.

Selected references

M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490
N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing System with Selection of the Shortest of Two Queues: An Asymptotic Approach, Problems of Information Transmission 32(1), 1996, pp. 15–27.
T. G. Kurtz, Approximation of Population Processes, SIAM, 1981. https://doi.org/10.1137/1.9781611970333

8 thms2 active usersReviewed

Harmonic Analysis Probability Theoretical Computer Science·Captain: mikedeng1

On Lattices, Learning with Errors, Random Linear Codes, and Cryptography 1: A Discrete Gaussian on L + u Plus Continuous Gaussian Noise ν_s Is Within Statistical Distance 4ε of ν_t, t = √(r² + s²)Research Paper

Motivation

The learning with errors (LWE) problem underlies most of post-quantum public-key cryptography. Its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). The reduction is iterative: it repeatedly turns samples of a discrete Gaussian on a lattice into samples of a narrower one. Its classical step, Lemma 3.11, needs the following fact. Adding continuous Gaussian noise to a discrete Gaussian sample gives, up to a small statistical distance, a continuous Gaussian. That fact is Claim 3.9 of the paper. Through Corollary 3.10 it turns a lattice point plus noise into an LWE-type sample with a periodic Gaussian error.

The tool behind it is the smoothing parameter of Micciancio and Regev (SIAM J. Comput. 2007). Above this width a discrete Gaussian on a lattice behaves like a continuous one. Claims of this type have since become standard in lattice-based cryptography: discrete Gaussian sampling, trapdoors, and the convolution theorems of Peikert (CRYPTO 2010).

This mission formalizes Claim 3.9 from the published J. ACM article (Article 34, 2009). 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$ with the Euclidean norm and Lebesgue measure. For $s > 0$ the Gaussian function is $\rho_s(x) = \exp(-\pi\|x/s\|^2)$ , its shift is $\rho_{s,c}(x) = \rho_s(x - c)$ , and $\nu_s = \rho_s/s^n$ is a probability density (Eqs. (4)–(5)). For a countable set $A$ , $\rho_s(A) = \sum_{x \in A}\rho_s(x)$ .

A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is $L^* = \{y : \langle x, y\rangle \in \mathbb{Z}\ \forall x \in L\}$ , and $\det(L^*) = 1/\det(L)$ , where $\det(L)$ is the volume of a fundamental parallelepiped. For $u \in \mathbb{R}^n$ and $r > 0$ , the discrete Gaussian $D_{L+u,r}$ is the distribution on the coset $L + u$ with mass $\rho_r(y)/\rho_r(L+u)$ at $y$ (Eq. (6)).

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

The statistical distance of two densities is $\Delta(\varphi_1,\varphi_2) = \int_{\mathbb{R}^n}|\varphi_1 - \varphi_2|$ , with no factor $\tfrac12$ , so it ranges in $[0,2]$ .

Let $r, s > 0$ and $t = \sqrt{r^2+s^2}$ . The distribution $Y$ is obtained by sampling $y \sim D_{L+u,r}$ and adding independent noise with density $\nu_s$ . Its density is

Y(x) = \sum_{y \in L+u} D_{L+u,r}(y)\,\nu_s(x - y).

Formalization targets

Goal: Claim 3.9 (p. 34:25)

If $rs/t \ge \eta_\epsilon(L)$ for some $0 < \epsilon < \tfrac12$ , then

\Delta(Y, \nu_t) \le 4\epsilon .

Milestones, in attack order

Lemma 2.14 (Poisson summation), already proved on the platform and used here as a reference: $f(L) = \det(L^*)\hat f(L^*)$ .
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)$ , with limits $\infty$ at $0$ and $0$ at $\infty$ , and $\eta_\epsilon(L)$ is its inverse.
The Fourier transform of a shifted Gaussian (p. 34:25), $\widehat{\rho_{\sigma,c}}(w) = e^{-2\pi i\langle c,w\rangle}\sigma^n\rho_{1/\sigma}(w)$ .
Claim 3.8 (p. 34:24). If $r \ge \eta_\epsilon(L)$ , then $\rho_r(L+c) \in r^n\det(L^*)(1\pm\epsilon)$ .
Eq. (11) (p. 34:25), $Y(x) = s^{-n}\rho_t(x)\,\rho_{rs/t,(r/t)^2x-u}(L)/\rho_{r,-u}(L)$ .
The pointwise bound (p. 34:26), $|Y(x) - \rho_t(x)/t^n| \le \rho_t(x)/t^n\cdot 4\epsilon$ .

A supporting item states the bridge used in both proofs: if $s \ge \eta_\epsilon(L)$ , then $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ .

Significance

Claim 3.9 is what makes Regev's iterative step classical. A discrete Gaussian sample, blurred by continuous noise, cannot be told apart from a continuous Gaussian of the combined width, except with probability $2\epsilon$ . Corollary 3.10 projects this onto a direction $z$ and reduces it modulo 1 to obtain LWE samples with periodic Gaussian error $\Psi_\beta$ . Without it, the reduction from lattice problems to LWE has no way to produce its error distribution. Claim 3.8, a milestone here, says that above the smoothing parameter the discrete Gaussian measure is almost invariant under shifts. It is the basic estimate of the theory.

The results are proved in the paper; none of them is formalized. Lean's Mathlib has lattices, their covolume, dual submodules and the Gaussian Fourier transform. The platform has the Poisson summation formula for lattices. This mission adds the smoothing parameter, discrete Gaussians on cosets, and the first machine-checked convolution theorem for discrete and continuous Gaussians. Later work, such as Corollary 3.10 or Peikert's general convolution theorem, can build on it.

Difficulty

Neither density is a finite object. $Y$ is an infinite sum over a coset of a lattice, normalized by another infinite sum. A direct term-by-term comparison of $Y(x)$ with $\nu_t(x)$ fails: the sum defining $Y(x)$ is a Gaussian sum over a shifted lattice, and its value genuinely varies with the position of $(r/t)^2x - u$ relative to $L$ ; for narrow Gaussians the variation is of order one. The claim is that this oscillation is uniformly small, with a relative error that depends only on $\epsilon$ , not on $n$ , $x$ or $u$ . Two ratios of lattice sums must be bounded at once, uniformly in $x$ . The constant $4\epsilon$ uses $\epsilon < \tfrac12$ in an essential way, because $(1+\epsilon)/(1-\epsilon)$ must stay below $1+4\epsilon$ .

The smoothing parameter is defined as a least element. That the least element exists, i.e. that the infimum is attained, is itself a statement about continuity and strict monotonicity of an infinite sum in its width.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n).
A lattice is a Submodule ℤ with [DiscreteTopology L] [IsZLattice ℝ L].
$L^*$ is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.
$\det(L^*)$ is written $\det(L)^{-1}$ with $\det(L)$ = ZLattice.covolume L.
Lattice sums are real tsums. They are genuinely summable, so no summability hypothesis is added.
$\eta_\epsilon(L)$ is the real infimum of $\{s > 0 : \rho_{1/s}(L^*\setminus\{0\}) \le \epsilon\}$ . Its attainment is milestone 2, not part of the definition.
$Y$ is defined by its density, the formula on the first line of the proof.
$\Delta$ is a lower Lebesgue integral with values in $[0,\infty]$ and no $\tfrac12$ . A Bochner integral of a non-integrable difference would be $0$ and make the bound free; this form rules that trivialization out.

Added hypotheses, each disclosed in the item.

$\epsilon > 0$ in Claim 3.9 and the pointwise bound (Claim 3.8 prints it). Definition 2.10 defines $\eta_\epsilon$ only for $\epsilon > 0$ , and for $\epsilon \le 0$ the defining set is empty, so the hypothesis $\eta_\epsilon(L) \le rs/t$ would be vacuous.
$r > 0$ in Claim 3.8, where $\rho_r$ requires it, and likewise $s > 0$ in the supporting item " $s \ge \eta_\epsilon(L) \Rightarrow \rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ ".
$n \ge 1$ in the smoothing remark, which fails for $n = 0$ , where $L^*\setminus\{0\}$ is empty.

Other conventions.

Lemma 2.14 is printed "for any function", with technical conditions omitted (p. 34:20). The referenced platform theorem is the version for Schwartz functions in translated form; every Gaussian used here is Schwartz.
Eq. (11) is formalized as the equality of its first and fifth lines, the real-valued completing-the-square identity. The Fourier-side lines are not stated.
The Fourier transform is Mathlib's 𝓕, $\int h(x)e^{-2\pi i\langle x,w\rangle}dx$ , as on p. 34:20.

Reusable beyond this mission: the Gaussian, coset-sum and smoothing-parameter definitions, Claim 3.8, and the shifted Fourier transform. Proofs of any milestone are welcome, and so are proofs of the summability and Schwartz facts for Gaussians on lattices that every milestone needs.

Selected references

O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
D. Micciancio and O. Regev, Worst-Case to Average-Case Reductions Based on Gaussian Measures, SIAM Journal on Computing 37(1), 2007. https://doi.org/10.1137/S0097539705447360
C. Peikert, An Efficient and Parallel Gaussian Sampler for Lattices, CRYPTO 2010, LNCS 6223. https://doi.org/10.1007/978-3-642-14623-7_5

9 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Revenue Management Without Forecasting or Optimization: An Adaptive Algorithm for Determining Airline Seat Protection Levels: Fill-Event Updates Converge to the Optimal Protection LevelsResearch Paper

Motivation

Airlines sell seats on a single flight in several fare classes. Discount classes book first, so the carrier must decide how many seats to protect for later, higher-paying passengers. The classical answer, from Littlewood's rule for two classes to the nested optimality conditions of Brumelle and McGill (1993), computes optimal protection levels from a forecast of the demand distribution of each class. Those forecasts must be built from censored booking data, which is where most of the practical difficulty lies.

van Ryzin and McGill (2000) observed that the optimality conditions themselves can drive an adaptive rule. After each flight one only records whether a fill event occurred (whether demand reached each protection level) and moves the levels by a stochastic-approximation step. No forecast and no optimization is needed. Their Theorem 1 asserts that this rule converges almost surely to the optimal protection levels, with an explicit mean-square rate. It is one of the standard references for model-free revenue management. The convergence proof combines Robbins–Monro theory, the Robbins–Siegmund supermartingale lemma and an induction over fare classes.

Setting

There are $k+1$ fare classes with fares $f_1 > f_2 > \cdots > f_{k+1} > 0$ and discount ratios $r_{i+1} = f_{i+1}/f_1$ . On a flight the class demands $X_1, \dots, X_{k+1}$ are independent, nonnegative and continuously distributed. Successive flights $X^1, X^2, \dots$ are independent with the same law.

A protection vector is $\theta = (\theta_1, \dots, \theta_k)$ . The fill events are

A_i(\theta, X) = \{X_1 > \theta_1,\ X_1 + X_2 > \theta_2,\ \dots,\ X_1 + \cdots + X_i > \theta_i\}, \qquad i = 1, \dots, k.

A vector $\theta^*$ is characterised by the optimality condition (3), $P(A_i(\theta^*, X)) = r_{i+1}$ for $i = 1, \dots, k$ . The adjustments are $H_i(\theta, X) = r_{i+1} - \mathbf 1(A_i(\theta, X))$ , and their means are $h_i(\theta) = r_{i+1} - P(A_i(\theta, X))$ . From an arbitrary $\theta^1$ the algorithm updates

\theta^{n+1} = \theta^n - \gamma_n H(\theta^n, X^n), \qquad \gamma_n = \frac{A}{n + B},\ A > 0,\ B \ge 0.

The interim protection levels $p_i(\theta) = \max\{\theta_j : 1 \le j \le i\}$ are what the airline actually uses to control bookings. The updates themselves monitor $A_i(\theta^n, X^n)$ .

Formalization targets

Goal: Theorem 1 (p. 765)

Assume:

A1: every $X_i$ has bounded support.
A2 (windowed): for each $R > 0$ there is $\delta_R > 0$ with $(\theta_i - \theta^*_i)\,h_i(\theta_i, \theta^*_{i-1}, \dots, \theta^*_1) \ge \delta_R|\theta_i - \theta^*_i|^2$ whenever $|\theta_i - \theta^*_i| \le R$ .
A3: the distribution functions of the partial sums $X_1 + \cdots + X_i$ are Lipschitz.

Then for $i = 1, \dots, k$ ,

\theta^n_i \to \theta^*_i \ \text{a.s.}, \qquad p_i(\theta^*) = \theta^*_i,

and there are $\beta > 0$ and $C$ with

E|\theta^n_i - \theta^*_i|^2 \le C\,\gamma_n^{\beta/2^{i-1}}.

The exponent is left existential, as in the paper, so any improvement of the rate constant still proves the goal.

Milestones

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

the base case $i = 1$ (p. 765);
the Lipschitz bound on $h_{i+1}$ (p. 766);
Lemma 3, boundedness of the iterates (p. 764);
the almost-supermartingale inequality (12) (p. 766);
Lemma 1 (p. 764);
the a.s. summability of $\gamma_n|\theta^n_i - \theta^*_i|$ (p. 766);
Lemma 2, Robbins–Siegmund (p. 764);
the induction step for (9) (p. 766);
Lemma 4, the rate recursion (p. 764).

Significance

Theorem 1 says that the nested optimality conditions of Brumelle and McGill can be reached by observing binary fill events alone. It also says that the limit is automatically ordered, $\theta^*_1 \le \cdots \le \theta^*_k$ , so the interim levels coincide with the limit. The algorithm is distribution-free and needs neither demand forecasts nor uncensoring, which is why it is used in practice and as a baseline for later data-driven and learning-based revenue management.

The theorem is proved in the paper. As far as is known it has no machine-checked proof. Formalizing it requires a vector Robbins–Monro argument with coupled coordinates, the Robbins–Siegmund lemma, and an explicit polynomial rate. Two of the milestones are general probability facts reusable far beyond this mission: Lemma 1, and Robbins–Siegmund, which no platform item states yet. The formalization also corrects the record on two printed slips, described under Formalization scope.

Difficulty

Coordinate $i+1$ is not a Robbins–Monro process by itself. Its fill event $A_{i+1}(\theta, X)$ depends on all of $\theta_1, \dots, \theta_{i+1}$ , so the drift of $\theta^n_{i+1}$ is perturbed by the errors of the lower coordinates. Applying a scalar convergence theorem coordinate by coordinate fails at this point. The perturbation has to be bounded via the Lipschitz assumption A3 and shown to be summable along the path, which uses the mean-square rate already established for class $i$ . The rate and the almost-sure convergence must therefore be carried through the induction together. The exponent halves at each class. A second difficulty is that A2 is only usable on a bounded set, so boundedness of the iterates (Lemma 3) has to come first and must be uniform.

Formalization scope

Classes are indexed from $1$ in Lean ( $\mathbb N$ -indexed vectors whose index $0$ and indices above $k+1$ are never read). A flight's demand vector has the product law $\bigotimes_i \nu_i$ , and the sample path has the countable product of copies of it. Lean's iterate … n is the paper's $\theta^{n+1}$ , so the rate pairs it with $\gamma_{n+1}$ . Continuity of a demand law is "every singleton is null". Expectations are Bochner integrals, and integrability is part of each rate conclusion. The fill event reuses the published NestedSeatAlloc.ProbCond.nestEvent.

Pinned and corrected statements:

A2 as printed is unsatisfiable. It asks for one $\delta$ valid for all $\theta_i$ . Since $|h_i| \le 1$ , the inequality fails once $|\theta_i - \theta^*_i| > 1/\delta$ , so the printed Theorem 1 is vacuously true. The mission uses the windowed A2 above. That is what the proof applies to bounded iterates, and what the paper's sufficient condition (a density bounded below near $\theta^*$ ) yields. A formalization with the printed A2, or with any other hypothesis no instance satisfies, is ruled out.
The base case. The page claims the rate "for all $0 < \beta < 1$ ". That is false in general. The milestone states "for some $\beta > 0$ ", which is all Theorem 1 uses.
Integrability. Lemma 2 assumes each $Z_n$ integrable, so that the conditional expectation is genuine. Lemma 3's "bounded (a.s.)" is read as a bound uniform in $n$ .
Standing assumptions. Nonnegative demands and positive fares are added where the argument uses them.

Not posed: §4's modifications (projection onto the capacity, randomized integer levels, booking lead times) and the simulations of §5.

Contributions welcome: proofs of the general lemmas (Lemma 1, Robbins–Siegmund) stated for arbitrary probability spaces, measurability facts for the recursion, and the elementary Lemma 4.

Selected references

G. van Ryzin and J. McGill, Revenue Management Without Forecasting or Optimization: An Adaptive Algorithm for Determining Airline Seat Protection Levels, Management Science 46(6), 760–775, 2000. https://doi.org/10.1287/mnsc.46.6.760.11936
S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1), 127–137, 1993. https://doi.org/10.1287/opre.41.1.127
H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
A. Benveniste, M. Métivier and P. Priouret, Adaptive Algorithms and Stochastic Approximations, Springer, 1990. https://doi.org/10.1007/978-3-642-75894-2
E. Lukacs, Stochastic Convergence, 2nd ed., Academic Press, 1975.

12 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Quantitative Stability in Stochastic Programming: The Method of Probability Metrics 4: Minimal-Risk Stable Portfolios Are Stable in the Stability Index and the Spectral MeasureResearch Paper

Motivation

Stable distributions were proposed as models of asset returns by Mandelbrot and Fama in the 1960s, because empirical returns show heavier tails than the normal law allows; Rachev and Mittnik's monograph Stable Paretian Models in Finance (2000) collects the later development. When the vector $\varrho$ of per-share returns of $s$ assets follows a multivariate $\alpha$ -stable law with $\alpha\in(1,2)$ , its distribution is determined by the stability index $\alpha$ , a shift $m_0\in\mathbb R^s$ , and a finite Borel measure $\Gamma$ on the unit sphere, the spectral measure. The risk of a portfolio is then measured by the scale parameter of the return, and choosing an efficient portfolio becomes a deterministic optimization problem in $(\alpha,\Gamma)$ .

In practice neither $\alpha$ nor $\Gamma$ is known: both are estimated from data. Whether the optimal portfolio is robust to estimation error is therefore a practical question. Section 5 of Rachev and Römisch, Quantitative stability in stochastic programming: The method of probability metrics (Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint), answers it with an explicit modulus, as an application of the paper's general stability theory for stochastic programs under perturbations of the underlying probability measure.

Setting

Fix $s\in\mathbb N$ and equip $\mathbb R^s$ with the Euclidean scalar product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ .

$\Sigma^s=\{\xi\in\mathbb R^s:\langle\xi,\xi\rangle=1\}$ is the unit sphere, and $\mathcal P(\Sigma^s)$ is the set of Borel probability measures on it (normalized spectral measures).
$X=\{x\in\mathbb R^s_+:\sum_{i=1}^s x_i=1\}$ is the set of portfolios: $x_i$ is the proportion of shares held in asset $i$ .
For $\alpha\in(1,2)$ and $\Gamma\in\mathcal P(\Sigma^s)$ , the risk of $x$ is

r_{\alpha,\Gamma}(x)=\int_{\Sigma^s}|\langle x,\xi\rangle|^\alpha\,\Gamma(d\xi).

Problem (22) is $\min\{r_{\alpha,\Gamma}(x):x\in X\}$ , with optimal value $v(\alpha,\Gamma)$ and solution set $S(\alpha,\Gamma)$ .
The dual Lipschitz metric $\zeta_1$ (the Fortet–Mourier metric of order $1$ ) on $\mathcal P(\Sigma^s)$ is

\zeta_1(\Gamma,\tilde\Gamma)=\sup\Big\{\Big|\int_{\Sigma^s}f\,d\Gamma-\int_{\Sigma^s}f\,d\tilde\Gamma\Big|: f:\Sigma^s\to\mathbb R,\ |f(\xi)-f(\tilde\xi)|\le\|\xi-\tilde\xi\|\Big\}.

The growth function of (22) is $\psi(\tau)=\min\{r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma): d(x,S(\alpha,\Gamma))\ge\tau,\ x\in X\}$ for $\tau\ge0$ , its generalized inverse is $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$ , and the stability modulus is $\Psi(\eta)=\eta+\psi^{-1}(2\eta)$ .
$\Gamma$ is nonsingular if $\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)=0$ implies $x=0$ .

Formalization targets

Goal: Theorem 5.2, first assertion (p. 25)

For each $(\alpha,\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ there is $\delta>0$ such that

\sup_{x\in S(\tilde\alpha,\tilde\Gamma)}d\big(x,S(\alpha,\Gamma)\big)\le\Psi\big(\alpha\,\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|\big)

whenever $(\tilde\alpha,\tilde\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ and $\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|<\delta$ . The modulus $\Psi$ is not fixed: it is whatever the growth of the unperturbed problem gives.

Companion: Theorem 5.2, "Moreover" (p. 25)

If $\Gamma$ is nonsingular, then (22) has a unique solution and $\Psi(\eta)\le C\eta^{1/2}$ for some $C>0$ and all sufficiently small $\eta\ge0$ .

Milestones

Lemma 5.1, first assertion (p. 24): $f_0(\xi,x)=|\langle x,\xi\rangle|^\alpha$ is convex in $x$ , and $|f_0(\xi,x)-f_0(\tilde\xi,\tilde x)|\le\alpha(\|\xi-\tilde\xi\|+\|x-\tilde x\|)$ on $\Sigma^s\times X$ .
Lemma 5.1, second assertion (p. 24): $S(\alpha,\Gamma)\ne\emptyset$ , and $\frac14\alpha(\alpha-1)\int_{\Sigma^s}|\langle x-x_*,z\rangle|^2\Gamma(dz)\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ for all $x\in X$ and some $x_*\in S(\alpha,\Gamma)$ .
Proof of Theorem 5.2 (p. 25): $\sup_{t\in[-1,1]}\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$ .
Proof of Theorem 5.2 (p. 25): $|r_{\alpha,\Gamma}(x)-r_{\tilde\alpha,\tilde\Gamma}(x)|\le\alpha\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|$ for $x\in X$ .
Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$ , $c\|x\|^2\le\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)$ for some $c=c(s,\Gamma)>0$ .
Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$ , (22) has a unique solution $x_*$ and $\frac14c\alpha(\alpha-1)\|x-x_*\|^2\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ on $X$ .

Significance

The theorem bounds how far the optimal portfolios can move when the stability index and the spectral measure are both perturbed, with a modulus computed from the unperturbed problem alone. Combined with the companion, the efficient portfolio of a nonsingular spectral measure is unique and moves by at most $O\big((\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|)^{1/2}\big)$ . Since $\zeta_1$ metrizes weak convergence on the compact sphere, any consistent estimator of $\Gamma$ in the weak topology, together with a consistent estimator of $\alpha$ , yields consistent estimates of the optimal portfolio, and convergence rates for $\zeta_1$ translate into rates for the portfolio. The paper notes (Example 5.3) that spectral measures of linear transformations of independent stable variables with a full-rank matrix are nonsingular, so the Hölder case covers the discrete spectral measures used in practice.

The result is proved in the paper; nothing here is open. To our knowledge none of it is machine-checked: Mathlib has strong convexity and the real power function but no stability theory of stochastic programs and no Fortet–Mourier metrics. The mission produces a checked proof of the result and a reusable formal treatment of the growth-function modulus $\Psi$ in a concrete, fully explicit instance.

Difficulty

The obvious argument compares the optimal values of the two problems and concludes that a perturbed minimizer is nearly optimal for the unperturbed problem. Turning near-optimality into a distance bound requires the growth function $\psi$ and its generalized inverse; $\psi$ is defined by an infimum over a set that may be empty, and $\psi^{-1}$ by a supremum that may be infinite, so this step has to be handled in extended arithmetic with care. A second difficulty is the $\zeta_1$ term: the map $\xi\mapsto|\langle x,\xi\rangle|^\alpha$ must be shown to be $\alpha$ -Lipschitz on the sphere uniformly over $x\in X$ , which uses $\|x\|\le1$ on the simplex. The change of exponent from $\alpha$ to $\tilde\alpha$ is controlled by a sharp calculus inequality whose constant $e^{-1}$ needs $\alpha,\tilde\alpha\ge1$ . In the nonsingular case, the quadratic form $\int|\langle x,\xi\rangle|^2\Gamma(d\xi)$ must be shown to dominate $c\|x\|^2$ , a compactness argument on the unit sphere of $\mathbb R^s$ .

Formalization scope

$\mathbb R^s$ is EuclideanSpace ℝ (Fin s) with coordinates indexed $0,\dots,s-1$ . The paper says "the (Euclidean) scalar product", so Euclidean norms are the paper's own.
$\Sigma^s$ is Metric.sphere 0 1. A spectral measure is a probability measure on $\mathbb R^s$ with $\Gamma((\Sigma^s)^c)=0$ , and every integral is a set integral over $\Sigma^s$ . For $s=0$ the sphere is empty, no spectral measure exists, and every statement is vacuous, as in the paper.
The standing assumption $\alpha\in(1,2)$ of Section 5 is a hypothesis of every statement. The $\alpha$ -stable law itself is not formalized: the characteristic function on p. 23 only motivates (22), and the mission captures problem (22) exactly.
$\zeta_1$ is a supremum in $[0,\infty]$ over functions on $\mathbb R^s$ that are $1$ -Lipschitz on $\Sigma^s$ , integrated over $\Sigma^s$ only. Such functions are continuous on the compact sphere, so no integral can collapse to a default value. For probability measures, $\zeta_1\le2$ .
$v$ is the real infimum of $r_{\alpha,\Gamma}$ over $X$ . $S$ is the set of minimizers. The paper's "min" in $\psi$ is read as an infimum in the extended reals, equal to $+\infty$ when no feasible point is at distance at least $\tau$ . Distances to sets are extended distances (Metric.infEDist, $+\infty$ to the empty set), and $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$ .
Ruled out: a real-valued supremum for $\psi^{-1}$ (which would be $0$ on unbounded sets), a real distance (which is $0$ to the empty set), and test functions integrated over all of $\mathbb R^s$ (whose off-sphere values could make an integral undefined). Any of these would make the goal trivially true.
"Sufficiently small $\eta$ " is read as "all $\eta\in[0,\eta_0]$ for some $\eta_0>0$ ". Milestone 6 holds for every constant $c>0$ of the norm bound of milestone 5, fixed before $\alpha$ , as $c=c(s,\Gamma)$ on the page.

Welcome contributions: the inequality $\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$ on $[-1,1]$ , strong convexity of $|t|^\alpha$ on $[-1,1]$ , and a general lemma converting a growth function and a uniform objective perturbation into a distance bound; the last is reusable for every stability result of the paper.

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 (preprint at edoc.hu-berlin.de, followed here).
S. T. Rachev, S. Mittnik, Stable Paretian Models in Finance, Wiley, Chichester, 2000 (reference [33] of the paper).
G. Samorodnitsky, M. S. Taqqu, Stable Non-Gaussian Random Processes, Chapman & Hall, 1994. https://doi.org/10.1201/9780203738818
B. Mandelbrot, The variation of certain speculative prices, Journal of Business 36(4) (1963) 394–419. https://doi.org/10.1086/294632
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

8 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Quantitative Stability in Stochastic Programming: The Method of Probability Metrics 1: Solution Sets Move by at Most Ψ of the Minimal Information DistanceResearch Paper

Motivation

A stochastic program minimizes an expected cost under expected-value constraints, and the expectation is taken with respect to a probability distribution $\mu$ of the random data. In applications $\mu$ is rarely known: it is estimated from samples, replaced by a finite scenario tree, or chosen from a parametric family. Whether the optimal value and the optimal decisions of the approximate problem are close to those of the true problem therefore decides whether the approximation can be trusted. Quantitative stability asks for explicit bounds on the change of optimal values and solution sets in terms of a distance between $\mu$ and its perturbation $\nu$ .

S. T. Rachev and W. Römisch (Quantitative stability in stochastic programming: The method of probability metrics, Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint) organize this question around a single probability distance, built directly from the integrands of the problem. Their general results (Section 2) are then specialized to two-stage linear and mixed-integer programs, to chance constraints, to empirical approximations, and to a portfolio problem. This mission covers the general part: Proposition 2.1 and Theorems 2.2 and 2.3.

Setting

Let $X\subseteq\mathbb R^m$ be a nonempty closed set, $\Xi\subseteq\mathbb R^s$ a closed set, and $f_j:\Xi\times\mathbb R^m\to\overline{\mathbb R}$ , $j=0,\dots,d$ , normal integrands: each epigraph $\{(x,r):f_j(\xi,x)\le r\}$ is closed and the epigraphical mapping $\xi\mapsto\operatorname{epi} f_j(\xi,\cdot)$ is measurable. 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,\ \int_\Xi f_j(\xi,x)\,\nu(d\xi)\le0,\ j=1,\dots,d\Big\},

with feasible set $M(\nu)$ , optimal value $v(\nu)$ and solution set $S(\nu)$ ; $\mu$ is the original measure.

For a nonempty set $\mathcal U\subseteq\mathbb R^m$ , the localized problem restricts $x$ to $X\cap\operatorname{cl}\mathcal U$ , with feasible set $M_{\mathcal U}(\nu)$ , value $v_{\mathcal U}(\nu)$ and solutions $S_{\mathcal U}(\nu)$ . The admissible measures $\mathcal P_{\mathcal F_{\mathcal U}}$ are those under which $\int\inf_{x\in X,\|x\|\le r}f_j(\xi,x)\nu(d\xi)>-\infty$ for every $r>0$ and $\sup_{x\in X\cap\operatorname{cl}\mathcal U}\int f_j(\xi,x)\nu(d\xi)<\infty$ . The minimal information distance is

d_{\mathcal F_{\mathcal U}}(\mu,\nu)=\sup_{x\in X\cap\operatorname{cl}\mathcal U}\ \max_{j=0,\dots,d}\Big|\int_\Xi f_j(\xi,x)\,\mu(d\xi)-\int_\Xi f_j(\xi,x)\,\nu(d\xi)\Big|.

The constraints are metrically regular at $(\bar x,0)$ if there are $a\ge0$ , $\varepsilon>0$ with $d(x,M_y(\mu))\le a\max_j\max\{0,\int f_j(\xi,x)\mu(d\xi)-y_j\}$ for $x\in X$ near $\bar x$ and small $y\in\mathbb R^d$ , where $M_y(\mu)$ is the feasible set with right-hand sides $y$ . A nonempty set is a CLM set (complete local minimizing set) with respect to an open $\mathcal U$ if it equals $S_{\mathcal U}(\nu)$ and lies in $\mathcal U$ . The growth function is $\psi(\tau)=\inf\{\int f_0(\xi,x)\mu(d\xi)-v(\mu):d(x,S(\mu))\ge\tau,\ x\in M_{\mathcal U}(\mu)\}$ , with $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$ and $\Psi(\eta)=\eta+\psi^{-1}(\eta)$ .

Formalization targets

Goal: Theorem 2.3, δ-local form

Under the assumptions of Theorem 2.2 — $\mu\in\mathcal P_{\mathcal F_{\mathcal U}}$ ; $S(\mu)\ne\emptyset$ and $\mathcal U$ an open bounded neighbourhood of $S(\mu)$ ; if $d\ge1$ , $x\mapsto\int f_0(\xi,x)\mu(d\xi)$ Lipschitz on $X\cap\operatorname{cl}\mathcal U$ ; metric regularity at every $(\bar x,0)$ , $\bar x\in S(\mu)$ — there are $\hat L\ge1$ and $\delta>0$ with

\emptyset\ne S_{\mathcal U}(\nu)\subseteq S(\mu)+\Psi\big(\hat L\,d_{\mathcal F_{\mathcal U}}(\mu,\nu)\big)\mathbb B\qquad\text{for all }\nu\in\mathcal P_{\mathcal F_{\mathcal U}},\ d_{\mathcal F_{\mathcal U}}(\mu,\nu)<\delta.

The constants are existential: the goal fixes the shape of the estimate, not its constants.

Milestones

Proposition 2.1: $(x,\nu)\mapsto\int f_j(\xi,x)\nu(d\xi)$ is lower semicontinuous on $(X\cap\operatorname{cl}\mathcal U)\times(\mathcal P_{\mathcal F_{\mathcal U}},d_{\mathcal F_{\mathcal U}})$ , and $\nu\mapsto M_{\mathcal U}(\nu)$ has a closed graph.
Display (5) and its converse: near $\bar x\in S(\mu)$ , $M_{\mathcal U}(\mu)$ and $M_{\mathcal U}(\nu)$ lie within $a\,d_{\mathcal F_{\mathcal U}}(\mu,\nu)$ of each other.
Theorem 2.2: Berge upper semicontinuity of $S_{\mathcal U}$ at $\mu$ , the Lipschitz estimate $|v(\mu)-v_{\mathcal U}(\nu)|\le L\,d_{\mathcal F_{\mathcal U}}(\mu,\nu)$ , and the CLM property, for $\nu$ near $\mu$ ; for $d=0$ , the estimate with $L=1$ for all $\nu$ .
Theorem 2.3 for $d=0$ , for every $\nu\in\mathcal P_{\mathcal F_{\mathcal U}}$ , as printed.

Significance

Theorem 2.2 shows that the distance $d_{\mathcal F_{\mathcal U}}$ carries exactly the information about $\mu$ that the problem uses: any probability metric that dominates it inherits the Lipschitz estimate of optimal values. This is the mechanism by which the paper derives stability with respect to Fortet–Mourier metrics for two-stage programs, with respect to discrepancies for mixed-integer and chance-constrained programs, and convergence rates for empirical approximations via empirical-process bounds. Theorem 2.3 adds the solution sets: their deviation is controlled by $\Psi$ , which is determined by the growth of the objective near $S(\mu)$ ; quadratic growth yields Hölder continuity with rate $\tfrac12$ (Remark 2.4).

The results are proved on paper. No machine-checked version of these stability theorems, of metric regularity for expected-value constraints, or of the minimal information distance exists on the platform. The formalization also settles the exact quantifier structure of Theorem 2.3: its printed form ("for each $\nu$ ") is true only for $d=0$ , and the mission states the δ-local form that the proof establishes.

Difficulty

The obvious argument compares the two problems pointwise in $x$ : the integrals differ by at most $d_{\mathcal F_{\mathcal U}}(\mu,\nu)$ , so the optimal values should too. This works without constraints, but with $d\ge1$ the feasible sets themselves move, and a point feasible for $\mu$ need not be feasible for $\nu$ . Controlling this displacement needs metric regularity of the constraint system, which is only local, around each point of $S(\mu)$ ; passing from local to uniform constants requires compactness of $S(\mu)$ and a covering argument. A second difficulty is extended-real analysis: the integrands take the value $+\infty$ , lower semicontinuity must come from Fatou's lemma under the integrability conditions defining $\mathcal P_{\mathcal F_{\mathcal U}}$ , and the existence of localized solutions depends on this lower semicontinuity on the compact set $X\cap\operatorname{cl}\mathcal U$ .

Formalization scope

$\mathbb R^m$ and $\mathbb R^s$ are EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin s); the paper never fixes its norm, and every statement has existential constants, so the Euclidean norm is a faithful instance. Measures are Borel probability measures on the subtype $\Xi$ . Integrals of extended-real integrands use the published DupacovaWets.Consistency.expect ( $+\infty$ when $\int f^+=\infty$ ). The integrands are indexed by Fin (d+1), with index $0$ the objective. Values $v$ , $v_{\mathcal U}$ and $\psi$ are infima in $\overline{\mathbb R}$ ( $+\infty$ on empty sets; the paper's "min" in $\psi$ is read as an infimum); $d_{\mathcal F_{\mathcal U}}$ , $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$ ; distances to sets are extended distances (infinite to the empty set). Lower semicontinuity and closed graphs in Proposition 2.1 are stated sequentially, which is equivalent in the extended pseudometric space $(\mathcal P_{\mathcal F_{\mathcal U}},d_{\mathcal F_{\mathcal U}})$ . The balls $B(\bar x,\bar\varepsilon)$ in (5) are closed balls.

Standing assumptions carried by every statement: $X$ nonempty and closed, $\Xi$ closed, all $f_j$ normal integrands, and measures in $\mathcal P_{\mathcal F_{\mathcal U}}$ . Every value estimate asserts that both optimal values are finite, so no bound holds through an $\infty-\infty$ convention, and the distance to an empty feasible set is $+\infty$ , so metric regularity cannot hold vacuously. The one deliberate deviation from the page is the δ in the goal, explained above.

A complete development needs Fatou's lemma for extended-real integrands bounded below by an integrable function, measurability of infima of normal integrands, and Berge's stability theorem for parametric programs. The first two are reusable for every stochastic-programming mission on the platform. Contributions of these lemmas as separate theorems are welcome.

Selected references

S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: The method of probability metrics, Math. Oper. Res. 27(4) (2002), 792–818. https://doi.org/10.1287/moor.27.4.792.304
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (normal integrands, Ch. 14; metric regularity, Ch. 9). https://doi.org/10.1007/978-3-642-02431-3
B. Bank, J. Guddat, D. Klatte, B. Kummer, K. Tammer, Non-Linear Parametric Optimization, Akademie-Verlag, Berlin, 1982 (Berge stability, Thm. 4.2.1).
D. Klatte, A note on quantitative stability results in nonlinear optimization, in: Proceedings 19. Jahrestagung Mathematische Optimierung, Seminarbericht Nr. 90, Humboldt-Universität Berlin, 1987, 77–86 (the proof pattern of Theorem 2.2).

10 thms2 active usersReviewed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

A Coordinate Gradient Descent Method for Nonsmooth Separable Minimization 3: The Local Lipschitzian Error Bound Holds for Polyhedral P with Quadratic or Composite f, and for Strongly Convex fResearch Paper

Motivation

Many problems in statistics, signal processing and machine learning minimize the sum of a smooth function and a convex but nonsmooth one: $\ell_1$ -regularized least squares (the Lasso), bound-constrained problems, and group-sparse regression are standard examples. Tseng and Yun (Math. Program. Ser. B 117 (2009) 387–423) proposed the coordinate gradient descent (CGD) method for this class and proved that it converges linearly under a local Lipschitzian error bound, Assumption 2(a) of their paper. An assumption is only as useful as the list of problems known to satisfy it. Section 6 of the paper supplies that list, and this mission formalizes it.

Error bounds of this kind have a history in smooth constrained optimization. Luo and Tseng proved them for quadratic objectives over polyhedral sets (Luo–Tseng 1992, SIAM J. Optim.), for strongly convex functions composed with a linear map (Luo–Tseng 1992, SIAM J. Control Optim.), and for dual functionals of linearly constrained strictly convex programs (Luo–Tseng 1993, Math. Oper. Res.), and used them to derive linear rates for feasible descent methods (Luo–Tseng 1993, Ann. Oper. Res.). Tseng and Yun carry these results over to the nonsmooth problem (1) by reformulating it as a smooth problem over the epigraph of the nonsmooth part.

Setting

Throughout, $\mathbb R^n$ carries the Euclidean norm $\|\cdot\|$ . The problem is

\min_x\; F_c(x) = f(x) + cP(x), \qquad (1)

where $c > 0$ , $P:\mathbb R^n \to (-\infty,\infty]$ is proper, convex and lower semicontinuous with effective domain $\operatorname{dom}P = \{x \mid P(x) < \infty\}$ , and $f$ is continuously differentiable on an open set containing $\operatorname{dom}P$ .

The residual at $x \in \operatorname{dom}P$ is

d_I(x) = \arg\min_d \Big\{\nabla f(x)^\top d + \tfrac12\|d\|^2 + cP(x+d)\Big\},

the unique minimizer of a strongly convex function. A point $x \in \operatorname{dom}P$ is stationary if the one-sided directional derivative satisfies $F_c'(x;d) \ge 0$ for every direction $d$ ; $\bar X$ denotes the set of stationary points and $\operatorname{dist}(x,\bar X)$ the distance to it. A point is stationary exactly when its residual vanishes.

Assumption 2(a) asks that $\bar X \neq \emptyset$ and that for every level $\zeta$ there be constants $\tau, \epsilon > 0$ with

\operatorname{dist}(x,\bar X) \le \tau\|d_I(x)\| \quad\text{whenever } F_c(x) \le \zeta,\ \|d_I(x)\| \le \epsilon.

Writing $\operatorname{epi}P = \{(x,\xi) \mid P(x) \le \xi\}$ , problem (1) is equivalent to the smooth problem $\min\{f(x) + c\xi \mid (x,\xi) \in \operatorname{epi}P\}$ (41). Its projection residual at $(x,\xi)$ is the optimal solution $(\tilde d,\tilde\delta)$ of

\min_{(d,\delta)}\Big\{\nabla f(x)^\top d + \tfrac12\|d\|^2 + \tfrac12\delta^2 + c\delta \;\Big|\; (x+d,\xi+\delta) \in \operatorname{epi}P\Big\}. \qquad (42)

$P$ is polyhedral if $\operatorname{epi}P$ is the solution set of finitely many linear inequalities in $(x,\xi)$ ; $f$ is quadratic if $f(x) = \tfrac12 x^\top Ax + b^\top x + c_0$ with $A$ symmetric, not necessarily positive semidefinite. The four problem classes are:

C1: $f$ quadratic, $P$ polyhedral;
C2: $f(x) = g(Ex) + q^\top x$ with $g$ strongly convex and differentiable on $\mathbb R^m$ , $\nabla g$ Lipschitz, $P$ polyhedral;
C3: $f(x) = \max_{y\in Y}\{(Ex)^\top y - g(y)\} + q^\top x$ with $Y$ polyhedral and $g$ as in C2, $P$ polyhedral;
C4: $f$ strongly convex with $\nabla f$ Lipschitz on $\operatorname{dom}P$ (condition (22)).

Formalization targets

Goal: Theorem 4 (p. 412)

\Big(\bar X \neq \emptyset \ \wedge\ (\mathrm{C1} \vee \mathrm{C2} \vee \mathrm{C3})\Big) \ \vee\ \mathrm{C4} \;\Longrightarrow\; \text{Assumption 2(a)}.

Under C4, nonemptiness of $\bar X$ is part of the conclusion. The constants $\tau, \epsilon$ are existential, so the goal does not depend on any particular estimate.

Milestone: Lemma 6 (p. 410)

If $P$ is Lipschitz on $\operatorname{dom}P$ with constant $K$ , there is $\kappa > 0$ depending only on $K$ with

\|(\tilde d,\tilde\delta)\| \le \kappa\,\|d_I(x)\| \qquad (x \in \operatorname{dom}P,\ \xi = P(x)).

Milestone: Lemma 7 (p. 411)

If $\bar X \neq \emptyset$ and C1, C2 or C3 holds, then for every $\zeta$ there are $\tau', \epsilon' > 0$ with

\operatorname{dist}(x,\bar X) \le \tau'\|(\tilde d,\tilde\delta)\| \quad\text{whenever } F_c(x) \le \zeta,\ \|(\tilde d,\tilde\delta)\| \le \epsilon', \qquad (44)

where $(\tilde d,\tilde\delta)$ solves (42) with $\xi = P(x)$ .

A further item, not a milestone, states the remark after Assumption 2 (p. 404) that Assumption 2(b) (stationary points with different objective values are uniformly separated) holds whenever $f$ is convex.

Significance

Theorem 4 is what makes the linear convergence theorem of the paper (Theorem 2, the subject of the second mission of this series) applicable. Through C1 it covers every problem with a quadratic $f$ and a polyhedral $P$ , including the Lasso and $\ell_1$ -regularized or bound-constrained quadratic programs, without convexity of $f$ . Through C2 it covers losses of the form $g(Ex)$ with $g$ strongly convex, such as least squares $\tfrac12\|Ex - b\|^2$ , where $f$ itself is not strongly convex because $E$ may have a nontrivial kernel. These error bounds became a standard tool for linear rates of proximal and coordinate methods without strong convexity.

The paper's result is proved, but Lemma 7 is proved by citation: it applies three error bounds of Luo and Tseng to the reformulation (41). A complete formalization therefore requires those error bounds for smooth problems over polyhedral sets, which are not in Mathlib. To our knowledge none of the results of this mission has a machine-checked proof.

Difficulty

Lemma 6 and the C4 case of Theorem 4 are short inequality arguments. The difficulty is Lemma 7. The natural first idea, proving an error bound from strong convexity, fails for C1–C3: $f$ may be nonconvex (C1) or have a degenerate Hessian (C2, C3), and the objective $f(x) + c\xi$ of (41) is never strongly convex in $(x,\xi)$ . What replaces strong convexity is the polyhedral structure of $\operatorname{epi}P$ , and the cited Luo–Tseng error bounds that exploit it are substantial results in their own right, each of which has to be established for a projection residual over a general polyhedron in $\mathbb R^{n+1}$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with indices $0,\dots,n-1$ . $P$ is the pair $(D, P)$ , its effective domain and its finite values there, with "proper, convex, lsc" given by the published ProxNewton.Inexact.IsProperClosedConvex. The value $+\infty$ is never computed: every statement quantifies over $x \in D$ , and membership in $\operatorname{epi}P$ is x + d ∈ D ∧ P (x + d) ≤ ξ + δ. $d_I(x)$ is a chosen minimizer of its subproblem, which at $x \in D$ is the paper's unique one. The solutions of (42) enter through a predicate, and every bound is asserted for every optimal solution. Stationarity is the liminf form of $F_c'(x;d) \ge 0$ . $\operatorname{dist}$ is the infimum distance. Assumption 2(a) quantifies over every real $\zeta$ , which agrees with the paper's " $\zeta \ge \min F_c$ " because the condition is vacuous below $\inf F_c$ . In Lemma 6 the constant $\kappa$ is quantified before the dimension and the data, so it depends on the Lipschitz constant only.

Explicit choices relative to the printed text:

In C4, strong convexity and (22) are required on $\operatorname{dom}P$ only, since $f$ is only assumed smooth near $\operatorname{dom}P$ . This hypothesis is weaker than the paper's, so the formal theorem is at least as strong.
In C2 and C3, $E$ is a continuous linear map $\mathbb R^n \to \mathbb R^m$ (equivalently an $m \times n$ matrix). Strong convexity has a positive modulus and $\nabla g$ is globally Lipschitz.
In C3, the maximum must be attained at every $x$ , which forces $Y \neq \emptyset$ , as the paper's formula presumes.
Assumption 2(b) for convex $f$ is stated with convexity on $\operatorname{dom}P$ .

A polyhedrality notion that admits only affine or constant $P$ , an Assumption 2(a) whose constants are chosen after $x$ , and a Lemma 7 whose residual is $d_I(x)$ instead of the solution of (42) would all trivialize or change the statements. The encoding rules out each of them: polyhedral means a finite system of linear inequalities in $(x,\xi)$ , the constants precede $x$ , and Lemma 7 is stated for (42).

Welcome contributions: proofs of Lemma 6 and of the C4 case; Lipschitz continuity of polyhedral functions on their domain (Rockafellar–Wets, Example 9.35); the Luo–Tseng error bounds for affine variational inequalities and for composite strongly convex objectives over polyhedra, which can be reused well beyond this mission.

Selected references

P. Tseng, S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Math. Program. Ser. B 117 (2009) 387–423. https://doi.org/10.1007/s10107-007-0170-0
Z.-Q. Luo, P. Tseng, Error bounds and the convergence analysis of matrix splitting algorithms for the affine variational inequality problem, SIAM J. Optim. 2 (1992) 43–54. https://doi.org/10.1137/0802004
Z.-Q. Luo, P. Tseng, On the linear convergence of descent methods for convex essentially smooth minimization, SIAM J. Control Optim. 30 (1992) 408–425. https://doi.org/10.1137/0330025
Z.-Q. Luo, P. Tseng, On the convergence rate of dual ascent methods for linearly constrained convex minimization, Math. Oper. Res. 18 (1993) 846–867. https://doi.org/10.1287/moor.18.4.846
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

7 thms2 active usersReviewed

Analysis Operations Research Probability+2·Captain: mikedeng1

Some Useful Functions for Functional Limit Theorems 3: The First-Passage-Time Map Is M₁-Continuous and J₁-Continuous at Strictly Increasing PathsResearch Paper

Why first passage times need a continuity theorem

Functional limit theorems in queueing and applied probability are rarely proved from scratch. A limit theorem is established once for a primitive process, such as a random walk, a cumulative input or a renewal-reward process, and then transferred to the quantities of interest through the continuous mapping theorem: if $X_n \Rightarrow X$ in a function space and $f$ is continuous at almost every path of $X$ , then $f(X_n) \Rightarrow f(X)$ . The method works only if the functions in use are known to be continuous, and in which topology.

Ward Whitt's 1980 paper supplies these facts for composition, addition, the supremum, the reflecting barrier, the inverse or first passage time, and time reversal. This mission covers §7, the first passage time. Its role in applications is direct: the counting process of a renewal process is the first passage time of the partial-sum process. A limit theorem for cumulative work can therefore yield one for the number of completed jobs, and a limit theorem for a cumulative input can yield one for the time it takes to reach a level, when the mapping theorem's hypotheses hold.

Timeline. Skorohod (1956) introduced the topologies $J_1$ and $M_1$ on the space $D$ of right-continuous paths with left limits. Vervaat (1972) studied functional central limit theorems for processes with positive drift and their inverses, and Whitt (1971) studied weak convergence of first passage time processes. Whitt's 1980 paper restates $M_1$ continuity (Theorem 7.1) and adds the $J_1$ result: the map is continuous at every strictly increasing path (Theorem 7.2), although it is not $J_1$ -continuous on its whole domain.

Setting

A path is a function $x : [0,\infty) \to \mathbb R$ . It belongs to $D = D([0,\infty),\mathbb R)$ when it is right-continuous and has a left limit at every $t > 0$ .

$J_1$ convergence. On a compact interval $[0,b]$ , $x_n \to x$ in $J_1$ when there are increasing homeomorphisms $\lambda_n$ of $[0,b]$ with $\sup_t |\lambda_n(t) - t| \to 0$ and $\sup_t |x_n(t) - x(\lambda_n(t))| \to 0$ . On $[0,\infty)$ this is required on $[0,b]$ for every $b$ at which $x$ is continuous.
$U$ convergence. Uniform convergence on compact subintervals.
$M_1$ convergence. The completed graph of $x$ on $[0,b]$ adds to the graph the vertical segment joining $x(t-)$ and $x(t)$ at each jump. $x_n \to x$ in $M_1$ when the completed graphs admit parametric representations (continuous, order-preserving maps from $[0,1]$ onto the completed graph) that are uniformly close in both time and space.
The supremum. $x^{\uparrow}(t) = \sup_{0 \le s \le t} x(s)$ .
The domain $E$ . The set of $x \in D$ that are unbounded above and have $x(0) \ge 0$ .
First passage time. For $x \in E$ ,

x^{-1}(t) = \inf\{s \ge 0 : x(s) > t\}, \qquad t \ge 0.

$D_0$ . The nondecreasing paths in $D$ , and $C$ the continuous ones.

Formalization targets

Goal: Theorem 7.2, continuity clause

If $x_n, x \in E$ , $x$ is strictly increasing, and $x_n \to x$ in $J_1$ , then

x_n^{-1} \to x^{-1} \quad (J_1).

The theorem says that every strictly increasing path is a continuity point of the first passage time map for $J_1$ . It fixes no constants, so a sharper variant of a milestone does not invalidate it.

Milestones

$J_1$ convergence implies $M_1$ convergence (§6, p. 80).
The supremum map is $M_1$ -continuous on paths with $x(0) \ge 0$ (§6, p. 80, as used in the proof of Theorem 7.1).
$x \in E$ implies $x^{-1} \in E \cap D_0([0,\infty),[0,\infty))$ (§7, p. 82).
$x^{\uparrow} \in E$ and $(x^{\uparrow})^{-1} = x^{-1}$ (proof of Theorem 7.1).
Theorem 7.1. If $x_n, x \in E$ and $x_n \to x$ in $M_1$ , then $x_n^{-1} \to x^{-1}$ in $M_1$ .
For strictly increasing $x \in E$ , $x^{-1}$ is continuous with $x^{-1}(0) = 0$ .
$M_1$ convergence to a continuous limit starting at $0$ is $U$ convergence.
$U$ convergence implies $J_1$ convergence.
Theorem 7.4. If $c_n \to \infty$ , $x_n \in E$ , $c_n(x_n^{\uparrow} - e) \to x$ and $c_n(x_n^{-1} - e) \to -x$ in $J_1$ , then $x \in C$ .

Significance

The result. Theorem 7.2 lets $J_1$ functional limit theorems pass to first passage times when the limit has strictly increasing paths. The typical case is the fluid limit $x(t) = \mu t$ of a cumulative process, with $\mu>0$ . Together with the composition results of §3, it supports Theorem 7.3's centered inverse limit: if $c_n \to \infty$ , $x_n \in E$ , $x(0)=0$ , $x$ has no positive jumps, and $c_n(x_n-e) \to x$ in $J_1$ , then $c_n(x_n^{-1}-e) \to -x$ in $J_1$ . This is one step from a central limit theorem for partial sums to one for counting processes. Theorem 7.4 shows a limitation: convergence of both the centered supremum and the centered inverse in $J_1$ forces a continuous limit.

Formalizing it. The results are proved and classical, but none of them has a machine-checked proof. The mission produces the $M_1$ topology on $D([0,\infty),\mathbb R)$ in Lean, the first passage time map with its basic properties, and the comparison between $J_1$ , $M_1$ and $U$ . That infrastructure is reused by every later formalization that goes through counting processes or the $M_1$ topology, including the planned wave of §§3–7 corollaries in this series.

Difficulty

The first passage time map is not $J_1$ -continuous. On p. 82 the paper gives paths $x_n \to x$ in $J_1$ whose inverses converge only in $M_1$ : a flat stretch of the limit becomes a jump of $x^{-1}$ , which the inverses of the approximating paths approach through two separate jumps. Inverting the time changes $\lambda_n$ of the $J_1$ convergence cannot handle that split, because $J_1$ matches jumps one to one. The hypothesis that $x$ is strictly increasing excludes flat stretches of the limit. The technical weight lies in completed graphs and their parametric representations, which Mathlib does not have, and in the restriction to compact intervals at continuity points of the limit.

Formalization scope

Paths are total functions $\mathbb R \to \mathbb R$ . Only $[0,\infty)$ matters, and every statement is on Ici 0. All convergences are sequential, which is equivalent because the spaces are metrizable (Theorem 2.6). Membership of every path in $D$ is part of each convergence.
$J_1$ is the shared layer of the series: the metric (2.1) with $[0,\infty]$ -valued distances, extended to $[0,\infty)$ through restrictions to $[a,b]$ whose endpoints are continuity points or endpoints.
$M_1$ is not defined in the paper. The mission defines it with the convention $x(0-) := 0$ at the origin, so the completed graph on $[0,b]$ starts with the segment from $(0,0)$ to $(0,x(0))$ . With the convention $x(0-) = x(0)$ , Theorem 7.1 is false. For $x(s) = (s-1)^+$ and $x_n = x + 1/n$ , $x_n^{-1}$ jumps from $0$ to $1$ at $t = 1/n$ while $x^{-1}(0) = 1$ . The convention is Whitt's later $M_1'$ . Two milestones carry a hypothesis that this convention forces, and each says so: the supremum milestone requires $x_n(0), x(0) \ge 0$ (as on $E$ ), and the $M_1 \Rightarrow U$ milestone requires $x(0) = 0$ . The goal, which is stated in $J_1$ , does not depend on the convention.
$x^{-1}$ is a real infimum. Its set is nonempty because paths in $E$ are unbounded above, so every statement that uses $x^{-1}$ assumes membership in $E$ . The inequality $x(s) > t$ is strict, as on the page.
Omitted. The measurability clause of Theorem 7.2 refers to the Borel σ-field of $J_1$ , which the series does not build, and it is not stated. Replacing it by measurability for the product σ-algebra would be a different statement. The second clause of the §6 sentence on $D_0$ is also not stated.
Ruled out. A formalization in which $x^{-1}$ is applied outside $E$ (giving the junk value $0$ ), or in which $J_1$ convergence omits membership in $D$ (making the restriction clause vacuous), would trivialize the goal. Both are excluded.

Contributions welcome: the general theory of parametric representations (existence, and the $M_1$ comparison with $J_1$ and $U$ ), which is reusable for any $M_1$ result. Alternative proofs of Theorem 7.2 that avoid $M_1$ are also welcome.

Selected references

W. Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, 67–85. https://doi.org/10.1287/moor.5.1.67
A. V. Skorohod, Limit theorems for stochastic processes, Theory of Probability and Its Applications 1(3), 1956, 261–290. https://doi.org/10.1137/1101022
W. Whitt, Weak convergence of first passage time processes, Journal of Applied Probability 8(2), 1971, 417–422. https://doi.org/10.2307/3211913
W. Vervaat, Functional central limit theorems for processes with positive drift and their inverses, Zeitschrift für Wahrscheinlichkeitstheorie 23, 1972, 245–253. https://doi.org/10.1007/BF00532510
W. Whitt, Stochastic-Process Limits, Springer, 2002, §13.6. https://doi.org/10.1007/b97479

14 thms2 active usersReviewed

Graph Theory Operations Research Probability+1·Captain: mikedeng1

Stability Properties of Constrained Queueing Systems and Scheduling Policies for Maximum Throughput in Multihop Radio Networks II: Outside C̄′ the Queues Grow to Infinity a.s. under Every PolicyResearch Paper

Motivation

In a multihop radio network, links that are close to each other interfere, so only certain sets of links can transmit in the same time slot. Tassiulas and Ephremides (IEEE TAC 1992) modelled this as a constrained queueing system and asked which arrival rates any scheduler can sustain. Their answer has two halves. The first, Theorem 3.2, shows that a maximum-weight ("back-pressure") policy stabilizes the network for every rate vector in an explicit region $C'$ , and that no stationary policy does better than its closure. The second, Theorem 4.1 and the subject of this mission, removes the restriction to stationary policies: outside the closure $\bar C'$ , every scheduler, however it uses the past, lets the queues grow without bound almost surely.

The pair of results is the origin of throughput-optimal scheduling in wireless and switched networks: max-weight scheduling in input-queued switches, back-pressure routing, and the Lyapunov-drift framework of network utility maximization all start from this region and this converse. The converse is what makes "throughput-optimal" a meaningful claim: it certifies that $\bar C'$ is a hard limit, not merely the limit of one policy class.

Setting

There are $L$ queues and $N$ servers (links). Server $i$ serves queue $q(i)$ and sends each served customer to a queue $h(i)$ or out of the system. Time is slotted and a service takes one slot. An activation set is a set of servers that may be active in the same slot; the constraint set $S$ is the family of all activation sets, and assumption C.1 says that every subset of an activation set is an activation set. The activation vector of a set $c$ is its indicator vector in $\{0,1\}^N$ , and $\mathrm{co}(S)$ is the convex hull of the activation vectors.

A history-dependent policy $\pi\in\tilde G$ chooses, at the start of slot $t$ , an activation set $E(t)\in S$ as a function of the queue-length vectors $X(0),\dots,X(t-1)$ , never activating more servers of a queue than it has customers. The queue lengths evolve by

X_l(t)=X_l(t-1)-\#\{i\in E(t):q(i)=l\}+\#\{i\in E(t):h(i)=l\}+A_l(t),

where the arrivals $A_l(t)$ are i.i.d. over $t$ , independent across queues, with finite second moments and means $a_l$ .

The routing matrix $R$ has $r_{li}=1$ if $h(i)=l$ and $r_{li}=-1$ if $q(i)=l$ . A vector $f\ge0$ indexed by servers is an $a$ -admissible flow if $a=-Rf$ . The region $C'$ is the set of $a\ge0$ that admit such a flow and a point $c\in\mathrm{co}(S)$ with $f_i<c_i$ wherever $f_i>0$ and $f_i=0$ wherever $c_i=0$ .

The proof uses the flow network $N_{af}$ : the queues plus an originator $o$ and a terminal $d$ , an edge $(o,l)$ of capacity $a_l$ for every queue, and an edge of capacity $f_k$ from $q(k)$ to $h(k)$ (or to $d$ ) for every server $k$ . A cut is a set $W$ of queues on the originator's side; its capacity $C_{af}$ is the total capacity of the edges leaving $W\cup\{o\}$ .

Formalization targets

Goal: Theorem 4.1

a\notin\bar C'\ \Longrightarrow\ \lim_{t\to\infty}\sum_{l=1}^L X_l(t)=\infty\quad\text{a.s., for every }\pi\in\tilde G\text{ and every initial state.}

Milestones, in the order the proof uses them

Lemma A.1: under C.1, $c\in\mathrm{co}(S)$ and $0\le x\le c$ imply $x\in\mathrm{co}(S)$ .
Lemma 3.1 (one class, unit service): $\bar C'=\{a\ge0:\exists f\in F_a,\ c\in\mathrm{co}(S),\ f\le c\}$ .
Lemma 4.1: if $a\notin\bar C'$ , the maximum over $f\in\mathrm{co}(S)$ of the mincut capacity of $N_{af}$ is attained and is strictly below $\sum_l a_l$ .
Corollary 4.1: there is one $\epsilon>0$ such that $\sum_{l\in W_{af}}a_l-\epsilon$ bounds the server capacity leaving $W_{af}$ , for every $f\in\mathrm{co}(S)$ and every mincut.
(4.7), pathwise: $\sum_l X_l(t)\ge\min_{Q}\sum_{\tau=1}^t\big(\sum_{l\in Q}(A_l(\tau)-a_l)+\epsilon\big)$ for every policy and every arrival sequence.
(4.12): each of these $2^L$ partial sums tends to $+\infty$ almost surely.

Significance

Theorem 4.1 closes the characterization of the throughput region of a constrained queueing network. With Theorem 3.2 it says that the set of sustainable rates is $C'$ up to its boundary, for all policies and not only stationary ones, and that allowing schedules to depend on the entire history, on time, or on long-range planning cannot enlarge it. Every later throughput-optimality result for max-weight-type policies in switches and wireless networks cites this converse, and the region $\mathrm{co}(S)$ of "average activation vectors" is the standard capacity region of interference-constrained networks.

The result has been proved since 1992 and has not, to our knowledge, been machine-checked. A formalization adds a precise statement of the policy class $\tilde G$ (history-dependent, non-anticipating, never serving empty queues), a sample-path inequality (4.7) that is independent of probability and reusable for any arrival model, and a cut-based description of $\bar C'$ through Lemma 4.1 and Corollary 4.1.

Difficulty

The obvious argument fails at the policy class. For a stationary policy the queue-length process is a Markov chain and an instability argument can use its ergodic behaviour; a history-dependent policy has no such structure, and the time-average activation vector $\lambda(t)=\frac1t\sum_{\tau\le t}E(\tau)$ wanders in $\mathrm{co}(S)$ without converging. The argument must therefore find, for every possible average $\lambda$ , a set of queues whose net inflow exceeds its outflow by a margin that does not depend on $\lambda$ . That uniformity is the content of Lemma 4.1 and Corollary 4.1: it needs the max-flow/min-cut theorem on $N_{af}$ , the continuity of the mincut capacity in $f$ , the compactness of $\mathrm{co}(S)$ , and Lemma A.1 to bring a maximum flow back into $\mathrm{co}(S)$ . Comparing $\sum_l a_l$ with the total service capacity, or using a single fixed cut, does not work: the bottleneck set of queues depends on how the policy spreads its activations.

Formalization scope

Queues are Fin L and servers Fin N, indexed from 0. A server's destination is Option (Fin L), none meaning out of the system. $S$ is a Set (Finset (Fin N)); C.1 is a predicate, and every theorem that needs it also assumes $\emptyset\in S$ (otherwise $S$ may be empty and no policy exists). Rate vectors are Fin L → ℝ, and $C'$ includes $a\ge0$ . Service times are one slot, so $M=I$ . The goal's hypothesis is $a\notin\bar C'$ with $C'$ defined from flows, as in the introduction of §IV; the printed theorem uses the closure of the stability region $C$ , which equals $\bar C'$ by Theorem 3.2 of the paper. A policy is a function from the history $X(0),\dots,X(t)$ to the activation set of slot $t+1$ , required to choose sets in $S$ and to activate no more servers of a queue than it has customers; the queue dynamics are written in $\mathbb N$ , where this requirement makes the subtraction exact. Arrivals are random vectors in $\mathbb N^L$ , i.i.d. in time (iIndepFun, IdentDistrib), independent across queues, with integrable squares; $a$ is their mean, not a free parameter.

The statement does not hold vacuously: a one-queue, one-server example with constant arrivals of two customers per slot satisfies every hypothesis of the goal, including the existence of runs, and lies outside $\bar C'$ (checked in a sanity file). A formalization in which policies may see future arrivals, or may serve empty queues, or in which $a$ is unrelated to the arrival law, is a different theorem.

A complete development needs: the max-flow/min-cut theorem for finite networks with parallel edges (posed elsewhere on the platform in other encodings, not proved), continuity of a minimum of finitely many linear functions, compactness of a convex hull of finitely many points, and Mathlib's strong law of large numbers. The pathwise bound (4.7) and the cut lemmas are reusable for any interference-constrained network. Proofs of any milestone, and alternative routes to Lemma 4.1 (for instance through linear-programming duality), are welcome.

Selected references

L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
C. H. Papadimitriou and K. Steiglitz, Combinatorial Optimization: Algorithms and Complexity, Prentice-Hall, 1982 (reference [17] of the paper, for the max-flow/min-cut theorem).
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5

9 thms2 active usersReviewed

Machine Learning Markov Chain Probability+1·Captain: mikedeng1

An Analysis of Temporal-Difference Learning with Function Approximation 2: For Every Sampling Distribution q and 5/6 < α < 1, Off-Line q-Sampled TD(0) Can Diverge in ExpectationResearch Paper

Motivation

Temporal-difference learning estimates the future cost of a system from observed transitions. In a Markov model, a state has a distribution of possible successors and each transition carries a cost. An agent may approximate the future cost with a small number of basis functions rather than store one number per state. This is useful when the state set is large or countably infinite, but the sampling rule then matters: the states used to update the approximation need not arrive in the same proportions as visits to the underlying Markov chain.

Tsitsiklis and Van Roy distinguish sampling along the chain from drawing current states independently from a chosen distribution $q$ . Their 1996 LIDS report, §9 constructs an example where the latter version of TD(0) has a mean parameter vector whose norm grows without bound. The example applies to every sampling distribution $q$ on a countable state space with at least two states and every discount factor $\alpha$ strictly between $5/6$ and $1$ . The mission formalizes that quantified counterexample, rather than selecting a particular two-state distribution.

Setting

Let $S$ be a finite or countably infinite set of states. A transition matrix $P$ assigns a probability distribution $p_{ij}$ over next states $j$ to each current state $i$ . A transition cost $g(i,j)$ is incurred when the chain moves from $i$ to $j$ , and $0<\alpha<1$ discounts later costs. The cost-to-go $J^*(i)$ is the expected sum of discounted costs along a chain started at $i$ . An invariant distribution $\pi$ satisfies $\pi^{\mathsf T}P=\pi^{\mathsf T}$ .

A feature vector $\phi(i)\in\mathbb R^K$ represents an approximate cost $\phi(i)^{\mathsf T}r$ , where $r\in\mathbb R^K$ is learned. The weighted norm $\|J\|_D$ uses the weights $\pi(i)$ , and $\Pi$ projects onto the span of the features in that norm. The one-step operator $T^{(0)}$ sends $J$ to the expected immediate cost plus $\alpha$ times the next-state value. These are the objects of §§2–4 of the report.

In $q$ -sampled TD(0), each current state $I_t$ is drawn independently from a probability distribution $q$ ; a successor $J_t$ is then drawn from row $P(I_t,\cdot)$ . Each new pair is independent of the earlier pairs. The parameter changes by

r_{t+1}=r_t+\gamma_t\phi(I_t)\left[g(I_t,J_t)+\alpha\phi(J_t)^{\mathsf T}r_t-\phi(I_t)^{\mathsf T}r_t\right].

The step sizes $\gamma_t$ satisfy the report's Assumption 4: they are chosen in advance, nonnegative and nonincreasing, their sum diverges, and the sum of their squares converges. Assumption 1 asks for a unique positive invariant law, finite stationary second moment of the transition costs, and finite cost-to-go from each state. Assumption 2 asks for linearly independent features with finite stationary second moments.

Formalization targets

Divergence of the mean

For every $q$ and $5/6<\alpha<1$ , Theorem 3 asserts the existence of $P$ , $g$ , and a feature map satisfying Assumptions 1 and 2, together with a unique projected fixed-point parameter $r^*$ , such that for every $r_0\ne r^*$ ,

\Pi T^{(0)}(\phi^{\mathsf T}r)=\phi^{\mathsf T}r\iff r=r^*, \qquad \lim_{t\to\infty}\bigl\|\mathbb E[r_t\mid r_0]\bigr\|=\infty.

The expectation is over the independent state–successor samples. The target is the norm of the mean vector; it does not assert divergence of individual sample paths. The formal goal quantifies over every probability space carrying samples with the stated joint law, so a choice of representation for the random process does not change the theorem.

Supporting statements

The milestones follow the claims in the proof of Theorem 3, pp. 24–25: existence of a full-support transition distribution; the one-feature construction and its assumptions; the general and specialized recurrences for $\mathbb E[r_t]$ ; a positive lower bound for their coefficient $\Delta$ ; and unbounded growth from that lower bound. The numerical inequality retains the report's threshold $5/(6\alpha)$ and its explicit positive factor $6\alpha p(s_2)-5$ .

Significance

The theorem identifies a limit of using TD(0) with linear approximation when the current states are sampled according to a distribution unrelated to the chain's invariant law. The constructed Markov chain itself has a well-defined zero cost-to-go, and the approximation uses only one nonzero feature direction. Nevertheless, the mean of the parameter sequence diverges for every nonfixed initialization. Thus the issue is present even without noisy costs or a complicated feature space. The report contrasts this with its convergence result for the on-line algorithm under additional assumptions; the counterexample says that those conclusions cannot be transferred to arbitrary independent state sampling by changing only the sample source. Tsitsiklis and Van Roy, §9.

The report proves Theorem 3 on paper. This mission asks for a machine-checked proof of its full quantifier structure, including countably infinite state spaces and arbitrary $q$ . A completed development would supply reusable Lean interfaces for countable Markov kernels, path laws, weighted projections, independent state–successor samples, and expected stochastic recurrences. The proposal currently contains the statements and definitions; the theorem proofs are open.

Difficulty

The apparent simplicity of the one-dimensional example hides two issues. First, the statement is uniform over $q$ , including distributions that put zero mass on nearly every state. A proof must choose the two feature states in response to $q$ while preserving the strict positivity needed for growth. Second, the recurrence concerns $\mathbb E[r_t]$ , where $r_t$ depends on all earlier random pairs. The step at time $t$ uses a fresh pair, and the factorization of its mean requires that temporal independence, plus justified integrability. Writing a positive scalar coefficient alone does not establish divergence of the expected parameter sequence for the sampled process.

Formalization scope

The Lean state space is a countable discrete measurable type with at least two elements. $P$ is a Markov kernel, its path law comes from the Ionescu–Tulcea construction, and the cost-to-go is the expectation of the discounted path sum. Weighted $L_2(S,D)$ membership is expressed by summability of $\pi(i)J(i)^2$ . The projection uses the inverse of the weighted Gram matrix under the independence and positive-mass assumptions that make it invertible. Only $T^{(0)}$ is needed here. The number $K$ of basis functions is existential, like the report's matrix $\Phi$ , but must be at least one: an empty parameter space would leave the universal divergence clause with no nonfixed initializations. The report's own example has $K=1$ .

Assumption 1 includes uniqueness of $\pi$ , positive mass at each state, the stationary squared-cost moment, and absolute integrability of the cost-to-go. Assumption 2 includes linear independence and integrability of squared features. Assumption 4 retains square-summability even though the displayed growth argument uses the divergent first-power sum. The general mean recurrence assumes bounded costs and features so its integrals and countable sums are meaningful; the constructed example satisfies those bounds. The goal additionally states finite-time integrability of the parameter vector. The source indexes states by 1 and 2; the formalization uses two distinct states $s_1,s_2$ and records the proof's ordering $0<q(s_1)$ and $q(s_2)\le q(s_1)$ in the growth milestone. The goal's quantification over probability spaces is restricted to Lean's Type universe.

The general mean recurrence is written with the immediate cost outside the matrix factor multiplying $\mathbb E[r_t]$ . This follows the algorithm displayed on p. 24 and corrects two slips in the printed recurrence on p. 25: its next-state subscript and the placement of the mean-cost term. Contributions to the path-law facts, independent-sampling calculations, countable weighted sums, and scalar growth theorem all support the same fixed goal.

Selected references

J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, MIT Laboratory for Information and Decision Systems report LIDS-P-2322, 1996; published in IEEE Transactions on Automatic Control 42(5), 1997. MIT record.

9 thms2 active usersReviewed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

A Coordinate Gradient Descent Method for Nonsmooth Separable Minimization 2: Under a Local Lipschitzian Error Bound, CGD with the Restricted Gauss–Seidel Rule Converges LinearlyResearch Paper

Motivation

Many problems in statistics, signal processing and machine learning minimize the sum of a smooth loss and a convex, nonsmooth, separable regularizer: smooth optimization with $\ell_1$ -regularization, bound-constrained optimization, the group Lasso and, through duality, support vector regression are special cases listed in §1 of the paper discussed below. For such problems, methods that update one coordinate, or one small block of coordinates, at a time are often the method of choice, because each update is cheap and exploits separability.

Paul Tseng and Sangwoon Yun (Math. Program. Ser. B 117 (2009) 387–423) introduced the coordinate gradient descent (CGD) method for this class: at each iteration it minimizes a quadratic model of the smooth part plus the exact nonsmooth part over a chosen block of coordinates, then takes an Armijo step. Their paper proves global convergence (Theorem 1) and, under a local error bound, linear convergence (Theorems 2 and 3). This mission is the second of a three-mission series on the paper; it targets the linear convergence theorem for the cyclic (Gauss–Seidel-type) choice of blocks.

The analysis follows Luo and Tseng's error-bound framework for smooth constrained problems (Ann. Oper. Res. 46 (1993) 157–178), which established linear rates for feasible descent methods without strong convexity. Tseng and Yun extend that framework to a nonsmooth convex term.

Setting

Let $\Re^n$ carry the Euclidean norm $\|\cdot\|$ , let $\mathcal N=\{1,\dots,n\}$ , and for $\mathcal J\subseteq\mathcal N$ let $x_{\mathcal J}$ be the subvector of coordinates in $\mathcal J$ . The problem (1) is

\min_x\ F_c(x)=f(x)+cP(x),

where $c>0$ , $P:\Re^n\to(-\infty,\infty]$ is proper, convex and lower semicontinuous, and $f$ is continuously differentiable on an open set containing $\operatorname{dom}P$ .

Given $x\in\operatorname{dom}P$ , a nonempty block $\mathcal J$ and a symmetric positive definite matrix $H$ , the direction (6) is

d_H(x;\mathcal J)=\arg\min_d\Big\{\nabla f(x)^Td+\tfrac12d^THd+cP(x+d)\ \Big|\ d_j=0\ \forall j\notin\mathcal J\Big\}.

The CGD method starts at $x^0\in\operatorname{dom}P$ , chooses at each iteration $k$ a block $\mathcal J^k$ and a matrix $H^k$ , computes $d^k=d_{H^k}(x^k;\mathcal J^k)$ , and sets $x^{k+1}=x^k+\alpha^kd^k$ . The Armijo rule takes $\alpha^k$ as the largest element of $\{\alpha^k_{\rm init}\beta^j\}_{j\ge0}$ with

F_c(x^k+\alpha^kd^k)\le F_c(x^k)+\alpha^k\sigma\Delta^k,\qquad \Delta^k=\nabla f(x^k)^Td^k+\gamma\,d^{kT}H^kd^k+cP(x^k+d^k)-cP(x^k),

with $0<\beta,\sigma<1$ and $0\le\gamma<1$ . The restricted Gauss–Seidel rule (12) asks for indices $0=t_0<t_1<\cdots$ (the set $\mathcal T$ ) such that the blocks used during each cycle $t_i\le k<t_{i+1}$ are pairwise disjoint and cover $\mathcal N$ . $P$ is block-separable with respect to $\mathcal J$ if $P(x)=P_{\mathcal J}(x_{\mathcal J})+P_{\mathcal J^C}(x_{\mathcal J^C})$ .

The analysis uses three assumptions: $\nabla f$ is $L$ -Lipschitz on $\operatorname{dom}P$ (22); Assumption 1, $\bar\lambda I\succeq H^k\succeq\underline\lambda I$ with $0<\underline\lambda\le\bar\lambda$ ; and Assumption 2. Writing $\bar X$ for the set of stationary points of $F_c$ and $d_I(x)$ for the full direction with $H=I$ , Assumption 2 says (a) $\bar X\ne\emptyset$ and the local Lipschitzian error bound $\operatorname{dist}(x,\bar X)\le\tau\|d_I(x)\|$ holds on every level set $\{F_c\le\zeta\}$ wherever $\|d_I(x)\|\le\epsilon$ ; (b) stationary points with different objective values are at least a fixed distance $\delta>0$ apart.

Formalization targets

Goal: Theorem 2(b)

Under (22), Assumptions 1 and 2, the restricted Gauss–Seidel rule, block-separability of $P$ with respect to every $\mathcal J^k$ , and Armijo steps with $\sup_k\alpha^k_{\rm init}\le1$ and $\inf_k\alpha^k_{\rm init}>0$ :

\{F_c(x^k)\}\downarrow-\infty\quad\text{or}\quad\big(\{F_c(x^k)\}_{\mathcal T}\ \text{Q-linear}\ \text{and}\ \{x^k\}_{\mathcal T}\ \text{R-linear}\big).

No rate constant is fixed: the goal asserts the shape of the convergence, so it is not invalidated by sharper constants.

Milestones

Lemma 4 (Hölder dependence of the subproblem's solution on its linear term), Lemma 5(a) (a per-block variational inequality), Lemma 5(b) (an explicit stepsize at which the Armijo test passes), Theorem 1(f) (Armijo stepsizes bounded away from zero, $\Delta^k\to0$ , $d^k\to0$ ), and Theorem 2(a) (the residual $\|d_I(x^k)\|$ at the start of a cycle is bounded by the step lengths of the cycle).

Significance

Theorem 2(b) gives a linear rate for a block coordinate method on a nonsmooth, possibly nonconvex composite problem without strong convexity: the rate follows from the error bound, which holds for a large class of problems studied in §6 of the paper (the third mission of this series).

The theorem is proved in the paper; none of it has been machine-checked, as far as a search of the Prove2Me library shows. Formalizing it requires a reusable treatment of extended-valued convex functions through their effective domains, of the coordinate-restricted proximal subproblem, and of the Armijo rule for composite objectives. The milestones Lemma 4 and Lemma 5 are self-contained facts about this subproblem and are reusable for other proximal coordinate methods.

Difficulty

The classical route to a linear rate, as in Luo and Tseng's smooth analysis, derives $F_c(x^{k+1})-\bar\upsilon\le\tau'\|x^{k+1}-x^k\|^2$ from the error bound, where $\bar\upsilon$ is the limit value. With a nonsmooth $P$ this inequality is not available: the authors say so on p. 405, and work with $-\Delta^k$ in place of the quadratic term. A second obstacle is that the error bound controls the full residual $d_I(x^k)$ , while each iteration only computes a block direction at a different point; relating the two over a cycle needs the disjointness of the blocks in the restricted rule and block-separability of $P$ . Neither the global analysis nor the error bound alone gives the rate.

Formalization scope

$\Re^n$ is EuclideanSpace ℝ (Fin n), with 0-based coordinates. The extended-valued $P$ is encoded as a pair: its effective domain $D=\operatorname{dom}P$ and its finite values on $D$ , with "proper convex lsc" given by the published definition ProxNewton.Inexact.IsProperClosedConvex; $F_c$ is never evaluated off $D$ , and every statement carries membership in $D$ explicitly. The direction $d_H(x;\mathcal J)$ is the unique minimizer of (6) when $x\in D$ and $H\succ0$ (chosen by Classical.epsilon), and runs of the method carry the minimizer property itself. The Armijo rule takes the first admissible exponent $j$ . $\mathcal T$ is a strictly increasing map $t$ with $t_0=0$ . Stationarity is $F_c'(x;d)\ge0$ for all $d$ , in liminf form. In Assumption 2, $\operatorname{dist}$ is the infimum distance and "for any $\zeta\ge\min F_c$ " is "for every real $\zeta$ " (equivalent, since the condition is empty below $\inf F_c$ ). Q-linear convergence includes convergence of the sequence; R-linear convergence is $\|x^{t_i}-\bar x\|\le Cq^i$ with $q<1$ . The rates in the goal are along $\mathcal T$ , as the paper states.

Explicit choices relative to the printed text:

Theorem 2(a) is corrected. As printed, $\|d_I(x^k)\|\le\sup_j\alpha^j\,C\,r^k$ fails for small constant stepsizes and fails without block-separability (counterexamples in the item's statement). The milestone states $\|d_I(x^k)\|\le\max\{1,\sup_j\alpha^j\}\,C\,r^k$ under block-separability of $P$ with respect to every $\mathcal J^k$ (both are what the paper's proof gives and what Theorem 2(b) supplies), with the iterates in $\operatorname{dom}P$ , and with $C$ quantified before the problem data, so it depends only on $n,L,\underline\lambda,\bar\lambda$ .
Lemma 5(b)'s range $0\le\alpha\le\min\{1,2\underline\lambda(1-\sigma+\sigma\gamma)/L\}$ is stated as $0\le\alpha\le1$ and $\alpha L\le2\underline\lambda(1-\sigma+\sigma\gamma)$ , so that $L=0$ gives $[0,1]$ as on paper rather than $\{0\}$ .
Lemma 5(a) holds for every decomposition of $P$ in (20), and $\bar x$ ranges over $\operatorname{dom}P_{\mathcal J}$ (outside it the left side is $-\infty$ ).
" $\lim F_c(x^k)>-\infty$ " is "the values $F_c(x^k)$ are bounded below"; " $\{F_c(x^k)\}\downarrow-\infty$ " is "nonincreasing and tending to $-\infty$ "; suprema and infima of stepsizes are explicit bounds.

A statement that replaces Assumption 2 by strong convexity, claims a rate along the whole sequence rather than along $\mathcal T$ , or asserts the Q-linear contraction without convergence to a limit is not this theorem and is out of scope.

Lemma 1, the claim after (10), Lemma 3 and Theorem 1(a), which the proof also uses, are milestones of the first mission of this series and are not restated here. Theorem 3 (the same conclusion along the whole sequence for the Gauss–Southwell-q rule) is not included: its proof is omitted in the paper. Contributions welcome: proofs of the milestones, and general facts about the coordinate-restricted proximal subproblem (existence and uniqueness of $d_H(x;\mathcal J)$ , optimality conditions) that the milestones rely on.

Selected references

P. Tseng and S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming Ser. B 117 (2009) 387–423. https://doi.org/10.1007/s10107-007-0170-0
Z.-Q. Luo and P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
J. M. Ortega and W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970, Chap. 9 (Q- and R-linear convergence). https://doi.org/10.1137/1.9780898719468
R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

9 thms2 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Consistent Nonparametric Regression II: Nearest-Neighbor Weights with Vanishing Coefficients Are Consistent for Every Distribution of X (Theorem 2)Research Paper

Motivation

Nonparametric regression estimates the regression function $x \mapsto E(Y \mid X = x)$ from i.i.d. observations $(X_1, Y_1), \dots, (X_n, Y_n)$ without assuming a parametric form. The simplest such estimates are local averages: to predict at a point $X$ , average the responses $Y_i$ of the sample points closest to $X$ . Nearest neighbor rules of this kind go back to Fix and Hodges (1951) for classification and are still a standard baseline in statistics and machine learning.

Before 1977, consistency results for such estimates assumed regularity of the distribution of $X$ : a density, continuity of the regression function, or bounded support. C. J. Stone's paper Consistent nonparametric regression (Ann. Statist. 5 (1977) 595–645) proved that suitable nearest neighbor estimates are consistent in $L^r$ for every joint distribution of $(X, Y)$ with $E|Y|^r < \infty$ . This property, now called universal consistency, is the subject of the first chapters of Györfi, Kohler, Krzyżak and Walk, A Distribution-Free Theory of Nonparametric Regression (Springer, 2002), where Stone's theorem is the organising result.

This mission formalizes Theorem 2 of Stone's paper, the universal consistency of nearest neighbor weights. Mission I of the series formalizes the general criterion (Theorem 1) that the proof applies; mission III treats conditional quantiles.

Setting

Let $X, X_1, X_2, \dots$ be i.i.d. random vectors in $\mathbb R^d$ with an arbitrary law $\mu$ . A weight function $W_n$ assigns to the query point $X$ and the sample numbers $W_{ni}(X) = W_{ni}(X, X_1, \dots, X_n)$ , $1 \le i \le n$ . It is a probability weight function if $W_{ni} \ge 0$ and $\sum_i W_{ni}(X) = 1$ . Given i.i.d. pairs $(X, Y), (X_1, Y_1), \dots$ with $Y$ real, the estimate of $E(Y \mid X)$ is

\hat E_n(Y \mid X) = \sum_{i=1}^n W_{ni}(X)\, Y_i .

The sequence $\{W_n\}$ is consistent if, whenever the pairs are i.i.d. with the given law of $X$ , $r \ge 1$ and $E|Y|^r < \infty$ , one has $E|\hat E_n(Y\mid X) - E(Y\mid X)|^r \to 0$ .

Scales and metrics. A scale is a nonnegative function $s_{nj} = s_{nj}(X, X_1, \dots, X_n)$ , $1 \le j \le d$ , and its pseudometric is

\rho_n(u, v) = \Big(\sum_{j:\, s_{nj} > 0} \Big(\frac{u_j - v_j}{s_{nj}}\Big)^2\Big)^{1/2}.

The choice $s_{nj} \equiv 1$ gives the Euclidean metric; the sample standard deviations of the coordinates give a unit-free one. The sequence $\{s_n\}$ is regular (p. 599) with constants $0 < a \le b$ if $P(s_{nj} > 0) \to 1$ for every coordinate of $X$ with a nondegenerate law, $s_{nj}/s_{nl}$ is bounded in probability for any two such coordinates, and condition (7) holds: interchanging $X$ and $X_i$ changes $s_{nj}$ by a factor in $[a, b]$ whenever the $j$ th coordinates of $X_1, \dots, X_n$ do not all coincide.

Nearest neighbor weights. Let $c_{n1} \ge \dots \ge c_{nn} \ge 0$ with $\sum_i c_{ni} = 1$ and $c_{ni} = 0$ for $i > n$ . The weight of $X_i$ is

W_{ni}(X) = \frac{c_{n\nu} + \dots + c_{n,\nu+\lambda-1}}{\lambda},

where $\nu - 1$ is the number of other sample points strictly $\rho_n$ -closer to $X$ than $X_i$ and $\lambda - 1$ the number at the same distance: the $k$ th closest point receives $c_{nk}$ , and tied points share the average of the coefficients of their ranks. The uniform $k$ -NN rule is $c_{ni} = 1/k$ for $i \le k$ .

Formalization targets

Goal: Theorem 2 (p. 600)

For every law $\mu$ of $X$ and every regular sequence of scales,

\lim_{n} \sum_{i > \alpha n} c_{ni} = 0 \ \ (\forall \alpha > 0) \quad\text{and}\quad \lim_n c_{n1} = 0 \quad\Longrightarrow\quad \{W_n\} \text{ is consistent.}

Uniform, triangular and quadratic $k_n$ -NN weights with $k_n \to \infty$ , $k_n / n \to 0$ satisfy both conditions (Corollary 3).

Milestones

Corollary 1 (sufficiency), p. 598. Probability weights with $E\sum_i W_{ni}(X) f(X_i) \le C\,Ef(X)$ for some $C \ge 1$ and all nonnegative Borel $f$ , with $\sum_i W_{ni}(X) I_{\{\|X_i - X\| > a\}} \to 0$ and $\max_i W_{ni}(X) \to 0$ in probability, are consistent.
Proposition 9, p. 611. For every $\delta > 0$ , $\lim_{\alpha\downarrow 0}\limsup_n P(\max_{i \in I_{n,\alpha n}(X)} \|X_i - X\| > \delta) = 0$ , where $I_{n,t}(X)$ are the indices of the $\lfloor t \rfloor$ nearest neighbors (with ties).
Proposition 10, p. 613. For $0 < a \le b_j \le b$ , two vectors $0 < \|u\| \le \|v\|$ in a set $V \in \mathcal V(d, a/b)$ satisfy $\|\tilde v\| > \|\tilde v - \tilde u\|$ after rescaling $\tilde u_j = b_j u_j$ , $\tilde v_j = b_j v_j$ . Here $\mathcal V(d, c)$ is the family of sets in which any two nonzero vectors satisfy $u\cdot v > (1 - c^2/2)\|u\|\|v\|$ , and $\beta(d, c)$ is the least number of members of $\mathcal V(d,c)$ covering $\mathbb R^d$ .
Proposition 12, p. 613. For fixed points, the swapped weights $U_{ni}(X) = W_{ni}(X_i, X_1, \dots, X, \dots, X_n)$ satisfy $\sum_i U_{ni}(X) \le \beta(d, a/b)$ .
Proposition 11, p. 613. $E \sum_i W_{ni}(X) f(X_i) \le \beta(d, a/b)\, Ef(X)$ for nonnegative Borel $f$ with $Ef(X) < \infty$ .

Significance

Theorem 2 established that a local averaging estimate can be consistent with no assumption on the distribution of $X$ beyond the moment condition on $Y$ . The same argument, through Theorem 1, became the standard template for proving universal consistency of kernel, partitioning and nearest neighbor estimates, and of the classification rules derived from them (Devroye, Györfi and Lugosi, A Probabilistic Theory of Pattern Recognition, 1996). The constant $\beta(d, a/b)$ of Proposition 11 is an early instance of the cone-covering bound on how many points can have a given point among their nearest neighbors, a lemma that reappears throughout nearest neighbor theory.

The result is proved (1977), and textbook proofs exist. Mathlib contains no formalization of Theorem 2, of Stone's criterion, or of the cone-covering lemma. A formal development would supply reusable infrastructure: nearest neighbor weights with averaged ties, the exchangeability argument behind Proposition 11, and $L^r$ consistency of weighted averages for i.i.d. data encoded through kernels.

Difficulty

The obvious argument estimates $\hat E_n(Y\mid X)$ by a continuity argument around $X$ , which needs a density or continuity of $E(Y\mid X)$ and is unavailable here. The difficulty is condition (1) of Stone's criterion: a single sample point may be a nearest neighbor of many query points, so $E\sum_i W_{ni}(X) f(X_i)$ is not obviously comparable to $Ef(X)$ for arbitrary $f$ and arbitrary $\mu$ (atoms, singular parts, unbounded support). The bound must hold uniformly in $n$ and in the distribution, with a data-dependent metric whose scale changes when $X$ and $X_i$ are interchanged. Ties in $\rho_n$ , which have positive probability when $\mu$ has atoms, must be handled by the averaged weights (8), not by an index tie-break.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). The i.i.d. sequence is the coordinate process of Measure.infinitePi, coordinate 0 being $X$ ; sample indices are 0-based, coefficients $c_{n,m}$ keep the paper's 1-based index. "Whenever the pairs are i.i.d." is encoded by quantifying over every Markov kernel $\kappa$ (the conditional law of $Y$ given $X$ ), with pairs distributed as $(\mu \otimes \kappa)^{\otimes\mathbb N}$ and $E(Y\mid X=x) = \int y\,\kappa(x, dy)$ . Expectations of nonnegative quantities are lower Lebesgue integrals in $[0,\infty]$ ; convergence in probability is TendstoInMeasure; limits of probabilities are taken in $[0,\infty]$ .

Standing assumptions and additions, each disclosed in the item statements:

the scales are regular (the standing assumption of §3, p. 599) and Borel measurable (added; the paper treats them as random variables);
condition (7) is read for all points, as Proposition 12's proof uses it, and "do not coincide" means "are not all equal";
"nondegenerate" means the coordinate's law is not a point mass; $s_{nj}/s_{nl}$ is real division ( $0$ where $s_{nl} = 0$ , an event of vanishing probability);
Corollary 1's weights are assumed jointly Borel;
Proposition 9's distance $a$ is renamed $\delta$ , and the maximum over an empty index set is read as "no index";
$\beta(d, c)$ is an infimum over $\mathbb N$ ; that a finite cover exists is part of the work, not an assumption.

No statement corrects the print.

The goal is stated as $L^r$ consistency over all kernels and all $r \ge 1$ , for an unrestricted law $\mu$ : it is not stated through Corollary 1's three conditions nor through $\beta$ , and no density, moment or support hypothesis on $X$ is present, so a proof cannot reduce to a special case.

A complete development needs: exchangeability of finite i.i.d. samples under the product measure, the finite cone cover of $\mathbb R^d$ , the strong law of large numbers (Proposition 9's proof), and Stone's criterion (mission I). Contributions proving any milestone, the cone-cover existence lemma, or the transfer of exchangeability through infinitePi are welcome.

Selected references

C. J. Stone, Consistent nonparametric regression, Ann. Statist. 5(4) (1977) 595–645. https://doi.org/10.1214/aos/1176343886
L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5
E. Fix, J. L. Hodges, Discriminatory analysis. Nonparametric discrimination: consistency properties, USAF School of Aviation Medicine, Report 4, 1951; reprinted in Int. Stat. Rev. 57(3) (1989) 238–247. https://doi.org/10.2307/1403797

8 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

The Primal-Dual Active Set Strategy as a Semismooth Newton Method II: Global Convergence and Monotonicity for M-MatricesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 (p. 7)

Milestones (Appendix A, p. 20)

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

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

Selected references

Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion 3: With Random Right-Hand Side and Known Dual Extreme Points, the Problem Equals the Semidefinite Program (14)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 (p. 589)

Milestones (§3.1 and the proof of Theorem 3.2, pp. 588–590)

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: the approximation is an upper bound

Milestones

Further result: the MIP represents the approximation

Significance

Difficulty

Formalization scope

Selected references

Designing a Call Center with Impatient Customers III: Square-Root Staffing Is Equivalent to a Nondegenerate Delay Probability and to Abandonment of Order 1/√NResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 219)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Sample Average Approximation Method for Stochastic Discrete Optimization 2: √N(v̂_N − v*) Converges in Distribution to the Minimum over S* of a Centered Gaussian VectorResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.3, (2.8)

Milestones (in the order of the paper's argument)

Companions

Significance

Difficulty

Formalization scope

Selected references

Uncoupled Dynamics Do Not Lead to Nash Equilibrium 1: Near the Two-Player Unit-Disk Game Γ₀ of Section II, No Uncoupled Dynamic Is Nash-ConvergentResearch Paper

Motivation

The Sample Average Approximation Method for Stochastic Discrete Optimization 2: √N(v̂_N − v) Converges in Distribution to the Minimum over S of a Centered Gaussian VectorResearch Paper

Goal: THEOREM 1 for the game $\Gamma_0$ of §II