Optimization

Algorithmic Game Theory Linear Optimization·Captain: mikedeng1

Bimatrix Equilibrium Points and Mathematical Programming: If Z Is Non-Degenerate and uᵀMu ≥ 0, uᵀMu = 0 ⇒ Mu + Mᵀu = 0 for All u ≥ 0, a Non-Empty Z Has an Equilibrium PointResearch Paper

Motivation

The linear complementarity problem asks, for a real square matrix $M$ of order $n$ and a vector $q\in\mathbb R^n$ , for a vector $z$ with

z\ge 0,\qquad w=Mz-q\ge 0,\qquad z^{\mathsf T}w=0 .

It is the common form of the Kuhn–Tucker conditions of linear and convex quadratic programs and of the equilibrium conditions of two-person non-zero-sum (bimatrix) games. In 1964 Lemke and Howson gave a constructive existence proof for equilibrium points of bimatrix games by following a path of adjacent extreme points of a polyhedron (Lemke–Howson 1964). In 1965 Lemke adapted that path-following technique to the general problem above, under a condition on $M$ that covers the positive semidefinite case treated by Dantzig and Cottle and the case $M>0$ (Lemke 1965). The resulting procedure, now called Lemke's algorithm or complementary pivoting, became a standard method for linear complementarity problems and a template for later path-following existence proofs (Cottle, Pang, Stone 1992).

Timeline:

1964: Lemke and Howson, adjacent-extreme-point path for bimatrix games.
1965: Lemke, existence for matrices satisfying conditions (i)–(ii) below (the goal of this mission), under a non-degeneracy assumption, by an augmented path with an artificial variable $z_0$ .
Later literature names matrices with (i)–(ii) copositive-plus, and removes non-degeneracy by lexicographic perturbation.

Setting

Fix a finite index set of size $n$ , a real $n\times n$ matrix $M$ and $q\in\mathbb R^n$ . Inequalities between vectors are componentwise and $e$ is the all-ones vector.

The set $Z=\{z\in\mathbb R^n : z\ge 0,\ w=Mz-q\ge 0\}$ ; $w$ is always the function $Mz-q$ of $z$ .
An equilibrium point is a point $z\in Z$ with $z^{\mathsf T}w=0$ ; $S$ is the set of them.
For any $z\in\mathbb R^n$ , the matrix $N(z)$ consists of the columns of $(M^{\mathsf T},I)$ that are kept when one deletes the $i$ -th column of $M^{\mathsf T}$ whenever $w_i\ne 0$ and the $i$ -th column of $I$ whenever $z_i\ne0$ .
An extreme point of $Z$ is a point $z\in Z$ with $\operatorname{rank}N(z)=n$ ; $z$ lies on an open edge if $z\in Z$ and $\operatorname{rank}N(z)=n-1$ . An open edge is the set of points of $Z$ sharing the matrix $N(z)$ of such a point; a ray is an open edge with exactly one end-point.
$Z$ is non-degenerate if for every $z\in\mathbb R^n$ the columns of $N(z)$ are linearly independent.
For an index $s$ , $Z_s=\{z\in Z : z^{\mathsf T}w=z_sw_s\}$ . An adjacency path is a non-empty connected class of closed edges of $Z$ no three of which meet; its end-points are the extreme points lying on exactly one of its edges.
The augmented sets: $Z^*=\{(z,z_0) : z\ge0,\ z_0\ge0,\ Mz+z_0e-q\ge0\}$ , its subset $Z_0^*$ where $z^{\mathsf T}w=0$ , and, for a number $k$ , $Z^{**}$ , the set of the form above for the bordered data $\begin{pmatrix}M&e\\-e^{\mathsf T}&0\end{pmatrix}$ , $\begin{pmatrix}q\\-k\end{pmatrix}$ .

Formalization targets

Goal: Theorem 4 (p. 7)

Suppose $Z$ is non-degenerate and that for every $u\ge0$

\text{(i)}\ u^{\mathsf T}Mu\ge 0,\qquad \text{(ii)}\ u^{\mathsf T}Mu=0\ \Longrightarrow\ Mu+M^{\mathsf T}u=0 .

Then

Z\ne\emptyset\ \Longrightarrow\ \exists z\in Z,\ z^{\mathsf T}(Mz-q)=0 .

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

Theorem 1 (p. 3): for non-degenerate $Z$ , $Z_s$ is empty or a disjoint union of adjacency paths whose end-points are exactly the equilibrium points.
Lemma 2 (p. 4): $Z=\emptyset$ iff some $u\ge0$ has $M^{\mathsf T}u\le0$ , $u^{\mathsf T}q>0$ .
Theorem 2 (p. 4): if some $Z_s$ contains precisely one ray of a non-degenerate $Z$ , the number of equilibrium points is odd.
p. 6: for $k$ chosen as in (12), the starting ray $E_0^*$ ( $z=0$ ) is a ray of $Z^{**}$ inside $Z_0^{**}$ , and it is the only one.
Lemma 2 (p. 6): $Z^{**}$ has an equilibrium point.
Lemma 3 (p. 7): a ray $(\bar z+\theta u,\bar z_0+\theta u_0)$ of $Z^*$ in $Z_0^*$ with $e^{\mathsf T}u=1$ satisfies $u^{\mathsf T}Mu+u_0=0$ .
(22)–(25) (pp. 7–8): under (i)–(ii) such a ray has $\bar z_0=0$ and $\bar z$ an equilibrium point of $Z$ , or $\bar z_0>0$ and $Z=\emptyset$ .

Companion results

The Corollary (p. 5: $q=e$ , $M>0$ gives an odd number of equilibrium points), Theorem 3 (p. 5: if $z^{\mathsf T}Mz\ge0$ for all $z$ , at most one equilibrium point) and Theorem 5 (p. 8: if moreover $Z\ne\emptyset$ , $Z$ has at least $n$ rays).

Significance

Theorem 4 is an existence theorem for a class of linear complementarity problems that contains convex quadratic programming (the case $z^{\mathsf T}Mz\ge0$ for all $z$ ) and strictly positive matrices, and its proof is an algorithm: the path followed is the sequence of pivots of Lemke's method. The parity statements (Theorem 2, the Corollary) are an early instance of the path-following parity arguments later abstracted in the complexity class PPAD (Papadimitriou 1994).

The theorem is classical and proved. To our knowledge neither Lemke's theorem nor the polyhedral path machinery of Theorems 1–2 has a machine-checked proof in Lean or Mathlib. This mission produces the vocabulary of non-degenerate complementarity polyhedra (the matrix $N(z)$ , open edges, rays, adjacency paths), the parity theorem, and the existence theorem itself; the Farkas-type Lemma 2 (p. 4) is already available on the platform.

Difficulty

The algebraic part (Lemma 3 and (22)–(25)) is short. The difficulty is combinatorial-geometric: Theorem 1 requires that, under non-degeneracy, every extreme point of $Z$ has exactly $n$ incident edges, that each point of $Z_s$ is an extreme point or lies on an open edge, and that the edges contained in $Z_s$ form paths whose end-points are exactly the equilibrium points; the parity of Theorem 2 then needs finiteness of the set of extreme points. None of this polyhedral structure (edges as zero-pattern classes, their closures and end-points) is in Mathlib. Moreover, the printed proof of Theorem 4 applies Theorem 2 to $Z^{**}$ , whose non-degeneracy the paper obtains from an informal perturbation remark, and it sketches the step from the end of the augmented path to a ray of $Z^*$ ; a complete proof of the goal must supply these steps or take another route.

Formalization scope

Vectors are functions from a finite index type $\iota$ to $\mathbb R$ ( $n=|\iota|$ ; $\mathrm{Fin}\,n$ is a special case); the bordered system lives on $\iota\oplus\{\ast\}$ . $w$ is always $Mz-q$ , never a free variable.
$N(z)$ is the indexed family of its columns, $\operatorname{rank}N(z)$ the dimension of their span; " $\operatorname{rank}N(z)=n-1$ " is written $\operatorname{rank}N(z)+1=n$ .
Non-degeneracy (Def. 3) is linear independence of the columns of $N(z)$ for every $z\in\mathbb R^n$ . The phrase "(but not all)" is read as excluding only the empty matrix; the other reading differs only when $q=0$ , and the formal definition is then the stronger hypothesis.
An open edge is the set of points of $Z$ with the zero pattern of a point $z_0$ with $\operatorname{rank}N(z_0)=n-1$ ; closed edges are closures; end-points of an open edge $E$ are the points of $\overline E\setminus E$ ; a ray has exactly one. Adjacency paths are classes of closed edges.
Conditions (i)–(ii) are quantified over $u\ge0$ only. "Non-negative definite" (Theorems 3, 5) is $z^{\mathsf T}Mz\ge0$ for all $z$ , with no symmetry assumed.
"An odd number" is finiteness plus odd cardinality; "at least $n$ rays" counts rays as an extended natural number; "at most one" is a subsingleton.
Equilibrium points include membership in $Z$ : $z^{\mathsf T}(Mz-q)=0$ alone holds at $z=0$ and would make the goal trivial. The goal mentions neither $Z^*$ , $Z^{**}$ , $k$ , rays nor paths; in particular non-degeneracy of $Z^{**}$ is not a hypothesis of the goal.
Deviations: Lemma 2 (p. 6) assumes non-degeneracy of $Z^{**}$ (Def. 3 does not define it for the non-square $Z^*$ ); milestone 4 holds for every $k$ without non-degeneracy; Lemma 3 and (22)–(25) parametrize the ray as in (15) without requiring $\bar z^*$ to be an extreme point, which makes them stronger.

Contributions welcome: the polyhedral lemmas for non-degenerate $Z$ (extreme points have $n$ edges, finitely many extreme points), the parity argument, and any complete route to Theorem 4.

Selected references

C. E. Lemke, Bimatrix Equilibrium Points and Mathematical Programming, Management Science 11(7):681–689, 1965. https://doi.org/10.1287/mnsc.11.7.681 (cited from the HAL deposit hal-01885823v1)
C. E. Lemke, J. T. Howson, Equilibrium Points of Bimatrix Games, J. SIAM 12(2):413–423, 1964. https://doi.org/10.1137/0112033
R. W. Cottle, J.-S. Pang, R. E. Stone, The Linear Complementarity Problem, Academic Press 1992; SIAM Classics 2009. https://doi.org/10.1137/1.9780898719000
C. H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Computer and System Sciences 48(3):498–532, 1994. https://doi.org/10.1016/S0022-0000(05)80063-7

10 thms3 active usersReviewed

Convex Optimization Operations Research Stochastic Systems·Captain: mikedeng1

Loss Networks 1: The Primal Problem Has a Unique Optimum x_r = ν_r ∏_j (1 − B_j)^{A_jr}; the Conditions on B Are Solvable, Uniquely if rank A = J, and Biject with Dual OptimaResearch Paper

Motivation

A loss network carries calls that require capacity on one or more links. A call is accepted only when every required link has enough free circuits; otherwise it is lost. This makes the traffic on different links dependent even when calls on different routes arrive independently. Network operators need to know where capacity constraints bind and how offered traffic is converted into carried traffic. Kelly's 1991 survey develops a continuous optimization problem that identifies a characteristic flow vector and gives a linkwise description of blocking in this setting. Kelly, Loss networks (1991), §§1.2 and 2.1.

The paper begins with the equilibrium distribution of the discrete network and uses a continuous relaxation when analyzing its likely state. The resulting primal problem is useful beyond the original probability calculation because it links route flows, capacity constraints, and a convex dual. Theorem 2.8 collects the existence, uniqueness, and correspondence statements for these descriptions. This mission targets that theorem and the intermediate claims Kelly states in §2.1. Kelly (1991), pp. 327–329.

Setting

There are finitely many links $j$ and finitely many routes $r$ . Link $j$ has $C_j$ circuits, and one call on route $r$ uses $A_{jr}$ circuits there, with $A_{jr}$ a nonnegative integer. Calls request route $r$ at positive offered rate $\nu_r$ . The matrix $A$ need not be a zero–one incidence matrix: one call may use more than one circuit on a link. Kelly's fixed-routing model and its general integer matrix are described in §1.2. Kelly (1991), p. 321.

A real route-flow vector $x=(x_r)$ is primal feasible if $x_r\ge0$ for every route and $\sum_r A_{jr}x_r\le C_j$ for every link. The objective is

F(x)=\sum_r\bigl(x_r\log\nu_r-x_r\log x_r+x_r\bigr),

with $x_r\log x_r=0$ at $x_r=0$ . The primal optimum maximizes $F$ over precisely this feasible set. This is the continuous problem (2.1), rather than an optimization over the integer-valued network state. Kelly (1991), p. 327, (2.1).

A nonnegative vector $y=(y_j)$ assigns one multiplier to each link. The dual objective is

D(y)=\sum_r\nu_r\exp\!\left(-\sum_jy_jA_{jr}\right)+\sum_jy_jC_j, \qquad y_j\ge0.

A blocking vector $B=(B_j)$ has $0\le B_j<1$ . Its carried route flow is $\nu_r\prod_i(1-B_i)^{A_{ir}}$ . The conditions on $B$ say that the total carried flow through link $j$ equals $C_j$ when $B_j>0$ , and is at most $C_j$ when $B_j=0$ . The multiplier and blocking coordinates are related by $B_j=1-e^{-y_j}$ , equivalently $y_j=-\log(1-B_j)$ . These are equations (2.3), (2.6), and (2.7). Kelly (1991), p. 328.

Formalization targets

Theorem 2.8: primal optimum, blocking solutions, and dual optima

The goal first asserts that the primal problem has exactly one optimizer. Every blocking solution must describe that same optimizer:

x_r=\nu_r\prod_j(1-B_j)^{A_{jr}}\quad\text{for every route }r.

It also asserts that a blocking solution exists, and that it is unique if $A$ has rank $J$ , the number of links. Finally, the transformations $B_j=1-e^{-y_j}$ and $y_j=-\log(1-B_j)$ give a bijection between all blocking solutions and all dual optima. The formal goal includes both directions and both inverse identities, even when the dual optimizer is not unique. Kelly (1991), p. 329, Theorem 2.8.

Claims leading to the theorem

The milestone list follows Kelly's stated progression: unique primal attainment; the Lagrangian maximum and the dual value in (2.2); feasibility and complementary slackness in (2.4)–(2.5); the substitution (2.6); dual attainment; both directions of the blocking–dual correspondence; and strict convexity plus uniqueness under full row rank. One direction of the correspondence is an existing, proved platform theorem, KellyStochasticNetworks.dual_optimum_conditions; it is referenced directly. The other direction remains a new target. Kelly (1991), pp. 327–329.

Significance

The theorem makes the carried flow uniquely determined even when several blocking vectors or dual optimizers describe it. Under full row rank, it also identifies a unique linkwise blocking vector. Its correspondence lets a statement in the flow language be translated to a statement in the multiplier language without selecting a preferred optimizer. The interpretation following Theorem 2.8 explains the linkwise condition: positive blocking occurs only on a saturated link. Kelly (1991), p. 329, discussion after Theorem 2.8.

The mathematical result was proved in the source paper. The work here is to obtain machine-checked proofs of its exact finite-dimensional statements. The published Kelly–Yudovina definition KellyStochasticNetworks.dualObjective already represents the dual formula, and its proved optimum-conditions theorem supplies one direction of the correspondence. The remaining development would give reusable facts about separable entropy objectives, nonnegative linear capacity constraints, complementary slackness, and exponential coordinate changes. Those facts can support later loss-network formalizations without changing this mission's target.

Difficulty

The boundary $x_r=0$ requires care: the objective has a continuous value there, but its logarithmic derivative does not. Thus a calculation that differentiates the objective throughout the closed nonnegative cone does not justify the printed differentiability sentence on p. 327. Dual existence is another boundary issue. A nonnegative capacity permits $C_j=0$ , while the paper's stated growth of the dual objective in every nonnegative coordinate can fail at that input. Any formal argument for the complete theorem must cover these domains accurately. Full row rank controls uniqueness of the dual coordinates; without it, the paper explicitly allows nonunique blocking solutions. Kelly (1991), pp. 327–329.

Formalization scope

Lean represents links by Fin J, routes by Fin R, $A_{jr}$ and $C_j$ by natural numbers, and $x_r$ , $y_j$ , $B_j$ , and $\nu_r$ by real numbers. The primal feasible set includes both coordinatewise nonnegativity and every link-capacity inequality. The dual optimum is minimal over the nonnegative orthant, using the published dual objective. The finite sums and products have their usual empty-index values; no hidden nonemptiness assumption is imposed. Matrix rank is taken over the reals and compared with $J$ , so the rank condition is full row rank.

The goal assumes $\nu_r>0$ and $C_j\ge1$ for every route and link. Positive rates give the logarithm in the primal objective its intended meaning. Positive capacities exclude a degeneracy in the dual-attainment and blocking parts of the theorem. The value at $x_r=0$ is the continuous extension $x_r\log x_r=0$ ; no differentiability assertion at that boundary is part of the formal target. Blocking values belong to $[0,1)$ , so the inverse logarithm is evaluated on a positive number. A flow optimum always ranges over the exact primal feasible set, and a blocking solution always ranges over the full conditions (2.7); neither can be replaced by an arbitrary vector with a convenient equation.

A complete proof may require finite-dimensional convex analysis, strict concavity of the entropy term, attainment on a closed feasible set, the dual first-order condition, and facts about exponentials, logarithms, products, and matrix rank. The definitions and theorems are kept separate so work on these pieces can be reused. Contributions proving either a milestone or a reusable supporting lemma are in scope.

Selected references

F. P. Kelly, Loss networks, The Annals of Applied Probability 1(3), 319–378, 1991. DOI: 10.1214/aoap/1177005872.

11 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 5

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

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

Milestones

In the order the proof uses them:

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Explicit readings of the paper's loose phrases:

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

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

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

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

Selected references

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

15 thms3 active usersReviewed

Completed

Convex Optimization Functional Analysis·Captain: mikedeng1

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

Motivation

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

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

Timeline.

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

Setting

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

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

The problem is

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3.1

For $r>0$ and every stepsize with

0<\rho<2r,

every run of the algorithm satisfies

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

Lean conventions:

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

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

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

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

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

Selected references

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

16 thms3 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

On the Relation Between Integer and Noninteger Solutions to Linear Programs: Deep in the Optimal-Basis Cone, z₂(b) = z₁(b) + φ(b) and the Group Problem Gives an Integer OptimumResearch Paper

Motivation

An integer program is a linear program whose variables must take integer values. Its linear relaxation can be solved efficiently, while the integer program itself is NP-hard in general, so a recurring question in integer programming is how much the optimal solution of the relaxation says about the integer optimum. Simple rounding of the fractional optimum does not answer it: examples show that the integer optimum need not lie within distance one of the LP optimum, even when the right-hand side is large.

R. E. Gomory's 1965 note in the Proceedings of the National Academy of Sciences (doi:10.1073/pnas.53.2.260) showed that, for right-hand sides lying deep inside the cone of an optimal LP basis, the integer program is solved exactly by the LP solution plus a correction computed in a finite abelian group. The resulting group relaxation (the "corner polyhedron" of Gomory's later work, Gomory 1969) underlies a large body of work on cutting planes, the master group problem, Gomory–Johnson functions and asymptotic integer programming.

Timeline. Gomory's fractional cutting-plane algorithm (Gomory 1958) introduced the "fractional rows" of the simplex tableau; the 1965 note identifies the group they generate with $M(I)/M(B)$ and proves the asymptotic theorem formalized here. Gomory 1969 develops the corner polyhedron; Gomory and Johnson (1972) study the continuous valid functions of the corner polyhedron.

Setting

