Machine Learning

Completed

Optimization Statistics·Captain: mikedeng1

Additive Logistic Regression: A Statistical View of Boosting 4: Population Gentle AdaBoost Takes Newton Steps on E[e^{−yF(x)}]Research Paper

Motivation

Boosting combines many weak classifiers into a strong one by refitting, again and again, to reweighted data. AdaBoost (Freund and Schapire, 1997) and its confidence-rated variant Real AdaBoost (Schapire and Singer, 1999) were introduced through the theory of online learning. Friedman, Hastie and Tibshirani (2000) recast them as stagewise fitting of an additive model $F(x) = \sum_m f_m(x)$ by minimizing the exponential criterion $J(F) = E\,e^{-yF(x)}$ , where $y\in\{-1,1\}$ is the class label. In that view Real AdaBoost minimizes $J(F+f)$ exactly over the new term $f$ at each stage.

The same paper proposes Gentle AdaBoost (Algorithm 4, §4.4), which replaces the exact minimization by a single Newton step. Its increments are bounded, and the authors report that it often matches or beats Real AdaBoost and LogitBoost, especially when numerical stability is an issue. The paper's stagewise view of boosting led on to gradient boosting (Friedman, 2001). This mission formalizes the paper's justification of the algorithm: its population version takes Newton steps on $E\,e^{-yF(x)}$ .

Setting

A feature $x$ ranges over a measurable space $X$ . The label $y$ takes values in $\{-1,1\}$ , and $(x,y)$ has a joint probability law $\nu$ on $X\times\{-1,1\}$ . Conditional expectations given $x$ , written $E(\cdot\mid x)$ , are integrals against the conditional law $\nu(\cdot\mid x)$ of $y$ given $x$ , and $P = P(y=1\mid x)$ .

The algorithm maintains a current additive fit $F : X\to\mathbb R$ , starting from $F = 0$ . For a new term $f(x)$ , the conditional exponential criterion is

J(F(x)+f(x)) = E\big(e^{-y(F(x)+f(x))}\mid x\big),

a function of the real number $f(x)$ for each fixed $x$ .

The weight attached to an observation is $w(x,y) = e^{-yF(x)}$ . The weighted conditional expectation (p. 347) is

E_w\big[g(x,y)\mid x\big] = \frac{E[w(x,y)\,g(x,y)\mid x]}{E[w(x,y)\mid x]},

and $P_w(y=b\mid x) = E_w[1_{[y=b]}\mid x]$ are the weighted class probabilities.

Gentle AdaBoost (Algorithm 4) repeats three steps: fit $f_m$ by weighted least squares of $y$ on $x$ with weights $w$ , update $F \leftarrow F + f_m$ , and update $w \leftarrow w\,e^{-yf_m(x)}$ with renormalization. In the population version the weighted least-squares fit is the weighted conditional mean, so one step is

F(x) \leftarrow F(x) + E_w(y\mid x),\qquad w(x,y) = e^{-yF(x)}.

For comparison with LogitBoost the paper uses the symmetric logistic $p(x) = e^{F(x)}/(e^{F(x)}+e^{-F(x)})$ and the 0/1 response $y^* = (y+1)/2$ .

Formalization targets

Goal: Result 4

For every $x$ , with $s(x) = -E(e^{-yF(x)}y\mid x)$ and $H(x) = E(e^{-yF(x)}\mid x)$ : $s(x)$ is the first derivative of $J(F(x)+f(x))$ at $f(x)=0$ , $H(x)$ is the second derivative, $H(x)>0$ , and

F(x) + E_w(y\mid x) = F(x) - \frac{s(x)}{H(x)}.

This is the paper's Result 4, "the Gentle AdaBoost algorithm (population version) uses Newton steps for minimizing $Ee^{-yF(x)}$ ", in the precise form its Derivation gives.

Milestones

The Derivation's derivatives:

\frac{\partial J}{\partial f(x)}\Big|_{0} = -E(e^{-yF(x)}y\mid x),\qquad \frac{\partial^2 J}{\partial f(x)^2}\Big|_{0} = E(e^{-yF(x)}\mid x).

The Newton update: $F(x) + E(e^{-yF(x)}y\mid x)/E(e^{-yF(x)}\mid x) = F(x) + E_w(y\mid x)$ .
The update as weighted class probabilities: $E_w(y\mid x) = P_w(y=1\mid x) - P_w(y=-1\mid x)$ .
The range: $E_w(y\mid x) \in [-1,1]$ .
Display (37):

\frac{E(e^{-yF(x)}y\mid x)}{E(e^{-yF(x)}\mid x)} = \frac{e^{-F(x)}P - e^{F(x)}(1-P)}{e^{-F(x)}P + e^{F(x)}(1-P)} = \frac{P-p(x)}{(1-p(x))P + p(x)(1-P)} \in [-1,1].

Display (38): the LogitBoost increment $\tfrac12 E(y^*-p(x)\mid x)/E(p(x)(1-p(x))\mid x)$ equals $\tfrac12 (P-p(x))/(p(x)(1-p(x)))$ .

Significance

The result. Result 4 places Gentle AdaBoost alongside LogitBoost (Result 3) as a Newton method. Real AdaBoost (Result 2) and Gentle AdaBoost minimize the same criterion, but one solves the stagewise problem exactly and the other takes one Newton step. Displays (37) and (38) then put Gentle AdaBoost and LogitBoost in the same coordinates $P$ and $p(x)$ . The two updates are close when $p(x)\approx \tfrac12$ . LogitBoost's update can be unbounded as $p(x)$ approaches $0$ or $1$ , while Gentle AdaBoost's always stays in $[-1,1]$ . This is the paper's explanation for the stability of Gentle AdaBoost.

Formalizing it. The result is proved on the page by direct calculation. No machine-checked version is known to exist. The mission produces a formal account of the population algorithm on an arbitrary joint law, through Mathlib's disintegration of a measure on $X\times\{-1,1\}$ , and of the Newton-step identity. It also gives a reusable treatment of the paper's weighted conditional expectation $E_w$ in the conditional-kernel language. The same objects appear in the other missions of this series (Real AdaBoost, LogitBoost).

Difficulty

The calculus on the page is short. The work is in the setting. "Differentiate the criterion with respect to $f(x)$ " has to mean differentiating an integral against the conditional law of $y$ given $x$ with respect to a parameter, with the derivative established, not read off a formula. A plain derivative equation proves nothing at a point where the function is not differentiable. The second derivative needs the first derivative as a function of $t$ , not only its value at $0$ . The Newton step divides by $H(x)$ , so its positivity must be established before the identity has content. Finally, (37) requires recovering $P(y=-1\mid x) = 1-P$ from the conditional law being a probability measure, and the second equality in (37) holds only for the symmetric logistic.

Formalization scope

Labels are Bool (true for $y=1$ , false for $y=-1$ ); $y$ is sgn b and $y^*$ is ystar b. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν], and $E(\cdot\mid x)$ is the Bochner integral against ν.condKernel x, a probability measure on the two-point type. Every statement holds for every $x$ . No almost-everywhere qualifier, integrability or measurability hypothesis is needed, and none is added. The kernel is unique only almost everywhere, and the statements hold for the chosen version. They use only the fact that it is a Markov kernel. The definitions file fixes the conditional criterion condCritAt, the weighted conditional expectation wCondExp with weight $e^{-yF(x)}$ , the weighted class probabilities wProb, the population step gentleStep, and the symmetric logistic symLogistic. All of these are written exactly as on the page.

Derivatives are HasDerivAt statements. The second derivative is the derivative at $0$ of an explicit first-derivative function, which is itself shown to be the derivative at every point. $H(x)>0$ is a conclusion of the goal, never a hypothesis. Several formalizations would trivialize the claims and are ruled out. The criterion is the integral against the conditional law, not a closed form $\eta e^{-F-t}+(1-\eta)e^{F+t}$ in a free parameter $\eta$ . No bare deriv equation and no division by an unproved nonzero quantity is used. The logistic is the symmetric $e^{F}/(e^{F}+e^{-F})$ , not $1/(1+e^{-F})$ , which differs by a factor $2$ in $F$ and makes (37) false. The sample version of Algorithm 4 (trees, terminal-node averages) is not formalized.

Welcome contributions: proofs of the milestones, general lemmas on differentiating integrals over finite label spaces with respect to a parameter, and lemmas connecting condKernel on Bool with the closed forms in $P$ .

Selected references

J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. Syst. Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Mach. Learn. 37(3):297–336, 1999. https://doi.org/10.1023/A:1007614523901
J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5):1189–1232, 2001. https://doi.org/10.1214/aos/1013203451

10 thms3 active usersReviewed

Completed

Optimization Statistics·Captain: mikedeng1

Additive Logistic Regression: A Statistical View of Boosting 3: Population LogitBoost Takes Newton Steps on the Binomial Log-LikelihoodResearch Paper

Motivation

Boosting combines many weak classifiers into a strong one by refitting, round after round, to a reweighted version of the training data. Freund and Schapire's AdaBoost was introduced as a procedure, with guarantees on the training error, and for several years it was not clear what statistical model it fitted. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) answered this by showing that boosting is stagewise additive modelling: each round adds one term to an additive function $F(x) = \sum_m f_m(x)$ so as to improve a population criterion.

Section 4.3 of that paper takes the step from interpretation to design. If boosting is stagewise fitting of an additive logistic model, one can choose the criterion directly: the Bernoulli log-likelihood. The resulting procedure, LogitBoost (Algorithm 3), fits at each round a weighted least-squares regression to a working response, exactly as iteratively reweighted least squares fits a logistic regression. Result 3 states that this is no accident: in the population, LogitBoost's update is a Newton step on the expected log-likelihood. The same Newton reading reappears in gradient boosting with logistic loss, where each terminal node of a tree takes one Newton step (Friedman 2001).

Timeline:

1997: Freund and Schapire, AdaBoost (J. Comput. Syst. Sci. 55).
1999: Schapire and Singer, Real AdaBoost with confidence-rated predictions (Mach. Learn. 37).
2000: Friedman, Hastie and Tibshirani, the statistical view; LogitBoost and Result 3.
2001: Friedman, gradient boosting machines (Ann. Statist. 29).

Setting

Let $X$ be a measurable space of features and let $\nu$ be a probability measure on $X\times\{0,1\}$ , the joint law of a feature $x$ and a 0/1 response $y^*$ . Write $E(\cdot\mid x)$ for the conditional expectation given $x$ , an integral against the regular conditional distribution of $y^*$ given $x$ .

A current fit is a function $F : X\to\mathbb R$ . The symmetric logistic model (30) represents $P(y^*=1\mid x)$ by

p(x) = \frac{e^{F(x)}}{e^{F(x)}+e^{-F(x)}}.

For an update $f(x)$ , the expected log-likelihood (31) is

E\,l(F+f) = E\Big[2y^*\big(F(x)+f(x)\big) - \log\big(1+e^{2(F(x)+f(x))}\big)\Big],

whose integrand is the Bernoulli log-likelihood $y^*\log p + (1-y^*)\log(1-p)$ of $y^*$ under the model.

For a positive weight $w$ , the weighted conditional expectation is $E_w(g\mid x) = E(wg\mid x)/E(w\mid x)$ . LogitBoost (Algorithm 3), population version, computes the working response and weight

z = \frac{y^*-p(x)}{p(x)(1-p(x))},\qquad w(x) = p(x)(1-p(x)),

fits $f(x) = E_w(z\mid x)$ (the population weighted least-squares regression of $z$ on $x$ ), and updates $F(x)\leftarrow F(x)+\tfrac12 f(x)$ .

Formalization targets

Goal: Result 3

Fix $x$ and let $\ell_x(t) = E[\,2y^*(F(x)+t) - \log(1+e^{2(F(x)+t)})\mid x]$ . Then $\ell_x$ has first derivative $s(x)$ and second derivative $H(x)$ at $t=0$ ,

s(x) = 2E\big(y^*-p(x)\mid x\big),\qquad H(x) = -4E\big(p(x)(1-p(x))\mid x\big),

$H(x)\neq0$ , and the population LogitBoost update equals the Newton update:

F(x) + \tfrac12E_w(z\mid x) = F(x) - H(x)^{-1}s(x).

Milestones

(31): the integrand of $E\,l(F+f)$ is the Bernoulli log-likelihood of the symmetric logistic model.
(32): the first derivative $s(x)$ .
(33): the second derivative $H(x)$ .
(34)–(35): $F(x) - H(x)^{-1}s(x) = F(x) + \frac12 \frac{E(y^*-p(x)\mid x)}{E(p(x)(1-p(x))\mid x)} = F(x)+\frac12E_w\big(\frac{y^*-p(x)}{p(x)(1-p(x))}\,\big|\,x\big)$ .
(36): the Newton update solves $\min_{f(x)} E_{w(x)}\big(F(x)+\frac12 z - (F(x)+f(x))\big)^2$ .

Significance

The result. Result 3 explains what LogitBoost computes: a stagewise Newton–Raphson ascent of the expected Bernoulli log-likelihood, one coordinate $F(x)$ at a time. It makes the working response and the weights of Algorithm 3 the score and curvature of the likelihood, and reduces each round to a weighted least-squares problem (36) that any regression method can solve.

Formalizing it. The result is proved on the page by a short calculation, and no machine-checked version exists. The mission produces a formal account of the population algorithm on an arbitrary joint law, with conditional expectations taken through a regular conditional distribution, the derivatives stated with differentiability, and the Newton step identified exactly, including the constants $2$ , $-4$ and $\tfrac12$ that the symmetric parametrization forces.

Difficulty

The algebra is short; the formal content is in keeping every object honest. The derivatives are of a conditional expectation in a parameter, so differentiation must pass through the integral against the conditional law. The second derivative needs the first derivative as a function of $t$ , not only its value at $0$ . The Newton step divides by $H(x)$ , which must be shown nonzero from $0<p(x)<1$ rather than assumed. A tempting shortcut, replacing the conditional expectation of the log-likelihood by its closed form in a free probability parameter, removes the joint law from the statement and is ruled out.

Formalization scope

Labels are Bool, with $y^*(\texttt{true}) = 1$ and $y^*(\texttt{false})=0$ . The joint law is a probability measure ν on X × Bool; $E(\cdot\mid x)$ is the integral against Mathlib's ν.condKernel x. Every statement is for every $x$ , conditional on $x$ as in the Derivation; because the label space is finite, no integrability or measurability hypotheses are needed.
The symmetric logistic is written exactly as (30), $e^{t}/(e^{t}+e^{-t})$ , not as $1/(1+e^{-t})$ , which differs by a factor $2$ in $t$ and would change every constant.
The conditional log-likelihood is defined as an integral against the conditional law, not by its closed form with a free parameter.
Derivatives are stated with HasDerivAt, never with deriv, which returns $0$ at non-differentiable points; $H(x)\neq0$ is a conclusion, so the division in the Newton step cannot silently return $0$ .
The weighted conditional expectation takes its weight as an explicit argument; here it is $p(x)(1-p(x))$ .
In (36) the page writes $E_{w(x)}$ without " $\mid x$ "; it is read as the conditional weighted expectation, since the Derivation conditions on $x$ throughout.
Out of scope: the data version of Algorithm 3 (regression trees, the $z_{\max}$ threshold and the weight floor of pp. 352–353), which are implementation choices, and the multiclass algorithm (§5).

Contributions welcome: differentiation of finite conditional expectations in a parameter, and derivative facts for the symmetric logistic, both reusable across the other missions of this series.

Selected references

J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. Syst. Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Mach. Learn. 37(3):297–336, 1999. https://doi.org/10.1023/A:1007614523901
J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5):1189–1232, 2001. https://doi.org/10.1214/aos/1013203451

7 thms3 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 4: The Continuous Master WMC Has Total Absolute Loss at Most ln(w_init/w_fin)/(1−β)Research Paper

Motivation

In sequential prediction, several forecasters can issue different answers for the same instance. A master algorithm must combine their advice before the true label is known. Littlestone and Warmuth's Weighted Majority framework gives worst-case guarantees for this setting: the instances and labels need not come from a probability distribution. The paper first studies binary predictions and then allows real predictions and labels in the unit interval. The continuous version matters when the distance between a prediction and a label carries information that a binary mistake count discards. The formal target here is the paper's total absolute-loss guarantee for that continuous master, WMC (Littlestone and Warmuth 1994, §5).

The result is part of the paper's generalized analysis, which also covers a binary master WMG and a randomized master WMR. These algorithms share a range of allowed weight updates, but their predictions and losses differ. This mission isolates WMC's deterministic, continuous-label theorem and the numbered lemmas on which its statement rests. The finite-sequence convention is explicit in the paper's notations and assumptions (Littlestone and Warmuth 1994, p. 220).

Setting

Fix a finite nonempty pool of $n$ forecasters and a finite sequence of $t$ trials. At trial $j$ , expert $i$ predicts $x_i^{(j)}\in[0,1]$ , and after the master predicts, a label $\rho^{(j)}\in[0,1]$ is revealed. Expert $i$ has weight $w_i^{(j)}$ before that trial. Every initial weight is positive, and weights remain nonnegative. The total weight and weighted mean prediction are

s^{(j)}=\sum_{i=1}^{n}w_i^{(j)},\qquad \gamma^{(j)}=\frac{\sum_{i=1}^{n}w_i^{(j)}x_i^{(j)}}{s^{(j)}}.

WMC predicts $\gamma^{(j)}$ . Its loss on the trial is the absolute error $|\gamma^{(j)}-\rho^{(j)}|$ , and its total absolute loss is $m=\sum_{j=1}^{t}|\gamma^{(j)}-\rho^{(j)}|$ . Write $w_{\mathrm{init}}=s^{(1)}$ and $w_{\mathrm{fin}}=s^{(t+1)}$ for total weight before the first and after the final update (Littlestone and Warmuth 1994, pp. 232–233).

WMC updates on every trial. For $0\le\beta<1$ , it multiplies each weight by a factor $F_i^{(j)}$ in the interval

\beta^{|x_i^{(j)}-\rho^{(j)}|}\le F_i^{(j)}\le 1-(1-\beta)|x_i^{(j)}-\rho^{(j)}|, \qquad w_i^{(j+1)}=F_i^{(j)}w_i^{(j)}.

The factor may depend on both trial and expert. The paper permits any choice in this interval, so WMC denotes a class of runs rather than one fixed recurrence. Its convention $0^0=1$ is used when $\beta=0$ and an expert has zero error (Littlestone and Warmuth 1994, p. 233, eq. (5.1)).

Formalization targets

Theorem 5.2: WMC total loss

For every run with positive final total weight, the target is the paper's explicit inequality

m\le\frac{\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})}{1-\beta}.

The bound uses the run's actual initial and final weights, so it applies whether the upper or lower permitted update factor was selected, or a factor between them. The finite-valued statement assumes $w_{\mathrm{fin}}>0$ ; the paper regards the bound as vacuous when the denominator of the logarithm is zero (Littlestone and Warmuth 1994, p. 236, Theorem 5.2).

Supporting numbered results

Lemma 5.1 states $\beta^r\le1+r(\beta-1)$ for $\beta\ge0$ and $0\le r\le1$ , ensuring the update interval is nonempty. Lemma 5.2 states the logarithmic potential estimate under only the update's upper inequality, including the special case in which $\beta=0$ and a master's unit loss forces the final total weight to zero. Lemma 5.3 turns those same conditions into the displayed total-loss bound. Each is a separate milestone with the paper's statement and page provenance (Littlestone and Warmuth 1994, pp. 233–236).

Significance

The theorem controls the master's accumulated real-valued prediction error by an observable change in the total pool weight. It requires no distributional assumption on the trial sequence and no single choice of update factor. That breadth lets the same estimate be used for different update rules within the allowed range, while the explicit $1/(1-\beta)$ constant records the dependence on the algorithm's parameter. The paper also uses Lemma 5.3 in its analysis of WMR's expected loss (Littlestone and Warmuth 1994, pp. 236, 240).

The paper proves these results; this mission asks for machine-checked proofs of their exact Lean statements. Its definition of a permitted continuous run and its upper-update potential conditions can also support subsequent formalizations of WMG and WMR. Lemma 5.1, the potential estimate, and the final loss bound remain distinct proof targets so that a solver can use or improve the underlying analytic infrastructure without changing the goal.

Difficulty

A binary mistake indicator cannot express the magnitude of an error between two unit-interval values. The generalized update contains a real exponent, absolute values, and a range of legal factors. An argument that handles only a selected endpoint of that range would leave permitted WMC runs uncovered. A further boundary occurs at $\beta=0$ : an allowed update can reduce a positive weight to zero, and real logarithms in Lean have a defined value at zero although the paper's logarithmic bound is infinite there. The formal statements therefore distinguish the zero-final-weight clause from the finite-logarithm clause.

Formalization scope

The pool is Fin n with $n>0$ and the trials are Fin t; an empty sequence of trials is allowed. Lean's trial index starts at zero, so w 0 represents $w^{(1)}$ and w t represents the weights after all $t$ trials. The inputs are the prediction array and label array. Instances are not stored separately because the theorem refers to them only through expert predictions. Values, factors, totals, and losses are real numbers. The run predicate requires positive initial weights, nonnegative weights, predictions and labels in $[0,1]$ , $0\le\beta<1$ , and a permitted factor for every expert on every trial.

The theorem quantifies over every permitted run. A sorry-free local example exhibits a one-trial run with positive final weight, ruling out a globally empty run predicate. For positive final weight, the update conditions ensure earlier total weights are positive, so every weighted mean used in the loss has its intended denominator. The finite logarithmic conclusions assume positive final weight because Real.log 0 would otherwise introduce an unrelated total-function value. The definition layer supplies total weight, weighted mean, loss, base conditions, the upper-update conditions, and WMC runs; the proof development needs finite-sum and real logarithm inequalities from Mathlib. Contributions that establish the three numbered lemmas or the goal under this interface are in scope.

Selected references

Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.

6 thms3 active usersReviewed

Optimization Probability Statistics·Captain: mikedeng1

Learning Models with Uniform Performance via Distributionally Robust Optimization 2: A Minimax Lower Bound of Order n^(−1/2) ∨ n^(−1/k*) for Estimating the Cressie–Read Robust Risk (Theorem 3)Research Paper

Motivation

Distributionally robust optimization replaces the expected loss $\mathbb E_{P_0}[\ell(\theta; X)]$ of a statistical model by its worst case over all distributions $Q$ close to the data distribution $P_0$ . When closeness is measured by an $f$ -divergence ball $\{Q : D_f(Q\|P_0) \le \rho\}$ of fixed radius $\rho > 0$ , the robust risk upper-bounds the risk of every subpopulation of $P_0$ that has sufficiently large probability, so a model with small robust risk performs uniformly well across latent subgroups. This is the program of J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization (arXiv:1810.08750; Ann. Statist. 49 (2021), doi:10.1214/20-AOS2004).

The robust risk is itself a statistical functional. It is estimated by plugging in the empirical distribution, and the paper shows (its Theorem 2) that for the Cressie–Read family of divergences with parameter $k$ the plug-in estimate concentrates at rate $n^{-1/(k_* \vee 2)}$ , with $k_* = k/(k-1)$ . For small $k$ (heavy protection against distribution shift) $k_*$ is large and this rate is far slower than the parametric $n^{-1/2}$ . This mission formalizes the paper's answer to whether the slow rate is an artefact of the plug-in estimator or intrinsic: its Theorem 3, a minimax lower bound valid for every estimator.

Setting

Fix $k \in (1,\infty)$ and write $k_* = k/(k-1)$ . The Cressie–Read function is

f_k(t) = \frac{t^k - kt + k - 1}{k(k-1)} \quad (t \ge 0), \qquad f_k(t) = +\infty \quad (t < 0).

For a probability measure $P$ , a real random variable $Z$ and a radius $\rho > 0$ , the robust risk is

\mathcal R_k(Z) = \sup\Bigl\{ \mathbb E_P[LZ] : L \ge 0,\ \mathbb E_P[L] = 1,\ \mathbb E_P[f_k(L)] \le \rho \Bigr\},

the supremum of $\mathbb E_Q[Z]$ over distributions $Q \ll P$ with likelihood ratio $L = dQ/dP$ and Cressie–Read divergence $D_{f_k}(Q\|P) = \mathbb E_P[f_k(L)]$ at most $\rho$ .

Write

c_k(\rho) = (1 + k(k-1)\rho)^{1/k}, \qquad p_k = (1 + k(k-1)\rho)^{-1/(k-1)}, \qquad \beta_k = \frac{k(k-1)\rho}{2(1+k(k-1)\rho)} .

Fix $M > 0$ and let $\mathcal P$ be the set of all distributions on the two points $\{0, M\}$ ; each is determined by its mass $p \in [0,1]$ at $M$ . An estimator is any function $\widehat R : \{0, M\}^n \to \mathbb R$ of a sample $Z_1^n = (Z_1, \dots, Z_n)$ drawn i.i.d. from $P_0 \in \mathcal P$ . The minimax risk of estimating the robust risk is

\mathfrak M_n(\mathcal P, f_k) = \inf_{\widehat R}\ \sup_{P_0 \in \mathcal P}\ \mathbb E_{P_0^n}\bigl|\widehat R(Z_1^n) - \mathcal R_k(Z)\bigr|, \qquad Z \sim P_0. \qquad (16)

The total variation distance between two product laws $P^n, P'^n$ on the finite set $\{0,M\}^n$ is $\|P^n - P'^n\|_{\mathrm{TV}} = \tfrac12\sum_z |P^n\{z\} - P'^n\{z\}|$ , and $D_{\mathrm{kl}}$ denotes the Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 3

For every $n \ge 1$ ,

