Optimization

Motivation

Best subset selection with ridge shrinkage, the $\ell_0\ell_2$-regularized least squares problem

$$\min_{\beta\in\mathbb R^p}\ \tfrac12\|y-X\beta\|_2^2+\lambda_0\|\beta\|_0+\lambda_2\|\beta\|_2^2,$$

is a mixed integer program. Exact solvers for it rely on branch-and-bound: at every node of the search tree a convex relaxation is solved, and the node is discarded if a lower bound on that relaxation already exceeds the best objective value found so far. Hazimeh, Mazumder and Saab (arXiv:2004.06152v2, Mathematical Programming 2022) build such a solver, L0BnB, for instances with $p$ in the millions. Its relaxations are solved only approximately, by first-order methods, and an approximate primal solution does not by itself certify a lower bound. The bound has to come from a dual feasible point. Theorem 2 of the paper supplies the duals of the node relaxation in closed form, together with explicit formulas for the optimal dual variables as functions of the primal optimum. Everything the paper later proves about the quality of its dual bounds (Section 3.2, Theorem 3) starts from these formulas.

Setting

Data are a matrix $X\in\mathbb R^{n\times p}$ with columns $X_1,\dots,X_p$, a response $y\in\mathbb R^n$, and parameters $\lambda_0,\lambda_2,M>0$, where $M$ bounds the coefficients. Write $[p]=\{1,\dots,p\}$ and $[a]_+=\max\{a,0\}$. The reverse Huber penalty is $\mathcal B(t)=|t|$ for $|t|\le1$ and $\mathcal B(t)=(t^2+1)/2$ for $|t|\ge1$. Define

$$\psi_1(b)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,$$

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$. The reduced relaxation (5) is

$$\min_{\beta\in\mathbb R^p}\ F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i)\quad\text{s.t.}\quad\|\beta\|_\infty\le M.$$

By Theorem 1 of the paper it is the interval relaxation of the perspective formulation, projected onto $\beta$.

The two dual objectives of Theorem 2 are, for $\alpha,\rho\in\mathbb R^n$ and $\gamma,\mu\in\mathbb R^p$,

$$h_1(\alpha,\gamma)=-\tfrac12\|\alpha\|_2^2-\alpha^Ty-\sum_{i\in[p]}v(\alpha,\gamma_i),\qquad v(\alpha,\gamma_i)=\Big[\frac{(\alpha^TX_i-\gamma_i)^2}{4\lambda_2}-\lambda_0\Big]_++M|\gamma_i|,$$ $$h_2(\rho,\mu)=-\tfrac12\|\rho\|_2^2-\rho^Ty-M\|\mu\|_1,$$

where $h_1$ is maximized over all of $\mathbb R^n\times\mathbb R^p$ (problem (20)) and $h_2$ subject to $|\rho^TX_i|-\mu_i\le\lambda_0/M+\lambda_2M$ for $i\in[p]$ (problem (22)). For an optimal $\beta^*$ of (5), with residual $r^*=y-X\beta^*$, the candidate dual variables are

$$\alpha^*=\rho^*=-r^*,\qquad \gamma^*_i=\mathbb 1_{[|\beta^*_i|=M]}\big(\alpha^{*T}X_i-2M\lambda_2\,\mathrm{sign}(\alpha^{*T}X_i)\big),\qquad \mu^*_i=\mathbb 1_{[|\beta^*_i|=M]}\big(|\rho^{*T}X_i|-\lambda_0/M-\lambda_2M\big).$$

In the Lean development these objects are F, box, h1, v, h2, Feas22, alphaStar, gammaStar, rhoStar, muStar in the namespace L0BnB.Duality.

Formalization targets

Goal: Theorem 2 (pp. 13–14)

Let $\beta^*$ minimize $F$ over $\|\beta\|_\infty\le M$.

• If $\sqrt{\lambda_0/\lambda_2}\le M$: $\ h_1(\alpha,\gamma)\le F(\beta)$ for all $\alpha,\gamma$ and all feasible $\beta$, and $h_1(\alpha^*,\gamma^*)=F(\beta^*)$.
• If $\sqrt{\lambda_0/\lambda_2}>M$: $\ h_2(\rho,\mu)\le F(\beta)$ for all $(\rho,\mu)$ feasible for (22) and all feasible $\beta$; $(\rho^*,\mu^*)$ is feasible for (22) and $h_2(\rho^*,\mu^*)=F(\beta^*)$.

This is "(20), respectively (22), is a dual of (5), and (23), respectively (24), are optimal dual variables", with the paper's remark that strong duality holds.

Milestones

1. (45) For $a\in\mathbb R$, $\eta\ge0$ and $D(b)=\psi_1(b)+ab+\eta|b|$, the point $0$ (if $2\sqrt{\lambda_0\lambda_2}+\eta-|a|\ge0$) or $-\sqrt{\lambda_0/\lambda_2}\,\mathrm{sign}(a)$ (otherwise) minimizes $D$ on $|b|\le\sqrt{\lambda_0/\lambda_2}$.
2. (47) If $|a|-\eta\ge2\sqrt{\lambda_0\lambda_2}$, then $\min_{b\in\mathbb R}D(b)=-\frac{1}{4\lambda_2}(|a|-\eta)^2+\lambda_0$.
3. Weak duality, the first halves of both bullets of the goal.
4. (23) $h_1(\alpha^*,\gamma^*)=F(\beta^*)$ when $\sqrt{\lambda_0/\lambda_2}\le M$.
5. (24) $(\rho^*,\mu^*)$ feasible for (22) and $h_2(\rho^*,\mu^*)=F(\beta^*)$ when $\sqrt{\lambda_0/\lambda_2}>M$.

Significance

The result. Theorem 2 turns the node relaxation of L0BnB into a pair of explicit concave maximization problems, one per regime of $\sqrt{\lambda_0/\lambda_2}$ versus $M$. The dual (20) is unconstrained, so any $(\alpha,\gamma)$ gives a valid lower bound; the paper's dual bounds (25)–(28) evaluate $h_1$ or $h_2$ at $\hat\alpha=-\hat r$ built from an inexact primal solution $\hat\beta$, with the remaining variable chosen in closed form. The formulas (23)–(24) explain why this choice is right: at the exact optimum it recovers the primal value. Theorem 3 of the paper, which bounds the loss of this dual bound by a quantity depending on the support size rather than on $p$, compares $v(\hat\alpha,\hat\gamma_i)$ to $v(\alpha^*,\gamma^*_i)$ term by term and therefore depends on (23).

Formalizing it. The paper proves the case $\sqrt{\lambda_0/\lambda_2}\le M$ in Appendix A and omits the proof of the case $\sqrt{\lambda_0/\lambda_2}>M$ ("follows along the lines similar to what was shown above"). The appendix also contains an intermediate formula for the coordinate minimum, $-[(|\alpha^TX_i|-\eta_i)^2/(4\lambda_2)-\lambda_0]_+$, that is incorrect when $\eta_i$ is large; the final dual (49) = (20) is nevertheless correct. A machine-checked proof supplies the omitted case and settles the correct statement. To our knowledge neither half has been formalized.