Let $A$ be an integer $m\times(m+n)$ matrix of the form $(A',I)$ , let $b\in\mathbb Z^m$ and $c\in\mathbb R^{m+n}$ . Problem P1 is

\max\ z_1=cx\quad\text{s.t.}\quad Ax=b,\ x\ge0,

and P2 is P1 with $x$ integer. A basis is a nonsingular $m\times m$ submatrix $B$ of $A$ ; after rearranging, $A=(B,N)$ with $B=(\alpha_1,\dots,\alpha_m)$ and $N=(\alpha_{m+1},\dots,\alpha_{m+n})$ , and $c=(c_B,c_N)$ . The relative cost of a nonbasic column is $c^*_i=c_i-c_BB^{-1}\alpha_i$ , and $B$ is an optimal basis when all $c^*_i\le0$ . The cone of the basis is $K^B=\{\beta\in\mathbb R^m: B^{-1}\beta\ge0\}$ ; removing from it all points within Euclidean distance $d$ of its boundary gives the reduced cone $K^B(d)$ .

Let $M(I)=\mathbb Z^m$ and $M(B)=\mathfrak L_B$ the lattice of integer combinations of $\alpha_1,\dots,\alpha_m$ . The factor module $M(I)/M(B)$ is a finite abelian group with $D=|\det B|$ elements; write $\bar\alpha_i$ , $\bar b$ for the classes of $\alpha_i$ , $b$ . The group problem (4) is

\max\ \sum_{i=1}^n c^*_{i+m}y_i\quad\text{s.t.}\quad\sum_{i=1}^n\bar\alpha_{i+m}y_i=\bar b,\quad y_i\ge0\text{ integer},

with optimal value $\varphi^B(b)$ . Finally $l=\max_{i>m}\|\alpha_i\|$ .

Formalization targets

Goal: THEOREM 1 (p. 261)

If $b\in K^B(l(D-1))$ , then P1, P2 and (4) attain their optima, the value $z_2(b)$ of P2 is

z_2(b)=z_1(b)+\varphi^B(b),

an optimal solution of P2 is

x(b)=\big(B^{-1}(b-Ny^B(b)),\ y^B(b)\big)

for an optimal solution $y^B(b)$ of (4) with $\sum_iy^B_i(b)\le D-1$ , and $\varphi^B$ , $y^B$ are $m$ -periodic: $\varphi^B(b+\alpha_i)=\varphi^B(b)$ .

Milestones

In the order of the paper's proof: $|M(I)/M(B)|=D$ (p. 262); periodicity of (4) (p. 263); the cost identity (5)–(6); " $c_BB^{-1}b$ is $z_1(b)$ ", the simplex optimality criterion (a published, proved theorem); the projection of a solution of P2 to a solution of (4); the bound (7), $z_2(b)\le z_1(b)+\varphi(b)$ ; the extension of a solution of (4) to an integer solution; the LEMMA (an optimal solution of (4) with $\sum y_i\le D-1$ ); and the bound $\|Ny\|\le(D-1)l$ that places $b-Ny$ in $K^B$ .

Companions

THEOREM 2: the optimal $x(b)$ satisfies $\sum_{i>m}x_i=\sum_iy_i\le D-1$ . THEOREM 4 (with the bound corrected, see below): if an optimal $y$ of (4) has $\prod_i(y_i+1)>D$ , the optimum of (4) is not unique.

Significance

THEOREM 1 reduces integer programming, for right-hand sides far from the boundary of an optimal cone, to a shortest-path-type problem over a group of order $D$ : the integer optimum is determined by the LP optimum and a periodic correction, and it can be computed in time polynomial in $n$ and $D$ (THEOREM 3, not formalized here). It explains why rounding fails while a structured correction succeeds, and it is the starting point of the corner-polyhedron and cutting-plane theory built on the group relaxation. THEOREM 2 bounds how far the integer optimum lies from a lattice point of $\mathfrak L_B$ , an early proximity result.

The results are classical and proved in the paper; none of them has a machine-checked proof that this mission is aware of. The mission produces a Lean statement and proof of the asymptotic theorem, together with reusable statements about the group $\mathbb Z^m/B\mathbb Z^m$ and the zero-sum shortening argument of the LEMMA.

Difficulty

The decomposition $z_2\le z_1+\varphi$ is a direct computation. The difficulty is the converse: an optimal solution $y$ of the group problem extends to an integer point $x_B=B^{-1}(b-Ny)$ , but nothing in (4) forces $x_B\ge0$ . Optimality of $y$ alone does not bound $y$ : an optimal solution may carry zero-cost cycles of arbitrary length, and then $b-Ny$ can leave the cone $K^B$ . The theorem therefore depends on choosing the right optimal solution of (4), one whose total size is bounded by the group order, and on relating that combinatorial bound to the Euclidean geometry of the cone.

Formalization scope

The basis is fixed: $B$ is an integer $m\times m$ matrix and $N$ an integer $m\times n$ matrix; column $j$ of $N$ ( $0$ -based) is the paper's $\alpha_{m+1+j}$ . The costs $c_B$ , $c_N$ are real.
The standing assumptions of pp. 260–262 are hypotheses of the goal: $\det B\neq0$ ; every unit vector of $\mathbb Z^m$ is a column of $B$ or of $N$ (the paper's $A=(A',I)$ , without which P2 can be infeasible); all relative costs $c^*_i\le0$ ( $B$ is optimal, without which (4) is unbounded).
P2's variables are natural numbers (integer and nonnegative). The group problem is written as " $b-Ny\in B\mathbb Z^m$ ", which is equivalent to $\sum\bar\alpha_{i+m}y_i=\bar b$ .
Optimal values are greatest elements of the sets of objective values, never suprema; the goal asserts that they are attained.
The norm in $l$ and in $K^B(d)$ is Euclidean. $K^B(d)$ is the set of points whose closed ball of radius $d$ lies in $K^B$ . $l=0$ when $n=0$ .
In part (3) of the goal, $y^B(b)$ ranges over optimal solutions of (4) with $\sum_iy_i\le D-1$ , the solutions the paper's LEMMA and dynamic program produce.
THEOREM 4 is stated with the hypothesis $\prod(y_i+1)>D$ : the printed $>D-1$ is false ( $m=n=1$ , $B=(2)$ , $N=(1)$ , $c=(2,0)$ , $b=1$ has the unique optimum $y=1$ with $\prod(y_i+1)=2$ ).
A trivializing formalization is ruled out: the goal assumes none of the LEMMA, the inequality (7), integrality of $B^{-1}(b-Ny)$ or the norm bound, and it states the existence of the optima instead of assuming them.
Not in scope: the operation counts of THEOREM 3 and the recursion (8), which need a machine model the paper does not define.

Needed infrastructure: the cardinality of $\mathbb Z^m/B\mathbb Z^m$ (available in Mathlib through determinants of basis changes), a zero-sum/pigeonhole argument in a finite abelian group, the simplex optimality criterion (published), and elementary Euclidean estimates. The group-theoretic lemmas are reusable for other group-relaxation and proximity missions. Proofs of the milestones, alternative arguments and the extension to the open-ball reading of $K^B(d)$ are welcome.

Selected references

R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53(2):260–265, 1965. https://doi.org/10.1073/pnas.53.2.260
R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bull. Amer. Math. Soc. 64:275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4
R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2:451–558, 1969. https://doi.org/10.1016/0024-3795(69)90017-2
R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Math. Programming 3:23–85, 1972.
J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer, 2007 (simplex optimality criterion). https://doi.org/10.1007/978-3-540-30717-4

11 thms3 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 1: Markdown Is Optimal Once Time-to-Go Falls Below a Strictly Increasing Threshold x_nResearch Paper

Why the timing of a markdown matters

A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.

The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.

Prices, demand, and admissible switches

Let $n\ge1$ be the initial stock and $t\ge0$ the time to go. The seller first charges price $p_1$ and may change once to a lower price $p_2$ . Demands at the two prices are independent Poisson counts with positive rates $\lambda_1$ and $\lambda_2$ . A lower price produces more arrivals, so $p_2<p_1$ and $\lambda_1<\lambda_2$ . Feng and Gallego also assume that lowering the price increases the revenue rate: $p_1\lambda_1<p_2\lambda_2$ . There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.

Write $N_1(s)$ for the observed sales count at the initial price by time $s$ . If the price changes at deterministic time $s\in[0,t]$ , let $J(n,t;s)$ be the expected total revenue. The count after the change is independent of $N_1(s)$ , and their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$ . The optimal value $J(n,t)$ allows the switch time $\tau$ to depend on the counts observed so far. An admissible $\tau$ lies between zero and $t$ , is a stopping time for the history of $N_1$ , and occurs before stock is exhausted almost surely. At $s=0$ , $J(n,t;0)$ is the revenue from charging $p_2$ immediately. The paper defines these quantities in §3, pp. 1377–1379.

Formalization targets

The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence $x_1<x_2<\cdots$ of inventory-dependent thresholds. When $t\le x_n$ , switching immediately earns the optimal value; when $t>x_n$ , a correction $F(n,t)$ is added:

J(n,t)=\begin{cases} J(n,t;0),&t\le x_n,\\ J(n,t;0)+F(n,t),&t>x_n. \end{cases}

The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with $F(0,t)=0$ . For $n\ge1$ , set $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$ , where $G$ is the Poisson-tail expression from §4.1. The threshold $x_n$ is the first nonnegative zero of $L(n,\cdot)$ . A function $H(n,\cdot)$ satisfies $\partial_tH=-\lambda_1H+L$ for positive time and $H(n,x_n)=0$ ; $F$ is zero below $x_n$ and equals $H$ at and above it. If $y_n$ is the first zero of $G(n,\cdot)$ , the theorem also gives $x_1=y_1$ and $x_n<y_n$ for $n>1$ .

Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of $G$ in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.

What the result provides

The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.

The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.

Where the mathematics is difficult

The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory $n$ depends on the correction at stock $n-1$ . Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of $G$ , the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.

The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.

Formalization scope

Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.

The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.

For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.

Selected references

Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

6 thms3 active usersReviewed

Dynamic Programming Graph Theory Operations Research·Captain: mikedeng1

The Complexity of Markov Decision Processes III: The Optimal Discounted Cost of a Deterministic Process Is the Least Discounted Cost of a SigmaResearch Paper

Motivation

A Markov decision process with finitely many states and decisions, a discount factor $\beta\in(0,1)$ and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).

The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its $t$ -th arc with weight $\beta^t$ . The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.

Setting

A deterministic stationary Markov decision process consists of a finite set $S$ of $n$ states, an initial state $s_0\in S$ , and for each state $s$ a finite nonempty set $D_s$ of decisions. Decision $i\in D_s$ costs $c(s,i)\in\mathbb R$ and leads with certainty to the state $\mathrm{next}(s,i)$ . Equivalently, it is a directed graph on $S$ with an arc $s\to\mathrm{next}(s,i)$ of weight $c(s,i)$ for each decision; parallel arcs and loops are allowed.

A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state $s$ and time $t=0,1,2,\dots$ ; it is stationary if $\delta(s,t)$ does not depend on $t$ . From $s_0$ it produces the states $s_{t+1}=\mathrm{next}(s_t,\delta(s_t,t))$ and the discounted cost

J_\beta(\delta)=\sum_{t=0}^{\infty}\beta^t c\bigl(s_t,\delta(s_t,t)\bigr).

The optimal discounted cost is $J^*_\beta(s_0)=\inf_\delta J_\beta(\delta)$ , the infimum over all policies $\delta(s,t)$ .

A sigma is a walk $w_0=s_0,w_1,\dots,w_N$ along decisions $e_t\in D_{w_t}$ whose nodes $w_0,\dots,w_{N-1}$ are distinct and whose last node repeats an earlier one, $w_N=w_j$ with $j<N$ : the walk from $s_0$ up to the first repetition of a node. It is a prefix of $j$ arcs followed by a cycle of $l=N-j\ge1$ arcs. Its discounted cost $c_\beta(P)$ is the discounted cost of the infinite walk that follows it and repeats its cycle forever.

In the min-plus semiring (addition is $\min$ , multiplication is $+$ , zero is $+\infty$ ), let $A_{uv}$ be the least cost of a decision from $u$ to $v$ ( $+\infty$ if none), let $rA$ multiply every finite entry by $r$ , and let

B_0=I,\qquad B_k=A\otimes\beta A\otimes\cdots\otimes\beta^{k-1}A ,

with $I$ the min-plus identity. The entry $(B_k)_{uv}$ is the least discounted cost $\sum_{t<k}\beta^t c_t$ of a $k$ -arc walk from $u$ to $v$ .

Formalization targets

Goal

For $0<\beta<1$ ,

J^*_\beta(s_0)=\min_{P\text{ sigma}}c_\beta(P)=\min\Bigl\{(B_k)_{s_0u}+\frac{\beta^{k}(B_l)_{uu}}{1-\beta^{l}}\;:\;u\in S,\ 0\le k\le n,\ 1\le l\le n,\ \text{both entries finite}\Bigr\},

with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).

Milestones

The closed form of the cost of a sigma (p. 446): $c_\beta(P)=\sum_{t<j}\beta^tc_t+\frac{\beta^j}{1-\beta^l}\sum_{t<l}\beta^tc_{j+t}$ .
A stationary optimal policy exists (§2, p. 444; cited on p. 446). The general finite stochastic statement is on the platform as BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.
The path of a stationary policy, cut at its first repeated node, is a sigma with the same discounted cost, and every sigma arises this way (p. 446).
The products $B_j$ are the cheapest discounted $j$ -arc walks (p. 447).

Significance

The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each $B_k$ is a product of $k$ min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).

On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.

Difficulty

The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies $\delta(s,t)$ , and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary $k$ -arc walks and closed $l$ -walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has $k\le n$ and $l\le n$ . Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of $\beta$ in two places.

Formalization scope

The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:

The model is stationary and deterministic. A DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set $D_s$ "; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.
Policies are maps $\delta(s,t)$ , time is $\mathbb N$ from $0$ , and the optimum optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.
Costs are tsums, which are junk ( $0$ ) for non-summable series; every statement that sums costs assumes $0<\beta<1$ , under which the series converge absolutely.
A sigma is encoded as a lasso, $w_N=w_j$ with $j<N$ . This includes $j=0$ , a sigma whose cycle passes through $s_0$ , which the printed form $(u_0,\dots,u_k,v_1,\dots,v_l,v_1)$ omits but the definition "a path from $u_0$ until the first repetition of a node" includes. The paper's $k$ is $j-1$ .
Corrected slips: (i) in the sigma display the cycle sum carries $\beta^{j-1}$ , not $\beta^j$ , for its $j$ -th arc, and the indices are made consistent; (ii) the algorithm's expression is $\lambda+\beta^k\mu/(1-\beta^l)$ with $l\ge1$ , not $\lambda+\beta^{k+1}\mu/(1+\beta^l)$ (one state with a loop of cost $1$ has optimum $1/(1-\beta)$ , which the printed form misses); (iii) $B_0$ , used but not defined, is the min-plus identity.
Matrix entries are in Tropical (WithTop ℝ), so $+\infty$ is ⊤ and the product is Mathlib's matrix product over the tropical semiring.

Not formalized: membership in NC, the processor count $n^4$ , the $\log^2 n+3\log n$ parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.

Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.

Selected references

C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. https://doi.org/10.1287/moor.12.3.441
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, §7.3 (discounted problems, Proposition 7.3.1).
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Ch. 6 (existence of stationary optimal policies for discounted models). https://doi.org/10.1002/9780470316887

7 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Bargaining Problem: The Nash Product Maximizer Is the Unique Solution Satisfying Invariance, Symmetry, IIA and Pareto EfficiencyResearch Paper

Motivation

Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).

Timeline:

1944. von Neumann and Morgenstern axiomatize expected utility. A utility is determined up to a positive affine transformation $au+b$ . Nash quotes this on p. 157.
1950. Nash introduces the two-person bargaining problem and the axioms of Pareto efficiency, independence of irrelevant alternatives and symmetry, the solution being invariant under the choice of utility scales. He proves that they force the maximizer of the product $u_1u_2$ (doi:10.2307/1907266).
1953. Nash's Two-Person Cooperative Games adds the threat game that fixes the disagreement point.
1975. Kalai and Smorodinsky replace independence of irrelevant alternatives by monotonicity and obtain a different solution.
1986. Binmore, Rubinstein and Wolinsky show that the Nash solution is the limit of equilibria of alternating-offers bargaining as the time between offers vanishes.

Setting

A bargaining problem is a pair $\langle S,d\rangle$ . Here $S\subseteq\mathbb R^2$ is the set of utility pairs $u=(u_1,u_2)$ the two players can reach by agreement, including lotteries over agreements. $d\in S$ is the disagreement point, the utilities of no cooperation. As in the platform goal, $S$ is compact and convex, and some $s\in S$ has $s_1>d_1$ and $s_2>d_2$ (both individuals could gain). Write $\mathcal B$ for the set of such pairs.

A bargaining solution is a map $g$ from $\mathcal B$ to $\mathbb R^2$ . Nash requires:

Selection. $g(S,d)\in S$ .
PAR (Nash's assumption 6). If $s,t\in S$ and $t$ is strictly better than $s$ for both players, then $g(S,d)\neq s$ .
IIA (assumption 7). If $S\subseteq T$ and $g(T,d)\in S$ , then $g(S,d)=g(T,d)$ .
SYM (assumption 8). If $d_1=d_2$ and $S$ is symmetric in the line $u_1=u_2$ , then $g(S,d)$ lies on that line.
INV. For $L(s)=(\alpha_1s_1+\beta_1,\ \alpha_2s_2+\beta_2)$ with $\alpha_1,\alpha_2>0$ , $g(L(S),L(d))=L(g(S,d))$ .

The paper has no separate INV axiom. It normalizes the disagreement utility to $0$ and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.

Formalization targets

Goal

The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by Nickrobbins95 and currently Open. This mission references it and does not restate it. It asserts that there is a solution $f$ such that a solution $g$ satisfies selection, INV, SYM, IIA and PAR if and only if $g=f$ , and that for every $\langle S,d\rangle\in\mathcal B$

f(S,d)\ge d,\qquad (s_1-d_1)(s_2-d_2)<(f_1-d_1)(f_2-d_2)\ \text{ for all } s\in S,\ s\ge d,\ s\neq f(S,d).

Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.

Milestones

On a compact convex $S\ni(0,0)$ that contains a point where both players gain, $u_1u_2$ has exactly one strict maximizer $p$ in the closed first quadrant, and $p_1,p_2>0$ .
Multiplying the utilities by positive constants maps the maximizer to the maximizer, so $p$ may be moved to $(1,1)$ .
If $S$ is convex and $(1,1)$ maximizes $u_1u_2$ , then $u_1+u_2\le2$ on all of $S$ .
A compact $S$ under that line lies in a square $Q_h=\{2-2h\le u_1+u_2\le2,\ |u_1-u_2|\le h\}$ .
$(1,1)$ is the only point of $Q_h$ on the diagonal that no point of $Q_h$ strictly dominates.
Necessity. Under the five conditions, $g(S,d)$ is the strict maximizer of $(s_1-d_1)(s_2-d_2)$ over $S\cap\{s\ge d\}$ .

Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex $(12,5)$ reached by exactly one exchange, and trade with money, where the solution gives equal money profits.

Significance

The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.

The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.

Difficulty

Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class $\mathcal B$ , and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of $S$ under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality $d=0$ and $p=(1,1)$ ". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of $d$ inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.

Formalization scope

Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work at $d=(0,0)$ , the paper's normalization. Milestone 6 has a general $d$ and the goal's encoding. Milestones 1–5 make the following readings explicit:

"First quadrant" is the closed quadrant $u_1\ge0,\ u_2\ge0$ .
"The point where $u_1u_2$ is maximized" is the strict maximizer over $S$ in that quadrant, in the goal's form. Milestone 1 also states $p_1,p_2>0$ , which follows from the point where both gain (p. 158).
Milestone 3's hypothesis is the weak maximum $s_1s_2\le1$ . Its conclusion covers every point of $S$ , not only first-quadrant points.
The square is the explicit set $Q_h$ . Its compactness, convexity and literal symmetry $(a,b)\in Q_h\iff(b,a)\in Q_h$ are part of milestone 4's conclusion.
"Satisfying assumptions (6) and (8)" in the square means lying on $u_1=u_2$ and being strictly dominated by no point of the square.

Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given $g$ . It does not restate the goal: it has no existence claim and no "if and only if".

Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of $u_1u_2=0$ . The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class $\mathcal B$ , which is nonempty.

The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.

Related platform work treats other bargaining models. These are Rubinstein's alternating-offers game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction (ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.

Selected references

J. F. Nash, Jr., The Bargaining Problem, Econometrica 18(2), 155–162, 1950. doi:10.2307/1907266
J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
J. F. Nash, Jr., Two-Person Cooperative Games, Econometrica 21(1), 128–140, 1953. doi:10.2307/1906951
E. Kalai, M. Smorodinsky, Other Solutions to Nash's Bargaining Problem, Econometrica 43(3), 513–518, 1975. doi:10.2307/1914280
K. Binmore, A. Rubinstein, A. Wolinsky, The Nash Bargaining Solution in Economic Modelling, RAND Journal of Economics 17(2), 176–188, 1986. doi:10.2307/2555382
M. J. Osborne, A. Rubinstein, Bargaining and Markets, Academic Press, 1990, Theorem 2.3.

10 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VI: With a Forecast Update, Buy-Back Terms with w₁ − w₂ + λc₂ = λc₁ Give the Retailer λΩ₁(q₁) and a Lower Period-2 Margin w₂ − c₂ < w₁ − c₁Textbook

Motivation

A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.

This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.

Setting

A demand signal $\xi \ge 0$ with density $g$ and distribution function $G$ is observed once before the selling season. Given $\xi$ , demand $D$ has distribution function $F(\cdot\,|\,\xi)$ , continuous and strictly increasing on $[0,\infty)$ . Demand is stochastically increasing in the signal: $F(x\,|\,\xi_h) < F(x\,|\,\xi_l)$ for $\xi_h > \xi_l$ . Expected sales are $S(q\,|\,\xi) = E[\min(q,D)\,|\,\xi]$ . Period 1 is before the signal and period 2 is after it. The retailer's total order is $q_1$ after period 1 and $q_2 \ge q_1$ after period 2. The supplier's unit production cost is $c_i$ in period $i$ , with $c_1 < c_2 < p$ , where $p$ is the retail price. Salvage values and goodwill costs are zero.

The supply chain's period-2 objective is

\Omega_2(q_2\,|\,q_1,\xi) = pS(q_2\,|\,\xi) - c_2 q_2 + c_2 q_1 ,

and $q_2(q_1,\xi)$ maximizes it over $q_2 \ge q_1$ . The supply chain's expected profit is $\Omega_1(q_1) = -c_1 q_1 + E[\Omega_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ .

Under the buy back contract $\{w_1, w_2, b\}$ the retailer pays $w_i$ per unit ordered in period $i$ , and the supplier refunds $b$ per unsold unit. The retailer's period-2 profit is $\pi_2(q_2\,|\,q_1,\xi) = (p-b)S(q_2\,|\,\xi) - (w_2-b)q_2 + w_2 q_1$ , and his period-1 profit is $\pi_1(q_1) = -w_1 q_1 + E[\pi_2(q_2(q_1,\xi)\,|\,q_1,\xi)]$ . The supplier's period-2 profit $\Pi_2$ and her period-1 profit $\Pi_1(x\,|\,q_1)$ , as functions of the stock $x$ she holds, are given in the mission's Profits definition.

Formalization targets

Goal: the buy back contract coordinates

For $\lambda \in [0,1]$ with

p - b = \lambda p,\qquad w_2 - b = \lambda c_2,\qquad w_1 - w_2 + \lambda c_2 = \lambda c_1,

the identities

\pi_2(q_2\,|\,q_1,\xi) = \lambda\big(\Omega_2(q_2\,|\,q_1,\xi) - c_2 q_1\big) + w_2 q_1,\qquad \pi_1(q_1) = \lambda\,\Omega_1(q_1)

hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for $\lambda > 0$ ). In addition,

