Convex Optimization

Motivation

A constraint $\mathbb E[v(x,\tilde z)] \le w$ on a decision $x$ requires the distribution of the random vector $\tilde z$. In practice that distribution is known only partially: its support, a few moments, or the probability mass of some regions estimated from data. Distributionally robust optimization asks that the constraint hold for every distribution consistent with this information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) proposed one standardized format for this information. Their format contains, as special cases, many ambiguity sets used earlier: support and moment information (Delage and Ye, 2010), and mean–covariance and directional-deviation information (Goh and Sim, 2010). They then characterized exactly when a worst-case expectation constraint over such a set has a finite conic reformulation. This mission formalizes that characterization: the paper's Theorem 1 and the steps of its proof.

Setting

The uncertain parameters are $\tilde z \in \mathbb R^P$, and an auxiliary random vector $\tilde u \in \mathbb R^Q$ may be added to describe structure of $\tilde z$. A proper cone $\mathcal K$ is a closed convex cone with $\mathcal K \cap(-\mathcal K) = \{0\}$ and nonempty interior. Write $x \preccurlyeq_{\mathcal K} y$ for $y - x \in \mathcal K$, and $\mathcal K^\star = \{y : x^\top y \ge 0\ \forall x \in \mathcal K\}$ for the dual cone. For indices $i \in \mathcal I = \{1,\dots,I\}$ the confidence sets are

$$\mathcal C_i = \{(z,u) : C_i z + D_i u \preccurlyeq_{\mathcal K_i} c_i\},$$

with matrices $C_i, D_i$, vectors $c_i$ and proper cones $\mathcal K_i$. The ambiguity set is

$$\mathcal P = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u) \in \mathcal C_i] \in [\underline p_i,\overline p_i]\ \ \forall i \in \mathcal I\Big\},$$

where $0 \le \underline p_i \le \overline p_i \le 1$. The paper imposes three conditions:

• (C1) $\mathcal C_I$ is bounded and $\underline p_I = \overline p_I = 1$;
• (C2) some $\mathbb P \in \mathcal P$ meets every non-degenerate probability bound strictly;
• (C3) the constraint function is a maximum of finitely many bi-affine pieces,

$$v(x,z) = \max_{l = 1,\dots,L} \big[(S_l z + s_l)^\top x + \mathbf t_l^\top z + t_l\big].$$

The distributionally robust constraint (3) is $\mathbb E_{\mathbb P}[v(x,\tilde z)] \le w$ for all $\mathbb P \in \mathcal P$.

A set $A$ is strictly included in $B$, written $A \Subset B$, if $A$ lies in the interior of $B$. The nesting condition (N) requires that any two distinct confidence sets be strictly nested or disjoint. For each $i$, $\mathcal A(i) = \{i\} \cup \{i' : \mathcal C_i \Subset \mathcal C_{i'}\}$ indexes the confidence sets containing $\mathcal C_i$.

Formalization targets

Goal: Theorem 1 (pp. 10–11)

Under (C1)–(C3), (N) and the two regularity conditions (S1)–(S2) described below, the constraint (3) holds if and only if there are $\beta \in \mathbb R^K$, $\kappa,\lambda \in \mathbb R^I_+$ and $\phi_{il} \in \mathcal K_i^\star$ such that, for all $i \in \mathcal I$ and $l$,

