Optimization

Motivation

A decision maker who does not want to be judged by expected loss alone needs a functional that weighs the bad outcomes more heavily than the good ones and still behaves well under optimization: monotone, convex, unchanged by shifting the loss, and scaling with it. Kusuoka's theorem (mission II) says every such law-invariant functional on an atomless space is a supremum of mixtures of Average Values-at-Risk. The mixtures themselves are the distortion risk functionals of Denneberg (Distorted probabilities and insurance premiums, Methods of Operations Research 63, 1990) and Acerbi (Spectral measures of risk: A coherent representation of subjective risk aversion, Journal of Banking and Finance 26, 2002, doi:10.1016/S0378-4266(02)00281-9), also called spectral risk measures: integrals of the quantile function against a nondecreasing density $\sigma$. They are the risk functionals used throughout Pflug and Pichler's book (doi:10.1007/978-3-319-08843-3) in the multistage objectives of Chapters 5 and 6, and the three representations proved in Sections 3.2 to 3.4 — as a supremum over densities $Z$, as a maximum over uniform variables, and as an infimum over convex-conjugate constraints — are what make them computable inside an optimization model. This mission formalizes those representations.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random variable $Y:\Omega\to\mathbb R$ is a loss, and the functionals act on $L^\infty$, the bounded measurable ones. The Value-at-Risk at level $u\in(0,1]$ is the lower quantile $\mathsf{V@R}_u(Y)=\inf\{y:P(Y\le y)\ge u\}$ and the Average Value-at-Risk at level $\alpha\in[0,1)$ is $\mathsf{AV@R}_\alpha(Y)=\frac{1}{1-\alpha}\int_\alpha^1\mathsf{V@R}_u(Y)\,du$, extended to $\alpha=1$ by the essential supremum (mission II). A risk functional satisfies the four axioms (M), (C), (T), (H) of Definition 3.2.

A distortion function is a nonnegative, nondecreasing $\sigma:[0,1)\to[0,\infty)$ with $\int_0^1\sigma=1$, and the distortion risk functional with density $\sigma$ is

$$\mathcal R_\sigma(Y)\;=\;\int_0^1\sigma(u)\,\mathsf{V@R}_u(Y)\,du .$$

The Average Value-at-Risk is the case $\sigma_\alpha=(1-\alpha)^{-1}\mathbf 1_{[\alpha,1)}$. A random variable $Z$ is dominated by $\sigma$, $Z\preccurlyeq\sigma$, when $Z\in L^1$, $\mathbb E(Z)=1$ and $\mathsf{AV@R}_\alpha(Z)\le\frac{1}{1-\alpha}\int_\alpha^1\sigma$ for every $\alpha\in[0,1)$. A variable $U$ is uniformly distributed when $P(U\le u)=u$ on $[0,1]$. For $h:\mathbb R\to\mathbb R$ the conjugate is $h^*(s)=\sup_y(s\,y-h(y))\in(-\infty,+\infty]$.

Formalization targets

Goal — Theorem 3.16 (printed pp. 105–106)

$$\mathcal R_\sigma(Y)\;=\;\sup\bigl\{\mathbb E(Y\cdot Z)\ :\ Z\preccurlyeq\sigma\bigr\} \qquad(Y\in L^\infty).$$

The distortion functional is a risk functional (printed p. 99)

$\mathcal R_\sigma$ satisfies (M), (C), (T) and (H).

Representation (3.11) (printed p. 100)

There is a probability measure $\mu$ on $[0,1]$ with $\mathcal R_\sigma(Y)=\int_0^1\mathsf{AV@R}_\alpha(Y)\,\mu(d\alpha)$ for all $Y\in L^\infty$.

Corollary 3.18 (printed pp. 107–108)

For $\alpha<1$, $\mathsf{AV@R}_\alpha(Y)=\sup\{\mathbb E(YZ):\mathbb EZ=1,\ \mathsf{AV@R}_p(Z)\le\frac1{1-\alpha}\ \forall p\in[\alpha,1]\} =\sup\{\mathbb E(YZ):\mathbb EZ=1,\ 0\le Z\le\frac1{1-\alpha}\}$; for $\alpha=1$ the latter with the upper bound dropped.

Corollary 3.19 (printed p. 108)

On an atomless space, $\mathcal R_\sigma(Y)=\max\{\mathbb E(Y\cdot\sigma(U)):U\text{ uniform}\}$, the maximum attained.

Theorem 3.22 (printed p. 111)

$\mathcal R_\sigma(Y)=\inf\{\mathbb E(h(Y)):\int_0^1h^*(\sigma(u))\,du\le 0\}$ over measurable $h:\mathbb R\to\mathbb R$.

Significance

Theorem 3.16 identifies the conjugate of a distortion functional: $\mathcal R_\sigma^*(Z)$ is $0$ when $Z\preccurlyeq\sigma$ and $+\infty$ otherwise, so $\mathcal R_\sigma$ is the support function of an explicit convex set of densities. Everything else follows from that. Corollary 3.18 recovers the classical dual of the Average Value-at-Risk and shows that its constraints can be relaxed to the levels in $[\alpha,1]$; Corollary 3.19 turns the supremum into a maximum over couplings and identifies the maximizer, the co-monotone one, which is how distortion functionals are evaluated on scenario trees; Corollary 3.21, not stated here, combines the theorem with Kusuoka's representation to give the dual of every version independent risk functional. Theorem 3.22 goes the other way and writes $\mathcal R_\sigma$ as an infimum, which is what converts a minimax problem — minimize a supremum over $Z$ — into a plain minimization over the decision and an auxiliary function $h$, the form in which the book solves risk-averse programs in Chapters 5 and 6.

Everything here is proved in the source and in the cited papers; the platform has the finite-scenario Artzner–Delbaen representation of coherent risk measures but nothing on distortion functionals, and Mathlib has no risk-measure material and no quantile-based representation theory. The definitions of this mission sit on those of mission II and are reused as such.

Difficulty

The obvious route to Theorem 3.16 is Fenchel–Moreau duality: $\mathcal R_\sigma$ is convex and lower semicontinuous on $L^\infty$, so it equals its biconjugate, and the task is to compute $\mathcal R_\sigma^*(Z)=\sup_Y\,\mathbb E(YZ)-\mathcal R_\sigma(Y)$. The step where the naive computation stalls is bounding $\mathbb E(YZ)$ by a quantity that depends only on the distributions of $Y$ and $Z$: this is the rearrangement (Chebyshev, Hardy–Littlewood) inequality $\mathbb E(YZ)\le\int_0^1G_Y^{-1}(u)G_Z^{-1}(u)\,du$, with equality for co-monotone couplings. Given it, $\mathcal R_\sigma^*(Z)=\sup_Y\int_0^1G_Y^{-1}(G_Z^{-1}-\sigma)$, and testing with indicator-type $Y$ shows the supremum is $0$ exactly when the upper-tail averages of $Z$ are dominated by those of $\sigma$, which is the constraint $Z\preccurlyeq\sigma$. Neither the rearrangement inequality nor the identification of the conjugate is available in Mathlib.

For the corollaries the difficulties are concrete. Corollary 3.18 needs $Z\ge 0$ to be deduced from the constraints, which the source does by contradiction through the value $p=P(Z<0)$. Corollary 3.19 needs the co-monotone coupling to exist, which is where the atomless hypothesis enters, and needs $\sigma(U)$ to be feasible for (3.15), which uses $G_{\sigma(U)}^{-1}=\sigma$. Theorem 3.22 needs, besides the inequality $\mathbb E(h(Y))\ge\mathcal R_\sigma(Y)$ from Fenchel–Young, an admissible $h$ that nearly attains it; the source builds it from $\sigma$ and $G_Y^{-1}$ via Corollary 3.23.

Formalization scope

Random variables are functions $\Omega\to\mathbb R$ on an arbitrary measurable space with a probability measure, exactly as in mission II, whose MemLinfty, valueAtRisk, averageValueAtRisk, IsRiskFunctional, Atomless and IsKusuokaMeasure are imported and not redefined. The distortion density is a function on $\mathbb R$ constrained on $[0,1)$; its integrability on $(0,1)$ is part of the definition, and both $\int_0^1\sigma$ and $\mathcal R_\sigma$ integrate over the open interval, which excludes the level $0$ where the quantile formula is not meaningful and changes no value.

Every supremum and infimum is over a subtype of functions satisfying the constraints, and the prose of each item records why the family is nonempty and bounded, so that no real supremum takes its junk value. Pointwise constraints on $Z$ are almost sure. The constraint of (3.15) is stated for $\alpha\in[0,1)$: at $\alpha=1$ the source's expression is $0/0$ and means the limit, and the constraint there is implied by the others; (3.19) at $\alpha=1$ is stated separately with the upper bound dropped. The conjugate takes values in the extended reals, and admissibility in Theorem 3.22 requires $h^*(\sigma(u))$ finite almost everywhere, integrable, with integral at most $0$, and $h(Y)$ integrable — the conditions under which the expectations in (3.24) are the integrals the source means.