w_2 - c_2 = w_1 - \big(\lambda c_1 + (1-\lambda)c_2\big) < w_1 - c_1 \quad (\lambda < 1).

Milestones

The structure of the period-2 problem, Eqs. (25)–(26): $q_2(\xi)$ solves $F(q_2(\xi)\,|\,\xi) = (p-c_2)/p$ and increases in $\xi$ , and the threshold $\xi(q_1)$ splits the signals into those that trigger a period-2 order and those that do not.
The retailer's period-2 identity (p. 65).
The supplier fills any period-2 order up to $q_2(q_1,\xi)$ , and for $\lambda < 1$ she does not fill a larger one (p. 65).
The retailer's period-1 identity (p. 66).
The first-order condition (27) for $q_1^o$ .
The supplier's period-2 profit increases in her stock below $q_1$ , so she produces at least the period-1 order (p. 66).
The supplier produces exactly the period-1 order (p. 67).
The margin comparison (p. 67).

Significance

The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through $\lambda$ . Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.

These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold $\xi(x)$ .

Difficulty

The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and $\partial \Pi_1(x\,|\,q_1)/\partial x = -c_1 + c_2(1 - G(\xi(x)))$ . The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum $\max(q_1, q_2(\xi))$ has a kink at $\xi = \xi(q_1)$ . The integrand switches between two regimes, and the switch point moves with $q_1$ . The supplier's period-1 profit is not differentiable at $x = q_1$ ; only its right derivative is negative at $q_1^o$ . Turning the page's derivative statements into the global claim that $x = q_1^o$ is her unique optimum needs a monotonicity argument on both sides of $q_1^o$ .

Formalization scope

The conditional law is a measurable family $\xi \mapsto D_\xi$ of probability measures on $\mathbb R$ supported on $[0,\infty)$ , each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on $[0,\infty)$ . The signal has a measurable density $g \ge 0$ with $\int_0^\infty g = 1$ , and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. $0 < c_2 < p$ makes the critical ratio lie in $(0,1)$ . Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).

The optimum $q_2(q_1,\xi)$ is a hypothesis-carried selection maximizing $\Omega_2$ over $q_2 \ge q_1$ . It is never an arbitrary function: a formalization that let $q_2(q_1,\xi)$ be unconstrained would make $\pi_1 = \lambda\Omega_1$ a statement about meaningless orders. The thresholds $\xi(q_1)$ enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over $q_1 \ge 0$ and $q_2 \ge q_1$ . Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).

Three corrections of the print are disclosed in the item notes:

the strict margin inequality fails at $\lambda = 1$ ;
the p. 66 identity for $\Pi_2(x, q_1, q_2, \xi)$ is off by the constant $(1-\lambda)c_2q_1$ ;
"retailer optimal equals chain optimal" needs $\lambda > 0$ in the converse direction.

Contributions are welcome on all milestones. A lemma that differentiates $q \mapsto E[\max_{q_2 \ge q} \Omega_2]$ with a density-driven threshold would be reusable beyond this mission.

Selected references

G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. https://doi.org/10.1016/S0927-0507(03)11006-7
K. L. Donohue, Efficient Supply Contracts for Fashion Goods with Forecast Updating and Two Production Modes, Management Science 46(11), 1397–1411, 2000. https://doi.org/10.1287/mnsc.46.11.1397.12088
M. Fisher and A. Raman, Reducing the Cost of Demand Uncertainty Through Accurate Response to Early Sales, Operations Research 44(1), 87–99, 1996. https://doi.org/10.1287/opre.44.1.87

12 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts VII: In the Single-Location Base-Stock Model the Transfers t_I = (1 − λ)h_r, t_B = β_r − λβ Make the Retailer's Cost λc(s_r)Textbook

Motivation

A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.

The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).

Setting

Let $D_r$ denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean $\mu_r=\mathbb E[D_r]$ , distribution function $F_r$ , and density $f_r$ . At inventory level $s\in\mathbb R$ , expected inventory is $I_r(s)=\mathbb E[(s-D_r)^+]$ and expected backorders are $B_r(s)=\mathbb E[(D_r-s)^+]$ , where $x^+=\max(x,0)$ . The section assumes $F_r(0)=0$ and a strictly increasing differentiable $F_r$ on nonnegative levels. These assumptions place the optimum above zero.

The retailer pays holding cost $h_r I_r(s)$ and its own backorder cost $\beta_r B_r(s)$ . The supplier pays a further backorder cost $\beta_s B_r(s)$ . All three cost rates are positive. Thus $c_r(s)=h_r I_r(s)+\beta_r B_r(s)$ and $c_s(s)=\beta_s B_r(s)$ are the firms' costs, while $c(s)=c_r(s)+c_s(s)$ is the channel cost. Write $\beta=\beta_r+\beta_s$ . Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.

The proposed contract pays the retailer $t_I I_r(s)+t_B B_r(s)$ from the supplier, where $t_I$ and $t_B$ are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter $\lambda\in(0,1]$ , the contract sets $t_I=(1-\lambda)h_r$ and $t_B=\beta_r-\lambda\beta$ . The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter $\lambda$ describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.

Formalization targets

The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum $s_r^\circ$ is unique and satisfies

F_r(s_r^\circ)=\frac{\beta}{h_r+\beta};

the uncontracted retailer has its own unique optimum $s_r^*$ with $s_r^*<s_r^\circ$ . Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family ( $t_I\ge0$ , with $t_I>0$ exactly for $\lambda<1$ , and $\{t_B:0<\lambda\le1\}=[-\beta_s,\beta_r)$ ); the decomposition

t_I I_r(y)+t_B B_r(y)=(t_I+t_B)I_r(y)+t_B(\mu_r-y);

and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price $p=h_r+\beta_r$ and wholesale price $w=h_r$ , the newsvendor retailer's profit $pS(q)-wq$ , with expected sales $S(q)=\mathbb E[\min(q,D_r)]$ , equals $-c_r(q)+\beta_r\mu_r$ . The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:

c_r^\lambda(s)=\lambda c(s),\qquad c_s^\lambda(s)=(1-\lambda)c(s) \quad\text{for all }s\in\mathbb R\text{ and }0<\lambda\le1.

Consequently, the retailer's contracted cost has the same unique minimizer $s_r^\circ$ as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in $\lambda$ , which is the page's statement that the retailer's share of the cost increases with $\lambda$ . The result does not prescribe one fixed allocation of cost: each $\lambda$ in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.

Significance

The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to $\beta_r$ , while the channel's stock decision uses $\beta_r+\beta_s$ . Under the contract, the retailer bears the fraction $\lambda$ of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.

The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).

Difficulty

The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as $\lambda c$ would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.

Formalization scope

Lean represents $D_r$ by a probability measure on $\mathbb R$ supported on $[0,\infty)$ , with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on $[0,\infty)$ , equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates $h_r,\beta_r,\beta_s$ are fields of one model, and $I_r,B_r$ are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.

Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that $t_I>0$ for all $\lambda\in(0,1]$ fails at $\lambda=1$ , where $t_I=0$ ; the formal statement asserts $t_I\ge0$ with strict positivity exactly for $\lambda<1$ . The contract range is exactly $0<\lambda\le1$ ; $\lambda=0$ would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.

Selected references

Gérard P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; source used here: author's third draft, January 2003, §6.7. DOI.

12 thms3 active usersReviewed

Dynamic Programming Graph Theory Operations Research·Captain: mikedeng1

Send-and-Split Method for Minimum-Concave-Cost Network Flows II: Subproblem Minimum Costs Are the Greatest Solution of the Send-and-Split Equations, Unique if Circulations Cost Positively (Theorem 2)Research Paper

Motivation

Many network-design and production-planning problems ask for a cheapest way to route a commodity from supply points to demand points when the cost of an arc grows less than proportionally with the amount sent: setup charges, economies of scale, and fixed-plus-linear costs all give concave arc costs. Minimizing a concave function over the flow polytope is NP-hard in general, and the classical linear-cost machinery (potentials, negative-cycle tests) no longer applies. Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987)) gave the send-and-split method, a dynamic program over subsets of the demand nodes that solves the uncapacitated problem in time polynomial in the number of nodes and arcs and exponential only in the number of demand nodes. It contains as special cases the Dreyfus–Wagner recursion for Steiner trees in graphs (Networks 1 (1971)), and the paper applies it to concave-cost production, inventory and network-design problems (§6).

Timeline. Zangwill (1968) solved minimum-concave-cost flows on special networks by dynamic programming. Dreyfus and Wagner (1971) gave the subset recursion for Steiner trees with positive arc lengths. Erickson, Monma and Veinott (1987) extended the subset recursion to arbitrary uncapacitated networks with additive concave arc costs and arbitrary real demands, proved that the minimum costs of the subproblems form the greatest solution of the resulting equations (Theorem 2), and showed it is the only solution when every simple circulation has positive cost.

Setting

A network consists of a directed graph $G = (N, A)$ with nodes $N = \{0, \dots, n-1\}$ and arcs $A$ , ordered pairs of distinct nodes, together with a real demand vector $r = (r_i)$ . A preflow is a nonnegative matrix $x = (x_{ij})$ supported on $A$ ; a flow for $r$ is a preflow with inflow minus outflow equal to $r_i$ at every node. Each arc has a cost function $c_{ij}$ , concave on $[0, \infty)$ with $c_{ij}(0) = 0$ , and the cost of a preflow is $c(x) = \sum_{(i,j)\in A} c_{ij}(x_{ij})$ . A minimum-cost flow is a flow whose cost is at most that of every flow. A simple circulation is a circulation equal to some $\theta > 0$ on the arcs of a simple directed circuit and $0$ elsewhere.

The demand nodes are $D = \{ i : r_i \neq 0 \}$ . For $\emptyset \subset I \subseteq D$ let $r_I = \sum_{j \in I} r_j$ . The subproblem $i \to I$ keeps the demands of the nodes in $I$ , sets all others to zero, and subtracts $r_I$ at node $i$ ; $C_{iI}$ is its minimum cost, $+\infty$ when it has no flow. Let $A_I = A$ if $r_I > 0$ and the reversed arcs if $r_I < 0$ , with sending cost $c_{ij}(r_I)$ , read as $c_{ji}(-r_I)$ when $r_I < 0$ . The send-and-split equations for an array $C'$ are

C'_{iI} = C'_{j, I\setminus\{j\}} \ (j \in I) \quad \text{if } r_I = 0, \qquad (1)

C'_{iI} = \min_{(i,j)\in A_I} \bigl[ c_{ij}(r_I) + C'_{jI} \bigr] \wedge B'_{iI} \quad \text{if } r_I \neq 0, \qquad (2)

with $B'_{iI} = \min_{\emptyset\subset J\subset I} [C'_{iJ} + C'_{i,I\setminus J}]$ for $|I| > 1$ , and $B'_{iI} = 0$ if $I = \{i\}$ , $+\infty$ otherwise, for $|I| = 1$ (3).

Formalization targets

Goal: Theorem 2 (Dynamic-Programming Equations)

If there is a minimum-cost flow for $r$ , then

C \text{ solves (1)–(3)}, \qquad C'_{jI} \le C_{jI} \ \text{ for every } +\infty\text{-or-real solution } C',

for all $j \in N$ and $\emptyset \subset I \subseteq D$ . If moreover every simple circulation has positive cost, then every $+\infty$ -or-real solution equals $C$ .

Milestones

In attack order: the subproblem alternative (a minimum-cost flow or no flow, p. 640); equation (1); inequalities (4), (5), (6) (p. 641); $C_{iI} = B_{iI}$ for $i \in I$ (p. 641); $C$ satisfies (1) and (2) (p. 642); and two generic statements about Bellman's equations (2)′ for minimum-cost chains in a graph with nonnegative, respectively positive, simple circuits: the minimum chain costs form the greatest solution and are nondecreasing in the arc costs, and with positive circuits the solution is unique (p. 642).

Significance

Theorem 2 is the correctness theorem of the send-and-split method: it says that solving equations (1)–(3) by increasing $|I|$ , with a shortest-chain computation for each $I$ , yields the true subproblem minimum costs, in particular the optimum $C_{iD}$ of the original problem. Its uniqueness clause identifies when the equations alone determine the answer, and the counterexample on p. 641 (zero costs on a strongly connected graph) shows that the positivity hypothesis cannot simply be dropped. The same structure underlies the Steiner-tree recursion.

The theorem is proved in the paper; to our knowledge none of it is formalized. This mission supplies Lean definitions of uncapacitated concave-cost flows with extended-real minimum costs and the send-and-split equations, and poses the correctness theorem as a proof goal. The two Bellman milestones are general facts about minimum-cost chains with $+\infty$ -or-real values and are reusable well beyond this paper. Related items on the platform are credited, not reused: the Dreyfus–Wagner Steiner recursion DreyfusWagner.Steiner.steinerLength_recurrence and DreyfusWagner.Steiner.optimal_decomposition (the special case of undirected positive lengths), and BellmanRouting.PolicySpace.routing_equation_unique (uniqueness of the routing equation on a complete graph with positive real times).

Difficulty

The equations (2) mix two minima: sending the whole demand $r_I$ across one arc, and splitting $I$ at the current node. Showing that $C$ satisfies them requires that some optimal flow of every subproblem has a tree-like structure, which in turn rests on the existence theory for concave-cost flows (an optimum is attained at an extreme flow whose support is a forest). Showing that $C$ is the greatest solution requires an induction on $|I|$ in which, for fixed $I$ , equation (2) is a shortest-chain system whose arc costs to an auxiliary node depend on the solution at smaller sets; comparison then needs monotonicity of minimum chain costs in the arc costs, including arcs whose cost drops from $+\infty$ . The naive attempt to prove uniqueness by iterating (2) fails without the positivity hypothesis, because zero-cost circuits admit spurious solutions.

Formalization scope

Nodes are Fin n; arcs are a Finset (Fin n × Fin n) with no loops; arc costs are functions $\mathbb{R} \to \mathbb{R}$ assumed concave on Set.Ici 0 with $c_{ij}(0) = 0$ at arcs (the paper's standing assumption, stated as a hypothesis). Minimum costs, sending costs, splitting terms and solutions take values in EReal; the empty infimum is $+\infty$ , as on the page.

Explicit readings of the paper's phrases:

"there is a minimum-cost flow" means a flow for $r$ whose cost is at most that of every flow for $r$ ;
" $+\infty$ or real-valued" means $\neq -\infty$ , required on every $\emptyset \subset I \subseteq D$ ;
"greatest solution" is two claims: $C$ is a solution, and every solution is $\le C$ entrywise;
"each simple circulation has positive cost" quantifies over every simple circuit and every $\theta > 0$ ;
" $C_{iI}$ is finite" is rendered as $C_{iI} = c(x)$ for a minimum-cost flow $x$ of the subproblem;
"minimum-cost chain" is the infimum of walk costs, attained or $+\infty$ ; arc costs of $+\infty$ in (2)′ are missing arcs.

The definition of $C_{iI}$ is the infimum over flows, never the equations themselves; a formalization defining $C$ by (1)–(3), or omitting the $\neq -\infty$ condition on solutions, or dropping the clause that $C$ is itself a solution, would make the theorem trivial or false and is ruled out. Arrays are compared only on admissible sets. The graph structure of (2)′ is the platform definition BertsekasSPGraph. Running-time bounds, the planar refinements of §4 (Theorem 3) and the capacitated reduction of §5 are out of scope. Proofs of any milestone, and a formalization of the paper's Theorem 1 that the proofs rely on, are welcome.

Selected references

R. E. Erickson, C. L. Monma, A. F. Veinott, Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4), 1987, 634–664. https://doi.org/10.1287/moor.12.4.634
S. E. Dreyfus, R. A. Wagner, The Steiner Problem in Graphs, Networks 1(3), 1971, 195–207. https://doi.org/10.1002/net.3230010302
R. Bellman, On a Routing Problem, Quarterly of Applied Mathematics 16(1), 1958, 87–90. https://doi.org/10.1090/qam/102435
W. M. Hirsch, A. J. Hoffman, Extreme Varieties, Concave Functions, and the Fixed Charge Problem, Communications on Pure and Applied Mathematics 14(3), 1961, 355–369. https://doi.org/10.1002/cpa.3160140312
W. I. Zangwill, Minimum Concave Cost Flows in Certain Networks, Management Science 14(7), 1968, 429–450. https://doi.org/10.1287/mnsc.14.7.429

15 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Supply Chain Coordination with Contracts II: With Price-Dependent Demand the Price-Contingent Buy-Back Gives the Retailer λΠ(q, p), as Revenue Sharing Does, and Coordinates Price and QuantityTextbook

Motivation

A retailer who controls both inventory and price can respond to a supply contract in two ways. A contract that induces the right order quantity at a fixed price may change the retailer's incentive to raise or lower that price. For a one-season supply chain, Cachon's chapter compares familiar contracts under price-dependent demand and identifies a price-contingent buy-back, also called a price-discount contract, that aligns both decisions. The mission concerns §6.3 of the author's January 2003 third draft, on printed pages 33–38. Those page and equation numbers belong to the draft and may differ from the typeset chapter.