\mathfrak M_n(\mathcal P, f_k) \ge M \max\Biggl\{ \frac{1}{8 k_* p_k}\Bigl( \sqrt{\frac{p_k(1-p_k)}{16 n}} \wedge \tfrac12(1-p_k) \wedge p_k \Bigr),\ \ \frac18 \beta_k^{1/k} c_k(\rho) \Bigl( \frac{1}{4n} \wedge p_k \wedge \bigl(1 - (1-\beta_k)^{1-k_*} p_k\bigr) \Bigr)^{1/k_*} \Biggr\}.

The first branch is of order $n^{-1/2}$ , the second of order $n^{-1/k_*}$ . The page prints $8n$ in the first branch; the target uses $16n$ (see Formalization scope).

Milestones

Lemma 12 (three claims): for $Z$ equal to $z_0 \le z_1$ with probabilities $1-p$ , $p$ : if $p \ge p_k$ then $\mathcal R_k(Z) = z_1$ ; if $p \le p_k$ then $\mathcal R_k(Z) \le c_k p^{1/k_*} z_1 + (1 - c_k p^{1/k_*}) z_0$ ; and if $p \le p_k \wedge (1 - (1-\beta)^{1-k_*} p_k)$ for some $\beta \in (0,1)$ then $\mathcal R_k(Z) \ge \beta^{1/k} c_k p^{1/k_*} z_1 + (1 - \beta^{1/k} c_k p^{1/k_*}) z_0$ .
The primal two-point formula (p. 47): for $p \in (0,1)$ ,

\mathcal R_k(Z) = z_0 + (z_1 - z_0)\sup\{q \in [0,1] : (1-p)^{1-k}(1-q)^k + p^{1-k}q^k \le c_k^k\}.

Le Cam's reduction (37): if $|\mathcal R_k(P_0) - \mathcal R_k(P_1)| \ge 2\delta > 0$ then $\mathfrak M_n \ge \frac\delta2(1 - \|P_0^n - P_1^n\|_{\mathrm{TV}})$ .
The Taylor display $c_k(p_k - \delta)^{1/k_*} \le 1 - \frac{1}{k_*}c_k^{k_*}\delta$ for $0 < \delta \le p_k$ .
The KL display $D_{\mathrm{kl}}(P_2\|P_1) \le 8\delta^2/(p_k(1-p_k))$ for the laws with masses $p_k \mp \delta$ at $M$ .
Pinsker for products $\|P_1^n - P_2^n\|_{\mathrm{TV}}^2 \le \frac n2 D_{\mathrm{kl}}(P_2\|P_1)$ .
The second-branch KL display $-\log(1-\delta) \le \delta/(1-\delta) \le 2\delta$ for $\delta \le \frac12$ .

Significance

Theorem 3 shows that the rate $n^{-1/(k_* \vee 2)}$ of the paper's concentration bound for the plug-in robust risk cannot be improved by any estimator, even when the data take only two values. For $k < 2$ the robust risk is therefore intrinsically harder to estimate than a mean: its value depends on how much mass $P_0$ puts on rare large values, and rare events are observed rarely. The same phenomenon drives the paper's lower bounds for minimizing the robust risk (its Section 5.2), which are not part of this mission.

The result is proved in the paper; no machine-checked version of it or of Lemma 12 is known. Formalizing it produces a verified two-point analysis of the Cressie–Read robust risk (Lemma 12 and its primal formula), which is reusable for any lower bound or worked example involving $f$ -divergence balls, and a verified finite-sample Le Cam two-point bound for estimating a functional of a distribution on two points. It also corrects a constant in the first branch of the printed statement.

Difficulty

The lower bound needs two distributions on $\{0,M\}$ that are statistically close yet have well-separated robust risks. Both requirements must be quantitative and must hold simultaneously at the stated constants. The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so the separation needs exact control of that supremum for two-point laws: an exact value above the threshold $p_k$ , and matching upper and lower bounds below it. For mass near $p_k$ the separation is linear in $\delta$ , while for small mass it is of order $\delta^{1/k_*}$ , which is where the slow rate comes from. Closeness requires the KL divergence of each pair to be at most $1/(2n)$ , and the two branches need different perturbations. A naive bound on the robust risk by $\max(z_0, z_1)$ or by the mean gives no separation at all.

Formalization scope

The Lean development lives in the namespace UniformDRO.LowerBound. Its conventions are:

$k > 1$ , $\rho > 0$ , $M > 0$ (all on the page); $n \ge 1$ in the goal (implicit on the page, since the bound contains $1/n$ ).
The robust risk is the real supremum in the likelihood-ratio form above, with the divergence constraint written as a lower Lebesgue integral of $f_k(L) \ge 0$ . Absolute continuity $Q \ll P$ is built in. For a two-point law the feasible values lie between the two points, so the supremum is genuine.
Laws on $\{0,M\}$ are $(1-p)\delta_0 + p\,\delta_M$ , $p \in [0,1]$ . Expectations under $P_0^n$ are finite sums over $\{0,M\}^n$ . The minimax risk takes values in $[0,\infty]$ , with the infimum over all real functions of the sample taken outside the supremum over $p$ . For these laws it agrees with the platform's general HighDimStat.Minimax.minimaxRisk.
$D_{\mathrm{kl}}$ between two-point laws is the platform's BanditAlgorithm.bernoulliRelativeEntropy, always evaluated with a second argument in $(0,1)$ , where it is the true divergence.
Real powers are Real.rpow. The primal formula is stated for $p \in (0,1)$ , where its negative powers are finite.
Correction of the print. In Theorem 3 the page has $\sqrt{p_k(1-p_k)/(8n)}$ . The paper's argument with that choice gives $D_{\mathrm{kl}} \le 1/n$ and, by Pinsker, total variation at most $1/\sqrt2$ , which does not yield the printed constant $1/(8k_*p_k)$ . The target uses $16n$ , for which the same argument gives total variation at most $\tfrac12$ and exactly the printed constant. The second branch is as printed. The milestone quotes keep the page's text.

The goal is the lower bound on the minimax risk (16) over all estimators and all laws on $\{0,M\}$ . It does not mention the two hypotheses, $\delta$ , total variation or KL divergence, so it cannot be satisfied by a statement about a particular pair of laws or a particular estimator.

Contributions are welcome at every level: proofs of Lemma 12 through the primal formula or through the dual representation of the robust risk, a general finite-space Le Cam lemma, and tensorization of KL and Pinsker for finite products, which are reusable beyond this mission.

Selected references

J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization, Ann. Statist. 49(3), 2021; arXiv:1810.08750v6. https://arxiv.org/abs/1810.08750, https://doi.org/10.1214/20-AOS2004
L. Le Cam, Asymptotic Methods in Statistical Decision Theory, Springer, 1986. https://doi.org/10.1007/978-1-4612-4946-7
B. Yu, Assouad, Fano, and Le Cam, in Festschrift for Lucien Le Cam, Springer, 1997, 423–435. https://doi.org/10.1007/978-1-4612-1880-7_29
A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
N. Cressie and T. R. C. Read, Multinomial goodness-of-fit tests, J. R. Stat. Soc. B 46(3), 1984, 440–464. https://doi.org/10.1111/j.2517-6161.1984.tb01318.x

13 thms3 active usersReviewed

Probability Statistics·Captain: mikedeng1

Fast Rates for Support Vector Machines Using Gaussian Kernels 1: Under Tsybakov and Geometric Noise, Gaussian-Kernel SVMs Reach Excess Risk Cx²n^{−β+ε} with Probability 1 − e^{−x}Research Paper

Motivation

Support vector machines classify observations by choosing a real-valued function from a reproducing kernel Hilbert space and using its sign as the predicted label. The Gaussian kernel is widely used because it gives a flexible class of functions, but that flexibility alone does not explain how quickly classification error approaches the best possible error as the training sample grows. Steinwart and Scovel's 2007 paper identifies distributional conditions under which a Gaussian-kernel SVM achieves a polynomial, and sometimes nearly linear, excess-risk rate. The conditions describe both ambiguity in the labels and the location of data relative to the decision boundary.

The article's result is already proved mathematically. This mission asks for machine-checked statements and proofs of its finite-geometric-exponent, no-offset rate and selected supporting results. It uses arXiv:0708.1838v1, the electronic reprint of the Annals of Statistics article. Its printed page number equals its PDF page number throughout; all page references below use those numbers.

Setting

Let $X$ be the closed unit ball of $\mathbb R^d$ , where $d>0$ , and let the label set be $Y=\{-1,1\}$ . A distribution $P$ on $X\times Y$ has input marginal $\mu=P_X$ and a measurable regression function $\eta(x)=P(y=1\mid x)$ . In the Lean representation, $\mu$ and one version of $\eta$ are carried explicitly; the joint law gives conditional masses $\eta(x)$ and $1-\eta(x)$ to the two labels. Classification predicts $\operatorname{sign}f(x)$ , with $\operatorname{sign}(0)=1$ . Write $R_P(f)$ for its error probability and $R_P$ for the smallest such risk over measurable decision functions.

The hinge loss is $\ell(y,t)=\max\{0,1-yt\}$ . The Gaussian kernel with parameter $\sigma>0$ is $k_\sigma(x,x')=\exp(-\sigma^2\|x-x'\|^2)$ , and $H_\sigma(X)$ is its restricted RKHS. Given a sample $T$ of size $n$ , an SVM without offset minimizes $\lambda\|f\|^2_{H_\sigma(X)}+R_{\ell,T}(f)$ over that space. The approximation error $a_\sigma(\lambda)$ is the infimum of the corresponding population objective minus the unrestricted Bayes hinge risk; equation (6) uses that unrestricted baseline.

Two assumptions describe the distribution. It has Tsybakov noise exponent $q\in[0,\infty]$ if, for sufficiently small $t>0$ , $\mu\{|2\eta-1|\le t\}\le C t^q$ for some $C>0$ . To define geometric noise exponent $\alpha>0$ , partition $X$ according to whether $\eta$ is below, above, or equal to $1/2$ . The distance $\tau_x$ goes from a point in either strict class to the opposite strict class together with the equal-probability class. The geometric condition is

\int_X |2\eta(x)-1|\exp(-\tau_x^2/t)\,d\mu(x) \le C t^{\alpha d/2}\qquad(t>0).

These are Definitions 2.2 and 2.3 and equation (7) of the paper.

Formalization targets

The goal is the finite- $\alpha$ , no-offset clause of Theorem 2.8. With the paper's two-case exponent $\beta=\beta(\alpha,q)$ , set $\lambda_n=n^{-(\alpha+1)\beta/\alpha}$ and $\sigma_n=n^{\beta/(\alpha d)}$ . For every $\varepsilon>0$ , one constant $C>0$ works uniformly for $x\ge1$ and $n\ge1$ :

\Pr^*\!\left\{T:R_P(f_{T,\lambda_n}) \le R_P+C x^2n^{-\beta+\varepsilon}\right\}\ge1-e^{-x}.

Here $\Pr^*$ is outer probability, and the statement applies to every empirical minimizer. The formula for $\beta$ is $\alpha/(2\alpha+1)$ in the first case, $\alpha\le(q+2)/(2q)$ , and $2\alpha(q+1)/(2\alpha(q+2)+3q+4)$ otherwise; the paper's limiting convention specifies $q=\infty$ .

Three milestones record results used on this path. Theorem 2.1 bounds empirical covering numbers of Gaussian RKHS balls, uniformly in $\sigma$ and the sample. Lemma 4.1 locates balls of radius $\tau_x$ inside the corresponding enlarged decision class. Theorem 2.7 bounds the approximation error by

a_\sigma(\lambda)\le c_d\bigl(\sigma^d\lambda+C(2d)^{\alpha d/2}\sigma^{-\alpha d}\bigr),

where $c_d$ depends only on dimension. Their exact source text and page positions appear in the milestone list.

Significance

Theorem 2.8 gives a quantitative guarantee for classification risk, rather than only convergence of the regularized hinge objective. The rate responds to both the label-noise exponent and the concentration of input mass near the decision boundary. In the regimes discussed after the theorem, the exponent can approach one; the paper's Remark 2.9 compares it with the $n^{-1/2}$ benchmark.

Formalizing this result adds a concrete Gaussian RKHS norm compatible with a kernel parameter that changes with $n$ , an explicit binary-law model, extended-valued risks and covering numbers, and source-indexed bounds on approximation and complexity. Those objects can be reused in later SVM and kernel-learning statements. The paper's argument is a published proof; the Lean theorem files here are open proof obligations, while the definition files have compiled bodies. No claim of a machine-checked proof of the rate is made.

Difficulty

It is not enough to combine a general consistency theorem with the noise assumptions. The kernel parameter grows with sample size, so the relevant hypothesis class changes with $n$ ; a complexity estimate for one fixed class gives no uniform rate. Geometric noise controls approximation error, while Tsybakov noise controls a different fluctuation quantity, and neither by itself supplies the stated exponent. The probability statement also concerns an event defined by empirical minimizers, whose measurability the source deliberately avoids by using outer probability. These are the points at which a direct fixed-class or ordinary-probability statement would fail to match Theorem 2.8.

Formalization scope

Lean represents functions on all of $\mathbb R^d$ but uses only their restrictions to $X$ . The joint distribution is built from a probability marginal and a fixed measurable $\eta:\mathbb R^d\to[0,1]$ . This makes the paper's choice of regression-function version explicit. The Gaussian RKHS squared norm is the supremum over finite normalized kernel-section combinations; it is $+\infty$ outside the RKHS. A covering number is the least positive finite cardinality of a cover with centers in the ambient empirical function space, or $+\infty$ if there is no such cover. Hinge and classification risks are extended nonnegative integrals, and Bayes risks range over measurable functions.

The assumptions $d>0$ and $n\ge1$ give the divisions and powers their intended domains. For $q=\infty$ , the small- $t$ noise bound uses zero on the right, as in the source convention. The paper leaves distance to an empty set unstated; this mission pins $d(x,\varnothing)=0$ . With the infinite-distance convention, Lemma 4.1 and Theorem 2.7 fail for a one-class regression function. The proof display (25) has a volume-factor slip in high dimension; Theorem 2.7 is stated with its printed conclusion, and the issue is recorded in the moderation notes. The goal event includes existence of an empirical minimizer, a fact stated in the paper's setup, and quantifies over every minimizer. This excludes a vacuous SVM predicate. The constant $C$ is chosen before $x$ and $n$ .

The clauses for $\alpha=\infty$ and an SVM with offset are outside this mission. The separate series mission addresses the implication from an envelope assumption to geometric noise. Further contributions toward the §5 empirical-process estimates, §6 variance estimates, and §7 shrinking and general-rate theorems are welcome; they are not asserted as milestones in this draft.

Selected references

Ingo Steinwart and Clint Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 2007, 575–607. arXiv:0708.1838v1, DOI:10.1214/009053606000001226.

11 thms3 active usersReviewed

Probability Statistics·Captain: mikedeng1

Empirical Bernstein Bounds and Sample Variance Penalization: Sample Variance Penalization Has Excess Risk at Most √(32V(f*,μ)ln(3M(n)/δ)/n) + 22ln(3M(n)/δ)/(n−1) (Theorem 15)Research Paper

Motivation

Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order $\sqrt{1/n}$ whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order $\sqrt{\mathbb V Z/n} + 1/n$ , but the variance $\mathbb V Z$ is unknown, so the bound cannot be evaluated from data.

Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger $1/n$ term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).

Setting

For a vector $x = (x_1,\dots,x_n)$ of reals, the sample mean and sample variance are

P_n(x) = \frac1n\sum_{i=1}^n x_i, \qquad V_n(x) = \frac{1}{n(n-1)}\sum_{i,j=1}^n\frac{(x_i-x_j)^2}{2}.

Let $\mu$ be a probability distribution on a set $\mathcal X$ , and $\mathcal F$ a class of hypotheses (loss functions) $f:\mathcal X\to[0,1]$ . For $f\in\mathcal F$ , its risk is $P(f,\mu) = \mathbb E f(X)$ and its variance is $V(f,\mu)=\mathbb V f(X)$ , with $X\sim\mu$ . For a sample $\mathbf X = (X_1,\dots,X_n)\sim\mu^n$ , $P_n(f,\mathbf X)$ and $V_n(f,\mathbf X)$ are $P_n$ and $V_n$ of the vector $(f(X_1),\dots,f(X_n))$ .

The complexity of $\mathcal F$ enters through the growth function. For $x\in\mathcal X^m$ let $\mathcal F(x) = \{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}\subseteq\mathbb R^m$ , and let $\mathcal N(\epsilon, A, \|\cdot\|_\infty)$ be the least number of sup-norm $\epsilon$ -balls centred in $A$ that cover $A$ . Then

\mathcal N_\infty(\epsilon,\mathcal F,m) = \sup_{x\in\mathcal X^m}\mathcal N(\epsilon,\mathcal F(x),\|\cdot\|_\infty), \qquad \mathcal M(n) = 10\,\mathcal N_\infty(1/n,\mathcal F,2n).

For $\lambda\ge0$ , sample variance penalization selects

SVP_\lambda(\mathbf X) = \arg\min_{f\in\mathcal F}\; P_n(f,\mathbf X) + \lambda\sqrt{\frac{V_n(f,\mathbf X)}{n}}.

With $\lambda = 0$ it is empirical risk minimization.

Formalization targets

Goal: Theorem 15 (p. 6)

Fix $\delta\in(0,1)$ , $n\ge2$ , $\lambda = \sqrt{18\ln(3\mathcal M(n)/\delta)}$ and any $f^*\in\mathcal F$ . With probability at least $1-\delta$ in $\mathbf X\sim\mu^n$ ,

P(SVP_\lambda(\mathbf X),\mu) - P(f^*,\mu) \le \sqrt{\frac{32\,V(f^*,\mu)\ln(3\mathcal M(n)/\delta)}{n}} + \frac{22\ln(3\mathcal M(n)/\delta)}{n-1}.

The constants are the paper's. The goal is stated for an arbitrary comparator $f^*$ , so it covers an optimal one when one exists.

Milestones

In the order of the proof:

the fourth-moment inequality (Lemma 8, Corollary 9);
the self-bounding concentration inequality the paper cites (Theorem 7, lower and upper tails);
the tails (5)–(6) of the sample variance and the standard-deviation bounds of Theorem 10;
the comparison $W\le\mathbb EV_n$ of (7)–(9);
Bennett's inequality for independent variables, together with the i.i.d. Theorem 3;
the empirical Bernstein bounds (Theorem 4 for i.i.d. variables, Theorem 11 for independent ones);
the Lipschitz properties of the confidence functionals $\Phi,\Psi$ (Lemma 12);
the symmetrization lemma (Lemma 13) and the swap bound (Lemma 14);
the uniform bound, Theorem 6:

\Pr\Big\{\exists f\in\mathcal F:\ P(f,\mu)-P_n(f,\mathbf X) > \sqrt{\tfrac{18V_n(f,\mathbf X)\ln(\mathcal M(n)/\delta)}{n}} + \tfrac{15\ln(\mathcal M(n)/\delta)}{n-1}\Big\}\le\delta \quad (n\ge16).

Significance

Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as $\ln\mathcal M(n)/n$ ; for a finite class $\mathcal M(n)$ does not depend on $n$ and the rate is $1/n$ . The paper gives a two-hypothesis example where empirical risk minimization cannot beat order $1/\sqrt n$ (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.

All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a $1/n$ -normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.

Difficulty

Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for $V_n$ itself with the right dependence on $\mathbb EV_n$ , and $V_n$ is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.

The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.

Formalization scope

Conventions:

The source is arXiv:0907.3740v1. It has no printed page numbers, so every page cited is the PDF page.
Indices $i=1,\dots,n$ are i : Fin n.
A sample is a vector Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in $[0,1]$ " have laws giving zero mass outside $[0,1]$ .
"With probability at least $1-\delta$ , $A$ " is written as $\mu^n\{\neg A\}\le\delta$ . For a set that is not measurable this is the outer measure.
$P_n$ is the published VarianceRegularization.Expansion.empMean. $V_n$ is a local sampleVar with the $1/(n(n-1))$ normalization. $V(f,\mu)$ is Mathlib's variance.
The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in the set, values in $\mathbb N\cup\{\infty\}$ ).
$\Pr_\sigma$ and $\mathbb E_\sigma$ are uniform averages over the $2^n$ sign vectors.
$SVP_\lambda$ is an arbitrary selector that returns, for every sample, a minimizer in $\mathcal F$ of the penalized objective. Every minimizer is covered.

Added hypotheses and repaired statements, each disclosed in the item:

The paper says "questions of measurability will be ignored throughout". This is made precise as follows:
- Theorems 6 and 15: $\mathcal F$ is countable and its members are measurable.
- Lemma 13: the function is measurable.
- Theorem 7: $Z$ is measurable, integrable and nonnegative, and its coordinate-wise infima are measurable.
Theorems 6 and 15 assume $\mathcal N_\infty(1/n,\mathcal F,2n)<\infty$ . With an infinite value the printed bound is vacuous.
Theorems 4 and 11 and Lemmas 12 and 14 add $n\ge2$ . Theorem 3 and Bennett's display add $n\ge1$ . Without these, Lean's convention $1/0=0$ makes the printed formulas false at the excluded $n$ .
Corollary 9's "set" $\{x_1,\dots,x_n\}$ is read as a list, so repetitions are allowed.

Ruled-out trivializations:

SVP is not defined as the comparator $f^*$ .
$\lambda$ is pinned to $\sqrt{18\ln(3\mathcal M(n)/\delta)}$ .
$V_n$ is the sample variance, not the true variance.
No measurability of the bad event or of the selector is assumed.

A complete development needs the following:

the entropy method for self-bounding functions (Theorem 7);
Bennett's inequality for independent non-identical bounded variables;
product-measure symmetrization;
covering-number bookkeeping.

The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.

Selected references

A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009; arXiv:0907.3740v1, 2009. https://arxiv.org/abs/0907.3740
A. Maurer, Concentration inequalities for functions of independent variables, Random Structures & Algorithms 29, 121–138, 2006. https://doi.org/10.1002/rsa.20105
C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998.
J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation trade-off using variance estimates in multi-armed bandits, Theoretical Computer Science 410(19), 2009. https://doi.org/10.1016/j.tcs.2009.01.016
V. Mnih, Cs. Szepesvári, J.-Y. Audibert, Empirical Bernstein stopping, ICML 2008. https://doi.org/10.1145/1390156.1390241
W. Hoeffding, Probability inequalities for sums of bounded random variables, JASA 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017; arXiv:1610.02581. https://arxiv.org/abs/1610.02581

21 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 2: Without a Bound on y^NV, Expanding-Projection AIM Has Regret ≤ max{b,h}(T^{δ−1/2} + T^{−1/2} + (y^NV)^{1+2/δ}/T)Research Paper

Motivation

A retailer who restocks a product every period must pick an order-up-to level without knowing the demand distribution. When a period ends with an empty shelf, the retailer records only its sales, so the true demand above the stock level is censored. The classical newsvendor solution, the critical fractile of the demand distribution, cannot be computed. Huh and Rusmevichientong (Math. Oper. Res., 2009) treat this as an online convex optimization problem: the expected one-period cost is convex in the stock level, and its derivative can be estimated without bias from the censored observation alone. Their Adaptive Inventory Management (AIM) algorithm is a projected stochastic subgradient method in the style of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). Its average expected cost converges to the newsvendor cost at rate $O(1/\sqrt T)$ .

That analysis assumes that the manager knows an upper bound $\bar y$ on the newsvendor quantity, and the algorithm projects onto $[0,\bar y]$ . This mission formalizes §3.1 of the paper, which removes the assumption. The projection interval grows with time, and the regret bound is explicit in the unknown newsvendor quantity. Earlier adaptive schemes for censored newsvendor problems include Godfrey and Powell (2001) and Burnetas and Smith (2000).

Setting

Periods are $t = 1, 2, \dots$ . Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with finite mean and distribution function $F$ . Inventory is perishable: every period starts empty, so the stock level is exactly the order-up-to level. With holding cost $h > 0$ per unit left over and shortage cost $b > 0$ per unit of unmet demand, the expected one-period cost at level $y \ge 0$ is

Q(y) = h\,E[y-D]^+ + b\,E[D-y]^+ .

The newsvendor quantity is $y^{NV} = \inf\{y \ge 0 : F(y) \ge b/(b+h)\}$ , the minimizer of $Q$ .

Write $\bar B = \max\{b,h\}$ and $P_{[0,a]}(z) = \max\{\min\{z,a\},0\}$ . After period $t$ , the manager observes whether demand fell short of the stock level and forms the signal

H_t(y) = \begin{cases} h, & D_t < y,\\ -b, & D_t \ge y.\end{cases}

Fix $\delta \in (0, 1/2)$ . The modified AIM algorithm starts from a level $\hat y^\delta_1 \in [0,1]$ and updates

\hat y^\delta_{t+1} = P_{[0,\,t^{\delta/2}]}\!\left(\hat y^\delta_t - \epsilon_t H_t(\hat y^\delta_t)\right), \qquad \epsilon_t = \frac{1}{\bar B\sqrt t}.

Neither the step size nor the projection interval uses any bound on $y^{NV}$ . The level $\hat y^\delta_t$ depends only on $D_1, \dots, D_{t-1}$ , and only through the censored observations.

Formalization targets

Goal: Theorem 7 (p. 11)

For every $\delta \in (0, 1/2)$ and every $T \ge 1$ ,

E\left[\frac1T\sum_{t=1}^T Q(\hat y^\delta_t)\right] - Q(y^{NV}) \le \max\{b,h\}\left[\frac{1}{T^{0.5-\delta}} + \frac{1}{T^{0.5}} + \frac{(y^{NV})^{1+2/\delta}}{T}\right].

