Machine Learning

Probability Statistics·Captain: mikedeng1

Robust Regression and Lasso 4: ‖b − Ax‖₂ + √n c‖x‖₁ + √n c Equals the Worst Case of √(n·E_μ[(b′ − r′ᵀx)²]) over Box-Constrained Distribution ClassesResearch Paper

Motivation

The Lasso fits a linear model to data $(b, A)$ by penalizing the $\ell_1$ norm of the coefficient vector. Xu, Caramanis and Mannor (arXiv:0811.1790) showed that $\ell_1$ -regularized regression is exactly a robust regression problem: it minimizes the worst-case residual when every feature column may be disturbed within a norm ball. That reading explains Lasso through what it protects against, not through a prior or a sparsity heuristic.

The paper's Section V turns the same identity into a statistical statement. For a fixed coefficient vector $x$ , the robust loss on the training data equals a worst-case expected loss: the largest expected squared prediction error over a class of probability distributions built around the samples. One of these distributions is a kernel density estimator of the data, and from this the authors derive the consistency of Lasso using robustness alone. This mission formalizes that bridge, Corollary 3 of the paper, together with the steps of its proof in Appendix D.

The same authors later generalized the underlying equivalence (Proposition 1 here) to weighted, possibly overlapping uncertainty sets in A distributional interpretation of robust optimization (Math. Oper. Res. 2012).

Setting

There are $n\ge1$ samples and $m$ features. The data are a response vector $b\in\mathbb R^n$ and an observation matrix $A=(a_{ij})\in\mathbb R^{n\times m}$ ; its $i$ -th row $r_i^\top$ is the feature vector of sample $i$ . A coefficient vector is $x\in\mathbb R^m$ , and $c\ge0$ is a fixed budget (the paper writes $c_n$ because its later consistency argument lets it depend on $n$ ). Norms are $\|v\|_2=\sqrt{\sum_i v_i^2}$ and $\|x\|_1=\sum_j|x_j|$ .

A pair $(\sigma,\Delta)$ , with $\sigma\in\mathbb R^n$ and $\Delta=(\delta_{ij})\in\mathbb R^{n\times m}$ with columns $\delta_1,\dots,\delta_m$ , is admissible if $\|\sigma\|_2\le\sqrt n\,c$ and $\|\delta_j\|_2\le\sqrt n\,c$ for every column $j$ . Each admissible pair defines one box per sample,

\mathcal Z_i=[b_i-\sigma_i,\,b_i+\sigma_i]\times\prod_{j=1}^m[a_{ij}-\delta_{ij},\,a_{ij}+\delta_{ij}]\subseteq\mathbb R^{m+1},

a rectangle around the observed pair $(b_i, r_i)$ in the joint response–feature space. The box-constrained class $\mathcal P_n(A,\Delta,b,\sigma)$ is the set of Borel probability measures $\mu$ on $\mathbb R^{m+1}$ such that

\mu\Big(\bigcup_{i\in S}\mathcal Z_i\Big)\ge\frac{|S|}{n}\qquad\text{for every }S\subseteq\{1,\dots,n\}.

The empirical distribution of the samples belongs to it, and so does any distribution that spreads the mass $1/n$ of each sample over its box. Finally $\hat{\mathcal P}(n)$ is the union of these classes over all admissible $(\sigma,\Delta)$ .

Formalization targets

Goal: Corollary 3, Eq. (8)

\|b-Ax\|_2+\sqrt n\,c\,\|x\|_1+\sqrt n\,c=\sup_{\mu\in\hat{\mathcal P}(n)}\sqrt{\,n\int_{\mathbb R^{m+1}}(b'-r'^\top x)^2\,d\mu(r',b')\,}\qquad\text{for every }x\in\mathbb R^m.

The equation holds for every data set: there is no assumption on how $(b,A)$ was generated (Remark 1 of the paper).

Milestones (Appendix D)

The robust identity with the response perturbed (first display): the worst case of $\|b+\sigma-(A+\Delta)x\|_2$ over admissible $(\sigma,\Delta)$ is attained and equals the left-hand side of (8).
The box decomposition (second and third displays): that worst case equals

\sup_{(\sigma,\Delta)}\ \sup_{(\hat b_i,\hat r_i)\in\mathcal Z_i}\sqrt{\textstyle\sum_i(\hat b_i-\hat r_i^\top x)^2}=\sup_{(\sigma,\Delta)}\sqrt{\textstyle\sum_i\sup_{\mathcal Z_i}(\hat b_i-\hat r_i^\top x)^2}.

The remaining step of the proof applies Proposition 1 of the paper: for Borel sets $\mathcal Z_1,\dots,\mathcal Z_n$ , $\frac1n\sum_i\sup_{\mathcal Z_i}h=\sup_{\mu\in\mathcal P_n}\int h\,d\mu$ . Its general weighted form is already posed on the platform as DistInterpRO.Equivalence.theorem_2_1 (inf form, weights $c_i>0$ summing to one; take $c_i=1/n$ and $f=-h$ ), and the one-set case (Lemma 2) as DistInterpRO.Equivalence.corollary_2_1. They are credited here and not posed again.

Significance

The result. Corollary 3 gives Lasso a distributional reading: minimizing $\|b-Ax\|_2+\sqrt n\,c\,\|x\|_1$ is, up to the additive constant $\sqrt n\,c$ , minimizing the worst-case root mean squared error over all distributions that stay, sample by sample, inside boxes of controlled size around the data. Because a box kernel density estimator lies in $\hat{\mathcal P}(n)$ , the paper's Theorem 7 derives the consistency of Lasso from this identity when $c_n\to0$ suitably. Without the corollary that argument has no starting point.

Formalizing it. The result is proved in the paper but has no machine-checked proof. A formal development yields three reusable pieces: the robust-regression identity with a perturbed response, the decomposition of a worst case over a product of boxes into per-sample worst cases, and the finite-dimensional instance of Proposition 1 with uniform weights. Together they are the deterministic half of a formal consistency proof for Lasso.

Difficulty

The left-hand side of (8) is a worst case over perturbations of the data; the right-hand side is a worst case over probability measures. Bounding the right-hand side above requires controlling $\int h\,d\mu$ for every $\mu$ in the class, and the constraint on $\mu$ is not that each box receives mass $1/n$ : the boxes may overlap, and a measure may concentrate mass on intersections. The natural argument of moving each sample's mass to the worst point of its box therefore does not apply to a general member of the class. A second, smaller difficulty is the order of the suprema: $\hat{\mathcal P}(n)$ is a union over $(\sigma,\Delta)$ , and the square root must be exchanged with a supremum over measures.

Formalization scope

$\mathbb R^{m+1}$ is Fin (m+1) → ℝ with its product (= Borel) σ-algebra, response first: $z_0=b'$ , $z_{j+1}=r'_j$ . This matches the boxes; the paper's $d\mu(r',b')$ ordering is notation only. $A$ is a Matrix (Fin n) (Fin m) ℝ, indices are Fin n, Fin m.
Readings of sup, max and the integral. The supremum in (8) is taken in $[0,\infty]$ and stated as a least upper bound (IsLUB), with no claim that it is attained. The integral is the Lebesgue integral of the nonnegative integrand with values in $[0,\infty]$ , never a Bochner integral. The "max" of the first display is an attained maximum (IsGreatest). The equalities of suprema in the second and third displays are stated as "the same real number is the least upper bound of each set". The inner supremum over a nonempty compact box is encoded as the greatest value of the loss on it.
Standing hypotheses. $n\ge1$ and $c\ge0$ are implicit on the page and are explicit here. $c$ is one constant, not a sequence. $\sigma$ and $\Delta$ carry no sign condition, as printed. A negative entry makes some box empty, and then $\mathcal P_n(A,\Delta,b,\sigma)$ is empty, so such pairs contribute nothing.
Ruled out. Neither side of (8) is defined by the other's closed form. No real sSup with a junk value $0$ and no Bochner integral that could silently vanish appear in any statement. The class keeps the constraint for every $S$ , including $S=\{1,\dots,n\}$ , which forces each measure onto $\bigcup_i\mathcal Z_i$ ; dropping it would make the supremum infinite.
Infrastructure. The development needs empirical (finite Dirac) measures, and the Lebesgue integral of bounded functions on compact sets. Proposition 1 in the generality of DistInterpRO.Equivalence.theorem_2_1 is reusable well beyond this mission. Proofs of either milestone, of the uniform-weight Proposition 1 for boxes, and of the goal are all welcome.

Selected references

H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Transactions on Information Theory 56(7), 2010. https://arxiv.org/abs/0811.1790 , https://doi.org/10.1109/TIT.2010.2048503
H. Xu, C. Caramanis, S. Mannor, A distributional interpretation of robust optimization, Mathematics of Operations Research 37(1), 2012. https://doi.org/10.1287/moor.1110.0531
R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1), 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
L. Devroye, L. Györfi, Nonparametric Density Estimation: The L1 View, Wiley, 1985.

4 thms2 active usersReviewed

Completed

Optimization Statistics·Captain: mikedeng1

Robust Regression and Lasso 1: Under Feature-Wise Norm-Bounded Column Disturbances, Worst-Case Least-Norm Regression Is Exactly ℓ1-Regularized Regression ‖b − Ax‖₂ + Σ cᵢ|xᵢ|Research Paper

Why robustness and the Lasso belong together

The Lasso (Tibshirani 1996; Chen, Donoho and Saunders 1998) fits a linear model $b \approx Ax$ by penalizing the ℓ¹ norm of the coefficients. It is one of the standard tools of high-dimensional statistics and signal processing, and its usual justification is statistical or geometric: the ℓ¹ penalty is a convex surrogate for sparsity, or the negative log-density of a Laplace prior. Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) give a different justification: an ℓ¹-regularized regression is exactly a robust regression, the problem of fitting the data well in the worst case when every feature of the observation matrix may be corrupted by a bounded disturbance.

This observation is the foundation of the rest of their paper (dual-norm regularizers from coupled disturbances, sparsity from robustness, consistency of the Lasso through a worst-case-expectation reading). It also connects two literatures. On the robust side, El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) computed the worst-case residual when the whole data matrix $[A\ b]$ is disturbed in a Frobenius-norm ball, obtaining $\|Ax-b\|+\sqrt{\|x\|^2+1}$ ; that result is already on the platform as RobustLS.Unstructured.worst_case_residual_closed_form. On the distributional side, Blanchet, Kang and Murthy (J. Appl. Probab. 56(3), 2019) obtained the square-root Lasso as a Wasserstein distributionally robust problem (RWPI.SqrtLasso.theorem_1). The present mission formalizes the feature-wise result that sits between them.

Setting

Fix integers $n$ (samples) and $m$ (features). The observation matrix $A\in\mathbb R^{n\times m}$ has columns $a_1,\dots,a_m\in\mathbb R^n$ , the features. The response is $b\in\mathbb R^n$ and a coefficient vector is $x\in\mathbb R^m$ , so that $Ax=\sum_{i=1}^m x_i a_i$ . All norms on $\mathbb R^n$ are Euclidean, $\|\cdot\|_2$ .

A disturbance of $A$ is a family $\Delta A=(\delta_1,\dots,\delta_m)$ of vectors $\delta_i\in\mathbb R^n$ , one per column; the disturbed matrix $A+\Delta A$ has columns $a_i+\delta_i$ . Given budgets $c_1,\dots,c_m\ge 0$ , the feature-wise uncoupled uncertainty set is

\mathcal U=\bigl\{(\delta_1,\dots,\delta_m)\;\big|\;\|\delta_i\|_2\le c_i,\ i=1,\dots,m\bigr\}. \tag{2}

Each feature is disturbed independently: no constraint couples the $\delta_i$ . The robust objective is the worst-case residual

R(x)=\sup_{\Delta A\in\mathcal U}\|b-(A+\Delta A)x\|_2,

and robust linear regression is problem (1), $\min_{x\in\mathbb R^m} R(x)$ . The ℓ¹-regularized regression problem is (3), $\min_{x\in\mathbb R^m} L(x)$ with

L(x)=\|b-Ax\|_2+\sum_{i=1}^m c_i|x_i| .

The loss in $L$ is the norm of the residual, not its square. In the Lean development, $Ax$ is matVec a x, $\mathcal U$ is uncertaintySet c, $R$ is robustObjective a b c, $L$ is l1RegularizedObjective a b c, and the disturbance $\delta_i^*=-c_i\,\mathrm{sgn}(x_i)\,u$ of the proof is worstCaseDisturbance c x u.

Formalization targets

Goal: Theorem 1 (p. 4)

For $n\ge1$ and budgets $c_i\ge 0$ , problem (1) with uncertainty set (2) is equivalent to problem (3): for every $x\in\mathbb R^m$ ,

x\ \text{minimizes}\ R\iff x\ \text{minimizes}\ L,\qquad\text{and}\qquad \inf_{x} R(x)=\inf_x L(x).

No minimizer is asserted to exist; the paper does not claim one.

Milestones (in the order the proof uses them)

Eq. (4), the upper bound: for every $\Delta A\in\mathcal U$ , $\|b-(A+\Delta A)x\|_2\le\|b-Ax\|_2+\sum_i|x_i|c_i$ .
Eq. (5), the attained worst case: with $u$ a unit vector equal to $(b-Ax)/\|b-Ax\|_2$ when $Ax\ne b$ , the disturbance $\delta_i^*=-c_i\,\mathrm{sgn}(x_i)\,u$ lies in $\mathcal U$ and

\|b-(A+\Delta A^*)x\|_2=\|b-Ax\|_2+\sum_i c_i|x_i| .

The per- $x$ identity stated at the start of the proof: for every $x$ ,

\max_{\Delta A\in\mathcal U}\|b-(A+\Delta A)x\|_2=\|b-Ax\|_2+\sum_{i=1}^m c_i|x_i|,

with the maximum attained.

Significance

The result. Theorem 1 turns a min–max problem whose inner maximization is nonconvex into a single convex, second-order-cone-representable problem, and it gives the regularization weights a concrete meaning: $c_i$ is the size of the disturbance feature $i$ is protected against. With equal budgets $c_i=c$ it recovers the Lasso with the unsquared loss, which coincides with the usual Lasso up to a data-dependent change of the regularization coefficient. Every later result of the paper (Theorem 3 for arbitrary norms, the coupled uncertainty sets of Corollary 1, the sparsity theorems of §IV, the kernel-density reading of §V) builds on this identity or its proof pattern.

Formalizing it. The theorem is proved in the paper; the mission formalizes that proof. No machine-checked version of it exists on the platform or, to our knowledge, elsewhere. The definitions here (the uncertainty set, the worst-case objective as a genuine supremum, the explicit worst-case disturbance) are the base on which the companion missions of this series (coupled norms, sparsity, worst-case expectation) restate their own objects.

Difficulty

The upper bound (4) is the triangle inequality. The substance is the lower bound: one must exhibit a single admissible disturbance that makes every column perturbation push the residual in the same direction, and check that it is admissible and that the resulting norm adds up exactly. Two edge cases make the obvious argument fail as written. When $Ax=b$ the direction $(b-Ax)/\|b-Ax\|_2$ is undefined and an arbitrary unit vector must be used instead, which requires $n\ge1$ ; for $n=0$ the identity reads $0=\sum_i c_i|x_i|$ and is false. When $x_i=0$ the sign must be $0$ , not $\pm1$ , for the computation in (5) to go through. Passing from the per- $x$ identity to the equivalence of the two minimization problems is then routine, but it must be done without assuming that either problem has a minimizer.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $A$ is the family of its columns a : Fin m → EuclideanSpace ℝ (Fin n), and $Ax=\sum_i x_i\,a_i$ . Indices $1,\dots,m$ are Fin m. A disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n), and $(A+\Delta A)x$ is matVec (a + δ) x.
Readings of "max" and "min". The paper writes "max" over $\mathcal U$ . $R(x)$ is defined as the supremum over $\mathcal U$ taken in EReal, so it is $-\infty$ on an empty set and $+\infty$ on an unbounded one and carries no junk value. That the maximum is attained is stated separately, as IsGreatest of the set of residual norms (milestone 3). "min" in (1) and (3) is read as: the same set of minimizers (IsMinOn … Set.univ) and the same infimum, computed in EReal. No existence of minimizers is claimed.
Added hypothesis. $n\ge1$ (0 < n), which the paper leaves implicit. The budgets $c_i\ge0$ are the paper's own assumption on (2).
Sign convention. $\mathrm{sgn}$ is Real.sign, with $\mathrm{sgn}(0)=0$ .
Trivializing formalizations ruled out. The robust objective is defined as the supremum over $\mathcal U$ , never by its closed form $\|b-Ax\|_2+\sum_i c_i|x_i|$ , which would make milestone 3 and the goal hold by definition; and no real sSup with junk value $0$ is used, so the identities cannot hold vacuously.
Not in scope. The remark that (3) "recovers the well-known Lasso" (it has the unsquared loss), §II-B and Theorem 2 (probabilistic construction of the budgets), and the other sections of the paper, which are separate missions.
Infrastructure. Only Mathlib's inner-product-space and EReal order theory are needed. The squared-loss Lasso definitions already on the platform (XuMannorRobust.Lasso.*, LassoDantzig.*) are different objects and are not used. Contributions are welcome on each milestone independently; a proof of the per- $x$ identity for an arbitrary norm on $\mathbb R^n$ would also serve Theorem 3 of the paper.

Selected references

H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7):3561–3574, 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1):267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
S. S. Chen, D. L. Donoho, M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1):33–61, 1998. https://doi.org/10.1137/S1064827596304010
L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein profile inference and applications to machine learning, J. Appl. Probab. 56(3):830–857, 2019. https://doi.org/10.1017/jpr.2019.49

5 thms2 active usersReviewed

Completed

Dynamic Programming Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning II: The Gradient of the Normalized Discounted Value Is the Sum over Actions of ∇π·Q under the Discounted Future State DistributionTextbook

Why the gradient of the value matters

Policy gradient methods search a parameterized family of stochastic policies $\pi(a\mid s,\theta)$ , $\theta\in\mathbb R^k$ , by following the gradient of the policy's performance. They are the standard tool when the state space is too large for tabular dynamic programming and when a compact policy class (a neural network, a linear softmax) is easier to represent than a value function. Every such method rests on one identity: a formula for the gradient of the value with respect to $\theta$ that involves only quantities of the current policy, so that it can be estimated from the policy's own trajectories.

Chapter 4 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), states this identity in two settings, the $T$ -epoch undiscounted setting and the $\gamma$ -discounted setting, both in the thesis's normalized convention, in which values lie in $[0,1]$ . The thesis then uses the formula to analyse how many samples a gradient estimate needs (§4.2.3), and in §5.4.2 rewrites it in terms of advantages to explain why gradient methods can stall far from optimal: the gradient weights advantages by the current policy's state distribution, not by the distribution of an optimal policy.

Timeline:

1992: R. J. Williams introduces the likelihood-ratio (REINFORCE) estimator for episodic tasks.
2000: Sutton, McAllester, Singh and Mansour state the policy gradient theorem with function approximation, for discounted and average-reward criteria (NeurIPS 1999 proceedings, 2000); Konda and Tsitsiklis give actor-critic counterparts.
2001: Baxter and Bartlett analyse biased gradient estimation in the infinite-horizon setting.
2003: Kakade's thesis restates both theorems for normalized values, introduces the future state-time distribution $d_{\pi,s_0}$ for non-stationary $T$ -epoch policies, and draws the "mismeasure" consequence.

Setting

A finite MDP has a finite state set $S$ , a finite nonempty action set $A$ , a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ .

$T$ -epoch case. Epochs are $t\in\{0,\dots,T-1\}$ , $T\ge1$ . A non-stationary policy chooses $a$ at epoch $t$ in state $s$ with probability $\pi(a\mid s,t)$ . Starting from $s_0$ , $\Pr(s_t=s\mid\pi,s_0)$ is the probability of being in $s$ at epoch $t$ . The normalized $t$ -value is

V_{\pi,t}(s)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\,\Big|\,\pi,s_t=s\Big],\qquad V_\pi=V_{\pi,0},

