Operations Research

Completed

Algorithmic Game Theory·Captain: mikedeng1

Potential Games 4: An Efficient Solution Is the Shapley Value on the Subgames of v If and Only If the Participation Game Γ(ψ, c, v) Is a Potential GameResearch Paper

Motivation

The Shapley value (Shapley 1953) is the most widely used single-valued solution of cooperative games with transferable utility. It is usually justified axiomatically, from cooperative principles. A recurring question in game theory, sometimes called the Nash program, asks whether cooperative solution concepts can also be recovered from the strategic behaviour of players in a non-cooperative game.

Section 6 of Monderer and Shapley, Potential Games (Games and Economic Behavior 14, 1996), gives such a recovery through the notion of a potential game, the central object of that paper. With every solution $\psi$ , vector of outside options $c$ and TU game $v$ it associates a simple non-cooperative participation game, in which each player decides whether to join. The Shapley value is then characterised, among efficient solutions, as exactly the solution for which every such participation game is a potential game. The characterisation rests on the potential of a TU game introduced by Hart and Mas-Colell (1989), whose marginal contributions are the Shapley value; Monderer and Shapley connect that cooperative potential to the strategic one of their paper.

Setting

Let $N = \{1, \dots, n\}$ be a finite set of players.

A game in strategic form $\Gamma(u^1, \dots, u^n)$ has strategy sets $Y^i$ and payoff functions $u^i : Y \to \mathbb R$ on $Y = Y^1 \times \dots \times Y^n$ . Writing $(y^{-i}, x)$ for the profile $y$ with player $i$ 's strategy replaced by $x$ , a function $P : Y \to \mathbb R$ is an exact potential if

u^i(y^{-i}, x) - u^i(y^{-i}, z) = P(y^{-i}, x) - P(y^{-i}, z)

for every $i$ , every $y^{-i}$ and all $x, z \in Y^i$ (condition (2.2) with unit weights). A game with an exact potential is a potential game.

For a coalition $S \subseteq N$ , $G(S)$ is the space of TU games on $S$ : real functions $v$ on the subsets of $S$ with $v(\emptyset) = 0$ . A solution $\psi$ assigns to every $v \in G(S)$ a payoff vector $\psi(v) \in \mathbb R^S$ . It is efficient if $\sum_{i \in S} \psi(v)(i) = v(S)$ for every $S$ and every $v \in G(S)$ . For $v \in G(N)$ , $v_S \in G(S)$ is its restriction to the subsets of $S$ . The Shapley value of $w \in G(S)$ is

\varphi_i(w) = \sum_{T \subseteq S \setminus \{i\}} \frac{|T|!\,(|S|-|T|-1)!}{|S|!}\bigl(w(T \cup \{i\}) - w(T)\bigr), \qquad i \in S.

Given a solution $\psi$ , a vector $c \in \mathbb R^N$ and $v \in G(N)$ , the participation game $\Gamma(\psi, c, v)$ has player set $N$ and strategy sets $Y^i = \{0, 1\}$ . Player $i$ either stays out (0) and receives $c^i$ , or participates (1). With $S(\varepsilon) = \{i : \varepsilon^i = 1\}$ the set of participants at the profile $\varepsilon$ ,

u^i(\varepsilon) = \begin{cases} c^i, & \varepsilon^i = 0,\\ \psi(v_{S(\varepsilon)})(i), & \varepsilon^i = 1.\end{cases}

For $S \subseteq N$ , $\varepsilon_S$ is the profile in which exactly the members of $S$ participate.

In Lean these are IsPotential, IsPotentialGame, Solution, IsEfficient, shapleyOn, joiners ( $S(\varepsilon)$ ), profileOf ( $\varepsilon_S$ ) and participationPayoff, all in the namespace MondererShapley.Participation.

Formalization targets

Goal: Theorem 6.1 (p. 137)

For every efficient solution $\psi$ , every $c \in \mathbb R^N$ and every $v \in G(N)$ ,

\psi(v_S)(i) = \varphi_i(v_S)\ \ \forall S \subseteq N,\ \forall i \in S \quad\Longleftrightarrow\quad \Gamma(\psi, c, v)\ \text{is a potential game}.

Milestones (proof of Theorem 6.1, p. 137)

(6.1) For every $i$ and $\varepsilon$ , with $S = \{j \ne i : \varepsilon^j = 1\}$ ,

u^i(\varepsilon^{-i}, 1) - u^i(\varepsilon^{-i}, 0) = \psi(v_{S \cup \{i\}})(i) - c^i.

(6.2) $\Gamma(\psi, c, v)$ is a potential game iff there is $Q : Y \to \mathbb R$ with $Q(\varepsilon_S) - Q(\varepsilon_{S \setminus \{i\}}) = \psi(v_{S\cup\{i\}})(i) - c^i$ for every $S$ and $i \in S$ .
(6.3) With $P(\varepsilon_S) = Q(\varepsilon_S) + \sum_{i \in S} c^i$ , $Q$ satisfies (6.2) iff $P(\varepsilon_S) - P(\varepsilon_{S\setminus\{i\}}) = \psi(v_{S\cup\{i\}})(i)$ for every $S$ and $i \in S$ .
The last step of the proof. For efficient $\psi$ and $v \in G(N)$ , a function $P$ on coalitions satisfying (6.3) exists iff $\psi(v_S)(i) = \varphi_i(v_S)$ for all $S$ and $i \in S$ . The paper obtains this from Theorem A of Hart and Mas-Colell (1989); that theorem is not a result of this paper.

Further: Theorem 6.2 (p. 137)

An efficient $\psi$ is the Shapley value on all of $G = \bigcup_S G(S)$ iff $\Gamma(\psi, c, v)$ is a potential game for every $v \in G(N)$ .

Significance

Theorem 6.1 is a local characterisation: for a single game $v$ it identifies the Shapley value of all subgames of $v$ through a property of one non-cooperative game, for any outside options $c$ . Theorem 6.2 turns it into a global axiomatisation of the Shapley value among efficient solutions, with "every participation game has a potential" in place of the usual symmetry, null-player and additivity axioms. It links the cooperative potential of Hart and Mas-Colell to the strategic potentials of Monderer and Shapley, and through the latter to the existence of pure equilibria and the convergence of improvement dynamics in the participation games.

Both theorems are proved in the paper, on the basis of Hart and Mas-Colell's Theorem A. To the curators' knowledge no machine-checked proof exists: neither the Hart–Mas-Colell potential nor its identification with the Shapley value of subgames is formalized on Prove2Me or in Mathlib. A complete development therefore formalizes the paper's reduction (milestones 1–3) and, as its substantial part, the Hart–Mas-Colell characterisation (milestone 4), which is reusable for any later work on cooperative potentials, consistency and the Shapley value.

Difficulty

Milestones 1–3 are bookkeeping on profiles in $\{0,1\}^N$ ; the obstacle is the identification of the potential of a game on $\{0,1\}^N$ with a function of coalitions, which is a translation between two indexings rather than an idea. The substance is milestone 4, which is Hart and Mas-Colell's Theorem A specialised to the subgames $v_S$ . The condition (6.3) speaks of marginal differences of an unknown function on coalitions, while the Shapley value is a closed weighted sum over subsets of $S$ whose weights depend on $|S|$ ; relating the two requires a genuine combinatorial identity over the subset lattice of every coalition, in both directions, and efficiency of $\psi$ on every subgame is used essentially. Unfolding the definitions does not suffice for either direction.

Formalization scope

Players are a finite type ι with decidable equality; the strategy set $\{0,1\}$ is Bool (false = 0, true = 1). $(\varepsilon^{-i}, x)$ is Function.update ε i x.
A coalition is a Finset ι; a TU game is w : Finset ι → ℝ, with " $w \in G(S)$ " encoded as w ∅ = 0 and only the values on subsets of $S$ meant. A solution is ψ : Finset ι → (Finset ι → ℝ) → ι → ℝ, ψ S w standing for $\psi(w|_{2^S})$ ; only the coordinates $i \in S$ are read. This admits solutions that look at values of w outside $2^S$ , so the Lean statements cover every solution of the paper and more; " $\psi$ is the Shapley value on $\{v_S\}$ " is ∀ S, ∀ i ∈ S, ψ S v i = shapleyOn S v i.
Efficiency is required for every coalition and every game, not only for $v$ , as in the paper.
The Shapley value formula shapleyOn is supplied: the paper uses the Shapley value without defining it. Its weights use $|S|$ , the size of the subgame's player set.
The page writes $\psi(v_{S\cup\{i\}})$ with $i \in S$ in (6.2) and (6.3); this equals $\psi(v_S)$ and is kept literally. The $P$ of (6.3) is stated as a function of coalitions, $P(S)$ for the page's $P(\varepsilon_S)$ .
The outside options $c$ are arbitrary reals; no sign or normalisation is assumed.
Trivializations ruled out: $\psi$ is an arbitrary efficient solution, never replaced by the Shapley value itself; v ∅ = 0 is kept as the meaning of $v \in G(N)$ (without it, efficiency does not constrain ψ S v); and the potential is an exact potential on all of $\{0,1\}^N$ , not only on profiles of a special form.
Welcome contributions: a general Hart–Mas-Colell potential for TU games, with its uniqueness and its identification with the Shapley value, stated so that it applies to subgames; proofs of milestones 1–3; Theorem 6.2 from Theorem 6.1.
Not included: Theorem 6.3 (weighted Shapley values), for which the paper gives no proof and does not define the weighted value.

Selected references

D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
S. Hart and A. Mas-Colell, Potential, Value, and Consistency, Econometrica 57 (1989), 589–614. https://doi.org/10.2307/1911054
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press (1953), 307–317. https://doi.org/10.1515/9781400881970-018

13 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 5: Nonquadratic Proximal Methods of Multipliers Converge to a Saddle PointResearch Paper

Motivation

The method of multipliers (augmented Lagrangian method) solves a constrained convex program by alternating an unconstrained minimization in the primal variables with an explicit update of the Lagrange multipliers. Rockafellar showed in 1976 that the classical quadratic version is the proximal point algorithm applied to the dual problem, and that a variant which also adds a proximal term in the primal variables, the proximal method of multipliers, is the proximal point algorithm applied to the saddle operator of the Lagrangian (Rockafellar 1976, Math. Oper. Res.). The primal proximal term makes each subproblem strictly convex, so its minimizer is unique, and the theory gives convergence of the primal and dual iterates together.

Penalty functions other than the quadratic one, such as the exponential multiplier method, were used in practice and studied by Bertsekas, Kort and Tseng, but their convergence theory was separate from the proximal point framework. Eckstein's 1993 paper (Math. Oper. Res. 18(1), 202–226) replaces the squared distance in the proximal point algorithm by the D-function of a Bregman function. Its §5 obtains the first nonquadratic generalization of the proximal method of multipliers and proves that it converges to a saddle point. This mission formalizes that theorem, Theorem 8.

1967: Bregman introduces D-functions for convex feasibility (Bregman 1967).
1976: Rockafellar proves convergence of the quadratic method of multipliers and the proximal method of multipliers via the proximal point algorithm.
1990–1992: Censor and Zenios propose the proximal minimization algorithm with D-functions.
1993: Eckstein proves convergence of the Bregman proximal point algorithm for maximal monotone operators (Theorem 1) and derives nonquadratic multiplier methods (Theorems 6–8).

Setting

A convex program of the form (10) is

\min f(x)\quad\text{subject to}\quad g_i(x)\le0\ (i=1,\dots,m),\ x\in C,

where $C\subseteq\mathbb R^n$ is closed, nonempty and convex, and $f,g_1,\dots,g_m:\mathbb R^n\to(-\infty,+\infty]$ are proper lower semicontinuous convex functions, finite on $C$ . Write $g(x)=(g_1(x),\dots,g_m(x))$ and $\overline{\Omega^+}=\{p\in\mathbb R^m:p\ge0\}$ . The Lagrangian is $l(x,p)=f(x)+\sum_ip_ig_i(x)$ for $x\in C$ , $p\ge0$ ; $l(x,p)=-\infty$ for $x\in C$ , $p\not\ge0$ ; $l(x,p)=+\infty$ for $x\notin C$ . A saddle pair $(x^*,p^*)$ satisfies $l(x^*,p)\le l(x^*,p^*)\le l(x,p^*)$ for all $x,p$ ; the paper calls these optimal solution–Lagrange multiplier pairs. The saddle operator on $\mathbb R^{n+m}$ is $K(x,p)=\partial_xl(x,p)\times(-\hat\partial_pl(x,p))$ , where $\partial_x$ is the subdifferential of the convex function $l(\cdot,p)$ and $\hat\partial_p$ the set of supergradients of the concave function $l(x,\cdot)$ .

For a differentiable $h$ , the D-function is $D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle$ . A Bregman function with open zone $S$ is a function $h:\overline S\to\mathbb R$ , continuously differentiable on $S$ , strictly convex and continuous on $\overline S$ , whose partial level sets of $D_h$ are bounded, and which satisfies two sequential conditions relating $D_h\to0$ to convergence (Definition 1). For $h:\mathbb R^m\to\mathbb R$ , the monotone conjugate is $h^{*+}(z)=\sup_{p\ge0}\{\langle p,z\rangle-h(p)\}$ .

Given Bregman functions $h_x$ on $\mathbb R^n$ and $h_p$ on $\mathbb R^m$ and step sizes $c_k>0$ , the nonquadratic proximal method of multipliers (12) is

x^{k+1}=\arg\min_{x\in C}\Big\{f(x)+\tfrac1{c_k}h_p^{*+}\big(\nabla h_p(p^k)+c_kg(x)\big)+\tfrac1{c_k}D_{h_x}(x,x^k)\Big\},\qquad p^{k+1}=\nabla h_p^{*+}\big(\nabla h_p(p^k)+c_kg(x^{k+1})\big).

Formalization targets

Goal: Theorem 8

Assume $c_k$ positive and bounded away from zero, $h_x$ a Bregman function with zone $S_x\supseteq C$ , $h_p$ a Bregman function with zone $S_p\supseteq\overline{\Omega^+}$ and $\operatorname{im}\nabla h_p=\mathbb R^m$ , and $\{(x^k,p^k)\}$ conforming to (12). Then

\exists\text{ saddle pair}\ \Longrightarrow\ (x^k,p^k)\to(x^*,p^*)\ \text{for some saddle pair }(x^*,p^*),

\nexists\text{ saddle pair}\ \Longrightarrow\ \{x^k\}\text{ or }\{p^k\}\text{ is unbounded}.

Existence clause

For the same step-size assumption, if in addition $\operatorname{im}\nabla h_x=\mathbb R^n$ , a sequence conforming to (12) exists from every $(x^0,p^0)\in C\times\overline{\Omega^+}$ . This is the third sentence of Theorem 8, stated as a separate item.

Milestones

Lemma 2 (four descriptions of $h^{*+}$ , monotonicity), Lemma 3 ( $h^{*+}$ finite and differentiable), Lemma A4 (a subdifferential chain rule), (14) (the $x$ -step is a Bregman proximal step on $\partial_xl$ ), the formula $\hat\partial_pl(x,p)=\{g(x)\}-\partial\delta^+(p)$ , maximal monotonicity of $K$ , saddle pairs $=$ zeros of $K$ , $h_x\oplus h_p$ is a Bregman function with zone $S_x\times S_p\supseteq\overline{\operatorname{dom}K}$ , the identity (13), Theorem 1 restated on $\mathbb R^{n+m}$ , Theorem 4 restated, and the existence clause.

Significance

Theorem 8 gives a family of primal–dual methods for convex programs, parametrized by two Bregman functions, each with the convergence guarantee of the quadratic proximal method of multipliers: convergence of both sequences to a saddle point when one exists, and divergence otherwise. Choosing $h_p$ to match the orthant (for instance entropy-like functions) yields exponential-type multiplier updates, and choosing $h_x$ to match $C$ adapts the primal regularization to the feasible set. The uniqueness of the primal minimizer, which the dual method of §4.2 lacks, is what allows convergence of the primal iterates without further assumptions.

The result is proved in the paper, with some steps asserted rather than proved (that $h_x\oplus h_p$ is a Bregman function; the maximality of $K$ , cited from Rockafellar). No machine-checked proof of Theorem 8, of Theorem 1, or of the monotone-conjugate lemmas is known. A formalization would check the reduction of (12) to (13) carefully, including the extended-value conventions of the Lagrangian, and would provide reusable statements about Bregman functions on product spaces and about saddle operators of convex programs.

Difficulty

The reduction of Theorem 8 to Theorem 1 is short on the page but uses several nontrivial facts. The $x$ -step is a constrained minimization of a composite function; turning its optimality condition into the inclusion (14) in $\partial_xl(x^{k+1},p^{k+1})$ needs a chain rule for a nondecreasing differentiable outer function composed with extended-valued convex functions (Lemma A4), together with properties of the monotone conjugate (Lemmas 2 and 3) that rest on recession arguments in the Appendix. The $p$ -step requires identifying $\partial[h_p^{*+}]^*$ with $\nabla h_p+\partial\delta^+$ , which uses $S_p\supseteq\overline{\Omega^+}$ . Maximal monotonicity of $K$ is a theorem about closed saddle functions, not a consequence of monotonicity alone. Theorem 1 itself is the main theorem of the paper and depends on all six conditions of Definition 1.

A natural first idea, applying Theorem 1 to $K$ directly with an arbitrary Bregman function on $\mathbb R^{n+m}$ , does not describe (12): the method is the specific instance $h=h_x\oplus h_p$ , and the identification of its steps with $(\nabla h+c_kK)^{-1}$ is the content of (13).

Formalization scope

$\mathbb R^k$ is EuclideanSpace ℝ (Fin k); $\mathbb R^{n+m}$ is WithLp 2 (E n × E m), which carries the Euclidean inner product. The §2 objects (Bregman function, $D_h$ , runs of (3) written through the equivalent inclusion (4)) are defined over any finite-dimensional real inner product space so that Theorem 1 applies on $\mathbb R^{n+m}$ .
Extended-real functions are EReal-valued; properness, convexity (of the epigraph) and subgradients use published definitions. $h_p^{*+}$ is EReal-valued; the recursion (12) uses its real value and the gradient of that real function, which is exact because Lemma 3, a milestone, proves finiteness and differentiability.
"Optimal solution–Lagrange multiplier pair" is the saddle inequality, as identified on p. 220. "Converges to one" means both sequences converge, to the two components of one saddle pair; "unbounded" means the range is not bounded.
The $x$ -step is a minimality predicate over $C$ rather than $\arg\min$ (equivalent; the minimizer is unique). A run requires $x^0\in S_x$ , not $x^0\in C$ , and $p^k\in S_p$ , so that every gradient in (12) is defined.
Corrected typos: the page's " $S_p\supset\overline{\Omega^+}$ " is read as $\supseteq$ ; in Lemma A4, "Lemma 5" is Lemma 2 and " $f(x)\in\mathbb R^n$ " is $\mathbb R^m$ ; Theorem 1's "monontone" is monotone; the supergradient formula's " $\delta^+(p)$ " denotes $\partial\delta^+(p)$ ; the existence clause's extra parenthesis is dropped. In Lemma A4 a term $y_i\partial f_i(x^0)$ with $y_i=0$ is $\{0\}$ , following the proof.
The §4.2 assumption that the dual functional is not everywhere $-\infty$ is not assumed; §5 does not use it.
A trivializing formalization is ruled out: the goal's hypotheses are satisfiable (with $h_x=h_p=\frac12\|\cdot\|^2$ , $C=\mathbb R$ , $f(x)=x^2$ , $g_1(x)=x-1$ there is a saddle pair, checked in Lean), $h^{*+}$ is not replaced by a real supremum with junk values, and the saddle predicate quantifies over all of $\mathbb R^n\times\mathbb R^m$ .
Infrastructure a full development needs: Bregman functions on products, the monotone conjugate and its smoothness, a subdifferential sum and chain rule for extended-valued functions, maximal monotonicity of saddle operators, and Theorem 1. The monotone conjugate lemmas and Theorem 1 are shared with the companion missions of this series. Contributions to any milestone are welcome, including proofs of the restated Theorems 1 and 4 independent of the companion missions.

Selected references

J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 1993, 202–226. https://doi.org/10.1287/moor.18.1.202
R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1(2), 1976, 97–116. https://doi.org/10.1287/moor.1.2.97
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3), 1967, 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
Y. Censor and S. A. Zenios, Proximal minimization algorithm with D-functions, Journal of Optimization Theory and Applications 73(3), 1992, 451–464. https://doi.org/10.1007/BF00940051

18 thms2 active usersReviewed

Algorithmic Game Theory Analysis Optimization·Captain: mikedeng1

Cooperative Fuzzy Games 3: The Diagonal Formula Is the Unique Continuous Linear Pareto-Optimal, Symmetric and Atomic Value of Smooth Fuzzy GamesResearch Paper

Motivation

A value for cooperative games assigns to every game a payoff vector, chosen by axioms rather than by bargaining. Shapley's value (1953) does this for finite games with side payments, and Aumann and Shapley (Values of Non-Atomic Games, 1974) extended it to games with a continuum of players, where it is given by a diagonal formula: a player's value is the average of their marginal worth along the diagonal from the empty coalition to the grand coalition. Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981, doi:10.1287/moor.6.1.1) brings this formula to finitely many players who may participate in coalitions at fractional rates, and characterises it by axioms in §8.

The result matters in cost allocation: the Aumann–Shapley price mechanism (Billera, Heath and Raanan 1978; Mirman and Tauman 1982) shares the cost of a bundle of products by exactly this diagonal formula, applied to a smooth cost function of the quantities produced. Theorem 8.1 is the finite-player, fuzzy-coalition version of the axiomatic justification behind that mechanism.

Setting

There are $n$ players $N=\{1,\dots,n\}$ . A fuzzy coalition is a vector $\tau\in[0,1]^n$ , where $\tau_i$ is the rate at which player $i$ participates; an ordinary coalition $A$ is its indicator vector $\tau^A$ , and $\tau^N=(1,\dots,1)$ is the grand coalition.

A smooth fuzzy game is a coalitional worth function $v:[0,1]^n\to\mathbb R$ that is continuously differentiable and satisfies $v(0)=0$ . These form the space $V^n$ , a Banach space under the $C^1$ norm $\sup_{[0,1]^n}|v|+\sup_{[0,1]^n}\|Dv\|$ .

A sequence of fuzzy values is a family of continuous linear operators $\psi_n:V^n\to\mathbb R^n$ satisfying three axioms.

Pareto optimality: $\sum_{i\in N}(\psi_n v)_i=v(\tau^N)$ .
Symmetry: for a permutation $\theta$ of $N$ , with $(\theta^*v)(\tau)=v(\tau_{\theta^{-1}(1)},\dots,\tau_{\theta^{-1}(n)})$ and $(\theta^*c)_i=c_{\theta(i)}$ , one has $\psi_n(\theta^*v)=\theta^*(\psi_n v)$ .
Atomicity: a partition $P=\{A_1,\dots,A_m\}$ of $N$ into nonempty types sends a fuzzy coalition $\sigma\in[0,1]^m$ of types to the fuzzy coalition $(P\cdot\sigma)_i=\sigma_j$ for $i\in A_j$ , and an $n$ -player game $v$ to the $m$ -type game $(P^*v)(\sigma)=v(P\cdot\sigma)$ . The axiom requires $\psi_m(P^*v)_j=\sum_{i\in A_j}(\psi_nv)_i$ : a type receives what its members receive.

The core of a game $v$ with side payments is the set of $c\in\mathbb R^n$ with $\sum_ic_i=v(\tau^N)$ and $\sum_i\tau_ic_i\ge v(\tau)$ for every $\tau\in[0,1]^n$ (§2 (4)).

Formalization targets

Goal: Theorem 8.1

There exists a unique sequence of fuzzy values, given by the diagonal formula

\psi_n v=\int_0^1 Dv(t\tau^N)\,dt\qquad(v\in V^n).\tag{4}

For every linear $A:\mathbb R^m\to\mathbb R^n$ with $A\tau^M=\tau^N$ ,

\psi_m(v\circ A)=A^*\psi_n v\qquad(v\in V^n),\tag{5}

where $A^*$ is the transpose of $A$ . If $v\in V^n$ is concave and positively homogeneous, then $\psi_nv$ is the unique element of the core.

Milestones

These are the steps of the proof in the paper (pp. 10–11), in attack order:

the maps (4) are linear, continuous and satisfy (5);
they satisfy the Pareto optimality, symmetry and atomicity axioms;
the monomials $\tau_1^{k_1}\cdots\tau_n^{k_n}$ ( $k\ne0$ ) span a dense subspace of $V^n$ ;
Pareto optimality and symmetry force $\psi_n(\tau_1\cdots\tau_n)=\frac1n\tau^N$ ;
the three axioms force $(\psi_n\tau^k)_i=k_i/(k_1+\dots+k_n)$ , which is also the value of (4);
for positively homogeneous $v$ , $Dv(t\tau^N)=Dv(\tau^N)$ , so $\psi_nv=Dv(\tau^N)$ ;
(Remark 8.2) $\psi_n$ applied to Owen's multilinear extension of a game with side payments is its Shapley value.

Significance

The result. Theorem 8.1 singles out the diagonal formula among all ways of valuing smooth fuzzy games, using only efficiency, anonymity and invariance under merging players into types. Property (5) shows that the value transforms correctly under every linear change of coordinates fixing the grand coalition. The core statement links the value to stability: for concave homogeneous games (for instance, market games), the value is the only allocation no fuzzy coalition can improve upon. Through Owen's extension, the classical Shapley value is recovered as a special case.

Formalizing it. The theorem is proved in the paper, briefly, and its proof leans on an unproved density claim and on a short appeal to atomicity. A formalization makes the uniqueness argument complete: in particular, how atomicity, which only allows nonempty types, determines the value of a monomial in which some player has exponent $0$ . No machine-checked version of the Aumann–Shapley diagonal formula or its axiomatisation is known to us. Mathlib has the Stone–Weierstrass theorem for continuous functions but no $C^1$ density of polynomials on a cube; the latter is reusable well beyond game theory.

Difficulty

Existence (milestones 1–2) is calculus: differentiation under the integral sign and the chain rule. The difficulty sits in uniqueness. The first idea, computing $\psi_n$ on monomials by symmetry alone, fails as soon as the exponents differ: symmetry relates only games that are permutations of each other. Atomicity relates games with different numbers of players, and its types must be nonempty, so a player with exponent $0$ cannot simply be merged away. Uniqueness on all of $V^n$ then needs density of polynomials in the $C^1$ norm, not merely the uniform norm: without continuity in the $C^1$ norm, linear maps that agree on polynomials can disagree elsewhere, and the theorem is false.

Formalization scope