The bound holds uniformly over all demand laws with finite mean. The price of not knowing $\bar y$ is the slower rate $T^{\delta - 1/2}$ and a transient term in which $y^{NV}$ enters polynomially.

Milestones (proof of Theorem 7, p. 12)

One-step inequality, the instance of Eq. (15) (Appendix A, p. 16) used in the proof. For each $t$ with $y^{NV} \le t^{\delta/2}$ ,

E[Q(\hat y^\delta_t) - Q(y^{NV})] \le \frac{E|\hat y^\delta_t - y^{NV}|^2}{2\epsilon_t} - \frac{E|\hat y^\delta_{t+1} - y^{NV}|^2}{2\epsilon_t} + \frac{\epsilon_t}{2} E|H_t(\hat y^\delta_t)|^2 .

Eq. (10): early rounds, where the projection interval has not yet reached $y^{NV}$ :

E\Big[\sum_{1 \le t \le T,\ t < (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\,(y^{NV})^{1+2/\delta}.

Eq. (11): late rounds:

E\Big[\sum_{1 \le t \le T,\ t \ge (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\, T^{0.5+\delta} + \bar B\, T^{0.5}.

Significance

The result. Theorem 7 shows that a distribution-free, censored-data policy can be asymptotically optimal without any prior bound on the optimal stock level. The only inputs are $b$ , $h$ and the tuning parameter $\delta$ . The explicit constant separates two effects. A transient cost grows with $y^{NV}$ and vanishes like $1/T$ . A steady-state rate $T^{\delta-1/2}$ approaches the known-bound rate $T^{-1/2}$ as $\delta \to 0$ , at the cost of a larger transient. The expanding-projection device applies to other stochastic subgradient methods whose feasible region is unbounded.

Formalizing it. The theorem is proved in the paper, but as far as is known it has no machine-checked proof. The mission produces the modified algorithm as an explicit function of the demand path, the per-step stochastic gradient inequality with a time-varying projection, and the two-phase regret decomposition. The per-step inequality with a varying domain is reusable for other growing-domain online methods.

Difficulty

The standard projected-gradient analysis compares every iterate with a fixed minimizer in a fixed compact set, and it bounds the telescoping distance terms by the diameter of that set. Neither applies here. In the early rounds the projection interval does not contain $y^{NV}$ , so the distance to $y^{NV}$ can grow from step to step. Once the interval contains $y^{NV}$ , the diameter that controls the telescoping sum grows with $t$ . The step sizes and the growing radii must be traded against each other through Abel summation. The bound on $E[H_t(\hat y^\delta_t)(\hat y^\delta_t - y^{NV})]$ needs the conditional-expectation argument that $H_t$ is an unbiased subgradient of $Q$ at a random point independent of $D_t$ . Applying the known-bound theorem with $\bar y$ replaced by $T^{\delta/2}$ does not work, because the algorithm is not given $T$ and the projection radius changes at every step.

Formalization scope

Demand: CappedBaseStock.DemandLaw (a probability law on $\mathbb R_{\ge 0}$ with finite and strictly positive mean) and the i.i.d. path demandPathLaw (Measure.infinitePi), from the published definition CappedBaseStock_Model. The path is zero-based: the paper's $D_t$ is coordinate $t-1$ . The positive-mean field is not needed by Theorem 7. It excludes only $D = 0$ almost surely.
$Q$ and $y^{NV}$ : backorderCost and newsvendorLevel from the published definition LostSalesOrderUpTo.Asymptotic.Backorder. Real levels are passed through Real.toNNReal, and the levels involved are always nonnegative.
The algorithm modAimTarget δ b h ŷ₁ d t is a deterministic recursion on the demand path, and expectations are Bochner integrals over the path measure. All integrands are bounded and measurable, so no non-integrability default enters.
Explicit readings of the paper's loose phrases:
- the first level, which the paper leaves unspecified, is assumed to satisfy $\hat y^\delta_1 \in [0,1]$ ; the theorem fails without it;
- $0 < b$ and $0 < h$ are assumed;
- the sums in (10) and (11) are restricted to $1 \le t \le T$ ;
- when $y^{NV} = 0$ , the sum in (11) starts at $t = 1$ ;
- all powers are real powers, with $0^p = 0$ for $p > 0$ ;
- "the manager does not know any upper bound" is not a hypothesis, because the algorithm uses none.
Trivializing formalizations are ruled out. The statements concern the algorithm's own iterates, not an arbitrary sequence of levels. The constants are the printed ones. The hypotheses are satisfiable, for example with $\hat y^\delta_1 = 0$ .
Useful contributions:
- convexity and Lipschitz continuity of $Q$ with constant $\max\{b,h\}$ ;
- the subgradient identity $E[H_t(y)] = (b+h)F(y^-) - b$ ;
- measurability and boundedness of the iterates;
- independence of $D_t$ from $\hat y^\delta_t$ under the product measure;
- the projected-step inequality.

Selected references

W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1), 2009. https://doi.org/10.1287/moor.1080.0355
M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
A. D. Flaxman, A. T. Kalai and H. B. McMahan, Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
G. A. Godfrey and W. B. Powell, An Adaptive, Distribution-Free Algorithm for the Newsvendor Problem with Censored Demands, Management Science 47(8), 2001. https://doi.org/10.1287/mnsc.47.8.1101.10231
A. N. Burnetas and C. E. Smith, Adaptive Ordering and Pricing for Perishable Products, Operations Research 48(3), 2000. https://doi.org/10.1287/opre.48.3.436.12437

7 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Smart "Predict, then Optimize": Under a Continuous, Centrally Symmetric Cost Law Every Minimizer of the SPO+ Risk Equals E[c|x] and Minimizes the SPO RiskResearch Paper

Motivation

Many decisions are made before their objective coefficients are known. A planner may know the feasible decisions and the form of a linear optimization problem, but must predict its cost vector from available features. Squared prediction error measures how close a forecast is to the eventual coefficients; it need not measure the quality of the decision chosen with that forecast. Elmachtoub and Grigas define a loss based on the excess realized cost of the resulting decision, then introduce a convex surrogate, SPO+, for training prediction rules Elmachtoub and Grigas, 2020, §§2–3.

The central population question is whether minimizing the surrogate still selects predictions that minimize the decision loss when the full data distribution is available. Their Theorem 1 answers this under conditions on the feasible region and the conditional distribution of costs Elmachtoub and Grigas, 2020, p. 21. The result concerns the loss itself, before sample size, model capacity, or an algorithm for fitting a predictor enter the picture.

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact, and convex. Given a cost vector $c\in\mathbb R^d$ , a decision $w\in S$ incurs cost $c^\top w$ . The nominal value, optimal-decision set, and support function are

z^*(c)=\min_{w\in S}c^\top w,\qquad W^*(c)=\arg\min_{w\in S}c^\top w,\qquad \xi_S(c)=\max_{w\in S}c^\top w.

An optimization oracle $w^*$ returns one element of $W^*(c)$ for each $c$ , without a tie-breaking rule. For a predicted cost $\hat c$ and realized cost $c$ , the unambiguous SPO loss uses the worst realized decision among all decisions optimal for the prediction:

\ell_{\mathrm{SPO}}(\hat c,c) =\max_{w\in W^*(\hat c)}c^\top w-z^*(c).

This is Definition 2 of the paper. Its SPO+ loss, Definition 3, is

\ell_{\mathrm{SPO+}}(\hat c,c) =\xi_S(c-2\hat c)+2\hat c^\top w^*(c)-z^*(c).

The factor $2$ is fixed by the paper's surrogate. Proposition 3 states that SPO+ upper-bounds SPO, is convex in $\hat c$ , and has the explicit subgradient $2(w^*(c)-w^*(2\hat c-c))$ Elmachtoub and Grigas, 2020, pp. 17–18.

Let $x$ denote an observed feature, $\nu$ its probability law, and $\kappa_x$ the conditional law of $c$ given $x$ . Their joint law is $D=\nu\otimes\kappa$ . A measurable predictor $f$ maps each $x$ to a cost prediction $f(x)$ . The population risks $R_{\mathrm{SPO}}(f)$ and $R_{\mathrm{SPO+}}(f)$ are expectations over $(x,c)\sim D$ of the corresponding losses at $(f(x),c)$ , as in displays (11) and (12) Elmachtoub and Grigas, 2020, p. 20. There is no prescribed parametric predictor class.

Formalization targets

Theorem 1: Fisher consistency of SPO+

Write $m(x)=\mathbb E[c\mid x]$ . Under Assumption 1, the optimal-decision set $W^*(m(x))$ is a singleton for almost every $x$ ; each conditional law is centrally symmetric about $m(x)$ and continuous on all of $\mathbb R^d$ ; and $S$ has nonempty interior. The goal says that every measurable minimizer $f$ of SPO+ population risk satisfies

f(x)=m(x)\quad\text{for }\nu\text{-almost every }x, \qquad R_{\mathrm{SPO}}(f)\le R_{\mathrm{SPO}}(g) \quad\text{for every measurable }g.

This is the paper's Fisher-consistency statement, including its stronger identification of every SPO+ minimizer with the conditional mean Elmachtoub and Grigas, 2020, Theorem 1. The goal does not assert that a minimizer exists.

Supporting propositions

The milestone list follows the paper's numbered results: Proposition 3's pointwise upper bound, convexity, and subgradient; Proposition 6's mean minimizer and uniqueness claims for a single cost law; and both directions of Proposition 5, which relate SPO risk minimizers to decisions optimal at the mean Elmachtoub and Grigas, 2020, pp. 18, 22–23. The single-law propositions have no feature variable.

Significance

Theorem 1 identifies a condition under which a convex training objective preserves the population target of the decision loss. Its identification statement is stronger than merely saying that one selected SPO+ minimizer is SPO-optimal: all SPO+ minimizers agree almost surely with conditional mean cost. The propositions isolate what this depends on. Proposition 6 concerns the surrogate risk, while Proposition 5 connects a prediction's optimal-decision set to the true risk.

The result was proved in the cited preprint and published in Management Science in 2022; this mission asks for a Lean proof of that known result, not a new consistency theorem. A completed development would provide reusable definitions for cost-based decision losses and a checked account of the distributional assumptions needed for uniqueness. The published oracle predicate is already available on the platform; the two losses, risks, and distributional predicates are introduced here.

Difficulty

The SPO loss may jump when a predicted cost admits more than one optimal decision. Its definition takes the maximum realized cost over that whole decision set. Consequently, showing that a prediction selects one mean-optimal decision does not by itself control the SPO loss; Proposition 5's converse requires a singleton set. The surrogate is convex but generally not differentiable, because the support function of $S$ need not be differentiable. Establishing the unique population minimizer also depends on how the cost law covers the space: absolute continuity by itself permits a bounded-support law for which nearby predictions tie. These are substantive issues in moving from the single-cost-law statements to an almost-sure claim about measurable predictors Elmachtoub and Grigas, 2020, §4 and Appendix B.

Formalization scope

The code represents $\mathbb R^d$ by EuclideanSpace ℝ (Fin d) and $c^\top w$ by its standard inner product. Every theorem assumes the paper's nonempty compact convex $S$ . Real infima and suprema encode the attained minima and maxima on $S$ . An oracle is an explicit parameter satisfying the published SPOBounds.Natarajan.IsOracle predicate; it is not given an extra measurability or tie-breaking assumption. The SPO loss is the paper's unambiguous Definition 2, which differs from the oracle-dependent loss in the published module.

Expected losses are extended nonnegative integrals, so an infinite risk remains infinite. Conditional costs are represented by a Markov kernel $\kappa$ , and the joint law by $\nu\otimes\kappa$ . Integrability of costs makes the conditional and joint means finite. Central symmetry means equality of the conditional law with its reflection $c\mapsto 2m(x)-c$ . Assumption 1.3, “continuous on all of $\mathbb R^d$ ,” is pinned to absolute continuity with respect to Lebesgue measure and full support, meaning every nonempty open set has positive probability. This full-support condition is needed for Proposition 6(b)'s uniqueness claim: a continuous law confined to a small ball supplies a counterexample to the weaker reading.

The risks range over all measurable predictors, as display (12) requires. A Bochner integral for an arbitrary nonintegrable loss, a restricted hypothesis class, the oracle-dependent SPO loss of Definition 1, or absolute continuity without full support would change or trivialize the target. Contributions to the support-function, measurable-risk, and conditional-law infrastructure are useful beyond this mission; the seven numbered proposition parts provide its immediate formalization targets.

Selected references

A. N. Elmachtoub and P. Grigas, Smart “Predict, then Optimize”, arXiv:1710.08005v5, 2020; published in Management Science 68(1), 2022. Preprint

10 thms3 active usersReviewed

Optimization Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 4: Log-Barrier-Regularized Softmax Policy Gradient Is ε-Optimal After 320|S|²|A|²D∞²/((1−γ)⁶ε²) StepsResearch Paper

Motivation

Policy gradient methods search directly over parameterized policies of a Markov decision process (MDP) by gradient ascent on the expected discounted reward. They are among the most widely used methods in reinforcement learning, yet the value $V^{\pi_\theta}(\rho)$ is a nonconcave function of the parameters, and until recently little was known about whether, or how fast, such methods reach a globally optimal policy. Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) give a systematic answer for tabular and function-approximation settings.

This mission formalizes one of their central results. Under the softmax parameterization, plain gradient ascent converges to optimal values only asymptotically (their Theorem 5.1, rate unknown): parameters can diverge and policies become nearly deterministic early, which stalls progress. Adding a log barrier regularizer, equivalent to a relative-entropy penalty towards the uniform policy, keeps action probabilities away from zero, and the paper shows that this yields an iteration count polynomial in every problem quantity. The result is the "softmax + log barrier" row of the paper's Table 1 and a reference point for later analyses of entropy-regularized policy gradient (for example Mei et al., 2020; Cen et al., 2021).

Setting

A finite MDP consists of finite sets $\mathcal S$ (states) and $\mathcal A$ (actions, nonempty), a transition kernel $P(s'\mid s,a)$ , rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$ . A policy $\pi$ assigns a probability distribution $\pi(\cdot\mid s)$ over actions to every state. Its value is $V^\pi(s)=\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid\pi,s_0=s]$ , and for a distribution $\rho$ over states $V^\pi(\rho)=\mathbb E_{s\sim\rho}V^\pi(s)$ . The action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and the advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$ . An optimal policy $\pi^\star$ maximizes $V^\pi(s)$ at every state simultaneously; $V^\star=V^{\pi^\star}$ .

The discounted state visitation distribution is $d^\pi_\rho(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\rho)$ . Given a start distribution $\mu$ used by the algorithm, the distribution mismatch coefficient is $\|d^{\pi^\star}_\rho/\mu\|_\infty=\max_s d^{\pi^\star}_\rho(s)/\mu(s)$ .

The softmax policy with parameter $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is $\pi_\theta(a\mid s)=\exp(\theta_{s,a})/\sum_{a'}\exp(\theta_{s,a'})$ . For $\lambda>0$ the log barrier regularized objective is

L_\lambda(\theta)=V^{\pi_\theta}(\mu)+\frac{\lambda}{|\mathcal S|\,|\mathcal A|}\sum_{s,a}\log\pi_\theta(a\mid s)+\lambda\log|\mathcal A| =V^{\pi_\theta}(\mu)-\lambda\,\mathbb E_{s\sim\mathrm{Unif}_{\mathcal S}}\mathrm{KL}(\mathrm{Unif}_{\mathcal A},\pi_\theta(\cdot\mid s)),

and gradient ascent with step size $\eta$ is $\theta^{(t+1)}=\theta^{(t)}+\eta\nabla_\theta L_\lambda(\theta^{(t)})$ . Write $V^{(t)}=V^{\pi_{\theta^{(t)}}}$ .

Formalization targets

Goal: Corollary 5.1 (iteration complexity)

Let $D\ge d^{\pi^\star}_\rho(s)/\mu(s)$ for all $s$ (for example the mismatch coefficient), $\epsilon>0$ , $\lambda=\epsilon(1-\gamma)/(2D)$ , $\beta_\lambda=8/(1-\gamma)^3+2\lambda/|\mathcal S|$ and $\eta=1/\beta_\lambda$ . Starting from a parameter whose softmax policy is uniform (e.g. $\theta^{(0)}=0$ ),

\min_{t<T}\big\{V^\star(\rho)-V^{(t)}(\rho)\big\}\le\epsilon\quad\text{whenever}\quad T\ge\frac{320\,|\mathcal S|^2|\mathcal A|^2}{(1-\gamma)^6\epsilon^2}\,D^2 .

Milestones

Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot|s)}A^{\pi'}(s,a)$ .
Lemma C.1 (softmax gradient): $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a|s)A^{\pi_\theta}(s,a)$ .
Display (14): the same plus $\frac{\lambda}{|\mathcal S|}(\frac1{|\mathcal A|}-\pi_\theta(a|s))$ for $\partial L_\lambda/\partial\theta_{s,a}$ .
Opening claim of the proof of Theorem 5.2: at an $\epsilon_{\rm opt}$ -stationary point with $\epsilon_{\rm opt}\le\lambda/(2|\mathcal S||\mathcal A|)$ , $\max_a A^{\pi_\theta}(s,a)\le 2\lambda/(\mu(s)|\mathcal S|)$ .
Theorem 5.2: under the same hypotheses, $V^{\pi_\theta}(\rho)\ge V^\star(\rho)-\frac{2\lambda}{1-\gamma}\|d^{\pi^\star}_\rho/\mu\|_\infty$ .
Lemma D.4: $L_\lambda$ has $\beta_\lambda$ -Lipschitz gradient, $\beta_\lambda=8/(1-\gamma)^3+2\lambda/|\mathcal S|$ .
Theorem E.1(3) (Beck, Theorem 10.15), unconstrained ascent form: for $\beta$ -smooth $f\le M$ and step $1/\beta$ , $\min_{t<T}\|\nabla f(x_t)\|\le\sqrt{2\beta(M-f(x_0))}/\sqrt T$ .

Significance

The corollary shows that a first-order method on a nonconcave objective reaches an $\epsilon$ -optimal policy in a number of steps polynomial in $|\mathcal S|$ , $|\mathcal A|$ , $1/(1-\gamma)$ , $1/\epsilon$ and the mismatch coefficient, with no dependence on the MDP's structure beyond these quantities. Theorem 5.2 is of independent use: it certifies any approximately stationary point of the regularized objective, however it was found, as approximately optimal for the original problem. The dependence on $\|d^{\pi^\star}_\rho/\mu\|_\infty$ makes precise why the exploratory start distribution $\mu$ matters.

The results are proved in the paper; none of them is machine-checked. A formal development adds a checked softmax policy gradient formula on an infinite-horizon discounted MDP, a checked smoothness bound for the regularized objective, the nonconvex gradient-method rate in Euclidean space, and a corrected statement of the corollary (see the next sections). Lemma 3.2 and Lemma C.1 are reused across the other missions of this series.

Difficulty

The value function is not concave in $\theta$ and its gradient vanishes where policies become deterministic, so the standard route "small gradient implies near-optimal" fails for the unregularized objective. With the regularizer, the link between stationarity and optimality has to hold with explicit constants that do not degrade as policies approach the boundary of the simplex, which is where the unregularized argument breaks down. The second obstacle is smoothness: $V^{\pi_\theta}(\mu)$ is an infinite discounted sum of products of transition probabilities, and its Hessian must be bounded uniformly in $\theta$ by $8/(1-\gamma)^3$ , which in Lean means differentiating a tsum of matrix-power–like terms in $\theta$ . The policy gradient formula itself requires the same interchange of differentiation and infinite summation.

Formalization scope

States and actions are finite types; $\mathcal A$ is nonempty. Parameters live in EuclideanSpace ℝ (S × A), so $\|\cdot\|$ is the $\ell_2$ norm and $\nabla_\theta$ is Mathlib's gradient. The MDP layer (transition kernel, policy, occupation probabilities, $V^\pi$ , $Q^\pi$ , optimal policy) is the published FoundationsML.ReinforcementLearning library, and $V^\pi(\rho)$ , $A^\pi$ , $d^\pi_\rho$ are defined on top of it. Standing assumptions are those of §3: $P$ a kernel, $r\in[0,1]$ , $0\le\gamma<1$ , $\mu,\rho$ probability distributions, $\pi^\star$ optimal at every state.

Conventions committed to:

the mismatch coefficient is replaced by any $D$ with $d^{\pi^\star}_\rho\le D\mu$ componentwise; no division by $\mu(s)$ occurs, and the same $D$ sets $\lambda$ ;
$\min_{t<T}$ is "there is $t<T$ with …";
$\lambda>0$ , implicit in the paper, is a hypothesis of Theorem 5.2 and its proof-step milestone; $\lambda\ge0$ in Lemma D.4;
Theorem E.1 is posed for ascent on $\mathbb R^d$ with an upper bound $M$ in place of an attained optimum.

Two corrections of the printed corollary. The printed statement allows "any initial $\theta^{(0)}$ ", but its proof uses $L_\lambda(\theta^\star)-L_\lambda(\theta^{(0)})\le1/(1-\gamma)$ , valid for a uniform initial policy and false in general; the formal goal assumes a uniform start. The printed $\beta_\lambda=8\gamma/(1-\gamma)^3+2\lambda/|\mathcal S|$ contradicts the proof, which takes $\beta_\lambda$ from Lemma D.4, $8/(1-\gamma)^3+2\lambda/|\mathcal S|$ ; the formal goal uses the latter, with the same iteration count.

The goal is not trivialized by its encoding: the hypotheses fix the run completely from $\theta^{(0)}$ , $\lambda$ and $\eta$ , they are jointly satisfiable (a sorry-free check exhibits a one-state, two-action MDP with an optimal policy and $D=1$ ), and the conclusion concerns the unregularized value of the iterates. Theorem 5.2, Lemma D.4 and Theorem E.1 are milestones, not hypotheses of the goal.

Infrastructure that a complete development needs, and that is reusable beyond this mission: differentiability of discounted values in the policy parameters and the policy gradient theorem for the softmax class; Hessian bounds for softmax; the descent lemma and the $O(1/\sqrt T)$ rate of gradient methods for smooth nonconvex functions on Euclidean space. Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261v5
S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
A. Beck, First-Order Methods in Optimization, SIAM, 2017. https://doi.org/10.1137/1.9781611974997
J. Mei, C. Xiao, C. Szepesvári, D. Schuurmans, On the Global Convergence Rates of Softmax Policy Gradient Methods, ICML 2020. https://arxiv.org/abs/2005.06392
S. Cen, C. Cheng, Y. Chen, Y. Wei, Y. Chi, Fast Global Convergence of Natural Policy Gradient Methods with Entropy Regularization, Operations Research 70(4), 2022. https://arxiv.org/abs/2007.06558

20 thms3 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

MNL-Bandit: A Dynamic Learning Approach to Assortment Selection II: Under a K-Cardinality Constraint Every Policy Has Regret at Least C√(NT/K)Research Paper

Motivation

A retailer with a large catalogue but a limited display (a web page, a shelf, a search result) must decide which assortment of products to show each arriving customer. Customers choose among the displayed products or leave without buying, and the retailer does not know their preferences in advance; it learns them only from the purchases it observes. This is the MNL-Bandit problem of Agrawal, Avadhanula, Goyal and Zeevi (arXiv:1706.03880v2; Operations Research 67(5), 2019), in which customer choices follow the multinomial logit model, the workhorse of revenue management and marketing.

The same paper gives an epoch-based upper-confidence-bound policy whose regret is at most of order $\sqrt{NT\log NT}$ (its Theorem 1). This mission formalizes the matching lower bound, the paper's Theorem 2: under a constraint that at most $K$ products be displayed, no policy can have regret smaller than order $\sqrt{NT/K}$ on every instance. Lower bounds of this kind are what certify that an algorithm is near-optimal rather than merely good.

Timeline. The square-root lower bound for $N$ -armed bandits goes back to Auer, Cesa-Bianchi, Freund and Schapire (2002), presented in the survey of Bubeck and Cesa-Bianchi (arXiv:1204.5721, 2012). Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013) minimized regret under MNL choice with explore-then-exploit policies, obtaining $O(N^2\log^2T)$ and $O(N\log T)$ bounds for instances whose best and second-best assortments are well separated. Agrawal et al. (2017–2019) proved the instance-independent $\Omega(\sqrt{NT/K})$ lower bound formalized here; Chen and Wang (2017) later obtained $\Omega(\sqrt{NT})$ when $K<N/4$ .

Setting

There are $n$ products. An instance consists of a no-purchase weight $v_0>0$ , attraction parameters $v_1,\dots,v_n$ with $0\le v_i\le v_0$ , and revenues $r_i\in[0,1]$ . At each period $t=1,\dots,T$ the seller offers an assortment $S_t\subseteq\{1,\dots,n\}$ and observes a choice $c_t\in S_t\cup\{0\}$ , where $0$ means no purchase. Under the multinomial logit (MNL) model,

p_i(S)=\frac{v_i}{v_0+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},

and choices are independent across periods given the offered sets. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i/(v_0+\sum_{j\in S}v_j)$ .

A policy chooses $S_t$ from the past assortments and choices, possibly at random. It satisfies the $K$ -cardinality constraint if $|S_t|\le K$ always. Its regret over $T$ periods is

\mathrm{Reg}_\pi(T,v)=\mathbb E_\pi\Big(\sum_{t=1}^{T}R(S^*,v)-R(S_t,v)\Big),

where $S^*$ maximizes $R(\cdot,v)$ over assortments of at most $K$ products.

A randomized instance is a probability distribution over instances with common known revenues and a common no-purchase weight; the regret against it is averaged over the hidden attraction parameters, the choices and the policy's randomization.

Formalization targets

Goal: Theorem 2 (p. 14)

There is an absolute constant $C>0$ such that for all $n\ge2$ , $1\le K\le n$ and $T\ge n$ there is a finitely supported randomized instance, chosen before the policy, such that every policy $\pi$ respecting the $K$ -cardinality constraint satisfies

\mathbb E_{v}\big[\mathrm{Reg}_\pi(T,v)\big]\ge C\sqrt{\frac{nT}{K}} .

The constant is not fixed; any positive value suffices.

Milestones

The paper proves Theorem 2 in two cases.

Lemma E.1 (p. 57): the Bernoulli divergence bound $\mathrm{kl}(\alpha,\alpha+\epsilon)\le 4\epsilon^2/\alpha$ in the direction used by Lemma E.2.
Lemma E.2 (p. 57): for a guessing algorithm on $N\ge12$ coins and $t\le N\alpha/(60\epsilon^2)$ , at least $N/3$ hiding places $j$ of the biased coin have $\mathcal P_j(a_t=j)\le 1/2$ .
Lemma 5.1 (p. 15): on the Bernoulli instance $I_{\mathrm{MAB}}$ with $\epsilon=\frac1{100}\sqrt{N\alpha/T}$ , every online algorithm has expected regret at least $\epsilon T/6$ .
Lemma E.4 (p. 60): one period of MNL feedback on the instance $\hat I_{\mathrm{MNL}}$ , where $\epsilon=\sqrt{1/(32T)}$ , has divergence at most $4\epsilon^2$ .
Lemma E.5 (p. 61): over $T$ periods the two choice laws of that instance have divergence at most $4T\epsilon^2$ .

Items 1–3 serve the case $K<n$ , which the paper reduces to a multi-armed bandit through the instance $I_{\mathrm{MNL}}$ of Definition 5.2 ( $NK$ products in $N$ groups of $K$ , one hidden group with larger attraction). Items 4–5 serve the case $K=n$ through the two-point instance $\hat I_{\mathrm{MNL}}$ of Definition E.1.

Significance

The theorem shows that the $\sqrt{T}$ growth of regret in assortment learning cannot be improved, and that the dependence on the number of products is polynomial: when the display size $K$ is fixed, the UCB policy of the same paper is optimal up to logarithmic factors (Remark 4). It separates what learning under the MNL model costs from what the combinatorics of the assortment adds, and the reduction it uses, simulating an assortment algorithm inside a bandit algorithm, is reusable for other choice-model bandits.

The result is proved in the paper, with its proof in Appendix E. To our knowledge neither the theorem nor its lemmas have been machine-checked. A formal proof has to repair several printed slips: Lemma 5.1's hypotheses do not exclude $\alpha$ close to $1$ , where the bound fails; the proof of Lemma E.2 uses a form of Pinsker's inequality with a wrong constant; Lemma E.1 states one direction of the divergence and computes the other; and the constants of the $K=N$ case do not match. The formal statements here carry the corrected hypotheses, each disclosed in its note.

Difficulty

The obvious argument fails at the reduction. The bandit lower bound is a statement about algorithms that pull one arm per round, while an assortment policy offers $K$ products at once and sees a choice among them. Transferring the bound requires simulating MNL feedback from Bernoulli coins (Algorithm 2 of the paper), whose loop has a random length, and then relating the regret of the simulated assortment algorithm over a random number of calls to the bandit regret over $T$ pulls. The paper does this in expectation, and the constants have to be tracked through the random horizon.

A second difficulty is that the lower bound must hold for every policy, including randomized ones, against a single randomized instance fixed in advance. Bounding the regret of each deterministic policy separately is not enough unless the instance does not depend on the policy, which the statement requires. The change-of-measure steps (Lemmas E.2 and E.5) need a chain rule for the divergence between laws of adaptively generated histories.

Formalization scope

Products, periods and arms are 0-based (Fin n); a choice is Option (Fin n) with none the no-purchase alternative. Histories have finite length $T$ , laws of histories are explicit products of policy weights and MNL (or Bernoulli) probabilities, and every expectation is a finite sum, so no measurability or integrability side conditions arise. The no-purchase weight $v_0$ is explicit (Definition 5.2 has $v_0=K$ ). $R(S^*,v)$ is a maximum over the finite, nonempty family $\{S:|S|\le K\}$ .

Policies are behavioural: at every history they give a probability vector over assortments, which by Kuhn's theorem covers the paper's admissible policies with external randomization. The randomized instance is a finite list of instances with nonnegative weights summing to one; every support point has the same revenues and no-purchase weight, which are known to the seller. The quantifiers are in the paper's order: the constant first, then $n,K,T$ , then the randomized instance, then every policy. A formalization with the policy quantified before the instance, with $C=0$ allowed, with varying known revenues across hidden support points, or with only deterministic policies, would be weaker and is ruled out.

Hypotheses added to the printed statements: $n\ge2$ and $K\ge1$ in Theorem 2 (the claim fails for $n=1$ and $K=0$ ); $0<\alpha$ , $0<\epsilon$ , $\alpha+\epsilon\le3/4$ in Lemma E.1; $0<\alpha$ , $0<\epsilon$ , $2\alpha+\epsilon\le1$ in Lemma E.2; $0<\alpha$ , $2\alpha+\epsilon\le1$ , $T\ge1$ in Lemma 5.1. Lemmas E.4 and E.5 use Definition E.1's $\epsilon=\sqrt{1/(32T)}$ , with $T\ge1$ and $n\ge2$ so the instance is defined. Lemma E.5 is stated, as in its proof, for deterministic policies.

The development reuses three published definitions: the MNL revenue ChoiceCDLP.MNL.mnlObjective, the Bernoulli divergence RegretBandits.Stochastic.klBern, and the discrete Kullback–Leibler divergence FoundationsRL.GeneralDM.klDivDiscrete (valued in $[0,\infty]$ ). Proved platform results useful to solvers include Pinsker's inequality (BanditAlgorithm.pinsker_inequality_total_variation), the Bernoulli bound $d(p,q)\le(q-p)^2/(p(2-p-q))$ (BanditAlgorithm.bernoulli_relative_entropy_le_sq_div_of_add_le_one) and a divergence decomposition for bandits. A chain rule for the divergence of finite adaptive histories, and a formal version of the simulation of Algorithm 2, would be reusable beyond this mission; both are welcome as supporting lemmas.

Selected references

S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880 — DOI https://doi.org/10.1287/opre.2018.1832
S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
X. Chen, Y. Wang, A Note on a Tight Lower Bound for MNL-Bandit Assortment Selection Models, arXiv:1709.06109, 2017. https://arxiv.org/abs/1709.06109

12 thms3 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 2: On Any Partition into Segments, WML Makes at Most Σ min(l_i, (log(n/(βγ)) + m_i log(1/β))/log(1/u)) MistakesResearch Paper

Motivation

Prediction with expert advice asks a master algorithm to combine the binary predictions of a pool of $n$ prediction algorithms, trial after trial, so that it makes few more mistakes than the best member of the pool, without any probabilistic assumption on the data. Littlestone and Warmuth's Weighted Majority Algorithm WM (Littlestone and Warmuth 1994) keeps a weight per member, predicts with the weighted vote, and multiplies the weights of the wrong members by a factor $\beta<1$ after each of its own mistakes. Its mistake bound is of order $\log n + m$ , where $m$ is the number of mistakes of the best member on the whole sequence.

That bound compares the master with a single fixed member. In many applications the member that predicts well changes over time: one algorithm is accurate for a while, then a second one, then a third. Against a shifting target of this kind, WM can do badly, because the weight of a member that was wrong for a long time has become so small that it takes many mistakes to recover it. Section 3 of the paper introduces the variant WML, which never decreases a weight that is already small relative to the total, and proves that it pays only a logarithmic cost per change of target. This was the first result of what is now called tracking the best expert; it was later refined by Herbster and Warmuth's Fixed-Share algorithm (Herbster and Warmuth 1998).

Timeline. 1989: a conference version of the paper appears at FOCS. 1994: the journal version, the source of this mission, gives Lemma 3.1 and Theorem 3.1 in their present form. 1998: Herbster and Warmuth's Tracking the Best Expert generalizes the shifting bound to other loss functions.

Setting

A run takes place over $T$ trials $t = 0, \dots, T-1$ . In trial $t$ each member $i \in \{1,\dots,n\}$ of the pool predicts $x_i^{(t)} \in \{0,1\}$ , the master predicts $\lambda^{(t)} \in \{0,1\}$ , and the label $\rho^{(t)} \in \{0,1\}$ is revealed. The predictions of the pool and the labels are arbitrary.

The master keeps weights $w_i^{(t)} > 0$ , the weights at the beginning of trial $t$ . Let $W^{(t)} = \sum_j w_j^{(t)}$ be the total weight and $q_b^{(t)}$ the total weight of the members predicting $b$ . WML has parameters $0 < \beta < 1$ and $0 \le \gamma < \tfrac12$ :

it predicts $0$ if $q_0^{(t)} > q_1^{(t)}$ , $1$ if $q_1^{(t)} > q_0^{(t)}$ , and either value on a tie;
if $\lambda^{(t)} \ne \rho^{(t)}$ , each member $i$ with $x_i^{(t)} \ne \rho^{(t)}$ and $w_i^{(t)} > \frac{\gamma}{n} W^{(t)}$ has its weight multiplied by $\beta$ ; all other weights stay;
if $\lambda^{(t)} = \rho^{(t)}$ , no weight changes.

With $\gamma = 0$ this is WM. Write $m$ for the number of mistakes of the master and

u = \frac{1+\beta}{2} + (1-\beta)\gamma ,

which lies in $[\tfrac12, 1)$ for the stated parameter ranges.

Formalization targets

Goal: Theorem 3.1 (p. 224)

Split the sequence into consecutive segments $\mathcal S_1, \dots, \mathcal S_k$ , with $l_i$ trials in $\mathcal S_i$ , and let $m_i$ be the smallest number of mistakes any single pool member makes on $\mathcal S_i$ . If $\gamma > 0$ and every initial weight is at least $\beta\gamma/n$ times the total initial weight, then

m \le \sum_{i=1}^{k} \min\left( l_i,\ \frac{\log\big(n/(\beta\gamma)\big) + m_i \log(1/\beta)}{\log(1/u)} \right).

The partition is arbitrary and unknown to the algorithm; the bound holds for all partitions simultaneously.

Milestone: Lemma 3.1 (pp. 223–224)

The single-segment case, $k = 1$ , together with the statement that the weight floor survives the run: if every initial weight is at least $\beta\gamma/n$ times the total, then

m \le \frac{\log\big(n/(\beta\gamma)\big) + m_0 \log(1/\beta)}{\log(1/u)},

and every final weight is at least $\beta\gamma/n$ times the total final weight.

Milestone: the contraction step (p. 224, proof of Lemma 3.1)

On every mistake trial, $W^{(t+1)} \le u\, W^{(t)}$ .

Significance

The result. Theorem 3.1 shows that an online algorithm with no knowledge of when or how often the best predictor changes can compete with the best sequence of predictors, at a price of $O(\log(n/(\beta\gamma)))$ mistakes per segment. The $\min$ with $l_i$ says that a segment never costs more than its length. The bound is the template for later tracking and adaptive-regret results in online learning and for algorithms whose weights are kept bounded away from zero.

Formalizing it. The result is proved in the paper; no machine-checked proof of a shifting-target bound exists on Prove2Me or, to our knowledge, in Mathlib. This mission produces a formal model of WML in which ties are arbitrary (a run is a relation, so the bounds cover every tie-breaking rule), the per-mistake contraction, the single-sequence bound with its preserved invariant, and the segment bound. The model of trials, majority votes and mistake counts is reusable for the other algorithms of the paper.

Difficulty

The standard argument for WM compares the decrease of the total weight with the final weight of the best member. For a shifting target this fails twice. First, the best member of a later segment may have been wrong during all earlier segments; under WM its weight has shrunk by $\beta$ per mistake, and the master has to make many mistakes before that member regains influence. Second, the floor that prevents this also prevents some wrong members from being penalized, so the total weight shrinks by less on each mistake than under WM. The statement has to control both effects at once, and the per-segment accounting has to restart from whatever weights the previous segments left behind. A natural first idea, applying the single-sequence bound to each part of an arbitrary (interleaved) partition, does not work: for interleaved subsequences the inequality is false, and the theorem is about consecutive segments.

Formalization scope

The pool is Fin n with $n > 0$ ; trials are Fin T; binary values are Bool; weights are real, w : ℕ → Fin n → ℝ, with w t the weights at the beginning of trial $t$ , w 0 the initial and w T the final weights. A run is the relation IsWMLRun β γ x ρ w lam; it fixes positive initial weights, the majority rule with arbitrary ties, and the update, whose threshold is strict and uses the total weight at the beginning of the trial. Logarithms are natural logarithms; the base cancels in every ratio. The minimum over the pool is an infimum in ℕ over Fin n. Segments are given by monotone boundaries b : Fin (k+1) → ℕ with b 0 = 0 and b (Fin.last k) = T; empty segments are allowed and contribute $0$ .

The paper allows $\gamma = 0$ for the algorithm, but then the bounds read $\log(n/0) = +\infty$ . In Lean, n / 0 = 0, so the bounds assume $\gamma > 0$ ; the contraction milestone holds for $0 \le \gamma < \tfrac12$ and is stated so. The hypothesis $\gamma < \tfrac12$ is kept as stated in the paper, not replaced by $u < 1$ . A trivializing formalization, such as fixing the tie-breaking rule, dropping the strict weight test, letting the floor hypothesis be unsatisfiable, or allowing interleaved subsequences (which makes the goal false), is ruled out: a run exists for every input from every positive initial weights, and equal initial weights satisfy the floor.

Contributions welcome: proofs of the three statements, and lemmas on restricting a WML run to a block of trials, which the goal needs and which apply to any segment-wise analysis.

Selected references

N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proc. 30th IEEE FOCS, 256–261, 1989. https://doi.org/10.1109/SFCS.1989.63487
M. Herbster, M. K. Warmuth, Tracking the Best Expert, Machine Learning 32, 151–178, 1998. https://doi.org/10.1023/A:1007424614876

4 thms3 active usersReviewed

Completed

Linear algebra Markov Chain Reinforcement Learning·Captain: mikedeng1

Learning to Predict by the Methods of Temporal Differences: Linear TD(0) Converges in Expected Value to the Ideal Predictions on Absorbing Markov ChainsResearch Paper

Motivation

Temporal-difference (TD) methods learn to predict an eventual outcome from the differences between successive predictions rather than from the difference between each prediction and the final outcome. Sutton's 1988 paper Learning to predict by the methods of temporal differences introduced the TD( $\lambda$ ) family and gave the first convergence proof for a TD method; before it, as the paper notes (p. 23), "no TD method has ever been proved stable or convergent to the correct predictions". TD learning is now the core of policy evaluation in reinforcement learning, and later analyses (Dayan 1992, Tsitsiklis and Van Roy 1997) start from the setting fixed here.

Timeline:

1960 — Widrow and Hoff introduce the LMS (Widrow–Hoff) rule; its predictions converge in expected value to the ideal predictions for small step sizes (Widrow and Stearns 1985).
1977 — Witten sketches a convergence proof for a TD-like procedure on discounted costs; many steps were left out, and Sutton (footnote 4) writes that it "now appears that the theorem he proposed is not true".
1988 — Sutton proves Theorem 2 (linear TD(0), expected-value convergence on absorbing chains) and Theorem 3 (convergence of batch linear TD(0) to the maximum-likelihood predictions).
1992–1997 — Dayan extends expected convergence to TD( $\lambda$ ); Tsitsiklis and Van Roy prove almost-sure convergence of linear TD( $\lambda$ ) under decreasing step sizes.

Setting

An absorbing Markov chain has a finite set $N$ of nonterminal states, a finite set $T$ of terminal states and transition probabilities $p_{ij}\ge0$ ( $i\in N$ , $j\in N\cup T$ ) with $\sum_{j\in N\cup T}p_{ij}=1$ . Let $Q$ be the $N\times N$ matrix $[Q]_{ij}=p_{ij}$ . "Absorbing" means that every sequence terminates with probability one; for a finite chain this is $Q^k\to0$ .

A sequence starts in a nonterminal state drawn from a distribution $\mu$ , follows the chain through nonterminal states $q_1,\dots,q_m$ until it enters a terminal state $q_{m+1}=j$ , and then produces a scalar outcome $z$ drawn from a distribution $\nu_j$ with finite mean $\bar z_j$ . Let $[h]_i=\sum_{j\in T}p_{ij}\bar z_j$ . The ideal prediction of state $i$ is the expected outcome from $i$ ,

E\{z\mid i\}=\Bigl[\sum_{k\ge0}Q^kh\Bigr]_i=\bigl[(I-Q)^{-1}h\bigr]_i .

The learner does not see states, only an observation vector $x_i\in\mathbb R^K$ for each $i\in N$ , and predicts linearly, $P_t=w^\top x_{q_t}$ . Linear TD(0) with weight updates after each sequence keeps $w$ fixed during a sequence and then sets, with $P_{m+1}=z$ ,

w\leftarrow w+\sum_{t=1}^m\alpha\,(P_{t+1}-P_t)\,x_{q_t}.

Sequences are experienced independently; $w_n$ is the weight vector after $n$ sequences. Let $d_i$ be the expected number of visits to $i$ in one sequence, $D=\operatorname{diag}(d)$ , and $X$ the matrix with columns $x_i$ .

Formalization targets

Goal: Theorem 2

For every absorbing chain, start distribution $\mu$ , outcome laws with finite means and linearly independent $\{x_i\}$ , with every $d_i>0$ , there is $\varepsilon>0$ such that for $0<\alpha<\varepsilon$ and every $w_0$ ,

\lim_{n\to\infty}E\{x_i^\top w_n\}=\bigl[(I-Q)^{-1}h\bigr]_i\qquad\forall i\in N .

The threshold $\varepsilon$ is existential, as in the paper; no explicit value is fixed.

Milestones on the goal's path

Theorem A.1 (Neumann series under $A^n\to0$ ); (5) the ideal predictions; (7) $d^\top=\mu^\top(I-Q)^{-1}$ ; the mean recursion $\bar w_{n+1}=\bar w_n+\alpha XD(h+QX^\top\bar w_n-X^\top\bar w_n)$ ; Theorem A.2 ( $A^\top A$ nonsingular); Theorem A.3 ( $A\succ0\iff A+A^\top\succ0$ ); the Lemma of p. 27; $D(I-Q)$ positive definite; the eigenvalues of $X^\top XD(I-Q)$ have positive real parts; and $(I-\alpha X^\top XD(I-Q))^n\to0$ for small $\alpha$ .

Further results

Theorem 3: under repeated presentations of a finite training set, batch linear TD(0) converges (deterministically) to the maximum-likelihood predictions $[(I-\hat Q)^{-1}\hat h]_i$ , with its two supporting steps ( $\hat Q^n\to0$ and $\hat d^\top=\hat\mu^\top(I-\hat Q)^{-1}$ ). Theorem 1: linear TD(1) and Widrow–Hoff produce the same per-sequence weight changes.

Significance

Theorem 2 shows that a bootstrapping method, which learns from its own earlier predictions, is not biased by them in the limit: in expectation it reaches the same predictions as supervised (Widrow–Hoff) learning. Theorem 3 says more: on a fixed data set, TD(0) converges to the predictions that would be exact if the maximum-likelihood model of the process were correct, which differs from the least-squares answer Widrow–Hoff converges to. Together they are the formal basis for preferring TD to Monte-Carlo targets in multi-step prediction.

The results are proved on paper, and not formalized in Lean. A formalization adds a precise model of the experience (i.i.d. sequences of an absorbing chain with terminal-dependent outcome laws), the integrability facts the paper leaves implicit, and a correct proof of the positive definiteness of $D(I-Q)$ , whose printed argument has a gap (see below). The matrix lemmas (Neumann series under $A^n\to0$ ; real-part positivity of eigenvalues of $GM$ for $G\succ0$ symmetric and $M$ positive definite in the non-symmetric sense; the step-size threshold) are reusable for other linear stochastic-approximation analyses.

Difficulty

The obvious argument writes $E\{w_{n+1}\}$ as a linear function of $E\{w_n\}$ and observes that the iteration matrix $I-\alpha X^\top XD(I-Q)$ is a contraction for small $\alpha$ . Two steps of this fail as printed. First, the paper proves that $D(I-Q)$ is positive definite through the Lemma of p. 27 with a weakened notion of diagonal dominance (weak in every row, strict in one), under which the Lemma is false; with the standard notion, $D(I-Q)+(D(I-Q))^\top$ is in general not strictly diagonally dominant (a row with $\mu_i=0$ that cannot leave $N$ in one step has row sum $0$ ). A correct proof combines weak dominance with reachability of every state from the support of $\mu$ , which is where $d_i>0$ enters. Second, $X^\top XD(I-Q)$ is not symmetric, so a small $\alpha$ does not make $I-\alpha X^\top XD(I-Q)$ a contraction in the Euclidean norm; the argument goes through its eigenvalues, and turning eigenvalues of modulus below one into $(I-\alpha X^\top XD(I-Q))^n\to0$ is a spectral-radius argument. The probabilistic step is also not free: $w_n$ is a polynomial in $n$ random sequences of unbounded length, and its integrability and the factorization $E\{\eta_{ij}w_n\}=d_ip_{ij}E\{w_n\}$ need independence across sequences.

Formalization scope

States are finite types N (nonempty) and T; the chain is the structure AbsorbingChain with blocks pN, pT and the field $Q^k\to0$ . Observation vectors are x : N → Fin K → ℝ with LinearIndependent ℝ x; $X$ is Matrix (Fin K) N ℝ. A sequence is an Episode (list of nonterminal states, terminal state, outcome); IsEpisodeStream states measurability, mutual independence (iIndepFun) and the law $P(\text{path}=s,\text{term}=j,\text{out}\in B)=\mu_{s_1}p_{s_1s_2}\cdots p_{s_mj}\,\nu_j(B)$ . Expectations are Bochner integrals, and the goal asserts integrability of $x_i^\top w_n$ , so a non-integrable junk value $0$ cannot satisfy it. $d_i$ is defined as an expectation (a sum over sequences), not as $[\mu^\top(I-Q)^{-1}]_i$ , so (7) is not circular. "Positive definite" is the paper's footnote 6 ( $y^\top Ay>0$ for real $y\ne0$ , no symmetry), not Mathlib's Matrix.PosDef.

Trivializations ruled out: the hypothesis $d_i>0$ is the paper's own discarding of never-visited states (without it the goal is false: an unvisited state's weight never moves); N is nonempty and $\mu$ sums to one, so the hypotheses are satisfiable and the goal is not vacuous; the sequences cannot be arbitrary random variables or a fixed sequence, since their law is pinned to $\mu$ , $p$ and $\nu$ ; $\varepsilon$ is chosen before $\alpha$ , $w_0$ and the probability space; and the update is per sequence, not the intra-sequence variant of §5.

