Optimization

Minimum discrimination information under moment constraints

Given a reference probability distribution $R$ and a set $\mathcal E$ of probability distributions, the minimum discrimination information problem asks for the member of $\mathcal E$ closest to $R$ in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations $\int f_i\,dP = a_i$, and the classical answer is that the minimizer is an exponential family member, with density $c\exp\sum_i t_i f_i$ with respect to $R$.

That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the $f_i$.

Timeline:

• 1959: Kullback formulates the minimum discrimination information theorem: an element of $\mathcal E$ of exponential form is the minimizer (a sufficient condition).
• 1966: Kullback and Khairat (Ann. Math. Statist. 37, 1966) refine the sufficient condition.
• 1972: Čencov proves existence of exponential-form minimizers under general conditions (Statistical Decision Rules and Optimal Inference, Theorem 23.1).
• 1975: Csiszár proves Theorem 3.3 by the minimizing-sequence method of his Theorem 2.1; a first version of the paper assumed $T_R = E^k$, weakened to "$T_R$ open" after Čencov's work.

Setting

All distributions (PD's) live on one measurable space $(X,\mathcal X)$. The I-divergence of $P$ from $Q$ is

$$I(P\|Q)=\int \log p_Q\,dP\ \text{ if } P\ll Q,\qquad I(P\|Q)=+\infty\ \text{ otherwise},$$

where $p_Q$ is the density of $P$ with respect to $Q$; it takes values in $[0,\infty]$ and vanishes only for $P=Q$. The variation distance is $|P-Q|=\int|p_R-q_R|\,dR$ for any PD $R$ dominating both. If $\mathcal E$ is a convex set of PD's containing some $P$ with $I(P\|R)<\infty$, a $Q\in\mathcal E$ with

$$I(Q\|R)=\min_{P\in\mathcal E} I(P\|R)$$

is the I-projection of $R$ on $\mathcal E$.

Fix real-valued measurable functions $f_1,\dots,f_k$ on $X$. For $a=(a_1,\dots,a_k)\in E^k$ (Euclidean $k$-space) the moment set $\mathcal E(a)$ is the set of PD's $P$ with $\int f_i\,dP=a_i$, $i=1,\dots,k$. Further:

• $A_R$ is the set of $a\in E^k$ for which $\mathcal E(a)$ contains some $P$ with $I(P\|R)<\infty$;
• $T_R=\{t\in E^k:\ \exp\sum_i t_i f_i \text{ is } R\text{-integrable}\}$, (3.16);
• $F(a)=\inf_{P\in\mathcal E(a)} I(P\|R)$, (3.18), the optimal value as a function of the constraint levels.

Formalization targets

Goal: Theorem 3.3

If $T_R$ is open in $E^k$, then for every point $a$ of the interior of $A_R$ the I-projection $Q$ of $R$ on $\mathcal E(a)$ exists and

$$q_R(x)=c\exp\sum_{i=1}^k t_i f_i(x)\qquad R\text{-a.e.},$$

for some constant $c$ and some $t\in E^k$.

Milestones

1. (2.2), the parallelogram identity: $I(P_m\|R)+I(P_n\|R)=2I(\tfrac{P_m+P_n}2\|R)+I(P_m\|\tfrac{P_m+P_n}2)+I(P_n\|\tfrac{P_m+P_n}2)$.
2. (2.4): a minimizing sequence $P_n$ in a convex set converges in variation to a PD $Q\ll R$ (closedness of the set is not used).
3. Lemma 3.1: if $e^{tf}$ is $Q$-integrable for small $|t|$, then $I(P_n\|Q)\to0$ implies $\int f\,dP_n\to\int f\,dQ$.
4. (3.18): $A_R$ is convex and $F$ is finite and convex on $A_R$.
5. (3.19): at an interior point $a$ of $A_R$ there is $t$ with $F(b)\ge F(a)+\sum_i t_i(b_i-a_i)$ for all $b\in A_R$.
6. Remark, p. 158: $F$ is differentiable at interior points of $A_R$, and $\operatorname{grad}F(a)=t$, the parameter vector of the I-projection.

Significance

Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.

The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).

Difficulty

The obvious argument fails at the first step: the moment set $\mathcal E(a)$ is convex but not closed in variation when the $f_i$ are unbounded, since $\int f_i\,dP$ is not continuous in variation. A minimizing sequence therefore converges in variation to some $Q$ (as in Theorem 2.1), but nothing places $Q$ in $\mathcal E(a)$: mass can escape to where $|f_i|$ is large. Ruling this out needs quantitative control of $I(P_n\|Q)$, which in turn requires knowing the form of $Q$ before knowing $Q$ is feasible; the interplay with the convexity of $F$ and the openness of $T_R$ is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.

Formalization scope