the $t$ state-action value is $Q_{\pi,t}(s,a)=\frac1T r(s,a)+\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_{\pi,t+1}(s')]$ with $V_{\pi,T}=0$ , and the future state-time distribution on $S\times\{0,\dots,T-1\}$ is $d_{\pi,s_0}(s,t)=\frac1T\Pr(s_t=s\mid\pi,s_0)$ .

Discounted case. For a stationary policy $\pi(a\mid s)$ and $0\le\gamma<1$ , the normalized value, state-action value, advantage and discounted future state distribution are

V_{\pi,\gamma}(s)=(1-\gamma)\,\mathbb E\Big[\sum_{\tau\ge0}\gamma^\tau r(s_\tau,a_\tau)\,\Big|\,\pi,s_0=s\Big],\qquad Q_{\pi,\gamma}(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[V_{\pi,\gamma}(s')],

A_\pi(s,a)=Q_{\pi,\gamma}(s,a)-V_{\pi,\gamma}(s),\qquad d_{\pi,s_0,\gamma}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,s_0).

A parameterized policy is a family $\pi(a\mid s,\theta)$ (resp. $\pi(a\mid s,t,\theta)$ ) of policies indexed by $\theta\in\mathbb R^k$ , each entry differentiable in $\theta$ ; $\nabla$ is the gradient in $\theta$ .

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

\nabla V_{\pi,\gamma}(s_0)=\frac1{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\Big[\sum_a\nabla\pi(a\mid s,\theta)\,Q_{\pi,\gamma}(s,a)\Big].

The statement asserts that $\theta\mapsto V_{\pi_\theta,\gamma}(s_0)$ is differentiable at the given parameter and that its derivative is the right-hand side. It is the thesis's version of the Sutton–McAllester–Singh–Mansour theorem, and the result the rest of the thesis's discussion of gradient methods builds on.

Milestones

Value representations (p. 47): $V_\pi(s_0)=\mathbb E_{(s,t)\sim d_{\pi,s_0}}\mathbb E_{a\sim\pi(\cdot\mid s,t)}[r(s,a)]$ and $V_{\pi,\gamma}(s_0)=\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\mathbb E_{a\sim\pi(\cdot\mid s)}[r(s,a)]$ .
Theorem 4.2.3 (p. 48), the $T$ -epoch gradient:

\nabla V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi,s_0}}\Big[\sum_a\nabla\pi(a\mid s,t,\theta)\,Q_{\pi,t}(s,a)\Big].

The advantage form (§5.4.2, p. 66), with $A=|A|$ the number of actions:

\nabla V_\pi(s_0)=\frac{A}{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0}}\,\mathbb E_{a\sim\mathrm{Uniform}}\big[A_\pi(s,a)\,\nabla\pi(a\mid s,\theta)\big].

Significance

The result. The gradient formula contains no derivative of the state distribution: the effect of $\theta$ on which states are visited cancels, and the gradient is an expectation over states drawn from the current policy, weighted by a sum over actions. This is what makes Monte Carlo and actor-critic estimators possible, and it is the reason the thesis's sample-size analysis of §4.2.3 has no dependence on the size of the state space. The advantage form makes the limitation equally explicit: a small gradient certifies small advantages only under $d_{\pi,s_0}$ , while the performance difference lemma (Lemma 5.2.1) shows that closeness to optimal is governed by advantages under $d_{\pi^*,s_0}$ . That gap motivates the conservative policy iteration of Chapter 7.

Formalizing it. The theorems are proved in the thesis and in the cited literature; none of them is machine-checked in this normalized convention. The platform has a proved finite-horizon policy gradient theorem for a scalar parameter, a stationary policy and unnormalized values (policy_gradient_discounted_finite, policy_gradient_finite_horizon), and a posed direct-parameterization gradient for Agarwal et al.'s unnormalized discounted value (PolicyGradTheory.ProjGA.direct_gradient). This mission adds the multi-parameter statements, the non-stationary $T$ -epoch version with its state-time distribution, and the infinite-horizon discounted version, where differentiability of an infinite series must be established rather than computed from a finite recursion.

Difficulty

In the $T$ -epoch case the value is a finite polynomial in the policy entries, and the work is bookkeeping: unrolling the backward recursion for $V_{\pi,t}$ against the forward recursion for $\Pr(s_t=\cdot)$ so that the terms involving $\nabla V_{\pi,t+1}$ telescope. In the discounted case the obvious route, differentiating the recursion $V=(1-\gamma)r_\pi+\gamma P_\pi V$ term by term and recursing forever, presupposes that $\theta\mapsto V_{\pi_\theta,\gamma}(s)$ is differentiable, which the thesis's proof takes for granted. The value is an infinite series in $t$ , so that differentiability is a genuine part of the claim, and the resulting formula must be matched with $d_{\pi,s_0,\gamma}$ and $Q_{\pi,\gamma}$ , which are themselves defined as infinite series.

Formalization scope

Finite $S$ and $A$ (Fintype), $A$ nonempty; transition kernel IsTransitionKernel P; rewards in $[0,1]$ as a standing hypothesis of every statement; $0\le\gamma<1$ ; $T\ge1$ . The thesis's later chapters allow infinite state spaces; this mission is finite.
Normalization exactly as in the thesis: $T$ -epoch values and $d_{\pi,s_0}$ carry $1/T$ , discounted values and $d_{\pi,s_0,\gamma}$ carry $1-\gamma$ . Hence the factors $T$ and $1/(1-\gamma)$ in the gradient formulas.
The discounted layer is the published normalized model ApproxOptRL.Shared.Model (value, qValue, advantage, futureStateDist; $d_{\pi,s_0,\gamma}$ is futureStateDist at the point mass on $s_0$ ). The $T$ -epoch layer is defined in this mission (TEpoch): 0-based epochs, tValue by backward recursion, tQValue, stateDist, stateTimeDist.
Parameters live in EuclideanSpace ℝ (Fin k). Every statement assumes that $\pi(\cdot\mid s,\theta)$ (resp. $\pi(\cdot\mid s,t,\theta)$ for $t<T$ ) is a probability distribution for every $\theta$ , and that each entry is differentiable at the parameter $\theta_0$ ("the derivatives $\nabla\pi$ exist", p. 48). Differentiability of the value is not assumed.
Gradients are stated with HasFDerivAt: the value map has the right-hand side as its Fréchet derivative at $\theta_0$ . A statement with fderiv of the value alone, or with a policy that does not depend on $\theta$ , would reduce to $0=0$ and is ruled out.
Expectations over finite sets are finite sums; the uniform expectation over actions is $\frac1{|A|}\sum_a$ .
Contributions welcome: the forward/backward recursion identity for $T$ -epoch values, summability and differentiability of the discounted series, and the closed form of $V_{\pi,\gamma}$ via $(I-\gamma P_\pi)^{-1}$ ; all are reusable by the other missions of this series.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 229–256, 1992. https://doi.org/10.1007/BF00992696
J. Baxter, P. L. Bartlett, Infinite-Horizon Policy-Gradient Estimation, Journal of Artificial Intelligence Research 15, 319–350, 2001. https://doi.org/10.1613/jair.806
V. R. Konda, J. N. Tsitsiklis, Actor-Critic Algorithms, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/6449f44a102fde848669bdd9eb6b76fa-Abstract.html

9 thms2 active usersReviewed

Completed

Dynamic Programming Optimization Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning I: Approximate Policy Iteration with Max-Norm Evaluation Error ε Is Eventually Within 2ε/(1−γ)² of OptimalTextbook

Motivation

Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.

Setting

A finite discounted Markov decision process consists of a finite set of states $S$ , a finite nonempty set of actions $A$ , a transition kernel $P(s'\mid s,a)$ (for every $(s,a)$ a probability distribution over $S$ ), a deterministic reward $r(s,a)\in[0,1]$ , and a discount factor $0\le\gamma<1$ . A policy $\pi(a\mid s)$ is a probability distribution over actions for every state; a deterministic policy is a map $f:S\to A$ , identified with the policy that plays $f(s)$ with probability one.

Values are normalized: the value of $\pi$ at $s$ is

V_\pi(s)=(1-\gamma)\,\mathbb E\Big[\sum_{t\ge0}\gamma^t r(s_t,a_t)\,\Big|\,\pi,\ s_0=s\Big],

and the state-action value is $Q_\pi(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_\pi(s')]$ . With rewards in $[0,1]$ , every value lies in $[0,1]$ . An optimal policy $\pi^*$ has $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and state $s$ ; write $V^*=V_{\pi^*}$ and $Q^*=Q_{\pi^*}$ . The max norm is $\|x\|_\infty=\max_s|x(s)|$ on state vectors and $\max_{s,a}|x(s,a)|$ on state-action arrays.

The backup operator is $[BJ](s)=\max_a\big((1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[J(s')]\big)$ . A deterministic policy $f$ is greedy with respect to $Q$ if $f(s)\in\arg\max_a Q(s,a)$ for every $s$ .

$\gamma$ -approximate value iteration produces vectors $J_0=0,J_1,J_2,\dots$ with $\|J_t-BJ_{t-1}\|_\infty\le\varepsilon$ , and greedy policies $\pi_t$ for the lookahead $(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[J_t(s')]$ .
$\gamma$ -approximate policy iteration starts from any deterministic $\pi_0$ , forms an estimate $\tilde Q_t$ of $Q_{\pi_t}$ with $\|\tilde Q_t-Q_{\pi_t}\|_\infty\le\varepsilon$ , and takes $\pi_{t+1}$ greedy with respect to $\tilde Q_t$ .

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

\limsup_{t\to\infty}\|V^*-V_{\pi_t}\|_\infty\le\frac{2\varepsilon}{(1-\gamma)^2}.

The policies need not converge; the statement bounds where they end up.

Milestones

Theorem 3.1.1: if $\|\tilde Q-Q^*\|_\infty\le\varepsilon$ and $\pi$ is greedy for $\tilde Q$ , then $V_\pi(s)\ge V^*(s)-\frac{2\varepsilon}{1-\gamma}$ for all $s$ .
Lemma 3.2.3: $\|V^*-V_{\pi_{t+1}}\|_\infty\le\gamma\|V^*-V_{\pi_t}\|_\infty+\frac{2\varepsilon}{1-\gamma}$ .
Rate of approximate policy iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\gamma^t+\frac{2\varepsilon}{(1-\gamma)^2}$ .
Contraction of the backup (p. 26): $\|BJ-BJ'\|_\infty\le\gamma\|J-J'\|_\infty$ .
Approximate value iteration (p. 40): $\|V^*-J_t\|_\infty\le\gamma^t+\frac{\varepsilon}{1-\gamma}$ .
Rate of approximate value iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\frac{2\gamma^t}{1-\gamma}+\frac{2\varepsilon}{(1-\gamma)^2}$ .
Theorem 3.2.1: the same lim sup bound $\frac{2\varepsilon}{(1-\gamma)^2}$ for approximate value iteration.

Significance

The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of $\varepsilon$ in max norm costs at most $2\varepsilon/(1-\gamma)^2$ in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor $2\varepsilon/(1-\gamma)$ of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon $1/(1-\gamma)$ in the limit bound are the reason the thesis turns to other error measures in later chapters.

All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor $\gamma$ to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.

Difficulty

Approximate policy iteration is not monotone: with evaluation errors, $V_{\pi_{t+1}}$ can be worse than $V_{\pi_t}$ at some states, so the argument of exact policy iteration, which uses $V_{\pi_{t+1}}\ge V_{\pi_t}$ everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value $V_\pi$ is defined as an infinite series, so its Bellman equation $V_\pi(s)=Q_\pi(s,\pi(s))$ , the optimality equation $V^*=BV^*$ and the bound $0\le V_\pi\le1$ have to be derived from that definition before any of the recursions can be run.

Formalization scope

The model is the published normalized model ApproxOptRL.Shared.Model: value P r γ π is $V_\pi$ (defined as $(1-\gamma)$ times a tsum), qValue is $Q_\pi$ . $S$ and $A$ are finite types, $A$ nonempty; $P$ satisfies IsTransitionKernel; every statement assumes $0\le r\le1$ and $0\le\gamma<1$ .
The optimal policy is a binder $\pi^*$ with IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.
Policies of the runs are deterministic, S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.
The runs are sequences indexed by ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices $t+1$ and $t$ .
$\|\cdot\|_\infty$ is Mathlib's sup norm on S → ℝ and S → A → ℝ.
The lim sup statements are in $\varepsilon$ – $N$ form: for every $\delta>0$ the bound plus $\delta$ holds eventually.
Ruled out: the accuracy hypothesis is stated against $Q_{\pi_t}$ , the value of the current policy, not against $Q^*$ , and the greedy relation genuinely constrains $\pi_{t+1}$ ; with either changed, the hypotheses would be unsatisfiable or the policies unconstrained and the theorem empty.
Infrastructure needed and reusable beyond this mission: the Bellman equation of the normalized value for indicator policies, $V^*=BV^*$ , monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound $0\le V_\pi\le1$ . Contributions of these lemmas are welcome.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996. ISBN 1-886529-10-8.
S. P. Singh and R. C. Yee, An upper bound on the loss from approximate optimal-value functions, Machine Learning 16 (1994), 227–233. https://doi.org/10.1007/BF00993104
S. M. Kakade and J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005

13 thms2 active usersReviewed

Dynamic Programming Optimization Reinforcement Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

Motivation

Policy iteration replaces the current policy by the greedy policy with respect to its state-action values. With exact values this improves the policy at every state. When the improvement step is only approximate, or is restricted to a class of policies, a greedy replacement can make the policy worse, and the resulting error bounds are stated in max norm over all states, a quantity that sampling cannot control in large state spaces.

Conservative policy iteration (CPI), introduced by Kakade and Langford (ICML 2002) and developed in Chapter 7 of Kakade's PhD thesis (UCL, 2003), takes a different route. Instead of switching to a new policy, it mixes the current policy with a small amount of a better one, and it measures progress by an average over states visited under the current policy rather than by a maximum over all states. The thesis proves that the exact form of the algorithm improves its objective at every step, halts after a number of updates polynomial in the horizon and the accuracy, and returns a policy whose average advantages against an entire policy class are small. The approach underlies later trust-region and conservative update methods in reinforcement learning.

Setting

A finite Markov decision process has a finite state set $S$ , a finite action set $A$ , transition probabilities $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ . A stationary policy $\pi$ chooses action $a$ in state $s$ with probability $\pi(a\mid s)$ . For a discount factor $0\le\gamma<1$ the normalized value of $\pi$ is

V_\pi(s)=(1-\gamma)\,\mathbb E\Big[\sum_{t\ge0}\gamma^t r(s_t,a_t)\,\Big|\,\pi,\ s_0=s\Big],

which lies in $[0,1]$ . The state-action value is $Q_\pi(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$ . The horizon time is $H=1/(1-\gamma)$ .

Fix a reset distribution $\mu$ on $S$ . The value of $\mu$ is $V_\pi(\mu)=\mathbb E_{s\sim\mu}V_\pi(s)$ . The discounted future state distribution is

d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,\ s_0\sim\mu),

and $d_{\pi,s_0}$ is the case where $\mu$ is the point mass at $s_0$ . For another policy $h$ :

the advantage under a distribution $\nu$ is $A_\pi(\nu,h)=\mathbb E_{s\sim\nu}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$ ;
the future state-action value is $\mathbb Q_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}Q_\pi(s,a)$ ;
the future advantage is $\mathbb A_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$ .

The conservative update with mixing weight $\alpha\in[0,1]$ is $\pi_{\rm new}=(1-\alpha)\pi+\alpha\pi'$ .

Exact CPI (Algorithm 11) works with a class $\Pi$ of stationary policies and an accuracy $\varepsilon>0$ . Starting from any stationary policy, it repeats three steps:

The ExactPolicyChooser returns $\pi'\in\arg\max_{h\in\Pi}\mathbb Q_\pi(\mu,h)$ .
If $\mathbb A_\pi(\mu,\pi')>\varepsilon/H$ , the algorithm sets $\alpha=\mathbb A_\pi(\mu,\pi')/(4H)$ and replaces $\pi$ by $(1-\alpha)\pi+\alpha\pi'$ .
Otherwise it halts and returns $\pi$ .

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

Every run $\pi_0,\pi_1,\dots$ of Exact CPI has a halting round $K$ with

K<\frac{8H^2}{\varepsilon^2},\qquad V_{\pi_{k+1}}(\mu)-V_{\pi_k}(\mu)>\frac{\varepsilon^2}{8H^2}\ \ (k<K),\qquad \mathbb A_{\pi_K}(\mu,h)\le\frac{\varepsilon}{H}\ \ (h\in\Pi).

The returned $\pi_K$ is a stationary policy. The thesis states the halting bound as $O(H^2/\varepsilon^2)$ calls to the chooser. The constant $8$ is the one the thesis's own Corollary 7.2.3 supplies, and the mission states it explicitly.

Milestones

Lemma 7.2.2. For every $\alpha\in[0,1]$ , with $\epsilon_\infty=\max_s|\mathbb E_{a\sim\pi'(\cdot\mid s)}A_\pi(s,a)|$ ,

V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A_\pi(\mu,\pi')-\frac{2\gamma\alpha}{1-\gamma(1-\alpha)}\epsilon_\infty\Big).

Corollary 7.2.3. If $\mathbb A_\pi(\mu,\pi')\ge0$ , the step $\alpha=\frac{1-\gamma}{4}\mathbb A_\pi(\mu,\pi')$ gives $V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\mathbb A_\pi(\mu,\pi')^2/8$ .
Domination of the start distribution (p. 88): $d_{\pi,\mu}\ge\mu/H$ .
Lemma 5.2.1, discounted half: $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\mid s)}A_\pi(s,a)$ .
Theorem 7.3.1. If $A_\pi(\nu,h)\le\varepsilon/H$ for all $h\in\Pi$ , then for every $\pi'\in\Pi$ and every state $s_0$ ,

V_\pi(s_0)\ge V_{\pi'}(s_0)-\varepsilon-H\|d_{\pi',s_0}-\nu\|_1.

Example 7.4.1. A two-state MDP on which the bound of Lemma 7.2.2 holds with equality for all $\alpha$ and $\gamma$ .

Milestones 1, 2 and 4 are already stated on the platform from Kakade–Langford (2002), in the same normalized model. They are included here as references and are not posed again.

Significance

The result. Theorem 7.3.2 is the exact-oracle core of CPI's sample-complexity analysis: the sample-based version later in the chapter replaces the exact chooser and the exact future advantage by estimates. The guarantee is stated through future advantages, so it does not depend on a max-norm accuracy over all states. Through Theorem 7.3.1 it translates into a value guarantee against every policy of the class whose future state distribution is close to the measure the algorithm was trained on. The output need not lie in $\Pi$ : even for a deterministic class the returned policy is in general stochastic.

Formalizing it. All results here are proved in the thesis, and the three referenced statements are proved on the platform. None of the new statements has a machine-checked proof. The mission adds a fully specified Exact CPI run as a Lean object, an explicit constant in place of the $O(\cdot)$ , and checked versions of the μ-optimality bound and of the tightness example. Its layer is shared with the Kakade–Langford missions, so later work on sample-based CPI can build on it directly.

Difficulty

The halting bound needs two ingredients that are easy to separate and easy to get wrong. The improvement guarantee of Corollary 7.2.3 holds only for a policy and a mixture weight in $[0,1]$ , so every iterate of the run must be shown to remain a policy and every step size to stay in range. The count of updates then rests on the normalized values being bounded in $[0,1]$ , a property of the model rather than of the algorithm. The output condition is stated for every $h\in\Pi$ , while the algorithm only tests the one policy the chooser returned, and the chooser maximizes future state-action values rather than future advantages.

A tempting shortcut is the thesis's remark on p. 88 that $\mathbb A_\pi(\mu,h)\le\varepsilon/H$ implies $A_\pi(\mu,h)\le\varepsilon$ . This is false in general: it would need $\mathbb E_{a\sim h}A_\pi(s,a)\ge0$ at every state. The mission formalizes only the true ingredient, $d_{\pi,\mu}\ge\mu/H$ .

Formalization scope

The layer is the published normalized model ApproxOptRL.Shared.Model: value, qValue, advantage, futureStateDist, and eta for $V_\pi(\mu)$ . The future advantage is ApproxOptRL.CPI.policyAdvantage and the conservative update is ApproxOptRL.CPI.mixPolicy. The model makes these commitments:

$S$ and $A$ are finite nonempty types.
Policies are maps $\pi:S\to A\to\mathbb R$ with IsPolicy, and deterministic policies are indicator policies.
Values carry the factor $1-\gamma$ , so all constants are the thesis's normalized ones. The thesis's statements for infinite state spaces are taken for finite $S$ , where $\|\cdot\|_1$ is a finite sum.
In Lean the policy class is called Pi because Π is reserved.

The run is the explicit predicate IsExactCPIRun: up to the round where the algorithm halts, the chooser output lies in $\Pi$ and maximizes $\mathbb Q_{\pi_k}(\mu,\cdot)$ over $\Pi$ , and the update uses exactly $\alpha_k=\mathbb A/(4H)$ . The halting round is part of the conclusion, never a hypothesis. A formalization in which the halting test or the step size is a free variable, or in which $\Pi$ is empty, would make "halts" an assumption or the run hypothesis unsatisfiable; the goal fixes both and requires $\Pi$ nonempty. The chooser's argmax is assumed to be attained, as in the thesis.

Contributions that would help: bounds $0\le V_\pi\le1$ and $|A_\pi|\le1$ for the normalized model, summability facts for futureStateDist, and a proof that a mixture of policies is a policy. These are reusable across every mission built on the same model.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003, Chapter 7. https://discovery.ucl.ac.uk/id/eprint/10100726/
S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002, pp. 267–274. https://dl.acm.org/doi/10.5555/645531.656005

12 thms2 active usersReviewed

Markov Chain Probability Reinforcement Learning·Captain: mikedeng1

An Analysis of Temporal-Difference Learning with Function Approximation 2: For Every Sampling Distribution q and 5/6 < α < 1, Off-Line q-Sampled TD(0) Can Diverge in ExpectationResearch Paper

Motivation

Temporal-difference learning estimates the future cost of a system from observed transitions. In a Markov model, a state has a distribution of possible successors and each transition carries a cost. An agent may approximate the future cost with a small number of basis functions rather than store one number per state. This is useful when the state set is large or countably infinite, but the sampling rule then matters: the states used to update the approximation need not arrive in the same proportions as visits to the underlying Markov chain.

Tsitsiklis and Van Roy distinguish sampling along the chain from drawing current states independently from a chosen distribution $q$ . Their 1996 LIDS report, §9 constructs an example where the latter version of TD(0) has a mean parameter vector whose norm grows without bound. The example applies to every sampling distribution $q$ on a countable state space with at least two states and every discount factor $\alpha$ strictly between $5/6$ and $1$ . The mission formalizes that quantified counterexample, rather than selecting a particular two-state distribution.

Setting

Let $S$ be a finite or countably infinite set of states. A transition matrix $P$ assigns a probability distribution $p_{ij}$ over next states $j$ to each current state $i$ . A transition cost $g(i,j)$ is incurred when the chain moves from $i$ to $j$ , and $0<\alpha<1$ discounts later costs. The cost-to-go $J^*(i)$ is the expected sum of discounted costs along a chain started at $i$ . An invariant distribution $\pi$ satisfies $\pi^{\mathsf T}P=\pi^{\mathsf T}$ .

A feature vector $\phi(i)\in\mathbb R^K$ represents an approximate cost $\phi(i)^{\mathsf T}r$ , where $r\in\mathbb R^K$ is learned. The weighted norm $\|J\|_D$ uses the weights $\pi(i)$ , and $\Pi$ projects onto the span of the features in that norm. The one-step operator $T^{(0)}$ sends $J$ to the expected immediate cost plus $\alpha$ times the next-state value. These are the objects of §§2–4 of the report.

In $q$ -sampled TD(0), each current state $I_t$ is drawn independently from a probability distribution $q$ ; a successor $J_t$ is then drawn from row $P(I_t,\cdot)$ . Each new pair is independent of the earlier pairs. The parameter changes by

r_{t+1}=r_t+\gamma_t\phi(I_t)\left[g(I_t,J_t)+\alpha\phi(J_t)^{\mathsf T}r_t-\phi(I_t)^{\mathsf T}r_t\right].

The step sizes $\gamma_t$ satisfy the report's Assumption 4: they are chosen in advance, nonnegative and nonincreasing, their sum diverges, and the sum of their squares converges. Assumption 1 asks for a unique positive invariant law, finite stationary second moment of the transition costs, and finite cost-to-go from each state. Assumption 2 asks for linearly independent features with finite stationary second moments.

Formalization targets

Divergence of the mean

For every $q$ and $5/6<\alpha<1$ , Theorem 3 asserts the existence of $P$ , $g$ , and a feature map satisfying Assumptions 1 and 2, together with a unique projected fixed-point parameter $r^*$ , such that for every $r_0\ne r^*$ ,

\Pi T^{(0)}(\phi^{\mathsf T}r)=\phi^{\mathsf T}r\iff r=r^*, \qquad \lim_{t\to\infty}\bigl\|\mathbb E[r_t\mid r_0]\bigr\|=\infty.

The expectation is over the independent state–successor samples. The target is the norm of the mean vector; it does not assert divergence of individual sample paths. The formal goal quantifies over every probability space carrying samples with the stated joint law, so a choice of representation for the random process does not change the theorem.

Supporting statements

The milestones follow the claims in the proof of Theorem 3, pp. 24–25: existence of a full-support transition distribution; the one-feature construction and its assumptions; the general and specialized recurrences for $\mathbb E[r_t]$ ; a positive lower bound for their coefficient $\Delta$ ; and unbounded growth from that lower bound. The numerical inequality retains the report's threshold $5/(6\alpha)$ and its explicit positive factor $6\alpha p(s_2)-5$ .

Significance

The theorem identifies a limit of using TD(0) with linear approximation when the current states are sampled according to a distribution unrelated to the chain's invariant law. The constructed Markov chain itself has a well-defined zero cost-to-go, and the approximation uses only one nonzero feature direction. Nevertheless, the mean of the parameter sequence diverges for every nonfixed initialization. Thus the issue is present even without noisy costs or a complicated feature space. The report contrasts this with its convergence result for the on-line algorithm under additional assumptions; the counterexample says that those conclusions cannot be transferred to arbitrary independent state sampling by changing only the sample source. Tsitsiklis and Van Roy, §9.

The report proves Theorem 3 on paper. This mission asks for a machine-checked proof of its full quantifier structure, including countably infinite state spaces and arbitrary $q$ . A completed development would supply reusable Lean interfaces for countable Markov kernels, path laws, weighted projections, independent state–successor samples, and expected stochastic recurrences. The proposal currently contains the statements and definitions; the theorem proofs are open.

Difficulty

The apparent simplicity of the one-dimensional example hides two issues. First, the statement is uniform over $q$ , including distributions that put zero mass on nearly every state. A proof must choose the two feature states in response to $q$ while preserving the strict positivity needed for growth. Second, the recurrence concerns $\mathbb E[r_t]$ , where $r_t$ depends on all earlier random pairs. The step at time $t$ uses a fresh pair, and the factorization of its mean requires that temporal independence, plus justified integrability. Writing a positive scalar coefficient alone does not establish divergence of the expected parameter sequence for the sampled process.

Formalization scope

The Lean state space is a countable discrete measurable type with at least two elements. $P$ is a Markov kernel, its path law comes from the Ionescu–Tulcea construction, and the cost-to-go is the expectation of the discounted path sum. Weighted $L_2(S,D)$ membership is expressed by summability of $\pi(i)J(i)^2$ . The projection uses the inverse of the weighted Gram matrix under the independence and positive-mass assumptions that make it invertible. Only $T^{(0)}$ is needed here. The number $K$ of basis functions is existential, like the report's matrix $\Phi$ , but must be at least one: an empty parameter space would leave the universal divergence clause with no nonfixed initializations. The report's own example has $K=1$ .

Assumption 1 includes uniqueness of $\pi$ , positive mass at each state, the stationary squared-cost moment, and absolute integrability of the cost-to-go. Assumption 2 includes linear independence and integrability of squared features. Assumption 4 retains square-summability even though the displayed growth argument uses the divergent first-power sum. The general mean recurrence assumes bounded costs and features so its integrals and countable sums are meaningful; the constructed example satisfies those bounds. The goal additionally states finite-time integrability of the parameter vector. The source indexes states by 1 and 2; the formalization uses two distinct states $s_1,s_2$ and records the proof's ordering $0<q(s_1)$ and $q(s_2)\le q(s_1)$ in the growth milestone. The goal's quantification over probability spaces is restricted to Lean's Type universe.

The general mean recurrence is written with the immediate cost outside the matrix factor multiplying $\mathbb E[r_t]$ . This follows the algorithm displayed on p. 24 and corrects two slips in the printed recurrence on p. 25: its next-state subscript and the placement of the mean-cost term. Contributions to the path-law facts, independent-sampling calculations, countable weighted sums, and scalar growth theorem all support the same fixed goal.

Selected references

J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, MIT Laboratory for Information and Decision Systems report LIDS-P-2322, 1996; published in IEEE Transactions on Automatic Control 42(5), 1997. MIT record.

9 thms2 active usersReviewed

Probability Statistics·Captain: mikedeng1

Consistent Nonparametric Regression II: Nearest-Neighbor Weights with Vanishing Coefficients Are Consistent for Every Distribution of X (Theorem 2)Research Paper

Motivation

Nonparametric regression estimates the regression function $x \mapsto E(Y \mid X = x)$ from i.i.d. observations $(X_1, Y_1), \dots, (X_n, Y_n)$ without assuming a parametric form. The simplest such estimates are local averages: to predict at a point $X$ , average the responses $Y_i$ of the sample points closest to $X$ . Nearest neighbor rules of this kind go back to Fix and Hodges (1951) for classification and are still a standard baseline in statistics and machine learning.

Before 1977, consistency results for such estimates assumed regularity of the distribution of $X$ : a density, continuity of the regression function, or bounded support. C. J. Stone's paper Consistent nonparametric regression (Ann. Statist. 5 (1977) 595–645) proved that suitable nearest neighbor estimates are consistent in $L^r$ for every joint distribution of $(X, Y)$ with $E|Y|^r < \infty$ . This property, now called universal consistency, is the subject of the first chapters of Györfi, Kohler, Krzyżak and Walk, A Distribution-Free Theory of Nonparametric Regression (Springer, 2002), where Stone's theorem is the organising result.

This mission formalizes Theorem 2 of Stone's paper, the universal consistency of nearest neighbor weights. Mission I of the series formalizes the general criterion (Theorem 1) that the proof applies; mission III treats conditional quantiles.

Setting

Let $X, X_1, X_2, \dots$ be i.i.d. random vectors in $\mathbb R^d$ with an arbitrary law $\mu$ . A weight function $W_n$ assigns to the query point $X$ and the sample numbers $W_{ni}(X) = W_{ni}(X, X_1, \dots, X_n)$ , $1 \le i \le n$ . It is a probability weight function if $W_{ni} \ge 0$ and $\sum_i W_{ni}(X) = 1$ . Given i.i.d. pairs $(X, Y), (X_1, Y_1), \dots$ with $Y$ real, the estimate of $E(Y \mid X)$ is

\hat E_n(Y \mid X) = \sum_{i=1}^n W_{ni}(X)\, Y_i .

The sequence $\{W_n\}$ is consistent if, whenever the pairs are i.i.d. with the given law of $X$ , $r \ge 1$ and $E|Y|^r < \infty$ , one has $E|\hat E_n(Y\mid X) - E(Y\mid X)|^r \to 0$ .

Scales and metrics. A scale is a nonnegative function $s_{nj} = s_{nj}(X, X_1, \dots, X_n)$ , $1 \le j \le d$ , and its pseudometric is

\rho_n(u, v) = \Big(\sum_{j:\, s_{nj} > 0} \Big(\frac{u_j - v_j}{s_{nj}}\Big)^2\Big)^{1/2}.

The choice $s_{nj} \equiv 1$ gives the Euclidean metric; the sample standard deviations of the coordinates give a unit-free one. The sequence $\{s_n\}$ is regular (p. 599) with constants $0 < a \le b$ if $P(s_{nj} > 0) \to 1$ for every coordinate of $X$ with a nondegenerate law, $s_{nj}/s_{nl}$ is bounded in probability for any two such coordinates, and condition (7) holds: interchanging $X$ and $X_i$ changes $s_{nj}$ by a factor in $[a, b]$ whenever the $j$ th coordinates of $X_1, \dots, X_n$ do not all coincide.

Nearest neighbor weights. Let $c_{n1} \ge \dots \ge c_{nn} \ge 0$ with $\sum_i c_{ni} = 1$ and $c_{ni} = 0$ for $i > n$ . The weight of $X_i$ is

W_{ni}(X) = \frac{c_{n\nu} + \dots + c_{n,\nu+\lambda-1}}{\lambda},

where $\nu - 1$ is the number of other sample points strictly $\rho_n$ -closer to $X$ than $X_i$ and $\lambda - 1$ the number at the same distance: the $k$ th closest point receives $c_{nk}$ , and tied points share the average of the coefficients of their ranks. The uniform $k$ -NN rule is $c_{ni} = 1/k$ for $i \le k$ .

Formalization targets

Goal: Theorem 2 (p. 600)

For every law $\mu$ of $X$ and every regular sequence of scales,

\lim_{n} \sum_{i > \alpha n} c_{ni} = 0 \ \ (\forall \alpha > 0) \quad\text{and}\quad \lim_n c_{n1} = 0 \quad\Longrightarrow\quad \{W_n\} \text{ is consistent.}

Uniform, triangular and quadratic $k_n$ -NN weights with $k_n \to \infty$ , $k_n / n \to 0$ satisfy both conditions (Corollary 3).

Milestones

Corollary 1 (sufficiency), p. 598. Probability weights with $E\sum_i W_{ni}(X) f(X_i) \le C\,Ef(X)$ for some $C \ge 1$ and all nonnegative Borel $f$ , with $\sum_i W_{ni}(X) I_{\{\|X_i - X\| > a\}} \to 0$ and $\max_i W_{ni}(X) \to 0$ in probability, are consistent.
Proposition 9, p. 611. For every $\delta > 0$ , $\lim_{\alpha\downarrow 0}\limsup_n P(\max_{i \in I_{n,\alpha n}(X)} \|X_i - X\| > \delta) = 0$ , where $I_{n,t}(X)$ are the indices of the $\lfloor t \rfloor$ nearest neighbors (with ties).
Proposition 10, p. 613. For $0 < a \le b_j \le b$ , two vectors $0 < \|u\| \le \|v\|$ in a set $V \in \mathcal V(d, a/b)$ satisfy $\|\tilde v\| > \|\tilde v - \tilde u\|$ after rescaling $\tilde u_j = b_j u_j$ , $\tilde v_j = b_j v_j$ . Here $\mathcal V(d, c)$ is the family of sets in which any two nonzero vectors satisfy $u\cdot v > (1 - c^2/2)\|u\|\|v\|$ , and $\beta(d, c)$ is the least number of members of $\mathcal V(d,c)$ covering $\mathbb R^d$ .
Proposition 12, p. 613. For fixed points, the swapped weights $U_{ni}(X) = W_{ni}(X_i, X_1, \dots, X, \dots, X_n)$ satisfy $\sum_i U_{ni}(X) \le \beta(d, a/b)$ .
Proposition 11, p. 613. $E \sum_i W_{ni}(X) f(X_i) \le \beta(d, a/b)\, Ef(X)$ for nonnegative Borel $f$ with $Ef(X) < \infty$ .

Significance

Theorem 2 established that a local averaging estimate can be consistent with no assumption on the distribution of $X$ beyond the moment condition on $Y$ . The same argument, through Theorem 1, became the standard template for proving universal consistency of kernel, partitioning and nearest neighbor estimates, and of the classification rules derived from them (Devroye, Györfi and Lugosi, A Probabilistic Theory of Pattern Recognition, 1996). The constant $\beta(d, a/b)$ of Proposition 11 is an early instance of the cone-covering bound on how many points can have a given point among their nearest neighbors, a lemma that reappears throughout nearest neighbor theory.

The result is proved (1977), and textbook proofs exist. Mathlib contains no formalization of Theorem 2, of Stone's criterion, or of the cone-covering lemma. A formal development would supply reusable infrastructure: nearest neighbor weights with averaged ties, the exchangeability argument behind Proposition 11, and $L^r$ consistency of weighted averages for i.i.d. data encoded through kernels.

Difficulty

The obvious argument estimates $\hat E_n(Y\mid X)$ by a continuity argument around $X$ , which needs a density or continuity of $E(Y\mid X)$ and is unavailable here. The difficulty is condition (1) of Stone's criterion: a single sample point may be a nearest neighbor of many query points, so $E\sum_i W_{ni}(X) f(X_i)$ is not obviously comparable to $Ef(X)$ for arbitrary $f$ and arbitrary $\mu$ (atoms, singular parts, unbounded support). The bound must hold uniformly in $n$ and in the distribution, with a data-dependent metric whose scale changes when $X$ and $X_i$ are interchanged. Ties in $\rho_n$ , which have positive probability when $\mu$ has atoms, must be handled by the averaged weights (8), not by an index tie-break.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). The i.i.d. sequence is the coordinate process of Measure.infinitePi, coordinate 0 being $X$ ; sample indices are 0-based, coefficients $c_{n,m}$ keep the paper's 1-based index. "Whenever the pairs are i.i.d." is encoded by quantifying over every Markov kernel $\kappa$ (the conditional law of $Y$ given $X$ ), with pairs distributed as $(\mu \otimes \kappa)^{\otimes\mathbb N}$ and $E(Y\mid X=x) = \int y\,\kappa(x, dy)$ . Expectations of nonnegative quantities are lower Lebesgue integrals in $[0,\infty]$ ; convergence in probability is TendstoInMeasure; limits of probabilities are taken in $[0,\infty]$ .

Standing assumptions and additions, each disclosed in the item statements:

the scales are regular (the standing assumption of §3, p. 599) and Borel measurable (added; the paper treats them as random variables);
condition (7) is read for all points, as Proposition 12's proof uses it, and "do not coincide" means "are not all equal";
"nondegenerate" means the coordinate's law is not a point mass; $s_{nj}/s_{nl}$ is real division ( $0$ where $s_{nl} = 0$ , an event of vanishing probability);
Corollary 1's weights are assumed jointly Borel;
Proposition 9's distance $a$ is renamed $\delta$ , and the maximum over an empty index set is read as "no index";
$\beta(d, c)$ is an infimum over $\mathbb N$ ; that a finite cover exists is part of the work, not an assumption.

No statement corrects the print.

The goal is stated as $L^r$ consistency over all kernels and all $r \ge 1$ , for an unrestricted law $\mu$ : it is not stated through Corollary 1's three conditions nor through $\beta$ , and no density, moment or support hypothesis on $X$ is present, so a proof cannot reduce to a special case.

A complete development needs: exchangeability of finite i.i.d. samples under the product measure, the finite cone cover of $\mathbb R^d$ , the strong law of large numbers (Proposition 9's proof), and Stone's criterion (mission I). Contributions proving any milestone, the cone-cover existence lemma, or the transfer of exchangeability through infinitePi are welcome.

Selected references

C. J. Stone, Consistent nonparametric regression, Ann. Statist. 5(4) (1977) 595–645. https://doi.org/10.1214/aos/1176343886
L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
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
E. Fix, J. L. Hodges, Discriminatory analysis. Nonparametric discrimination: consistency properties, USAF School of Aviation Medicine, Report 4, 1951; reprinted in Int. Stat. Rev. 57(3) (1989) 238–247. https://doi.org/10.2307/1403797

8 thms2 active usersReviewed

Probability Statistics·Captain: mikedeng1

Consistent Nonparametric Regression III: Consistent Probability Weights Give Consistent Estimators of Conditional Quantiles (Theorem 3)Research Paper

Motivation

Many prediction tasks ask not for the mean of a response $Y$ given covariates $X$ but for a quantile of its conditional distribution: a median that is robust to outliers, a high quantile that sets a safety stock or a value at risk, or a pair of quantiles that forms a prediction interval. Conditional quantiles are also the Bayes rules for piecewise linear loss, which makes them the decision-theoretic answer to asymmetric prediction costs.

C. J. Stone's 1977 paper Consistent nonparametric regression (DOI 10.1214/aos/1176343886) introduced a single framework for local averaging estimators (nearest-neighbor, kernel and related rules) built from weight functions, and proved that their consistency can be decided from simple conditions on the weights, for every distribution of $(X,Y)$ . Section 7 of the paper extends the framework from conditional means to conditional quantiles: the same weights that estimate $E(Y\mid X)$ define a weighted empirical distribution of $Y$ near $X$ , whose quantiles estimate the conditional quantiles. Theorem 3 says that consistency for the mean already gives one-sided consistency for the quantiles. This mission formalizes Theorem 3 and the results its proof rests on.

Setting

Let $X, X_1, X_2, \dots$ be independent $\mathbb R^d$ -valued random variables with common law $\mu$ , and let $Y, Y_1, Y_2,\dots$ be real responses such that the pairs $(X,Y), (X_1,Y_1), (X_2,Y_2),\dots$ are i.i.d. The conditional law of $Y$ given $X=x$ is a probability measure $\kappa(x,\cdot)$ on $\mathbb R$ .

A weight function $W_n$ assigns to a point $x$ and a sample $x_1,\dots,x_n$ real weights $W_{ni}(x)=W_{ni}(x;x_1,\dots,x_n)$ , $1\le i\le n$ . A sequence $\{W_n\}$ is a sequence of probability weights if for every $n\ge1$ the weights are nonnegative and sum to $1$ . The weights define the regression estimate $\hat E_n(Y\mid X)=\sum_i W_{ni}(X)Y_i$ . The sequence is consistent if, whenever $r\ge1$ and $E|Y|^r<\infty$ ,

E\,\big|\hat E_n(Y\mid X)-E(Y\mid X)\big|^r\to0,

for every response $Y$ with i.i.d. pairs as above. Consistency is a property of the weights and the law of $X$ alone.

The conditional distribution function is $F^Y(y\mid X)=P(Y\le y\mid X)$ . For $0<p<1$ the lower and upper $p$ th conditional quantiles are

L^Y(p\mid X)=\inf\{y:F^Y(y\mid X)\ge p\},\qquad U^Y(p\mid X)=\sup\{y:F^Y(y\mid X)\le p\}.

They coincide unless the conditional distribution function is flat at level $p$ . The weights estimate the conditional distribution function by $\hat F_n^Y(y\mid X)=\sum_i W_{ni}(X)I_{\{Y_i\le y\}}$ , and the quantiles by

\hat L_n^Y(p\mid X)=\inf\{y:\hat F_n^Y(y\mid X)\ge p\},\qquad \hat U_n^Y(p\mid X)=\sup\{y:\hat F_n^Y(y\mid X)\le p\}.

Write $x^-=-(x\wedge0)$ and $x^+=x\vee0$ .

Formalization targets

Goal: Theorem 3 (p. 604)

For a consistent sequence of probability weights and $0<p<1$ ,

(\hat L_n^Y(p\mid X)-L^Y(p\mid X))^-\to0\quad\text{and}\quad(\hat U_n^Y(p\mid X)-U^Y(p\mid X))^+\to0\quad\text{in probability},

and if $r\ge1$ and $E|Y|^r<\infty$ , both convergences hold in $L^r$ . The theorem is one-sided on purpose: when the conditional quantile is not unique, $\hat L_n$ and $\hat U_n$ may oscillate inside $[L,U]$ .

Milestones

Corollary 1, necessity (p. 598). Consistent probability weights satisfy condition (1), $E\sum_i W_{ni}(X)f(X_i)\le C\,Ef(X)$ for some $C\ge1$ ; condition (3), $\sum_i W_{ni}(X)I_{\{\|X_i-X\|>a\}}\to0$ in probability; and condition (5), $\max_i W_{ni}(X)\to0$ in probability.
Proposition 4 (p. 609). Under (1)–(3), for every Borel $f$ and $\varepsilon>0$ , $\sum_i|W_{ni}(X)|I_{\{|f(X_i)-f(X)|>\varepsilon\}}\to0$ in probability.
Proposition 13 (p. 616). $P(\hat L_n^Y(p\mid X)\ge L^Y(p\mid X)-\varepsilon)\to1$ and $P(\hat U_n^Y(p\mid X)\le U^Y(p\mid X)+\varepsilon)\to1$ for every $\varepsilon>0$ .
Proposition 14 (p. 616). $E|L^Y(p\mid X)|^r\le E|Y|^r/(p\wedge(1-p))$ , and the same for $U^Y$ .
Proposition 15 (p. 617). For a probability weight function satisfying (1), $E|\hat L_n^Y|^rI_{\{|\hat L_n^Y|\ge M\}}\le \frac{C}{p\wedge(1-p)}E|Y|^rI_{\{|Y|\ge M\}}$ , and the same for $\hat U_n^Y$ .

Significance

Theorem 3 transfers every consistency result for conditional means to conditional quantiles at no extra cost. In particular, the nearest-neighbor weights of Stone's Theorem 2, which are consistent for every distribution of $X$ , give universally consistent one-sided estimates of conditional quantiles, and when the conditional $p$ th quantile is unique, the midpoint estimate $(\hat L_n+\hat U_n)/2$ is consistent (Corollary 5 of the paper). The theorem is also the input for the consistency in Bayes risk of approximate Bayes rules under piecewise linear loss (Theorem 4, Model 2), which connects nonparametric regression to data-driven decision making such as the newsvendor problem with covariates.

The result has been proved since 1977; it has no machine-checked proof that this mission is aware of. A formalization produces a reusable layer for distribution-free statistics in Lean: weighted empirical distributions, conditional quantiles defined from a Markov kernel, convergence in probability and in $L^r$ of statistics of an i.i.d. sequence, and the moment bounds of Propositions 14 and 15, which hold for every weight function and do not depend on the asymptotics.

Difficulty

The obvious argument fails because the conditional distribution function at $X$ is never estimated uniformly. Consistency controls the weighted average $\sum_iW_{ni}(X)g(Y_i)$ only for responses that are a fixed function of the pair; the event $\{\hat L_n<L(X)-\varepsilon\}$ involves the random threshold $L(X)$ , which varies with the target point while the sample responses $Y_i$ are drawn at the sample points $X_i$ . Connecting the two requires a statement about the weights alone, Proposition 4, that holds for an arbitrary Borel function with no continuity or integrability; the conditional quantile function is in general neither continuous nor integrable.

A second difficulty is that convergence in probability does not give convergence in $L^r$ without uniform integrability, and the estimated quantiles are not averages of the $Y_i$ . The bound in Proposition 15 must hold for each $n$ separately, with a constant independent of $n$ , for an estimator defined as an infimum.

Finally, the two-sided statement $\hat L_n\to L$ need not hold when the conditional distribution function has a flat stretch at level $p$ , which is why the paper asks for a unique conditional quantile in Corollary 5; a solver should not aim for it.

Formalization scope

The i.i.d. sequences are the coordinate processes of infinite product measures, Measure.infinitePi, with coordinate $0$ the point $X$ (or the pair $(X,Y)$ ) and coordinate $i+1$ the $(i+1)$ st sample; sample indices are 0-based. The response is given by its conditional law, a Markov kernel $\kappa$ from $\mathbb R^d$ to $\mathbb R$ , and the joint law of a pair is $\mu\otimes\kappa$ . "Whenever the pairs are i.i.d." in the definition of consistency is a quantifier over all Markov kernels; every joint law with $X$ -marginal $\mu$ arises this way. This also provides the independent standard normal variables that the paper assumes on its probability space.

Committed conventions:

Measurability (added). Every weight function $W_n$ is assumed jointly Borel in $(x,x_1,\dots,x_n)$ . The paper treats $W_{ni}(X)$ as random variables without saying so.
Expectations of nonnegative quantities ( $E|Y|^r$ , the $L^r$ errors, the moment bounds) are $[0,\infty]$ -valued lower integrals, so an infinite expectation is never read as $0$ .
Convergence in probability is Mathlib's TendstoInMeasure.
Quantiles are real sInf/sSup. For a Markov kernel, $0<p<1$ , probability weights and $n\ge1$ , the defining sets are nonempty and bounded on the relevant side, so the values are the paper's; at $n=0$ the estimates are a junk value that no limit statement sees.
Conditions (1)–(5) are stated with $|W_{ni}|$ , as in Theorem 1; for probability weights they coincide with Corollary 1's.

Corrections and choices of range. Proposition 14 is printed for $r>1$ . The proof of Theorem 3 applies it for every $r\ge1$ , and the statement is posed for $r\ge1$ . Proposition 15 leaves $r$ unquantified and is posed for $r\ge1$ , the range Theorem 3 uses.

A goal stated through the probabilities of Proposition 13, or through truncated moments, would be a different and weaker theorem; the goal states convergence of the quantile errors $(\hat L_n-L)^-$ and $(\hat U_n-U)^+$ themselves, in probability and in $L^r$ . Swapping the negative and positive parts gives a false statement.

Corollary 1 (necessity) is a special case of Theorem 1, the goal of the first mission of this series; it is posed here as a milestone so that this mission is self-contained, and can be replaced by a reference once that mission is published. Contributions are welcome on any milestone, and on general infrastructure for Markov kernels, conditional distribution functions and quantiles, which is reusable beyond this mission.

Selected references

C. J. Stone, Consistent nonparametric regression, Annals of Statistics 5(4), 595–645, 1977. https://doi.org/10.1214/aos/1176343886
L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
R. Koenker, G. Bassett, Regression quantiles, Econometrica 46(1), 33–50, 1978. https://doi.org/10.2307/1913643

8 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 5: With Pool Predictions in [0,1], the Binary Master WMG Makes at Most log(w_init/w_fin)/log(2/(1+β)) MistakesResearch Paper

Motivation

Prediction with expert advice asks how a learner should combine the forecasts of a pool of prediction algorithms when nothing is assumed about the data: the instances and labels may be chosen by an adversary, and the learner's performance is compared with that of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) introduced the multiplicative-weights master algorithm WM for binary pool predictions and proved that its number of mistakes is at most logarithmic in the pool size plus a constant times the mistakes of the best pool member. The same multiplicative update now underlies boosting, online convex optimization and approximate solvers for linear programs and zero-sum games (Arora, Hazan, Kale 2012).

In many applications the pool members do not output a bit but a degree of confidence in $[0,1]$ , while the master must still commit to a binary decision. Section 5 of the paper treats exactly this setting with the algorithm WMG, and shows that WM's mistake bound survives unchanged.

Setting

A nonempty pool of $n$ prediction algorithms is run on a finite sequence of trials. In trial $k$ the pool member $i$ predicts $x_{k,i}\in[0,1]$ , the master predicts $\lambda_k\in\{0,1\}$ , and then the binary label $\rho_k\in\{0,1\}$ is revealed. The master keeps a non-negative weight $w_{k,i}$ per pool member, with positive initial weights. Write

s_k=\sum_{i=1}^n w_{k,i},\qquad \gamma_k=\frac{\sum_{i=1}^n w_{k,i}\,x_{k,i}}{s_k},

and $w_{\mathrm{init}}=s_0$ , $w_{\mathrm{fin}}$ the total weight after the last trial.

WMG with parameter $0\le\beta<1$ predicts $\lambda_k=1$ if $\gamma_k>1/2$ and $\lambda_k=0$ if $\gamma_k<1/2$ ; at $\gamma_k=1/2$ either prediction is allowed. A mistake is a trial with $\lambda_k\ne\rho_k$ , and $m$ is the number of mistakes. An update step multiplies every weight by a factor

w_{k+1,i}=F\,w_{k,i},\qquad \beta^{|x_{k,i}-\rho_k|}\le F\le 1-(1-\beta)\,|x_{k,i}-\rho_k| \tag{5.1}

with $0^0=1$ . WMG executes an update step in every trial, or only in mistake trials; more generally (footnote 8 of the paper) in every mistake trial and possibly in others. Outside update steps the weights do not change. When the $x_{k,i}$ are binary, WMG coincides with WM.

Formalization targets

Goal: Theorem 5.1 (pp. 234–235)

For every run of WMG with $0\le\beta<1$ , whatever the tie-breaking, the update criterion and the factors in (5.1), if $w_{\mathrm{fin}}>0$ then

m\le\frac{\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})}{\ln\bigl(2/(1+\beta)\bigr)}.

The bound involves only the total weights, not the losses of individual pool members; Corollary 5.1 of the paper, which compares $m$ with the total absolute loss $m_i$ of each pool member, follows from it and from the lower bound in (5.1).

Milestones

Appendix, p. 256. In a mistake trial the total weight drops by at least a factor $(1+\beta)/2$ : $s_{k+1}\le\frac{1+\beta}{2}s_k$ .
§5, p. 235. Unless $\beta=0$ and $|\gamma_k-\rho_k|=1$ in some update trial,

\sum_{k\ \text{update}}\ln\bigl(1-(1-\beta)|\gamma_k-\rho_k|\bigr)\le\sum_{k\ \text{mistake}}\ln\bigl(1-(1-\beta)|\gamma_k-\rho_k|\bigr)\le m\ln\bigl(\tfrac12+\tfrac12\beta\bigr).

The paper gives two proofs of Theorem 5.1, one through each milestone; the second also uses Lemma 5.2, the potential lemma shared with the continuous master WMC, which is posed in the companion mission on WMC.

Significance

Theorem 5.1 says that the master's mistake count is controlled by how much total weight the pool loses, with the same constant $1/\ln(2/(1+\beta))$ as for binary pools. With equal initial weights it gives Corollary 5.1: WMG makes at most $(\log n+m_i\log(1/\beta))/\log(2/(1+\beta))$ mistakes for every pool member $i$ , so pool members may report graded confidences at no cost in the master's guarantee. The same weight-potential argument is the template for the randomized master WMR of §6 and for later analyses of exponential weights.

The result is classical and proved in the paper. What this mission adds is a machine-checked statement and proof against the paper's own model: a relation that covers both update criteria, all tie-breaks at $\gamma=1/2$ and the whole interval of admissible factors, rather than a single deterministic instance. No formalization of WMG or of Theorem 5.1 is known; the platform's existing weighted-majority results (Hazan's textbook version) concern binary experts, unit initial weights and a fixed update factor.

Difficulty

The obvious argument, copied from WM, tracks the weight $q_0$ of members predicting $0$ and the weight $q_1$ of members predicting $1$ . With predictions in $[0,1]$ a member supports both outcomes, and the update factor is only constrained to an interval, so the two-bucket bookkeeping must be redone for fractional contributions. The factor's upper bound $1-(1-\beta)r$ is affine in $r=|x-\rho|$ , while the natural exponential factor $\beta^r$ is convex; the argument must use the right one of the two bounds of (5.1). A further subtlety is the case $\beta=0$ : a factor may be $0$ , the total weight can vanish, and both the logarithmic bound and the weighted average $\gamma$ degenerate.

Formalization scope

The pool is Fin n with $n>0$ , and the trials are Fin T, all trials of the sequence; weights are w : ℕ → Fin n → ℝ, with w 0 the initial and w T the final weights.
Pool predictions are real numbers in $[0,1]$ , labels and master predictions are real numbers in $\{0,1\}$ .
The update criterion is a Boolean flag per trial that must be set in every mistake trial; the factor is an arbitrary real number in the interval (5.1) for each trial and member, where $\beta^{r}$ is Real.rpow (so $0^0=1$ ).
The paper writes a ratio of logarithms with the base omitted; Real.log is used.
The case $w_{\mathrm{fin}}=0$ , where the paper's bound is $+\infty$ , is excluded by the hypothesis $0<w_{\mathrm{fin}}$ . Without it, Lean's Real.log 0 = 0 would turn the paper's vacuous bound into the false claim $m\le0$ ; with it, no Lean junk value enters the statement.
The goal must be stated for the relation, not for a single run: fixing the tie-break, updating in every trial only, or fixing $F$ to one endpoint of (5.1) would state a special case. Stating the theorem only for binary pool predictions would state Theorem 2.1 instead.

A complete development needs only finite sums, real logarithms and real powers from Mathlib. Proofs of either milestone, of the existence of a run for every input (using Lemma 5.1, $\beta^r\le1+r(\beta-1)$ ), and of Corollary 5.1 on top of the goal are welcome.

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
V. Vovk, Aggregating Strategies, Proc. 3rd COLT, 371–383, 1990. https://dl.acm.org/doi/10.5555/92571.92672
S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8, 121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006

5 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

MNL-Bandit: A Dynamic Learning Approach to Assortment Selection III: On Instances Separated by Δ(v) the UCB Policy Has Regret at Most B₁N² log T/Δ(v) + B₂Research Paper

Motivation

A retailer with limited shelf or screen space must choose which subset of its products to show each arriving customer. Which assortment earns the most depends on customer preferences, and those are unknown at first: the seller learns them from the purchases it observes. This is dynamic assortment selection, and it is a standard model in online retail and revenue management. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 67(5), 2019; preprint arXiv:1706.03880v2) study it under the multinomial logit (MNL) choice model as the MNL-Bandit problem. They propose an epoch-based upper-confidence-bound policy (Algorithm 1) that needs no prior knowledge of the parameters.

Their worst-case guarantee (Theorem 1) is regret of order $\sqrt{NT\log NT}$ . Many instances are easier than the worst case: the best assortment beats every other feasible assortment by a fixed margin. For such well-separated instances, earlier policies obtained logarithmic regret, but only when told a lower bound on that margin:

Rusmevichientong, Shen and Shmoys (2010), $O(N^2\log^2 T)$ ;
Sauré and Zeevi (2013), $O(N\log T)$ for fixed cardinality.

This mission formalizes the paper's §6.1, which shows that the same parameter-free Algorithm 1 adapts to the separation.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$ and unknown attraction parameters $v_i\ge0$ . The no-purchase option has weight $v_0=1$ . Offered an assortment $S$ , a customer buys $i\in S$ with probability $v_i/(1+\sum_{j\in S}v_j)$ and buys nothing with probability $1/(1+\sum_{j\in S}v_j)$ (2.1). The expected revenue of $S$ is

R(S,\mathbf v)=\frac{\sum_{i\in S}r_iv_i}{1+\sum_{j\in S}v_j}\quad(2.2).

Feasible assortments form a family $\mathcal S$ defined by totally unimodular constraints $A\,x(S)\le b$ (2.3). Assumption 4.1 asks that $v_i\le v_0=1$ for all $i$ and that $\mathcal S$ be closed under taking subsets.

A policy chooses $S_t\in\mathcal S$ from the past choices. The regret after $T$ customers is $\mathrm{Reg}_\pi(T,\mathbf v)=T\,R(S^*,\mathbf v)-\mathbb E_\pi\sum_{t=1}^TR(S_t,\mathbf v)$ , where $S^*$ maximizes $R(\cdot,\mathbf v)$ over $\mathcal S$ (2.6).

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ until a customer buys nothing. It keeps three statistics for each product $i$ :

$T_i(\ell)$ , the number of epochs up to $\ell$ that offered $i$ ;
$\bar v_{i,\ell}$ , the average number of purchases of $i$ per such epoch;
the upper confidence bound $v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,48\log(\sqrt N\ell+1)/T_i(\ell)}+48\log(\sqrt N\ell+1)/T_i(\ell)$ .

The next epoch offers an assortment maximizing the MNL revenue computed with $v^{\mathrm{UCB}}$ in place of $\mathbf v$ .

The separation of an instance is the gap between the optimal and the second-best expected revenue among feasible assortments,

\Delta(\mathbf v)=\min_{S\in\mathcal S:\,R(S,\mathbf v)\neq R(S^*,\mathbf v)}\big(R(S^*,\mathbf v)-R(S,\mathbf v)\big)\quad(6.1).

The analysis uses the threshold $\tau=4NC\log NT/\Delta^2(\mathbf v)$ (6.2), with $C=\max\{C_1^2,C_2\}$ , $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ . It also uses good epochs: those in which every $v^{\mathrm{UCB}}_{i,\ell}$ lies above $v_i$ and within the confidence width of Lemma 4.1.

Formalization targets

Goal: Theorem 3 (p. 20)

There are absolute constants $B_1,B_2$ such that for every instance satisfying Assumption 4.1 with $r_i\in[0,1]$ , every tie-breaking rule and every $T$ ,

\mathrm{Reg}_\pi(T,\mathbf v)\le B_1\,\frac{N^2\log T}{\Delta(\mathbf v)}+B_2.

The constants are not fixed, so the goal survives any improvement of them.

Milestones

Lemma 4.1 (p. 13): $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability $\ge1-6/(N\ell)$ , and $v^{\mathrm{UCB}}_{i,\ell}-v_i\le C_1\sqrt{v_i\log(\sqrt N\ell+1)/T_i(\ell)}+C_2\log(\sqrt N\ell+1)/T_i(\ell)$ with probability $\ge1-7/(N\ell)$ .
Lemma 4.3 (p. 14): $(1+\sum_{j\in S}v_j)(\tilde R(S)-R(S,\mathbf v))$ is at most the sum of these widths over the offered set, with probability $\ge1-13/\ell$ .
Lemma 6.1 (p. 20): in a good epoch, if every offered product has $T_i(\ell)\ge\tau$ , the offered assortment is optimal.
Lemma 6.2 (p. 20): at most $N\tau$ good epochs offer a sub-optimal assortment.
Corollary C.1 (p. 48): at most $N\log NT$ epochs offer a product with $T_i(\ell)<\log NT$ .
(C.5) (p. 48): the regret is at most $\mathbb E_\pi\sum_{\ell\le L}(1+V(S_\ell))(R(S^*,\mathbf v)-R(S_\ell,\mathbf v))$ .

Companion: Corollary 6.1 (p. 21)

Under the cardinality constraint $|S|\le K$ : $\mathrm{Reg}_\pi(T,\mathbf v)\le B_1\,NK\log NT/\Delta(\mathbf v)+B_2$ .

Significance

The result. Theorem 3 shows that one policy is simultaneously near-optimal in the worst case (Theorem 1, $\tilde O(\sqrt{NT})$ , matched by the lower bound of Theorem 2 up to logarithms) and logarithmic on separated instances. It does so without being told $\Delta(\mathbf v)$ , which the separation-based policies of Rusmevichientong et al. and Sauré–Zeevi require. Under a cardinality constraint, Corollary 6.1 matches the order of Sauré–Zeevi's bound.

Formalizing it. The theorem is proved in the paper (Appendix C), and no machine-checked version exists. A formal proof has to make several things precise:

Algorithm 1 as a function of the observed history;
the epoch structure of a finite horizon;
the pathwise counting arguments of Lemmas 6.1–6.2 and Corollary C.1;
the probabilistic estimates inherited from the worst-case analysis.

Two printed details need care, and the formal statements fix them: Appendix C defines good epochs with "or" where both inequalities are meant, and Lemma 6.2's proof skips one case.

Difficulty

The counting part looks routine but depends on indexing. The bounds that are good at the end of epoch $\ell$ select the assortment of epoch $\ell+1$ , so "a good epoch offering a sub-optimal set" pairs two consecutive epochs. A per-product count of under-sampled epochs is then off by one per product, so the printed bound $N\tau$ does not follow from the statement of Lemma 6.1 by counting alone.

The probabilistic part is the harder one. The per-epoch purchase counts are geometric with mean $v_i$ only conditionally on adaptively chosen assortments. The confidence statements must hold uniformly over a random number of samples, and the regret must be converted from customers to epochs, whose lengths are random and truncated at $T$ . A union bound over all epochs costs a factor $\log T$ , and that factor has to stay within the claimed $N^2\log T/\Delta$ .

Formalization scope

Products are Fin N (0-based), and choices are Option (Fin N) with none the no-purchase option. A policy maps the past choices to an assortment. The law of a length- $T$ history is the product of MNL probabilities, so every expectation is a finite sum. Revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1, and $R(S^*,\mathbf v)$ is a Finset.sup' over the nonempty family $\mathcal S$ . Algorithm 1 is defined as an explicit state machine and never reads $\mathbf v$ . Ties in its argmax are broken by an arbitrary selector, and every statement quantifies over all selectors.

Standing assumptions carried by every statement:

$0\le v_i\le1$ ;
$r_i\in[0,1]$ ;
the totally unimodular form of $\mathcal S$ ;
closure under subsets;
nonemptiness of $\mathcal S$ (needed for $S^*$ to exist).

Disclosed conventions:

UCB before sampling. $v^{\mathrm{UCB}}_{i,\ell}=1$ while $T_i(\ell)=0$ .
Degenerate separation. $\Delta(\mathbf v)=1$ when every feasible assortment is optimal; the regret is then $0$ .
Lemma 4.1 constants. $C_1,C_2$ take the values established in the proof of Lemma 4.1.
Probabilistic lemmas. They are stated for every horizon $T$ as probabilities that epoch $\ell$ is completed and the bound fails.
Lemma 4.3. The printed free index $i$ is read as the sum over the offered set, and $\tilde R$ uses the bounds of the preceding epoch.
(C.5). It is stated as " $\le$ ", since the last epoch is truncated at $T$ .

The constants $B_1,B_2$ are quantified before every other object. A constant depending on $N$ , $\mathbf v$ or $\Delta$ would make the theorem say only that regret is finite. The policy is pinned to Algorithm 1, not to any optimistic rule.

Contributions are welcome at every level:

the pathwise lemmas (6.1, 6.2, C.1), which need no probability;
the epoch rewriting (C.5);
the concentration Lemmas 4.1 and 4.3, shared with the companion mission on Theorem 1;
reusable infrastructure: MNL choice probabilities and finite-horizon history laws for adaptive policies.

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. https://doi.org/10.1287/opre.2018.1832 ; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880v2
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. https://doi.org/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. https://doi.org/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. https://doi.org/10.1287/mnsc.1030.0147

9 thms2 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Fast Rates for Support Vector Machines Using Gaussian Kernels 2: An Envelope of Order γ and Tsybakov Noise Exponent q Give Geometric Noise Exponent (q+1)γ/dResearch Paper

Motivation

A binary classifier is learned from a sample of a distribution $P$ on $X \times \{-1, 1\}$ , and its quality is measured by its excess classification risk over the Bayes classifier. Without assumptions on $P$ no learning method converges at a uniform rate, so every rate theorem rests on a condition that describes how hard $P$ is. Two such conditions are standard: Tsybakov's noise condition (Tsybakov 2004), which bounds the mass of the region where the label is close to a fair coin flip, and smoothness of the regression function $\eta(x) = P(y = 1 \mid x)$ .

Steinwart and Scovel (arXiv:0708.1838v1, the reprint of Ann. Statist. 35 (2007) 575–607) analyse support vector machines with Gaussian RBF kernels. Their rates rest on a new condition, the geometric noise exponent, which measures how much of the weighted measure $|2\eta - 1|\,dP_X$ lies close to the decision boundary. It is tailored to the approximation properties of the Gaussian kernel and is less familiar than the classical conditions. Theorem 2.6 of the paper connects it to them: an envelope condition on $\eta$ near the decision boundary, together with a Tsybakov exponent, yields an explicit geometric noise exponent. This mission formalizes that theorem.

Setting

Let $X \subset \mathbb R^d$ be compact and let $P$ be a distribution on $X \times \{-1, 1\}$ with marginal $P_X$ and regression function $\eta(x) = P(y = 1 \mid x) \in [0, 1]$ . The classes of $P$ are $X_{-1} = \{\eta < \tfrac12\}$ , $X_1 = \{\eta > \tfrac12\}$ and $X_0 = \{\eta = \tfrac12\}$ , all intersected with $X$ . The distance to the decision boundary is

\tau_x = d(x, X_0 \cup X_1) \text{ on } X_{-1}, \qquad \tau_x = d(x, X_0 \cup X_{-1}) \text{ on } X_1, \qquad \tau_x = 0 \text{ otherwise},

with $d(x, A)$ the Euclidean distance of $x$ to $A$ (equation (7), p. 7).

Tsybakov noise exponent $q \in [0, \infty]$ (Definition 2.2, p. 6): for some $C > 0$ and all sufficiently small $t > 0$ , $P_X(|2\eta - 1| \le t) \le C t^q$ .
Geometric noise exponent $\alpha > 0$ (Definition 2.3, p. 7): for some $C > 0$ ,

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

Envelope of order $\gamma > 0$ (Definition 2.5, p. 8): for some $c_\gamma > 0$ , $|2\eta(x) - 1| \le c_\gamma \tau_x^\gamma$ for $P_X$ -almost all $x \in X$ .

In Lean these are TsybakovNoise, GeometricNoise and Envelope, built on Tau, in the namespace FastRatesSVM.GeomNoise.

Formalization targets

Goal: Theorem 2.6 (p. 8)

If $P$ has an envelope of order $\gamma > 0$ and Tsybakov noise exponent $q \in [0, \infty)$ , then

q \ge 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \frac{(q+1)\gamma}{d}, \qquad 0 \le q < 1 \;\Longrightarrow\; P \text{ has geometric noise exponent } \alpha \text{ for all } 0 < \alpha < \frac{(q+1)\gamma}{d}.

Both clauses are stated, as one conjunction.

Milestones

Display (33), pp. 18–19. Under the Tsybakov bound for all $s > 0$ with constant $C$ and the envelope bound with constant $c_\gamma$ , for all $t > 0$ and $\tau \ge 0$ :

\mathbb E_{P_X}\big(|2\eta - 1|\, e^{-\tau_x^2/t}\big) \le C\tau^{q+1} + \exp\big(-(\tau/c_\gamma)^{2/\gamma} t^{-1}\big).

The $\tau$ -estimate, p. 19. With $\hat a = c_\gamma^{2/\gamma}(q+1)$ , for all small $t > 0$ the equation $\tau^{q+1} = \exp(-(\tau/c_\gamma)^{2/\gamma}t^{-1})$ has a positive solution, and every positive solution satisfies $\tau \le (\hat a\gamma/2)^{\gamma/2}\,(t\ln\frac{1}{\hat a t})^{\gamma/2}$ .
Theorem 2.6, case $0 \le q < 1$ .
Theorem 2.6, case $q \ge 1$ .

Significance

Theorem 2.6 makes the paper's learning rates usable under familiar assumptions. The main rate theorem of the paper (Theorem 2.8) is stated in terms of the geometric noise exponent; through Theorem 2.6 it becomes a rate in terms of a Tsybakov exponent and the order of an envelope, which is a Hölder-type behaviour of $\eta$ at the decision boundary. Example: with $d = 1$ , $X = [-1, 1]$ , $P_X$ uniform and $\eta(x) = (1 + x)/2$ , the distribution has envelope order $1$ and Tsybakov exponent $1$ , hence geometric noise exponent $2$ .

The result is proved in the paper. As far as known, none of it is machine-checked: none of these noise conditions has a Lean formalization, on Prove2Me or in Mathlib. The mission produces the definitions themselves (the class decomposition, $\tau_x$ and the three noise conditions), which any later formalization of margin-based classification rates can import, and a formal proof of the implication. A companion mission of the same series formalizes the paper's rate theorem, which takes the geometric noise exponent as its hypothesis.

Difficulty

The case $0 \le q < 1$ is elementary once the right splitting level is chosen: the expectation is split at a level $\tau$ of $|2\eta - 1|$ , and $\tau$ is then tuned to $t$ . Tuning it requires the asymptotics of the solution of a transcendental equation. This yields every exponent below the critical value $(q+1)\gamma/d$ , but not the critical value itself: a logarithmic factor is lost.

Reaching the critical exponent when $q \ge 1$ is the substantial step. The paper does it with Hölder's inequality for Lorentz spaces $L_{q,\infty}$ and $L_{q',1}$ and an estimate of a nonincreasing rearrangement (display (32)). Mathlib has neither Lorentz spaces nor nonincreasing rearrangements, so this part either builds that infrastructure or replaces it with a direct layer-cake argument against the distribution function of $|2\eta - 1|$ . The obvious approach, the same splitting as for $q < 1$ , does not work: it always loses the logarithm.

Formalization scope

Representation of $P$ . $P$ is given by $\mu = P_X$ , a probability measure on EuclideanSpace ℝ (Fin d) with $\mu(X^c) = 0$ , and a measurable version $\eta$ of the regression function with values in $[0,1]$ everywhere. Every Borel distribution on $X \times \{-1,1\}$ has this form, and the paper defines $\tau_x$ "for some choice of $\eta$ ".
Pinned convention $d(x, \emptyset) := 0$ . The paper leaves $d(x, \emptyset)$ undefined. Lean's Metric.infDist gives $0$ . For Theorem 2.6 both readings give a true statement. Under the reading $\infty$ , the companion statements Theorem 2.7 and Lemma 4.1 are false for a version of $\eta$ with an empty class. The convention is chosen for agreement with the companion mission.
Integrals. All integrals are $[0,\infty]$ -valued Lebesgue integrals of nonnegative integrands (lintegral), so a bound can never hold through a junk value of a non-integrable function.
Added hypotheses. $d \ge 1$ , because the exponent $(q+1)\gamma/d$ divides by $d$ . In the second clause, $\alpha > 0$ : this is the range of Definition 2.3, not a new restriction.
Display (33). It is stated for every $q \ge 0$ , where it holds verbatim, and for $t > 0$ (the page writes $t \ge 0$ , but $t^{-1}$ is undefined at $0$ ). Its hypotheses are the all- $t$ form of (5), which by the remark on p. 6 is equivalent to Definition 2.2 for $q < \infty$ up to the constant, and (10) with its constant named. The page's equality that splits the integral is not stated separately.
Printed slip. The proof on p. 19 ends "for the case $0 < q < 1$ ", while the statement covers $q = 0$ . The milestone is stated for $0 \le q < 1$ ; the argument works verbatim at $q = 0$ .
Small $t$ . In Definition 2.2, "sufficiently small" is a threshold $t_0 \in (0,1)$ . The $\tau$ -estimate has its threshold chosen before $t$ and $\tau$ , and it also states the existence of a solution, which the page presupposes.
No trivializing reading. The hypotheses are satisfiable: the example in Significance meets all of them. $\tau_x$ is not identically $0$ there, since it equals $|x|$ . So the goal cannot hold vacuously.
Not formalized. The Lorentz-space step (30) and the rearrangement estimate (32) are not milestones. Contributions of Lorentz quasi-norms or a layer-cake lemma are welcome as supporting theorems.

The source is arXiv:0708.1838v1, the reprint of the Annals article. Its printed page numbers equal the PDF page numbers, and every page cited here is that number.

Selected references

I. Steinwart, C. Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 575–607, 2007. arXiv reprint: https://arxiv.org/abs/0708.1838 ; DOI: https://doi.org/10.1214/009053606000001226
A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 135–166, 2004. https://doi.org/10.1214/aos/1079120131

9 thms2 active usersReviewed

Dynamic Programming Markov Chain Probability+1·Captain: mikedeng1

An Analysis of Temporal-Difference Learning with Function Approximation 1: Linear TD(λ) Converges with Probability 1 to the Fixed Point of ΠT^(λ), with Error ≤ ‖ΠJ* − J*‖_D/(1 − α(1−λ)/(1−αλ))Research Paper

Motivation

Temporal-difference learning, TD( $\lambda$ ), is the basic algorithm of reinforcement learning for estimating the expected discounted cost of a Markov chain from observed transitions (Sutton, 1988). On large or infinite state spaces it is run with a linear function approximator: the cost-to-go is represented as a weighted sum of $K$ fixed basis functions, and the algorithm updates the weights. With a lookup table (one basis function per state) its convergence follows from general results on contraction mappings. With function approximation that argument breaks down. Before 1996 there were only results on convergence in the mean (Dayan, 1992), sketches restricted to linearly independent feature vectors $\phi(i)$ , and counterexamples in which related algorithms diverge.

Tsitsiklis and Van Roy (MIT report LIDS-P-2322, 1996; IEEE Trans. Automatic Control 42(5), 1997) proved that on-line TD( $\lambda$ ) with linear function approximation converges with probability 1 on finite or countably infinite ergodic chains. They identified the limit as the fixed point of a projected Bellman-type operator $\Pi T^{(\lambda)}$ and bounded its error. This analysis is the reference point for later results: finite-time bounds for linear TD, the off-policy divergence examples, and the gradient-TD family.

Timeline:

1988: Sutton introduces TD( $\lambda$ ) and proves convergence in the mean for TD(0) on absorbing chains with linearly independent features.
1992: Dayan extends convergence in the mean to general $\lambda$ .
1994: Jaakkola, Jordan and Singh, and Tsitsiklis, prove almost-sure convergence for lookup tables, using maximum-norm contraction.
1996: Tsitsiklis and Van Roy prove almost-sure convergence with linear function approximation and the error bound below.

Setting

A Markov chain $i_0, i_1, \dots$ lives on a finite or countably infinite state space $S$ , with transition matrix $P = (p_{ij})$ . A transition from $i$ to $j$ costs $g(i,j)$ , and $\alpha \in (0,1)$ is a discount factor. The cost-to-go is

J^*(i) = E\Big[\sum_{t=0}^\infty \alpha^t g(i_t,i_{t+1}) \,\Big|\, i_0 = i\Big].

Basis functions $\phi_1,\dots,\phi_K : S \to \mathbb R$ give the feature vector $\phi(i) \in \mathbb R^K$ and the approximation $\tilde J(i,r) = r'\phi(i)$ , written $\Phi' r$ as a vector over $S$ .

Starting from an arbitrary $r_0$ , TD( $\lambda$ ) with $\lambda \in [0,1]$ and step sizes $\gamma_t$ forms the eligibility vector $z_t = \sum_{k=0}^t (\alpha\lambda)^{t-k}\phi(i_k)$ and the temporal difference $d_t = g(i_t,i_{t+1}) + \alpha\phi(i_{t+1})'r_t - \phi(i_t)'r_t$ , and updates $r_{t+1} = r_t + \gamma_t d_t z_t$ .

Let $\pi$ be the invariant distribution, $D = \mathrm{diag}(\pi)$ , $\|J\|_D^2 = \sum_i \pi(i)J(i)^2$ , and $L_2(S,D) = \{J : \|J\|_D < \infty\}$ . Write $\Pi = \Phi'(\Phi D\Phi')^{-1}\Phi D$ for the $D$ -orthogonal projection onto $\{\Phi'r\}$ . The operator $T^{(\lambda)}$ averages $m$ -stage truncated costs:

(T^{(\lambda)}J)(i) = (1-\lambda)\sum_{m=0}^\infty \lambda^m E\Big[\sum_{t=0}^m \alpha^t g(i_t,i_{t+1}) + \alpha^{m+1}J(i_{m+1}) \,\Big|\, i_0 = i\Big],

for $\lambda < 1$ , and $T^{(1)}J = J^*$ . The paper makes four assumptions:

the chain has a unique invariant distribution with $\pi(i) > 0$ , $E_0[g^2] < \infty$ , and finite $J^*$ ;
the $\phi_k$ are linearly independent with $E_0[\phi_k^2] < \infty$ ;
polynomial moment growth and summable mixing conditions, relative to coordinates $\sigma(i) \in \mathbb R^N$ of the states;
nonnegative, nonincreasing step sizes with $\sum\gamma_t = \infty$ and $\sum\gamma_t^2 < \infty$ .

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumptions 1–4: $J^* \in L_2(S,D)$ ; for every $\lambda \in [0,1]$ , TD( $\lambda$ ) converges with probability 1, from every initial state and every $r_0$ , to a vector $r^*$ ; $r^*$ is the unique solution of

\Pi T^{(\lambda)}(\Phi' r^*) = \Phi' r^*;

and

\|\Phi' r^* - J^*\|_D \le \frac{\|\Pi J^* - J^*\|_D}{1 - \alpha(1-\lambda)/(1-\lambda\alpha)}.

Milestones

Lemma 1: $\|PJ\|_D \le \|J\|_D$ .
Lemma 2: $J^*$ is finite, lies in $L_2(S,D)$ , and $J^* = \sum_t(\alpha P)^t\bar g$ .
Lemma 3: $T^{(\lambda)}$ maps $L_2(S,D)$ into itself and has a closed-form series.
Lemma 4: $T^{(\lambda)}$ is a $\|\cdot\|_D$ -contraction with modulus $\alpha(1-\lambda)/(1-\alpha\lambda)$ .
Lemma 5: $\Pi T^{(\lambda)}$ has a unique fixed point $\Phi'r^*$ , with the error bound above.
Lemma 6: steady-state moments of $\phi$ and $z_t$ .
Lemma 7: the steady-state mean step is $E_0[s(r,X_t)] = \Phi D(T^{(\lambda)}(\Phi'r) - \Phi'r)$ .
Lemma 8: $(r - r^*)'E_0[s(r,X_t)] < 0$ for $r \neq r^*$ .
Theorem 2: a stochastic approximation theorem with Markov noise.
§6: $A = E_0[A(X_t)]$ is negative definite and $Ar^* + b = 0$ .

Significance

Theorem 1 says that TD( $\lambda$ ), run on-line along a single trajectory, converges for every $\lambda$ , and that its limit has a precise meaning: the fixed point of the projected operator. The error bound shows that as $\lambda \to 1$ the limit approaches the best approximation $\Pi J^*$ , and that for smaller $\lambda$ the error can grow by at most a factor $(1-\alpha\lambda)/(1-\alpha)$ . The analysis also explains the failures of related schemes: the projection and the contraction must use the same norm, $\|\cdot\|_D$ , which holds only when states are sampled along the chain.

The result is proved on paper. To our knowledge no part of it has been machine-checked; it is not in Mathlib or on this platform. This mission produces:

a Lean model of countable-state Markov chains with costs, their path law, the weighted space $L_2(S,D)$ and the projection $\Pi$ , which is reusable for later work on linear TD, LSTD and approximate policy evaluation;
the deterministic layer (Lemmas 1–5, 7, 8), which is self-contained functional analysis on $L_2(S,D)$ ;
Theorem 2, a stochastic approximation theorem with Markov noise, which the paper quotes from Benveniste, Métivier and Priouret (1987) without proof. A formal proof of it would be a library result in its own right.

Difficulty

The obvious approach treats TD( $\lambda$ ) as a noisy version of the deterministic iteration $\bar r_{t+1} = \bar r_t + \gamma_t\Phi D(T^{(\lambda)}(\Phi'\bar r_t) - \Phi'\bar r_t)$ . It fails at the noise. The increments $s(r_t,X_t)$ are driven by the Markov process $X_t = (i_t,i_{t+1},z_t)$ , not by independent samples. They are not martingale differences, and on an infinite state space they are unbounded. The standard ODE method with martingale-difference noise therefore does not apply, and the bias from Markov dependence must be controlled through the mixing and growth conditions of Assumption 3. The algorithm also starts with $z_{-1} = 0$ rather than in steady state, so the steady-state identities of Lemmas 6–8 must be transferred to the actual trajectory. The contraction argument needs care for a different reason: $\Pi$ is a nonexpansion of $\|\cdot\|_D$ only because $D$ is the invariant distribution of the same chain that defines $T^{(\lambda)}$ .

Formalization scope

$S$ is a countable type with the discrete $\sigma$ -algebra, $P$ a Markov kernel ( $p_{ij} = P(i)(\{j\})$ , $P^m$ the kernel power), and the path law of the chain is Mathlib's Ionescu–Tulcea measure Kernel.trajMeasure. Standing conventions:

$\alpha \in (0,1)$ and $\lambda \in [0,1]$ ;
"with probability 1" is almost-sure convergence under the path law from each deterministic initial state;
$J^*$ and $T^{(\lambda)}$ are defined by the page's path expectations, not by the series of Lemmas 2 and 3;
$L_2(S,D)$ membership is summability of $\pi(i)J(i)^2$ ;
Assumption 1(c) means absolute integrability of the discounted cost series;
vector norms are Euclidean and matrix norms Frobenius (equivalent to the induced norm and used only under existential constants);
$(\Phi D\Phi')^{-1}$ is Lean's matrix inverse, invertible under Assumptions 1(a) and 2;
the steady-state process of Lemmas 6–8 is any two-sided chain on a probability space with the stationary finite-dimensional distributions.

Lean's integral of a non-integrable function and sum of a non-summable series are $0$ . A trivializing formalization is excluded by stating every expectation and series with its integrability or summability: "well defined and finite" is always a conjunct or a hypothesis, never left to junk values.

The development needs the following:

Markov-chain path measures and stationary two-sided chains;
Bochner integrals of vector-valued functions;
the Cauchy–Schwarz inequality on $L_2(S,D)$ ;
a Markov-noise stochastic approximation theorem.

Contributions are welcome at every level: proofs of the deterministic lemmas, a construction of the stationary chain from $\pi$ and $P$ (showing that the steady-state hypotheses are satisfiable), and a proof of Theorem 2 or a stronger stochastic approximation result that implies it.

Selected references

J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, MIT LIDS report LIDS-P-2322, 1996; IEEE Transactions on Automatic Control 42(5):674–690, 1997. https://doi.org/10.1109/9.580874
A. Benveniste, M. Métivier and P. Priouret, Adaptive Algorithms and Stochastic Approximations, Springer, 1990 (French original 1987). https://doi.org/10.1007/978-3-642-75894-2
R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3:9–44, 1988. https://doi.org/10.1007/BF00115009
P. Dayan, The convergence of TD(λ) for general λ, Machine Learning 8:341–362, 1992. https://doi.org/10.1007/BF00992701
T. Jaakkola, M. I. Jordan and S. P. Singh, On the convergence of stochastic iterative dynamic programming algorithms, Neural Computation 6(6):1185–1201, 1994. https://doi.org/10.1162/neco.1994.6.6.1185
J. N. Tsitsiklis, Asynchronous stochastic approximation and Q-learning, Machine Learning 16:185–202, 1994. https://doi.org/10.1007/BF00993306

13 thms2 active usersReviewed

Probability Statistics·Captain: mikedeng1

Consistent Nonparametric Regression I: Conditions (1)–(5) on a Sequence of Weights Are Sufficient for Consistency, and Consistency Forces Them Back (Theorem 1)Research Paper

Motivation

Nonparametric regression estimates the conditional mean $E(Y\mid X=x)$ of a real response $Y$ given a predictor $X\in\mathbb R^d$ without assuming that it belongs to a finite-dimensional family. Most practical estimators of this kind are local averages: kernel estimators (Nadaraya 1964, Watson 1964), nearest-neighbor rules (Cover and Hart 1967), and their many variants all predict at a point $X$ by a weighted average $\sum_i W_{ni}(X)Y_i$ of the observed responses, with weights that depend only on the predictors.

C. J. Stone's 1977 paper in the Annals of Statistics (DOI 10.1214/aos/1176343886) asked when such a rule is consistent: when it converges to the true regression function in $L^r$ for every joint distribution of $(X,Y)$ with $E|Y|^r<\infty$ , without smoothness or moment assumptions beyond that. Its Theorem 1 answers the question in terms of five conditions on the weights alone. The result is the standard starting point for distribution-free regression theory; it is the first theorem of the monograph of Györfi, Kohler, Krzyżak and Walk (2002), where it is called Stone's theorem, and it underlies the universal consistency of nearest-neighbor, kernel and partitioning estimates.

Setting

Let $\mu$ be a probability measure on $\mathbb R^d$ and let $X, X_1, X_2,\dots$ be independent with law $\mu$ . A sequence of weights $\{W_n\}$ assigns to each $n\ge1$ and each point $(x,x_1,\dots,x_n)$ real numbers

W_{ni}(x) = W_{ni}(x, x_1,\dots,x_n),\qquad 1\le i\le n .

The weights are nonnegative if every $W_{ni}\ge0$ and probability weights if in addition $\sum_i W_{ni}(x)=1$ .

When $(X,Y),(X_1,Y_1),(X_2,Y_2),\dots$ are i.i.d. with $Y$ real valued, the estimate of $E(Y\mid X)$ is

\hat E_n(Y\mid X) = \sum_{i=1}^n W_{ni}(X)\,Y_i .

The sequence $\{W_n\}$ is consistent if, for every such joint distribution with $X$ -marginal $\mu$ and every $r\ge1$ with $E|Y|^r<\infty$ ,

\lim_{n\to\infty} E\big|\hat E_n(Y\mid X) - E(Y\mid X)\big|^r = 0 .

The five conditions of Theorem 1 are:

there is a $C\ge1$ with $E\sum_i|W_{ni}(X)|f(X_i)\le C\,Ef(X)$ for every nonnegative Borel $f$ and every $n\ge1$ ;
there is a $D\ge1$ with $P\big(\sum_i|W_{ni}(X)|\le D\big)=1$ for every $n\ge1$ ;
$\sum_i|W_{ni}(X)|\,I_{\{\|X_i-X\|>a\}}\to0$ in probability for every $a>0$ ;
$\sum_i W_{ni}(X)\to1$ in probability;
$\max_i|W_{ni}(X)|\to0$ in probability.

Formalization targets

Goal: Theorem 1 (p. 598)

\text{(1)–(5)}\ \Longrightarrow\ \{W_n\}\text{ consistent},

and conversely, if $\{W_n\}$ is consistent, then (4) and (5) hold; if moreover $W_n\ge0$ for all $n\ge1$ , then (3) holds; and if $W_n\ge0$ and (2) holds, then (1) holds. The goal is the full theorem, both directions, as one statement.

Milestones (§10, pp. 607–610)

Proposition 1: under (1)–(3), $E\sum_i|W_{ni}(X)||f(X_i)-f(X)|^r\to0$ whenever $r\ge1$ and $E|f(X)|^r<\infty$ .
Propositions 2 and 3: for nonnegative weights (respectively for $W_{ni}^2$ ), bounds on $\liminf$ and $\limsup$ of $E\sum_i W_{ni}(X)f(X_i)$ in terms of constants $M_n\le\sum_i W_{ni}(X)\le N_n$ holding with probability tending to one.
Proposition 5: under (1)–(4), $\sum_i W_{ni}(X)f(X_i)\to f(X)$ in $L^r$ .
Proposition 6: nonnegative weights that reproduce every bounded continuous $f$ in probability satisfy (3).
Proposition 7: if $\limsup_n E\sum_i W_{ni}(X)f(X_i)<\infty$ for every integrable nonnegative $f$ , a single pair $(n_0, C)$ works for all $f$ .
Proposition 8: if $\sum_i W_{ni}(X)Y_i\to0$ in probability for independent standard normal $Y_i$ , then $\sum_i W^2_{ni}(X)\to0$ in probability.

Significance

The result. Theorem 1 reduces a statement about all joint distributions of $(X,Y)$ to properties of the weights under the law of $X$ alone. For probability weights, conditions (2) and (4) hold automatically, and (1), (3), (5) become necessary and sufficient (Corollary 1). This is how Stone proves that nearest-neighbor weights with suitably vanishing coefficients are universally consistent (Theorem 2 of the paper), and how consistency transfers to estimators of conditional quantiles and to approximate Bayes rules in classification and decision problems (Sections 7–8). Condition (1), the only condition that is not a convergence statement, is the one that later work on kernel and partitioning estimates had to verify by geometric covering arguments.

Formalizing it. The theorem is proved in the paper and in textbooks; it has no machine-checked proof that we know of. A formalization produces a reusable criterion: any later development of local-averaging estimators can discharge consistency by checking five conditions about the predictor distribution. The supporting propositions are of independent use: Proposition 1 is an $L^r$ approximation lemma for weighted empirical averages, and Proposition 7 is a uniform-boundedness principle for sequences of positive operators on $L^1(\mu)$ .

Difficulty

The sufficiency half combines three ingredients that have to fit together at the level of measure theory: approximation of an arbitrary $L^r$ function by continuous functions with compact support, uniformly over $n$ through condition (1); a variance computation for the noise term that conditions on the predictors; and a truncation argument to pass from bounded responses and $r=2$ to all $r\ge1$ . The natural first idea, to apply a weak law of large numbers to $\sum_i W_{ni}(X)Y_i$ , fails because the weights are dependent on all of $X, X_1,\dots,X_n$ and are not identically distributed.

The necessity half needs separate arguments for each condition: a test-function argument with bounded continuous $f$ for (3), a contradiction argument summing a sequence of functions $f_\nu$ for (1), and a Gaussian anti-concentration argument for (5), which is where the auxiliary normal variables of the paper enter.

Formalization scope

Data. The i.i.d. sequence $X, X_1, X_2,\dots$ is the coordinate process of the product measure $\mu^{\otimes\mathbb N}$ on $(\mathbb R^d)^{\mathbb N}$ , coordinate $0$ being $X$ . "Whenever $(X,Y),(X_1,Y_1),\dots$ are i.i.d." is encoded by quantifying over every Markov kernel $\kappa$ from $\mathbb R^d$ to $\mathbb R$ (the conditional law of $Y$ given $X$ ); the pairs are the coordinates of $(\mu\otimes\kappa)^{\otimes\mathbb N}$ and $E(Y\mid X=x)=\int y\,\kappa(x,dy)$ . Every joint law with $X$ -marginal $\mu$ arises in this way.
Standing assumptions. The paper's assumption (p. 596) that independent standard normal variables are available on the probability space is supplied by the kernel $\kappa\equiv N(0,1)$ . The weights are assumed jointly Borel in $(x,x_1,\dots,x_n)$ ; the paper treats $W_{ni}(X)$ as random variables without saying so.
Conventions. Expectations of nonnegative quantities (in (1), in $E|Y|^r$ , in the $L^r$ distances and in Propositions 1–3, 5, 7) are lower Lebesgue integrals in $[0,\infty]$ , and the $\liminf$ / $\limsup$ of Propositions 2, 3, 7 are in $[0,\infty]$ , so no infinite expectation is silently read as $0$ . Convergence in probability is Mathlib's TendstoInMeasure. Sample indices are $0$ -based. Conditions on individual $n$ are stated for $n\ge1$ .
Correction of the print. The definition of consistency on p. 597 prints " $r>1$ "; the proof of Theorem 1 (p. 611, (13)) and the rest of the paper work with every $r\ge1$ , which is the formalized reading.
Not a trivialization. The goal quantifies over every conditional law $\kappa$ and every real $r\ge1$ ; a version for bounded $Y$ or for $r=2$ only would be weaker than the theorem, and the converse parts conclude the conditions (1), (3), (4), (5) themselves.
Infrastructure. A complete development needs products of probability measures and their coordinate processes, Lusin-type density of compactly supported continuous functions in $L^r(\mu)$ , conditional variance computations given finitely many coordinates, and the Gaussian tail bound. These pieces are reusable well beyond this mission. Proofs of individual propositions, and of either direction of Theorem 1 separately, are welcome contributions.

Selected references

C. J. Stone, Consistent nonparametric regression, Ann. Statist. 5(4), 595–645, 1977. https://doi.org/10.1214/aos/1176343886
L. Györfi, M. Kohler, A. Krzyżak, H. Walk, A Distribution-Free Theory of Nonparametric Regression, Springer, 2002. https://doi.org/10.1007/b97848
T. M. Cover, P. E. Hart, Nearest neighbor pattern classification, IEEE Trans. Inform. Theory 13(1), 21–27, 1967. https://doi.org/10.1109/TIT.1967.1053964
E. A. Nadaraya, On estimating regression, Theory Probab. Appl. 9(1), 141–142, 1964. https://doi.org/10.1137/1109020
G. S. Watson, Smooth regression analysis, Sankhyā Ser. A 26(4), 359–372, 1964. https://www.jstor.org/stable/25049340

9 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 1: WM Makes at Most log(w_init/w_fin)/log(2/(1+β)) Mistakes on Any SequenceResearch Paper

Motivation

In online prediction, a learner makes a forecast before seeing the next label. A collection of other forecasters may offer useful advice, but the learner need not know beforehand which forecaster will perform well. Littlestone and Warmuth's Weighted Majority Algorithm (WM) gives a deterministic way to combine such advice. Its guarantees hold for every finite sequence of instances and labels, including sequences chosen without any probability model. That worst-case setting is useful when the reliability of the forecasters can change or when no data-generating distribution has been justified. The paper develops WM and several variants; this mission isolates its basic mistake bound. Littlestone and Warmuth, 1994.

Setting

A finite pool has $n$ members, each of which predicts either $0$ or $1$ on every trial. The true label on trial $t$ is $\rho_t\in\{0,1\}$ , and member $i$ predicts $x_{t,i}\in\{0,1\}$ . The master prediction is $\lambda_t\in\{0,1\}$ . Pool members may themselves be learning algorithms, so their predictions may reflect all earlier labels. The mission treats their prediction vectors and the labels as arbitrary finite sequences; no independence or stationarity is assumed.

Each member begins with a strictly positive real weight $w_{0,i}$ . Before trial $t$ , let $w_{t,i}$ be its current weight. For $b\in\{0,1\}$ , let $q_{t,b}$ be the sum of weights of members predicting $b$ . WM predicts the value with the larger backing total. When the two totals tie, either binary prediction is allowed. After the label is revealed, WM changes weights only if its own prediction was wrong. On such a trial, each member that predicted the wrong label has its weight multiplied by a fixed factor $\beta$ with $0\le\beta<1$ ; every other member retains its weight. If WM predicted correctly, every weight stays as it was. This is the version of the algorithm stated in §1 of the paper. A footnote there says the bounds also apply to the variant that updates on every trial. Littlestone and Warmuth, 1994, p. 215.

Write $W_t=\sum_i w_{t,i}$ for the total pool weight at a trial boundary. Thus $W_0=w_{\mathrm{init}}$ and $W_T=w_{\mathrm{fin}}$ after $T$ trials. Let $m$ count the trials with $\lambda_t\ne\rho_t$ . The default initial weights in the paper are all one, but its Theorem 2.1 permits arbitrary positive initial weights. Littlestone and Warmuth, 1994, pp. 220–221.

Formalization targets

The two milestones state the weight facts used immediately before and within Theorem 2.1. First, on each trial where WM errs,

W_{t+1}\le \frac{1+\beta}{2}W_t.

Across the whole sequence, with $m$ master mistakes, the corresponding estimate is

W_T\le W_0\left(\frac{1+\beta}{2}\right)^m.

The goal is the paper's Theorem 2.1, retaining its explicit constant:

m\le \frac{\log(W_0/W_T)} {\log\!\left(2/(1+\beta)\right)} \qquad\text{when }W_T>0.

The logarithm base is immaterial because the same base occurs above and below the fraction. The paper explicitly uses this convention for ratios of logarithms. The positive-final-weight condition represents the paper's statement that the displayed logarithmic bound is vacuous when all weight has vanished, which can happen for $\beta=0$ . The whole-sequence weight estimate remains meaningful in that case. Littlestone and Warmuth, 1994, pp. 220–221.

Significance

The result limits the mistakes of a master predictor without assigning probabilities to the predictions or labels. It relates a visible property of the run, the reduction of total weight, to the number of master errors. Later bounds in the paper use this starting point to compare WM with an individual pool member and to analyze related algorithms; this mission fixes the initial, exact-constant result on which those comparisons rest. The $\beta=0$ case includes the paper's Halving Algorithm interpretation when initial weights are equal. Littlestone and Warmuth, 1994, pp. 215, 221–222.

The mathematical theorem is proved in the 1994 paper. The remaining task here is to represent its algorithm and finite-sequence bound in Lean and supply machine-checked proofs. A complete development would give later formalizations a reusable finite-pool voting and weight-update model, along with a checked potential estimate. The local draft statements compile; their proofs remain open. A separate, sorry-free local check constructs a run for every finite prediction and label sequence with a nonempty pool and valid weights and parameter, so the quantified run relation has witnesses.

Difficulty

The master can be wrong even when some pool members are right, and members may change their predictions over time. Counting one member's errors therefore does not directly control the master's error count. The exact contraction constant also depends on which side of a weighted vote the master chose, including the permitted tie case. When $\beta=0$ , a single mistake can erase all weight backing the wrong label, so the logarithmic expression must be interpreted with care if no positive weight remains. These are features of the stated algorithm, rather than assumptions about how the sequence was generated.

Formalization scope

The formalization indexes pool members by Fin n and trials by Fin T. Booleans represent binary predictions and labels; weights and $\beta$ are real. A WM run is a relation on the full sequence of weights and master predictions, admitting every choice at a tied vote. Its update rule changes weights only after a master mistake, scales exactly the members that disagreed with the label, and leaves all other weights unchanged. Theorems require $0\le\beta<1$ and strictly positive initial member weights. The goal additionally requires $W_T>0$ , while the two weight inequalities permit $W_T=0$ . Natural logarithms instantiate the paper's common-base logarithm convention. Finite sums and a finite mistake count match the paper's finite-sequence convention.

The statement ranges over arbitrary pool predictions and labels, so it cannot be satisfied merely by selecting an easy input sequence. The run relation allows both legal outcomes of a tie; selecting one favorable tie rule would weaken the target. The sorry-free run-existence check also rules out a vacuous theorem caused by an inconsistent update relation. The paper's update-on-every-trial variant, its member-specific corollaries, and its later algorithms are outside this mission's goal.

A completed formalization needs finite sums of real weights, cardinalities of finite sets of mistake trials, a finite induction over trial boundaries, and real logarithm inequalities. The run definition and the first two bounds can be reused in the later parts of this paper's formalization. Contributions that prove the exact stated milestones or supply supporting facts about legal runs and nonnegative weights are within 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.

4 thms2 active usersReviewed

Dynamic Programming Probability Reinforcement Learning·Captain: mikedeng1

Technical Note: Q-Learning: With Bounded Rewards and Learning Rates with Σα = ∞, Σα² < ∞ at Every State–Action Pair, Tabular Q-Learning Converges to Q* with Probability 1Research Paper

Motivation

Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.

Timeline.

1989: Watkins' thesis introduces Q-learning and sketches a convergence argument.
1992: Watkins and Dayan publish the proof via the action-replay process, for bounded rewards, discount $0<\gamma<1$ and learning rates satisfying condition (3) at every state–action pair.
1994: Jaakkola, Jordan and Singh (Neural Computation 6) and Tsitsiklis (Machine Learning 16) give proofs through stochastic approximation for asynchronous iterations, with predictable random choices of state, action and step.
Later work (Szepesvári 1997; Even-Dar and Mansour 2003) quantifies the convergence rate.

Setting

A finite controlled Markov process has a finite state set $X$ , a finite nonempty action set $\mathfrak A$ (the same in every state), mean rewards $\mathcal R_x(a)$ and transition probabilities $P_{xy}[a]$ . Rewards received $s$ steps later are discounted by $\gamma^s$ with $0<\gamma<1$ . The optimal action-value function $Q^*$ is the unique solution of the Bellman optimality equation

Q^*(x,a)=\mathcal R_x(a)+\gamma\sum_y P_{xy}[a]\max_b Q^*(y,b).

In the $n$ -th episode the agent observes a state $x_n$ , performs an action $a_n$ , observes the next state $y_n$ and a reward $r_n$ of mean $\mathcal R_{x_n}(a_n)$ , and updates its table with a learning rate $\alpha_n$ :

Q_n(x,a)=\begin{cases}(1-\alpha_n)Q_{n-1}(x,a)+\alpha_n\bigl[r_n+\gamma\max_b Q_{n-1}(y_n,b)\bigr]&(x,a)=(x_n,a_n),\\ Q_{n-1}(x,a)&\text{otherwise,}\end{cases}

from given initial values $Q_0$ . Episodes need not form a single trajectory. Writing $n^i(x,a)$ for the episode of the $i$ -th visit to $(x,a)$ , the learning-rate condition is

\sum_{i=1}^\infty\alpha_{n^i(x,a)}=\infty,\qquad\sum_{i=1}^\infty\bigl[\alpha_{n^i(x,a)}\bigr]^2<\infty\qquad\forall x,a.\tag{3}

The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states $\langle x,n\rangle$ (a real state and a level $n$ ), in which taking $a$ at $\langle x,n\rangle$ replays a randomly chosen earlier episode that tried $a$ in $x$ , emitting its reward and dropping to the level below that episode. Its expected one-step reward is $\mathcal R^{(n)}_x(a)$ and its aggregated transition probabilities are $P^{(n)}_{xy}[a]$ .

Formalization targets

Goal: the Theorem (p. 282)

Given bounded rewards $|r_n|\le\mathcal R$ , learning rates $0\le\alpha_n<1$ and (3),

Q_n(x,a)\to Q^*(x,a)\quad\text{as }n\to\infty,\ \forall x,a,\ \text{with probability }1.

Milestones (the paper's appendix, in attack order)

Lemma A (p. 288): $Q_n(x,a)=Q^*_{\mathrm{ARP}}(\langle x,n\rangle,a)$ for all $a,x$ and $n\ge0$ .
Lemma B.1 (p. 289): the values of $s$ actions with and without a continuation policy differ by at most $\gamma^s\mathcal R/(1-\gamma)$ .
Lemma B.2 (p. 289): started high enough, the ARP strays below any level $l$ within $s$ actions with arbitrarily small probability.
The stochastic-convergence theorem quoted in the proof of B.3 (p. 290): $X_{n+1}=X_n+\beta_n(\xi_n-X_n)$ with $\sum\beta_n=\infty$ , $\sum\beta_n^2<\infty$ and bounded $\xi_n$ of mean $\Xi$ converges to $\Xi$ almost surely.
Lemma B.3 (p. 290): almost surely $P^{(n)}_{xy}[a]\to P_{xy}[a]$ and $\mathcal R^{(n)}_x(a)\to\mathcal R_x(a)$ .
Lemma B.4 (p. 291): rewards within $\eta$ and transition rows within $\eta/\mathcal R$ give values of $s$ actions within $\eta s(s+1)/2$ .

A further item states that the optimality equation has exactly one solution for $0\le\gamma<1$ .

Significance

The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD( $\lambda$ ), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.

Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.

Difficulty

The update touches one table entry at a time, at random times chosen by the agent, and its target $r_n+\gamma\max_b Q_{n-1}(y_n,b)$ depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize $Q_n$ as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.

Formalization scope

Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:

$X$ and $\mathfrak A$ are Fintypes with decidable equality, $\mathfrak A$ is nonempty, and $\max_b$ is Finset.sup'. The process is a structure with R x a $=\mathcal R_x(a)$ and P x a y $=P_{xy}[a]$ , rows nonnegative and summing to $1$ .
$Q^*$ enters the goal through the predicate IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.
Lean index $n$ is the paper's episode $n\ge1$ ; index $0$ of the episode data is unused and qIter … 0 $=Q_0$ .
Condition (3) is written over episodes: the learning rate charged to $(x,a)$ at episode $n$ is $\alpha_n$ if $(x_n,a_n)=(x,a)$ and $0$ otherwise; its partial sums tend to $+\infty$ and its squares are summable. This equals (3) and forces infinitely many visits.
Probability model (pinned). The paper describes it in words only. On a filtered probability space, $x_n,a_n,\alpha_n$ are $\mathcal F_{n-1}$ -measurable, $y_n,r_n$ are $\mathcal F_n$ -measurable, $\Pr[y_n=y\mid\mathcal F_{n-1}]=P_{x_ny}[a_n]$ , $\mathbb E[r_n\mid\mathcal F_{n-1}]=\mathcal R_{x_n}(a_n)$ , $|r_n|\le\mathcal R$ , $0\le\alpha_n<1$ , and (3) holds almost surely. Fixed episode schedules with independent outcomes are a special case.
The ARP deck at level $n$ includes card $n$ (as in the card game and Lemma A's proof); $P^{(n)}$ keeps the printed range of levels $1,\dots,n-1$ ; ARP optimality is over deterministic Markov policies of the ARP. Finite action sequences are lists of actions with $0$ terminal reward.
Corrections disclosed in the items. B.1 is stated with $\le$ (the page's strict inequalities fail for a constant reward). B.4 assumes closeness of transition rows in $\ell^1$ and $s\ge1$ : with the page's entrywise closeness the printed constant is false once $|X|\ge4$ . The stochastic-convergence theorem is read with conditional mean $\Xi$ and adapted steps.

Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.

The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.

Selected references

C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292. https://doi.org/10.1023/A:1022676722315
C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989.
T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994), 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. https://doi.org/10.1007/BF00993306
H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8

8 thms2 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 6: Under the Weak Independence Condition, the Randomized Master WMR Has E(m) ≤ E(ln(w_init/w_fin))/(1−β)Research Paper

Motivation

Prediction with expert advice asks a learner to predict a binary label in each of a sequence of trials, having seen the predictions of a pool of $n$ prediction algorithms (the experts), and to make not many more mistakes than the best of them, with no probabilistic assumption on how the instances and labels are generated. Littlestone and Warmuth's Weighted Majority Algorithm (Littlestone, Warmuth 1994) maintains a weight for each pool member, predicts by a weighted vote, and shrinks the weights of members that err. Its mistake bounds are the origin of the multiplicative-weights method used throughout online learning, game theory and optimization (Arora, Hazan, Kale 2012).

A deterministic master with binary predictions can be forced to err in every trial in which the weight is split evenly, which costs it a factor of about two against the best expert. Section 6 of the paper introduces a randomized master, WMR, which predicts $1$ with probability equal to the weighted average prediction of the pool. Theorem 6.1 bounds its expected number of mistakes under a precisely stated condition on how its randomization interacts with the choice of instances and labels.

Timeline:

1989: Littlestone and Warmuth's technical report and FOCS paper introduce the Weighted Majority Algorithm and its randomized variant.
1991: Maass independently analyses the case $\beta = 0$ with binary pool predictions and a lazy update ([Maa91], cited in the paper).
1994: the journal version states the weak independence condition and proves Theorem 6.1 (p. 240).
1997: Freund and Schapire's Hedge algorithm recasts the randomized master as a distribution over experts in a decision-theoretic setting (Freund, Schapire 1997).

Setting

A pool of $n$ algorithms is run for $t$ trials on a probability space $(\Omega, \mathcal F, P)$ . In trial $j$ the pool member $i$ predicts $x_i^{(j)} \in [0,1]$ , the label is $\rho^{(j)} \in \{0,1\}$ , and the master predicts $\lambda^{(j)} \in \{0,1\}$ . All of these are random variables; deterministic sequences are a special case. Write $x^{(j)} = (x_1^{(j)}, \dots, x_n^{(j)})$ .

Each member carries a weight. The initial weights $w_i^{(1)}$ are positive, and the update step (5.1) multiplies the weight of member $i$ in trial $j$ by a factor $F$ that depends on $\beta$ , $x_i^{(j)}$ and $\rho^{(j)}$ :

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

where $0 \le \beta < 1$ and $0^0 = 1$ . WMR updates in every trial. Let $s^{(j)} = \sum_i w_i^{(j)}$ , so $s^{(1)} = w_{\mathrm{init}}$ and $s^{(t+1)} = w_{\mathrm{fin}}$ , and let

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

be the weighted average prediction. WMR predicts $1$ with probability $\gamma^{(j)}$ . Its number of mistakes is $m = \sum_{j=1}^t |\lambda^{(j)} - \rho^{(j)}|$ .

The weak independence condition (p. 238) requires, for $j = 1, \dots, t$ ,

\mathbf E\big(\lambda^{(j)} \,\big|\, (x^{(1)},\rho^{(1)}), \dots, (x^{(j)},\rho^{(j)})\big) = \gamma^{(j)} \quad \text{almost surely}.

The conditioning includes the current predictions of the pool and the current label. It allows instances and labels to depend on the master's past predictions, and it holds, for instance, when WMR draws one uniform number $r \in [0,1]$ and predicts $1$ whenever $\gamma^{(j)} \ge r$ , provided the instances and labels are generated independently of $r$ .

Formalization targets

Goal: Theorem 6.1

Under the weak independence condition, and with $w_{\mathrm{fin}} > 0$ almost surely,

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

The statement fixes neither the pool, nor the update factors within (5.1), nor the distribution of instances and labels.

Milestone: expected mistakes equal expected loss of the weighted average

The step of the proof on p. 240: under the weak independence condition, $\mathbf E(|\lambda^{(j)}-\rho^{(j)}| \mid \mathcal F_j) = |\gamma^{(j)}-\rho^{(j)}|$ almost surely, and hence

\mathbf E(m) = \mathbf E\Big(\sum_{j=1}^t |\gamma^{(j)}-\rho^{(j)}|\Big).

Significance

Theorem 6.1 gives the randomized master the same bound that Theorem 5.2 gives the deterministic master WMC, whose predictions are allowed to lie in $[0,1]$ . With equal initial weights, $\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}) \le \ln n + m_i \ln(1/\beta)$ for every pool member $i$ with total loss $m_i$ , and the bound yields Corollary 6.1 (p. 241): $\mathbf E(m) \le (\ln n + \mathbf E(m_i)\ln(1/\beta))/(1-\beta)$ . For $\beta$ close to $1$ this is better by nearly a factor of two than the bound for the deterministic binary master WMG. The weak independence condition is also what makes the bound valid against labels that adapt to the master's past predictions, which is the setting of later regret analyses.

The result is proved in the paper; this mission produces a machine-checked version. The platform has proofs of the randomized weighted majority bound in the form of Hazan's Lemma 1.4 and of Mohri et al.'s Theorem 8.4, but both state an expectation over the algorithm's internal distribution with deterministic data, unit weights and one fixed update rule. Neither covers random instances and labels, the conditional-expectation condition, or the whole class of updates (5.1).

Difficulty

The pathwise part of the argument is the loss bound for the weighted average (Lemma 5.3, posed in the companion mission on WMC). The new difficulty is probabilistic. The predictions, labels and weights are random and may depend on each other across trials, so the mistake indicator $|\lambda^{(j)}-\rho^{(j)}|$ cannot be replaced by $|\gamma^{(j)}-\rho^{(j)}|$ pointwise. The replacement holds only after conditioning on the $\sigma$ -algebra $\mathcal F_j$ , and requires that $\rho^{(j)}$ is $\mathcal F_j$ -measurable and binary, so that the indicator is affine in $\lambda^{(j)}$ . A reading that conditions on less (dropping the current label) or uses unconditional expectations does not support this step when the label depends on earlier randomness.

A second difficulty is that $\mathbf E(\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}))$ may be infinite: the weights can become arbitrarily small with positive probability.

Formalization scope

The pool is Fin n; trials are indexed from $0$ to $t-1$ , so totalWeight … 0 is $w_{\mathrm{init}}$ and totalWeight … t is $w_{\mathrm{fin}}$ . The probability space is a measure P with IsProbabilityMeasure P. Predictions, labels and master predictions are real-valued measurable random variables; pool predictions lie in $[0,1]$ and labels and master predictions in $\{0,1\}$ on every sample path. Initial weights are deterministic and positive. The update factor of member $i$ in trial $j$ is a measurable function $F_{j,i}(x, r)$ of the member's prediction and the label, satisfying (5.1) on every sample path; the weights are computed from it, so they are random variables determined by the predictions and labels. $\mathcal F_j$ is the supremum of the $\sigma$ -algebras generated by the pairs $(x^{(k)}, \rho^{(k)})$ , $k \le j$ , and the weak independence condition is stated with Mathlib's conditional expectation P[λ j | 𝓕 j].

Expectations in the goal are lower Lebesgue integrals in $[0,\infty]$ , so the right-hand side may be $+\infty$ and no integrability of the logarithm is assumed. The hypothesis $w_{\mathrm{fin}} > 0$ almost surely excludes the case where the paper's bound is infinite and Lean's $\ln 0 = 0$ would make the literal statement false. A formalization that replaces the conditional expectation by the unconditional one, takes the logarithm's Bochner integral (which is $0$ when the logarithm is not integrable), or restricts to deterministic instances and labels does not state Theorem 6.1.

A complete development needs the pathwise loss bound of Lemma 5.3 for this weight model, the pull-out property of conditional expectations for bounded measurable factors, and the exchange of expectation and finite sums. The weight model and the filtration are reusable for Theorem 6.3 and for the lazy variant of the Appendix. Proofs of the milestone and of the goal are welcome, as are formalizations of Corollary 6.1.

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
Y. Freund, R. E. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, Journal of Computer and System Sciences 55(1), 119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8, 121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006
N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

3 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

The Weighted Majority Algorithm 3: On a Countably Infinite Pool, WMI2 Makes at Most inf_i (log(Ŵ(1)/W(i)) + m_i log(1/β) + log 2)/log(1/u) MistakesResearch Paper

Motivation

In prediction with expert advice, a master algorithm predicts a binary label in each of a sequence of trials, after seeing the predictions of a pool of other algorithms (the "experts"), and is charged one mistake whenever its prediction differs from the label. No probabilistic assumption is made on the sequence: the goal is a bound on the master's mistakes, valid for every sequence, in terms of the mistakes of the best pool member. The Weighted Majority Algorithm of Littlestone and Warmuth (Inform. and Comput. 108, 1994) achieves this for a finite pool of $n$ members with $O(\log n + m_i)$ mistakes, where $m_i$ is the number of mistakes of member $i$ .

Many natural pools are infinite: all programs in an enumeration, all hypotheses of a countable class, all values of a discretised parameter. Section 4 of the paper asks whether a master can compete with every member of a countably infinite pool $A_1, A_2, \dots$ , making at most $c(\log i + m_i)$ mistakes for every $i$ , while keeping only finitely many weights at any time. Running the Weighted Majority Algorithm on infinitely many weights would give such a bound, but cannot be implemented.

Timeline. Barzdin and Freivalds (1972, 1974) studied prediction of a sequence by an enumerable family of functions and gave an essentially optimal bound for the case of a pool containing a member consistent with the whole sequence ( $\beta = 0$ below). Littlestone and Warmuth's earlier versions of the paper (1989) introduced an algorithm WMI for infinite pools; the journal version (1994) replaced it by $\mathrm{WMI}_2$ , which matches the Barzdin–Freivalds bound when $\beta = 0$ and a consistent member exists, and extends it to pools in which every member may err.

Setting

Fix a parameter $\beta$ with $0 \le \beta < 1$ and put $u = (1+\beta)/2$ . Fix two real functions $W$ and $\hat W$ on the positive integers with

W(i) > 0, \qquad \sum_{i} W(i) < \infty, \qquad \hat W(i) \ge \sum_{j \ge i} W(j), \qquad \lim_{i \to \infty} \hat W(i) = 0 .

$W(i)$ is the initial weight of the pool member $A_i$ , and $\hat W(i)$ bounds the weight of the tail $A_i, A_{i+1}, \dots$ .

A sequence of $T$ trials gives, for each trial $t$ , the prediction $x_t(i) \in \{0,1\}$ of every pool member and a label $\rho_t \in \{0,1\}$ . Member $A_i$ makes at most $m_i$ mistakes: $x_t(i) \ne \rho_t$ for at most $m_i$ trials $t$ .

The master $\mathrm{WMI}_2$ keeps an active pool $A_1, \dots, A_l$ and a weight for each active member. With $m$ the number of its own mistakes so far, let

\theta(m) = \frac{u^{m+1}\,\hat W(1)}{(1-\beta)(m+1)(m+2)} .

Initially, and after each trial in which it errs, $\mathrm{WMI}_2$ raises $l$ (starting from $l = 0$ ) to the least value with $\hat W(l+1) \le \theta(m)$ ; a newly activated $A_i$ gets weight $W(i)$ . In a trial it computes the active weight $q_0$ predicting $0$ and $q_1$ predicting $1$ ; it predicts $0$ if $q_0 > q_1 + \theta(m)$ , predicts $1$ if $q_1 > q_0 + \theta(m)$ , and may predict either otherwise. After a mistake, every active member that disagreed with the label has its weight multiplied by $\beta$ . The weights $\omega_i$ of the analysis are the current weight of an active member and $W(i)$ for an inactive one.

Formalization targets

The goal is Theorem 4.1, part 3 (p. 227). Let $m$ be the total number of mistakes of $\mathrm{WMI}_2$ on the sequence.

Goal: the mistake bound of $\mathrm{WMI}_2$

If $0 < \beta < 1$ , then

m \le \inf_{i \ge 1} \frac{\log\bigl(\hat W(1)/W(i)\bigr) + m_i \log(1/\beta) + \log 2}{\log(1/u)} ,

and if $\beta = 0$ and $m_i = 0$ for some $i$ , then $m \le 1 + \log_2\bigl(\hat W(1)/W(i)\bigr)$ .

Milestone: the size of the active pool (Theorem 4.1, part 1)

At the beginning of any trial, $l$ is the minimum $l$ with $\hat W(l+1) \le \theta(m)$ , where $m$ counts the mistakes made in prior trials.

Milestone: the weight invariant (Theorem 4.1, part 2)

After any initial sequence of trials in which $m$ mistakes have been made,

\sum_{i=1}^{\infty} \omega_i \le \Bigl(2 - \frac{1}{m+1}\Bigr) u^{m}\, \hat W(1) .

Significance

The result. The bound holds simultaneously for every pool member, so the master competes with the best member of an infinite pool, paying $\log(\hat W(1)/W(i))$ for the position of that member in the enumeration. With $W(i) = 1/(i(i+1))$ and $\hat W(i) = 1/i$ (the paper's Corollary 4.1) this is $O(\log i + m_i)$ mistakes, with an active pool that grows exponentially in the number of mistakes but is finite at every time. Different choices of $W$ trade the mistake bound against the growth of the active pool. The same analysis shows how the predictions can be computed from finite-precision approximations of the weights, which is the reason for the slack band in the prediction rule. Its $\beta = 0$ case recovers the Barzdin–Freivalds bound.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist, and there is no formalization of the Weighted Majority Algorithm on infinite pools on Prove2Me. The work is to formalize the paper's proof: the size statement for the active pool, the inductive invariant for the total weight, and the final logarithmic bound. The definition of a run of $\mathrm{WMI}_2$ , with free predictions in the slack band and lazily activated weights, is reusable for other lazy-activation algorithms on countable pools, and the paper's Corollaries 4.1–4.3 are direct instances once the goal is proved.

Difficulty

The ordinary Weighted Majority analysis tracks the total weight of the whole pool, which shrinks by the factor $u$ after each mistake. For $\mathrm{WMI}_2$ that argument does not apply as is: the master only sees the active weights, and the inactive tail, whose weight is unknown to the algorithm and charged at its initial value, may vote with the label. The obvious bound on the tail is too weak if applied with a fixed slack; it must shrink with the number of mistakes at the right rate so that the accumulated overhead stays below a constant factor. The slack band in the prediction rule interacts with this: when the master errs inside the band, the active majority may not have been wrong by much, and the shrinkage factor must be recovered from the band's width. The factor $2 - 1/(m+1)$ is where these effects are balanced.

Formalization scope

The pool is indexed by ℕ+ and trials by Fin T; false encodes the prediction $0$ , true the prediction $1$ . IsWMI2Run is a relation between the input sequence and the master's predictions, the weights $w_t(i)$ and the active-pool sizes $l_t$ at every trial boundary $t \in \{0, \dots, T\}$ ; a prediction inside the slack band is unconstrained, so the theorems hold for every run. Only active weights are constrained; the analysis uses omega, which counts inactive members at $W(i)$ . The bound $m_i$ is any upper bound on the mistakes of $A_i$ . The tail hypothesis is stated with a tsum together with Summable W, and the milestone on the total weight asserts summability of $\omega$ in its conclusion, so it cannot hold through the value $0$ that Lean assigns to a divergent series. The infimum in the goal is stated as a bound for every $i$ , which is equivalent. Logarithms in the ratio are natural logarithms (the base cancels); the $\beta = 0$ bound uses Real.logb 2. The paper requires $W$ and $\hat W$ to be computable; this only makes the algorithm implementable, and the formal statements hold for arbitrary real functions with the stated analytic properties.

A statement for an algorithm whose runs do not exist would be vacuous; runs of $\mathrm{WMI}_2$ exist for every sequence under the hypotheses (this has been checked locally in Lean), because $\hat W \to 0$ and $\theta(m) > 0$ keep the active pool finite.

Needed infrastructure: finite sums over the active pool, tsum manipulations for sequences that agree with $W$ outside a finite set, and real logarithm inequalities. Contributions welcome: proofs of the two milestones and the goal, and the Corollaries 4.1–4.3 as follow-up statements.

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
J. M. Barzdin, R. V. Freivalds, On the prediction of general recursive functions, Soviet Mathematics Doklady 13, 1224–1228, 1972.
J. M. Barzdin, R. V. Freivalds, Prognozirovanie i predel'nyi sintez effektivno perechislimykh klassov funktsii [Prediction and limit synthesis of effectively enumerable classes of functions], in Theory of Algorithms and Programs (J. M. Barzdin, ed.), Vol. 1, 101–111, Latvian State University, 1974 (in Russian).
N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proceedings of the 30th Annual Symposium on Foundations of Computer Science, 256–261, IEEE, 1989 (cited in the journal paper as [LW89a]).

4 thms2 active usersReviewed

Completed

Convex Optimization Statistics·Captain: mikedeng1

Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers VI: The Group-Lasso Block Update Is Zero iff ‖Aᵢᵀv‖₂ ≤ λ/ρ, Otherwise Ridge with ν‖xᵢ‖₂ = λ/ρTextbook

Why distributed model fitting

Fitting a statistical model usually means solving a convex problem of the form

\text{minimize}\quad l(Ax-b)+r(x),

where $A\in\mathbb R^{m\times n}$ holds one training example per row and one feature per column, $b\in\mathbb R^m$ is the response, $l$ is a convex loss and $r$ a convex regularizer. Least squares, the lasso, logistic regression and the support vector machine are all of this form. When either dimension is very large, or the data are stored on many machines, the problem has to be solved by processors that each see only a block of $A$ .

Chapter 8 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) shows how ADMM does this in two ways: by splitting $A$ by rows (splitting across examples, §8.2), which turns the problem into a global consensus problem, and by splitting it by columns (splitting across features, §8.3), which turns it into a sharing problem. In both cases the method is only practical because the individual updates have closed forms or reduce to small standard problems. This mission formalizes those closed forms, culminating in the update for the group lasso.

Setting

Vectors are in $\mathbb R^n$ with the Euclidean norm $\|\cdot\|_2$ ; $\|x\|_1=\sum_j|x_j|$ . Throughout, $\rho>0$ is the ADMM penalty parameter and $\lambda>0$ a regularization weight.

Splitting across examples. Partition $A$ and $b$ by rows into $N$ blocks $A_i\in\mathbb R^{m_i\times n}$ , $b_i\in\mathbb R^{m_i}$ . With scaled dual variables $u_i$ and averages $\bar x=\frac1N\sum_ix_i$ , $\bar u=\frac1N\sum_iu_i$ , the consensus ADMM iteration is

x_i^{k+1}=\operatorname*{argmin}_{x_i}\Bigl(l_i(A_ix_i-b_i)+\tfrac{\rho}{2}\|x_i-z^k+u_i^k\|_2^2\Bigr),\quad z^{k+1}=\operatorname*{argmin}_{z}\Bigl(r(z)+\tfrac{N\rho}{2}\|z-\bar x^{k+1}-\bar u^k\|_2^2\Bigr),

followed by $u_i^{k+1}=u_i^k+x_i^{k+1}-z^{k+1}$ . For the lasso, $l(w)=\frac12\|w\|_2^2$ and $r=\lambda\|\cdot\|_1$ .

Splitting across features. Partition $x=(x_1,\dots,x_N)$ with $x_i\in\mathbb R^{n_i}$ and $A=[A_1\cdots A_N]$ with $A_i\in\mathbb R^{m\times n_i}$ , so $Ax=\sum_iA_ix_i$ . Introducing $z_i=A_ix_i$ gives a sharing problem; its ADMM $z$ -update minimizes $l(\sum_iz_i-b)+\sum_i\frac\rho2\|A_ix_i-z_i+u_i\|_2^2$ . Writing $\overline{Ax}=\frac1N\sum_iA_ix_i$ and $\bar z$ for the average of the $z_i$ , this reduces to a single problem in $\bar z\in\mathbb R^m$ , all dual variables coincide, and each block update minimizes

\tfrac{\rho}{2}\|A_ix_i-v\|_2^2+r_i(x_i)

for a vector $v\in\mathbb R^m$ assembled from the previous iterate. For the group lasso, $r_i(x_i)=\lambda\|x_i\|_2$ (not squared).

Soft thresholding is $S_\kappa(a)=a-\kappa$ for $a>\kappa$ , $0$ for $|a|\le\kappa$ , $a+\kappa$ for $a<-\kappa$ .

Formalization targets

Goal: the group-lasso block update (§8.3.2, pp. 69–70)

Let $h(x)=\frac\rho2\|A_ix-v\|_2^2+\lambda\|x\|_2$ on $\mathbb R^{n_i}$ and $x(\nu)=(A_i^TA_i+\nu I)^{-1}A_i^Tv$ . Then

0\in\operatorname*{argmin}h\iff\|A_i^Tv\|_2\le\lambda/\rho,

and then $0$ is the only minimizer; if $\|A_i^Tv\|_2>\lambda/\rho$ , there is exactly one $\nu>0$ with $\nu\|x(\nu)\|_2=\lambda/\rho$ , the point $x(\nu)$ minimizes $h$ , and every minimizer is of this form.

Milestones

Ridge $x_i$ -update (§8.2.1, p. 65): $x_i^{k+1}=(A_i^TA_i+\rho I)^{-1}(A_i^Tb_i+\rho(z^k-u_i^k))$ , the unique minimizer.
Soft-thresholding $z$ -update (§8.2.1, p. 65): $z^{k+1}=S_{\lambda/(\rho N)}(\bar x^{k+1}+\bar u^k)$ componentwise.
Reduction to $\bar z$ and equal duals (§8.3, p. 68): minimizers of the $N$ -block $z$ -update are exactly the vectors $z_i=\bar z+A_ix_i+u_i-\overline{Ax}-\bar u$ with $\bar z$ solving the $\bar z$ -update, and then $u_i^{k+1}=\overline{Ax}^{k+1}+\bar u^k-\bar z^{k+1}$ for every $i$ .
Feature-split lasso $\bar z$ -update (§8.3.1, p. 69): $\bar z^{k+1}=(b+\rho\overline{Ax}^{k+1}+\rho u^k)/(N+\rho)$ .
Lasso zero test, corrected (§8.3.1, p. 69): $0$ minimizes $\frac\rho2\|A_ix-v\|_2^2+\lambda\|x\|_1$ iff $\|A_i^Tv\|_\infty\le\lambda/\rho$ .
Eigendecomposition identity (§8.3.2, p. 70): if $A_i^TA_i=Q\,\mathbf{diag}(\mu)Q^T$ with $Q$ orthogonal, then $\|x(\nu)\|_2=\|\mathbf{diag}(\mu+\nu\mathbf 1)^{-1}Q^TA_i^Tv\|_2$ for $\nu>0$ .
SVM $\bar z$ -update (§8.3.4, pp. 70–71): the minimizer of $\mathbf 1^T(N\bar z+\mathbf 1)_++\frac\rho2\|\bar z-\overline{Ax}-u\|_2^2$ is a shifted soft thresholding of $v=\overline{Ax}+u$ .

Significance

The goal result says that a group-lasso block either switches off entirely, which is how group sparsity arises, or solves a ridge regression whose ridge parameter is the unique root of a scalar monotone equation; this is what makes the distributed group lasso implementable with one cached factorization per block and a bisection. The milestones are the remaining closed forms that turn the two distributed schemes of Chapter 8 into concrete algorithms, and the reduction of milestone 3 is the structural fact that lets feature splitting carry a single dual variable.

The book derives these facts in running text and states them without proof. None of them is formalized on Prove2Me, and the book's printed zero test for the lasso (p. 69) uses the wrong norm; a machine-checked collection of the correct updates removes that kind of error from the record and gives later ADMM missions a verified library of update formulas.

Difficulty

Each statement is a characterization of all minimizers of a nonsmooth convex function, not a check that a formula satisfies a stationarity equation. For the goal, the nonsmooth term $\lambda\|x\|_2$ has a kink at $0$ , $h$ need not be strictly convex when $A_i$ has a nontrivial kernel, and the existence and uniqueness of the parameter $\nu$ is part of the claim rather than an assumption: the obvious move of assuming a suitable $\nu$ and checking the formula proves nothing about the case split or about uniqueness, and the singular case of $A_i^TA_i$ is exactly where naive arguments break. Milestone 3 must handle an arbitrary convex loss $l$ , with no closed form at all.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n); matrices are Matrix (Fin m) (Fin n) ℝ acting through Matrix.toEuclideanLin; blocks are indexed by Fin N (0-based); the regularization weight $\lambda$ is lam; the eigenvalue vector the book also calls $\lambda$ (p. 70) is μ. " $x$ minimizes $F$ " is Mathlib's IsMinOn F Set.univ x. Iteration superscripts are dropped: each statement is about one update with the previous iterate given. Explicit choices:

$\rho>0$ , $\lambda>0$ and $N\ge1$ are hypotheses wherever the book uses them.
Closed forms are stated as "minimizer $\iff$ formula", which contains existence and uniqueness; the book's "the solution" in §8.3.2 is stated as existence and uniqueness of $\nu$ plus a characterization of every minimizer, with no invertibility hypothesis on $A_i^TA_i$ .
$(A_i^TA_i+\nu I)^{-1}$ is Mathlib's matrix inverse, used only for $\nu>0$ , where it is the true inverse.
The loss in milestone 3 is real valued and convex, as in (8.1).
The lasso zero test is stated with $\|\cdot\|_\infty$ ; the book prints $\|\cdot\|_2$ , which is false for the $\ell_1$ term.
The SVM $\bar z$ -update uses the coefficient $\rho/2$ printed on p. 70, which matches the printed thresholds $N/\rho$ .
The book's "assuming $A_i$ is tall" (p. 70) is not imposed; the identity holds without it.

A statement that only checks that $x(\nu)$ satisfies the optimality equation, or that assumes the parameter $\nu$ exists, does not capture the goal; the goal asserts existence and uniqueness of $\nu$ and describes every minimizer of $h$ .

Contributions welcome: subgradient calculus for $\|\cdot\|_2$ and $\|\cdot\|_1$ in EuclideanSpace, first-order optimality for convex quadratics plus a convex nonsmooth term, and the monotonicity of $\nu\mapsto\nu\|(M+\nu I)^{-1}c\|_2$ for positive semidefinite $M$ ; these are reusable for every proximal and ADMM update.

Selected references

S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1):1–122, 2011. https://doi.org/10.1561/2200000016
M. Yuan, Y. Lin, Model selection and estimation in regression with grouped variables, Journal of the Royal Statistical Society B 68(1):49–67, 2006. https://doi.org/10.1111/j.1467-9868.2005.00532.x
R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1):267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x

10 thms2 active usersReviewed

Completed

Optimization Reinforcement Learning·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 3: Softmax Policy Gradient Ascent with Step Size η ≤ (1−γ)³/8 Converges to the Optimal ValuesResearch Paper

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective $\theta \mapsto V^{\pi_\theta}(\mu)$ is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?

Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an $O(1/t)$ rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.

Setting

A finite MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions ( $\mathcal A$ 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 to each state a probability vector $\pi(\cdot\mid s)$ on $\mathcal A$ . Its value $V^\pi(s)$ is the expected discounted sum of rewards $\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid s_0=s]$ when actions are drawn from $\pi$ ; its state–action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and its advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$ . For a distribution $\mu$ on states, $V^\pi(\mu)=\sum_s\mu(s)V^\pi(s)$ , and the discounted state visitation distribution is $d^\pi_\mu(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\mu)$ . A policy $\pi^\star$ is optimal if $V^{\pi}(s)\le V^{\pi^\star}(s)$ for every policy $\pi$ and every state $s$ ; $V^\star=V^{\pi^\star}$ .

The softmax policy with parameters $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is

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

Softmax policy gradient ascent with step size $\eta$ produces, from an arbitrary $\theta^{(0)}$ , the iterates

\theta^{(t+1)}=\theta^{(t)}+\eta\,\nabla_\theta V^{(t)}(\mu),\qquad V^{(t)}=V^{\pi_{\theta^{(t)}}} .

The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ $=V^{\pi_\theta}(\mu)$ , and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.

Formalization targets

Goal: Theorem 5.1

If $\mu(s)>0$ for every state and $0<\eta\le(1-\gamma)^3/8$ , then for every state $s$

V^{(t)}(s)\longrightarrow V^\star(s)\qquad(t\to\infty).

Milestones (Appendices C.1 and D)

Lemma C.1, the gradient formula $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a\mid s)A^{\pi_\theta}(s,a)$ .
Lemma D.1, smoothness $5\|c\|_\infty$ of $\theta_s\mapsto\sum_a\pi_\theta(a\mid s)c_a$ .
Lemma D.4 at $\lambda=0$ , smoothness $8/(1-\gamma)^3$ of $\theta\mapsto V^{\pi_\theta}(\mu)$ .
Lemma C.2, pointwise monotone improvement of $V^{(t)}(s)$ and $Q^{(t)}(s,a)$ for $\eta\le(1-\gamma)^2/5$ .
Lemma C.3, existence of the limits $V^{(\infty)}$ , $Q^{(\infty)}$ and the bound (40).
Lemma C.4, eventual sign separation (41) of the advantages on $I^s_+=\{a:Q^{(\infty)}(s,a)>V^{(\infty)}(s)\}$ and $I^s_-=\{a:Q^{(\infty)}(s,a)<V^{(\infty)}(s)\}$ .
Lemma C.5, vanishing gradients, $\pi^{(t)}(a\mid s)\to0$ off $I^s_0=\{a:Q^{(\infty)}(s,a)=V^{(\infty)}(s)\}$ , and $\sum_{a\in I^s_0}\pi^{(t)}(a\mid s)\to1$ .
Lemma C.6, eventual strict monotonicity of $\theta^{(t)}_{s,a}$ on $I^s_\pm$ .
Lemma C.7, divergence of $\max_{a\in I^s_0}\theta^{(t)}_{s,a}$ and $\min_a\theta^{(t)}_{s,a}$ when $I^s_+\neq\emptyset$ .
Lemma C.11, lower boundedness of $\theta^{(t)}_{s,a}$ on $I^s_+$ and $\theta^{(t)}_{s,a}\to-\infty$ on $I^s_-$ .

The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.

Significance

The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to $V^\star$ at every state, not only on average under $\mu$ . It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether $\mu>0$ can be dropped.

The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.

Difficulty

The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from $\nabla_\pi V^\pi(\mu)\to0$ , but under softmax $\partial V/\partial\theta_{s,a}=\pi_\theta(a\mid s)\,\partial V/\partial\pi_\theta(a\mid s)$ , so a vanishing $\theta$ -gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters $\theta^{(t)}_{s,a}$ move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets $I^s_0, I^s_\pm$ and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.

Formalization scope

Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in $[0,1]$ , $0\le\gamma<1$ ); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\theta$ ; the coordinate $(s,a)$ of the gradient is $\partial/\partial\theta_{s,a}$ . Logarithms do not appear. Conventions committed to:

$V^\star(s)$ is PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.
The step size satisfies $0<\eta$ , which "gradient ascent" presupposes and the page does not write; at $\eta=0$ the theorem is false.
$\mu(s)>0$ for every $s$ is a hypothesis of the goal and of Lemmas C.5–C.11; Lemmas C.1–C.4 are stated without it, and Lemma C.1 for an arbitrary real weighting $\mu$ .
In Lemmas C.4–C.11 the limits $V^{(\infty)}$ , $Q^{(\infty)}$ are parameters with the hypotheses that they are the limits of $V^{(t)}$ , $Q^{(t)}$ . The paper's $\Delta=\min_{A^{(\infty)}(s,a)\neq0}|A^{(\infty)}(s,a)|$ is replaced by any $\Delta>0$ bounded by every nonzero $|A^{(\infty)}(s,a)|$ , which avoids an undefined minimum over an empty set.
" $\to\pm\infty$ " is Tendsto … atTop atTop / atBot; "strictly increasing for $t\ge T_1$ " is StrictMonoOn on Set.Ici T1, with $T_1$ existentially quantified.

The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets $I^s_0, I^s_\pm$ ; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis $I^s_+\neq\emptyset$ of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.

A full development needs: differentiability of $\theta\mapsto V^{\pi_\theta}$ and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for $L$ -smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument 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.00261
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. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 1999. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation

21 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

From Predictive to Prescriptive Analytics 2: For Costs in [0, c̄] That Are L-Lipschitz, w.p. ≥ 1 − δ Every Decision Rule in F Costs ≤ Its Empirical Cost + c̄√(log(1/δ)/2N) + L·ℜ_N(F)Research Paper

Motivation

Many operations decisions are made after observing side information: an inventory manager sees weather, search trends and calendar effects before ordering; a supply-chain planner sees market signals before shipping. Bertsimas and Kallus, in From Predictive to Prescriptive Analytics (arXiv:1402.5481v4, Management Science 2020), study how to turn such data into decisions. Besides their local, weight-based prescriptions (the subject of mission 1 of this series), their §8 analyses a second approach: choose a decision rule $z(\cdot)$ from a structured class, such as norm-bounded linear rules, by empirical risk minimization — minimizing the average historical cost of the rule.

The question this mission formalizes is the one any practitioner of that approach must answer: how far can the true expected cost of the chosen rule exceed its in-sample cost? Classical statistical learning answers it with Rademacher complexity (Bartlett and Mendelson, JMLR 2002), but only for real-valued predictors. Operations decisions are vectors (order quantities for several products, shipments to several locations), so the paper extends the theory to multivariate decision rules.

Setting

Covariates $x$ take values in a measurable space $\mathcal X$ , the uncertain quantity $y$ in a measurable space $\mathcal Y$ , and decisions $z$ in $\mathbb R^{d}$ , unconstrained. Data are an i.i.d. sample $S_N=((x^1,y^1),\dots,(x^N,y^N))$ from a probability measure $\mu$ on $\mathcal X\times\mathcal Y$ , and $S_N^x=(x^1,\dots,x^N)$ is its covariate part. A cost $c(z;y)$ is incurred when decision $z$ meets outcome $y$ . A decision rule is a measurable map $z(\cdot):\mathcal X\to\mathbb R^d$ ; $\mathcal F$ is a class of decision rules. Its expected cost is $\mathbb E[c(z(X);Y)]$ , and its empirical cost is $\frac1N\sum_{i=1}^N c(z(x^i);y^i)$ , the objective of problem (4).

The empirical multivariate Rademacher complexity of $\mathcal F$ (Definition 3) on a sample $s_1,\dots,s_N$ is

\widehat{\mathfrak R}_N(\mathcal F;S_N)=\mathbb E_\sigma\Big[\frac2N\sup_{g\in\mathcal F}\sum_{i=1}^N\sum_{k=1}^d\sigma_{ik}\,g_k(s_i)\Big],

with $\sigma_{ik}$ independent uniform signs, and the marginal complexity $\mathfrak R_N(\mathcal F)$ is its expectation over the sample. For real-valued classes ( $d=1$ ) these are the usual Rademacher complexities with factor $2/N$ and no absolute value. Lean notation: empRademacher, margRademacher, expCost, empCost, costClass in PrescAnalytics.ERM.

Formalization targets

Goal: Theorem 13 (out-of-sample guarantees)

If $0\le c(z;y)\le\bar c$ and $|c(z;y)-c(z';y)|\le L\|z-z'\|_\infty$ , then for any $\delta>0$ each of the following holds with probability at least $1-\delta$ :

\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+\bar c\sqrt{\frac{\log(1/\delta)}{2N}}+L\,\mathfrak R_N(\mathcal F)\quad\forall z\in\mathcal F,\tag{26}

\mathbb E[c(z(X);Y)]\le\frac1N\sum_{i=1}^N c(z(x^i);y^i)+3\bar c\sqrt{\frac{\log(2/\delta)}{2N}}+L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)\quad\forall z\in\mathcal F.\tag{27}

In particular they hold for the empirical risk minimizer. The goal is stated for a general class $\mathcal F$ , not only the linear rules (25).

Milestones

Lemma 1 (comparison): for $\mathcal G=\{(x,y)\mapsto c(f(x);y):f\in\mathcal F\}$ , $\widehat{\mathfrak R}_N(\mathcal G;S_N)\le L\,\widehat{\mathfrak R}_N(\mathcal F;S_N^x)$ and $\mathfrak R_N(\mathcal G)\le L\,\mathfrak R_N(\mathcal F)$ .
Theorem 14 (29): for a class $\mathcal G$ of functions with values in $[0,\bar g]$ , with probability at least $1-\delta$ , $\mathbb E g\le\frac1N\sum_i g(u^i)+\bar g\sqrt{\log(1/\delta)/(2N)}+\mathfrak R_N(\mathcal G)$ for all $g\in\mathcal G$ .
Theorem 14 (30): the data-dependent version with $3\bar g\sqrt{\log(2/\delta)/(2N)}+\widehat{\mathfrak R}_N(\mathcal G;S_N)$ .

Significance

Theorem 13 says that the quantity empirical risk minimization optimizes is, up to confidence terms that do not depend on the rule, an upper bound on the true expected cost of every rule in the class, uniformly. Bound (27) is computable from data, so it certifies a learned policy without a holdout set. Combined with complexity bounds for norm-restricted linear rules (the paper's Lemmas 2 and 3, not part of this mission), it shows the confidence terms vanish as $N\to\infty$ .

The results are known: (29) and (30) for $[0,\bar g]$ -valued classes are the standard Rademacher bounds (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Thm 3.3, after rescaling). What is new in the paper is the $\infty$ -norm vector comparison inequality of Lemma 1 with constant $1$ . None of these statements has a machine-checked proof on the platform. A formal development would supply a reusable symmetrization-plus-McDiarmid pipeline and a vector contraction lemma. Related items posed in this repository are Bartlett–Mendelson's Theorem 8 (RadGauss.RiskBound.theorem_8, with an absolute value in the complexity and constant $\sqrt{8\ln(2/\delta)/n}$ ), Maurer's Euclidean vector contraction with constant $\sqrt2$ (SPOBounds.Margin.maurer_vector_contraction), and the open uniform law HighDimStat.UniformLaws.uniform_law_rademacher_complexity; none is the same statement as a target here.

Difficulty

The uniform bound needs three ingredients: a concentration inequality for the supremum of the deviation over the class (bounded differences), a symmetrization step relating the expected supremum to the Rademacher complexity, and a comparison inequality to pass from the cost class to the decision rules. The scalar contraction principle of Ledoux and Talagrand does not apply directly, since each cost depends on a $d$ -dimensional output; applying it coordinatewise loses a factor of $d$ , and Euclidean vector contraction loses $\sqrt2$ and uses the wrong norm. Lemma 1 needs an argument specific to the $\infty$ -norm. Measure theory adds its own difficulty: the supremum over an uncountable class must be shown measurable before its expectation or probability means anything.

Formalization scope

Decisions are Fin d → ℝ, whose Lean norm is the $\infty$ -norm; $\mathcal X$ , $\mathcal Y$ are general measurable spaces. Samples are drawn from the product measure Measure.pi (fun _ : Fin N => μ), with $N\ge1$ . The following readings are explicit:

Each "with probability at least $1-\delta$ , … for all $z\in\mathcal F$ " is a bound $\le\delta$ on the outer measure of the set of samples where the inequality fails for some $z$ ; the quantifier over the class is inside the event.
Empirical complexities are in EReal (an unbounded class gives $+\infty$ ), marginal ones are lower Lebesgue integrals in $[0,\infty]$ ; $0\cdot\infty=0$ .
The paper assumes only $\sup c\le\bar c$ (resp. $|g|\le\bar g$ ). With that alone (26) and (29) are false — a two-point outcome with a constant rule violates them with probability $1/2$ — so the costs are assumed to take values in $[0,\bar c]$ , keeping every printed constant.
The undefined $\delta',\delta''$ are $\delta$ (the i.i.d. case of the paper's Theorem 21); the Lipschitz denominator printed as $\|z_k-z'_k\|_\infty$ is $\|z-z'\|_\infty$ .
Decision rules and the cost are measurable and the class is pointwise separable (a countable subclass approximates every member pointwise). The paper takes probabilities and expectations of suprema over the class without comment; without such a convention the statement fails for pathological classes.

A trivializing formalization is ruled out: the quantifier over the class sits inside the probability, the complexity has no absolute value and is never a junk $0$ for unbounded classes, and the hypotheses are satisfied by a clipped newsvendor cost. Solvers will need McDiarmid's inequality, symmetrization with a ghost sample, and the comparison lemma; each is reusable for any Rademacher-based generalization bound. Formalizations of these tools as separate lemmas are welcome.

Selected references

D. Bertsimas, N. Kallus, From Predictive to Prescriptive Analytics, arXiv:1402.5481v4, 2018; Management Science 66(3), 2020. https://arxiv.org/abs/1402.5481 , https://doi.org/10.1287/mnsc.2018.3253
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, JMLR 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
M. Ledoux, M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018. https://mitpress.mit.edu/9780262039406/
A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, ALT 2016. https://arxiv.org/abs/1605.00251

5 thms2 active usersReviewed

Completed

Bandit Algorithms Probability Statistics·Captain: mikedeng1

Kullback–Leibler Upper Confidence Bounds for Optimal Sequential Allocation II: Empirical KL-UCB Draws a Suboptimal Arm log(T)/K_inf(ν_a, μ*) + O((log T)^{4/5} log log T) TimesResearch Paper

Motivation

In a stochastic multi-armed bandit a player repeatedly chooses one of $K$ arms and receives a random reward drawn from that arm's unknown distribution; the aim is to pull suboptimal arms as rarely as possible. Lai and Robbins (1985) and, for general models, Burnetas and Katehakis (1996) showed that any reasonable strategy must pull a suboptimal arm $a$ at least $(1+o(1))\log T/\mathcal K_{\inf}(\nu_a,\mu^\star)$ times in $T$ rounds, where $\mathcal K_{\inf}$ is a minimal Kullback–Leibler divergence defined below. A strategy whose expected number of pulls matches this constant is asymptotically optimal.

For rewards in $[0,1]$ , classical index policies such as UCB (Auer, Cesa-Bianchi and Fischer, 2002) achieve $O(\log T)$ pulls but with a constant governed by the gap of the means, not by $\mathcal K_{\inf}$ . Cappé, Garivier, Maillard, Munos and Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3), 2013 (arXiv:1210.1136v4), introduce the KL-UCB family of index policies and prove finite-time bounds whose leading term is the Lai–Robbins/Burnetas–Katehakis constant. This mission formalizes their result for empirical KL-UCB (Algorithm 3, Theorem 2), which is asymptotically optimal in the nonparametric model of finitely supported distributions on $[0,1]$ . A companion mission covers kl-UCB in one-parameter exponential families (Theorem 1).

Timeline: Lai and Robbins (1985), lower bound for parametric families; Burnetas and Katehakis (1996), lower bound and asymptotically optimal policies for general models; Honda and Takemura (2010, 2011), the DMED algorithm, asymptotically optimal for finitely supported and bounded rewards; Cappé et al. (2013), the first index policy with a non-asymptotic bound whose leading term is optimal in this model.

Setting

A bandit has $K\ge2$ arms with reward distributions $\nu_1,\dots,\nu_K$ in a known model $\mathcal F$ : the set of probability distributions over $[0,1]$ with finite support. Write $\mathrm E(\nu)=\int x\,d\nu(x)$ , $\mu_a=\mathrm E(\nu_a)$ and $\mu^\star=\max_a\mu_a$ ; arm $a$ is suboptimal if $\mu_a<\mu^\star$ . At each round $t\ge1$ the player picks an arm $A_t$ based on past observations and observes a reward drawn from $\nu_{A_t}$ . $N_a(T)=\sum_{t=1}^T\mathbb I\{A_t=a\}$ is the number of pulls of arm $a$ up to round $T$ .

Equivalently, each arm has a reward stack $X_{a,1},X_{a,2},\dots$ of i.i.d. draws from $\nu_a$ , all stacks independent, and the $n$ -th pull of arm $a$ returns $X_{a,n}$ . The empirical distribution of the first $n$ rewards is $\hat\nu_{a,n}=\frac1n\sum_{k=1}^n\delta_{X_{a,k}}$ , and $\hat\nu_a(t)=\hat\nu_{a,N_a(t)}$ .

The minimal divergence is

\mathcal K_{\inf}(\nu,\mu)=\inf\bigl\{\mathrm{KL}(\nu,\nu'):\nu'\in\mathcal F,\ \mathrm E(\nu')>\mu\bigr\}\in[0,+\infty],

the smallest Kullback–Leibler divergence from $\nu$ to a distribution of the model whose mean exceeds $\mu$ .

Empirical KL-UCB (Algorithm 3) pulls each arm once, then for $t=K,K+1,\dots$ pulls an arm maximizing

U_a(t)=\sup\Bigl\{\mathrm E(\nu):\nu\in\mathfrak M_1\bigl(\mathrm{Supp}(\hat\nu_a(t))\cup\{1\}\bigr),\ \mathrm{KL}(\hat\nu_a(t),\nu)\le\frac{f(t)}{N_a(t)}\Bigr\},

where $\mathfrak M_1(A)$ is the set of probability distributions carried by $A$ and $f(t)=\log t+\log\log t$ . The added point $1$ is essential: without it the index is the empirical-likelihood bound, which equals the empirical mean when every observation is $0$ .

Formalization targets

Goal: Theorem 2 (pp. 15–16)

Assume $\mu_a>0$ for all arms and $\mu^\star<1$ . There is a constant $M(\nu_a,\mu^\star)>0$ depending only on $\nu_a$ and $\mu^\star$ such that, for every suboptimal arm $a$ and all $T\ge3$ ,

\begin{aligned}\mathbb E[N_a(T)]\le{}&\frac{\log T}{\mathcal K_{\inf}(\nu_a,\mu^\star)}+\frac{36}{(\mu^\star)^4}(\log T)^{4/5}\log\log T+\Bigl(\frac{72}{(\mu^\star)^4}+\frac{2\mu^\star}{(1-\mu^\star)\mathcal K_{\inf}(\nu_a,\mu^\star)^2}\Bigr)(\log T)^{4/5}\\&+\frac{(1-\mu^\star)^2M(\nu_a,\mu^\star)}{2(\mu^\star)^2}(\log T)^{2/5}+\frac{\log\log T}{\mathcal K_{\inf}(\nu_a,\mu^\star)}+\frac{2\mu^\star}{(1-\mu^\star)\mathcal K_{\inf}(\nu_a,\mu^\star)^2}+4.\end{aligned}

The constants are the paper's. $M$ is the one quantity the main text does not give; it is existentially quantified, before the bandit, so it may depend on nothing but $(\nu_a,\mu^\star)$ .

Milestones

(7), p. 9: the sets $\mathcal C_{\mu,\gamma}=\{\nu:\exists\nu'\in\mathcal F,\ \mathrm E(\nu')>\mu,\ \mathrm{KL}(\nu,\nu')\le\gamma\}$ satisfy $\mathcal C_{\mu,\gamma}\subseteq\{\nu:\mathcal K_{\inf}(\nu,\mu)\le\gamma\}$ .
(5), p. 9: the decomposition $\{A_{t+1}=a\}\subseteq\{\mu^\dagger\ge U_{a^\star}(t)\}\cup\{\mu^\dagger<U_a(t),\ A_{t+1}=a\}$ .
The display after (7), p. 9: $\mathbb E[N_a(T)]\le1+\sum_{t=K}^{T-1}\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}+\sum_{t=K}^{T-1}\mathbb P\{\hat\nu_{a,N_a(t)}\in\mathcal C_{\mu^\dagger,f(t)/N_a(t)},\ A_{t+1}=a\}$ .
(8), p. 10: the second sum is at most $\sum_{n=1}^{T-K}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$ .
(9)–(10), p. 10: $\mathbb E[N_a(T)]\le f(T)/\mathcal K_{\inf}(\nu_a,\mu^\star)+\sum_{n>n_0}\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}+\sum_t\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}+2$ with $n_0=\lceil f(T)/\mathcal K_{\inf}(\nu_a,\mu^\star)\rceil$ .
p. 15: the supremum defining $U_a(t)$ over $\mathcal F$ equals the supremum over $\mathfrak M_1(\mathrm{Supp}(\hat\nu_a(t))\cup\{1\})$ .
Implicit in Theorem 2: $0<\mathcal K_{\inf}(\nu,\mu)<\infty$ for $\nu\in\mathcal F$ and $\mathrm E(\nu)<\mu<1$ .
Proposition 1, p. 20: for $n$ i.i.d. observations from any $\nu_0$ on $[0,1]$ with $\mathrm E(\nu_0)\in(0,1)$ and every $\varepsilon>0$ ,

\mathbb P\{U(\hat\nu_n,\varepsilon)\le\mathrm E(\nu_0)\}\le\mathbb P\{\mathcal K_{\inf}(\hat\nu_n,\mathrm E(\nu_0))\ge\varepsilon\}\le e(n+2)\exp(-n\varepsilon).

Significance

Theorem 2 gives a finite-time bound whose leading term, $\log T/\mathcal K_{\inf}(\nu_a,\mu^\star)$ , equals the Burnetas–Katehakis lower bound for the model $\mathcal F$ . Hence empirical KL-UCB is asymptotically optimal among all strategies for finitely supported rewards in $[0,1]$ , and the regret $\sum_a(\mu^\star-\mu_a)\mathbb E[N_a(T)]$ inherits the optimal constant. Since $\mathcal K_{\inf}(\nu_a,\mu^\star)$ is at least the Bernoulli divergence of the means, and usually larger, the bound improves on kl-UCB and UCB for the same rewards. Proposition 1 is a non-asymptotic coverage bound for the empirical-likelihood upper confidence bound with the point $1$ added, valid for every law on $[0,1]$ , not only finitely supported ones.

The proofs of Theorem 2 and Proposition 1 are in the paper's supplemental article (Appendix B), not in the main text; no machine-checked proof of either exists. The mission produces formal statements of the theorem and of the proof skeleton (5)–(10) that the paper shares with Theorem 1, and of the two facts about $\mathcal K_{\inf}$ that the bound needs. A formal proof would supply an explicit $M(\nu_a,\mu^\star)$ , which the paper defines only inside the supplement.

Difficulty

The skeleton (5)–(10) is elementary bookkeeping; the difficulty lies in the two sums it leaves, both of which must be shown to be $o(\log T)$ with explicit constants. The second, $\sum_n\mathbb P\{\hat\nu_{a,n}\in\mathcal C_{\mu^\dagger,f(T)/n}\}$ , needs a deviation estimate for the empirical $\mathcal K_{\inf}$ of a suboptimal arm that is precise enough to keep the leading constant $1/\mathcal K_{\inf}(\nu_a,\mu^\star)$ : a bound that only controls the deviation of the empirical mean loses it, since $\mathcal K_{\inf}$ depends on the whole distribution. The first, $\sum_t\mathbb P\{\mu^\dagger\ge U_{a^\star}(t)\}$ , concerns the optimal arm after a random number of pulls $N_{a^\star}(t)$ , which the algorithm itself determines, so fixed-sample bounds such as Proposition 1 do not apply directly. Both need regularity of $\mathcal K_{\inf}$ as a function of a distribution in an infinite-dimensional model, where none of the closed forms of the exponential-family case is available.

Formalization scope

Arms are Fin K, and arm $a$ of the paper is index $a-1$ . The bandit is the platform's stack-of-rewards model RegretBandits.Stochastic.IsStochasticBandit: $X_{a,k}$ (indexed from $0$ ) are independent, identically distributed within each arm, with mean $\mu_a$ . Pull counts and $\mu^\star$ are the platform's pullCount and bestMean. Added to the page, and disclosed in each statement: every reward lies in $[0,1]$ pathwise (a representation of " $\nu_a$ is carried by $[0,1]$ "), every arm choice is measurable, and in the goal the strategy is non-anticipating ( $A_{t+1}$ is measurable with respect to the arms and rewards of rounds $1,\dots,t$ ). A run of Algorithm 3 is a pathwise predicate: rounds $1,\dots,K$ pull distinct arms, and every later round pulls a maximizer of $U_\cdot(t)$ , with ties broken by any rule. KL is Mathlib's InformationTheory.klDiv in $[0,+\infty]$ , with the empirical distribution as first argument. $\mathcal K_{\inf}$ is kept in $[0,+\infty]$ and converted to a real number only in the final bounds, where it is finite and positive. Probabilities of events whose measurability is not asserted are outer probabilities. The page's $\sum_{n\ge n_0+1}$ in (10) is stated as the finite sum over $n_0<n\le T-K$ that (8) produces. The probability space of Theorem 2 lies in Type.

Trivializing formalizations are ruled out. The index is a supremum over a set that is nonempty (it contains $\mathrm E(\hat\nu_a(t))$ ) and bounded above, so it is never Lean's junk value. $\mathcal K_{\inf}$ and $\mathcal C_{\mu,\gamma}$ range over $\mathcal F$ , not over all measures. The run predicate has both the initialization and the argmax clause. $M$ is quantified before the bandit and the horizon.

Reusable beyond this mission: $\mathcal K_{\inf}$ for $\mathcal F$ , the empirical-likelihood bound $U$ of (15), and Proposition 1, a concentration inequality for empirical $\mathcal K_{\inf}$ that applies to any bounded i.i.d. sample. Proofs of any milestone are welcome, as are proofs of the skeleton (5)–(10) that also apply to the companion kl-UCB mission.

Selected references

O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3):1516–1541, 2013. arXiv:1210.1136v4, doi:10.1214/13-AOS1119; supplement doi:10.1214/13-AOS1119SUPP.
T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6(1):4–22, 1985. doi:10.1016/0196-8858(85)90002-8
A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Adv. Appl. Math. 17(2):122–142, 1996. doi:10.1006/aama.1996.0007
J. Honda, A. Takemura, An asymptotically optimal bandit algorithm for bounded support models, COLT 2010, 67–79.
P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Mach. Learn. 47:235–256, 2002. doi:10.1023/A:1013689704352

13 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity X: Nesterov's Accelerated Gradient Descent on a β-Smooth α-Strongly Convex Function Has Rate ((α + β)/2)‖x₁ − x*‖² exp(−(t − 1)/√κ)Textbook

Why accelerated rates matter

First-order methods, which query only function values and gradients, are the workhorse of large-scale optimization in machine learning, signal processing and operations research, because each step costs little more than one gradient evaluation. For a function that is both strongly convex and smooth, plain gradient descent converges geometrically, but the number of steps needed to reach accuracy $\varepsilon$ scales with the condition number $\kappa$ of the problem. In 1983 Nesterov showed that a gradient method with a carefully chosen momentum term needs a number of steps proportional to $\sqrt\kappa$ instead, and that this is optimal for black-box first-order methods. On ill-conditioned problems, where $\kappa$ is in the thousands or millions, the difference between $\kappa$ and $\sqrt\kappa$ is the difference between practical and impractical.

This mission is the tenth of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2). It covers §3.7.1, the smooth and strongly convex case of Nesterov's accelerated gradient descent, and its main result, Theorem 3.18.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$ . Let $f:\mathbb R^n\to\mathbb R$ be differentiable with gradient $\nabla f$ .

$f$ is $\beta$ -smooth if its gradient is $\beta$ -Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|$ for all $x,y$ .
$f$ is $\alpha$ -strongly convex ( $\alpha>0$ ) if for all $x,y$

f(y)\ge f(x)+\nabla f(x)^\top(y-x)+\frac\alpha2\|y-x\|^2 .

The condition number is $\kappa=\beta/\alpha$ ; for $n\ge1$ one always has $\kappa\ge1$ .
$x^*$ denotes a minimizer of $f$ on $\mathbb R^n$ .

Nesterov's accelerated gradient descent starts at an arbitrary point $x_1=y_1$ and iterates, for $t\ge1$ ,

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

The point $y_{t+1}$ is a gradient step from $x_t$ , and $x_{t+1}$ moves beyond $y_{t+1}$ in the direction $y_{t+1}-y_t$ by the fixed momentum factor $(\sqrt\kappa-1)/(\sqrt\kappa+1)$ .

The analysis in the book uses auxiliary quadratic functions $\Phi_s$ (an estimate sequence), defined from the points $x_s$ by

\Phi_1(x)=f(x_1)+\frac\alpha2\|x-x_1\|^2,\qquad \Phi_{s+1}(x)=\Big(1-\frac1{\sqrt\kappa}\Big)\Phi_s(x)+\frac1{\sqrt\kappa}\Big(f(x_s)+\nabla f(x_s)^\top(x-x_s)+\frac\alpha2\|x-x_s\|^2\Big),

together with their centres $v_s$ (with $v_1=x_1$ and the recursion (3.21) of the book) and their minimum values $\Phi^*_s$ .

Formalization targets

Goal: Theorem 3.18

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

f(y_t)-f(x^*)\le\frac{\alpha+\beta}2\,\|x_1-x^*\|^2\exp\Big(-\frac{t-1}{\sqrt\kappa}\Big).

Milestones, from the book's proof

(3.18): $\Phi_{s+1}(x)\le f(x)+(1-1/\sqrt\kappa)^s(\Phi_1(x)-f(x))$ for all $x$ .
(3.19): $f(y_s)\le\min_{x\in\mathbb R^n}\Phi_s(x)$ .
The geometric rate: $f(y_t)-f(x^*)\le\frac{\alpha+\beta}2\|x_1-x^*\|^2(1-1/\sqrt\kappa)^{t-1}$ .
The form $\Phi_s(x)=\Phi^*_s+\frac\alpha2\|x-v_s\|^2$ with $v_s$ given by (3.21).
The identity (3.22) for $\Phi^*_{s+1}$ .
The inequality (3.20), the inductive step of (3.19).
The coupling $v_s-x_s=\sqrt\kappa\,(x_s-y_s)$ .

The geometric form in milestone 3 is slightly stronger than the goal, which follows from $1-u\le e^{-u}$ .

Significance

Theorem 3.18 gives $\varepsilon$ -accuracy after $O(\sqrt\kappa\log(1/\varepsilon))$ gradient evaluations. Projected gradient descent with step $1/\beta$ on the same class contracts only at the rate $\exp(-t/\kappa)$ (Theorem 3.10 of the book). The lower bound of Theorem 3.15 shows that no black-box first-order method can do better than $((\sqrt\kappa-1)/(\sqrt\kappa+1))^{2(t-1)}$ , so the accelerated rate is optimal up to constants. The estimate-sequence argument is the template for many later accelerated methods: proximal, stochastic and variance-reduced variants such as Katyusha, and accelerated coordinate descent.

The result is classical and fully proved on paper. No machine-checked proof of the accelerated rate for strongly convex smooth functions is known to exist in Lean's Mathlib. This mission produces one, with the estimate sequence $\Phi_s$ , its centres and its minimum values as reusable objects, and with every algebraic identity of the book's proof stated separately.

Difficulty

The algorithm is two lines, but its analysis is not a one-step contraction: neither $\|x_t-x^*\|$ nor $f(y_t)-f(x^*)$ decreases by the factor $1-1/\sqrt\kappa$ at every step. A Lyapunov argument for gradient descent, applied directly to $y_t$ , gives only the rate $1-1/\kappa$ . The book obtains the rate through the auxiliary functions $\Phi_s$ . The inequality (3.18) is easy, but (3.19), that the minimum of $\Phi_s$ never drops below $f(y_s)$ , depends on the exact choice of the momentum factor. It holds only through the identity $v_s-x_s=\sqrt\kappa(x_s-y_s)$ , which ties the centre of $\Phi_s$ to the iterates. Formally, the obstacles are the bookkeeping of the recursive quadratics on $\mathbb R^n$ and the algebra in $\sqrt\kappa$ , $1/\sqrt\kappa$ and $1/(\alpha\sqrt\kappa)=\sqrt\kappa/\beta$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map g with HasGradientAt f (g x) x at every point, which is part of the smoothness predicate IsBetaSmooth f g β. Strong convexity is the published definition OnlineConvexOpt.ConvexBasics.StronglyConvexOn Set.univ f g α, which is the book's (3.13).
A run of the method is a predicate IsNesterovSCRun g α β x y on two sequences indexed from $1$ , with $x_1=y_1$ arbitrary. Every theorem holds for every run, that is, every starting point.
$\kappa$ is kappa α β = β / α. All theorems assume $\alpha>0$ and $\beta>0$ . The second is implied by the other hypotheses for $n\ge1$ ; no hypothesis $\alpha\le\beta$ is added.
The existence of a minimizer $x^*$ is the book's standing assumption, written as a hypothesis.
$\Phi_s$ , $v_s$ and $\Phi^*_s=\Phi_s(v_s)$ are explicit recursive definitions. The book's $\Phi^*_s=\min\Phi_s$ is recovered by milestone 4, and no real infimum is used. The minimum in (3.19) is stated as $f(y_s)\le\Phi_s(x)$ for every $x$ .
The identities of milestones 4, 5 and 7 are algebraic and are stated without convexity or smoothness, for arbitrary sequences or runs.
Ruled out as trivializing: a run predicate that drops $x_1=y_1$ breaks (3.19) at $s=1$ and is not used. A minimum value $\Phi^*_s$ defined through (3.22) would make that identity a tautology, so $\Phi^*_s$ is defined as a value of $\Phi_s$ .
The definitions are local to the namespace ConvexOptAlg.NesterovStrong. β-smoothness duplicates the predicate of other missions of the series and will be merged afterwards. Contributions welcome: proofs of the milestones, and general lemmas on quadratics $z\mapsto c+\frac\alpha2\|z-v\|^2$ that the algebraic milestones need.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §3.7.1, Theorem 3.18, pp. 290–293.
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983.
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

10 thms2 active usersReviewed

Completed

Optimal Transport Optimization Statistics·Captain: mikedeng1

Robust Wasserstein Profile Inference and Applications to Machine Learning 2: ℓp-Regularized Logistic Regression and the Hinge-Loss SVM Are Wasserstein DRO under a Label-Preserving Transport CostResearch Paper

Motivation

Regularized logistic regression and the support vector machine (SVM) are two of the most widely used linear classifiers. Both are usually introduced as empirical risk minimization plus a norm penalty $\|\beta\|_p$ whose size is tuned by cross-validation, with the penalty justified heuristically as a guard against overfitting. Distributionally robust optimization (DRO) offers a different reading: instead of minimizing the average loss on the training sample, minimize the worst average loss over all distributions close to the empirical one. Blanchet, Kang and Murthy (arXiv:1610.05627v4; J. Appl. Probab. 56(3), 2019) show that, for a suitable notion of closeness based on optimal transport, the robust problem and the penalized problem coincide exactly. The penalty is then the price of robustness against perturbations of the predictors, and the regularization parameter becomes the radius of an uncertainty set, which the same paper later chooses by a statistical criterion (the robust Wasserstein profile).

Related earlier work: Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) studied Wasserstein-robust logistic regression with a metric that charges a finite price $\kappa$ for flipping a label, and obtained regularized logistic regression only in the limit $\kappa \to \infty$ . The result formalized here is the exact statement at $\kappa = \infty$ , together with the analogous statement for the hinge loss.

Setting

Training data are pairs $(X_1,Y_1),\dots,(X_n,Y_n)$ with predictors $X_i \in \mathbb R^d$ and labels $Y_i \in \{-1,+1\}$ , $n \ge 1$ . Their empirical distribution is $P_n = \frac1n\sum_{i=1}^n \delta_{(X_i,Y_i)}$ , a probability measure on $Z = \mathbb R^d \times \mathbb R$ .

For a cost $c : Z \times Z \to [0,\infty]$ , the optimal transport cost between probability measures $P$ and $Q$ on $Z$ is

D_c(P,Q) = \inf\big\{\mathbb E_\pi[c(U,W)] : \pi \text{ a probability measure on } Z\times Z,\ \pi_U = P,\ \pi_W = Q\big\}.

The cost used here is the label-preserving cost: for $q \in [1,\infty]$ ,

N_q\big((x,y),(u,v)\big) = \|x - u\|_q \text{ if } y = v, \qquad +\infty \text{ otherwise}.

Every distribution $P$ with $D_{N_q}(P,P_n) < \infty$ has the same label distribution as $P_n$ ; only the predictors are perturbed. The exponent $p$ is the conjugate of $q$ , $1/p + 1/q = 1$ .

The losses are the log-exponential loss $\log(1 + e^{-y\beta^T x})$ and the hinge loss $(1 - y\beta^T x)^+$ , for a coefficient vector $\beta \in \mathbb R^d$ . The worst-case expected loss at radius $\delta \ge 0$ is $\sup\{\mathbb E_P[l] : D_{N_q}(P,P_n) \le \delta\}$ , the supremum over probability measures $P$ on $Z$ .

Formalization targets

Goal: Theorem 2 (p. 11)

For every $\delta \ge 0$ and every $\beta \in \mathbb R^d$ ,

\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[\log(1 + e^{-Y\beta^T X})\big] = \frac1n\sum_{i=1}^n \log(1 + e^{-Y_i\beta^T X_i}) + \delta\|\beta\|_p,

\sup_{P:\ D_{N_q}(P,P_n)\le\delta} \mathbb E_P\big[(1 - Y\beta^T X)^+\big] = \frac1n\sum_{i=1}^n (1 - Y_i\beta^T X_i)^+ + \delta\|\beta\|_p,

and consequently the two identities obtained by taking $\inf_{\beta}$ on both sides, which is how the paper prints the theorem.

Milestones

Proposition 1 (p. 10): strong duality, $\sup_{P: D_c(P,P_n)\le\delta}\mathbb E_P[l] = \min_{\gamma\ge0}\{\gamma\delta + \frac1n\sum_i\varphi_\gamma(X_i,Y_i)\}$ with $\varphi_\gamma(z_0) = \sup_z\{l(z) - \gamma c(z,z_0)\}$ , for a lower semicontinuous cost vanishing on the diagonal, an upper semicontinuous loss and $\delta > 0$ .
Logistic inner supremum (proof of Theorem 2, p. 30): $\sup_x\{\log(1+e^{-y_0\beta^T x}) - \lambda\|x - x_0\|_q\}$ equals the loss at $x_0$ if $\|\beta\|_p \le \lambda$ and $+\infty$ otherwise.
Logistic outer minimisation (p. 30): the infimum over $\lambda \ge 0$ of $\delta\lambda$ plus the average of these suprema equals the regularized empirical loss.
Hinge inner supremum (pp. 30–31) and 5. hinge outer minimisation (p. 31): the same two steps for the hinge loss.

Significance

The theorem identifies two standard estimators as exact solutions of a robust decision problem. Consequences: the penalty $\delta\|\beta\|_p$ has a quantitative meaning (the adversary's transport budget), the regularization parameter can be chosen by the paper's robust Wasserstein profile instead of cross-validation, and the norm of the penalty is tied to the geometry of the perturbations (perturbations measured in $\ell_\infty$ give an $\ell_1$ penalty). The same identity is the input of the paper's coverage bound (Proposition 6) for $\rho = 1$ .

The result is proved on paper; no machine-checked version is known. The formalization adds a precise statement of the objects involved (couplings with both marginals fixed, an infinite cost across labels, expectations of nonnegative losses with values in $[0,\infty]$ ), a checked version of the duality step specialised to this cost, and the treatment of boundary cases ( $\delta = 0$ , $\beta = 0$ , $q \in \{1,\infty\}$ ) that the paper does not discuss.

Difficulty

The identities are short once Proposition 1 is available, so the weight of the mission lies in two places. First, Proposition 1 itself is a strong duality theorem for optimal transport over all probability measures on $\mathbb R^{d+1}$ , with a cost that takes the value $+\infty$ and an unbounded loss, and with attainment of the dual minimum; it is quoted from Blanchet and Murthy (Math. Oper. Res. 2019) and not proved in this paper. The weak-duality inequality is routine; the reverse inequality requires constructing near-optimal distributions from the dual, which needs measurable selection of near-maximizers and does not follow from finite-dimensional convex duality. Second, the inner suprema require an exact Hölder-attainment argument for the pair of conjugate norms $\ell_p$ and $\ell_q$ , including $q = 1$ and $q = \infty$ , and for the hinge loss a minimax exchange over $\alpha \in [0,1]$ . Bypassing duality by a direct construction of the worst distribution is possible for the upper value but not obviously for the lower bound at the boundary $\lambda = \|\beta\|_p$ .

Formalization scope

Predictors are Fin d → ℝ, a data point is (Fin d → ℝ) × ℝ with the product Borel σ-algebra, and samples are indexed by Fin n with 0 < n. Labels are real numbers with the hypothesis $Y_i \in \{-1,+1\}$ , which Theorem 2 inherits from Example 2; the cost $N_q$ is defined on all of $\mathbb R^d\times\mathbb R$ .
The $\ell_q$ norm is the norm of PiLp q, with q p : ℝ≥0∞ and p.HolderConjugate q; $q = 1$ and $q = \infty$ are included, and no further restriction on $q$ is imposed.
The transport cost is an infimum in $[0,\infty]$ over probability measures on $Z\times Z$ with both marginals fixed. Expectations are lower Lebesgue integrals of the nonnegative losses, and the worst case is a supremum in $[0,\infty]$ over probability measures. The empirical distribution is the published platform definition WassersteinDRO.Regularization.empiricalDistribution.
Readings. The paper prints the SVM identity without $\inf_\beta$ on the right; the goal states the per- $\beta$ identities (what the proof establishes) and the identities of infima with $\inf_\beta$ on both sides. The proof's displays write the transport norm as $\|\cdot\|_p$ and the penalty as $\|\beta\|_q$ , the reverse of the theorem; milestones use the theorem's convention. The logistic chain's printed indicators $\mathbf 1_{\{\lambda>\|\beta\|\}}$ , $\infty\mathbf 1_{\{\lambda\le\|\beta\|\}}$ should read $\ge$ and $<$ ; the stated end-to-end identity is unaffected. Proposition 1 is stated with a fixed nonnegative loss and $\delta > 0$ .
A trivializing formalization is ruled out: a cost infimum over sub-probability couplings or with one marginal free, or a Bochner expectation that vanishes on non-integrable laws, would make the worst case $+\infty$ or $0$ ; the definitions here fix both marginals, use probability measures only and integrate in $[0,\infty]$ . At $\delta = 0$ the ball is $\{P_n\}$ and both sides reduce to the empirical loss.
Infrastructure needed: optimal-transport duality with extended-valued lower semicontinuous costs (reusable well beyond this mission), Hölder equality cases for PiLp, and calculus for the logistic function. Contributions to any of these are welcome, as are proofs of the inner suprema, which are independent of Proposition 1.

Selected references

J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019; arXiv:1610.05627v4. https://arxiv.org/abs/1610.05627
J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, NIPS 2015. https://arxiv.org/abs/1509.09259

12 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity VIII: No Black-Box Method Beats 3β‖x₁ − x*‖²/(32(t + 1)²) on β-Smooth Convex FunctionsTextbook

Why lower bounds for first-order methods

Upper bounds for an optimization method say how fast it converges; oracle complexity lower bounds say how fast any method of a given kind can possibly converge. Chapter 3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015, arXiv:1405.4980) proves upper bounds for subgradient descent on Lipschitz functions and for gradient methods on smooth functions. Section 3.5 (Lower bounds, pp. 279–283) shows that these rates cannot be improved by more than a numerical constant, as long as the number of queries is smaller than the dimension. For smooth convex functions the matching lower bound is what identifies Nesterov's accelerated gradient descent, with its $1/t^2$ rate, as an optimal method.

Timeline. The lower bounds first appeared in A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization (Wiley, 1983). The presentation followed by the book, with an explicit tridiagonal quadratic as the hard instance and the "span of past gradients" restriction on the method, is that of Y. Nesterov, Introductory Lectures on Convex Optimization (Kluwer, 2004), §2.1.2. Nesterov's accelerated method (1983) attains the matching upper bound.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^\top y$ , coordinates $x(1),\dots,x(n)$ , canonical basis $e_1,\dots,e_n$ and balls $\mathrm B_2(R)=\{x:\|x\|\le R\}$ . A first-order oracle for $f$ answers a query $x$ with a subgradient $g\in\partial f(x)$ (the gradient when $f$ is differentiable). A black-box procedure maps the history $(x_1,g_1,\dots,x_t,g_t)$ to the next query $x_{t+1}$ . Section 3.5 restricts attention to procedures with

x_1=0,\qquad x_{t+1}\in\mathrm{Span}(g_1,\dots,g_t)\quad(t\ge0), \tag{3.15}

which covers gradient descent, its accelerated variants and conjugate gradient. A function is $\beta$ -smooth if its gradient is $\beta$ -Lipschitz; $L$ -Lipschitz on $\mathcal X$ if every subgradient at every point of $\mathcal X$ has norm at most $L$ ; $\alpha$ -strongly convex if $x\mapsto f(x)-\frac\alpha2\|x\|^2$ is convex.

The hard smooth instance uses, for $k\le n$ , the symmetric tridiagonal matrix $A_k$ with entries $2$ on the first $k$ diagonal positions and $-1$ on the neighbouring off-diagonal positions of the leading $k\times k$ block, zero elsewhere, and the quadratics

f_k(x)=\frac\beta8x^\top A_kx-\frac\beta4x^\top e_1 ,\qquad f_k^*=\inf_{x\in\mathbb R^n}f_k(x).

Formalization targets

Goal: Theorem 3.14 (p. 282)

For $1\le t\le\frac{n-1}2$ and $\beta>0$ there are a $\beta$ -smooth convex $f$ and a minimizer $x^*$ such that every procedure satisfying (3.15) has

\min_{1\le s\le t}f(x_s)-f(x^*)\ \ge\ \frac{3\beta}{32}\,\frac{\|x_1-x^*\|^2}{(t+1)^2}.

The constant $3/32$ is the book's.

Milestones (proof of Theorem 3.14, pp. 282–283)

$0\preceq A_k\preceq4I_n$ , through $x^\top A_kx=x(1)^2+x(k)^2+\sum_{i=1}^{k-1}(x(i)-x(i+1))^2$ .
For $f=f_{2t+1}$ and any procedure satisfying (3.15), $x_s\in\mathrm{Span}(e_1,\dots,e_{s-1})$ ; hence $f(x_s)=f_s(x_s)$ for $s\le t$ .
$x_k^*(i)=1-\frac i{k+1}$ solves $A_kx=e_1$ , minimizes $f_k$ , and $f_k^*=-\frac\beta8\bigl(1-\frac1{k+1}\bigr)$ .
$\|x_k^*\|^2\le\frac{k+1}3$ .
$f_t^*-f_{2t+1}^*=\frac\beta8\bigl(\frac1{t+1}-\frac1{2t+2}\bigr)\ge\frac{3\beta}{32}\frac{\|x^*_{2t+1}\|^2}{(t+1)^2}$ .

Companion: Theorem 3.13 (p. 280)

For $1\le t\le n$ and $L,R>0$ there are a convex $f$ , $L$ -Lipschitz on $\mathrm B_2(R)$ , and a first-order oracle for it such that every procedure satisfying (3.15) has $\min_{s\le t}f(x_s)-\min_{\mathrm B_2(R)}f\ge\frac{RL}{2(1+\sqrt t)}$ ; and for $\alpha>0$ there are an $\alpha$ -strongly convex $f$ , $L$ -Lipschitz on $\mathrm B_2(\frac L{2\alpha})$ , and an oracle with gap at least $\frac{L^2}{8\alpha t}$ over that ball.

Significance

The upper bounds of Chapter 3 (projected subgradient descent at rate $RL/\sqrt t$ , accelerated gradient descent at rate $\beta\|x_1-x^*\|^2/t^2$ ) become optimal statements only through these lower bounds: no method in the class (3.15) can be faster by more than a constant factor while $t$ is below the dimension. The restriction to $t\lesssim n$ is necessary, since Chapter 2's cutting-plane methods converge exponentially once the number of queries exceeds the dimension.

The results are classical and proved. Formalizing them yields machine-checked versions of the quadratic-form computation for the tridiagonal matrix, of the Krylov-type support argument under (3.15), and of the explicit minimizer of $f_k$ , each reusable in other lower-bound arguments (Theorem 3.15 in $\ell_2$ , lower bounds for strongly convex smooth functions, conjugate gradient analyses). The platform held no formal statement of these oracle lower bounds when this mission was drafted.

Difficulty

Each analytic step is elementary; the difficulty is in the bookkeeping. The span argument is an induction that must track, at each step, that the gradient of a tridiagonal quadratic at a vector supported on the first $s-1$ coordinates is supported on the first $s$ , and that the span hypothesis transfers this to the next query. The minimizer computation requires solving $A_kx=e_1$ on the leading block and showing that the coordinates beyond $k$ do not affect $f_k$ . A natural first attempt, choosing the hard function after seeing the procedure, proves a much weaker statement and is excluded by the quantifier order: the function is fixed first and must defeat every procedure.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Coordinates in Lean are 0-based; the definitions provide the book's 1-based coordinate coord x i and basis vector basisVec n i, and the matrix tridiag n k translates book index $i$ to Fin n index $i-1$ . The query sequence starts at index $1$ . The oracle is a fixed map $g$ , so (3.15) reads $x_{t+1}\in\mathrm{Span}(g(x_1),\dots,g(x_t))$ with $x_1=0$ . In Theorem 3.14 the oracle is the gradient, given as a map with HasGradientAt everywhere; $\beta$ -smoothness is the Lipschitz bound on that map. In Theorem 3.13 the oracle is part of what is constructed, because the book's proof uses a specific "resisting" subgradient selection and the claim fails for an arbitrary one.

Committed conventions, each stated in the item's Formalization Note: the minimum over $1\le s\le t$ is the bound for every such $s$ , and $t\ge1$ is required; $t\le(n-1)/2$ is $2t+1\le n$ ; the minimizer $x^*$ is existentially chosen together with $f$ (the hard function has many minimizers when $2t+1<n$ , and the bound is false for some of them); the minimum over a ball is the bound against every point of the ball; $f_k^*$ is the real infimum, asserted to be attained.

A formalization that let the function depend on the procedure, dropped $x_1=0$ , or took the span over gradients at points other than the queries would state a different and weaker theorem; the statements here keep $f$ (and the oracle) before the universally quantified procedure.

Infrastructure needed: quadratic forms of explicit matrices on EuclideanSpace, gradients of quadratics, and span/support lemmas for EuclideanSpace.single-type vectors. Contributions of proofs for any milestone, and of the strongly convex $\ell_2$ lower bound (Theorem 3.15, not included here), are welcome.

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.4980
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

8 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity VII: Conditional Gradient Descent (Frank–Wolfe) with γ_s = 2/(s + 1) Has Rate 2βR²/(t + 1) in Any NormTextbook

Motivation

Many constrained optimization problems in machine learning and statistics have a feasible set $\mathcal X$ over which a linear function is cheap to minimize but a Euclidean projection is expensive: the $\ell_1$ -ball, the simplex, the nuclear-norm ball, the convex hull of a combinatorial family. Projected gradient descent needs a projection at every step. Conditional gradient descent, introduced by Frank and Wolfe in 1956 for quadratic programming, replaces the projection by a call to a linear minimization oracle over $\mathcal X$ , and its iterates are convex combinations of oracle outputs, which makes them sparse when $\mathcal X$ is a polytope.

This mission is the seventh of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980v2). It covers Section 3.3, whose main result, Theorem 3.8, is the $O(1/t)$ rate of the method in the form given by Jaggi (2013), going back to Dunn and Harshbarger (1978).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ . For a linear form $g$ on $E$ , written $v\mapsto g^\top v$ , the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$ . Let $\mathcal X\subseteq E$ be nonempty, compact and convex, with diameter $R=\sup_{x,y\in\mathcal X}\|x-y\|$ .

Let $f:E\to\mathbb R$ be differentiable with gradient $\nabla f(x)$ , a linear form on $E$ . For $\beta\ge0$ , $f$ is β-smooth with respect to $\|\cdot\|$ on $\mathcal X$ if

\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|\qquad(x,y\in\mathcal X).

A point $x^*\in\mathcal X$ with $f(x^*)=\min_{x\in\mathcal X}f(x)$ is fixed throughout, and $\delta_t=f(x_t)-f(x^*)$ .

Given step sizes $(\gamma_s)_{s\ge1}$ , a run of conditional gradient descent is a pair of sequences with $x_1\in\mathcal X$ and, for every $t\ge1$ ,

y_t\in\operatorname*{argmin}_{y\in\mathcal X}\nabla f(x_t)^\top y\quad(3.8),\qquad x_{t+1}=(1-\gamma_t)x_t+\gamma_ty_t\quad(3.9).

The minimizer $y_t$ need not be unique; any choice is allowed.

Formalization targets

Goal: Theorem 3.8 (p. 272)

If $f$ is convex and $\beta$ -smooth with respect to $\|\cdot\|$ and $\gamma_s=\frac{2}{s+1}$ for $s\ge1$ , then every run satisfies, for every $t\ge2$ ,

f(x_t)-f(x^*)\le\frac{2\beta R^2}{t+1}.

Milestones

Inequality (3.4) in an arbitrary norm (p. 267, used on p. 272): for $x,y\in\mathcal X$ , $0\le f(x)-f(y)-\nabla f(y)^\top(x-y)\le\frac{\beta}{2}\|x-y\|^2$ .
The one-step recursion (pp. 272–273): for any run with $\gamma_s\in[0,1]$ ,

\delta_{s+1}\le(1-\gamma_s)\delta_s+\frac{\beta}{2}\gamma_s^2R^2 .

Initialization (p. 273): if $\gamma_1=1$ , then $\delta_2\le\frac{\beta}{2}R^2$ .
The induction (p. 273): a real sequence with $\delta_2\le\frac{\beta}{2}R^2$ and the recursion of milestone 2 with $\gamma_s=\frac{2}{s+1}$ for $s\ge2$ satisfies $\delta_t\le\frac{2\beta R^2}{t+1}$ for $t\ge2$ .

Significance

Theorem 3.8 is the basic guarantee for projection-free first-order optimization. Its rate does not depend on the dimension, and it depends on the geometry only through the product $\beta R^2$ , both measured in the same norm, which may be chosen to fit $\mathcal X$ : for the $\ell_1$ -ball, smoothness in $\|\cdot\|_1$ with dual norm $\|\cdot\|_\infty$ gives much better constants than the Euclidean analysis. The book applies it this way to a LASSO-type problem (Section 3.3, pp. 274–276), and the same bound underlies the sparse-approximation corollary on the simplex (p. 273) and the many later variants of the method (away steps, stochastic and online conditional gradient).

The result is classical and proved in the book. What this mission adds is a machine-checked statement and proof in an arbitrary finite-dimensional normed space, with the dual norm as the operator norm on linear forms, and a reusable encoding of norm-smoothness and of conditional gradient runs. On Prove2Me a related result is already proved: Lan's Theorem 7.1 (First-order and Stochastic Optimization Methods), which bounds $f(y_k)-f^*$ by $\frac{2L}{k(k+1)}\sum_{i\le k}\|x_i-y_{i-1}\|^2$ with a different indexing; after the diameter bound it yields $2\beta R^2/t$ at Bubeck's iterate $x_t$ , which is weaker than Theorem 3.8 by one step.

Difficulty

The difficulty is in the bookkeeping of norms and indices, not in a deep idea. Inequality (3.4) is proved in the book only for the Euclidean norm, where $\nabla f(x)\in\mathbb R^n$ and the Cauchy–Schwarz inequality is used; in a general norm it needs the pairing between a linear form and a vector and the bound $|g^\top v|\le\|g\|_*\|v\|$ . The rate $2\beta R^2/(t+1)$ is attained only by starting the induction at $t=2$ , where the step $\gamma_1=1$ erases the dependence on the starting point; at $t=1$ the bound can fail, since $\delta_1$ is arbitrary. A first attempt that runs the induction from $t=1$ with an arbitrary $\delta_1$ does not give the stated constant.

Formalization scope

$E$ is a type with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]; nothing is specialised to the Euclidean norm. The gradient is an explicit derivative map f' : E → (E →L[ℝ] ℝ) with HasFDerivAt f (f' x) x for every x; $\nabla f(x)^\top v$ is f' x v, and $\|\cdot\|_*$ is the operator norm, which equals $\sup_{\|v\|\le1}g^\top v$ . $R$ is Metric.diam X, which equals the supremum of $\|x-y\|$ over $\mathcal X$ because $\mathcal X$ is compact. Sequences are indexed by ℕ with the first iterate at index 1.