Difficulty

The dual objective (20) hides the box constraint inside the term $M|\gamma_i|$ and the penalty inside $[\,\cdot\,]_+$, and the reverse Huber penalty is piecewise, so even the weak-duality half has to handle both pieces of $\psi_1$ and the junction $|b|=\sqrt{\lambda_0/\lambda_2}$. The attainment half is where the work lies: it needs the optimality conditions of a nonsmooth convex problem over a box, at coordinates where $\beta^*_i=0$ (where $\psi$ is not differentiable), where $|\beta^*_i|=M$ (where the box is active), and where both may interact with the regime boundary $\sqrt{\lambda_0/\lambda_2}=M$. The natural first idea, to read (23) off the Lagrangian derivation in the paper, does not yield a proof: that derivation assumes a dual optimum $(\alpha^*,\eta^*)$ exists and relates it to $\beta^*$ by complementary slackness, whereas the theorem asserts an identity for the explicit $(\alpha^*,\gamma^*)$ built from $\beta^*$ alone.

Formalization scope

Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; $[p]$ is Fin p. Norms and inner products are explicit sums: $\alpha^TX_i=\sum_r\alpha_rX_{ri}$, $\|\alpha\|_2^2=\sum_r\alpha_r^2$, $\|\mu\|_1=\sum_i|\mu_i|$, $[a]_+=\max\{a,0\}$, and $\|\beta\|_\infty\le M$ is $|\beta_i|\le M$ for every $i$. The regime split is written $\sqrt{\lambda_0/\lambda_2}\le M$ versus $M<\sqrt{\lambda_0/\lambda_2}$. sign is Real.sign, with $\mathrm{sign}(0)=0$; where it is evaluated in (23) the argument is nonzero at an optimum. The optimal solution $\beta^*$ is a hypothesis (feasible and minimizing $F$ over the box); its existence is not part of the statements. The coordinate milestones (45) and (47) are stated for a scalar $a$ standing for $\alpha^TX_i$ and a multiplier $\eta\ge0$. No normalization of $X$ or $y$ is assumed: the unit-norm convention that opens Section 3 is not used by Theorem 2. The paper writes no $O(\cdot)$ in these results, so no constants are instantiated.

"A dual is given by" is formalized as weak duality over all dual-feasible points together with equality at the explicit dual variables. Weak duality alone would not be Theorem 2, and neither would the equality alone; the goal requires both in both regimes. Uniqueness of the dual optimum is not claimed.

A complete development needs elementary convex analysis of the scalar penalty $\psi_1$ (its conjugate and subdifferential), first-order optimality conditions for a convex function over a box in $\mathbb R^p$, and finite-sum bookkeeping. The scalar facts about the reverse Huber penalty are reusable in the companion missions on the reduced relaxation and on dual-bound quality. Contributions to any milestone, or a direct proof of the goal, are welcome.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2 (2021); Mathematical Programming (2022). https://arxiv.org/abs/2004.06152v2
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/
• A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007. https://doi.org/10.1090/conm/443/08555
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388
• H. Hazimeh, R. Mazumder, Fast best subset selection: coordinate descent and local combinatorial optimization algorithms, Operations Research 68(5), 1517–1537, 2020. https://arxiv.org/abs/1803.01454

Motivation

The martingale optimal transport problem asks for a coupling of two probability measures $\mu,\nu$ on $\mathbb R$ that is the law of a one-step martingale and minimizes an expected cost. It arises in robust finance, where the marginals are the risk-neutral laws of an asset at two dates implied by option prices, and model-independent price bounds for exotic options are the extreme values of the problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014).

Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 44(1), 2016) construct a canonical martingale coupling, the left-curtain coupling, which plays the role that the monotone (quantile) coupling plays in classical transport. Its construction rests on one object, the shadow of a measure in another, and on one structural property of it: shadows are associative. This mission formalizes that property, Theorem 4.8 of the paper, together with the chain of results in §2.3 and §4.1–4.3 on which it rests.

Setting

Let $\mathcal M$ be the set of finite Borel measures on $\mathbb R$ with finite first moment, of any total mass. For $\mu,\nu\in\mathcal M$:

• the convex order $\mu\preceq_C\nu$ holds if $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ (this forces equal masses and equal barycentres);
• the extended convex order $\mu\preceq_E\nu$ holds if the same inequality holds for every nonnegative convex $\varphi$; it holds both when $\mu\preceq_C\nu$ and when $\mu\le\nu$ setwise;
• the potential function of $\mu$ is $u_\mu(x)=\int|y-x|\,d\mu(y)$;
• a sequence $(\nu_n)$ converges weakly in $\mathcal M$ to $\nu$ if $\int f\,d\nu_n\to\int f\,d\nu$ for every continuous bounded $f$ and $\int|x|\,d\nu_n\to\int|x|\,d\nu$.

If $\mu\preceq_E\nu$, a shadow of $\mu$ in $\nu$ is a measure $\eta$ with (i) $\eta\le\nu$, (ii) $\mu\preceq_C\eta$, and (iii) $\eta\preceq_C\eta'$ for every $\eta'$ satisfying (i) and (ii). Lemma 4.6 of the paper shows that it exists and is unique; it is written $S^\nu(\mu)$. It is the least spread-out part of $\nu$ into which $\mu$ can be transported by a martingale. An atom is a measure $\alpha\,\delta_x$ with $\alpha\ge0$.

In the Lean development these objects are InM, ConvexLE, ExtConvexLE, potential, ConvergesInM and the predicate IsShadow ν μ η, in the namespace MartOT.Shadow.

Formalization targets

Goal: Theorem 4.8 (shadow of a sum), p. 25

For $\gamma_1,\gamma_2,\nu\in\mathcal M$ with $\gamma_1+\gamma_2\preceq_E\nu$,

$$\gamma_2\preceq_E\nu-S^\nu(\gamma_1)\qquad\text{and}\qquad S^\nu(\gamma_1+\gamma_2)=S^\nu(\gamma_1)+S^{\nu-S^\nu(\gamma_1)}(\gamma_2).$$

Milestones, in attack order

