Convex Optimization

Motivation

In distributed optimization, $m$ agents connected by a communication network jointly minimize the average of their private losses, exchanging vectors only with their neighbours. This is the computational model of decentralized machine learning (data held by many machines, no central server), of sensor networks and of multi-agent control. A central family of methods is gradient tracking: each agent keeps, besides its copy of the decision variable, an estimate of the network-wide average gradient, refreshed by mixing with neighbours. Gradient tracking removes the steady-state bias of plain decentralized gradient descent and, for smooth strongly convex problems, converges linearly (Nedić, Olshevsky & Shi 2017; Qu & Li 2018).

Sun, Daneshmand and Scutari (arXiv:1905.02637v2, SIAM J. Optim. 2022) study SONATA, a gradient-tracking scheme in which each agent replaces its loss by a strongly convex surrogate and solves a small local problem per round. The setting is broader than earlier linear-rate results in three ways: the problem may be composite (a convex, possibly nonsmooth regularizer $G$), constrained (a closed convex set $\mathcal K$), and only the average loss needs to be strongly convex, not each local loss. Linearizing surrogates recover proximal gradient tracking; surrogates that keep the full local loss recover DANE- and CEASE-type methods, whose rates improve when the local losses are similar.

Setting

Agents $i=1,\dots,m$ hold functions $f_i:\mathbb R^d\to\mathbb R$. With $F=\frac1m\sum_if_i$, Problem (P) is

$$\min_{\mathbf x\in\mathcal K}\ U(\mathbf x)=F(\mathbf x)+G(\mathbf x).$$

Assumption A: $\mathcal K$ is nonempty, closed and convex; each $f_i$ is twice differentiable on an open set $\mathcal O\supseteq\mathcal K$ and convex; $\mu\mathbf I\preceq\nabla^2F(\mathbf x)\preceq L\mathbf I$ on $\mathcal K$ with $\mu>0$; $G$ is convex on $\mathcal K$. Then $\mu_i\mathbf I\preceq\nabla^2f_i\preceq L_i\mathbf I$ on $\mathcal K$ for some constants (display (1)), and $L_{\rm mx}=\max_iL_i$.

The network is a connected undirected graph $\mathcal G$ on the agents (Assumption B) and a doubly stochastic weight matrix $\mathbf W=(w_{ij})$ with $w_{ii}>0$, $w_{ij}>0$ on edges and $w_{ij}=0$ off edges (Assumption D). Its mixing rate is $\rho=\sigma(\widehat{\mathbf W}-\mathbf J)$, the largest singular value of $\mathbf W-\frac1m\mathbf 1\mathbf 1^\top$ (tensored with $\mathbf I_d$).

Each agent has a surrogate $\tilde f_i(\mathbf x;\mathbf z)$, $C^2$ on $\mathcal O\times\mathcal O$, whose gradient in $\mathbf x$ matches $\nabla f_i$ at $\mathbf x=\mathbf z$, is $\tilde L_i$-Lipschitz, and which is $\tilde\mu_i$-strongly convex in $\mathbf x$ (Assumption C). Display (15) supplies constants with $D_i^\ell\mathbf I\preceq\nabla^2\tilde f_i(\mathbf x,\mathbf y)-\nabla^2F(\mathbf x)\preceq D_i^u\mathbf I$ on $\mathcal K\times\mathcal K$; $D_i=\max\{|D_i^\ell|,|D_i^u|\}$, $\tilde\mu_{\rm mn}=\min_i\tilde\mu_i$, $D^\ell_{\rm mn}=\min_iD_i^\ell$, $D_{\rm mx}=\max_iD_i$.

SONATA (Algorithm 1) with step size $\alpha\in(0,1]$ starts from $\mathbf x_i^0\in\mathcal K$, $\mathbf y_i^0=\nabla f_i(\mathbf x_i^0)$ and repeats

$$\hat{\mathbf x}_i^\nu\in\operatorname*{argmin}_{\mathbf x_i\in\mathcal K}\tilde f_i(\mathbf x_i;\mathbf x_i^\nu)+(\mathbf y_i^\nu-\nabla f_i(\mathbf x_i^\nu))^\top(\mathbf x_i-\mathbf x_i^\nu)+G(\mathbf x_i),\qquad \mathbf x_i^{\nu+1/2}=\mathbf x_i^\nu+\alpha(\hat{\mathbf x}_i^\nu-\mathbf x_i^\nu),$$ $$\mathbf x_i^{\nu+1}=\sum_jw_{ij}\mathbf x_j^{\nu+1/2},\qquad \mathbf y_i^{\nu+1}=\sum_jw_{ij}\big(\mathbf y_j^\nu+\nabla f_j(\mathbf x_j^{\nu+1})-\nabla f_j(\mathbf x_j^\nu)\big).$$

With $\mathbf x^\star$ the optimal solution, the analysis tracks the optimality gap $p^\nu=\sum_i(U(\mathbf x_i^\nu)-U(\mathbf x^\star))$, the consensus errors $\mathbf x_\perp^\nu$, $\mathbf y_\perp^\nu$ (deviations from the network averages), the tracking error $\boldsymbol\delta_i^\nu=\nabla F(\mathbf x_i^\nu)-\mathbf y_i^\nu$ and the step $\mathbf d_i^\nu=\hat{\mathbf x}_i^\nu-\mathbf x_i^\nu$.

Formalization targets

Goal: Theorem 3.9

If $\tilde\mu_{\rm mn}\ge D^\ell_{\rm mn}$, there is $\bar\alpha\in(0,1]$ such that for every $\alpha\in(0,\bar\alpha)$, every SONATA run and every agent $i$,

$$\exists\,C,\ z\in[0,1):\qquad |U(\mathbf x_i^\nu)-U^\star|\le C\,z^\nu\quad\text{for all }\nu .$$

The goal fixes no rate: it asserts R-linear convergence for all small step sizes, which is the shape the paper proves. The explicit rate of Theorem 3.10 and the iteration counts of Corollaries 3.11–3.14 are not posed.

Milestones

In the order of the proof: the tracking invariant (19); Lemma 3.1 (per-agent descent); Lemma 3.2 (a lower bound on $\|\mathbf d^\nu\|^2$); Lemma 3.3 ($\|\boldsymbol\delta^\nu\|^2\le4L_{\rm mx}^2\|\mathbf x_\perp^\nu\|^2+2\|\mathbf y_\perp^\nu\|^2$); Proposition 3.4 ($p^{\nu+1}\le\sigma(\alpha)p^\nu+\eta(\alpha)(\cdots)$); Proposition 3.5 (consensus errors contract at rate $\rho$ up to $\|\mathbf d^\nu\|$); Proposition 3.6 ($\|\mathbf d^\nu\|^2$ bounded by $p^\nu$ and $\|\mathbf y_\perp^\nu\|^2$); Proposition 3.8 (the four inequalities (50a)–(50d) for the transformed sequences $S^K(z)=\max_{\nu\le K}|s^\nu|z^{-\nu}$); and (54), $D^K(z)\le\mathcal P(\alpha,z)D^K(z)+\mathcal R(\alpha,z)$.

Significance

Theorem 3.9 gives a linear rate for distributed composite, constrained optimization with gradient tracking, under strong convexity of the average loss only. It covers, through the choice of surrogate, proximal gradient tracking and the distributed versions of DANE and CEASE, and the constants $D_i$ quantify how much a surrogate gains when local losses are similar. The chain of Propositions 3.4–3.8 is a reusable template: an optimality-gap recursion, consensus recursions and a step bound, closed by a small-gain argument.

The result is proved in the paper; to our knowledge no part of it has been formalized. The mission produces a machine-checked statement of the model and of the full chain. Useful contributions include proofs of the individual milestones, a proof of the goal from the milestones, and the general facts they rest on.

Difficulty

The obvious argument fails in two places. First, the local step does not descend on $U$ by itself: the tracker $\mathbf y_i^\nu$ is not $\nabla F(\mathbf x_i^\nu)$, and the surrogate's curvature differs from $F$'s, so Lemma 3.1 must compare Hessians of $\tilde f_i$ and $F$ along a segment through (15), and the descent holds only up to the tracking error. Second, no single quantity contracts: $p^\nu$ contracts up to consensus errors, consensus errors contract up to $\|\mathbf d^\nu\|$, and $\|\mathbf d^\nu\|$ is bounded back by $p^\nu$. No Lyapunov function is given, and the loop gain $\mathcal P(\alpha,z)$ of (55) involves every constant of the problem, so showing it can be pushed below 1 for some $z<1$ is where the step-size threshold $\bar\alpha$ comes from. Also, $\rho<1$ is not an assumption: it must be derived from connectivity and Assumption D.

Formalization scope

Agents' vectors live in EuclideanSpace ℝ (Fin d), stacked vectors are Fin m → EuclideanSpace ℝ (Fin d), and their norm is always the Euclidean norm written out ($\sum_i\|\mathbf x_i\|^2$), never Lean's sup norm. Hessians are derivatives of gradients; Loewner bounds are quadratic-form inequalities. The surrogate's gradient and Hessian are in its first argument. $\rho$ is the operator norm of $\mathbf W-\frac1m\mathbf 1\mathbf 1^\top$ on Euclidean $\mathbb R^m$. Time is 0-based.