Corrected slips: "For each nonterminal state $j$ " (p. 24) means terminal; the diagonal-dominance definition of p. 27 is replaced by the standard one; $I-\alpha XD(I-Q)X^\top$ (p. 28) means $I-\alpha X^\top XD(I-Q)$ . Not formalized: the variance and TD( $\lambda$ ) conjectures of p. 29, §4.3, and the extension claims of §5.

Related open goals on this platform (different models, credited, not re-posed): SuttonBartoRL.BatchTD.batch_td_converges_to_certainty_equivalence (tabular, discounted analogue of Theorem 3), and SuttonBartoRL.LinearTD.keyMatrix_posDef, posDef_of_row_col_sums, expected_td_update (continuing discounted chain with stationary $D$ , where every row sum of $D(I-\gamma P)$ is positive). Contributions of any milestone, of general matrix lemmas, and of reusable infrastructure for i.i.d. episode streams are welcome.

Selected references

R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3(1), 9–44, 1988. https://doi.org/10.1023/A:1022633531479
B. Widrow and M. E. Hoff, Adaptive switching circuits, IRE WESCON Convention Record, 96–104, 1960.
B. Widrow and S. D. Stearns, Adaptive Signal Processing, Prentice-Hall, 1985.
J. G. Kemeny and J. L. Snell, Finite Markov Chains, Springer, 1976. https://link.springer.com/book/9780387901923
R. S. Varga, Matrix Iterative Analysis, Prentice-Hall, 1962 (2nd ed., Springer, 2000: https://doi.org/10.1007/978-3-642-05156-2).
P. Dayan, The convergence of TD(λ) for general λ, Machine Learning 8, 341–362, 1992. https://doi.org/10.1007/BF00992701
J. N. Tsitsiklis and B. Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 674–690, 1997. https://doi.org/10.1109/9.580874

24 thms3 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

MNL-Bandit: A Dynamic Learning Approach to Assortment Selection I: The Epoch-Based UCB Policy Has Regret at Most C₁√(NT log NT) + C₂N log² NT Under the No-Purchase AssumptionResearch Paper

Motivation

A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).

The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order $\sqrt{NT}$ up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$ . At each time $t=1,\dots,T$ the seller offers an assortment $S_t$ from a family $\mathcal S$ of feasible subsets of $\{1,\dots,N\}$ , and one customer either buys a product $c_t\in S_t$ or buys nothing ( $c_t=0$ ). Given $S_t=S$ , the choice follows the MNL model with attraction parameters $v_1,\dots,v_N\ge0$ and $v_0=1$ :