Players are Fin n, fuzzy coalitions and payoff vectors are Fin n → ℝ, and the cube is Set.Icc 0 1 in the product order.
$V^n$ is a submodule of functions on all of $\mathbb R^n$ that are $C^1$ there and vanish at $0$ . Every $C^1$ function on the cube extends to such a function, and only values and derivatives on the cube enter the norm and the axioms. The global domain makes $v\circ A$ meaningful for every linear $A$ .
"Continuous" means $\|\psi_nv\|\le C\,\|v\|_{C^1}$ with the $C^1$ seminorm of the cube (sup norm on $\mathbb R^n$ , operator norm on $Dv$ ). This is the continuity of the Banach space $V^n$ . Continuity for the uniform norm alone would make formula (4) discontinuous, and dropping continuity would make uniqueness false.
The axioms are stated for all $n\ge1$ ; the paper's " $\forall n\in N$ " in the symmetry axiom is read as $n\ge1$ . In the atomicity axiom (3), the paper's " $\forall v\in V^m$ " is read as $v\in V^n$ , because $P^*v$ is defined by (2) for an $n$ -player game. A partition into nonempty types is a surjection Fin n → Fin m. The symbols $\tau_{\theta-1(i)}$ are $\tau_{\theta^{-1}(i)}$ .
The games $\theta^*v$ , $P^*v$ and $v\circ A$ are passed as elements of $V^n$ , $V^m$ together with their defining identities; they always lie in those spaces.
In the core statement, concavity and positive homogeneity ( $v(t\tau)=tv(\tau)$ for $t>0$ , $\tau\ge0$ ) are required on the orthant $\mathbb R^n_+$ , to which §2 (2) extends $v$ ; the core quantifies over the cube, as in §2 (4)(a). The paper's " $V^N$ " there is $V^n$ .
Remark 8.2 is stated for games defined on all coalitions with $v(\emptyset)=0$ , since formula (7) uses $v(A\setminus\{i\})$ for every $A$ . The Shapley value is the published platform definition Supermodularity.Cooperative.ShapleyValue, whose formula is (7) re-indexed by $S=A\setminus\{i\}$ . The Cornet extension of the same remark is left out because it is not $C^1$ on the boundary of the cube.
A trivializing reading is ruled out: the goal asserts both existence of a sequence satisfying all axioms with $C^1$ continuity and uniqueness among all such sequences, so neither an empty axiom system nor a vacuous continuity requirement makes it hold.

Infrastructure that a complete development needs, and that is welcome as separate contributions: $C^1$ approximation of functions on a cube by polynomials; differentiation under the integral sign for the diagonal integral; Euler's identity and the supergradient inequality for concave homogeneous $C^1$ functions.

Selected references

J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28 (1953) 307–317. https://doi.org/10.1515/9781400881970-018
G. Owen, Multilinear Extensions of Games, Management Science 18(5) (1972) P64–P79. https://doi.org/10.1287/mnsc.18.5.64
L. J. Billera, D. C. Heath and J. Raanan, Internal Telephone Billing Rates — A Novel Application of Non-Atomic Game Theory, Operations Research 26(6) (1978) 956–965. https://doi.org/10.1287/opre.26.6.956
L. J. Mirman and Y. Tauman, Demand Compatible Equitable Cost Sharing Prices, Mathematics of Operations Research 7(1) (1982) 40–56. https://doi.org/10.1287/moor.7.1.40

12 thms2 active usersReviewed

Analysis Probability Stochastic Systems·Captain: mikedeng1

Implicit Renewal Theory and Tails of Solutions of Random Equations 3: Rate of Approach — t^κP(R > t) Equals C₊ Minus a Contour Integral Plus O(t^{−β/2})Research Paper

Motivation

Random equations of the form $R \overset{\mathcal L}{=} \Psi(R)$ , with $\Psi$ a random function independent of $R$ , describe the stationary laws of many stochastic recursions: perpetuities in insurance and finance, the stationary law of ARCH-type volatility models, random difference equations $R = Q + MR$ , and the stationary workload of certain queueing and storage models. When $\Psi(t)$ acts like multiplication by a random variable $M$ for large $|t|$ , and $\mathbf E|M|^\kappa = 1$ for some $\kappa > 0$ , the solution has power-law tails: $P(R > t) \sim C_+ t^{-\kappa}$ . This is the implicit renewal theorem of Goldie (Ann. Appl. Probab. 1991, Theorem 2.3), which recovers and extends Kesten's 1973 theorem on random difference equations.

A tail asymptotic alone says nothing about how fast $t^\kappa P(R > t)$ approaches $C_+$ . For tail estimation, for the accuracy of extreme-quantile approximations used in risk management, and for second-order regular variation, the rate matters. Section 3 of the same paper answers this: under an exponential moment condition slightly beyond the Cramér condition, the error has an explicit second-order term determined by the zeros of $1 - \hat\eta$ , where $\eta$ is a tilted law of $\log M$ , plus a remainder $O(t^{-\beta/2})$ .

Timeline: Kesten (1973) proved power tails for random difference equations; Grincevičius (1975) developed an implicit-renewal approach; Stone (1966) decomposed exponentially decaying renewal measures into an absolutely continuous part with explicit asymptotics and a finite part; Ganelius (1962) proved the Tauberian remainder theorem used to unsmooth; Goldie (1991) combined these into the rate result formalized here.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space carrying independent real random variables $M \ge 0$ and $R$ . Fix $\kappa > 0$ with $\mathbf E M^\kappa = 1$ (the Cramér condition, (2.3)) and $\beta > 0$ with $\mathbf E M^{\kappa+\beta} < \infty$ (3.3).

The tilted law of $M$ is the probability measure $\eta(dx) = e^{\kappa x} P(\log M \in dx)$ on $\mathbb R$ , computed on $\{M > 0\}$ . Its transforms are $\tilde\eta(\beta) = \int e^{\beta t}\eta(dt)$ for real $\beta$ and $\hat\eta(\theta) = \int e^{i\theta t}\eta(dt)$ for complex $\theta$ ; for a function $f$ , $\hat f(\theta) = \int e^{i\theta t} f(t)\,dt$ . Convolution powers are $\eta^{(0)} = \delta_0$ , $\eta^{(n+1)} = \eta^{(n)} * \eta$ , and the renewal measure is $\nu = \sum_{n \ge 0}\eta^{(n)}$ . A law is spread out when some convolution power has a nonzero absolutely continuous component; (3.4) asks this of the conditional law of $\log M$ given $M \ne 0$ .

Set $m = \mathbf E M^\kappa \log M$ and

g_1(t) = e^{\kappa t}\big(P(R > e^t) - P(MR > e^t)\big), \qquad C_+ = \frac1m\int_0^\infty \big(P(R > t) - P(MR > t)\big) t^{\kappa - 1}\,dt,

with $g_{-1}$ and $C_-$ defined the same way for the lower tail. The strip is $D = \{\theta : -\beta < \Im\theta < 0\}$ , and $\mathscr C$ denotes a positively oriented closed contour in $D$ enclosing every zero of $1 - \hat\eta$ in $D$ .

Formalization targets

Goal: Theorem 3.2

If, in addition, $\eta^{(n_0)} = (1 - \delta)\varphi_0 + \delta\varphi_1$ for some $n_0$ , with $\delta \in [0, 1)$ , $\varphi_0$ absolutely continuous and $\delta\tilde\varphi_1(\beta) < 1$ , and $\hat\eta \ne 1$ on $\Im\theta = -\beta$ , then $\int_0^\infty |P(R > t) - P(MR > t)|\,t^{\kappa+\beta-1}dt < \infty$ implies

t^\kappa P(R > t) = C_+ - \frac1{2\pi}\,\Re\oint_{\mathscr C} e^{-i\theta\log t}\,\frac{\hat g_1(\theta)}{1 - \hat\eta(\theta)}\,d\theta + O(t^{-\beta/2}), \qquad t \to \infty,

with the analogous statement for $P(R < -t)$ ; and if $R \overset{\mathcal L}{=} \Psi(R)$ with $R$ independent of $(M, \Psi)$ , the integrability hypotheses may be replaced by $\mathbf E|(\Psi(R)^\pm)^{\kappa+\beta} - ((MR)^\pm)^{\kappa+\beta}| < \infty$ . The theorem also asserts that $\eta$ is a spread-out probability measure.

Milestones

Lemma 9.5: Stone's inversion formula for the density of $\sum_n \chi * \mu^{(n)}$ .
Theorem 3.1: the renewal measure splits as $\nu = \nu_0 + \nu_1$ , $\nu_1$ finite with $\tilde\nu_1(\beta) < \infty$ , $\nu_0$ with continuous bounded density

p(t) = \frac1m - \frac1{2\pi}\oint_{\mathscr C} e^{-i\theta t}\frac{d\theta}{1 - \hat\eta(\theta)} + o(e^{-\beta t}).

(9.23) and (9.24): the smoothed identity and the smoothed rate $K * \Re r_1(t) = o(e^{-\beta t})$ for the kernel $K(t) = be^{-bt}\mathbf 1_{t>0}$ .
Theorem 9.6: the Beurling–Ganelius Tauberian remainder theorem.

Significance

Theorem 3.2 turns the first-order tail asymptotic of the implicit renewal theorem into an expansion: the second-order terms are finitely many terms of the form $(\log t)^{j-1}t^{\Im\theta_l}$ times oscillating factors, one family for each zero $\theta_l$ of $1 - \hat\eta$ with $0 < -\Im\theta_l \le \beta/2$ , and their form does not depend on the unknown law of $R$ . It applies to every random equation covered by the implicit renewal theorem once the stronger moment condition holds, including perpetuities and the random difference equation. Theorem 3.1 is of independent use: it is an explicit-rate version of Stone's decomposition of renewal measures with exponential moments.

The results are proved in the paper; none is formalized. Mathlib has the Fourier transform on the real line, convolution of measures, and rectangle Cauchy theorems, but no renewal theory, no Stone decomposition, and no Tauberian remainder theorem. Formalizing the mission produces a machine-checked renewal density expansion and a checked Beurling–Ganelius theorem, both reusable outside this paper.

Difficulty

The first-order theorem follows from the key renewal theorem applied to $r(t) = e^{\kappa t}P(R > e^t)$ . That route gives no rate: the key renewal theorem has no remainder, and the integrability hypothesis yields $e^{\beta t}g_1 \in L^1$ but not $e^{\beta t}g_1(t) = o(1)$ , so a remainder cannot be read off directly even with a spread-out step law. The proof therefore works with a smoothed version of $r$ , where Stone's decomposition with the contour expansion of the renewal density gives an $o(e^{-\beta t})$ remainder, and has to unsmooth. Unsmoothing is the Tauberian step: it requires a one-sided regularity condition on the unsmoothed function, verified for $r$ and for the contour term, and costs half the exponent. The contour expansion itself requires showing that $1 - \hat\eta$ has finitely many zeros in the strip and handling their orders through residues.

Formalization scope

All objects live in the namespace GoldieRenewal.Rates. Random variables are measurable maps $\Omega \to \mathbb R$ on a probability space; $M \ge 0$ almost surely; independence is IndepFun. Tail probabilities are real numbers P.real {ω | t < R ω}. Moments such as $\mathbf E M^{\kappa+\beta}$ and $\tilde\mu(\beta)$ are lower Lebesgue integrals in $[0, \infty]$ . The transforms $\hat\mu$ and $\hat f$ are Bochner integrals at complex arguments with the $+i$ sign of the paper. Asymptotic statements use Asymptotics.IsBigO and IsLittleO along atTop.

The contour. A contour $\mathscr C$ is the positively oriented boundary of an axis-parallel rectangle whose closure lies in $D$ and whose interior contains every zero of $1 - \hat\eta$ in $D$ ; the contour integral is the sum of the four edge integrals (RectangleIntegral, from the published ResidueCalcOnRectangles_defs). Expansions are stated for every such rectangle.

The variable in (3.8) and (3.10). The paper prints $e^{-i\theta t}$ in the contour term, but its proof establishes the expansion in the logarithmic variable $s = \log t$ . The targets are stated with $e^{-i\theta\log t}$ , which is what the proof gives. With the printed $e^{-i\theta t}$ the contour term would decay exponentially and the statement would claim $t^\kappa P(R > t) = C_+ + O(t^{-\beta/2})$ , which is not what is proved. Hypothesis (3.7) is printed with $P(R > -t)$ and is read with $P(R > t)$ .

Excluded trivializations. The contour term may not be dropped; the hypotheses do not exclude zeros of $1 - \hat\eta$ in $D$ ; and the contour must enclose all zeros in the strip, not a chosen subset.

Theorem 9.6 is stated for a complex-valued kernel and a finite strip width $a$ ; the application with $a = \infty$ follows by restricting to a finite strip. Lemma 9.5 carries an added hypothesis that the density of $\chi$ has compact support, which the proof uses and the application provides.

Contributions welcome: renewal-measure infrastructure (convolution powers, Blackwell-type limits), Fourier analysis of measures at complex arguments, residue computations on rectangles, and Tauberian remainder theory. Each is reusable well beyond this paper.

Selected references

C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Ann. Appl. Probab. 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Math. 131:207–248, 1973. https://doi.org/10.1007/BF02392040
C. Stone, On absolutely continuous components and renewal theory, Ann. Math. Statist. 37(1):271–275, 1966. https://doi.org/10.1214/aoms/1177699617
T. H. Ganelius, The remainder in Wiener's Tauberian theorem, Acta Univ. Gothoburgensis, Mathematica Gothoburgensia 1, 1962 (cited in Goldie 1991).
A. K. Grincevičius, One limit distribution for a random walk on the line, Lithuanian Math. J. 15:580–589, 1975 (cited in Goldie 1991).

12 thms2 active usersReviewed

Control Theory Probability Stochastic Systems·Captain: mikedeng1

Reflected Solutions of Backward SDE's, and Related Obstacle Problems for PDE's 2: With a Concave Coefficient, the Reflected BSDE Is the Value of a Minimax Optimal Stopping–Control ProblemResearch Paper

Motivation

A backward stochastic differential equation (BSDE) prescribes the terminal value of an adapted process instead of its initial value. Pardoux and Peng (1990) proved existence and uniqueness for Lipschitz coefficients, and BSDEs have since become a standard tool in stochastic control, mathematical finance and the probabilistic treatment of semilinear PDEs. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE, whose solution is constrained to stay above a given obstacle process. Reflected BSDEs describe the price of American options in nonlinear markets (El Karoui, Pardoux and Quenez 1997), Dynkin games (Cvitanić and Karatzas 1996), and obstacle problems for parabolic PDEs.

In §7 of the 1997 paper the coefficient is assumed concave. Then the solution of the reflected BSDE is the value of a game: one player chooses a stopping time, the other chooses a control that sets the discount rate and the change of measure, and the value does not depend on which player moves first. This mission formalizes that statement (Theorem 7.2) and the results its proof uses.

Setting

Let $(\Omega,\mathcal F,P)$ carry a $d$ -dimensional standard Brownian motion $B$ , fix a horizon $T\ge0$ , and let $\mathcal F_t$ be the natural filtration of $B$ augmented by the $P$ -null sets. Write $\mathbb L^2$ for the square-integrable $\mathcal F_T$ -measurable random variables, $\mathbb H^2$ for the progressively measurable processes $\varphi$ with $E\int_0^T|\varphi_t|^2dt<\infty$ , and $\mathcal S^2$ for those with $E\sup_{t\le T}|\varphi_t|^2<\infty$ .

The data are a terminal value $\xi\in\mathbb L^2$ ; a coefficient $f(\omega,t,y,z)$ , $y\in\mathbb R$ , $z\in\mathbb R^d$ , with $f(\cdot,y,z)\in\mathbb H^2$ for every $(y,z)$ and Lipschitz in $(y,z)$ with a constant $K$ ; and a continuous progressively measurable obstacle $S$ with $E\sup_t(S_t^+)^2<\infty$ and $S_T\le\xi$ . A solution of the reflected BSDE is a triple $(Y,Z,K)$ of progressively measurable processes with $Z\in\mathbb H^2$ , $Y\in\mathcal S^2$ , $K_T\in\mathbb L^2$ , and

Y_t=\xi+\int_t^Tf(s,Y_s,Z_s)\,ds+K_T-K_t-\int_t^T(Z_s,dB_s),\qquad Y_t\ge S_t,

where $K$ is continuous, nondecreasing, $K_0=0$ and $\int_0^T(Y_t-S_t)\,dK_t=0$ : $K$ pushes $Y$ up only when $Y$ touches $S$ .

For $t\le T$ , $\mathcal T_t$ is the set of stopping times $v$ with $t\le v\le T$ . When $f(\omega,t,\cdot,\cdot)$ is concave, its conjugate is

F(\omega,t,\beta,\gamma)=\sup_{(y,z)}\big[f(\omega,t,y,z)-\beta y-\langle\gamma,z\rangle\big]\in(-\infty,+\infty].

The admissible controls $\mathcal A$ are the bounded progressively measurable $(\beta_t,\gamma_t)$ with $E\int_0^TF(t,\beta_t,\gamma_t)^2dt<\infty$ . Each $(\beta,\gamma)\in\mathcal A$ gives the affine coefficient $f^{\beta,\gamma}(t,y,z)=F(t,\beta_t,\gamma_t)+\beta_ty+\langle\gamma_t,z\rangle$ , its reflected BSDE solution $Y^{\beta,\gamma}$ , the process $\Gamma^{\beta,\gamma}_{t,s}$ solving $d\Gamma_{t,s}=\Gamma_{t,s}(\beta_sds+(\gamma_s,dB_s))$ , $\Gamma_{t,t}=1$ , and the payoff

\Phi(t,v,\beta,\gamma)=\Gamma^{\beta,\gamma}_{t,v}\big[S_v1_{\{v<T\}}+\xi1_{\{v=T\}}\big]+\int_t^v\Gamma^{\beta,\gamma}_{t,s}F(s,\beta_s,\gamma_s)\,ds.

Formalization targets

Goal: Theorem 7.2 (p. 725)

For every $t\in[0,T]$ and $(\beta,\gamma)\in\mathcal A$ , $Y^{\beta,\gamma}_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Phi(t,v,\beta,\gamma)\mid\mathcal F_t]$ , and

Y_t=\operatorname*{ess\,inf}_{\mathcal A}Y^{\beta,\gamma}_t=\operatorname*{ess\,inf}_{\mathcal A}\operatorname*{ess\,sup}_{v\in\mathcal T_t}E[\Phi\mid\mathcal F_t]=\operatorname*{ess\,sup}_{v\in\mathcal T_t}\operatorname*{ess\,inf}_{\mathcal A}E[\Phi\mid\mathcal F_t].

The last equality, the interchange of the two essential extrema, is the minimax content.

Milestones

Theorem 4.1 (p. 712): comparison. If $\xi\le\xi'$ , $f\le f'$ and $S\le S'$ , and one of $f,f'$ is Lipschitz, then $Y\le Y'$ .
§7 conjugacy (p. 724): a concave Lipschitz $f$ equals $\min_{(\beta,\gamma)\in D^F_t}\{F(t,\beta,\gamma)+\beta y+\langle\gamma,z\rangle\}$ , the minimum is attained, and the domain $D^F_t$ of $F$ is a.s. bounded.
Proposition 7.1 (p. 724): for an affine coefficient $\delta_t+\beta_ty+\langle\gamma_t,z\rangle$ , $\Gamma_tY_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Gamma_v\xi1_{\{v=T\}}+\Gamma_vS_v1_{\{v<T\}}+\int_t^v\Gamma_s\delta_sds\mid\mathcal F_t]$ .
§7 optimal control (p. 725): some $(\beta^*,\gamma^*)\in\mathcal A$ satisfies $f(t,Y_t,Z_t)=F(t,\beta^*_t,\gamma^*_t)+\beta^*_tY_t+\langle\gamma^*_t,Z_t\rangle$ $dt\times dP$ -a.e., so $(Y,Z,K)$ solves the reflected BSDE with coefficient $f^{\beta^*,\gamma^*}$ .

Significance

Theorem 7.2 identifies the solution of a nonlinear reflected BSDE with the value of a zero-sum game between a stopper and a controller. In finance, with $f$ the driver of a pricing rule under constraints or ambiguity, it says that the nonlinear price of an American claim is the worst case, over a family of discount rates and changes of measure, of linear American prices; and the stopper may announce the stopping rule first without changing the value. Concave drivers include the hedging equations with different borrowing and lending rates. The representation reduces questions about the nonlinear equation to a family of linear ones, which is how monotonicity, convexity and stability properties of nonlinear American prices are usually derived.

All four results and the goal are proved in the paper, with references to standard convex analysis and a measurable section theorem for two steps. None of them has a machine-checked proof. Mathlib has Brownian motion, filtrations, stopping times and conditional expectation, but no stochastic integral; the mission uses the Itô integral of the published Peng1990.SMP.Stochastic layer. A formal proof would give, beyond the theorem, a reusable comparison theorem for reflected BSDEs, a Snell-envelope representation for linear reflected BSDEs, and a measurable selection of supergradients along a process.

Difficulty

The inequality $Y_t\le Y^{\beta,\gamma}_t$ for each control is a direct consequence of comparison, since $f\le f^{\beta,\gamma}$ . The difficulty is the reverse inequality, which needs a single admissible control that attains the conjugate representation along the solution $(Y,Z)$ for almost every $(t,\omega)$ . Choosing a supergradient pointwise is easy; choosing it progressively measurable, bounded, and with $F(t,\beta^*_t,\gamma^*_t)$ square integrable is a measurable-selection problem. The interchange of ess inf and ess sup does not follow from a general minimax theorem: the family $\mathcal A$ is not compact and the payoff is not convex–concave in any usable topology. It uses a specific stopping time, the first time $Y$ touches $S$ , together with comparison on the random interval before it. Proposition 7.1 requires the linear change of variables $\Gamma_tY_t$ , whose transformed equation lacks the square integrability of the original one, so the Snell-envelope argument has to be rerun with weaker moments.

Formalization scope

Time and spaces. Time is $\mathbb R_{\ge0}$ with $T:\mathbb R_{\ge0}$ , and time integrals run over $[t,T]\subset\mathbb R$ . $\mathbb H^2$ is the published L2F (progressive in place of predictable); $\mathcal S^2$ and the obstacle condition are lower Lebesgue integrals in $[0,\infty]$ .
Filtration. The natural filtration of $B$ joined with the σ-algebra of $P$ -null sets.
Norms. $|z|$ is the Euclidean norm and $\langle\gamma,z\rangle=\sum_j\gamma_jz_j$ .
Lipschitz condition. Read as: almost surely, for all $t\le T$ and all $y,y',z,z'$ .
Solutions. Solutions are in the square-integrable class (v)–(viii). $Y$ has continuous paths. Equation (vi) holds for each $t$ almost surely, and $Y\ge S$ holds almost surely for all $t$ . $K$ is continuous and nondecreasing on every path. $\int_0^T(Y-S)\,dK=0$ is taken against the Lebesgue–Stieltjes measure of the path of $K$ .
Extended values. $F$ takes values in the extended reals. $F^2$ in the definition of $\mathcal A$ is taken in $[0,\infty]$ , so admissibility forces $F<\infty$ almost everywhere along the control.
Stochastic exponential. $\Gamma^{\beta,\gamma}_{t,s}$ is the Doléans-Dade exponential, built from Itô integrals of $\gamma$ with continuous paths.
Essential extrema. They are predicates relative to $\mathcal F_t$ , real valued: the essential infimum is the published MultiperiodRisk.Bellman.EssInf, and the essential supremum is its mirror image.
Added hypothesis. $S\in\mathcal S^2$ is assumed wherever a conditional expectation of the payoff appears (Remark 3.2: without loss of generality). Otherwise the payoff may fail to be integrable, and Lean's conditional expectation of a non-integrable function is $0$ .
Hypothesized families. The solutions $Y^{\beta,\gamma}$ and the Itô integrals defining $\Gamma^{\beta,\gamma}$ are hypotheses indexed by $\mathcal A$ . They exist by the existence theorem of the first mission of this series and by continuity of Itô integrals.

Several formalizations of the goal would make it trivial, and each is ruled out. The conjugate is not a real-valued supremum, which takes a junk value when unbounded. The essential infimum over $\mathcal A$ is not a pointwise infimum. The interchange of ess inf and ess sup is not dropped. The coefficient is a random field $f(\omega,t,y,z)$ , not a deterministic or Markovian one.

The closing gloss of Theorem 7.2, that the triple $(\beta^*,\gamma^*,D_t)$ is optimal, is not stated separately; milestone 4 is its control half. Contributions are welcome on a continuous version of the Itô integral, Itô's formula for products with $\Gamma$ , the Snell envelope in continuous time, and measurable selection of supergradients; all of these are reusable beyond this mission.

Selected references

N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng, M.-C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, Ann. Probab. 25(2), 1997, 702–737. https://doi.org/10.1214/aop/1024404416
É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14, 1990, 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
N. El Karoui, S. Peng, M.-C. Quenez, Backward stochastic differential equations in finance, Math. Finance 7(1), 1997, 1–71. https://doi.org/10.1111/1467-9965.00022
J. Cvitanić, I. Karatzas, Backward stochastic differential equations with reflection and Dynkin games, Ann. Probab. 24(4), 1996, 2024–2056. https://doi.org/10.1214/aop/1041903216
S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990, 966–979. https://doi.org/10.1137/0328054

10 thms2 active usersReviewed

Completed

Linear Optimization Optimization·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 3: Under Box Uncertainty, Worst-Case CVaR Minimization (16)–(20) Is Equivalent to the Linear Program (24)–(30)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the expected loss in the worst $(1-\beta)$ fraction of outcomes. Rockafellar and Uryasev showed that, for a finite set of scenarios, minimizing CVaR is a linear program whenever the loss is linear in the decision (Rockafellar–Uryasev 2000; 2002). That linear program needs the scenario probabilities, and in practice they are estimates. Zhu and Fukushima (2009) replace the single distribution by a set of distributions and minimize the worst-case CVaR over that set. The resulting problem, (16)–(20) below, contains a maximization over distributions inside a constraint, which no standard solver accepts directly.

This mission treats the first of the two cases the paper works out explicitly: the scenario probabilities are only known to lie in a box around a nominal distribution. Proposition 2 of the paper shows that the worst-case problem is then equivalent to a single problem, (24)–(30), with finitely many explicit constraints. The tool is linear programming duality applied to the inner maximization.

Setting

A decision $x \in \mathbb R^n$ is chosen from a set $\mathcal X \subseteq \mathbb R^n$ . The random vector takes one of $S$ values $y_{[1]}, \dots, y_{[S]} \in \mathbb R^m$ , and $f(x, y)$ is the loss of decision $x$ in outcome $y$ . A distribution over the scenarios is a vector $\pi \in \mathbb R^S$ . Vectors are compared componentwise, $e$ is the all-ones vector, and $\beta \in (0,1)$ is the confidence level.

The box uncertainty set (21) is built from a nominal distribution $\pi^0$ and bounds $\underline\eta, \overline\eta \in \mathbb R^S$ :

\mathcal P_\pi^B = \{\pi : \pi = \pi^0 + \eta,\ e^\top\eta = 0,\ \underline\eta \le \eta \le \overline\eta\}.

Problem (16)–(20) minimizes $\theta$ over $(x, u, \alpha, \theta) \in \mathbb R^n \times \mathbb R^S \times \mathbb R \times \mathbb R$ subject to

x \in \mathcal X,\qquad \max_{\pi \in \mathcal P_\pi^B} \alpha + \tfrac{1}{1-\beta}\pi^\top u \le \theta,\qquad u_k \ge f(x, y_{[k]}) - \alpha,\quad u_k \ge 0\ (k = 1, \dots, S).

By Theorem 2 of the paper its optimal value is the minimum of the worst-case CVaR over $\mathcal X$ .

For fixed $u$ , the worst case over the box involves the linear program (22) and its dual (23):

\gamma^*(u) = \max_{\eta}\{u^\top\eta : e^\top\eta = 0,\ \underline\eta \le \eta \le \overline\eta\},\qquad \min_{(z,\xi,\omega)}\{\overline\eta^\top\xi + \underline\eta^\top\omega : e z + \xi + \omega = u,\ \xi \ge 0,\ \omega \le 0\}.

Problem (24)–(30) minimizes $\theta$ over $(x, u, z, \xi, \omega, \alpha, \theta)$ subject to $x \in \mathcal X$ ,

\alpha + \tfrac{1}{1-\beta}(\pi^0)^\top u + \tfrac{1}{1-\beta}(\overline\eta^\top\xi + \underline\eta^\top\omega) \le \theta,\qquad e z + \xi + \omega = u,\quad \xi \ge 0,\quad \omega \le 0,

