Operations Research

Functional Analysis Probability·Captain: mikedeng1

Conditional and Dynamic Convex Risk Measures I: Robust Representation of Conditional Convex Risk MeasuresResearch Paper

Motivation

A convex risk measure assigns to a bounded financial position $X$ (a random net payoff) a number $\rho(X)$ , interpreted as the capital that must be added to $X$ to make it acceptable. The axiomatic theory began with coherent risk measures (Artzner, Delbaen, Eber and Heath, 1999) and was extended to convex ones by Föllmer and Schied (2002) and Frittelli and Rosazza Gianin (2002). Its central structural result is a robust representation: a convex risk measure that is continuous from above equals a worst case of expected losses over a family of probabilistic models, each penalized by how implausible it is.

Regulators and risk managers do not assess positions once and for all; they reassess them as information arrives. Detlefsen and Scandolo (2005) extend the representation to conditional risk measures, whose value $\rho(X)$ is itself a random variable measurable with respect to the information available to the agent. This is the building block of dynamic (time-consistent) risk measurement, studied in later work on dynamic risk measures and backward stochastic differential equations.

Timeline. Artzner et al. (1999): coherent risk measures on finite $\Omega$ . Delbaen (2002): coherent risk measures on general probability spaces, Fatou property. Föllmer–Schied (2002) and Frittelli–Rosazza Gianin (2002): convex risk measures and their robust representation; Föllmer–Schied, Stochastic Finance, Theorem 4.26 (2002 edition) for $L^\infty$ with continuity from above. Detlefsen–Scandolo (2005): the conditional version, Theorem 3.2 of the paper formalized here.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub- $\sigma$ -algebra $\mathcal G\subseteq\mathcal F$ describing the available information. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$ -measurable part; every (in)equality between random variables holds $P$ -almost surely.

A map $\rho:L^\infty\to L^\infty_{\mathcal G}$ is a conditional convex risk measure if $\rho(0)=0$ and, for $X,Y\in L^\infty$ :

(conditional translation invariance) $\rho(X+Z)=\rho(X)-Z$ for every $Z\in L^\infty_{\mathcal G}$ ;
(monotonicity) $X\le Y$ implies $\rho(X)\ge\rho(Y)$ ;
(conditional convexity) $\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for every $\Lambda\in L^\infty_{\mathcal G}$ with $0\le\Lambda\le1$ .

The admissible models are

\mathcal P_{\mathcal G}=\{Q \text{ probability on }(\Omega,\mathcal F): Q\ll P,\ Q(A)=P(A)\text{ for all }A\in\mathcal G\}.

For a family $\mathcal X$ of $[-\infty,+\infty]$ -valued random variables, the essential supremum $\operatorname{ess.sup}\mathcal X$ is the $P$ -a.s. smallest random variable that dominates every member $P$ -a.s.; it replaces the pointwise supremum, which is not meaningful for uncountable families of equivalence classes.

A map $\rho$ is representable if there is a penalty $\alpha:\mathcal P_{\mathcal G}\to L^0_{\mathcal G}([0,+\infty])$ with

\rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha(Q)\},\qquad X\in L^\infty .

The minimal penalty is $\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\}$ . $\rho$ is continuous from above if $X_n\searrow X$ $P$ -a.s. implies $\rho(X_n)\nearrow\rho(X)$ $P$ -a.s.

Formalization targets

Goal: Theorem 3.2

For a conditional convex risk measure $\rho$ , the following are equivalent:

\text{(a) } \rho \text{ continuous from above}\iff\text{(b) } \rho\text{ representable}\iff\text{(c) } \rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}.

Milestones

Theorem A.1: existence and a.s. uniqueness of the essential supremum; an increasing sequence converging to it for upward directed families.
Lemma A.2: $E_P(\operatorname{ess.sup}\mathcal X)=\sup_{X\in\mathcal X}E_PX$ for upward directed $\mathcal X$ .
The easy inequality $\rho(X)\ge\operatorname{ess.sup}_{Q}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}$ .
The unconditional representation (Föllmer–Schied, Theorem 4.26) of a convex risk measure $\rho_0:L^\infty\to\mathbb R$ continuous from above: $\rho_0(X)=\sup_{Q\ll P}\{-E_QX-\alpha^*_0(Q)\}$ .
For $\rho_0=E_P[\rho(\cdot)]$ : $\alpha^*_0(Q)<\infty$ forces $Q\in\mathcal P_{\mathcal G}$ .
The family $B_Q=\{-E_Q(X\mid\mathcal G)-\rho(X):X\in L^\infty\}$ is upward directed.
$E_P[\alpha^*(Q)]=\alpha^*_0(Q)$ for $Q\in\mathcal P_{\mathcal G}$ .
Representable implies continuous from above.
Remark 3.3: $\alpha^*\le\alpha$ for every penalty $\alpha$ , and $\alpha^*(Q)=\operatorname{ess.sup}_{X\in\mathcal A_\rho}\{-E_Q(X\mid\mathcal G)\}$ .

Significance

The result. Theorem 3.2 shows that a conditional convex risk measure is determined by a random penalty on the models consistent with the available information, exactly when it satisfies a sequential continuity condition. The representation is the input for the paper's later sections: the conditional entropic risk measure, whose minimal penalty is the conditional relative entropy, and the consistency of dynamic risk measures via Lemma 3.4, which is expressed through the minimal penalty. The restriction to $\mathcal P_{\mathcal G}$ has an interpretation: the more information, the fewer models can enter the worst case.

Formalizing it. The theorem has been proved in the literature since 2005; to our knowledge neither it nor its unconditional counterpart has a machine-checked proof. The mission produces an essential supremum of arbitrary families of extended random variables with its existence theorem, the exchange of expectation and essential supremum for directed families, and the unconditional Föllmer–Schied representation on $L^\infty$ . The last of these is the standard representation theorem of the theory of convex risk measures and is useful well beyond this paper.

Difficulty

The obvious route, applying the unconditional representation pathwise or $\omega$ by $\omega$ , fails: $\rho(X)(\omega)$ is not a risk measure of anything, and conditional expectations are only defined up to null sets that depend on $Q$ , of which there are uncountably many. The essential supremum is what turns an uncountable supremum of classes into a well-defined class, and passing expectations through it requires directedness. The unconditional step itself (continuity from above implies the dual representation) rests on a Krein–Šmulian / weak* closedness argument on $L^\infty$ , which is not available off the shelf.

Formalization scope

Payoffs are real functions $\Omega\to\mathbb R$ with MemLp X ⊤ P; $\rho$ is a map $(\Omega\to\mathbb R)\to(\Omega\to\mathbb R)$ constrained only on $L^\infty$ . Because it acts on functions, $\rho$ is required to respect $P$ -a.s. equality, and $\rho(X)$ is required to be $\mathcal G$ -strongly measurable and essentially bounded; the paper's $\rho$ acts on classes, so this adds nothing in substance. $\mathcal G$ is a MeasurableSpace m with m ≤ mΩ.
Translation invariance and convexity quantify over $\mathcal G$ -measurable $Z$ and $\Lambda$ (not constants). $\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$ — equality on $\mathcal G$ , not mutual absolute continuity.
$E_Q(X\mid\mathcal G)$ is Mathlib's Q[X | m]; it is $\mathcal G$ -measurable, hence determined $P$ -a.s. for $Q\in\mathcal P_{\mathcal G}$ .
Extended values live in EReal; penalties are ENNReal-valued and coerced, so only (real) $-(+\infty)=-\infty$ occurs, never $+\infty-(+\infty)$ .
The essential supremum is a predicate IsEssSup P F Z (a.e. upper bound of every member, a.e. below every a.e.-measurable a.e. upper bound). The minimal penalty is a predicate IsMinimalPenalty on a candidate; statement (c) of the goal asserts that a $\mathcal G$ -measurable $[0,+\infty]$ -valued essential supremum of $B_Q$ is a penalty for $\rho$ .
Continuity from above: $X_n,X\in L^\infty$ , $(X_n)$ a.s. non-increasing and a.s. convergent to $X$ implies $(\rho(X_n))$ a.s. non-decreasing and a.s. convergent to $\rho(X)$ . It is not norm or weak* continuity.
Lemma A.2's "provided the expectations exist" is pinned as: each member has an expectation in $[-\infty,+\infty]$ and some member has integrable negative part (without the latter the lemma is false). Theorem A.1's directed part assumes a nonempty family. The acceptance set of Remark 3.3 is $\{X\in L^\infty:\rho(X)\le0\}$ (the paper's $L^\infty_{\mathcal G}$ on p. 4 is a misprint).
Ruled out: an essential supremum defined as a pointwise ⨆ over the family, or via Mathlib's essSup of a single function, and an index set equal to all $Q\ll P$ or to the $Q$ equivalent to $P$ ; each of these changes statement (b) or makes it vacuous.
Needed infrastructure: essential suprema of families, extended expectations with monotone convergence, conditional expectation under a change of measure agreeing on $\mathcal G$ , and the $L^\infty$ – $L^1$ duality behind Föllmer–Schied 4.26. The essential-supremum layer and the unconditional representation are reusable in any mission on risk measures or robust optimization; contributions to either are welcome.

Selected references

K. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized here; journal version: Finance and Stochastics 9(4), 539–561, 2005, https://doi.org/10.1007/s00780-005-0159-6)
H. Föllmer, A. Schied, Stochastic Finance — An Introduction in Discrete Time, de Gruyter Studies in Mathematics 27, 2002. https://doi.org/10.1515/9783110198065
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4), 429–447, 2002. https://doi.org/10.1007/s007800200072
M. Frittelli, E. Rosazza Gianin, Putting order in risk measures, Journal of Banking and Finance 26, 1473–1486, 2002. https://doi.org/10.1016/S0378-4266(02)00270-4
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 203–228, 1999. https://doi.org/10.1111/1467-9965.00068
F. Delbaen, Coherent risk measures on general probability spaces, in Advances in Finance and Stochastics, Springer, 2002. https://doi.org/10.1007/978-3-662-04790-3_1

14 thms2 active usersReviewed

Control Theory Optimization·Captain: mikedeng1

Optimizing Static Linear Feedback: Gradient Method I: The Gradient Method Converges to a Stationary Point, and Linearly to the Optimal Gain under State FeedbackResearch Paper

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost. When the full state is measured and the gain may be chosen freely, the optimal feedback is given by the algebraic Riccati equation (Kalman, 1960). In many applications only an output $y = Cx$ is measured, and the controller is restricted to a static feedback $u = -Ky$ . For this output-feedback problem no Riccati-type characterization exists; the design problem is a non-convex optimization over the gain matrix $K$ .

Direct optimization of the gain by gradient descent, known in the control literature since Levine and Athans (1970) and revived in reinforcement learning as policy gradient (Fazel, Ge, Kakade and Mesbahi, 2018, arXiv:1801.05039), is therefore of interest both to control engineers and to the learning community. Fatkhullin and Polyak (arXiv:2004.09875, SIAM J. Control Optim. 2021) give a self-contained analysis of the continuous-time problem: the cost is coercive on the set of stabilizing gains, smooth on sublevel sets, and, for state feedback, satisfies a gradient-domination (Łežanski–Polyak–Łojasiewicz) inequality. From these they derive convergence guarantees for the gradient method.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$ , $B\in\mathbb R^{n\times m}$ , $C\in\mathbb R^{r\times n}$ and weights $Q\in\mathbb R^{n\times n}$ , $R\in\mathbb R^{m\times m}$ , and an initial-state covariance $\Sigma\in\mathbb R^{n\times n}$ . A gain is a matrix $K\in\mathbb R^{m\times r}$ , and the closed-loop matrix is $A_K = A - BKC$ . A square matrix is Hurwitz if all its complex eigenvalues have negative real part. The set of stabilizing gains is

\mathcal S = \{K\in\mathbb R^{m\times r} : A_K \text{ is Hurwitz}\}.

For $K\in\mathcal S$ let $X(K)$ be the unique solution of the Lyapunov equation

A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,

and define the cost $f(K)=\mathrm{Tr}\big(X(K)\Sigma\big)$ , the expected integrated quadratic cost of the closed loop from a random initial state with covariance $\Sigma$ . With $Y(K)$ the solution of $A_KY+YA_K^\top+\Sigma=0$ , the gradient of $f$ in the Frobenius inner product is

\nabla f(K)=2\big(RKC-B^\top X(K)\big)Y(K)C^\top .

A known stabilizing gain $K_0\in\mathcal S$ is given, and $\mathcal S_0=\{K\in\mathcal S: f(K)\le f(K_0)\}$ is its sublevel set. The standing assumptions are $Q,R,\Sigma\succ0$ , $\operatorname{rank}C=r$ and $B\neq0$ . State feedback (SLQR) is the case $C=I$ .

The gradient method with step sizes $\gamma_j$ is

K_{j+1}=K_j-\gamma_j\nabla f(K_j),\qquad j\ge0 .

A number $L>0$ is a smoothness constant if $\|\nabla f(K)-\nabla f(K')\|_F\le L\|K-K'\|_F$ for all $K,K'\in\mathcal S_0$ .

Formalization targets

Goal: Theorem 4.2 for state feedback

For $C=I$ , an optimal gain $K_*\in\mathcal S$ , and any smoothness constant $L$ :

if $0<\gamma_j\le 2/L$ for all $j$ , then every $K_j\in\mathcal S_0$ and

f(K_{j+1})\le f(K_j)-\gamma_j\Big(1-\frac{L\gamma_j}{2}\Big)\|\nabla f(K_j)\|_F^2 ;

if $0<\varepsilon_1\le\gamma_j\le 2/L-\varepsilon_2$ with $\varepsilon_2>0$ , then $\nabla f(K_j)\to0$ ,

\min_{0\le j\le k}\|\nabla f(K_j)\|_F^2\le\frac{f(K_0)}{c_1k}\quad(k\ge1),\qquad c_1=\frac{\varepsilon_1\varepsilon_2L}{2},

and there are $c\ge0$ , $0\le q<1$ with $\|K_j-K_*\|_F\le c\,q^j$ .

Milestones

In attack order:

Appendix A lemmas. Trace duality of dual Lyapunov equations (Lemma A.1), the trace sandwich (Lemma A.4), and eigenvalue lower bounds for Lyapunov solutions (Lemma A.5).
Coercivity and existence. Coercivity of $f$ with the lower bounds (3.1)–(3.2) (Lemma 3.8), boundedness of $\mathcal S_0$ (Corollary 3.9), and existence of a minimizer (Corollary 3.10).
Smoothness. The gradient formula (Lemma 3.11) and existence of a smoothness constant on $\mathcal S_0$ (Theorem 3.15, qualitative form).
Gradient domination for state feedback. Lemmas C.2, C.3 and C.1, and the LPL inequality with the explicit constant (3.11):

\tfrac12\|\nabla f(K)\|_F^2\ge\mu\big(f(K)-f(K_*)\big),\qquad K\in\mathcal S_0 \qquad\text{(Theorem 3.17)}.

Theorem 4.2 for output feedback. Descent and stationarity, parts 1 and 2 without the linear rate, for general $C$ .

Significance

The theorem shows that a plain first-order method, started from any stabilizing gain, never destabilizes the closed loop and decreases the cost monotonically, for output feedback as well as state feedback. For state feedback it converges globally and linearly to the optimal gain. The cost is non-convex, and its domain $\mathcal S$ is open, possibly non-convex and unbounded, so this does not follow from convex optimization theory. It is the continuous-time counterpart of the policy-gradient guarantees of Fazel et al. for discrete-time LQR, and it underlies model-free and data-driven variants of gain tuning.

The result is proved in the paper, but it has not been formalized. The formalization adds three things. It makes the invariance argument (the iterates stay in $\mathcal S_0$ ) explicit, and the paper describes that argument as the non-trivial part. It corrects the statements where the printed text is wrong (see below). It also produces a reusable library of Lyapunov-equation facts. Mathlib has no Lyapunov equation, no LQR cost and no Hurwitz stability theory, and the platform has no continuous-time LQR material. The nearest platform items treat discrete-time Riccati iteration (BertsekasDP.riccati_convergence_stability) and Polyak–Łojasiewicz rates on a whole normed space (ShiOptRates.pl_rate). Neither applies to a function defined only on a non-convex open subset.

Difficulty

The standard descent-lemma argument assumes $f$ is defined and $L$ -smooth on the whole space. Here $f$ is defined only on $\mathcal S$ , and it is not smooth on all of $\mathcal S$ : it blows up at the boundary. A gradient step from a point of $\mathcal S_0$ could in principle jump out of $\mathcal S$ , where the Lyapunov equation has no meaningful solution. The smoothness bound is available only inside $\mathcal S_0$ , so the argument must show that the whole segment from $K_j$ to $K_{j+1}$ stays in $\mathcal S_0$ before the descent inequality can be used on it. That requires coercivity, compactness of $\mathcal S_0$ and an exit-time argument. For the linear rate, gradient domination has to be established on $\mathcal S_0$ with constants controlled by $f(K_0)$ , and passing from function values to distances to $K_*$ needs that minimizer's structure. Gradient domination fails for output feedback (the paper's Example 3.4 has two disconnected components with different minima), so the linear rate is stated only for $C=I$ .

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every element of the complex spectrum has negative real part. $X(K)$ , $Y(K)$ are "the unique solution of the Lyapunov equation, $0$ if there is none or several"; this junk value is never used, because every statement evaluates $f$ and $\nabla f$ only at gains proved or assumed to lie in $\mathcal S$ . The iterates' membership in $\mathcal S_0$ is a conclusion of the goal, never a hypothesis; assuming it would delete the theorem's content. $\nabla f$ is defined by the formula (3.3), and Lemma 3.11 is the theorem that it is the gradient. $\|\cdot\|_F$ is $\sqrt{\sum M_{ij}^2}$ , $\|\cdot\|$ is the spectral (operator) norm, and $\lambda_1,\lambda_n$ are the minimum and maximum eigenvalue of a symmetric matrix. State feedback is the instance $r=n$ , $C=1$ . In (4.6) the Frobenius norm replaces the paper's spectral norm, which is equivalent because $c$ is existential. The minimum over $0\le j\le k$ requires $k\ge1$ .

Deviations from the printed text, each recorded in the item's Formalization Note:

The smoothness constant. The explicit $L$ of (3.8) is false as printed (for $n=m=1$ , $A=0$ , $B=100$ , $Q=100$ , $R=10^{-3}$ , $\Sigma=0.1$ , $K_0=10^{-6}$ , one has $f''(K_0)=2L$ ). The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$ , which is the paper's definition of $L$ -smoothness (§3.6) and all that its proof uses. Theorem 3.15 enters only as "some such $L>0$ exists".
Lemma C.1. It is stated with $\lambda_1^2(\Sigma)$ in the denominator, as its proof concludes and as (3.11) requires.
Lemma A.5. It is stated for $A^\top X+XA+Q=0$ ; the printed $-Q$ admits no positive definite solution.
The gain space. $\mathcal S\subseteq\mathbb R^{m\times r}$ , where p. 3 prints $\mathbb R^{m\times n}$ .

Not stated: Theorem 4.3 and Algorithm 4.1, Lemma 3.6, Lemmas 3.12–3.14, Corollary 3.16 and the explicit constant (3.8). Welcome contributions include a Lyapunov-equation library (existence, uniqueness, integral representation, positivity), continuity of the spectrum, and the exit-time argument, which is reusable for any descent method on a sublevel set of an open domain.

Selected references

I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59(5), 2021; preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
W. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15(1), 1970. https://doi.org/10.1109/TAC.1970.1099363
H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5, 1960.

16 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Optimization·Captain: mikedeng1

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 1: The Augmentation Bound for Shortest Augmenting PathsResearch Paper

Why the number of augmentations matters

The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It is a basic model in operations research, underlies bipartite matching, transportation and scheduling problems, and is a standard subroutine inside larger combinatorial algorithms.

The classical method for it is the labeling method of Ford and Fulkerson: starting from some flow, repeatedly find an augmenting path from source to sink along which flow can be increased, push as much as the path allows, and stop when no such path exists. When all capacities are integers, each augmentation raises the flow value by at least one, so the method terminates, but the number of augmentations can be as large as the final flow value, which is exponential in the size of the input. Edmonds and Karp give a four-node example in which the method alternates between two paths and needs $2M$ augmentations for capacities $M$ (Edmonds–Karp 1972, p. 250). With irrational capacities, Ford and Fulkerson showed that the method need not terminate at all and may converge to a non-maximum flow.

Timeline.

1956 — Ford and Fulkerson introduce the labeling method and the max-flow min-cut theorem (Ford–Fulkerson 1956).
1962 — Flows in Networks records the non-termination example for incommensurable capacities.
1970 — Dinic independently obtains a polynomial bound using layered (shortest-path) networks (Dinic 1970).
1972 — Edmonds and Karp prove that choosing each augmenting path with fewest arcs bounds the number of augmentations by $\tfrac14(n^3-n)$ , for arbitrary real capacities (Edmonds–Karp 1972, Theorem 1).

Setting

A network $N$ consists of a finite set of $n$ nodes, a source $s$ and a sink $t \ne s$ , and a set of arcs, which are ordered pairs $(u,v)$ with $u \ne v$ ; there is at most one arc from a node to another. One arc is the special return arc $(t,s)$ , and $A$ denotes the set of all other arcs. Each $(u,v) \in A$ has a real capacity $c(u,v) > 0$ .

A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and with inflow equal to outflow at every node, the return arc included. The value $f(t,s)$ is the amount sent from $s$ to $t$ ; a maximum flow maximizes it.

Given a flow $f$ , the residual network $N^f$ has the same nodes, and $(u,v)$ is an arc of $N^f$ when $(u,v) \in A$ with $c(u,v) - f(u,v) > 0$ , or $(v,u) \in A$ with $f(v,u) > 0$ . An augmenting path is a sequence of distinct nodes $s = u_1, \dots, u_p = t$ whose consecutive pairs are arcs of $N^f$ . Each step carries a number $\varepsilon_i > 0$ (residual capacity forward, flow backward, or their sum when both $(u_i,u_{i+1})$ and $(u_{i+1},u_i)$ lie in $A$ ); $\varepsilon = \min_i \varepsilon_i$ , and a step with $\varepsilon_i = \varepsilon$ is a bottleneck arc. Augmenting raises $f(t,s)$ by $\varepsilon$ and shifts the flow on the path's arcs accordingly, using the paper's own rule for opposite arcs, which never exceeds a capacity.

A run with fewest-arc augmentations is a sequence $f^0, \dots, f^K$ where $f^0$ is a flow and each $f^{k+1}$ arises from $f^k$ by augmenting along a path $P^k$ with fewest arcs. The distance $\delta^k(u,v)$ is the least number of arcs of a directed path from $u$ to $v$ in $N^k = N^{f^k}$ , or $\infty$ .

Formalization targets

Goal — Theorem 1

For every network on $n$ nodes and every run of length $K$ with fewest-arc augmentations,

K \le \tfrac14\,(n^3 - n),

and if no augmenting path exists relative to $f^K$ , then $f^K$ is a maximum flow. The capacities are arbitrary positive reals, and the initial flow is arbitrary.

Milestones

§1.1: augmentation yields a flow with value $f(t,s) + \varepsilon$ , $\varepsilon > 0$ .
§1.1: a flow is maximum if and only if it admits no augmenting path.
Proposition 1: a bottleneck arc of $P^k$ is not an arc of $N^{k+1}$ .
Proposition 2: $(u,v) \in N^{k+1}$ implies $(u,v) \in N^k$ or $(v,u) \in P^k$ .
Lemma 1: if $(u,v)$ is a bottleneck arc at steps $k < m$ , then $(v,u) \in P^l$ for some $k < l < m$ .
Proposition 3: $\delta^k(s,u) \le \delta^{k+1}(s,u)$ and $\delta^k(u,t) \le \delta^{k+1}(u,t)$ .
Lemma 2: if $k < l$ , $(u,v) \in P^k$ and $(v,u) \in P^l$ , then $\delta^l(s,t) \ge \delta^k(s,t) + 2$ .
Proof of Theorem 1: each pair $\{u,v\}$ occurs as a bottleneck at most $\tfrac12(n+1)$ times.

Significance

The theorem shows that one simple rule for choosing augmenting paths, which a breadth-first labeling process implements, makes the number of augmentations depend on the number of nodes alone, independent of the capacities and of their arithmetic nature. It removes both pathologies of the unrestricted labeling method at once: exponential running time for integer capacities, and non-termination for irrational ones. Together with Dinic's work it is the starting point of the theory of strongly polynomial network-flow algorithms, and the distance-monotonicity argument (Proposition 3, Lemma 2) reappears in blocking-flow and push-relabel analyses.

The result is classical and fully proved in the paper. What this mission adds is a machine-checked version of the complete argument in the paper's own model: return arc, arbitrary real capacities, and the paper's augmentation rule for pairs of opposite arcs, which differs from Ford and Fulkerson's (footnote 1, p. 249). The platform has a max-flow min-cut theorem and an integer termination theorem for the Ford–Fulkerson method in the Bertsimas–Tsitsiklis model (Introduction to Linear Optimization, missions IX–X), but no bound on the number of augmentations. No machine-checked proof of Theorem 1 in Lean is known to exist.