Setting

One risk-neutral supplier and one risk-neutral retailer have full information before a single selling season. The retailer chooses a nonnegative stocking quantity $q$ and a retail price $p$ from an admissible price set $P$ ; the price stays fixed during the season. Demand has a probability law $D_p$ that depends on $p$ . Write $F(y\mid p)$ for its distribution function, $S(q,p)=\mathbb E_p[\min(q,D)]$ for expected sales, and $\mu(p)=\mathbb E_p[D]$ for mean demand. Demand is nonnegative, has a finite mean and, in the chapter's regular setting, its distribution function increases with demand level and has a positive price derivative at positive demand levels. Higher prices thus lower demand in the stochastic order used by the chapter. The price set is nonempty and open so an admissible price optimum has an interior first-order condition.

The supplier's unit cost is $c_s$ , the retailer's unit procurement cost is $c_r$ , and $c=c_s+c_r$ is total unit cost. Their goodwill penalties for unmet demand are $g_s$ and $g_r$ , with $g=g_s+g_r$ . An unsold unit has salvage value $v$ at the retailer. The integrated channel's expected profit is

\Pi(q,p)=(p-v+g)S(q,p)-(c-v)q-g\mu(p).

A buy-back contract charges a wholesale price $w_b$ for each ordered unit and pays the retailer $b$ for each unsold unit. A revenue-sharing contract charges a wholesale price $w_r$ and gives the retailer a fraction $\phi$ of sales and salvage revenue. In this section the supplier offers the terms and the retailer chooses $(q,p)$ . The profit formulas use the chapter's convention that a positive transfer goes from retailer to supplier.

Formalization targets

The goal is the price-contingent buy-back on p. 35, with $\lambda\in[0,1]$ :

b(p)=(1-\lambda)(p-v+g)-g_s,\qquad w_b(p)=\lambda c_s+(1-\lambda)(p+g-c_r)-g_s.

In the chapter's zero-goodwill case, $g_r=g_s=0$ , every feasible $(q,p)$ then gives the retailer $\lambda\Pi(q,p)$ and the supplier $(1-\lambda)\Pi(q,p)$ . The same retailer profit is obtained from revenue sharing with $\phi=\lambda$ and $w_r=\lambda(c-v)-c_r+\lambda v$ . Thus every existing maximizer $(q^\circ,p^\circ)$ of the integrated profit maximizes each firm's profit under the contingent buy-back. At $\lambda=0$ the retailer is indifferent; at $\lambda=1$ the supplier is indifferent.

The milestones follow the chapter's printed claims in attack order:

the integrated price condition (14), p. 34;
the quantity-flexibility condition (15), p. 34: price coordination forces $w_q=v-c_r$ or $\delta=0$ ;
the fixed buy-back condition (16), p. 35: price coordination forces $b=-g_s$ and then $w_b=c_s-g_s$ ;
the linear price-contingent terms derived from (5)–(6), p. 35;
the p. 36 profit split $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$ , $\pi_s=(1-\lambda)\Pi-(\lambda g-g_r)\mu$ , valid for all goodwill penalties as an identity;
the zero-goodwill revenue-sharing price claim following (17), p. 36 (the milestone quotes its restatement in §6.3.2, p. 38);
the price-contingent revenue-sharing parameters, p. 37;
the quantity discount $w_d(q)$ , pp. 37–38: with $g_s=0$ it does not distort the price, and given $p^\circ$ it makes $q^\circ$ optimal for both firms.

Significance

The result identifies a contract schedule under which the same quantity-price pair is best for the integrated channel and for the two firms' reported profit functions. It also explains the relation between a buy-back whose terms vary with the chosen price and a revenue-sharing arrangement. In the zero-goodwill setting, both allocate every realized choice's expected channel profit in fixed shares. The general-goodwill identity shows the additional mean-demand terms that matter when the retailer controls price.

The source presents these results analytically; this mission asks for Lean proofs of the stated price and profit relationships. A published Prove2Me definition already supplies expected sales and mean demand for a single demand law, and the model here applies those functions to each price's law. The earlier open theorem RevShareCoord.Single.price_quantity_coordination (from Cachon and Lariviere's revenue-sharing paper) treats deterministic revenue and a simpler cost convention. It is an overlap in theme, but its statement does not include price-indexed demand, salvage value, retailer cost or the contingent buy-back terms, so it is not posed again here. The new model can support further price-dependent contract comparisons in the chapter.

Difficulty

The obstacle is that matching the retailer's quantity incentive at a fixed price can change the retailer's price incentive. The buy-back rate required by the fixed-price coordination equations depends on $p$ ; a fixed buy-back contract therefore does not generally align both choices. Revenue sharing with goodwill penalties has a similar price dependence. The integrated profit need not be concave or unimodal in $(q,p)$ , so a price first-order condition by itself does not establish coordination. The chapter assumes a finite integrated optimum exists and treats the price condition as necessary, not sufficient.

Formalization scope

Lean represents price-dependent demand as a family of probability measures on $\mathbb R$ , one for each price in $P$ . Each admissible law is supported on nonnegative demand, has no atom at zero and has an integrable identity function, so $\mu(p)$ is a genuine finite expectation. Sales are defined by $\mathbb E_p[\min(q,D)]$ , using the published SupplyChainTheory_contracts definition; they are not defined by the equivalent CDF integral. The admissible decisions are exactly $q\ge0$ and $p\in P$ . Unit costs and goodwill penalties are nonnegative, each admissible price exceeds $c=c_s+c_r$ , and $v<c$ , as in the model of §6.2. The chapter's standing risk-neutrality and full-information conventions appear in the use of expected profit with the same demand laws available to both firms.

There is a material qualification. With price-dependent demand, $\mu(p)$ may change with $p$ . The printed first-order condition (14) and the p. 36 inference from $\pi_r=\lambda(\Pi+g\mu)-g_r\mu$ to a joint optimum omit that effect when goodwill penalties are positive. Price first-order and optimality statements here therefore use $g_r=g_s=0$ , a case explicitly discussed in the chapter; general-goodwill claims are limited to algebraic identities. The printed p. 36 equality of price derivatives under revenue sharing also misses its factor $\phi$ , which the formal statement restores. The contingent buy-back terms are defined by the chapter's linear formulas, not by a property that hard-codes coordination. The algebraic statement permits parameter values that may violate economic buy-back bounds such as $0\le b\le w_b$ ; those bounds need separate checks when selecting a contract.

Two first-order statements, (15) and (16), compare price derivatives; they take the derivative of expected sales in price as a hypothesis, and (15) also takes differentiation under the integral sign of $\int_{(1-\delta)q}^{q}F(y\mid p)\,dy$ as a disclosed regularity hypothesis. For the quantity discount, the statement claims what the page shows, undistorted prices for each $q$ and optimality of $q^\circ$ given $p^\circ$ , not joint optimality of $(q^\circ,p^\circ)$ for the retailer. The page's claim that revenue sharing with goodwill coordinates only with $\phi=g_r/g$ is not stated, for the mean-demand reason above.

A trivializing formalization is ruled out: no contract term is defined by the profit identity it should satisfy, the demand family cannot be replaced by a single law, and the optimal pair is a hypothesis about the integrated profit, not a chosen witness.

Reusable contributions include the price-indexed demand family, the expected-profit model with five contract types, and the price-maximizer statements. Proofs of the first-order milestones need Fermat's interior-extremum theorem on the open price set and, for (15), positivity of an interval integral; the identities need the expectation algebra of $S$ and $\mu$ , including $S(0,p)=0$ .

Selected references

Gérard P. Cachon, “Supply Chain Coordination with Contracts,” in Handbooks in Operations Research and Management Science, vol. 11, Supply Chain Management, North-Holland, 2003. DOI 10.1016/S0927-0507(03)11006-7. Formalization source: author's third draft, January 2003, §6.3, pp. 33–38.
Fernando Bernstein and Awi Federgruen, “Decentralized supply chains with competing retailers under demand uncertainty,” Management Science 51(1), 2005 (the price-discount sharing contract; cited in the draft as a 2000 working paper). DOI 10.1287/mnsc.1040.0230
Nicholas C. Petruzzi and Maqbool Dada, “Pricing and the newsvendor problem: a review with extensions,” Operations Research 47(2), 1999, 183–194. DOI 10.1287/opre.47.2.183

12 thms3 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research·Captain: mikedeng1

Finding Minimum-Cost Circulations by Successive Approximation II: For Real Costs, the Strongly Polynomial Loop Reaches a Minimum-Cost Circulation After at Most m⌈log₂(2n)⌉ RefinementsResearch Paper

Why minimum-cost circulation needs a real-cost iteration bound

A minimum-cost circulation is a way to send flow around a directed network while respecting capacities and paying a cost per unit on each arc. It is a basic form of network optimization: a minimum-cost flow with prescribed supplies and demands can be reduced to a circulation problem, and the circulation formulation exposes the residual arcs on which a flow can be improved. Goldberg and Tarjan's successive-approximation method relaxes exact optimality by an error parameter and repeatedly reduces that error. Its ordinary stopping rule for integer costs depends on the largest cost. For arbitrary real costs, including irrational costs, a decreasing positive error need never cross a fixed numerical cutoff. The strongly polynomial loop in their 1987 technical report, later published in Mathematics of Operations Research instead tests the smallest error parameter appropriate to the current circulation and stops when it is zero.

This mission formalizes the number of refinement calls made by that loop. It builds on the related Goldberg–Tarjan 1988 max-flow and 1989 minimum-mean cycle-canceling series: those develop different algorithms for network flow, while the published 1989 circulation and approximate-optimality definitions provide this mission's common network model. The result here concerns successive approximation and its fixed-arc progress measure.

Network and approximate optimality

The vertex set $V$ is finite, with $n=|V|$ , and $E$ is a symmetric set of directed arcs, with $m=|E|$ . Symmetry means that $(v,w)\in E$ brings $(w,v)\in E$ too. Each arc has a real capacity $u(v,w)$ and a real cost $c(v,w)$ ; costs obey $c(v,w)=-c(w,v)$ . A circulation $f$ obeys $f(v,w)\le u(v,w)$ , $f(v,w)=-f(w,v)$ , and conservation of flow at every vertex. Its total cost is half the sum of $c(v,w)f(v,w)$ over directed arcs, since each unordered edge appears twice. A minimum-cost circulation costs no more than any other circulation of the network.

The residual capacity is $u_f(v,w)=u(v,w)-f(v,w)$ . For a price function $p:V\to\mathbb R$ , the report writes the reduced cost as $c_p(v,w)=c(v,w)-p(v)+p(w)$ . A circulation is $\varepsilon$ -optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$ . It is $\varepsilon$ -optimal if some price function works, where $\varepsilon\ge0$ . The tight error $\varepsilon(f)$ is the least such error. A circulation is $\varepsilon$ -tight when it is $\varepsilon$ -optimal but fails to be $\varepsilon'$ -optimal at every $\varepsilon'<\varepsilon$ . This includes attainment at $\varepsilon$ .

An arc is $\varepsilon$ -fixed if all $\varepsilon$ -optimal circulations carry the same flow through it. Write $F_\varepsilon$ for the set of these arcs. Theorem 4.2 supplies an arc-fixing criterion from a large absolute reduced cost. Lemma 4.4 says that when a positive tight error falls by a factor of $2n$ , $F_\varepsilon$ becomes strictly larger. Both are numbered results on printed pages 16–17 of the source report's journal counterpart.

Formalization targets

The goal is the circulation-level form of Theorem 4.5. Begin with a circulation $f_0$ and a sequence $f_0,f_1,\ldots$ whose positive-error steps satisfy the contract of Figure 3: if $\varepsilon(f_k)>0$ , the next circulation is $\varepsilon(f_k)/2$ -optimal. With the report's standing $n\ge2$ and $m\ge n-1$ , the target is

\exists k\le m\left\lceil\log_2(2n)\right\rceil:\quad \varepsilon(f_k)=0\quad\text{and}\quad f_k\text{ is minimum-cost}.

The milestone list contains the already proved complementary-slackness characterization of minimum cost (Theorem 2.2), the cross-parameter arc-fixing result (Theorem 4.2), and strict growth of fixed arcs (Lemma 4.4). The report states Theorem 4.5 as $O(m\log n)$ iterations when each refinement decreases error by a constant factor. The target makes explicit the factor two used by the paper's refinements and the resulting finite count.

What the result establishes

The theorem gives a bound on the number of refinement calls that depends on the number of vertices and arcs, not on the magnitude, precision, or integrality of the costs. It gives an exact minimum-cost circulation rather than an arbitrary small-error approximation. This distinguishes the real-cost loop from an integer-cost stopping rule based on $1/n$ . The bound counts refinement calls only; the report analyzes the work within particular implementations separately.

The published 1989 definitions and the complementary-slackness theorem already have machine-checked status on the platform. Theorem 4.2, Lemma 4.4, and this iteration theorem are the open formalization targets. A complete development will connect the tight error to residual-cycle structure, establish that its infimum is attained for circulations, and prove that zero tight error implies minimum cost. The mission thereby makes the fixed-arc argument reusable for other circulation algorithms that lower an approximate-optimality parameter.

Why the bound needs more than repeated halving

Repeatedly dividing a positive real error by two gives errors approaching zero, but it does not by itself produce a finite step with zero error. The missing finite progress is structural: an arc must become fixed after enough reductions, and only finitely many arcs exist. Proving that fixedness is strict is delicate because it compares all circulations at two different error levels, not just two consecutive flows. Theorem 4.2 is the quantitative bridge between a price certificate for one flow and agreement of an arc across every sufficiently accurate flow. At the boundary $\varepsilon=0$ , the printed wording of Lemma 4.4 would require $F_0$ to be a proper subset of itself, so its positive-error regime must be made explicit.

Formalization scope

The Lean network uses CycleCanceling.MinMean.CircNetwork with a finite vertex type, a finite symmetric arc set, and real-valued capacities, costs, and flows. Off-arc values of these functions are irrelevant. The report assumes $m\ge n-1\ge1$ on printed page 5; the theorem binders express it as $n\ge2$ and $m\ge n-1$ . The arc count is for ordered arcs, exactly as the report defines $m$ . No integrality, rounding, or bounded-cost hypothesis is imposed. A feasible initial circulation is required because Figure 3 starts from one; infeasibility detection is outside this target.

The reused 1989 definitions write reduced cost as $c(v,w)+p(v)-p(w)$ . Substituting $-p$ for $p$ gives the report's $c(v,w)-p(v)+p(w)$ , so existential price certificates, $\varepsilon$ -optimality, and absolute reduced-cost conditions agree. The tight error is represented by a real infimum; proving that it is attained is part of the work. The set $F_\varepsilon$ is filtered from $E$ and includes only arcs whose flow is shared by all $\varepsilon$ -optimal circulations. The halving run computes its error from the current circulation; it does not take an unrelated error sequence. Once that error is zero, the loop has returned and later sequence entries are unconstrained. These choices exclude a vacuous or artificially fixed error parameter and a preselected optimal flow.

The explicit reading of the report's asymptotic count is $t=\lceil\log_2(2n)\rceil$ halvings per factor- $2n$ reduction and at most $m$ such blocks, giving $m t$ refinements. This is a statement about refinement count, not a RAM-operation bound. Contributions on Theorem 4.2, the residual-cycle characterization of positive tight error, the fixed-arc strictness lemma, and the final finite counting argument all support the goal. The circulation, price, and fixed-arc infrastructure can be reused beyond this particular implementation.

Selected references

A. V. Goldberg and R. E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987; journal version in Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI: 10.1287/moor.15.3.430. The mission's page and theorem indices refer to the 1987 report.

9 thms3 active usersReviewed

Completed

Machine Learning Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 6: Agnostic Q-NPG for Log-Linear Policies, Bounded by Transfer Error, Excess Risk and Condition NumberResearch Paper

Motivation

Policy gradient methods optimize a decision rule by changing the parameters that determine its action probabilities. In reinforcement learning, the objective is the expected total reward collected over time. Once a policy is restricted to a feature-based class, the best policy may be less effective than the unrestricted optimum. A useful guarantee must therefore compare the computed policy with a chosen comparator and account for both the limits of the features and the error in estimating an update direction. Agarwal, Kakade, Lee and Mahajan give such a guarantee for a version of the natural policy gradient method that fits action values with linear features, called Q-NPG (Agarwal et al., §6.2).

The result matters when a policy has far fewer parameters than there are state-action pairs. A bound phrased only for exact action values or an unrestricted policy class would leave out the errors introduced by fitting from samples and by moving the fitting distribution from the states of a comparator to the states visited by the current policy. Theorem 6.1 keeps those effects visible as separate terms. It also avoids assuming that the comparator is an optimal policy; the comparator can be a policy selected for an application or a benchmark within a restricted class.

Setting

A discounted Markov decision process has a finite state set S, a finite nonempty action set A, transition probabilities P(s'|s,a), immediate rewards r(s,a) in [0,1], and a discount factor γ in [0,1). A policy π assigns a probability distribution over A to every state. The value V^π(s) is the expected sum of discounted rewards from s, and V^π(ρ) averages this value over an initial state distribution ρ. The action value Q^π(s,a) starts by choosing a in s and then follows π. Its advantage is A^π(s,a)=Q^π(s,a)−V^π(s). These are the unnormalized value conventions of §3, pp. 9–12.

For each state-action pair, fix a feature vector φ(s,a) in Euclidean d-space. The log-linear policy with parameter θ assigns probability proportional to exp(θ·φ(s,a)):

\pi_\theta(a\mid s)= \frac{\exp(\theta\cdot\phi(s,a))} {\sum_{a'\in A}\exp(\theta\cdot\phi(s,a'))}.

The Q-NPG fitting loss $L(w;\theta,\upsilon)$ is the mean squared error of predicting $Q^{\pi_\theta}(s,a)$ by $w\cdot\phi(s,a)$ under a state-action distribution $\upsilon$ . Q-NPG uses an approximate minimizer w of this loss under its current on-policy measure and updates θ by ηw. The distribution ν specifies the initial state-action pair for that measure. At time zero, the pair is drawn directly from ν; the given initial action is executed before later actions follow the current policy. These definitions are (19)–(20) of §6.2, pp. 27–28.

The comparison policy π⋆ has discounted state visitation distribution $d^{\pi^\star}_\rho$ . The paper's transfer measure $d^\star$ pairs those states with a uniform action from A. The excess risk measures how much worse an approximate fitting direction is than an exact constrained minimizer under the current on-policy measure. The transfer error measures the exact minimizer's loss under $d^\star$ . A relative condition number κ bounds, in every feature direction, the covariance quadratic form under $d^\star$ by κ times that under ν (Assumptions 6.1–6.2, pp. 28–29).

Formalization targets

Agnostic Q-NPG guarantee

The goal is Theorem 6.1, p. 29. Starting with θ⁽⁰⁾=0, taking T positive updates with step size $\eta=\sqrt{2\log|A|/(B^2W^2T)}$ , bounding feature norms by B and update norms by W, and assuming the expected excess and transfer errors are at most $\varepsilon_{\rm stat}$ and $\varepsilon_{\rm bias}$ , respectively, it asserts

\mathbb E\!\left[ \min_{t<T}\{V^{\pi^\star}(\rho)-V^{\pi_{\theta^{(t)}}}(\rho)\} \right] \le \frac{BW}{1-\gamma}\sqrt{\frac{2\log|A|}{T}} + \sqrt{\frac{4|A|\kappa\varepsilon_{\rm stat}}{(1-\gamma)^3}} + \frac{\sqrt{4|A|\varepsilon_{\rm bias}}}{1-\gamma}.

The expectation encloses the minimum: each random run may have a different best iterate. The claim gives a finite-horizon comparison with π⋆ even when π⋆ is not globally optimal.

Supporting targets

The milestones are the paper's performance-difference identity (Lemma 3.2), smoothness of bounded-feature log-linear policies (Remark 6.7), the deterministic NPG regret lemma (Lemma 6.2), and the two displayed bounds that control transfer and estimation terms ((25) and (26)). Together they connect the MDP's value comparison with the two statistical errors in the goal. Each milestone states a source result rather than a weakened surrogate.