Two hypotheses are added beyond the printed statements and are flagged in the items: atomless for Corollary 3.19, because otherwise no uniform variable need exist and the maximum would be over an empty set; and integrability of $h(Y)$ in Theorem 3.22, without which Lean's integral of a non-integrable $h(Y)$ is $0$. Theorem 3.16 itself carries no atomless hypothesis, and the mission notes check the identity on two-point spaces by hand. A trivializing formalization — a constraint set that is empty or unbounded, so that the supremum is $0$ — is excluded by the constant density $Z\equiv 1$, feasible for every $\sigma$, and by $Z\ge 0$.

Welcome contributions beyond the milestones: Corollary 3.15 (the representation through the distribution function for $Y\ge 0$), Corollary 3.21 (the dual of a version independent risk functional through its Kusuoka set), Corollary 3.23, and the explicit mixing measure (3.12).

Selected references

• Georg Ch. Pflug and Alois Pichler, Multistage Stochastic Optimization, Springer, 2014, Sections 3.2–3.4. doi:10.1007/978-3-319-08843-3
• Carlo Acerbi, Spectral measures of risk: A coherent representation of subjective risk aversion, Journal of Banking and Finance 26 (2002). doi:10.1016/S0378-4266(02)00281-9
• Shigeo Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3 (2001). doi:10.1007/978-4-431-67891-5_4
• Alois Pichler, The natural Banach space for version independent risk measures, Insurance: Mathematics and Economics 53 (2013). doi:10.1016/j.insmatheco.2013.07.005
• Georg Ch. Pflug and Werner Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007. doi:10.1142/6478

Motivation

Regularization — adding a penalty on model complexity to an empirical risk minimization objective — is one of the oldest and most reliably effective tools in statistical learning: ridge regression, LASSO, and margin-based support vector machines all fit this template. For decades the regularization weight and penalty function were chosen heuristically or by cross-validation, with only asymptotic or worst-case generalization bounds explaining why they help. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter on Wasserstein distributionally robust optimization (DRO) gives regularization a different, non-asymptotic justification: a decision rule that is robust to adversarial perturbations of its training data, measured in Wasserstein distance, is exactly a regularized empirical risk minimizer — no approximation, no asymptotics. This mission formalizes the general form of that equivalence, Theorem 10 (p. 14), which underlies every regularization-by-robustification result the chapter derives for classification and regression alike.

Setting

Fix a normed space $\Xi = \mathbb{R}^m$, a convex loss function $\ell : \Xi \to \mathbb{R}$, a radius $\varepsilon \ge 0$, and $N$ training samples $\hat\xi_1,\dots,\hat\xi_N \in \Xi$ ($N \ge 1$). The empirical distribution is $\hat P_N = \frac{1}{N}\sum_{i=1}^N \delta_{\hat\xi_i}$. The worst-case risk of $\ell$ at radius $\varepsilon$ (eq. (6), p. 6) is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)],$$