Difficulty

The obvious argument, "each augmentation saturates a bottleneck arc, which then disappears", fails because a saturated arc can reappear after later augmentations push flow back along its reverse. Counting augmentations therefore requires control over how often the same pair of nodes can supply a bottleneck again, and no property of a single augmentation provides it; the bound has to come from an invariant of the whole run that holds for real capacities, where no integrality argument is available. A second trap is that the converse direction of milestone 2 (no augmenting path implies maximality) is a max-flow min-cut statement that the paper cites without proof; it must be proved in the paper's model with the return arc.

Formalization scope

Nodes form a finite type V with decidable equality and $n$ = Fintype.card V counts all nodes, $s$ and $t$ included. The arc set A is a Finset (V × V) with no loops and without $(t,s)$ ; capacities are real and positive on A. A flow is a function V → V → ℝ whose values off the arcs are ignored. A maximum flow is the predicate " $f(t,s) \ge g(t,s)$ for every flow $g$ ", never a real supremum. Paths are lists of distinct nodes with every consecutive pair a residual arc, so the return arc is never on a path. Distances take values in ℕ∞. A run is a pair of ℕ-indexed sequences constrained on indices up to $K$ . The explicit constants are stated as printed: $4K \le n^3 - n$ in ℕ (the truncated subtraction is harmless since $n \le n^3$ ) and $2\,b(u,v) \le n + 1$ for the per-pair count.

Case (b) of the paper's definition of augmenting paths is misprinted (its hypothesis repeats that of Case (c)); the formalization uses the reading $(u_i,u_{i+1}) \notin A$ , $(u_{i+1},u_i) \in A$ , which the paper's own description of $N^f$ on p. 251 confirms.

A trivializing formalization is ruled out: a run predicate that no sequence satisfies (for instance, one that requires paths through the return arc, or computes $\varepsilon = 0$ ) would make the bound vacuous; the step predicate here is satisfiable, and a concrete four-node run has been checked. Replacing the paper's augmentation rule by "increase the forward arc by $\varepsilon$ " would also change the theorem, because that rule can violate capacities.

A complete development needs basic facts on simple paths in finite digraphs, shortest paths and their subpaths, and a max-flow min-cut theorem in the paper's model. These are reusable well beyond this mission, as are the network, residual-network and augmentation definitions. Contributions proving any milestone independently are welcome.

Selected references

J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
L. R. Ford, D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
E. A. Dinic, Algorithm for Solution of a Problem of Maximum Flow in a Network with Power Estimation, Soviet Mathematics Doklady 11:1277–1280, 1970. https://www.cs.bgu.ac.il/~dinitz/D70.pdf
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 7 (network flow problems; formalized on the platform in missions IX–X).

24 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Optimization·Captain: mikedeng1

A Three-Operator Splitting Scheme and its Optimization Applications 2: The Objective Rate of the Weighted Ergodic IterateResearch Paper

Motivation

Many problems in signal processing, statistics and machine learning minimise a sum of three convex terms: a smooth data-fit term and two nonsmooth regularisers or constraints, each of which is easy to handle on its own (through its proximal map) but not in combination. Examples are constrained sparse regression, matrix completion with a nuclear-norm penalty and box constraints, and support-vector machines with a norm penalty. Davis and Yin (Set-Valued Var. Anal. 25 (2017)) introduced a three-operator splitting scheme that evaluates each proximal map and the gradient of the smooth term once per iteration and reduces to Douglas–Rachford splitting (Lions and Mercier 1979) and forward–backward splitting as special cases. Section 3 of that paper gives the objective-error rates of the scheme on convex problems. This mission formalizes those rates for general convex problems.

Setting

Let $H$ be a real Hilbert space. The problem is

\min_{x \in H}\; f(x) + g(x) + h(x), \tag{3.1}

where $f, g : H \to (-\infty, +\infty]$ are closed, proper, convex functions (lower semicontinuous, never $-\infty$ , finite somewhere, with convex epigraph) and $h : H \to \mathbb R$ is convex and differentiable with $\beta^{-1}$ -Lipschitz gradient $\nabla h$ , $\beta > 0$ .

For $\gamma > 0$ the proximal map $\operatorname{prox}_{\gamma f}(x)$ is the unique minimiser of $y \mapsto f(y) + \frac{1}{2\gamma}\|y - x\|^2$ . Algorithm 2 of the paper picks $z^0 \in H$ and $\gamma \in (0, 2\beta)$ and iterates, with relaxation $\lambda_k \equiv 1$ ,

x^k_g = \operatorname{prox}_{\gamma g}(z^k),\qquad x^k_f = \operatorname{prox}_{\gamma f}\big(2x^k_g - z^k - \gamma\nabla h(x^k_g)\big),\qquad z^{k+1} = z^k + x^k_f - x^k_g .

Equivalently $z^{k+1} = T z^k$ for the three-operator map

T z = \operatorname{prox}_{\gamma f}\big(2\operatorname{prox}_{\gamma g}(z) - z - \gamma\nabla h(\operatorname{prox}_{\gamma g}(z))\big) + z - \operatorname{prox}_{\gamma g}(z).

If $z^*$ is a fixed point of $T$ , then $x^* = \operatorname{prox}_{\gamma g}(z^*)$ minimises (3.1). The weighted ergodic iterate is

\bar x^k_g = \frac{2}{(k+1)(k+2)}\sum_{i=0}^{k} (i+1)\,x^i_g ,

and $\bar x^k_f$ is defined the same way from $(x^i_f)$ .

Formalization targets

Goal: Theorem 3.2 (p. 840)

Let $z^*$ be a fixed point of $T$ , $x^* = \operatorname{prox}_{\gamma g}(z^*)$ , and suppose $f$ is $L$ -Lipschitz continuous on the closed ball $B\big(x^*, (1+\gamma/\beta)\|z^0 - z^*\|\big)$ . Then there is a constant $C$ , independent of $k$ , with

(f+g+h)(\bar x^k_g) - (f+g+h)(x^*) \le \frac{C}{k+1}\qquad (k \ge 0).

The goal asserts the order $O(1/(k+1))$ and leaves the constant free, so it is not invalidated by a sharper constant.

Milestones

Corollary 2.1, Part 1 (p. 834): $\|z^j - z^*\|$ is nonincreasing.
Lemma 3.1 (p. 838): $x^j_f, x^j_g \in B\big(x^*, (1+\gamma/\beta)\|z^0 - z^*\|\big)$ for all $j$ .
Eq. (3.2) (p. 839): for all $k \ge 0$ ,

2\gamma\big(f(x^k_f) + g(x^k_g) + h(x^k_g) - (f+g+h)(x^*)\big) \le \|z^k - x^*\|^2 - \|z^{k+1} - x^*\|^2 - \|z^k - z^{k+1}\|^2 + 2\gamma\langle z^k - z^{k+1}, \nabla h(x^k_g)\rangle .

Theorem 3.1 (p. 838): the last-iterate rate $(f+g+h)(x^k_g) - (f+g+h)(x^*) = o\big(1/\sqrt{k+1}\big)$ .
Eq. (2.7) (p. 836), with $\lambda_k \equiv 1$ : for $\gamma/(2\beta) < \varepsilon < 1$ ,

\sum_{i=k}^\infty \|\nabla h(x^i_g) - \nabla h(x^*)\|^2 \le \frac{\|z^k - z^*\|^2}{\gamma(2\beta - \gamma/\varepsilon)} .

Eq. (3.4) (p. 840): $\|\bar x^k_f - \bar x^k_g\| \le 5\|z^0 - z^*\|/(k+1)$ .

Significance

The result. Theorem 3.1 gives the last iterate an objective error of $o(1/\sqrt{k+1})$ . Theorem 3.2 shows that averaging with linearly increasing weights improves this to $O(1/(k+1))$ , the rate of the standard uniform ergodic average, while putting more weight on recent iterates. The paper notes that this matters when the iterates $x^k_g$ are sparse vectors or low-rank matrices and the average should stay close to them. The rates hold under a local Lipschitz condition on one of the two nonsmooth terms only, so $g$ may be the indicator function of a constraint set. They therefore cover the constrained applications of Section 4 of the paper.

Formalizing it. The results are proved in the paper. No machine-checked version of this scheme or its rates exists on the platform or, as far as is known, in Mathlib. A formalization produces a checked proof in an arbitrary real Hilbert space with extended-valued $f, g$ . It also produces infrastructure that Mathlib lacks: proximal maps characterised by minimisation, the prox-subgradient inclusion, Fejér monotonicity of an averaged-operator iteration, and a weighted Jensen inequality for extended-valued convex functions. All of these can be reused by other splitting and proximal-gradient missions. The formalization also checks the constants: the last display of the published proof of Theorem 3.2 drops a factor $2\gamma$ in front of the Lipschitz term, and the printed ball in both theorems is centred at $0$ where the proof needs $x^*$ .

Difficulty

The obvious argument sums the one-step inequality (3.2). That controls the objective at the two different points $x^k_f$ and $x^k_g$ , and only $f(x^k_f)$ appears, never $f(x^k_g)$ . Moving from one point to the other needs the Lipschitz hypothesis on $f$ , and so it needs every iterate, and every weighted average, to stay in the ball on which that hypothesis holds. For the weighted average there is a further obstacle: the cross term $2\gamma\langle z^k - z^{k+1}, \nabla h(x^k_g)\rangle$ does not telescope under the weights $(i+1)$ . Controlling it requires the summability of the gradient differences (2.7), which is inherited from the averagedness analysis of Section 2 and not from convexity alone. Uniform averaging with the same argument does not give the weighted statement, and the weights must not be replaced.

Formalization scope

$H$ is an arbitrary real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not $\mathbb R^n$ .
$f, g : H \to$ EReal. They are proper (never $\bot$ , somewhere $\ne \top$ ), lower semicontinuous, and have a convex epigraph in $H \times \mathbb R$ . $h : H \to \mathbb R$ is convex and differentiable, and Mathlib's gradient h is $\beta^{-1}$ -Lipschitz.
Proximal maps are not constructed. A map $P$ is assumed to minimise $f(y) + \|y - x\|^2/(2\gamma)$ for every $x$ . Such a map exists and is unique for closed proper convex $f$ , so nothing is lost.
Algorithm 2 is fixed with $\lambda_k \equiv 1$ , the only case of Theorems 3.1 and 3.2. Iterates are indexed from $0$ . The fixed point $z^*$ is a hypothesis, $T z^* = z^*$ , and $x^* := \operatorname{prox}_{\gamma g}(z^*)$ . Assumption 1 of the paper follows from this and is not assumed separately.
Ball centre. The theorems print $B(0, (1+\gamma/\beta)\|z^0 - z^*\|)$ . The proofs use Lemma 3.1, whose ball is centred at $x^*$ , so the ball here is centred at $x^*$ . " $f$ is $L$ -Lipschitz on the ball" is stated as: $f$ is finite on the ball, and its real-valued restriction is $L$ -Lipschitz there.
O(·) and o(·). $O(1/(k+1))$ is $\exists C \in \mathbb R,\ \forall k,\ (f+g+h)(\bar x^k_g) \le (f+g+h)(x^*) + C/(k+1)$ , with $C$ chosen after all data. $o(1/\sqrt{k+1})$ is $\sqrt{k+1}\,\big((f+g+h)(x^k_g) - (f+g+h)(x^*)\big) \to 0$ , together with finiteness of the objective values as part of the conclusion. No explicit constant from the proof is stated, because the published constant drops a factor.
Corollary 2.1 Part 1 and Eq. (2.7) are stated for Algorithm 2 with $\lambda_k \equiv 1$ , $\gamma \in (0, 2\beta)$ and $\varepsilon \in (\gamma/(2\beta), 1)$ . As printed, Corollary 2.1's condition on $\tau_k$ excludes $\lambda_k \equiv 1$ , but Section 3 uses Part 1 in exactly this case. Summability in (2.7) is part of the conclusion.
Trivialization ruled out. Objective values are extended reals, and the goal compares them without subtraction. The value $(f+g+h)(x^*)$ is proved finite as part of the conclusion. So the goal cannot hold through $\infty - \infty$ or through an infinite right-hand side.

Welcome contributions: the prox–subgradient inclusion for EReal-valued convex functions, averagedness and Fejér monotonicity of $T$ (the companion mission on Section 2 treats the general operator case), a weighted Jensen inequality in EReal, and proofs of the milestones in the listed order.

Selected references

D. Davis and W. Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued and Variational Analysis 25 (2017) 829–858. https://doi.org/10.1007/s11228-017-0421-z
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
P.-L. Lions and B. Mercier, Splitting Algorithms for the Sum of Two Nonlinear Operators, SIAM J. Numer. Anal. 16 (1979) 964–979. https://doi.org/10.1137/0716071
D. Davis and W. Yin, Convergence Rate Analysis of Several Splitting Schemes, in Splitting Methods in Communication, Imaging, Science, and Engineering, Springer, 2016. https://doi.org/10.1007/978-3-319-41589-5_4

9 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Optimization·Captain: mikedeng1

A Three-Operator Splitting Scheme and its Optimization Applications 1: Weak and Strong Convergence of the Three-Operator Splitting IterationResearch Paper

Motivation

Many problems in convex optimization, variational inequalities and signal processing reduce to a monotone inclusion: find a point $x$ at which the sum of several monotone operators contains $0$ . When the sum has two terms, the classical operator-splitting methods (Douglas–Rachford, forward–backward, forward–backward–forward) solve it by iterating a fixed-point map that uses each operator separately, through its resolvent or through a forward (explicit) step. Problems with three terms, for instance a smooth loss plus two nonsmooth regularizers or constraints, are common in practice, and before 2015 no fixed-point map was known that handled three operators one at a time without a product-space reformulation.

Davis and Yin (Set-Valued Var. Anal. 25 (2017) 829–858; preprint arXiv:1504.01032) introduced such a map, now called Davis–Yin three-operator splitting. It contains Douglas–Rachford splitting ( $C = 0$ ) and forward–backward splitting ( $B = 0$ ) as special cases, and it has become a standard building block of first-order methods for composite optimization. This mission formalizes Section 2 of the paper: the fixed-point encoding, the averagedness of the map, and the weak and strong convergence of the resulting iteration.

Setting

Let $H$ be a real Hilbert space. A set-valued operator $A : H \to 2^H$ is monotone if $\langle x - y, u - v\rangle \ge 0$ for all $u \in Ax$ , $v \in Ay$ , and maximal monotone if its graph is not properly contained in the graph of another monotone operator. Its domain is $\operatorname{dom}(A) = \{x : Ax \ne \emptyset\}$ and the zero set of an operator $M$ is $\operatorname{zer}(M) = \{x : 0 \in Mx\}$ . A single-valued $C : H \to H$ is $\beta$ -cocoercive ( $\beta > 0$ ) if $\beta\|Cx - Cy\|^2 \le \langle Cx - Cy, x - y\rangle$ for all $x, y$ .

Problem (1.1) is: given maximal monotone $A, B$ and $\beta$ -cocoercive $C$ , find

x \in H \quad\text{with}\quad 0 \in Ax + Bx + Cx .

For $\gamma > 0$ the resolvent $J_{\gamma A} = (I + \gamma A)^{-1}$ is the map with $x \in J_{\gamma A}x + \gamma A(J_{\gamma A}x)$ . The Davis–Yin operator (Eq. (1.2)) is

T := J_{\gamma A} \circ (2J_{\gamma B} - I - \gamma C \circ J_{\gamma B}) + I - J_{\gamma B}.

Algorithm 1 starts from $z^0 \in H$ and, for relaxation parameters $\lambda_k > 0$ , iterates

x_B^k = J_{\gamma B}(z^k),\qquad x_A^k = J_{\gamma A}(2x_B^k - z^k - \gamma Cx_B^k),\qquad z^{k+1} = z^k + \lambda_k(x_A^k - x_B^k),

so that $z^{k+1} = (1 - \lambda_k)z^k + \lambda_k Tz^k$ . A sequence converges weakly, $u_k \rightharpoonup u$ , if $\langle u_k, y\rangle \to \langle u, y\rangle$ for every $y \in H$ .

Formalization targets

Goal: Theorem 2.1 (Main convergence theorem)

Fix $\varepsilon \in (0,1)$ , $\gamma \in (0, 2\beta\varepsilon)$ , $\alpha = 1/(2-\varepsilon)$ and $\lambda_k \in (0, 1/\alpha)$ with $\sum_k \tau_k = \infty$ , where $\tau_k = \lambda_k(1-\lambda_k) + \lambda_k(1-\alpha)/\alpha$ , and $\inf_k \lambda_k > 0$ . If $\operatorname{Fix} T \ne \emptyset$ , there is $z^* \in \operatorname{Fix} T$ with $z^k \rightharpoonup z^*$ and

Cx_B^k \to Cx^* \ \ (\forall x^* \in \operatorname{zer}(A+B+C)),\qquad x_B^k \rightharpoonup J_{\gamma B}(z^*) \in \operatorname{zer}(A+B+C),\qquad x_A^k \rightharpoonup J_{\gamma B}(z^*),

and if $A$ or $B$ is uniformly monotone on every nonempty bounded subset of its domain, or $C$ is demiregular at every zero of $A + B + C$ , then $x_B^k$ and $x_A^k$ converge strongly to a common point of $\operatorname{zer}(A + B + C)$ .

Milestones

In the order the proof uses them: Lemma 2.1 (the identities for one application of $T$ ), Lemma 2.2 ( $\operatorname{zer}(A+B+C) = J_{\gamma B}(\operatorname{Fix} T)$ ), Lemma 2.3 (inequality (2.1)), Proposition 2.1 ( $T$ is $2\beta/(4\beta-\gamma)$ -averaged, inequality (2.2)), Remark 2.1 (the strengthened inequality (2.4)), Corollary 2.1 Parts 1–3 (Fejér monotonicity, vanishing residual, weak convergence of $z^k$ ), Corollary 2.1 Part 4 (the residual rates $\|Tz^k - z^k\|^2 \le \|z^0 - z^*\|^2/(\underline\tau(k+1))$ and $o(1/(k+1))$ ), and Eqs. (2.6)–(2.7) (the per-step descent inequality and its summed form).

Significance

Theorem 2.1 is the basic convergence guarantee for three-operator splitting: it certifies that the computable sequences $x_B^k$ , $x_A^k$ , not only the auxiliary sequence $z^k$ , approach a solution of (1.1). In infinite dimensions this is the delicate part: for Douglas–Rachford splitting ( $C = 0$ ) weak convergence of the shadow sequence $J_{\gamma B}(z^k)$ was only established by Svaiter in 2011. The result underlies the convergence of the many algorithms obtained from it by specialization (Douglas–Rachford, forward–backward, and the three-block methods of Section 4 of the paper), and the averagedness coefficient of Proposition 2.1 reduces, for $B = 0$ , to the best known one for forward–backward splitting.

All statements of this mission are proved in the paper, partly by appeal to Bauschke and Combettes' monograph (Krasnosel'skiĭ–Mann convergence, the demiclosedness of maximal monotone graphs). None of them has a machine-checked proof: Mathlib has no maximal monotone operators, resolvents, averaged maps or Krasnosel'skiĭ–Mann theorem. The mission therefore produces both a formal proof of the Davis–Yin theorem and a first body of monotone-operator theory in Lean.

Difficulty

The fixed-point part is standard once $T$ is known to be averaged: Krasnosel'skiĭ–Mann theory and Opial's argument give $z^k \rightharpoonup z^*$ . The obstacle is transferring this to $x_B^k = J_{\gamma B}(z^k)$ . Resolvents are nonexpansive but not weakly continuous, so $z^k \rightharpoonup z^*$ does not imply $J_{\gamma B}(z^k) \rightharpoonup J_{\gamma B}(z^*)$ ; the naive argument fails at exactly this step. Identifying the weak cluster points of $x_B^k$ requires a closedness property of sums of maximal monotone operators under mixed weak and strong convergence, fed by the strong convergence of $Cx_B^k$ , which in turn needs the extra term of (2.4) that (2.2) discards. Strong convergence in Part 2 needs yet another argument for each of the three alternative hypotheses.

Formalization scope

$H$ is an arbitrary real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); a finite-dimensional space would identify weak and strong convergence and change the theorems.
Operators $A, B$ are H → Set H; $C$ is single-valued H → H. The resolvents are not constructed: $J_A, J_B$ are maps satisfying the resolvent inclusion $\gamma^{-1}(x - Jx) \in A(Jx)$ , which for maximal monotone operators determines them uniquely and exists by Minty's theorem.
Weak convergence is $\langle u_k, y\rangle \to \langle u, y\rangle$ for every $y$ ; strong convergence is norm convergence. Iterates are indexed from $0$ .
The printed hypothesis $\alpha = 1/(2-\varepsilon) < 2\beta/(4\beta-\gamma)$ of Corollary 2.1 and Theorem 2.1 contradicts $\gamma < 2\beta\varepsilon$ (it is a typo for $>$ ) and is not assumed. The printed $\tau_k = (1-\lambda_k/\alpha)\lambda_k/\alpha$ is replaced by the $\tau_k$ of the proof (p. 836), a weaker hypothesis.
Uniform monotonicity uses a nondecreasing $\varphi : [0,\infty) \to [0,+\infty]$ with $\varphi(0) = 0$ that vanishes only at $0$ , as the proof requires; with $\varphi \equiv 0$ allowed, Part 2(a) would be false.
The O-constant of Corollary 2.1 Part 4 is explicit, $\|z^0 - z^*\|^2/\underline\tau$ , and the little- $o$ is stated as $(k+1)\|Tz^k - z^k\|^2 \to 0$ . Eq. (2.7) is stated with a uniform lower bound $\underline\lambda \le \lambda_i$ in place of the printed $\lambda_k$ , with summability part of the conclusion.
A formalization with $T$ an arbitrary averaged map, with resolvents replaced by arbitrary nonexpansive maps, or with the contradictory comparison of $\alpha$ kept as a hypothesis would make the theorem vacuous or different; all three are ruled out.

