Machine Learning

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)

1. 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$.
2. 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| .$$

3. 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

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

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

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

1. 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$.
2. §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

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

1. 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).$$

2. 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}$.
3. Theorem 2.6, case $0 \le q < 1$.
4. 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

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.

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