Significance

The theorem separates three quantities that can vary independently in an application: the number of iterations, the statistical quality of the update direction, and the mismatch between the comparator's visited states and the fitting distribution. If both errors vanish, the displayed bound decreases with T at a square-root rate. With imperfect features, the transfer term shows the remaining performance limit. With finite-sample fitting, the excess-risk term shows how estimation quality affects the policy value. This is an agnostic statement because the comparator need not belong to a globally complete policy class (Agarwal et al., Theorem 6.1 and discussion, pp. 29–30).

The paper proves these claims mathematically. This mission asks for machine-checked proofs of the same statements in Lean, including the probabilistic expectation and the exact constants. The reusable parts are the state-action visitation distribution with a prescribed initial action, the log-linear policy and its smoothness property, the least-squares loss, and the deterministic regret lemma. Those objects can support other policy-gradient analyses with different fitting guarantees.

Difficulty

The update direction minimizes a loss under the distribution generated by the current policy, while the value comparison uses states visited by a different policy. The two distributions need not agree, and prediction error under one cannot simply be substituted for error under the other. The relative condition number controls the feature geometry of this shift, while the transfer error separately measures how well an exact on-policy fit predicts under the comparator's measure. Random approximate minimizers add a further layer: the bound concerns the expectation of the best iterate in each run, rather than a deterministic iterate chosen in advance. These are the obstacles identified around Assumptions 6.1–6.2 and the proof of Theorem 6.1.

Formalization scope

The Lean development uses finite state and action types, as in the paper's §3 standing setting. It imports published definitions of transition kernels, policies, occupation probabilities, value and Q-functions, and defines this paper's advantage, discounted visitation, log-linear class and fitting loss on top of them. Parameters and features lie in EuclideanSpace ℝ (Fin d), so the norm is the Euclidean norm used by the paper. A general probability space carries the random update directions and exact constrained minimizers; their measurability and boundedness make the displayed loss expectations integrable.

The action type is nonempty so that the uniform action distribution exists. B and W are positive and T is positive, because the prescribed step size divides by $B^2W^2T$ and the result minimizes over $t<T$ . The comparator is assumed to be a policy, with no optimality hypothesis. The nonnegative condition number is represented by its quadratic-form upper-bound property for every direction. This avoids undefined real ratios when a covariance form vanishes and includes the finite coefficient in Assumption 6.2. The value and loss expressions are calculated from P, r, π and φ; they are not free variables. The Q-NPG parameter sequence is defined by the update rule from θ⁽⁰⁾=0. In particular, the goal does not assume the regret lemma or either of the two statistical inequalities that the proof must establish.

The paper notes that some §6 results extend beyond finite state or action spaces. This mission fixes the finite case inherited from §3. Contributions that prove the source milestones, establish the required summability and integrability facts, or generalize the development to larger measurable spaces are useful; a generalization must keep the same statistical and comparator conventions.

Selected references

Alekh Agarwal, Sham M. Kakade, Jason D. Lee and Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5
Sham M. Kakade and John Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning, 2002. PDF

16 thms3 active usersReviewed

Completed

Machine Learning Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 2: On a Chain MDP All Low-Order Derivatives of the Value Are Exponentially Small at Suboptimal PoliciesResearch Paper

Motivation

Policy gradient methods adjust a policy by following derivatives of its expected reward. A common expectation is that a small gradient indicates a policy close to optimal. For discounted Markov decision processes, that interpretation can fail when a policy rarely reaches the states where reward is available. Agarwal, Kakade, Lee, and Mahajan study this obstruction as part of their analysis of optimality and distribution shift in policy gradient methods. Their chain example makes the obstruction quantitative: even derivatives of several orders can be exponentially small while the value gap grows with the chain length. Agarwal et al., §4.3 and Proposition 4.1.

The example isolates a specific issue for local optimization. A parameter change at an early state affects reward only after the agent has passed through many intermediate decisions. A local derivative therefore measures the behavior of a policy under its own visitation pattern, which can be very different from the visitation pattern of an optimal policy. This mission states the resulting separation with explicit constants rather than treating “vanishing gradients” as a qualitative description.

Setting

A discounted Markov decision process has a finite set of states, a finite set of actions, a transition probability for each state and action, a reward in $[0,1]$ , and a discount $0\le\gamma<1$ . The value $V^\pi(s)$ of a policy $\pi$ is the expected sum of discounted rewards when the process starts in state $s$ and follows $\pi$ . An optimal policy $\pi^\star$ has value at least as large as every other policy at every state. These conventions are those of §3 of the paper and its unnormalized infinite-horizon value definition. Agarwal et al., §3, pp. 9–12.

The central model is a deterministic chain with states $s_0,s_1,\ldots,s_{H+1}$ and four actions. At $s_0$ the process moves to $s_1$ . At each interior state $s_i$ , action $a_1$ moves forward to $s_{i+1}$ , while $a_2,a_3,a_4$ move backward to $s_{i-1}$ . State $s_{H+1}$ is absorbing. The only positive reward is $r(s_{H+1},a_1)=1$ , and $\gamma=H/(H+1)$ . This is Figure 2 and the transition matrix in equation (27). Agarwal et al., Figure 2, p. 11, and (27), p. 50.

The direct policy parameter $\theta$ has three free coordinates at each interior state: the probabilities assigned to $a_1,a_2,a_3$ . The probability of $a_4$ is their complement. Write $\pi_\theta$ for this policy expression and $F_H(\theta)=V^{\pi_\theta}(s_0)$ for its value from the starting state. The paper studies parameters whose free coordinates lie strictly between zero and one and whose forward-action coordinates satisfy $\theta_{i,a_1}<1/4$ .

Formalization targets

The goal is Proposition 4.1. For $H\ge1$ , every such $\theta$ , and every nonnegative integer $k$ satisfying $k\le H/(40\log(2H))-1$ , it asserts the multilinear operator-norm bound

\|\nabla^k F_H(\theta)\|_{\mathrm{op}}\le (1/3)^{H/4}.

The same statement compares this policy with an optimal policy:

V^{\pi^\star}(s_0)-F_H(\theta) \ge \frac{H+1}{8}-\frac{(H+1)^2}{3^H}.

Both clauses and their constants are part of the target. The derivative order includes $k=0$ whenever the displayed threshold admits it. Agarwal et al., Proposition 4.1, p. 16.

Three supporting targets follow the appendix's attack path. First, $F_H(\theta)$ equals the $(0,H+1)$ entry of the resolvent $M^p=(I-\gamma P^p)^{-1}$ , where $p_i=\theta_{i,a_1}$ . Second, equation (32) gives the derivative of any entry of $M^p$ in one forward probability. Third, the appendix separately bounds the optimal value below by $(H+1)/8$ and $F_H(\theta)$ above by $(H+1)^2/3^H$ . A companion theorem records Lemma 3.1: a five-state deterministic example has a value function that is nonconcave in both the direct and softmax parameterizations. Agarwal et al., Appendix B.2, pp. 51, 54, 59; Lemma 3.1, p. 11.

Significance

The proposition supplies an explicit family in which local derivative information, even at orders growing with $H/\log H$ , is small at policies with a large value gap. It limits what a guarantee based only on finding a point with small low-order derivatives can imply about global policy quality. The paper uses this example to motivate attention to state visitation and distribution mismatch in its positive results. Agarwal et al., §4.3, pp. 16–17.

The mathematical result is proved in the cited paper. The remaining work is a machine-checked development of the chain model, its value and resolvent identities, the higher derivative estimates, and the value-gap inequality. The reusable parts include finite-state discounted value calculations, differentiation of a matrix inverse, and operator-norm estimates for multilinear derivatives. The statements in this proposal are proof targets; they do not themselves claim that those proofs have been formalized.

Difficulty

A policy can have a small gradient simply because it almost never reaches the rewarding state. The obvious inference from a near-zero gradient to near-optimal value therefore fails in this model. The technical difficulty is quantitative: each differentiation of a resolvent entry produces terms involving several entries, and the operator norm combines all mixed partial derivatives. The bound must remain exponentially small after that combination, uniformly over every derivative order allowed by the threshold. The second clause must simultaneously show that a policy taking the forward action reaches the reward often enough to create a large value gap. Agarwal et al., Appendix B.2, pp. 54–59.

Formalization scope

States are Fin (H + 2) and actions are Fin 4; the parameter space is EuclideanSpace ℝ (Fin H × Fin 3). Its norm is the Euclidean norm, so the norm of the iterated Fréchet derivative is the paper's multilinear operator norm. The first and last states have no free policy parameters. All four actions at $s_0$ induce the same transition to $s_1$ , and the parameterized policy chooses $a_1$ at both boundary states. The resolvent is the matrix inverse of $I-\gamma P^p$ ; its milestone statements are restricted to interior probabilities $0<p_i<1$ , where that inverse is nonsingular.

The displayed coordinate assumptions of Proposition 4.1 do not require the three free probabilities at a state to sum to at most one. The Lean goal retains exactly those assumptions. Its value expression is still determined by the forward probabilities, because every other action has the same backward transition and only the absorbing state yields reward. This prevents an added simplex constraint from silently narrowing the proposition. A constant function or a free value variable cannot replace the chain value: $F_H$ is computed from the concrete transition and reward arrays.

The development uses the published finite-state transition-kernel, policy, occupation, value, and optimal-policy definitions. Contributions needed for a proof include stochasticity of the chain, geometric-series evaluation of its absorbing reward, nonsingularity and differentiation of its resolvent, and estimates that pass from mixed partial derivatives to the Euclidean operator norm. For the companion example, direct parameters lie in the product of action simplices, with positive discount; at zero discount its value is constant and the nonconcavity claim would be false.

Selected references

Alekh Agarwal, Sham M. Kakade, Jason D. Lee, Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5.

12 thms3 active usersReviewed

Completed

Linear algebra Machine Learning·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers VII: Factor Model Fitting — the ADMM X-Update in Closed Form, Entry by EntryTextbook

Motivation

Alternating direction methods are used when one part of an optimization problem is easy to minimize and another part has a simple projection. Chapter 9 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) examines this idea with nonconvex constraints. Its examples include sparse vectors, Boolean vectors and low-rank matrices. The chapter says explicitly that ADMM can fail to converge in this setting and that a limit need not be globally optimal. The useful claim here is narrower and concrete: several individual updates can still be computed exactly.

The capstone is factor-model fitting. A symmetric data matrix, such as an empirical covariance matrix, is approximated by a positive semidefinite matrix of prescribed rank plus a nonnegative diagonal matrix. This decomposition gives one component that captures shared variation and another that represents coordinate-specific variation. The chapter separates the diagonal fit from the rank constraint and writes the resulting ADMM X-update entry by entry. This mission formalizes that exact update and two other projection rules stated in the same chapter.

Setting

Fix a positive integer $n$ . Write $\mathbb S^n$ for the real symmetric $n\times n$ matrices, and let $\Sigma\in\mathbb S^n$ be the matrix to approximate. The Frobenius norm squares and sums every ordered matrix entry: $\|X\|_F^2=\sum_{i,j}X_{ij}^2$ . A vector $d\in\mathbb R^n$ is nonnegative when $d_i\ge0$ for every $i$ , and $\operatorname{diag}(d)$ places those entries on a diagonal matrix. The book's reduced fitting loss is

f_\Sigma(X)=\inf_{d\ge0}\frac12\|X+\operatorname{diag}(d)-\Sigma\|_F^2.

In the scaled ADMM iteration, $Z$ carries the positive semidefinite rank constraint and $U$ is the scaled dual matrix. Given the current symmetric matrices $Z,U$ and a penalty $\rho>0$ , the X-step minimizes $f_\Sigma(X)+(\rho/2)\|X-Z+U\|_F^2$ over $X\in\mathbb S^n$ . The X-step itself has no rank or positive semidefinite restriction. The following Z-step projects onto the chosen rank-constrained positive semidefinite set. The theorem here concerns the X-step, whose definition is independent of the chosen rank.

The other two results concern Euclidean projection of vectors $v\in\mathbb R^n$ . The cardinality $\operatorname{card}(x)$ is the number of nonzero coordinates of $x$ . The sparse set is $\{x:\operatorname{card}(x)\le c\}$ for a nonnegative integer $c$ . The Boolean cube is $\{0,1\}^n$ . Projection means a nearest point in squared Euclidean distance; it may have more than one value when coordinates tie.

Formalization targets

Partial minimization of the diagonal

The first milestone identifies the book's infimum as the explicit componentwise loss and states that the optimizing diagonal is attained:

f_\Sigma(X)=\frac12\sum_{i\ne j}(X_{ij}-\Sigma_{ij})^2+ \frac12\sum_i(X_{ii}-\Sigma_{ii})_+^2, \qquad d_i=(\Sigma_{ii}-X_{ii})_+.

The sum over $i\ne j$ counts both $(i,j)$ and $(j,i)$ . The statement preserves that convention instead of treating a symmetric matrix as a list of independent upper-triangular entries.

Exact projections for two nonconvex sets

The page 74 milestones say that retaining the $\min(c,n)$ entries of largest absolute value gives a nearest point in $\{x:\operatorname{card}(x)\le c\}$ , and that rounding every coordinate to a nearest element of $\{0,1\}$ gives a nearest Boolean vector. They assert nearest-point status for ties without asserting uniqueness. These are chapter results on the same theme of exact nonconvex updates, although they are independent of the factor-model goal.

Factor-model X-update

The goal identifies the unique symmetric minimizer $X^+$ of the X-subproblem. With $a_{ij}=Z_{ij}-U_{ij}$ , its off-diagonal and diagonal entries are

X^+_{ij}=\frac{\Sigma_{ij}+\rho a_{ij}}{1+\rho}\quad(i\ne j),\qquad X^+_{ii}=\begin{cases} \dfrac{\Sigma_{ii}+\rho a_{ii}}{1+\rho},&\Sigma_{ii}\le a_{ii},\\ a_{ii},&\Sigma_{ii}>a_{ii}. \end{cases}

The target asserts both the formula and global minimality over symmetric matrices. It does not replace minimality with a stationarity condition.

Significance

The exact X-update separates the matrix fit from the nonconvex rank projection. It establishes that the factor-model algorithm's X-step is a well-defined, single-valued minimization for every symmetric current state and every positive penalty. It also makes the one-sided diagonal loss explicit: a nonnegative diagonal can absorb a shortfall below $\Sigma_{ii}$ , but cannot absorb an excess. The two vector projections give similarly exact updates for sparse and Boolean constraint sets.

The mathematical claims are given in §9.1–9.1.2 of the published monograph; they are not open conjectures. The formalization work is to check the infimum, projection and unique-minimizer statements with every domain and tie convention explicit. The mission poses theorem statements for proofs; these draft statements themselves do not yet supply machine-checked proofs. A complete development can reuse its finite matrix loss and finite vector projection vocabulary in other splitting algorithms.

Difficulty

The diagonal partial minimization is one-sided, while the proximal penalty is symmetric around $Z-U$ . An entrywise formula alone does not show that the assembled matrix minimizes the full objective or that it is the only minimizer. Symmetry also couples the two displayed off-diagonal positions $(i,j)$ and $(j,i)$ , so a scalar statement on one entry must agree with its transpose. For sparse projection, ties at the cutoff make a rule phrased as “the projection” ambiguous. For Boolean projection, the midpoint is a tie and requires a declared convention. These issues are part of the theorem statements, not numerical implementation details.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; symmetry is an entrywise equality predicate. The factor-model statements assume $n\ge1$ , symmetric $\Sigma,Z,U$ , and $\rho>0$ . The book uses $Z^k,U^k$ at an iteration; the Lean theorem uses those current matrices as parameters and does not posit convergence of an ADMM sequence. The reduced loss is literally the infimum over all componentwise nonnegative $d$ , and the Frobenius square is the finite sum of entry squares. The stated X-minimization ranges over all symmetric matrices, with no positive semidefinite or rank hypothesis on $X$ .

For sparse vectors, the index set has size $\min(c,n)$ and its selected magnitudes dominate unselected ones. This covers $c=0$ , $c>n$ and cutoff ties. The Boolean rounding function chooses zero when an entry equals $1/2$ . The book uses indices $1,\ldots,n$ ; Fin n uses $0,\ldots,n-1$ . On page 75 the printed diagonal branch conditions omit the superscript $k$ on $Z$ and $U$ ; the formalization uses the current $Z,U$ that appear in the surrounding ADMM update. The theorem requires the candidate to minimize the book's reduced loss, preventing an arbitrary replacement loss from making the statement trivial.

The development needs finite-sum algebra, real infima with an attained lower bound, symmetry of matrices, and nearest-point arguments for finite vectors. The rank- $c$ singular-value projection on page 74 is already an open target elsewhere and is outside this mission. The positive semidefinite rank- $k$ eigenvalue projection on page 76 is also outside this goal; it would require a separate spectral development. Contributions that prove the three milestones or the goal against these definitions are in scope. The page also mentions rounding under integer constraints; this mission selects the preceding Boolean claim as its projection milestone.

Selected references

Stephen Boyd, Neal Parikh, Eric Chu, Borja Peleato and Jonathan Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 73–76, §§9.1–9.1.2. DOI: 10.1561/2200000016.

7 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

Contraction Mappings in the Theory Underlying Dynamic Programming 2: Under N-Stage Contraction and Monotonicity the Optimal Return Is the Unique Fixed Point of the Maximization OperatorResearch Paper

Motivation

Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return $f$ solves the optimality equation $v = Av$ , where $A$ maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return $h$ , contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.

The plain contraction assumption (each one-step operator shrinks distances by a factor $c<1$ ) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only $N$ steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.

Timeline:

1953: Shapley proves that the value of a discounted stochastic game is the fixed point of a contraction.
1960: Howard introduces policy iteration for finite discounted Markov decision processes.
1962–1965: Blackwell studies discrete and discounted dynamic programming, including the existence of optimal stationary policies.
1967: Denardo, in this paper, states the contraction and monotonicity assumptions for an abstract return and proves Theorems 1–4.
1977: Bertsekas, "Monotone mappings with application in dynamic programming", drops contraction and keeps only monotonicity.

Setting

Let $\Omega$ be a set of points. Each point $x$ has a decision set $D_x$ . A policy $\delta$ picks a decision $\delta_x\in D_x$ at every point, so the policy space is $\Delta=\times_{x\in\Omega}D_x$ . Let $V$ be the bounded real functions on $\Omega$ with the metric $\rho(u,v)=\sup_x|u(x)-v(x)|$ ; $V$ is complete. Write $u\ge v$ when $u(x)\ge v(x)$ for every $x$ .

The return $h$ assigns a real number $h(x,d_x,v)$ to each point $x$ , decision $d_x\in D_x$ and $v\in V$ . It defines two kinds of operators on $V$ :

[H_\delta v](x)=h(x,\delta_x,v),\qquad (Av)(x)=\sup_{d_x\in D_x}h(x,d_x,v),

and both are assumed to map $V$ into $V$ . An operator $B$ on $V$ has modulus $c$ or less when $\rho(Bu,Bv)\le c\,\rho(u,v)$ for all $u,v$ .

Monotonicity assumption: if $u\ge v$ then $H_\delta u\ge H_\delta v$ for every $\delta$ .
N-stage contraction assumption: for a positive integer $N$ and a number $c<1$ , both independent of $\delta$ , every $H_\delta^N$ has modulus $c$ or less and every $H_\delta$ has modulus $1$ or less.

Under these assumptions $H_\delta^N$ is a contraction, so it has a unique fixed point $v_\delta$ , the return function of $\delta$ . The optimal return is $f(x)=\sup_\delta v_\delta(x)$ . The auxiliary operator $E$ is $(Ev)(x)=\sup_\delta(H_\delta^Nv)(x)$ .

Formalization targets

Goal: Theorem 4 (p. 169)

Under the monotonicity and N-stage contraction assumptions:

\text{(a) } H_\delta v_\delta=v_\delta \text{ and } v_\delta \text{ is the only fixed point of } H_\delta;\qquad \text{(b) } \rho(v_\delta,v)\le\frac{\rho(H_\delta v,v)\,N}{1-c};

\text{(c) } E \text{ has modulus } c \text{ or less};\qquad \text{(d) } f\in V,\ Ef=f,\ Af=f,\ \text{ and } f \text{ is the only fixed point of } E \text{ and of } A;