A SONATA run is a relation: $\hat{\mathbf x}_i^\nu$ is any minimizer of the local problem, and $\mathbf x^\star$ any minimizer of $U$ on $\mathcal K$. Assumption A gives no lower semicontinuity of $G$, so minimizers need not exist in general; the paper assumes they do, and so does the formalization, without adding a hypothesis on $G$. A sanity file exhibits instances of all assumptions and of runs (including a nonconstant one), so the run predicate is not empty. "$f_i$ convex" is read as convexity on $\mathcal K$ plus a positive semidefinite Hessian on $\mathcal O$; $G$ is convex on $\mathcal K$ only. The constants of (1) and (15) are parameters: each statement holds for every valid choice. All of Assumptions A–D are hypotheses of every statement (the paper's standing assumption of §3.3).

Trivializing formalizations are ruled out: $\rho<1$ is not assumed in place of Assumptions B and D; $\bar\alpha$ is chosen before the step size, the starting point and the run; $z<1$ is required; norms of stacked vectors are Euclidean. Two printed slips are handled openly: $\sigma(\alpha)\in(0,1)$ in Proposition 3.4 is stated with positivity only when $D_{\rm mx}>0$ or $\alpha<1$ (at $D_{\rm mx}=0$, $\alpha=1$ (41) gives $\sigma=0$), and $C_2=4/\tilde\mu_{\rm mn}^2$ is kept as printed in (52d) although (47) has 3. In Lemma 3.2, Lean's $\mu/0=0$ makes the bound trivial when $D_{\rm mx}=0$.

A full development needs: the mean-value and Taylor estimates for functions with bounded Hessian on a convex set, first-order optimality for constrained convex minimization, the spectral bound $\rho<1$ for graph-compliant doubly stochastic matrices (posed elsewhere on the platform as StochGradTrack.Const.lemma_1 for a closely related model), and elementary estimates on finite maxima. These are reusable beyond this mission.

Selected references

• Y. Sun, A. Daneshmand, G. Scutari, Distributed Optimization Based on Gradient-tracking Revisited: Enhancing Convergence Rate via Surrogation, arXiv:1905.02637v2, 2020; SIAM J. Optim. 32 (2022). https://arxiv.org/abs/1905.02637v2
• A. Nedić, A. Olshevsky, W. Shi, Achieving Geometric Convergence for Distributed Optimization over Time-Varying Graphs, SIAM J. Optim. 27 (2017). https://doi.org/10.1137/16M1084316
• G. Qu, N. Li, Harnessing Smoothness to Accelerate Distributed Optimization, IEEE Trans. Control Netw. Syst. 5 (2018). https://doi.org/10.1109/TCNS.2017.2698261
• P. Di Lorenzo, G. Scutari, NEXT: In-Network Nonconvex Optimization, IEEE Trans. Signal Inf. Process. Netw. 2 (2016). https://doi.org/10.1109/TSIPN.2016.2524588

Motivation

Nesterov's accelerated gradient method for smooth convex objectives, here called NAG-C, reaches function-value accuracy $O(L\|x_0-x^\star\|^2/k^2)$ after $k$ gradient evaluations, which is optimal among first-order methods (Nesterov 1983; Nesterov 2004). In many uses the quantity of interest is not the function gap but the squared gradient norm $\|\nabla f(x_k)\|^2$: it is computable without knowing the optimal value, it serves as a stopping criterion, and it controls duality gaps when the objective is a dual function. Combining the function-value rate with $L$-smoothness gives only $\|\nabla f(x_k)\|^2=O(L^2/k^2)$.

Shi, Du, Jordan and Su (arXiv:1810.08907) derived high-resolution ODEs for accelerated methods, keeping terms of order $\sqrt s$ that the earlier low-resolution limit of Su, Boyd and Candès (2016) discards. One of the discrete consequences is Theorem 6: unmodified NAG-C minimizes the squared gradient norm at the inverse cubic rate $O(L^2/k^3)$.

Timeline. Nesterov (1983) introduced the method and its $O(1/k^2)$ rate. Nesterov (2012) established an $\Omega(L^2/k^4)$ lower bound for the squared gradient norm and matched it up to a logarithmic factor with a regularized scheme built on the strongly convex variant of the method, which takes $\|x_0-x^\star\|$ as input. Ghadimi and Lan (2016) reached $O(L^2/k^3)$ with a modified accelerated method that adds a sequence of iterates and a larger step size. Attouch and Peypouquet (2016) proved $o(1/k^2)$ function values for a variant with momentum $(k-1)/(k+\alpha-1)$, $\alpha>3$. Shi, Du, Jordan and Su (arXiv 2018; Math. Program. 2021) proved the $O(L^2/k^3)$ rate for NAG-C itself, through a Lyapunov function suggested by the high-resolution ODE.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For $L>0$, the class $\mathcal F^1_L(\mathbb R^n)$ consists of the differentiable $f:\mathbb R^n\to\mathbb R$ with

$$f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle,\qquad \|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|\qquad(x,y\in\mathbb R^n).$$

A point $x^\star$ is a minimizer of $f$ when $f(x^\star)\le f(z)$ for every $z$.

Given a step size $s>0$ and an initial point $x_0$, NAG-C generates $y_0=x_0$ and, for $k\ge0$,

$$y_{k+1}=x_k-s\nabla f(x_k),\qquad x_{k+1}=y_{k+1}+\frac{k}{k+3}\,(y_{k+1}-y_k).$$

The velocity is $v_k=(x_{k+1}-x_k)/\sqrt s$, and the discrete Lyapunov function of the paper is

$$\mathcal E(k)=s(k+3)(k+1)\bigl(f(x_k)-f(x^\star)\bigr)+\tfrac12\bigl\|(k+1)\sqrt s\,v_k+2(x_{k+1}-x^\star)+(k+1)s\nabla f(x_k)\bigr\|^2 .$$

The last summand inside the norm, $(k+1)s\nabla f(x_k)$, is the gradient correction that the high-resolution ODE contributes and that the low-resolution analysis lacks.

Formalization targets

Goal: Theorem 6

For $f\in\mathcal F^1_L$, a minimizer $x^\star$, $0<s\le1/(3L)$ and every $k\ge0$,

$$\min_{0\le i\le k}\|\nabla f(x_i)\|^2\le\frac{8568\,\|x_0-x^\star\|^2}{s^2(k+1)^3} \qquad\text{and}\qquad f(x_k)-f(x^\star)\le\frac{119\,\|x_0-x^\star\|^2}{s(k+1)^2}.$$

The goal is the paper's theorem with its printed constants and both of its claims.

Milestones

In the paper's order of proof:

1. the phase-space form (4.5) of NAG-C, the identity (4.13), and the exact one-step change (4.14) of $\mathcal E$;
2. Lemma 4.3: $\mathcal E(k+1)-\mathcal E(k)\le-\tfrac{s^2}{2}\bigl((k+3)(k-1)-Ls(k+3)(k+1)\bigr)\|\nabla f(x_{k+1})\|^2$ for $k\ge0$;
3. the sign condition (4.7)–(4.8) for $k\ge2$, the sum identity $\sum_{i=3}^{k-1}[(i+3)(i-1)-\tfrac13(i+3)(i+1)]=(2k^3-38k+60)/9\ge(k+1)^3/36$, and (4.10);
4. the initial estimates of Appendix C.1: $\|\nabla f(x_k)\|^2$ for $k\le3$, $f(x_k)-f(x^\star)$ for $k\le1$, and $\mathcal E(3)\le\mathcal E(2)\le119\|x_0-x^\star\|^2$;
5. the rates (4.11) for $k\ge4$ and (4.12) for $k\ge2$.

Significance

The result. With $s=1/(3L)$, Theorem 6 gives $\min_{i\le k}\|\nabla f(x_i)\|^2=O(L^2\|x_0-x^\star\|^2/k^3)$ for the textbook method, with no restart, regularization or extra sequence. The rate is dimension-free and holds from the first iteration. It is a factor $k$ better than what the function-value rate gives, and it separates the high-resolution description of NAG-C from the low-resolution one: the paper explains the bound by the gradient correction in $\mathcal E$.

Formalizing it. The theorem is proved in the paper and, as far as the platform's catalogue shows, has no machine-checked proof. The mission produces a checked statement of NAG-C, its phase-space form and its Lyapunov function, which the other accelerated-method missions of this series (NAG-SC, the high-resolution ODEs) can mirror. Part of the paper's argument is a brute-force computation in Appendix C.1. A checked version would confirm the printed constants $8568$ and $119$; tighter constants or cleaner small-$k$ arguments are welcome as separate theorems.

Difficulty

The obvious route goes through the function-value rate $f(x_k)-f(x^\star)=O(1/k^2)$ and the smoothness inequality $\|\nabla f(x)\|^2\le2L(f(x)-f(x^\star))$. It stalls at $O(1/k^2)$ for the gradient, and no rearrangement of the classical estimate-sequence argument yields more. The extra factor of $k$ comes from a Lyapunov function whose one-step decrease is weighted by $k^2\|\nabla f(x_{k+1})\|^2$, and that decrease must be extracted exactly. The bookkeeping involves the $k$-dependent momentum $k/(k+3)$, the identity coupling $v_k$, $v_{k-1}$ and two gradients, and the cocoercivity of $\nabla f$. The sign of the decrease is lost for $k\le1$, so the first iterates need a separate argument with explicit constants.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $\nabla f$ is Mathlib's gradient. The class $\mathcal F^1_L$ is a structure in the paper's first-order form ($L>0$, differentiability, the convexity inequality, the Lipschitz gradient) and the velocity $v_k$ is defined once, both in the shared definitions HighResODE.NAGSC.FunctionClass and HighResODE.NAGSC.Setting; this mission's definition file, HighResODE.NAGC.Setting, holds NAG-C as a predicate on two sequences indexed from $k=0$ and $\mathcal E$. Conventions:

• The minimizer. $x^\star$ is a binder with the hypothesis that it minimizes $f$. The paper presupposes a minimizer for a merely convex $f$; this is the only hypothesis beyond the page's.
• Real arithmetic in $k$. The momentum $k/(k+3)$ and the factor $k-1$ of Lemma 4.3 are real numbers. A natural-number quotient would turn NAG-C into gradient descent, and a natural-number subtraction would change Lemma 4.3 at $k=0$.
• Index shifts. Identities the page states for $k\ge1$ with index $k-1$ are stated at $k+1$ for every $k\ge0$.
• Minima. $\min_{0\le i\le k}$ and $\min_{4\le i\le k}$ are finite minima (Finset.inf'), never a real infimum that could collapse to $0$.
• The whole theorem. The goal is the conjunction of both claims of Theorem 6, for every $k\ge0$, with the printed constants. Dropping the function-value claim, restricting to $k\ge4$, or a degenerate momentum would each give a weaker, different statement.

Milestones (4.5), (4.13) and (4.14) assume only $s>0$ and the NAG-C recursion, which is stronger than the page. The remaining items carry the hypotheses of Theorem 6 or, for pure arithmetic, none beyond $L,s>0$. Needed infrastructure: elementary inner-product algebra, the cocoercivity inequality $f(y)-f(x)\le\langle\nabla f(y),y-x\rangle-\tfrac1{2L}\|\nabla f(y)-\nabla f(x)\|^2$ for $f\in\mathcal F^1_L$, which is reusable for any smooth convex method, and finite telescoping sums.

Selected references

• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, arXiv:1810.08907v3, 2018; Math. Program. (2021). https://arxiv.org/abs/1810.08907v3, https://doi.org/10.1007/s10107-021-01681-8
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27(2):372–376 (1983). No DOI; cited as [Nes83] in arXiv:1810.08907v3, p. 36.
• Y. Nesterov, Introductory Lectures on Convex Optimization, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Y. Nesterov, How to make the gradients small, Optima 88:10–11 (2012). https://www.mathopt.org/Optima-Issues/optima88.pdf
• S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Math. Program. 156:59–99 (2016). https://doi.org/10.1007/s10107-015-0871-8
• H. Attouch, J. Peypouquet, The rate of convergence of Nesterov's accelerated forward-backward method is actually faster than 1/k², SIAM J. Optim. 26(3):1824–1834 (2016). https://doi.org/10.1137/15M1046095
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method, J. Mach. Learn. Res. 17 (2016). https://jmlr.org/papers/v17/15-084.html

Motivation

Nesterov's accelerated gradient method is the standard example of a first-order method that is provably faster than gradient descent. On a $\mu$-strongly convex function with $L$-Lipschitz gradient, gradient descent reduces the objective gap by a factor $1-O(\mu/L)$ per step, while the accelerated method achieves $1-O(\sqrt{\mu/L})$, the best possible rate for first-order methods (Nesterov, 2004/2013). The classical proof uses the estimate sequence technique, which certifies the rate but does not explain where the acceleration comes from.

Shi, Du, Jordan and Su (arXiv:1810.08907, published in Mathematical Programming, 2021) propose an explanation through high-resolution ordinary differential equations: continuous-time limits of the algorithms that keep terms of order $\sqrt s$ in the step size $s$. The heavy-ball method and Nesterov's method have the same low-resolution limit but different high-resolution limits; the extra term, a gradient correction $\sqrt s\,\nabla^2 f(X)\dot X$, is what separates the two. From the high-resolution ODE of Nesterov's method the authors derive a discrete Lyapunov function and use it to give, in their words, the first Lyapunov-function-based proof of the accelerated linear rate of Nesterov's method for strongly convex functions. This mission formalizes that discrete result, Theorem 3 of the paper.

Timeline:

• 1964: Polyak introduces the heavy-ball method, with local accelerated convergence.
• 1983: Nesterov introduces the accelerated gradient method, with global accelerated rates.
• 2004/2013: Nesterov's textbook proves the rate $f(x_k)-f(x^\star)=O((1-\sqrt{\mu/L})^k)$ for NAG-SC with $s=1/L$ by estimate sequences.
• 2014–2016: Su, Boyd and Candès derive the low-resolution ODE limit of Nesterov's method for convex functions; Wilson, Recht and Jordan give Lyapunov analyses in continuous and discrete time.
• 2018: Shi, Du, Jordan and Su introduce high-resolution ODEs and prove Theorem 3 with an explicit Lyapunov function.

Setting

Let $\|\cdot\|$ be the Euclidean norm on $\mathbb R^n$ and $\langle\cdot,\cdot\rangle$ the inner product. For $L>0$, the class $\mathcal F^1_L(\mathbb R^n)$ consists of differentiable functions $f$ with $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle$ for all $x,y$ (convexity) and $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ (an $L$-Lipschitz gradient). For $0<\mu\le L$, the class $\mathcal S^1_{\mu,L}(\mathbb R^n)$ consists of those $f\in\mathcal F^1_L$ with

$$f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\mu2\|y-x\|^2\qquad\text{for all }x,y.$$

Such an $f$ has a unique minimizer $x^\star$.

NAG-SC with step size $s>0$ starts from any $x_0=y_0\in\mathbb R^n$ and iterates

$$y_{k+1}=x_k-s\nabla f(x_k),\qquad x_{k+1}=y_{k+1}+\frac{1-\sqrt{\mu s}}{1+\sqrt{\mu s}}\,(y_{k+1}-y_k),\qquad k\ge0.$$

The velocity is $v_k=(x_{k+1}-x_k)/\sqrt s$, and the discrete Lyapunov function of the paper is

$$\mathcal E(k)=\frac{1+\sqrt{\mu s}}{1-\sqrt{\mu s}}\big(f(x_k)-f(x^\star)\big)+\frac14\|v_k\|^2+\frac14\Big\|v_k+\frac{2\sqrt\mu}{1-\sqrt{\mu s}}(x_{k+1}-x^\star)+\sqrt s\,\nabla f(x_k)\Big\|^2-\frac{s\|\nabla f(x_k)\|^2}{2(1-\sqrt{\mu s})}.$$

In Lean these are IsF1, IsS1, IsNAGSC, vel and lyap in the namespace HighResODE.NAGSC.

Formalization targets

Goal: Theorem 3 (p. 16)

For $f\in\mathcal S^1_{\mu,L}(\mathbb R^n)$ and step size $s=1/(4L)$, the iterates of NAG-SC satisfy, for every $k\ge0$,

$$f(x_k)-f(x^\star)\le\frac{5L\|x_0-x^\star\|^2}{\big(1+\frac1{12}\sqrt{\mu/L}\big)^k}.$$

The statement mentions only $f$, $x^\star$, the iterates and the constants; the Lyapunov function does not appear in it.

Milestones, in the order of the proof

1. (2.5), p. 11: the phase-space representation of NAG-SC in terms of $x_k$ and $v_k$, and the initial velocity $v_0=-2\sqrt s\,\nabla f(x_0)/(1+\sqrt{\mu s})$.
2. (3.15), p. 19: an upper bound on $\mathcal E(k)$ by $f(x_k)-f(x^\star)$, $\|v_k\|^2$, $\|x_k-x^\star\|^2$ and $f(x_k)-f(x^\star)-\frac s2\|\nabla f(x_k)\|^2$.
3. (B.2), p. 51: a bound on $\mathcal E(k+1)-\mathcal E(k)$ by $\langle\nabla f(x_{k+1}),x_{k+1}-x^\star\rangle$, $\|v_{k+1}\|^2$ and $\|\nabla f(x_{k+1})-\nabla f(x_k)\|^2$.
4. (3.16), pp. 19–20: the first-difference bound in the same quantities as (3.15), for $s\le1/(2L)$.
5. Lemma 3.4, p. 16: for $0<s\le1/(4L)$, $\mathcal E(k+1)-\mathcal E(k)\le-\frac{\sqrt{\mu s}}6\mathcal E(k+1)$.
6. (3.7), p. 16: at $s=1/(4L)$, $f(x_k)-f(x^\star)\le\frac{4(1-\sqrt{\mu/(4L)})}{3+4\sqrt{\mu/(4L)}}\mathcal E(k)$.
7. (3.8), p. 17: at $s=1/(4L)$, $\mathcal E(k)\le\mathcal E(0)/(1+\frac1{12}\sqrt{\mu/L})^k$.
8. (3.9), p. 17: $\mathcal E(0)\le[\cdots]\cdot L\|x_0-x^\star\|^2$ with the bracket printed on the page.

A further item, not a milestone, states that the resulting constant $C_{\mu/L}$ (p. 17) is less than five.

Significance

Theorem 3 recovers the optimal accelerated rate of NAG-SC, $\log(f(x_k)-f(x^\star))\le-\Omega(k\sqrt{\mu/L})$, with fully explicit constants: step size $1/(4L)$, rate $(1+\sqrt{\mu/L}/12)^{-1}$ and prefactor $5L\|x_0-x^\star\|^2$. The proof is a single Lyapunov inequality (Lemma 3.4) rather than an estimate sequence, and the same Lyapunov function, read in continuous time, explains acceleration through the gradient correction term. The heavy-ball method, which lacks this term, admits only a non-accelerated global rate under the same analysis.

The theorem is proved in the paper; nothing here is open. To our knowledge neither Theorem 3 nor its Lyapunov function has a machine-checked proof. The platform carries a formalization target for a different statement about Nesterov's method in the strongly convex case (Bubeck's Theorem 3.18, step $1/L$, rate $(1-1/\sqrt\kappa)^{t-1}$, constant $(\alpha+\beta)/2$), which is not this theorem. A completed mission yields a checked discrete Lyapunov proof of acceleration, with every inequality of the paper's proof as a separate reusable statement.

Difficulty

The obvious approach, unrolling the two-step recursion and bounding it as a linear system, works only for quadratics and loses the constants. The Lyapunov route avoids this, but its core step, the first-difference bound (B.2), is a long computation in the appendix (pp. 51–56): the cross terms coming from the momentum and from the gradient difference $\nabla f(x_{k+1})-\nabla f(x_k)$ must cancel exactly, and the small negative term of $\mathcal E$ exists only to make them cancel. Lemma 3.4 then needs the comparison of four coefficient pairs between (3.15) and (3.16), which holds only because $s\le1/(4L)$ forces $\sqrt{\mu s}\le1/2$. Finally, the inequality $C_{\mu/L}<5$ is an elementary but unpleasant one-variable estimate.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with $n$ arbitrary; $\nabla f$ is Mathlib's gradient f.
• The classes are structures stating the page's first-order inequalities; differentiability, $L>0$ and $0<\mu\le L$ are fields. Strong convexity is the page's inequality with $\|y-x\|^2$.
• The minimizer $x^\star$ is a binder with ∀ z, f xs ≤ f z; the stationarity $\nabla f(x^\star)=0$ is not assumed separately.
• NAG-SC is a predicate on the pair of sequences that fixes them from $x_0$ (with $y_0=x_0$), indexed from $k=0$. The goal holds for every $k\ge0$.
• The step size in the goal, (3.7) and (3.8) is exactly $1/(4L)$; Lemma 3.4, (3.15) and (B.2) assume $0<s\le1/(4L)$ (for (3.15) and (B.2) this is the standing range of the proof of Lemma 3.4); (3.16) assumes $0<s\le1/(2L)$ as printed; (2.5) and (3.9) assume $s>0$ and $\mu s<1$, which is all their formulas need.
• Square roots are Real.sqrt, with $\sqrt{\mu s}$ and $\sqrt{\mu/(4L)}$ written as on the page.

A formalization that let the NAG-SC predicate constrain only the $y$-update, dropped the Lipschitz-gradient bound from the class, or left the step size as a free parameter unrelated to $L$ would make the goal false or vacuous; the statements here do none of these.

A complete development needs the standard smoothness facts for $\mathcal F^1_L$ (the descent lemma, $\frac1{2L}\|\nabla f(x)\|^2\le f(x)-f(x^\star)$, co-coercivity), which are reusable well beyond this mission, followed by the algebra of (B.2). Contributions of proofs of individual milestones, in any order, are welcome.

Selected references

• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, arXiv:1810.08907v3, 2018; Mathematical Programming, 2021. https://arxiv.org/abs/1810.08907, https://doi.org/10.1007/s10107-021-01681-8
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27, 1983.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, Journal of Machine Learning Research 17, 2016. https://jmlr.org/papers/v17/15-084.html
• A. C. Wilson, B. Recht, M. I. Jordan, A Lyapunov Analysis of Accelerated Methods in Optimization, Journal of Machine Learning Research 22, 2021 (arXiv:1611.02635). https://arxiv.org/abs/1611.02635
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, Theorem 3.18. https://arxiv.org/abs/1405.4980

Motivation

Accelerated first-order methods, above all Nesterov's accelerated gradient (NAG) method, minimize a convex function with an $L$-Lipschitz gradient to accuracy $\varepsilon$ in $O(\sqrt{L/\varepsilon})$ gradient evaluations, and a $\mu$-strongly convex one in $O(\sqrt{L/\mu}\log(1/\varepsilon))$, against $O(L/\varepsilon)$ and $O((L/\mu)\log(1/\varepsilon))$ for gradient descent. Since Su, Boyd and Candès (arXiv:1503.01243) read Nesterov's method as a discretization of the ODE $x''+\frac3tx'+\nabla f(x)=0$, a line of work has tried to derive accelerated methods from continuous-time models with a Lyapunov function, e.g. Wibisono, Wilson and Jordan (arXiv:1603.04245) and Wilson, Recht and Jordan (arXiv:1611.02635).

Luo and Chen (arXiv:1909.03145, Math. Program. 2022) propose a single ODE, the NAG flow, that covers the convex case $\mu=0$ and the strongly convex case $\mu>0$ at once, through a time-dependent scaling factor $\gamma(t)$. Its Lyapunov function decays like $e^{-t}$ for every $\mu\ge0$. The rest of their paper discretizes this flow (implicit, predictor–corrector, gradient-corrected and semi-implicit schemes; missions 3–8 of this series) and transfers the decay to the discrete Lyapunov function. This mission formalizes the continuous result, Lemma 3.2 of the paper, on which those discretizations are modelled.

Setting

Let $V$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. A function $f:V\to\mathbb R$ is in the class $\mathcal S^1_\mu$ if it is continuously differentiable and, for some $\mu\ge0$,

$$f(x)-f(y)-\langle\nabla f(y),x-y\rangle\ \ge\ \frac{\mu}{2}\|x-y\|^2\qquad\forall\,x,y\in V,$$

the $\mu$-convexity of $f$ (strong convexity when $\mu>0$). It is in $\mathcal S^{1,1}_{\mu,L}$ if moreover $\nabla f$ is $L$-Lipschitz with $0<L<\infty$. A global minimizer $x^*$ of $f$ is assumed to exist.

The scaling factor solves $\gamma'=\mu-\gamma$, $\gamma(0)=\gamma_0>0$:

$$\gamma(t)=\mu+(\gamma_0-\mu)e^{-t},\qquad t\ge0 .$$

It is positive for all $t\ge0$ and tends to $\mu$; for $\mu=0$ it is $\gamma_0e^{-t}$.

The NAG flow is the first-order system

$$x'=v-x,\qquad \gamma v'=\mu(x-v)-\nabla f(x),\qquad x(0)=x_0,\ v(0)=v_0, \tag{56}$$

or, equivalently, the second-order equation

$$\gamma x''+(\mu+\gamma)x'+\nabla f(x)=0,\qquad x(0)=x_0,\ x'(0)=v_0-x_0. \tag{57}$$

Its Lyapunov function is

$$\mathcal L(t)=f(x(t))-f(x^*)+\frac{\gamma(t)}{2}\|v(t)-x^*\|^2,\qquad v=x+x'. \tag{58}$$

Formalization targets

Goal: Lemma 3.2 (p. 13)

If $f\in\mathcal S^{1,1}_{\mu,L}$ with $\mu\ge0$, then (57) has a unique solution $x\in C^2([0,\infty);V)$, and

$$\mathcal L'(t)\le-\mathcal L(t)-\frac{\mu}{2}\|x'(t)\|^2, \tag{59}$$ $$\mathcal L(t)+\frac{\mu}{2}\int_0^te^{s-t}\|x'(s)\|^2\,ds\le e^{-t}\mathcal L(0),\qquad t\ge0. \tag{60}$$

In particular $f(x(t))-f(x^*)\le e^{-t}\mathcal L(0)$ for all $\mu\ge0$, with no dependence on $L$ in the rate.

Milestones (pp. 12–14)

1. Lemma 3.1: $2(u-v,v-w)=\|u-w\|^2-\|u-v\|^2-\|v-w\|^2$.
2. (54): $\gamma(t)=\mu+(\gamma_0-\mu)e^{-t}$ is the solution of $\gamma'=\mu-\gamma$, $\gamma(0)=\gamma_0$, is positive, and tends to $\mu$ monotonically and exponentially.
3. Well-posedness of (56): a unique classical solution $(x,v)\in C^1([0,\infty);V)^2$.
4. (56) ⇔ (57): a $C^1$ solution of (56) gives a $C^2$ solution of (57), and conversely $(x,x+x')$ solves (56).
5. (61): along a solution of (56), $\mathcal L'=\langle\nabla f(x),x'\rangle+\frac{\mu-\gamma}{2}\|v-x^*\|^2+\langle\mu(x-v)-\nabla f(x),v-x^*\rangle$.
6. (63): $\mathcal L'=\frac{\mu}{2}\|x-x^*\|^2-\langle\nabla f(x),x-x^*\rangle-\frac{\gamma}{2}\|v-x^*\|^2-\frac{\mu}{2}\|x'\|^2$.
7. (59) along every solution of (56), for $f\in\mathcal S^1_\mu$.
8. Remark 3.1: with $\gamma'\le\mu-\gamma$ in place of (54), (59) still holds.

Significance

The lemma gives one continuous model whose energy decays at the rate $e^{-t}$ uniformly in $\mu\ge0$, without separate treatment of the convex and the strongly convex cases. The paper's discrete results (Theorems 4.1, 5.1, 5.2, 6.1, 7.2 and 7.3) prove the discrete counterpart $\mathcal L_{k+1}\le\mathcal L_k/(1+\alpha_k)$ by mimicking the computation (61)–(63) step by step, so the continuous identities are the template of the whole paper. The integral term in (60) also bounds $\int_0^te^{s-t}\|x'(s)\|^2ds$ when $\mu>0$.

The result is proved in the paper; nothing in this mission is open. To our knowledge neither the NAG flow nor its Lyapunov analysis has been formalized in Lean or another proof assistant. The mission produces a machine-checked well-posedness theorem for a non-autonomous ODE in a Hilbert space whose coefficient $1/\gamma(t)$ is unbounded on $[0,\infty)$ when $\mu=0$, and a machine-checked Lyapunov computation that later missions can mirror in discrete time.

Difficulty

The Lyapunov computation (61)–(63) is a direct, if careful, calculus exercise. The work lies elsewhere. Existence and uniqueness on the whole half-line $[0,\infty)$ do not follow from a single application of a local Picard–Lindelöf theorem: the vector field $(x,v)\mapsto\big(v-x,\ (\mu(x-v)-\nabla f(x))/\gamma(t)\big)$ is globally Lipschitz in $(x,v)$, but with a constant of order $1/\gamma(t)$, which grows like $e^{t}$ when $\mu=0$. A local existence theorem on a short interval does not by itself give a solution on $[0,\infty)$, and uniqueness must hold relative to $[0,\infty)$ with one-sided derivatives at $t=0$. Passing from the differential inequality (59) to (60) requires $\mathcal L$ to be differentiable relative to $[0,\infty)$, including the endpoint $t=0$, and the integrand $\|x'(s)\|^2$ to be continuous, so the regularity of the solution has to be carried through every step.

Formalization scope

• $V$ is a real Hilbert space (InnerProductSpace ℝ V, CompleteSpace V); the paper's duality pairing and dual norm are the inner product and the norm (Riesz).
• The gradient is an explicit map gradf with HasGradientAt f (gradf x) x for every $x$ and gradf continuous; Mathlib's gradient is not used. $\mathcal S^{1,1}_{\mu,L}$ includes $0\le\mu\le L$ and $0<L$.
• Time derivatives are relative to $[0,\infty)$ (derivWithin x (Ici 0)), so one-sided at $0$. Every curve differentiated this way is assumed $C^1$ or $C^2$ on $[0,\infty)$, so the junk value $0$ of derivWithin at a point of non-differentiability never enters.
• Uniqueness is equality on $[0,\infty)$; values at negative times are unconstrained.
• Standing assumptions made explicit: $V$ Hilbert, a global minimizer $x^*$ exists, $\gamma_0>0$. Remark 3.1 adds that its relaxed $\gamma$ is positive on $[0,\infty)$, which the paper takes for granted.
• $\mu=0$ is allowed throughout; no milestone assumes $\mu>0$. The Lipschitz hypothesis appears only where existence is claimed (milestone 3 and the goal); milestones 4–8 assume $f\in\mathcal S^1_\mu$ only.
• The goal is stated for the solution of (57), whose existence and uniqueness are part of the conclusion. The trivializing reading, "if a function satisfies $\mathcal L'\le-\mathcal L$ then $\mathcal L(t)\le e^{-t}\mathcal L(0)$", is Grönwall's inequality and is not the target.

A complete development needs: a global existence and uniqueness theorem for Lipschitz non-autonomous ODEs on $[0,\infty)$ with locally bounded Lipschitz constant (Mathlib's IsPicardLindelof and ODE_solution_unique_of_mem_Icc are the starting points), and one-sided calculus for $t\mapsto f(x(t))$ and $t\mapsto\|v(t)-x^*\|^2$. The global existence result for half-line ODEs is reusable well beyond this mission. Contributions are welcome on any milestone independently.

Selected references

• H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization, Mathematical Programming (2022); preprint arXiv:1909.03145v4. https://arxiv.org/abs/1909.03145
• W. Su, S. Boyd and E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, Journal of Machine Learning Research 17 (2016). https://arxiv.org/abs/1503.01243
• A. Wibisono, A. C. Wilson and M. I. Jordan, A variational perspective on accelerated methods in optimization, PNAS 113 (2016). https://arxiv.org/abs/1603.04245
• A. C. Wilson, B. Recht and M. I. Jordan, A Lyapunov analysis of accelerated methods in optimization, Journal of Machine Learning Research 22 (2021). https://arxiv.org/abs/1611.02635
• Y. Nesterov, Lectures on Convex Optimization, Springer, 2018. https://doi.org/10.1007/978-3-319-91578-4

Motivation

In a financial market with a single probability model, the Optional Decomposition Theorem describes the processes that can be dominated by trading. If a process $V$ is a supermartingale under every equivalent martingale measure, then it can be written as an initial value plus a stochastic integral against the stock price, minus an increasing process that represents consumption. El Karoui and Quenez proved it for diffusion models (SIAM J. Control Optim. 33 (1995)) and Kramkov for locally bounded semimartingales (Probab. Theory Related Fields 105 (1996)). It is the step that turns the superhedging price, a supremum of expectations over martingale measures, into an actual dynamic hedging strategy.

Model uncertainty replaces the single model by a set $\mathcal P$ of probability measures that may be mutually singular. This happens, for example, when volatility is only known to lie in an interval. There is then no reference measure, "almost surely" becomes "quasi surely" (outside a set that is null under every model), and the classical proofs, which rely on one dominating measure, do not apply. Bouchard and Nutz (Ann. Appl. Probab. 2015, arXiv:1305.6008) built the discrete-time theory of this setting: no-arbitrage, the fundamental theorem of asset pricing, superhedging duality and, in §6, a nondominated optional decomposition. This mission formalizes that last result.

Timeline:

• 1995: El Karoui and Quenez, optional decomposition in diffusion models.
• 1996: Kramkov, for locally bounded semimartingales.
• 2014: Nutz, superreplication duality under model uncertainty in discrete time (Finance Stoch. 18 (2014)).
• 2015: Bouchard and Nutz, the fundamental theorem, superhedging duality and the optional decomposition in nondominated discrete time (Theorem 6.1).

Setting

Fix a Polish space $\Omega_1$, a horizon $T \in \mathbb N$ and $d \in \mathbb N$. Let $\Omega_t := \Omega_1^t$ for $t = 0, \dots, T$. Then $\Omega_0$ is a single point and $\Omega := \Omega_T$, and a point of $\Omega_t$ is read as the first $t$ coordinates of a path. The $\sigma$-field $\mathcal F_t$ is the universal completion of $\mathcal B(\Omega_t)$.

For each $t < T$ and each node $\omega \in \Omega_t$ a nonempty convex set $\mathcal P_t(\omega)$ of probability measures on $\Omega_1$ is given, and its graph is an analytic set. The set of possible models $\mathcal P$ consists of all products $P_0 \otimes P_1 \otimes \cdots \otimes P_{T-1}$ whose kernels take values in $\mathcal P_t(\cdot)$. A set is $\mathcal P$-polar if it is null under every $P \in \mathcal P$. A property holds $\mathcal P$-quasi surely (q.s.) if it holds outside a polar set.

Stock prices $S_t : \Omega_t \to \mathbb R^d$ are Borel. A strategy $H \in \mathcal H$ is predictable: $H_u$ is a function of the first $u-1$ coordinates. The wealth at time $t$ is

$$H \bullet S_t = \sum_{u=1}^t H_u \Delta S_u, \qquad \Delta S_u = S_u - S_{u-1}.$$

NA($\mathcal P$) holds if $H \bullet S_T \ge 0$ q.s. implies $H \bullet S_T = 0$ q.s. A martingale measure is a probability $Q$ under which $S$ is a martingale. The set

$$\mathcal Q = \{Q \lll \mathcal P : Q \text{ is a martingale measure}\}$$

contains those $Q$ that are absolutely continuous with respect to some $P \in \mathcal P$ (written $Q \lll \mathcal P$). A function $f$ with values in $[-\infty, \infty]$ is upper semianalytic if every set $\{f > c\}$ is analytic.

At one node $\omega \in \Omega_t$, the increment $\Delta S_{t+1}(\omega, \cdot)$ defines a one-period market under $\mathcal P_t(\omega)$, with its own no-arbitrage condition NA($\mathcal P_t(\omega)$) and one-period martingale measures $\mathcal Q_t(\omega)$. The conditional sublinear expectation is

$$\mathcal E_t(f)(\omega) = \sup_{Q \in \mathcal Q_t(\omega)} E_Q[f(\omega, \cdot)].$$

Formalization targets

Goal: Theorem 6.1 (nondominated optional decomposition)

Let NA($\mathcal P$) hold and let $V$ be an adapted process such that $V_t$ is upper semianalytic and in $L^1(Q)$ for all $Q \in \mathcal Q$ and $t \in \{1, \dots, T\}$. Then the following are equivalent:

1. $V$ is a supermartingale under each $Q \in \mathcal Q$;
2. there exist $H \in \mathcal H$ and an adapted increasing process $K$ with $K_0 = 0$ such that

$$V_t = V_0 + H \bullet S_t - K_t \quad \mathcal P\text{-q.s.}, \qquad t = 0, 1, \dots, T.$$

Milestones

• Lemma 4.6: the set $N_t$ of nodes where NA($\mathcal P_t(\omega)$) fails is universally measurable, and it is polar under NA($\mathcal P$).
• Theorem 4.5: NA($\mathcal P$) holds if and only if every $N_t$ is polar, if and only if every $P \in \mathcal P$ is absolutely continuous with respect to some $Q \in \mathcal Q$.
• Lemma 4.10: $\mathcal E_t(f)$ is upper semianalytic, and there is a universally measurable $y$ with

$$\mathcal E_t(f)(\omega) + y(\omega)\,\Delta S_{t+1}(\omega, \cdot) \ge f(\omega, \cdot) \quad \mathcal P_t(\omega)\text{-q.s.}$$

at every arbitrage-free node where $f(\omega,\cdot) > -\infty$ q.s.

• (6.1): under condition 1 of the goal, $\mathcal E_t(V_{t+1}) \le V_t$ $\mathcal P$-q.s. for every $t < T$.

Significance

The decomposition is the dynamic counterpart of superhedging duality. Duality identifies the price $\sup_{Q} E_Q[f]$. The optional decomposition, applied to the process of conditional superhedging prices, produces one strategy that superhedges under all models at once and a nonnegative increasing process recording the surplus. The proof works in a nondominated model with one strategy $H$ that is measurable in the universal completion, and this is what makes the theorem usable under volatility or model uncertainty, where no single model can be singled out. The equivalence also characterizes the processes that are supermartingales under every $Q \in \mathcal Q$: up to a polar set they are exactly the wealth processes of strategies that consume.

The result is proved in the paper; no part of it has a machine-checked proof, on the platform or in Mathlib. Mathlib has martingales, conditional expectation and analytic sets. It has no quasi-sure analysis, no product of measurable selectors of a random set of measures, no conditional sublinear expectation and no superhedging. The mission produces a machine-checked development of the one-period-to-multi-period machinery of the paper (Theorem 4.5, Lemmas 4.6 and 4.10) and of the decomposition itself.

Difficulty

With one dominating measure, the classical proof works under a fixed equivalent martingale measure and uses conditional expectations and a single null-set structure. Here the measures in $\mathcal P$ may be mutually singular, so conditional expectations under different $Q$ disagree off their supports, and no countable family of measures controls all null sets. The proof has to work node by node, $\omega \mapsto \mathcal P_t(\omega)$. Every object built at a node (the worst-case conditional expectation, a near-optimal measure, a hedging ratio) must then be glued back together measurably in $\omega$. Borel measurability is not preserved by taking suprema over the random set $\mathcal Q_t(\omega)$. Upper semianalyticity is, but only together with measurable selection theorems for analytic sets (Jankov–von Neumann) and the universal completion. The first idea, which is to apply the classical theorem under each $P \in \mathcal P$ separately, fails. It gives one strategy per model, and in general uncountably many models cannot be aggregated into one strategy.

Formalization scope

The Lean development uses the following conventions.

• Paths and measures. $\Omega_t$ is Fin t → Ω₁, and measures are Borel. $\mathcal F_t$-measurability is universal measurability, which is the published platform definition BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable.
• Polar sets. A polar set is null in outer measure under every model. The exceptional sets in the statements are universally measurable, and for such sets this agrees with the paper's definition.
• The model set. $\mathcal P$ consists of the laws of Borel Markov kernels that lie in $\mathcal P_t$ almost surely, which is the paper's equivalent formulation on p. 4.
• Processes. A process is a family V t : (Fin t → Ω₁) → ℝ, so adaptedness is built into the type.
• Strategies. The Lean strategy H u is the paper's $H_{u+1}$.
• Expectations. Expectations of functions with values in $[-\infty, \infty]$ follow (1.1) in EReal, with $\infty - \infty = -\infty$. Suprema over $\mathcal Q_t(\omega)$ are taken in EReal.
• Options. The setting has no options ($e = 0$).
• Page numbers. Pages and indices are those of the arXiv v3 reprint (arXiv:1305.6008v3), not the journal pagination 823–859.

The increasing process $K$ must be adapted and nondecreasing on every path. Dropping monotonicity would make condition 2 trivially true, with $K := V_0 + H \bullet S - V$ for any $H$. Integrability and supermartingale properties are always stated with explicit $Q$-integrability, so Bochner integrals of non-integrable functions cannot make a statement vacuous.

The development needs the following infrastructure:

• analytic sets and measurable selection (some of it exists for Bertsekas–Shreve on the platform);
• measurability of $(\omega, Q) \mapsto E_Q[f(\omega,\cdot)]$;
• products of kernels;
• the one-period fundamental theorem and superhedging duality.

These pieces are shared with the companion mission Arbitrage and Duality in Nondominated Discrete-Time Models I, which formalizes the superhedging theorem. Contributions to either side are welcome. The paper derives (ii) ⇒ (i) from Lemma A.1, a classical fact about local and generalized martingales under one measure, which is not posed as a milestone here.

Selected references

• B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Ann. Appl. Probab. 25(2), 823–859, 2015. https://doi.org/10.1214/14-AAP1011, arXiv:1305.6008v3 https://arxiv.org/abs/1305.6008
• N. El Karoui, M.-C. Quenez, Dynamic programming and pricing of contingent claims in an incomplete market, SIAM J. Control Optim. 33, 29–66, 1995. MR1311659, https://mathscinet.ams.org/mathscinet-getitem?mr=1311659
• D. O. Kramkov, Optional decomposition of supermartingales and hedging contingent claims in incomplete security markets, Probab. Theory Related Fields 105, 459–479, 1996. MR1402653, https://mathscinet.ams.org/mathscinet-getitem?mr=1402653
• M. Nutz, Superreplication under model uncertainty in discrete time, Finance Stoch. 18, 791–803, 2014. MR3255751, https://mathscinet.ams.org/mathscinet-getitem?mr=3255751
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Mathematics in Science and Engineering 139, Academic Press, 1978. MR0511544, https://mathscinet.ams.org/mathscinet-getitem?mr=0511544