A complete development needs the basic theory of monotone operators (monotonicity of resolvents' graphs, firm nonexpansiveness of resolvents, weak-to-strong closedness of maximal monotone graphs), Krasnosel'skiĭ–Mann iteration with Opial's lemma, and weak sequential compactness of bounded sets in Hilbert space. All of this is reusable far beyond this mission, and contributions of any of these pieces as separate theorems are welcome.

Selected references

D. Davis and W. Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued and Variational Analysis 25 (2017) 829–858. https://doi.org/10.1007/s11228-017-0421-z
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
B. F. Svaiter, On weak convergence of the Douglas–Rachford method, SIAM J. Control Optim. 49 (2011) 280–287. https://doi.org/10.1137/100788100
D. Davis and W. Yin, Convergence rate analysis of several splitting schemes, in: Splitting Methods in Communication, Imaging, Science, and Engineering, Springer, 2016. https://arxiv.org/abs/1406.4834

14 thms2 active usersReviewed

Analysis Optimization·Captain: mikedeng1

Generalized Gradients and Applications I: The Generalized Gradient of a Max FunctionResearch Paper

Motivation

Many objective functions in optimization are pointwise maxima: the worst case of a loss over an uncertainty set, the value of a minimax problem as a function of the outer variable, a penalty $\max_i g_i(x)$ for a system of constraints, or the largest eigenvalue of a symmetric matrix. Such a function

f(x)=\max\{g(x,u):u\in U\}

is typically not differentiable even when every piece $g(\cdot,u)$ is smooth, because the maximizing $u$ jumps. Descent methods, optimality conditions and sensitivity analysis for these problems all need a substitute for the gradient of $f$ and a formula for its directional derivatives.

Danskin's theorem (Danskin 1966) answers this when $\nabla_x g(x,u)$ exists and is continuous in $(x,u)$ and $U$ is compact: $f$ has one-sided directional derivatives $f'(x;v)=\max\{\nabla_x g(x,u)\cdot v:u\in M(x)\}$ , where $M(x)$ is the set of maximizers. Convex analysis gives the analogue when each $g(\cdot,u)$ is convex (Rockafellar 1970). In Generalized gradients and applications (Clarke 1975) Frank Clarke introduced the generalized gradient of a locally Lipschitz function and proved, as his first application, a single theorem, Theorem (2.1), that contains both cases. The generalized gradient became the standard object of nonsmooth analysis (Clarke 1983), and Theorem (2.1) is the prototype of every "subdifferential of a max function" rule used in minimax optimization.

Setting

Work in $\mathbb R^n$ with the Euclidean norm $|\cdot|$ and inner product $\zeta\cdot v$ . A function $f:\mathbb R^n\to\mathbb R$ is locally Lipschitz if for every bounded set $B$ there is $K$ with $|f(x_1)-f(x_2)|\le K|x_1-x_2|$ for $x_1,x_2\in B$ . By Rademacher's theorem such $f$ is differentiable almost everywhere.

The generalized gradient $\partial f(x)$ (Definition (1.1)) is the convex hull of all limits $\lim_i\nabla f(x+h_i)$ , where $h_i\to0$ , $f$ is differentiable at each $x+h_i$ , and the gradients converge.
The generalized directional derivative (Definition (1.3)) is

f^\circ(x;v)=\limsup_{h\to0,\ \delta\downarrow0}\frac{f(x+h+\delta v)-f(x+h)}{\delta},

and the one-sided directional derivative is $f'(x;v)=\lim_{\delta\downarrow0}[f(x+\delta v)-f(x)]/\delta$ when the limit exists.

A multifunction $\Phi$ into subsets of $\mathbb R^n$ is upper semicontinuous if $x_i\to x$ , $v_i\to v$ and $v_i\in\Phi(x_i)$ imply $v\in\Phi(x)$ .

For the max function, $U$ is a nonempty sequentially compact topological space and $g:\mathbb R^n\times U\to\mathbb R$ . Write $\partial_xg(x,u)$ , $g^\circ_x(x,u;v)$ , $g'_x(x,u;v)$ for the objects above applied to $y\mapsto g(y,u)$ at $x$ . Let $f(x)=\max_{u\in U}g(x,u)$ and $M(x)=\{u\in U:g(x,u)=f(x)\}$ . The hypotheses of Theorem (2.1) are:

(a) $g$ is upper semicontinuous in $(x,u)$ ;
(b) $g$ is locally Lipschitz in $x$ uniformly in $u$ : for each bounded $B$ one constant $K$ serves for every $u\in U$ ;
(c) for all $x,u,v$ , $g'_x(x,u;v)$ exists and equals $g^\circ_x(x,u;v)$ ;
(d) $(x,u)\mapsto\partial_xg(x,u)$ is upper semicontinuous on $\mathbb R^n\times U$ .

Formalization targets

Goal: Theorem (2.1)

Under (a)–(d):

$f$ is locally Lipschitz;
$f'(x;v)$ exists for all $x,v$ ;
$f'(x;v)=f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial_xg(x,u),\ u\in M(x)\}$ ;
for every $x$ ,

\partial f(x)=\operatorname{co}\{\partial_xg(x,u):u\in M(x)\}.

Milestones

Proposition (1.4): $f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial f(x)\}$ for locally Lipschitz $f$ .
Corollary (1.10): if $\zeta\cdot v\le\limsup_{\delta\downarrow0}[f(x+\delta v)-f(x)]/\delta$ for all $v$ , then $\zeta\in\partial f(x)$ .
Theorem (2.1)(1): under (a), (b), $f$ is locally Lipschitz.
(2.2): $\operatorname{co}\{\partial_xg(x,u):u\in M(x)\}\subseteq\partial f(x)$ .
(2.3): if $f$ is differentiable at $\bar x$ and $u\in M(\bar x)$ , then $\partial_xg(\bar x,u)=\{\nabla f(\bar x)\}$ .
Theorem (2.1)(4): the equality above.

Significance

The result. Theorem (2.1) computes the directional derivatives and the generalized gradient of a max function from those of its active pieces. It yields Danskin's theorem when $\nabla_xg$ is continuous, and the convex max rule when each $g(\cdot,u)$ is convex, and it applies to nonsmooth, nonconvex families satisfying (c), a property later called regularity (Clarke 1983, §2.3). In the same paper it is applied to the distance function $d_E(x)=\min_{e\in E}|x-e|$ to compute $\partial d_E$ (Proposition (2.4), Corollary (2.5)), which then drives the characterization of flow-invariant sets in §4. Proposition (1.4) and Corollary (1.10), which the theorem rests on, are the duality between $\partial f$ and $f^\circ$ used throughout nonsmooth optimization: Clarke stationarity, bundle methods and subgradient methods for weakly convex functions all state their results against them.

Formalizing it. The results are classical and proved; none of them, to the platform's knowledge, has a machine-checked proof. Mathlib has Rademacher's theorem, gradients and convex hulls, but no Clarke generalized gradient. This mission builds the first layer of nonsmooth analysis: the definitions of $\partial f$ , $f^\circ$ , $f'$ and upper semicontinuity of multifunctions, the support-function duality, and the max rule.

Difficulty

The obvious approach reads $\partial f(x)$ off a single active piece. It fails because the active set $M(x+h)$ changes as $h\to0$ , may be infinite, and need not converge; $f$ can be differentiable at points where no individual piece is known to be. Hypothesis (c) cannot be dropped: for $U$ a single point and $g(x,u)=-|x|$ on $\mathbb R$ , $f=g$ has $f'(0;v)=-|v|$ while $f^\circ(0;v)=|v|$ , so conclusion (3) fails. Limits of maximizers exist only through the sequential compactness of $U$ together with (a), and limits of gradients only through the joint closed-graph condition (d) in $(x,u)$ ; continuity in $x$ for each fixed $u$ is not enough. Proposition (1.4), on which everything rests, is itself a measure-theoretic statement: it relates the upper limit of difference quotients over all nearby base points to gradients that exist only almost everywhere.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\zeta\cdot v$ is inner ℝ ζ v, $\nabla f$ is Mathlib's gradient, and " $\nabla f(x)$ exists" is DifferentiableAt ℝ f x.
"Locally Lipschitz" is the paper's bounded-set form, LipschitzOnBounded. Hypothesis (b) is ∀ B bounded, ∃ K, ∀ u, LipschitzOnWith K (g · u) B: the constant is uniform in $u$ .
$\partial f(x)$ is the plain convex hull (no closure) of limits of gradients taken only at differentiability points; without that restriction $0$ would belong to every $\partial f(x)$ , because gradient is $0$ where $f$ is not differentiable.
$f^\circ$ is Filter.limsup in $\mathbb R$ along $\mathcal N(0)\times\mathcal N_{>}(0)$ ; this is a junk value for non-Lipschitz $f$ , so every statement using $f^\circ$ assumes the Lipschitz hypothesis. The one-sided derivative is a Tendsto along $\mathcal N_{>}(0)$ .
"max" in conclusions is IsGreatest, which asserts attainment. The max function is ⨆ u, g x u; $U$ is nonempty ([Nonempty U]) and SeqCompactSpace, and (a) is Mathlib's UpperSemicontinuous on $\mathbb R^n\times U$ . The paper uses $U\ne\emptyset$ implicitly; with $U=\emptyset$ conclusion (4) would be false.
(d) is the sequential closed-graph property in $(x,u)$ jointly, not Mathlib's UpperHemicontinuous.
A formalization in which $\partial f$ contains junk gradients, $f^\circ$ is a limsup without the Lipschitz hypothesis, or "max" is sSup without attainment would make the statements trivial or false; these are ruled out as above.

Contributions welcome: proofs of the milestones, in particular Proposition (1.4) and Corollary (1.10), which are reusable for every later nonsmooth-analysis mission; lemmas that $\partial f(x)$ is nonempty and compact; the equivalence of LipschitzOnBounded with Mathlib's LocallyLipschitz.

Selected references

F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975), 247–262. https://doi.org/10.1090/s0002-9947-1975-0367131-6
J. M. Danskin, The theory of max-min, with applications, SIAM J. Appl. Math. 14 (1966), 641–664. https://doi.org/10.1137/0114053
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; SIAM Classics reprint 1990. https://doi.org/10.1137/1.9781611971309

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Optimization·Captain: mikedeng1

On Minimizing a Convex Function Subject to Linear Inequalities II: Optimality Conditions for the Sum of the Largest Linear FormsResearch Paper

Motivation

In 1955 E. M. L. Beale showed how Dantzig's simplex method, which was built for linear objectives, can be carried over to certain nonlinear convex objectives that are minimized subject to linear inequalities (Beale 1955). Section 4 of that paper treats one such objective: the sum of the $t$ largest of a set of $g$ linear forms. Beale's motivation comes from the theory of games: "if the enemy has to choose $t$ out of a set of $g$ possible actions, and $L_f$ represents his average gain through using the $f$ th", then the defender wants to minimize the sum of the $t$ largest $L_f$ .

The same objective can be written as a linear program. One introduces a bound $u$ and requires every sum of $t$ forms to be at most $u$ . That formulation has $\binom{g}{t}$ constraints, which is unwieldy once $t>1$ and $g$ is large. Beale's alternative works with the nonlinear objective directly, and he needs a test that tells him when the current basic solution is already optimal. This mission formalizes that test, Theorem 1 of the paper.

The objective reappears in later work under other names: the sum of the $k$ largest components of a vector, the "top- $k$ sum", and $k$ times the conditional value-at-risk of an empirical distribution. Beale's paper is an early source for its optimality conditions.

Setting

There are real variables $z_l$ , indexed by $l$ in a finite set (possibly empty), and $u_1,\dots,u_s$ . Two linear forms in these variables are given,

A=A_0+\sum_l A_l z_l+\sum_{f=1}^{s}\varphi_f u_f,\qquad L_0=c_{00}+\sum_l c_{0l} z_l+\sum_{f=1}^{s}\theta_f u_f,

together with $s$ further forms

L_f=L_0-u_f\qquad(f=1,\dots,s).

For an integer $\tau\ge0$ the objective is

C=A+\bigl(\text{sum of the }\tau\text{ largest of }L_0,L_1,\dots,L_s\bigr).

The sum of the $\tau$ largest of $s+1$ numbers is the largest total of any $\tau$ of them. Ties do not make it ambiguous.

The feasible region is fixed by a set $F$ of indices. The variables $z_l$ with $l\in F$ and all the $u_f$ are free, and every other $z_l$ is restricted to $z_l\ge0$ . At the origin $z=0$ , $u=0$ all $s+1$ forms are equal to $c_{00}$ , so the origin is where $C$ fails to be differentiable. In Beale's algorithm the origin is the current basic solution: the $u_f$ measure how far the "borderline" forms sit from a chosen critical form, and $A$ collects the forms that are certainly among the largest.

Write $a_l=A_l+\tau c_{0l}$ and $w_f=\varphi_f+\tau\theta_f$ .

Formalization targets

Goal: Theorem 1 (a), p. 179

For $\tau\le s$ , $C$ is minimized over the feasible region when all the $z_l$ and $u_f$ vanish if and only if

\begin{aligned} &a_l\ge0\ \text{for all } l, \qquad a_l=0\ \text{for all } l\in F,\\ &0\le w_f\le1\ \text{for all } f,\qquad \tau-1\le\sum_{f=1}^{s}w_f\le\tau . \end{aligned}\tag{4.5}

"Minimized" means a global minimum: $C(0,0)\le C(z,u)$ at every feasible point.

Milestones

Convexity (p. 179). $C$ is a convex function of $(z,u)$ for $\tau\le s+1$ .
Descent rules (second half of Theorem 1 (a), p. 179). When a condition of (4.5) fails, a stated move of one variable, or of all $u_f$ together, lowers $C$ below $C(0,0)$ for every small enough step. There are six moves: $z_l\uparrow$ if $a_l<0$ ; $z_l\downarrow$ if $a_l>0$ and $l\in F$ ; $u_f\uparrow$ if $w_f<0$ ; $u_f\downarrow$ if $w_f>1$ ; all $u_f\uparrow$ if $\sum w_f<\tau-1$ ; all $u_f\downarrow$ if $\sum w_f>\tau$ .
The rearrangement identity (proof of Theorem 1 (a), p. 180). If $1\le\tau\le s$ , $u'_1\le\dots\le u'_s$ and $u'_\tau\le0$ , then

C=A_0+\tau c_{00}+\sum_l a_l z'_l+\sum_{f=1}^{\tau}(w_f-1)(u'_f-u'_\tau)+\sum_{f=\tau+1}^{s}w_f(u'_f-u'_\tau)+\Bigl\{\sum_{f=1}^{s}w_f-\tau\Bigr\}u'_\tau .

Theorem 1 (b) (p. 180). For $\tau=s+1$ , the origin is a minimum if and only if (4.5) holds and $w_f=1$ for every $f$ . Otherwise some value of $u_f$ with the sign opposite to $w_f-1$ lowers $C$ .

Significance

Theorem 1 is the optimality test of Beale's simplex method for the sum-of-largest objective. The algorithm on pp. 178–179 changes nonbasic variables one at a time. When no single change is profitable it applies Theorem 1: either (4.5) holds and the current solution is optimal, or one of the six descent rules names the variable to change next. The test is exact even though the objective is not differentiable at the current point. It is a closed-form description of the subdifferential of a top- $\tau$ sum at a point where all the forms tie. The theorem is also the base case of the multi-group generalization that Beale mentions on p. 181.

The paper proves Theorem 1 by hand. To our knowledge neither the theorem nor the rearrangement identity behind it has been formalized in any proof assistant. The mission produces:

a checked statement and proof of the test, including the degenerate cases $\tau=0$ and $s=0$ , which the paper does not discuss separately;
the boundary case $\tau=s+1$ ;
a reusable Lean definition of the sum of the $\tau$ largest entries of a finite real family, with its convexity.

Difficulty

Necessity, the "only if" direction, is the part the paper calls obvious: each descent rule changes $C$ linearly for small steps. Two features still have to be handled explicitly. The step must be small only in rule-dependent ways, and the ordering of the forms changes along the moves of rules 4 and 6.

Sufficiency is where the work lies. The naive argument, "the directional derivative in every coordinate direction is non-negative, so the origin is a minimum", fails because $C$ is not differentiable at the origin. Nonnegative derivatives along the coordinate axes do not control mixed directions in which several $u_f$ move by different amounts, which reorders the forms. Which $\tau$ forms are the largest then depends on the point, and the paper settles the configurations in which $L_0$ is among the $\tau$ largest by an informal appeal to the "essential symmetry" between $L_0$ and the other forms. A formal proof cannot leave that appeal informal: the forms are parametrised relative to $L_0$ (each $L_f$ is $L_0-u_f$ ), so the symmetry is a change of variables that has to be written down and shown to preserve (4.5).

Formalization scope

Data. The variables are z : Fin r → ℝ (any r, including $0$ ) and u : Fin s → ℝ. The paper's $u_f$ for $f=1,\dots,s$ is Lean's u f for $f=0,\dots,s-1$ . The coefficients $(A_0,A_l,\varphi_f,c_{00},c_{0l},\theta_f)$ form a structure Forms r s.
Forms. The family $L_0,\dots,L_s$ is Fin (s+1) → ℝ, with index $0$ for $L_0$ and index f.succ for $L_0-u_f$ . The free set $F$ is a Finset (Fin r), and $\tau$ is a natural number cast to $\mathbb R$ wherever it multiplies a coefficient.
Sum of the largest. sumLargest τ v is the maximum over $\tau$ -element subsets $S$ of $\sum_{i\in S}v_i$ (Finset.sup' over powersetCard). It is the junk $0$ for $\tau$ larger than the number of entries, a case no statement uses.
Minimality. "Minimized when all variables vanish" is the global statement $C(0,0)\le C(z,u)$ for all $(z,u)$ with $z_l\ge0$ for $l\notin F$ . It is not a local minimum, and the sign constraints on restricted $z_l$ are kept: they are why the first condition of (4.5) is an inequality.
Descent. " $C$ can be decreased by moving $x$ from zero" is a strict decrease for all step sizes in some interval $(0,\varepsilon)$ , with every other variable at zero.
No trivialization. The goal is an equivalence with no hypothesis beyond $\tau\le s$ . Neither direction can be satisfied vacuously, and the cases $\tau=0$ and $s=0$ are included, as on the page.
Added hypotheses. The rearrangement milestone assumes $\tau\ge1$ , because the paper's $u'_\tau$ does not exist at $\tau=0$ . Its second line uses $c_{0l}$ where the page misprints $c_l$ .

Needed infrastructure:

basic lemmas on sumLargest: its value at a constant family, at a family sorted by a monotone shift, and under adding a common constant;
the change of variables behind the paper's symmetry between $L_0$ and the other forms.

These lemmas are reusable for any top- $k$ -sum or empirical-CVaR objective. Contributions are welcome at any level: lemmas about sumLargest, any of the milestones, or an alternative sufficiency proof through convexity and one-sided directional derivatives.

Not in scope: the pivoting rules (4.2)–(4.4), the degeneracy discussion on pp. 180–181, and the multi-group generalization, which the paper says is "cumbersome to state" and does not state.

Selected references

E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2), 173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
G. B. Dantzig, A. Orden and P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2), 183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
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

7 thms2 active usersReviewed

Completed

Partial Differential Equations Probability Stochastic Systems·Captain: mikedeng1

Revenue Management of a Make-to-Stock Queue: Exponential Stationary Density under Normal Reflection (Proposition 2)Research Paper

Motivation

A make-to-stock manufacturer who also sells on a spot market must decide, at every moment, whether to keep producing and whether to accept or reject incoming orders at the prevailing price. Caldentey and Wein (Revenue Management of a Make-to-Stock Queue, Operations Research 54(5), 2006) study this problem in heavy traffic. The limit is a two-dimensional singular control problem for a diffusion: the inventory level and the logarithm of the price move jointly as a correlated Brownian motion, and the controls push the inventory only when it reaches one of two free boundaries. The optimal boundaries are characterized by an elliptic free-boundary problem that the authors could not solve in closed form.

The paper's way forward is an approximation: change the direction of reflection on the boundary so that the stationary distribution of the controlled process becomes an explicit exponential. Proposition 2 states that exponential form, and it turns the free-boundary problem into a calculus-of-variations problem for the two boundary curves. Explicit stationary densities of reflected diffusions in two dimensions are rare; the classical condition for an exponential stationary density of a reflected Brownian motion, and the characterization of the stationary law by a basic adjoint relation, are due to Harrison and Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15, 1987, the reference the paper cites. This mission formalizes the analytic core of Proposition 2: the exponential density satisfies that relation for the reflection field the proposition singles out.

Setting

Points of the plane are $(x,y)$ , with $x$ the inventory level and $y$ the logarithm of the price. The limiting process $(\mathcal X,\mathcal Y)$ has drift $(\theta,0)$ and covariance matrix

\Sigma=\begin{pmatrix}\sigma^2&\sigma\delta\varrho\\ \sigma\delta\varrho&\delta^2\end{pmatrix},\qquad \sigma>0,\ \delta>0,\ -1<\varrho<1,

so its generator is

\Gamma=\theta\frac{\partial}{\partial x}+\frac{\sigma^2}{2}\frac{\partial^2}{\partial x^2}+\sigma\delta\varrho\frac{\partial^2}{\partial x\,\partial y}+\frac{\delta^2}{2}\frac{\partial^2}{\partial y^2}.

Two curves bound the region where the process lives: the rejection boundary $x=\eta(y)$ (below it, orders are rejected) and the idleness boundary $x=\xi(y)$ (above it, production stops). For $y_{\min}<y_{\max}$ the region is

\Omega=\{(x,y):\ y_{\min}<y<y_{\max},\ \eta(y)<x<\xi(y)\},

and its boundary splits into four pieces: $x=\eta(y)$ , $x=\xi(y)$ , $y=y_{\min}$ , $y=y_{\max}$ . Write $\vec n$ for the inward unit normal on $\partial\Omega$ and $dl$ for arc length. A reflection field $\vec v$ on $\partial\Omega$ gives the direction in which the process is pushed back into $\Omega$ . The basic adjoint relation (BAR) of the paper, equation (43), is

\int_\Omega \Gamma f\,\pi_\Omega\,ds+\frac12\int_{\partial\Omega}\vec v\cdot\nabla f\,\pi_\Omega\,dl=0\quad\text{for all test functions } f,

and the paper cites Harrison and Williams for the fact that the stationary distribution $\pi_\Omega$ of the reflected process satisfies it. Proposition 2 introduces the eigen-decomposition $\Sigma=V'EV$ ( $V$ a rotation whose rows are eigenvectors, $E$ diagonal), the whitening map $T=E^{-1/2}V$ and $\Omega^*=T(\Omega)$ , and assumes that $T\vec v$ is normal to $\partial\Omega^*$ . The exponents are

m_x=\frac{2\theta}{\sigma^2(1-\varrho^2)},\qquad m_y=\frac{-2\varrho\theta}{\sigma\delta(1-\varrho^2)}.\tag{47}

Formalization targets

Goal: the exponential density satisfies the BAR under conormal reflection

For $\eta,\xi$ continuously differentiable with $\eta<\xi$ on $[y_{\min},y_{\max}]$ , $\pi(x,y)=e^{m_xx+m_yy}$ , and every $C^2$ function $f$ on $\mathbb R^2$ ,

\int_\Omega \Gamma f\;\pi\,ds+\frac12\int_{\partial\Omega}(\Sigma\vec n)\cdot\nabla f\;\pi\,dl=0 .

The boundary integral is written out on the four pieces, with $\vec n\,dl$ equal to $(1,-\eta'(y))\,dy$ , $(-1,\xi'(y))\,dy$ , $(0,1)\,dx$ and $(0,-1)\,dx$ respectively. The normalizing constant is left out because the relation is linear in $\pi$ .

Milestones

The interior equation: $\Gamma^*\pi=-\theta\pi_x+\frac{\sigma^2}{2}\pi_{xx}+\sigma\delta\varrho\,\pi_{xy}+\frac{\delta^2}{2}\pi_{yy}=0$ everywhere.
The zero-flux identity: $\frac12\Sigma\nabla\pi=(\theta,0)\,\pi$ everywhere.
The meaning of the hypothesis: with $T=E^{-1/2}V$ , $(Tv)\cdot(Tw)=v\cdot\Sigma^{-1}w$ , and for $n\neq0$ , $Tv$ is orthogonal to $T$ of every vector orthogonal to $n$ exactly when $v$ is a multiple of $\Sigma n$ .
The normalizing constant: $\pi$ is integrable on $\Omega$ and a unique $K_\Omega>0$ makes $K_\Omega\pi$ integrate to one.

Significance

For the operations model, Proposition 2 is what makes the problem computable. Once the stationary density is explicit, the long-run average cost of any pair of boundary curves is an explicit integral, and optimizing over $(\eta,\xi)$ becomes a variational problem with Euler–Lagrange equations; the paper's proposed policy and its numerical comparisons all rest on it.

For formalization, the mission produces a machine-checked version of a statement whose proof the paper does not contain (it is in an online companion) and whose hypothesis is stated only in words. The formal statements fix exactly which reflection field makes the claim true, which the prose leaves ambiguous. None of the statements has, to our knowledge, a machine-checked proof anywhere; the result itself is classical in spirit (an integration by parts on a planar region), but no divergence theorem on a region between two graphs with an anisotropic operator is currently available as a ready-made statement.

Difficulty

The interior equation and the zero-flux identity are finite computations with the exponential. The difficulty is the goal: it is an integration-by-parts identity on a curved planar region with an anisotropic second-order operator. The obvious first step, "apply Green's identity", presupposes a divergence theorem on a region bounded by two graphs $x=\eta(y)$ , $x=\xi(y)$ and two horizontal segments, with the boundary integral written in the parametrization of each piece and the orientation of every normal tracked. Mathlib has the divergence theorem on rectangular boxes, not on such regions, and the moving limits $\eta(y)$ , $\xi(y)$ are exactly where the terms in $\eta'$ and $\xi'$ of the boundary integral come from.

The second trap is the reflection field. The page describes the modification as substituting the inward unit normal $\vec n$ for $\vec v$ ; with $\vec v=\vec n$ the identity is false as soon as $\Sigma$ is not a multiple of the identity (on a random instance the residual is of order one). Only the conormal field $\Sigma\vec n$ , which is what the hypothesis of Proposition 2 selects, gives a true statement.

Formalization scope

Everything lives in the namespace MakeToStockRM.ExpDensity. The plane is ℝ × ℝ with the inventory first; partial derivatives are Fréchet derivatives applied to (1, 0) and (0, 1), and the mixed partial is $\partial_x(\partial_y f)$ . Parameters satisfy $\sigma>0$ , $\delta>0$ , $|\varrho|<1$ ; $\theta$ is any real number, and $\theta=0$ (then $\pi\equiv1$ ) is allowed.

This is the analytic, pinned-down content of Proposition 2. The identification "the BAR characterizes the stationary law of the reflected diffusion" (Harrison–Williams 1987) is out of scope: Mathlib has no reflected Brownian motion. Relative to the page, the formalization commits to the following:

The reflection field is $\vec v=\Sigma\vec n$ with $\vec n$ the inward unit normal and $dl$ arc length. The hypothesis " $T\vec v$ is normal to $\partial\Omega^*$ " fixes only the direction of $\vec v$ (milestone 3); the length $\Sigma\vec n$ is the one for which the BAR holds. The page's phrase "substituting the inward unit normal $\vec n$ for $\vec v$ " is inconsistent with the proposition's own hypothesis and is not followed.
The boundary curves are $C^1$ on $\mathbb R$ with $\eta<\xi$ on $[y_{\min},y_{\max}]$ , and $y_{\min}<y_{\max}$ , so $\Omega$ is a nonempty bounded region; the paper assumes this implicitly.
Test functions are all $C^2$ functions on $\mathbb R^2$ , which are bounded with bounded derivatives on the closure of $\Omega$ (the paper's "twice continuous and bounded").
The constant $K_\Omega$ is dropped from the goal and treated in milestone 4.

The goal quantifies over every $C^2$ test function; restricting to functions supported inside $\Omega$ would delete the boundary term and reduce the goal to milestone 1, and that trivialization is ruled out. The second half of Proposition 2 ("(45)–(46) is equivalent to (48)–(49)"), Proposition 1, the heavy-traffic limit, the HJB equation and the proposed policy are not formalized: their normalizations or proofs are only in the online companion.

A complete development needs a divergence theorem on regions between two $C^1$ graphs, which is reusable for any planar PDE statement on such regions. Contributions of that lemma, and of the four milestones, are welcome.

Selected references

R. Caldentey, L. M. Wein, Revenue Management of a Make-to-Stock Queue, Operations Research 54(5):859–875, 2006. https://doi.org/10.1287/opre.1060.0289
J. M. Harrison, R. J. Williams, Multidimensional reflected Brownian motions having exponential stationary distributions, Annals of Probability 15(1):115–137, 1987. https://doi.org/10.1214/aop/1176992259
F. John, Partial Differential Equations, 4th ed., Springer, 1982. https://doi.org/10.1007/978-1-4684-9333-7

10 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Exit Problems for Spectrally Negative Lévy Processes and Applications to (Canadized) Russian Options I: Joint Laplace Transform of the Exit Time and Exit Position of the Reflected ProcessResearch Paper

Motivation

A spectrally negative Lévy process is a process with stationary independent increments whose jumps are all downward: Brownian motion with drift plus a compound Poisson or infinite-activity stream of negative jumps. It is the standard model for a risk reserve that earns premiums continuously and pays claims in lumps, for a storage level or a queue workload seen in reverse, and, in mathematical finance, for a log-price that can crash but not jump up. Exit problems (when and where such a process first leaves an interval) are the basic quantities in ruin theory, in dividend and barrier problems, and in the pricing of path-dependent options.

The reflected process $Y=\overline X-X$ , the distance of $X$ below its running maximum, is the drawdown of $X$ . Its first passage above a level $k$ is the time at which a drawdown of size $k$ first occurs. Avram, Kyprianou and Pistorius (AKP 2004) computed the joint Laplace transform of this passage time and of the overshoot $Y_{\tau_k}$ in closed form, in terms of the scale functions of $X$ . This is the first of three missions on that paper. The two others use this identity for the perpetual Russian option and its Canadized version.

Timeline. Bertoin gave the upward two-sided exit identity for spectrally negative Lévy processes in terms of scale functions (Bertoin 1996, Theorem VII.8) and the downward one (Bertoin 1997, Corollary 1). Avram, Kyprianou and Pistorius (2004) obtained the joint transform of $(\tau_k,Y_{\tau_k})$ for every spectrally negative Lévy process of unbounded variation, or of bounded variation with absolutely continuous Lévy measure.

Setting

Let $X=\{X_t,t\ge0\}$ be a spectrally negative Lévy process on $(\Omega,\mathcal F,\mathbb P)$ : it starts at $0$ , has independent and stationary increments, càdlàg paths, no positive jumps, and paths that are not monotone. Its Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$ , and " $\psi(v)<\infty$ " means that $e^{vX_1}$ is integrable. For such $v$ , the tilted exponent is $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$ .

The paper assumes throughout that $X$ has unbounded variation, or has bounded variation and a Lévy measure $\Lambda$ with $\Lambda(dx)\ll dx$ .

For $q\ge0$ , $\Phi(q)$ is the largest root of $\psi(\theta)=q$ . The $q$ -scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$ , is continuous on $(0,\infty)$ , and satisfies

\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=\frac1{\psi(\theta)-q},\qquad\theta>\Phi(q).

For $q<0$ it is defined by the series $W^{(q)}=\sum_{k\ge0}q^kW^{\star(k+1)}$ , where $W=W^{(0)}$ and $\star$ is convolution on $[0,\infty)$ . Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$ . The functions $W_v^{(p)}$ and $Z_v^{(p)}$ are the same objects built from $\psi_v$ instead of $\psi$ .

Under $\mathbb P_{s,x}$ the process starts at $x$ with a prior maximum $s\ge x$ . Its running maximum is $\overline X_t=\max\{s,\sup_{0\le u\le t}X_u\}$ , and the reflected process is $Y=\overline X-X$ , which starts at $z=s-x$ . For $k>0$ ,

\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}.

Formalization targets

Goal: Theorem 1

For $u\ge0$ and $v$ with $\psi(v)<\infty$ , with $z=s-x\ge0$ and $p=u-\psi(v)$ ,

\mathbb E_{s,x}\big[e^{-u\tau_k-vY_{\tau_k}}\big]=e^{-vz}\left(Z_v^{(p)}(k-z)-W_v^{(p)}(k-z)\frac{pW_v^{(p)}(k)+vZ_v^{(p)}(k)}{W_v^{(p)\prime}(k)+vW_v^{(p)}(k)}\right).

Here $v$ may be negative, so $p$ may be negative, which is where the series extension of $W$ enters.

Milestones

(2) $\mathbb E[e^{\theta X_t}]=e^{t\psi(\theta)}$ .
Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$ for every real $u$ .
Proposition 1, (9) and (10): for $x\in(a,b)$ , the Laplace transforms of the exit time of $X$ from $(a,b)$ on the events of exit above and exit below.
(13): the splitting of the goal's expectation at the first zero of $Y$ .
(14)–(15) and (16): the two expectations of (13).
(22): the value $C$ of the functional for $Y$ started at $0$ .
Remark 6, (23): the stopped process whose martingale property is equivalent to Theorem 1.

Items (13)–(22) are stated under the proof's restriction $u\ge\psi(v)\vee0$ . The goal is not.

Significance

The identity gives, for every spectrally negative Lévy process, the law of the first drawdown of size $k$ and of its overshoot. With $v=0$ it is the Laplace transform of the drawdown time. With $u=0$ it is the transform of the overshoot. The paper uses it, through its Corollary 1, to solve the perpetual Russian option and the Canadized Russian option in closed form. Identities of this form, written in scale functions, are the standard tool for drawdown and reflected-process problems for spectrally negative Lévy processes.

The theorem is proved. As far as the platform and Mathlib show, none of it is formalized: Mathlib has independent increments and cumulant generating functions but no Lévy process, no scale function and no excursion theory. This mission produces a formal statement of the paper's model and of the exit identities. A complete development would also give Mathlib its first fluctuation-theory results for Lévy processes.

Difficulty

The natural first idea is to treat $Y$ like $X$ and read off its exit from $[0,k)$ from the two-sided exit identities of Proposition 1. This works only until $Y$ first returns to $0$ . Up to that time $Y$ is a copy of $-X$ . After it, $Y$ is reflected at $0$ , it is not a Lévy process, and no two-sided exit problem of $X$ describes it. The whole content of the theorem is the constant $C$ of (13), the value of the functional for $Y$ started at $0$ , where the reflection acts at every instant. A second difficulty is the range of $(u,v)$ . For $v<0$ the integrand $e^{-vY_{\tau_k}}$ is unbounded, because $Y$ can jump far above $k$ . Its finiteness is part of the claim. So is the passage from the region $u\ge\psi(v)\vee0$ , where every scale function in (12) comes from Definition 2, to all $u\ge0$ , where $p$ can be negative.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a real process with $X_0=0$ . $\mathbb P_x$ is encoded by the path $x+X$ , and $\mathbb P_{s,x}$ by that path together with the prior maximum $s$ . Random times take values in WithTop ℝ≥0, with $\infty$ as "never". The functional $e^{-u\tau_k-vY_{\tau_k}}$ and discount factors $e^{-qT}$ are set to $0$ where the time is infinite. Every stated expectation carries its integrability as part of the conclusion.

Readings of the paper's informal words:

"Lévy process": the paths start at $0$ , are càdlàg and have no positive jumps for every $\omega$ , not only almost surely.
"We exclude the case that X has monotone paths": the paths are neither almost surely nondecreasing nor almost surely nonincreasing.
"unbounded variation": not of bounded variation. The standing assumption is "bounded variation implies (AC)".
" $\Lambda(dx)\ll dx$ ": for every Lebesgue-null Borel $A$ , almost surely no nonzero jump in $(0,1]$ lands in $A$ . The Lévy measure is not constructed.
" $\psi(v)<\infty$ ": $e^{vX_1}$ is integrable.
"the largest root": the supremum of the nonnegative roots.
"the unique function": a definite description by choice.
"analytic extension": the series (5) for real negative index. Complex indices are out of scope.
" $W'$ ": the derivative at $k>0$ .
"is a martingale" in (23): a martingale for the natural filtration of $X$ .
Misprint: (23) prints $vZ_v^{(q)}(k)$ , and the statement uses $vZ_v^{(p)}(k)$ .

The scale functions are defined from the exponent $\psi$ of the given $X$ . A formalization in which $W$ is an arbitrary function satisfying a Laplace-transform hypothesis is ruled out. So is one in which $W_v^{(p)}$ is defined as $e^{-vx}W^{(p+\psi(v))}(x)$ , which would make Remark 4 a tautology.

Infrastructure a complete development needs: Lévy processes and their Laplace exponent, the strong Markov property at stopping times, existence and regularity of scale functions (via Laplace inversion), and the Esscher change of measure. No statement of the mission mentions excursion theory. Contributions of reusable infrastructure for Lévy processes are welcome.

Selected references

F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
J. Bertoin, Lévy Processes, Cambridge University Press, 1996. https://www.cambridge.org/core/books/levy-processes/
J. Bertoin, Exponential decay and ergodicity of completely asymmetric Lévy processes in a finite interval, Ann. Appl. Probab. 7(1), 156–169, 1997. https://doi.org/10.1214/aoap/1034625254

16 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 3: Optimal Contingent-Pricing Revenue with Myopic Customers and Exponential ValuationsResearch Paper

Motivation

Retailers of seasonal goods (fashion, electronics, holiday items) sell a fixed stock over a short season and routinely cut prices toward its end. A markdown of this kind segments the market over time: customers with high valuations buy early at a premium price, and customers with lower valuations are served later at a discount price. Aviv and Pazgal (MSOM 2008) study how much such two-price schemes are worth when customers arrive over time, differ in their valuations, and may or may not anticipate the discount.

To measure the value of price segmentation, the paper compares every two-price scheme with the best fixed-price policy, a single price held for the whole season. Its benchmark is the case of myopic customers, who never delay a purchase strategically. Proposition 3 of the paper computes this benchmark in closed form in the simplest nontrivial setting: exponentially distributed valuations that do not decline over the season, and unlimited inventory. The resulting formula explains the pattern of the paper's Table 1, where the benefit of segmentation grows with the heterogeneity of valuations and with a late discount time.

Setting

A seller offers a product during the season $[0, H]$ ; throughout this mission $H = 1$ , so time is measured as a fraction of the season. Customers arrive as a Poisson process with rate $\lambda > 0$ . Customer $j$ has a base valuation $V_j$ drawn independently from a distribution $F$ with tail $\bar F(x) = 1 - F(x)$ , and values the product at $V_j e^{-\alpha t}$ at time $t$ , where $\alpha \ge 0$ is the decline factor. The paper reparametrizes it as $\rho = e^{-\alpha H}$ , the fraction of the base valuation left at the end of the season.

In the numerical study, $F$ is a Gamma law with mean $\mu$ and coefficient of variation $c$ (standard deviation over mean): shape $1/c^2$ and rate $1/(\mu c^2)$ . The paper sets $\mu = 1$ . For $c = 1$ this is the exponential law with mean one, $\bar F(x) = e^{-x}$ for $x \ge 0$ .

A contingent two-price policy posts the premium price $p_1$ on $[0, T)$ , where $0 < T \le 1$ is fixed, and a discount price $p_2 \le p_1$ from time $T$ on. A myopic customer arriving at $t < T$ buys at $p_1$ if his valuation is at least $p_1$ ; otherwise he waits and buys at $T$ if his valuation is then at least $p_2$ . Customers arriving at or after $T$ buy if their valuation is at least $p_2$ . The numbers of customers in these groups are Poisson with means

\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1 e^{\alpha t})\,dt, \quad \Lambda_W(p_1,p_2) = \lambda\int_0^T \big[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1e^{\alpha t})\big]dt, \quad \Lambda_L(p_2) = \lambda\int_T^H \bar F(p_2e^{\alpha t})\,dt .

With unlimited inventory, the expected revenue of the policy is

R_{C/N}(p_1, p_2) = p_1\Lambda_I(p_1) + p_2\big(\Lambda_W(p_1,p_2) + \Lambda_L(p_2)\big),

and the expected revenue of a single price $p$ is $R_F(p) = p\,\lambda\int_0^H \bar F(p e^{\alpha t})\,dt$ (Eq. (9) of the paper). The optimal values are $\pi^*_{C/N} = \max_{p_2 \le p_1} R_{C/N}(p_1,p_2)$ and $\pi^*_F = \max_p R_F(p)$ .

Formalization targets

Goal: Proposition 3

Suppose $c = 1$ , $\rho = 1$ and $Q/\lambda \to \infty$ (unlimited inventory), with $\mu = 1$ and $H = 1$ . Then

\pi^*_{C/N} = (\lambda e^{-1})\cdot e^{T/e} = \pi^*_F \cdot e^{T/e}.

Both maxima are attained. The goal states the two optimal values; it does not fix the optimal prices.

Milestones from the paper's proof

The reduced problem: for $0 \le p_2 \le p_1$ , $R_{C/N}(p_1,p_2) = p_2\cdot\lambda e^{-p_2} + (p_1-p_2)\cdot\lambda T e^{-p_1}$ .
Its solution: over $p_2 \le p_1$ the maximum is $\lambda e^{-1+T/e}$ , attained exactly at $p_1^* = 2 - T/e \ge 1$ , $p_2^* = p_1^* - 1 \le 1$ .
The fixed-price optimum (a supporting item of the goal, stated in the proof on pp. 358–359): $p^* = \mu = 1$ is the unique optimal single price and $\pi^*_F = \lambda e^{-1}$ .

Significance

Proposition 3 gives the relative benefit of contingent pricing over a single price, $e^{T/e} - 1$ , as a function of the discount time alone. It increases in $T$ and is largest at $T = 1$ , where it equals $e^{1/e} - 1 \approx 44.46\%$ . This is the paper's analytic anchor for its numerical findings: segmentation is most valuable when valuations are heterogeneous and customers are carried to the discount at little cost, and a late discount exposes more customers to the premium price. Under strategic customers the same quantity serves as an upper bound on the benefit of segmentation (§6.1 of the paper).

The result is proved in the paper, in a short appendix argument that states the reduced problem and its solution without the calculus. No machine-checked version exists. Formalizing it produces a reusable Lean encoding of the paper's segment rates $\Lambda_I, \Lambda_W, \Lambda_L$ as integrals of a valuation tail, a Gamma valuation law through Mathlib's gammaMeasure, and a complete verification that the integral model reduces to the two-variable problem and that the stated prices are its unique maximizer.

Difficulty

The obvious route is to write the revenue in closed form and set the gradient to zero. Two steps of that route are not automatic. First, the reduction requires evaluating the three integrals with the piecewise tail of the exponential law, including the $\min$ inside $\Lambda_W$ , and the reduced formula is valid only for nonnegative prices; negative prices must be handled separately in the model itself, where the tail equals one. Second, the reduced objective $p_2\lambda e^{-p_2} + (p_1-p_2)\lambda T e^{-p_1}$ is not concave on the region $p_2 \le p_1$ , so a stationary point is not automatically a global maximizer, and the boundary $p_2 = p_1$ and unbounded directions have to be ruled out. Uniqueness of the maximizer, which the paper asserts, fails at $T = 0$ and needs $T > 0$ .

Formalization scope

All declarations sit in the namespace SeasonalPricing.MyopicExp. Time, prices and rates are real numbers. The season is $[0, 1]$ with $0 < T \le 1$ and $\lambda > 0$ . Integrals are interval integrals. The valuation tail is gammaValuationTail μ c x = 1 - cdf (gammaMeasure (1/c^2) (1/(μ c^2))) x, used at $\mu = c = 1$ . The hypothesis $\rho = 1$ is decayRatio α 1 = 1 with $\alpha \ge 0$ .

Readings of the paper's informal words:

" $Q/\lambda \to \infty$ " is read as unlimited inventory: the truncated Poisson mean $N(q,\Lambda)$ of §4.2 is replaced by $\Lambda$ and stock-outs never occur. This is what the proof computes, what p. 348 writes as $Q = \infty$ , and what §7.1 calls inventory that is "practically unlimited". A limit of finite-inventory optimal revenues is not stated.
"max" is an attained maximum (IsGreatest), not a supremum.
The optimum is taken over all real prices with $p_2 \le p_1$ , as printed; the paper never restricts signs, and negative prices are never optimal in the model.
The seller's discount at $T$ is a best response to $p_1$ in the paper ( $R(q \mid p_1)$ , p. 349). With unlimited inventory it does not depend on the realized sales, and the nested maximum equals the joint maximum over $(p_1, p_2)$ , which is what the goal states.
"The solution … is" (milestone 2) and "the optimal single price is given by $p^* = \mu = 1$ " (the fixed-price item) are read as unique maximizers.

The Gamma density printed on p. 349 has the exponent $1/(sc^2-1)$ , a misprint for $1/c^2 - 1$ ; at $c = 1$ the exponent is $0$ either way.

A trivializing formalization would state the goal on the reduced two-variable function, dropping the model: the goal here is about $R_{C/N}$ built from $\Lambda_I, \Lambda_W, \Lambda_L$ and the Gamma tail, and about $R_F$ built from Eq. (9). The platform's BuyingToBundle.monopolyRevenue (definition monopoly_pricing) is a related object, $\sup_p p\,\nu([p,\infty))$ ; with $\rho = 1$ and $H = 1$ , $\pi^*_F$ equals $\lambda$ times it for the exponential law, but it is a supremum without arrivals or time and is not reused.

Contributions welcome: closed forms of the segment rates for the exponential tail, a general lemma that negative prices are dominated, and the two-variable maximization.

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Optimization Probability·Captain: mikedeng1

Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers 1: Threshold Purchasing Policies under Contingent PricingResearch Paper

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark the remaining stock down later. When customers anticipate the markdown, some of them who would buy at the premium price instead wait, trading a lower price against the risk that the item sells out and against the decline of their own valuation over the season. How forward-looking ("strategic") customers respond to a markdown policy is the first question any model of such pricing has to answer, because the seller's optimal prices depend on it.

Aviv and Pazgal (MSOM 2008) model a seller with a fixed inventory, Poisson arrivals of customers with heterogeneous, exponentially declining valuations, and two pricing regimes: contingent pricing, where the discount depends on the inventory left at the markdown time, and announced fixed discounts. The first step of their analysis of contingent pricing is Theorem 1: whatever the other customers do, a customer's best response is a threshold rule on his current valuation, with a threshold that rises as the markdown approaches. Their numerical study of equilibria and of the value of price commitment (§§4.2–7) is built on this reduction.

Setting

A seller holds $Q$ units over a season $[0, H]$ split at a fixed time $T$ with $0 < T \le H$ . On $[0, T)$ the premium price $p_1$ applies. At time $T$ the seller observes the remaining inventory $Q_T \in \{0, 1, \dots, Q\}$ and charges the discount menu price $p_2(Q_T)$ , where $p_2(q) \le p_1$ for $q = 1, \dots, Q$ . Customer $j$ has a base valuation $V_j$ and valuation $V_j(t) = V_j e^{-\alpha t}$ at time $t$ , with a common decline factor $\alpha \ge 0$ .

A customer arriving at $t < T$ either buys immediately at $p_1$ or waits until $T$ , when he requests a unit if the discounted price leaves him a nonnegative surplus. Waiting is uncertain in two ways: the remaining inventory $Q_T$ is random, and when fewer units remain than customers request them, units are rationed at random. A belief is a probability mass function $\pi$ of $Q_T$ on $\{0, \dots, Q\}$ together with allocation probabilities $a(q) = \Pr\{\mathcal A \mid Q_T = q\} \in [0,1]$ , $a(0) = 0$ , where $\mathcal A$ is the event that the customer is allocated a unit. It is determined by the other customers' strategies, which are arbitrary.

With $\delta = e^{-\alpha(T-t)}$ , the expected surplus of waiting of a customer with current valuation $\psi$ is

W_t(\psi) = \mathrm E_{Q_T}\!\left[\max\{\psi\delta - p_2(Q_T), 0\}\cdot \mathbf 1\{\mathcal A \mid Q_T\}\right] = \sum_{q=0}^{Q}\pi(q)\,a(q)\,\max\{\psi\delta - p_2(q), 0\}.

The paper's purchase rule (p. 344): buy immediately iff the current surplus $V(t) - p_1$ is nonnegative and at least $W_t(V(t))$ .

Formalization targets

Goal: Theorem 1 and Corollary 1

Assume $p_1 \ge 0$ , and $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$ . For every $t \in [0,T)$ the equation

\psi - p_1 = W_t(\psi) \tag{2}

has a unique solution $\psi(t) \ge p_1$ ; a customer arriving at $t$ buys immediately under the purchase rule if and only if $V(t) \ge \psi(t)$ ; and the threshold function $\psi : [0, T) \to [p_1, \infty)$ is nondecreasing in $t$ .

Milestones

The right-hand side of (2) is nonnegative and nondecreasing in $\psi$ , with increments bracketed by $\delta\,\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ at the two endpoints, and this slope is below one.
Equation (2) has a unique solution $\psi \ge p_1$ .

Significance

Theorem 1 reduces a customer's strategy, a function of arrival time and valuation, to one threshold function $\psi$ on $[0, T)$ . The segment sizes $\Lambda_I, \Lambda_S, \Lambda_W, \Lambda_L$ of §4.2, the seller's menu problem (3), the equilibrium iteration (4) and the closed form of Proposition 2 are all written in terms of $\psi$ ; without Theorem 1 none of them is defined. Corollary 1, that the threshold rises toward the markdown, is what the paper calls "useful in our analyses below"; the customer segments of Figure 1 are drawn with it.

The result is proved in the paper, with a short appendix argument. No machine-checked version exists. The mission produces a formal statement and proof of the reduction for an arbitrary belief, which fixes the exact hypotheses under which it holds: the paper's slope bound needs either valuation decline ( $\alpha > 0$ ) or imperfect availability, and the monotonicity of the threshold needs a nonnegative premium price. A formal $W_t$ and threshold are the starting point for formalizing the equilibrium and pricing results of the paper.

Difficulty

The mathematics is one-dimensional. The difficulty is in stating it exactly. $W_t$ is piecewise linear with a kink wherever $\psi\delta$ crosses a menu price, so the paper's derivative is only a one-sided derivative, and the uniqueness argument has to use increments. The paper's bound "slope $< 1$ " is false when $\alpha = 0$ and a unit is allocated with certainty; then (2) has either no finite solution or a half-line of them. The threshold's monotonicity in $t$ rests on $W_t(\psi)$ increasing in $t$ for fixed $\psi$ , which needs $\psi \ge 0$ ; with a negative premium price the threshold can decrease. The naive reading of "optimal to use a threshold" as an abstract fixed-point fact about any monotone function with slope below one discards the model and is not the goal.

Formalization scope

Lean namespace SeasonalPricing.Contingent. Time, prices and valuations are real numbers. The belief is a pair pmf alloc : ℕ → ℝ restricted to {0, …, Q} (IsInventoryBelief), not a random variable on a probability space; only the law of $(Q_T, \mathbf 1\{\mathcal A\})$ enters (2). The menu is p2 : ℕ → ℝ with $p_2(q) \le p_1$ required on $\{1, \dots, Q\}$ only; $p_2(0)$ never matters because $a(0) = 0$ . The belief does not depend on the arrival time, as in Eq. (4) of the paper. waitingSurplus is $W_t$ with $e^{-\alpha(T-t)}$ written Real.exp (-(α * (T - t))); buysNow is the purchase rule, stated on the current valuation $V(t)$ .

Readings of the paper's words:

"the unique solution" of (2): existence and uniqueness of a real $\psi \ge p_1$ (∃!). The paper's " $\psi \in [p_1, \infty]$ " includes $\infty$ only in the case excluded by the added hypothesis.
"it is optimal to base purchasing decisions on a threshold function": the purchase rule of p. 344 holds exactly when $V(t) \ge \psi(t)$ .
"derivative … $< 1$ ": a two-sided bracket on increments of $W_t$ , with right slope $\delta\Pr\{\psi\delta \ge p_2(Q_T), \mathcal A\}$ , below one.
"increasing" (Corollary 1): nondecreasing (MonotoneOn), since $\psi$ is constant on an initial interval whenever no menu price is reachable (p. 347).