p_i(S)=\frac{v_i}{1+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},

independently of the past. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i\big/\big(1+\sum_{j\in S}v_j\big)$ . The family $\mathcal S$ is described by totally unimodular constraints, $\mathcal S=\{S : A\,x(S)\le b\}$ with $x(S)$ the incidence vector of $S$ , $A$ totally unimodular and $b$ integral (cardinality constraints are the main example). A policy chooses $S_t$ from the past choices, and its regret is

\mathrm{Reg}_\pi(T,v)=T\,R(S^*,v)-\mathbb E_\pi\Big[\sum_{t=1}^TR(S_t,v)\Big],\qquad R(S^*,v)=\max_{S\in\mathcal S}R(S,v).

The seller knows $r$ and $\mathcal S$ but not $v$ .

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ repeatedly until a customer buys nothing. Let $\hat v_{i,\ell}$ be the number of purchases of $i$ in epoch $\ell$ , $T_i(\ell)$ the number of the first $\ell$ epochs that offered $i$ , and $\bar v_{i,\ell}$ the average of $\hat v_{i,\tau}$ over those epochs. The algorithm forms the upper confidence bounds

v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)}}+\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)},

starting from $v^{\mathrm{UCB}}_{i,0}=1$ , and offers next the assortment in $\mathcal S$ that maximizes $R(S,v^{\mathrm{UCB}}_{\cdot,\ell})$ .

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumption 4.1 (every $v_i\le v_0=1$ , and $\mathcal S$ is closed under taking subsets) there are absolute constants $C_1,C_2$ such that for every instance and every horizon $T$ ,

\mathrm{Reg}_\pi(T,v)\le C_1\sqrt{NT\log NT}+C_2N\log^2NT .

The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.

Milestones

The milestones follow the proof in Appendix A of the paper:

The law of an epoch's purchase count: Lemma A.1, its moment generating function given the offered assortment.
Concentration: Theorem 5, Chernoff bounds for geometric variables; Corollary D.1; and Lemma A.2 for the averages $\bar v_{i,\ell}$ along Algorithm 1.
Lemma 4.1: $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability at least $1-6/(N\ell)$ , and its rate of convergence.
Optimism of the revenue estimate: Lemma A.3 (monotonicity of the optimal revenue in $v$ ) and Lemma 4.2.
The per-epoch error: Lemma A.4 (a Lipschitz bound) and Lemma 4.3.
The epoch decomposition of the regret, (A.14).

Significance

Theorem 1 shows that learning the choice model costs only $\tilde O(\sqrt{NT})$ revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order $\sqrt{NT/K}$ under a $K$ -cardinality constraint (its Theorem 2), so for small $K$ the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each $v_i$ .

The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.

Difficulty

The estimates $\hat v_{i,\ell}$ are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean $v_i$ has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples $T_i(\ell)$ is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length $1+\sum_{j\in S_\ell}v_j$ under a random number of epochs and a horizon that cuts the last one.

Formalization scope

Model. Products are Fin N; a choice is none (no purchase) or some i. The parameter $v_0$ is normalized to $1$ , as the paper allows. Algorithm 1 is deterministic, so a history of horizon $T$ is a sequence of $T$ choices with the product law $\prod_tp_{c_t}(S_t)$ , and every expectation is a finite sum. The revenue $R(S,v)$ is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.
Feasible family. $\mathcal S$ is a finite family with the TU representation (2.3), closed under subsets, and nonempty (the paper presupposes nonemptiness when it writes $S^*=\arg\max$ ).
Algorithm. Algorithm 1 is a policy defined by recursion on the history. It receives $r$ and an argmax selector for $\mathcal S$ , never $v$ . Every statement quantifies over all selectors, that is, over every tie-breaking rule. While a product has never been offered, its $v^{\mathrm{UCB}}$ stays at the initial value $1$ .
Epoch events. The lemmas about epoch $\ell$ are stated for every finite horizon $T$ , on the event that epoch $\ell$ is completed by customer $T$ ; uniformity in $T$ is the paper's infinite-horizon statement.
Repairs of the page, all disclosed in the items:
1. Lemma A.2's misprinted $\log(\ell+1)$ is replaced by $\log(\sqrt N\ell+1)$ .
2. Lemmas 4.2 and 4.3 are indexed by the estimate built at the end of epoch $\ell$ .
3. Lemma 4.3's free index $i$ becomes the sum over $i\in S_{\ell+1}$ .
4. Lemmas 4.1 and 4.3 use the explicit constants $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ of the proof.
5. Lemma A.3 and Lemma 4.2 require positive parameters on the optimal set; the printed versions are false otherwise.
6. (A.14) is an inequality, since the horizon cuts the last epoch.
Not stated. Corollary A.1 (the epoch estimates are i.i.d. geometric across the epochs of the adaptive policy) is not posed as an item: a single-epoch law would be a weaker statement than the page's.
No trivialization. The policy cannot see $v$ , the constants of the goal precede every other quantifier, and the regret is the paper's (2.6), so the goal cannot be met by a policy that offers $S^*$ or by constants that depend on the instance.
Welcome contributions. Infrastructure for adaptive sampling (the i.i.d. property of the epoch estimates), Chernoff bounds for geometric and sub-exponential variables, and a Wald-type identity for epochs.

The paper's own proofs are in its Appendices A and D.

Selected references

S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019. arXiv:1706.03880v2, doi:10.1287/opre.2018.1832
P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6):1666–1680, 2010. doi:10.1287/opre.1100.0866
D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3):387–404, 2013. doi:10.1287/msom.2013.0429
K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. doi:10.1287/mnsc.1030.0147
M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005.

15 thms3 active usersReviewed

Completed

Optimization Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 6: Agnostic Q-NPG for Log-Linear Policies, Bounded by Transfer Error, Excess Risk and Condition NumberResearch Paper

Motivation

Policy gradient methods optimize a decision rule by changing the parameters that determine its action probabilities. In reinforcement learning, the objective is the expected total reward collected over time. Once a policy is restricted to a feature-based class, the best policy may be less effective than the unrestricted optimum. A useful guarantee must therefore compare the computed policy with a chosen comparator and account for both the limits of the features and the error in estimating an update direction. Agarwal, Kakade, Lee and Mahajan give such a guarantee for a version of the natural policy gradient method that fits action values with linear features, called Q-NPG (Agarwal et al., §6.2).

The result matters when a policy has far fewer parameters than there are state-action pairs. A bound phrased only for exact action values or an unrestricted policy class would leave out the errors introduced by fitting from samples and by moving the fitting distribution from the states of a comparator to the states visited by the current policy. Theorem 6.1 keeps those effects visible as separate terms. It also avoids assuming that the comparator is an optimal policy; the comparator can be a policy selected for an application or a benchmark within a restricted class.

Setting

A discounted Markov decision process has a finite state set S, a finite nonempty action set A, transition probabilities P(s'|s,a), immediate rewards r(s,a) in [0,1], and a discount factor γ in [0,1). A policy π assigns a probability distribution over A to every state. The value V^π(s) is the expected sum of discounted rewards from s, and V^π(ρ) averages this value over an initial state distribution ρ. The action value Q^π(s,a) starts by choosing a in s and then follows π. Its advantage is A^π(s,a)=Q^π(s,a)−V^π(s). These are the unnormalized value conventions of §3, pp. 9–12.

For each state-action pair, fix a feature vector φ(s,a) in Euclidean d-space. The log-linear policy with parameter θ assigns probability proportional to exp(θ·φ(s,a)):

\pi_\theta(a\mid s)= \frac{\exp(\theta\cdot\phi(s,a))} {\sum_{a'\in A}\exp(\theta\cdot\phi(s,a'))}.

The Q-NPG fitting loss $L(w;\theta,\upsilon)$ is the mean squared error of predicting $Q^{\pi_\theta}(s,a)$ by $w\cdot\phi(s,a)$ under a state-action distribution $\upsilon$ . Q-NPG uses an approximate minimizer w of this loss under its current on-policy measure and updates θ by ηw. The distribution ν specifies the initial state-action pair for that measure. At time zero, the pair is drawn directly from ν; the given initial action is executed before later actions follow the current policy. These definitions are (19)–(20) of §6.2, pp. 27–28.

The comparison policy π⋆ has discounted state visitation distribution $d^{\pi^\star}_\rho$ . The paper's transfer measure $d^\star$ pairs those states with a uniform action from A. The excess risk measures how much worse an approximate fitting direction is than an exact constrained minimizer under the current on-policy measure. The transfer error measures the exact minimizer's loss under $d^\star$ . A relative condition number κ bounds, in every feature direction, the covariance quadratic form under $d^\star$ by κ times that under ν (Assumptions 6.1–6.2, pp. 28–29).

Formalization targets

Agnostic Q-NPG guarantee

The goal is Theorem 6.1, p. 29. Starting with θ⁽⁰⁾=0, taking T positive updates with step size $\eta=\sqrt{2\log|A|/(B^2W^2T)}$ , bounding feature norms by B and update norms by W, and assuming the expected excess and transfer errors are at most $\varepsilon_{\rm stat}$ and $\varepsilon_{\rm bias}$ , respectively, it asserts

\mathbb E\!\left[ \min_{t<T}\{V^{\pi^\star}(\rho)-V^{\pi_{\theta^{(t)}}}(\rho)\} \right] \le \frac{BW}{1-\gamma}\sqrt{\frac{2\log|A|}{T}} + \sqrt{\frac{4|A|\kappa\varepsilon_{\rm stat}}{(1-\gamma)^3}} + \frac{\sqrt{4|A|\varepsilon_{\rm bias}}}{1-\gamma}.

The expectation encloses the minimum: each random run may have a different best iterate. The claim gives a finite-horizon comparison with π⋆ even when π⋆ is not globally optimal.

Supporting targets

The milestones are the paper's performance-difference identity (Lemma 3.2), smoothness of bounded-feature log-linear policies (Remark 6.7), the deterministic NPG regret lemma (Lemma 6.2), and the two displayed bounds that control transfer and estimation terms ((25) and (26)). Together they connect the MDP's value comparison with the two statistical errors in the goal. Each milestone states a source result rather than a weakened surrogate.

Significance

The theorem separates three quantities that can vary independently in an application: the number of iterations, the statistical quality of the update direction, and the mismatch between the comparator's visited states and the fitting distribution. If both errors vanish, the displayed bound decreases with T at a square-root rate. With imperfect features, the transfer term shows the remaining performance limit. With finite-sample fitting, the excess-risk term shows how estimation quality affects the policy value. This is an agnostic statement because the comparator need not belong to a globally complete policy class (Agarwal et al., Theorem 6.1 and discussion, pp. 29–30).

The paper proves these claims mathematically. This mission asks for machine-checked proofs of the same statements in Lean, including the probabilistic expectation and the exact constants. The reusable parts are the state-action visitation distribution with a prescribed initial action, the log-linear policy and its smoothness property, the least-squares loss, and the deterministic regret lemma. Those objects can support other policy-gradient analyses with different fitting guarantees.

Difficulty

The update direction minimizes a loss under the distribution generated by the current policy, while the value comparison uses states visited by a different policy. The two distributions need not agree, and prediction error under one cannot simply be substituted for error under the other. The relative condition number controls the feature geometry of this shift, while the transfer error separately measures how well an exact on-policy fit predicts under the comparator's measure. Random approximate minimizers add a further layer: the bound concerns the expectation of the best iterate in each run, rather than a deterministic iterate chosen in advance. These are the obstacles identified around Assumptions 6.1–6.2 and the proof of Theorem 6.1.

Formalization scope

The Lean development uses finite state and action types, as in the paper's §3 standing setting. It imports published definitions of transition kernels, policies, occupation probabilities, value and Q-functions, and defines this paper's advantage, discounted visitation, log-linear class and fitting loss on top of them. Parameters and features lie in EuclideanSpace ℝ (Fin d), so the norm is the Euclidean norm used by the paper. A general probability space carries the random update directions and exact constrained minimizers; their measurability and boundedness make the displayed loss expectations integrable.

The action type is nonempty so that the uniform action distribution exists. B and W are positive and T is positive, because the prescribed step size divides by $B^2W^2T$ and the result minimizes over $t<T$ . The comparator is assumed to be a policy, with no optimality hypothesis. The nonnegative condition number is represented by its quadratic-form upper-bound property for every direction. This avoids undefined real ratios when a covariance form vanishes and includes the finite coefficient in Assumption 6.2. The value and loss expressions are calculated from P, r, π and φ; they are not free variables. The Q-NPG parameter sequence is defined by the update rule from θ⁽⁰⁾=0. In particular, the goal does not assume the regret lemma or either of the two statistical inequalities that the proof must establish.

The paper notes that some §6 results extend beyond finite state or action spaces. This mission fixes the finite case inherited from §3. Contributions that prove the source milestones, establish the required summability and integrability facts, or generalize the development to larger measurable spaces are useful; a generalization must keep the same statistical and comparator conventions.

Selected references

Alekh Agarwal, Sham M. Kakade, Jason D. Lee and Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5
Sham M. Kakade and John Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning, 2002. PDF

16 thms3 active usersReviewed

Completed

Optimization Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 2: On a Chain MDP All Low-Order Derivatives of the Value Are Exponentially Small at Suboptimal PoliciesResearch Paper

Motivation

Policy gradient methods adjust a policy by following derivatives of its expected reward. A common expectation is that a small gradient indicates a policy close to optimal. For discounted Markov decision processes, that interpretation can fail when a policy rarely reaches the states where reward is available. Agarwal, Kakade, Lee, and Mahajan study this obstruction as part of their analysis of optimality and distribution shift in policy gradient methods. Their chain example makes the obstruction quantitative: even derivatives of several orders can be exponentially small while the value gap grows with the chain length. Agarwal et al., §4.3 and Proposition 4.1.

The example isolates a specific issue for local optimization. A parameter change at an early state affects reward only after the agent has passed through many intermediate decisions. A local derivative therefore measures the behavior of a policy under its own visitation pattern, which can be very different from the visitation pattern of an optimal policy. This mission states the resulting separation with explicit constants rather than treating “vanishing gradients” as a qualitative description.

Setting

A discounted Markov decision process has a finite set of states, a finite set of actions, a transition probability for each state and action, a reward in $[0,1]$ , and a discount $0\le\gamma<1$ . The value $V^\pi(s)$ of a policy $\pi$ is the expected sum of discounted rewards when the process starts in state $s$ and follows $\pi$ . An optimal policy $\pi^\star$ has value at least as large as every other policy at every state. These conventions are those of §3 of the paper and its unnormalized infinite-horizon value definition. Agarwal et al., §3, pp. 9–12.

The central model is a deterministic chain with states $s_0,s_1,\ldots,s_{H+1}$ and four actions. At $s_0$ the process moves to $s_1$ . At each interior state $s_i$ , action $a_1$ moves forward to $s_{i+1}$ , while $a_2,a_3,a_4$ move backward to $s_{i-1}$ . State $s_{H+1}$ is absorbing. The only positive reward is $r(s_{H+1},a_1)=1$ , and $\gamma=H/(H+1)$ . This is Figure 2 and the transition matrix in equation (27). Agarwal et al., Figure 2, p. 11, and (27), p. 50.

The direct policy parameter $\theta$ has three free coordinates at each interior state: the probabilities assigned to $a_1,a_2,a_3$ . The probability of $a_4$ is their complement. Write $\pi_\theta$ for this policy expression and $F_H(\theta)=V^{\pi_\theta}(s_0)$ for its value from the starting state. The paper studies parameters whose free coordinates lie strictly between zero and one and whose forward-action coordinates satisfy $\theta_{i,a_1}<1/4$ .

Formalization targets

The goal is Proposition 4.1. For $H\ge1$ , every such $\theta$ , and every nonnegative integer $k$ satisfying $k\le H/(40\log(2H))-1$ , it asserts the multilinear operator-norm bound

\|\nabla^k F_H(\theta)\|_{\mathrm{op}}\le (1/3)^{H/4}.

The same statement compares this policy with an optimal policy:

V^{\pi^\star}(s_0)-F_H(\theta) \ge \frac{H+1}{8}-\frac{(H+1)^2}{3^H}.

Both clauses and their constants are part of the target. The derivative order includes $k=0$ whenever the displayed threshold admits it. Agarwal et al., Proposition 4.1, p. 16.

Three supporting targets follow the appendix's attack path. First, $F_H(\theta)$ equals the $(0,H+1)$ entry of the resolvent $M^p=(I-\gamma P^p)^{-1}$ , where $p_i=\theta_{i,a_1}$ . Second, equation (32) gives the derivative of any entry of $M^p$ in one forward probability. Third, the appendix separately bounds the optimal value below by $(H+1)/8$ and $F_H(\theta)$ above by $(H+1)^2/3^H$ . A companion theorem records Lemma 3.1: a five-state deterministic example has a value function that is nonconcave in both the direct and softmax parameterizations. Agarwal et al., Appendix B.2, pp. 51, 54, 59; Lemma 3.1, p. 11.

Significance

The proposition supplies an explicit family in which local derivative information, even at orders growing with $H/\log H$ , is small at policies with a large value gap. It limits what a guarantee based only on finding a point with small low-order derivatives can imply about global policy quality. The paper uses this example to motivate attention to state visitation and distribution mismatch in its positive results. Agarwal et al., §4.3, pp. 16–17.

The mathematical result is proved in the cited paper. The remaining work is a machine-checked development of the chain model, its value and resolvent identities, the higher derivative estimates, and the value-gap inequality. The reusable parts include finite-state discounted value calculations, differentiation of a matrix inverse, and operator-norm estimates for multilinear derivatives. The statements in this proposal are proof targets; they do not themselves claim that those proofs have been formalized.

Difficulty

A policy can have a small gradient simply because it almost never reaches the rewarding state. The obvious inference from a near-zero gradient to near-optimal value therefore fails in this model. The technical difficulty is quantitative: each differentiation of a resolvent entry produces terms involving several entries, and the operator norm combines all mixed partial derivatives. The bound must remain exponentially small after that combination, uniformly over every derivative order allowed by the threshold. The second clause must simultaneously show that a policy taking the forward action reaches the reward often enough to create a large value gap. Agarwal et al., Appendix B.2, pp. 54–59.

Formalization scope

States are Fin (H + 2) and actions are Fin 4; the parameter space is EuclideanSpace ℝ (Fin H × Fin 3). Its norm is the Euclidean norm, so the norm of the iterated Fréchet derivative is the paper's multilinear operator norm. The first and last states have no free policy parameters. All four actions at $s_0$ induce the same transition to $s_1$ , and the parameterized policy chooses $a_1$ at both boundary states. The resolvent is the matrix inverse of $I-\gamma P^p$ ; its milestone statements are restricted to interior probabilities $0<p_i<1$ , where that inverse is nonsingular.

The displayed coordinate assumptions of Proposition 4.1 do not require the three free probabilities at a state to sum to at most one. The Lean goal retains exactly those assumptions. Its value expression is still determined by the forward probabilities, because every other action has the same backward transition and only the absorbing state yields reward. This prevents an added simplex constraint from silently narrowing the proposition. A constant function or a free value variable cannot replace the chain value: $F_H$ is computed from the concrete transition and reward arrays.

The development uses the published finite-state transition-kernel, policy, occupation, value, and optimal-policy definitions. Contributions needed for a proof include stochasticity of the chain, geometric-series evaluation of its absorbing reward, nonsingularity and differentiation of its resolvent, and estimates that pass from mixed partial derivatives to the Euclidean operator norm. For the companion example, direct parameters lie in the product of action simplices, with positive discount; at zero discount its value is constant and the nonconcavity claim would be false.

Selected references

Alekh Agarwal, Sham M. Kakade, Jason D. Lee, Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5.

12 thms3 active usersReviewed

Completed

Linear algebra Optimization·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers VII: Factor Model Fitting — the ADMM X-Update in Closed Form, Entry by EntryTextbook

Motivation

Alternating direction methods are used when one part of an optimization problem is easy to minimize and another part has a simple projection. Chapter 9 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) examines this idea with nonconvex constraints. Its examples include sparse vectors, Boolean vectors and low-rank matrices. The chapter says explicitly that ADMM can fail to converge in this setting and that a limit need not be globally optimal. The useful claim here is narrower and concrete: several individual updates can still be computed exactly.

The capstone is factor-model fitting. A symmetric data matrix, such as an empirical covariance matrix, is approximated by a positive semidefinite matrix of prescribed rank plus a nonnegative diagonal matrix. This decomposition gives one component that captures shared variation and another that represents coordinate-specific variation. The chapter separates the diagonal fit from the rank constraint and writes the resulting ADMM X-update entry by entry. This mission formalizes that exact update and two other projection rules stated in the same chapter.

Setting

Fix a positive integer $n$ . Write $\mathbb S^n$ for the real symmetric $n\times n$ matrices, and let $\Sigma\in\mathbb S^n$ be the matrix to approximate. The Frobenius norm squares and sums every ordered matrix entry: $\|X\|_F^2=\sum_{i,j}X_{ij}^2$ . A vector $d\in\mathbb R^n$ is nonnegative when $d_i\ge0$ for every $i$ , and $\operatorname{diag}(d)$ places those entries on a diagonal matrix. The book's reduced fitting loss is

f_\Sigma(X)=\inf_{d\ge0}\frac12\|X+\operatorname{diag}(d)-\Sigma\|_F^2.

In the scaled ADMM iteration, $Z$ carries the positive semidefinite rank constraint and $U$ is the scaled dual matrix. Given the current symmetric matrices $Z,U$ and a penalty $\rho>0$ , the X-step minimizes $f_\Sigma(X)+(\rho/2)\|X-Z+U\|_F^2$ over $X\in\mathbb S^n$ . The X-step itself has no rank or positive semidefinite restriction. The following Z-step projects onto the chosen rank-constrained positive semidefinite set. The theorem here concerns the X-step, whose definition is independent of the chosen rank.

The other two results concern Euclidean projection of vectors $v\in\mathbb R^n$ . The cardinality $\operatorname{card}(x)$ is the number of nonzero coordinates of $x$ . The sparse set is $\{x:\operatorname{card}(x)\le c\}$ for a nonnegative integer $c$ . The Boolean cube is $\{0,1\}^n$ . Projection means a nearest point in squared Euclidean distance; it may have more than one value when coordinates tie.

Formalization targets

Partial minimization of the diagonal

The first milestone identifies the book's infimum as the explicit componentwise loss and states that the optimizing diagonal is attained:

f_\Sigma(X)=\frac12\sum_{i\ne j}(X_{ij}-\Sigma_{ij})^2+ \frac12\sum_i(X_{ii}-\Sigma_{ii})_+^2, \qquad d_i=(\Sigma_{ii}-X_{ii})_+.

The sum over $i\ne j$ counts both $(i,j)$ and $(j,i)$ . The statement preserves that convention instead of treating a symmetric matrix as a list of independent upper-triangular entries.

Exact projections for two nonconvex sets

The page 74 milestones say that retaining the $\min(c,n)$ entries of largest absolute value gives a nearest point in $\{x:\operatorname{card}(x)\le c\}$ , and that rounding every coordinate to a nearest element of $\{0,1\}$ gives a nearest Boolean vector. They assert nearest-point status for ties without asserting uniqueness. These are chapter results on the same theme of exact nonconvex updates, although they are independent of the factor-model goal.

Factor-model X-update

The goal identifies the unique symmetric minimizer $X^+$ of the X-subproblem. With $a_{ij}=Z_{ij}-U_{ij}$ , its off-diagonal and diagonal entries are

X^+_{ij}=\frac{\Sigma_{ij}+\rho a_{ij}}{1+\rho}\quad(i\ne j),\qquad X^+_{ii}=\begin{cases} \dfrac{\Sigma_{ii}+\rho a_{ii}}{1+\rho},&\Sigma_{ii}\le a_{ii},\\ a_{ii},&\Sigma_{ii}>a_{ii}. \end{cases}

The target asserts both the formula and global minimality over symmetric matrices. It does not replace minimality with a stationarity condition.

Significance

The exact X-update separates the matrix fit from the nonconvex rank projection. It establishes that the factor-model algorithm's X-step is a well-defined, single-valued minimization for every symmetric current state and every positive penalty. It also makes the one-sided diagonal loss explicit: a nonnegative diagonal can absorb a shortfall below $\Sigma_{ii}$ , but cannot absorb an excess. The two vector projections give similarly exact updates for sparse and Boolean constraint sets.

The mathematical claims are given in §9.1–9.1.2 of the published monograph; they are not open conjectures. The formalization work is to check the infimum, projection and unique-minimizer statements with every domain and tie convention explicit. The mission poses theorem statements for proofs; these draft statements themselves do not yet supply machine-checked proofs. A complete development can reuse its finite matrix loss and finite vector projection vocabulary in other splitting algorithms.

Difficulty

The diagonal partial minimization is one-sided, while the proximal penalty is symmetric around $Z-U$ . An entrywise formula alone does not show that the assembled matrix minimizes the full objective or that it is the only minimizer. Symmetry also couples the two displayed off-diagonal positions $(i,j)$ and $(j,i)$ , so a scalar statement on one entry must agree with its transpose. For sparse projection, ties at the cutoff make a rule phrased as “the projection” ambiguous. For Boolean projection, the midpoint is a tie and requires a declared convention. These issues are part of the theorem statements, not numerical implementation details.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; symmetry is an entrywise equality predicate. The factor-model statements assume $n\ge1$ , symmetric $\Sigma,Z,U$ , and $\rho>0$ . The book uses $Z^k,U^k$ at an iteration; the Lean theorem uses those current matrices as parameters and does not posit convergence of an ADMM sequence. The reduced loss is literally the infimum over all componentwise nonnegative $d$ , and the Frobenius square is the finite sum of entry squares. The stated X-minimization ranges over all symmetric matrices, with no positive semidefinite or rank hypothesis on $X$ .