Committed conventions: $\mathcal X$ compact, convex and containing $x^*$ (hence nonempty); convexity of $f$ and the Lipschitz bound on the gradient are assumed on $\mathcal X$ only, which is weaker than the book's global assumptions; $\beta\ge0$ ; the existence of the minimizer $x^*$ is the book's standing assumption (p. 242); the conclusion is stated for $t\ge2$ , as in the book. Runs are predicates: $y_t$ is any minimizer of the linear form over $\mathcal X$ and $y_t\in\mathcal X$ is required, so the goal quantifies over every run with $\gamma_s=2/(s+1)$ . A formalization in which $y_t$ need not lie in $\mathcal X$ , or in which smoothness is assumed only along the iterates, states a different theorem and is excluded.

A complete development needs the descent inequality (3.4) for Fréchet derivatives in a normed space (reusable for every smooth method in the series and beyond), the fact that the iterates stay in $\mathcal X$ , and a scalar induction. Proofs of the milestones are welcome independently; milestone 4 is a statement about real sequences only.

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.4980
M. Frank and P. Wolfe, An algorithm for quadratic programming, Naval Research Logistics Quarterly 3(1–2):95–110, 1956. https://doi.org/10.1002/nav.3800030109
J. C. Dunn and S. Harshbarger, Conditional gradient algorithms with open loop step size rules, Journal of Mathematical Analysis and Applications 62(2):432–444, 1978. https://doi.org/10.1016/0022-247X(78)90137-3
M. Jaggi, Revisiting Frank–Wolfe: projection-free sparse convex optimization, Proceedings of ICML 2013, PMLR 28(1):427–435. https://proceedings.mlr.press/v28/jaggi13.html
G. Lan, First-order and Stochastic Optimization Methods for Machine Learning, Springer, 2020, Theorem 7.1. https://doi.org/10.1007/978-3-030-39568-1