• Probability distributions are Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions $\log 0=-\infty$, $\log\frac a0=+\infty$, $0\cdot(\pm\infty)=0$.
• The variation distance uses $P+Q$ as dominating measure (the page allows any dominating PD; the value is the same).
• The I-projection carries $I(Q\|R)<\infty$ explicitly: the page defines it only when $\mathcal E$ meets $\{P: I(P\|R)<\infty\}$.
• $\mathcal E(a)$ requires $P$-integrability of every $f_i$, so the constraint integrals are genuine. $E^k$ is Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. $k=0$ is allowed.
• $F$ is an infimum in $[0,\infty]$ (equal to $\infty$ outside $A_R$); statements use its real value only on $A_R$, where it is finite. (3.18) prints $I(P\|Q)$; the reference measure is $R$, as the definition of $A_R$ and the proof show. (3.16) prints $(t_1,\dots,t_n)$ for $(t_1,\dots,t_k)$.
• Densities are Radon–Nikodym derivatives and the form (3.2) is an $R$-almost-everywhere identity with no exceptional set of positive measure.
• Lemma 3.1 asserts that $f$ is $P_n$-integrable for large $n$ as well as the convergence, so that $\int f\,dP_n$ is not a default value.
• Trivializing readings are excluded: the goal asserts existence of the I-projection rather than assuming it, $T_R$ is an integrability set (not a set where a junk integral is finite), and the infimum is never a real sInf over a possibly empty set.

A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) $I(P\|R)-I(P\|Q)=\int\log q_R\,dP$), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.

Selected references

• I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probab. 3(1), 146–158, 1975. https://doi.org/10.1214/aop/1176996454
• S. Kullback, Information Theory and Statistics, Wiley, 1959.
• S. Kullback and M. A. Khairat, A note on minimum discrimination information, Ann. Math. Statist. 37, 279–280, 1966.
• E. T. Jaynes, Information theory and statistical mechanics, Phys. Rev. 106, 620–630, 1957. https://doi.org/10.1103/PhysRev.106.620
• N. N. Čencov, Statistical Decision Rules and Optimal Inference (Russian), Nauka, 1972; English translation, American Mathematical Society, 1982.
• I. N. Sanov, On the probability of large deviations of random variables (Russian), Mat. Sbornik 42, 11–44, 1957.

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

1. 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.
2. Lemma 2 (p. 4): $Z=\emptyset$ iff some $u\ge0$ has $M^{\mathsf T}u\le0$, $u^{\mathsf T}q>0$.
3. Theorem 2 (p. 4): if some $Z_s$ contains precisely one ray of a non-degenerate $Z$, the number of equilibrium points is odd.
4. 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.
5. Lemma 2 (p. 6): $Z^{**}$ has an equilibrium point.
6. 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$.
7. (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

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.

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.

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

1. 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}$.
2. 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.
3. 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).
4. 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

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

Motivation

Interior-point methods minimize a linear function $x\mapsto\langle c,x\rangle$ over a convex set $\mathcal K\subset\mathbb R^n$ by following the minimizers of $\langle c,x\rangle+\frac1t g(x)$ as $t\to\infty$, where $g$ is a self-concordant barrier for $\mathcal K$. Each Newton step of such a method shrinks $1/t$ by a factor $1-1/\sqrt\nu$, where $\nu$ is the self-concordance parameter of $g$, so $\nu$ controls the iteration count of every interior-point method built on $g$ (Nesterov and Nemirovski 1994; Nesterov 2004).

Timeline:

• 1994. Nesterov and Nemirovski construct the universal barrier for any convex body and show it is a $\nu$-self-concordant barrier with $\nu\le Cn$ for a universal constant $C$. They also show that $\nu\ge n$ is necessary for some bodies (the simplex, the cube).
• 2014–2015. Hildebrand (Math. Oper. Res. 2014) and Fox (Ann. Mat. Pura Appl. 2015) show that the canonical barrier of a convex cone has parameter equal to the dimension, which gives parameter $n+1$ for convex bodies.
• 2015. Bubeck and Eldan (arXiv:1412.1587, COLT 2015) show that the Fenchel dual of the log-Laplace transform of the uniform measure on $\mathcal K$, which they call the entropic barrier, is a $(1+o(1))n$-self-concordant barrier, with an explicit $o(1)$ term.

Beyond optimization, the entropic barrier is the mirror map that pairs naturally with the exponential-family sampling scheme in bandit linear optimization, which the paper discusses in its §3.1.

Setting

Let $\mathcal K\subset\mathbb R^n$ be a convex body: compact, convex, with non-empty interior $\operatorname{int}(\mathcal K)$. The log-Laplace transform of $\mathcal K$ is

$$f(\theta)=\log\left(\int_{x\in\mathcal K}\exp(\langle\theta,x\rangle)\,dx\right),\qquad\theta\in\mathbb R^n,$$