and the same constraints $u_k \ge f(x, y_{[k]}) - \alpha$ , $u_k \ge 0$ . A point solves a problem when it is feasible and no feasible point has a smaller $\theta$ .

Formalization targets

Goal: Proposition 2 (p. 1159)

If $(x^*, u^*, z^*, \xi^*, \omega^*, \alpha^*, \theta^*)$ solves (24)–(30), then $(x^*, u^*, \alpha^*, \theta^*)$ solves (16)–(20).
If $(\tilde x^*, \tilde u^*, \tilde\alpha^*, \tilde\theta^*)$ solves (16)–(20) and $(\tilde z^*, \tilde\xi^*, \tilde\omega^*)$ is an optimal solution of (23) with $u = \tilde u^*$ , then $(\tilde x^*, \tilde u^*, \tilde z^*, \tilde\xi^*, \tilde\omega^*, \tilde\alpha^*, \tilde\theta^*)$ solves (24)–(30).
In the situation of 2, an optimal solution of (23) exists.

Milestones, in the order the paper's argument uses them

The decomposition before (22) (p. 1159): if (22) is feasible, then

\max_{\pi \in \mathcal P_\pi^B} \alpha + \tfrac{1}{1-\beta}\pi^\top u = \alpha + \tfrac{1}{1-\beta}(\pi^0)^\top u + \tfrac{\gamma^*(u)}{1-\beta},

and both maxima are attained.

Weak duality for (22)–(23): $u^\top\eta \le \overline\eta^\top\xi + \underline\eta^\top\omega$ for feasible points of the two programs, hence $\gamma^*(u) \le \overline\eta^\top\xi + \underline\eta^\top\omega$ .
Strong duality for (22)–(23): if (22) is feasible, (23) has an optimal solution, with value $\gamma^*(u)$ .
Feasibility transfer from (24)–(30) to (16)–(20), by projection.
Feasibility transfer from (16)–(20) to (24)–(30), by appending an optimal solution of (23).

Significance

Proposition 2 makes worst-case CVaR minimization under box uncertainty computable with standard software. When $f$ is linear in $x$ and $\mathcal X$ is a polyhedron, (24)–(30) is a linear program whose size grows only linearly in $S$ , and when $f$ is convex in $x$ and $\mathcal X$ is convex it is a convex program. The robust portfolio models of §3 of the paper rest on this reformulation. Setting $\underline\eta = \overline\eta = 0$ recovers the Rockafellar–Uryasev linear program (Remark 2 of the paper).

Proposition 2 is proved in the paper. As far as is known, neither it nor the duality pair (22)–(23) has a machine-checked proof; this mission would supply one. The development also exercises LP duality for a specific bounded-variable program, one with a single equality constraint, in a form that can be reused by other robust-optimization reformulations over boxes.

Difficulty

The obvious argument says "replace the max by its dual". Two steps need care. First, the inner maximum is over a polytope that may be empty, and the substitution of (18) by (26)–(28) is correct only when the box is nonempty; it must be shown that an optimal solution of either problem forces the box to be nonempty. Second, the equivalence is a statement about optimal solutions, not feasible ones, so both directions need the comparison of objective values over all feasible points of the other problem. The printed proof assumes in each direction that some optimal solution with a smaller objective exists, where only a feasible one is available; the argument must be run with feasible points. Strong duality for (22)–(23) is a genuine LP duality theorem: Mathlib does not provide it in this form, and it must be derived from a general duality or Farkas-type result.

Formalization scope

Vectors are Fin S → ℝ and Fin n → ℝ, compared pointwise, with zero-based indices. Dot products are ⬝ᵥ, and $e^\top\eta$ is ∑ k, η k. Points of the three problems are structures (Var16, Var24, Dual23) with fields named as in the paper. The factor $\frac{1}{1-\beta}$ is (1 - β)⁻¹, and every theorem assumes $0 < \beta < 1$ .

Committed readings:

Constraint (18), printed as " $\max_{\pi \in \mathcal P_\pi^B} \ldots \le \theta$ ", is stated as "for all $\pi \in \mathcal P_\pi^B$ ". The two agree whenever the maximum exists, and the $\forall$ form stays correct on an empty box. A real supremum there would silently become the constraint $0 \le \theta$ .
$\gamma^*(u)$ is a real supremum, and every statement using it assumes (22) feasible.
"Solves" means feasible and minimal in $\theta$ (IsMinOn). Feasibility alone would make the proposition trivial and is ruled out.
Clause 3 of the goal states the existence of an optimal solution of (23). Without it, clause 2 could hold vacuously.
No hypothesis is placed on $f$ , $\mathcal X$ , $\pi^0$ , $\underline\eta$ or $\overline\eta$ . The paper intends $\pi^0 + \underline\eta \ge 0$ and $\pi^0$ a distribution, but Proposition 2 holds without these assumptions.

Needed infrastructure: LP strong duality for the pair (22)–(23), derivable from Mathlib's Farkas lemma or from LP duality theorems already on the platform; finite sums and dot products. Proofs of the milestones, of the goal from the milestones, and of a general bounded-variable LP duality lemma are all welcome.

Not in scope: the ellipsoidal case (31)–(40), Remark 2, and the portfolio instances of §3.

Selected references

S. Zhu, M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar, S. Uryasev, Optimization of Conditional Value-at-Risk, Journal of Risk 2:21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar, S. Uryasev, Conditional Value-at-Risk for General Loss Distributions, Journal of Banking & Finance 26:1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
A. Ben-Tal, A. Nemirovski, Robust Optimization — Methodology and Applications, Mathematical Programming Ser. B 92:453–480, 2002. https://doi.org/10.1007/s101070100286

8 thms2 active usersReviewed

Complexity Theory Linear Optimization Optimization·Captain: mikedeng1

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 1: In O(√nL) Predictor-Corrector Iterations It Finds LP and Dual Optima or Detects InfeasibilityResearch Paper

Motivation

Interior-point methods solve linear programs in polynomially many iterations, but the classical analyses assume something about the instance before the algorithm starts: a known strictly feasible primal–dual pair, a nonempty interior, or a big- $M$ bound on the feasible region of order $2^L$ , where $L$ is the bit length of the data. In practice none of this is known in advance, and an infeasible or unbounded instance should be reported rather than assumed away.

Ye, Todd and Mizuno (1994) removed these assumptions. They embed a standard-form linear program and its dual into a single homogeneous and self-dual artificial program (HLP), which always has a known interior starting point, and apply the Mizuno–Todd–Ye predictor–corrector method to it. The resulting algorithm needs no regularity assumption, no big- $M$ parameter, and an $O(\sqrt n L)$ iteration bound, the best known for interior-point methods. Self-dual embeddings of this kind are now the standard initialization in interior-point solvers for linear and conic programs.

Timeline. Karmarkar (1984) gave the first polynomial interior-point method on a homogeneous canonical form. Mizuno, Todd and Ye (1990) introduced the predictor–corrector method with $O(\sqrt nL)$ iterations under a known interior start. Kojima, Mizuno and Yoshise (1993) built a self-dual big- $M$ artificial problem. Ye, Todd and Mizuno (1994) combined homogeneity and self-duality without big $M$ , obtaining the result formalized here.

Setting

Given $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , the primal problem is (LP) $\min\{c^Tx : Ax=b,\ x\ge0\}$ and its dual is (LD) $\max\{b^Ty : A^Ty\le c\}$ , with dual slacks $s=c-A^Ty$ .

Fix $x^0>0$ , $s^0>0$ , $y^0$ and put $\bar b=b-Ax^0$ , $\bar c=c-A^Ty^0-s^0$ , $\bar z=c^Tx^0+1-b^Ty^0$ . The homogeneous self-dual program (HLP) in the variables $(y,x,\tau,\theta,s,\kappa)$ is

\begin{aligned} \min\ & ((x^0)^Ts^0+1)\,\theta\\ \text{s.t. } & Ax-b\tau+\bar b\theta=0,\qquad s=-A^Ty+c\tau-\bar c\theta\ge0,\qquad \kappa=b^Ty-c^Tx+\bar z\theta\ge0,\\ & -\bar b^Ty+\bar c^Tx-\bar z\tau=-(x^0)^Ts^0-1,\qquad x\ge0,\ \tau\ge0 . \end{aligned}

Its feasible set is $\mathcal F_h$ , and $\mathcal F_h^0$ is the subset with $(x,\tau,s,\kappa)>0$ . A strictly self-complementary solution is an optimal solution with $\theta=0$ and $(x+s;\tau+\kappa)>0$ . The paper then fixes $y^0=0$ , $x^0=s^0=e$ , so the objective is $(n+1)\theta$ and $(0,e,1,1,e,1)\in\mathcal F_h^0$ .

With $\mu=(x^Ts+\tau\kappa)/(n+1)$ , the neighborhood of the central path is $\mathcal N(\beta)=\{z\in\mathcal F_h^0 : \|(Xs;\tau\kappa)-\mu e\|\le\beta\mu\}$ (Euclidean norm). The predictor–corrector algorithm starts at $(0,e,1,1,e,1)$ . At even steps it solves a Newton system with centering parameter $\gamma=0$ and moves by the largest step keeping the iterate in $\mathcal N(1/2)$ . At odd steps it takes a full Newton step with $\gamma=1$ . A termination projection then solves a least-squares problem on the columns where $x_j^k\ge s_j^k$ and produces a candidate exact solution.

Formalization targets

Goal: Corollary 7

For integer data with bit length $L$ and $n\ge1$ , there is an absolute constant $C$ and a finite predictor–corrector run that reaches, within

k\le C\sqrt n\,L

iterations, an iterate whose termination output $u=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ either has $\tau^*>0$ with $x^*/\tau^*$ optimal for (LP) and $(y^*/\tau^*,s^*/\tau^*)$ optimal for (LD), or has $\tau^*=0$ with $c^Tx^*<0$ and (LD) infeasible, or $-b^Ty^*<0$ and (LP) infeasible.

Theorem 6

The same bound, with the conclusion that the termination output, rescaled to the normalization $e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1$ , is a strictly self-complementary solution of (HLP).

Milestones

Proposition 1 (self-duality of skew-symmetric programs), Theorem 2 (ii), (iv), (v), Theorem 5 (ii), the two Mizuno–Todd–Ye estimates in the proof of Theorem 6, the predictor-step and corrector-step claims, the termination claim, the integrality and $O(L)$ size of the (HLP) data, and Theorem 3 (i), (ii).

Significance

The result. Corollary 7 gives a single polynomial algorithm that decides the status of an arbitrary linear program. It returns optimal primal and dual solutions when they exist and an infeasibility certificate otherwise. It needs no Phase I, no big- $M$ constant and no interior assumption, and its $O(\sqrt nL)$ iteration count matches the best bound known under those assumptions. Theorem 3 is the bridge: an exact strictly self-complementary solution of (HLP) determines the status of (LP) and (LD).

Formalizing it. The paper's result is proved; no machine-checked proof of it is known. The mission produces a formal account of the self-dual embedding, the central-path neighborhood analysis for (HLP), an exact finite-termination step from an approximate iterate, and the reading of a bit-length complexity bound with explicit quantifier order. The neighborhood estimates and the bit-length machinery are reusable for other interior-point and complexity results.

Difficulty

The per-step estimates are short calculations once the orthogonality $d_x^Td_s+d_\tau d_\kappa=0$ is available. The step that resists is termination. Geometric decrease of the gap reaches $2^{-O(L)}$ in $O(\sqrt nL)$ iterations, but turning such an iterate into an exact strictly self-complementary solution requires a quantitative separation: on $\mathcal N(1/2)$ , once the gap is below $2^{-O(L)}$ , the comparison $x_j\ge s_j$ must identify the optimal partition and the least-squares projection must land in the positive orthant. That separation bound rests on determinant estimates for integer matrices (Hadamard-type bounds in terms of $L$ ) and on the strict complementarity of (HLP), neither of which comes from the iteration analysis itself. A second subtlety is that the algorithm is not a function: without a rank assumption the Newton system leaves $d_y$ undetermined.

Formalization scope

Data for the complexity statements are integer matrices and vectors, cast to $\mathbb R$ ; all optimization objects are real. $L$ is Schrijver's encoding size, $\sum(1+\lceil\log_2(|v|+1)\rceil)$ over the entries plus the dimensions, so $L\ge1$ whenever $n\ge1$ .
Every $O(\cdot)$ is pinned with an absolute constant chosen before $m$ , $n$ and the data: $O(\sqrt nL)$ as $C\sqrt n\,L$ , $2^{-O(L)}$ as $2^{-C'L}$ , and $O(L)$ as $C\cdot L$ . The hypothesis $n\ge1$ , implicit in the paper, is explicit.
The algorithm is a relation on finite runs: any solution of the Newton system may be used, and each predictor step taken before termination must attain the maximum in (13). The conclusion asserts a successful run and its output. Stopping at the successful iterate avoids requiring a later step whose maximum may not exist.
The termination projection is defined relationally (an output is built from a minimizer) and its existence is part of the conclusion. Theorem 6 is stated for the output rescaled to the normalization (9): the projection imposes only homogeneous constraints, so the unscaled output need not be feasible for (HLP).
"(LP) has a solution (feasible and bounded)" is read as "(LP) has an optimal solution". "An indication that (LP) or (LD) is infeasible" is the negative sign of $c^Tx^*$ or $-b^Ty^*$ together with the infeasibility it certifies, not the bare disjunction "one of them is infeasible".
"Optimal for (HLP)" means minimizing the objective over $\mathcal F_h$ . It is not defined as $\theta=0$ , which would make Theorem 2 (iv) definitional.
Norms are Euclidean and written out explicitly, since Lean's default norm on $\mathbb R^n$ is the sup norm.
(LP) and (LD) are built on the published general-form LP definitions (LinearOptimization_DualLP). The self-dual objects of the Vanderbei and Matoušek series are different embeddings and are not reused.

A complete development needs: skew-symmetric LP duality and strict complementarity (Goldman–Tucker) for (HLP), the Mizuno–Todd–Ye neighborhood calculus, and Hadamard-type bounds on integer determinants. Contributions to any milestone, or to these supporting libraries, are welcome.

Selected references

Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt nL)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
S. Mehrotra, Y. Ye, Finding an interior point in the optimal face of linear programs, Mathematical Programming 62, 497–515, 1993. https://doi.org/10.1007/BF01585180
M. Kojima, S. Mizuno, A. Yoshise, A little theorem of the big M in interior point algorithms, Mathematical Programming 59, 361–375, 1993. https://doi.org/10.1007/BF01581253
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 373–395, 1984. https://doi.org/10.1007/BF02579150
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

22 thms2 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 2: For a Compact Convex Set of Discrete Distributions, Worst-Case CVaR Equals min_α max_π G_β(x, α, π)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection and risk-averse optimization: for a confidence level $\beta$ it is, roughly, the expected loss in the worst $(1-\beta)$ fraction of outcomes. Its practical appeal comes from the representation of Rockafellar and Uryasev (2000, 2002), which writes CVaR as the minimum over a scalar threshold $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex (often linear) program.

That representation presupposes that the distribution of the uncertain data is known exactly. In practice the scenario probabilities are estimated, and decisions that are optimal for the estimate can perform poorly under a nearby distribution. Zhu and Fukushima (Oper. Res. 57(5), 2009) study the worst-case CVaR: the largest CVaR over a set of distributions that the decision maker considers plausible. For a finite scenario model they show (Theorem 2) that when the plausible set of probability vectors is compact and convex, the worst-case CVaR again has a min–max representation in the threshold $\alpha$ . This is what makes worst-case CVaR minimization tractable: under box uncertainty it becomes a linear program and under ellipsoidal uncertainty a second-order cone program (§2.2.1–2.2.2 of the paper).

Setting

A decision $x \in \mathbb R^n$ incurs the loss $f(x,y)$ , where $y \in \mathbb R^m$ is random. In the discrete model $y$ takes the finitely many values $y_{[1]},\dots,y_{[S]}$ , the scenarios, with probabilities $\pi_1,\dots,\pi_S$ , where $\pi_k \ge 0$ and $\sum_k \pi_k = 1$ . Fix a confidence level $0<\beta<1$ and write $[t]^+ = \max\{t,0\}$ . The Rockafellar–Uryasev function for the distribution $\pi$ is

G_\beta(x,\alpha,\pi) = \alpha + \frac{1}{1-\beta}\sum_{k=1}^S \pi_k\,[f(x,y_{[k]})-\alpha]^+, \qquad \alpha\in\mathbb R,

and the CVaR of the loss at $x$ under $\pi$ is

\mathrm{CVaR}_\beta(x,\pi) = \min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).

The distribution is not known; it is only known to lie in an ambiguity set $\mathcal P_\pi \subseteq \mathbb R^S$ of probability vectors. The worst-case CVaR at $x$ is

\mathrm{WCVaR}_\beta(x) = \sup_{\pi\in\mathcal P_\pi}\mathrm{CVaR}_\beta(x,\pi) = \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).

In the Lean development these objects are WorstCaseCVaR.Discrete.G, cvar and wcvar, with the scenarios given as ys : Fin S → (Fin m → ℝ) and $\mathcal P_\pi$ as a set P of vectors Fin S → ℝ.

Formalization targets

Goal: Theorem 2 (p. 1159)

If $\mathcal P_\pi$ is a nonempty compact convex set of probability vectors, then for each $x$

\mathrm{WCVaR}_\beta(x) = \min_{\alpha\in\mathbb R}\max_{\pi\in\mathcal P_\pi} G_\beta(x,\alpha,\pi),

with the inner maximum attained for every $\alpha$ and the outer minimum attained at some $\alpha_0$ . The statement fixes no constants and no particular ambiguity set.

Milestones (the steps of the paper's proof, p. 1167)

$G_\beta(x,\alpha,\pi)$ is convex in $\alpha$ for each probability vector $\pi$ and affine in $\pi$ for each $\alpha$ .
There is one nonempty closed bounded interval $\mathcal A$ such that, for every $\pi\in\mathcal P_\pi$ , $\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi) = \min_{\alpha\in\mathcal A} G_\beta(x,\alpha,\pi)$ .
Lemma 1 (p. 1157, Ky Fan's minimax theorem): for convex–concave, suitably semicontinuous $\phi$ on a product of nonempty compact convex sets, $\min_x\max_y\phi = \max_y\min_x\phi$ .
Lemma 1 on $\mathcal A\times\mathcal P_\pi$ : $\max_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathcal A}G_\beta = \min_{\alpha\in\mathcal A}\max_{\pi\in\mathcal P_\pi}G_\beta$ .
The min-max inequality $\inf_{\alpha\in\mathbb R}\sup_{\pi\in\mathcal P_\pi}G_\beta(x,\alpha,\pi) \ge \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R}G_\beta(x,\alpha,\pi)$ .

Significance

Theorem 2 converts a supremum over distributions of a minimum over thresholds into a minimum over thresholds of a worst case of a function that is affine in $\pi$ . Minimizing $\mathrm{WCVaR}_\beta(x)$ over decisions $x$ is therefore the single minimization problem (16)–(20) of the paper in the variables $(x,u,\alpha,\theta)$ , whose only nonstandard constraint is $\max_{\pi\in\mathcal P_\pi}(\alpha+\frac{1}{1-\beta}\pi^Tu)\le\theta$ . For box and ellipsoidal ambiguity sets that constraint is dualized into linear or conic constraints, which gives the robust portfolio models of §§2.2.1–3 of the paper. The same exchange of $\sup_\pi$ and $\min_\alpha$ underlies many later distributionally robust CVaR models.

The result is proved in the paper (appendix, p. 1167) and is not open. The mission produces a machine-checked proof of it, which to our knowledge does not exist. Mathlib contains Sion's minimax theorem (Sion.exists_isSaddlePointOn), which covers Lemma 1; what is missing is the CVaR-specific part: the convexity of $G_\beta$ in $\alpha$ , the reduction of the threshold to a compact interval uniform over $\mathcal P_\pi$ , and the passage from the compact interval back to all of $\mathbb R$ .

Difficulty

The obvious approach applies a minimax theorem directly to $G_\beta$ on $\mathbb R\times\mathcal P_\pi$ . That fails because $\mathbb R$ is not compact, and minimax equalities on a noncompact factor can fail; the threshold must first be confined to a bounded interval, and the interval must work for every $\pi\in\mathcal P_\pi$ simultaneously. After the exchange on the interval, the minimum over the interval has to be identified with the infimum over all of $\mathbb R$ , which needs the min-max inequality on the unrestricted line. A second subtlety is attainment: every "min" and "max" in the statement is a claim that an extremum exists, and in the real-valued formalization each must be exhibited rather than read off from a supremum.

Formalization scope

Conventions committed to in the Lean statements:

Scenarios are indexed zero-based by Fin S; probability vectors are elements of stdSimplex ℝ (Fin S).
The confidence level satisfies $0<\beta<1$ in every statement (the paper says only that $\beta$ is a confidence level, usually above $0.9$ ).
$\mathrm{CVaR}_\beta(x,\pi)$ is defined as the paper does for discrete distributions, as the minimum of $G_\beta(x,\cdot,\pi)$ , encoded as the real infimum of its values; $\mathrm{WCVaR}_\beta(x)$ is the real supremum of the image of $\mathcal P_\pi$ . Both are true infima and suprema under the hypotheses carried by every theorem.
Theorem 2's hypothesis " $\mathcal P_\pi$ is a compact convex set" is completed by two standing assumptions of §2.2: $\mathcal P_\pi$ consists of probability vectors, and it is nonempty. Without the first, $G_\beta(x,\cdot,\pi)$ can be unbounded below and the real infimum returns a junk value; without the second the supremum is over the empty set.
Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$ , which the paper omits and which are needed for the extrema to exist; its conclusion is a saddle point, equivalent to the attained min–max equality.
In the goal, the right-hand side exhibits an explicit minimizer $\alpha_0$ and the inner maximum is shown to be attained; neither is replaced by a bare infimum or supremum.

No vacuous version of the goal is admissible: the ambiguity set must be nonempty and consist of probability vectors, and the minimum over $\alpha$ must be witnessed.

The development needs only finite sums, convexity on $\mathbb R$ and on the simplex, compactness of $\mathcal P_\pi$ and of closed intervals, and Mathlib's minimax theorem. The reduction to a bounded interval and the min-max inequality are reusable for other finite-scenario CVaR results. Proofs of any milestone are welcome, as are alternative proofs of the goal that avoid the interval reduction.

Selected references

S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar and S. Uryasev, Optimization of Conditional Value-at-Risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar and S. Uryasev, Conditional Value-at-Risk for General Loss Distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
K. Fan, Minimax Theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
M. Sion, On General Minimax Theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171

7 thms2 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 1: Under Mixture Distribution Uncertainty, Worst-Case CVaR Equals the Minimum over α of max_i F^i_β(x, α)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection, insurance and stochastic programming. Its practical appeal comes from a variational formula of Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002): CVaR at level $\beta$ is the minimum over a scalar $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex program, a linear program when the distribution is given by scenarios.

The formula needs the distribution of the random returns, and in practice that distribution is estimated and uncertain. Zhu and Fukushima (Oper. Res. 57(5), 2009) introduce the worst-case CVaR: the supremum of CVaR over a set $\mathcal P$ of candidate distributions. They show it is again a coherent risk measure and that, for several natural choices of $\mathcal P$ , minimizing it remains a tractable convex program. This mission formalizes the first of these results, for $\mathcal P$ the set of all mixtures of finitely many given distributions, a model used in robust statistics and in finance to describe returns under several market regimes.

Setting

A decision $x\in\mathbb R^n$ and a random vector $y\in\mathbb R^m$ determine a loss $f(x,y)\in\mathbb R$ . A confidence level $\beta$ satisfies $0<\beta<1$ (in applications $\beta\ge0.9$ ). Write $[t]^+=\max\{t,0\}$ .

For a probability distribution $P$ of $y$ under which $f(x,\cdot)$ is integrable, the Rockafellar–Uryasev function is

F_\beta(x,\alpha)=\alpha+\frac1{1-\beta}\int_{\mathbb R^m}[f(x,y)-\alpha]^+\,dP(y),\qquad\alpha\in\mathbb R, \tag{1}

and CVaR is its minimum over $\alpha$ :

\mathrm{CVaR}_\beta(x)=\min_{\alpha\in\mathbb R}F_\beta(x,\alpha). \tag{2}

Fix $l\ge1$ likelihood distributions $P^1,\dots,P^l$ on $\mathbb R^m$ and let $\Lambda=\{\lambda\in\mathbb R^l:\lambda_i\ge0,\ \sum_i\lambda_i=1\}$ be the probability simplex. The ambiguity set is the set of mixtures

\mathcal P_M=\Big\{\textstyle\sum_{i=1}^l\lambda_iP^i:\ \lambda\in\Lambda\Big\},

and the worst-case CVaR of $x$ is

\mathrm{WCVaR}_\beta(x)=\sup_{\lambda\in\Lambda}\ \mathrm{CVaR}_\beta(x)\ \text{ under }\ \textstyle\sum_i\lambda_iP^i. \tag{3}

Write $F^i_\beta(x,\alpha)$ for the function (1) with $P=P^i$ , $F^{\mathcal L}_\beta(x,\alpha)=\max_{i\in\mathcal L}F^i_\beta(x,\alpha)$ with $\mathcal L=\{1,\dots,l\}$ , and $H_\beta(x,\alpha,\lambda)$ for the function (1) of the mixture $\sum_i\lambda_iP^i$ .

Formalization targets

Goal: Theorem 1

For every $x$ with $f(x,\cdot)$ integrable under every $P^i$ ,

\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\ \max_{i\in\mathcal L}F^i_\beta(x,\alpha),

with the minimum attained. The supremum over infinitely many distributions on the left becomes a minimum of the pointwise maximum of $l$ functions on the right.

Milestones

The milestones follow the paper's appendix proof (pp. 1166–1167) in order:

(53): $H_\beta(x,\alpha,\lambda)=\sum_i\lambda_iF^i_\beta(x,\alpha)$ for $\lambda\in\Lambda$ .
(54): $\mathrm{WCVaR}_\beta(x)=\max_{\lambda\in\Lambda}\min_{\alpha}H_\beta(x,\alpha,\lambda)$ , both extrema attained.
The minimizer set of $F_\beta(x,\cdot)$ is a nonempty closed bounded interval $[\underline\alpha^*,\overline\alpha^*]$ .
Minimizers of a nonnegative combination of two convex functions on $\mathbb R$ lie between the extreme endpoints of their minimizer intervals.
Every minimizer of $H_\beta(x,\cdot,\lambda)$ lies in $\mathcal A=[\min_i\underline\alpha^*_i,\max_i\overline\alpha^*_i]$ , and the minimum over $\mathbb R$ is attained in $\mathcal A$ .
Lemma 1, the minimax equality for convex–concave functions on compact convex sets.
(55): $\max_\lambda\min_{\mathbb R}H_\beta=\max_\lambda\min_{\mathcal A}H_\beta=\min_{\mathcal A}\max_\lambda H_\beta$ .
(56)–(57): $\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)$ .
(58)–(59): $\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)=\max_iF^i_\beta(x,\alpha)$ .

An additional item states Corollary 1: $(x^*,\alpha^*)$ minimizes $F^{\mathcal L}_\beta$ over $\mathcal X\times\mathbb R$ exactly when $x^*$ minimizes $\mathrm{WCVaR}_\beta$ over $\mathcal X$ and $\alpha^*$ minimizes $F^{\mathcal L}_\beta(x^*,\cdot)$ .

Significance