For sparse vectors, the index set has size $\min(c,n)$ and its selected magnitudes dominate unselected ones. This covers $c=0$ , $c>n$ and cutoff ties. The Boolean rounding function chooses zero when an entry equals $1/2$ . The book uses indices $1,\ldots,n$ ; Fin n uses $0,\ldots,n-1$ . On page 75 the printed diagonal branch conditions omit the superscript $k$ on $Z$ and $U$ ; the formalization uses the current $Z,U$ that appear in the surrounding ADMM update. The theorem requires the candidate to minimize the book's reduced loss, preventing an arbitrary replacement loss from making the statement trivial.

The development needs finite-sum algebra, real infima with an attained lower bound, symmetry of matrices, and nearest-point arguments for finite vectors. The rank- $c$ singular-value projection on page 74 is already an open target elsewhere and is outside this mission. The positive semidefinite rank- $k$ eigenvalue projection on page 76 is also outside this goal; it would require a separate spectral development. Contributions that prove the three milestones or the goal against these definitions are in scope. The page also mentions rounding under integer constraints; this mission selects the preceding Boolean claim as its projection milestone.

Selected references

Stephen Boyd, Neal Parikh, Eric Chu, Borja Peleato and Jonathan Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 73–76, §§9.1–9.1.2. DOI: 10.1561/2200000016.

7 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XVI: Random Coordinate Descent RCD(γ) on a Strongly Convex Coordinate-Smooth Function Has Rate (1 − 1/κ_γ)^tTextbook

Motivation

When a problem has millions of variables, even one full gradient can be too expensive to compute, while a single partial derivative $\partial f/\partial x_i$ is often cheap: in regularized regression, support vector machines and many structured problems, updating one coordinate costs a small fraction of a full gradient step. Coordinate descent methods exploit this by moving along one coordinate at a time. They are among the oldest optimization schemes and were for a long time analysed only for cyclic orders and only asymptotically.

Nesterov (2012) showed that choosing the coordinate at random, with probabilities depending on the coordinate-wise smoothness constants, gives global, non-asymptotic rates that can beat full gradient descent in total work. This mission formalizes that analysis as presented in §6.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 338–342, and in particular its linear rate for strongly convex functions (Theorem 6.8).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be differentiable, write $\nabla_i f(x)=\frac{\partial f}{\partial x_i}(x)$ and let $e_i$ be the $i$ -th standard basis vector. The function is directionally smooth with constants $\beta_1,\dots,\beta_n>0$ if

|\nabla_i f(x+ue_i)-\nabla_i f(x)|\le\beta_i|u|\qquad\text{for all } i\in[n],\ x\in\mathbb R^n,\ u\in\mathbb R,

equivalently, each one-variable restriction $u\mapsto f(x+ue_i)$ is $\beta_i$ -smooth.

For a real exponent $c$ , the weighted norms are

\|x\|_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{c}x_i^2},\qquad \|x\|^*_{[c]}=\sqrt{\textstyle\sum_{i}\beta_i^{-c}x_i^2}.

For $\alpha>0$ , $f$ is $\alpha$ -strongly convex w.r.t. a norm $\|\cdot\|$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y$ . The point $x^*$ is a minimizer of $f$ .

For $\gamma\ge0$ , RCD( $\gamma$ ) starts at $x_1\in\mathbb R^n$ and iterates

x_{s+1}=x_s-\frac{1}{\beta_{i_s}}\nabla_{i_s}f(x_s)\,e_{i_s},

where $i_1,i_2,\dots$ are drawn independently from $p_\gamma(i)=\beta_i^\gamma/\sum_{j}\beta_j^\gamma$ . The case $\gamma=0$ is uniform sampling; $\gamma=1$ samples proportionally to $\beta_i$ .

Formalization targets

Goal: Theorem 6.8 (p. 341)

Let $\gamma\ge0$ , let $f$ be $\alpha$ -strongly convex w.r.t. $\|\cdot\|_{[1-\gamma]}$ and directionally smooth with constants $\beta_i$ , and let $\kappa_\gamma=\sum_i\beta_i^\gamma/\alpha$ . Then for every $t\ge0$

\mathbb E f(x_{t+1})-f(x^*)\le\Big(1-\frac{1}{\kappa_\gamma}\Big)^t\big(f(x_1)-f(x^*)\big).

Milestones

Lemma 6.9 (p. 341): for $f$ $\alpha$ -strongly convex w.r.t. any norm, $f(x)-f(x^*)\le\frac{1}{2\alpha}\|\nabla f(x)\|_*^2$ .
One coordinate step (p. 340): $f\big(x-\frac{1}{\beta_i}\nabla_i f(x)e_i\big)-f(x)\le-\frac{1}{2\beta_i}(\nabla_i f(x))^2$ .
Expected decrease (p. 340): $\mathbb E_{i_s}f(x_{s+1})-f(x_s)\le-\frac{1}{2\sum_i\beta_i^\gamma}\big(\|\nabla f(x_s)\|^*_{[1-\gamma]}\big)^2$ .
Lemma 6.9 in the weighted norm (p. 342): $\big(\|\nabla f(x)\|^*_{[1-\gamma]}\big)^2\ge2\alpha(f(x)-f(x^*))$ .
Contraction (pp. 341–342): one step multiplies the expected gap by at most $1-1/\kappa_\gamma$ .

Companion: Theorem 6.7 (pp. 339–340)

For $f$ convex and directionally smooth, and $t\ge2$ ,

\mathbb E f(x_t)-f(x^*)\le\frac{2R_{1-\gamma}^2(x_1)\sum_i\beta_i^\gamma}{t-1},\qquad R_{1-\gamma}(x_1)=\sup_{f(x)\le f(x_1)}\|x-x^*\|_{[1-\gamma]}.

Significance

Theorem 6.8 says random coordinate descent converges linearly, with a rate governed by $\sum_i\beta_i^\gamma/\alpha$ instead of the global smoothness constant. For $\gamma=1$ , directional smoothness implies $f$ is $\beta$ -smooth with $\beta\le\sum_i\beta_i$ , so for functions whose global smoothness constant is of the order of $\sum_i\beta_i$ , RCD(1) attains the accuracy of gradient descent after the same number of iterations (book, p. 340, comparing Theorem 6.7 with Theorem 3.3), while each iteration touches a single coordinate. The same per-step inequalities underlie later accelerated and parallel coordinate methods.

These results are proved in the literature (Nesterov 2012; Bubeck 2015). Their contribution here is a machine-checked version. As far as a search of the Prove2Me catalogue shows, no coordinate descent rate of this kind has been formalized there; a Euclidean-norm special case of Lemma 6.9 exists on the platform as a separate result, but not the arbitrary-norm lemma or the weighted-norm instance used here.

Difficulty

The main obstacle is bookkeeping of the randomness: the per-step inequality holds for each fixed iterate, while the theorem is about the expectation over the whole sequence of draws $i_1,\dots,i_t$ , so the pointwise contraction has to be passed through the tower of conditional expectations. In the strongly convex case this is linear and exact; for Theorem 6.7 the recursion on $\delta_s=\mathbb Ef(x_s)-f(x^*)$ is quadratic, and since $\delta_s$ is an expectation while the gradient norm at $x_s$ is random, the pointwise inequality does not transfer to $\delta_s$ verbatim. A second point is geometric: strong convexity, the dual norm and the sampling distribution must use matching weights ( $\beta_i^{1-\gamma}$ against $\beta_i^{\gamma}$ ), and a mismatch silently changes the constant.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map $g$ with HasGradientAt f (g x) x, so $\nabla_i f(x)=g(x)_i$ . Lemma 6.9 is stated for a finite-dimensional real normed space with the Fréchet derivative and the operator norm as the dual norm.
Powers $\beta_i^c$ are real powers. The theorems assume $n\ge1$ , $\alpha>0$ and $\beta_i>0$ , which the book uses implicitly; $\gamma\ge0$ is the book's.
RCD(γ) is a deterministic function of the drawn coordinates, and the expectation over $t$ independent draws from $p_\gamma$ is the finite sum $\sum_{(i_1,\dots,i_t)\in[n]^t}\prod_s p_\gamma(i_s)\,F(i_1,\dots,i_t)$ . No measure theory or integrability conventions are involved.
The minimizer $x^*$ is assumed to exist, as the book does throughout; its uniqueness, which the book assumes "only for sake of notation", is not used.
In Theorem 6.7 the supremum $R_{1-\gamma}(x_1)$ is passed as any real upper bound $R$ on the sublevel set, which is equivalent when the supremum is finite and avoids Lean's value $0$ for an unbounded supremum.
Directional smoothness is required at every $x$ and $u$ , and $p_\gamma$ is fixed by the $\beta_i$ ; neither is weakened to hold only along the iterates, which would change the theorem.

A complete development needs the one-dimensional descent lemma (3.5), weighted Cauchy–Schwarz for the dual pair $\|\cdot\|_{[c]},\|\cdot\|^*_{[c]}$ , and a decomposition of the finite expectation over $[n]^{t+1}$ into the last draw and the first $t$ . The weighted-norm and finite-expectation lemmas are reusable for other randomized coordinate and sampling methods. Proofs of the milestones and of either theorem are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §6.4, pp. 338–342.
Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2):341–362, 2012. doi:10.1137/100802001
P. Richtárik and M. Takáč, Parallel coordinate descent methods for big data optimization, Mathematical Programming 156:433–484, 2016. arXiv:1212.0873

7 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XV: SVRG with η = 1/(10β) and k = 20κ Contracts the Expected Optimality Gap by 0.9 per EpochTextbook

Motivation

Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.

Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order $(m+\kappa)\log(1/\varepsilon)$ for the same regime, where $m$ is the number of components and $\kappa$ is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.

Setting

Let $f_1,\ldots,f_m:\mathbb R^n\to\mathbb R$ be differentiable convex functions, with $m\ge1$ , and define the finite-sum objective and its gradient by

f(x)=\frac1m\sum_{i=1}^m f_i(x),\qquad G(x)=\frac1m\sum_{i=1}^m \nabla f_i(x).

Each component is $\beta$ -smooth when its gradient is $\beta$ -Lipschitz in the Euclidean norm: $\|\nabla f_i(x)-\nabla f_i(z)\|_2\le\beta\|x-z\|_2$ for all $x,z$ . The average $f$ is $\alpha$ -strongly convex, meaning that for all $x,z$ it lies at least $\frac\alpha2\|z-x\|_2^2$ above its first-order affine approximation at $x$ . The constants $\alpha$ and $\beta$ are positive, $x^*$ minimizes $f$ over $\mathbb R^n$ , and $\kappa=\beta/\alpha$ .

An epoch begins at an anchor $y$ . Its first inner iterate is $x_1=y$ . For $t=1,\ldots,k$ , draw $i_t$ uniformly from $\{1,\ldots,m\}$ , independently across steps and epochs, and update

x_{t+1}=x_t-\eta\bigl(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)+G(y)\bigr).

The next anchor is the average $y^+=k^{-1}\sum_{t=1}^k x_t$ . In particular, this average uses $x_1$ through $x_k$ , while the last updated point $x_{k+1}$ is excluded. Starting from an arbitrary $y^{(1)}$ and repeating the epoch produces $y^{(s+1)}$ . The expectation of $f(y^{(s+1)})$ is over all $sk$ sampled indices in the first $s$ epochs.

Formalization targets

Goal: geometric contraction across epochs

Theorem 6.5 sets $\eta=1/(10\beta)$ and $k=20\kappa$ and asserts, for every $s\ge1$ ,

\mathbb E f(y^{(s+1)})-f(x^*) \le 0.9^s\bigl(f(y^{(1)})-f(x^*)\bigr).

The epoch length is a count, so the statement takes $k\in\mathbb N$ and explicitly requires $k=20\beta/\alpha$ . The goal uses exactly the book's step size, epoch length, and contraction factor.

Milestones: second moments and a single epoch

Lemma 6.4 bounds $\mathbb E_i\|\nabla f_i(x)-\nabla f_i(x^*)\|_2^2$ by $2\beta(f(x)-f(x^*))$ . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to $x^*$ . The later display on p. 338 bounds one epoch for any positive step size with $2\beta\eta<1$ . Finally, equation (6.1) substitutes the stated constants to obtain the factor $0.9$ for one epoch. These seven source claims form the milestone list in reading order.

Significance

The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap $D$ falls below $0.9^sD$ in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.

The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.

Difficulty

The sampled component gradient $\nabla f_{i_t}(x_t)$ need not be small when $x_t$ is near $x^*$ , so a bound using only its norm does not yield the desired fixed-step contraction. The correction $-\nabla f_{i_t}(y)+G(y)$ has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both $x_t$ and $y$ . The proof must control those two gaps while respecting the fact that $x_t$ depends on earlier samples. A single-index estimate with $x_t$ held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and $m\ge1$ and $k\ge1$ prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.

The component assumptions include differentiability with an explicit gradient map, convexity on all of $\mathbb R^n$ , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing $x^*$ exists; this is explicit. Positivity of $\alpha$ and $\beta$ , and integrality of $20\beta/\alpha$ , make the displayed divisions and epoch length meaningful. The general epoch bound also requires $0<\eta$ and $2\beta\eta<1$ . Dimension zero is allowed: the theorem remains a statement about the unique point of $\mathbb R^0$ and its zero objective gap.

The direction always contains the sampled difference $\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)$ and the full anchor gradient $G(y)$ . Replacing that direction with $G(x_t)$ would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.

Selected references

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, pp. 231–358. arXiv:1405.4980v2
Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, Advances in Neural Information Processing Systems 26 (NIPS), 2013 (the origin of SVRG, cited by Bubeck on p. 335). https://proceedings.neurips.cc/paper/2013/hash/ac1dd209cbcc5e5d1c6e28598e8cbbe8-Abstract.html

10 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XIV: Stochastic Mirror Descent on a β-Smooth Function with Noise σ Has Rate Rσ√(2/t) + βR²/tTextbook

Motivation

Many optimization problems in statistics and machine learning ask to minimize an expected loss $f(x)=\mathbb E_\xi\,\ell(x,\xi)$ , or an average $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ over a large data set. Exact gradients of such an $f$ are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.

Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order $1/\sqrt t$ and a smoothness term of order $1/t$ . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ . Gradients are linear forms $g$ on $E$ , the value of $g$ at $v$ is written $g^\top v$ , and the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ . Let $\mathcal X\subseteq E$ be compact and convex.

A mirror map is a function $\Phi$ on an open convex set $\mathcal D$ with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . It is strictly convex and differentiable on $\mathcal D$ , its gradient $\nabla\Phi$ takes every value, and $\|\nabla\Phi(x)\|_*\to\infty$ as $x$ approaches the boundary of $\mathcal D$ . Its Bregman divergence is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ . The map is 1-strongly convex on $\mathcal X\cap\mathcal D$ if $D_\Phi(y,x)\ge\frac12\|x-y\|^2$ there. A function $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

A stochastic oracle returns, at a query point $x$ , a random linear form $\tilde g(x)$ . When the query point is itself random, the book requires the conditional expectation given the query point, $\mathbb E(\tilde g(x)\mid x)$ , to be a subgradient of $f$ at $x$ . In the smooth case it requires $\mathbb E(\tilde g(x)\mid x)=\nabla f(x)$ together with the variance bound $\mathbb E(\|\tilde g(x)-\nabla f(x)\|_*^2\mid x)\le\sigma^2$ .

S-MD with step $\gamma$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, writing $\tilde g_s=\tilde g(x_s)$ , iterates

x_{s+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}\ \gamma\,\tilde g_s^\top x+D_\Phi(x,x_s).

Let $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , and let $x^*$ minimize $f$ on $\mathcal X$ .

Formalization targets

Goal: Theorem 6.3

Let $f$ be convex and $\beta$ -smooth, and let the oracle have variance at most $\sigma^2$ . Then for every $t\ge1$ , S-MD with step $1/(\beta+1/\eta)$ and $\eta=\frac R\sigma\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^t x_{s+1}\Big)-f(x^*)\le R\sigma\sqrt{\frac2t}+\frac{\beta R^2}{t}.

Milestones (the proof's four displays)

For points $x_s,x_{s+1}\in\mathcal X\cap\mathcal D$ and $\eta>0$ , the smoothness step is

f(x_{s+1})-f(x_s)\le\tilde g_s^\top(x_{s+1}-x_s)+\tfrac\eta2\|\nabla f(x_s)-\tilde g_s\|_*^2+(\beta+1/\eta)D_\Phi(x_{s+1},x_s).

If $x_{s+1}$ is the S-MD step, the mirror step is

\tfrac{1}{\beta+1/\eta}\tilde g_s^\top(x_{s+1}-x^*)\le D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})-D_\Phi(x_{s+1},x_s).

Combining the two gives a pathwise bound on $f(x_{s+1})$ with the cross term $(\tilde g_s-\nabla f(x_s))^\top(x^*-x_s)$ . Taking expectations gives the expected one-step bound

\mathbb Ef(x_{s+1})-f(x^*)\le(\beta+1/\eta)\,\mathbb E\big(D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})\big)+\frac{\eta\sigma^2}{2}.

Companion: Theorem 6.1 and (4.10)

For a convex $f$ with $\mathbb E(\|\tilde g(x)\|_*^2\mid x)\le B^2$ , S-MD with $\eta=\frac RB\sqrt{2/t}$ satisfies

\mathbb E\,f\Big(\frac1t\sum_{s=1}^tx_s\Big)-\min_{\mathcal X}f\le RB\sqrt{2/t}.

This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors $g_s$ :

\sum_{s\le t}g_s^\top(x_s-x)\le\frac{R^2}{\eta}+\frac{\eta}{2\rho}\sum_{s\le t}\|g_s\|_*^2.

Significance

Theorem 6.3 says exactly how much smoothness helps under noise. As $\sigma\to0$ it recovers the $\beta R^2/t$ rate of deterministic smooth optimization. For large $t$ the noise term $R\sigma\sqrt{2/t}$ dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging $m$ independent oracle answers divides the variance by $m$ , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by $\sqrt m$ while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.

These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.

Difficulty

The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point $x_s$ is random, so unbiasedness enters only through the conditional expectation given $x_s$ . Making the cross term vanish requires pulling the $\sigma(x_s)$ -measurable vector $x^*-x_s$ out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When $\nabla\Phi$ blows up at the boundary of $\mathcal D$ , the Bregman terms $D_\Phi(x^*,x_s)$ are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer $x^*$ may lie on the boundary of $\mathcal D$ , where $\Phi$ is not part of the book's data. Treating $\mathbb E$ informally, or assuming $x^*\in\mathcal D$ , skips exactly these points.

Formalization scope

Spaces and gradients. $E$ is a finite-dimensional real normed space. Gradients are explicit maps Φ' f' : E → (E →L[ℝ] ℝ), $g^\top v$ is g v, and $\|\cdot\|_*$ is the operator norm. $\beta$ -smoothness is stated with derivatives relative to $\mathcal X$ . $\Phi$ is a total function, constrained only by the mirror-map axioms on $\mathcal D$ .
Runs and oracle. S-MD is a run predicate. For every outcome, $x_1$ minimizes $\Phi$ on $\mathcal X\cap\mathcal D$ , and $x_{s+1}$ is some minimizer of the step objective. The oracle is a predicate on the random sequences $(x_s,\tilde g_s)$ : each $x_s$ is measurable, and the conditional expectations are taken given $\sigma(x_s)$ . Every conditioned quantity is integrable.
Conclusions. Every bound on an expectation also asserts integrability. Without it, the Lean integral of a non-integrable function is $0$ and the bound could hold trivially.
Standing assumptions. The book's $R^2=\sup(\Phi-\Phi(x_1))$ is replaced by any upper bound $R^2$ . The minimizer $x^*\in\mathcal X$ exists (p. 242). $\mathcal X$ is compact and convex (Chapter 4), and convex functions are closed (p. 236).
Positivity side conditions. $R,\sigma,B>0$ and $t\ge1$ make the step sizes and bounds defined, and $\beta\ge0$ .

A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let $x_{s+1}$ be an arbitrary point of $\mathcal X\cap\mathcal D$ would make the theorems false, and are not used either.

A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, https://arxiv.org/abs/1405.4980 (Chapter 6, pp. 329–333; Chapter 4, pp. 297–307).
O. Dekel, R. Gilad-Bachrach, O. Shamir, L. Xiao, Optimal distributed online prediction using mini-batches, Journal of Machine Learning Research 13:165–202, 2012. https://jmlr.org/papers/v13/dekel12a.html
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277

6 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XII: Mirror Prox on a Convex β-Smooth Function Has Rate βR²/(ρt)Textbook

Motivation

First-order methods for constrained convex optimization are usually analysed in the Euclidean norm, where gradient descent and its projected and accelerated variants have well-understood rates. Many constraint sets of practical interest, such as the probability simplex, the $\ell_1$ ball and the spectrahedron, are poorly adapted to the Euclidean geometry: the Euclidean diameter and the Euclidean Lipschitz or smoothness constants grow with the dimension. Mirror descent, due to Nemirovski and Yudin, replaces the Euclidean step by a step taken in the dual space through a mirror map $\Phi$ , so that the rate depends on constants measured in a norm matched to the set. For non-smooth Lipschitz functions it attains the rate $1/\sqrt t$ (Theorem 4.2 of the source, the subject of the previous mission of this series).

For smooth functions, a rate of order $1/t$ is available in any geometry by an extragradient-type modification. Mirror prox was introduced by Nemirovski in 2004 (Prox-method with rate of convergence O(1/t)) for variational inequalities with Lipschitz monotone operators and convex–concave saddle-point problems. It is the basis of smoothing approaches to non-smooth optimization and of stochastic saddle-point methods. This mission formalizes the version for minimizing a single smooth convex function, Theorem 4.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), §4.5.

Setting

Fix an arbitrary norm $\|\cdot\|$ on a finite-dimensional real space $E$ . Gradients are linear functionals on $E$ ; for a functional $g$ write $g^\top v$ for its value at $v$ , and $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ for the dual norm. Let $\mathcal X\subseteq E$ be compact and convex.

The Bregman divergence of a differentiable $\Phi$ is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$ .
Let $\mathcal D$ be a convex open set with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$ . A mirror map on $\mathcal D$ is a function $\Phi$ that is strictly convex and differentiable on $\mathcal D$ , whose gradient takes every value ( $\nabla\Phi(\mathcal D)$ is the whole dual space), and whose gradient norm tends to $+\infty$ at the boundary of $\mathcal D$ .
The Bregman projection of $y\in\mathcal D$ is $\Pi^\Phi_{\mathcal X}(y)=\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y)$ .
$\Phi$ is $\rho$ -strongly convex on $\mathcal X\cap\mathcal D$ if $\Phi(x)-\Phi(y)\le\nabla\Phi(x)^\top(x-y)-\frac\rho2\|x-y\|^2$ there; $f$ is $\beta$ -smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$ .

Mirror prox with step size $\eta$ generates, from $x_t$ ,

\nabla\Phi(y'_{t+1})=\nabla\Phi(x_t)-\eta\nabla f(x_t),\qquad y_{t+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y'_{t+1}),

\nabla\Phi(x'_{t+1})=\nabla\Phi(x_t)-\eta\nabla f(y_{t+1}),\qquad x_{t+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,x'_{t+1}).

The first half is a mirror descent step from $x_t$ to $y_{t+1}$ ; the second restarts from $x_t$ with the gradient evaluated at $y_{t+1}$ .

Formalization targets

Goal: Theorem 4.4

With $\eta=\rho/\beta$ , $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ , $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$ , $f$ convex and $\beta$ -smooth and $x^*$ a minimizer of $f$ on $\mathcal X$ , for every $t\ge1$

f\Bigl(\frac1t\sum_{s=1}^t y_{s+1}\Bigr)-f(x^*)\le\frac{\beta R^2}{\rho t}.

Milestones

Lemma 4.1 (Bregman projections): $(\nabla\Phi(\Pi^\Phi_{\mathcal X}(y))-\nabla\Phi(y))^\top(\Pi^\Phi_{\mathcal X}(y)-x)\le0$ and $D_\Phi(x,\Pi^\Phi_{\mathcal X}(y))+D_\Phi(\Pi^\Phi_{\mathcal X}(y),y)\le D_\Phi(x,y)$ for $x\in\mathcal X\cap\mathcal D$ , $y\in\mathcal D$ .
First term: $\eta\nabla f(y_{t+1})^\top(x_{t+1}-x)\le D_\Phi(x,x_t)-D_\Phi(x,x_{t+1})-D_\Phi(x_{t+1},x_t)$ .
Second term, (4.9): $\eta\nabla f(x_t)^\top(y_{t+1}-x_{t+1})\le D_\Phi(x_{t+1},x_t)-\frac\rho2\|x_{t+1}-y_{t+1}\|^2-\frac\rho2\|y_{t+1}-x_t\|^2$ .
Third term: $(\nabla f(y_{t+1})-\nabla f(x_t))^\top(y_{t+1}-x_{t+1})\le\frac\beta2\|y_{t+1}-x_t\|^2+\frac\beta2\|y_{t+1}-x_{t+1}\|^2$ .
Per-step bound: $f(y_{t+1})-f(x)\le\bigl(D_\Phi(x,x_t)-D_\Phi(x,x_{t+1})\bigr)/\eta$ for $x\in\mathcal X\cap\mathcal D$ .

The three-point identity (4.1), $(\nabla f(x)-\nabla f(y))^\top(x-z)=D_f(x,y)+D_f(z,x)-D_f(z,y)$ , is already posed on the platform as BeckTeboulleMD.EMDA.lemma_4_1 and is included by reference.