and the entropic barrier is its Fenchel dual

$$f^*(x)=\sup_{\theta\in\mathbb R^n}\ \langle\theta,x\rangle-f(\theta),\qquad x\in\operatorname{int}(\mathcal K).$$

For a function $g:\operatorname{int}(\mathcal K)\to\mathbb R$ write $\nabla g(x)[h]$, $\nabla^2g(x)[h,h]$, $\nabla^3g(x)[h,h,h]$ for its directional derivatives. Following Definition 1 of the paper:

1. $g$ is a barrier for $\mathcal K$ if $g(x)\to+\infty$ as $x\to\partial\mathcal K$;
2. a $C^3$ convex $g$ is self-concordant if $\nabla^3g(x)[h,h,h]\le2(\nabla^2g(x)[h,h])^{3/2}$ for all $x\in\operatorname{int}(\mathcal K)$, $h\in\mathbb R^n$;
3. it is $\nu$-self-concordant if moreover $\nabla g(x)[h]\le\sqrt{\nu\cdot\nabla^2g(x)[h,h]}$ for all such $x,h$.

The proof works with the canonical exponential family $p_\theta$, the probability measure with density $\exp(\langle\theta,x\rangle-f(\theta))\mathbb 1\{x\in\mathcal K\}$, its mean $x(\theta)$, covariance $\Sigma(\theta)$ and third central moment $T(\theta)$; with $Y=\langle\theta/\|\theta\|,X\rangle$ for $X\sim p_\theta$ and its density $\rho$; and with the section marginal $\lambda(y)=\mathrm{Vol}_{n-1}(\mathcal K\cap\{y\theta/\|\theta\|+\theta^\perp\})/\mathrm{Vol}(\mathcal K)$.

Formalization targets

Goal: Theorem 1

For every $n\ge80$ and every convex body $\mathcal K\subset\mathbb R^n$, $f^*$ is a $\nu$-self-concordant barrier for $\mathcal K$ with

$$\nu=(1+\varepsilon_n)\,n,\qquad\varepsilon_n=100\sqrt{\frac{\log n}{n}}.$$

Milestones, in attack order