$$b^\top\beta + \sum_{i}\big[\overline p_i\kappa_i - \underline p_i\lambda_i\big] \le w,\qquad c_i^\top\phi_{il} + s_l^\top x + t_l \le \sum_{i' \in \mathcal A(i)}[\kappa_{i'} - \lambda_{i'}],$$ $$C_i^\top\phi_{il} + A^\top\beta = S_l^\top x + \mathbf t_l,\qquad D_i^\top\phi_{il} + B^\top\beta = 0.$$

Milestones

1. Theorem 1, sufficiency. The system implies (3), under (C1), (C3) and (N) alone.
2. Lemma 1 (p. 34). For a strictly feasible conic confidence set, the semi-infinite constraint $v(x,z) + f^\top z + g^\top u \le h$ on the set holds iff multipliers $\phi_l \in \mathcal K^\star$ exist with $c^\top\phi_l + s_l^\top x + t_l \le h$, $C^\top\phi_l = S_l^\top x + \mathbf t_l + f$ and $D^\top\phi_l = g$.
3. The dual of the moment problem (p. 35). Constraint (3) holds iff some $\beta$, $\kappa,\lambda \ge 0$ have objective value $\le w$ and satisfy $[Az+Bu]^\top\beta + \sum_i \mathbf 1_{\mathcal C_i}(z,u)[\kappa_i - \lambda_i] \ge v(x,z)$ on $\mathcal C_I$.
4. The partition step (p. 35). Under (N), the indicator constraint on $\mathcal C_I$ is equivalent to constraints with the constant $\sum_{\mathcal A(i)}$ on the pieces $\overline{\mathcal C}_i = \mathcal C_i \setminus \bigcup_{\mathcal C_{i'} \Subset \mathcal C_i} \mathcal C_{i'}$.
5. The boundary step (pp. 35–36). The $i$-th constraint holds on $\overline{\mathcal C}_i$ iff it holds on all of $\mathcal C_i$.

Significance

When the $\mathcal K_i$ are orthants, second-order cones or semidefinite cones, Theorem 1 turns the semi-infinite, measure-valued constraint (3) into a linear, conic-quadratic or semidefinite system of size polynomial in the data. The paper's Theorem 2 shows that when nesting fails, even checking $\mathcal P \neq \emptyset$ is strongly NP-hard. Theorem 1 is therefore the tractable side of a sharp dividing line. The paper builds its conservative approximation for non-nested sets (Theorem 3) and its lifting results (Section 3) on it.

The result is proved in the paper; nothing here is open. The formalization contributes two things. First, the duality theory for finite moment problems over measures on a compact set, and conic strong duality for strictly feasible sets: neither exists in Mathlib as stated. Second, a corrected statement. As printed, the "only if" direction of Theorem 1 is false, because (C2) does not give the strong duality the proof attributes to it. No machine-checked version of Theorem 1 is known.

Difficulty

The sufficiency half is weak duality: a pointwise inequality on $\mathcal C_I$ integrated against any $\mathbb P \in \mathcal P$. The necessity half needs three facts.

• Strong duality, with attainment, for an infinite-dimensional linear program over nonnegative measures. Here the obvious reference to a general conic duality theorem needs a constraint qualification on all moment constraints jointly, and (C2) controls only the probability bounds.
• A geometric step: under (N), a constraint imposed on $\overline{\mathcal C}_i$ extends to all of $\mathcal C_i$. This uses convexity of $v$ in $(z,u)$ together with the compactness of $\mathcal C_i$ and the strict inclusion of its descendants.
• Conic duality with dual attainment for each confidence set (Lemma 1), which fails without strict feasibility.

Formalization scope

Vectors are Fin n → ℝ, products are Matrix.mulVec and dotProduct, and the outcome space is (Fin nP → ℝ) × (Fin nQ → ℝ) with its Borel $\sigma$-algebra. The index set is Fin (nI + 1), 0-based, with $\mathcal C_I$ = Fin.last nI. Probabilities are μ.real. Constraint (3) is stated in its "for all $\mathbb P$" form, so no supremum of reals appears. The scalar $t_l$ and the vector $\mathbf t_l$ are separate fields.

Every member of $\mathcal P$ is a probability measure with finite first moment, so $\mathbb E_{\mathbb P}[A\tilde z + B\tilde u]$ is a genuine integral and not Lean's default value $0$. The expectation $\mathbb E_{\mathbb P}[v(x,\tilde z)]$ is genuine as well, since $v$ grows at most linearly. Hypothesis (C2) keeps $\mathcal P$ nonempty, so (3) cannot hold vacuously. A sorry-free sanity file exhibits two nested intervals for which all hypotheses of the goal hold at once.

Hypotheses added to the paper's, each needed for a true statement:

• (S1) moment-problem regularity. Every small common shift of $b$ and of each probability interval stays feasible over finite measures on $\mathcal C_I$. It is needed because with $\mathcal C_1$ the unit disk, $\mathbb E[\tilde z_1] = 1$, $v = z_2$ and $w = 0$, constraint (3) holds but the system has no solution.
• (S2) strict feasibility of every confidence set. It is needed because a confidence set that is a single boundary point of a second-order cone constraint admits no dual multipliers in Lemma 1.
• $\mathcal C_i \subseteq \mathcal C_I$ and $P + Q \ge 1$ in the partition and boundary steps. In dimension zero a set is strictly included in itself and $\overline{\mathcal C}_i$ can be empty.

(S1) also excludes some instances the page allows: $\overline p_i = 0$ or $\underline p_i = 1$ for $i \ne I$, and expectation rows that cannot be shifted in every direction by measures on $\mathcal C_I$.

The sufficiency milestone drops (C2) and the standing bounds $0 \le \underline p_i \le \overline p_i \le 1$, which only strengthens it.

Needed infrastructure, all reusable: conic duality for closed convex cones, Lagrangian duality for linear programs over finite measures on a compact set, and the extension of a convex inequality from the boundary of a compact set. Contributions of any of these as separate lemmas are welcome.

Selected references

• W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757, version of September 22, 2013. https://optimization-online.org/wp-content/uploads/2013/02/3757.pdf ; Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, chapter 7, Kluwer, 2001 (reference [56] of the paper; the result the proof of Theorem 1 cites as Proposition 3.4).
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• J. Goh, M. Sim, Distributionally robust optimization and its tractable approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0712
• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

Why this ODE needs a well-posedness theorem

Nesterov’s accelerated gradient method is a discrete procedure for minimizing a smooth convex function. Its iterates use both a gradient step and a momentum term, so the position at the next step depends on recent motion as well as on the current gradient. Su, Boyd, and Candès study a continuous-time model of that behavior: a trajectory whose acceleration is driven by the negative gradient and opposed by a time-dependent damping term. The model is useful only if its prescribed starting point determines an actual trajectory. The first theorem of the paper supplies that guarantee for the damping coefficient $3/t$. Su, Boyd, and Candès, 2015, Theorem 1.

The coefficient $3/t$ is undefined at the stated initial time $t=0$. Standard results for differential equations with a continuous right-hand side at the initial time therefore cannot be applied directly. The existence and uniqueness claim is substantive: it makes the trajectory used in the paper’s later rate and restart theorems a defined mathematical object, including its behavior at the singular endpoint. The source proves the result; this mission asks for a machine-checked formalization of its statement and its supporting appendix lemmas.

The setting

Fix a dimension $n$, a starting point $x_0\in\mathbb R^n$, and a real-valued objective $f$. For a constant $L>0$, the paper’s class $\mathcal F_L$ consists of functions that are convex, continuously differentiable, and have an $L$-Lipschitz gradient:

$$\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\| \qquad\text{for all }x,y\in\mathbb R^n.$$

The larger class $\mathcal F_\infty$ is the union of these classes over positive $L$. In particular, the objective need not be strongly convex and need not have a minimizer for this mission.

A solution is a position $X:[0,\infty)\to\mathbb R^n$ and its velocity $V=\dot X$, starting at $X(0)=x_0$ and $V(0)=0$, that satisfy equation (3) at every positive time:

$$\dot V(t)+\frac{3}{t}V(t)+\nabla f(X(t))=0,\qquad t>0.$$

The trajectory is continuously differentiable through the initial endpoint, with a right derivative there, and twice continuously differentiable for $t>0$. The paper also uses a smoothed equation indexed by $\delta>0$, replacing $3/t$ with $3/\max(\delta,t)$. Its solutions are denoted $X_\delta$, and its velocity-growth quantity is

$$M_\delta(t)=\sup_{0<u\le t}\frac{\|\dot X_\delta(u)\|}{u}.$$

For local uniqueness, two solutions $X,Y$ on $[0,a)$ are compared using $\widetilde M(t)=\sup_{0\le u<t}\|\dot X(u)-\dot Y(u)\|$. These quantities appear in the appendix lemmas and are represented by pointwise bounds in the formal statements.

Formalization targets

The goal is Theorem 1, the well-posedness of equation (3). For every $f\in\mathcal F_\infty$ and every $x_0$, it asserts both existence of a global trajectory with the regularity above and uniqueness on nonnegative time:

$$\exists X\ \text{solving (3) from }(x_0,0), \qquad X,Y\ \text{both solve (3) from }(x_0,0) \Longrightarrow X(t)=Y(t)\quad(t\ge0).$$

The milestone list follows the numbered statements in Appendix A. Lemma 16 controls the change in $\nabla f$ along a smoothed trajectory. Lemmas 15 and 17 bound $M_\delta$ on the initial smoothing interval and beyond it, with the explicit thresholds $\delta<\sqrt{6/L}$ and $t<\sqrt{12/L}$. Lemma 18 states that the family of smoothed trajectories with $\delta=\sqrt{3/L}/2^m$ is uniformly bounded and equicontinuous on $[0,\sqrt{6/L}]$. Lemma 14 gives existence for equation (3). Lemma 20 bounds the difference between gradients along two local solutions, and Lemma 19 gives uniqueness in a neighborhood of zero. The goal and milestones preserve the source’s domains, constants, and order of dependence.

What the result provides

Theorem 1 permits the rest of the paper to refer to “the” trajectory of equation (3) from a specified initial point. In particular, statements about its objective value, energy, and restarts need an actual trajectory, and uniqueness makes those statements independent of a choice of solution. The appendix estimates also provide reusable facts about this singular second-order equation: quantitative control of smoothed velocities and local agreement at the singular time.

The paper proves Theorem 1 and the seven listed lemmas on pp. 6 and 28–32. This mission does not claim a new analytical result. Its output would be checked Lean statements and, when solvers finish the proofs, a machine-checked development of the singular initial-value problem. The formal definitions are shared by all items in this mission; the lemmas can be reused in later formal work on accelerated gradient trajectories. No machine-checked proof of these particular statements is being claimed by the draft proposal.

The central difficulty

The initial time is precisely where the damping $3/t$ has no finite value. Treating the problem as an ordinary initial-value problem at $t=0$ leaves the differential equation undefined there. Imposing the equation at $t=0$ after Lean’s total division would instead change it: Lean assigns a value to division by zero, while the paper imposes equation (3) only for $t>0$. The demanded derivative at zero is one-sided, and control of the behavior as $t\downarrow0$ is part of the result.

The smoothed equations are regular at zero, but a statement about each smoothed trajectory does not by itself give a solution of the original singular equation. The appendix’s uniform bounds and equicontinuity are formulated on a common compact interval for a specified sequence of smoothing parameters. Uniqueness has a second boundary issue: local agreement near zero must be connected to ordinary uniqueness at positive time to obtain agreement for every $t\ge0$.

Formalization scope

The Lean space is $\mathrm{EuclideanSpace}\ \mathbb R\ (\mathrm{Fin}\ n)$, with its Euclidean norm; $n$ is arbitrary. The objective class includes convexity, $C^1$ regularity, a positive Lipschitz constant, and a globally Lipschitz gradient. A solution is encoded as a pair $(X,V)$, so $V=\dot X$ is witnessed by derivative assertions rather than by a total derivative operator. The initial conditions specify $X(0)=x_0$, $V(0)=0$, a right derivative of $X$, and right continuity of $V$. The differential equation and ordinary derivatives are required only at positive times. For the smoothed equation, $\delta>0$ is part of the solution predicate.

These choices rule out a vacuous solution predicate and prevent division by zero from defining a different equation. Lean functions are represented on all real times, but the source’s solution lives on $[0,\infty)$; uniqueness is therefore equality on that half-line. At negative times the formal representatives are unrestricted. The paper’s real suprema $M_\delta$ and $\widetilde M$ are expressed as bounds on every member of their defining ranges, so an empty or unbounded real supremum cannot acquire a misleading default value. Every denominator in Lemmas 15 and 17 has the paper’s strict threshold in its hypotheses.

A full proof development needs ordinary differential equation existence and uniqueness at positive time, continuity and derivative facts at the right endpoint, and compactness of uniformly bounded equicontinuous families. The definitions of the objective class and solution predicates, the quantitative estimates, and the local uniqueness statement are welcome solver contributions. The target is the source theorem with its stated hypotheses and conclusion; a special objective, a weakened time interval, or a proof by an impossible hypothesis does not close it.

Selected references

• Weijie Su, Stephen Boyd, and Emmanuel J. Candès, A Differential Equation for Modeling Nesterov’s Accelerated Gradient Method: Theory and Insights, arXiv:1503.01243v2, 2015; published in Journal of Machine Learning Research 17(153), 2016. Preprint.

Why parameter-free regret matters

In online convex optimization, a learner makes a prediction before seeing the next loss. A standard regret guarantee often depends on a learning rate chosen using the size of the comparator that will be assessed later. That comparator is unknown during play. Chapter 13 of Orabona's textbook uses coin betting to obtain a bound that adapts to every comparator while the algorithm uses only its initial wealth and a bound on the observed subgradients. The coordinate-wise form allows the guarantee to reflect a comparator whose important coordinates differ greatly in size.

The motivating task is deterministic. An adversary may choose convex losses over successive rounds, and the performance measure compares the learner's cumulative loss with the loss of a single fixed vector. The algorithm is allowed to know the coordinate bound $L_\infty$ and its initial wealth parameter $\varepsilon$; it does not know the final comparator $u$ or a suitable learning rate for it. The capstone is Theorem 13.9, p. 215, the chapter's coordinate-wise Krichevsky–Trofimov result.

The learner and the betting rule

There are $T$ rounds, numbered $1,\ldots,T$, in a space $\mathbb R^d$. In round $t$ the learner outputs $x_t$, pays $\ell_t(x_t)$, and then receives a subgradient $g_t$ of the loss at $x_t$. A subgradient supports the loss everywhere: $\ell_t(y)\ge\ell_t(x_t)+\langle g_t,y-x_t\rangle$ for every $y\in\mathbb R^d$. Each coordinate obeys $|g_{t,i}|\le L_\infty$. For a fixed comparator $u$, regret is

$$\operatorname{Regret}_T(u)=\sum_{t=1}^T\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

The underlying KT bettor begins with wealth $\varepsilon>0$. Given coin outcomes $c_t\in[-1,1]$, it wagers a fraction $\beta_t=(\sum_{j=1}^{t-1}c_j)/t$ of its wealth before outcome $c_t$ arrives. Its signed wager is $b_t=\beta_t\operatorname{Wealth}_{t-1}$, and $\operatorname{Wealth}_t=\operatorname{Wealth}_{t-1}+c_tb_t$. The denominator is $t$, including the first round, when the past sum and the wager are zero. Algorithm 13.1, p. 208 defines this update.

For optimization, Algorithm 13.3, p. 215 applies a separate KT update to every coordinate. With $L_\infty>0$, the prediction is fixed by past gradients and past predictions:

$$x_{t,i}=-\frac{\sum_{j=1}^{t-1}g_{j,i}}{L_\infty t} \left(\varepsilon-\sum_{j=1}^{t-1}\frac{g_{j,i}}{L_\infty}x_{j,i}\right).$$

This is the algorithm studied in the target theorem. A run includes the update and an admissible subgradient at each round; it is not an arbitrary sequence of predictions satisfying a bound after the fact.

Formalization targets

The main target records both inequalities in Theorem 13.9. For every comparator $u\in\mathbb R^d$,

$$\operatorname{Regret}_T(u) \le L_\infty\sum_{i=1}^d |u_i|\sqrt{2T\ln\left(1+\frac{e|u_i|T}{\varepsilon}\right)}+d\varepsilon L_\infty \le \|u\|_1L_\infty\sqrt{2T\ln\left(1+\frac{e\|u\|_\infty T}{\varepsilon}\right)}+d\varepsilon L_\infty.$$

The milestone path consists of three statements drawn directly from the chapter: the gamma-potential one-step inequality (13.1), the continuous-coin wealth guarantee of Theorem 13.4, and the one-dimensional KT regret display in §13.2.1. The first controls the change in the betting potential, the second relates that potential to final wealth, and the third is the scalar guarantee used by the coordinate-wise theorem. All three retain the printed constants and the source's one-based indexing.

What the theorem gives

The first inequality charges each comparator coordinate according to its own magnitude. The second expresses the result using familiar $\ell_1$ and $\ell_\infty$ norms. Both apply to the same run without choosing a new algorithm for a new $u$. At $u=0$, the bound is $d\varepsilon L_\infty$, showing directly the cost of the initial-wealth choice. For a sparse or uneven comparator, the coordinate sum can be more informative than a bound that uses only the largest coordinate.

The mathematical results are proved in the cited textbook. This mission supplies Lean statements for those results; the theorem files are proof targets and do not yet contain machine-checked proofs. A completed development would connect the betting potential, the one-dimensional optimization reduction, and the coordinate aggregation through reusable lemmas. Its definition layer can also serve later formalizations of coin-betting algorithms with other wealth potentials.

Where the difficulty lies

The prediction uses a changing wager fraction determined by the previous outcomes. A direct fixed-fraction calculation does not describe that sequence of wagers. The chapter instead identifies a gamma-function potential that can be compared with the changing wealth at every round. For continuous coin outcomes, the potential must satisfy an inequality for every real $c\in[-1,1]$, including interior values rather than only the binary endpoints.

The optimization guarantee adds another boundary: a lower bound on betting wealth must become an upper bound on regret for every real comparator. The desired expression has a logarithm, a square root, and the exact factor $e$ inside it. The coordinate-wise result must preserve the scalar constant in every coordinate and then justify the second inequality involving $\|u\|_\infty$. These are the places where a weaker or altered constant would change the target.

Formalization scope

Lean represents $\mathbb R^d$ as functions Fin d → ℝ; its function norm is the sup norm, while the $\ell_1$ quantity is the explicit sum $\sum_i|u_i|$. The theorem assumes $d\ge1$, $T\ge1$, $\varepsilon>0$, and $L_\infty>0$. These make the finite-dimensional setting nonempty and the printed quotients and logarithms operate on their intended domains. Time index zero is unused. All sums over rounds use $1,\ldots,T$.

Losses are real-valued and subdifferentiable on the whole space, as in Algorithm 13.3. The run records full-space subgradients selected at the learner's predictions and their coordinate bounds. This selected-gradient condition is sufficient for the printed regret inequalities; global boundedness of every possible subgradient is a stronger convention used in the one-dimensional prose. The gamma potential is a separate definition with Real.Gamma; its arguments are positive on the domains used by the wealth theorem. The bettor's wealth is a finite product of its exact per-round returns.

The formalization must keep the explicit update in the run predicate. Allowing $x_t$ to depend on the current $g_t$, or replacing the update by a generic betting rule, would no longer state Algorithm 13.3's guarantee. Contributions are welcome on the gamma-potential inequality, the wealth bound, the one-dimensional regret bound, and the final coordinate aggregation. The supporting results should retain the chapter's constants and handle the first round and zero-valued coin outcomes.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv.

Motivation

Online prediction compares the losses of a sequence of decisions with the losses of one fixed decision chosen after the sequence is known. A learner would like a regret guarantee that remains valid for every such competitor, even when the losses arrive in an arbitrary order. Exponentially weighted averaging is a way to make each decision from all feasible points rather than committing to one candidate early. The method gives the Weighted Average Algorithm (WAA) in Chapter 11 of Orabona's text. It is particularly effective when the exponential of each negative loss is concave, a condition called exp-concavity.

The chapter first compares WAA with a competing probability distribution. Theorem 11.5 turns that guarantee into a bound against an individual feasible point. That distinction matters when the benchmark is a concrete portfolio, parameter vector, or other fixed decision, rather than a distribution over decisions. The same chapter later extends the weighted-average viewpoint to mixable losses through the Aggregating Algorithm; this mission focuses on the earlier deterministic-comparator result.

Setting

The feasible set $V$ is a closed, bounded, convex, full-dimensional subset of $\mathbb R^d$, with $d\geq1$. Its uniform distribution assigns a measurable subset probability equal to its Euclidean volume divided by $\operatorname{Vol}(V)$. Because $V$ is bounded and full-dimensional, its volume is finite and positive. Rounds are $t=1,\ldots,T$, with $T\geq1$. In round $t$, the learner predicts $x_t$, then observes a loss $\ell_t$ and pays $\ell_t(x_t)$. A competitor $u\in V$ is fixed across all rounds. Its regret is

$$R_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

For a parameter $\alpha>0$, a real-valued loss $\ell_t$ is $\alpha$-exp-concave on $V$ if $x\mapsto e^{-\alpha\ell_t(x)}$ is concave on $V$. Definition 7.31 in the source also permits a loss value of $+\infty$, with $e^{-\alpha(+\infty)}=0$. The mission defines that extended-valued concept for Proposition 7.34 and uses real-valued losses in its WAA target. The weighted average in round $t$ is

$$x_t=\frac{\int_V x\,\exp\!\left(-\alpha\sum_{s=1}^{t-1}\ell_s(x)\right)\,dx}{\int_V\exp\!\left(-\alpha\sum_{s=1}^{t-1}\ell_s(x)\right)\,dx}.$$

Thus $x_1$ is the centroid of $V$. This formula is Algorithm 11.1 with the uniform initial distribution and $1/\lambda_t=\alpha$. The existing published EWOO point definition uses precisely this one-based formula, so the mission imports that object. The integrals are with respect to Euclidean Lebesgue measure.

Formalization targets

The main target is Theorem 11.5, equation (11.6): for every $u\in V$,

$$R_T(u)\leq\frac d\alpha\left(1+\ln\left(\frac Td+1\right)\right).$$

The target fixes the exact dimension, horizon, and exp-concavity dependence from the source. It applies to each fixed competitor, with no distribution chosen in the statement. The milestone list records three source claims in reading order. Proposition 7.34 says that exp-concavity implies convexity, including the book's extended-real convention. Two displays in the proof of Theorem 11.5 describe the translated, contracted set $V'=\{\frac{T/d}{T/d+1}u+\frac{1}{T/d+1}w:w\in V\}$: the exponential losses there are bounded against those at $u$, and its uniform-prior mass is $1/(T/d+1)^d$. These are the chapter's explicit geometric and loss-comparison targets.

Significance

The theorem converts a distributional WAA guarantee into a bound for each deterministic competitor. Its dimension factor is $d$, and its logarithm contains $T/d+1$. This exact expression is sharper than replacing that logarithm by $\ln(T+1)$ for $d>1$; the distinction is visible in the target statement. A related EWOO result with the weaker $(d/\alpha)(1+\ln(T+1))$ form is already represented in the platform's library, but it does not establish the bound selected here. The source theorem is proved in the book; the remaining work is a machine-checked proof of this statement and the geometric milestones, with the source's constants intact.

The formal development can also support later results on exponentially weighted prediction. Its reusable pieces are the definition of exp-concavity, the extended-real epigraph convention, and the volume identity for a translated scaling of a convex body. The WAA prediction itself is represented by a previously published definition, giving future results a common algorithmic object rather than another copy of the same integral formula.

Difficulty

The general WAA statement compares the algorithm with a probability distribution, whereas Theorem 11.5 compares it with a point $u$. A point mass at $u$ is unsuitable as a comparator to a uniform continuous prior: it has no density with respect to that prior, so its relative entropy is infinite. The finite bound depends on identifying a region around $u$ that has positive uniform mass while retaining control of every exp-concave loss on that region. A formal treatment must also ensure that the weighted vector integral denotes an actual mean and that the normalization denominator is positive, rather than inheriting a default value from a total integral or division operator.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d), and a loss is indexed from round one; index zero is unused. The prior is uniform on $V$, and the point played is the published one-based EWOO weighted mean. The hypotheses $d,T\geq1$ make the printed ratios meaningful. Closedness, boundedness, convexity, and positive volume express the source's full-dimensional convex-body setting. The theorem additionally records almost-everywhere measurability of each loss on $V$, and integrability of each exponential weight and its vector moment; these are explicit analytic conditions for the real and Bochner integrals in Lean. They are not algorithmic restrictions or assumptions of the regret inequality's conclusion. Positive volume and integrability rule out a vacuous zero denominator or Lean's zero value for a non-integrable integral.

The source allows extended-real losses, but the goal uses real-valued losses on $V$. Proposition 7.34 separately retains the full extended-real statement through WithTop ℝ: $+\infty$ maps to zero under the exponential, and convexity is expressed by a convex epigraph. A complete proof needs the exp-concavity and Jensen facts, the weighted-mean properties on convex $V$, the measure and volume properties of $V'$, and the distributional WAA inequality from the chapter. Contributions that supply these lemmas under the stated conventions are within scope. The prediction cannot be replaced by an arbitrary point of $V$: the exact uniform-prior weighted mean is part of the goal.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. Chapter 11 and Proposition 7.34.

Motivation

An online learning algorithm chooses a decision before seeing each round's data and is judged by regret: how much more loss it incurs than a fixed decision chosen in hindsight. Statistical learning asks a different question. After seeing data drawn from a distribution, how small is the decision's expected loss on another draw? Chapter 3 of Orabona's textbook connects these settings. It shows that a deterministic online rule with a pathwise regret guarantee also controls expected loss when its input data are independent samples. The chapter's high-probability result is the target here.

The distinction matters when an online guarantee is already available. A regret theorem holds for every loss sequence, including adversarial sequences, yet it does not by itself state what a learner achieves on future data from a distribution. The conversion supplies that statistical reading. It applies to the sequence of predictions produced along one sample path, with no need to select an empirical-risk minimizer from the full decision set. Chapter 3 also studies finite-set validation, in which a separate sample selects one candidate from a fixed collection Orabona, Chapter 3.

Setting

The decision set $V$ is a subset of Euclidean space $\mathbb R^d$. A data point $z$ belongs to a measurable space $D$ and is drawn according to a probability distribution $\rho$. The loss $f(x,z)$ lies in $[0,1]$ for every $x\in V$ and $z\in D$, and is measurable as a function of $z$ when $x$ is fixed. Its true risk is $F(x)=\mathbb E_{z\sim\rho}[f(x,z)]$. For a sample $\xi_1,\ldots,\xi_T$ drawn independently from $\rho$, round $t$ presents the loss function $\ell_t(x)=f(x,\xi_t)$.

A deterministic online algorithm produces predictions $x_1,\ldots,x_{T+1}$ in $V$. Its prediction $x_t$ uses only $\xi_1,\ldots,\xi_{t-1}$. For a fixed competitor $u\in V$, its regret is $\operatorname{Regret}_T(u)=\sum_{t=1}^T\ell_t(x_t)-\sum_{t=1}^T\ell_t(u)$. A proposed regret bound $R(u,T)$ is required to hold on every sample path and for every competitor $u$. The risk comparison uses a minimizer of the full expression $F(u)+R(u,T)/T$, whose existence the theorem assumes.

Formalization targets

The goal is Theorem 3.10, with $T\ge1$ and $0<\delta<1$:

$$\mathbb P\!\left\{\frac1T\sum_{t=1}^T F(x_t) \le \min_{u\in V}\left(F(u)+\frac{R(u,T)}{T}\right) +2\sqrt{\frac{2\ln(2/\delta)}{T}}\right\}\ge1-\delta.$$

The minimum includes both risk and normalized regret. The theorem controls the average risk of the produced predictions; it does not require $F$ to be convex or claim the risk of their average decision. This makes the result applicable to decision sets and losses beyond the convex setting of the chapter's expectation result.

The first milestone is the two-sided bounded-martingale inequality of Theorem 3.9. A second milestone is the displayed concentration estimate in the proof of Theorem 3.10, which compares average true risk with average observed loss for the adaptive predictions. The final milestone is Theorem 3.17: if a fixed nonempty finite set $S\subseteq V$ is evaluated on fresh data and $\widehat x$ minimizes its empirical risk, then

$$F(\widehat x)\le\min_{x\in S}F(x) +2\sqrt{\frac{2\ln(2|S|/\delta)}{T}}$$

with probability at least $1-\delta$ Orabona, pp. 27–32.

Significance

The goal gives a direct way to read an online regret certificate as a distributional risk certificate. The bound retains the competitor-dependent function $R(u,T)$ inside the minimization: a decision with slightly larger risk but substantially smaller regret bound may give the better guarantee. Its deviation term has the exact constant and confidence dependence stated in the textbook. The finite-set theorem supplies a distinct validation guarantee for choosing one candidate from a fixed collection; it applies even when the risk is not convex.

Formalizing these results adds the probability layer absent from a deterministic regret statement: independent samples, a prediction rule constrained by past observations, true risk as an integral, and probability events for the adaptive sequence. Related online-to-batch statements already exist in the platform's developments of Hazan's online convex optimization text and Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning. They use different algorithm and loss models and do not state this competitor-dependent bound. The present mission records the precise Chapter 3 formulation as an open formal proof target; the local Lean statements compile, but their proofs are not supplied.

Difficulty

The observed loss $f(x_t,\xi_t)$ uses a prediction chosen from earlier observations, while the event in the goal concerns its expected loss $F(x_t)$. Treating the predictions as fixed would ignore their dependence on the sample history. Allowing a prediction to inspect the current sample would break the comparison. The required concentration statement therefore has to retain the exact information available at each round. The comparator in the final bound is fixed before the samples are observed, while the online predictions remain sample dependent Orabona, proof of Theorem 3.10.

For the finite-set result, the selected predictor depends on the validation sample. A concentration estimate for a single fixed predictor does not immediately give the asserted guarantee for that selected predictor. The finite set must remain fixed before sampling, and the statement must account for every possible selected member.

Formalization scope

The Lean decision space is EuclideanSpace ℝ (Fin d). Samples are functions $\mathbb N\to D$ under the infinite product measure of $\rho$; their values at index zero are unused. The algorithm is a function of the full sample path constrained by a non-anticipation predicate: changing samples from round $t$ onward cannot change $x_t$. Regret is against a fixed $u$, with sums over rounds $1,\ldots,T$. The pathwise regret guarantee quantifies over every sample path, so it cannot be replaced by an expected-regret assumption.

The integral defining $F$ is used with the book's measurable $[0,1]$ losses on $V$, avoiding an undefined-integral convention. Measurability of each prediction, realized loss, and realized risk is stated explicitly where a probability event uses them. These regularity conditions make the probability statements meaningful and are the only extra conditions beyond the textbook's mathematical setup. A minimizer $u_\star\in V$ represents the assumed minimum in Theorem 3.10. The finite-set minimum is a real infimum whose input is nonempty, finite, and bounded. The positive horizon guards division by $T$; $0<\delta<1$ guards the logarithms. In Theorem 3.9, $B>0$ and $\varepsilon\ge0$ make its printed tail formula valid, including at the threshold boundary.

A complete development needs Mathlib's infinite product measure, filtration and martingale interfaces, conditional expectation or conditional moment bounds, and the sub-Gaussian concentration library. The risk, regret, non-anticipation, and empirical-risk definitions can be reused for later stochastic learning results. Contributions that establish the concentration milestone, connect it to the regret identity, or prove the finite-set validation statement all fit this scope.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv
• Elad Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016; revised arXiv version, 2019. arXiv

Motivation

Many problems in statistical learning and signal processing take the form of minimizing an expectation $f(x)=\mathbb E_\xi[F(x,\xi)]$ plus a regularizer or constraint $r(x)$, where the only access to $f$ is through samples $\xi\sim P$. The classical tool is the stochastic (proximal) subgradient method, which replaces $f$ at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss $F(\cdot,\xi)$, and the stochastic prox-linear method linearizes only the smooth inner part of a composite loss $h(c(x,\xi))$. In experiments the richer models are markedly less sensitive to the choice of step size.

Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization, in which each step minimizes a sampled one-sided model $f_{x_t}(\cdot,\xi_t)$ of $f$ plus $r$ plus a quadratic penalty. Their main theorem (Theorem 4.3) covers weakly convex problems through the Moreau envelope. This mission formalizes the companion result for the convex setting, Theorem 4.1: when the models lower-bound $f$ in expectation without quadratic error and $f_x(\cdot,\xi)+r$ is convex, the expected function gap at a weighted average of the iterates decays like $1/\sqrt T$. As the paper notes (p. 22), for the stochastic proximal subgradient method this improves earlier bounds (Cruz 2017; Duchi–Singer 2009) because no subgradient norm of $r$ enters the estimate.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. The problem is

$$\min_{x\in\mathbb R^d}\ \varphi(x):=f(x)+r(x),$$

where $f:\mathbb R^d\to\mathbb R$ is locally Lipschitz and $r:\mathbb R^d\to\mathbb R\cup\{+\infty\}$ is closed (its epigraph is closed) with nonempty domain $D=\operatorname{dom}r$. A function $\psi$ is $\rho$-weakly convex if $x\mapsto\psi(x)+\frac\rho2\|x\|^2$ is convex; $\rho=0$ is ordinary convexity.

Assumption B (p. 18) fixes a probability space $(\Omega,\mathcal F,P)$, an open convex set $U\supseteq D$, real constants $\tau,\eta,\mathsf L$, a measurable model $(x,y,\xi)\mapsto f_x(y,\xi)$ on $U\times U\times\Omega$ and a measurable $L:\Omega\to\mathbb R_+$ such that:

1. (B1) i.i.d. samples $\xi_0,\xi_1,\dots\sim P$ can be drawn;
2. (B2) $\mathbb E_\xi[f_x(x,\xi)]=f(x)$ and $\mathbb E_\xi[f_x(y,\xi)-f(y)]\le\frac\tau2\|y-x\|^2$ for $x,y\in U$;
3. (B3) $f_x(\cdot,\xi)+r$ is $\eta$-weakly convex for every $x\in U$ and almost every $\xi$;
4. (B4) $\sqrt{\mathbb E[L(\xi)^2]}\le\mathsf L$ and $f_x(x,\xi)-f_x(y,\xi)\le L(\xi)\|x-y\|$ for $x,y\in U$ and almost every $\xi$.

Algorithm 4.1 (p. 19) starts at $x_0$ and, for $t=0,\dots,T$, samples $\xi_t\sim P$ and sets

$$x_{t+1}=\operatorname*{argmin}_{x}\Big\{r(x)+f_{x_t}(x,\xi_t)+\frac{\beta_t}{2}\|x-x_t\|^2\Big\}.$$

The convex setting is $\tau=0$ and $\eta=0$. Write $\alpha_t=\beta_t^{-1}>0$ for the step sizes and let $x^*$ be any minimizer of $\varphi$.

Formalization targets

Goal: Theorem 4.1, (4.17) and (4.18)

For every $T>0$,

$$\mathbb E\Big[\varphi\Big(\tfrac{1}{\sum_{t=0}^T\alpha_t}\textstyle\sum_{t=0}^T\alpha_t x_{t+1}\Big)-\varphi(x^*)\Big]\le\frac{\frac12\|x_0-x^*\|^2+2\mathsf L^2\sum_{t=0}^T\alpha_t^2}{\sum_{t=0}^T\alpha_t},$$

and with the constant step $\alpha_t=\gamma/\sqrt{T+1}$, $\gamma>0$,

$$\mathbb E\Big[\varphi\Big(\tfrac{1}{T+1}\textstyle\sum_{t=1}^{T+1}x_t\Big)-\varphi(x^*)\Big]\le\frac{\frac12\|x_0-x^*\|^2+2\mathsf L^2\gamma^2}{\gamma\sqrt{T+1}}.$$

The factor $2$ in front of $\mathsf L^2$ is the constant the paper's proof establishes; see Formalization scope.

Milestones

1. Lemma 4.1: $\varphi$ is $(\tau+\eta)$-weakly convex and $|f(x)-f(y)|\le\mathsf L\|x-y\|$ on $U$.
2. Lemma 4.2, (4.8): for every $x\in\operatorname{dom}r$, with $x_t$ fixed and $\mathbb E_t$ the expectation over $\xi_t$,

$$\mathbb E_t\|x_{t+1}-x\|^2\le\frac{\beta_t+\tau}{\beta_t-\eta}\|x_t-x\|^2-\frac{2}{\beta_t-\eta}\mathbb E_t[\varphi(x_{t+1})-\varphi(x)]+\frac{4\mathsf L^2}{\beta_t(\beta_t-\eta)}.$$

3. Proof of Theorem 4.1, first display (p. 23): $2\alpha_t\mathbb E[\varphi(x_{t+1})-\varphi(x^*)]\le\mathbb E\|x_t-x^*\|^2-\mathbb E\|x_{t+1}-x^*\|^2+4\mathsf L^2\alpha_t^2$.

Significance

Theorem 4.1 is the function-value guarantee of the model-based framework. Theorem 4.3 measures progress by the gradient of the Moreau envelope, which is the right quantity for nonconvex problems but says nothing directly about suboptimality; under convexity, Theorem 4.1 gives the familiar $O(1/\sqrt T)$ rate for the gap itself. It applies to the stochastic proximal point and prox-linear methods as well as to the proximal subgradient method, and §4.2 of the paper uses it for minimizing an expectation of a pointwise maximum of convex functions, such as the conditional value-at-risk. The estimate (4.8) behind it is also the engine of the strongly convex rate $O(1/(\mu T))$ (Theorem 4.2, a separate mission of this series).

The result is proved in the paper; nothing in it is open. To our knowledge none of these statements has a machine-checked proof. The formalization contributes a checked version of the one-step estimate (4.8) with its corrected constant, a reusable Lean encoding of Assumption B and of Algorithm 4.1 with extended-valued $r$, and the passage from conditional one-step bounds to expectations over the product measure of the samples.

Difficulty

The argument is short on paper; the work lies in the measure theory the paper leaves implicit. The iterate $x_{t+1}$ is an argmin that depends on $x_t$ and on the fresh sample $\xi_t$, and the one-step estimate holds only conditionally, with $x_t$ frozen. Turning it into an inequality between unconditional expectations requires measurability of the iterates, independence of $\xi_t$ from the past, and integrability of $\varphi(x_{t+1})$ and $\|x_{t+1}-x^*\|^2$, which the paper takes for granted. The convex function $\varphi$ is extended-valued, so the function gap is meaningful only because every iterate and every average lies in $\operatorname{dom}r$.

A naive one-step argument that bounds $f(x_t)-f(x_{t+1})$ and $f_{x_t}(x_t,\xi_t)-f_{x_t}(x_{t+1},\xi_t)$ separately, each by a Lipschitz constant times $\|x_{t+1}-x_t\|$, gives the constant $4\mathsf L^2$ in (4.8) and not the printed $2\mathsf L^2$. The printed constant is false (see below), so the constant cannot be improved simply by tightening that one step.

Formalization scope

• Space and encoding. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The extended-valued $r$ is a real function together with its domain D; closedness of $r$ is closedness of $\{(x,t):x\in D,\ r(x)\le t\}$, and convexity is ConvexOn ℝ D. $\mathsf L$ is L and $L(\xi)$ is Lfun.
• Randomness. The $T+1$ samples are a point of $\Omega^{T+1}$ under the product measure $P^{\otimes(T+1)}$; expectations are Bochner integrals. Every theorem that bounds an expectation also concludes integrability of the integrand, so the junk value $0$ of a non-integrable integral cannot make a bound hold vacuously. The single-step estimate (4.8) holds $x_t$ fixed and integrates over one sample; integrability of $r(x_{t+1})$ is a hypothesis there, and a conclusion in the run-level statements, where the minimizer $x^*$ supplies the lower bound.
• Algorithm. The iterates are the run of an update map that always lies in $D$, is jointly measurable, and is a minimizer of the subproblem for almost every sample. An unconstrained update map would make the goal false; this one is pinned to the paper's step. $x_0\in U$ is assumed, since the model is only defined on $U$. The parameter $\bar\rho$ of Algorithm 4.1 does not affect the iterates, and requiring $\beta_t>\bar\rho>\tau+\eta=0$ over the steps used is the same as $\alpha_t>0$.
• Minimizer. $x^*\in D$ with $\varphi(x^*)\le\varphi(y)$ for all $y\in D$. A minimizer of $f$ alone, or an arbitrary point, would trivialize the goal; convexity of $\varphi$ is not assumed separately, since it follows from Lemma 4.1.
• Corrected constant (paper typo). The paper prints $2\mathsf L^2/(\beta_t(\beta_t-\eta))$ in (4.8), $2\mathsf L^2\alpha_t^2$ in the first display of the proof of Theorem 4.1, and $\mathsf L^2$ in (4.17)–(4.18). Its own proof of (4.8) (p. 21) bounds the error terms by $2\mathsf L^2/\beta_t$ and divides by $(\beta_t-\eta)/2$, which gives $4\mathsf L^2/(\beta_t(\beta_t-\eta))$. The printed (4.8) and the printed first display fail on a one-dimensional example ($r=0$, $f=|\cdot|$, a linear model with slope $\pm1$ at the origin, $\beta=1$). The Lean statements carry the constants the proof establishes: $4\mathsf L^2$ in (4.8) and the display, $2\mathsf L^2$ in (4.17)–(4.18). Whether the printed (4.17) holds by a sharper argument is not settled here; the milestone texts quote the page verbatim.
• Needed infrastructure. Product measures and independence of coordinates (Measure.pi), Fubini–Tonelli over $\Omega^{t}\times\Omega$, measurability of the run, Jensen's inequality for a convex function on a convex set, and strong convexity of the subproblem. Proofs of any milestone are welcome, as are a general "conditional one-step bound to expectation over the run" lemma reusable by the other missions of this series.

Selected references

• D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM J. Optim. 29(1):207–239, 2019; arXiv:1803.06523v3. https://arxiv.org/abs/1803.06523
• J. Duchi, Y. Singer, Efficient online and batch learning using forward backward splitting, J. Mach. Learn. Res. 10:2899–2934, 2009. https://jmlr.org/papers/v10/duchi09a.html
• J. Cruz, On proximal subgradient splitting method for minimizing the sum of two nonsmooth convex functions, Set-Valued Var. Anal. 25:245–263, 2017. https://doi.org/10.1007/s11228-016-0376-5

Motivation

Many problems in statistical learning and signal processing minimize an expectation $f(x)=\mathbb E_\xi[F(x,\xi)]$ plus a regularizer or constraint $r(x)$, with access to $f$ only through samples $\xi\sim P$. The standard tool is the stochastic (proximal) subgradient method, which replaces $f$ at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss $F(\cdot,\xi)$, and the stochastic prox-linear method linearizes only the smooth inner map of a composite loss $h(c(x,\xi))$. The richer models are markedly less sensitive to the step size in practice.

Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization: each step minimizes a sampled one-sided model $f_{x_t}(\cdot,\xi_t)$ of $f$, plus $r$, plus a quadratic penalty. Their main theorem (Theorem 4.3) concerns weakly convex problems. This mission formalizes the companion result for the strongly convex setting, Theorem 4.2: when the models lower-bound $f$ in expectation and $f_x(\cdot,\xi)+r$ is $\mu$-strongly convex, the expected function gap at a nonuniformly weighted average of the iterates decays like $1/(\mu T)$. The weighting is the technique of Schmidt, Le Roux and Bach (2012) for the projected stochastic subgradient method; the paper extends it to the fully proximal, model-based setting (p. 23).

Setting

Work in $\mathbb R^d$ with the Euclidean norm. The problem is

$$\min_{x\in\mathbb R^d}\ \varphi(x):=f(x)+r(x),$$

where $f:\mathbb R^d\to\mathbb R$ is locally Lipschitz and $r:\mathbb R^d\to\mathbb R\cup\{+\infty\}$ is closed (its epigraph is closed) with nonempty domain $D=\operatorname{dom}r$. A function $\psi$ is $\rho$-weakly convex if $x\mapsto\psi(x)+\frac\rho2\|x\|^2$ is convex; a negative modulus $\rho=-\mu$ is $\mu$-strong convexity.

Assumption B (p. 18) fixes a probability space $(\Omega,\mathcal F,P)$, an open convex set $U\supseteq D$, real constants $\tau,\eta,\mathsf L$, a measurable model $(x,y,\xi)\mapsto f_x(y,\xi)$ on $U\times U\times\Omega$ and a measurable $L:\Omega\to\mathbb R_+$ such that:

1. (B1) i.i.d. samples $\xi_0,\xi_1,\dots\sim P$ can be drawn;
2. (B2) $\mathbb E_\xi[f_x(x,\xi)]=f(x)$ and $\mathbb E_\xi[f_x(y,\xi)-f(y)]\le\frac\tau2\|y-x\|^2$ for $x,y\in U$;
3. (B3) $f_x(\cdot,\xi)+r$ is $\eta$-weakly convex for every $x\in U$ and almost every $\xi$;
4. (B4) $\sqrt{\mathbb E[L(\xi)^2]}\le\mathsf L$ and $f_x(x,\xi)-f_x(y,\xi)\le L(\xi)\|x-y\|$ for $x,y\in U$ and almost every $\xi$.

Algorithm 4.1 (p. 19) starts at $x_0$ and, for $t=0,\dots,T$, samples $\xi_t\sim P$ and sets

$$x_{t+1}=\operatorname*{argmin}_{x}\Big\{r(x)+f_{x_t}(x,\xi_t)+\frac{\beta_t}{2}\|x-x_t\|^2\Big\}.$$

The strongly convex setting is $\tau=0$ and $\eta=-\mu$ with $\mu>0$, run with $\beta_t=\mu(t+1)/2$. Let $x^*$ be any minimizer of $\varphi$.

Formalization targets

Goal: Theorem 4.2

For every integer $T>0$,

$$\mathbb E\Big[\varphi\Big(\frac{2}{(T+2)(T+3)-2}\sum_{t=1}^{T+1}(t+1)\,x_t\Big)-\varphi(x^*)\Big]\le\frac{\mu\|x_0-x^*\|^2}{(T+2)^2}+\frac{16\mathsf L^2}{\mu(T+2)},$$

together with integrability of the function inside the expectation. The paper prints $8\mathsf L^2$; see Formalization scope.

Milestones

1. Lemma 4.1 (p. 18): $\varphi$ is $(\tau+\eta)$-weakly convex and $|f(x)-f(y)|\le\mathsf L\|x-y\|$ on $U$.
2. Lemma 4.2, (4.8) (p. 20): for a fixed current point $x_t$ and any $x\in\operatorname{dom}r$,

$$\mathbb E_t\|x_{t+1}-x\|^2\le\frac{\beta_t+\tau}{\beta_t-\eta}\|x_t-x\|^2-\frac{2}{\beta_t-\eta}\mathbb E_t[\varphi(x_{t+1})-\varphi(x)]+\frac{4\mathsf L^2}{\beta_t(\beta_t-\eta)}.$$

3. Proof of Theorem 4.2, first display (p. 23): with $\Delta_t=\frac12\mathbb E\|x^*-x_t\|^2$,

$$\mathbb E[\varphi(x_{t+1})-\varphi(x^*)]\le\beta_t\Delta_t-(\beta_t+\mu)\Delta_{t+1}+\frac{2\mathsf L^2}{\beta_t}.$$

Significance

The result. Theorem 4.2 is the $O(1/(\mu T))$ rate for a whole family of stochastic methods at once: the stochastic proximal point, prox-linear and proximal subgradient methods all satisfy Assumption B (§4.2 of the paper). The rate is in function values at an explicit averaged point, with explicit constants, and needs neither smoothness of $f$ nor bounded subgradients of $r$: the regularizer enters only through the strong convexity of the subproblems. The $1/(\mu T)$ order is the one Schmidt, Le Roux and Bach obtained for the projected stochastic subgradient method; Theorem 4.2 extends it to models that are not linear and to a general closed $r$.

Formalizing it. The result is proved in the paper; it is not formalized anywhere to our knowledge. Formalizing it pins down the exact constant (the printed one does not follow from the paper's lemmas; see below), the measure-theoretic content of "iterates generated by Algorithm 4.1" (a measurable selection of the argmin, the product measure of the samples, conditional expectation as an integral over one fresh sample) and the integrability that the expectations presuppose. The one-step estimate (4.8) is shared with mission 4 of this series (Theorem 4.1, convex setting); a proof of it serves both.

Difficulty

The telescoping that turns the one-step bound into the rate is elementary once the weights $t+2$ are chosen. The work lies in two places. First, (4.8) itself: it combines the strong convexity of the subproblem, the one-sided accuracy (B2) used in expectation, the Lipschitz bound (B4) at the random point $x_{t+1}$ (so the exceptional null set must not depend on that point), Cauchy–Schwarz, and Lemma 4.1. Second, the passage from one step with $x_t$ held fixed to expectations over the whole run: this needs the independence of $\xi_t$ from $\xi_0,\dots,\xi_{t-1}$ (Fubini on the product measure) and integrability of $r$, $\|x_t-x^*\|^2$ and $\varphi(x_{t+1})$ along the run, none of which is stated on the page. A natural first attempt, bounding $\varphi$ at the average by the average of $\varphi$ before checking that the average lies in $D$, is valid only because the weights sum to one and $D$ is convex by (B3).

Formalization scope

• Carrier and extended values. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The extended-valued $r$ is encoded by its domain D and its real values on D; closedness is closedness of $\{(x,t):x\in D,\ r(x)\le t\}$. $\mu$-strong convexity is $(-\mu)$-weak convexity: convexity of $\psi-\frac\mu2\|\cdot\|^2$ on D.
• Randomness. The $T+1$ samples are a point of $\Omega^{T+1}$ under Measure.pi; expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion, so a junk value $0$ cannot make a bound hold. $\mathbb E_t$ in (4.8) is the integral over one fresh sample with $x_t$ held fixed.
• Iterates. The update is a jointly measurable map that lies in $D$ and is a minimizer of the subproblem for almost every sample; the run is driven by it. Measurability of the update and $x_0\in U$ are added hypotheses. The parameter $\bar\rho$ of Algorithm 4.1 does not affect the iterates (any $\bar\rho\in(-\mu,\mu/2)$ is admissible for all $t$) and does not appear. $x^*$ is any minimizer of $\varphi=f+r$ over $D$.
• Constant correction. The proof of (4.8) on p. 21 bounds the $\delta$-terms by $2\mathsf L^2/\beta_t$ and divides by $(\beta_t-\eta)/2$, which gives $4\mathsf L^2/(\beta_t(\beta_t-\eta))$; the display prints $2\mathsf L^2/(\beta_t(\beta_t-\eta))$, which fails on a one-dimensional example. Carried through the proof of Theorem 4.2, the corrected constant gives $2\mathsf L^2/\beta_t$ in the first display (printed $\mathsf L^2/\beta_t$) and $16\mathsf L^2/(\mu(T+2))$ in the theorem (printed $8\mathsf L^2$). The Lean states the proof's constants; the milestone texts are quoted as printed. Whether the printed $8\mathsf L^2$ bound holds by a sharper argument is open here.
• Trivializations ruled out. The stepsize is fixed to $\beta_t=\mu(t+1)/2$, the update is constrained to the argmin, $x^*$ minimizes $\varphi$ (not $f$), and the modulus is $-\mu$, not $\mu$ ($\mu$-weak convexity would make the theorem false).
• Contributions welcome. A proof of (4.8) from Assumption B, the Fubini/independence step for the run, and integrability lemmas for argmin selections are reusable across the series.

Selected references

• D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM J. Optim. 29(1):207–239, 2019; arXiv:1803.06523v3. https://arxiv.org/abs/1803.06523
• M. Schmidt, N. Le Roux, F. Bach, A simpler approach to obtaining an O(1/t) convergence rate for the projected stochastic subgradient method, arXiv:1212.2002, 2012 (cited as [62] in the paper). https://arxiv.org/abs/1212.2002