The result. Theorem 1 makes worst-case CVaR under mixture uncertainty no harder to optimize than ordinary CVaR. Since each $F^i_\beta$ is jointly convex in $(x,\alpha)$ when $f$ is convex in $x$ , $F^{\mathcal L}_\beta$ is convex, and Corollary 1 turns robust CVaR minimization into one convex program in $(x,\alpha)$ ; with sampled scenarios it is a linear program (the paper's (10)–(15)). It is the starting point for the paper's robust portfolio models (§3), whose ambiguity sets are mixtures of a few estimated return distributions.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof contributes a measure-theoretic treatment of the Rockafellar–Uryasev function for arbitrary distributions (the paper argues with densities and appeals to Remark 1 for the general case), a reusable statement that the minimizer set of $F_\beta$ is a compact interval, and a worked instance of the minimax theorem in Mathlib (Sion) applied to a problem with an unbounded variable.

Difficulty

The obvious argument is to exchange $\sup_\lambda$ and $\min_\alpha$ in $\sup_\lambda\min_\alpha\sum_i\lambda_iF^i_\beta(x,\alpha)$ , since the function is convex in $\alpha$ and affine in $\lambda$ . Minimax theorems for this exchange need compactness of one of the two sets, and the variable $\alpha$ ranges over all of $\mathbb R$ . The step that has to be supplied is a localization: all minimizers in $\alpha$ , for every $\lambda$ at once, lie in one compact interval $\mathcal A$ determined by the minimizer sets of the components. This in turn requires knowing that each $F^i_\beta(x,\cdot)$ has a nonempty bounded minimizer set, which uses $0<\beta<1$ and integrability of the loss: at $\beta=0$ the minimizer set can be a half-line and the localization fails. A second point is attainment: the outer supremum over $\Lambda$ is a maximum only because the inner minimum depends continuously on $\lambda$ .

Formalization scope

Distributions are probability measures on Fin m → ℝ (not densities); Remark 1 of the paper extends all results to general distributions, and a density is a special case. Decisions are Fin n → ℝ, the loss is f : (Fin n → ℝ) → (Fin m → ℝ) → ℝ, and the likelihood distributions are P : Fin l → Measure (Fin m → ℝ) with indices zero-based and [NeZero l].
Every theorem assumes $0<\beta<1$ , that each $P^i$ is a probability measure, and that $f(x,\cdot)$ is integrable under each $P^i$ (the paper's $E|f(x,y)|<\infty$ ).
CVaR is defined by (2) as the infimum of the values of $F_\beta(x,\cdot)$ ; the tail-mean definition and the Rockafellar–Uryasev identity between the two are not part of the mission. The mixture is the finite sum of measures $\sum_i\lambda_iP^i$ , $\Lambda$ is Mathlib's stdSimplex, and WCVaR is the supremum of the image of $\Lambda$ .
Every min and max in the paper is stated as attained, with an explicit minimizer or as IsGreatest/IsLeast; no real sInf or sSup is evaluated on an empty or unbounded set, so no statement can hold through Lean's junk value $0$ .
Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$ , which the printed statement omits and without which the extrema need not exist.
The definitions $F_\beta$ , CVaR, mixture and WCVaR are reusable for any risk-measure development; the interval property of $\arg\min F_\beta$ is of independent use. Proofs of any milestone, and lemmas on the Rockafellar–Uryasev function for general measures, are welcome.

Selected references

S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar and S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

11 thms2 active usersReviewed

Linear Optimization Optimization·Captain: mikedeng1

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 3: If (LP) and (LD) Have Interior Feasible Points, Every Self-Complementary Solution of (HLP) Has τ* > 0Research Paper

Motivation

Linear programming algorithms often compute a solution to an auxiliary problem before extracting a solution to the original primal and dual pair. For a homogeneous self-dual formulation, the extraction requires a positive scaling coordinate. If that coordinate vanishes, the same auxiliary solution may instead describe infeasibility or unboundedness. Ye, Todd, and Mizuno introduced a homogeneous self-dual linear program that can start from arbitrary positive primal and dual slack vectors, even when the original programs have no known feasible point (Ye–Todd–Mizuno 1994).

Their Theorem 3 concerns strictly self-complementary optimal solutions of the auxiliary program. Theorem 9 addresses a different question: under a regularity assumption on the original programs, does a general optimal solution of the auxiliary program still have a positive scaling coordinate? The distinction matters because optimality alone does not require every complementary pair to have a positive member. This mission formalizes the statement of Theorem 9 and the numbered identities that frame it.

Setting

Fix a real matrix $A\in\mathbb R^{m\times n}$ , a right-hand side $b\in\mathbb R^m$ , and a cost vector $c\in\mathbb R^n$ . The primal linear program (LP) minimizes $c^Tx$ subject to $Ax=b$ and $x\ge0$ . Its dual (LD) maximizes $b^Ty$ subject to $A^Ty\le c$ ; $y\in\mathbb R^m$ is unrestricted. The dual slack is $s=c-A^Ty$ .

An interior feasible point of (LP) is an $x$ with $Ax=b$ and every $x_j>0$ . An interior feasible point of (LD) is a $y$ with every component of $c-A^Ty$ positive. “Interior” here is the paper's strict coordinatewise feasibility condition, not the topological interior of an equality-constrained set in ambient space. The existence of such a point implies ordinary feasibility for the corresponding program.

The paper builds an auxiliary program (HLP) from initial vectors $x^0>0$ , $s^0>0$ , and $y^0$ . It uses the derived data

\bar b=b-Ax^0,\qquad \bar c=c-A^Ty^0-s^0,\qquad \bar z=c^Tx^0+1-b^Ty^0.

A point is a tuple $(y,x,\tau,\theta,s,\kappa)$ with $x,s,\tau,\kappa\ge0$ and free $y,\theta$ . Its equality constraints are

\begin{aligned} Ax-b\tau+\bar b\theta&=0,\\ s&=-A^Ty+c\tau-\bar c\theta,\\ \kappa&=b^Ty-c^Tx+\bar z\theta,\\ -\bar b^Ty+\bar c^Tx-\bar z\tau&=-(x^0)^Ts^0-1. \end{aligned}

The objective is to minimize $((x^0)^Ts^0+1)\theta$ . A feasible point is optimal when no feasible point has a smaller objective. The paper calls an optimal point self-complementary, whether or not its complementary pairs satisfy strict inequalities (p. 57, after Theorem 2(v)). After introducing the general construction, the paper fixes $y^0=0$ and $x^0=s^0=e$ , the all-ones vector. That is the instance used in Theorem 9.

Formalization targets

Goal: Theorem 9

If both (LP) and (LD) have interior feasible points, then every self-complementary solution $w^*=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ of this fixed (HLP) satisfies

\tau^*>0.

The theorem quantifies over every optimal point, including those that are not strictly self-complementary. The printed tuple writes $\theta^*=0$ ; Theorem 2(iv) entails that fact from optimality, so it is not an extra hypothesis in the goal (Theorem 9, p. 64).

Supporting targets

Theorem 2(iv) states that (HLP) has zero optimal value and, for every feasible point under arbitrary positive initial $x^0,s^0$ , satisfies

((x^0)^Ts^0+1)\theta=x^Ts+\tau\kappa.

Corollary 4 states that a positive $\kappa$ at an optimum under the fixed initialization entails infeasibility of (LP) or (LD). Equation (9) states the corresponding normalization identity

e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1.

These are separate milestone statements, each tied to its index and page in the paper (Theorem 2(iv), p. 57; equation (9), p. 58; Corollary 4, p. 59).

Significance

Theorem 9 says that the auxiliary model does not lose its positive scale at any optimum when the primal and dual programs are both strictly feasible. With $\tau^*>0$ , the homogeneous primal and dual variables can be divided by $\tau^*$ to recover solutions in the original scale. The result applies even when the auxiliary optimum lacks strict complementarity; that is the additional coverage beyond the strictly self-complementary case of Theorem 3 (Ye–Todd–Mizuno 1994, pp. 58 and 64).

The mathematical result was proved in 1994. This mission's remaining work is a machine-checked proof of the stated regularity result and its supporting claims in the paper's specific (HLP) model. The definitions of the homogeneous feasible set, its slacks, and its optimality relation are reusable for the other results in the same paper. The full algorithm and complexity estimate belong to the other missions in this series.

Difficulty

The optimality condition controls the objective, and Theorem 2(iv) identifies that objective with a sum of complementarity terms. Those facts alone permit $\tau^*=0$ ; they do not force the scaling coordinate to be positive. Theorem 3's assertion for a strictly self-complementary point cannot be applied to an arbitrary optimal point, because its strict support condition may fail. The challenge is to use interior feasibility of both original programs to exclude all zero-scale optima while retaining the full set of HLP optima in the quantifier.

Formalization scope

The Lean model uses finite-dimensional real vectors indexed by Fin m and Fin n, a real matrix $A$ , and a six-field HLP point in the paper's order $(y,x,\tau,\theta,s,\kappa)$ . The standard-form primal and dual feasible sets are reused from a published LP definition with the same minimization and maximization orientation. Paper-specific interior predicates and the homogeneous program are defined locally. Slack fields in an HLP point are constrained to equal their formulas, so they cannot be chosen independently to make a statement true.

The model first defines (HLP) for general $x^0,y^0,s^0$ and then substitutes the paper's choice (7). It treats self-complementarity as objective minimization over the whole feasible set. Defining it by $\theta=0$ or by a complementarity equation would erase the content of Theorem 2(iv). The objective and normalization constants are exact, including the $n+1$ in the fixed instance. No real supremum or infimum is used to define optimality; it is a direct comparison against every feasible point.

The dimensions $m,n$ may be zero. Empty coordinatewise inequalities then have their usual vacuous meaning, but the equations remain in force. In particular the prescribed point $(0,e,1,1,e,1)$ is strictly feasible for every $A,b,c$ , as a separate sorry-free local verification checks. This excludes an empty-feasible-set reading of the HLP definitions. Contributions proving the three numbered milestones, the goal, or reusable finite-dimensional LP lemmas are within scope.

Selected references

Yinyu Ye, Michael J. Todd, and Shinji Mizuno, An $O(\sqrt nL)$ -Iteration Homogeneous and Self-Dual Linear Programming Algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. DOI 10.1287/moor.19.1.53.

7 thms2 active usersReviewed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Negative Dynamic Programming II: With Non-Positive Rewards on Borel Spaces, the Optimal Return Satisfies the Optimality EquationResearch Paper

Motivation

Negative dynamic programming is the study of infinite-horizon sequential decision problems in which every one-stage reward is non-positive and nothing is discounted. Equivalently, a non-negative cost accumulates forever and the controller minimizes its expected total. Stochastic shortest-path problems, optimal stopping with a cost per step, and inventory or replacement models without discounting all have this form. The total cost of a policy can be infinite, and none of the contraction arguments of discounted dynamic programming apply.

Blackwell settled the discounted case on Borel state and action spaces (Blackwell 1965). There the optimal return is Borel measurable and is the unique bounded solution of the optimality equation. Strauch's paper (Strauch 1966) treats the negative case on the same Borel model. One of its main results is that the optimal return still satisfies the optimality equation, even though it need not be Borel measurable.

Timeline. Blackwell (1965): discounted case, Borel spaces. Blackwell (1967, Positive dynamic programming): positive bounded case. Strauch (1966): negative case on Borel spaces. The optimal return is absolutely measurable, $(p,\varepsilon)$ -optimal Markov policies exist, and the optimality equation holds. Bertsekas and Shreve (1978, Stochastic Optimal Control: The Discrete-Time Case) later recast the theory with universally measurable policies, a lower semianalytic optimal cost, and Bellman's equation $J^* = T(J^*)$ under (P), (N) and (D).

Setting

The states $S$ and actions $A$ are non-empty Borel sets. A law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$ . The return $r(s,a,t)$ is a Borel function with $-\infty < r \le 0$ whose expectation $\int r(s,a,t)\,dq(t\mid s,a)$ is finite for every $(s,a)$ . A policy $\pi = (\pi_1,\pi_2,\dots)$ draws the $n$ th action from a kernel $\pi_n(\cdot\mid s_1,a_1,\dots,s_n)$ that may depend on the whole history. A Markov policy $(f_1,f_2,\dots)$ uses measurable maps $f_n:S\to A$ , and a stationary policy $f^{(\infty)}$ uses one map at every stage. The expected return from the initial state $s$ is

I(\pi)(s) = \sum_{n\ge1} E^\pi_s\, r(s_n,a_n,s_{n+1}) \in [-\infty,0],

and the optimal return is

v^*(s) = \sup_\pi I(\pi)(s),

the supremum over all policies. Write $M(S)$ for the non-positive, extended real-valued Borel functions on $S$ . For $u\in M(S)$ and an action $a$ ,

T_a u(s) = \int \big[r(s,a,t) + u(t)\big]\,dq(t\mid s,a).

$T$ denotes the same operator for a measurable rule $f$ in place of $a$ , and $U = \sup_n T_n$ for a Markov policy $(f_1,f_2,\dots)$ . A policy $\pi^*$ is $(p,\varepsilon)$ -optimal, for a probability $p$ on $S$ , if $p\{I(\pi^*) \ge v^* - \varepsilon\} = 1$ . The Lean development uses the same names: Problem, I, In, vstar, T, Ta, U, IsPEOptimal, Conserves.

Formalization targets

Goal: the optimality equation (Theorem 8.2, negative case)

v^*(s) = \sup_{a\in A} T_a v^*(s) \qquad\text{for all } s\in S.

The equation involves no constants and no regularity hypotheses on $v^*$ .

Milestones

Theorem 5.2 (a)–(g): monotonicity, translation, sup-, limit- and selection properties of $U$ .
Theorem 6.1: if $Uv\ge v$ for $v\in M(S)$ , some Markov policy generated from $\hat\pi$ has $I(\pi)\ge v-\varepsilon$ .
Lemma 6.2: $U$ conserves $\sup_n I({}^n\pi)$ and $\lim_n U^n \sup_n I({}^n\pi)$ .
Theorem 6.2: one Markov policy comes within $\varepsilon$ of the supremum of the returns of countably many Markov policies.
Lemma 7.1, Lemma 7.2: measurability of $(s,\nu)\mapsto\int u(s,x)\,d\nu(x)$ , and Borel measurability of the set of pairs $(s, e_\pi(s))$ , where $e_\pi(s)$ is the law of the future under $\pi$ .
Theorem 7.1: $v^*$ is absolutely measurable.
Theorem 8.1: for every $p$ and $\varepsilon>0$ a $(p,\varepsilon)$ -optimal Markov policy exists.

Optional extras: Corollary 6.1 and Theorems 6.3, 6.4, 6.5 and 8.4 (bounds and characterizations for Markov policies).

Significance

The result. The optimality equation is the entry point to every structural statement about optimal policies in the negative case. With it, a stationary policy whose rule attains the supremum in $\sup_a T_a v^*$ can be tested for optimality. Value iteration and policy improvement can be compared with $v^*$ . The gap between the negative case and the discounted and positive cases can be located precisely: in the negative case $v^*$ satisfies the equation, but it need not be its unique or extremal solution. Along the way the paper proves that $v^*$ is absolutely measurable and that nearly optimal Markov policies exist for every initial distribution. These two facts are used repeatedly in later Borel-space dynamic programming.

Formalizing it. The results are proved; none is machine-checked. A formal development would contain the first Lean treatment of a total-reward Markov decision process on Borel spaces with possibly infinite returns. It would include the policy-dependent law of the future via Ionescu-Tulcea, the measurability of the optimal return over all randomized history-dependent policies, and the Bellman equation for a non-measurable value function. Bertsekas–Shreve's version of the optimality equation (universally measurable policies) appears on the platform as a separate open statement. It concerns a different policy class and is not the statement posed here.

Difficulty

Two steps of the obvious argument fail. First, the classical proof of the optimality equation picks, at each next state $t$ , a policy that is $\varepsilon$ -optimal from $t$ and concatenates. Without measurable selection this concatenation is not a policy. The set of $t$ where a given policy is $\varepsilon$ -optimal need not be Borel, and $v^*$ itself need not be Borel measurable, so even $\int v^*\,dq$ needs justification. Second, the contraction argument of the discounted case is unavailable. $U$ does not contract, it conserves $v+c$ along with $v$ , and value iteration from $0$ can converge to a function strictly above $v^*$ . The paper's Example 6.1 shows that the limit of $U^n0$ , the best return of generated Markov policies, and the best stationary return can all differ. Any argument has to work with policies that are only nearly optimal, and only outside sets of measure zero that depend on the initial distribution.

Formalization scope

States and actions are non-empty standard Borel types. Policies are the published Blackwell plans (DiscountedDP.Stationary.Plan): randomized and history-dependent, one Markov kernel per decision, with decisions numbered from $0$ (Lean's π.κ n is the paper's $\pi_{n+1}$ ). Markov policies are MarkovPlan; " $\pi$ -generated" and $G(\hat\pi)$ are the published IsGenerated and IsGeneratedPlan.
Only the negative case is formalized: $r\le0$ real-valued, $qr$ integrable, $\beta=1$ . The discounted and positive parts of Theorems 5.2, 7.1, 8.1 and 8.2, including the uniqueness and minimality clauses of Theorem 8.2, are not stated.
Returns take values in EReal and are computed as minus a lower Lebesgue integral (lintegral) of the non-negative loss. A Bochner integral is never used for a return: it would map $-\infty$ to $0$ and make the goal false or vacuous.
$v^*$ is the supremum over all plans. It is not assumed measurable and is never replaced by a measurable modification. $T_a v^*$ is a lintegral of a possibly non-measurable function, which equals the completion integral because $v^*$ is absolutely measurable (Theorem 7.1).
Explicit readings of the page: the hypothesis $u\in M(S)$ of each operator statement is IsNegM u. Theorem 5.2(b) assumes $u+c\in M(S)$ . " $U$ conserves $v$ " includes $v\in M(S)$ . Lemma 6.2 asserts that the limit defining $v_\pi$ exists. Theorem 6.2 states $\ge$ everywhere and $>$ where $\sup_j I(\pi^j) > -\infty$ (the printed $>$ fails where the supremum is $-\infty$ ). $(p,\varepsilon)$ -optimality is " $p$ -almost everywhere". Absolute measurability is NullMeasurable for every probability measure. $P(X)$ carries the Giry σ-field. The extra Theorem 8.4 reads the printed " $I(\pi) < u$ " as " $\le$ " (the strict reading is false).
Reusable infrastructure: the negative model, the Ionescu-Tulcea law of the future (futureLaw), and the measurability lemmas for integrals against random measures. Contributions of measurable-selection and analytic-set results (projections of Borel sets are universally measurable; von Neumann selection) are welcome and needed.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. Blackwell, Positive Dynamic Programming, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
L. E. Dubins and L. J. Savage, How to Gamble If You Must, McGraw-Hill, 1965.
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

21 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research III: Minimum Average Journey Time on Alternative Routes — Equal Marginal Times ε and the Closed Forms (32)–(33)Research Paper

Motivation

J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259) introduced the two criteria that still organise traffic assignment. When a flow of traffic can choose between several routes from one origin to one destination, the paper (p. 345) considers two ways the traffic might divide:

the journey times on all the routes actually used are equal, and less than those that a single vehicle would experience on any unused route;
the average journey time is a minimum.

The first is now called Wardrop's first principle, or user equilibrium: no driver can shorten their trip by switching route. The second, Wardrop's second principle, is the system optimum: it "minimizes the vehicle-hours spent on the journey". The gap between the two is the quantity later studied as the price of anarchy of selfish routing (Roughgarden and Tardos, J. ACM 2002), and the marginal-cost characterisation of the system optimum underlies congestion pricing (Beckmann, McGuire and Winsten, Studies in the Economics of Transportation, 1956).

This mission formalizes the paper's solution of criterion (2) on parallel routes, section (2) Minimum Average Time, pp. 345–347. Mission II of the same series treats criterion (1) on the same model.

Setting

A total additional flow $Q$ is divided among $D$ alternative routes $i = 1, \dots, D$ . Route $i$ carries an additional flow $q_i$ and has journey time, equation (22),

t_i(q_i) = \frac{b_i}{1 - q_i/p_i},

where $b_i > 0$ is the journey time on route $i$ with no additional flow and $p_i > 0$ is the additional flow at which its speed would fall to zero (routeTime b p i x). A feasible split of $Q$ is a vector $q$ with $0 \le q_i < p_i$ for every $i$ and $\sum_i q_i = Q$ (IsFeasible p Q q).

The number of additional vehicles on route $i$ at an instant is $z_i = q_i t_i$ , and $Z = \sum_i z_i$ (totalExtra b p q). The average journey time is, equations (25)–(26),

T = \sum_{i=1}^D \frac{q_i t_i}{Q} = \frac{Z}{Q}

(avgTime b p Q q). Criterion (2) asks for a feasible split $q$ with $T(q) \le T(z)$ for every feasible split $z$ (IsMinAvgTime b p Q q).

The marginal journey time of route $i$ is $d(q_i t_i)/dq_i$ , the rate at which $Z$ grows when flow is added to that route. For a threshold $\varepsilon$ , $U(\varepsilon) = \{i : b_i < \varepsilon\}$ (usedSet b ε) is the set of routes whose marginal time at zero flow lies below $\varepsilon$ ; with the routes labelled so that $b_1 < \dots < b_D$ it is the paper's "first $j$ routes".

Formalization targets

Goal: the closed forms (32)–(33)

For $b_i, p_i > 0$ and $0 < Q < \sum_i p_i$ , every split $q$ minimizing $T$ admits a threshold $\varepsilon > 0$ with $\sum_{i \in U} p_i > Q$ , where $U = U(\varepsilon)$ , such that

q_h = \begin{cases} p_h\left\{1 - \dfrac{\left(\sum_{i\in U} p_i - Q\right)\sqrt{b_h}}{\sum_{i\in U} p_i\sqrt{b_i}}\right\}, & b_h < \varepsilon,\\[1ex] 0, & \text{otherwise,}\end{cases} \qquad T = \frac1Q\left\{\frac{\left(\sum_{i\in U} p_i\sqrt{b_i}\right)^2}{\sum_{i\in U} p_i - Q} - \sum_{i\in U} p_i b_i\right\}.

Milestones

(29)–(30): $d(q_i t_i)/dq_i = b_i/(1 - q_i/p_i)^2$ , equal to $b_i$ at $q_i = 0$ .
(27)–(28): at a minimum, all routes in use have the same marginal time $\varepsilon$ .
A route $j$ with $b_j \ge \varepsilon$ is not used.
The routes in use are exactly those with $b_i < \varepsilon$ , and on them $1 - q_i/p_i = \sqrt{b_i/\varepsilon}$ .
(31): $\sum_{i\in U} p_i - Q = \sum_{i\in U} p_i\sqrt{b_i/\varepsilon}$ .

A companion theorem states that a minimizing split exists whenever $0 < Q < \sum_i p_i$ .

Significance

The closed forms give the system-optimal assignment on parallel routes with the travel-time law (22) explicitly: which routes carry traffic, how much, and the resulting average time. Together with the equal-times solution (23)–(24) of mission II they quantify, for this model, how much average time selfish route choice costs; the paper's Fig. 8 compares the two numerically and finds the difference small in its example. The marginal-time conditions (27)–(28) are the parallel-route instance of the general statement that a system optimum is an equilibrium with respect to marginal costs.

The derivation on pp. 346–347 is a first-order argument that the paper does not make rigorous: it assumes a minimizer exists, that it satisfies the stationarity condition, and leaves (32)–(33) to "a few lines of algebra". This mission produces the rigorous version, including existence. No machine-checked statement of (27)–(33) is on the platform; the related platform items on Wardrop equilibria concern the Beckmann potential and atomic congestion games, not the system optimum of this model.

Difficulty

The stationarity condition (27) comes from moving an infinitesimal flow between two routes in use. Turning this into a theorem needs the one-sided version at unused routes, since $q_j = 0$ is a boundary point and the condition there is an inequality, and needs the constraint $\sum_i q_i = Q$ to be preserved by the perturbation. The step "only the first $j$ routes will be in use" is the converse direction: a route with $b_i < \varepsilon$ that carries no flow must be shown to contradict minimality, not just to violate the equal-marginals equation.

Existence is not a compactness argument on a closed set: the feasible set is open in the direction $q_i \to p_i$ , where $q_i t_i \to \infty$ , and that coercivity has to be used. The algebra from (31) to (32)–(33) is routine once the set $U$ and the value of $\varepsilon$ are fixed.

Formalization scope

Routes are indexed by Fin D; all quantities are real. The standing hypotheses are $b_i > 0$ , $p_i > 0$ , $0 < Q$ and $Q < \sum_i p_i$ ; without the last the feasible set is empty and every statement about a minimizer is vacuous, and with $Q \le 0$ the average time $Z/Q$ is undefined. Feasibility requires $q_i < p_i$ , of the minimizer and of every competitor: at $q_i = p_i$ Lean evaluates $b_i/0$ as $0$ , which would let a "minimizer" place flow at capacity for free. The paper's labelling $b_1 < \dots < b_D$ is not assumed; "the first $j$ routes" is $U(\varepsilon)$ . Marginal times are written in the closed form (29), and milestone 1 identifies that form with the derivative via HasDerivAt. Minimality is stated for $T$ , the paper's criterion, not for $Z$ .

Corrected slip. The paper prints the denominator of (33) as $\sum_{i=1}^j p_i b_i$ . The formalization uses $\sum_{i=1}^j p_i\sqrt{b_i}$ : from (31), $1/\sqrt\varepsilon = (\sum p_i - Q)/\sum p_i\sqrt{b_i}$ , and $q_h = p_h(1 - \sqrt{b_h/\varepsilon})$ . The printed form is not dimensionally consistent and gives wrong flows, e.g. for $b = (4, 9)$ , $p = (10, 10)$ , $Q = 35/3$ . Equation (32) is correct as printed.

The goal cannot be satisfied trivially: the threshold $\varepsilon$ is existential and the flows and $T$ are pinned to explicit formulas, and the companion existence theorem shows the hypothesis IsMinAvgTime is met for every admissible $Q$ . The route time and feasible split come from the shared WardropTraffic.EqualTimes.Setting definition; this mission adds the total and average time and criterion (2). Proofs of any item, including the existence theorem and a uniqueness statement (the objective is strictly convex), are welcome.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Instn Civ. Engrs Part II 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
M. Beckmann, C. B. McGuire, C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
T. Roughgarden, É. Tardos, How bad is selfish routing?, J. ACM 49(2) (2002), 236–259. https://doi.org/10.1145/506147.506153

8 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Understanding the Efficiency of Multi-Server Service Systems I: With Poisson Arrivals and Finitely Many Service-Time Values of Mean 1, the Number of Busy Servers in M/G/∞ Is Poisson(λ)Research Paper

Motivation

Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate $\lambda$ , how many servers $s$ are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule

s = \lambda + \gamma\sqrt{\lambda},

where the grade of service $\gamma > 0$ sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.

Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers $N$ in the IS model is Poisson with mean $\lambda$ , its mean and variance are both $\lambda$ , so the event "more than $s$ servers busy" has roughly constant probability when $s - \lambda$ is a fixed multiple of $\sqrt\lambda$ . The Poisson law of $N$ is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean $1$ (M/G/∞ with finite support).

Timeline:

The stationary number in system of M/G/∞ is classically known to be Poisson with mean $\lambda \cdot E[S]$ for general service-time laws (Palm's theorem; see Gross et al., Fundamentals of Queueing Theory).
Halfin and Whitt (Operations Research 29, 1981) proved the heavy-traffic limit theorem that justifies square-root staffing for GI/M/s queues.
Whitt (1992) gave the elementary IS derivation formalized here, with the finite-support M/G/∞ case argued through splitting a Poisson stream into independent class streams.

Setting

Time is measured in units of the mean service time. Let $T_0, T_1, T_2, \dots$ be i.i.d. exponential random variables with rate $\lambda > 0$ , the interarrival times, and let $\tau_n = T_0 + \cdots + T_{n-1}$ be the $n$ -th arrival epoch. The arrival counting process $A(t)$ is the number of $n \ge 1$ with $\tau_n \le t$ , the number of arrivals in $(0, t]$ . This is a Poisson process of rate $\lambda$ .

Customers are numbered $k = 0, 1, 2, \dots$ ; customer $k$ arrives at $\tau_{k+1}$ , is served at once, and has service time $D_k$ . Following the paper (proof of Proposition 2.3, p. 712), an arrival at time $t$ is counted and a departure at time $t$ is not, so customer $k$ is present at $t$ iff $\tau_{k+1} \le t < \tau_{k+1} + D_k$ . The number of busy servers is

N(t) = \#\{k : \tau_{k+1} \le t < \tau_{k+1} + D_k\}.

For the M/G/∞ case fix $m \ge 1$ classes with probabilities $p_1, \dots, p_m$ and values $d_1, \dots, d_m \ge 0$ . Each customer carries a class label $J_k$ , the labels are i.i.d. with $P(J_k = i) = p_i$ and independent of the interarrival times, and $D_k = d_{J_k}$ . The class- $i$ busy count is $N_i(t) = \#\{k : J_k = i,\ \tau_{k+1} \le t < \tau_{k+1} + d_i\}$ .

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

If $\sum_{i=1}^m p_i d_i = 1$ and $t > \max_i d_i$ , then

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

The law depends on the service-time distribution only through its mean.

Milestones

Proposition 2.3 (p. 712): with unit service times, $N(t) = A(t) - A(t-1)$ , pathwise.
Proof of Proposition 2.4 (p. 712): for $t \ge 1$ , $A(t) - A(t-1)$ has the same law as $A(1)$ .
Proposition 2.4 (p. 712): in M/D/∞ with unit service times, $N(t) \sim \mathrm{Poisson}(\lambda)$ for each $t > 1$ .
§2.5, splitting (p. 713): the class- $i$ arrivals form independent Poisson streams of rates $\lambda p_i$ ; stated as independence and Poisson laws of the class counts in one window $(a_i, b_i]$ per class.
§2.5, "Hence" (p. 713): for $t > \max_i d_i$ , the $N_i(t)$ are independent, $N_i(t) \sim \mathrm{Poisson}(\lambda p_i d_i)$ , and $N(t) = \sum_i N_i(t)$ almost surely.

A companion item, Proposition 2.1 (p. 710), states that (2) implies $\lambda = s + \gamma^2/2 - \gamma\sqrt{s + \gamma^2/4}$ and $s - \gamma\sqrt s \le \lambda \le s - \gamma\sqrt s + \gamma^2/2$ , connecting (2) to the utilization equation $\lambda = s - \gamma\sqrt s$ .

Significance

The goal is the step that turns the IS heuristic from a special case into a statement about general service: since $N(t)$ is Poisson with mean $\lambda$ whatever the finite service-time law of mean $1$ , the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that $s$ -server congestion is nearly insensitive to the service distribution beyond its mean when $s$ is large.

The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:

a Poisson process built from exponential interarrival times, with the stationary-increment property derived rather than assumed;
Poisson splitting (thinning by i.i.d. labels) with independence of the class streams, a tool reused throughout queueing and inventory theory;
the M/G/∞ Poisson law for discrete service times, complementing the open platform items ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.

The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law $A(t) \sim \mathrm{Poisson}(\lambda t)$ ) is related but distinct from milestone 2, which concerns the increment over $(t-1, t]$ .

Difficulty

The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time $t - 1$ : the residual time to the next arrival after $t-1$ must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by $t-1$ ), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows $(t - d_i, t]$ of different classes make this unavoidable.

