Optimization

Motivation

Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of $m$ ads out of $d$, a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of $d$ arms) and is a standard model in online advertising, routing and ranking.

Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret $O(\sqrt{mdn})$ with no logarithmic factor. For $m=1$ this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).

Setting

Vectors live in $\mathbb R^d$. The arm set is a nonempty $\mathcal C\subseteq\{0,1\}^d$ with $\|v\|_1=m$ for every $v\in\mathcal C$, and $\mathcal K=\mathrm{Conv}(\mathcal C)$. An oblivious adversary fixes loss vectors $\ell_1,\dots,\ell_n\in[0,1]^d$. In round $t$ the learner plays a random arm $v_t\in\mathcal C$, pays $\ell_t^\top v_t$, and observes $(\ell_t(1)v_t(1),\dots,\ell_t(d)v_t(d))$. The pseudo-regret is

$$\bar R_n=\mathbb E\sum_{t=1}^n\ell_t^\top v_t-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t^\top x .$$

A Legendre function on $\bar D$, for a nonempty open convex $D$, is a continuous $F:\bar D\to\mathbb R$ that is strictly convex and $C^1$ on $D$ and whose gradient norm tends to $+\infty$ at $\bar D\setminus D$. Its Bregman divergence is $D_F(x,y)=F(x)-F(y)-(x-y)^\top\nabla F(y)$, and its Legendre–Fenchel transform is $F^*(u)=\sup_{x\in\bar D}(x^\top u-F(x))$.

Online Mirror Descent with learning rate $\eta>0$ and vectors $g_t$ starts at $x_1\in\arg\min_{\mathcal K}F$. It then sets $\nabla F(w_{t+1})=\nabla F(x_t)-\eta g_t$ and $x_{t+1}=\arg\min_{y\in\mathcal K}D_F(y,w_{t+1})$. OSMD uses a random estimate $g_t=\tilde\ell_t$ of the loss. In the semi-bandit case it plays $v_t$ with $\mathbb E[v_t\mid x_t]=x_t$ and uses

$$\tilde\ell_t(i)=\frac{\ell_t(i)\,v_t(i)}{x_t(i)}. \tag{5.5}$$

A $0$-potential is a convex, $C^1$, increasing $\psi:(-\infty,a)\to(0,\infty)$ with $\psi(-\infty)=0$, $\psi(a^-)=+\infty$ and $\int_0^1|\psi^{-1}|<\infty$. It defines the Legendre function $F_\psi(x)=\sum_i\int_0^{x_i}\psi^{-1}(s)\,ds$ on $[0,\infty)^d$. With $\psi=\exp$ this is the negative entropy.

Formalization targets

Goal: Theorem 5.7 (p. 80)

For every $0$-potential $\psi$ and non-negative unbiased estimates,

$$\bar R_n\le\frac{\sup_{\mathcal K}F_\psi-F_\psi(x_1)}{\eta}+\frac\eta2\sum_{t=1}^n\sum_{i=1}^d\mathbb E\left[\frac{\tilde\ell_t(i)^2}{(\psi^{-1})'(x_t(i))}\right].$$

For $\psi(x)=(-x)^{-q}$ with $q>1$, the estimate (5.5) and $\eta=\sqrt{\tfrac{2}{q-1}\,m^{1-2/q}/(n\,d^{1-2/q})}$,

$$\bar R_n\le q\sqrt{\tfrac{2}{q-1}\,mdn},\qquad\text{and }\ \bar R_n\le2\sqrt{2mdn}\ \text{ at }q=2.$$

Milestones

1. Lemma 5.1: $F^{**}=F$, $\nabla F^*=(\nabla F)^{-1}$ on $D^*$, and $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$.
2. Lemma 5.2: existence, uniqueness and the Pythagorean inequality of Bregman projections.
3. Theorem 5.3: $\sum_t\ell_t(x_t)-\sum_t\ell_t(x)\le\frac{F(x)-F(x_1)}\eta+\frac1\eta\sum_tD_{F^*}(\nabla F(x_t)-\eta\nabla\ell_t(x_t),\nabla F(x_t))$.
4. Theorem 5.5, linear losses, and its corrected general form.
5. Lemma 5.3: $F_\psi$ is Legendre and $D_{F_\psi^*}(u,v)\le\frac12\sum_i\psi'(v_i)(u_i-v_i)^2$ for $u\le v$.
6. Theorem 5.6: with the negative entropy, $\bar R_n\le\sqrt{2mdn\ln(d/m)}$.

Significance

Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the $\sqrt{\ln(d/m)}$ factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.

All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside $D$ and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant $q\sqrt{2mdn/(q-1)}$, with two of the printed statements corrected (below).

Difficulty

The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of $D$. Another is the differentiability of $F^*$ on the open dual space and the identity $\nabla F^*=(\nabla F)^{-1}$. A third is the closed form of $F_\psi^*$ for a potential defined through an improper integral of $\psi^{-1}$.

The probabilistic step is not a martingale argument. Only conditioning on the current iterate $x_t$ is available. The estimate (5.5) divides by $x_t(i)$, so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, $\sum_ix_1(i)^{1-1/q}\le m^{(q-1)/q}d^{1/q}$, and the matching bound $\sum_ix_t(i)^{1/q}\le m^{1/q}d^{1-1/q}$.

Formalization scope

Vectors are Fin d → ℝ. The arm set is a Set of $0/1$ vectors with coordinate sum $m$, and $\mathcal K$ is convexHull ℝ C. Rounds are $t=1,\dots,n$, sums run over Finset.Icc 1 n, and index $0$ is unused. A randomized run is a family of measurable processes $x_t, v_t, \tilde\ell_t, w_t$ on a probability space, with the deterministic OMD recursion holding on every sample path. $\mathbb E[\cdot\mid x_t]$ is the coordinatewise conditional expectation given $\sigma(x_t)$, which is exactly what the book's proofs use. Losses are oblivious, so $\bar R_n\le B$ is stated as "for every $x\in\mathcal K$, $\mathbb E\sum_t\ell_t^\top v_t-\sum_t\ell_t^\top x\le B$". $F^*$ is valued in EReal, and $D_{F^*}$ is evaluated only on the open dual space, where $F^*$ is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then $+\infty$ and trivial, while Lean's integral would be $0$.

Corrections and instantiations, each labelled in the item's Formalization Note:

• Theorem 5.7, corrected misprint. The book prints $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{d^{1-2/q}}}$. The proof (p. 81) gives the stated bound only for $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{n\,d^{1-2/q}}}$, which is stated. At $q=2$ this is $\eta=\sqrt{2/n}$.
• Theorem 5.5, corrected misprint. In the first bound the book prints $\mathbb E[\|x_t-\tilde x_t\|\,\|\tilde g_t\|_*]$. That statement fails for $\ell_t(x)=x^2$ on $[-1,1]$ with $F=x^2/2$ and $\tilde x_t=\pm1$. The version stated uses $\|\nabla\ell_t(\tilde x_t)\|_*$, as the proof's first inequality does. The linear-loss bound is stated as printed.
• Lemma 5.2. "For all $z\in K\cap D$" is read as "for the projection $z$", which lies in $K\cap D$.
• Hypotheses made explicit: $q>1$; non-negativity of the estimates in Theorem 5.6 (used in its proof); unbiasedness $\mathbb E[\tilde\ell_t\mid x_t]=\ell_t$ in the general parts of Theorems 5.6 and 5.7; $\mathcal K\cap(0,\infty)^d\ne\emptyset$ (OMD's requirement $K\cap D\ne\emptyset$); a subgradient selection as an explicit input.
• Theorem 5.6's particular bound uses the book's $\eta=\sqrt{\frac{2m}{nd}\ln\frac dm}$ as printed. There are no O(·) constants in the chapter's statements.

A trivializing formalization would let $\eta$, $x_t$ or the estimate be junk values: an OSMD step at $\eta=0$, a Lean division $x/0=0$, or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in $\mathcal K$.

Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the $\omega$-potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012; arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921
• J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in online combinatorial optimization, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0598

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$, which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

• 1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
• 1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$.
• 1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
• 1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
• Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$, where $1\le k\le\min(m,n)$, keeps $k$ rows and $k$ columns of $A$. The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$. So $\Delta(0)=0$, and $\Delta(A)\ge 1$ whenever $A\ne 0$. Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$.

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$. An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$. For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$. A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$, $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$.

If $ay\le\beta$ for all $y\in P$, with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$. The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$. Then $P_I\subseteq P^{(i)}$ for all $i$. The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$. The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$.

Formalization targets

Goal: Theorem 10 (p. 260)

$$\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.$$

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$.

Milestones, in attack order

1. Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$-distance $n\Delta(A)$, and every IP optimum has an LP optimum within the same distance.
2. Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$.
3. Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$. This result is off the goal's path.
4. Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$-distance $n\Delta(A)$.
5. Theorem 7 (p. 257). A single integral matrix $M$, with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
6. Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$.
7. Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$.

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$. They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$: polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$. That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$. Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$, and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

• Rationality. Everything is over $\mathbb{Q}$, following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$, and a polyhedron is a finite system of rational inequalities.
• $\Delta(A)$. Only nonempty submatrices count, so $\Delta(0)=0$.
• Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
• Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$, using all integral $a$ and rational $\beta$. The rank is valued in $\mathbb{N}\cup\{\infty\}$, with $\infty$ if no iterate equals $P_I$. A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$, as printed.
• Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$. For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
• Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$.

A complete development needs the following:

• cone generation with Cramer bounds and Carathéodory's theorem;
• LP duality and Farkas' lemma over $\mathbb{Q}$;
• the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
• Schrijver's face lemma and unimodular invariance;
• a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

• W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
• V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
• A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
• W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
• F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322

Motivation

The ground-state energy of a mixed $p$-spin spin glass, $\mathsf{OPT}_N=\max_{\sigma\in\{\pm1\}^N}H_N(\sigma)/N$, converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).

The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier $\tfrac12\xi''\gamma$. Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional $\mathsf P(\gamma)$. This mission formalizes that duality and the verification argument behind it (Section 7).

Setting

Mixture. Real coefficients $(c_k)_{k\ge2}$ define the mixture $\xi(t)=\sum_{k\ge2}c_k^2t^k$, with the standing assumption $\xi(1+\varepsilon)<\infty$ for some $\varepsilon>0$. Its derivatives $\xi'$, $\xi''$ are nonnegative and nondecreasing on $[0,1]$.

Order parameters. $\mathsf{SF}_+$ is the set of nonnegative step functions

$$\gamma=\sum_{i=1}^m\gamma_i\,\mathbb I_{[t_{i-1},t_i)},\qquad 0=t_0<t_1<\dots<t_m=1,\ \gamma_i\ge0 .$$

Put $\nu(t)=\int_t^1\xi''(s)\gamma(s)\,ds$.

Parisi PDE and functional. $\Phi_\gamma:[0,1]\times\mathbb R\to\mathbb R$ solves

$$\partial_t\Phi_\gamma+\tfrac12\xi''(t)\big(\partial_x^2\Phi_\gamma+\gamma(t)(\partial_x\Phi_\gamma)^2\big)=0,\qquad\Phi_\gamma(1,x)=|x| .$$

For $\gamma\in\mathsf{SF}_+$ it is given explicitly by the Cole–Hopf recursion: with $r(t)=\xi'(1)-\xi'(t)$ and $G\sim\mathsf N(0,1)$, for $t\in[t_{i-1},t_i)$,

$$\Phi_\gamma(t,x)=\frac1{\gamma_i}\log\mathbb E\exp\big\{\gamma_i\Phi_\gamma(t_i,x+\sqrt{r(t)-r(t_i)}\,G)\big\}.$$

The Parisi functional is $\mathsf P(\gamma)=\Phi_\gamma(0,0)-\tfrac12\int_0^1t\,\xi''(t)\gamma(t)\,dt$.

Control problem. Let $B$ be a standard Brownian motion. A control $u\in D[t,1]$ is a process on $[t,1]$, progressively measurable for the filtration of $(B_r)_{r\in[t,1]}$, with $\mathbb E\int_t^1\xi''(s)u_s^2\,ds<\infty$. The value is

$$\mathcal J_\gamma(t,z)=\sup_{u\in D[t,1]}\mathbb E\Big[\int_t^1\xi''(s)u_s\,ds+\frac12\int_t^1\nu(s)\big(\xi''(s)u_s^2-1\big)ds\Big]\quad\text{s.t.}\quad z+\int_t^1\sqrt{\xi''(s)}\,u_s\,dB_s\in(-1,1)\ \text{a.s.}$$

Candidate value function. With $\Phi^*_\gamma(t,z)=\inf_x\{\Phi_\gamma(t,x)-xz\}$,

$$V(t,z)=\Phi^*_\gamma(t,z)-\tfrac12\nu(t)z^2-\tfrac12\int_t^1\nu(s)\,ds .$$

Formalization targets

Goal: Proposition 4.1

$$\mathcal J_\gamma(0,0)=\mathsf P(\gamma)\qquad\text{for every }\gamma\in\mathsf{SF}_+ .$$

Milestones