1. Proposition 4.2 (p. 21): for equal masses, $\mu\preceq_C\nu\iff u_\mu\le u_\nu$; $\mu\le\nu\iff u_\nu-u_\mu$ is convex; for fixed mass and mean, convergence in $\mathcal M$ is pointwise convergence of potential functions.
2. Proposition 4.4 (p. 21): $\mu\preceq_E\nu$ implies $\mu\preceq_C\theta$ for some $\theta\le\nu$.
3. Lemma 4.6 (p. 23): existence, uniqueness and property (iii′) of the shadow.
4. Example 4.7 (p. 24): the shadow of an atom is the restriction of $\nu$ between two quantiles.
5. Lemma 4.11 (p. 27): $\eta-S^\eta(\delta)\le\nu-S^\nu(\delta)$ for an atom $\delta\preceq_E\eta\le\nu$.
6. Lemma 4.12 (p. 27): the goal when $\gamma_1$ is an atom.
7. Lemma 4.13 (p. 28): the shadow of finitely many atoms, built one atom at a time.
8. Lemma 2.9 (p. 15): approximation of $\gamma\in\mathcal M$ by a $\preceq_C$-increasing sequence of finitely supported measures below it.
9. Proposition 4.15 (p. 29): shadows pass to limits of $\preceq_C$-increasing sequences.
10. Lemma 4.16 (p. 29): the goal when $\gamma_2$ is an atom, with $\delta\preceq_E S^\nu(\gamma+\delta)-S^\nu(\gamma)$.

Significance

Theorem 4.8 is what makes the left-curtain coupling well defined and consistent. That coupling is the martingale plan which, for every $x$, sends $\mu|_{]-\infty,x]}$ onto $S^\nu(\mu|_{]-\infty,x]})$ (Theorem 4.18). Associativity says that the parts of $\nu$ assigned to $\mu|_{]-\infty,x]}$ and to $\mu|_{]x,x']}$ fit together into the part assigned to $\mu|_{]-\infty,x']}$, so the family of shadows defines a single coupling. The uniqueness of left-monotone martingale plans and the optimality of the left-curtain coupling for the costs $h(y-x)$ with $h'$ strictly convex, both later results of the paper, rest on it.

The result is proved in the paper. As far as is known it has no machine-checked proof. This mission produces a statement of it, and of the supporting results, in terms of measures of arbitrary finite mass with no reference to a chosen shadow function. A complete development would give Lean a theory of the convex order on finite measures through potential functions, which is reusable well beyond martingale transport.

Difficulty

For finitely atomic measures the identity follows by adding one atom at a time (Lemmas 4.12, 4.13, 4.16), but even the single-atom step needs a monotonicity property of shadows of atoms in varying targets (Lemma 4.11), and that property comes from their explicit description through quantile functions. The general case cannot be obtained by a direct manipulation of the minimality property (iii): minimality of $S^\nu(\gamma_1)$ and of $S^{\nu-S^\nu(\gamma_1)}(\gamma_2)$ separately says nothing obvious about minimality of their sum among measures dominating $\gamma_1+\gamma_2$, because a competitor for the sum need not split into competitors for the summands. The paper passes to the limit along convex-order approximations, which requires a continuity property of the shadow (Proposition 4.15) in the topology of $\mathcal M$.

Formalization scope

• Measures are MeasureTheory.Measure ℝ with membership in $\mathcal M$ stated explicitly (InM: finite measure, identity integrable). Masses are arbitrary; nothing is normalized to probability measures.
• Integrals of convex test functions are taken in EReal through the published ModelRiskOT.Duality.extIntegral (positive minus negative part), never as Bochner integrals, so a non-integrable test function cannot produce a junk value. The extended convex order uses lower Lebesgue integrals of nonnegative functions.
• Shadows are the predicate IsShadow ν μ η, never a function built by choice. Every statement about $S^\nu(\cdot)$ quantifies over all shadows, which with existence and uniqueness (Lemma 4.6, a milestone) is the paper's statement. Uniqueness is part of the conclusion of Lemma 4.6 and is not assumed elsewhere.
• $\nu-\eta$ is Mathlib's truncated subtraction of measures. It is used only where $\eta\le\nu$ is guaranteed by property (i) of a shadow. Lemma 4.16 additionally asserts $S^\nu(\gamma)\le S^\nu(\gamma+\delta)$, so that the difference there is a genuine one.
• Not a trivialization: in the goal, neither $\eta_1+\eta_2\le\nu$ nor $\gamma_1+\gamma_2\preceq_C\eta_1+\eta_2$ nor the minimality of $\eta_1+\eta_2$ is assumed; all three are the content of the conclusion IsShadow ν (γ1 + γ2) (η1 + η2).
• Added relative to the page: Lemma 4.11 states $\nu\in\mathcal M$, which the paper takes from context. Proposition 4.2's third bullet is split into an equivalence for each candidate limit and a uniqueness clause, which together are equivalent to the printed sentence. Lemma 4.10 (continuity of $\nu\mapsto S^\nu(\delta)$ in the Kantorovich metric) and Proposition 4.17 are not included.
• Needed infrastructure: potential functions and their second distributional derivatives, quantile functions of finite measures, weak convergence of finite measures with first moments. Contributions to any of these are welcome.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509v2, doi:10.1214/14-AOP966
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3), 477–501, 2013. doi:10.1007/s00780-013-0205-8
• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24(1), 312–336, 2014. doi:10.1214/13-AAP925
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36, 423–439, 1965. doi:10.1214/aoms/1177700153

Motivation

Online retailers show their catalogue on a sequence of pages, and most visitors never reach the last one. Which products appear on the first page, and at what prices, therefore decides what a typical consumer can buy at all. Gallego, Li, Truong and Wang (Operations Research, 2020) model this as the product framing problem: the consideration set of a consumer is the set of products on the pages that consumer is willing to view, and the number of pages viewed is random. Their Section 7 adds prices to the problem and asks how a retailer should frame and price jointly when consumers choose by the multinomial logit (MNL) model.

The question connects two literatures. In assortment pricing under MNL with a common price sensitivity, the optimal prices of all offered products are known to be equal (Anderson, de Palma and Thisse 1992; Gallego and Stefanescu, as cited on p. 16 of the paper), and the nested-logit extension of Gallego and Wang (Operations Research, 2014) keeps an adjusted markup constant across nests. In search and ranking models, the order in which products are shown changes which ones are bought. The paper's structural results say what survives of the equal-price rule once consideration sets are nested by page, and which products belong on the early pages.

Setting

There are $n$ products, $i \in [n] = \{1,\dots,n\}$, and $m$ pages, each holding at most $p$ products. A framing places each product on one page $x(i)\in[m]$ or leaves it undisplayed. A consumer views the first $X$ pages, where $X\in[m]$ is random with law $\lambda(x)=\mathbf P[X=x]$, independent of the framing. A consumer who views $x$ pages considers $S(x)$, the products on pages $1,\dots,x$, so $S(1)\subseteq S(2)\subseteq\cdots\subseteq S(m)$.

Product $i$ has a quality $a_i\in\mathbb R$ and a price $r_i\in\mathbb R$, and the price sensitivity is $\beta>0$. The mean utility of product $i$ is $u_i=a_i-\beta r_i$, and the outside option has utility $u_0=0$. Under the MNL model a consumer with consideration set $S$ buys $i\in S$ with probability