Formalization scope

The arrival process is the published definition QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.
The model IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.
Counts are Set.ncard, which is $0$ on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by $t$ , and the decomposition $N(t) = \sum_i N_i(t)$ is stated almost surely. Poisson laws are stated pointwise, $P(X = k) = e^{-c}c^k/k!$ , avoiding pushforwards of possibly non-measurable maps.
Standing conventions: service rate $1$ ; the system starts empty at time $0$ ; arrival counted at $t$ , departure not; "steady state" means the law at each fixed $t > \max_i d_i$ , with no limit $t \to \infty$ ; the paper's $1 \le i \le n$ is Fin m. The constraint $\sum_i p_i d_i = 1$ forces $m \ge 1$ , and the label law forces $p_i \ge 0$ and $\sum_i p_i = 1$ . Added hypotheses: $d_i \ge 0$ (service times are nonnegative) and, in Proposition 2.1, $\gamma > 0$ (the paper's grade of service).
Infrastructure welcome: memorylessness of the Poisson process at a fixed time, Poisson thinning with independent marks, and the finite-sum version of Mathlib's IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.

Selected references

W. Whitt, Understanding the efficiency of multi-server service systems, Management Science 38(5):708–723, 1992. https://doi.org/10.1287/mnsc.38.5.708
S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

8 thms2 active usersReviewed

Analysis Stochastic Systems·Captain: mikedeng1

The G/GI/N Queue in the Halfin–Whitt Regime 1: The Regulator Equation z(t) = x(t) + ∫₀ᵗ (z(t−s)+a)⁺ dB(s) Has a Unique Càdlàg Solution, Lipschitz on Bounded Intervals and Measurable in xResearch Paper

Motivation

The $G/GI/N$ queue has $N$ identical servers, a general arrival process, and independent service times with a common distribution $F$ . In the Halfin–Whitt regime the number of servers and the offered load grow together, so that the fraction of delayed customers stays strictly between $0$ and $1$ . This is the standard asymptotic model of large call centers and service systems (Halfin and Whitt, Operations Research 29, 1981, doi:10.1287/opre.29.3.567). For exponential service times the diffusion limit has been known since 1981; for general service distributions the queue length is no longer Markov, and its limit requires a different device.

Reed (Annals of Applied Probability 19, 2009, arXiv:0912.2837) supplied that device. The number in system $Q$ satisfies a nonlinear convolution equation, (2.8) on p. 9 of the paper, in which the only nonlinearity is the term $\int_0^t (Q(t-s)-N)^+\,dF(s)$ . Section 3 of the paper isolates that equation as a deterministic regulator map: a map that takes an input path to the unique solution of the equation. Its fluid limit (Theorem 4.1) and diffusion limit (Theorem 5.1) are both obtained by applying this map, through the continuous mapping theorem, to the limits of simpler free processes. The regulator map plays here the role that the one-sided reflection map plays in conventional heavy-traffic theory.

Timeline:

1981. Halfin and Whitt: the diffusion limit for exponential service times.
2000. Puhalskii and Reiman: the $GI/PH/N$ case, with phase-type service (MR1778580).
2004. Jelenković, Mandelbaum and Momčilović: deterministic service times (MR2074672).
2009. Reed: general service times, via the regulator map of Proposition 3.1. This mission covers that proposition.

Setting

A path is a function $x:[0,\infty)\to\mathbb R$ . It is càdlàg if it is right continuous everywhere and has a finite left limit at every $t>0$ . $D[0,\infty)$ is the set of càdlàg paths. For $T\ge0$ the supremum metric on $[0,T]$ is $\|x\|_T=\sup_{0\le t\le T}|x(t)|$ .

Let $B$ be a cumulative distribution function on $\mathbb R$ , that is, $B(t)=\mu((-\infty,t])$ for a probability measure $\mu$ , and let $a\in\mathbb R$ . Write $y^+=\max(y,0)$ . For an input $x\in D[0,\infty)$ , the regulator equation (3.1) asks for a path $z\in D[0,\infty)$ with

z(t)=x(t)+\int_{[0,t]}\big(z(t-s)+a\big)^+\,dB(s),\qquad t\ge0 .

The integral runs over the closed interval $[0,t]$ , so an atom of $B$ at $0$ counts. The regulator map $\varphi^a_B$ sends $x$ to the solution $z$ . The paper applies it with $B=F$ , the service-time distribution: $a=-1$ for the fluid-scaled queue and $a=0$ for the diffusion-scaled one.

The proof works with the operator $\Psi^a_B(u)(t)=\int_{[0,t]}(u(t-s)+a)^+\,dB(s)$ and the successive approximations $u_0=0$ , $u_{n+1}=x+\Psi^a_B(u_n)$ of (A.3).

$D[0,\infty)$ carries the Kolmogorov σ-algebra, the one generated by the evaluations $x\mapsto x(t)$ , $t\ge0$ . In the Lean development the objects are IsCadlag, supNorm, Dpath, SolvesRegulator, psi and picard.

Formalization targets

Goal: Proposition 3.1

Assume $\mu(\{0\})<1$ . Then there is a map $\varphi^a_B:D[0,\infty)\to D[0,\infty)$ with the following properties:

$\varphi^a_B(x)$ solves (3.1) for every $x$ ;
every càdlàg solution of (3.1) agrees with $\varphi^a_B(x)$ on $[0,\infty)$ ;
for each $T\ge0$ there is a constant $C_T$ with

\|\varphi^a_B(x_1)-\varphi^a_B(x_2)\|_T\le C_T\,\|x_1-x_2\|_T\quad\text{for all } x_1,x_2\in D[0,\infty);

$\varphi^a_B$ is measurable for the Kolmogorov σ-algebra.

The constant $C_T$ is not fixed. The proof gives $(1-\varepsilon)^{-\lceil T/\delta\rceil}$ , but the goal asserts only its existence.

Milestones, in the order of the paper's proof

Point mass at $c>0$ , (A.1)–(A.2). Equation (3.1) is the recursion $z=x$ on $[0,c)$ and $z(t)=x(t)+(z(t-c)+a)^+$ for $t\ge c$ . Its solution is unique, and $\|z_1-z_2\|_t\le k\|x_1-x_2\|_t$ for $(k-1)c\le t<kc$ .
Uniqueness. Assume $B(y+\delta)-B(y)<\varepsilon<1$ for all $y\ge0$ and $\mu([0,\delta])<\varepsilon$ . Then two càdlàg solutions agree on $[0,\infty)$ .
Lipschitz continuity. Under the same assumption, $\|z_2-z_1\|_{k\delta}\le(1-\varepsilon)^{-k}\|x_2-x_1\|_{k\delta}$ for every $k\ge1$ .
Existence. Under the same assumption, the successive approximations converge uniformly on every $[0,T]$ to a càdlàg solution.
Measurability of $\Psi^a_B$ . $\Psi^a_B$ maps càdlàg paths to càdlàg paths, and $u\mapsto\Psi^a_B(u)(t)$ is measurable for each $t\ge0$ .
Example 1. For unit deterministic service times, the fluid equation (4.7) has the unique solution $\bar Q(t)=1+t-\lfloor t\rfloor$ .
Proof of Corollary 5.1. Take equilibrium initial conditions. The input of (4.7) is then identically $1$ , and $\bar Q\equiv1$ is the unique solution.

Significance

Proposition 3.1 is the deterministic core of the paper. Uniqueness makes the queue length a well-defined function of its free process. Lipschitz continuity in the topology of uniform convergence on compacts carries convergence of the inputs over to convergence of the outputs. Measurability is needed because the inputs are random: it makes the output a random element of $D[0,\infty)$ , so that the continuous mapping theorem applies. Without the proposition neither Theorem 4.1 nor Theorem 5.1 can be stated in the form the paper gives. Example 1 and Corollary 5.1 are the two explicit solutions the paper extracts from it: a periodic, discontinuous sawtooth, and a constant.

The proposition is proved in the paper's Appendix (pp. 32–36). As far as the platform's records show, none of it has been formalized. The mission produces a machine-checked version with every convention fixed. It also corrects the statement: as printed, the proposition fails when $B$ is the unit mass at $0$ , because the equation then reads $z(t)=x(t)+(z(t)+a)^+$ . With $a=0$ and $x\equiv1$ this has no solution. The goal therefore carries the hypothesis $\mu(\{0\})<1$ . That hypothesis holds for every service distribution of mean $1$ on $[0,\infty)$ , which is the only case the paper uses. It also covers the mixed cases that fall between the two cases of the printed proof, such as an atom at $0$ together with mass elsewhere.

Theorems 4.1 and 5.1 themselves, which are weak convergence in $D[0,\infty)$ with the Skorohod $J_1$ topology, are not part of this mission.

Difficulty

The equation is a Volterra equation with a nonlinear but $1$ -Lipschitz integrand. The first idea is to treat it as a contraction in $\|\cdot\|_T$ . That fails: the kernel $B$ has total mass $1$ , so on $[0,T]$ the operator $\Psi^a_B$ is only nonexpansive, not contractive. The contraction has to be recovered locally, from windows of length $\delta$ on which $B$ puts mass less than $1$ . This works only if such windows exist, and they do not exist when $B$ is a point mass at $0$ .

Atoms are the second difficulty. With atoms, $t\mapsto\Psi^a_B(u)(t)$ is càdlàg but not continuous, and the closed-interval convention matters at every step. The third is measurability. The map $u\mapsto\int(u(t-s)+a)^+\,dB(s)$ is not continuous in $u$ for the Skorohod topology when $B$ has atoms, so the paper splits $B$ into its continuous and discrete parts.

Formalization scope

Paths. A path is ℝ → ℝ, and only its values on $[0,\infty)$ are constrained or read. Every equation is asserted for $t\ge0$ , and every uniqueness claim is equality on $[0,\infty)$ (Set.EqOn … (Set.Ici 0)). $D[0,\infty)$ is the structure Dpath of càdlàg paths.
Integrals. $B$ is a probability measure $\mu$ on $\mathbb R$ . $\int_0^t\cdots dB(s)$ is the integral over the closed interval Set.Icc 0 t, so it includes an atom at $0$ , and mass on $(-\infty,0)$ never enters.
Explicit readings of the paper's phrases.
- "Unique solution in $D[0,\infty)$ " means unique among càdlàg paths, up to equality on $[0,\infty)$ .
- "Lipschitz continuous in the topology of uniform convergence over bounded intervals" means $\forall T\ \exists C_T\ \forall x_1,x_2$ . The constant is chosen before the inputs.
- "Measurable with respect to the Borel σ-field generated by the Skorohod $J_1$ topology" means measurable for the Kolmogorov σ-algebra generated by the evaluations at times $t\ge0$ . The paper uses this identification on p. 35, and it is Theorem 16.6 of Billingsley (1999). $J_1$ is not defined.
- "Uniform convergence" in the existence proof means $\|u_n-u^\star\|_T\to0$ for every $T$ .
Added hypothesis in the goal: $\mu(\{0\})<1$ (see Significance).
Window conditions in milestones 2–4. These are the paper's $B(y+\delta)-B(y)<\varepsilon$ for $y\ge0$ , plus $\mu([0,\delta])<\varepsilon$ for the first window, which the proof uses as " $B(\delta)<\varepsilon$ ".
Junk values. The real supremum $\|\cdot\|_T$ and the Bochner integral take junk values (zero) on unbounded or non-integrable data. Every statement applies them only to càdlàg paths, which are bounded and measurable on $[0,T]$ . This is also why solutions are required to be càdlàg: a solution taken among arbitrary functions could exploit the zero value of a non-integrable integral. Likewise, the goal cannot be satisfied by a $\varphi$ whose values solve (3.1) only vacuously, and cannot be satisfied by dropping the càdlàg requirement on the output.
Printed slips corrected in the Lean and disclosed in the items:
- (A.2)'s step " $k<t\le(k+1)c$ " means $kc\le t<(k+1)c$ ;
- (A.3) "for $n\ge1$ " starts at $n=0$ ;
- (4.18) has $\bar Q(t)$ on the right where (4.7) gives $\bar Q(t-1)$ ;
- Corollary 5.1 cites "Theorem 5.1 of Section 4", meaning Theorem 4.1.

Infrastructure. A complete development needs the following, all reusable beyond this mission:

càdlàg paths on a half-line and their boundedness on compacts;
Lebesgue–Stieltjes convolution integrals of càdlàg paths against a probability measure;
the Kolmogorov σ-algebra on path space.

The related platform objects are of other shapes:

ChenWhitt93.Reflection.Basic (IsCadlagOn, vector-valued paths on $[0,T]$ ) and EthierKurtz_HasCadlagPaths (processes indexed by $\mathbb R_{\ge0}$ ) define càdlàg paths in other settings.
BellmanDP.Inventory.renewal_equation_exists_unique is a linear renewal equation with a density kernel of mass below $1$ .

Contributions are welcome on any milestone, in any order. The windowed estimates (milestones 2–4) and the measurability step (milestone 5) are independent of each other.

Selected references

J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Annals of Applied Probability 19(6), 2009, 2211–2269. arXiv:0912.2837v1, doi:10.1214/09-AAP609
S. Halfin, W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981, 567–588. doi:10.1287/opre.29.3.567
A. A. Puhalskii, M. I. Reiman, The multiclass GI/PH/N queue in the Halfin–Whitt regime, Advances in Applied Probability 32, 2000, 564–595. MR1778580
P. Jelenković, A. Mandelbaum, P. Momčilović, Heavy traffic limits for queues with many deterministic servers, Queueing Systems 47, 2004, 53–69. MR2074672
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Chapter 16. doi:10.1002/9780470316962

13 thms2 active usersReviewed

Linear Optimization Optimization Theoretical Computer Science·Captain: mikedeng1

Fast Approximation Algorithms for Fractional Packing and Covering Problems 2: An ε-Relaxed Decision Procedure for Fractional Covering Using O(m + ρ log² m + ε⁻²ρ log(m/ε)) Oracle CallsResearch Paper

Motivation

Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form $Ax\ge b$ with $A\ge 0$ : the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and the cutting-stock relaxation all have this shape. General-purpose LP methods solve such problems exactly but slowly. Plotkin, Shmoys and Tardos showed that when a fast subroutine can optimize a linear function over the convex set, a Lagrangean-relaxation scheme with an exponential potential finds an approximate solution with a number of subroutine calls that depends on a width parameter and on the accuracy, not on the dimension of the set (Plotkin, Shmoys, Tardos, Cornell ORIE TR 999, 1992; journal version Math. Oper. Res. 20(2), 1995).

The covering half of that paper (§3) is the object of this mission. It is the template for later covering and mixed packing–covering solvers, including those of Garg and Könemann (SIAM J. Comput. 2007) and Young (FOCS 2001).

Setting

Fix integers $m\ge1$ , $n$ . Let $A$ be a real $m\times n$ matrix with nonnegative entries and rows $a_1,\dots,a_m$ , write $a_ix=\sum_j A_{ij}x_j$ , let $b\in\mathbb R^m$ with $b>0$ , and let $P\subseteq\mathbb R^n$ be a nonempty convex set contained in the nonnegative orthant.

COVERING asks whether there is $x\in P$ with $Ax\ge b$ ; such an $x$ is an exact solution. For $\varepsilon>0$ , an $\varepsilon$ -approximate solution is $x\in P$ with $Ax\ge(1-\varepsilon)b$ .
For $x\in\mathbb R^n$ , $\lambda(x)=\min_i a_ix/b_i$ is the largest $\lambda$ with $Ax\ge\lambda b$ , and $\lambda^*=\max\{\lambda(x):x\in P\}$ . A point $x\in P$ is $\varepsilon$ -optimal when $\lambda(x)\ge(1-\varepsilon)\lambda^*$ .
The width is $\max_i\max_{x\in P}a_ix/b_i$ ; a number $\rho>0$ with $a_ix\le\rho\,b_i$ for all $x\in P$ and all $i$ is a width bound.
Subroutine (7) receives $y\in\mathbb R^m$ , $y\ge0$ , and returns $\tilde x\in P$ maximizing $y^tAx$ over $P$ ; $C_{\mathcal C}(y)$ is that maximum.
For $\alpha>0$ , the dual solution corresponding to $x$ is $y_i=\frac1{b_i}e^{-\alpha a_ix/b_i}$ , and the potential is $\Phi=y^tb=\sum_ie^{-\alpha a_ix/b_i}$ .
The relaxed optimality conditions are $(\mathcal C1)$ : $(1+\varepsilon)\lambda\,y^tb\ge y^tAx$ , and $(\mathcal C2)$ : $C_{\mathcal C}(y)-y^tAx\le\varepsilon\,(C_{\mathcal C}(y)+y^tb)$ .
IMPROVE-COVER $(x,\varepsilon)$ (Figure 3) sets $\lambda_0=\lambda(x)$ , $\alpha=4\lambda_0^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ and $\sigma=\varepsilon/(4\alpha\rho)$ ; while $\lambda(x)\le2\lambda_0$ and $\mathcal C2$ fails, it moves $x$ to $(1-\sigma)x+\sigma\tilde x$ , $\tilde x$ the subroutine's answer for the current dual solution.
The covering algorithm obtains a start with $Ax\ge\frac1mb$ from $m$ subroutine calls, calls IMPROVE-COVER with $\varepsilon=1/6$ until $\mathcal C2$ holds or an exact solution appears, then halves $\varepsilon$ phase by phase.

The Lean names match: rowVal, lam, WidthBound, IsMaxOracle, C1, C2, dualY, potential, improveCover, initCover, coverAlgorithm, in the namespace FracPackCover.Covering.

Formalization targets

Goal: Theorem 3.7 (p. 21)

For every instance as above, every width bound $\rho$ , every exact maximization oracle and every $0<\varepsilon_0<1$ , the covering algorithm stops after at most

N=m+\big(\lceil\log_2m\rceil+1\big)\big(2+4320\,\rho\ln(24m)\big)+2\lceil\log_2\varepsilon_0^{-1}\rceil+9408\,\rho\,\varepsilon_0^{-2}\ln\frac{24m}{\varepsilon_0}

calls to subroutine (7), and either returns $x\in P$ with $Ax\ge(1-\varepsilon_0)b$ , or reports that no $x\in P$ has $Ax\ge b$ , correctly. This is the paper's $O(m+\rho\log^2m+\varepsilon^{-2}\rho\log(m\varepsilon^{-1}))$ with the constants of its proof.

Milestones

In the order the proof uses them:

Lemma 3.1: $\mathcal C1$ and $\mathcal C2$ imply that no exact solution exists if $\lambda\le1-3\varepsilon$ , and that $x$ is $3\varepsilon$ -optimal if $\lambda\ge1-3\varepsilon$ .
Lemma 3.2: if $\alpha\ge2\lambda^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ , the dual solution corresponding to $x$ satisfies $\mathcal C1$ .
Lemma 3.3: while $\mathcal C2$ fails, a step of size $\sigma\le\varepsilon/(4\alpha\rho)$ lowers the potential: $\Phi-\hat\Phi\ge\varepsilon\alpha\sigma\Phi$ .
Lemma 3.4: during IMPROVE-COVER, $\lambda\ge\frac34\lambda_0$ .
Theorem 3.5: one call of IMPROVE-COVER makes at most $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ oracle calls, and at most $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ from a $6\varepsilon$ -optimal start with $\varepsilon\le1/12$ .
Lemma 3.6: $m$ oracle calls give $x\in P$ with $Ax\ge\frac1mb$ , or prove that no exact solution exists.

Significance

Theorem 3.7 says that approximate fractional covering is no harder, in subroutine calls, than about $\rho\varepsilon^{-2}\log(m/\varepsilon)$ linear optimizations over $P$ , plus lower-order terms in $m$ . In §6 of the paper this yields fast approximation algorithms for covering-type relaxations such as the Held–Karp bound and the bin-packing and cutting-stock relaxations, where $P$ is a product of simple sets and the subroutine is a minimum-spanning-tree or knapsack computation. The result also certifies infeasibility: when the algorithm reports that no exact solution exists, the dual vector at hand proves it.

The result has been proved since 1991 and has been reproved in several later frameworks. As far as is known, it has not been machine-checked. A formal development contributes the explicit constants and a precise statement of the driver, which the paper gives only in prose. It also provides a reusable Lean account of exponential-potential methods with an optimization oracle.

Difficulty

The obvious argument tracks the potential $\Phi$ and stops when it is small. This does not work directly, because $\alpha$ is tied to $\lambda_0$ , and the guarantee $\mathcal C1$ depends on $\lambda$ staying close to $\lambda_0$ throughout. Lemma 3.4 controls that, and it is a statement about the reachable states of a while loop, not about an arbitrary point. Two further points are delicate. Unlike packing, condition $\mathcal C2$ is not scaled by $\lambda$ , so $\mathcal C1$ and $\mathcal C2$ give $\varepsilon$ -optimality only when $\lambda$ is near $1$ ; the first phase must first raise $\lambda$ from $1/m$ by repeated doubling. And the cost of $\varepsilon$ -scaling is bounded only because each phase starts from a $6\varepsilon$ -optimal point, which requires carrying Lemma 3.1 across phase boundaries. The bookkeeping that turns per-call bounds into a single explicit $N$ , over a fuel-bounded run, is substantial.

Formalization scope

Rows are Fin m with [NeZero m], coordinates Fin n; $A$ is a Matrix (Fin m) (Fin n) ℝ; $P$ is a Set (Fin n → ℝ), convex, nonempty and in the nonnegative orthant. $\lambda(x)$ is a Finset.inf' over the rows. Conventions committed to:

Width. $\rho$ is any upper bound with $\rho>0$ , not a supremum; the theorems hold for every such bound, the exact width included.
Oracle. Subroutine (7) is a function that, for every $y\ge0$ , returns a maximizer of $y^tAx$ over $P$ ; every theorem quantifies over all such functions. Box (7) of the report prints "min", but every use maximizes; the maximizer reading is adopted.
Optimality without $\lambda^*$ . " $x$ is $c\varepsilon$ -optimal" is stated as $(1-c\varepsilon)\lambda(x')\le\lambda(x)$ for every $x'\in P$ .
Runs. IMPROVE-COVER and the driver are fuel-bounded functions returning some (result, oracle calls) when they stop within the fuel. Each while-test that reaches the $\mathcal C2$ check costs one oracle call; the loop body reuses that answer. The goal asserts that the run with fuel $\lceil N\rceil$ stops; it does not assume termination.
Driver. The prose of pp. 20–21 is written down as initCover, firstPhase and scalingPhases with $\varepsilon_k=\frac16 2^{-k}$ .
Constants replacing $O(\cdot)$ . Theorem 3.5: $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ and $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ oracle calls. Theorem 3.7: the $N$ above.
Implicit hypotheses made explicit. $y\ne0$ and $\varepsilon<\frac13$ in Lemma 3.1; $\lambda>0$ in Lemmas 3.2–3.4 and Theorem 3.5; $\sigma\ge0$ in Lemma 3.3.
Misprint. Theorem 3.5's second sentence names IMPROVE-PACKING; it is stated for IMPROVE-COVER.

A trivializing formalization is ruled out: the goal requires the run to return an outcome within the stated number of oracle calls, for every exact oracle and every width bound, and each outcome must be correct.

A complete development needs elementary real analysis (the second-order bound $e^{x+\delta}\le e^x+\delta e^x+\frac\varepsilon2|\delta|e^x$ for $|\delta|\le\varepsilon/4$ ), geometric-decay counting arguments, and induction over fuel-bounded loops. The potential-decrease and termination lemmas are reusable for the packing and general missions of the same paper. Proofs of any milestone, and alternative arguments with better constants, are welcome.

Selected references

S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Cornell University School of ORIE Technical Report No. 999, February 1992. https://core.ac.uk/download/79020349.pdf
S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Mathematics of Operations Research 20(2), 257–301, 1995. https://doi.org/10.1287/moor.20.2.257
N. Garg, J. Könemann, Faster and Simpler Algorithms for Multicommodity Flow and Other Fractional Packing Problems, SIAM Journal on Computing 37(2), 630–652, 2007. https://doi.org/10.1137/S0097539704446232
N. E. Young, Sequential and Parallel Algorithms for Mixed Packing and Covering, Proc. 42nd IEEE FOCS, 538–546, 2001. https://arxiv.org/abs/cs/0110040

10 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

A Dual Approach to Solving Nonlinear Programming Problems by Unconstrained Optimization 2: For a Normal Convex Program and Any Dual Optimal ȳ, x̄ Is Optimal iff x̄ Minimizes L_r(·, ȳ)Research Paper

Motivation

Lagrangian duality turns a constrained minimization problem into the maximization of a dual function over multipliers. For convex programs the duality is clean: under mild conditions the dual optimal value equals the primal one, and an optimal multiplier vector $\bar y$ exists. Computationally, however, the ordinary Lagrangian has a well-known defect. Knowing an optimal $\bar y$ does not tell where the primal optimum is, because the minimizers of $x \mapsto L_0(x, \bar y)$ over $X$ typically include points that are not optimal and not even feasible. A linear program is the extreme case: $L_0(\cdot, \bar y)$ is then often constant.

The penalty Lagrangian (also called the augmented Lagrangian) of Hestenes, Powell and Rockafellar repairs this defect. R. T. Rockafellar's 1973 paper Math. Programming 5, 354–373 develops its duality theory for convex programs in an arbitrary real vector space. This mission formalizes the "exactness" part of that theory, §3 of the paper: for $r > 0$ , minimizing the penalty Lagrangian at an optimal multiplier gives exactly the optimal solutions of the original problem. The paper puts it as "a strong property whose well-known absence for $L_0$ has been a serious impediment to computational approaches based on duality" (p. 362). Together with the smoothness of the dual function (Theorem 3.2, another mission of this series), this property is what justifies the method of multipliers as an algorithm for constrained optimization.

Timeline. Hestenes (1969) and Powell (1969) proposed the multiplier method for equality constraints. Rockafellar (1973, this paper) gave the inequality-constrained penalty Lagrangian $L_r$ below and its convex duality theory. Bertsekas's monograph Constrained Optimization and Lagrange Multiplier Methods (1982) systematized the theory.

Setting

Let $E$ be a real vector space, $X \subseteq E$ a nonempty convex set, and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex functions. The problem is

\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \quad\text{subject to } f_i(x) \le 0,\ i = 1, \dots, m.

A point is feasible if it lies in $X$ and satisfies the constraints. The optimal value "inf in (P)" is the infimum of $f_0$ over the feasible points, an element of $[-\infty, +\infty]$ . An optimal solution is a feasible $\bar x$ with $f_0(\bar x) \le f_0(x)$ for every feasible $x$ .

For $y \in \mathbb R^m$ (no sign restriction), $\theta(t) = \max\{0, t\}$ and $r > 0$ , the penalty Lagrangian is

L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big].

The ordinary Lagrangian is $L_0(x, y) = f_0(x) + \sum_i y_i f_i(x)$ for $y \ge 0$ , and $-\infty$ otherwise. The dual objectives are $g_r(y) = \inf_{x \in X} L_r(x, y)$ and $g_0(y) = \inf_{x \in X} L_0(x, y)$ . Problem $(D_r)$ maximizes $g_r$ over $\mathbb R^m$ .

A dual optimal solution is a maximizer $\bar y$ of $g_r$ with $g_r(\bar y) > -\infty$ .
(P) is normal if the dual optimal value $\sup g_0$ equals the optimal value of (P).
$\bar y$ is a Kuhn–Tucker vector relative to $L_r$ if $-\infty < \inf_{x \in X} L_r(x, \bar y) = \inf$ in (P).
$(\bar x, \bar y)$ is a saddle point of $L_r$ if $\bar x \in X$ and $L_r(\bar x, y) \le L_r(\bar x, \bar y) \le L_r(x, \bar y)$ for all $x \in X$ , $y \in \mathbb R^m$ .

In Lean these are Lr, L0, gr, g0, primalValue, dualValue, IsNormal, IsDualOptimal, IsKTVector, IsSaddle, IsOptimal and KuhnTuckerConditions, in the namespace PenaltyLag.Exact.

Formalization targets

Goal: Theorem 3.5 (p. 362)

Assume (P) is normal, $\bar y$ is a dual optimal solution, and $r > 0$ . Then for every $\bar x \in E$

\bar x \text{ is optimal for (P)} \iff \bar x \in X \text{ and } L_r(\bar x, \bar y) \le L_r(x, \bar y) \ \ \forall x \in X.

Milestones (attack order)

§3 after (3.17), pp. 361–362: for $r > 0$ , $\bar y$ is a Kuhn–Tucker vector relative to $L_r$ iff $\bar y$ is optimal for $(D_r)$ and (P) is normal.
§3, p. 362: for $r > 0$ , $(\bar x, \bar y)$ is a saddle point of $L_r$ iff $\bar x$ is optimal for (P) and $\bar y$ is a Kuhn–Tucker vector.
Corollary 3.4, $r > 0$ (p. 362): $L_r$ and $L_0$ have the same Kuhn–Tucker vectors and the same saddle points, and the saddle points of $L_r$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions

\bar y_i \ge 0,\ f_i(\bar x) \le 0,\ \bar y_i f_i(\bar x) = 0\ (\forall i), \qquad \bar x \in \operatorname{argmin}_X \Big(f_0 + \sum_i \bar y_i f_i\Big).

Corollary 3.4, $r = 0$ : the saddle points of $L_0$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions.
Proof of Theorem 3.5, pp. 362–363: if $\bar y$ is optimal for $(D_r)$ and $\bar x \in X$ minimizes $L_r(\cdot, \bar y)$ over $X$ , then $\nabla_y L_r(\bar x, \bar y) = 0$ and $\bar y$ maximizes $L_r(\bar x, \cdot)$ over $\mathbb R^m$ .

Significance

The result. Theorem 3.5 turns a constrained problem into an unconstrained one with no loss of exactness. Once an optimal multiplier is known, every minimizer of $L_r(\cdot, \bar y)$ over $X$ solves (P), and conversely. Section 4 of the paper builds the computational scheme on this: maximize the smooth concave function $g_r$ over $\mathbb R^m$ , then minimize $L_r(\cdot, \bar y)$ over $X$ . For the ordinary Lagrangian the corresponding statement is false (p. 363), so the theorem marks precisely what the quadratic penalty term adds. Corollary 3.4 records the other half of the picture: in Kuhn–Tucker vectors and saddle points, $L_r$ behaves exactly like $L_0$ .

Formalizing it. All results are proved in the paper, partly by citation of Rockafellar's Convex Analysis (§§28–30, 36). On the Prove2Me platform, saddle-point characterizations exist only for the ordinary Lagrangian on $\mathbb R^n$ (for instance ConvexOptimization.lagrangian_saddle_iff_strong_duality, and Beck's Theorem 2.7 as FirstOrderOpt.ConvexTheory.saddle_point_sufficient / saddle_point_necessary). This mission adds the penalty Lagrangian, convex sets in an arbitrary real vector space, extended-real dual values, and the exactness theorem itself. None of these statements is known to us to be machine-checked elsewhere.

Difficulty

The "if" direction is the substantive one. A minimizer $\bar x$ of $L_r(\cdot, \bar y)$ is not known to be feasible; feasibility must come from maximality of $\bar y$ in the dual. The natural argument for $L_0$ breaks at exactly this point: $L_0(\bar x, \cdot)$ is affine on the orthant, and minimality in $x$ gives no information about $\nabla_y$ . For $L_r$ the link is the differentiability of the dual function $g_r$ with $\nabla g_r(\bar y) = \nabla_y L_r(\bar x, \bar y)$ (Theorem 3.2), which is posed in another mission of this series and is not available as a platform result. Every statement involves extended-real dual values on a vector space with no topology, so $\pm\infty$ must be handled at each step.

Formalization scope

$E$ is a bare real vector space (AddCommGroup E, Module ℝ E), as in the paper; no norm or topology is used.
$X$ is a Set E. Each statement assumes the paper's standing hypothesis (p. 358): $X$ convex and nonempty, $f_0, \dots, f_m$ convex on $X$ .
The $f_i$ are total functions E → ℝ, and only their values on $X$ enter. Constraint indices are Fin m (0-based), with $f_0$ a separate argument.
$\mathbb R^m$ is EuclideanSpace ℝ (Fin m).
$g_r$ , $g_0$ , $L_0$ , the optimal value of (P) and the dual optimal value are EReal-valued. An infeasible (P) has value $+\infty$ , and $g_0 = -\infty$ off $y \ge 0$ .
$r > 0$ is an explicit hypothesis wherever the paper has it. Theorem 3.5 is false for $r = 0$ (p. 363), and the Lean expression Lr at $r = 0$ is not $L_0$ .
"Dual optimal solution" in Theorem 3.5 is read as optimal for $(D_r)$ with the same $r$ , with $g_r(\bar y) > -\infty$ (the convention of p. 361). The paper's reading, optimal for $(D_0)$ , is equivalent by Theorem 3.2, which is posed in mission 1 of this series.
" $\bar x$ minimizes $L_r(\cdot, \bar y)$ over $X$ " includes $\bar x \in X$ . The equivalence is stated for every $\bar x \in E$ . No sign condition is imposed on $\bar y$ : nonnegativity is a consequence of dual optimality, not a hypothesis.
Saddle points are taken over $X \times \mathbb R^m$ (Rockafellar's Convex Analysis, §36). For $L_0$ they are taken in the extended reals.
Trivializing readings ruled out: normality is neither dropped nor replaced by existence of an optimal solution or by Slater's condition, and the minimization on the right of Theorem 3.5 is never over a set containing points outside $X$ .

The solver needs the representation $L_r(x, y) = \min_u\{F_r(x, u) + u \cdot y\}$ , weak duality, the envelope formula and differentiability of $g_r$ (Theorem 3.2), and a convex-duality fact for normal programs. Those parts are reusable beyond this mission, and proofs of the paper's Theorem 3.2 in this setting are welcome as auxiliary results.

Selected references

R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982.

8 thms2 active usersReviewed

Markov Chain Stochastic Systems·Captain: mikedeng1

Stability Properties of Constrained Queueing Systems and Scheduling Policies for Maximum Throughput in Multihop Radio Networks I: Policy π₀ Is Throughput-Optimal, C′ ⊂ C_π₀ ⊂ C ⊂ C̄′Research Paper

Motivation

In a wireless multihop network, a switch, or a parallel computer, transmissions interfere: two links that share a receiver, or two crossbar paths that share a port, cannot be active in the same time slot. The scheduler must choose, slot by slot, a set of links that may operate together and decide which traffic each one carries. The basic question is which arrival rates a network can sustain at all, and whether a single scheduling rule sustains every one of them without knowing the rates.

Tassiulas and Ephremides answered both questions in 1992 for a general slotted model with interference constraints, multihop routing and several traffic classes (IEEE Trans. Automat. Control 37(12):1936–1948). Their policy, here called $\pi_0$ , weighs each link by the largest queue-length difference it can reduce and activates a maximum-weight feasible set. It is the origin of the max-weight and back-pressure scheduling rules that later became standard in switch scheduling (McKeown, Mekkittikul, Anantharam and Walrand, 1999) and in stochastic network optimization (Georgiadis, Neely and Tassiulas, 2006).

Setting

A constrained queueing network has $L$ nodes, $N$ servers (links) and $J$ customer classes. Server $i$ moves customers from its origin node $q(i)$ to its destination node $h(i)$ . Class $j$ leaves the network on reaching a node of its destination set $V_j$ ; at every other node $l$ it has a queue $(l,j)$ , whose length at the end of slot $t$ is $X_{lj}(t)\in\mathbb N$ .

The constraint set $S$ is the family of sets of servers that may be active in the same slot. Assumption C.1 says that every subset of an activation set is an activation set. In each slot a stationary policy, given the state $x=X(t-1)$ , chooses a set of servers in $S$ and the class each active server serves; an activation rule never activates more servers of queue $(l,j)$ than there are customers $x_{lj}$ . The class of all such rules is $H$ . An activated server $i$ completes its service with probability $m_i$ , independently. New arrivals $A_{lj}(t)$ are i.i.d. over slots, independent across queues and of the services, with finite second moments and means $a_{lj}$ . Under a stationary rule the vector $X(t)$ is a Markov chain on $\mathbb N^{\{\text{queues}\}}$ .

The chain is stable (Definition 3.1) if, from every transient state, it enters a closed communicating class with probability one, and every state of a closed communicating class is positive recurrent. The stability region $C_\pi$ of a policy is the set of rate vectors $a$ for which the system is stable under $\pi$ ; the stability region of the system is $C=\bigcup_{\pi\in H}C_\pi$ .

A family $f=(f_{ij})\ge0$ is an $a$ -admissible flow if it satisfies flow conservation, $a_{lj}=\sum_{q(i)=l}f_{ij}-\sum_{h(i)=l}f_{ij}$ at every queue; $\hat f_i=\sum_jf_{ij}$ is its total flow through server $i$ . With $\mathrm{co}(S)$ the convex hull of the indicator vectors of the activation sets,

C'=\{a\ge0:\ \exists f\in F_a,\ c\in\mathrm{co}(S),\ m_i^{-1}\hat f_i<c_i\text{ if }\hat f_i>0,\ \hat f_i=0\text{ if }c_i=0\}.

Formalization targets

Goal: Theorem 3.2

C'\subset C\subset\bar C',\qquad C'\subset C_{\pi_0}\subset C\subset\bar C_{\pi_0}.

The system stability region is pinned between $C'$ and its closure, and policy $\pi_0$ , whatever its tie-breaking, stabilizes every rate vector in $C'$ . Inclusions are not strict.

Milestones

Lemma A.1: $\mathrm{co}(S)$ is closed under $0\le a\le c$ (under C.1).
Lemma 3.1: $\bar C'=\{a:\exists f\in F_a,\ c\in\mathrm{co}(S),\ M^{-1}\hat f\le c\}$ .
Theorem 3.1: a function bounded below with drift $\le-\epsilon$ outside a finite set, and finite conditional expectation on it, makes a countable chain stable in the sense of Definition 3.1.
(A.6)–(A.7): for $V(x)=\sum_{l,j}x_{lj}^2$ , the one-step drift under $\pi_0$ is finite everywhere and below $-\epsilon$ once $V(x)\ge b$ .
Lemma 3.2: $C'\subset C_{\pi_0}$ .
Lemma 3.3: for $a\notin\bar C'$ , the system is unstable under every policy in $H$ .

An optional item states the claim of Remark 1: if $a\in\bar C'\setminus C'$ , then $\delta a\notin\bar C'$ for every $\delta>1$ .

Significance

Theorem 3.2 shows that a throughput-optimal stationary policy exists, which is not obvious: stability regions of different policies need not be nested, so a policy whose region contains all the others has to be exhibited. It also describes the system stability region by a deterministic flow condition, $C'$ , which can be checked without simulating any policy. The same drift argument underlies the stability proofs of max-weight switch schedulers, back-pressure routing and the drift-plus-penalty method.

The result is proved in the paper, with a proof sketched in places (Theorem 3.1 is called "a trivial extension of Foster's criteria", Lemma A.1 is omitted, Lemma 3.3 is argued by ergodicity in a paragraph). As far as a search of the platform shows, none of these statements has a machine-checked proof: Foster's criterion is posed on the platform only for irreducible chains on $\mathbb N$ , and the back-pressure results already posed concern fluid models of other networks. A complete formal development would supply the reducible-chain Foster criterion, the convex-geometry lemma on $\mathrm{co}(S)$ , the quadratic drift computation and the ergodic converse.

Difficulty

The obvious argument is a quadratic Lyapunov drift bound, but it does not go through as is in three places. First, the drift bound needs a direction of decrease from every large state: the largest queue must be connected to a destination through servers that can actually be activated, which is where assumption C.2 and the topology of $S$ enter (A.21)–(A.24). Second, stage 3 of $\pi_0$ defers some activations to respect the rule "no service for nonexisting customers", so the chosen schedule is not exactly maximum-weight and the loss has to be bounded uniformly. Third, the chain is in general reducible, so Foster's criterion for irreducible chains does not apply; the extension must show that every closed class meets the finite exceptional set and that transient states are left almost surely. The converse, Lemma 3.3, needs a law-of-large-numbers argument for an arbitrary stationary rule on a positive recurrent class, together with compactness of acyclic flows (Lemma 3.1).

Formalization scope

Nodes, servers and classes are Fin L, Fin N, Fin J (0-based). $S$ is a Set (Finset (Fin N)); a queue is a pair $(l,j)$ with $l\notin V_j$ , and a state is a function from queues to $\mathbb N$ . A multiclass activation vector assigns to each server an optional class. The transition matrix of the queue-length chain is written out explicitly as a sum over arrival vectors and Bernoulli service outcomes; Definition 3.1 is stated through this matrix (first-entry probabilities, essential states, positive recurrence), with values in $[0,\infty]$ .

Conventions committed to, and hypotheses added relative to the page:

Standing assumptions of the goal: C.1; $\emptyset\in S$ (the idle schedule is always allowed); $0<m_i\le1$ ; and C.2 in a topological form, a chain of servers from every non-destination node of class $j$ to $V_j$ (stronger than the printed sentence, which covers only nodes that class $j$ can reach).
Every single server is an activation set, $\{i\}\in S$ . The proof of Lemma 3.2 uses this at (A.24) without stating it; without it a server that can never be activated breaks the drift bound and Lemma 3.2.
Stability regions quantify over laws. $C_\pi$ is the set of nonnegative rate vectors for which the chain is stable for every arrival law with finite second moments and those means. $C'$ is intersected with $a\ge0$ .
$\pi_0$ is a family. Statements hold for every rule satisfying the three stages, with arbitrary tie-breaking.
Expectations of unbounded functions are real series with explicit summability, so a divergent expectation is never read as $0$ .

A formalization in which $C_\pi$ asks for stability under one convenient arrival law, or in which negative rates are admitted, or in which $\pi_0$ is one fixed tie-break, would be a different theorem; the definitions rule each of these out.

Infrastructure needed: hitting probabilities and positive recurrence for countable chains (reusable beyond this mission), convex hulls of finite point sets, a cycle-cancelling bound for multicommodity flows, and the ergodic theorem for positive recurrent chains. Proofs of any milestone, and reusable lemmas on countable Markov chains, 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 Trans. Automat. Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3):355–360, 1953. https://doi.org/10.1214/aoms/1177728976
N. McKeown, A. Mekkittikul, V. Anantharam and J. Walrand, Achieving 100% throughput in an input-queued switch, IEEE Trans. Commun. 47(8):1260–1267, 1999. https://doi.org/10.1109/26.780463
L. Georgiadis, M. J. Neely and L. Tassiulas, Resource allocation and cross-layer control in wireless networks, Found. Trends Netw. 1(1):1–144, 2006. https://doi.org/10.1561/1300000001

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

Incentive Compatibility and the Bargaining Problem II: Every Equilibrium of Every Choice Mechanism Yields an Incentive-Feasible Allocation, F** = F*Research Paper

Motivation

An arbitrator who must choose among collective options for a group of players usually does not know the players' private characteristics. The arbitrator can only ask, and a player who expects to profit from a false answer may give one. Before designing any procedure, the arbitrator therefore needs to know which expected-payoff allocations can be reached at all once strategic misreporting is taken into account.

Myerson (1979) answers this for Bayesian collective choice problems with finitely many types. Restricting attention to mechanisms that simply ask each player for their type, and that make honest answers optimal, loses nothing: every expected-payoff allocation that any mechanism can produce in equilibrium is already produced honestly by such a direct mechanism, and conversely. This is the revelation principle in the form used throughout Bayesian mechanism design. It is what makes incentive-compatibility constraints the starting point for auction design, bilateral trade, and the bargaining solution in the second half of the same paper.

Timeline. Gibbard (1973) gave the dominant-strategy form of the principle. Rosenthal (Review of Economic Studies, 1978) studied arbitration of two-party disputes under uncertainty; Myerson notes that Theorem 2 could be derived as a corollary of Rosenthal's Theorem 3. Dasgupta, Hammond and Maskin (1979) gave general Bayesian implementation results in the same year. Myerson's Theorem 2 states the principle as an equality of interim payoff sets over all finite response sets. Myerson (1982) later extended it to principal–agent problems with moral hazard.

Setting

A Bayesian collective choice problem $(C,A_1,\dots,A_n,U_1,\dots,U_n,P)$ has a nonempty finite set of players $i$ , a nonempty finite set $A_i$ of types for each player, a nonempty finite set $C$ of collective choices, utilities $U_i(c,\alpha)$ depending on the choice and on the true type profile $\alpha=(\alpha_1,\dots,\alpha_n)$ , and a probability distribution $P$ on type profiles. With $R_i(a_i)=\sum_{\beta:\beta_i=a_i}P(\beta)$ the marginal of type $a_i$ , a player of type $a_i$ assigns the conditional probability $P_i(\alpha\mid a_i)=P(\alpha)/R_i(a_i)$ to profiles with $\alpha_i=a_i$ , and $0$ to the others.

A choice mechanism on response sets $S_1,\dots,S_n$ (nonempty finite sets of possible answers) is a function $\pi(c\mid s)\ge0$ with $\sum_{c}\pi(c\mid s)=1$ for every response profile $s$ . On the standard response sets $S_i=A_i$ , the payoff of type $a_i$ who reports $b_i$ while the others are honest is

Z_i(\pi,b_i\mid a_i)=\sum_\alpha\sum_{c}P_i(\alpha\mid a_i)\,\pi(c\mid\alpha_{-i},b_i)\,U_i(c,\alpha).

The mechanism is Bayesian incentive-compatible if $Z_i(\pi,a_i\mid a_i)\ge Z_i(\pi,b_i\mid a_i)$ for all $i,a_i,b_i$ . Its honest allocation is the vector $V(\pi)$ with coordinates $V_i(\pi\mid a_i)=Z_i(\pi,a_i\mid a_i)$ , indexed by the disjoint union of the $A_i$ . The incentive-feasible set is

F^*=\{V(\pi):\pi\text{ a Bayesian incentive-compatible choice mechanism on the standard response sets}\}.

On general response sets, a response plan $\sigma_i(s_i\mid a_i)$ is a probability distribution over $S_i$ for each type $a_i$ . Plans $\sigma=(\sigma_1,\dots,\sigma_n)$ give type $a_i$ the payoff

W_i(\pi,\sigma\mid a_i)=\sum_\alpha\sum_s\sum_c P_i(\alpha\mid a_i)\Big(\prod_{j}\sigma_j(s_j\mid\alpha_j)\Big)\pi(c\mid s)\,U_i(c,\alpha).

They form a response-plan equilibrium for $\pi$ if no type $a_i$ of any player gains by switching to any other response plan $\sigma_i'$ . The equilibrium-feasible set $F^{**}$ collects $W(\pi,\sigma)$ over all choice mechanisms $\pi$ , on all nonempty finite response sets, and all response-plan equilibria $\sigma$ for $\pi$ .

Formalization targets

Goal: Theorem 2

F^{**}=F^*.

Both inclusions are asserted for every Bayesian collective choice problem. $F^{**}\subseteq F^*$ says equilibrium behaviour under any mechanism can be replicated honestly by an incentive-compatible direct mechanism. $F^*\subseteq F^{**}$ says honest reporting is itself an equilibrium of every incentive-compatible mechanism.

Milestones (the steps of the paper's proof)

For any choice mechanism $\pi$ and response plans $\sigma$ , the induced direct mechanism $\pi'(c\mid\alpha)=\sum_s\pi(c\mid s)\prod_i\sigma_i(s_i\mid\alpha_i)$ is a choice mechanism and $V(\pi')=W(\pi,\sigma)$ .
If $\sigma$ is a response-plan equilibrium for $\pi$ , then $\pi'$ is Bayesian incentive-compatible.
If $\pi'$ is a Bayesian incentive-compatible choice mechanism, the honest plans $\sigma_i'(b_i\mid a_i)=\mathbf 1[b_i=a_i]$ form a response-plan equilibrium for $\pi'$ , and $W(\pi',\sigma')=V(\pi')$ .

Significance

The result. Theorem 2 reduces a search over all communication protocols, an unbounded family of response sets and mixed reporting behaviours, to a finite system of linear inequalities in $\pi$ on a fixed finite domain. Combined with Theorem 1 of the paper, which shows $F^*$ is a nonempty compact convex set, it justifies applying a bargaining solution to $F^*$ rather than to some larger, ill-defined set of attainable outcomes. The same reduction underlies the use of incentive constraints in optimal auctions, bilateral trade and correlated-type mechanism design.

Formalizing it. The result is classical and its proof is short, but it is a statement about all finite response sets at once, and the equality of two sets of payoff vectors is sensitive to the conventions: which plans are allowed as deviations, where the conditioning happens, and whether the induced mechanism is a genuine probability distribution. A machine-checked version pins these down. To our knowledge no formal proof of this finite Bayesian revelation principle exists. The platform has related, unproved items in other models: MechanismDesign.Robust.revelation_principle (Börgers, Prop. 10.2, on a countable Harsanyi type space with PMF lotteries; one inclusion, outcome equivalence) and single-agent, quasi-linear and dominant-strategy revelation principles from the same book. None of them is the statement here.

Difficulty

The mathematics consists of finite sums, but the bookkeeping is the obstacle. Milestone 1 requires exchanging a sum over response profiles with a product over players and using that each plan sums to one. Milestone 2 requires recognizing a lie $b_i$ in $\pi'$ as a particular whole response plan in $\pi$ : the plan that, at every type, behaves as type $b_i$ would. Because $P_i(\alpha\mid a_i)$ vanishes off $\alpha_i=a_i$ , only its value at $a_i$ matters. For milestone 3, a mixed deviation from honesty has to be bounded by the best pure misreport, a convex-combination argument over $A_i$ . Identifying the $F^{**}$ side of the goal also needs instances on an existentially chosen family of types.

Formalization scope

All objects live in MyersonBargaining.Revelation. Players form a nonempty finite type ι; types A i, choices C and response sets S i are nonempty finite types in Type. Mechanisms and plans are real-valued functions with the probability constraints as predicates (IsChoiceMechanism, IsResponsePlan), event first and condition second: π c s, σ i s a. Allocation vectors are functions on Σ i, A i. The paper's loose phrases are read as follows:

"probability distribution" means nonnegativity and sum one;
(3) divides by $R_i(a_i)$ , so the problem requires $R_i(a_i)>0$ ; individual profiles may have probability zero;
the consistent (common-prior) reading of (3)–(4) is formalized, not the subjective reading the paper permits on p. 63;
"for every possible alternative response plan" in (14) ranges over all mixed response plans, compared type by type;
" $\pi$ is a choice mechanism" in (15) ranges over all nonempty finite response sets, with an explicit existential over the family S : ι → Type and its instances;
"incentive-compatible mechanism" means a choice mechanism satisfying (6).

The product in (12) is printed with $\sigma_j(s_j\mid a_j)$ ; it is formalized with $\alpha_j$ , as the paper's own induced mechanism on p. 66 uses. Milestone 1 is stated for arbitrary response plans, not only for equilibria. Section 6's numerical example is not formalized.

A trivializing formalization is ruled out explicitly: fixing $S_i=A_i$ in $F^{**}$ , restricting deviations to pure plans, or stating only $F^{**}\subseteq F^*$ would each change the theorem, and none is done.