6 thms2 active usersReviewed

Missions

Robust Regression and Lasso 4: ‖b − Ax‖₂ + √n c‖x‖₁ + √n c Equals the Worst Case of √(n·E_μ[(b′ − r′ᵀx)²]) over Box-Constrained Distribution ClassesResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 3, Eq. (8)

Milestones (Appendix D)

Significance

Difficulty

Formalization scope

Selected references

Robust Regression and Lasso 1: Under Feature-Wise Norm-Bounded Column Disturbances, Worst-Case Least-Norm Regression Is Exactly ℓ1-Regularized Regression ‖b − Ax‖₂ + Σ cᵢ|xᵢ|Research Paper

Why robustness and the Lasso belong together

Setting

Formalization targets

Goal: Theorem 1 (p. 4)

Milestones (in the order the proof uses them)

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning II: The Gradient of the Normalized Discounted Value Is the Sum over Actions of ∇π·Q under the Discounted Future State DistributionTextbook

Why the gradient of the value matters

Setting

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning I: Approximate Policy Iteration with Max-Norm Evaluation Error ε Is Eventually Within 2ε/(1−γ)² of OptimalTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Analysis of Temporal-Difference Learning with Function Approximation 2: For Every Sampling Distribution q and 5/6 < α < 1, Off-Line q-Sampled TD(0) Can Diverge in ExpectationResearch Paper

Motivation

Setting

Formalization targets

Divergence of the mean

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

Consistent Nonparametric Regression II: Nearest-Neighbor Weights with Vanishing Coefficients Are Consistent for Every Distribution of X (Theorem 2)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 600)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Consistent Nonparametric Regression III: Consistent Probability Weights Give Consistent Estimators of Conditional Quantiles (Theorem 3)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 604)

Milestones

Significance

Difficulty