\text{(e) } v\le f\ \Longrightarrow\ \rho(A^Nv,f)\le c\,\rho(v,f).

Milestones

The observation at the end of §3 (p. 168): if every operator in a nonempty family has modulus $c$ or less, then their pointwise supremum has modulus $c$ or less, provided it maps $V$ into $V$ .
Lemma 1 (p. 168): under monotonicity, $A$ is monotone; $Av\ge v$ implies that $A^nv$ is nondecreasing in $n$ ; $H_\delta v\ge v$ implies that $H_\delta^nv$ is nondecreasing in $n$ .
Theorem 4 (a)–(c), the part the paper proves in the text of §5 before stating the theorem. This milestone also includes the existence of $E$ as an operator on $V$ and $f\in V$ .
Lemma 2 (p. 169): $Av\le v$ implies $v\ge f$ , and $Av\ge v$ implies $v\le f$ ; $Av_\delta\ge v_\delta$ ; $H_\delta v\ge v$ implies $v_\delta\ge H_\delta v$ .

The mission also contains two consequences that are not milestones: $f$ is optimal for the mathematical programs $\min v$ s.t. $Av\le v$ and $\max v$ s.t. $Av\ge v$ (§6, p. 171), and a policy is optimal exactly when it attains $f(x)=h(x,\delta_x,f)$ at every point (§7, p. 173).

Significance

Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation $v=Av$ has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that $f$ is the least $v$ with $Av\le v$ and the greatest $v$ with $Av\ge v$ . This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization $\Delta^*=\Delta^+$ reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.

The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after $N$ steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.

Difficulty

The obvious argument would apply the Banach fixed-point theorem to $A$ . That does not work: under the N-stage assumption, $A^N$ need not be a contraction. The paper gives an example (p. 170) with $N=2$ , $c=\tfrac12$ , where $A^n$ has modulus $1$ for every $n$ . The supremum over decisions does not commute with composition, so the contraction of each $H_\delta^N$ says nothing directly about $A^N$ . The paper therefore works through the auxiliary operator $E$ , which is a contraction. The hard step is to show that $f$ , the supremum of the policy returns, is a fixed point of $A$ . This is the second half of Lemma 2(a), an $\varepsilon$ -argument that uses both monotonicity and the modulus- $1$ bound on $H_\delta$ .

Part (e) holds only for $v\le f$ . It is not a contraction property of $A^N$ on all of $V$ .

Formalization scope

$V$ is lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is $\rho$ . The order is pointwise (PLe).
$H$ , $A$ and $E$ are given as functions $V\to V$ , which is the paper's "range contained in $V$ ". They are tied to $h$ by IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including $f$ (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.
"Modulus $c$ or less" is the inequality ModulusLE B c. NStageContractionAssumption H N c holds $0<N$ , $c<1$ , ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with $N$ and $c$ independent of $\delta$ .
The return functions are a family v with $H_\delta^Nv_\delta=v_\delta$ , the paper's §5 definition. $H_\delta v_\delta=v_\delta$ is the conclusion (a), never a hypothesis.
In the goal, $E$ is an operator with IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. $f$ is never defined as a fixed point of $A$ or $E$ . The goal asserts that the pointwise least upper bound of $\{v_\delta(x)\}$ exists in $V$ and is the unique fixed point of both.
The trivializing formalizations are ruled out explicitly: assuming $H_\delta v_\delta=v_\delta$ , defining $f$ as $A$ 's fixed point, or dropping $v\le f$ from (e) would each change the theorem.

A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to $H_\delta^N$ ), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.

Selected references

E. V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2) (1967) 165–177. https://doi.org/10.1137/1009030
L. S. Shapley, Stochastic Games, Proc. Nat. Acad. Sci. 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36 (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. P. Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031

7 thms3 active usersReviewed

Completed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case 2: General Demand: Sym-k-Concave Profit-to-Go, Optimal (s, S, A, p) PolicyResearch Paper

Motivation

A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary $k$ -concavity and to optimality of a standard $(s,S,p)$ policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).

Setting

There are periods $t=1,\ldots,T$ . At the start of period $t$ , the firm has inventory $x$ , which may be negative because unmet demand is backlogged. It may order to any level $y\ge x$ . If $y>x$ , it pays a fixed ordering cost $k$ as well as a variable cost $c_t(y-x)$ . After ordering it chooses an expected demand level $d$ in a closed interval $[\underline d_t,\overline d_t]$ . The corresponding price is $P_t(d)$ , the inverse of the period's decreasing demand curve, and expected revenue is $R_t(d)=dP_t(d)$ .

Actual demand is $\alpha_t d+\beta_t$ . The random pair $(\alpha_t,\beta_t)$ has a period-dependent law $\mu_t$ , with $\mathbb E[\alpha_t]=1$ and $\mathbb E[\beta_t]=0$ . No sign restriction is placed on $\alpha_t$ in the paper's general model. The inventory after demand is $y-\alpha_t d-\beta_t$ , incurring a convex holding or backlog cost $h_t$ and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).

The profit-to-go $v_t(x)$ starts with $v_{T+1}(x)=0$ . For a post-order inventory $y$ and expected demand $d$ , write

g_t(y,d)=R_t(d)-c_ty+\mathbb E[-h_t(y-\alpha_t d-\beta_t)+v_{t+1}(y-\alpha_t d-\beta_t)].

The firm maximizes $g_t(y,d)$ over admissible $d$ and then maximizes the resulting value, less the fixed ordering charge, over $y\ge x$ . This defines $v_t(x)$ by equation (2) of the paper. A symmetrically $k$ -convex real function $f$ satisfies

f((1-\lambda)x_0+\lambda x_1)\le(1-\lambda)f(x_0)+\lambda f(x_1)+\max\{\lambda,1-\lambda\}k

for every $x_0,x_1\in\mathbb R$ and $\lambda\in[0,1]$ . A function is symmetrically $k$ -concave when its negative is symmetrically $k$ -convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).

Formalization targets

The goal is Theorem 4.1(c)–(d). If $G_t(y)=\max_{d\in[\underline d_t,\overline d_t]}g_t(y,d)$ , then for every period

G_t\text{ and }v_t\text{ are symmetrically }k\text{-concave}.

There are thresholds $s_t\le S_t$ and a possibly empty set $A_t\subseteq[s_t,(s_t+S_t)/2]$ . An optimal policy orders to $S_t$ if $x<s_t$ or $x\in A_t$ , and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to $S_t$ can use the same demand level $d_t(S_t)$ and hence the same price $P_t(d_t(S_t))$ .

The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier $k$ -convexity to symmetric $k$ -convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.

Significance

The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set $A_t$ records states where ordering to $S_t$ is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).

Formalizing the result requires a reusable account of symmetric $k$ -convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.

Difficulty

In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand $\alpha_t d+\beta_t$ , that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord $k$ -concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within $[s_t,(s_t+S_t)/2]$ . The statement must assert Bellman optimality at every $x$ , including those ties, rather than only the geometry of $A_t$ (Chen and Simchi-Levi, 2004, pp. 891–892).

Formalization scope

The Lean model uses expected demand $d$ as the decision variable and obtains price from $P_t(d)$ , matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers $1,\ldots,T$ , with $T>0$ and terminal value $v_{T+1}=0$ . Random demand is integrated against a probability measure on $\mathbb R\times\mathbb R$ . The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's $O(|y|^\rho)$ statements are encoded by constants multiplying $1+|y|^\rho$ .

The formal assumptions include $k\ge0$ and $c_t\ge0$ , and set $c_{T+1}=0$ where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's $(y,p)$ in Theorem 4.1(b) is expressed as $(y,d)$ through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on $\alpha_t$ .

The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.

Selected references

Xin Chen and David Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. DOI: 10.1287/opre.1040.0127.

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Probability·Captain: mikedeng1

The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs: Fully-Supported Problems Attain the Binomial Violation Tail ExactlyResearch Paper

Motivation

Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter $\delta$ : a solution must satisfy $x\in\mathcal X_\delta$ for every $\delta$ in a possibly infinite set $\Delta$ . Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws $N$ independent samples of $\delta$ , solves the convex program with those $N$ constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.

Timeline.

Calafiore and Campi (Math. Program. 2005; IEEE TAC 2006) introduced the method and bounded the probability that the violation exceeds $\varepsilon$ by a quantity of order $\binom Nd(1-\varepsilon)^{N-d}$ . The bound is valid but loose.
Campi and Garatti (SIAM J. Optim. 2008, this mission's source) proved the bound $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for every convex problem satisfying existence and uniqueness of solutions. They showed it is attained with equality by every fully-supported problem, so it cannot be improved without further assumptions.
Later work extended the result to non-unique solutions, constraint removal, and non-convex decisions (Campi and Garatti, Introduction to the Scenario Approach, SIAM 2018).

Setting

Let $(\Delta,\mathcal D,\mathbb P)$ be a probability space, $c\in\mathbb R^d$ with $d\ge1$ , and let $\mathcal X\subseteq\mathbb R^d$ and $\mathcal X_\delta\subseteq\mathbb R^d$ ( $\delta\in\Delta$ ) be convex closed sets. The violation probability of a point $x$ is

V(x)=\mathbb P\{\delta\in\Delta:\ x\notin\mathcal X_\delta\}.

For a multi-extraction $(\delta^{(1)},\dots,\delta^{(m)})\in\Delta^m$ , the program $P_m$ minimises $c^\top x$ over $x\in\mathcal X\cap\bigcap_{i=1}^m\mathcal X_{\delta^{(i)}}$ . It is assumed that every $P_m$ has a unique solution $x^*_m$ . A constraint $\delta^{(r)}$ is a support constraint of $P_m$ if its removal changes the solution. A convex $P_m$ has at most $d$ support constraints (Proposition 2.2). The problem is fully-supported if, for every $m\ge d$ , the program $P_m$ built from $m$ independent samples has exactly $d$ support constraints with $\mathbb P^m$ -probability one.

Two further objects carry the argument. For $\mathcal I\subseteq\{1,\dots,m\}$ of cardinality $d$ , $S_{\mathcal I}$ is the set of multi-extractions whose support constraints have exactly the indexes in $\mathcal I$ . The violation law is

F(\alpha)=\mathbb P^d\{V(x^*_d)\le\alpha\},

the distribution of the violation of the solution built from $d$ samples.

Formalization targets

Goal: Theorem 2.4, equation (2.3)

For a fully-supported problem, every $N\ge d$ and every $\varepsilon\in[0,1]$ ,

\mathbb P^N\{V(x^*_N)>\varepsilon\}=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.

Milestones (PART 1 of §3)

Proposition 2.2: at most $d$ support constraints.
$S_{\bar{\mathcal I}}\subseteq\widetilde S_{\bar{\mathcal I}}$ for $\bar{\mathcal I}=\{1,\dots,d\}$ , where $\widetilde S_{\bar{\mathcal I}}$ is the set where $\delta^{(d+1)},\dots,\delta^{(m)}$ are not violated by the solution generated by $\delta^{(1)},\dots,\delta^{(d)}$ ; and $\widetilde S_{\bar{\mathcal I}}\subseteq S_{\bar{\mathcal I}}$ up to a probability-zero set.
(3.3): $\mathbb P^m\{S_{\mathcal I}\}=\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)$ for every $\mathcal I$ of cardinality $d$ .
(3.4): $\binom md\int_0^1(1-\alpha)^{m-d}F(\mathrm d\alpha)=1$ for all $m\ge d$ .
Moment uniqueness: $F(\alpha)=\alpha^d$ is the only distribution on $[0,1]$ satisfying (3.4).
(3.2): $F(\alpha)=\alpha^d$ .
Partition chain: $\mathbb P^N\{V(x^*_N)>\varepsilon\}=\binom Nd\int_{(\varepsilon,1]}(1-\alpha)^{N-d}F(\mathrm d\alpha)$ .
Integration by parts: $\binom Nd\int_\varepsilon^1(1-\alpha)^{N-d}\,d\,\alpha^{d-1}\,\mathrm d\alpha=\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ .

Significance

The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on $N$ , $d$ and $\varepsilon$ can be smaller, because a fully-supported problem attains it. The distribution of $V(x^*_N)$ is then a Beta law, $\mathbb P^N\{V(x^*_N)\le\varepsilon\}$ being the probability that a $\mathrm{Binomial}(N,\varepsilon)$ variable is at least $d$ , the same for every fully-supported problem. This is what fixes the sample sizes used in practice: $N$ is chosen so that the binomial tail is below a confidence level $\beta$ . Fact (3.2), that $V(x^*_d)$ has distribution function $\alpha^d$ whatever the problem, is a distribution-free statement of independent interest.

Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on $[0,1]$ given the moments $\int(1-\alpha)^k\,\mathrm dF=1/\binom{d+k}d$ , and the incomplete-beta identity for binomial tails.

Difficulty

The obvious route would compute the law of $V(x^*_N)$ directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of $V(x^*_d)$ only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than $d$ support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first $d$ constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by $d$ .

Formalization scope

Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.

Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so $\bar{\mathcal I}$ is $\{i : i<d\}$ and " $\delta^{(d+1)},\dots,\delta^{(m)}$ " are the indexes $j\ge d$ . $\mathbb P^m$ is Measure.pi (fun _ : Fin m => P). $V$ , the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.

Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve $P_k$ and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of $\{(x,\delta):x\in\mathcal X_\delta\}$ and measurability of the solution maps, the same two hypotheses as the goal. No set $S_{\mathcal I}$ is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.

Conventions. $F$ is the push-forward measure violationLaw on $\mathbb R$ , with $F(\alpha)$ = violationLaw … (Set.Iic α). Integrals against $F$ are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over $[0,1]$ for $\int_0^1$ , and over $(\varepsilon,1]$ for $\int_\varepsilon^1$ in the partition chain, since that integral comes from the event $V>\varepsilon$ . The integration-by-parts identity is a real interval integral. Ranges are $1\le d$ , $d\le m$ , $d\le N$ and $0\le\varepsilon\le1$ .

Ruled out. A pointwise "exactly $d$ support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event $\{V(x^*_N)>\varepsilon\}$ or of $S_{\mathcal I}$ , or the identity $\mathbb P^m\{S_{\mathcal I}\}=\mathbb P^m\{\widetilde S_{\mathcal I}\}$ , as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.

Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on $[0,1]$ , and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.

Selected references

M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19(3) (2008) 1211–1230. https://doi.org/10.1137/07069821X
G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Math. Program. 102 (2005) 25–46. https://doi.org/10.1007/s10107-003-0499-y
G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Trans. Automat. Control 51(5) (2006) 742–753. https://doi.org/10.1109/TAC.2006.875041
M. C. Campi, S. Garatti, Introduction to the Scenario Approach, SIAM, 2018. https://doi.org/10.1137/1.9781611975444
A. N. Shiryaev, Probability, 2nd ed., Springer, 1996, Chapter II, §12. https://doi.org/10.1007/978-1-4757-2539-1

14 thms3 active usersReviewed

Completed

Combinatorics Convex Optimization Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVII: Goemans–Williamson Rounding of the MAXCUT SDP Relaxation Has Expected Value at Least 0.878 Times the Maximum CutTextbook

Motivation

MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor $1/2$ was essentially the best known.

Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least $0.878$ times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant $2/\pi$ .

This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.

Setting

Let $n\ge 0$ and let $A\in\mathbb R^{n\times n}$ be a symmetric matrix with non-negative entries; $A_{i,j}$ is the weight between points $i$ and $j$ . The graph Laplacian is $L=D-A$ , where $D$ is the diagonal matrix with entries $\sum_{j=1}^n A_{i,j}$ . For $x\in\{-1,1\}^n$ the vector $x$ encodes a partition, and MAXCUT is (6.7)

\max_{x\in\{-1,1\}^n} x^\top L x .

Write $\langle M,X\rangle=\operatorname{Tr}(M^\top X)$ for the Frobenius inner product and $\mathbb S^n_+$ for the symmetric positive semidefinite matrices. Since $x^\top Lx=\langle L,xx^\top\rangle$ and $xx^\top\in\mathbb S^n_+$ has unit diagonal, MAXCUT is bounded above by the SDP relaxation

\max\bigl\{\langle L,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1,\ i\in[n]\bigr\}.

A solution $\Sigma$ of the relaxation is any feasible matrix attaining this maximum. The rounding draws $\xi\sim\mathcal N(0,\Sigma)$ , a centered Gaussian vector with covariance $\Sigma$ , and outputs $\zeta=\operatorname{sign}(\xi)\in\{-1,1\}^n$ coordinatewise.

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

For $A$ symmetric with non-negative entries, $L=D-A$ , $\Sigma$ any solution of the relaxation, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$ :

\mathbb E\,\zeta^\top L\zeta\ \ge\ 0.878\max_{x\in\{-1,1\}^n}x^\top Lx.

Milestones

Bounded entries. If $\Sigma\in\mathbb S^n_+$ and $\Sigma_{i,i}=1$ , then $|\Sigma_{i,j}|\le 1$ (remark in the proof of Lemma 6.12).
Lemma 6.12 (Sheppard's formula). If $\xi\sim\mathcal N(0,\Sigma)$ with $\Sigma_{i,i}=1$ and $\zeta=\operatorname{sign}(\xi)$ , then $\mathbb E\,\zeta_i\zeta_j=\frac{2}{\pi}\arcsin(\Sigma_{i,j})$ .
Inequality (6.8). $1-\frac{2}{\pi}\arcsin(t)\ge 0.878(1-t)$ for all $t\in[-1,1]$ .
Relaxation inequality. $\max_{x}x^\top Lx=\max_x\langle L,xx^\top\rangle\le\langle L,\Sigma\rangle$ for every solution $\Sigma$ .

The separately stated Laplacian identity on p. 346 is also included as a theorem item: if $X_{i,i}=1$ for all $i$ , then $\langle L,X\rangle=\sum_{i,j}A_{i,j}(1-X_{i,j})$ ; for $x\in\{-1,1\}^n$ , $x^\top Lx=\sum_{i,j}A_{i,j}(1-x_ix_j)$ .

Companion: Theorem 6.13 (Nesterov)

For $B\in\mathbb S^n_+$ , $\Sigma$ a solution of $\max\{\langle B,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1\}$ , $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$ :

\mathbb E\,\zeta^\top B\zeta\ \ge\ \frac{2}{\pi}\max_{x\in\{-1,1\}^n}x^\top Bx.

Significance

The result. Theorem 6.11 is a polynomial-time randomized $0.878$ -approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to $0.878$ times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.

Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of $\Sigma$ . All three are reusable.

Difficulty

The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair $(\xi_i,\xi_j)$ has the law of $(\langle V_i,\varepsilon\rangle,\langle V_j,\varepsilon\rangle)$ for a standard Gaussian $\varepsilon$ , and then computing an angular measure in the plane, including the degenerate cases $\Sigma_{i,j}=\pm1$ , where the pair is supported on a line. A density-based argument fails there, because $\mathcal N(0,\Sigma)$ has no density when $\Sigma$ is singular, and singular solutions of the relaxation occur (for instance $\Sigma=xx^\top$ ). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ( $0.878$ against the true minimum $\approx0.87856$ ), so crude estimates do not suffice near the minimizer $t\approx-0.689$ .

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. $\mathbb S^n_+$ is Matrix.PosSemidef, which includes symmetry, and $\langle M,X\rangle$ is trace (Mᵀ * X).
$\mathcal N(0,\Sigma)$ is Mathlib's ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite $\Sigma$ , singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.
The sign is $\{-1,1\}$ -valued: $\operatorname{sign}(r)=1$ for $r\ge0$ and $-1$ for $r<0$ . Mathlib's Real.sign would give $\operatorname{sign}(0)=0$ , which takes $\zeta$ out of $\{-1,1\}^n$ ; the two agree almost surely because $\Sigma_{i,i}=1$ .
The maximum over the hypercube is a finite maximum (Finset.sup') over the $2^n$ Boolean vectors read as $\pm1$ vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.
Standing hypotheses: in Theorem 6.11, $A$ symmetric with non-negative entries (the book's MAXCUT setting); in Lemma 6.12, $\Sigma$ positive semidefinite (implicit in " $\xi\sim\mathcal N(0,\Sigma)$ "); in Theorem 6.13, $B$ positive semidefinite. The identities of milestones 4 and 5 hold for every real matrix $A$ and are stated without hypotheses on $A$ .
Ruled out: tying $\xi$ 's law to anything other than $\Sigma$ , or dropping optimality of $\Sigma$ , would make the goal false or vacuous; here the law is exactly $\mathcal N(0,\Sigma)$ and $\Sigma$ is a maximizer.
Welcome contributions: Sheppard's formula in Mathlib's multivariate Gaussian language, a proof of (6.8), and the Schur product theorem ( $A,B\succeq0\Rightarrow A\circ B\succeq0$ ) used in Theorem 6.13.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6):1115–1145, 1995. doi:10.1145/227683.227684
Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optim. Methods Softw. 9(1–3):141–160, 1998. doi:10.1080/10556789808805690
S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37(1):319–357, 2007. doi:10.1137/S0097539705447372
W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation, Phil. Trans. R. Soc. A 192:101–167, 1899. doi:10.1098/rsta.1899.0003

6 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVI: Random Coordinate Descent RCD(γ) on a Strongly Convex Coordinate-Smooth Function Has Rate (1 − 1/κ_γ)^tTextbook

Motivation

When a problem has millions of variables, even one full gradient can be too expensive to compute, while a single partial derivative $\partial f/\partial x_i$ is often cheap: in regularized regression, support vector machines and many structured problems, updating one coordinate costs a small fraction of a full gradient step. Coordinate descent methods exploit this by moving along one coordinate at a time. They are among the oldest optimization schemes and were for a long time analysed only for cyclic orders and only asymptotically.

Nesterov (2012) showed that choosing the coordinate at random, with probabilities depending on the coordinate-wise smoothness constants, gives global, non-asymptotic rates that can beat full gradient descent in total work. This mission formalizes that analysis as presented in §6.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 338–342, and in particular its linear rate for strongly convex functions (Theorem 6.8).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be differentiable, write $\nabla_i f(x)=\frac{\partial f}{\partial x_i}(x)$ and let $e_i$ be the $i$ -th standard basis vector. The function is directionally smooth with constants $\beta_1,\dots,\beta_n>0$ if

|\nabla_i f(x+ue_i)-\nabla_i f(x)|\le\beta_i|u|\qquad\text{for all } i\in[n],\ x\in\mathbb R^n,\ u\in\mathbb R,

equivalently, each one-variable restriction $u\mapsto f(x+ue_i)$ is $\beta_i$ -smooth.

For a real exponent $c$ , the weighted norms are

\|x\|_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{c}x_i^2},\qquad \|x\|^*_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{-c}x_i^2}.

For $\alpha>0$ , $f$ is $\alpha$ -strongly convex w.r.t. a norm $\|\cdot\|$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y$ . The point $x^*$ is a minimizer of $f$ .

For $\gamma\ge0$ , RCD( $\gamma$ ) starts at $x_1\in\mathbb R^n$ and iterates

x_{s+1}=x_s-\frac{1}{\beta_{i_s}}\nabla_{i_s}f(x_s)\,e_{i_s},

where $i_1,i_2,\dots$ are drawn independently from $p_\gamma(i)=\beta_i^\gamma/\sum_{j}\beta_j^\gamma$ . The case $\gamma=0$ is uniform sampling; $\gamma=1$ samples proportionally to $\beta_i$ .

Formalization targets

Goal: Theorem 6.8 (p. 341)

Let $\gamma\ge0$ , let $f$ be $\alpha$ -strongly convex w.r.t. $\|\cdot\|_{[1-\gamma]}$ and directionally smooth with constants $\beta_i$ , and let $\kappa_\gamma=\sum_i\beta_i^\gamma/\alpha$ . Then for every $t\ge0$

\mathbb E f(x_{t+1})-f(x^*)\le\Big(1-\frac{1}{\kappa_\gamma}\Big)^t\big(f(x_1)-f(x^*)\big).

Milestones

Lemma 6.9 (p. 341): for $f$ $\alpha$ -strongly convex w.r.t. any norm, $f(x)-f(x^*)\le\frac{1}{2\alpha}\|\nabla f(x)\|_*^2$ .
One coordinate step (p. 340): $f\big(x-\frac{1}{\beta_i}\nabla_i f(x)e_i\big)-f(x)\le-\frac{1}{2\beta_i}(\nabla_i f(x))^2$ .
Expected decrease (p. 340): $\mathbb E_{i_s}f(x_{s+1})-f(x_s)\le-\frac{1}{2\sum_i\beta_i^\gamma}\big(\|\nabla f(x_s)\|^*_{[1-\gamma]}\big)^2$ .
Lemma 6.9 in the weighted norm (p. 342): $\big(\|\nabla f(x)\|^*_{[1-\gamma]}\big)^2\ge2\alpha(f(x)-f(x^*))$ .
Contraction (pp. 341–342): one step multiplies the expected gap by at most $1-1/\kappa_\gamma$ .

Companion: Theorem 6.7 (pp. 339–340)

For $f$ convex and directionally smooth, and $t\ge2$ ,

\mathbb E f(x_t)-f(x^*)\le\frac{2R_{1-\gamma}^2(x_1)\sum_i\beta_i^\gamma}{t-1},\qquad R_{1-\gamma}(x_1)=\sup_{f(x)\le f(x_1)}\|x-x^*\|_{[1-\gamma]}.

Significance

Theorem 6.8 says random coordinate descent converges linearly, with a rate governed by $\sum_i\beta_i^\gamma/\alpha$ instead of the global smoothness constant. For $\gamma=1$ , directional smoothness implies $f$ is $\beta$ -smooth with $\beta\le\sum_i\beta_i$ , so for functions whose global smoothness constant is of the order of $\sum_i\beta_i$ , RCD(1) attains the accuracy of gradient descent after the same number of iterations (book, p. 340, comparing Theorem 6.7 with Theorem 3.3), while each iteration touches a single coordinate. The same per-step inequalities underlie later accelerated and parallel coordinate methods.

These results are proved in the literature (Nesterov 2012; Bubeck 2015). Their contribution here is a machine-checked version. As far as a search of the Prove2Me catalogue shows, no coordinate descent rate of this kind has been formalized there; a Euclidean-norm special case of Lemma 6.9 exists on the platform as a separate result, but not the arbitrary-norm lemma or the weighted-norm instance used here.

Difficulty

The main obstacle is bookkeeping of the randomness: the per-step inequality holds for each fixed iterate, while the theorem is about the expectation over the whole sequence of draws $i_1,\dots,i_t$ , so the pointwise contraction has to be passed through the tower of conditional expectations. In the strongly convex case this is linear and exact; for Theorem 6.7 the recursion on $\delta_s=\mathbb Ef(x_s)-f(x^*)$ is quadratic, and since $\delta_s$ is an expectation while the gradient norm at $x_s$ is random, the pointwise inequality does not transfer to $\delta_s$ verbatim. A second point is geometric: strong convexity, the dual norm and the sampling distribution must use matching weights ( $\beta_i^{1-\gamma}$ against $\beta_i^{\gamma}$ ), and a mismatch silently changes the constant.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map $g$ with HasGradientAt f (g x) x, so $\nabla_i f(x)=g(x)_i$ . Lemma 6.9 is stated for a finite-dimensional real normed space with the Fréchet derivative and the operator norm as the dual norm.
Powers $\beta_i^c$ are real powers. The theorems assume $n\ge1$ , $\alpha>0$ and $\beta_i>0$ , which the book uses implicitly; $\gamma\ge0$ is the book's.
RCD(γ) is a deterministic function of the drawn coordinates, and the expectation over $t$ independent draws from $p_\gamma$ is the finite sum $\sum_{(i_1,\dots,i_t)\in[n]^t}\prod_s p_\gamma(i_s)\,F(i_1,\dots,i_t)$ . No measure theory or integrability conventions are involved.
The minimizer $x^*$ is assumed to exist, as the book does throughout; its uniqueness, which the book assumes "only for sake of notation", is not used.
In Theorem 6.7 the supremum $R_{1-\gamma}(x_1)$ is passed as any real upper bound $R$ on the sublevel set, which is equivalent when the supremum is finite and avoids Lean's value $0$ for an unbounded supremum.
Directional smoothness is required at every $x$ and $u$ , and $p_\gamma$ is fixed by the $\beta_i$ ; neither is weakened to hold only along the iterates, which would change the theorem.

A complete development needs the one-dimensional descent lemma (3.5), weighted Cauchy–Schwarz for the dual pair $\|\cdot\|_{[c]},\|\cdot\|^*_{[c]}$ , and a decomposition of the finite expectation over $[n]^{t+1}$ into the last draw and the first $t$ . The weighted-norm and finite-expectation lemmas are reusable for other randomized coordinate and sampling methods. Proofs of the milestones and of either theorem are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §6.4, pp. 338–342.
Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2):341–362, 2012. doi:10.1137/100802001
P. Richtárik and M. Takáč, Parallel coordinate descent methods for big data optimization, Mathematical Programming 156:433–484, 2016. arXiv:1212.0873

7 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XV: SVRG with η = 1/(10β) and k = 20κ Contracts the Expected Optimality Gap by 0.9 per EpochTextbook

Motivation

Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.

Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order $(m+\kappa)\log(1/\varepsilon)$ for the same regime, where $m$ is the number of components and $\kappa$ is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.

Setting

Let $f_1,\ldots,f_m:\mathbb R^n\to\mathbb R$ be differentiable convex functions, with $m\ge1$ , and define the finite-sum objective and its gradient by

f(x)=\frac1m\sum_{i=1}^m f_i(x),\qquad G(x)=\frac1m\sum_{i=1}^m \nabla f_i(x).

Each component is $\beta$ -smooth when its gradient is $\beta$ -Lipschitz in the Euclidean norm: $\|\nabla f_i(x)-\nabla f_i(z)\|_2\le\beta\|x-z\|_2$ for all $x,z$ . The average $f$ is $\alpha$ -strongly convex, meaning that for all $x,z$ it lies at least $\frac\alpha2\|z-x\|_2^2$ above its first-order affine approximation at $x$ . The constants $\alpha$ and $\beta$ are positive, $x^*$ minimizes $f$ over $\mathbb R^n$ , and $\kappa=\beta/\alpha$ .

An epoch begins at an anchor $y$ . Its first inner iterate is $x_1=y$ . For $t=1,\ldots,k$ , draw $i_t$ uniformly from $\{1,\ldots,m\}$ , independently across steps and epochs, and update

x_{t+1}=x_t-\eta\bigl(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)+G(y)\bigr).

The next anchor is the average $y^+=k^{-1}\sum_{t=1}^k x_t$ . In particular, this average uses $x_1$ through $x_k$ , while the last updated point $x_{k+1}$ is excluded. Starting from an arbitrary $y^{(1)}$ and repeating the epoch produces $y^{(s+1)}$ . The expectation of $f(y^{(s+1)})$ is over all $sk$ sampled indices in the first $s$ epochs.

Formalization targets

Goal: geometric contraction across epochs

Theorem 6.5 sets $\eta=1/(10\beta)$ and $k=20\kappa$ and asserts, for every $s\ge1$ ,

\mathbb E f(y^{(s+1)})-f(x^*) \le 0.9^s\bigl(f(y^{(1)})-f(x^*)\bigr).

The epoch length is a count, so the statement takes $k\in\mathbb N$ and explicitly requires $k=20\beta/\alpha$ . The goal uses exactly the book's step size, epoch length, and contraction factor.

Milestones: second moments and a single epoch

Lemma 6.4 bounds $\mathbb E_i\|\nabla f_i(x)-\nabla f_i(x^*)\|_2^2$ by $2\beta(f(x)-f(x^*))$ . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to $x^*$ . The later display on p. 338 bounds one epoch for any positive step size with $2\beta\eta<1$ . Finally, equation (6.1) substitutes the stated constants to obtain the factor $0.9$ for one epoch. These seven source claims form the milestone list in reading order.

Significance

The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap $D$ falls below $0.9^sD$ in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.

The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.

Difficulty

The sampled component gradient $\nabla f_{i_t}(x_t)$ need not be small when $x_t$ is near $x^*$ , so a bound using only its norm does not yield the desired fixed-step contraction. The correction $-\nabla f_{i_t}(y)+G(y)$ has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both $x_t$ and $y$ . The proof must control those two gaps while respecting the fact that $x_t$ depends on earlier samples. A single-index estimate with $x_t$ held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and $m\ge1$ and $k\ge1$ prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.

The component assumptions include differentiability with an explicit gradient map, convexity on all of $\mathbb R^n$ , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing $x^*$ exists; this is explicit. Positivity of $\alpha$ and $\beta$ , and integrality of $20\beta/\alpha$ , make the displayed divisions and epoch length meaningful. The general epoch bound also requires $0<\eta$ and $2\beta\eta<1$ . Dimension zero is allowed: the theorem remains a statement about the unique point of $\mathbb R^0$ and its zero objective gap.

The direction always contains the sampled difference $\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)$ and the full anchor gradient $G(y)$ . Replacing that direction with $G(x_t)$ would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.

Selected references

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, pp. 231–358. arXiv:1405.4980v2
Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, Advances in Neural Information Processing Systems 26 (NIPS), 2013 (the origin of SVRG, cited by Bubeck on p. 335). https://proceedings.neurips.cc/paper/2013/hash/ac1dd209cbcc5e5d1c6e28598e8cbbe8-Abstract.html

10 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XIV: Stochastic Mirror Descent on a β-Smooth Function with Noise σ Has Rate Rσ√(2/t) + βR²/tTextbook

Motivation

Many optimization problems in statistics and machine learning ask to minimize an expected loss $f(x)=\mathbb E_\xi\,\ell(x,\xi)$ , or an average $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ over a large data set. Exact gradients of such an $f$ are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.

Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order $1/\sqrt t$ and a smoothness term of order $1/t$ . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ . Gradients are linear forms $g$ on $E$ , the value of $g$ at $v$ is written $g^\top v$ , and the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ . Let $\mathcal X\subseteq E$ be compact and convex.

A mirror map is a function $\Phi$ on an open convex set $\mathcal D$ with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . It is strictly convex and differentiable on $\mathcal D$ , its gradient $\nabla\Phi$ takes every value, and $\|\nabla\Phi(x)\|_*\to\infty$ as $x$ approaches the boundary of $\mathcal D$ . Its Bregman divergence is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ . The map is 1-strongly convex on $\mathcal X\cap\mathcal D$ if $D_\Phi(y,x)\ge\frac12\|x-y\|^2$ there. A function $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

A stochastic oracle returns, at a query point $x$ , a random linear form $\tilde g(x)$ . When the query point is itself random, the book requires the conditional expectation given the query point, $\mathbb E(\tilde g(x)\mid x)$ , to be a subgradient of $f$ at $x$ . In the smooth case it requires $\mathbb E(\tilde g(x)\mid x)=\nabla f(x)$ together with the variance bound $\mathbb E(\|\tilde g(x)-\nabla f(x)\|_*^2\mid x)\le\sigma^2$ .

S-MD with step $\gamma$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, writing $\tilde g_s=\tilde g(x_s)$ , iterates

x_{s+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}\ \gamma\,\tilde g_s^\top x+D_\Phi(x,x_s).

Let $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , and let $x^*$ minimize $f$ on $\mathcal X$ .

Formalization targets

Goal: Theorem 6.3

Let $f$ be convex and $\beta$ -smooth, and let the oracle have variance at most $\sigma^2$ . Then for every $t\ge1$ , S-MD with step $1/(\beta+1/\eta)$ and $\eta=\frac R\sigma\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^t x_{s+1}\Big)-f(x^*)\le R\sigma\sqrt{\frac2t}+\frac{\beta R^2}{t}.

Milestones (the proof's four displays)

For points $x_s,x_{s+1}\in\mathcal X\cap\mathcal D$ and $\eta>0$ , the smoothness step is

f(x_{s+1})-f(x_s)\le\tilde g_s^\top(x_{s+1}-x_s)+\tfrac\eta2\|\nabla f(x_s)-\tilde g_s\|_*^2+(\beta+1/\eta)D_\Phi(x_{s+1},x_s).

If $x_{s+1}$ is the S-MD step, the mirror step is

\tfrac{1}{\beta+1/\eta}\tilde g_s^\top(x_{s+1}-x^*)\le D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})-D_\Phi(x_{s+1},x_s).

Combining the two gives a pathwise bound on $f(x_{s+1})$ with the cross term $(\tilde g_s-\nabla f(x_s))^\top(x^*-x_s)$ . Taking expectations gives the expected one-step bound

\mathbb Ef(x_{s+1})-f(x^*)\le(\beta+1/\eta)\,\mathbb E\big(D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})\big)+\frac{\eta\sigma^2}{2}.

Companion: Theorem 6.1 and (4.10)

For a convex $f$ with $\mathbb E(\|\tilde g(x)\|_*^2\mid x)\le B^2$ , S-MD with $\eta=\frac RB\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^tx_s\Big)-\min_{\mathcal X}f\le RB\sqrt{2/t}.

This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors $g_s$ :

\sum_{s\le t}g_s^\top(x_s-x)\le\frac{R^2}{\eta}+\frac{\eta}{2\rho}\sum_{s\le t}\|g_s\|_*^2.

Significance

Theorem 6.3 says exactly how much smoothness helps under noise. As $\sigma\to0$ it recovers the $\beta R^2/t$ rate of deterministic smooth optimization. For large $t$ the noise term $R\sigma\sqrt{2/t}$ dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging $m$ independent oracle answers divides the variance by $m$ , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by $\sqrt m$ while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.

These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.

Difficulty

The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point $x_s$ is random, so unbiasedness enters only through the conditional expectation given $x_s$ . Making the cross term vanish requires pulling the $\sigma(x_s)$ -measurable vector $x^*-x_s$ out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When $\nabla\Phi$ blows up at the boundary of $\mathcal D$ , the Bregman terms $D_\Phi(x^*,x_s)$ are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer $x^*$ may lie on the boundary of $\mathcal D$ , where $\Phi$ is not part of the book's data. Treating $\mathbb E$ informally, or assuming $x^*\in\mathcal D$ , skips exactly these points.

Formalization scope

Spaces and gradients. $E$ is a finite-dimensional real normed space. Gradients are explicit maps Φ' f' : E → (E →L[ℝ] ℝ), $g^\top v$ is g v, and $\|\cdot\|_*$ is the operator norm. $\beta$ -smoothness is stated with derivatives relative to $\mathcal X$ . $\Phi$ is a total function, constrained only by the mirror-map axioms on $\mathcal D$ .
Runs and oracle. S-MD is a run predicate. For every outcome, $x_1$ minimizes $\Phi$ on $\mathcal X\cap\mathcal D$ , and $x_{s+1}$ is some minimizer of the step objective. The oracle is a predicate on the random sequences $(x_s,\tilde g_s)$ : each $x_s$ is measurable, and the conditional expectations are taken given $\sigma(x_s)$ . Every conditioned quantity is integrable.
Conclusions. Every bound on an expectation also asserts integrability. Without it, the Lean integral of a non-integrable function is $0$ and the bound could hold trivially.
Standing assumptions. The book's $R^2=\sup(\Phi-\Phi(x_1))$ is replaced by any upper bound $R^2$ . The minimizer $x^*\in\mathcal X$ exists (p. 242). $\mathcal X$ is compact and convex (Chapter 4), and convex functions are closed (p. 236).
Positivity side conditions. $R,\sigma,B>0$ and $t\ge1$ make the step sizes and bounds defined, and $\beta\ge0$ .

A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let $x_{s+1}$ be an arbitrary point of $\mathcal X\cap\mathcal D$ would make the theorems false, and are not used either.

A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, https://arxiv.org/abs/1405.4980 (Chapter 6, pp. 329–333; Chapter 4, pp. 297–307).
O. Dekel, R. Gilad-Bachrach, O. Shamir, L. Xiao, Optimal distributed online prediction using mini-batches, Journal of Machine Learning Research 13:165–202, 2012. https://jmlr.org/papers/v13/dekel12a.html
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277

6 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XII: Mirror Prox on a Convex β-Smooth Function Has Rate βR²/(ρt)Textbook

Motivation

First-order methods for constrained convex optimization are usually analysed in the Euclidean norm, where gradient descent and its projected and accelerated variants have well-understood rates. Many constraint sets of practical interest, such as the probability simplex, the $\ell_1$ ball and the spectrahedron, are poorly adapted to the Euclidean geometry: the Euclidean diameter and the Euclidean Lipschitz or smoothness constants grow with the dimension. Mirror descent, due to Nemirovski and Yudin, replaces the Euclidean step by a step taken in the dual space through a mirror map $\Phi$ , so that the rate depends on constants measured in a norm matched to the set. For non-smooth Lipschitz functions it attains the rate $1/\sqrt t$ (Theorem 4.2 of the source, the subject of the previous mission of this series).

For smooth functions, a rate of order $1/t$ is available in any geometry by an extragradient-type modification. Mirror prox was introduced by Nemirovski in 2004 (Prox-method with rate of convergence O(1/t)) for variational inequalities with Lipschitz monotone operators and convex–concave saddle-point problems. It is the basis of smoothing approaches to non-smooth optimization and of stochastic saddle-point methods. This mission formalizes the version for minimizing a single smooth convex function, Theorem 4.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), §4.5.

Setting

Fix an arbitrary norm $\|\cdot\|$ on a finite-dimensional real space $E$ . Gradients are linear functionals on $E$ ; for a functional $g$ write $g^\top v$ for its value at $v$ , and $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ for the dual norm. Let $\mathcal X\subseteq E$ be compact and convex.

The Bregman divergence of a differentiable $\Phi$ is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ .
Let $\mathcal D$ be a convex open set with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . A mirror map on $\mathcal D$ is a function $\Phi$ that is strictly convex and differentiable on $\mathcal D$ , whose gradient takes every value ( $\nabla\Phi(\mathcal D)$ is the whole dual space), and whose gradient norm tends to $+\infty$ at the boundary of $\mathcal D$ .
The Bregman projection of $y\in\mathcal D$ is $\Pi^\Phi_{\mathcal X}(y)=\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y)$ .
$\Phi$ is $\rho$ -strongly convex on $\mathcal X\cap\mathcal D$ if $\Phi(x)-\Phi(y)\le\nabla\Phi(x)^\top(x-y)-\frac\rho2\|x-y\|^2$ there; $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

Mirror prox with step size $\eta$ generates, from $x_t$ ,

\nabla\Phi(y'_{t+1})=\nabla\Phi(x_t)-\eta\nabla f(x_t),\qquad y_{t+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y'_{t+1}),

\nabla\Phi(x'_{t+1})=\nabla\Phi(x_t)-\eta\nabla f(y_{t+1}),\qquad x_{t+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,x'_{t+1}).

The first half is a mirror descent step from $x_t$ to $y_{t+1}$ ; the second restarts from $x_t$ with the gradient evaluated at $y_{t+1}$ .

Formalization targets

Goal: Theorem 4.4

With $\eta=\rho/\beta$ , $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ , $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , $f$ convex and $\beta$ -smooth and $x^*$ a minimizer of $f$ on $\mathcal X$ , for every $t\ge1$

f\Bigl(\frac1t\sum_{s=1}^t y_{s+1}\Bigr)-f(x^*)\le\frac{\beta R^2}{\rho t}.

Milestones

Lemma 4.1 (Bregman projections): $(\nabla\Phi(\Pi^\Phi_{\mathcal X}(y))-\nabla\Phi(y))^\top(\Pi^\Phi_{\mathcal X}(y)-x)\le0$ and $D_\Phi(x,\Pi^\Phi_{\mathcal X}(y))+D_\Phi(\Pi^\Phi_{\mathcal X}(y),y)\le D_\Phi(x,y)$ for $x\in\mathcal X\cap\mathcal D$ , $y\in\mathcal D$ .
First term: $\eta\nabla f(y_{t+1})^\top(x_{t+1}-x)\le D_\Phi(x,x_t)-D_\Phi(x,x_{t+1})-D_\Phi(x_{t+1},x_t)$ .
Second term, (4.9): $\eta\nabla f(x_t)^\top(y_{t+1}-x_{t+1})\le D_\Phi(x_{t+1},x_t)-\frac\rho2\|x_{t+1}-y_{t+1}\|^2-\frac\rho2\|y_{t+1}-x_t\|^2$ .
Third term: $(\nabla f(y_{t+1})-\nabla f(x_t))^\top(y_{t+1}-x_{t+1})\le\frac\beta2\|y_{t+1}-x_t\|^2+\frac\beta2\|y_{t+1}-x_{t+1}\|^2$ .
Per-step bound: $f(y_{t+1})-f(x)\le\bigl(D_\Phi(x,x_t)-D_\Phi(x,x_{t+1})\bigr)/\eta$ for $x\in\mathcal X\cap\mathcal D$ .

The three-point identity (4.1), $(\nabla f(x)-\nabla f(y))^\top(x-z)=D_f(x,y)+D_f(z,x)-D_f(z,y)$ , is already posed on the platform as BeckTeboulleMD.EMDA.lemma_4_1 and is included by reference.

Significance

Theorem 4.4 shows that the $1/t$ rate of gradient descent on smooth functions survives in non-Euclidean geometries, with the dimension entering only through $R^2/\rho$ . With the negative entropy on the simplex, $R^2/\rho$ is of order $\log n$ for the $\ell_1$ norm, against a polynomial dependence for Euclidean methods. Beyond this single-function version, the same three-term argument is the core of the analysis of mirror prox for monotone variational inequalities and saddle-point problems (§4.6 and §5.2 of the source), where it gives the $1/t$ rate for smooth convex–concave games.

The result is proved in the source and in Nemirovski's paper. As far as this mission is aware it has no machine-checked proof; Mathlib has no Bregman divergences, mirror maps or mirror-descent-type algorithms. A formal proof would supply reusable infrastructure: the Bregman projection lemma (Lemma 4.1) and the three-point identity are used by every mirror-descent analysis, including the stochastic and online variants later in the source.

Difficulty

The obvious argument for mirror descent bounds $f(x_t)-f(x)$ by $\nabla f(x_t)^\top(x_t-x)$ and leaves a stability term of size $\eta^2\|\nabla f\|_*^2$ , which yields only $1/\sqrt t$ . Smoothness has to be used to cancel that term, and a single gradient step does not do so in a general norm. Mirror prox evaluates the gradient at the extrapolated point $y_{t+1}$ ; the analysis must show that the error created by using $\nabla f(x_t)$ for the first step is paid for by the strong convexity of $\Phi$ , which requires splitting $\nabla f(y_{t+1})^\top(y_{t+1}-x)$ into three terms and bounding each with matching constants.

In Lean the difficulty is in the infrastructure: first-order optimality of a Bregman projection over $\mathcal X\cap\mathcal D$ , which need not be closed; the passage from $x\in\mathcal X\cap\mathcal D$ to a minimizer $x^*$ that may lie on the boundary of $\mathcal D$ ; and Jensen's inequality for the average of the $y_{s+1}$ .

Formalization scope

$E$ is a finite-dimensional real normed space. Gradients are continuous linear functionals E →L[ℝ] ℝ given by explicit maps Φ' and f'; the dual norm is the operator norm. Φ' is the Fréchet derivative of $\Phi$ at each point of $\mathcal D$ ; f' is the derivative of $f$ relative to $\mathcal X$ at each point of $\mathcal X$ .
The mirror map definition keeps all three properties of §4.1, including surjectivity of the gradient and divergence at each frontier point of $\mathcal D$ .
Projections and runs are relations: every admissible argmin choice is covered; no choice function is used. The run is indexed from $t=1$ ; index $0$ is unused.
Standing and implicit hypotheses: $\mathcal X$ compact convex; a minimizer $x^*\in\mathcal X$ exists (the source's standing assumption); $\rho>0$ and $\beta>0$ (so that $\eta=\rho/\beta$ and the division by $\rho t$ are meaningful); $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ (unspecified in §4.5, taken as in mirror descent, §4.2).
$R$ is any real with $\Phi-\Phi(x_1)\le R^2$ on $\mathcal X\cap\mathcal D$ . The source's $R^2=\sup$ is the case where the supremum is finite; when it is infinite, the source's bound is void.
A run in which the second step started from $y_{t+1}$ , or projected $y'_{t+1}$ again, would be mirror descent, for which the claimed rate is false; the formal run follows the four equations of the source exactly. The average is over the extrapolated points $y_{s+1}$ , $s=1,\dots,t$ .

Contributions welcome: proofs of Lemma 4.1 and the three-term bounds, which are reusable for the stochastic mirror descent and saddle-point missions of this series, and the final telescoping and limit argument.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980v2
A. Nemirovski, Prox-method with rate of convergence O(1/t) for variational inequalities with Lipschitz continuous monotone operators and smooth convex-concave saddle point problems, SIAM Journal on Optimization 15(1):229–251, 2004. https://doi.org/10.1137/S1052623403425629
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

8 thms3 active usersReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XI: Mirror Descent with a ρ-Strongly Convex Mirror Map Has Rate RL√(2/(ρt))Textbook

Motivation

The projected subgradient method of Chapter 3 measures distances in the Euclidean norm, and its rate $RL/\sqrt t$ depends on the geometry only through a Euclidean radius $R$ and a Euclidean bound $L$ on the subgradients. For many constraint sets that occur in practice this is the wrong geometry. On the probability simplex $\Delta_n$ with subgradients bounded in $\ell_\infty$ , as for linear losses with bounded coefficients, the Euclidean constants make $RL$ grow like $\sqrt n$ , while the problem itself is nearly dimension-free.

Mirror descent, introduced by Nemirovski and Yudin (1983), repairs this. The gradient step is taken in the dual space, after mapping the current point through the gradient of a strictly convex mirror map $\Phi$ , and feasibility is restored by a projection in the Bregman divergence of $\Phi$ rather than in the Euclidean distance. Beck and Teboulle (2003, doi:10.1016/S0167-6377(02)00231-6) recast it as a nonlinear projected subgradient method and showed that with the negative entropy on the simplex its rate is $O(L\sqrt{\log n/t})$ . Nesterov (2009, doi:10.1007/s10107-007-0149-x) introduced dual averaging, a lazy variant that averages the subgradients in the dual space and maps back only when a primal point is needed. Both methods underlie online learning (exponential weights is mirror descent with the entropy), stochastic optimization, and saddle-point methods such as mirror prox.

This mission is the eleventh of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980). It covers the preamble of Chapter 4, Sections 4.1 and 4.2, and Section 4.4.

Setting

Let $E$ be a finite-dimensional real vector space (the book's $\mathbb R^n$ ) with an arbitrary norm $\|\cdot\|$ . A linear functional $g$ on $E$ acts on $x$ by $g^\top x$ and has dual norm $\|g\|_*=\sup_{\|x\|\le1}g^\top x$ . Let $\mathcal X\subseteq E$ be compact and convex.

Let $\mathcal D\subseteq E$ be a convex open set with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\neq\emptyset$ . A function $\Phi:\mathcal D\to\mathbb R$ is a mirror map if it is strictly convex and differentiable, its gradient takes every value in the dual space, and $\|\nabla\Phi(x)\|\to+\infty$ as $x$ tends to the boundary of $\mathcal D$ . Its Bregman divergence is

D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y),

and the Bregman projection of $y\in\mathcal D$ is $\Pi^\Phi_{\mathcal X}(y)=\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y)$ . The mirror map is $\rho$ -strongly convex on $\mathcal X\cap\mathcal D$ if $\Phi(x)-\Phi(y)\le\nabla\Phi(x)^\top(x-y)-\frac\rho2\|x-y\|^2$ for all $x,y\in\mathcal X\cap\mathcal D$ .

Let $f$ be convex on $\mathcal X$ with a minimizer $x^*\in\mathcal X$ . A linear functional $g$ is a subgradient of $f$ at $x$ if $f(x)-f(y)\le g^\top(x-y)$ for all $y\in\mathcal X$ , and $f$ is $L$ -Lipschitz if the subgradients satisfy $\|g\|_*\le L$ .

Mirror descent with step $\eta$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, for $t\ge1$ , picks $g_t\in\partial f(x_t)$ and

\nabla\Phi(y_{t+1})=\nabla\Phi(x_t)-\eta g_t,\quad y_{t+1}\in\mathcal D,\qquad x_{t+1}=\Pi^\Phi_{\mathcal X}(y_{t+1}).\tag{4.2–4.3}

Dual averaging instead sets $x_t\in\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}\eta\sum_{s=1}^{t-1}g_s^\top x+\Phi(x)$ (4.6). Let $R^2$ bound $\Phi(x)-\Phi(x_1)$ over $\mathcal X\cap\mathcal D$ .

Formalization targets

Goal: Theorem 4.2

With $\eta=\frac RL\sqrt{\frac{2\rho}{t}}$ , every run of mirror descent satisfies

f\Big(\frac1t\sum_{s=1}^t x_s\Big)-f(x^*)\le RL\sqrt{\frac{2}{\rho t}}.

Milestones

The three-point identity (4.1): $(\nabla f(x)-\nabla f(y))^\top(x-z)=D_f(x,y)+D_f(z,x)-D_f(z,y)$ .
Lemma 4.1: for $x\in\mathcal X\cap\mathcal D$ and $y\in\mathcal D$ , $D_\Phi(x,\Pi^\Phi_{\mathcal X}(y))+D_\Phi(\Pi^\Phi_{\mathcal X}(y),y)\le D_\Phi(x,y)$ , together with the first-order inequality that implies it.
The per-step inequality: $f(x_s)-f(x)\le\frac1\eta\big(D_\Phi(x,x_s)+D_\Phi(x_s,y_{s+1})-D_\Phi(x,x_{s+1})-D_\Phi(x_{s+1},y_{s+1})\big)$ .
The stability term: $D_\Phi(x_s,y_{s+1})-D_\Phi(x_{s+1},y_{s+1})\le(\eta L)^2/(2\rho)$ .
The summed bound: $\sum_{s=1}^t(f(x_s)-f(x))\le D_\Phi(x,x_1)/\eta+\eta L^2t/(2\rho)$ .

Companion: Theorem 4.3

With $\eta=\frac RL\sqrt{\frac{\rho}{2t}}$ , dual averaging satisfies $f\big(\frac1t\sum_{s=1}^tx_s\big)-f(x^*)\le2RL\sqrt{\frac2{\rho t}}$ , with the two displays (4.7) and (4.8) of its proof as supporting items.

Significance

Theorem 4.2 is the basic rate of non-Euclidean first-order optimization. With the Euclidean mirror map $\Phi=\frac12\|\cdot\|_2^2$ it recovers the projected subgradient rate of Chapter 3; with the negative entropy on the simplex, which is $1$ -strongly convex for $\ell_1$ by Pinsker's inequality and has $R^2=\log n$ , it gives $L_\infty\sqrt{2\log n/t}$ , so the dependence on the dimension becomes logarithmic. The same analysis, with $f$ replaced by a sequence of losses, is the regret bound of online mirror descent, and its per-step and stability inequalities are reused for stochastic mirror descent and mirror prox in later chapters of the book.

The results are classical and fully proved in the book. What this mission adds is a machine-checked version in a general finite-dimensional normed space, with gradients as linear functionals and the dual norm as the operator norm, for an arbitrary mirror map on an arbitrary open domain. On Prove2Me the three-point identity (4.1) is already posed, as Lemma 4.1 of the Beck–Teboulle formalization, and is reused here; a regret bound for online mirror descent with Legendre functions is proved in another library, but it is not this theorem and does not cover a domain $\mathcal D$ distinct from the whole space or a Bregman projection onto $\mathcal X\cap\mathcal D$ .

Difficulty

The algebra of the proof is short. The difficulty lies at the boundary of $\mathcal D$ . The minimizer $x^*$ may lie on $\partial\mathcal D$ , where $\Phi$ and $\nabla\Phi$ are not defined; this is the typical case for the entropy on the simplex, where $x^*$ is often a vertex. The per-step bound holds only for comparison points $x\in\mathcal X\cap\mathcal D$ , so the bound at $x^*$ has to be recovered from points of $\mathcal X\cap\mathcal D$ , where no regularity of $f$ beyond convexity on $\mathcal X$ is available. Lemma 4.1 needs the first-order optimality condition of the Bregman projection over the convex set $\mathcal X\cap\mathcal D$ , which is not closed. In the non-Euclidean setting the gradient step cannot be written in the primal space at all: the update (4.2) is an equation between linear functionals, and the norm and dual norm must be kept apart throughout.

Formalization scope

The space is a finite-dimensional real normed space E with an arbitrary norm; gradients and subgradients are elements of E →L[ℝ] ℝ, the dual norm is the operator norm, and $\nabla\Phi$ is an explicit map Φ' with HasFDerivAt Φ (Φ' x) x on $\mathcal D$ .
The mirror map carries all three properties (i)–(iii) of the book; the standing setting ( $\mathcal X$ compact convex, $\mathcal X\subseteq\overline{\mathcal D}$ , $\mathcal X\cap\mathcal D\neq\emptyset$ ) is a single predicate.
Runs are predicates over the first $t$ steps, quantified universally: any subgradient, any $y_{t+1}$ solving (4.2), any minimizer. A run whose next iterate were an arbitrary point of $\mathcal X\cap\mathcal D$ , rather than the Bregman projection, would make the theorem false; the projection is part of the run.
Sequences are indexed from $1$ ; $t\ge1$ , $\rho>0$ , $L>0$ , $R>0$ and $\eta>0$ are explicit, since the step and the bound divide by them.
$R^2$ is any upper bound of $\sup_{\mathcal X\cap\mathcal D}\Phi-\Phi(x_1)$ (the book's $R$ is the least one); when the supremum is infinite the hypotheses cannot be met, as on the page.
" $f$ is $L$ -Lipschitz" is assumed for the subgradients the run uses. Subgradients relative to $\mathcal X$ are unbounded at boundary points of $\mathcal X$ , so the literal "every subgradient at every point" would make the hypothesis unsatisfiable.
The definitions (Bregman divergence, mirror map, Bregman projection, the two runs) are reusable by the later chapters on mirror prox and stochastic mirror descent. Proofs of any milestone, and of the general facts they need (nonnegativity of Bregman divergences, first-order optimality over a convex set that is not closed), are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983 (book; no DOI).
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. doi:10.1016/S0167-6377(02)00231-6
Y. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120(1):221–259, 2009. doi:10.1007/s10107-007-0149-x

7 thms3 active usersReviewed

Missions

Bimatrix Equilibrium Points and Mathematical Programming: If Z Is Non-Degenerate and uᵀMu ≥ 0, uᵀMu = 0 ⇒ Mu + Mᵀu = 0 for All u ≥ 0, a Non-Empty Z Has an Equilibrium PointResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 7)

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

Companion results

Significance

Difficulty

Formalization scope

Selected references

Loss Networks 1: The Primal Problem Has a Unique Optimum x_r = ν_r ∏_j (1 − B_j)^{A_jr}; the Conditions on B Are Solvable, Uniquely if rank A = J, and Biject with Dual OptimaResearch Paper

Motivation

Setting

Formalization targets

Theorem 2.8: primal optimum, blocking solutions, and dual optima

Claims leading to the theorem

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Theorem 5

Milestones

Significance

Difficulty

Formalization scope

Selected references

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

Motivation

Setting

Formalization targets

Goal: Theorem 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Relation Between Integer and Noninteger Solutions to Linear Programs: Deep in the Optimal-Basis Cone, z₂(b) = z₁(b) + φ(b) and the Group Problem Gives an Integer OptimumResearch Paper

Motivation

Setting

Formalization targets

Goal: THEOREM 1 (p. 261)

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares 1: Markdown Is Optimal Once Time-to-Go Falls Below a Strictly Increasing Threshold x_nResearch Paper

Why the timing of a markdown matters

Prices, demand, and admissible switches

Formalization targets

What the result provides

Where the mathematics is difficult

Formalization scope

Selected references

The Complexity of Markov Decision Processes III: The Optimal Discounted Cost of a Deterministic Process Is the Least Discounted Cost of a SigmaResearch Paper

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Bargaining Problem: The Nash Product Maximizer Is the Unique Solution Satisfying Invariance, Symmetry, IIA and Pareto EfficiencyResearch Paper

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

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