Significance

Theorem 4.4 shows that the $1/t$ rate of gradient descent on smooth functions survives in non-Euclidean geometries, with the dimension entering only through $R^2/\rho$ . With the negative entropy on the simplex, $R^2/\rho$ is of order $\log n$ for the $\ell_1$ norm, against a polynomial dependence for Euclidean methods. Beyond this single-function version, the same three-term argument is the core of the analysis of mirror prox for monotone variational inequalities and saddle-point problems (§4.6 and §5.2 of the source), where it gives the $1/t$ rate for smooth convex–concave games.

The result is proved in the source and in Nemirovski's paper. As far as this mission is aware it has no machine-checked proof; Mathlib has no Bregman divergences, mirror maps or mirror-descent-type algorithms. A formal proof would supply reusable infrastructure: the Bregman projection lemma (Lemma 4.1) and the three-point identity are used by every mirror-descent analysis, including the stochastic and online variants later in the source.

Difficulty

The obvious argument for mirror descent bounds $f(x_t)-f(x)$ by $\nabla f(x_t)^\top(x_t-x)$ and leaves a stability term of size $\eta^2\|\nabla f\|_*^2$ , which yields only $1/\sqrt t$ . Smoothness has to be used to cancel that term, and a single gradient step does not do so in a general norm. Mirror prox evaluates the gradient at the extrapolated point $y_{t+1}$ ; the analysis must show that the error created by using $\nabla f(x_t)$ for the first step is paid for by the strong convexity of $\Phi$ , which requires splitting $\nabla f(y_{t+1})^\top(y_{t+1}-x)$ into three terms and bounding each with matching constants.

In Lean the difficulty is in the infrastructure: first-order optimality of a Bregman projection over $\mathcal X\cap\mathcal D$ , which need not be closed; the passage from $x\in\mathcal X\cap\mathcal D$ to a minimizer $x^*$ that may lie on the boundary of $\mathcal D$ ; and Jensen's inequality for the average of the $y_{s+1}$ .

Formalization scope

$E$ is a finite-dimensional real normed space. Gradients are continuous linear functionals E →L[ℝ] ℝ given by explicit maps Φ' and f'; the dual norm is the operator norm. Φ' is the Fréchet derivative of $\Phi$ at each point of $\mathcal D$ ; f' is the derivative of $f$ relative to $\mathcal X$ at each point of $\mathcal X$ .
The mirror map definition keeps all three properties of §4.1, including surjectivity of the gradient and divergence at each frontier point of $\mathcal D$ .
Projections and runs are relations: every admissible argmin choice is covered; no choice function is used. The run is indexed from $t=1$ ; index $0$ is unused.
Standing and implicit hypotheses: $\mathcal X$ compact convex; a minimizer $x^*\in\mathcal X$ exists (the source's standing assumption); $\rho>0$ and $\beta>0$ (so that $\eta=\rho/\beta$ and the division by $\rho t$ are meaningful); $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ (unspecified in §4.5, taken as in mirror descent, §4.2).
$R$ is any real with $\Phi-\Phi(x_1)\le R^2$ on $\mathcal X\cap\mathcal D$ . The source's $R^2=\sup$ is the case where the supremum is finite; when it is infinite, the source's bound is void.
A run in which the second step started from $y_{t+1}$ , or projected $y'_{t+1}$ again, would be mirror descent, for which the claimed rate is false; the formal run follows the four equations of the source exactly. The average is over the extrapolated points $y_{s+1}$ , $s=1,\dots,t$ .

Contributions welcome: proofs of Lemma 4.1 and the three-term bounds, which are reusable for the stochastic mirror descent and saddle-point missions of this series, and the final telescoping and limit argument.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980v2
A. Nemirovski, Prox-method with rate of convergence O(1/t) for variational inequalities with Lipschitz continuous monotone operators and smooth convex-concave saddle point problems, SIAM Journal on Optimization 15(1):229–251, 2004. https://doi.org/10.1137/S1052623403425629
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

8 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity XI: Mirror Descent with a ρ-Strongly Convex Mirror Map Has Rate RL√(2/(ρt))Textbook

Motivation

The projected subgradient method of Chapter 3 measures distances in the Euclidean norm, and its rate $RL/\sqrt t$ depends on the geometry only through a Euclidean radius $R$ and a Euclidean bound $L$ on the subgradients. For many constraint sets that occur in practice this is the wrong geometry. On the probability simplex $\Delta_n$ with subgradients bounded in $\ell_\infty$ , as for linear losses with bounded coefficients, the Euclidean constants make $RL$ grow like $\sqrt n$ , while the problem itself is nearly dimension-free.

Mirror descent, introduced by Nemirovski and Yudin (1983), repairs this. The gradient step is taken in the dual space, after mapping the current point through the gradient of a strictly convex mirror map $\Phi$ , and feasibility is restored by a projection in the Bregman divergence of $\Phi$ rather than in the Euclidean distance. Beck and Teboulle (2003, doi:10.1016/S0167-6377(02)00231-6) recast it as a nonlinear projected subgradient method and showed that with the negative entropy on the simplex its rate is $O(L\sqrt{\log n/t})$ . Nesterov (2009, doi:10.1007/s10107-007-0149-x) introduced dual averaging, a lazy variant that averages the subgradients in the dual space and maps back only when a primal point is needed. Both methods underlie online learning (exponential weights is mirror descent with the entropy), stochastic optimization, and saddle-point methods such as mirror prox.

This mission is the eleventh of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980). It covers the preamble of Chapter 4, Sections 4.1 and 4.2, and Section 4.4.

Setting

Let $E$ be a finite-dimensional real vector space (the book's $\mathbb R^n$ ) with an arbitrary norm $\|\cdot\|$ . A linear functional $g$ on $E$ acts on $x$ by $g^\top x$ and has dual norm $\|g\|_*=\sup_{\|x\|\le1}g^\top x$ . Let $\mathcal X\subseteq E$ be compact and convex.

Let $\mathcal D\subseteq E$ be a convex open set with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\neq\emptyset$ . A function $\Phi:\mathcal D\to\mathbb R$ is a mirror map if it is strictly convex and differentiable, its gradient takes every value in the dual space, and $\|\nabla\Phi(x)\|\to+\infty$ as $x$ tends to the boundary of $\mathcal D$ . Its Bregman divergence is

D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y),

and the Bregman projection of $y\in\mathcal D$ is $\Pi^\Phi_{\mathcal X}(y)=\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}D_\Phi(x,y)$ . The mirror map is $\rho$ -strongly convex on $\mathcal X\cap\mathcal D$ if $\Phi(x)-\Phi(y)\le\nabla\Phi(x)^\top(x-y)-\frac\rho2\|x-y\|^2$ for all $x,y\in\mathcal X\cap\mathcal D$ .

Let $f$ be convex on $\mathcal X$ with a minimizer $x^*\in\mathcal X$ . A linear functional $g$ is a subgradient of $f$ at $x$ if $f(x)-f(y)\le g^\top(x-y)$ for all $y\in\mathcal X$ , and $f$ is $L$ -Lipschitz if the subgradients satisfy $\|g\|_*\le L$ .

Mirror descent with step $\eta$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, for $t\ge1$ , picks $g_t\in\partial f(x_t)$ and

\nabla\Phi(y_{t+1})=\nabla\Phi(x_t)-\eta g_t,\quad y_{t+1}\in\mathcal D,\qquad x_{t+1}=\Pi^\Phi_{\mathcal X}(y_{t+1}).\tag{4.2–4.3}

Dual averaging instead sets $x_t\in\operatorname{argmin}_{x\in\mathcal X\cap\mathcal D}\eta\sum_{s=1}^{t-1}g_s^\top x+\Phi(x)$ (4.6). Let $R^2$ bound $\Phi(x)-\Phi(x_1)$ over $\mathcal X\cap\mathcal D$ .

Formalization targets

Goal: Theorem 4.2

With $\eta=\frac RL\sqrt{\frac{2\rho}{t}}$ , every run of mirror descent satisfies

f\Big(\frac1t\sum_{s=1}^t x_s\Big)-f(x^*)\le RL\sqrt{\frac{2}{\rho t}}.

Milestones

The three-point identity (4.1): $(\nabla f(x)-\nabla f(y))^\top(x-z)=D_f(x,y)+D_f(z,x)-D_f(z,y)$ .
Lemma 4.1: for $x\in\mathcal X\cap\mathcal D$ and $y\in\mathcal D$ , $D_\Phi(x,\Pi^\Phi_{\mathcal X}(y))+D_\Phi(\Pi^\Phi_{\mathcal X}(y),y)\le D_\Phi(x,y)$ , together with the first-order inequality that implies it.
The per-step inequality: $f(x_s)-f(x)\le\frac1\eta\big(D_\Phi(x,x_s)+D_\Phi(x_s,y_{s+1})-D_\Phi(x,x_{s+1})-D_\Phi(x_{s+1},y_{s+1})\big)$ .
The stability term: $D_\Phi(x_s,y_{s+1})-D_\Phi(x_{s+1},y_{s+1})\le(\eta L)^2/(2\rho)$ .
The summed bound: $\sum_{s=1}^t(f(x_s)-f(x))\le D_\Phi(x,x_1)/\eta+\eta L^2t/(2\rho)$ .

Companion: Theorem 4.3

With $\eta=\frac RL\sqrt{\frac{\rho}{2t}}$ , dual averaging satisfies $f\big(\frac1t\sum_{s=1}^tx_s\big)-f(x^*)\le2RL\sqrt{\frac2{\rho t}}$ , with the two displays (4.7) and (4.8) of its proof as supporting items.

Significance

Theorem 4.2 is the basic rate of non-Euclidean first-order optimization. With the Euclidean mirror map $\Phi=\frac12\|\cdot\|_2^2$ it recovers the projected subgradient rate of Chapter 3; with the negative entropy on the simplex, which is $1$ -strongly convex for $\ell_1$ by Pinsker's inequality and has $R^2=\log n$ , it gives $L_\infty\sqrt{2\log n/t}$ , so the dependence on the dimension becomes logarithmic. The same analysis, with $f$ replaced by a sequence of losses, is the regret bound of online mirror descent, and its per-step and stability inequalities are reused for stochastic mirror descent and mirror prox in later chapters of the book.

The results are classical and fully proved in the book. What this mission adds is a machine-checked version in a general finite-dimensional normed space, with gradients as linear functionals and the dual norm as the operator norm, for an arbitrary mirror map on an arbitrary open domain. On Prove2Me the three-point identity (4.1) is already posed, as Lemma 4.1 of the Beck–Teboulle formalization, and is reused here; a regret bound for online mirror descent with Legendre functions is proved in another library, but it is not this theorem and does not cover a domain $\mathcal D$ distinct from the whole space or a Bregman projection onto $\mathcal X\cap\mathcal D$ .

Difficulty

The algebra of the proof is short. The difficulty lies at the boundary of $\mathcal D$ . The minimizer $x^*$ may lie on $\partial\mathcal D$ , where $\Phi$ and $\nabla\Phi$ are not defined; this is the typical case for the entropy on the simplex, where $x^*$ is often a vertex. The per-step bound holds only for comparison points $x\in\mathcal X\cap\mathcal D$ , so the bound at $x^*$ has to be recovered from points of $\mathcal X\cap\mathcal D$ , where no regularity of $f$ beyond convexity on $\mathcal X$ is available. Lemma 4.1 needs the first-order optimality condition of the Bregman projection over the convex set $\mathcal X\cap\mathcal D$ , which is not closed. In the non-Euclidean setting the gradient step cannot be written in the primal space at all: the update (4.2) is an equation between linear functionals, and the norm and dual norm must be kept apart throughout.

Formalization scope

The space is a finite-dimensional real normed space E with an arbitrary norm; gradients and subgradients are elements of E →L[ℝ] ℝ, the dual norm is the operator norm, and $\nabla\Phi$ is an explicit map Φ' with HasFDerivAt Φ (Φ' x) x on $\mathcal D$ .
The mirror map carries all three properties (i)–(iii) of the book; the standing setting ( $\mathcal X$ compact convex, $\mathcal X\subseteq\overline{\mathcal D}$ , $\mathcal X\cap\mathcal D\neq\emptyset$ ) is a single predicate.
Runs are predicates over the first $t$ steps, quantified universally: any subgradient, any $y_{t+1}$ solving (4.2), any minimizer. A run whose next iterate were an arbitrary point of $\mathcal X\cap\mathcal D$ , rather than the Bregman projection, would make the theorem false; the projection is part of the run.
Sequences are indexed from $1$ ; $t\ge1$ , $\rho>0$ , $L>0$ , $R>0$ and $\eta>0$ are explicit, since the step and the bound divide by them.
$R^2$ is any upper bound of $\sup_{\mathcal X\cap\mathcal D}\Phi-\Phi(x_1)$ (the book's $R$ is the least one); when the supremum is infinite the hypotheses cannot be met, as on the page.
" $f$ is $L$ -Lipschitz" is assumed for the subgradients the run uses. Subgradients relative to $\mathcal X$ are unbounded at boundary points of $\mathcal X$ , so the literal "every subgradient at every point" would make the hypothesis unsatisfiable.
The definitions (Bregman divergence, mirror map, Bregman projection, the two runs) are reusable by the later chapters on mirror prox and stochastic mirror descent. Proofs of any milestone, and of the general facts they need (nonnegativity of Bregman divergences, first-order optimality over a convex set that is not closed), are welcome.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983 (book; no DOI).
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. doi:10.1016/S0167-6377(02)00231-6
Y. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120(1):221–259, 2009. doi:10.1007/s10107-007-0149-x

7 thms3 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity IX: Nesterov's Accelerated Gradient Descent on a Convex β-Smooth Function Has Rate 2β‖x₁ − x*‖²/t²Textbook

Motivation

Minimizing a convex function $f:\mathbb R^n\to\mathbb R$ whose gradient is Lipschitz is the basic problem of first-order optimization, and it is the regime in which most large-scale methods of machine learning, signal processing and operations research are analysed. The natural method, gradient descent, reaches accuracy $\varepsilon$ after $O(1/\varepsilon)$ gradient evaluations. In 1983 Nesterov showed that a method using the same oracle, but combining the current and the previous iterate, reaches accuracy $\varepsilon$ after only $O(1/\sqrt\varepsilon)$ evaluations, and that no method using only gradient information can do better by more than a constant factor. This accelerated gradient descent and its proximal variants (FISTA) are now the default fast first-order methods for smooth and composite convex problems.

This mission formalizes the accelerated rate as presented in S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §3.7.2, Theorem 3.19, whose proof follows Beck and Teboulle (2009).

Timeline.

1983: Nesterov introduces the accelerated method with rate $O(1/t^2)$ for convex functions with Lipschitz gradient (Soviet Math. Dokl. 27).
1983: Nemirovski and Yudin's black-box lower bounds show that $\Omega(1/t^2)$ is the best possible rate for this class (Theorem 3.14 of the book gives $3\beta\|x_1-x^*\|^2/(32(t+1)^2)$ ).
2009: Beck and Teboulle's FISTA extends the method, with the same step sequence $\lambda_t$ , to composite problems with a simple nonsmooth term (SIAM J. Imaging Sci. 2(1)).
2008: Tseng gives a unified treatment with simpler step sizes (manuscript).

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$ . A differentiable function $f:\mathbb R^n\to\mathbb R$ is β-smooth if its gradient is $\beta$ -Lipschitz:

\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad(x,y\in\mathbb R^n).

Assume $f$ is convex and $\beta$ -smooth with $\beta>0$ , and let $x^*$ be a minimizer of $f$ .

Define the step sequences $\lambda_0=0$ ,

\lambda_t=\frac{1+\sqrt{1+4\lambda_{t-1}^2}}{2}\quad(t\ge1),\qquad\gamma_t=\frac{1-\lambda_t}{\lambda_{t+1}}.

Then $\lambda_1=1$ , $\lambda_t\ge1$ for $t\ge1$ , and $\gamma_t\le0$ . Nesterov's accelerated gradient descent for the smooth case starts from an arbitrary point $x_1=y_1$ and sets, for $t\ge1$ ,

y_{t+1}=x_t-\frac1\beta\nabla f(x_t),\qquad x_{t+1}=(1-\gamma_t)\,y_{t+1}+\gamma_t\,y_t.

The primary sequence $(y_t)$ consists of gradient steps of length $1/\beta$ ; the sequence $(x_t)$ , at which the gradient is queried, moves past $y_{t+1}$ away from $y_t$ (since $\gamma_t\le0$ ). Write $\delta_t=f(y_t)-f(x^*)$ for the optimality gap.

Formalization targets

Goal: Theorem 3.19

For every run of the method and every $t\ge1$ ,

f(y_t)-f(x^*)\le\frac{2\beta\|x_1-x^*\|^2}{t^2}.

The constant $2$ and the exponent $2$ are those printed in the book.

Milestones

In the order of the book's proof (pp. 294–295):

Lemma 3.6, unconstrained (p. 270): $f(x-\tfrac1\beta\nabla f(x))-f(y)\le\nabla f(x)^\top(x-y)-\tfrac1{2\beta}\|\nabla f(x)\|^2$ for all $x,y$ .
(3.23): $f(y_{s+1})-f(y_s)\le\beta(x_s-y_{s+1})^\top(x_s-y_s)-\tfrac\beta2\|x_s-y_{s+1}\|^2$ .
(3.24): $f(y_{s+1})-f(x^*)\le\beta(x_s-y_{s+1})^\top(x_s-x^*)-\tfrac\beta2\|x_s-y_{s+1}\|^2$ .
The λ identity: $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ for $s\ge1$ .
(3.25): $\lambda_s^2\delta_{s+1}-\lambda_{s-1}^2\delta_s\le\tfrac\beta2\bigl(\|\lambda_sx_s-(\lambda_s-1)y_s-x^*\|^2-\|\lambda_sy_{s+1}-(\lambda_s-1)y_s-x^*\|^2\bigr)$ .
(3.26): $\lambda_{s+1}x_{s+1}-(\lambda_{s+1}-1)y_{s+1}=\lambda_sy_{s+1}-(\lambda_s-1)y_s$ .
Telescoped bound: $\delta_t\le\frac{\beta}{2\lambda_{t-1}^2}\|u_1\|^2$ for $t\ge2$ , with $u_1=\lambda_1x_1-(\lambda_1-1)y_1-x^*$ .
Growth of λ: $\lambda_{t-1}\ge t/2$ for $t\ge2$ .

Significance

The result. Theorem 3.19 is the upper half of the statement that first-order methods on smooth convex functions have complexity $\Theta(\sqrt{\beta\|x_1-x^*\|^2/\varepsilon})$ : together with the black-box lower bound of Theorem 3.14 it shows that the accelerated method is optimal up to a constant factor, while plain gradient descent (Theorem 3.3, rate $2\beta\|x_1-x^*\|^2/(t-1)$ ) is not. The same potential-function argument, with the gradient step replaced by a proximal step, yields the rate of FISTA for composite objectives, and the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ is the algebraic core of most later analyses of accelerated and momentum methods.

Formalizing it. The theorem is classical and fully proved on paper. What this mission adds is a machine-checked proof of the $O(1/t^2)$ rate for the exact step sequence of the book, with every intermediate inequality of the proof stated separately so that each can be closed and reused. A Lean development of accelerated gradient descent with this rate is not, to our knowledge, in Mathlib.

Difficulty

The rate does not follow from monotone decrease of $f(y_t)$ , which is the engine of the analysis of plain gradient descent: the accelerated iterates are not monotone, and no single-step inequality on $\delta_t$ alone gives $1/t^2$ . The proof instead tracks a weighted potential $\lambda_{s-1}^2\delta_s+\frac\beta2\|u_s\|^2$ and needs three exact algebraic coincidences: the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ , the completion of a square $2a^\top b-\|a\|^2=\|b\|^2-\|b-a\|^2$ , and the rewriting (3.26) of the update rule, which makes consecutive potentials match exactly. In Lean the work is in this bookkeeping (vector identities in an inner-product space, a real recursion with square roots, and a telescoping sum indexed from $1$ ), not in any deep analytic fact.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $x^\top y$ is ⟪x, y⟫_ℝ.
The gradient is an explicit map $g$ with HasGradientAt f (g x) x for every $x$ ; β-smoothness is the Lipschitz bound on $g$ (not the quadratic upper bound (3.4), which is a consequence). Convexity is ConvexOn ℝ Set.univ f.
$\lambda$ is a real sequence defined by recursion on $\mathbb N$ with $\lambda_0=0$ ; $\gamma_t=(1-\lambda_t)/\lambda_{t+1}$ never divides by zero because $\lambda_{t+1}\ge1$ .
A run is a predicate on two sequences $x,y:\mathbb N\to\mathbb R^n$ , indexed from $1$ as in the book; index $0$ is unconstrained. Every theorem quantifies over all runs.
Standing assumptions: $x^*$ is a minimizer of $f$ (book, p. 242); $\beta>0$ (implicit in the step $1/\beta$ ) is a stated hypothesis.
The page prints the update as $x_{t+1}=(1-\gamma_s)y_{t+1}+\gamma_ty_t$ ; the formalization uses $\gamma_t$ in both places, as the proof's (3.26) requires. A run predicate with a fixed coefficient $\gamma_s$ would describe a different (non-accelerated) method and is ruled out.
The goal is stated for all $t\ge1$ , including $t=1$ , which the printed proof does not cover but which follows from (3.4). The growth bound $\lambda_{t-1}\ge t/2$ is stated for $t\ge2$ , since $\lambda_0=0$ . The telescoping display prints $\delta_s^2$ for $\delta_s$ ; the formalization uses $\delta_s$ .

Contributions of every kind are welcome: proofs of the λ facts and of (3.26) are pure algebra; (3.23)–(3.25) need the descent lemma for β-smooth functions and first-order convexity, both of which are reusable well beyond this mission.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983. mathnet
A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sciences 2(1):183–202, 2009. doi:10.1137/080716542
P. Tseng, On accelerated proximal gradient methods for convex-concave optimization, manuscript, 2008. pdf
A. Nemirovski, D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

10 thms3 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Rademacher and Gaussian Complexities: Risk Bounds and Structural Results 6: The Expected Maximum Discrepancy Lies Between R_n(F)/2 − 2√(2/n) and R_n(F) + 4√(2/n)Research Paper

Motivation

Data-dependent risk bounds in statistical learning theory control the gap between the expected loss of a learned function and its empirical loss by a complexity penalty that is computed from the training data. The first such penalties were the maximum discrepancy of a function class (Bartlett, Boucheron and Lugosi, Model selection and error estimation, Machine Learning 48, 2002) and its Rademacher complexity (Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Trans. Inf. Theory 47, 2001; Koltchinskii and Panchenko 2000). The maximum discrepancy compares the behaviour of the class on two fixed halves of the sample; the Rademacher complexity compares it on two random halves. Bartlett and Mendelson (JMLR 3, 2002), Lemma 3, show that these two quantities are equivalent up to a factor 2 and an additive $O(1/\sqrt n)$ . This mission formalizes that lemma from the published JMLR article (pp. 463–482); the proof is its Appendix A.

Setting

Let $\mu$ be a probability measure on a measurable space $\mathcal X$ and let $X_1,\dots,X_n$ be independent samples from $\mu$ . Let $F$ be a class of measurable functions $f:\mathcal X\to[-1,1]$ . Let $\sigma_1,\dots,\sigma_n$ be independent uniform $\{\pm1\}$ -valued random variables, independent of the sample.

The Rademacher complexity of $F$ is

R_n(F) = \mathbf E\sup_{f\in F}\left|\frac2n\sum_{i=1}^n\sigma_i f(X_i)\right|.

For even $n$ , the maximum discrepancy of $F$ is the random variable

\hat D_n(F) = \sup_{f\in F}\left(\frac2n\sum_{i=1}^{n/2}f(X_i) - \frac2n\sum_{i=n/2+1}^n f(X_i)\right),

with no absolute value, and the expected maximum discrepancy is $D_n(F)=\mathbf E\hat D_n(F)$ . The class is closed under negation if $f\in F$ implies $-f\in F$ , and $-F=\{-f:f\in F\}$ .

The proof works with the conditional supremum function

s(N) = \frac2n\,\mathbf E\left[\sup_{f\in F}\sum_{i=1}^n\sigma_i f(X_i)\;\middle|\;\sum_{i=1}^n\sigma_i=N\right],

defined for the values $N$ that $\sum_i\sigma_i$ can take.

Formalization targets

Goal: Lemma 3, first and second displays

For every even $n\ge2$ ,

\frac{R_n(F)}{2} - 2\sqrt{\frac2n} \le D_n(F) \le R_n(F) + 4\sqrt{\frac2n},

and if $F$ is closed under negation,

R_n(F) - 4\sqrt{\frac2n} \le D_n(F).

Milestones (Appendix A, pp. 479–480)

$R_n(F)\ge\mathbf E\,s(\sum_i\sigma_i)$ , with equality when $F$ is closed under negation.
$D_n(F) = s(0)$ .
$|s(N_1)-s(N_2)|\le 4|N_2-N_1|/n$ .
$|\mathbf E s(N)-s(\mathbf EN)|\le\mathbf E|s(N)-s(\mathbf EN)|\le4\sqrt{2/n}$ for $N=\sum_i\sigma_i$ .
$R_n(F)=R_n(F\cup-F)\le D_n(F\cup-F)+4\sqrt{2/n}$ .
$D_n(F\cup-F)\le 2D_n(F)+D_n(\{f_0,-f_0\})$ for any $f_0\in F$ (a corrected form of the printed step, see below).

Significance

Lemma 3 makes the maximum discrepancy and the Rademacher complexity interchangeable in risk bounds: a bound in terms of one gives a bound in terms of the other with an explicit additive loss. The maximum discrepancy can be computed by a single empirical risk minimization on a relabelled sample, while the Rademacher complexity has the structural properties (monotonicity, convex-hull invariance, contraction) that make it easy to bound for concrete classes; the lemma transfers the second kind of estimate to the first quantity.

The lemma is proved in the paper; no machine-checked proof of it, or of the comparison between fixed and random half-sample splits, is known to exist. Formalizing it requires the exchangeability argument for i.i.d. samples, the conditioning of a uniform sign vector on its sum, and a moment bound for the Rademacher sum $\sum_i\sigma_i$ , all with explicit constants.

Difficulty

The heart of the proof is that, conditioned on the number of positive signs, a uniform sign vector splits the i.i.d. sample into two random subsets of fixed sizes, and every split of the same sizes has the same law as the fixed split. Making this precise requires a permutation-invariance argument for product measures applied to a supremum over an arbitrary class, where measurability is not automatic. The step from classes closed under negation to general classes is where the printed argument is loose: since $\hat D_n$ has no absolute value, $\hat D_n(F\cup-F)$ is a maximum of two suprema that may be negative, and the naive bound $D_n(F\cup-F)\le2D_n(F)$ fails.

Formalization scope

The Lean development lives in the namespace RadGauss.Discrepancy. Sign vectors are Fin n → Bool (true ↦ 1, false ↦ -1) and expectations over signs are finite averages over all $2^n$ sign vectors; $s(N)$ is the average over the sign vectors with sum $N$ . $R_n$ takes values in $[0,\infty]$ (a lower Lebesgue integral of an $[0,\infty]$ -valued supremum), while $\hat D_n$ , $D_n$ and $s$ are real, because the maximum discrepancy is signed. Inequalities of the form $a-c\le D$ are written $a\le D+c$ with real terms embedded by ENNReal.ofReal; this is equivalent to the printed form since $D_n(F)\ge0$ for nonempty $F$ .

Hypotheses added to the page, all disclosed in each item:

the sample size is even, $n=2m$ with $m\ge1$ , since $\hat D_n$ needs half sums;
$F$ is nonempty (the supremum over the empty class is $-\infty$ in the paper and $0$ in Lean);
every $f\in F$ is measurable, and for every sign vector $\sigma$ the map $x\mapsto\sup_{f\in F}\sum_i\sigma_if(x_i)$ is measurable. This is the measurability guard: without it the Bochner integrals defining $D_n$ and $s$ would silently be $0$ .

Corrections of printed statements:

The Lipschitz bound on $s$ is printed for $0\le n_2<n_1\le n$ but used for negative values of $\sum_i\sigma_i$ ; it is stated for every pair of attainable values.
The printed step $D_n(F\cup-F)\le2D_n(F)$ is false for the signed $\hat D_n$ of p. 464 ( $F=\{f\}$ , $f(X)$ uniform on $\{\pm1\}$ , $n=2$ gives $1\le0$ ); the milestone states it with the additional term $D_n(\{f_0,-f_0\})\le2/\sqrt n$ . The goal itself remains true.
The third display of Lemma 3, $P\{|\hat D_n(F)-D_n(F)|\ge\epsilon\}\le2\exp(-\epsilon^2n/2)$ , is false as printed ( $F=\{f\}$ as above, $n=2$ , $\epsilon=2$ : the probability is $1/2>2e^{-4}$ ) and is not part of the mission.

A formalization in which $D_n$ or $s$ is a junk value (non-integrable or non-measurable suprema, an empty class, an odd sample size with truncated $n/2$ ) would make the goal trivial or meaningless; the hypotheses above rule that out, and the class $F=\{0\}$ satisfies all of them.

Welcome contributions include general lemmas on the invariance of $\mathbf E\sup_{f\in F}\Phi_f(X_{\pi(1)},\dots,X_{\pi(n)})$ under permutations $\pi$ of an i.i.d. sample, conditioning of uniform sign vectors on their sum, and the bound $\mathbf E|\sum_i\sigma_i|\le\sqrt n$ . These are reusable well beyond this mission.

Selected references

P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002) 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48 (2002) 85–113. https://doi.org/10.1023/A:1013999503812
V. Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Transactions on Information Theory 47 (2001) 1902–1914. https://doi.org/10.1109/18.930926
L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5