A complete development needs finite sums over dependent product types (Fintype.piFinset, Finset.prod_univ_sum), Function.update on dependent families, and nothing beyond Mathlib. The two definition modules (the model and the response-plan objects) are reusable by any finite Bayesian mechanism-design formalization. Proofs of any milestone, alternative proofs via Rosenthal's argument, and cleaner restatements as lemmas about stochastic matrices are welcome.

Selected references

Roger B. Myerson, Incentive compatibility and the bargaining problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
Robert W. Rosenthal, Arbitration of two-party disputes under uncertainty, Review of Economic Studies 45(3), 1978 (cited in the source as reference [8], "forthcoming").
Allan Gibbard, Manipulation of voting schemes: a general result, Econometrica 41(4), 587–601, 1973. https://doi.org/10.2307/1914083
Partha Dasgupta, Peter Hammond, Eric Maskin, The implementation of social choice rules: some general results on incentive compatibility, Review of Economic Studies 46(2), 185–216, 1979. https://doi.org/10.2307/2297045
Roger B. Myerson, Optimal coordination mechanisms in generalized principal–agent problems, Journal of Mathematical Economics 10(1), 67–81, 1982. https://doi.org/10.1016/0304-4068(82)90006-4

6 thms2 active usersReviewed

Completed

Probability Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 2: The Ergodic Theorem — a Cumulative Process Satisfies w_t/t → κ₁/μ₁ with Probability OneResearch Paper

Motivation

Many quantities in operations research accumulate over time in a system that periodically starts afresh: the cost incurred by an inventory system that returns to the same stock level, the work completed by a server between successive moments it empties, the reward collected by a machine between repairs. The basic question about such a quantity is its long-run rate: does the amount accumulated by time $t$ , divided by $t$ , settle down, and to what?

W. L. Smith's 1955 paper Regenerative stochastic processes (DOI 10.1098/rspa.1955.0198) introduced the class of cumulative processes to answer this question, and §5·3 of the paper proves the answer, Theorem 7, which Smith calls "the ergodic theorem": the long-run rate equals the expected accumulation per cycle divided by the expected cycle length. In later textbooks this is the renewal–reward theorem, the standard tool for computing long-run averages of regenerative systems in queueing, inventory and reliability models.

Timeline. Doob (1948) proved the strong law $n_t/t \to 1/\mu_1$ for renewal counting processes (Trans. AMS 63). Smith (1955) defined cumulative processes by conditions (C1)–(C2) and proved Theorem 7 under a first-moment condition on the variation per cycle, together with central limit theorems (Theorems 9–10) for the same processes.

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ .

A renewal process is a sequence $t_1, t_2, \dots$ of independent, identically distributed, non-negative random variables that are not zero with probability one, i.e. $P\{t_1 = 0\} < 1$ . Write $\mu_1 = E t_1$ . In this mission the delay is $t_0 = 0$ , the regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ , and the counting variable

n_t = \#\{k \ge 0 : T_k \le t\}