1. Lemma 1 (p. 5): strict convexity of $f$, $f^*$; $\nabla f^*:\operatorname{int}(\mathcal K)\to\mathbb R^n$ is a bijection; $\nabla^2f=\Sigma$, $\nabla^3f=T$ (eqs. (4)–(5)); $\nabla^2f^*(x)=\Sigma(\theta(x))^{-1}$ (eq. (6)).
2. $f^*$ is a barrier (§4, p. 6).
3. Lemma 2 (p. 7): $\mathbb EX^3\le2(\mathbb EX^2)^{3/2}$ for a real centered log-concave $X$; its consequence $\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^3\le2(\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^2)^{3/2}$; $f^*$ is self-concordant (§4, pp. 6–7).
4. Reduction of (3) (p. 7): $f^*$ satisfies (3) with parameter $\nu$ iff $\langle\Sigma(\theta)\theta,\theta\rangle\le\nu$ for all $\theta$.
5. $\lambda$ is $n$-concave on its support (p. 9) and Lemma 5 (p. 9): $\varphi$ is $n$-concave iff $(\log\varphi)''\le-\frac1n((\log\varphi)')^2$.
6. Lemma 3 (p. 8): $\rho(y+y_0)=\rho(y_0)\zeta(y)e^{-y^2/(2\sigma^2)}$ on $[-M,M]$, with $\zeta\in[0,1]$ unimodal, $M=\sqrt{7n\log n}/\|\theta\|$, $\sigma^2=\frac{n}{\|\theta\|^2}\frac{1}{1-\sqrt{7\log(n)/n}}$; and its consequence (9): $\mathbb E(|Y-y_0|^2\mid|Y-y_0|\le M)\le\sigma^2$.
7. Lemma 4 (p. 8): $(1-2c(\varepsilon)\varepsilon\log^2(1/\varepsilon))\mathrm{Var}(X)\le\int_{x_1}^{x_2}(x-x_0)^2\lambda(x)dx\le\mathbb E(|X-x_0|^2\mid X\in[x_1,x_2])$ for log-concave $X$.
8. (7) (p. 7): $\mathrm{Var}(Y)\le\frac{n}{\|\theta\|^2}(1+\varepsilon_n)$.

Significance

The result. Theorem 1 gives, for every convex body, an explicit barrier whose parameter is $n$ up to a second-order term, against the $Cn$ of the universal barrier, and it is optimal up to that term because $\nu\ge n$ is necessary for some bodies. The barrier is defined by a single formula, its derivatives are moments of an explicit probability measure, and its parameter bound reduces to a variance bound for one-dimensional log-concave marginals. Lemmas 2 and 4 are self-contained facts about log-concave laws on $\mathbb R$ (a sharp third-moment bound and a variance-localization bound) that are usable outside this paper.

Formalizing it. The theorem is proved in the paper; nothing here is formalized elsewhere. The platform has a definition of self-concordance (reused here) and results for given self-concordant functions, but no universal or entropic barrier, no exponential family over a convex body, and no moment bounds for log-concave laws. A complete development produces machine-checked versions of the duality facts of Lemma 1, of the two log-concave lemmas, and of the Brunn–Minkowski consequence for section volumes. Two steps of the paper are sketched rather than proved in full: the end of the proof of Lemma 2 ("We omit further details of this proof", p. 12) and, in Lemma 4, a normalization step that cites a lemma stated for isotropic densities. A formal proof either fills or replaces them.

Difficulty

Self-concordance of $f^*$ reduces to self-concordance of $f$ by a general duality fact, and that reduces to Lemma 2; the difficulty there is the sharp constant $2$, since generic moment comparisons for log-concave laws give a worse constant. The parameter bound is the hard part. The obvious bound $\langle\Sigma(\theta)\theta,\theta\rangle\le Cn$ follows from standard concentration for log-concave measures, but any argument that loses a constant factor proves only the 1994 result. The $1+o(1)$ requires the one-dimensional marginal of the tilted measure to be compared with a Gaussian of variance $n/\|\theta\|^2$ to within a factor $1+O(\sqrt{\log n/n})$, using the fact that $\lambda$ is $n$-concave and not merely log-concave. The paper does this pointwise near the mode (Lemma 3) and controls the tails separately (Lemma 4). The pointwise argument assumes $\rho$ smooth, which holds for smooth bodies, and an approximation argument passes to general convex bodies.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so $n$ is the dimension, not a separate parameter. A convex body is compact, convex, with non-empty interior; a lower-dimensional set is excluded, which rules out a formalization in which the barrier and self-concordance clauses hold vacuously.

• $f^*$ is a real supremum. On $\operatorname{int}(\mathcal K)$ it is the true supremum; elsewhere Lean returns a junk value that no statement reads. The barrier property is a limit within $\operatorname{int}(\mathcal K)$ at every frontier point.

• Self-concordance (2) is the published ConvexOptimization.IsSelfConcordantOn on interior K, stated by line restrictions with an absolute value. It is equivalent to (2), because $h\mapsto-h$ flips the sign of the third derivative.

• The goal states the parameter as the explicit number $\nu=(1+100\sqrt{\log(n)/n})\,n$. The page says $\varepsilon_n\le100\sqrt{\log(n)/n}$, and (3) is monotone in $\nu$, so this is the same claim. An existential $\nu$ is not used.

• Corrections and implicit hypotheses:

  • Lemma 4 is stated for $0<\varepsilon<1$. The page says $\varepsilon>0$, but the statement is false for $\varepsilon\ge1$ and the paper applies it only with $\varepsilon<1$.
  • Lemma 5 assumes $\varphi>0$, which is implicit in $\zeta=\log\varphi$.
  • The reduction of (3) assumes $\nu\ge0$.
  • Lemma 3 and (9) carry the smoothness of $\rho$ (the paper's own without-loss-of-generality step on p. 7) as a hypothesis, and the theorem's range $n\ge80$.

• Section volumes use Mathlib's unnormalized $(n-1)$-dimensional Hausdorff measure. The normalization constant cancels in $\rho$ and does not affect $n$-concavity. $\lambda$ and $\rho$ are fixed pointwise functions, because Lemma 3 evaluates $\rho$ at a maximizer.

• Log-concavity on $\mathbb R$ is the published ConvexOptimization.LogConcaveOn on the whole line.

• Needed infrastructure that is reusable beyond this mission:

  • differentiation under the integral sign for exponential families on compact sets;
  • Fenchel duality for smooth strictly convex functions;
  • Brunn's concavity theorem for sections of convex bodies;
  • moment and tail bounds for log-concave densities on $\mathbb R$.

  Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

• S. Bubeck, R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, COLT 2015; arXiv:1412.1587v3. https://arxiv.org/abs/1412.1587
• Y. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• R. Hildebrand, Canonical barriers on convex cones, Mathematics of Operations Research 39:841–850, 2014.
• D. Fox, A Schwarz lemma for Kähler affine metrics and the canonical potential of a proper convex cone, Annali di Matematica Pura ed Applicata 194:1–42, 2015.
• B. Klartag, On convex perturbations with a bounded isotropic constant, Geometric and Functional Analysis 16(6):1274–1290, 2006.
• C. Borell, Convex set functions in d-space, Periodica Mathematica Hungarica 6(2):111–136, 1975.