$$P(i,S)=\frac{e^{u_i}}{1+\sum_{k\in S}e^{u_k}},$$

and $P(i,S)=0$ for $i\notin S$. The expected revenue from that consumer is $R(r\mid S)=\sum_{i\in S}r_iP(i,S)$, and the total expected revenue of a framing and a price vector is

$$\mathbf E\big[R(r\mid S(X))\big]=\sum_{x=1}^m\lambda(x)\,R\big(r\mid S(x)\big).$$

For a fixed framing, $R(a)$ denotes the optimal value of this quantity over all price vectors, as a function of the quality vector $a$.

Formalization targets

Goal: Theorem 6 (p. 17)

The goal is the existence of an optimal joint solution with the paper's structure: there are a feasible framing and prices $r\in\mathbb R^n$ such that no feasible framing with any prices earns more, and

$$|S(x)|=\min(n,\;x\,p)\quad\text{for all }x\in[m],\qquad a_k\le a_i\ \text{ whenever } i \text{ is displayed and } k \text{ is undisplayed or on a later page.}$$

Pages are filled in order until all products are displayed, and the products appear in descending order of quality.

Milestones

1. (15), p. 43. The partial derivative of the total expected revenue in the price of a displayed product:

$$\frac{\partial\,\mathbf E[R(r\mid S(X))]}{\partial r_i}=\beta\sum_{l=x(i)}^m\lambda(l)P\big(i,S(l)\big)\Big\{\tfrac1\beta+R\big(r\mid S(l)\big)-r_i\Big\}.$$

2. (17), p. 43. At every optimal price vector, each displayed price is $1/\beta$ plus a weighted average of the revenues $R(r\mid S(l))$, $l\ge x(i)$.
3. Theorem 5, p. 16. For a fixed framing, every optimal price vector is constant on each page, $r_i=\theta_{x(i)}$, with $\theta_1\le\theta_2\le\cdots\le\theta_m$.
4. (19), p. 44. The optimal value $R(a)$ is nondecreasing in the quality of any displayed product.

Significance

Theorem 5 reduces the pricing problem of a fixed framing from $n$ prices to $m$ page prices and says that later pages carry higher prices; this is the page-level analogue of the constant-markup property of MNL pricing, and it runs opposite to the ordering found in oligopoly search models (Arbatskaya 2007). Theorem 6 removes the framing decision almost entirely: a joint optimum is obtained by sorting the products by quality and filling pages in that order, leaving only page prices to choose. The paper's approximation algorithm for joint pricing and framing (Theorem 7, NEST-P, with guarantee $6/\pi^2$) starts from this structure.

None of these statements has a machine-checked proof. A complete development would give the first formal treatment of MNL price optimization with nested consideration sets, including the existence of optimal prices, which the paper takes for granted. The paper's argument for the monotonicity $\theta_1\le\cdots\le\theta_m$ and its envelope-theorem step (19) are informal; a formal proof has to supply both.

Difficulty

The expected revenue is not concave in the prices, even with two products on two pages (Example 1, p. 17), so the first-order condition alone does not identify the optimum, and existence of an optimal price vector has to be argued from the behaviour of the revenue as prices tend to $\pm\infty$. The within-page equality of prices follows from the first-order condition, but the ordering of page prices needs a global comparison of revenues across consideration sets. In Theorem 6, the obvious exchange argument (swap a higher-quality product forward) does not obviously keep revenue from decreasing when the swapped products have different prices; the paper splits into two cases, and in one of them the improvement comes from continuously moving qualities, which requires control of the optimal value as a function of $a$ rather than of a fixed price vector.

Formalization scope