10 thms3 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Rademacher and Gaussian Complexities: Risk Bounds and Structural Results 5: Kernel Expansions with α′Kα ≤ B² Have Rademacher and Gaussian Complexity at Most 2B√(E k(X,X)/n)Research Paper

Motivation

Kernel methods, such as support vector machines, predict with functions of the form $x \mapsto \sum_i \alpha_i k(x, x_i)$ : finite expansions of a fixed similarity function $k$ centred at data points. Their statistical behaviour is governed by the size of the class of such expansions that the method searches. Bartlett and Mendelson, in Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002), develop risk bounds in terms of the Rademacher and Gaussian complexities of a class, and in §4.3 (pp. 476–478) compute these complexities for the class of kernel expansions whose coefficient vector has quadratic form $\alpha' K \alpha \le B^2$ . The resulting bound depends on the kernel only through its diagonal $k(x,x)$ , which is what makes margin bounds for support vector machines dimension-free. This mission formalizes that computation. The source is the published JMLR article (pages cited by the journal's printed numbers).

Setting

Let $\mathcal X$ be a compact topological space. A kernel is a continuous function $k : \mathcal X \times \mathcal X \to \mathbb R$ such that for every $m$ and all $x_1, \dots, x_m \in \mathcal X$ the Gram matrix $K_{ij} = k(x_i, x_j)$ is symmetric and positive semidefinite. For $B \ge 0$ the class of kernel expansions is

F = \Big\{x \mapsto \sum_{i=1}^m \alpha_i k(x, x_i) : m \in \mathbb N,\ x_i \in \mathcal X,\ \alpha_i \in \mathbb R,\ \sum_{i,j}\alpha_i\alpha_j k(x_i, x_j) \le B^2\Big\},

with centres anywhere in $\mathcal X$ (Lean: kernelClass k B).

For a class $F$ of real functions on $\mathcal X$ and a sample $x_1, \dots, x_n$ , let $\sigma_1, \dots, \sigma_n$ be independent uniform signs and $g_1, \dots, g_n$ independent standard Gaussians. The empirical Rademacher complexity and empirical Gaussian complexity (Definition 2, p. 464) are

\hat R_n(F) = \mathbb E_\sigma \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n \sigma_i f(x_i)\Big|, \qquad \hat G_n(F) = \mathbb E_g \sup_{f\in F}\Big|\frac2n\sum_{i=1}^n g_i f(x_i)\Big|.

For a probability measure $\mu$ on $\mathcal X$ and an i.i.d. sample $X_1, \dots, X_n \sim \mu$ , the Rademacher complexity is $R_n(F) = \mathbb E \hat R_n(F)$ and the Gaussian complexity is $G_n(F) = \mathbb E \hat G_n(F)$ (Lean: empiricalRademacher, empiricalGaussian, rademacherComplexity, gaussianComplexity).

A feature map of $k$ is a map $\Phi : \mathcal X \to \mathcal H$ into a real Hilbert space with $k(x_1, x_2) = \langle \Phi(x_1), \Phi(x_2) \rangle$ .

Formalization targets

Goal: the expected complexity bound (§4.3, p. 478, display after the proof of Lemma 22)

With $X \sim \mu$ ,

R_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}, \qquad G_n(F) \le 2B\sqrt{\frac{\mathbb E\, k(X,X)}{n}}.

Milestone 1: feature-map inclusion (p. 477)

For any feature map $\Phi$ of $k$ , $\|\sum_i \alpha_i \Phi(x_i)\|^2 = \sum_{i,j}\alpha_i\alpha_j k(x_i,x_j)$ , and hence $F \subseteq \{x \mapsto \langle w, \Phi(x)\rangle : \|w\| \le B\}$ .

Milestone 2: Lemma 22 (p. 477)

For every sample $X_1, \dots, X_n$ ,

\hat G_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}, \qquad \hat R_n(F) \le \frac{2B}{n}\sqrt{\sum_{i=1}^n k(X_i, X_i)}.

Significance

The goal shows that the kernel class has complexity of order $n^{-1/2}$ , with a constant given by $B$ and the quantity $\mathbb E\, k(X,X)$ , which is the trace of the integral operator $T_k f = \int k(\cdot, y) f(y)\, d\mu(y)$ on $L_2(\mu)$ . No dimension of the feature space enters. Fed into the paper's margin-cost risk bound (Theorem 21, p. 476), the sample-wise Lemma 22 gives a data-dependent misclassification bound for support vector machines in terms of the trace of the Gram matrix of the training sample. Bounds of this form are the standard complexity estimate for kernel classes in learning theory textbooks.

The result is proved in the paper; nothing in this mission is open mathematics. What the mission adds is a machine-checked version with the paper's normalization (factor $2/n$ , absolute value inside the supremum), covering both the Rademacher and the Gaussian complexity, for expansions with centres anywhere in $\mathcal X$ . Related statements on the platform (Mohri et al.'s Theorem 5.10 and Proposition 9.3) use the $1/n$ normalization without absolute value, assume a uniform bound $\sup_x k(x,x) \le r^2$ , and treat only the Rademacher case, so they do not imply the targets here.

Difficulty

The class $F$ is defined through the kernel, not through a feature map, and its expansions have arbitrarily many centres anywhere in $\mathcal X$ . The supremum over $F$ is therefore a supremum over an infinite-dimensional family, and must be controlled without assuming a separate numerical upper bound on $k(x,x)$ or that the feature space is finite dimensional. For the Gaussian complexity the supremum sits inside an expectation over a continuous random vector, and the passage from the sample-wise bound to the expected bound must move an expectation inside a square root in the right direction. A bound with $\sup_x k(x,x)$ in place of $\mathbb E\, k(X,X)$ is weaker and is not the target.

Formalization scope

Conventions committed to in Lean:

Complexities take values in $[0, \infty]$ (ℝ≥0∞); expectations over the Gaussian vector and over the sample are lower Lebesgue integrals against product measures, and the Rademacher expectation is the exact average over the $2^n$ sign vectors $\sigma : \mathrm{Fin}\,n \to \mathbb Z^\times$ . An unbounded class has complexity $+\infty$ , so a junk value of $0$ for a real supremum or a non-integrable expectation cannot make the bounds trivial.
A kernel (IsKernel k) carries compactness of $\mathcal X$ , joint continuity, and positive semidefiniteness (with symmetry) of every Gram matrix, as in the paper's definition. The goal puts the Borel $\sigma$ -algebra on $\mathcal X$ and assumes $\mu$ is a probability measure; $\mathbb E\, k(X,X)$ is the Bochner integral of the continuous function $x \mapsto k(x,x)$ .
$B \ge 0$ is assumed in every statement (the paper fixes $B > 0$ ). For $B < 0$ the right-hand sides are negative while the left-hand sides are not, and the inclusion of milestone 1 fails.
No $n \ge 1$ hypothesis: at $n = 0$ both sides of every bound are $0$ in Lean.
The feature map in milestone 1 is a hypothesis (any real Hilbert space and any $\Phi$ with $k = \langle \Phi(\cdot), \Phi(\cdot)\rangle$ ); its existence is the RKHS theorem, referenced as the supporting platform item FoundationsML.Kernels.RKHS_exists.
No measurability or integrability hypotheses on $\hat R_n(F)$ or $\hat G_n(F)$ are assumed, and none is needed.

A trivializing formalization is ruled out: the goal is stated for the kernel class $F$ itself, not for the larger ball of linear functionals of a feature map, and not for the subclass with centres at the sample points.

Infrastructure a complete development needs: Gaussian integration over $\mathbb R^n$ (second moments of a standard Gaussian vector), Jensen's inequality for the square root under a lower Lebesgue integral, and Cauchy–Schwarz for positive semidefinite bilinear forms (or the RKHS feature map). The Definition 2 complexities are shared with the paper's other missions and reusable. Contributions of any of these milestones, and of proofs of the goal that avoid the feature map, are welcome.

Selected references

P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
N. Cristianini and J. Shawe-Taylor, An Introduction to Support Vector Machines, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511801389
N. Aronszajn, Theory of Reproducing Kernels, Transactions of the American Mathematical Society 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/

8 thms3 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Local Rademacher Complexities I: The Error Is Bounded by the Fixed Point of a Sub-Root Bound on Local Rademacher Averages of the Star-Hull (Theorem 3.3, Part 2)Research Paper

Motivation

A learning algorithm that picks a function $\hat f$ from a class $\mathcal F$ by minimizing an empirical average is only as good as the gap between the empirical average $P_n f$ and the true mean $Pf$ , uniformly over the functions it might choose. The classical way to control this gap uses a global complexity of the whole class, such as its Rademacher average, and yields rates of order $1/\sqrt n$ . These rates are too slow in many problems of statistics and learning theory, where the functions that matter (those close to the best one) have small variance. Bartlett, Bousquet and Mendelson (arXiv:math/0508275, Annals of Statistics 33 (2005) 1497–1537) showed that the gap can instead be controlled by a local complexity, the Rademacher average of the small-variance part of the class. The resulting bounds give fast rates, often of order $\log n / n$ , and the paper is the standard reference for this method in empirical process theory and statistical learning.

The method builds on Koltchinskii and Panchenko (2000), Massart (2000) and Lugosi and Wegkamp (2004), and its concentration step uses Bousquet's form of Talagrand's inequality (2002). It is the basis of the fast-rate analyses in Koltchinskii's 2006 Annals of Statistics paper on local Rademacher complexities and oracle inequalities, and in later work on variance-regularized risk minimization.

Setting

Let $(\mathcal X, P)$ be a probability space and $X_1, \dots, X_n$ independent random variables with law $P$ . For a function $f : \mathcal X \to \mathbb R$ write

Pf = \mathbb E f(X), \qquad P_n f = \frac1n \sum_{i=1}^n f(X_i).

Let $\sigma_1, \dots, \sigma_n$ be independent signs, $\Pr(\sigma_i = 1) = \Pr(\sigma_i = -1) = 1/2$ . For a class $\mathcal G$ of functions, the empirical Rademacher average is

\mathbb E_\sigma R_n \mathcal G = \frac1n\, \mathbb E_\sigma \sup_{g \in \mathcal G} \sum_{i=1}^n \sigma_i g(X_i),

the expectation over the signs with the sample fixed, and the Rademacher average $\mathbb E R_n \mathcal G$ is its expectation over the sample.

The star-hull of $\mathcal F$ around $0$ is $\operatorname{star}(\mathcal F, 0) = \{\alpha f : f \in \mathcal F,\ \alpha \in [0,1]\}$ . A functional $T$ assigns a number $T(f)$ to each function; it plays the role of a variance proxy (for instance $T(f) = \operatorname{Var}[f]$ or $T(f) = Pf^2$ ).

A function $\psi : [0,\infty) \to [0,\infty)$ is sub-root if it is nondecreasing and $r \mapsto \psi(r)/\sqrt r$ is nonincreasing on $r > 0$ . A nontrivial sub-root function has a unique positive fixed point $r^*$ , the solution of $\psi(r^*) = r^*$ (Lemma 3.2 of the paper).

Formalization targets

Goal: Theorem 3.3, second part (with corrected constants)

Let $\mathcal F$ be a class of functions with values in $[a, b]$ , $B > 0$ , and $T$ a functional with $0 \le T(f)$ , $\operatorname{Var}[f] \le T(f) \le B\, Pf$ and $T(\alpha f) \le \alpha^2 T(f)$ for $f \in \mathcal F$ , $\alpha \in [0,1]$ . Let $\psi$ be sub-root with fixed point $r^*$ and assume, for every $r \ge r^*$ ,

\psi(r) \ge B\, \mathbb E R_n \{ f \in \operatorname{star}(\mathcal F, 0) : T(f) \le r \}.

Then for every $K > 1$ and $x > 0$ , with probability at least $1 - e^{-x}$ ,

\forall f \in \mathcal F \qquad Pf \le \max\Big\{P_n f, \frac{K}{K-1} P_n f\Big\} + \frac{7.04\,K}{B} r^* + \frac{x\,(21(b-a) + 6.4\,BK)}{n},

and, with probability at least $1 - e^{-x}$ ,

\forall f \in \mathcal F \qquad P_n f \le \frac{K+1}{K} Pf + \frac{7.04\,K}{B} r^* + \frac{x\,(21(b-a) + 6.4\,BK)}{n}.

Milestones

Lemma 3.2 (p. 10): a nontrivial sub-root function is continuous on $(0,\infty)$ , has a unique positive fixed point $r^*$ , and $r \ge \psi(r)$ iff $r \ge r^*$ .
Sub-root growth (p. 16): $\psi(\beta r) \le \sqrt{\beta}\,\psi(r)$ for $\beta \ge 1$ and $r \ge 0$ ; at the fixed point it gives $\psi(r) \le \sqrt{r r^*}$ for $r \ge r^*$ .
Containment (p. 17): $\tilde{\mathcal G}_r = \{ r f/(T(f) \vee r) : f \in \mathcal F\} \subset \{ f \in \operatorname{star}(\mathcal F, 0) : T(f) \le r\}$ , and hence $\mathbb E R_n \tilde{\mathcal G}_r \le \psi(r)/B$ .
Theorem 2.1, first part (p. 8): the concentration inequality for $\sup_{f}(Pf - P_n f)$ in terms of $\mathbb E R_n \mathcal F$ , a variance bound and $(b-a)$ ; an existing platform statement.
The largest-root bound (p. 16) for $A\sqrt r + C = r/(\lambda BK)$ ; an existing platform statement.
Lemma 3.8, third and fourth claims (pp. 14–15): from $\sup_{g \in \tilde{\mathcal G}_r}(Pg - P_n g) \le r/(BK)$ to the first bound of the goal, and symmetrically.
Lemma A.3 (p. 34): $\sqrt{u+v} \le \sqrt u + \sqrt v$ and $2\sqrt{uv} \le \alpha u + v/\alpha$ .

Significance

The theorem replaces the global complexity $\sup_r \psi(r)$ that a direct application of Talagrand's inequality would give by the fixed point $r^*$ , which is never larger and is often much smaller. For a class with a Bernstein-type variance condition ( $T(f) = Pf^2 \le B\,Pf$ , as for excess losses of empirical risk minimizers), $r^*$ is of order $d \log n / n$ for VC-type classes and of order of the eigenvalue tail for kernel classes, which yields the fast rates of the paper's Sections 4–6. The second part, formalized here, gives better constants than the first by working with the star-hull of the class, and it is the version the paper's later results (Theorem 4.1 and its corollaries) are built on.

On the formal side, nothing of local Rademacher theory is in Mathlib or, beyond the definitions reused here, on the platform. The concentration inequality used in the proof (Theorem 2.1, from Bousquet's form of Talagrand's inequality) is posed but unproved on the platform. A complete formalization would make the fixed-point machinery available to every fast-rate result built on it. The paper's printed constants for this statement are wrong (see below), so a machine-checked version also settles which constants the argument supports.

Difficulty

The obvious approach applies a concentration inequality directly to $\mathcal F$ and bounds the complexity term by a single Rademacher average; this loses the variance information and gives only $1/\sqrt n$ rates. The localized argument needs a level $r$ that is simultaneously above the fixed point and large enough that the deviation of the rescaled class $\tilde{\mathcal G}_r$ is at most $r/(BK)$ . Converting a bound on the rescaled class back into a bound on $\mathcal F$ requires the multiplicative structure of $T(f) \le B\,Pf$ . The probabilistic core is Talagrand's concentration inequality for suprema of empirical processes with Bousquet's constants, whose proof (entropy method) is the main piece of missing infrastructure. Measurability of the suprema involved is a separate technical obstacle.

Formalization scope

Representation. Functions are X → ℝ on a measurable space with a probability measure P; the sample is s : Fin n → X under the product measure, with n ≥ 1. $P_n f$ is empMean s f, $\mathbb E_\sigma R_n$ is empRademacher (the average over all $2^n$ sign vectors of a real supremum, without absolute value), $\mathbb E R_n$ is expRademacher, and IsSubRoot is Definition 3.1; these are reused published definitions.
Standing assumption. The paper assumes throughout that suprema of empirical processes are measurable (p. 7). This is encoded by taking $\mathcal F$ countable with measurable members. Every expectation of an empirical Rademacher average comes with an integrability hypothesis, so it cannot hold through the junk value $0$ of a non-integrable Bochner integral.
Added hypotheses, implicit on the page: $B > 0$ , $n \ge 1$ , $T \ge 0$ on $\mathcal F$ . The functional $T$ is defined on all real functions; only its values on $\mathcal F$ are constrained. The localization hypothesis is required only for $r \ge r^*$ , as printed.
High-probability statements are two separate bounds on the (outer) product measure of the failure event "some $f \in \mathcal F$ violates the inequality", each at most $e^{-x}$ .
Corrections of the print. The page states the second part with $c_1 = 6$ , $c_2 = 5$ and $11(b-a)$ . Its proof, at the paper's $\alpha = 1/10$ , gives $c_1 = 4(1+\alpha)^2 + 2(1+\alpha) = 7.04$ , $c_2 = 4(1+\alpha) + 2 = 6.4$ and $\tfrac{62}{3}(b-a) \le 21(b-a)$ (the display on p. 16 drops the factor 2 of the term $2C$ ). The first claim's $\frac{K}{K-1}P_n f$ holds only when $P_n f \ge 0$ and is replaced by $\max\{P_n f, \frac{K}{K-1}P_n f\}$ ; Lemma 3.8's third claim is corrected the same way. Lemma 3.2's "continuous on $[0,\infty)$ " becomes $(0,\infty)$ , since $\mathbf 1\{r > 0\}$ is a nontrivial sub-root function discontinuous at $0$ . Part 1 of Theorem 3.3 is not stated.
No trivialization. The goal does not mention the proof's rescaled class, its suprema, or the auxiliary root $r_0$ ; it is stated about $\mathcal F$ , $T$ , $B$ , $\psi$ , $r^*$ , the star-hull, $Pf$ and $P_n f$ only, and a sanity check exhibits an instance satisfying all its hypotheses.
Infrastructure needed and welcome: a proof of the referenced concentration inequality (Bousquet's version of Talagrand's inequality, with symmetrization); monotonicity and measurability lemmas for empRademacher; elementary sub-root calculus. The sub-root lemmas and the containment step are reusable by any later mission on local Rademacher complexities.

Selected references

P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4) (2005) 1497–1537. arXiv:math/0508275, doi:10.1214/009053605000000282
O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, C. R. Math. Acad. Sci. Paris 334 (2002) 495–500. MR1890640
V. Koltchinskii, D. Panchenko, Rademacher processes and bounding the risk of function learning, High Dimensional Probability II, Birkhäuser (2000) 443–459. MR1857339
P. Massart, Some applications of concentration inequalities to statistics, Ann. Fac. Sci. Toulouse Math. (6) 9 (2000) 245–303. MR1813803
G. Lugosi, M. Wegkamp, Complexity regularization via localized random penalties, Annals of Statistics 32 (2004) 1679–1697. MR2089138
V. Koltchinskii, Local Rademacher complexities and oracle inequalities in risk minimization, Annals of Statistics 34(6) (2006) 2593–2656. arXiv:0708.0083

13 thms3 active usersReviewed

Missions

Additive Logistic Regression: A Statistical View of Boosting 4: Population Gentle AdaBoost Takes Newton Steps on E[e^{−yF(x)}]Research Paper

Motivation

Setting

Formalization targets

Goal: Result 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Additive Logistic Regression: A Statistical View of Boosting 3: Population LogitBoost Takes Newton Steps on the Binomial Log-LikelihoodResearch Paper

Motivation

Setting

Formalization targets

Goal: Result 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Weighted Majority Algorithm 4: The Continuous Master WMC Has Total Absolute Loss at Most ln(w_init/w_fin)/(1−β)Research Paper

Motivation

Setting

Formalization targets

Theorem 5.2: WMC total loss

Supporting numbered results

Significance

Difficulty

Formalization scope

Selected references

Learning Models with Uniform Performance via Distributionally Robust Optimization 2: A Minimax Lower Bound of Order n^(−1/2) ∨ n^(−1/k*) for Estimating the Cressie–Read Robust Risk (Theorem 3)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fast Rates for Support Vector Machines Using Gaussian Kernels 1: Under Tsybakov and Geometric Noise, Gaussian-Kernel SVMs Reach Excess Risk Cx²n^{−β+ε} with Probability 1 − e^{−x}Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Empirical Bernstein Bounds and Sample Variance Penalization: Sample Variance Penalization Has Excess Risk at Most √(32V(f*,μ)ln(3M(n)/δ)/n) + 22ln(3M(n)/δ)/(n−1) (Theorem 15)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 15 (p. 6)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 2: Without a Bound on y^NV, Expanding-Projection AIM Has Regret ≤ max{b,h}(T^{δ−1/2} + T^{−1/2} + (y^NV)^{1+2/δ}/T)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7 (p. 11)

Milestones (proof of Theorem 7, p. 12)

Significance

Difficulty

Formalization scope

Selected references

Smart "Predict, then Optimize": Under a Continuous, Centrally Symmetric Cost Law Every Minimizer of the SPO+ Risk Equals E[c|x] and Minimizes the SPO RiskResearch Paper

Motivation

Setting

Formalization targets

Theorem 1: Fisher consistency of SPO+

Supporting propositions

Significance

Difficulty

Formalization scope

Selected references