is the number of regenerations in $[0, t]$ (the paper's "greatest integer $k$ such that $T_{k-1} \le t$ "). The forward variable $Z_t = \sum_{i=1}^{n_t+1} t_i - t$ measures how far $t$ is from the regeneration epoch $T_{n_t+1}$ .

Let $w = (w_t)$ be a real-valued process with $w_0 = 0$ . Its cycle increments are $y_n = w_{T_n} - w_{T_{n-1}}$ , $n \ge 1$ , and $\kappa_1 = E y_1$ . On a path of bounded variation on every finite interval, the variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ is the total variation of the path over $[0, t]$ ; the cycle variations are $\tilde y_n = \tilde w_{T_n} - \tilde w_{T_{n-1}}$ , and $\tilde\kappa_p = E \tilde y_1^{\,p}$ .

The process $w$ is a cumulative process when

(C1) $y_1, y_2, \dots$ are independent and identically distributed, and
(C2) with probability one, $w$ is of bounded variation in every finite interval.

Formalization targets

Goal: Theorem 7 (the ergodic theorem)

If $w$ is a cumulative process, $\mu_1 < \infty$ , $\tilde\kappa_1 < \infty$ , $t_0 = 0$ and $w_0 = 0$ , then

\lim_{t \to \infty} \frac{w_t}{t} = \frac{\kappa_1}{\mu_1} \quad \text{with probability one.}

The statement fixes no rate and no constant; it is the exact limit of the paper.

Milestones, in the order the proof uses them

Lemma 7. For i.i.d. $x_n$ with $E|x_n|^p < \infty$ , $p > 0$ : $x_n / n^{1/p} \to 0$ with probability one.
Renewal strong law (proof of Lemma 8): $n_t / t \to 1/\mu_1$ with probability one when $\mu_1 < \infty$ .
Lemma 8. If $t_0 = 0$ , $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$ ( $p > 0$ ), then

\lim_{t \to \infty} \frac{w_{t+Z_t} - w_t}{t^{1/p}} = 0 \quad \text{with probability one.}

(5·3·4). $\sum_{i=1}^{n_t+1} y_i / (n_t + 1) \to \kappa_1$ with probability one.
The limit along regeneration epochs. $w_{t+Z_t} / t \to \kappa_1/\mu_1$ with probability one.

Significance

The ergodic theorem turns a question about a whole sample path into a question about one cycle. Once a system is shown to regenerate, its long-run average cost, throughput or utilization is the ratio of two one-cycle expectations, which can often be computed in closed form. This is how long-run averages are evaluated for $M/G/1$ -type queues, $(s,S)$ inventory policies and alternating-renewal reliability models, and it is the first step in average-cost analyses of regenerative Markov decision processes. Lemma 8, with $p > 1$ , also controls the error term in Smith's central limit theorem for cumulative processes.

The result is classical and proved. As far as the platform and Mathlib are concerned, it is not formalized: Mathlib has the strong law of large numbers for i.i.d. sequences (ProbabilityTheory.strong_law_ae) but no renewal counting process, no renewal strong law, and no renewal–reward theorem. A complete development gives machine-checked versions of all three, stated for real time and for cycle lengths that may vanish with positive probability.

Difficulty

The obvious argument writes $w_t / t$ as $\big(\sum_{i \le n_t} y_i / n_t\big) \cdot (n_t / t)$ and applies the strong law to each factor. This fails in two places. First, $w_t$ is not a sum of whole cycles: the cycle containing $t$ is only partly completed, and its contribution has to be shown negligible. The increment $y_n$ does not control it, because $w$ may oscillate inside a cycle and return; it is the variation $\tilde y_n$ that bounds the partial contribution, which is why the hypothesis is on $\tilde\kappa_1$ rather than on $\kappa_1$ . Second, the strong law is a statement about a deterministic index $n \to \infty$ , while here the index $n_t$ is random and depends on the cycle lengths, which need not be independent of the increments. Transferring almost-sure convergence through the random index requires $n_t \to \infty$ almost surely, which in turn uses $P\{t_1 = 0\} < 1$ .

Formalization scope

Time is real: every limit is along $t \to \infty$ in $\mathbb R$ (Filter.atTop on ℝ), and "with probability one" is an almost-everywhere statement placed outside the limit. Random variables are real-valued. The renewal process is the structure IsRenewalProcess (cycle lengths measurable, mutually independent, identically distributed, non-negative everywhere, $P\{t_1 = 0\} < 1$ ); $t_0 = 0$ and $w_0 = 0$ are explicit hypotheses holding at every sample point. Moments are Bochner integrals guarded by integrability hypotheses: $\mu_1 < \infty$ is integrability of $t_1$ , $\tilde\kappa_p < \infty$ is integrability of $\tilde y_1^{\,p}$ . The positivity $\mu_1 > 0$ is never assumed; it follows from $P\{t_1 = 0\} < 1$ .

The count $n_t$ is a cardinality; on the null event where infinitely many epochs lie below $t$ it takes the value $0$ , and finiteness is never assumed. The variation process is Mathlib's eVariationOn of the path over $[0, t]$ , set to $0$ on paths that are not of bounded variation, exactly as the paper prescribes.

Condition (C1) is read literally: only the increments $y_n$ are i.i.d., and no independence between cycle lengths and increments is assumed. In addition the cycle variations $\tilde y_n$ are assumed identically distributed; the paper's notation $\tilde\kappa_p$ presupposes this. The statement is not trivialized by a stronger model: taking $w$ to be a Lévy process, or a deterministic multiple of $t$ , would make the theorem immediate and is not what is formalized.

Two misprints of the paper are corrected in the formal statements and kept in the verbatim milestone text: (5·3·4) prints the limit as $\nu_1$ , which must be $\kappa_1$ ; and the proof bound (5·3·1) uses $\tilde y_{n_t+1}$ alone, where the interval $[t, t+Z_t]$ also meets cycle $n_t$ .

Needed infrastructure: a renewal counting process in continuous time with its strong law; a lemma that almost-sure convergence of a sequence passes to a random index tending to infinity; the comparison $|w_b - w_a| \le \tilde w_b - \tilde w_a$ for paths of bounded variation. All three are reusable well beyond this mission (renewal–reward arguments, regenerative simulation, average-cost Markov decision processes). Contributions of any milestone, and of these general lemmas as separate theorems, are welcome.

Selected references

W. L. Smith, Regenerative stochastic processes, Proceedings of the Royal Society of London, Series A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
J. L. Doob, Renewal theory from the point of view of the theory of probability, Transactions of the American Mathematical Society 63(3):422–438, 1948. https://doi.org/10.1090/S0002-9947-1948-0025098-8

9 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 4: Cumulative Processes on the Same Regeneration Points Are Jointly Asymptotically NormalResearch Paper

Motivation

Many quantities in queueing, inventory and reliability models are additive functionals of a regenerative process: the total work processed by a server up to time $t$ , the cost accumulated by an inventory policy, the time a machine spends broken. Each such quantity grows by independent, identically distributed amounts over the cycles between successive regeneration points. W. L. Smith called these cumulative processes in Regenerative stochastic processes (Proc. R. Soc. Lond. A, 1955), the paper that introduced the term "regenerative process" and laid out its limit theory. Long-run averages of such quantities are estimated by simulation and by statistical observation of real systems. Confidence intervals for these estimates, and the regenerative method of simulation output analysis, rest on the central limit theorem for cumulative processes. When several quantities are estimated at once (a ratio of two rewards, a vector of costs), they rest on its joint version for several cumulative processes driven by the same regenerations.

Timeline:

1949. Feller proves the central limit theorem for the renewal counting process.
1952. Anscombe proves that a central limit theorem survives replacing the number of summands by a random index $m_t$ with $m_t/\psi(t)\to 1$ in probability, without independence between the index and the summands (Anscombe, Proc. Camb. Phil. Soc. 48, 1952).
1955. Smith extends Anscombe's theorem to random vectors and deduces the univariate (Theorem 9, Corollary 9·1) and multivariate (Theorem 10) central limit theorems for cumulative processes (Smith 1955).

Setting

On a probability space $(\Omega, P)$ , let $t_1, t_2, \dots$ be independent, identically distributed, non-negative random variables with $P\{t_1 = 0\} < 1$ (a renewal process), and $t_0 = 0$ . The regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ ( $k \ge 0$ ), and $n_t$ is the number of epochs in $[0,t]$ (in Smith's words, the greatest $k$ with $T_{k-1} \le t$ , where $T_{-1} = 0$ ). Write $\mu_r = E t_1^r$ .

A real process $w_t$ with $w_0 = 0$ is a cumulative process if (C1) its cycle increments $y_n = \Delta_n w_t = w_{T_n} - w_{T_{n-1}}$ , $n \ge 1$ , are i.i.d., and (C2) with probability one its paths have bounded variation on every finite interval. The variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ has increments $\tilde y_n = \Delta_n \tilde w_t$ . Moments are written $\kappa_r = E y_n^r$ and $\tilde\kappa_r = E \tilde y_n^{\,r}$ .

$M$ cumulative processes $w^{(1)}_t, \dots, w^{(M)}_t$ are based on the same sequence of regeneration points when the cycle vectors $(t_n, y^{(1)}_n, \dots, y^{(M)}_n, \tilde y^{(1)}_n, \dots, \tilde y^{(M)}_n)$ are i.i.d. in $n$ . Put $\kappa^{(i)}_1 = E y^{(i)}_1$ . The covariance matrices are

a_{kl} = \operatorname{cov}(y^{(k)}_1, y^{(l)}_1), \qquad b_{kl} = \operatorname{cov}\Big(y^{(k)}_1 - \tfrac{\kappa^{(k)}_1}{\mu_1} t_1,\; y^{(l)}_1 - \tfrac{\kappa^{(l)}_1}{\mu_1} t_1\Big).

Formalization targets

Goal: Theorem 10

If $\mu_1 < \infty$ and $E(\tilde y^{(i)}_1)^2 < \infty$ for every $i$ , then as $t \to \infty$

\left(\frac{w^{(i)}_t - \kappa^{(i)}_1 n_t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, a),

and if in addition $\mu_2 < \infty$ ,

\left(\frac{w^{(i)}_t - (\kappa^{(i)}_1/\mu_1)\,t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, b).

Milestones

The renewal strong law $n_t/t \to 1/\mu_1$ almost surely (§5·3).
Lemma 8: if $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$ , then $(w_{t+Z_t} - w_t)/t^{1/p} \to 0$ almost surely, where $Z_t = \sum_1^{n_t+1} t_i - t$ .
Theorem B (Anscombe): $P\{\sum_1^{m_t} y_i/(\sigma\psi(t)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ for i.i.d. centred $y_i$ with variance $\sigma^2 > 0$ and $m_t/\psi(t) \to 1$ in probability.
Its $M$ -dimensional form (§5·4): $\psi(t)^{-1/2}\sum_1^{m_t} \mathbf y_j \xrightarrow{d} \mathcal N(0, a)$ for i.i.d. centred random vectors.
Theorem 9: if $E y_1 = 0$ and $\operatorname{var} y_1 = \sigma^2 > 0$ , then $P\{w_t/(\sigma(t/\mu_1)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ .
Corollary 9·1: the univariate forms of both assertions of the goal, with normalisations $\sigma = (\kappa_2 - \kappa_1^2)^{1/2}$ and $\gamma = \operatorname{var}(y_1 - (\kappa_1/\mu_1)t_1)$ .

Significance

Theorem 10 is the multivariate central limit theorem for regenerative processes. Its second assertion with $M = 2$ and the delta method gives the asymptotic normality of ratio estimators $w^{(1)}_t / w^{(2)}_t$ , the basis of the regenerative method of simulation output analysis. With $w_t = n_t$ , Corollary 9·1 recovers Feller's central limit theorem for renewal processes, which Smith points out (p. 9). The first assertion, with the random centring $\kappa_1 n_t$ , needs only $\mu_1 < \infty$ , which matters for heavy-tailed cycle lengths.

The results are classical and proved, and none of them is formalized. Mathlib has the central limit theorem for i.i.d. real sums with a deterministic number of terms and multivariate Gaussian laws, but no random-index central limit theorem, no renewal counting process and no regenerative process. A formal development would supply Anscombe's theorem (useful well beyond renewal theory, for sequential analysis and random sums), the renewal strong law and a reusable model of cumulative processes.

Difficulty

The obvious argument writes $w_t$ as the sum of the first $n_t$ cycle increments plus a remainder and applies the classical central limit theorem. This fails at two points. First, the number of summands $n_t$ is random and depends on the summands themselves (cycle lengths and rewards are typically dependent), so the classical theorem with a deterministic index does not apply and conditioning on $n_t$ destroys the i.i.d. structure. Anscombe's theorem is needed exactly for this; it requires control of the partial sums uniformly over a window of indices around $t/\mu_1$ , not at a single index. Second, the remainder over the incomplete cycle at time $t$ must be shown negligible on the scale $\sqrt t$ using only a second moment of the cycle variation; Lemma 8 does this almost surely. For the vector statement, the scalar theorem must be lifted to convergence in distribution in $\mathbb R^M$ with a possibly degenerate covariance matrix, where the scalar theorem's hypothesis $\sigma > 0$ can fail along some directions.

Formalization scope

Time is real; every limit is along $t \to \infty$ in $\mathbb R$ . Processes are functions $w : \mathbb R \to \Omega \to \mathbb R$ (or a family indexed by Fin M); cycle lengths are a sequence $\mathbb N \to \Omega \to \mathbb R$ with $t_0 = 0$ .
$n_t$ is a natural number, the number of epochs $T_j \le t$ ; on the null event where infinitely many epochs are $\le t$ it is $0$ . Finiteness is never assumed.
$\tilde w_t$ is the total variation (eVariationOn) of the path on $[0,t]$ , set to $0$ for all $t$ on paths of infinite variation, as Smith allows.
Condition (C1) is read for the whole cycle vector $(t_n, y_n, \tilde y_n)$ . No independence between components is assumed. Assuming the cycle length independent of the rewards, or the components independent, would make $a$ diagonal or force $b$ into a special form; that trivialization is ruled out.
"Jointly normally distributed with covariance matrix $a$ " is TendstoInDistribution to multivariateGaussian 0 a on EuclideanSpace ℝ (Fin M). The matrices $a$ and $b$ are defined as covariance matrices, hence positive semidefinite, so the limit is a genuine (possibly degenerate) Gaussian law and not Mathlib's Dirac fallback for non-PSD input.
The scalar statements keep the paper's form: convergence of $P\{\cdot \le \alpha\}$ to $\Phi(\alpha) =$ cdf (gaussianReal 0 1) α for every real $\alpha$ . The paper's implicit $\sigma > 0$ and $\gamma > 0$ are explicit hypotheses; without them the quotients are $0$ in Lean and the statements would be false.
$\mu_1 < \infty$ , $\mu_2 < \infty$ and $E\tilde y^2 < \infty$ are Integrable hypotheses, never encoded through the value of an integral.

Contributions welcome: a proof of Anscombe's theorem from Mathlib's central limit theorem; the renewal strong law from strong_law_ae; measurability lemmas for $n_t$ and $\tilde w_t$ ; the Cramér–Wold step.

Selected references

W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
F. J. Anscombe, Large-sample theory of sequential estimation, Proc. Cambridge Philos. Soc. 48, 600, 1952 (cited in Smith 1955, p. 31).
W. Feller, Fluctuation theory of recurrent events, Trans. Amer. Math. Soc. 67, 98, 1949 (cited in Smith 1955, p. 31).
J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63, 422, 1948 (cited in Smith 1955, p. 31).

9 thms2 active usersReviewed

Convex Optimization Numerical Analysis Optimization·Captain: mikedeng1

Fixed Point and Bregman Iterative Methods for Matrix Rank Minimization: The Matrix Shrinkage Fixed Point Iteration Converges to an Optimal Solution of the Nuclear Norm Regularized ProblemResearch Paper

Motivation

Many estimation problems ask for a matrix of low rank that is consistent with a small number of linear measurements: completing a partially observed ratings matrix, identifying a low-order linear system, or embedding points from a few pairwise distances. Rank minimization under linear constraints is NP-hard, and the standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values (Recht, Fazel and Parrilo, 2010). Under incoherence assumptions the surrogate recovers the low-rank matrix exactly (Candès and Recht, 2009).

The surrogate is a semidefinite program, and interior point methods for it do not scale past matrices of a few hundred rows. Ma, Goldfarb and Chen (2009) proposed a first-order method for the regularized form of the problem: a gradient step on the data-fit term followed by singular value shrinkage. Their algorithms FPC and FPCA are built on this two-line iteration, and the paper's one convergence theorem says that the iteration, run with a fixed step size, converges to a minimizer. This mission formalizes that theorem and the lemmas used to prove it.

Timeline of the closest results:

2005: Combettes and Wajs prove convergence of forward–backward splitting for the sum of a convex function and a convex function with Lipschitz gradient in a Hilbert space.
2008: Hale, Yin and Zhang analyse the fixed point continuation (FPC) method for $\ell_1$ -regularized least squares, with vector shrinkage in place of matrix shrinkage.
2008–2010: Cai, Candès and Shen introduce singular value thresholding (SVT) for matrix completion, prove that the shrinkage is the proximal map of the nuclear norm, and prove convergence of a different iteration (Uzawa's method on a strongly convex problem with equality constraints).
2009: Ma, Goldfarb and Chen state and prove convergence of the matrix shrinkage fixed point iteration for the nuclear norm regularized least squares problem (1.8), following Hale, Yin and Zhang's argument.

Setting

Fix natural numbers $m,n,p$ . Matrices $X\in\mathbb R^{m\times n}$ carry the Frobenius norm $\|X\|_F=(\sum_{ij}X_{ij}^2)^{1/2}$ and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$ . A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by matrices $A_0,\dots,A_{p-1}$ through $\mathcal A(X)_i=\langle A_i,X\rangle$ ; equivalently $\mathcal AX=A\,\mathrm{vec}(X)$ for a matrix $A\in\mathbb R^{p\times mn}$ . Its adjoint is $\mathcal A^*$ , and $\lambda_{\max}(A^\top A)=\|\mathcal A\|_2^2$ , the square of its spectral norm. Fix $b\in\mathbb R^p$ and $\mu>0$ .

Problem (1.8) is

\min_{X\in\mathbb R^{m\times n}}\ \mu\|X\|_*+\tfrac12\|\mathcal A(X)-b\|_2^2 ,

and $\mathcal X^*$ denotes its set of optimal solutions. Write $g(X)=\mathcal A^*(\mathcal A(X)-b)$ for the gradient of the data-fit term and $h(X)=X-\tau g(X)$ for a gradient step of size $\tau>0$ .

For $\nu>0$ , the matrix shrinkage operator $S_\nu$ takes a singular value decomposition $Y=U\,\mathrm{Diag}(\sigma)V^\top$ to $S_\nu(Y)=U\,\mathrm{Diag}(\bar\sigma)V^\top$ , where $\bar\sigma_i=\max(\sigma_i-\nu,0)$ . The fixed point iterations (2.1) start from an arbitrary $X^0$ and repeat

Y^k=X^k-\tau g(X^k),\qquad X^{k+1}=S_{\tau\mu}(Y^k).

Formalization targets

Goal: Theorem 4

For $\tau\in(0,2/\lambda_{\max}(A^\top A))$ and every starting point, there is $X^*\in\mathcal X^*$ with

\lim_{k\to\infty}\|X^k-X^*\|_F=0 .

The goal fixes no rate and no particular limit: it asserts convergence of the whole sequence to some minimizer.

Milestones, in attack order

Theorem 3. $S_\nu(Y)$ is an optimal solution of $\min_X\nu\|X\|_*+\tfrac12\|X-Y\|_F^2$ . This is already posed on the platform as Cai, Candès and Shen's Theorem 2.1 (which adds uniqueness) and is referenced, not restated.
Corollary 1. For every $\tau>0$ : $X^*\in\mathcal X^*$ if and only if $X^*=S_{\tau\mu}(h(X^*))$ .
Lemma 1. $\|S_\nu(Y_1)-S_\nu(Y_2)\|_F\le\|Y_1-Y_2\|_F$ , with equality if and only if $Y_1-Y_2=S_\nu(Y_1)-S_\nu(Y_2)$ .
Lemma 2. For $\tau$ in the step range, $\|h(X)-h(X')\|_F\le\|X-X'\|_F$ , and $h(X)-h(X')=X-X'$ if and only if equality holds.
Lemma 3. If $X^*\in\mathcal X^*$ , then $X\in\mathcal X^*$ if and only if $\|S_{\tau\mu}(h(X))-X^*\|_F=\|X-X^*\|_F$ .

The mission also contains the paper's Theorem 2, the optimality condition for (1.8) written with a reduced singular value decomposition $X=U\,\mathrm{Diag}(\sigma)V^\top$ : $X\in\mathcal X^*$ if and only if some $W$ satisfies $\mu(UV^\top+W)+g(X)=0$ , $U^\top W=0$ , $WV=0$ and $\|W\|_2\le1$ . The chain to Theorem 4 does not use it.

Significance

Theorem 4 is the correctness guarantee for FPC and FPCA, which were among the first algorithms to solve nuclear norm regularized problems with matrices in the thousands of rows. It certifies that the output of the plain iteration is an exact minimizer in the limit, for every starting point and every step below $2/\lambda_{\max}(A^\top A)$ . Lemmas 1–3 are the reusable part: non-expansiveness of the matrix shrinkage with a precise equality case, and the fixed point characterization of the optimal set, are the ingredients of every proximal gradient analysis with nuclear norm regularization.

Status: the theorem is proved on paper, and it is also a special case of the general convergence of forward–backward splitting. No machine-checked proof of it is known. The platform holds general forward–backward and inertial forward–backward convergence statements in Hilbert space (for example NesterovFB.Weak.theorem_3, InertialFB.IFB.theorem1_convergence) and the nonexpansiveness of abstract proximal maps (MoreauProx.Characterization.prox_nonexpansive). None is stated for the nuclear norm, for matrix shrinkage defined through the SVD, or with Ma, Goldfarb and Chen's equality cases. Formalizing this mission connects Mathlib's singular values to these operator-theoretic statements.

Difficulty

The obvious route goes through Fejér monotonicity: every step brings the iterate no farther from any minimizer, so the iterates are bounded and have a limit point. Two steps of this route do not come for free. First, the argument presupposes a minimizer; nothing in the hypotheses provides one, so the existence of an optimal solution of (1.8) has to be established from the data. Second, a limit point must be shown to be optimal, which requires the equality cases of Lemmas 1 and 2, not just the inequalities. Lemma 1's equality case concerns the singular value decompositions of two unrelated matrices whose singular vectors need not be aligned; non-expansiveness alone does not deliver it. Nonexpansive maps in general need not have convergent iterates (a rotation is nonexpansive), so continuity plus boundedness is not enough.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ. The Frobenius norm, the nuclear norm (the sum of Mathlib's LinearMap.singularValues), the linear map $\mathcal A$ as $p$ matrices Aop, its adjoint and spectral norm, and the shrinkage relation IsShrink are reused from the published Cai–Candès–Shen definitions.
$S_\nu$ is a relation, IsShrink ν Y X: $X$ is the shrinkage of $Y$ for some reduced SVD (orthonormal columns, positive singular values). Every statement takes the shrinkage output as a variable with an IsShrink hypothesis. The paper's Definition 4 also allows zero singular values, which shrink to zero and change nothing.
The step range $\tau\in(0,2/\lambda_{\max}(A^\top A))$ is written $0<\tau$ and $\tau\|\mathcal A\|_2^2<2$ , without division. For $\mathcal A=0$ this is the range $(0,\infty)$ , as on paper, rather than the empty range that Lean's $2/0=0$ would give.
$\mu>0$ is an explicit hypothesis, and so is $\nu>0$ in Lemma 1; in Corollary 1, $\tau>0$ is the only condition on the step, as on the page ("for any $\tau>0$ "). $\nu=\tau\mu$ is built into the statements.
The run of (2.1) is a predicate on the whole sequence with an arbitrary $X^0$ ; it is not the continuation scheme FPC and does not fix $X^0=0$ .
Convergence is in the Frobenius norm to some minimizer chosen after the run. Neither $\mathcal X^*\neq\emptyset$ nor boundedness of the iterates is a hypothesis; a statement that assumes either is a different, weaker theorem and is ruled out.
No statement assumes $m\le n$ ; the paper's "without loss of generality" belongs to its proofs.

A complete development needs the SVD of real matrices in terms of Mathlib's singular values, the subdifferential of the nuclear norm, and a Fejér-monotone convergence argument in finite dimension. The first two are reusable for any nuclear norm or spectral function result, and contributions of general lemmas about singular value shrinkage (functionality of IsShrink, its proximal characterization) are welcome.

Selected references

S. Ma, D. Goldfarb, L. Chen, Fixed point and Bregman iterative methods for matrix rank minimization, Math. Program. 128 (2011); preprint arXiv:0905.1643v2, 2009. https://arxiv.org/abs/0905.1643
J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://arxiv.org/abs/0810.3286
E. T. Hale, W. Yin, Y. Zhang, Fixed-point continuation for ℓ1-minimization: methodology and convergence, SIAM J. Optim. 19(3), 2008. https://doi.org/10.1137/070698920
P. L. Combettes, V. R. Wajs, Signal recovery by proximal forward-backward splitting, Multiscale Model. Simul. 4(4), 2005. https://doi.org/10.1137/050626090
B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://arxiv.org/abs/0706.4138
E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Found. Comput. Math. 9, 2009. https://arxiv.org/abs/0805.4471

10 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments I: An Optimal Assortment Always Consists of the k Most Popular Variants for Some kResearch Paper

Motivation

A retailer deciding which variants of a product to carry (colors, sizes, flavors) trades the extra sales that variety brings against the inventory cost of stocking many low-volume items. van Ryzin and Mahajan (Management Science 45(11), 1999) gave the first model that couples a multinomial logit (MNL) choice model of consumer substitution with newsvendor inventory costs, and showed that the resulting assortment problem has a simple structure. Their paper is a standard starting point of the assortment-planning literature in operations management: the "popular set" structure it proves is the benchmark that later work on assortment optimization under MNL demand (with capacity constraints, dynamic substitution, or other choice models) compares against.

This mission formalizes the paper's first main result, Theorem 1, together with the facts its proof rests on.

Setting

A store offers a subset $S$ of the variants $N=\{1,\dots,n\}$ of a category. Each variant $j$ has an MNL preference $v_j>0$ , and the option of buying nothing has preference $v_0>0$ . A customer facing $S$ buys variant $j\in S$ with probability

q_j(S)=\frac{v_j}{\sum_{i\in S}v_i+v_0}.

Variants are labelled so that $v_1\ge v_2\ge\cdots\ge v_n$ , and the most-popular sets are $A_i=\{1,\dots,i\}$ .

The retailer sells at price $p$ and buys at unit cost $c$ , with $0<c<p$ , and stocks $x_j$ units of each variant before the season. The critical fractile is $z=\Phi^{-1}(1-c/p)$ , with $\Phi$ the standard normal distribution function. Two models of aggregate demand $Y_j$ are considered, both with store volume $\lambda>0$ :

Independent population model. $Y_j$ is normal with mean $\lambda q_j$ and standard deviation $\sigma(\lambda q_j)^\beta$ , where $\sigma>0$ and $0\le\beta<1$ . The optimal expected profit $\max_{x\ge0}\sum_{j\in S}E[p\min\{x_j,Y_j\}-cx_j]$ equals

\pi_I(S,v)=(p-c)\lambda\sum_{j\in S}q_j-\frac{p\sigma\lambda^\beta e^{-z^2/2}}{\sqrt{2\pi}}\sum_{j\in S}q_j^\beta .

Trend-following population model. All customers make the same choice, so $Y_j=\lambda$ with probability $q_j$ and $Y_j=0$ otherwise. The optimal expected profit is

\pi_T(S,v)=\sum_{j\in S}(pq_j-c)^+\lambda .

The assortment problem is $\max_{S\subseteq N}\pi(S,v)$ for $\pi=\pi_I$ or $\pi=\pi_T$ .

For Lemma 1, fix $S$ and let $\delta\ge0$ be the preference of a variant added to it: $f(\delta)=\sum_{j\in S}v_j+\delta+v_0$ , $g_I$ and $g_T$ are the numerators of the profit after the addition, and $h_I=g_I/f$ , $h_T=g_T/f$ .

Formalization targets

Goal: Theorem 1 (p. 1503)

For each demand model there is a most-popular set that is optimal among all $2^n$ assortments:

\exists\,i\in\{0,\dots,n\}\ \forall S\subseteq N:\ \pi_I(S,v)\le\pi_I(A_i,v),\qquad \exists\,i\in\{1,\dots,n\}\ \forall S\subseteq N:\ \pi_T(S,v)\le\pi_T(A_i,v).

The paper prints $i\in\{1,\dots,n\}$ for both models. In the independent model the empty assortment can be the unique optimum (when $\pi_I(A_1,v)<0$ , for instance at small $\lambda$ ), so $i=0$ is allowed there; the trend-following range is the printed one.

Milestones

(4)–(7): under normal demand, $x^*_j=\lambda q_j+z\sigma(\lambda q_j)^\beta$ is the optimal stocking vector and the optimal profit is $\pi_I(S,v)$ .
(8): under trend-following demand, stocking $\lambda$ exactly when $pq_j\ge c$ is optimal and the optimal profit is $\pi_T(S,v)$ .
Mangasarian (1969): a convex function divided by a positive affine function is quasiconvex.
Appendix: $g_I$ and $g_T$ are convex in $\delta$ on $[0,v_1]$ .
Lemma 1: $h_I$ and $h_T$ are quasi-convex on $[0,v_1]$ .
§3.1: $h(v_j)=\pi(S\cup\{j\},v)$ for $j\notin S$ , and $h(0)=\pi(S,v)$ .

Significance

The search over assortments is a priori a search over $2^n$ subsets. Theorem 1 cuts it to the $n+1$ nested sets $A_0\subset A_1\subset\cdots\subset A_n$ , so the optimal assortment is found by comparing $n+1$ numbers. The result is not obvious: the paper's example ( $n=8$ , $v_1=v_2=10$ , $v_8=1$ ) shows that $\{1,8\}$ can beat $\{1,2\}$ , so the best assortment of a given size need not be the most popular one, and yet the overall optimum is always a most-popular set. The structure is used in the paper's own comparative statics (how optimal variety moves with price, store volume and the no-purchase preference) and its comparison of fashion categories under majorization, which are the other two missions of this series.

The theorem is proved in the paper; nothing here is open. To our knowledge no part of it, nor the closed-form normal newsvendor optimum (7), has a machine-checked proof. Formalizing it fixes the edge cases the printed statement glosses over (the empty assortment, the $\beta=0$ boundary) and produces reusable pieces: the normal newsvendor profit formula and Mangasarian's ratio criterion for quasiconvexity.

Difficulty

The obvious argument, "add variants in order of popularity", fails because adding a variant both brings new sales and cannibalizes the shares of the others, and the inventory term $\sum q_j^\beta$ is concave in the shares, so profit is not monotone or submodular in $S$ in any simple sense. The proof instead compares a set with the sets obtained by removing its least popular member or exchanging it for a more popular outside variant, and needs the profit after adding a variant of preference $\delta$ to be quasi-convex in $\delta$ . That quasi-convexity is not visible from (7) directly; it requires rewriting the profit as a ratio $g/f$ with $f$ affine and proving $g_I$ convex, which in turn needs concavity of $(\sum_{j\in S}v_j^\beta+\delta^\beta)(\sum_{j\in S}v_j+\delta+v_0)^{1-\beta}$ . The exchange argument must also handle ties among the $v_j$ , which the printed proof passes over. Milestone 1 needs the derivative of the normal newsvendor objective and the identity $E(Z-z)^+=\varphi(z)-z(1-\Phi(z))$ , neither of which is in Mathlib in this form.

Formalization scope

Variants are Fin n, 0-based: the paper's variant $j$ is index $j-1$ , $A_i$ is the set of indices below $i$ , and the paper's $v_1$ is the first entry v ⟨0, _⟩. The no-purchase preference $v_0$ is a separate real v0, never a variant. Preferences are strictly positive and the sorting $v_1\ge\cdots\ge v_n$ is the hypothesis Antitone v.
Standing hypotheses: $0<c<p$ , $\lambda>0$ , $\sigma>0$ , $0\le\beta<1$ ; the goal also assumes $n\ge1$ (the trend-following range $1\le i\le n$ needs it).
$z$ is defined from $p$ and $c$ as the least $x$ with $\Phi(x)\ge1-c/p$ , $\Phi$ the c.d.f. of Mathlib's gaussianReal 0 1; a separate theorem states $\Phi(z)=1-c/p$ and uniqueness.
Powers are Real.rpow, so $0^0=1$ . At $\beta=0$ this keeps (7) correct ( $\sum_{j\in S}q_j^0=|S|$ ), but $h_I(0)=\pi_I(S,v)$ then fails; that one clause carries $\beta>0$ . The goal keeps $0\le\beta<1$ .
The positive part $(\cdot)^+$ is max · 0. In (11), $\lambda$ multiplies both terms; the printed (11) has it on the sum only, which would break $h_T(v_j)=\pi_T(S\cup\{j\},v)$ unless $\lambda=1$ .
"Optimal" means $\pi(S,v)\le\pi(A_i,v)$ for every $S\subseteq N$ , including $S=\emptyset$ . A formalization that maximizes only over prefix sets, assumes the optimum nonempty or the profit nonnegative, treats $z$ as a free real unrelated to $p$ and $c$ , or drops one of the two demand models, is a different and weaker statement and does not count.
In milestone 1 the order-up-to levels $x^*_j$ are assumed nonnegative, the formal content of the paper's assumption $\lambda^{1-\beta}q_j\gg\sigma q_j^\beta$ .

Needed infrastructure: the normal loss function and the first-order condition for the newsvendor under gaussianReal; quasiconvexity of convex-over-positive-affine ratios; concavity of weighted geometric means. The newsvendor and quasiconvexity pieces are reusable well beyond this mission. Proofs of any milestone, and alternative routes to Theorem 1 that avoid Lemma 1, are welcome.

Selected references

G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11):1496–1509, 1999. https://doi.org/10.1287/mnsc.45.11.1496
O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969 (reprinted SIAM Classics in Applied Mathematics 10, 1994). https://doi.org/10.1137/1.9781611971255
R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, 1959.

9 thms2 active usersReviewed

Completed

Combinatorics Optimization·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 5: Full-Batch LPT Is Within 4/3 − 1/(3m) of the Optimal Makespan on Parallel Batch MachinesResearch Paper

Motivation

Burn-in is the final reliability test of integrated circuits: boards loaded with chips are held in an oven at elevated temperature for a minimum specified time, so that marginal devices fail before shipment. An oven holds several boards at once, and a load may stay in the oven longer than its specification but never shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model such an oven as a batch processing machine and study the resulting scheduling problems. Burn-in is often the bottleneck of the test stage, which is why throughput (makespan) and due-date performance on several ovens in parallel are of practical interest.

This mission covers the paper's makespan result for parallel ovens. On ordinary identical parallel machines, Graham (SIAM J. Appl. Math. 17, 1969) proved that the LPT rule (list the jobs longest first and give each to the machine that frees up first) has worst-case ratio $4/3 - 1/(3m)$ on $m$ machines. The paper shows that the same factor holds for batch machines once the jobs are first grouped into full batches of the longest jobs.

Setting

There are $n$ jobs with processing times $p_j > 0$ , all available at time $0$ , and $m \ge 1$ identical batch processing machines. Each machine processes up to $B \ge 1$ jobs at the same time. A batch is a set of at most $B$ jobs processed together; once started it cannot be interrupted or joined, and its batch time is that of its longest job,

p(P) = \max_{j \in P} p_j .

A schedule forms the jobs into disjoint nonempty batches covering all jobs, assigns each batch to a machine, and runs every machine's batches back to back from time $0$ . The makespan is the largest machine load, the total batch time on a machine. The problem of minimizing it is written $P/B/C_{\max}$ , and $C^*$ denotes its optimal value, over every way of forming batches (any sizes up to $B$ , any grouping) and every assignment. For $B = 1$ it is the classical problem $P//C_{\max}$ .

Algorithm BLPT.

Rank the jobs in nonincreasing order of processing time and cut the ranked list into successive groups of $B$ jobs, the last possibly smaller.
Order these batches in nonincreasing order of batch time and assign each in turn to a machine with least current load.

$C(\mathrm{BLPT})$ is the resulting makespan.

For the optional lateness result, each job also has a due date $d_j \ge 0$ . The maximum lateness of a schedule is $L_{\max} = \max_j (C_j - d_j)$ , $L$ is its value under BLPT, $L^*$ its optimum and $d_{\max} = \max_j d_j$ .

Formalization targets

Goal: Proposition 3 (p. 773)

C(\mathrm{BLPT}) \le \left(\frac43 - \frac1{3m}\right) C^* .

It is claimed for every run of BLPT, whatever order the algorithm gives to equal processing times and equal batch times.

Milestones

Proposition 2 (p. 772). With the jobs re-indexed longest first, some optimal schedule has batches of consecutive jobs, all full except possibly the one containing the last job. In other words, its batches are exactly the groups formed in Step 1 of BLPT.
The reduction (§5, p. 772). $C^*$ equals the optimal makespan of $P//C_{\max}$ on the aggregate jobs $p(B_1), \dots, p(B_{\lceil n/B\rceil})$ .
Graham's LPT bound, as quoted (p. 772). For jobs $q_0 \ge \dots \ge q_{M-1} \ge 0$ on $m$ machines, list scheduling in that order has makespan at most $(4/3 - 1/(3m))$ times the optimum.
Proposition 5 (p. 773, further result).

\frac{L - L^*}{L^* + d_{\max}} \le \left(\frac13 - \frac1{3m}\right) + \frac{d_{\max}}{L^* + d_{\max}} .

Significance

Proposition 3 gives a constant-factor guarantee for a strongly NP-hard problem. The guarantee does not depend on $B$ , whereas arbitrary batch list scheduling only gets $B + 1 - 1/m$ (Proposition 1 of the same paper). For one machine the factor is $1$ , so BLPT is then exact. Proposition 2 is a structural statement: it fixes the batch composition of an optimal schedule before any assignment decision. It turns the batch problem into an ordinary parallel-machine problem, so other results for $P//C_{\max}$ transfer as well. Proposition 5 carries the guarantee over to maximum lateness, measured relative to $L^* + d_{\max}$ because $L^*$ may be negative.

All results are proved in the paper, Proposition 3 by a one-line appeal to Proposition 2 and Graham. This mission produces machine-checked versions of the reduction and the bound. Graham's LPT bound itself is not formalized anywhere on the platform. Its proof here is a reusable result about the published list-scheduling definitions, independent of batching.

Difficulty

The obvious argument is "batch as in Step 1, then apply Graham". It has two gaps. First, $C^*$ ranges over all batchings, and an optimal schedule need not use full batches or consecutive jobs. The exchange argument behind Proposition 2 has to move jobs between batches, possibly on different machines, without increasing any machine's load. Ties among equal processing times also have to be handled, since the claim is made for every longest-first ranking. Second, Graham's bound is not on the platform and has to be proved. It is a finite combinatorial statement, but its known proofs are not short. Proposition 5 additionally needs the bound for sub-instances formed by a prefix of the batches.

Formalization scope

Jobs are Fin n, 0-based. Processing times are real, p : Fin n → ℝ with 0 < p j; due dates (Proposition 5 only) are d : Fin n → ℝ with 0 ≤ d j. A batching is a list of nonempty, pairwise disjoint Finsets of size at most B covering every job. The batch time is the maximum of p over the batch.

Machine loads, assignments, the per-batching optimum and list scheduling reuse the published definitions NumStochOpt.ListScheduling.ListSchedule (firstAvailable, lsLoads, listMakespan) and NumStochOpt.ListScheduling.Makespan (machineLoad, makespan, optMakespan) from the Rinnooy Kan–Stougie mission, applied to the sequence of batch times (padded with zeros beyond the last batch, which these definitions never read). $C^*$ is the infimum of optMakespan over all valid batchings, never only over the consecutive ones of Step 1, which would assume Proposition 2.

Explicit readings of the paper's phrases:

"rank jobs in decreasing order" is any list of all jobs that is nonincreasing in p;
the batches of Step 1 are List.toChunks B of that list;
"order the batches in nonincreasing order of $p(B_k)$ " is any permutation of those chunks that is nonincreasing in batch time;
every statement is quantified over both choices;
"assign them to the machines as they become free" is least-loaded list scheduling with the published lowest-index tie rule. With no idle time, the machine that becomes free first is a least-loaded one, and the tie rule does not change the multiset of loads;
" $1/3m$ " is $1/(3m)$ ;
"optimal solution" in Proposition 2 is a valid batching with an assignment whose makespan equals $C^*$ , and "consecutive, all full except the one containing the highest indexed job" is "equal, up to order, to the chunks of the ranked list";
schedules on each machine run in list order without idle time, and every processing order is a reordering of the list. For $L^*$ this covers every semi-active schedule.

Proposition 5 adds the hypothesis $d_j \ge 0$ , which the paper's proof uses but does not print. It also makes $L^* + d_{\max}$ positive, so the printed ratios are well defined. Running times and the paper's other algorithms are out of scope.

A statement with $C^*$ restricted to consecutive batches, a sorry-free bound obtained from a degenerate $m = 0$ or empty-job reading, or a BLPT fixed to one convenient tie-break would trivialize or weaken the goal and is ruled out by the statements as posed. Welcome contributions: Graham's LPT bound on the published list-scheduling definitions (reusable for any $P//C_{\max}$ work), the exchange lemma behind Proposition 2, and the permutation invariance of optMakespan under reordering of items.

Selected references

C.-Y. Lee, R. Uzsoy, L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. https://doi.org/10.1287/opre.40.4.764
R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. https://doi.org/10.1137/0117039
A. H. G. Rinnooy Kan, L. Stougie, Stochastic Integer Programming, Ch. 8 of Y. Ermoliev, R. J.-B. Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer, 1988 (source of the reused list-scheduling definitions). https://doi.org/10.1007/978-3-642-61370-8

10 thms2 active usersReviewed

Completed

Machine Learning Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 1: WM Makes at Most log(w_init/w_fin)/log(2/(1+β)) Mistakes on Any SequenceResearch Paper

Motivation

In online prediction, a learner makes a forecast before seeing the next label. A collection of other forecasters may offer useful advice, but the learner need not know beforehand which forecaster will perform well. Littlestone and Warmuth's Weighted Majority Algorithm (WM) gives a deterministic way to combine such advice. Its guarantees hold for every finite sequence of instances and labels, including sequences chosen without any probability model. That worst-case setting is useful when the reliability of the forecasters can change or when no data-generating distribution has been justified. The paper develops WM and several variants; this mission isolates its basic mistake bound. Littlestone and Warmuth, 1994.

Setting

A finite pool has $n$ members, each of which predicts either $0$ or $1$ on every trial. The true label on trial $t$ is $\rho_t\in\{0,1\}$ , and member $i$ predicts $x_{t,i}\in\{0,1\}$ . The master prediction is $\lambda_t\in\{0,1\}$ . Pool members may themselves be learning algorithms, so their predictions may reflect all earlier labels. The mission treats their prediction vectors and the labels as arbitrary finite sequences; no independence or stationarity is assumed.

Each member begins with a strictly positive real weight $w_{0,i}$ . Before trial $t$ , let $w_{t,i}$ be its current weight. For $b\in\{0,1\}$ , let $q_{t,b}$ be the sum of weights of members predicting $b$ . WM predicts the value with the larger backing total. When the two totals tie, either binary prediction is allowed. After the label is revealed, WM changes weights only if its own prediction was wrong. On such a trial, each member that predicted the wrong label has its weight multiplied by a fixed factor $\beta$ with $0\le\beta<1$ ; every other member retains its weight. If WM predicted correctly, every weight stays as it was. This is the version of the algorithm stated in §1 of the paper. A footnote there says the bounds also apply to the variant that updates on every trial. Littlestone and Warmuth, 1994, p. 215.

Write $W_t=\sum_i w_{t,i}$ for the total pool weight at a trial boundary. Thus $W_0=w_{\mathrm{init}}$ and $W_T=w_{\mathrm{fin}}$ after $T$ trials. Let $m$ count the trials with $\lambda_t\ne\rho_t$ . The default initial weights in the paper are all one, but its Theorem 2.1 permits arbitrary positive initial weights. Littlestone and Warmuth, 1994, pp. 220–221.

Formalization targets

The two milestones state the weight facts used immediately before and within Theorem 2.1. First, on each trial where WM errs,

W_{t+1}\le \frac{1+\beta}{2}W_t.

Across the whole sequence, with $m$ master mistakes, the corresponding estimate is

W_T\le W_0\left(\frac{1+\beta}{2}\right)^m.

The goal is the paper's Theorem 2.1, retaining its explicit constant:

m\le \frac{\log(W_0/W_T)} {\log\!\left(2/(1+\beta)\right)} \qquad\text{when }W_T>0.

The logarithm base is immaterial because the same base occurs above and below the fraction. The paper explicitly uses this convention for ratios of logarithms. The positive-final-weight condition represents the paper's statement that the displayed logarithmic bound is vacuous when all weight has vanished, which can happen for $\beta=0$ . The whole-sequence weight estimate remains meaningful in that case. Littlestone and Warmuth, 1994, pp. 220–221.

Significance

The result limits the mistakes of a master predictor without assigning probabilities to the predictions or labels. It relates a visible property of the run, the reduction of total weight, to the number of master errors. Later bounds in the paper use this starting point to compare WM with an individual pool member and to analyze related algorithms; this mission fixes the initial, exact-constant result on which those comparisons rest. The $\beta=0$ case includes the paper's Halving Algorithm interpretation when initial weights are equal. Littlestone and Warmuth, 1994, pp. 215, 221–222.

The mathematical theorem is proved in the 1994 paper. The remaining task here is to represent its algorithm and finite-sequence bound in Lean and supply machine-checked proofs. A complete development would give later formalizations a reusable finite-pool voting and weight-update model, along with a checked potential estimate. The local draft statements compile; their proofs remain open. A separate, sorry-free local check constructs a run for every finite prediction and label sequence with a nonempty pool and valid weights and parameter, so the quantified run relation has witnesses.

Difficulty

The master can be wrong even when some pool members are right, and members may change their predictions over time. Counting one member's errors therefore does not directly control the master's error count. The exact contraction constant also depends on which side of a weighted vote the master chose, including the permitted tie case. When $\beta=0$ , a single mistake can erase all weight backing the wrong label, so the logarithmic expression must be interpreted with care if no positive weight remains. These are features of the stated algorithm, rather than assumptions about how the sequence was generated.

Formalization scope

The formalization indexes pool members by Fin n and trials by Fin T. Booleans represent binary predictions and labels; weights and $\beta$ are real. A WM run is a relation on the full sequence of weights and master predictions, admitting every choice at a tied vote. Its update rule changes weights only after a master mistake, scales exactly the members that disagreed with the label, and leaves all other weights unchanged. Theorems require $0\le\beta<1$ and strictly positive initial member weights. The goal additionally requires $W_T>0$ , while the two weight inequalities permit $W_T=0$ . Natural logarithms instantiate the paper's common-base logarithm convention. Finite sums and a finite mistake count match the paper's finite-sequence convention.

The statement ranges over arbitrary pool predictions and labels, so it cannot be satisfied merely by selecting an easy input sequence. The run relation allows both legal outcomes of a tie; selecting one favorable tie rule would weaken the target. The sorry-free run-existence check also rules out a vacuous theorem caused by an inconsistent update relation. The paper's update-on-every-trial variant, its member-specific corollaries, and its later algorithms are outside this mission's goal.

A completed formalization needs finite sums of real weights, cardinalities of finite sets of mistake trials, a finite induction over trial boundaries, and real logarithm inequalities. The run definition and the first two bounds can be reused in the later parts of this paper's formalization. Contributions that prove the exact stated milestones or supply supporting facts about legal runs and nonnegative weights are within scope.

Selected references

Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.

4 thms2 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

Efficient Algorithms for Scheduling Semiconductor Burn-In Operations 3: Dynamic Program DP3 Minimizes the Number of Tardy Equal-Length Jobs on a Batch Machine with Agreeable Release and Due DatesResearch Paper

Motivation

Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).

Setting

There are $n$ jobs and one batch processing machine with capacity $B\ge1$ . Job $j$ has release time $r_j$ , due date $d_j$ , and processing time $p_j$ . In the main problem every processing time equals a common value $p$ . A batch is a nonempty set of at most $B$ jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.

The completion time $C_j(S)$ of job $j$ in schedule $S$ is the completion time of its batch. A job is on time when $C_j(S)\le d_j$ and tardy when $d_j<C_j(S)$ . Write $U(S)=\#\{j:d_j<C_j(S)\}$ and let $U^*$ be the minimum of $U(S)$ over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.

For the structural lemmas, agreeable release times and due dates mean that $r_i<r_j$ implies $d_i\le d_j$ . For the dynamic program, jobs are indexed so that both $r_j$ and $d_j$ are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).

Formalization targets

Structural optimal schedules

Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which $U^*$ is defined.

Correctness of Algorithm DP3

Let $f(i,j)$ be the table defined by Algorithm DP3 for the first $j$ jobs and a selected count $i$ of on-time jobs. Its boundary values are $f(0,j)=0$ and $f(i,j)=+\infty$ for $i>j$ . For $1\le i\le j$ , it takes the minimum of $f(i,j-1)$ and the eligible transitions that append a batch of $k$ jobs, $1\le k\le\min(B,i)$ . A transition uses $\max\{f(i-k,j-k),r_j\}+p$ and is eligible when that completion time does not exceed $d_{j-k+1}$ . The main target is

U^*=n-\max\{i\in\{0,\ldots,n\}:f(i,n)<+\infty\}.

The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).

Unequal processing times

The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common $p$ by $f(i-k,j-k)+p_j$ . The corresponding correctness statement is a further milestone (p. 771).

Significance

The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.

The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.

Difficulty

The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.

Formalization scope

Jobs use Fin n, with index zero representing the paper's job 1; the table's $j$ is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; $+\infty$ in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most $B$ , pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.

The strict implication $r_i<r_j\Rightarrow d_i\le d_j$ makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that $r_j$ is the last batch's latest release and $d_{j-k+1}$ its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range $1\le k\le\min(B,i)$ , with an empty range giving $+\infty$ . Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.

This mission covers correctness only. The paper's $O(n^2B)$ running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.

Selected references

C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 1992, pp. 764–775. DOI: 10.1287/opre.40.4.764.

9 thms2 active usersReviewed

Operations Research

Missions

Potential Games 4: An Efficient Solution Is the Shapley Value on the Subgames of v If and Only If the Participation Game Γ(ψ, c, v) Is a Potential GameResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1 (p. 137)

Milestones (proof of Theorem 6.1, p. 137)

Further: Theorem 6.2 (p. 137)

Significance

Difficulty

Formalization scope

Selected references

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 5: Nonquadratic Proximal Methods of Multipliers Converge to a Saddle PointResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8

Existence clause

Milestones

Significance

Difficulty

Formalization scope

Selected references

Cooperative Fuzzy Games 3: The Diagonal Formula Is the Unique Continuous Linear Pareto-Optimal, Symmetric and Atomic Value of Smooth Fuzzy GamesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Implicit Renewal Theory and Tails of Solutions of Random Equations 3: Rate of Approach — t^κP(R > t) Equals C₊ Minus a Contour Integral Plus O(t^{−β/2})Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Reflected Solutions of Backward SDE's, and Related Obstacle Problems for PDE's 2: With a Concave Coefficient, the Reflected BSDE Is the Value of a Minimax Optimal Stopping–Control ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7.2 (p. 725)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 3: Under Box Uncertainty, Worst-Case CVaR Minimization (16)–(20) Is Equivalent to the Linear Program (24)–(30)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 1159)

Milestones, in the order the paper's argument uses them

Significance

Difficulty

Formalization scope

Selected references

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 1: In O(√nL) Predictor-Corrector Iterations It Finds LP and Dual Optima or Detects InfeasibilityResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 7

Theorem 6

Milestones

Significance

Difficulty

Formalization scope

Selected references

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 2: For a Compact Convex Set of Discrete Distributions, Worst-Case CVaR Equals min_α max_π G_β(x, α, π)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 1159)