Products are Fin n, pages are the natural numbers $1,\dots,m$ with $m\ge1$, and capacities satisfy $p\ge1$. A framing is f : Fin n → ℕ with page f i ∈ [m] for displayed products and f i = 0 for undisplayed ones (the paper's $x(i)=m+1$); feasibility means at most $p$ products per page. The law of $X$ is a nonnegative function on $[m]$ summing to one. Prices are finite reals: the paper's priced-out products ($r_i=+\infty$) coincide with undisplayed ones, which the framing already allows. "Descending order" and "increases" are read weakly.

Theorem 5 and (17) are stated for every maximizing price vector and only for products on pages that some consumer reaches ($\Lambda(x)=\mathbf P[X\ge x]>0$), a restriction the paper never discusses: a product on a page no consumer reaches can carry any price at an optimum. They do not assert that a maximizer exists. Theorem 6 is read existentially ("some optimal solution has this structure"); the universal reading is false when some $\lambda(x)=0$, because exchanging products between pages $x$ and $x+1$ then changes no revenue. (19) is formalized as its stated consequence, the monotonicity of the optimal value $R(a)=\sup_r\mathbf E[R(r\mid S(X))]$, together with the boundedness of the revenues; the envelope identity itself would need a differentiable selection of optimal prices that the paper does not establish.

A trivializing formalization of the goal would take the optimum over framings that are already sorted, over a single fixed framing, or over prices fixed in advance; the goal's optimality clause ranges over all feasible framings and all real price vectors. The development needs elementary calculus of the MNL revenue (HasDerivAt, Real.exp), finite sums over pages, and a compactness or limiting argument for the existence of optimal prices. Pages are those of the authors' accepted manuscript, which differ from the journal typesetting. Proofs of any milestone, and lemmas on MNL pricing reusable beyond this paper (boundedness of $R(r\mid S)$, existence of optimal MNL prices, the constant-price property for a single assortment), are welcome.

Selected references

• G. Gallego, A. Li, V.-A. Truong, X. Wang, Approximation Algorithms for Product Framing and Pricing, Operations Research 68(1), 2020. https://doi.org/10.1287/opre.2019.1875
• S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992 (book; cited by the paper for the equal-price property of MNL pricing).
• G. Gallego, R. Wang, Multiproduct Price Optimization and Competition under the Nested Logit Model with Product-Differentiated Price Sensitivities, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2013.1249
• M. Arbatskaya, Ordered Search, The RAND Journal of Economics 38(1), 2007. http://www.jstor.org/stable/25046295

Motivation

A martingale transport plan between two laws $\mu$ and $\nu$ on $\mathbb R$ is a joint law of a pair $(X,Y)$ with $X\sim\mu$, $Y\sim\nu$ and $E[Y\mid X]=X$. Minimizing or maximizing $E[c(X,Y)]$ over such plans gives the model-independent price bounds of an option with payoff $c(X,Y)$ when the market quotes vanilla options at two maturities, and so fixes the marginal laws $\mu$ and $\nu$ of the asset price. For the forward-starting straddle, with payoff $|Y-X|$, the two bounds are the problems with costs $-|y-x|$ and $|y-x|$.

• 1965: Strassen (doi:10.1214/aoms/1177700153) shows that martingale plans between $\mu$ and $\nu$ exist if and only if $\mu$ and $\nu$ are in convex order.
• 2012: Hobson and Neuberger (doi:10.1111/j.1467-9965.2010.00473.x) identify the optimizer for $-|y-x|$ through a construction of dual maximizers, under conditions on the marginals.
• 2012: Hobson and Klimmek communicate a description of the optimizer for $+|y-x|$ to Beiglböck and Juillet, cited there as private communication (arXiv:1208.1509v2, §7.4 and reference 15).
• 2016: Beiglböck and Juillet (arXiv:1208.1509v2) prove existence, uniqueness and the shape of the optimizer for $|y-x|$ for every continuous starting law, using only the primal problem and their variational lemma.

Setting

$\mu$ and $\nu$ are Borel probability measures on $\mathbb R$ with finite first moments, in convex order: $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ (Definition 2.1). $\Pi_M(\mu,\nu)$ is the set of measures $\pi$ on $\mathbb R^2$ with marginals $\mu$ and $\nu$ such that $y-x$ is $\pi$-integrable and

$$\int\rho(x)\,(y-x)\,d\pi(x,y)=0\qquad\text{for every bounded Borel }\rho,$$

which is the paper's characterization (4) of "the disintegration $\pi_x$ has barycentre $x$". For the cost $c(x,y)=|y-x|$ the cost of a plan is $\int|y-x|\,d\pi\in[0,\infty)$, and $\pi$ is optimal if it minimizes this over $\Pi_M(\mu,\nu)$. $\mu$ is continuous if $\mu(\{x\})=0$ for every $x$.

$\mu\wedge\nu$ is the largest measure below both $\mu$ and $\nu$ (Example 2.5); $(\mathrm{Id}\otimes\mathrm{Id})_\#\eta$ is the image of $\eta$ under $x\mapsto(x,x)$, a measure on the diagonal $\Delta=\{(x,x)\}$. For $\Gamma\subseteq\mathbb R^2$, $\Gamma_x=\{y:(x,y)\in\Gamma\}$, and $\operatorname{graph}(T)=\{(x,T(x))\}$.

Formalization targets

Goal: Theorem 7.4 (p. 43)

If $\mu\preceq_C\nu$ and $\mu$ is continuous, there is a unique optimal $\pi_{\mathrm{abs}}\in\Pi_M(\mu,\nu)$ for $c(x,y)=|y-x|$; it is concentrated on a set $\Gamma$ with $|\Gamma_x|\le3$ for every $x$; and

$$\pi_{\mathrm{abs}}=(\mathrm{Id}\otimes\mathrm{Id})_\#(\mu\wedge\nu)+\pi_{\mathrm{go}},\qquad \pi_{\mathrm{go}}\ \text{concentrated on}\ \operatorname{graph}(T_1)\cup\operatorname{graph}(T_2)$$

for some functions $T_1,T_2:\mathbb R\to\mathbb R$.

Milestones, in attack order

1. Attainment of the minimum (§2.1, pp. 10–11).
2. Lemma 1.11, the variational lemma (p. 8).
3. Lemma 7.5, the sign of a three-point cost difference (pp. 43–44).
4. The forbidden configurations (24) on a finitely optimal set (p. 45).
5. The static part: $\pi|_\Delta=(\mathrm{Id}\otimes\mathrm{Id})_\#(\mu\wedge\nu)$ for every optimal $\pi$ (pp. 45–46).
6. Lemma 3.2, accumulation of uncountably many large fibres (p. 19).
7. At most two off-diagonal points per fibre (p. 46).
8. The reduced problem between $\mu-\mu\wedge\nu$ and $\nu-\mu\wedge\nu$ (p. 46).
9. Lemma 5.5, two Borel graphs (p. 35), and Lemma 5.6, uniqueness from at most two points per fibre (p. 36).

Significance

The theorem identifies the lower model-independent bound for the forward-starting straddle: the extremal model keeps the mass that $\mu$ and $\nu$ share in place and splits every other starting point between at most two destinations. With Theorem 7.3 for $-|y-x|$ it settles both bounds for continuous $\mu$ without any dual attainment, which is known to fail in general. The decomposition into a static part $\mu\wedge\nu$ and a part between marginals with $\bar\mu\wedge\bar\nu=0$ is a reduction that applies to other costs vanishing on the diagonal.

The result is proved in the paper; nothing in it has been machine-checked. The mission produces a formal statement of Theorem 7.4 and of each step of its proof, a Lean vocabulary for martingale transport on $\mathbb R$ shared with the other missions of this series, and the general measure-theoretic lemmas (3.2, 5.5, 5.6) that the structure theorems of the paper all use.

Difficulty

Lemma 7.5 and (24) are elementary; the work lies in passing from them to statements about measures. The variational lemma needs Kellerer's duality-type result for finitely optimal sets. The static part requires showing that a positive defect $\kappa=\mu\wedge\nu-\pi(\Delta\text{-projection})$ produces, at $\kappa$-almost every point, a forbidden configuration, which uses the disintegration of the moving part. The cardinality bound requires the accumulation argument of Lemma 3.2, and the forbidden configurations only hold for points that lie strictly inside the range of their own fibre, which the martingale condition supplies only almost everywhere. Uniqueness does not follow from strict convexity of a cost functional, since the problem is linear: it comes from the two-graph structure through Lemma 5.6, and it fails if $\mu$ has atoms (Remark 7.7).

Formalization scope

Measures are Mathlib Measure ℝ and Measure (ℝ × ℝ) with Borel σ-algebras. Costs are integrals in the extended reals through the published ModelRiskOT.Duality.extIntegral; the cost $|y-x|$ is nonnegative and, under finite first moments, finite. Martingale plans are encoded by condition (4), competitors by the same device. $\mu\wedge\nu$ is the infimum in Mathlib's complete lattice of measures, measure subtraction is Mathlib's truncated subtraction, cardinalities of fibres are Set.encard in $\mathbb N\cup\{\infty\}$, and "concentrated on $A$" is $\pi(A^c)=0$. Continuity of $\mu$ is $\mu(\{x\})=0$ for all $x$. As on the page, $\Gamma$, $T_1$ and $T_2$ in the goal carry no measurability requirement.

Two choices differ from a literal reading and are disclosed in the items: (24) carries the hypothesis $y^-<x<y^+$ of Lemma 7.5, which the page invokes and without which (24) is false; and the steps that do not need continuity of $\mu$ (the static part, the reduced problem) are stated without it.

A trivializing formalization is ruled out: $\mu\wedge\nu$ is the lattice infimum of measures, not a product and not a pointwise minimum of set values, and all four conjuncts of the goal (existence, uniqueness, the bound 3, the decomposition) are asserted together.

Reusable beyond this mission: the Setting layer (convex order, $\Pi_M$, competitors), Lemma 3.2, Lemma 5.5 (a Lusin–Novikov consequence) and Lemma 5.6. Proofs of any milestone, and infrastructure on disintegrations of plans on $\mathbb R^2$, are welcome.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509v2, doi:10.1214/14-AOP966
• D. Hobson, A. Neuberger, Robust bounds for forward start options, Mathematical Finance 22(1), 31–56, 2012. doi:10.1111/j.1467-9965.2010.00473.x
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36, 423–439, 1965. doi:10.1214/aoms/1177700153
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995 (Theorem 18.11). doi:10.1007/978-1-4612-4190-4

Motivation

In classical optimal transport on the real line, one coupling plays a distinguished role: the monotone (Hoeffding–Fréchet) coupling, which sends the $q$-quantile of the first marginal to the $q$-quantile of the second. It is canonical (every initial segment of the first marginal goes as far left as possible) and it is optimal for a whole family of costs at once.

Martingale optimal transport adds the constraint that the coupling be the law of a one-step martingale $(X, Y)$, $\mathbb E[Y\mid X]=X$. The problem arises in robust (model-independent) mathematical finance: prices of vanilla options fix the marginal laws $\mu$ of $X$ and $\nu$ of $Y$, and bounds on the price of an exotic option $c(X,Y)$ that hold under every arbitrage-free model are values of the martingale transport problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). Martingale couplings exist exactly when $\mu$ and $\nu$ are in convex order (Strassen 1965).

Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 44(1), 2016) asked for the martingale counterpart of the monotone coupling, and found it: the left-curtain coupling $\pi_{\mathrm{lc}}$. This mission formalizes its existence and uniqueness (Theorem 1.5), which is the foundation for the paper's later optimality results (Theorems 1.7, 6.1 and 6.3, other missions of this series).