1. Lemma 7.2 (a)–(e): $\Phi_\gamma(t,\cdot)$ is smooth for $t<1$, with derivatives jointly continuous on $[0,1)\times\mathbb R$ and $C^1$ in time where $\gamma$ is constant. The range of $\partial_x\Phi_\gamma(t,\cdot)$ is $(-1,1)$, it is strictly increasing, and $0<\partial_x^2\Phi_\gamma(t',x)\le C(t,\gamma)$ for $t'\le t$.
2. Envelope identities (proof of Lemma 7.3): $\partial_z\Phi^*_\gamma(t,z)=-x^*_t(z)$ and $\partial_z^2\Phi^*_\gamma(t,z)=-1/\partial_x^2\Phi_\gamma(t,x^*_t(z))$, where $x^*_t(z)$ is the unique root of $\partial_x\Phi_\gamma(t,x)=z$.
3. Lemma 7.3: $V$ solves the HJB equation

$$\partial_tV+\xi''(t)\sup_{\lambda\in\mathbb R}\Big\{\lambda+\frac{\lambda^2}{2}\big(\nu(t)+\partial_z^2V\big)\Big\}-\frac12\nu(t)=0,\qquad V(1,z)=0 .$$

4. Evaluation at the origin: $V(0,0)=\mathsf P(\gamma)$.
5. Proposition 7.1: $\mathcal J_\gamma(t,z)=V(t,z)$ for all $(t,z)\in[0,1]\times(-1,1)$.

Proposition 7.1 at $(0,0)$ together with milestone 4 gives the goal.

Significance

The result. By integration by parts (Eq. (4.4) of the paper), $\mathcal J_\gamma(0,0)$ bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into $\inf_{\gamma\in\mathsf{SF}_+}\mathsf P(\gamma)$, which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint ($M_1\in(-1,1)$), Itô's formula for a $C^{1,2}$ function that is only piecewise $C^1$ in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.

Difficulty

The value function $\mathcal J_\gamma$ is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.

First, the guess $V$ is a Legendre transform. Its regularity, and the sign $\nu+\partial_z^2V<0$ that makes the HJB supremum finite, rest on strict convexity and bounded curvature of $\Phi_\gamma(t,\cdot)$ (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with $\gamma_i=0$.

Second, the verification argument applies Itô's formula to $V(s,M^u_s)$, where $M^u$ is a martingale confined to $(-1,1)$ and $V$ is only $C^1$ in time between the jumps of $\gamma$. The boundary $\theta\to1$ needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.

Formalization scope

• Mixture. $\xi$ is a coefficient sequence $c:\mathbb N\to\mathbb R$ with $c_0=c_1=0$ imposed. $\xi'$ and $\xi''$ are explicit termwise series.
• Step functions. $\mathsf{SF}_+$ is represented by its data (breakpoints and values). $\gamma$ is extended by $0$ outside $[0,1)$; its value at $t=1$ never matters.
• Cole–Hopf. $\Phi_\gamma$ is defined by the recursion. When $\gamma_i=0$, the recursion uses its limit, the heat semigroup, instead of dividing by zero. Expectations over $G$ are integrals against gaussianReal 0 1.
• Derivatives. Space derivatives are deriv/iteratedDeriv. Time derivatives are right derivatives, because $\gamma$ jumps.
• Legendre transform. $\Phi^*_\gamma$ is a real infimum, used only for $|z|<1$, where it is bounded below.
• Brownian motion and filtration. $B$ is a Mathlib IsBrownianReal process on $\mathbb R_{\ge0}$, with each $B_r$ measurable. The filtration is $\mathcal F^t_s=\sigma(B_r:t\le r\le s)$.
• Stochastic integral. It is the $L^2$ Itô integral of the published definition Peng1990.SMP.IsItoIntegral (horizon $1$), whose integrability class is exactly $\mathbb E\int\xi''u^2<\infty$.
• Supremum. $\mathcal J_\gamma(t,z)=v$ is stated as "$v$ is the least upper bound of the objective values of admissible controls" (IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.
• Disclosed hypothesis. Lemma 7.2, the envelope identities and Lemma 7.3 assume that $\xi$ is not identically zero (some $c_k\neq0$). For $\xi\equiv0$ one has $\Phi_\gamma(t,x)=|x|$ for all $t$, and these statements fail. Proposition 7.1, the evaluation at the origin and the goal need no such hypothesis.
• Lemma 7.3. The statement includes the inequality $\nu+\partial_z^2V<0$, which the page proves. This rules out reading the HJB supremum as a default value.

The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.

Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for $C^{1,2}$ functions.

Selected references

• A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
• A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144, 2016. https://arxiv.org/abs/1502.04398
• N. Touzi, Optimal Stochastic Control, Stochastic Target Problems, and Backward SDE, Fields Institute Monographs 29, Springer, 2012 (cited as [Tou12] in the paper; the verification argument of Section 7 follows its Theorem 4.1).

Motivation

The mixed $p$-spin model is a random polynomial on the hypercube $\{-1,+1\}^N$: a centered Gaussian process $H_N(\boldsymbol\sigma)$ with covariance $\mathbb E\{H_N(\boldsymbol\sigma)H_N(\boldsymbol\sigma')\} = N\xi(\langle\boldsymbol\sigma,\boldsymbol\sigma'\rangle/N)$. Its maximum $\mathrm{OPT}_N = \max_{\boldsymbol\sigma} H_N(\boldsymbol\sigma)/N$ is a canonical random optimization problem; for $\xi(t) = c_2^2t^2$ it is the ground state of the Sherrington–Kirkpatrick model. Auffinger and Chen (AC17) proved that $\mathrm{OPT}_N$ converges almost surely to the infimum of the zero-temperature Parisi functional $\mathsf P$ over a space $\mathscr U$ of non-decreasing order parameters.

El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) characterize what a class of message-passing algorithms achieves on this problem. The answer is the infimum of the same functional over a larger space $\mathscr L$ of order parameters that need not be monotone. Whether these algorithms reach the true optimum is therefore the question whether $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$. The paper proves this equality under the no-overlap gap assumption, that the Parisi minimizer over $\mathscr U$ can be taken strictly increasing (Assumption 2, p. 8). This is believed to hold for the Sherrington–Kirkpatrick model and to fail for pure $p$-spin models with $p \ge 3$. This mission formalizes that equality, stated as a property of the minimizer.

Timeline. Parisi's formula (1979) was proved by Talagrand (2006) and Panchenko (2013). Auffinger and Chen (2017) gave its zero-temperature form (1.7). Jagannath and Tobasco (JT16) gave a PDE and variational treatment of the Parisi functional at positive temperature, including its convexity. Montanari (Mon19) gave a message-passing algorithm for the Sherrington–Kirkpatrick model under no overlap gap. El Alaoui, Montanari and Sellke (2020) extended it to mixed $p$-spin models and introduced the extended principle over $\mathscr L$.

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$, with derivatives $\xi'$ and $\xi''$ given by the termwise series. Order parameters are functions $\gamma : [0,1) \to \mathbb R_{\ge0}$, in one of two spaces:

$$\mathscr U = \Big\{\gamma \text{ non-decreasing},\ \int_0^1\gamma(t)\,dt < \infty\Big\},\qquad \mathscr L = \Big\{\|\xi''\gamma\|_{TV[0,t]} < \infty\ \forall t<1,\ \int_0^1\xi''(t)\gamma(t)\,dt < \infty\Big\}.$$

Here $\|\cdot\|_{TV[0,t]}$ is total variation on $[0,t]$, and $\mathscr U \subseteq \mathscr L$.

For a step function $\gamma = \sum_i \gamma_i \mathbb I_{[t_{i-1},t_i)}$ with $\gamma_i \ge 0$ (the space $\mathrm{SF}_+$), the Parisi PDE

$$\partial_t\Phi + \tfrac12\xi''(t)\big(\partial_x^2\Phi + \gamma(t)(\partial_x\Phi)^2\big) = 0,\qquad \Phi(1,x) = |x|,$$

is solved explicitly by the Cole–Hopf recursion (7.3). It is a Gaussian log-moment-generating step on each piece, and a heat-semigroup step where $\gamma_i = 0$. For general $\gamma \in \mathscr L$, $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n \to \gamma$ in the weighted norm $\int_0^1\xi''|\gamma_n - \gamma|$. The Parisi functional is

$$\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .$$

The process $X$ is the strong solution of $dX_t = \xi''(t)\gamma(t)\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$, $X_0 = 0$ (Eq. (6.3)), driven by a standard Brownian motion $B$.

Formalization targets

Goal: the monotone minimizer is a minimizer over $\mathscr L$ (Section 6.3, p. 34)

If $\gamma_* \in \mathscr U$ is strictly increasing on $[0,1)$ and $\mathsf P(\gamma_*) \le \mathsf P(\gamma)$ for every $\gamma \in \mathscr U$, then

$$\mathsf P(\gamma_*) \le \mathsf P(\gamma)\qquad\text{for every }\gamma \in \mathscr L .$$

Since $\mathscr U \subseteq \mathscr L$, this is the paper's main result 2 (p. 4), $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ under no overlap gap.

Milestones

1. Lemma 6.7 (p. 27): for $\gamma\in\mathscr L$, $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$.
2. Proposition 6.8 (p. 27): the right derivative of $s\mapsto\mathsf P(\gamma+s\delta)$ at $0$ is $\frac12\int_0^1\xi''(t)\delta(t)\big(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t\big)\,dt$, for admissible directions $\delta$ that vanish near $t = 1$.
3. Lemma 6.15 (p. 33): under no overlap gap, $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\} = t$ for every $t\in[0,1)$.
4. Convexity (Section 6.3, p. 34): $\mathsf P$ is convex on $\mathscr L$.

Significance

The result. The goal identifies the value reached by the paper's message-passing algorithm with the ground-state energy whenever the Parisi minimizer is strictly increasing. Combined with the paper's algorithmic theorem, it yields a $(1-\varepsilon)$-approximation of $\mathrm{OPT}_N$ in time linear in the input size, for the Sherrington–Kirkpatrick model and any other mixture with no overlap gap (Corollary 2.2). It also gives a structural fact about the variational problem: when the minimizer is strictly increasing, the monotonicity constraint in $\mathscr U$ is not binding.

Formalizing it. The result is proved in the paper, but the proof leans on an external citation ([JT16, Theorem 20]) for convexity of $\mathsf P$ on $\mathscr L$. It also applies the first-variation formula in a direction that does not meet that formula's stated hypotheses. A machine-checked development closes both gaps. No part of this theory (the Parisi PDE, its Cole–Hopf solution, or the extended functional) has been formalized before, to our knowledge.

Difficulty

The obvious argument is: convexity plus stationarity gives a global minimum. Both inputs are hard. Stationarity (Lemma 6.15) needs the first variation of $\mathsf P$ in directions that keep $\gamma_*+s\delta$ monotone. That variation is a derivative of the solution of a nonlinear PDE with respect to its coefficient, expressed through an SDE driven by that solution's own gradient. Convexity of $\mathsf P$ on $\mathscr L$ is not visible from the formula: $\Phi^\gamma(0,0)$ is defined through a limit of nested Cole–Hopf recursions, and the paper does not prove it, citing a positive-temperature argument instead. Finally, the goal needs the first variation in the direction $\gamma - \gamma_*$, which is generally non-zero near $t = 1$, where $\xi''\gamma$ may blow up. Proposition 6.8 as stated excludes such directions.

Formalization scope

• Mixture. A coefficient sequence c : ℕ → ℝ with $c_0 = c_1 = 0$ and $\sum_k c_k^2(1+\varepsilon)^k < \infty$ for some $\varepsilon>0$. $\xi'$ and $\xi''$ are explicit power series.
• Order parameters. Functions $\mathbb R\to\mathbb R$; membership in $\mathscr U$ and $\mathscr L$ reads only $[0,1)$. Total variation is eVariationOn; finiteness of integrals is IntegrableOn (which includes measurability).
• Cole–Hopf. Step-function data $(m,t,a)$ with $m\ge1$. The $\gamma_i = 0$ pieces use the heat semigroup, the limit of (7.3). The terminal condition is $|x|$. Gaussian expectations are integrals against gaussianReal 0 1.
• $\Phi^\gamma$ on $\mathscr L$. limUnder of the Cole–Hopf values along step-function data converging to $\gamma$ in the weighted $L^1$ distance. $\partial_x$ is deriv in $x$.
• SDE. The published definition EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by $0$ after time $1$. Brownian motion is Mathlib's IsBrownianReal, and expectations are Bochner integrals.
• Minimality. Always attainment, $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma$ in the space, never a real infimum (which Lean sets to $0$ on unbounded sets).
• Disclosed hypothesis. Lemma 6.15 assumes that some $c_k \ne 0$. For $\xi\equiv0$ it is false: $\mathsf P\equiv0$, $X\equiv0$, and the left side is constant in $t$. The goal does not need it.
• Ruled out. A formalization that defines $\Phi^\gamma$ as an arbitrary weak solution of the PDE, or via a choice from an unproved existence statement, would make $\mathsf P$ unconstrained. It is not acceptable. Encoding the hypothesis on $\gamma_*$ as minimality over $\mathscr L$ would make the goal trivial.
• Proof gaps in the source. Convexity of $\mathsf P$ on $\mathscr L$ is cited, not proved. The step from stationarity to the goal applies Proposition 6.8 outside its stated hypotheses. The statements are the paper's and are believed true.
• Out of scope. The paper's algorithmic results (Theorems 2–4, Corollary 2.2) assert algorithms with complexity bounds in an informal computation model, and rest on a long state-evolution analysis. They are not part of this mission.

Contributions welcome: Cole–Hopf regularity (smoothness and the bound $|\partial_x\Phi|\le1$), the Lipschitz estimate in $\gamma$ that makes $\Phi^\gamma$ well defined, well-posedness of the SDE, and Itô calculus for the first variation. The Cole–Hopf layer and the SDE well-posedness are reusable for the companion missions on the full-support theorem and the stochastic-control duality of the same paper.

Selected references

• A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904v1
• A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144(7), 2016. https://arxiv.org/abs/1502.04398
• A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
• M. Talagrand, The Parisi formula, Ann. Math. 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
• D. Panchenko, The Parisi ultrametricity conjecture, Ann. Math. 177(1), 2013. https://arxiv.org/abs/1112.1003

Motivation

In an impulse control problem a controller does not steer a process continuously: at times of its choosing it shifts the state by a finite jump, paying a fixed cost plus a cost proportional to the jump. Such models describe central-bank interventions on an exchange rate, inventory replenishment and cash management. Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) study nonzero-sum games in which two players control the same diffusion by impulses. They prove a verification theorem for such games and apply it to a linear game whose Nash equilibria are explicit.

The paper's interpretation of the linear game is two central banks with different targets for an exchange rate. An explicit equilibrium gives explicit intervention thresholds, and Section 4.4 of the paper asks how these thresholds respond to the fixed cost of intervening. This mission formalizes that comparative-statics question: when intervening becomes more expensive, do the players intervene less?

Setting

The game of Section 4.1 has a discount rate $\rho > 0$, a volatility $\sigma > 0$, running payoffs $f_1(x) = x - s_1$ and $f_2(x) = s_2 - x$ with $s_1 < s_2$, and intervention costs: a player who shifts the state by $\delta$ pays $c + \lambda|\delta|$ and the opponent receives $\tilde c + \tilde\lambda|\delta|$. The standing assumptions of the section are

$$c \ge \tilde c \ge 0,\qquad \lambda \ge \tilde\lambda \ge 0,\qquad (c,\lambda) \ne (\tilde c,\tilde\lambda),\qquad 1 - \lambda\rho > 0 .$$

All parameters except the fixed cost $c$ are held fixed. Set $\theta = \sqrt{2\rho/\sigma^2}$ and $\eta = (1-\lambda\rho)/\rho$, both positive. For $c > 0$ the function

$$F_c(y) = 2y + \theta c - \eta\log\frac{\eta + y}{\eta - y},\qquad y \in (0,\eta),$$

has a unique zero $\xi(c) \in (0,\eta)$. With

$$\Gamma(c) = \frac{\theta(c-\tilde c)}{4\xi(c)} + \frac{\theta c(\lambda-\tilde\lambda)}{4\eta\,\xi(c)} + \frac{\lambda-\tilde\lambda}{2\eta}$$

and a parameter $\tilde s \in \mathbb R$, the paper's formulas (4.20) are

$$\bar x_i(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta+\xi}{\eta-\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],\qquad x_i^*(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta-\xi}{\eta+\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],$$

for $i \in \{1,2\}$, with $\xi = \xi(c)$ and $\Gamma = \Gamma(c)$. In the Nash equilibrium of the paper's Proposition 4.7, player 1 intervenes when the state falls below $\bar x_1$ and moves it to $x_1^*$; player 2 intervenes above $\bar x_2$ and moves it to $x_2^*$. The interval $]\bar x_1(c), \bar x_2(c)[$ is the continuation region, where nobody intervenes. The equilibrium payoffs $V_1^c$, $V_2^c$ are explicit as well (4.27).

Formalization targets

Goal: Proposition 4.13

$$c \mapsto \bar x_2(c)\ \text{is strictly increasing and}\ c \mapsto \bar x_1(c)\ \text{is strictly decreasing on}\ ]\tilde c, +\infty[ .$$

The continuation region therefore widens strictly as the fixed cost grows. The statement concerns the explicit functions (4.20); that they are equilibrium thresholds is mission 2 of this series.

Milestones

1. (4.17). For $c > 0$, $\xi(c)$ is the unique zero of $F_c$ in $(0,\eta)$.
2. (4.28). $\xi \in C^\infty(]0,\infty[)$ with $\xi' = \frac\theta2\frac{\eta^2-\xi^2}{\xi^2}$ and $\xi'' = -\theta\eta^2\frac{\xi'}{\xi^3} = -\frac{\theta^2\eta^2}{2}\frac{\eta^2-\xi^2}{\xi^5}$.
3. (4.29). $\xi$, $c/\xi$ and $c\,\xi'$ tend to $0$ as $c \to 0^+$; $c(\eta-\xi) \to 0$ and $\xi \to \eta$ as $c \to +\infty$.
4. Proposition 4.12. As $c \to +\infty$, $\bar x_2, x_1^* \to +\infty$, $\bar x_1, x_2^* \to -\infty$, and pointwise $V_1^c(x) \to (x-s_1)/\rho$, $V_2^c(x) \to (s_2-x)/\rho$.
5. Proposition 4.14 (with a corrected hypothesis, below). If $\tilde c = 0$, then $x_2^*$ is strictly decreasing and $x_1^*$ strictly increasing on $]0,\infty[$; if moreover $\lambda = \tilde\lambda$, then $x_2^*(c) < \tilde s < x_1^*(c)$ for all $c > 0$.

Significance

Proposition 4.13 is the rigorous form of the economic intuition that costlier intervention makes players more patient. Together with Proposition 4.12 it describes the whole range of costs: the region of inaction grows strictly and invades the real line as $c \to \infty$, where the payoffs converge to those of the uncontrolled Brownian motion. Proposition 4.14 adds that, when the fixed gain vanishes, the targets $x_i^*$ move away from the centre $\tilde s$. The paper's numerical section shows that without $\tilde c = 0$ the targets need not be monotone.

The results are proved in the paper, in a few lines each, by differentiating the implicit function $\xi(c)$. None of them is formalized. The mission produces a machine-checked treatment of a parametrised implicit function, $c \mapsto \xi(c)$ defined by a transcendental equation: smoothness, explicit derivatives, and the asymptotics at both ends. On top of it, it gives a fully verified comparative-statics result for an explicit game equilibrium.

Difficulty

The thresholds depend on $c$ only through $\xi(c)$, which has no closed form, and through $\Gamma(c)$, a sum of terms in $c/\xi(c)$ and $1/\xi(c)$. Monotonicity of $\xi$ alone does not settle the goal: $c/\xi(c)$ is a ratio of two increasing functions, and its direction is decided by how fast $\xi$ grows compared with $c$, uniformly on $]\tilde c,\infty[$, including near $c = 0$, where $F_0$ has no zero and $\xi$ degenerates. The limits as $c \to +\infty$ need more than $\xi(c) \to \eta$: $\Gamma(c)$ grows linearly in $c$, so the rate at which $\eta - \xi(c)$ decays decides whether the targets $x_i^*$ diverge and whether the payoff coefficients vanish.

Formalization scope

The parameters $\rho, \sigma, \lambda, \tilde\lambda, \tilde c, \tilde s, s_1, s_2$ are bundled in a structure, and the standing assumptions not involving $c$ in a predicate $\rho > 0$, $\sigma > 0$, $s_1 < s_2$, $\tilde c \ge 0$, $\lambda \ge \tilde\lambda \ge 0$, $1 - \lambda\rho > 0$. $\theta$ and $\eta$ are computed from $\rho, \sigma, \lambda$ as in (4.21), not taken as free parameters. All quantities are real numbers.

$\xi(c)$ is defined as $\sup\{y \in (0,\eta) : F_c(y) \ge 0\}$. Milestone 1 proves that this is the paper's unique zero for every $c > 0$. For $c \le 0$ the set is empty and the definition returns the placeholder $0$. Every statement therefore restricts $c$ to $c > 0$, to $c > \tilde c$, or to $c \to +\infty$, and no statement can be satisfied through a junk value. On $]\tilde c, \infty[$ one has $\Gamma > 0$, so the square roots in (4.20) are the paper's. "Increasing" and "decreasing" are read strictly, as the proofs give. $C^\infty$ is ContDiffOn ℝ ∞, and $\xi'$ is deriv ξ. Limits at $0^+$ use the right neighbourhood filter.

Two departures from the page are disclosed in the items:

• $c > 0$ in (4.17). The standing assumptions allow $c = 0$ when $\tilde c = 0$ and $\lambda > \tilde\lambda$, but then $F_0$ has no zero; the paper's argument uses $F(0^+) = \theta c > 0$.
• $\lambda = \tilde\lambda$ in the last sentence of Proposition 4.14. For $\lambda > \tilde\lambda$, Proposition 4.11 gives $x_2^*(0^+) > \tilde s$ and the inequality $x_2^* < \tilde s$ fails for small $c$. The monotonicity claims keep the hypothesis $\tilde c = 0$ alone.

A complete development needs the intermediate value theorem and strict monotonicity on an interval, a differentiable implicit (or inverse) function theorem in one variable, and asymptotic estimates of $\log\frac{\eta+y}{\eta-y}$ near $0$ and near $\eta$. These one-variable lemmas about implicitly defined functions are reusable beyond this mission. Proofs of the milestones in any order are welcome.

Selected references

• R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0989 — accepted manuscript arXiv:1605.00039v4, https://arxiv.org/abs/1605.00039