where $B_{\varepsilon,p}(\hat P_N)$ is the type-$p$ Wasserstein ball of radius $\varepsilon$ around $\hat P_N$ (Definition 1, p. 3) — the set of probability measures on $\Xi$ within Wasserstein distance $\varepsilon$ of the empirical distribution, under a norm $\|\cdot\|$ on $\Xi$ and its transportation exponent $p$. The Lipschitz modulus $\mathrm{Lip}(\ell) = \sup_{\xi\ne\xi'} \frac{|\ell(\xi)-\ell(\xi')|}{\|\xi-\xi'\|}$ (possibly $+\infty$) measures how fast $\ell$ can grow.

Formalization targets

Goal (Theorem 10, convex loss and $p=1$). If $\ell$ is convex and $p=1$, then the worst-case risk of $\ell$ over the type-1 Wasserstein ball around the empirical distribution coincides with the Lipschitz-regularized empirical loss:

$$R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon \cdot \mathrm{Lip}(\ell),$$

where $R(\hat P_N,\ell) = \frac{1}{N}\sum_{i=1}^N \ell(\hat\xi_i)$ is the ordinary empirical risk. The left side is the worst-case expected loss under adversarial perturbations of the training data of bounded aggregate Wasserstein cost; the right side is the ordinary empirical risk plus a regularization term proportional to the perturbation radius $\varepsilon$ and the loss's own Lipschitz modulus — no approximation, an exact equality for every convex $\ell$.

Significance

This is the single result underlying every specific regularization-by-robustification corollary the chapter derives — the $\ell_2$-regularized SVM and its $\ell_1$/$\ell_\infty$ variants, regularized logistic regression, and the regression analogue with a Lipschitz loss (Proposition 3) — because each of those is obtained by substituting a specific convex, Lipschitz loss (hinge, logloss, a linear-model margin loss) for the general $\ell$ here and reading off $\mathrm{Lip}(\ell)$ in closed form. Theorem 10 is exact ($p=1$, Ξ = R^m) precisely because a type-1 transportation cost is dual to the Lipschitz modulus (a consequence of the Kantorovich- Rubinstein duality this book's earlier duality theorems establish), whereas the corresponding statement for $p \ge 2$ (Theorem 11 elsewhere in the chapter) needs a strictly stronger hypothesis on $\ell$. Formalizing Theorem 10 fixes, machine-checkably, the exact scope of the equivalence — which losses qualify (convex, no boundedness or smoothness needed), which transportation exponent is required ($p=1$, not any $p\ge1$), and that the equality is exact, not an upper or lower bound — the single fact every classification- and regression-specific robustification corollary in the chapter cites without re-deriving.

Difficulty

The natural first attempt treats the worst-case risk as an instance of the general finite convex reduction (Theorem 8, which needs $\ell$ or a related concave/convex-conjugate structure and applies for a general norm exponent $p,q$ with $1/p+1/q=1$) and specializes it to $p=1$. This is not the paper's own route for Theorem 10: at $p=1$ the dual exponent $q=\infty$, and the general finite-convex-program reduction (11) degenerates in a way that is more naturally derived directly from the type-1 Wasserstein distance's own dual (Kantorovich-Rubinstein) representation — a Lipschitz test function pairs exactly with a type-1 transportation cost, which is why the answer is Lipschitz-regularization and not some other penalty. The Lean statement records only the final equality (the proof itself, via Theorem 8 or the direct Kantorovich-Rubinstein route, is left as sorry, as required for a draft item), but the choice of which milestones would support that proof is exactly this: the type-1/Lipschitz-modulus duality is a structurally different argument from the finite-convex-program machinery Theorem 8 needs for other $p$, which is why this chapter's earlier draft mistakenly tried to reach a specialization of Theorem 10 (Proposition 2, restated for a labeled, $\kappa=\infty$ ambiguity set) through a finite-atom shortcut that does not actually capture the general type-1 ball Theorem 10's own proof needs — see Formalization scope.

Formalization scope

$\Xi$ is EuclideanSpace ℝ (Fin m) (fixed to Set.univ, matching the theorem's own "Ξ = R^m" hypothesis) with an arbitrary fixed norm as a type-class parameter, not specialized to Euclidean. The worst-case risk, Wasserstein distance, ambiguity set, nominal risk, empirical distribution and Lipschitz modulus are all redefined locally in this chapter's own namespace, verbatim restatements of 01-duality's own drafts of the same objects (identical EReal/ENNReal/Integrable conventions), because 01-duality is not yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once it is live. hN : 0 < N excludes the empty-sample case the paper's own "N training samples" presupposes; hℓ : Integrable ℓ (empiricalDistribution ξhat) guards the empirical risk's Bochner integral (automatically satisfied under any real-valued ℓ since the empirical distribution is a finite convex combination of Dirac masses, but stated explicitly rather than assumed silently). No constant is pinned to a numeral. This mission originally targeted Proposition 2 (regularization by robustification for classification, p. 25), a specialization of Theorem 10 to a labeled, κ=∞ input-output ambiguity set — but that draft's κ=∞ ambiguity set restricted admissible perturbations to a finite family of exactly N atoms, each sample's entire mass moving as one indivisible unit, which is a strict, non-faithful subset of the true κ=∞ Wasserstein ball (splitting a sample's mass across several destinations is a legitimate, and for a convex loss strictly more powerful, perturbation by Jensen's inequality). This made the goal theorem false for at least one of the three loss functions (Table 1) the mission itself certified as covered (logloss), not merely narrower than the paper's claim — moderation caught this and required either a faithful general-ambiguity-set reformulation or retargeting the goal. This mission takes the latter: Theorem 10 itself, already correctly and generally stated using the unrestricted Wasserstein ball throughout, is now the goal, with no further milestone (no other numbered result in this chunk's scope is needed for Theorem 10's own statement beyond the shared definitions above). A future mission in this series can revisit Proposition 2/3 with a properly general labeled ambiguity set once that construction (label-pinned marginal plus an aggregate coupling condition on the input coordinate, rather than a finite atom family) is built.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Shafieezadeh-Abadeh, S., Esfahani, P. M., & Kuhn, D. (2015). Distributionally robust logistic regression. Advances in Neural Information Processing Systems, 28.
• Blanchet, J., Kang, Y., & Murthy, K. (2019). Robust Wasserstein profile inference and applications to machine learning. Journal of Applied Probability, 56(3), 830–857.

Motivation

A decision maker who solves a distributionally robust optimization (DRO) problem over a Wasserstein ball chooses a radius $\varepsilon$ by hand, and it is natural to ask what guarantee that choice actually buys: how large must $\varepsilon$ be, as a function of the sample size $N$ and a desired confidence level, before the resulting worst-case risk is provably not an underestimate of the true (unknown-distribution) risk? Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter answers this for the mean-covariance relaxation of Wasserstein DRO introduced via the Gelbrich hull (Section 2.3): Theorem 21 gives a concentration inequality for how fast the sample mean and covariance approach the true mean and covariance, and Theorem 22 turns that concentration bound into a finite-sample statistical guarantee for the Gelbrich risk itself. This mission formalizes both.

Setting

Fix $m \in \mathbb{N}$. Let $P$ be the unknown true distribution on $\mathbb{R}^m$ with mean vector $\mu$ and covariance matrix $\Sigma \in S^m_+$, and suppose $P$ is light-tailed: there exist $\alpha > 2$ and $A > 0$ with $E_P[\exp(\|\xi\|_2^\alpha)] \le A$. Let $\hat\xi_1,\dots,\hat \xi_N$ be $N$ independent, identically distributed samples from $P$; write $P^N$ for their joint law (the $N$-fold product measure) and $\hat\mu, \hat\Sigma$ for the resulting sample mean and sample covariance, i.e. the mean and covariance of the empirical distribution $\hat P_N = \frac{1}{N}\sum_i \delta_{\hat\xi_i}$. Recall from the Gelbrich construction the mean-covariance uncertainty set $U_\varepsilon(\hat\mu,\hat\Sigma) = \{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2} \Sigma\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2\}$, and the Gelbrich risk $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ of a loss function $\ell$ over the Gelbrich hull $G_\varepsilon(\hat\mu,\hat \Sigma)$.

Formalization targets

Milestone (Theorem 21, concentration inequalities II). There is $c > 1$, depending on $P$ only through $\mu,\Sigma,\alpha,A,m$ (not on any finer feature of $P$), such that for every $\eta \in (0,1]$,

$$P^N\big[(\mu,\Sigma) \in U_\varepsilon(\hat\mu,\hat\Sigma)\big] \ge 1-\eta \quad \text{whenever} \quad \varepsilon \ge \varepsilon_N(\eta) := \frac{\log(c/\eta)}{\sqrt N}.$$

Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every $\eta \in (0,1)$ and $\varepsilon \ge \varepsilon_N(\eta)$,

$$P^N\Big\{R(P,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell) \;\; \forall \ell \in L\Big\} \ge 1-\eta.$$

With probability at least $1-\eta$ over the draw of the training sample, the Gelbrich risk computed from that sample upper-bounds the true risk of every admissible loss function simultaneously — not just of one fixed $\ell$ chosen in advance. (The paper's part (b), the analogous guarantee $P^N\{R(P,\ell^\star) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell^\star)\} \ge 1-\eta$ for the specific optimizer $\ell^\star$ of the Gelbrich risk minimization problem, is not formalized in this mission — see Formalization scope.)

Significance

Theorem 22 is what makes the Gelbrich-risk relaxation of Wasserstein DRO more than a computational convenience: it certifies that solving the tractable Gelbrich risk minimization problem gives a decision whose true out-of-sample risk is, with high probability, no worse than the value the solver reports — a genuine confidence guarantee, not merely an approximation of the Wasserstein worst-case risk. Theorem 21's rate, $\varepsilon_N(\eta) = O(N^{-1/2})$, is also of independent interest: it is dimension-free (no curse of dimensionality), in contrast to the paper's earlier general-distribution concentration result (Theorem 18, out of scope for this mission) whose rate degrades with $m$. Formalizing Theorem 21 fixes, machine-checkably, the exact functional form of $\varepsilon_N(\eta)$ and the precise sense in which $c$ is "distribution-free" given $(\mu,\Sigma,\alpha,A,m)$ — a subtlety easy to state informally but easy to get wrong formally (see Difficulty).

Difficulty

The central formalization difficulty is not proving the theorems (both are left as sorry in this draft) but stating the existential constant $c$ correctly. The paper says $c$ "depends on $P$ only through $\mu,\Sigma,\alpha,A,m$" — informally, a promise that $c$ is uniform across every distribution $P$ sharing those five parameters, not merely that some $c$ exists for each $P$ separately (a vacuously true, much weaker statement obtained by naively quantifying $c$ after $P$). The correct encoding places $\exists c$ before the universal quantifier over $P$: for fixed $(\mu,\Sigma,\alpha,A,m)$, one $c$ must work for every $P$ with that mean, covariance, and tail bound. Getting this quantifier order backwards silently converts a genuine finite-sample guarantee into a triviality (FAITHFULNESS_TRAPS.md trap 8).

Formalization scope

Distributions live on EuclideanSpace ℝ (Fin m); $P^N$, the law of $N$ iid samples, is the $N$-fold product measure MeasureTheory.Measure.pi (fun _ => P) on Fin N → EuclideanSpace ℝ (Fin m) — an event about the random sample sequence is a set of such tuples, and "$P^N[\text{event}] \ge 1-\eta$" is that product measure's mass on the event set. All risk and uncertainty-set definitions (meanVector, covarianceMatrix, meanCovarianceUncertaintySet, gelbrichHull, gelbrichRisk, nominalRisk, empiricalDistribution) are redefined locally in this chapter's own namespace, matching 02-gelbrich's conventions exactly, since neither 01-duality nor 02-gelbrich is yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once those missions are live. The existential constant c is placed before the universal quantifier over P in both theorems, exactly capturing "depends on P only through µ,Σ,α,A,m" — see Difficulty. Only Theorem 22's part (a) (the uniform bound over a loss class L) is formalized; part (b) — the bound for the specific optimizer ℓ* of the Gelbrich risk minimization problem (19) — is left out, because it requires first formalizing "ℓ* is an optimizer of problem (19)" as an object (an infimum-attaining selection over a data-dependent optimization problem), which is additional infrastructure this mission's time budget did not cover; formalizing it as an unconditional bound over an arbitrary data-dependent ℓ* (dropping the optimality hypothesis) would be unfaithful — the guarantee genuinely depends on ℓ* being an optimizer, not an arbitrary measurable function of the sample. The goal theorem also carries hΞ, stating Ξ contains the support of P (the paper's own standing assumption, p. 6, for every later use of Ξ), and hLInt, an Integrable ℓ P guard for every ℓ ∈ L, matching Assumption 1 (p. 9); both were added after moderation found the goal's original statement, without them, admitted a counter-instance (Ξ = ∅ collapses the Gelbrich hull to empty and the risk supremum to ⊥, making the guarantee provably false rather than merely undisclosed). Theorem 18 (the general, dimension- dependent concentration inequality with its piecewise ε_N(η) formula) and Theorems 19/20/23 (its downstream guarantees and the asymptotic-consistency results) are out of scope for this mission, which targets the Gelbrich-risk branch (Theorems 21/22) specifically.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Fournier, N., & Guillin, A. (2015). On the rate of convergence in Wasserstein distance of the empirical measure. Probability Theory and Related Fields, 162(3), 707–738.
• Gao, R., & Kleywegt, A. J. (2023). Distributionally robust stochastic optimization with Wasserstein distance. Mathematics of Operations Research, 48(2), 603–655.

Motivation

Compressed sensing asks a question that looks impossible at first: can a signal $x\in\mathbb R^n$ be reconstructed exactly from far fewer than $n$ linear measurements $y=Ax\in\mathbb R^m$, $m\ll n$? Classical linear algebra says no — an underdetermined system has infinitely many solutions. But if $x$ is known in advance to be sparse (most of its coordinates are zero), the extra structure makes recovery possible: solving the convex program that minimizes the $\ell_1$ norm of a candidate solution, subject to matching the measurements, recovers $x$ exactly, for a measurement matrix $A$ with a suitable geometric property. This idea, developed by Candès, Romberg, Tao and Donoho in the mid-2000s, underlies modern MRI acceleration, single-pixel cameras, and sparse signal processing generally.

The chapter isolates the exact geometric property a measurement matrix needs — the restricted isometry property (RIP) — and proves, purely by linear algebra with no probability involved, that RIP alone is sufficient for exact recovery by $\ell_1$ minimization. (A companion result, outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once $m$ is large enough, which is what makes the deterministic guarantee here practically useful; this mission formalizes the deterministic half.)

Setting

For a vector $v$ indexed by a finite set, write $\|v\|_0$ for its number of non-zero coordinates (so $v$ is $s$-sparse if $\|v\|_0\le s$), $\|v\|_1:=\sum_i|v_i|$ for its $\ell_1$ norm, and $\|v\|_2:=\sqrt{\sum_i v_i^2}$ for its Euclidean norm.

An $m\times n$ matrix $A$ satisfies the restricted isometry property (RIP) with parameters $\alpha,\beta,s$ if

$$\alpha\|v\|_2 \;\le\; \|Av\|_2 \;\le\; \beta\|v\|_2 \qquad\text{for every } s\text{-sparse } v\in\mathbb R^n,$$

i.e. $A$ acts as an approximate isometry on every $s$-sparse vector — equivalently (the book's own Exercise 10.5.9), the singular values of every $m\times s$ column-submatrix of $A$ lie in $[\alpha,\beta]$.

Given a matrix $A$ and measurements $y=Ax$ for an unknown sparse $x$, the exact-recovery program is

$$\text{minimize } \|x'\|_1 \quad\text{subject to}\quad y = Ax'.$$

Formalization targets

Goal (Theorem 10.5.10, RIP implies exact recovery)

$$\exists\,\hat x = x \quad\text{whenever}\quad \hat x \text{ solves the exact-recovery program for } y=Ax,$$

precisely: suppose $A$ satisfies RIP with parameters $\alpha,\beta,(1+\lambda)s$ where $\lambda>(\beta/\alpha)^2$; then for every $s$-sparse $x$, every $\hat x$ that is feasible ($A\hat x=Ax$) and $\ell_1$-optimal among feasible vectors satisfies $\hat x=x$. No constant here is hard-coded beyond the book's own explicit threshold $\lambda>(\beta/\alpha)^2$ — the weakest stable form of the claim.

Significance

RIP isolates exactly the geometric mechanism that makes $\ell_1$-minimization work for sparse recovery: once a matrix is known to satisfy it, exact recovery is a deterministic, provable consequence with no appeal to randomness, no failure probability, and no measurement-count formula to verify beyond the RIP parameters themselves. This clean separation — a purely geometric sufficient condition (RIP), proved separately (in the book's Theorem 10.5.11, outside this mission) to hold with high probability for random sub-gaussian matrices — is the template compressed sensing theory follows throughout: geometric/deterministic guarantee first, probabilistic verification that random constructions meet it second. The theorem is one of the two standard routes (with the direct probabilistic argument of Theorem 10.5.1) to the chapter's central claim that $m=O(s\log n)$ measurements suffice to recover any $s$-sparse signal in $\mathbb R^n$ — exponentially fewer than the $n$ measurements a naive linear-algebraic argument would need.

The result itself, and the RIP framework, are classical and well-established (Candès-Tao 2005). This mission formalizes the deterministic linear-algebra core of the argument — the statement infrastructure (RIP, sparsity, the exact-recovery program stated as an explicit optimization problem) and the goal theorem — for a solver to close with a proof.

Difficulty

The natural first idea for showing $\hat x=x$ is to try to bound the recovery error $h:=\hat x-x$ directly using $\|Ah\|_2$ (which vanishes, since both $x$ and $\hat x$ are feasible) together with RIP applied to $h$ itself — but $h$ need not be sparse at all: it is the difference of two sparse-ish vectors and can have full support. The actual argument decomposes $h$'s support into blocks by descending magnitude (the support $I_0$ of $x$, then the $\lambda s$ largest remaining coordinates $I_1$, then the next $\lambda s$, and so on), applies RIP only to the leading block $I_{0,1}=I_0\cup I_1$ (which genuinely has bounded sparsity $\le(1+\lambda)s$), and separately bounds the contribution of every later block using the fact that $\hat x$ is $\ell_1$-optimal (so $\|h_{I_0^c}\|_1\le\|h_{I_0}\|_1$, the "cone constraint"): each later block's $\ell_2$ norm is controlled by the $\ell_1$ mass of the previous block divided by its size. This is a genuinely multi-step argument combining a purely geometric fact (RIP on one bounded-sparsity block) with a purely combinatorial one (the magnitude-sorted decomposition), and the "obvious" idea of applying RIP to $h$ as a whole does not typecheck, since RIP says nothing about vectors with more than $(1+\lambda)s$ non-zero entries.

Formalization scope

Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's fixed $\ell_2$ norm instance cannot also host the $\ell_1$ norm the program's objective needs, so both norms (L2Norm, L1Norm) are defined directly by their defining sums on the same underlying type. Sparsity (Sparsity) takes a real-valued threshold s : ℝ, matching that the RIP parameter $(1+\lambda)s$ used by the goal theorem is a real number even at integer base sparsity. A solution $\hat x$ "of the program" is formalized as an explicit argmin membership — feasibility (A.mulVec xhat = A.mulVec x) conjoined with optimality over the exact feasible set (∀ x', A.mulVec x' = A.mulVec x → l1Norm xhat ≤ l1Norm x') — never "there exists an estimator such that", the trivialization risk this chapter's own triage brief flags explicitly (shared with Chapter 3's Max-Cut): an existential reading would prove a different, strictly weaker statement. The conclusion is stated for every such $\hat x$, not one witness, matching that RIP forces uniqueness.

This mission covers Theorem 10.5.10 only, as the sole item; the probabilistic goal Theorem 10.5.1 (exact recovery for random sub-gaussian measurement matrices, which needs Theorem 10.5.10 together with a separate probabilistic argument, Theorem 10.5.11, that random matrices satisfy RIP), and the Lasso guarantee (Theorem 10.6.1), are both left out for lack of session time: each would need a fresh probabilistic apparatus (independent isotropic sub-gaussian random rows, a failure-probability bound) built from scratch in this chapter's own sub-namespace, with no reusable published definition from an earlier chunk. L2Norm, L1Norm, Sparsity and RIP are reusable by any later chapter or mission needing sparse vectors or the restricted isometry property; solvers' contributions are welcome on completing the proof of Theorem 10.5.10 itself (the magnitude-sorted support decomposition sketched under Difficulty above), and, beyond this mission's current scope, on Theorem 10.5.11 and Theorem 10.5.1.

Selected references

• E. J. Candès, T. Tao, Decoding by linear programming, IEEE Transactions on Information Theory 51 (2005), 4203–4215. https://doi.org/10.1109/TIT.2005.858979
• D. L. Donoho, Compressed sensing, IEEE Transactions on Information Theory 52 (2006), 1289–1306. https://doi.org/10.1109/TIT.2006.871582
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 10. https://doi.org/10.1017/9781108231596

Motivation

A cooperative game with side payments models a set of economic agents who can form coalitions and split the proceeds. The central question is stability: is there a way to split the total payoff among all the players so that no subset of them would do better by breaking away and acting on its own? The set of such stable splits is the core, introduced by Gillies [1959] and studied extensively since (Shapley [1971], Shapley [1953]). Sharkey [1982c] surveys the core's role in the economics of natural monopoly, where "no coalition wants to secede" is exactly the condition that a cost-sharing scheme is defensible against any subgroup of customers.

The core of an arbitrary cooperative game can be empty — there may be no split that satisfies every coalition simultaneously — and even when nonempty it can be hard to exhibit a point in it, since it is cut out by $2^n$ linear inequalities. Shapley [1971] identified a large and economically natural class, the convex games (characteristic functions that are supermodular in the coalition), for which the core is always nonempty, and for which an explicit family of core points — one per ordering of the players — can be written down directly. This mission formalizes Shapley's theorem and its later sharpening: this book's central result of Chapter 5, together with a genuine converse (Moulin [1990], sharpening an observation of Sharkey [1982a]) and comparative-statics theorem (Topkis [1987]) showing how these core points move as the underlying economics changes.

Setting

Fix a finite set of players $N = \{1,\dots,n\}$. A characteristic function $f$ assigns a real number $f(S)$ to every coalition $S \subseteq N$, with $f(\emptyset) = 0$; $f(S)$ is the net return a coalition $S$ could earn on its own. The pair $(N,f)$ is a cooperative game, and throughout this chapter $f$ is assumed superadditive: $f(S') + f(S'') \le f(S' \cup S'')$ for disjoint $S', S''$. A payoff vector $y \in \mathbb{R}^N$ is feasible if $\sum_{i \in N} y_i = f(N)$, and acceptable if $\sum_{i \in S} y_i \ge f(S)$ for every coalition $S$. The core is the set of payoff vectors that are both:

$$\mathrm{Core}(N,f) = \Big\{ y \in \mathbb{R}^N : \sum_{i \in N} y_i = f(N) \text{ and } f(S) \le \sum_{i \in S} y_i \ \forall S \subseteq N \Big\}.$$

$(N,f)$ is a convex game if $f$ is supermodular on the Boolean lattice of coalitions: $f(S) + f(S') \le f(S \cup S') + f(S \cap S')$ for all $S, S'$. ("Convex" is the game-theory literature's name for this supermodularity property; it has no relation to convexity of sets or of real functions, a collision the book itself flags.) Equivalently, by Theorem 2.6.1/2.6.4, a game is convex exactly when the marginal value $f(S \cup \{i\}) - f(S)$ of any player $i$ to any coalition $S$ not containing $i$ increases as $S$ grows — the more players already committed to a project, the more valuable one more player is to it.

Given a permutation $\pi$ of $N$, let $S_\pi(j) = \{\pi(1),\dots,\pi(j)\}$. The greedy algorithm builds the payoff vector $y^\pi$ by paying each player its marginal contribution when added in the order $\pi$: $y^\pi_{\pi(j)} = f(S_\pi(j)) - f(S_\pi(j-1))$. The Shapley value pays player $i$ the average of $y^\pi_i$ over all $n!$ permutations $\pi$, equivalently $\sum_{S \subseteq N\setminus\{i\}} \frac{|S|!(n-|S|-1)!}{n!}(f(S\cup\{i\}) - f(S))$.

A core is large if every acceptable payoff vector is dominated, coordinatewise, by one in the core; a subgame $(N',f)$ restricts $f$ to subsets of $N' \subseteq N$; a core is totally large if the core of every subgame is large.

Formalization targets

Goal — Theorem 5.2.1 (Shapley [1971])

$$\text{if } (N,f) \text{ is a convex game, then for every permutation } \pi,\ y^\pi \in \mathrm{Core}(N,f); \quad \mathrm{Core}(N,f) \ne \emptyset; \quad \text{Shapley value} \in \mathrm{Core}(N,f).$$

The weakest stable statement here is already the union of these three claims: nonemptiness of the core (b) is a formal consequence of (a) for any single permutation, and (c) is a genuinely separate fact about the average of the $y^\pi$'s, not implied by (a) and (b) alone.

Milestones

• Lemma 5.2.1(a): $\sum_{i \in S_\pi(j)} y^\pi_i = f(S_\pi(j))$ for every $j = 1,\dots,n$ — the partial-sum identity the goal's proof of acceptability is built on.
• Theorem 5.2.6 (Moulin [1990]): a cooperative game is convex if and only if its core is totally large — the converse direction that a large core alone (Theorem 5.2.1's easy corollary) does not give.
• Theorem 5.2.7(a,b) (Topkis [1987]): if the characteristic function $f^t$ of a family of games has increasing differences in a parameter $t$ (a complementary parameter), the greedy payoff vector and the Shapley value both increase in $t$.

Significance

Theorem 5.2.1 is the reason convex games are the tractable case of cooperative game theory: it turns an existence question about $2^n$ linear inequalities into an explicit construction (any ordering of the players gives a point in the core), and it identifies the Shapley value — an axiomatically motivated but a priori only feasible payoff rule — as one that always respects every coalition's participation constraint on this class. Theorem 5.2.6 shows this is not an accident of the sufficient condition: total largeness of the core is a genuine characterization of convexity, so "does every subgame's core dominate every acceptable vector" is an equivalent, purely core-theoretic way to test convexity. Theorem 5.2.7 gives the comparative statics that make convex games useful in applied models (Chapter 5's later sections build monopoly, surplus sharing, and procurement games on exactly this apparatus): as a game's characteristic function improves in a complementary way with some parameter (a price, a technology level, a capacity), every player's greedy payoff and Shapley value improve monotonically, with no separate argument needed for each application.

Formalizing this mission produces, for the first time on the platform, machine-checked statements of the core, convex games, the greedy algorithm and the Shapley value — definitions that later missions in this series's own polyhedral-structure sections, and any future cooperative-game-theory mission, can reuse rather than re-derive. All three results already have a complete proof in the literature; this mission's remaining work is formalizing that known argument, not any open mathematics.

Difficulty

The routine first idea — check acceptability for the greedy vector one subset at a time using only the definition of supermodularity — does not directly work: Theorem 5.2.1(a)'s proof needs to compare a subset $S'$ against the initial coalitions $S_\pi(j)$ built by the particular permutation $\pi$, splitting $S'$ by the first and last time one of its elements appears in $\pi$'s order and applying supermodularity along the resulting chain, not a single inequality. Theorem 5.2.6's converse direction is the harder half: showing a totally large core forces supermodularity requires constructing an auxiliary characteristic function $g(S) = \max_{S \subseteq S' \subseteq N} \big(f(S') - \sum_{i \in S'} y''_i\big)$ from an arbitrary acceptable vector $y''$ and showing $g$ is itself supermodular (via Theorem 2.6.4 and Theorem 2.7.6, results from the earlier monotone-comparative-statics chapter this mission depends on) before the argument closes.

Formalization scope

Players are modeled as Fin n and a characteristic function as f : Finset (Fin n) → ℝ; a payoff vector is y : Fin n → ℝ, and the core's feasibility and acceptability conditions are stated with respect to Finset.univ (the whole player set) or a coalition U : Finset (Fin n) for a subgame, never approximated by a finite sample of coalitions or by feasibility alone — the acceptability condition genuinely quantifies over every subset. The Shapley value's coefficient is the exact rational weight S.card.factorial * (n - S.card - 1).factorial / n.factorial cast to ℝ, not a placeholder constant. The greedy algorithm's InitialCoalition σ j uses Lean's 0-indexed Equiv.Perm (Fin n) throughout, with the book's 1-indexed $S_\pi(j)$ absorbed into the definition rather than into the index j, so the definition and the goal read the same j consistently. Theorem 5.2.7(c), which needs Theorem 5.2.4's convex-combination-of-extreme-points machinery beyond this section, is out of scope for this mission.

A trivializing formalization would state acceptability only on singleton coalitions, or would let n = 0/an empty player set stand in for the general case; neither is used here — every Core/IsLargeCore statement quantifies over arbitrary subsets, and none of the theorems restrict n.

This mission reuses Supermodularity.Monotonicity.SupermodularOn and Supermodularity.Monotonicity.IncreasingDifferencesOn from this series's chunk II (02-monotonicity) rather than restating supermodularity or increasing differences for coalitions from scratch. InitialCoalition, Core, GreedyPayoff, IsConvexGame, IsLargeCore, IsTotallyLargeCore and ShapleyValue are new to this mission and reusable by any later mission on cooperative games, polymatroids, or the polyhedral structure of the core (Section 5.2.3 of this chapter). Contributions completing the sorrys — Theorem 5.2.1(a)'s chain-splitting argument, Theorem 5.2.6's auxiliary-function construction, and Theorem 5.2.7(a,b)'s direct comparison — are all welcome.

Selected references

• L. S. Shapley, "Cores of convex games," International Journal of Game Theory, 1(1), 1971, 11–26. https://doi.org/10.1007/BF01753431
• L. S. Shapley, "A value for n-person games," in Contributions to the Theory of Games II, Princeton University Press, 1953, 307–317.
• H. Moulin, "Cores and large cores when population varies," International Journal of Game Theory, 19(3), 1990, 219–232. https://doi.org/10.1007/BF01766437
• W. W. Sharkey, "Cooperative games with large cores," International Journal of Game Theory, 11(3-4), 1982, 175–182. https://doi.org/10.1007/BF01766193
• D. M. Topkis, "Activity optimization games with complementarity," European Journal of Operational Research, 28(3), 1987, 358–368. https://doi.org/10.1016/0377-2217(87)90232-5
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011, Chapter 5. https://doi.org/10.1515/9781400822539

Motivation

Which workers end up at which firms, and does higher quality always land at the more productive employer? This is the question of assortative matching: whether an efficient assignment pairs the best workers with the best firms, the second-best with the second-best, and so on down the line. The question has a long history in labor economics. Becker [1973] showed, for the simplest case of two-sided homogeneous firms and a single worker characteristic, that profit maximization under complementarity forces exactly this kind of sorting. Kremer [1993] extended the analysis to firms with many workers of a single type, under a specific Cobb–Douglas production function. What was missing was a general theory: one that covers firms hiring several types of workers simultaneously, firms that differ in efficiency, and labor markets of any degree of tightness, while still deriving sorting from a single primitive economic condition rather than from functional-form assumptions.

Topkis's Chapter 3, §3.2 supplies exactly that theory, as an application of the book's central tool — supermodularity — to the assignment problem. The condition that drives every result in this mission is a single complementarity hypothesis on the firms' profit functions: no concavity, no differentiability, no specific functional form. That a purely order-theoretic hypothesis pins down the qualitative shape of an optimal assignment is the mission's central content, and the platform currently has no lattice-theoretic treatment of matching at all — its one matching result formalizes Gale–Shapley two-sided stable matching by preference, an entirely different mechanism (see Formalization scope below).

Setting

Fix $n$ worker types, indexed $i = 1,\dots,n$, each with a lattice $X_i$ of available worker qualities, and $m$ firms, indexed $j = 1,\dots,m$. A matching assigns to each firm $j$ a vector of qualities $x^j = (x^j_1,\dots,x^j_n) \in \prod_{i=1}^n X_i$ — one worker of each type hired by that firm (a firm that hires no worker of some type, or several, is accommodated by adjoining an artificial "no worker" element to $X_i$, or by splitting a type into several, as Topkis notes on p. 97; the model itself needs neither device). If firm $j$ hires the quality vector $x$, it earns profit $f(x,j) \in \mathbb{R}$; the dependence on $j$ reflects differences among firms such as technology or management efficiency. A matching is optimal if it maximizes the total profit $\sum_{j=1}^m f(x^j,j)$ over every matching.

A matching is increasing if $x^1 \preceq x^2 \preceq \cdots \preceq x^m$ — a single chain, firm by firm, under the pointwise order on $\prod_i X_i$ — and ordered if every two of its firm-assignments are comparable (a weaker, only pairwise, condition). The labor market is loose if each firm's hiring problem can be solved by unconstrained maximization over the whole quality space $\prod_i X_i$, without regard to the other firms' decisions, and tight if the supply of each worker type is exactly $m$, so a feasible matching must assign every available worker to exactly one firm.

The hypothesis common to every result is that $f(x,j)$ is supermodular in the joint variable $(x,j)$ on $\bigl(\prod_i X_i\bigr) \times \{1,\dots,m\}$: for every $(x,j)$ and $(x',j')$, $f(x,j) + f(x',j') \le f(x\vee x', j\vee j') + f(x\wedge x', j\wedge j')$. By Theorem 2.6.1 of Chapter 2, this is equivalent to $f$ having increasing differences both between any two worker types' qualities (complementarity among the worker types) and between each worker type's quality and the firm index (complementarity between quality and firm efficiency).

Formalization targets

Goal — Theorem 3.2.3

$$f \text{ supermodular in } (x,j) \text{ on } \Bigl(\textstyle\prod_{i=1}^n X_i\Bigr)\times\{1,\dots,m\} \ \Longrightarrow\ \exists\, x \text{ increasing and optimal.}$$ $$\text{If, in addition, the labor market is tight, every increasing (tight) matching is optimal.}$$

Existence of an increasing optimal matching, with no loose-market hypothesis — the general case, and the harder of this mission's results to formalize, since its proof is a non-constructive lexicographic-minimization argument rather than a direct reduction to per-firm optimization.

Supporting milestones

• Theorem 3.2.1 (the loose case): under an unconstrained labor market, each firm's set of optimal hiring decisions is increasing in the firm index with respect to the induced set ordering, and an increasing optimal matching exists — proved directly from Chapter 2's monotone-comparative-statics theorems (mission II of this series).
• Theorem 3.2.4: joint supermodularity in $(x,j)$ together with strict supermodularity in $x$ alone, for each fixed $j$, forces every optimal matching to be ordered.
• Theorem 3.2.5: joint strict supermodularity in $(x,j)$ forces every optimal matching to be increasing, the stronger of the two conclusions.

Significance

The result gives a clean, hypothesis-light account of assortative matching: sorting by quality is a structural consequence of complementarity in the profit function, not an artifact of a particular production technology. It generalizes Becker's and Kremer's special cases to arbitrarily many worker types, heterogeneous firms, and any degree of labor-market tightness, identifying supermodularity in $(x,j)$ as the single condition doing all the work. Formalizing it contributes a genuinely new object to the platform: a firm-quality matching model driven by lattice-theoretic complementarity rather than by preference orderings, together with the four distinct comparative-statics conclusions (loose-market optimality, general existence, orderedness, increasingness) that the strength of the supermodularity hypothesis buys. No prior formalized proof of any of these four theorems exists on the platform or, to the author's knowledge, in any other proof assistant library.

Difficulty

The obvious approach — prove the goal (Theorem 3.2.3) by reducing to the loose case, firm by firm, as in Theorem 3.2.1 — does not work, because the loose-market argument crucially uses that each firm's decision does not constrain any other's; without that, a locally optimal per-firm choice need not combine into a globally optimal matching. Topkis's actual proof is non-constructive: among all optimal matchings, pick one that lexicographically minimizes the "latest" failure of the increasing property (a well-ordering argument over the finite but unbounded set of optimal matchings, not an inequality chase), then show that if it still fails to be increasing, exchanging the two offending firms' assignments via $\vee,\wedge$ strictly increases total profit — contradicting optimality by supermodularity. Formalizing this requires setting up the lexicographic minimization (over pairs $(j,i)$ ordered by $j$ then $i$) as a well-founded induction, not merely restating the inequality (3.2.3) at the end of the proof.

Formalization scope

Worker-type quality spaces $X_i$ are modeled as finite, nonempty lattices (Lattice, Fintype, Nonempty); firms are indexed by Fin m. A matching is Fin m → ∀ i, X i with no constraint beyond membership — the general matching problem (3.2.1) imposes no injectivity or supply constraint on its own, a modeling choice Topkis's own text supports (p. 96: the "$\{x^1_i,\dots,x^m_i\}\subseteq X_i$" representation of a matching "may not distinguish between all distinct assignments of workers to firms if the qualities of different workers of any given type are not all distinct, but that ambiguity is inconsequential"). Tightness is instead formalized as an explicit feasibility predicate (a bijection between firms and the $m$ available workers of each type) supplied as a hypothesis exactly where a tight-market theorem needs it, never folded into the general optimality predicate.

A trivializing formalization to avoid: collapsing Theorem 3.2.4's "ordered" conclusion and Theorem 3.2.5's "increasing" conclusion into the same statement, or conflating their two distinct supermodularity hypotheses (joint-non-strict-plus-per-firm-strict versus jointly strict) — the mission's four milestones are kept as four genuinely different claims with their own hypotheses, not variations proved once and restated. AGT.stable_matching_exists (Gale–Shapley) is not reused here, despite the shared word "matching": it produces a two-sided, preference-based stable matching with no notion of aggregate profit, a mechanism unrelated to this mission's profit-maximizing, supermodularity-driven assignment.

Reused from earlier missions in this series: the induced set ordering InducedSetOrder (mission I) and joint supermodularity SupermodularOn (mission II), both published platform definitions. Contributions most welcome on the goal theorem's lexicographic-minimization argument, the mission's hardest step.

Selected references

• G. S. Becker, A Theory of Marriage: Part I, Journal of Political Economy 81 (1973), 813–846. https://doi.org/10.1086/260084
• M. Kremer, The O-Ring Theory of Economic Development, Quarterly Journal of Economics 108 (1993), 551–575. https://doi.org/10.2307/2118400
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 2011 (orig. 1998). https://doi.org/10.1515/9781400822539

Motivation

Composite convex programs — objectives split into a smooth piece and a nonsmooth piece — are ubiquitous in data analysis: LASSO-type inverse problems, regularized empirical-risk minimization, and total-variation-type image reconstruction all minimize $f(x)+h(x)+\chi(x)$ over a convex set, where $f$ is smooth (a data-fidelity term, often expensive to differentiate — a large matrix-vector product, a PDE solve, a black-box simulation), $h$ is nonsmooth but structurally cheap (an $\ell_1$-type penalty, a simple subgradient), and $\chi$ enforces a "relatively simple" constraint absorbed into the proximal step. Classical accelerated proximal-gradient methods (Nesterov; Beck–Teboulle) solve such problems by computing $\nabla f$ and a subgradient $h'$ once per iteration, giving an optimal $O(1/\varepsilon^2)$ bound on evaluations of both. But in every example above, the two oracle calls have wildly different costs, and paying for $\nabla f$ as often as for $h'$ is wasteful. Ghadimi, Lan and Zhang (SIAM J. Optim., 2014, arXiv:1406.5613, "Generalized Uniformly Optimal Methods for Nonlinear Programming") posed the resulting question: given separate first-order access to $f$ and $h$, can the number of $\nabla f$-evaluations be reduced without inflating the (already-optimal) number of $h'$-evaluations? The gradient sliding (GS) algorithm formalized here, from Lan's textbook treatment (Chapter 8, building on Lan's own 2016 Mathematical Programming paper "Gradient sliding for composite optimization"), answers this in the affirmative: it "slides" past $\nabla f$-evaluations on most iterations while still achieving the optimal $O(1/\varepsilon^2)$ subgradient count for $h'$.

Setting

Fix a real inner-product space $E$ and a closed convex set $X\subseteq E$. The composite problem is

$$\Psi^* \equiv \min_{x\in X}\{\Psi(x) := f(x)+h(x)+\chi(x)\}, \qquad (8.1.1)$$

where $\chi$ is a "relatively simple" convex function (its own proximal step is assumed cheap), $f:X\to\mathbb R$ is convex with $L$-Lipschitz gradient,

$$f(x)\le f(y)+\langle\nabla f(y),x-y\rangle+\tfrac L2\|x-y\|^2, \qquad \forall x,y\in X, \quad (8.1.2)$$

and $h:X\to\mathbb R$ is convex and $M$-Lipschitz-like in the sense that for every subgradient $h'(y)\in\partial h(y)$,

$$h(x)\le h(y)+\langle h'(y),x-y\rangle+M\|x-y\|, \qquad \forall x,y\in X. \quad (8.1.3)$$

Let $V(a,b)$ be a Bregman-type prox-function built from a 1-strongly-convex distance-generating function $\nu$ (Sect. 3.2), so $V(a,b)\ge\tfrac12\|b-a\|^2$.

The gradient sliding (GS) algorithm (Algorithm 8.1) keeps an outer iterate $x_k$, model point $g_k(\cdot)\equiv l_f(x_k,\cdot):=f(x_k)+\langle\nabla f(x_k),\cdot-x_k\rangle$, and running average $\bar x_k$ ($\bar x_0=x_0$). Each outer step $k=1,\dots,N$ delegates to the prox-sliding (PS) procedure: given the affine model $g_k$, prox-center $x_{k-1}$, parameter $\beta_k$, and sliding length $T_k$, PS runs $T_k$ inner iterations

$$u_t = \arg\min_{u\in X}\{g(u)+l_h(u_{t-1},u)+\beta V(x,u)+\beta p_tV(u_{t-1},u)+\chi(u)\}, \qquad \tilde u_t = (1-\theta_t)\tilde u_{t-1}+\theta_tu_t, \quad (8.1.17)\text{--}(8.1.18)$$

where $l_h(y;u):=h(y)+\langle h'(y),u-y\rangle$ (8.1.14), without ever recomputing $\nabla f$ during these $T_k$ steps — the single affine model $g$ is reused throughout. This is the mechanism by which GS "slides" past most $\nabla f$-evaluations. PS returns $(x_k,\tilde x_k)$, and the outer loop updates $\bar x_k=(1-\gamma_k)\bar x_{k-1}+\gamma_k\tilde x_k$.

Formalization targets

Building block (Proposition 8.1)

$$\beta(1-P_t)^{-1}V(u_t,u)+[\Phi(\tilde u_t)-\Phi(u)] \le P_t(1-P_t)^{-1}\Big[\beta V(u_0,u)+ \frac{M^2}{2\beta}\sum_{i=1}^t(p_i^2P_{i-1})^{-1}\Big], \quad \forall u\in X, \, t\ge1,$$

where $\Phi(u):=g(u)+h(u)+\beta V(x,u)+\chi(u)$ and $\{p_t\},\{\theta_t\},\{P_t\}$ satisfy the recursion (8.1.20). This is the per-inner-iteration guarantee on how close $(u_t,\tilde u_t)$ comes to solving $\Phi$'s own minimization.

Intermediate (Theorem 8.1(a))

Assuming the PS schedule (8.1.20) and GS schedule conditions (8.1.25), (8.1.33) (the case where $X$ may be unbounded),

$$\Psi(\bar x_N)-\Psi(x^*) \le \frac{\Gamma_N\beta_1}{1-P_{T_1}}V(x_0,x^*) + \frac{M^2\Gamma_N}{2}\sum_{k=1}^N\sum_{i=1}^{T_k}\frac{\gamma_kP_{T_k}} {\Gamma_k\beta_k(1-P_{T_k})p_i^2P_{i-1}}, \qquad \forall N\ge1,$$

a general bound in terms of the abstract schedule, obtained by telescoping Proposition 8.1's guarantee (via Proposition 8.2's per-outer-step recursion, cited but not restated here) across outer iterations.

Goal (Corollary 8.1(a))

With the concrete schedule $p_t=t/2$, $\theta_t=2(t+1)/(t(t+3))$ (8.1.39), and, for a fixed horizon $N$ and free parameter $\tilde D>0$,

$$\beta_k=\frac{2L}{k}, \qquad \gamma_k=\frac2{k+1}, \qquad T_k=\Big\lceil\frac{M^2Nk^2}{\tilde DL^2}\Big\rceil, \quad (8.1.40)$$ $$\Psi(\bar x_N)-\Psi(x^*) \le \frac{2L}{N(N+1)}\big[3V(x_0,x^*)+2\tilde D\big], \qquad \forall N\ge1. \quad (8.1.41)$$

This is the explicit-constant complexity bound: it is the weakest statement stable under changing $L,M,N,\tilde D$, obtained purely algebraically from Theorem 8.1(a)'s general bound once the schedule is plugged in.

Significance

Corollary 8.1(a), together with the schedule of $T_k$, shows the total number of outer iterations — and hence $\nabla f$-evaluations — needed for an $\varepsilon$-solution is $O(L/ \varepsilon)$, matching the optimal rate for smooth-only minimization (no penalty for the nonsmooth term's presence), while the total number of inner iterations $\sum_kT_k$ — and hence $h'$-evaluations — remains $O(1/\varepsilon^2)$, the rate that is already known to be unimprovable for nonsmooth convex minimization. GS is thus the first method (per the section's own account) to decouple the two oracle costs at their respective optimal rates, rather than paying the worse of the two for both. This underlies later chapters' extensions (accelerated gradient sliding, decentralized optimization over networks) and is directly applicable whenever a composite objective's two components have asymmetric evaluation cost, as in the LASSO-type and regularized-loss examples above. Formalizing it contributes a machine-checked account of the telescoping/recursion argument across two nested loops (outer GS, inner PS) — a pattern distinct from the single-loop accelerated-gradient arguments already in this series (Chapters 3, 7) and not otherwise present in the corpus (q=gradient sliding, q=prox sliding, q=composite optimization all return zero hits as of 2026-09-18).

Difficulty

The obvious first idea — treat the PS procedure's inexact inner solve as adding an error term to a standard accelerated-gradient argument and bound that error by the number of inner steps — fails because a naive termination criterion (the function-value optimality gap of the PS subproblem) does not yield the accelerated rate; the book's own analysis (the paragraph preceding Proposition 8.1) states this explicitly. The working criterion instead combines the optimality gap and the distance to the optimal solution, weighted by the $P_t$-sequence — this is exactly the left-hand side of (8.1.21), not a simpler quantity, and it is this specific combination that telescopes cleanly across both the inner PS loop and, subsequently, the outer GS loop.

Formalization scope

E is NormedAddCommGroup E, InnerProductSpace ℝ E; X : Set E. The Bregman divergence V, model function g/lh, and constraint function chi are hypothesis-carrying objects (functions with the defining (in)equalities as hypotheses), matching this series' convention rather than fixing them to the Euclidean/entropic special case. ps_procedure_bound (Proposition 8.1) takes the three-point inequality that the argmin in (8.1.17) yields (a standard consequence of Lemma 3.5, cited but not re-derived) as an explicit hypothesis on the sequence u, rather than proving well-posedness of the argmin itself. gs_convergence_bound (Theorem 8.1(a)) similarly takes Proposition 8.2's per-outer-step recursion (8.1.26) as a hypothesis — its own proof composes Proposition 8.1 with model-function inequalities (8.1.27)-(8.1.31) that are outside this mission's selected scope — and formalizes only part (a) (unbounded X), not part (b) (compact X, reverse monotonicity), since only (a) is on the goal's dependency path. explicit_gs_rate (Corollary 8.1(a)) uses the closed forms $P_t=2/((t+1)(t+2))$ and $\Gamma_k=2/(k(k+1))$ that the specific schedule (8.1.39)-(8.1.40) produces (8.1.44, 8.1.46 — cited, not restated), rather than the general recursion, and takes Theorem 8.1(a)'s bound, specialized to this schedule, as a hypothesis: its own content is the purely algebraic simplification (8.1.45)-(8.1.48) into the closed-form bound (8.1.41), not a re-derivation of the general theorem. The source PDF's own printed $\beta_k=2L/(\nu k)$ (8.1.40) is a text-extraction artifact (no such $\nu$-indexed quantity appears anywhere in this section); the proof's own algebra ($\gamma_k\beta_k/(\Gamma_k(1-P_{T_k}))=2L/(1-P_{T_k})$, using $\Gamma_k=2/(k(k+1))$, $\gamma_k=2/(k+1)$) is consistent only with $\beta_k=2L/k$, which is what is formalized. A trivializing formalization would fix $h\equiv0$ or $\chi\equiv0$, collapsing the composite problem to plain smooth minimization and making the entire PS-procedure apparatus vacuous; this is ruled out by keeping $h$ and $\chi$ as free convex functions throughout with hMLip an active, non-degenerate hypothesis. Proposition 8.2 (the recursion gs_convergence_bound cites) and Theorem 8.1(b) (the compact-X case) are natural extensions a further contribution could add.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, 2020, Chapter 8. https://doi.org/10.1007/978-3-030-39568-1
• G. Lan, Gradient sliding for composite optimization, Mathematical Programming 159 (2016), 201–235. https://doi.org/10.1007/s10107-015-0955-5
• S. Ghadimi, G. Lan, H. Zhang, Generalized Uniformly Optimal Methods for Nonlinear Programming, Journal of Scientific Computing, 2019 (arXiv preprint 2015). arXiv:1406.5613

Motivation

Online convex optimization (OCO) asks a learner to repeatedly pick a point in a convex set $K$, pay a cost that an adversary reveals only after the choice is made, and be judged against the best fixed point in hindsight. Chapter III of this series formalized the simplest general-purpose answer, online gradient descent (OGD): take a gradient step, project back onto $K$. OGD's analysis, however, is tied to the Euclidean geometry of the projection step — it treats every coordinate of $K$ alike, and its regret bound degrades badly when $K$'s natural geometry is not Euclidean (the probability simplex under the $\ell_1$ norm is the standard example, where a Euclidean-projection algorithm's regret scales with $\sqrt{n}$ in the dimension $n$, while an algorithm that exploits the simplex's own geometry attains regret scaling only with $\sqrt{\log n}$).

Regularized Follow the Leader (RFTL) is the meta-algorithm this chapter introduces to fix this: rather than fixing a specific geometry, RFTL is parameterized by an arbitrary regularization function $R$, and its regret bound depends on $R$ only through two scalar quantities the mission makes explicit — the range of $R$ over $K$, and a $R$-dependent "local norm" of the gradients. Choosing $R$ to match $K$'s geometry (entropy regularization on the simplex, for instance) recovers the sharp bounds that plain OGD cannot. RFTL and its close relative Online Mirror Descent (OMD), also introduced here, are the ancestors of essentially every regularization-based online learning algorithm in use today, including the multiplicative-weights/Hedge algorithm of Chapter I as a special case (entropy regularization on the simplex) and the exponentiated-gradient algorithm this book's own Chapter VIII reuses (Corollary 5.7, a further specialization of Theorem 5.2 this mission's Theorem 5.2 underlies). The naive "Follow the Leader" strategy this chapter opens by refuting — always play the empirically best point so far — is a natural first idea and provably fails: the book gives an explicit two-point cost sequence on which it incurs regret linear in the horizon. Regularization is the fix, and quantifying exactly how much it costs and buys is this chapter's content.

Setting

Fix a convex, nonempty decision set $K$ in a real inner product space $E$ and a sequence of convex cost functions $f_1, f_2, \dots : K \to \mathbb{R}$. As in Chapter III, regret after $T$ rounds is

$$\mathrm{Regret}_T = \sum_{t=1}^{T} f_t(x_t) - \min_{x^\star \in K} \sum_{t=1}^{T} f_t(x^\star).$$

A regularization function $R : K \to \mathbb{R}$ is a strongly convex, smooth, twice differentiable function with a positive-definite Hessian on the interior of $K$. Its Bregman divergence measures the gap between $R$ and its own first-order Taylor approximation:

$$B_R(x \| y) = R(x) - R(y) - \nabla R(y)^\top(x - y).$$

By the mean value theorem, $B_R(x\|y) = \tfrac12\|x-y\|_z^2$ for some point $z$ on the segment $[x,y]$, where $\|\cdot\|_z$ is the norm induced by the Hessian $\nabla^2 R(z)$; its dual norm, denoted $\|\cdot\|_z^*$, is the local norm at $z$. Writing $\|\cdot\|_t$ for the local norm between consecutive iterates $x_t, x_{t+1}$, the $R$-diameter of $K$ is $D_R^2 = \max_{x,y\in K}(R(x)-R(y))$.

The RFTL algorithm (Algorithm 13), with step size $\eta > 0$, plays $x_1 = \arg\min_{x\in K} R(x)$, then at every round updates

$$x_{t+1} = \arg\min_{x \in K}\Big\{\eta \sum_{s=1}^{t} \nabla_s^\top x + R(x)\Big\}, \qquad \nabla_t := \nabla f_t(x_t).$$

The agile Online Mirror Descent algorithm (Algorithm 14, agile version) instead maintains a dual point $y_t$ with $\nabla R(y_1) = 0$, updates it by $\nabla R(y_{t+1}) = \nabla R(x_t) - \eta \nabla_t$, and projects via the Bregman divergence, $x_{t+1} = \arg\min_{x\in K} B_R(x\|y_{t+1})$ (with $x_1$ defined the same way from $y_1$). RFTL and the lazy variant of OMD coincide for linear costs (Lemma 5.5, not formalized here — it is not used by either target); the agile variant's analysis is genuinely different and is the mission's second target.

Formalization targets

Target (Theorem 5.2 — RFTL's regret bound)

$$\mathrm{Regret}_T \;\le\; 2\eta \sum_{t=1}^{T} \|\nabla_t\|_t^{*2} \;+\; \frac{R(u) - R(x_1)}{\eta}, \qquad \text{for every } u \in K.$$

This is the mission's goal: RFTL, run with any admissible regularizer, attains a regret bound governed only by the cumulative squared local norm of the gradients and $R$'s range over $K$. The bound is proved via two milestones: Lemma 5.3 (regret controlled by the total "prediction drift" $\sum_t \nabla_t^\top(x_t - x_{t+1})$ plus $D_R^2/\eta$), which in turn rests on Lemma 5.4 (a "follow-the-leader beats be-the-leader" comparison inequality, proved by induction on the horizon).

Further target (Theorem 5.6 — agile OMD's regret bound)

$$\mathrm{Regret}_T \;\le\; \frac{\eta}{4} \sum_{t=1}^{T} \|\nabla_t\|_t^{*2} \;+\; \frac{R(u) - R(x_1)}{2\eta}, \qquad \text{for every } u \in K.$$

A structurally similar bound for the agile variant, included as its own goal-level item since — as the book states explicitly — its proof technique is unrelated to RFTL's, not a corollary of it.

Both targets are the book's own tightest, non-asymptotic statements: neither is weakened to an $O(\cdot)$ form, and the book's own further (unnumbered) corollary specializing Theorem 5.2 to a uniform local-norm bound $\|\nabla_t\|_t^* \le G_R$ is left out, matching this series' convention of formalizing only the numbered results.

Significance

The results themselves. Theorem 5.2 is the general regret theorem behind every regularization scheme in online learning: instantiating $R$ recovers the projected-gradient bound of Chapter III (Euclidean $R$), the multiplicative-weights bound of Chapter I (entropy $R$ on the simplex), and — through the exponentiated-gradient specialization (Corollary 5.7, not itself a target here) — the row-player regret bound this book's own Chapter VIII cites as "Eq. (8.1)" in its reduction of zero-sum games to regret minimization. Theorem 5.6 gives the same guarantee for an algorithm (agile OMD) that, unlike RFTL, maintains a feasible point at every round, which the book notes is preferable in the adaptive-regret setting of Chapter X.

Formalizing it. Both theorems have complete, elementary proofs in the source (no gaps, no "with high probability", no hidden regularity conditions); the mission's work is converting the analytic argument — the Bregman-divergence identity, the generalized Cauchy-Schwarz inequality bounding the drift term by the local norm, and the two induction arguments underlying Lemma 5.4 — into machine-checked statements. No formalization of RFTL, OMD, or the local-norm machinery exists on the platform (checked below); the closest Formalpedia entries state a related but distinctly narrower result.

Difficulty

The central obstacle is that the regularizer $R$ is a hypothesis, not a fixed function: the theorem must hold for every admissible $R$ simultaneously, so nothing about $R$ beyond its stated properties (strong convexity, smoothness, twice differentiability) may be used. A newcomer's first instinct — bound the local norm $\|\nabla_t\|_t^*$ by a fixed multiple of the Euclidean dual norm $\|\nabla_t\|_2$ — fails in general and is exactly the bound RFTL is designed to avoid needing; the whole point of the local-norm formulation is that it can be tight for regularizers (like entropy) whose Hessian is very far from a multiple of the identity. A second obstacle is Lemma 5.4's induction, which compares $x_{t+1}$ (a minimizer over $t+1$ terms) against $u$ using the minimality of $x_{t+1}$ at exactly the right instantiation — an argument that looks almost circular until the induction hypothesis is applied at $u = x_{t+2}$, not at the theorem's free variable.

Formalization scope

$K$ ranges over an arbitrary real, complete inner product space (a real Hilbert space), matching Chapters III and IV, not a fixed $\mathbb{R}^n$. The RFTL and agile-OMD update rules are represented relationally (IsArgMinOn), since Mathlib has no canonical argmin operator for a general convex set — mirroring IsMetricProjection's precedent from Chapter III. The Hessian at the mean-value-theorem's intermediate point is represented via the second Fréchet derivative of $R$'s gradient map (HasFDerivAt), since Mathlib has no dedicated Hessian type; the local dual norm is then any value satisfying the resulting existential characterization (IsLocalDualNormSq), stated once and shared by both targets. A boundedness hypothesis on $R$ over $K$ is added to Lemma 5.3's statement to keep the $R$-diameter $D_R^2$ from collapsing to Mathlib's junk value for an unbounded supremum — a condition every regularizer the book actually uses (strongly convex and smooth over a bounded $K$) already satisfies, so it narrows nothing.

Trivializing formalization ruled out. A regret bound stated for an "algorithm" defined loosely enough to include the after-the-fact optimal choice would be vacuous; IsRFTLRun and IsOMDAgileRun instead pin down the exact history-dependent update rule of Algorithms 13 and 14 (the current gradient sequence, the current regularizer, and nothing else) as a hypothesis, so a proof must genuinely use the specific update. Theorem 5.2 and Theorem 5.6 are kept as two separate items rather than one theorem parameterized by an algorithm choice, since — per the chapter's own remark that their analyses are unrelated — a merged statement would either need to branch internally on the algorithm or silently identify two genuinely different update rules.

Reuse and prior art. OnlineConvexOpt.FirstOrder.RegretT (Chapter III, published) is imported and reused verbatim, keeping the regret functional identical across the whole book. Definitions specific to Chapter IV (OnlineConvexOpt.SecondOrder, not yet published) are not imported per this series' convention that a draft cannot import another draft; quadForm is redeclared locally instead. On the platform, BanditAlgorithm.ftrl_regret_bound, BanditAlgorithm.mirror_descent_regret_bound, and BanditAlgorithm.ftrl_simplex_exp_weights_regret (the Bandit Algorithms series, Chapter XII) state regret bounds for FTRL and Mirror Descent in the linear-cost, bandit-idiom setting (a fixed linear loss $\langle a, y_t\rangle$ at each round, regret compared via a Bregman-divergence potential at fixed points). Hazan's Theorem 5.2 and 5.6 are for general convex $f_t$ and use the book's own local-norm object, which has no counterpart in those statements; they are read in full and are not faithful substitutes (different hypothesis class), so this mission drafts its own, independent items rather than reusing them.

Selected references

• Hazan, Introduction to Online Convex Optimization, 2nd ed., Chapter 5. arXiv:1909.05207v3
• Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning, 2012 (surveys RFTL/Mirror Descent under the name "Online Mirror Descent"). https://doi.org/10.1561/2200000018
• Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003 (the Euclidean special case this chapter generalizes). https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf