Optimization

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$. Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$-divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$, keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$-Lipschitz on a convex set $\Theta$ for every $x$, and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$.

For a radius $\rho\ge0$, the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

$$\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},$$

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$.

For $\epsilon\ge0$ the $\epsilon$-suboptimal sets of the risk and of the robust risk are

$$S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},$$

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$,

$$R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}$$

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$, with independent uniform signs $\varepsilon_i\in\{\pm1\}$.

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$, $\rho\ge0$, and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

$$\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}$$ $$\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.$$

Milestones, in attack order

1. Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$.
2. Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$.
3. Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$, the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$.
4. Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$.
5. Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$.

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$-dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$, which for quadratic growth ($\gamma=2$) is $\rho/n$, the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$-approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$, which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$, to every $2\epsilon$-suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$, and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ($R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$). Each supremum "$\sup\ge c$" is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$, as printed.

Corrections and presuppositions:

• $\epsilon>0$. The paper prints $0\le\epsilon$. At $\epsilon=0$, $\rho=0$, both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$. The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$.
• $S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
• Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$, $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$, or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

Why revenue sharing

A supplier who sells to an independent retailer through a plain per-unit wholesale price faces double marginalization: the retailer orders less than the quantity that maximizes the profit of the supply chain as a whole, because each unit costs him the wholesale price rather than the production cost. Supply chain contracting studies payment schemes under which the retailer's own optimum coincides with the system optimum. Such a scheme is said to coordinate the channel. The usual examples are buy-back contracts (Pasternack, 1985), quantity-flexibility contracts (Tsay and Lovejoy, 1999) and quantity discounts (Jeuland and Shugan, 1983; Moorthy, 1987).

Cachon and Lariviere study revenue sharing, in which the retailer pays a low wholesale price and also hands over a fixed fraction of his revenue. The scheme was common in video-cassette rental in the late 1990s, where it let rental chains stock far more copies of new releases. This mission formalizes the paper's single-retailer result: revenue sharing coordinates the channel, and the supplier can choose any split of the channel's maximal profit. It also includes the three further results of the paper that use the same argument.

The source is the authors' working paper of June 2000. Its results are unnumbered, so every item cites a section, a displayed equation and a printed page. The 2005 Management Science version renumbers and revises the material.

Setting

A supplier sells to one retailer, who orders $q \ge 0$ units before a selling season. The retailer's expected revenue is a function $R(q)$ of the quantity alone. Leftover units have zero salvage value, and the supplier produces each unit at cost $c > 0$. The paper's standing assumptions (Sec. 1, p. 5) are:

• $R$ is strictly concave and differentiable for $q \ge 0$, with marginal revenue $R'(q)$;
• the product is viable: $R'(0) > c$;
• a finite quantity is optimal: $R'(\infty) < c$.

A revenue-sharing contract $\{\phi, w\}$ has two terms. The retailer pays the wholesale price $w \ge 0$ per unit, and he keeps the share $\phi$ of the revenue and transfers $(1-\phi)R(q)$ to the supplier. The case $\phi = 1$ is the plain wholesale-price contract. The profits of the supply chain, the retailer and the supplier are

$$\Pi(q) = R(q) - qc,\qquad \pi_r(q) = \phi R(q) - qw,\qquad \pi_s(q) = (1-\phi)R(q) + qw - qc .$$

The integrated channel quantity $q_I$ is the maximizer of $\Pi$ over $q \ge 0$. In Lean these objects are RevShareCoord.Single.Model (fields R, R', c and the three assumptions) and its functions Pi, retailerProfit and supplierProfit.

Formalization targets

Goal: revenue sharing coordinates the channel (Sec. 2.2, p. 6)

Let $\phi \in (0,1]$ and $w(\phi) = \phi c$. Then

$$q_I = \operatorname*{arg\,max}_{q\ge 0}\ \pi_r(q) \ \text{(uniquely)},\qquad w(\phi)\le c,\qquad \pi_r(q_I) = \phi\,\Pi(q_I),\qquad \pi_s(q_I) = (1-\phi)\,\Pi(q_I).$$

The statement fixes no revenue function and no share. It holds for every model and every $\phi \in (0, 1]$, which is what "the supplier can take any share of the channel profit" means.

Milestones on the way

1. Eq. (1), p. 6. $q_I$ exists, is unique and positive, and is the only positive root of $R'(q_I) = c$.
2. Retailer's first-order condition, p. 6. If $R'(0) > w/\phi$, an order $\hat q \ge 0$ is optimal for the retailer exactly when $\hat q > 0$ and $\phi R'(\hat q) = w$. The retailer has at most one optimal order.
3. Profit identities, p. 6. Under $\{\phi, \phi c\}$, $\pi_r(q) = \phi\Pi(q)$ and $\pi_s(q) = (1-\phi)\Pi(q)$ at every $q$.
4. Heterogeneous retailers, p. 7. Given $c$ and $\phi$, a single wholesale price, chosen before the revenue function, coordinates every retailer of the model.

Further results on the same argument

5. Buy-back equivalence, Sec. 2.3, p. 9. Take the fixed-price newsvendor and the buy-back contract $b^* = p(1-\phi)$, $w_b^* = p(1-\phi)+\phi c$. It gives the retailer and the supplier the same realized profits as $\{\phi, \phi c\}$, for every order and every demand realization.
6. Endogenous price, Sec. 3.1 and footnote 3, p. 11. Let revenue $\mathrm{Rev}(q,p)$ be any function of quantity and price, with costs linear in quantity. Then $\pi_r(q,p) = \phi\,\Pi(q,p)$ under $\{\phi,\phi c\}$, and the integrated optimum $(q_I,p_I)$, assumed unique, is the retailer's unique optimum.

Significance

The result separates coordination from profit division. A contract family coordinates for every value of a parameter, and that parameter then moves profit between the firms without changing the quantity, so the contract terms can be settled by bargaining power alone. The heterogeneous-retailer milestone gives the practical advantage over quantity discounts: the coordinating terms do not depend on the retailer's demand, so one price list serves retailers who face different markets. The Sec. 2.3 equivalence shows that, in the fixed-price newsvendor, buy-backs are a special case of revenue sharing. The Sec. 3.1 statement shows that revenue sharing still coordinates when the retailer also sets the price, a setting in which Emmons and Gilbert (1998) showed buy-backs fail.

All of these results are proved in the paper, and none is open. The mission adds a machine-checked version of the single-retailer theory for a general strictly concave revenue function. A related newsvendor version is already formalized on the platform: SupplyChainTheory.revenue_sharing_coordinates, from Snyder and Shen, Fundamentals of Supply Chain Theory, Thm 14.6. That version has a newsvendor revenue with salvage values and goodwill costs, and it concludes the optimality of three profits, not the $\phi$-split of this paper. It is a different statement, so it is not reused here.

Difficulty

The algebra is short. The identity $\pi_r = \phi\Pi$ under $w = \phi c$ is a single line, and it is a milestone, not the goal. The work lies in the optimization claims over a half-line with only one-sided information at $0$. The integrated optimum must be shown to exist. $R'(\infty) < c$ gives only an eventual bound on the derivative, so the existence argument needs the continuity of a concave function and its supergradient inequality. It must also be shown positive, which uses $R'(0) > c$ as a one-sided derivative. Its uniqueness rests on strict concavity. The retailer's first-order condition needs the same machinery for $\phi R - wq$, including the observation that the boundary point $0$ is never optimal. A stationary point of $\pi_r$ is not enough. The goal asserts that $q_I$ is the unique maximizer over all of $[0,\infty)$.

Formalization scope

• Quantities, prices and shares are real numbers. $R$ and $R'$ are functions $\mathbb R \to \mathbb R$, constrained only on $[0,\infty)$. Differentiability is HasDerivWithinAt R (R' q) (Set.Ici 0) q for $q \ge 0$, so it is one-sided at $0$. Strict concavity is StrictConcaveOn ℝ (Set.Ici 0) R.
• $R'(\infty) < c$ is encoded as "$R'(Q) < c$ for some $Q \ge 0$". For a decreasing $R'$ this is equivalent, and it allows $R' \to -\infty$.
• "Optimal" means IsMaxOn over $[0,\infty)$ (over $[0,\infty)\times P$ in Sec. 3.1), and "unique" means every other maximizer equals it.
• The supplier's profit $\pi_s$ is not displayed in the paper. It is read off the sequence of events of Sec. 1.
• The goal and the first-order condition take $\phi \in (0,1]$. At $\phi = 0$ the retailer's profit is identically zero and $q_I$ is not the unique optimum. The profit identities and the buy-back identities hold for all real parameters and are stated that way.
• Corrected slips. (a) Eq. (1) is introduced with "$R'(0) \ge c$". This contradicts the standing assumption $R'(0) > c$: with equality, $q_I = 0$ is not positive. The statement uses $R'(0) > c$. (b) The display $\pi_r(q_I) = \phi R(q_I) - q_I c = \phi\Pi(q_I)$ has a wrong middle term, which should read $\phi R(q_I) - q_I\phi c$. The outer equality is stated.
• The first-order-condition milestone adds the converse direction and uniqueness to the paper's "must satisfy". It does not claim that an optimum exists, which may fail when $w/\phi < c$.
• Sec. 3.1 is stated in the generality of footnote 3: an arbitrary revenue function $\mathrm{Rev}(q,p)$ and a set $P$ of admissible prices, with the integrated optimum's uniqueness as a hypothesis, as the paper assumes it. The paper's monotonicity of $F(x,p)$ in $p$ is unused and omitted.
• Sec. 2.3 is formalized pathwise. The expected-profit equations (2)–(4) are not part of the mission.
• A goal that only asserts $\pi_r(\phi, \phi c, q) = \phi\,\Pi(q)$ would be an unfolding of definitions. The goal therefore carries the argmax-and-uniqueness claim, which needs strict concavity and the model's assumptions.
• Needed infrastructure: first-order conditions for concave functions on a closed half-line with one-sided derivatives, and existence of maximizers from an eventual derivative bound. Both are reusable beyond this mission. Contributions of that general kind are welcome.

Selected references

• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, working paper, June 2000. Published version: Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• B. A. Pasternack, Optimal pricing and return policies for perishable commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• K. S. Moorthy, Managing channel profits: Comment, Marketing Science 6(4):375–379, 1987. https://doi.org/10.1287/mksc.6.4.375
• A. A. Tsay, W. S. Lovejoy, Quantity flexibility contracts and supply chain performance, Manufacturing & Service Operations Management 1(2):89–111, 1999. https://doi.org/10.1287/msom.1.2.89
• H. Emmons, S. M. Gilbert, Note: The role of returns policies in pricing and inventory decisions for catalogue goods, Management Science 44(2):276–283, 1998. https://doi.org/10.1287/mnsc.44.2.276
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Ch. 14. https://doi.org/10.1002/9781119584445

Motivation

Many problems in optimization and numerical analysis reduce to finding a point in the intersection of finitely many closed convex sets: solving a system of linear equations or inequalities, reconstructing an image from projections, or finding a feasible point of a convex program. The classical methods for this convex feasibility problem project the current point onto one set at a time, in Euclidean distance: Kaczmarz (1937) for linear equations, Agmon and Motzkin–Schoenberg (1954) for linear inequalities, and the cyclic projection method for general convex sets studied by Gubin, Polyak and Raik (1967).

L. M. Bregman's 1967 paper replaces the Euclidean distance by a general function $D(x,y)$ satisfying a short list of axioms, and shows that the projection method still works. The functions $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$ built from a strictly convex $f$ are the ones now called Bregman divergences, and the paper is the origin of Bregman projections, of the row-action methods of Censor and collaborators, and indirectly of mirror descent. Its §2 uses the abstract result to solve convex programs with linear constraints by relaxation.

This mission formalizes §1 of the paper for the cyclic control, in which the sets are visited in a fixed round-robin order. A companion mission treats the remotest-set control of Theorem 2, and two further missions treat the convex-programming results of §2.

Setting

Let $X$ be a real linear topological space and $A_0,\dots,A_{m-1}$ closed convex subsets of $X$, with intersection $R=\bigcap_i A_i$. Let $S\subset X$ be a convex set with $S\cap R\ne\emptyset$, and let $D:S\times S\to\mathbb R$. The paper requires:

• I. $D(x,y)\ge 0$, with equality if and only if $x=y$.
• II. For every $y\in S$ and every $i$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$; it is the $D$-projection of $y$ onto $A_i$.
• III. For every $i$ and $y\in S$, the function $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$.
• IV. $D(\cdot,y)$ has derivative $0$ at the point $y$.
• V. For every $z\in R\cap S$ and real $L$, the sublevel set $\{x\in S\mid D(z,x)\le L\}$ is compact.
• VI. If $D(x^n,y^n)\to 0$, $y^n\to y^*\in\bar S$, and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$.

The relaxation sequence with control $(i_n)$ starts at any $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. Under the cyclic control $i_n=n\bmod m$, the sets are projected onto in the order $A_0,A_1,\dots,A_{m-1},A_0,\dots$. A limiting point of $\{x^n\}$ is the limit of a convergent subsequence $x^{n_k}$.

The Lean development uses the namespace BregmanRelax.Cyclic: DConditions A S D P bundles conditions I–IV and VI together with the closedness and convexity of the sets, CondV S D Z is condition V for the points of $Z$, IsRelaxSeq S P i x is the relaxation sequence with control $i$, and cyclicControl hm is $n\mapsto n\bmod m$.

Formalization targets

Goal: Theorem 1 (p. 203)

Under conditions I–VI, with the cyclic control, every limiting point of every relaxation sequence lies in every set:

$$x^{n_k}\to x^* \quad\Longrightarrow\quad x^*\in\bigcap_{i=0}^{m-1}A_i .$$

The statement is about every starting point $x^0\in S$ and every convergent subsequence. It does not assert that the whole sequence converges.

Milestones

1. Lemma 1 (pp. 201–202): for $z\in A_i\cap S$ and $y\in S$,

$$D(P_iy,y)\le D(z,y)-D(z,P_iy).$$

2. Lemma 2 (2) (p. 202): for any control and any $z\in R\cap S$, $\lim_{n\to\infty}D(z,x^n)$ exists.
3. Lemma 2 (3) (p. 202): for any control, $D(x^{n+1},x^n)\to 0$.
4. Lemma 2 (1) (p. 202): for any control, $\{x^n\}$ lies in a compact set.

Further result: Note 1, condition (1) (pp. 204–205)

For any control whose relaxation sequence has all its limiting points in $R$ (the cyclic control, by Theorem 1), if in addition $S$ is closed and $y\mapsto D(z_1,y)-D(z_2,y)$ is continuous on $S$ for all $z_1,z_2\in R\cap S$, then the relaxation sequence converges to a point of $R$.

Significance

Theorem 1 is the abstract convergence theorem behind cyclic Bregman projections. With $D(x,y)=\|x-y\|^2$ in a Hilbert space it gives the convergence of cyclic orthogonal projections onto finitely many closed convex sets in the weak topology (the paper's Example 1). With $D$ given by a Bregman divergence it gives the method that the paper's §2 turns into an algorithm for convex programs with linear equality and inequality constraints, including entropy maximization. Lemma 1, the generalized Pythagorean inequality, is used throughout the later literature on Bregman projections, mirror descent and online learning.

The results are proved in the paper and are classical. To our knowledge no machine-checked version exists: Mathlib has orthogonal projections onto closed convex sets in Hilbert spaces, but no Bregman projections and no convergence theorem for cyclic projection methods. A formalization supplies an axiomatic interface (conditions I–VI) that does not depend on any particular divergence, so special cases (Euclidean distance, Kullback–Leibler divergence, Bregman divergences of Legendre functions) can be obtained by checking the conditions.

Difficulty

There is no norm and no metric: $D$ is neither symmetric nor subject to a triangle inequality, and $X$ is only a topological vector space. The usual Fejér-monotonicity argument for Euclidean projections, which compares distances to a fixed point of $R$, works only one way in $D$. Convergence of a subsequence $x^{n_k}$ does not by itself say anything about the shifted subsequences $x^{n_k+1},\dots,x^{n_k+m-1}$, and these are needed to reach every set $A_i$. That step requires condition VI together with compactness, and condition VI has a compactness premise that has to be supplied separately. Throughout, convergence is in a general topology where "compact" and "sequentially compact" may differ.

Formalization scope

The formalization commits to the following readings, each recorded in the items' Formalization Notes.

• The projection is a map. $P:\iota\to X\to X$ is fixed, and condition II states that $P_iy$ is a minimizer. Condition III is stated for this map.
• Condition IV, one-sided. The paper asks for $\lim_{t\to0}D(y+tz,y)/t=0$ for every $z\in X$. The formalization assumes only the right-hand limit in the directions $w-y$ with $w\in S$, which is what the proofs use and what the paper's IV implies. Every theorem is therefore at least as strong as the paper's.
• Compactness is sequential. "Compact" in V, VI and Lemma 2 (1) is IsSeqCompact. The set of elements of $\{x^n\}$ being compact is read as $\{x^n\}$ lying in a sequentially compact set.
• Hausdorff space. The proof of Theorem 1 identifies two limits of one sequence, so T2Space X is assumed. $X$ is a real topological vector space (IsTopologicalAddGroup, ContinuousSMul ℝ).
• Limiting point means the limit of x ∘ φ for a strictly increasing φ : ℕ → ℕ.
• Index base. The sets are indexed by Fin m with $0<m$, and the cyclic control is $n\mapsto n\bmod m$, the paper's $i_n=(n\bmod m)+1$ shifted by one.
• Translation typos. Condition II is printed as "$D(x,y)=\min_{z\in A_i\cap S}D(z,x)$" with "$i\in T$". The formalization reads $\min_z D(z,y)$ and $i\in I$. In Lemma 2 (2) the faint set symbol is read as $R$, and $z$ is taken in $R\cap S$, as in the proof.
• Domain of $D$. $D$ is a total function X → X → ℝ; every condition constrains it on $S\times S$ only, and the standing assumption $S\cap R\ne\emptyset$ is an explicit hypothesis.

A trivializing formalization is ruled out: the hypotheses are satisfiable (a sorry-free local check takes $X=\mathbb R$, $D(x,y)=(x-y)^2$, two overlapping closed intervals and the clamp projections), the conclusion concerns every limiting point of every cyclic run, and the goal neither assumes convergence nor restricts the control.

Contributions welcome: proofs of the milestones, a proof of the goal, and instances of DConditions for concrete divergences (squared Euclidean distance in finite dimension, Bregman divergences of strictly convex differentiable functions). These instances are reusable by the companion missions of this paper.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• L. G. Gubin, B. T. Polyak, E. V. Raik, The method of projections for finding the common point of convex sets, USSR Computational Mathematics and Mathematical Physics 7(6) (1967) 1–24. https://doi.org/10.1016/0041-5553(67)90113-9
• T. S. Motzkin, I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, Journal of Optimization Theory and Applications 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

Motivation

A single machine must process a set of jobs, each with a processing time and a due date, and the cost of a schedule depends on how late the jobs finish. Total tardiness is the classical criterion, but in many applications lateness is penalised more than proportionally: a job one week late costs more than twice a job half a week late, and a quadratic or other convex penalty describes this better. Hamilton Emmons's 1969 paper in Operations Research (DOI 10.1287/opre.17.4.701) derives dominance rules for total tardiness and then asks which of them survive when total tardiness is replaced by $\sum_J g(T_i)$ for an arbitrary convex nondecreasing loss $g$.

Timeline of the relevant results:

• 1955 — Jackson shows that ordering jobs by earliest due date (EDD) minimises the maximum lateness, and hence produces a schedule without late jobs whenever one exists.
• 1956 — Smith gives the ratio rule for weighted completion time and an adjacent-interchange criterion for pairs of jobs.
• 1969 — Emmons proves the precedence theorems for total tardiness that underlie later branch-and-bound and dynamic programming algorithms for $1\,||\,\sum T_j$, and shows (p. 713) that Theorems 2 and 3 and part of Theorem 1 extend to any sum of identical convex nondecreasing tardiness penalties.
• 1977 — Lawler's pseudo-polynomial algorithm for total tardiness builds on Emmons's conditions; the problem is later shown NP-hard (Du and Leung, 1990).

Setting

A finite set $J$ of jobs is to be sequenced on one machine. Job $J_i$ has a processing time $p_i\ge 0$ and a due date $d_i$. All jobs are available at time $0$, and the machine processes them one after another without idle time. A schedule is an ordering $l$ of the jobs of $J$. The completion time $C_i$ of $J_i$ in $l$ is the sum of the processing times of $J_i$ and of every job before it; its waiting (starting) time is $W_i=C_i-p_i$, and its tardiness is

$$T_i=\max(0,\,C_i-d_i).$$

A loss function $g:\mathbb R\to\mathbb R$, convex and nondecreasing on $[0,\infty)$, is fixed, the same for every job. The objective is $\sum_{i\in J} g(T_i)$, and a schedule is optimal if no schedule of $J$ has a smaller objective. With $g(T)=T$ this is total tardiness.

Where the paper uses job indices, the jobs are indexed in SPT order: $j<k$ implies $p_j<p_k$, or $p_j=p_k$ and $d_j\le d_k$. The notation $j\leftarrow k$ means that some optimal schedule has $J_j$ before $J_k$; for a set $A_k$ of jobs, $k\leftarrow A_k$ means that some optimal schedule has $J_k$ before every job of $A_k$, and $A_k'$ is the set of jobs of $J$ not in $A_k$. An EDD schedule sequences the jobs in nondecreasing order of due dates.

Formalization targets

Goal: Corollary 2.2* (p. 713)

If an EDD schedule $l$ of $J$ satisfies

$$W_i\le d_i\qquad\text{for every } i\in J,$$

then $l$ minimises $\sum_J g(T_i)$ over all schedules of $J$, for every $g$ convex and nondecreasing on $[0,\infty)$.

The goal fixes no constant and no particular $g$: it is a statement about the whole class of convex nondecreasing penalties.

Milestones (in attack order)

1. Convex exchange condition (p. 713): if $T_{ja}\le T_{jb}$, $T_{kb}\le T_{ka}$ (all nonnegative), $T_{ka}-T_{kb}\le T_{jb}-T_{ja}$ and $T_{jb}\ge T_{ka}$, then $g(T_{ka})-g(T_{kb})\le g(T_{jb})-g(T_{ja})$.
2. Theorem 1* (p. 713): for $j<k$, if $d_j\le d_k$ then $j\leftarrow k$.
3. Theorem 2* (p. 713): for $j<k$, if $k\leftarrow A_k$, $d_j>d_k$ and $d_j+p_j\ge\sum_{A_k'}p_i$, then $k\leftarrow j$.
4. Corollary 2.1* (p. 713): if $d_j=\max_i d_i$ and $d_j+p_j\ge\sum_J p_i$, then some optimal schedule ends with $J_j$.
5. Last-job reduction (proof of Corollary 2.2, p. 706): if some optimal schedule ends with $J_j$, any optimal schedule of $J\setminus\{J_j\}$ followed by $J_j$ is optimal for $J$.

Two further statements of the same section are included as items: Corollary 1.3* (the SPT schedule is optimal if it coincides with the EDD schedule) and Theorem 3 for the generalised objective.

Significance

The goal says that EDD is optimal for every convex nondecreasing tardiness penalty as long as no job starts after its due date. The classical sufficient condition, that at most one job is tardy, follows from Jackson's rule; Emmons's condition allows any or all jobs to be tardy, provided each is tardy by at most its own processing time. Because the conclusion holds for the whole class of penalties at once, an instance satisfying it needs no knowledge of $g$: total tardiness, total squared tardiness, and any other convex nondecreasing cost are minimised by the same sequence. Theorems 1* and 2* are the dominance rules that the paper's ordering procedure applies pairwise; they reduce the search space of branch-and-bound methods for convex tardiness objectives.

The results are proved in the paper (for $\sum g(T_i)$ the proofs are said to be "easily established" and omitted). None of them has, to our knowledge, a machine-checked proof. The mission produces formal statements and proofs of the generalised results, including the omitted ones, on top of a reusable single-machine model.

Difficulty

The total-tardiness proofs compare changes in tardiness additively: an interchange is good if the decrease in one job's tardiness is at least the increase in another's. For a convex $g$ this comparison is not enough, because a unit of tardiness costs more at higher tardiness levels; the changes must also occur at the right height on the curve, and part (b) of the proof of Theorem 1 fails for this reason. Each generalised argument therefore has to check, for every job whose tardiness changes, both the size and the location of the change, including jobs whose tardiness changes from zero to positive. Ties for the latest due date are a further obstacle: the printed proof of Corollary 2.1 cites Theorem 2, whose hypothesis $d_j>d_k$ is strict, so a job sharing the maximum due date is not covered by the argument as written, although the corollary is stated without excluding ties.

Formalization scope

Jobs are elements of a type $\iota$; the job set is a Finset $J$, processing times and due dates are real functions $p,d:\iota\to\mathbb R$. Where the paper's index matters, $\iota$ is linearly ordered and its order is the job index, together with the SPT-indexing hypothesis. A schedule is a duplicate-free list whose elements are exactly $J$, and completion times are the published single-machine definition MooreLateJobs.Shared.completionTime (Moore 1968), which starts the machine at time $0$ with no idle time. Optimality is against every schedule of $J$. The relation $j\leftarrow k$ is formalised as the existence of an optimal schedule with $J_j$ before $J_k$ (keeping the premise $k\leftarrow A_k$ in the conclusion where the theorem has one); the paper's cumulative reading of the notation is not formalised.

Standing assumptions and deviations:

• $g$ is convex and nondecreasing on $[0,\infty)$ only; the page's "increasing" is read as nondecreasing, as in the abstract. No smoothness, strict monotonicity or $g(0)=0$ is assumed.
• Processing times are assumed nonnegative; this is added (they are durations).
• The reduction $d_i<\sum_J p_i$ of p. 703 is not assumed, which makes the statements apply to more instances.
• "The EDD schedule" is any schedule with nondecreasing due dates; ties are arbitrary.

A trivializing formalization is ruled out: the goal requires optimality of the given EDD list against every schedule of $J$, not of some EDD list, and a sorry-free check shows its hypotheses hold on a two-job instance in which both jobs are tardy.

A complete development needs list lemmas for moving one job to a later position, the effect of such moves on completion times, and slope inequalities for convex functions on $[0,\infty)$. The schedule-manipulation lemmas are reusable for other single-machine sequencing results. Proofs of any milestone, of the two further items, and of general interchange lemmas are welcome.

Selected references

• H. Emmons, One-Machine Sequencing to Minimize Certain Functions of Job Tardiness, Operations Research 17(4):701–715, 1969. https://doi.org/10.1287/opre.17.4.701
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3:59–66, 1956. https://doi.org/10.1002/nav.3800030106
• E. L. Lawler, A "Pseudopolynomial" Algorithm for Sequencing Jobs to Minimize Total Tardiness, Annals of Discrete Mathematics 1:331–342, 1977. https://doi.org/10.1016/S0167-5060(08)70742-8
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. Du and J. Y.-T. Leung, Minimizing Total Tardiness on One Machine is NP-Hard, Mathematics of Operations Research 15(3):483–495, 1990. https://doi.org/10.1287/moor.15.3.483

Motivation

Gradient methods are the workhorse of large-scale nonlinear optimization and of the training of statistical models. In practice the direction actually used is rarely the exact negative gradient: it may be scaled, computed incrementally one data component at a time, or perturbed by approximation error. The classical convergence theory of such methods often assumes that the iterates stay bounded, that the objective is bounded below, or that the errors vanish at a prescribed rate, and these assumptions must then be checked separately for each method.

Bertsekas and Tsitsiklis (2000) proved convergence results for gradient methods with errors that need none of these assumptions. Their deterministic result (Proposition 1) allows a general descent direction together with an error whose size is proportional to the stepsize, and concludes that either the objective values diverge to $-\infty$ or they converge and the gradients tend to zero. It applies, among others, to the incremental gradient method for a sum of functions (Proposition 2 of the same paper), which underlies backpropagation-style training. The stochastic counterpart (Proposition 3, zero-mean errors) is the subject of a companion mission.

Setting

Throughout, $f:\mathbb R^n\to\mathbb R$ is a continuously differentiable function whose gradient is Lipschitz continuous: for some constant $L$,

$$\|\nabla f(x)-\nabla f(\bar x)\|\le L\|x-\bar x\|\qquad\forall x,\bar x\in\mathbb R^n. \tag{2.1}$$

Here $\|\cdot\|$ is the Euclidean norm and $x'y$ the standard inner product. The gradient method with errors generates a sequence of iterates

$$x_{t+1}=x_t+\gamma_t(s_t+w_t),\qquad t=0,1,\dots,$$

where $\gamma_t>0$ is the stepsize, $s_t$ is a descent direction and $w_t$ is an error vector. Nothing is assumed about how $s_t$ and $w_t$ are produced, beyond the two conditions below, which hold for some positive scalars $c_1,c_2,p,q$ and every $t$:

$$c_1\|\nabla f(x_t)\|^2\le-\nabla f(x_t)'s_t,\qquad\|s_t\|\le c_2\bigl(1+\|\nabla f(x_t)\|\bigr), \tag{2.2}$$ $$\|w_t\|\le\gamma_t\bigl(q+p\|\nabla f(x_t)\|\bigr). \tag{2.3}$$

The stepsizes are diminishing in the standard sense:

$$\sum_{t=0}^\infty\gamma_t=\infty,\qquad\sum_{t=0}^\infty\gamma_t^2<\infty.$$

A stationary point of $f$ is a point $\bar x$ with $\nabla f(\bar x)=0$; a limit point of $(x_t)$ is the limit of some subsequence.

Formalization targets

Goal: Proposition 1 (p. 630)

Under (2.1), (2.2), (2.3) and the stepsize conditions, either

$$f(x_t)\to-\infty,$$

or else $f(x_t)$ converges to a finite value and

$$\lim_{t\to\infty}\nabla f(x_t)=0.$$

Furthermore, every limit point of $(x_t)$ is a stationary point of $f$.

Milestones

The milestones follow the paper's own argument, in order.

1. Lemma 1 (p. 629). For real sequences with $W_t\ge0$, $Y_{t+1}\le Y_t-W_t+Z_t$ and $\sum_{t=0}^T Z_t$ convergent, either $Y_t\to-\infty$, or $Y_t$ converges and $\sum_t W_t<\infty$.
2. (2.4) (p. 630). Under (2.1), $f(x+z)\le f(x)+z'\nabla f(x)+\tfrac L2\|z\|^2$ for all $x,z$.
3. (2.5) (p. 631). For some $\beta_1,\beta_2>0$ and all sufficiently large $t$, $f(x_{t+1})\le f(x_t)-\gamma_t\beta_1\|\nabla f(x_t)\|^2+\gamma_t^2\beta_2$.
4. (2.6) (p. 631). Either $f(x_t)\to-\infty$, or $f(x_t)$ converges and $\sum_t\gamma_t\|\nabla f(x_t)\|^2<\infty$.
5. After (2.6) (p. 631). If $f(x_t)\not\to-\infty$, then $\liminf_{t\to\infty}\|\nabla f(x_t)\|=0$.

Significance

The result. Proposition 1 separates two concerns that are usually entangled: what the method guarantees, and what must be known about $f$. It concludes stationarity of all limit points and convergence of the gradients to zero without assuming that the iterates are bounded or that $f$ is bounded below; when $f$ is bounded below the first alternative is excluded and $\nabla f(x_t)\to0$ follows outright. Because $s_t$ need not be the negative gradient and $w_t$ need not vanish faster than the stepsize, the result covers scaled gradient methods, incremental gradient methods for sums of functions, and gradient methods with deterministic approximation error. The descent inequality (2.4) and the deterministic supermartingale-type Lemma 1 are standard tools that recur throughout optimization theory.

Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof would give a reusable, verified convergence theorem for a broad class of first-order methods on $\mathbb R^n$, together with a formal descent lemma for functions with Lipschitz gradient, which Mathlib does not currently state in this form, and a deterministic Robbins–Siegmund-type lemma for sequences.

Difficulty

The summability estimate (2.6) gives only $\liminf\|\nabla f(x_t)\|=0$. Passing to $\lim\nabla f(x_t)=0$ is the main step: the obvious argument (a summable series $\sum_t\gamma_t\|\nabla f(x_t)\|^2$ with $\sum_t\gamma_t=\infty$ forces the gradient norms to zero) is false in general, because a nonnegative sequence with these two properties may still have infinitely many large terms. What is missing is a bound on how far $\|\nabla f(x_t)\|$ can travel while the stepsizes are small, and only (2.1) and (2.2)–(2.3) together supply it. A second difficulty is that there is no boundedness of the iterates: every estimate must hold globally, and the error $w_t$ is controlled only relative to $\|\nabla f(x_t)\|$, which may be unbounded along the sequence.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $x'y$ is the real inner product ⟪x, y⟫_ℝ, and $\nabla f$ is Mathlib's gradient f; the hypothesis ContDiff ℝ 1 f makes it the true gradient. The paper's statement is for $\mathbb R^n$ and the formalization does not generalize to Hilbert spaces.
• The standing assumption (2.1) of §2 is part of every statement about $f$, as LipschitzWith L (gradient f) with L : ℝ≥0; this is equivalent to (2.1) for some real constant.
• The sequences $x_t,s_t,w_t$ and $\gamma_t$ are arbitrary data indexed from $t=0$, constrained only by the recursion and by (2.2), (2.3), $\gamma_t>0$ (all four constants $c_1,c_2,p,q$ are positive, as printed).
• $\sum_t\gamma_t=\infty$ is divergence of the partial sums to $+\infty$; $\sum_t\gamma_t^2<\infty$ is summability of nonnegative terms. In Lemma 1 the convergence of $\sum_t Z_t$ is convergence of the partial sums, not absolute convergence, since $Z_t$ may change sign.
• $\lim\inf$ is written out as "for every $\epsilon>0$, infinitely often below $\epsilon$", avoiding junk values of a lim inf of an unbounded sequence. Limit points are cluster points of the sequence.
• "Every limit point is stationary" is a separate conjunct, outside the dichotomy, exactly as on the page.
• The constants $\beta_1,\beta_2$ in (2.5) are existential. The milestones (2.5) and (2.6) retain the stepsize hypotheses of Proposition 1, where the paper derives them.
• A trivializing formalization would drop the "$-\infty$" alternative or require $f$ bounded below; neither is done. Instances satisfying all hypotheses with $f(x_t)\to-\infty$ and $\nabla f\not\to0$ exist (a linear $f$), so the first alternative is genuinely needed.
• Out of scope: Proposition 2 (the incremental gradient method of §3), which is a corollary of the goal, and the stochastic results of §4–§5.

Contributions welcome: proofs of the descent lemma and Lemma 1 (both reusable well beyond this mission), and of the steps (2.5)–(2.6) and the excursion argument.

Selected references

• D. P. Bertsekas and J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM Journal on Optimization 10(3):627–642, 2000. https://doi.org/10.1137/S1052623497331063
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999.
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

Calibrated forecasting

A forecaster announces, each day, a probability that it will rain; afterwards nature reveals whether it did. The forecaster is calibrated if, on the days on which it announced roughly 30%, it rained roughly 30% of the time, and likewise for every other announced value. Calibration is a minimal consistency requirement for probabilistic forecasts, used in meteorology, in the evaluation of probabilistic classifiers, and in game theory, where calibrated forecasts of the opponents' play lead to correlated equilibrium (Foster and Vohra, 1997).

Calibration is achievable even against an adversary who chooses the outcomes, provided the forecaster randomizes. Timeline:

• 1998. Foster and Vohra construct an asymptotically calibrated randomized forecaster against an arbitrary outcome sequence.
• 1999. Foster reduces calibration to Blackwell's approachability theorem by exhibiting, for each halfspace, a forecast that keeps the payoff inside it.
• 2009. Mannor and Stoltz give an approachability-based calibration procedure concurrently with the paper below.
• 2011. Abernethy, Bartlett and Hazan prove that Blackwell approachability and no-regret online linear optimization are equivalent, and use the equivalence to obtain an efficient calibrated forecaster: $O(\log 1/\varepsilon)$ time per round and calibration rate $O(1/\sqrt{\varepsilon T})$.

This mission formalizes the last result, Theorem 22 of the 2011 paper, in the explicit form given by its proof.

Setting

Fix a positive integer $m$ and the grid width $\varepsilon = 1/m$. Each round $t = 1, \dots, T$ the forecaster chooses a probability vector $w_t$ in the simplex $\Delta_{m+1}$ over the grid indices $i = 0, \dots, m$, draws $i_t \sim w_t$ and announces $p_t = i_t/m$. Nature then reveals $y_t \in \{0, 1\}$.

Vectors live in $\mathbb R^{m+1}$ with the Euclidean norm $\|\cdot\|_2$. The ℓ₁ norm is $\|x\|_1 = \sum_i |x_i|$, the ℓ₁ ball is $B_1(r) = \{y : \|y\|_1 \le r\}$, and the unit cube is $B_\infty(1) = \{\theta : |\theta_i| \le 1 \text{ for all } i\}$.

The calibration game (11) has payoff

$$u(w, y) = \Bigl(w(0)\bigl(y - \tfrac0m\bigr),\ w(1)\bigl(y - \tfrac1m\bigr),\ \dots,\ w(m)(y - 1)\Bigr) \in \mathbb R^{m+1}.$$

The $(\ell_1, \varepsilon)$-calibration rate (Definition 19) of the announced forecasts is $\max\{0, \sum_{i=0}^m |\frac1T\sum_{t=1}^T \mathbb I[p_t = i/m](i/m - y_t)| - \varepsilon/2\}$. Replacing each indicator by its expectation $w_t(i)$ gives the rate of the forecast distributions,

$$\bar C^\varepsilon_T = \max\Bigl\{0,\ \sum_{i=0}^m \Bigl|\frac1T \sum_{t=1}^T w_t(i)\Bigl(\frac im - y_t\Bigr)\Bigr| - \frac\varepsilon2\Bigr\},$$

which is $\max\{0, \|\bar u_T\|_1 - \varepsilon/2\}$ for the average payoff $\bar u_T = \frac1T\sum_t u(w_t, y_t)$.

The forecaster is Algorithm 5. It keeps a point $\theta_t$ in the cube, starting from $\theta_1 = 0$ with $w_1$ arbitrary. After round $t$ it takes a projected gradient step (Algorithm 4, online gradient descent) against the loss vector $f_t = -u(w_t, y_t)$:

$$\theta_{t+1} = \Pi_{B_\infty(1)}\bigl(\theta_t + \eta\, u(w_t, y_t)\bigr),$$

where $\Pi$ is the Euclidean projection. It then sets $w_{t+1}$ to the output of the oracle Algorithm 3 on $\theta_{t+1}$, which puts weight on at most two adjacent grid points where $\theta$ changes sign.

Formalization targets

Goal: Theorem 22 in the form (14)

For $m \ge 1$, $T \ge 1$, every outcome sequence $y_1, \dots, y_T \in \{0, 1\}$ and every run of Algorithm 5 with $\eta = \sqrt{(m+1)/T}$,

$$\bar C^\varepsilon_T \le \sqrt{\frac{2}{\varepsilon T}}.$$

This is the bound $C^\varepsilon_T \le GD/\sqrt T$ of display (14) with the paper's constant $G = \sqrt 2$.

Milestones

1. Claim 1 (proof): $\min_{\|y\|_1 \le \varepsilon/2}\|x - y\|_1 = \max\{0, -\varepsilon/2 + \|x\|_1\}$.
2. Display (13): for $\|x\|_1 > \varepsilon/2$, also $= -\varepsilon/2 - \min_{\|\theta\|_\infty \le 1}\langle -x, \theta\rangle$.
3. Algorithm 3: for every $\theta$ in the cube there is an output $w \in \Delta_{m+1}$, and every output satisfies $\langle u(w, y), \theta\rangle \le \varepsilon/2$ for all $y \in [0, 1]$.
4. Display (12): under that guarantee, $\max\{0, \|\bar u_T\|_1 - \varepsilon/2\} \le \frac1T\bigl(\sum_t \langle -u_t, \theta_t\rangle - \min_{\theta \in B_\infty(1)}\sum_t\langle -u_t, \theta\rangle\bigr)$.
5. Online gradient descent: regret at most $DG\sqrt T$ with step $\eta = D/(G\sqrt T)$.
6. Theorem 21 (response-satisfiability and approachability): for every $y \in [0,1]$ some $w \in \Delta_{m+1}$ has $u(w, y) \in B_1(\varepsilon/2)$; hence some algorithm choosing $w_t$ from $y_1, \dots, y_{t-1}$ drives the distance of the average payoff to $B_1(\varepsilon/2)$ to $0$ against every outcome sequence in $[0,1]$.

Significance

The bound shows that a forecaster with logarithmic per-round cost has calibration error vanishing at rate $T^{-1/2}$ against every outcome sequence. Earlier calibrated forecasters required solving a linear program or computing a fixed point each round. The construction is also the paper's worked instance of its general equivalence: a calibration problem, posed as approachability of an ℓ₁ ball, is solved by a no-regret learner on the dual unit cube together with a halfspace oracle.

The result is proved in the paper; no machine-checked version is known to exist. The formalization makes explicit three points the paper leaves informal: the step size, the sign of the gradient step, and the gap between the forecast distributions and the sampled forecasts. The milestones are reusable on their own: the ℓ₁/ℓ∞ duality, and the regret bound of online gradient descent for linear losses on a general closed convex set.

Difficulty

The chain (12)–(14) looks like a direct composition, but each link has content. The oracle guarantee needs a case analysis over the sign pattern of $\theta$, including the degenerate case $\theta(i+1) = 0$. The reduction (12) needs the duality (13) with attained minima, and it holds only outside the ball $B_1(\varepsilon/2)$. The regret bound of online gradient descent needs the non-expansiveness of the Euclidean projection and a telescoping argument. The tempting shortcut of quoting "OGD has regret $O(\sqrt T)$" does not give the stated constant without fixing the step size.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin (m+1)), with grid index $i \in \{0, \dots, m\}$ as Fin (m+1) and $i/m$ as a real quotient; the ℓ₁ norm and the cube are written out coordinatewise. Rounds are $t = 1, \dots, T$. Minima over sets are stated through IsLeast or as the infimum of the image of a nonempty bounded set. Algorithm 3 is a relation that allows every sign-change index the binary search might return. The projection is any Euclidean minimizer onto the cube.

Conventions and corrections, each disclosed in the item's Formalization Note:

• Gradient-step sign. Algorithm 4 prints $\theta_t - \eta u_t$, but the proof runs the learner on the losses $f_t = -u_t$ (condition 2), so the step is $\theta_t + \eta u_t$. With the printed sign the bound fails.
• Step size. The page sets $\eta = O(T^{-1/2})$; the goal pins $\eta = \sqrt{(m+1)/T}$, the standard tuning with radius $\sqrt{m+1}$ of the cube and $\|u_t\|_2 \le 1$. The page's $D = \sqrt{1/\varepsilon}$ is not the cube's diameter.
• Forecast distributions. The rate is that of the distributions $w_t$, the expectation of the calibration vector over the forecaster's draws (Lemma 20). The high-probability statement for the sampled forecasts is not formalized, nor is the running-time claim.
• Other misprints. Algorithm 3's header "$w \mapsto \theta$" is $\theta \mapsto w$, and the calibration vector has $m + 1$ coordinates, not $\lfloor \varepsilon^{-1} \rfloor$.
• Added hypotheses. $m \ge 1$ and $T \ge 1$.

A trivializing formalization is ruled out. The rate is defined from Definition 19's formula, not as a distance, and the step size is pinned. A free step size would make the bound false, and an empty oracle relation would make it vacuous; milestone 3's existence clause excludes the latter.

Contributions are welcome on each milestone. The online gradient descent bound and the ℓ₁/ℓ∞ duality are independent of calibration. The published one-step inequality LogRegretOCO.OGD.one_step_inequality is included as a reference item for the regret bound.

Selected references

• J. Abernethy, P. L. Bartlett, E. Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, COLT 2011, JMLR W&CP 19, pp. 27–46, 2011. https://proceedings.mlr.press/v19/abernethy11b.html
• D. P. Foster, R. V. Vohra, Asymptotic calibration, Biometrika 85(2), 1998. https://doi.org/10.1093/biomet/85.2.379
• D. P. Foster, A proof of calibration via Blackwell's approachability theorem, Games and Economic Behavior 29, 1999. https://doi.org/10.1006/game.1999.0724
• D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21, 1997. https://doi.org/10.1006/game.1997.0595
• S. Mannor, G. Stoltz, A geometric proof of calibration, Mathematics of Operations Research 35(4), 2010. https://arxiv.org/abs/0908.3576
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955

Motivation

Many problems in signal processing, statistics and machine learning take the additively separable form

$$\min\{\Psi(x) + \Phi(x) : x \in \mathcal H\},$$

a smooth term $\Phi$ plus a nonsmooth but "simple" term $\Psi$, such as an $\ell^1$ penalty or the indicator function of a convex constraint set. The forward-backward method alternates a gradient step on $\Phi$ with a proximal step on $\Psi$. Beck and Teboulle's FISTA (Beck–Teboulle 2009) combined it with Nesterov's acceleration and improved the worst-case rate for function values from $\mathcal O(k^{-1})$ to $\mathcal O(k^{-2})$. Whether the iterates of the accelerated scheme converge at all, and not just their function values, remained unsettled for a long time; in the words of Attouch and Peypouquet, it "puzzled researchers for over two decades".

Timeline.

• 1967: Opial proves that weak convergence of a sequence in a Hilbert space follows from two facts, the convergence of its distance to every point of a target set and the location of its weak cluster points in that set (Opial 1967).
• 2009: Beck and Teboulle introduce FISTA, with an $\mathcal O(k^{-2})$ rate for function values.
• 2014: Su, Boyd and Candès read the accelerated method as a discretization of the ODE $\ddot x + \frac{\alpha}{t}\dot x + \nabla\Theta(x) = 0$ (Su–Boyd–Candès 2014).
• 2014–2015: for the variant with inertial coefficient $\frac{k-1}{k+\alpha-1}$ and $\alpha > 3$, Chambolle and Dossal (2015) and, independently, Attouch, Chbani, Peypouquet and Redont (arXiv:1507.04782) prove weak convergence of the iterates.
• 2016: Attouch and Peypouquet (arXiv:1510.08740, SIAM J. Optim. 26(3), 2016) prove the $o(k^{-2})$ rate and, as Theorem 3, give a short proof of weak convergence from the same energy estimates.

The case $\alpha = 3$, the original choice of FISTA, is not covered by this result.

Setting

Let $\mathcal H$ be a real Hilbert space with scalar product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$.

• $\Psi : \mathcal H \to \mathbb R \cup \{+\infty\}$ is proper (finite somewhere), lower-semicontinuous and convex. The value $+\infty$ matters: indicator functions of closed convex sets are the main example.
• $\Phi : \mathcal H \to \mathbb R$ is convex and continuously differentiable, and its gradient $\nabla\Phi$ is $L$-Lipschitz continuous.
• $\Theta = \Psi + \Phi$, and $S = \operatorname{argmin}\Theta$ is assumed nonempty.
• For $s > 0$, the proximal map $\operatorname{prox}_{s\Psi}(x)$ is the unique minimizer of $y \mapsto \Psi(y) + \frac{1}{2s}\|y - x\|^2$.

Given $\alpha > 0$ and $s > 0$, algorithm (2) generates $(x_k)$ by

$$y_k = x_k + \frac{k-1}{k+\alpha-1}(x_k - x_{k-1}),\qquad x_{k+1} = \operatorname{prox}_{s\Psi}\big(y_k - s\nabla\Phi(y_k)\big).$$

The auxiliary sequence (6) is $z_k = x_k + \frac{k-1}{\alpha-1}(x_k - x_{k-1})$. For a point $x^*$, the proof of Theorem 3 uses

$$\delta_k = (k-1)\big[\|x_k - x^*\|^2 - \|x_{k-1} - x^*\|^2\big] + (\alpha-1)\|x_k - x^*\|^2 .$$

A sequence $(x_k)$ converges weakly to $\bar x$, written $x_k \rightharpoonup \bar x$, if $\langle x_k, y\rangle \to \langle \bar x, y\rangle$ for every $y \in \mathcal H$.

In Lean these are theta, extrap ($y_k$), IsAccelFBRun and zSeq (shared definitions in the namespace NesterovFB.Rates), and deltaSeq in the namespace NesterovFB.Weak. The predicates IsProperClosedConvex and IsProx and the predicate WeakTendsto are reused from the platform.

Formalization targets

Goal: Theorem 3 (p. 5)

Under the assumptions above, with $\alpha > 3$ and $0 < s < 1/L$,

$$\exists\, \bar x \in S:\quad x_k \rightharpoonup \bar x .$$

The limit is required to be a minimizer of $\Theta$; weak convergence to an arbitrary point would be a weaker statement.

Milestones (proof of Theorem 3, p. 5)

For every $x^* \in S$ and $k \ge 1$:

$$\|x_{k+1} - x^*\|^2 \le \|y_k - x^*\|^2,$$ $$\delta_{k+1} - \delta_k \le 2(k+\alpha-1)\,\|x_k - x_{k-1}\|^2,$$ $$\lim_{k\to\infty}\|z_k - x^*\| \text{ exists},\qquad \lim_{k\to\infty}\|x_k - x^*\| \text{ exists}.$$

Significance

The result. Theorem 3 shows that the accelerated forward-backward method with $\alpha > 3$ behaves like the unaccelerated method in one important respect: its iterates converge to a solution rather than just producing small function values. In infinite-dimensional settings (inverse problems, PDE-constrained optimization, signal recovery in function spaces) weak convergence is the natural notion, and strong convergence can fail. The four milestones are the steps that matter for other analyses too: a "Fejér-type" step inequality from the extrapolated point, and the convergence of the distance to every minimizer.

Formalizing it. The result is proved in the literature; no machine-checked proof of it is known. A complete formalization needs the energy estimates of the paper's §1.1–1.2 (summability of $k\|x_k - x_{k-1}\|^2$, boundedness of $(z_k)$, and the convergence of $k^2\|x_{k+1}-x_k\|^2 + (k+1)^2(\Theta(x_{k+1}) - \min\Theta)$), which a companion mission poses separately, and Opial's lemma, which is not in Mathlib.

Difficulty

The unaccelerated forward-backward method is Fejér monotone: $\|x_{k+1} - x^*\|$ decreases for every minimizer $x^*$, and Opial's lemma applies directly. The accelerated iterates are not Fejér monotone. The first milestone only compares $x_{k+1}$ with the extrapolated point $y_k$, and $\|y_k - x^*\|$ can exceed $\|x_k - x^*\|$ by the inertial term. The quantity $\|x_k - x^*\|^2$ therefore satisfies only a second-order inequality with coefficients that grow in $k$. The obvious attempt, to show that $\|x_k - x^*\|$ is eventually monotone and apply Opial's lemma as for the unaccelerated method, fails.

A second difficulty is the passage from distances to weak convergence: in a Hilbert space this needs the weak sequential compactness of bounded sets and the weak lower-semicontinuity of $\Theta$ (to place weak cluster points in $S$).

Formalization scope

• $\mathcal H$ is a general real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not $\mathbb R^n$; in finite dimensions weak and strong convergence coincide and the goal would be a different, weaker theorem.
• $\Psi$ and $\Theta$ take values in EReal; $\Psi$ is never assumed real-valued.
• $L$ is a nonnegative real and "$0 < s < 1/L$" is written $0 < s$, $sL < 1$, which also allows $L = 0$.
• $\operatorname{prox}_{s\Psi}$ is a map $P$ given with its minimization property; under the hypotheses it is unique, so this is the proximal map.
• The run starts at $k = 1$ with $x_0, x_1$ arbitrary. At $k = 1$ the inertial coefficient vanishes, so $x_0$ never matters; every sequence the paper generates satisfies the predicate.
• "The limit exists" means a real limit. Weak convergence is the platform's WeakTendsto, not convergence in norm.
• The milestones keep the standing hypothesis $\alpha > 3$ of Theorem 3, although the first two do not need it.

A trivializing formalization is ruled out by the sanity check: the hypotheses are jointly satisfiable, and the goal asks for weak convergence to a minimizer, so neither a vacuous hypothesis nor an arbitrary limit point is admitted.

Infrastructure that a complete development needs, and that is reusable beyond this mission: the descent inequality (9) of the proximal-gradient operator, Opial's lemma in a real Hilbert space, the weak lower-semicontinuity of proper lower-semicontinuous convex functions, and the lemma that a bounded real sequence whose positive increments are summable converges. Contributions of any of these are welcome.

Selected references

• H. Attouch, J. Peypouquet, The rate of convergence of Nesterov's accelerated forward-backward method is actually faster than $1/k^2$, SIAM J. Optim. 26(3):1824–1834, 2016. https://arxiv.org/abs/1510.08740 (v4 is the source of this mission)
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168, 2018. https://arxiv.org/abs/1507.04782
• A. Chambolle, C. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166, 2015. https://doi.org/10.1007/s10957-015-0746-4
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2(1):183–202, 2009. https://doi.org/10.1137/080716542
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73:591–597, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, NIPS 2014. https://arxiv.org/abs/1503.01243