Setting

All measures are Borel measures on $\mathbb R$ or $\mathbb R\times\mathbb R$. $\mathcal M$ is the set of finite measures $\mu$ with $\int|x|\,d\mu<\infty$. For $\mu,\nu\in\mathcal M$:

• Convex order $\mu\preceq_C\nu$: $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$ (Definition 2.1). It forces equal mass and equal mean. Extended convex order $\mu\preceq_E\nu$: the same inequality for nonnegative convex $\varphi$ only (Definition 4.3); it allows $\mu(\mathbb R)<\nu(\mathbb R)$.
• Martingale transport plans $\Pi_M(\mu,\nu)$: measures $\pi$ on $\mathbb R^2$ with marginals $\mu$ and $\nu$ and $\int\rho(x)(y-x)\,d\pi(x,y)=0$ for every bounded Borel $\rho$, that is, the conditional barycentre of $\pi_x$ is $x$ for $\mu$-a.e. $x$.
• Left-monotone plans (Definition 1.4): $\pi$ is concentrated on a Borel set $\Gamma$ that contains no three points $(x,y^-),(x,y^+),(x',y')$ with $x<x'$ and $y^-<y'<y^+$. Mass leaving a point $x$ to both sides of $y'$ forbids any later point $x'>x$ from sending mass to $y'$.
• Shadow (Lemma 4.6): for $\mu\preceq_E\nu$, $S^\nu(\mu)$ is the measure $\eta\le\nu$ with $\mu\preceq_C\eta$ that is least in the convex order among all such $\eta$: the least spread-out part of $\nu$ into which $\mu$ can be embedded by a martingale.
• Left-curtain coupling (Theorem 4.18): the plan $\pi_{\mathrm{lc}}$ with $\operatorname{proj}^x_\#(\pi_{\mathrm{lc}}|_{]-\infty,x]\times\mathbb R})=\mu|_{]-\infty,x]}$ and $\nu^{\pi_{\mathrm{lc}}}_x:=\operatorname{proj}^y_\#(\pi_{\mathrm{lc}}|_{]-\infty,x]\times\mathbb R})=S^\nu(\mu|_{]-\infty,x]})$ for every $x$.

In Lean these are InM, ConvexLE, ExtConvexLE, IsMartingalePlan, IsLeftMonotone, IsShadow, IsLeftCurtain and targetUpTo in the shared namespace MartOT.Var. The mission's own theorems are in MartOT.Curtain.

Formalization targets

Goal: Theorem 1.5 (p. 6)

For probability measures $\mu\preceq_C\nu$ on $\mathbb R$ with finite first moments,

$$\exists!\,\pi\quad\pi\in\Pi_M(\mu,\nu)\ \text{ and }\ \pi\text{ is left-monotone}.$$

Existence alone, or uniqueness only among left-curtain plans, is not the goal: the statement says that monotonicity alone singles out one martingale coupling.

Milestones

1. Lemma 4.6: shadows exist and are unique, and satisfy (iii′) for the extended order.
2. Monotonicity of shadows (§4.4, p. 31): $\mu\le\mu'\preceq_E\nu$ implies $S^\nu(\mu)\le S^\nu(\mu')$.
3. Theorem 4.18: $\pi_{\mathrm{lc}}$ exists, is unique, is a probability measure and lies in $\Pi_M(\mu,\nu)$.
4. Theorem 1.8: $\nu^{\pi_{\mathrm{lc}}}_t\preceq_C\nu^\pi_t$ for every $t$ and every $\pi\in\Pi_M(\mu,\nu)$.
5. Lemma 1.11 (variational lemma): an optimal plan of finite cost lives on a Borel set on which no finitely supported measure has a cheaper competitor.
6. Proof of Theorem 4.21: $\pi_{\mathrm{lc}}$ is optimal for every cost $c_{s,t}(x,y)=\mathbf 1_{]-\infty,s]}(x)|y-t|$.
7. Theorem 4.21: $\pi_{\mathrm{lc}}$ is left-monotone (the existence half of the goal).
8. Lemma 5.1: end-point behaviour of $\mu\preceq_C\nu$ at $\sup\operatorname{spt}\mu$ and $\inf\operatorname{spt}\mu$.
9. Lemma 5.2: a nonzero signed measure of mass $0$ is detected by a test function $g_{a,b}$ anchored in the support of its positive part.
10. Theorem 5.3: every left-monotone martingale plan is the left-curtain coupling of its marginals (the uniqueness half).

Significance

Theorem 1.5 identifies a canonical martingale coupling defined by a geometric property of its support alone. The paper then shows that $\pi_{\mathrm{lc}}$ is the unique optimizer of the martingale transport problem for costs $h(y-x)$ with $h'$ strictly convex (Theorem 1.7) and that it is characterized by the convex-order minimality of Theorem 1.8. The left-curtain coupling has since been studied and generalized in a series of works (for instance Henry-Labordère and Touzi 2016).

The result is proved in the paper. It has, as far as the platform's catalogue shows, no machine-checked proof: no statement about martingale transport plans, shadows or the left-curtain coupling exists on Prove2Me. A formal development would produce reusable infrastructure: the convex order on finite measures of arbitrary mass, shadows, and the passage between the barycentre characterization (4) of martingale plans and their disintegrations.