Added hypotheses, both named in the statements: $\alpha > 0$ or $\sum_q \pi(q)a(q) < 1$ , the one hypothesis the paper's proof uses without stating it; and $p_1 \ge 0$ , the model's convention that prices are nonnegative. Only the branch $0 \le t < T$ of the threshold $\theta$ is stated: for $t \ge T$ the paper's $\theta(t) = p_2$ is the model's rule for late customers. The belief enters through the explicit sum; a formalization with an unspecified monotone $W$ , or with $\psi(t)$ defined by choice inside a definition, is not the target.

No new library is needed beyond finite sums, max and Real.exp. A lemma on unique roots of $\psi \mapsto \psi - c - f(\psi)$ for $f$ with increments bounded by $k(\psi' - \psi)$ , $k < 1$ , is reusable. Proofs of the milestones and the goal, in any order, are welcome.

Selected references

Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999

5 thms2 active usersReviewed

Algorithmic Game Theory Probability·Captain: mikedeng1

Subjectivity and Correlation in Randomized Strategies II: Subjective Events Let Both Zero-Sum Players Beat the ValueResearch Paper

Motivation

In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value $v$ of the game is the most player 1 can guarantee and the least player 2 can hold him to, and no arrangement between the players can give player 1 more than $v$ and player 2 more than $-v$ at the same time. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) replaces objective coin flips by ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. Sect. 6 of the paper shows that this breaks the zero-sum logic: once the players disagree about the probability of events they can observe, a zero-sum game becomes, in expectation as each player computes it, a game in which both can gain.

The phenomenon is the game-theoretic form of betting between people who disagree: two players with different beliefs can each expect to profit from the same wager. Aumann's proposition identifies exactly what information structure makes such an agreement possible inside a given zero-sum game, and shows by an example that informing only one player of a subjective event is not enough. The same paper introduced correlated equilibrium; the companion mission of this series formalizes its two-person result on subjective mixed equilibria (Proposition 5.1).

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$ . Player $i$ has a utility $u_i:X\to\mathbb R$ ; write $h_i(a)=u_i(g(a))$ for $a\in S$ .

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$ -field $\mathcal B$ of events, a sub- $\sigma$ -field $\mathcal J_i\subseteq\mathcal B$ for each player (the events regarding which $i$ is informed), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$ ). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets lie in $\mathcal J_i$ . For a profile $s$ of strategies, player $i$ 's payoff is computed under his own beliefs:

H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega).

An event $A$ is objective if all $p_i(A)$ coincide, and subjective otherwise. It is $i$ -secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$ -field generated by the $\mathcal J_k$ , $k\ne i$ . It is public if it lies in every $\mathcal J_i$ . A measure is non-atomic on a $\sigma$ -field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub- $\sigma$ -field of $\mathcal B$ on which every $p_j$ is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player $i$ has a $\sigma$ -field $\mathcal R_i$ of $i$ -secret events on which every $p_j$ is non-atomic.

The game is two-person zero-sum if $n=2$ and $u_1(x)+u_2(x)=0$ for all $x\in X$ . Its value $v$ is player 1's payoff $F_1(\sigma)=\sum_{a\in S}h_1(a)\sigma_1(a_1)\sigma_2(a_2)$ at a Nash equilibrium $\sigma$ of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair $(v,-v)$ .

Formalization targets

Goal: Proposition 6.1 (p. 80)

Let $G$ be a two-person zero-sum game with value $v$ , and assume

\exists\,x,y\in X:\ u_1(x)>v>u_1(y),\tag{6.2}

\text{for each } i\in\{1,2\} \text{ there is } B_i\in\mathcal J_i \text{ with } p_1(B_i)\ne p_2(B_i).\tag{6.3}

Then there is a pair $s=(s_1,s_2)$ of strategies with

H_1(s)>v,\qquad H_2(s)>-v.\tag{6.4}

The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.

Milestones

Lemma 7.1 (p. 81): in a roulette $\mathcal R$ there is, for every $\alpha\in[0,1]$ and events $B^1,\dots,B^l$ , an objective event $A\in\mathcal R$ with $p(A)=\alpha$ , independent of each $B^k$ .
Lemma 4.2 (p. 77): for every $i$ , event $B$ and $\alpha\in[0,1]$ there is an objective $i$ -secret event of probability $\alpha$ independent of $B$ .
Lemma 4.4 (p. 77): if there is a public roulette, the same holds with "public" in place of " $i$ -secret".
Remark after Proposition 6.1 (p. 80): the conclusion (6.4) under (6.2) and

\text{there is a public subjective event } B \text{ and there is a public roulette,}\tag{6.5}

a special case of the goal in which the players share both the subjective event and the correlating device.

Significance

The proposition shows that the value of a zero-sum game is a property of objective randomization, not of the game alone. With subjective randomization available to both players, the conflict of a zero-sum game can be resolved by agreement, so the classical prediction (each player receives his security level) is not robust to disagreement about probabilities. The counterexample on p. 81 (the game with matrix rows $(1,1)$ and $(2,0)$ ) shows that hypothesis (6.3) is needed for both players, and the paper notes that in any specific game only one player need use a subjective strategy, though which one depends on the game.

Lemmas 4.2, 4.4 and 7.1 are the model's basic existence results for objective randomization: every probability can be realised by an event that is secret (or public) and independent of finitely many given events. They are used throughout the paper, including in the companion mission.

The paper's proofs are published and accepted; none of these statements has a machine-checked proof. This mission produces the formal statements and invites complete proofs; Lemma 7.1 requires Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures, which is not in Mathlib.

Difficulty

The central difficulty for the goal is that (6.3) gives each player only some subjective event, of unknown size and in his own information field, while (6.4) requires strict gains for both players under two different measures at once. The obvious approach, betting on one subjective event, gives one player a strict gain but, when that event is not known to the other player, the other player cannot condition his choice on it; the example on p. 81 shows that one-sided information genuinely fails. Both inequalities must be arranged simultaneously, and the strategies must remain measurable with respect to each player's own information.

For Lemma 7.1, a non-atomic scalar measure takes every value in $[0,p(\Omega)]$ , but the lemma asks for one event with prescribed values under $n$ measures and $nl$ further measures simultaneously; this is the range of a vector measure, not of a scalar one.

Formalization scope

Players of the zero-sum game are 0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.
$\mathcal B$ is the σ-field mΩ, an explicit parameter of RandomizingStructure; $\mathcal J_i$ are σ-fields below it, and each $p_i$ is a probability measure on $\mathcal B$ . Probabilities are ℝ≥0∞-valued; "probability $\alpha$ " is ENNReal.ofReal α with $0\le\alpha\le1$ .
Non-atomicity is the standard notion on a sub-σ-field, not Mathlib's NoAtoms, which would trivialize the roulette hypotheses.
$H_i$ is a Bochner integral under $p_i$ ; for strategies with finitely many values it is the finite sum $\sum_a p_i\{s=a\}h_i(a)$ .
The value $v$ is not a free real: IsValue u g v requires $v=F_1(\sigma)$ for a Nash equilibrium $\sigma$ of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free $v$ would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.
Assumption II is a hypothesis of every theorem, including those whose proofs do not need it.
The conclusion of the goal and of the Remark asks for strategies, not for an equilibrium point, and does not require the strategies to be independent or objective.

Needed infrastructure: Lyapunov's theorem (or a direct argument for the finite-dimensional case), manipulation of σ-fields generated by families of sub-σ-fields, and computation of $H_i$ for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.

Selected references

R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
A. Lyapunov, Sur les fonctions-vecteurs complètement additives, Bull. Acad. Sci. URSS Sér. Math. 4 (1940) 465–478.
J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928) 295–320. https://doi.org/10.1007/BF01448847
J. Nash, Non-cooperative games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529

9 thms2 active usersReviewed

Completed

Dynamic Programming Probability·Captain: mikedeng1

The Theory of Dynamic Programming: The Index Rule for Bellman's Stochastic Gold-Mining ProblemResearch Paper

Motivation

Richard Bellman's survey The theory of dynamic programming (Bull. Amer. Math. Soc. 60 (1954), 503–515, DOI 10.1090/s0002-9904-1954-09848-8) introduced dynamic programming to a general mathematical audience. It states the principle of optimality (§2, p. 504): "An optimal policy has the property that whatever the initial state and initial decisions are, the remaining decisions must constitute an optimal policy with regard to the state resulting from the first decisions", and derives from it the functional equations of finite and infinite stochastic decision processes, (4.2) and (5.1) (p. 506).

The survey illustrates the method on a small number of worked examples. The second of them, §8 "Stochastic gold mining" (pp. 508–509), is the one with a sharp answer: a two-armed sequential allocation problem with an absorbing failure state, whose optimal policy is a simple index rule. It is an early instance of the allocation-index phenomenon later made general by Gittins and Jones (1974) and Gittins (1979), and the paper itself notes (p. 509) that the rule "is not valid generally in more complicated decision processes", citing a counterexample of Karlin and Shapiro. The full treatment is in Bellman's RAND report R-245 and his 1957 book Dynamic Programming.

Setting

Two gold mines, Anaconda ( $A$ ) and Bonanza ( $B$ ), hold amounts $x \ge 0$ and $y \ge 0$ of gold. A single machine can be used in either mine. A use in Anaconda succeeds with probability $p$ : it then mines a fraction $r$ of the gold currently in Anaconda and the machine stays undamaged. With probability $1-p$ it mines nothing and the machine is destroyed. Bonanza behaves the same way with probability $q$ and fraction $s$ . While the machine works, the operator chooses the next mine; the aim is to maximize the expected amount mined before the machine is destroyed.

The only information the operator ever receives is that the machine still works. A policy is therefore a choice sequence $\sigma = (\sigma_0, \sigma_1, \dots) \in \{A, B\}^{\mathbb N}$ : the mine for use number $n$ , applied if uses $0, \dots, n-1$ succeeded. With $a_n$ , $b_n$ the numbers of $A$ - and $B$ -uses among the first $n$ , use $n$ collects $g_n = r x (1-r)^{a_n}$ if $\sigma_n = A$ and $g_n = s y (1-s)^{b_n}$ if $\sigma_n = B$ , and does so with probability $\prod_{k=0}^{n} \pi_{\sigma_k}$ ( $\pi_A = p$ , $\pi_B = q$ ). The expected return is

J(\sigma; x, y) = \sum_{n \ge 0} \Big(\prod_{k=0}^{n} \pi_{\sigma_k}\Big) g_n ,

and Bellman's (8.1) defines the optimal return

f(x, y) = \sup_\sigma J(\sigma; x, y).

In Lean these are expectedReturn p q r s σ x y and optimalReturn p q r s x y in the namespace BellmanTheoryDP.GoldMining.

Formalization targets

Milestone: the functional equation (8.2), p. 508

f(x, y) = \max\Big\{ p\,[r x + f((1-r)x, y)],\ q\,[s y + f(x, (1-s)y)] \Big\}.

Goal: the decision rule (8.3), p. 509, corrected

Write $V_A = p[rx + f((1-r)x, y)]$ and $V_B = q[sy + f(x, (1-s)y)]$ for the two branches of (8.2). For $0 < p, q, r, s < 1$ and $x, y \ge 0$ :

\frac{prx}{1-p} > \frac{qsy}{1-q} \Rightarrow V_A > V_B, \qquad \frac{prx}{1-p} < \frac{qsy}{1-q} \Rightarrow V_A < V_B, \qquad \frac{prx}{1-p} = \frac{qsy}{1-q} \Rightarrow V_A = V_B .

The paper prints the rule with $(1-r)$ and $(1-s)$ in the denominators:

a. For $prx/(1 - r) > qsy/(1 - s)$ , choose A, b. For $prx/(1 - r) < qsy/(1 - s)$ , choose B, c. For $prx/(1 - r) = qsy/(1 - s)$ , choose either.

and glosses it as "the locus of points where immediate expected gain over immediate expected loss is the same for both choices". The immediate expected loss is the probability of destroying the machine, $1-p$ (resp. $1-q$ ), not $1 - r$ . As printed the rule is false: with $p = 1/2$ , $r = 0.9$ , $q = 0.9$ , $s = 0.1$ , $x = 1$ , $y = 2$ the printed indices are $4.5 > 0.2$ , but $V_A \approx 0.924 < V_B \approx 1.055$ . The mission's goal is the corrected rule, the one the paper describes in words.

Companion: the index policy is optimal, p. 509

"Using this prescription, $f(x, y)$ may be computed recurrently": the choice sequence $\sigma^*$ generated by applying the corrected rule to the current amounts at every use satisfies $J(\sigma^*; x, y) = f(x, y)$ .

Significance

The decision rule reduces an optimization over infinite sequences to comparing two explicit numbers, one per mine, each depending only on that mine's own data. This is the defining property of an index policy, and gold mining is one of the earliest problems where it was observed. The functional equation (8.2) is the concrete form, for this process, of the infinite-horizon equation (5.1) that the paper states formally.

Formalizing the example yields a complete machine-checked instance of the principle of optimality for an infinite-horizon stochastic process whose state space (the amounts left in the two mines) is infinite, where the supremum over policies is not attained trivially and the finite-horizon recursion does not apply directly. It also records, with a checked statement, the correction of the misprint in (8.3). No machine-checked proof of (8.2) or (8.3) is known to exist.

Difficulty

The equation (8.2) looks immediate, and the paper calls it "easily seen". The informal argument treats $f$ as the value of an optimal policy, but $f$ is a supremum over infinite sequences that need not be attained a priori, and the return of a sequence is an infinite series. The finite-horizon recursion (4.2) does not apply as it stands, because the process has no last stage and its state space, the amounts left in the two mines, is infinite.

The rule (8.3) compares the two optimal continuations $f((1-r)x, y)$ and $f(x, (1-s)y)$ , which are themselves unknown. A comparison of the one-step gains alone does not decide it, as the misprinted rule shows. Parts a and b are strict preferences, so it is not enough to show that one choice is at least as good as the other.

Formalization scope

Representation. The mines are a two-element inductive type Mine; a policy is a function ℕ → Mine (ChoiceSeq). All quantities are real numbers. Randomized policies are mixtures of choice sequences and give no larger return, so they are not modelled. No restriction to stationary or Markov policies is made: $f$ is the supremum over all sequences.
Parameter ranges. The paper does not state them. The theorems assume $0 < p, q, r, s < 1$ and $x, y \ge 0$ (zero amounts allowed). $p, q < 1$ keeps the indices $prx/(1-p)$ , $qsy/(1-q)$ well defined.
Series and supremum. $J$ is a real tsum and $f$ a real iSup. For the parameter ranges above the terms are nonnegative, the partial sums are bounded by $x + y$ , and the family is bounded above, so neither Lean default value (0 for a divergent series or an unbounded supremum) arises; this is stated as the auxiliary theorem expectedReturn_le_add.
Survival indexing. The gold of use $n$ is counted only if use $n$ itself succeeds, so the survival product runs over $k \le n$ .
The misprint. The goal and the index policy use $(1-p)$ , $(1-q)$ in place of the printed $(1-r)$ , $(1-s)$ . The printed rule appears only as the quotation above.
No trivializing encoding. $f$ is defined as the supremum of expected returns over all choice sequences, per (8.1); it is not defined as a solution of (8.2), as the value of the index policy, or as a limit of value iteration, any of which would make the milestone or the goal true by definition.
Auxiliary theorems (not from the paper). The bound $0 \le J \le x + y$ with summability, the one-step unrolling $J(\sigma) = p[rx + J(\sigma'; (1-r)x, y)]$ when $\sigma_0 = A$ (and symmetrically), and the single-mine values $f(x, 0) = prx/(1 - p(1-r))$ , $f(0, y) = qsy/(1-q(1-s))$ are included as footholds. They are not milestones.
Related platform content. AllocationIndices.two_discount_index_policy_optimal (Gittins et al., Theorem 3.4) concerns Markov bandits whose rewards are discounted by $a^t$ at global time $t$ ; gold mining multiplies by the success probability of each use of the mine used, so it is a different model and is not reused. BertsekasDP.dp_algorithm_optimality is finite-horizon and does not give (8.2).

Contributions welcome: proofs of the auxiliary theorems, of (8.2), of the decision rule, and of the optimality of the index policy.

Selected references

R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), no. 6, 503–515. https://doi.org/10.1090/s0002-9904-1954-09848-8
R. Bellman, Dynamic Programming, Princeton University Press, 1957.
J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
J. C. Gittins, K. D. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033

4 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Online Decision Making with High-Dimensional Covariates: Regret Bound of the LASSO BanditResearch Paper

Motivation

Many sequential decisions are personalised: a physician chooses a drug dose for each arriving patient, a platform chooses which offer to show each arriving user. Each decision is made after observing a vector of covariates describing the individual, and its outcome is observed only for the option chosen. This is the contextual (covariate) bandit problem, studied in operations research and machine learning since Auer (JMLR 2002) and Goldenshluger and Zeevi (Stochastic Systems 2013).

In medical and e-commerce applications the covariate vector is often high-dimensional: the number of covariates $d$ is comparable to or larger than the number of decisions that will ever be made, while the outcome of each option depends on a few of them. Low-dimensional bandit algorithms then incur regret that grows polynomially with $d$ . Bastani and Bayati (Operations Research 2020) proposed the LASSO Bandit, which estimates each option's reward model with the LASSO, and proved a regret bound that grows only logarithmically in $d$ . The paper evaluates the method on warfarin dosing data.

Timeline:

2002–2003: Auer introduces linear-reward contextual bandits with confidence bounds.
2013: Goldenshluger and Zeevi give a forced-sampling algorithm for two arms in low dimension with $O(\log T)$ regret under a margin condition and an arm-optimality condition, and an information-theoretic lower bound of the same order.
2020: Bastani and Bayati extend the forced-sampling scheme to $K$ arms and high-dimensional sparse parameters, with regret $O(s_0^2[\log T+\log d]^2)$ .

Setting

There are $K$ arms with unknown parameters $\beta_1,\dots,\beta_K\in\mathbb R^d$ . At each time $t=1,2,\dots,T$ a covariate vector $X_t\in\mathbb R^d$ arrives; the $X_t$ are i.i.d. with law $\mathcal P_X$ and take values in a fixed set $\mathcal X$ . If arm $i$ is pulled, the reward is $X_t^\top\beta_i+\varepsilon_{i,t}$ , where the noises $\varepsilon_{i,t}$ are independent, $\sigma$ -subgaussian ( $\mathbb E[e^{s\varepsilon}]\le e^{\sigma^2s^2/2}$ for all $s$ ), and independent of the covariates. A policy chooses the arm $\pi_t$ from $X_t$ and the past covariates, arms and observed rewards. Its cumulative expected regret is

R_T=\sum_{t=1}^T\mathbb E\Big[\max_jX_t^\top\beta_j-X_t^\top\beta_{\pi_t}\Big].

The sparsity $s_0$ is the smallest integer $s_0\ge1$ with $\|\beta_i\|_0\le s_0$ for all $i$ .

The four assumptions are: (1) $\|x\|_\infty\le x_{\max}$ on $\mathcal X$ and $\|\beta_i\|_1\le b$ ; (2) a margin condition $\Pr[0<|X^\top(\beta_i-\beta_j)|\le\kappa]\le C_0\kappa$ ; (3) arm optimality: every arm is either suboptimal by a margin $h$ at every covariate, or optimal by margin $h$ on a region $U_i$ of probability at least $p_*$ ; (4) a compatibility condition: the conditional second-moment matrix $\Sigma_i=\mathbb E[XX^\top\mid X\in U_i]$ of each optimal arm lies in the set $\mathcal C(\mathrm{supp}(\beta_i),\phi_0)$ of matrices $M\succeq0$ with $\|v_I\|_1^2\le|I|\,v^\top Mv/\phi_0^2$ whenever $\|v_{I^c}\|_1\le3\|v_I\|_1$ .

The LASSO estimator on $n$ samples is any minimizer of $\|Y-\mathbf X\beta'\|_2^2/n+\lambda\|\beta'\|_1$ . The LASSO Bandit forces arm $i$ at the prescribed times $\mathcal T_i=\{(2^n-1)Kq+j : n\ge0,\ q(i-1)<j\le qi\}$ . At every other time it keeps the arms whose forced-sample estimate $\hat\beta(\mathcal T_{i,t-1},\lambda_1)$ is within $h/2$ of the best. Among them it plays the arm with the largest all-sample estimate $\hat\beta(\mathcal S_{i,t-1},\lambda_{2,t-1})$ , trained on every past pull of the arm, with $\lambda_{2,t}=\lambda_{2,0}\sqrt{(\log t+\log d)/t}$ .

Formalization targets

Goal: Theorem 1 (regret of the LASSO Bandit)

For $q\ge4\lceil q_0\rceil$ , $K\ge2$ , $d>2$ , $T\ge C_5$ , $\lambda_1=\phi_0^2p_*h/(64s_0x_{\max})$ and $\lambda_{2,0}=[\phi_0^2/(2s_0)]\sqrt{1/(p_*C_1)}$ ,

R_T\le C_3(\log T)^2+\big[2Kbx_{\max}(6q+4)+C_3\log d\big]\log T+\big(2bx_{\max}C_5+2Kbx_{\max}+C_4\big),

with the explicit constants $C_1,\dots,C_5$ , $q_0$ of the paper (p. 285).

Milestones

Proposition 1: a LASSO tail inequality for adaptively collected rows with conditionally subgaussian noise.
Lemma 1: a LASSO tail inequality when a constant fraction of the rows is i.i.d. with a compatible second-moment matrix.
Proposition 2: the forced-sample estimator of an optimal arm is within $h/(4x_{\max})$ of $\beta_i$ except with probability $5/t^4$ .
Proposition 3: the all-sample estimator of an optimal arm is within $16\sqrt{(\log t+\log d)/(p_*^3C_1t)}$ of $\beta_i$ except with probability $2/t+2e^{-p_*^2C_2^2t/32}$ .

Significance

The theorem shows that exploiting sparsity makes the regret depend on the ambient dimension only through $\log d$ , while its dependence on the horizon is within one $\log T$ factor of the $\Omega(\log T)$ lower bound known in low dimension. Proposition 1 is a LASSO oracle inequality for adapted designs, where each row may depend on earlier observations. It applies whenever a LASSO is fitted to data gathered by a feedback policy: adaptive experiments, dynamic pricing, sequential treatment assignment.

The results are proved in the paper and its online appendix; none of them has a machine-checked proof. This mission produces a formal model of the covariate bandit with a non-anticipating algorithm, a formal LASSO for adapted designs, and, when complete, a verified regret bound with every constant explicit. Proposition 1 and Lemma 1 are reusable beyond bandits.

Difficulty

The all-sample estimator is trained on the times at which the algorithm chose an arm, and those choices depend on earlier estimates. Its design rows are therefore neither independent nor identically distributed, and the standard LASSO analysis, which starts from i.i.d. rows and a restricted-eigenvalue bound on their population covariance, does not apply. The forced samples are i.i.d. but only $O(\log t)$ in number, too few for the $\sqrt{\log t/t}$ rate the regret bound needs. Controlling the compatibility constant of the adaptively selected sample covariance, and the martingale noise term, is where the naive argument breaks.

Formalization scope

Arms are Fin K (paper arm $i$ is i.val + 1), coordinates Fin d, times are natural numbers from $1$ . The model is a structure IsCovariateNoiseModel on a probability space: i.i.d. measurable covariates in a measurable set $\mathcal X$ , independent subgaussian noises (Mathlib's HasSubgaussianMGF with parameter $\sigma^2$ ), noise independent of covariates. Assumptions 1–4 are separate predicates. $\|x\|_\infty$ is Mathlib's sup norm, logarithms are natural, and $\Sigma_i$ is the uncentred conditional second moment.

The LASSO minimizer and the arg max need not be unique, so the algorithm takes a selection rule and a tie-breaking rule as parameters, and the theorems hold for all of them. Each round reads only the current covariate, the past covariates, the past arms and their observed rewards. The regret theorem and Proposition 3, whose data set $\mathcal S_{i,t}$ is chosen by the algorithm, require both rules to be measurable. Otherwise the trajectory would not be a random variable, and the expectations in $R_T$ could be integrals of non-measurable functions, which Lean evaluates to $0$ and which would make the goal trivially true. For the same reason every assumption constant is required to be positive, and $T\ge C_5$ is imposed on the horizon. Only the explicit inequality of Theorem 1 is stated, not the trailing $O(s_0^2[\log T+\log d]^2)$ or $q_0=O(s_0^2\log d)$ . Proposition 2 is stated for optimal arms (see its note).

A complete development needs matrix concentration for bounded i.i.d. rows, the Azuma–Hoeffding inequality, and the deterministic LASSO basic inequality under a compatibility condition. Contributions of any of these as standalone lemmas are welcome.

Selected references

H. Bastani and M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1):276–294, 2020. https://doi.org/10.1287/opre.2019.1902
A. Goldenshluger and A. Zeevi, A Linear Response Bandit Problem, Stochastic Systems 3(1):230–261, 2013. https://doi.org/10.1287/11-SSY032
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
P. Bühlmann and S. van de Geer, Statistics for High-Dimensional Data, Springer, 2011. https://doi.org/10.1007/978-3-642-20192-9

9 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

Single-Period Multiproduct Inventory Models with Substitution: No Order for a Product Stocked Above Its Base-Stock LevelResearch Paper

Motivation

A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.

Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with $N$ products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector $y^*$ ; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general $N$ -product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).

Setting

There are $N$ products and $N$ demand classes, both numbered $1,\dots,N$ . Class $i$ can be served by product $j$ whenever $j \le i$ , at a unit substitution cost $b$ when $j < i$ . Each class $i$ has unit revenue $p_i$ and unit backorder cost $\pi_i$ ; each product $j$ has unit purchase cost $c_j$ and effective unit salvage value $s_j$ (salvage value minus holding cost, possibly negative). Put $a_{ji} = p_i$ if $j = i$ , $a_{ji} = p_i - b$ if $j < i$ , and $T_k = p_k + \pi_k - b$ . The standing assumptions are: (1) $\pi_i + p_i \ge \pi_j + p_j$ for $i < j$ ; (2) $s_i \ge s_j$ for $i < j$ ; (3) $a_{ij} + \pi_j - s_i \ge 0$ for $i \le j$ .

The sequence of events: the starting inventory $x$ is observed; stock is raised to $y \ge x$ at unit costs $c$ ; the demand vector $d$ is realized; stock is allocated to classes; leftovers are salvaged. For fixed $y$ and $d$ the allocation is the linear program

G(y,d) = \max \sum_{i}\sum_{j \le i} a_{ji} w_{ji} + \sum_i s_i v_i - \sum_i \pi_i u_i

subject to $u_i + \sum_{j\le i} w_{ji} = d_i$ , $v_j + \sum_{i \ge j} w_{ji} = y_j$ , and $w, u, v \ge 0$ , where $w_{ji}$ is the amount of product $j$ given to class $i$ , $u_i$ the shortage of class $i$ and $v_j$ the leftover of product $j$ . The expected profit is

P(x,y) = -\sum_k c_k (y_k - x_k) + \mathbb E\, G(y, D),

and the ordering problem is $\max_{y \ge x} P(x,y)$ ; a maximizer is an optimal level $\bar y(x)$ .

Allocation Algorithm (A) serves the classes in the order $1,2,\dots,N$ , class $i$ first from product $i$ and then from the leftovers of products $i-1,\dots,1$ . The subproblem shortage $S^k_j$ is the unmet demand of class $j$ when (A) runs on the classes $k,\dots,j$ with the products $k,\dots,j$ only; $\vec S^k_{a,n} = 0$ means $S^k_m = 0$ for all $a \le m \le n$ . The paper's first partial derivatives of $P$ are sums of salvage values, substitution costs and the $T_k$ , weighted by probabilities of such shortage events.

Formalization targets

Goal: Theorem 2

With $y^*$ a maximizer of $P(0,\cdot)$ over $y \ge 0$ , every optimal level $\bar y$ for every starting inventory $x \ge 0$ satisfies

x_i \ge y^*_i \implies \bar y_i = x_i .

Milestones

Proposition 1: Algorithm (A) is feasible and optimal for the allocation LP, and its value is $G(y,d)$ .
Proposition 2: $y \mapsto P(x,y)$ is concave and submodular on $\{y \ge 0\}$ .
Eq. (4): the explicit formula for $\partial P/\partial y_i$ in terms of shortage probabilities.
Theorem 1: there is $y^* \ge 0$ with $\bar y(x) = y^*$ whenever $0 \le x \le y^*$ .
Lemmas 1, 2, 3, 5: identities and monotonicity properties of the shortage probabilities used to compare $\partial P/\partial y_i$ and $\partial P/\partial y_{i+1}$ .

Significance

Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector $y^*$ , computed once, determines the decision for every starting inventory in the region $x \le y^*$ and fixes the order of every overstocked product elsewhere. The paper builds its bounds on $y^*$ , its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.

The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair $j = i+1$ , and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.

Difficulty

The obvious argument for Theorem 2 is the one-dimensional one: if $x_i \ge y^*_i$ then $\partial P/\partial y_i \le 0$ at $\bar y$ , so product $i$ should not be raised. It fails because $\partial P/\partial y_i$ depends on the other coordinates: at $\bar y$ some products are raised above $x$ and others kept at $x_j > y^*_j$ , and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product $i$ propagates through the greedy allocation of every later class.

Formalization scope

Products and classes are indexed by Fin N (the paper's index $k$ is Lean index $k-1$ ); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs $w_{ji}$ , $i < j$ , forbidden (fixed to $0$ ), as in the paper's proof of Proposition 1; $G$ is the supremum of the LP objective. The demand law is a product $\nu_1 \otimes \dots \otimes \nu_N$ . Submodularity is the lattice inequality $P(x, y \vee y') + P(x, y \wedge y') \le P(x,y) + P(x,y')$ , which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.

Hypotheses the paper uses without stating, made explicit here:

the substitution cost is nonnegative, $b \ge 0$ (Proposition 1 is false for $b < 0$ );
the demand classes are independent (product forms in Lemma 3 and Appendix B);
each demand is nonnegative, has finite mean and has a density;
$s_i < c_i < p_i + \pi_i$ for every product (Theorem 1's proof);
every demand law charges every nonempty open interval of $[0,\infty)$ , standing in for the uniqueness of the optimal level $\bar y(x)$ that the notation presupposes (Theorems 1 and 2).

The goal quantifies over every maximizer $y^*$ of $P(0,\cdot)$ and every optimal $\bar y$ ; it is not an existence statement, and $y^*$ is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for $x_i \ge y^*_i$ .

A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of $S^k_j$ in $y$ and $d$ ), are welcome.

Selected references

Y. Bassok, R. Anupindi, R. Akella, Single-Period Multiproduct Inventory Models with Substitution, Operations Research 47(4):632–642, 1999. https://doi.org/10.1287/opre.47.4.632
A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
E. Ignall, A. F. Veinott, Jr., Optimality of Myopic Inventory Policies for Several Substitute Products, Management Science 15(5):284–304, 1969. https://doi.org/10.1287/mnsc.15.5.284
A. J. Hoffman, On Simple Linear Programming Problems, in V. Klee (ed.), Convexity, Proceedings of Symposia in Pure Mathematics, Vol. 7, AMS, 1963.

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

School Choice: A Mechanism Design Approach 2: The Top Trading Cycles Mechanism with Type-Specific Quotas Is Strategy-ProofResearch Paper

Motivation

Many US school districts assign children to public schools centrally. Each family ranks the schools. Each school ranks the children by priority, which is set by state or local law (siblings, walking distance, a lottery). A procedure then turns these rankings into an assignment. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) cast this as a mechanism design problem. They showed that the mechanisms then in use in Boston, Columbus and Minneapolis gave families reasons to misreport their preferences. They proposed two alternatives: the student-optimal stable mechanism of Gale and Shapley, and a school-choice version of Shapley and Scarf's top trading cycles (TTC) mechanism.

Many districts also operate under controlled choice: court-ordered or voluntary rules that keep the racial or ethnic composition of each school within bounds. In Minneapolis, for instance, a 100-seat school could admit at most 75 majority and at most 55 minority students (paper, Section III). Such rules are implemented as type-specific quotas. Section III.B of the paper modifies TTC to respect these quotas. It proves that the modified mechanism keeps both properties that recommend TTC: it wastes nothing beyond what the quotas force (constrained efficiency, Proposition 6), and truth-telling is a dominant strategy (strategy-proofness, Proposition 7). This mission formalizes those two results.

Setting

There is a finite set $I$ of students and a finite set $S$ of schools. School $s$ has a capacity $q_s$ , and the total number of seats suffices: $|I|\le\sum_s q_s$ . Each student $i$ has a strict preference over all schools, encoded as a ranking $P_i : S\to\{0,\dots,|S|-1\}$ with rank $0$ the favourite. Each school $s$ has a strict priority ranking over all students, with rank $0$ the highest priority. Each student belongs to exactly one type $\tau(i)$ , and school $s$ has a type quota $q_s^t$ for each type $t$ .

An assignment $\nu$ gives each student a school or nothing ( $\varnothing$ , worse than every school). It satisfies the controlled choice constraints if every school $s$ receives at most $q_s$ students, and at most $q_s^t$ students of each type $t$ . An assignment $\mu$ is constrained efficient if no assignment satisfying the constraints makes every student weakly better off and some student strictly better off.

The top trading cycles mechanism with type-specific quotas, $\mathrm{TTC}^q$ , runs in steps. Each school keeps a counter $c_s$ (initially $q_s$ ) and one type counter $c_s^t$ for each type (initially $q_s^t$ ). A school is removed when $c_s$ reaches zero. At each step:

every remaining student points to her favourite remaining school with room for her type, that is, with $c_s>0$ and $c_s^{\tau(i)}>0$ ;
every remaining school points to its highest-priority remaining student, whatever her type;
every student on a cycle of this graph is assigned the school she points to and leaves;
that school's counter and its counter for her type each drop by one.

A direct mechanism is strategy-proof if no student can ever gain by misreporting her preference, whatever the others report.

Formalization targets

Goal: Proposition 7 (p. 23)

For every student $i$ , every profile $P$ of announced preferences and every alternative report $Q_i$ ,

\mathrm{TTC}^q(Q_i,P_{-i})(i)=s' \implies \mathrm{TTC}^q(P)(i)=s \text{ with } P_i(s)\le P_i(s').

This holds for all capacities without shortage, all quotas, all types and all priorities. The priorities are fixed data, not reported.

Milestones

Section III.B, Step 1 (p. 22). At every step there is at least one cycle, after the convention below has removed the students who cannot point.
The Lemma (Appendix, pp. 28–29; declared valid for the modified mechanism on p. 30). Fix the other students' reports, and suppose student $i$ is still present at the beginning of a step under two different reports of hers. Then the two runs have the same remaining students and the same counters at that point.
Proposition 6 (p. 23). $\mathrm{TTC}^q(P)$ satisfies the controlled choice constraints and is constrained efficient with respect to $P$ .

Significance

Strategy-proofness is what lets a district publish a simple instruction: rank the schools in your true order. A strategy-proof mechanism does not reward families who can afford to gather information and game the system. Proposition 7 shows that this guarantee survives the addition of flexible diversity quotas, which many districts are legally bound to impose. Proposition 6 shows that the quotas cost nothing beyond the losses they themselves cause. Both results were proved in 2003 by pen and paper. The published proof of Proposition 7 is a short adaptation of the proof of Proposition 4 (strategy-proofness of plain TTC). It rests on a lemma about how the algorithm's intermediate states depend on one student's report.

To our knowledge neither result has a machine-checked proof. The related platform theorem AGT.ttc_strategyproof concerns the Shapley–Scarf housing market, where every agent owns one house and the mechanism selects the core. It does not cover capacities, priorities or quotas. A formal proof here would check the adaptation that the paper leaves to the reader, and would give a reusable formal model of cycle-clearing allocation algorithms with multiple counters.

Difficulty

The algorithm clears all cycles of a step at once, and a student's report changes the graph at every step she is present. The paper's argument compares two whole runs of the algorithm, under the true report and under a misreport, step by step. That comparison needs precise control of which parts of the state a single student's report can influence, and when. A local argument about one step does not suffice. The student's outcome can depend on cycles that form several steps after the two runs could first have diverged.

With quotas, the pointing graph also depends on the type counters. A school can be present but closed to one type, and a school points to its best remaining student even when it has no room for her type. The comparison must therefore track the type counters as well as the set of remaining schools. Efficiency cannot be read off step by step against unrestricted matchings either: every competing assignment must satisfy both the capacity and the quota constraints.

Formalization scope

Students, schools and types are finite types; no nonemptiness is assumed. Preferences and priorities are bijective rankings onto Fin, so strictness is built in. Rank $0$ is the favourite or the highest priority. The no-shortage condition $|I|\le\sum_s q_s$ appears in every theorem, as the standing assumption of Section I. No relation between $q_s$ and $q_s^t$ is imposed, which generalises the paper.

The algorithm is a concrete, total definition: a state with remaining students, counters, type counters and partial assignments, a step map that clears all cycles simultaneously, and $|I|$ iterations. run … t is the state at the beginning of the paper's Step $t+1$ .

The paper's step is undefined when a remaining student has no remaining school with room for her type. She cannot point, and the promised cycle may not exist. The formalization adopts one convention: at the beginning of each step, such a stuck student is removed unassigned, and her outcome is $\varnothing$ , ranked below every school. Counters only decrease, so a stuck student stays stuck. Whenever nobody gets stuck, the algorithm is exactly the paper's, and when every quota is at least the capacity it is plain TTC. The goal and Proposition 6 are stated for assignments that may leave students unassigned. When everyone is assigned, they coincide with the paper's statements over matchings.

The formalization does not add a hypothesis that the run never gets stuck. Such a hypothesis would restrict the algorithm's own behaviour and could make the theorems vacuous. Nor may strategy-proofness be weakened to comparisons at the truthful profile only: the others' reports and the misreport are arbitrary.

Contributions welcome: invariants of the step map (counters bounded by the initial values, assigned students leave for good), the cycle-existence lemma for functional graphs on finite sets, and the comparison lemma. These pieces are shared with the plain-TTC mission of this series.

Selected references

Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

School Choice: A Mechanism Design Approach 1: The Top Trading Cycles Mechanism Is Strategy-ProofResearch Paper

Motivation

Public school districts in many US cities let families rank schools and then assign seats by a centralized procedure. Each school has a limited number of seats, and state or local law gives some students priority at some schools, for example for a sibling already enrolled or for living within walking distance. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) framed this as a mechanism design problem and showed that the mechanism then used in Boston rewards families who misreport their preferences. They proposed two replacements with written proofs of their properties. This mission covers the second one, the top trading cycles mechanism, and its two properties: every outcome is Pareto efficient, and no student can gain by misreporting.

The paper drew on earlier results for simpler allocation problems:

1974: Shapley and Scarf introduce housing markets and Gale's top trading cycles algorithm, in which each agent owns one house.
1977: Roth and Postlewaite show the algorithm finds the unique core allocation of a housing market.
1982: Roth proves the core mechanism for housing markets is strategy-proof.
1999: Abdulkadiroğlu and Sönmez adapt the algorithm to house allocation with existing tenants and prove strategy-proofness.
2000: Pápai introduces hierarchical exchange rules, a wider class that includes these mechanisms.
2003: the paper formalized here extends the algorithm to schools with capacities and school-specific priorities (Propositions 3 and 4).

Setting

A school choice problem consists of a finite set $I$ of students, a finite set $S$ of schools, a capacity $q_s \in \mathbb N$ for each school, a strict preference $P_i$ of each student over all schools, and a strict priority ordering $\succ_s$ of each school over all students. The standing assumption is that there is no shortage of seats:

|I| \le \sum_{s\in S} q_s .

Preferences are rankings: $P_i(s)\in\{0,\dots,|S|-1\}$ is the rank of $s$ for student $i$ , with rank $0$ the favourite. Priorities are rankings of students in the same way, with rank $0$ the highest priority. A matching is a map $\mu : I\to S$ with $\#\{i:\mu(i)=s\}\le q_s$ for every school $s$ . A matching $\mu$ is Pareto efficient if no other matching $\nu$ gives every student a weakly better school ( $P_i(\nu(i))\le P_i(\mu(i))$ ) and some student a strictly better one.

A direct mechanism maps the reported preference profile, together with the fixed priorities and capacities, to a matching. It is strategy-proof if no student can ever obtain a school she strictly prefers by changing her own report while the others keep theirs.

The top trading cycles algorithm keeps a counter $c_s$ of free seats at each school, starting at $q_s$ . A school is remaining while $c_s>0$ . At each step every remaining student points to her favourite remaining school, and every remaining school points to the remaining student with the highest priority for it. A cycle is a list $(s_1,i_1,\dots,s_k,i_k)$ of distinct schools and students in which $s_1$ points to $i_1$ , $i_1$ points to $s_2$ , and so on, and $i_k$ points to $s_1$ . Every student on a cycle is assigned the school she points to and is removed. Each school on a cycle loses one seat. All cycles present at a step are cleared at that same step. The top trading cycles mechanism $\mathrm{TTC}(q,\succ,P)$ returns the resulting assignment.

Formalization targets

Goal: Proposition 4 (strategy-proofness)

For all capacities with no shortage, all priorities, every profile $P$ , every student $i$ and every alternative report $Q_i$ , student $i$ is assigned schools $s = \mathrm{TTC}(q,\succ,P)(i)$ and $s' = \mathrm{TTC}(q,\succ,(Q_i,P_{-i}))(i)$ , and

P_i(s) \le P_i(s') .

Milestones

At every step at which some student remains, there is a cycle (Section II.B, p. 15).
After $|I|$ steps no student remains, and the outcome is a matching (Section II.B, p. 16).
Lemma (Appendix, pp. 28–29): if student $i$ is still remaining at the beginning of a step under two different reports of her own, the remaining students and the remaining schools at that point are the same under both reports.
Proposition 3 (p. 17): the outcome is a Pareto efficient matching with respect to the reported profile.
When all schools share one priority ordering $\pi$ , the mechanism equals the serial dictatorship induced by $\pi$ (Section II.B, p. 16).

Significance

Strategy-proofness means truthful reporting is a dominant strategy for every student. Families need no information about other families' reports. Under the Boston mechanism, ranking a popular school first can cost a student her priority at her second choice. Proposition 3 separates the top trading cycles mechanism from the Gale–Shapley student-optimal stable mechanism, which is also strategy-proof but can select Pareto dominated matchings.

The results are proved in the paper, in short prose arguments in its Appendix. To the best of our knowledge they have no machine-checked proof. The platform already has the housing-market version, AGT.ttc_strategyproof, but that statement covers one house per agent with the mechanism characterised as the core. Capacities, school priorities and the step-by-step algorithm are absent from it. This mission produces a checked account of the algorithm with capacities and counters, together with its termination and invariance properties.

Difficulty

The paper's argument moves from the step at which student $i$ leaves under one report to the step at which she leaves under another. It relies on the claim that the cycles formed before either step are unaffected by $i$ 's report. Informally, $i$ is not on a cycle yet, so what she points to does not matter. Formally, "the same cycles form" requires comparing two runs of a simultaneous-clearing procedure step by step. At each step one has to show that the set of cycles, and hence the counters and the remaining schools, agree, even though $i$ points to different schools in the two runs. Reasoning about a single cycle at a time does not work, because the algorithm clears all cycles of a step at once. Termination is also not immediate: without the no-shortage condition the algorithm can leave students unassigned. Seats are counted with multiplicity, so a school can stay in the market for several steps.

Formalization scope

Everything lives in the namespace SchoolChoice.TTC. Students and schools are arbitrary finite types with decidable equality; the set of students may be empty. Capacities are q : S → ℕ, and a school of capacity zero is never remaining. A preference is a bijection S ≃ Fin (card S) and a priority is a bijection I ≃ Fin (card I), in both cases with rank 0 the best. Strictness and completeness of both therefore hold by construction, and every school is acceptable. A state of the algorithm consists of the remaining students, the counters and the assignments made so far. run q pri P t is the state after t completed steps, which is the beginning of the paper's Step t + 1. The mechanism ttc q pri P : I → Option S reads off the assignment after card I steps. Every theorem assumes card I ≤ ∑ s, q s.

The algorithm is a concrete, deterministic definition that clears all cycles at every step. The mechanism is not defined as "some Pareto efficient matching" or characterised by properties, since that would make Proposition 3 trivial. The goal asserts that both outcomes exist, so an unassigned outcome cannot satisfy it vacuously. The misreport, the other students' reports and the priorities are all universally quantified.

A complete development needs termination of the algorithm, a combinatorial account of the pointing graph (cycles in a finite functional graph), and the step-by-step invariance argument of the Lemma. The last two are reusable for the type-specific quota variant and for other trading-cycle mechanisms. Contributions of intermediate lemmas are welcome: counter invariants such as "the sum of the counters is at least the number of remaining students", monotonicity of the remaining sets, and the fact that a student on a cycle receives her favourite remaining school.

Selected references

Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0
Alvin E. Roth and Andrew Postlewaite, Weak versus Strong Domination in a Market with Indivisible Goods, Journal of Mathematical Economics 4(2), 131–137, 1977. https://doi.org/10.1016/0304-4068(77)90004-0
Alvin E. Roth, Incentive Compatibility in a Market with Indivisible Goods, Economics Letters 9(2), 127–132, 1982. https://doi.org/10.1016/0165-1765(82)90003-9
Atila Abdulkadiroğlu and Tayfun Sönmez, House Allocation with Existing Tenants, Journal of Economic Theory 88(2), 233–260, 1999. https://doi.org/10.1006/jeth.1999.2553
Szilvia Pápai, Strategyproof Assignment by Hierarchical Exchange, Econometrica 68(6), 1403–1433, 2000. https://doi.org/10.1111/1468-0262.00166

9 thms2 active usersReviewed

Algorithmic Game Theory Linear Optimization Probability·Captain: mikedeng1

A General Framework for the Study of Decentralized Distribution Systems: A Core Allocation Rule Whose Nash Equilibrium Is First-BestResearch Paper

Pooling inventory among independent retailers

Retailers that sell the same product can raise their joint profit by pooling: stock left over at one location is shipped to meet unmet demand at another, and stock can be held in shared warehouses until demand is known (Eppen 1979; Eppen and Schrage 1981). When the retailers are independent firms, pooling creates two questions at once. After demand is realized, the extra profit from shipping must be split in a way no group of retailers would reject. Before demand is realized, each retailer chooses its own stock, and that choice depends on how the split will be made. A split that is fair ex post may lead to stocking decisions that are poor for the system as a whole.

Anupindi, Bassok and Zemel (MSOM 2001) model the ex-post split as a cooperative game, the ex-ante stocking as a non-cooperative game, and ask whether a single allocation rule can serve both. Their framework is a standard reference for "coopetition" models in supply chains, where firms compete on stocking decisions and cooperate on redistribution.

Setting

There are retailers $\mathcal N=\{1,\dots,N\}$ and warehouses $\mathcal W=\{1,\dots,W\}$ . Retailer $n$ has unit cost $c_n$ , revenue $r_n$ and salvage value $v_n$ ; warehouse $w$ has purchasing cost $c_w$ and salvage value $v_w$ . Shipping from location $i$ to retailer $n$ costs $t_{i,n}$ per unit, and a fraction $\beta_{i,n}\in[0,1]$ of the customers at $n$ accept service from $i$ .

Before demand, retailer $n$ chooses a position $\vec Z_n=(X_n,Y_{1,n},\dots,Y_{W,n})$ : local stock $X_n$ and claims $Y_{w,n}$ on warehouse stock, so warehouse $w$ holds $Y_w=\sum_nY_{w,n}$ . A profile is $[Z]=(\vec Z_1,\dots,\vec Z_N)$ . Demand $\vec D$ is random with law $\mu$ . After demand, retailer $n$ has local sales $S_n=\min\{X_n,D_n\}$ , residual inventory $H_n=\max\{X_n-D_n,0\}$ and residual demand $E_n=\max\{D_n-X_n,0\}$ .

The snapshot allocation game SAG $([Z],\vec D)$ gives each coalition $\mathcal S\subseteq\mathcal N$ the value $W^*_{\mathcal S}([Z],\vec D)$ : the optimal value of the linear program (6), which ships $q_{i,n}$ units from $i\in\mathcal S\cup\mathcal W$ to $n\in\mathcal S$ at profit $r_n-v_i-t_{i,n}$ per unit, subject to $\sum_nq_{i,n}\le H_i$ , $\sum_nq_{w,n}\le\sum_{n\in\mathcal S}Y_{w,n}$ and $\sum_iq_{i,n}/\beta_{i,n}\le E_n$ . Its core is the set of allocations $\alpha$ with $\sum_{j\in\mathcal S}\alpha_j\ge W^*_{\mathcal S}$ for every $\mathcal S$ and $\sum_{j\in\mathcal N}\alpha_j=W^*_{\mathcal N}$ (7).

An allocation rule AR- $m$ assigns surplus $\alpha^m_n([Z],\vec D)$ ; retailer $n$ earns

P^m_n([Z],\vec D)=r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}+\alpha^m_n([Z],\vec D)\qquad(9)

and expects $J^m_n([Z])=E_{\vec D}P^m_n$ . A Nash equilibrium (10) is a profile at which no retailer gains by changing its own position. The first-best profile $[Z]^{c*}$ maximizes the expected centralized profit $J^c_{\mathcal N}([Z])=E_{\vec D}P^c_{\mathcal N}([Z],\vec D)$ , where $P^c_{\mathcal N}=\sum_n[r_nS_n+v_nH_n-c_nX_n]-\sum_w(c_w-v_w)Y_w+W^*_{\mathcal N}$ .