Difficulty

Existence is not the hard part in the abstract: a left-monotone plan can be obtained as an optimizer for a suitable cost via the variational lemma. The construction through shadows is more delicate: one must show that the shadows of the initial segments $\mu|_{]-\infty,x]}$ increase with $x$ (this rests on Theorem 4.8, the shadow of a sum) and that the resulting plan satisfies the martingale property.

Uniqueness is the main obstacle. The classical argument for uniqueness of optimal plans (averaging two candidates and using strict convexity) requires a continuous first marginal and does not apply to arbitrary $\mu$ with atoms. The paper's argument is specific to the problem: it compares $\nu^\pi_x$ with the shadow $\nu^{\pi_{\mathrm{lc}}}_x$ through the test functions $g_{u,v}$ and a case analysis at the support end-points, which needs the measure-theoretic Lemmas 5.1 and 5.2.

Formalization scope

• Measures are MeasureTheory.Measure ℝ and Measure (ℝ × ℝ) with Borel σ-algebras. The goal and Theorems 1.8, 4.18, 4.21 take $\mu,\nu$ probability measures (IsProbabilityMeasure) in convex order; Lemma 4.6, the shadow monotonicity, Lemma 5.1 and Theorem 5.3 work in $\mathcal M$, as the paper's Sections 4–5 do.
• Integrals of convex functions and costs are extended-real valued (EReal, through the published ModelRiskOT.Duality.extIntegral), so no Bochner integral of a non-integrable function enters a statement. $\Pi_M$ is encoded by characterization (4) of the paper, not by disintegrations.
• Shadows and the left-curtain coupling are predicates (IsShadow, IsLeftCurtain), never chosen functions: their existence and uniqueness are milestones, not definitions. A formalization that defined $\pi_{\mathrm{lc}}$ by a choice and the left-monotone plan as "the left-curtain plan" would make the goal circular; the goal mentions only $\Pi_M$ and left-monotonicity.
• "$\pi(\Gamma)=1$" is written $\pi(\Gamma^c)=0$; the support of a measure is Mathlib's Measure.support.
• No hypothesis is added to any statement of the page. In Lemma 5.1, $\sup\operatorname{spt}\mu$ is the real supremum of the support under BddAbove; at $\mu=0$ Lean's convention $\sup\emptyset=0$ applies.
• Reading: Theorem 1.8's "minimal" is formalized as "least" (below every member of the family), which is how the paper uses it.
• Strassen's theorem is not restated; it is already posed on the platform as PalmQueueing.Ordering.strassen_cx.

Contributions are welcome at every level: proofs of the milestones, auxiliary lemmas on the convex order of finite measures (potential functions $u_\mu$, equality of mass and mean), and the equivalence between (4) and the disintegration form of the martingale property.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509, doi:10.1214/14-AOP966
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3), 477–501, 2013. arXiv:1106.5929
• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24(1), 312–336, 2014. doi:10.1214/13-AAP925
• V. Strassen, The existence of probability measures with given marginals, Ann. Math. Statist. 36(2), 423–439, 1965. doi:10.1214/aoms/1177700153
• P. Henry-Labordère, N. Touzi, An explicit martingale version of the one-dimensional Brenier theorem, Finance Stoch. 20(3), 635–668, 2016. arXiv:1302.4854

Motivation

Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks: a stochastic gradient method that keeps an exponential moving average $m_n$ of past gradients and an exponential moving average $v_n$ of their coordinatewise squares, and divides the first by the square root of the second. Its practical success came well before any convergence theory for nonconvex objectives. Reddi, Kale and Kumar (2018) showed that Adam with constant momentum parameters can fail to converge even on convex problems, which made the question of under which parameter schedules Adam provably converges a live one.

Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 2021) answer it through the ODE method of stochastic approximation (Benaïm, 1999). This mission takes the paper's almost-sure convergence theorem for Adam with decreasing stepsizes, Theorem 5.2. Under a stepsize schedule in which $1 - \alpha_n$ and $1 - \beta_n$ shrink in proportion to the stepsize $\gamma_n$, the iterates converge almost surely to the critical points of the objective, provided they stay bounded.

Setting

Let $\xi$ be a random variable on a measurable space $\Xi$ with law $\mu$, let $f : \mathbb R^d \times \Xi \to \mathbb R$ be an integrand with gradient $\nabla f(x, \xi)$ in $x$, and set

$$F(x) = \mathbb E f(x, \xi), \qquad S(x) = \mathbb E\big(\nabla f(x,\xi)^{\odot 2}\big), \qquad \mathcal S = \nabla F^{-1}(\{0\}),$$

where $\odot 2$ is the coordinatewise square and $\mathcal S$ is the critical set. Let $\xi_1, \xi_2, \dots$ be iid copies of $\xi$ on a probability space $(\Omega, \mathcal F, \mathbb P)$.

Algorithm 5.1 takes stepsizes $\gamma_n > 0$, weights $\alpha_n, \beta_n \in [0,1]$ and a constant $\varepsilon > 0$. Starting from $x_0 \in \mathbb R^d$, $m_0 = v_0 = 0$ and $r_0 = \bar r_0 = 0$, it computes for $n \ge 1$, with all vector operations coordinatewise:

$$\begin{aligned} m_n &= \alpha_n m_{n-1} + (1-\alpha_n)\nabla f(x_{n-1}, \xi_n), & v_n &= \beta_n v_{n-1} + (1-\beta_n)\nabla f(x_{n-1}, \xi_n)^{\odot 2},\\ r_n &= \alpha_n r_{n-1} + (1 - \alpha_n), & \bar r_n &= \beta_n \bar r_{n-1} + (1 - \beta_n),\\ x_n &= x_{n-1} - \gamma_n \frac{\hat m_n}{\varepsilon + \sqrt{\hat v_n}}, & \hat m_n &= m_n / r_n,\quad \hat v_n = v_n / \bar r_n . \end{aligned}$$

The divisions by $r_n$, $\bar r_n$ are the bias correction.

The stepsizes satisfy Assumption 5.1: $\gamma_{n+1}/\gamma_n \to 1$, $\sum_n \gamma_n = +\infty$, $\sum_n \gamma_n^2 < +\infty$, and there are $a, b$ with $0 < b < 4a$, $(1-\alpha_n)/\gamma_n \to a$ and $(1-\beta_n)/\gamma_n \to b$. The limiting dynamics is the autonomous ODE $\dot z = h_\infty(z)$ on $\mathcal Z_+ = \mathbb R^d \times \mathbb R^d \times [0,\infty)^d$, written $(\mathrm{ODE}_\infty)$, with

$$h_\infty(x, m, v) = \Big( -\frac{m}{\varepsilon + \sqrt v},\ a(\nabla F(x) - m),\ b(S(x) - v) \Big).$$

Formalization targets

Goal: Theorem 5.2

Assume Assumption 2.2 (regularity and moments of $f$), $F$ coercive (2.3), $S(x) > 0$ coordinatewise (2.4), iid samples (4.1), Assumption 5.1, $\sup_{x\in K}\mathbb E\|\nabla f(x,\xi)\|^4 < \infty$ on compacts (4.2 i) with $p = 4$), that $F(\mathcal S)$ has empty interior, and that $(x_n, m_n, v_n)$ is bounded with probability one. Then, almost surely,

$$d(x_n, \mathcal S) \to 0, \qquad m_n \to 0, \qquad S(x_n) - v_n \to 0,$$

and if $\mathcal S$ is countable, almost surely $(x_n, m_n, v_n) \to (x^*, 0, S(x^*))$ for some $x^* \in \mathcal S$.

Milestones

1. Lemma 9.1 i)–ii): $r_n = 1 - \prod_{i=1}^n \alpha_i$, and $r_n$ increases to $1$.
2. §9.1: in the decomposition $\bar z_{n+1} = \bar z_n + \gamma_{n+1} h_\infty(\bar z_n) + \gamma_{n+1}\chi_{n+1} + \gamma_{n+1}\varsigma_{n+1}$ of $\bar z_n = (x_{n-1}, m_n, v_n)$, the remainder satisfies $\varsigma_n \to 0$ almost surely.
3. §9.1: the piecewise-affine interpolation of $(\bar z_n)$ on the times $\tau_n = \sum_{k\le n}\gamma_k$ is almost surely a bounded asymptotic pseudotrajectory of the semiflow of $(\mathrm{ODE}_\infty)$.
4. Proposition 7.13: $(\mathrm{ODE}_\infty)$ is well posed on $\mathcal Z_+$ and defines a semiflow $\Phi$.
5. Proposition 7.14 (after Benaïm): the limit set of a relatively compact asymptotic pseudotrajectory of a semiflow with a strict Lyapunov function lies in the set of equilibria.
6. Proposition 7.15: on the closed hull of the orbits of a compact set, $W_\delta = V_\infty - \delta\langle\nabla F(x), m\rangle + \delta\|S(x) - v\|^2$ is a strict Lyapunov function for some $\delta > 0$.

Significance

The theorem identifies a regime of Adam's hyperparameters, $1 - \alpha_n \sim a\gamma_n$ and $1 - \beta_n \sim b\gamma_n$ with $b < 4a$, in which the algorithm behaves like a gradient method with vanishing noise: the iterates approach critical points, the momentum dies out, and the second-moment estimate converges to $S(x_n)$. The condition $b < 4a$ ties the two averaging rates together. It is the condition under which the paper's Lyapunov function for the continuous dynamics decreases (Lemma 7.5). The argument structure is also a template for other adaptive methods: once the limiting ODE has a strict Lyapunov function, almost-sure convergence of the iterates follows from the same steps.

The paper proves the result on paper; none of it is machine-checked. A formal proof would also be the first formal instance on Prove2Me of the full ODE method for a concrete stochastic algorithm. That pipeline runs from the iterates to a perturbed Euler scheme, then to an asymptotic pseudotrajectory and a limit-set theorem, and finally to convergence. Benaïm's general results are being formalized separately on the platform (the asymptotic-pseudotrajectory definition this mission reuses comes from that effort), so the two developments meet in milestone 3.

Difficulty

The obvious approach is to treat Adam as stochastic gradient descent with a preconditioner and run a descent-lemma argument on $F(x_n)$. This fails because the update direction $\hat m_n/(\varepsilon + \sqrt{\hat v_n})$ is not a descent direction for $F$: $m_n$ lags behind $\nabla F(x_n)$. Any Lyapunov function has to involve the momentum, and $F$ alone does not decrease. The continuous-time energy $V_\infty$ decreases only weakly, and only its perturbation $W_\delta$ is strict, and only on compact sets. A second difficulty is that the stepsize-dependent coefficients $(1-\alpha_{n+1})/\gamma_{n+1}$ and the bias corrections $r_n$, $\bar r_n$ make the recursion a non-autonomous perturbation of the Euler scheme of $h_\infty$. The remainder must be shown to vanish along almost every path before the general theory applies. Finally, the abstract limit-set theorem needs the semiflow to be well defined on the closed set $\mathcal Z_+$, where $h_\infty$ involves $\sqrt v$ and is not Lipschitz at $v = 0$.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The state space $\mathcal Z$ is the product of three copies with Mathlib's max-of-factors norm, which is equivalent to the Euclidean norm of $\mathbb R^{3d}$ and leaves boundedness and limits unchanged. $F$ and $S$ are Bochner integrals against the law $\mu$. Assumption 2.2 makes the integrands integrable, so they are the true expectations. Moments are lower Lebesgue integrals. Algorithm 5.1 is a pathwise recursion adamIter, driven by a random sequence $\xi : \mathbb N \to \Omega \to \Xi$ whose index $0$ is unused. The iid hypothesis is iIndepFun with every $\xi_{n+1}$ of law $\mu$.

Two hypotheses are left implicit on the page and are added explicitly. The first is $\varepsilon > 0$. The second is $\alpha_1 < 1$ and $\beta_1 < 1$: Assumption 5.1 iii) permits $\alpha_1 = 1$, which gives $r_1 = 0$, and Lean's division by zero returns $0$. Lemma 9.1 is stated with $\gamma_n > 0$ and $\sum\gamma_n = \infty$, which its convergence claim needs. Semiflows are Flow ℝ≥0 on the subtype $\mathcal Z_+$, and the asymptotic pseudotrajectory and limit set are the published StochApproxDyn.LimitSet definitions. The ODE milestones 4–6 hold for abstract $F$, $S$ under Assumptions 7.1–7.2 with $0 < b \le 4a$, as in the paper's §7.

The goal concerns the iterates of Algorithm 5.1 itself. A statement about trajectories of $(\mathrm{ODE}_\infty)$, or one that replaces almost-sure boundedness by a bound uniform in $\omega$ together with deterministic gradients, is a different and much weaker theorem and is ruled out. The interior condition on $F(\mathcal S)$ and the countability of $\mathcal S$ enter exactly as on the page.

A complete development needs the following:

• well-posedness of the ODE on a closed set with a non-Lipschitz field;
• the Benaïm machinery: martingale-noise control via Doob's convergence theorem, and the passage from vanishing perturbations to asymptotic pseudotrajectories;
• the limit-set theorem for strict Lyapunov functions.

The last two are reusable for any stochastic approximation scheme, and contributions to them are welcome independently of Adam.

Selected references

• A. Barakat, P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• D. P. Kingma, J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
• S. J. Reddi, S. Kale, S. Kumar, On the Convergence of Adam and Beyond, ICLR 2018. https://arxiv.org/abs/1904.09237