The fractional rule AR-f (11) pays $\alpha^f_n=\theta_nP^c_{\mathcal N}-[\,r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}]$ with fixed shares $\theta_n\in(0,1)$ , $\sum_n\theta_n=1$ . The dual allocation (8) is $\alpha^d_n=\nu_nH_n+\sum_w\gamma_wY_{w,n}+\delta_nE_n$ for optimal dual prices $(\nu,\gamma,\delta)$ of (6) for $\mathcal N$ . The modified rule AR-c is $\alpha^c_n([Z],\vec D)=\alpha^f_n([Z],\vec D)+w_n([Z]^{c*},\vec D)$ with $w_n=\alpha^d_n([Z]^{c*},\cdot)-\alpha^f_n([Z]^{c*},\cdot)$ .

Formalization targets

Goal: Corollary 5.1 (p. 361)

For a first-best profile $[Z]^{c*}$ and a measurable choice of dual prices at $[Z]^{c*}$ ,

[Z]^{c*}\ \text{is a pure Nash equilibrium under AR-c, and}\ \ \alpha^c([Z]^{c*},\vec D)\in\operatorname{Core}\big(\mathrm{SAG}([Z]^{c*},\vec D)\big)\ \ \forall\vec D,

with integrable side payments.

Milestones

Examples 1 and 2 (pp. 358–359): a transfer-price allocation outside the core; the dual allocation $(8,8,8,0)$ and the non-dual core allocation $(0,0,0,24)$ .
Theorem 4.1 (p. 358): if all inventory is claimed, the core of SAG $([Z],\vec D)$ is nonempty and contains the dual allocation (8) for every optimal dual.
Theorem 5.2 (p. 361): under AR-f every first-best profile is a Nash equilibrium.
Theorem 5.1 (p. 361): for any rule and any of its equilibria $[Z]^{m*}$ there are integrable demand-dependent side payments that leave the set of equilibria unchanged and put the allocations at $[Z]^{m*}$ in the core for every $\vec D$ .

Significance

The goal answers the paper's central question positively: there is an allocation mechanism under which the centrally optimal stock levels are an equilibrium of the decentralized stocking game, while every ex-post split of the pooling surplus is stable against all coalitions. Theorem 4.1 is the ex-post half: shadow prices of the shipping LP give a stable split for every realization, independently of who owns which units. The paper also shows (Proposition 5.1, not included here) that the dual allocation alone does not induce first-best stocking, which is why the side payments of Theorem 5.1 are needed.

The results are proved in the paper; Theorem 4.1 is proved there only by reference to the LP-game literature (Owen 1975; Samet and Zemel 1984). None of them has a machine-checked proof. The mission would produce the first formal treatment on Prove2Me of a linear-production (LP) game and its core, and of a model combining a cooperative second stage with a non-cooperative first stage.

Difficulty

Theorem 4.1 is an instance of Owen's theorem on LP games, but the instance is not a standard linear production game: coalition LPs have variables only on arcs inside the coalition, warehouse capacity is limited to the coalition's own claims, and the acceptance constraint divides by $\beta_{i,n}$ , which may be zero, so the general theorem cannot be quoted as it stands. The paper leaves the dual of (6) unwritten, and Mathlib has no ready-made LP duality in this form.

The stochastic layer is the other obstacle. Expected payoffs are integrals, and the side payment is built from a choice of dual prices for each demand realization. Its integrability requires measurability of that choice and of the LP value as a function of demand; neither is given by the paper, which treats the side payments as "constants".

Formalization scope

Retailers are Fin N, warehouses Fin W, locations Fin N ⊕ Fin W; quantities, prices and demands are real numbers; demand is a probability measure on Fin N → ℝ; expectations are Bochner integrals. $W^*_{\mathcal S}$ is the real supremum of (6a) over the feasible set, and profiles are required to be nonnegative, which makes the feasible set nonempty and bounded. Arcs with $\beta_{i,n}=0$ carry no shipment. The core is the platform definition Supermodularity.Cooperative.Core. The dual of (6) is written out explicitly (the paper does not state it). The paper's continuous-CDF assumption is not used and is dropped.

Pinned readings:

"Dual prices" means any optimal solution of the dual of (6) for $\mathcal N$ ; Theorem 4.1 is stated for every such solution.
"Induces the same equilibrium inventory levels as the first-best" (Theorem 5.2) and "the NE using $\alpha^c$ is first-best" (Corollary 5.1) are stated as "every first-best profile is a Nash equilibrium", the direction the proofs give.
" $[Z]^{\tilde m*}=[Z]^{m*}$ " (Theorem 5.1) is stated as equality of the two sets of equilibria; the continuity and unimodality assumptions, which only guarantee existence of an equilibrium, are dropped because the equilibrium is a hypothesis.
"An appropriate way of breaking ties" is a measurable choice of optimal dual prices; demand is almost surely nonnegative; the rule's payoffs in Theorem 5.1 are integrable.
The shares $\gamma_n$ of Theorem 5.2 are written $\theta_n$ , and Eq. (11) is used with $+v_nH_n$ in the bracket (printed $-v_nH_n$ ), as the proof on p. 367 requires.

Not acceptable: a core without the efficiency equation (7b); a feasible set that lets $q_{i,n}/0=0$ sell to customers who balk; an arbitrary side payment instead of the constructed one; or a Nash equilibrium evaluated through non-integrable payoffs, whose Bochner integral is $0$ and makes every profile an equilibrium.

Useful infrastructure: finite-dimensional LP duality in inequality form, measurable selection of LP optimal solutions, and continuity of LP values in the right-hand side. All of it can be reused in other LP-game and two-stage stochastic programming missions.

Selected references

R. Anupindi, Y. Bassok, E. Zemel, A General Framework for the Study of Decentralized Distribution Systems, Manufacturing & Service Operations Management 3(4):349–368, 2001. https://doi.org/10.1287/msom.3.4.349.9973
G. Owen, On the core of linear production games, Mathematical Programming 9:358–370, 1975. https://doi.org/10.1007/BF01681356
D. Samet, E. Zemel, On the core and dual set of linear programming games, Mathematics of Operations Research 9(2):309–316, 1984. https://doi.org/10.1287/moor.9.2.309
G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5):498–501, 1979. https://doi.org/10.1287/mnsc.25.5.498

10 thms2 active usersReviewed

Completed

Discrete Geometry Linear Optimization Optimization·Captain: mikedeng1

Elementare Theorie der konvexen Polyeder I: A Point on All Extreme Supports of a Finite Cone Is a Nonnegative Combination of at Most n GeneratorsResearch Paper

Motivation

A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension $n$ . This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.

Timeline:

1896, H. Minkowski, Geometrie der Zahlen: polytopes as bounded intersections of half-spaces and as convex hulls of finitely many points.
1911, C. Carathéodory: a point in the convex hull of a set in $\mathbb{R}^d$ is a convex combination of at most $d+1$ of its points (Rend. Circ. Mat. Palermo 32).
1935, H. Weyl: the present paper; Satz 1 and Satz 2 for cones, with the dual statements in §3 and the polytope theorem in §4.

Setting

Points of $\mathbb{R}^n$ are $n$ -tuples $x = (x_1, \ldots, x_n)$ , and $\langle \alpha, x \rangle = \alpha_1 x_1 + \cdots + \alpha_n x_n$ . A vector $\alpha \ne 0$ determines the half-space $\{x : \langle\alpha,x\rangle \ge 0\}$ ; positive multiples of $\alpha$ give the same half-space.

A point system $S$ is a finite set of points of $\mathbb{R}^n$ . It is non-degenerate if its points do not all satisfy one equation $\langle\alpha,x\rangle = 0$ with $\alpha \neq 0$ , i.e. the only $\alpha$ orthogonal to every point of $S$ is $0$ .

A half-space $\langle\alpha,x\rangle\ge 0$ ( $\alpha\ne 0$ ) is a support of $S$ if every point of $S$ lies in it. It is an extreme support if, in addition, equality $\langle\alpha,x\rangle = 0$ holds at $n-1$ linearly independent points $x$ of $S$ .

A point $x$ is representable by $S$ if it is a nonnegative combination of the points of $S$ :

x = \sum_{s\in S} c_s\, s, \qquad c_s \ge 0 .

The set of points lying in all extreme supports of $S$ is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and $\langle\alpha,x\rangle$ written α ⬝ᵥ x.

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

For a finite non-degenerate $S \subset \mathbb{R}^n$ and a point $x$ with $\langle\alpha,x\rangle\ge 0$ for every extreme support $\alpha$ of $S$ ,

\exists\, T \subseteq S,\quad |T| \le n,\quad x = \sum_{t\in T} c_t\, t,\ \ c_t \ge 0 .

Satz 1 (Hauptsatz), p. 291

Under the same hypotheses, $x$ is representable by $S$ . Satz 2 contains Satz 1.

Steps of the proof (§1–§2)

A finite non-degenerate $S$ has only finitely many extreme supports, up to positive scaling (p. 291).
The reduction step of case a) (p. 292): if $S$ has an extreme support $\beta$ and $p$ satisfies all extreme supports, there are $e \in S$ with $\langle\beta,e\rangle>0$ and $\lambda\ge 0$ such that $q = p-\lambda e$ still satisfies all extreme supports and lies on the plane of one of them.
The lifting step (p. 293): with $x_n \ge 0$ an extreme support of $S$ and $S_0$ the points on $x_n = 0$ , every extreme support $\beta$ of $S_0$ in $\mathbb{R}^{n-1}$ lifts to the extreme support $\beta_1x_1+\cdots+\beta_{n-1}x_{n-1} - \mu x_n \ge 0$ of $S$ (inequality (6)).
Case b) (p. 291, proved pp. 293–294): if $S$ has no extreme support, every point of $\mathbb{R}^n$ is representable by $S$ .

Significance

Satz 1 together with its trivial converse identifies the cone generated by $S$ with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in $\mathbb{R}^n$ is a nonnegative combination of at most $n$ generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.

On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.

Difficulty

The hypothesis only controls $x$ against the extreme supports, not against every support. Showing that $x$ lies in the cone generated by $S$ whenever $\langle\alpha,x\rangle\ge 0$ holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.

The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives $n$ generators in one case and $n+1$ in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound $n$ . The case where $S$ has no extreme support at all must also be handled separately; it is not vacuous, since $S$ can then generate all of $\mathbb{R}^n$ .

Formalization scope

Conventions committed to in Lean:

$\mathbb{R}^n$ is Fin n → ℝ; points and normals share this type (the dual space is identified with $\mathbb{R}^n$ , as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.
A point system is a Finset (Fin n → ℝ). The zero vector is not excluded.
A support normal satisfies α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space $\mathbb{R}^n$ .
"All extreme support equations are satisfied" in Satz 1 is read as the inequalities $\langle\alpha,x\rangle\ge0$ for every extreme normal $\alpha$ , as the proof and Satz 2 make explicit. The hypothesis quantifies over all extreme normals, so no representatives are chosen.
"Positive-linear" combinations have nonnegative coefficients (display (3)). In Satz 2 the subset $T$ is not required to be linearly independent.
Finiteness of extreme supports is stated up to positive scaling.
The lifting step is stated in the coordinates Weyl fixes on p. 293: $\mathbb{R}^n$ is Fin (m+1) → ℝ, the extreme support is $x_n \ge 0$ (Fin.last m), $S_0$ is projected by Fin.init, and $\mu$ is given together with hypotheses that it is the attained minimum. The hypothesis $n \ge 2$ is made explicit.

Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for $S = \{e_1\} \subset \mathbb{R}^2$ the extreme supports are $\pm x_2 \ge 0$ , and $x = (-1, 0)$ satisfies both without being a nonnegative multiple of $e_1$ .

A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through $n-1$ independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.

Selected references

H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici 7 (1935), 290–306. https://doi.org/10.1007/BF01292722
C. Carathéodory, Über den Variabilitätsbereich der Fourier'schen Konstanten von positiven harmonischen Funktionen, Rendiconti del Circolo Matematico di Palermo 32 (1911), 193–217. https://doi.org/10.1007/BF03014795
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (the Farkas–Minkowski–Weyl theorem). ISBN 978-0-471-98232-6
G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Lecture 1. https://doi.org/10.1007/978-1-4613-8431-1

9 thms2 active usersReviewed

Algorithmic Game Theory Complexity Theory·Captain: mikedeng1

Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities II: An Exact 3-Cover Exists iff the Constructed Market Has an EquilibriumResearch Paper

Motivation

Market equilibrium is the central solution concept of general equilibrium theory: prices at which every agent buys a utility-maximizing bundle and supply meets demand. Arrow and Debreu (1954) proved that equilibria exist under mild conditions on endowments and utilities, and a line of work in algorithmic game theory asks how hard it is to compute them. For linear utilities an equilibrium can be computed in polynomial time, and there is an efficiently checkable condition for its existence. The next natural class, additively separable piecewise-linear concave utilities, models diminishing marginal utility and is the class most used in applications.

Vazirani and Yannakakis (J. ACM 58(3), 2011) settle the complexity of this class. They show that equilibria are rational whenever they exist (Theorems 4.1 and 5.1), that computing an equilibrium under the standard sufficient conditions is PPAD-complete (Theorems 6.1 and 7.1, building on Chen, Dai, Du and Teng 2009), and — the subject of this mission — that deciding whether an equilibrium exists at all is NP-complete (Theorem 8.1). The hardness half rests on an explicit construction: from an instance of Exact Cover by 3-Sets, a market whose equilibria encode exact covers.

Setting

An Arrow–Debreu market has a finite set $B$ of agents and a finite set $G$ of divisible goods. Agent $i$ owns an endowment $w_{ij}\ge 0$ of each good $j$ and has utility $u_i(y)=\sum_{j} f^i_j(y_j)$ , where each $f^i_j$ is a piecewise-linear concave utility function: slopes $c_1\ge c_2\ge\dots\ge c_m>0$ on consecutive pieces of lengths $a_1,\dots,a_m$ , followed by a last piece of slope $t\in[0,c_m]$ until infinity ( $t=0$ means the function goes flat).

At prices $p$ , agent $i$ 's income is $\sum_j p_j w_{ij}$ . An optimal bundle is an affordable $y\ge 0$ maximizing $u_i$ among affordable bundles, bought only along the pieces of $f^i_j$ that carry utility. A price equilibrium is a price vector $p$ in the unit simplex ( $p\ge 0$ , $\sum_j p_j=1$ ) together with an allocation of optimal bundles such that $\sum_i x_{ij}=\sum_i w_{ij}$ for every good $j$ . It is an $\epsilon$ -approximate equilibrium if instead $|\sum_i x_{ij}-\sum_i w_{ij}|\le\epsilon\sum_i w_{ij}$ for every $j$ .

An X3C instance is a family $\mathcal C=(C_1,\dots,C_n)$ of $3$ -element subsets of $X=\{x_1,\dots,x_n\}$ ; an exact cover is a subfamily in which every element of $X$ lies in exactly one set. Following the paper, $n$ is a multiple of $3$ , $n>35$ , and $\bigcup_i C_i=X$ .

The market $D(\mathcal C)$ has $2n+1$ goods (good $0$ , goods $C_i$ , goods $x_j$ ) and $2n+2$ agents, with $e_0=n^3$ :

agent $0$ owns $e_0$ units of every good; his utility for every good has slope $2$ up to $e_0$ units and slope $1$ beyond;
agent $C_i$ owns one unit of good $C_i$ ; segments of slope $1$ , length $1/2$ for good $0$ , slope $1/3$ , length $1/6$ for each good $x_j\in C_i$ , slope $1/9$ , length $1/4$ for good $C_i$ ;
agent $x_j$ owns $1/6$ unit of good $x_j$ ; one segment of slope $1$ , length $1/12$ for good $0$ ;
the extra agent owns $n/2$ units of good $0$ ; one segment of slope $1$ , length $3/4$ for each good $C_i$ .

All other utility functions are flat.

Formalization targets

Goal: the reduction statement

\mathcal C\ \text{has an exact cover}\iff D(\mathcal C)\ \text{has an equilibrium}\iff D(\mathcal C)\ \text{has an } n^{-5}\text{-approximate equilibrium}.

This is the mathematical content of the NP-hardness half of Theorem 8.1, assembled by the paper from Lemmas 8.2 and 8.3.

Milestones

Lemma 8.2: an exact cover yields an equilibrium of $D(\mathcal C)$ .
Lemma 7.2, as applied in Lemma 8.3: in an $n^{-5}$ -approximate equilibrium of $D(\mathcal C)$ all prices are positive and within a factor $2$ of each other.
Claims 8.4–8.7: in such an equilibrium, with $p_m$ the minimum price, $p(0)=2p_m$ ; $p(x_j)<2p_m$ ; with $S=\{i: p(C_i)\ge p_m+\tfrac16\sum_{x_j\in C_i}p(x_j)\}$ , every $i\notin S$ has $p(C_i)=p_m$ ; and the sets indexed by $S$ are pairwise disjoint.
Lemma 8.3: an equilibrium, or an $n^{-5}$ -approximate equilibrium, of $D(\mathcal C)$ yields an exact cover.

Significance

Theorem 8.1 shows that there is no efficiently checkable necessary and sufficient condition for the existence of an equilibrium in piecewise-linear concave markets unless P = NP, in contrast with the linear case. Together with the PPAD results of the same paper it separates two questions: under the classical sufficient conditions an equilibrium exists and finding one is PPAD-complete; without them, even deciding existence is NP-hard, and remains so for $n^{-5}$ -approximate equilibria. The construction illustrates the technique the paper uses for both of its negative results: well-chosen piecewise-linear pieces make an agent buy a segment wholly or not at all, depending on how prices compare, which gives the equilibrium problem a discrete character.

The result is proved in the paper. To our knowledge no part of it has been machine-checked. This mission formalizes the reduction's correctness at full strength, including the approximate version, which requires quantitative control of clearing errors that the exact version does not.

Difficulty

The direction "exact cover ⇒ equilibrium" is an explicit verification: prescribed prices and an allocation, and a check that every bundle is optimal, which for separable piecewise-linear utilities is a bang-per-buck comparison. The converse is the substantial part. An arbitrary approximate equilibrium must be shown to have the rigid price structure — every price in $[p_m,2p_m]$ , good $0$ at $2p_m$ , unused sets at $p_m$ — before a counting argument on agent $0$ 's savings forces $|S|=n/3$ . Each step is an excess-demand argument in which the error $\epsilon$ times the supply must be compared with quantities of order $1/n$ ; this is where $n>35$ and the exponent $5$ enter, and why the approximate statement does not follow from the exact one. Optimality of bundles is a statement about all affordable bundles, so each claim needs the structure of optimal bundles under piecewise-linear concave utility, which is not in Mathlib.

Formalization scope

Lean namespace PLCMarkets.ExactCover. Market data (endowments, slopes, lengths) are rationals; prices and allocations are reals. Goods and agents of $D(\mathcal C)$ are small inductive types named as in the paper; indices are 0-based. Supplies are not normalized to $1$ , so clearing is $\sum_i x_{ij}=\sum_i w_{ij}$ ; prices are normalized to the simplex in both equilibrium notions, as in the proof of Lemma 8.3. The family $\mathcal C$ is indexed and may repeat a set; exact cover and the disjointness of $S$ count indices.

Standing hypotheses of every theorem: each $C_i$ has three elements, $3\mid n$ , $n>35$ , $\bigcup_i C_i=X$ — the paper's own "without loss of generality" assumptions (p. 10:19). Two conventions depart from the printed page, both necessary and both disclosed on the items:

Optimal bundles buy only utility-bearing pieces. If a utility function is flat beyond its segments, the agent does not buy beyond them. The paper uses this throughout (an agent "can only spend $p_m/6$ on the single segment", Claim 8.5). Without it, agents can spend leftover income on goods worth nothing to them; then setting $p(0)=2p_m$ and every other price to $p_m$ gives an exact equilibrium of every $D(\mathcal C)$ , and the goal is false.
The extra agent's segments have length $3/4$ . The page prints $3n/4$ ; every computation in the paper (Lemma 8.2, Claim 8.6, the end of Lemma 8.3) uses $3/4$ per good, and with $3n/4$ the prices of Lemma 8.2 are not an equilibrium.

Trivializing encodings are excluded: optimality of bundles is part of both equilibrium notions (without it the endowment itself clears every market), clearing is relative and per good, and the goal quantifies only over $n$ and $\mathcal C$ , with $D(\mathcal C)$ an explicit function of $\mathcal C$ .

Out of scope: the complexity-class statement "NP-complete" and NP membership (which comes from the rationality theorems of the companion mission); polynomial-time computability of the construction and string encodings of markets; and the Fisher market $F$ of §8, whose half of Lemmas 8.2 and 8.3 is a natural follow-up. Reusable infrastructure: piecewise-linear concave utilities, Arrow–Debreu markets with exact and approximate equilibria, and bang-per-buck characterizations of optimal bundles. Contributions proving that characterization as a standalone lemma are welcome.

Selected references

V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, Journal of the ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, Proceedings of the IEEE Symposium on Foundations of Computer Science (FOCS), 2009 (reference [Chen et al. 2009a] of the paper).
M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 1954. https://doi.org/10.2307/1907353

12 thms2 active usersReviewed

Algorithmic Game Theory Linear Optimization·Captain: mikedeng1

Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities I: Fisher Markets with an Equilibrium Have Rational Equilibrium Prices of Polynomial Bit SizeResearch Paper

Motivation

A Fisher market is the simplest model of a market in which prices are set by supply and demand: buyers bring money, sellers bring goods, and a price vector is an equilibrium when every buyer, spending her money optimally at those prices, leaves every good exactly sold out. Computing equilibria is one of the central questions of algorithmic game theory, because a polynomial-time algorithm is what would make the equilibrium concept usable as a prediction or as a pricing mechanism.

For linear utilities an equilibrium always exists, is rational, and can be computed in polynomial time (Eisenberg and Gale 1959; Devanur, Papadimitriou, Saberi and Vazirani, J. ACM 2008, https://doi.org/10.1145/1411509.1411512). The next natural class, additively separable, piecewise-linear, concave utilities, captures diminishing marginal utility and is the class studied by Vazirani and Yannakakis (J. ACM 58(3), Article 10, 2011, https://doi.org/10.1145/1970392.1970394). Their paper shows that equilibria in this class are hard to compute (PPAD-complete) and that deciding whether one exists is NP-complete. Both results rest on a structural fact proved first: whenever such a market has an equilibrium at all, it has one whose prices are rational numbers of polynomial bit length. That fact is the subject of this mission.

Timeline:

1959, Eisenberg and Gale: a convex program whose optimal solutions are the equilibria of linear Fisher markets; equilibrium prices are rational.
2008, Devanur, Papadimitriou, Saberi and Vazirani: a combinatorial polynomial-time algorithm for linear Fisher markets, based on a max-flow test of candidate prices.
2009, Chen, Dai, Du and Teng, and Chen and Teng (FOCS 2009; ISAAC 2009): PPAD-hardness for additively separable piecewise-linear concave utilities in Arrow–Debreu and Fisher markets.
2011, Vazirani and Yannakakis: rationality of equilibria with polynomial bit size (Theorem 4.1 for Fisher markets, Theorem 5.1 for Arrow–Debreu markets), PPAD membership, and NP-completeness of existence.

Setting

There are $n$ buyers $B=\{1,\dots,n\}$ and $g$ divisible goods $G=\{1,\dots,g\}$ , one unit of each good. Buyer $i$ has a rational budget $e(i)>0$ . For each buyer $i$ and good $j$ a function $f^i_j:\mathbb R_+\to\mathbb R_+$ gives the utility that $i$ derives from an amount of good $j$ . It is piecewise linear and concave: it is given by a finite list of bounded segments $(c_1,a_1),\dots,(c_m,a_m)$ with rational amounts $a_k>0$ , followed by a last, unbounded segment, with rational slopes $c_1\ge c_2\ge\dots\ge c_m\ge c_\infty\ge 0$ . The function has slope $c_k$ on $[a_1+\dots+a_{k-1},\,a_1+\dots+a_k]$ and slope $c_\infty$ afterwards. Buyer $i$ 's utility for a bundle $x=(x_1,\dots,x_g)$ is additively separable:

u_i(x)=\sum_{j\in G}f^i_j(x_j).

Given prices $p\in\mathbb R^g_{\ge0}$ , a bundle $x\ge0$ is optimal for buyer $i$ if $\sum_jp_jx_j\le e(i)$ and no bundle $y\ge0$ with $\sum_jp_jy_j\le e(i)$ has $u_i(y)>u_i(x)$ . The prices $p$ are equilibrium prices if there is an allocation $(x_{ij})$ that gives each buyer an optimal bundle and sells every good exactly: $\sum_ix_{ij}=1$ for every $j$ .

The bit size of a rational number $a/b$ in lowest terms is the binary length of $|a|$ plus that of $b$ . The encoding size $\|M\|$ of a market $M$ is $n+g$ plus the bit sizes of all budgets, slopes and amounts, plus the number of bounded segments.

For the intermediate results, fix positive prices $p$ . The bang per buck of a segment $s$ of good $j$ is $\mathrm{slope}(s)/p_j$ and its value is $\mathrm{amount}(s)\cdot p_j$ (infinite for an unbounded segment). Sorting buyer $i$ 's segments by decreasing bang per buck into classes of equal bang per buck, the first class at which the cumulative value exceeds $e(i)$ is her flexible class. Segments of strictly larger bang per buck are forced, the others undesirable. From these the paper defines $\mathrm{spent}(i)$ (value of the forced segments), $\mathrm{unspent}(i)=e(i)-\mathrm{spent}(i)$ , $\mathrm{unsold}(j)$ (the part of good $j$ not taken by forced segments), and a network $N(p)$ from a source through goods and buyers to a sink.

Formalization targets

Goal: Theorem 4.1 (p. 10:9)

There is a polynomial $P$ such that for every Fisher market $M$ as above,

M\text{ has equilibrium prices }p\in\mathbb R^g\ \Longrightarrow\ M\text{ has equilibrium prices }q\in\mathbb Q^g\text{ with }\sum_{j}\operatorname{bits}(q_j)\le P(\|M\|).

The polynomial is fixed before the market. Nothing beyond the existence of some real equilibrium is assumed.

Milestones

Lemma 3.1 (p. 10:8). For positive prices with $\sum_jp_j=\sum_ie(i)$ , $\mathrm{unspent}\ge0$ and $\mathrm{unsold}\ge0$ : $p$ are equilibrium prices iff the max-flow value of $N(p)$ is $\sum_i\mathrm{unspent}(i)$ .
Proof of Theorem 4.1, first sentence (p. 10:9). From a positive equilibrium $p'$ with $\sum_jp'_j=\sum_ie(i)$ , build the linear program of §4, whose variables are prices and flows and whose combinatorial data are fixed by $p'$ . Then $p'$ , with a suitable flow, is an optimal solution of value $\sum_ie(i)$ .
§4, second paragraph (p. 10:8). Every optimal solution of that LP with positive prices gives equilibrium prices.

Significance

The result is what makes the existence problem for these markets a problem in NP: a rational equilibrium of polynomial size is a certificate that can be checked, with Lemma 3.1, by one max-flow computation. The same rationality statement underlies the paper's PPAD-membership proof and its NP-completeness result for existence. It also marks the boundary with markets whose equilibria can be irrational, as happens for some non-separable utilities. In that sense it shows that separable piecewise-linear concave utilities keep the "linear" character of the problem even though computing an equilibrium becomes hard.

All three statements are proved in the source, and none of them has a machine-checked proof on the platform or, as far as is known, anywhere else. The mission produces the first formal account of piecewise-linear Fisher markets: the model, the forced/flexible/undesirable classification of segments, the max-flow test for equilibrium, and the linear program of §4. It also forces precision where the paper is informal. The §4 bang-per-buck inequalities are printed with their directions reversed, and the claim about optimal LP solutions needs positive prices. The formal statements record each of these choices.

Difficulty

The obvious argument is: "equilibria are solutions of a linear system, so a rational one exists". It fails as stated, because the set of equilibrium prices is not a polyhedron. Which segments a buyer buys depends on the prices themselves, through the ordering of the ratios $\mathrm{slope}/p_j$ , so the equilibrium conditions are a finite union of polyhedral pieces glued along the price-dependent ordering. The work is to freeze the combinatorial structure of one given equilibrium and to show that the resulting fixed linear program still certifies equilibrium at every one of its optimal points. That second step is what Lemma 3.1 is for. The polynomial bit bound then needs a quantitative bound on the vertices of a rational LP, uniform in the market's encoding.

Formalization scope

Buyers and goods are Fin n and Fin g. Budgets, slopes and amounts are rationals (ℚ). Prices and allocations are reals (ℝ), so that "admits rational prices" is a real conclusion: the goal returns q : Fin g → ℚ whose cast is an equilibrium. The committed conventions are:

each good has unit supply;
budgets are positive;
each $f^i_j$ is a list of (slope, amount) pairs of bounded segments together with the slope of its last, unbounded segment ("the last (infinite) segment", §6), with nonnegative slopes, positive amounts and nonincreasing slopes, stored inside the market structure;
the unbounded segment has infinite value and, when flexible, gives its network edge infinite capacity; this is encoded logically (no upper bound on that edge);
equilibrium requires exact clearing of every good, which by the paper's footnote 3 gives the same equilibrium prices as leaving zero-price goods partly unsold;
the classes $Q_l$ are represented by the bang per buck of the flexible class, not by an index;
parallel network edges are merged;
max-flow is the supremum of the values of feasible flows on the good–buyer edges.

Hypotheses added relative to the page, each disclosed in its statement:

positivity of the LP solution's prices (milestone 3).

The §2 condition on p. 10:7 is a sufficient condition for existence and is deliberately not a hypothesis of the goal, which assumes only that an equilibrium exists. Complexity-class statements ("in NP", "PPAD-complete") are out of scope. What is formalized is the explicit polynomial bit bound, with a polynomial chosen before the market. A goal with the polynomial chosen after the market, an encoding size that ignores the bits of the data, or an equilibrium notion without utility-maximizing bundles would be trivially satisfiable. The statements rule all three out.

Beyond this mission, a complete development needs LP theory with rational data: existence of optimal basic solutions and determinant bounds on their bit size. Existing platform results that may serve as substrate include SmaleNinth.exists_square_subsystem and SmaleNinth.abs_det_le_factorial_mul_pow. Contributions welcome: proofs of the milestones, a reusable bit-size theory for rational LP vertices, and the Arrow–Debreu analogue (Theorem 5.1).

Selected references

V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, J. ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
N. R. Devanur, C. H. Papadimitriou, A. Saberi and V. V. Vazirani, Market Equilibrium via a Primal–Dual Algorithm for a Convex Program, J. ACM 55(5), 2008. https://doi.org/10.1145/1411509.1411512
E. Eisenberg and D. Gale, Consensus of Subjective Probabilities: The Pari-Mutuel Method, Ann. Math. Statist. 30(1), 1959. https://doi.org/10.1214/aoms/1177706369
X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, FOCS 2009. https://doi.org/10.1109/FOCS.2009.29
W. C. Brainard and H. E. Scarf, How to Compute Equilibrium Prices in 1891, Cowles Foundation Discussion Paper 1272, 2000. https://cowles.yale.edu/research/cfdp-1272

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Optimization+1·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem II: Every Insertion Method Is Within ⌈lg n⌉ + 1 of the Optimal TourResearch Paper

Motivation

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.

Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most $\lceil \lg n\rceil + 1$ times longer than an optimal one (Theorem 3, p. 571).

Timeline. 1977: Rosenkrantz, Stearns and Lewis prove $\lceil\lg n\rceil+1$ for every insertion method (Theorem 3), $\tfrac12(\lceil\lg n\rceil+1)$ for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant $2$ for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio $\Omega(\log n/\log\log n)$ , so the logarithmic growth cannot be replaced by a constant for the family as a whole.

Setting

A traveling salesman graph with $n$ nodes consists of a finite node set $N$ with $|N|=n$ and a distance $d:N\times N\to\mathbb R$ with $d(i,j)=d(j,i)$ , $d(i,j)\ge 0$ and $d(i,j)+d(j,k)\ge d(i,k)$ for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.

A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour $T$ and a node $k\notin T$ , TOUR $(T,k)$ is obtained by choosing an edge $(x,y)$ of $T$ minimizing

d(x,k)+d(k,y)-d(x,y)

and replacing it by the edges $(x,k)$ and $(k,y)$ ; if $T$ is a single node $i$ , TOUR $(T,k)$ is the two-node tour $(i,k),(k,i)$ . COST $(T,k)$ is the length of TOUR $(T,k)$ minus the length of $T$ .

An insertion method constructs subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ a single node and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some node $a_i\notin T_i$ , $1\le i<n$ . The final tour $T_n$ is the approximation, and INSERT denotes its length. No rule for choosing the $a_i$ is fixed, and ties between minimizing edges are broken arbitrarily.

Write $\lg$ for the logarithm to base 2 and $\lceil x\rceil$ for the least integer $\ge x$ .

Formalization targets

Goal: Theorem 3

For every traveling salesman graph with $n\ge 1$ nodes and every run of every insertion method,

\mathrm{INSERT}\ \le\ \bigl(\lceil\lg n\rceil+1\bigr)\cdot\mathrm{OPTIMAL}.

Milestones

(2.2), shortcutting: visiting a subset of the nodes in the order of a tour gives a tour of the subset that is no longer.
(2.1): if the numbers $l_1\ge\dots\ge l_n$ satisfy $d(p,q)\ge\min(l_p,l_q)$ for distinct $p,q$ , then $\mathrm{OPTIMAL}\ge 2\sum_{i=k+1}^{\min(2k,n)} l_i$ for $1\le k\le n$ .
Lemma 1: if $d(p,q)\ge\min(l_p,l_q)$ for distinct nodes and $l_p\le\frac12\mathrm{OPTIMAL}$ for all $p$ , then

\sum_p l_p\le\tfrac12\bigl(\lceil\lg n\rceil+1\bigr)\mathrm{OPTIMAL}.

Lemma 2: $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for every node $j$ of $T$ .
(3.7): $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$ .
(3.10): $\mathrm{COST}(T_i,a_i)\le 2\,d(a_i,a_j)$ whenever $j<i$ .
(3.12): $\mathrm{COST}(T_i,a_i)\le\mathrm{OPTIMAL}$ for $1\le i<n$ .

Significance

The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of $\lceil\lg n\rceil+1$ from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant $2(1-1/n)$ (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.

Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.

Difficulty

The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up $n-1$ costs each at most OPTIMAL, gives only the ratio $n-1$ . The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.

Formalization scope

Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length $d(x_0,x_1)+\dots+d(x_{m-1},x_0)$ . TOUR $(T,k)$ is encoded as inserting $k$ at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of $T$ and raises the length by exactly $d(x,k)+d(k,y)-d(x,y)$ , so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept ( $T_1=[a_0]$ , $T_n$ final). $\lceil\lg n\rceil$ is Nat.clog 2 n. All quantities are real.

Conventions and deviations, each disclosed in the item statements:

The distance satisfies $d(i,i)=0$ , a normalization not in the paper; a loop never enters any length.
Ratios are multiplied out ( $\mathrm{INSERT}\le c\cdot\mathrm{OPTIMAL}$ ), so the paper's exclusion of the identically zero distance (1.1) is not needed.
Condition a) of Lemma 1 is required for distinct nodes only. The page says "for all nodes $p$ and $q$ ", which for $p=q$ would force every $l_p\le 0$ and make the lemma inapplicable in the proof of Theorem 3; the proof uses the condition only on edges of a tour.
(2.2) is stated for every subset of the nodes and every tour, which is what the shortcut argument shows; the paper applies it to one specific subset and an optimal tour.
(2.1) uses 0-based node labels, so its range $k+1,\dots,\min(2k,n)$ becomes $k,\dots,\min(2k,n)-1$ .

The goal quantifies over every run: any choice of the inserted nodes $a_i$ and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL $=0$ or to a fixed small $n$ would trivialize it.

Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.

Selected references

D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
V. Bafna, B. Kalyanasundaram, K. Pruhs, Not all insertion methods yield constant approximate tours in the Euclidean plane, Theoretical Computer Science 125(2):345–353, 1994.

10 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Robust Mean-Covariance Solutions for Stochastic Optimization I: The General Projection Property of Mean-Covariance Distribution ClassesResearch Paper

Motivation

In robust stochastic optimization a decision maker chooses a decision $x$ whose outcome depends on a random vector $\mathbf R$ , but knows only the first two moments of $\mathbf R$ : its mean vector $\mu$ and its covariance matrix $\Sigma$ . The decision is evaluated by its worst-case expected utility over every distribution consistent with those moments. This model is standard in portfolio selection, where estimated means and covariances are the usual inputs, and in pricing and inventory problems with mean-variance information. It goes back to Scarf's min-max newsvendor (1958) and the Chebyshev-type moment bounds of Bertsimas and Popescu (2005).

For a linear outcome $x'\mathbf R$ , such as the return of a portfolio with weights $x$ , the robust objective is

U(x) = \min_{\mathbf R \sim (\mu,\Sigma)} E[u(x'\mathbf R)],

an optimization over an infinite-dimensional set of $n$ -variate distributions. Popescu (2007) showed that this problem depends on $\mu$ and $\Sigma$ only through the scalar mean $\mu_x = x'\mu$ and variance $\sigma_x^2 = x'\Sigma x$ . The multivariate robust problem then reduces to a univariate moment problem, and for many utilities to a parametric quadratic program. The reduction rests on one structural fact, the general projection property, which this mission formalizes.

Setting

Fix a dimension $n$ . A law on $\mathbb R^n$ is a Borel probability measure on $\mathbb R^n$ . For a vector $\mu \in \mathbb R^n$ and a real $n\times n$ matrix $\Sigma$ , the mean-covariance class $\mathbb M^n_{(\mu,\Sigma)}$ is the set of laws $P$ under which every coordinate $R_i$ has a finite second moment and

\int R_i\,dP(R) = \mu_i, \qquad \int (R_i-\mu_i)(R_j-\mu_j)\,dP(R) = \Sigma_{ij} \qquad (1\le i,j\le n).

Writing $\mathbf R \sim (\mu,\Sigma)$ means that the law of $\mathbf R$ lies in $\mathbb M^n_{(\mu,\Sigma)}$ . For $n=1$ the superscript is dropped: for real $m$ and $v$ , $\mathbb M_{(m,v)}$ is the set of laws on $\mathbb R$ with finite second moment, mean $m$ and variance $v$ .

For a vector $x \in \mathbb R^n$ , the $x$ -projection sends the law $P$ of $\mathbf R$ to the law of the scalar $\mathbf r = x'\mathbf R$ , that is, to the pushforward of $P$ under $R \mapsto x'R$ . Write $\mu_x = x'\mu$ and $\sigma_x^2 = x'\Sigma x$ . The matrix $\Sigma$ is positive semidefinite, $\Sigma \succeq 0$ , when $x'\Sigma x \ge 0$ for all $x$ (and $\Sigma$ is symmetric); $\Sigma^{1/2}$ denotes its positive semidefinite square root.

Formalization targets

Goal: Theorem 1 (General Projection Property)

For every $\mu \in \mathbb R^n$ , every $\Sigma \succeq 0$ and every nonzero $x \in \mathbb R^n$ , the $x$ -projection maps $\mathbb M^n_{(\mu,\Sigma)}$ into and onto $\mathbb M_{(\mu_x,\sigma_x^2)}$ :

\bigl\{\, \text{law of } x'\mathbf R \;:\; \mathbf R \sim (\mu,\Sigma) \bigr\} \;=\; \mathbb M_{(x'\mu,\; x'\Sigma x)}.

The "into" half says every projected law has the right mean and variance. The "onto" half says that every univariate law with mean $\mu_x$ and variance $\sigma_x^2$ , however heavy-tailed or irregular, is the law of $x'\mathbf R$ for some $\mathbf R \sim (\mu,\Sigma)$ . The degenerate case $x'\Sigma x = 0$ is included.

Milestones

The into half (§2.1, justification of (4)): $x'\mathbf R$ has mean $x'\mu$ and variance $x'\Sigma x$ .
The degenerate case: if $x'\Sigma x = 0$ then $x'\mathbf R = x'\mu$ almost surely.
Standardization: if $\mathbf r \sim (m, v)$ with $v > 0$ , then $v^{-1/2}(\mathbf r - m) \sim (0,1)$ .
Normalization: for $x'\Sigma x > 0$ , the vector $y = (x'\Sigma x)^{-1/2}\Sigma^{1/2}x$ satisfies $y'y = 1$ .
Isotropic lift: if $y'y = 1$ and $\mathbf z \sim (0,1)$ , there is $\mathbf Z \sim (0, I_n)$ with $y'\mathbf Z$ distributed as $\mathbf z$ .
Affine image: if $\mathbf Z \sim (0,I_n)$ then $\mu + \Sigma^{1/2}\mathbf Z \sim (\mu,\Sigma)$ , and $x'(\mu + \Sigma^{1/2}Z) = x'\mu + (x'\Sigma x)^{1/2}\,y'Z$ for every $Z$ .

Significance

The result. Theorem 1 immediately yields Proposition 1 of the paper: for every objective $u$ ,

\min_{\mathbf R\sim(\mu,\Sigma)} E[u(x'\mathbf R)] = \min_{\mathbf r\sim(\mu_x,\sigma_x^2)} E[u(\mathbf r)],

with minima in the wide sense of infima. The robust objective is therefore a function of $(\mu_x, \sigma_x)$ alone, which makes every robust mean-covariance problem with a linear outcome a bicriteria mean-variance problem. The paper's later results use this: the two-point and one-point support properties, the parametric quadratic programming solution, and the portfolio applications (bonus schemes, value at risk). The projection property holds with no assumption on $u$ , so it serves non-concave, discontinuous and quantile-based objectives alike.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. The mission produces a formal definition of mean-covariance classes that treats integrability honestly, a proof of the projection property, and through it a formally verified reduction of multivariate moment-robust problems to univariate ones. The paper's own construction of the lifted vector has a gap (see Difficulty), so a formal proof also records a corrected argument.

Difficulty

The into half is a computation with linearity of expectation. The difficulty is entirely in the onto half. Given an arbitrary univariate law with prescribed mean and variance, one must build an $n$ -variate law with a prescribed full covariance matrix whose one-dimensional marginal in direction $x$ is exactly the given law. This is a coupling problem: the obvious approach, taking independent coordinates, fixes the marginal in direction $x$ as a convolution and cannot reproduce an arbitrary target. Taking $\mathbf R$ supported on the line through $\mu$ in a single direction reproduces the target law but has a rank-one covariance and fails whenever $\Sigma$ has rank above one.

The paper's appendix constructs the lift through conditional distributions of the remaining coordinates given the projected one. As printed, the conditional second-moment requirement it imposes cannot hold for unbounded targets, so that argument does not go through verbatim. The milestone for the lift states only the claim, not the printed construction.

The integrability bookkeeping is real work: every intermediate law must be shown to have finite second moments before its moments can be computed.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Borel σ-algebra; $x'R$ is the inner product $\langle x, R\rangle$ ; $x'\Sigma x$ is x.ofLp ⬝ᵥ S *ᵥ x.ofLp, where the matrix $\Sigma$ is named S (the symbol Σ is reserved in Lean).
Laws are probability measures. Both classes require finite second moments (MemLp … 2), so that means and covariances are genuine integrals, not the default value $0$ that Lean assigns to non-integrable functions. The univariate class is parametrized by the variance $v = \sigma^2$ , not by $\sigma$ .
The projection is the pushforward P.map (fun R => ⟪x, R⟫) under a continuous map. "Pathwise" identities in the paper become equalities of pushforward laws, or pointwise algebraic identities.
$\Sigma^{1/2}$ is CFC.sqrt S, acting through Matrix.toEuclideanCLM, as in Mathlib's multivariateGaussian.
The goal is stated as Set.MapsTo ∧ Set.SurjOn with both classes explicit. Its only hypotheses are $\Sigma \succeq 0$ and $x \ne 0$ , as in the paper. No bound on $n$ , no invertibility of $\Sigma$ and no positivity of $x'\Sigma x$ is assumed. Restricting the target to Gaussian, bounded or finitely supported laws, or dropping the finite-second-moment clause (which would admit Cauchy laws as "mean 0, variance 0"), would trivialize or change the theorem and is ruled out.
Milestones 3, 4 and 6 assume $x'\Sigma x > 0$ (or $v > 0$ ), the case the proof treats after its first sentence; milestone 2 covers the complementary case.

Needed infrastructure: moments of pushforwards under linear and affine maps, a covariance calculus for coordinates of random vectors, and a coupling that realizes the isotropic lift. Mathlib's multivariateGaussian, stdGaussian and CFC.sqrt are available. A reusable lemma "the covariance of $A\mathbf Z + b$ is $A\,\mathrm{Cov}(\mathbf Z)A'$ " would serve beyond this mission. Related platform work on moment-based ambiguity sets: Wasserstein Distributionally Robust Optimization II. Contributions of any milestone, and alternative proofs of the lift, are welcome.

Selected references

I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903
H. Scarf, A Min-Max Solution of an Inventory Problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
W. W. Rogosinski, Moments of Non-Negative Mass, Proceedings of the Royal Society A 245:1–27, 1958. https://doi.org/10.1098/rspa.1958.0062

10 thms2 active usersReviewed

Optimization Probability Statistics+1·Captain: mikedeng1

Acceleration of Stochastic Approximation by Averaging: Almost-Sure Convergence and Asymptotic Normality of the Averaged IterateResearch Paper

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$ , by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$ . It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$ , which requires knowing $G$ .

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$ : run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

1951, Robbins and Monro: the recursion and its convergence in probability.
1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$ .
1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$ -valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$ , algorithm (7) is

x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$ .

The hypotheses are:

Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$ , Lipschitz gradient, $V(0)=0$ , $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$ , and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$ .
Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$ , with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$ . It splits as $\xi_t=\xi_t(0)+\zeta_t$ , where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$ .
Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ , $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$ , $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$ .

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).

Milestones

Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$ .
Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$ .
Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$ .
Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$ , $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$ .

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$ " is written with shifted indices ( $\xi_{t+1}$ given $\mathcal F_t$ ). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$ , with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$ . Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$ – $\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$ . Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$ ). The drift constant is renamed $\lambda_1$ , since the paper uses $\lambda$ also in Assumption 3.2.
Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$ , the form of Assumptions 4.7 and 5.6 and of p. 851.
Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$ .
$\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
$R$ is assumed continuous. The paper states no regularity of $R$ , but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$ , which continuity and Assumption 3.1 provide.
Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ( $A=\mathrm{diag}(1,10)$ , $\gamma=1$ ), and Theorem 2 does not use it.
(A3) is stated with the norm inside, as its proof establishes.
(A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$ . The printed $+$ signs contradict (A8) at $t=2$ .

Several formalizations would make the goal trivial, and all are ruled out:

conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$ );
a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
an arbitrary process with a property in place of the recursion (7);
a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

10 thms2 active usersReviewed

Convex Optimization Linear algebra Linear Optimization+1·Captain: mikedeng1

Path-Finding Methods for Linear Programming II: Properties of the Regularized D-Optimal-Design Weight FunctionResearch Paper

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$ , where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$ , defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$ , and $1\le n<m$ . For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$ , $W=\mathrm{diag}(w)$ , $W^\alpha=\mathrm{diag}(w_i^\alpha)$ , and $A_s=S^{-1}A$ . For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$ .

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$ , and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$ , with $G(s)=\mathrm{diag}(g(s))$ , $G'(s)$ the Jacobian of $g$ at $s$ , and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$ :

Size: $\|g(s)\|_1\le c_1$ ;
Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$ ;
Step consistency: $c_r\ge1$ and for all $r\ge c_r$ , $y\in\mathbb R^m$ : $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$ ;
Uniformity: $\|g(s)\|_\infty\le2$ .

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$ ,

\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$ , and the resulting $g$ is a weight function with

c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .

Milestones: the three bullets of Theorem 1

Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$ .
Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$ .
Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$ .

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ -iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$ -sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$ . The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$ , and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$ ) and $A^\top W^\alpha A$ (which defines $g$ ). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$ , $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$ -norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$ , and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$ , and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$ ).
$1\le n<m$ . $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$ ; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
Reading of $\alpha$ : the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$ , giving $\alpha\in(0,1)$ .
Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$ , while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$ ).
The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$ .
$g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$ . Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

7 thms2 active usersReviewed

Operations Research

Missions

Conditional and Dynamic Convex Risk Measures I: Robust Representation of Conditional Convex Risk MeasuresResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimizing Static Linear Feedback: Gradient Method I: The Gradient Method Converges to a Stationary Point, and Linearly to the Optimal Gain under State FeedbackResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.2 for state feedback

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 1: The Augmentation Bound for Shortest Augmenting PathsResearch Paper

Why the number of augmentations matters

Setting

Formalization targets

Goal — Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Three-Operator Splitting Scheme and its Optimization Applications 2: The Objective Rate of the Weighted Ergodic IterateResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 (p. 840)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Three-Operator Splitting Scheme and its Optimization Applications 1: Weak and Strong Convergence of the Three-Operator Splitting IterationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1 (Main convergence theorem)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Generalized Gradients and Applications I: The Generalized Gradient of a Max FunctionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem (2.1)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Minimizing a Convex Function Subject to Linear Inequalities II: Optimality Conditions for the Sum of the Largest Linear FormsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (a), p. 179

Milestones

Significance

Difficulty

Formalization scope

Selected references

Revenue Management of a Make-to-Stock Queue: Exponential Stationary Density under Normal Reflection (Proposition 2)Research Paper

Motivation

Setting

Formalization targets

Goal: the exponential density satisfies the BAR under conormal reflection

Milestones

Significance

Difficulty