Machine Learning

Motivation

In the local model of differential privacy, each individual randomizes their own data before handing it to an untrusted learner. Local protocols are the deployed form of private data collection, and in practice every round of interaction with the population is expensive: the learner must broadcast new instructions and wait for new reports. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are those of arXiv v3) show that local learning is equivalent to learning with statistical queries (SQ) in the sense of Kearns (1998), and that the equivalence maps noninteractive local learners to nonadaptive SQ learners. The question whether interaction is ever necessary in the local model therefore becomes the question whether adaptivity is ever necessary for SQ learning.

This mission formalizes the paper's answer (§5.3, Theorem 5.16): a concept class, MASKED-PARITY, that an adaptive SQ learner learns exactly with $d+1$ queries in two rounds, while every nonadaptive SQ learner with fewer than exponentially many queries fails against a specific valid oracle, under the uniform distribution on examples.

Setting

Fix $d$, a power of two. The domain is $D=\{0,1\}^d\times\{0,1\}^{\log d}\times\{0,1\}$, with points $u=(x,i,b)$, and examples are drawn from the uniform distribution $\mathcal D$ on $D$. For $r\in\{0,1\}^d$ and $a\in\{0,1\}$, the concept $c_{r,a}:D\to\{+1,-1\}$ is

$$c_{r,a}(x,i,b)=\begin{cases}(-1)^{r\odot x+a}&b=0,\\(-1)^{r_i}&b=1,\end{cases}$$

where $r\odot x$ is the inner product modulo 2. MASKED-PARITY is the class $\{c_{r,a}\}$: on the half $b=0$ it is the parity $r$ or its negation, according to the mask $a$; on the half $b=1$ it reveals the bit $r_i$.

A statistical query is a function $g(u,y)$ of an example and a label together with a tolerance $\tau$. The SQ oracle for the target $c$ answers with any real $v$ such that $|v-\mathbb E_{u\sim\mathcal D}[g(u,c(u))]|\le\tau$; the learner must succeed for every such answer. An SQ learner is nonadaptive if it fixes all its queries before receiving any answer, and adaptive otherwise. Write $\langle f,h\rangle=\mathbb E_{u\sim\mathcal D}[f(u)h(u)]$ and $\mathrm{err}(f,h)=\Pr_{u\sim\mathcal D}[f(u)\ne h(u)]$.

The lower bound uses the decomposition of a query into $f_g(u)=\frac{g(u,1)-g(u,-1)}2$ and $C_g=\frac12\mathbb E[g(u,1)+g(u,-1)]$, the restrictions $c^s_{r,a}$, $f^s_g$ of $c_{r,a}$ and $f_g$ to the half $b=s$ (equation (6)), and the oracle

$$\mathcal O_{c_{r,a},\mathcal D}(g,\tau)=\begin{cases}C_g+\langle f^1_g,c^1_{r,a}\rangle&\text{if }|\langle f^0_g,c^0_{r,a}\rangle|<\tau,\\ \mathbb E[g(u,c_{r,a}(u))]&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 5.16 (p. 27)

1. There is a two-round SQ learner ($d$ queries, then one), with $\{0,1\}$-valued queries of tolerance at least $\frac1{4d+1}$, that outputs $c_{r,a}$ for every target and every valid answers.
2. $\mathcal O$ is a valid SQ oracle, and every nonadaptive learner making $t$ queries with values $\pm1$ and tolerance at least $2^{-d/3}$, run against $\mathcal O$ on a uniformly random target, satisfies

$$\Pr_{c_{\bar r,\bar a}}\Bigl[\mathrm{err}(c_{\bar r,\bar a},h)\ge\tfrac14\Bigr]\ge\frac12-\frac t{2^{d/3+2}}.$$

Milestones

• Proposition 5.18 (p. 28): the learner $\mathcal A_{\mathrm{MP}}$ recovers $\hat r=r$ and $\hat a=a$ from every valid answers.
• Equation (7) (p. 29): $\mathbb E[g(u,c_{r,a}(u))]=C_g+\langle f^0_g,c^0_{r,a}\rangle+\langle f^1_g,c^1_{r,a}\rangle$.
• The oracle (p. 30): $\mathcal O$ is valid and answers identically on $c_{r,0}$ and $c_{r,1}$ when $|\langle f^0_g,c^0_{r,0}\rangle|<\tau$.
• Orthogonality (p. 30): $\langle c^0_{r,a},c^0_{r',a}\rangle$ is $1/2$ if $r=r'$ and $0$ otherwise.
• Bessel bound (p. 30): $\sum_{(r,a)}2\langle f^0_g,c^0_{r,a}\rangle^2\le1$ for $\pm1$-valued $g$.
• Counting (p. 30): at most $2^{2d/3-1}$ pairs $(r,a)$ have $|\langle f^0_g,c^0_{r,a}\rangle|\ge2^{-d/3}$.
• $\Pr[\mathit{Good}]\ge1-t/2^{d/3+2}$ (p. 30).

Significance

The result. Combined with the paper's equivalence between local and SQ learning (Theorem 5.14), Theorem 5.16 shows that interaction is sometimes necessary in local differential privacy: there is a class learnable by an interactive local protocol with polynomially many examples, but not by any noninteractive one with fewer than exponentially many (Corollary 5.17). The separation concerns strong learning under a fixed distribution; the paper notes that adaptive and nonadaptive SQ learning coincide for weak learning, and that a distribution-free separation was left open.

Formalizing it. The result is proved in the paper and has, to our knowledge, no machine-checked proof. The mission produces a self-contained Lean model of statistical query learning with labelled queries and adversarial oracles, a finite Fourier calculus for parities on $\{0,1\}^d$ (orthogonality and a Bessel inequality for $\pm1$-valued functions), and the counting and union-bound argument of SQ lower bounds. The proof of part (2) contains several printed slips (listed below); a formal proof settles the corrected argument.

Difficulty

The upper bound is a direct computation. The difficulty is in part (2): the learner's hypothesis may be any function, not a concept of the class, and the lower bound must hold for every nonadaptive strategy at once. A naive argument that each query "reveals little about $a$" fails, because the true answer to a query does depend on $a$; the argument needs an oracle that is valid (within tolerance of the truth) and yet independent of $a$ on most targets, and a quantitative bound on how many targets any single $\pm1$-valued query can correlate with on the half $b=0$. That bound is an $L^2$ statement over all $2^{d+1}$ concepts, not a pointwise one.

Formalization scope

• Domain and distribution. The index $i\in\{0,1\}^{\log d}$ is encoded as Fin d, and every theorem assumes $d=2^m$ (implicit in the paper). Vectors are Fin d → ZMod 2, with 0-based bits. Expectations are averages over the finite domain; probabilities over the target are counts of pairs $(r,a)$ divided by $2^{d+1}$.
• Values. Concepts, hypotheses and queries are real-valued; labels $\pm1$ are reals. Queries in part (1) take values in $\{0,1\}$, as $\mathcal A_{\mathrm{MP}}$'s do; queries in part (2) take values $\pm1$ on labels $\pm1$, as in the paper's proof. The paper allows non-Boolean queries (p. 19); a version of part (2) for real queries with values in $[-1,1]$ is a true strengthening that the same argument supports, and is not stated.
• Oracles. An SQ oracle is adversarial within the tolerance: the upper bound holds for every valid answer. Part (2) exhibits the paper's oracle $\mathcal O$ and asserts its validity for every $\tau>0$. Without that conjunct an "oracle" that ignores the tolerance would make part (2) trivial; the statement rules this out.
• Learners. Learners are deterministic structures (a nonadaptive learner is a list of queries and tolerances plus an output map; a two-round learner's second-round queries are functions of the first-round answers). A randomized learner is a mixture over its coins and the bounds hold coin by coin. "Efficient" is not modelled. The informal "with a polynomial number of queries" is formalized through its quantitative "Specifically" sentence.
• Real powers. $2^{d/3}$, $2^{2d/3-1}$ and $2^{d/3+2}$ are real powers; no natural-number division is used.
• Corrections of the proof (not of the theorem). The event $\mathit{Good}$ on p. 30 is printed with $c_{\bar r,\bar a}$ and $\le$; the milestone uses $c^0_{\bar r,\bar a}$ and the strict $<$, which is what the counting display and the oracle's test require. The quotient $2^{2d/3-1}/2^{d+1}$ is printed as $2^{-d/3}$ and equals $2^{-d/3-2}$; "$c^0_{r,0}=-c^0_{r,0}$" should read $c^0_{r,1}=-c^0_{r,0}$. The final display of the proof gives $\frac12(1-t/2^{d/3+2})$, which is at least the theorem's bound.

Contributions welcome: the Fourier facts for $\{0,1\}^d$ (reusable for any parity-based SQ lower bound), the general decomposition (7), and the probability bound of part (2) from the milestones.

Selected references

• S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090.
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. DOI 10.1145/293347.293351.
• A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly learning DNF and characterizing statistical query learning using Fourier analysis, STOC 1994. DOI 10.1145/195058.195147.
• N. Bshouty, V. Feldman, On using extended statistical queries to avoid membership queries, J. Mach. Learn. Res. 2 (2002) 359–395. JMLR.

Motivation

Approximate dynamic programming replaces the exact value functions of a Markov decision process by approximations, typically produced by a regression algorithm. The classical guarantees for the resulting policies are stated in the max norm: if every state-action value is estimated to within $\varepsilon$ uniformly over the state space, the greedy policy loses at most a multiple of $\varepsilon$ (Williams and Baird 1993; Bertsekas and Tsitsiklis 1996). Regression algorithms, however, control an average error under the distribution on which they are trained, not a worst-case error, so these guarantees rarely apply to the approximations actually computed.

Chapter 5 of S. M. Kakade's PhD thesis (On the Sample Complexity of Reinforcement Learning, UCL 2003, pp. 57–66) identifies the distribution under which the error of an approximate policy iteration algorithm should be measured. For the finite-horizon, non-stationary approximate policy iteration algorithm (NAPI), the loss relative to any competitor policy is bounded by twice the horizon times the regression error averaged under the future state-time distribution of that competitor. Taking the competitor optimal, the relevant "test" distribution is the one visited by an optimal policy, generally not the distribution on which the regressor was trained; the thesis calls this the "mismeasure" of reinforcement learning. The key tool, the performance difference lemma, was proved for the discounted case by Kakade and Langford (ICML 2002) and is used throughout the conservative policy iteration and policy search literature.

Setting

A $T$-epoch MDP has a finite state set $S$, a finite nonempty action set $A$, decision epochs $t\in\{0,\dots,T-1\}$, a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$. A policy $\pi$ is a sequence of decision rules $\pi(\cdot\mid s,t)$, distributions on $A$; it may be stochastic and non-stationary. A deterministic policy $h$ chooses the action $h(s,t)$.

Values are normalized. The $t$-value is $V_{\pi,t}(s)=\frac1T\mathbb E\big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\mid s_t=s\big]$, so $V_{\pi,t}=0$ for $t\ge T$ and

$$V_{\pi,t}(s)=\sum_a\pi(a\mid s,t)\Big(\tfrac1T r(s,a)+\sum_{s'}P(s'\mid s,a)V_{\pi,t+1}(s')\Big),\qquad V_\pi=V_{\pi,0}.$$

The 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')$, the advantage is $A_{\pi,t}=Q_{\pi,t}-V_{\pi,t}$, and the optimal value is $V^*(s)=\sup_\pi V_\pi(s)$. The future state-time distribution of $\pi$ from $s_0$ is

$$d_{\pi,s_0}(s,t)=\tfrac1T\Pr(s_t=s\mid\pi,s_0)\quad\text{on } S\times\{0,\dots,T-1\}.$$

NAPI (Algorithm 6) starts from an arbitrary deterministic policy and updates its decision rules backwards, $t=T-1,\dots,0$: at update $t$ a PolicyChooser receives the current policy $\pi$ and returns a decision rule $h_t$, which replaces the rule at time $t$. The output is $(h_0,\dots,h_{T-1})$. With RegressionPolicyChooser (Algorithm 7), a regressor returns an approximation $\tilde Q_{\pi,t}$ of $Q_{\pi,t}$ and $h_t$ is greedy for it. The per state error and per state regression error at update $t$ are

$$\varepsilon_t(s)=\max_aQ_{\pi,t}(s,a)-Q_{\pi,t}(s,h_t(s)),\qquad \tilde\varepsilon_t(s)=\max_a|Q_{\pi,t}(s,a)-\tilde Q_{\pi,t}(s,a)|,$$

both measured against the input policy $\pi$ of update $t$.

The discounted companions use the normalized discounted value $V_{\pi,\gamma}=(1-\gamma)\mathbb E[\sum_t\gamma^tr(s_t,a_t)]$, its advantage $A_{\pi,\gamma}$, and the Bellman error $B_J=\sup_{s,a}|Q_J(s,a)-J(s)|$ of a state vector $J$, where $Q_J(s,a)=(1-\gamma)r(s,a)+\gamma\mathbb E_{s'}J(s')$.

Formalization targets

Goal: Theorem 5.3.2 (p. 64)

For the policy $\pi$ returned by NAPI with RegressionPolicyChooser, every policy $\pi'$ and every state $s_0$,

$$V_\pi(s_0)\ \ge\ V_{\pi'}(s_0)-2T\,\mathbb E_{(s,t)\sim d_{\pi',s_0}}\big[\tilde\varepsilon_t(s)\big].$$

The regression outputs are arbitrary; the statement holds for every regressor and every tie-breaking rule.

Milestones

• Lemma 5.2.1, undiscounted (p. 59): $V_{\pi'}(s_0)-V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi',s_0}}\mathbb E_{a\sim\pi'(\cdot\mid s,t)}[A_{\pi,t}(s,a)]$.
• Lemma 5.3.1 (p. 63): for NAPI's output $\tilde\pi$ and the input policy $\pi$ of update $t$, $Q_{\tilde\pi,t}=Q_{\pi,t}$ and $A_{\tilde\pi,t}(s,a)\le\varepsilon_t(s)$.
• Display in the proof of Theorem 5.3.2 (p. 64): $\varepsilon_t(s)\le2\tilde\varepsilon_t(s)$ when $h_t$ is greedy for $\tilde Q_{\pi,t}$.
• Corollary 5.2.2 (p. 61): $V_\pi(s_0)\ge V^*(s_0)-T\|A_{\pi,t}\|_\infty$ and $V_{\pi,\gamma}(s_0)\ge V^*_\gamma(s_0)-\frac{1}{1-\gamma}\|A_{\pi,\gamma}\|_\infty$.
• Theorem 5.1.3 (Williams–Baird, p. 59): a policy greedy for $Q_J$ satisfies $V_{\pi,\gamma}(s)\ge V^*_\gamma(s)-\frac{2B_J}{1-\gamma}$.

The discounted half of Lemma 5.2.1 is already on the platform as ApproxOptRL.CPI.performance_difference and is referenced, not restated.

Significance

The goal replaces a max-norm hypothesis by an average one, under an explicit distribution. Its consequences: the approximation error only matters on the state-time pairs an optimal (or any good) policy visits; a regressor trained under a distribution $\mu$ over state-times performs well when $\mu$ resembles the state-time distribution of a good policy; and only one factor of the horizon $T$ appears, against two factors of $1/(1-\gamma)$ in the max-norm bounds for discounted approximate value and policy iteration (Chapter 3 of the thesis). The same chain, Lemma 5.2.1 and Lemma 5.3.1, underlies the μ-policy search analysis of Chapter 6 and, in the discounted case, conservative policy iteration.

All statements are proved in the thesis; none of the finite-horizon ones is formalized on the platform. A related performance difference identity, FoundationsRL.RLBasics.performance_difference, is proved on the platform for episodic MDPs with layer-dependent kernels and unnormalized values, with roll-in by one policy; it is the same mathematics up to the $1/T$ normalization but a different object, and is not reused. The mission produces a reusable normalized $T$-epoch layer (values, advantages, state-time distributions) and machine-checked proofs of the chapter's results.

Difficulty

The obvious approach to Theorem 5.3.2 compares $V_\pi$ with $V_{\pi'}$ through max-norm contraction arguments, as in the discounted analysis of Chapter 3; that route only yields a bound in terms of $\max_{s,t}\tilde\varepsilon_t(s)$ and loses the averaging under $d_{\pi',s_0}$. The averaged bound needs an exact identity between value differences and advantages along the competitor's trajectory distribution, which for non-stationary stochastic competitors requires a careful telescoping over epochs of the state distribution recursion. The second difficulty is bookkeeping in the algorithm: the regression error at update $t$ is measured against the input policy of that update, whose decision rules at later times have already been replaced, while the bound concerns the returned policy; relating the two requires showing that later updates do not change $Q_{\cdot,t}$.

Formalization scope

• Model. S, A are Fintypes with decidable equality, A nonempty; P s a s' is $P(s'\mid s,a)$ with IsTransitionKernel P; rewards satisfy 0 ≤ r s a ≤ 1 in every statement (the thesis's standing assumption, p. 22). The thesis also allows infinite state spaces; here S is finite.
• Epochs and normalization. Epochs are 0-based, $t\in\{0,\dots,T-1\}$, with 0 < T. All values carry the factor $1/T$ (discounted: $1-\gamma$), and $d_{\pi,s_0}$ carries $1/T$; the constants $T$ and $2T$ are right only in this normalization.
• Policies. A policy is ℕ → S → A → ℝ, valid when every rule at a time $t<T$ is a distribution. Deterministic policies ℕ → S → A enter through their indicator policies. $V^*$ is the supremum over the subtype of valid policies. Discounted statements use the published ApproxOptRL.Shared.Model; $V^*_\gamma$ is the value of an optimal stationary policy.
• The NAPI run is an explicit recursion (napiPolicy): the policy after updates $T-1,\dots,t$, so the input of update $t$ is the policy at stage $t+1$ and the output is the policy at stage $0$. The printed loop "For $t=T-1,\dots,1$" omits the update at $t=0$, which would leave the time-0 rule random and make the theorem false; the loop here runs to $t=0$, as in the proof and in Algorithms 8–9.
• Ruled out. A "run" whose returned policy is unconstrained, or regression errors measured against the returned policy instead of the input policy of each update, would trivialize or alter the goal; both are excluded by the explicit recursion. That the two measurements agree is Lemma 5.3.1, a milestone, not a definition.
• Maxima. Maxima over actions are Finset.sup'; $\|\cdot\|_\infty$ on state-action functions is Mathlib's sup norm on S → A → ℝ. $B_J$ is a single number, as printed in Definition 5.1.2.

Welcome contributions: proofs of the milestones, general lemmas about the $T$-epoch layer (values in $[0,1]$, normalization of $d_{\pi,s_0}$, the path-expectation form of $V_{\pi,t}$), and links to the platform's discounted performance difference results.

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/
• S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. J. Williams and L. C. Baird, Tight Performance Bounds on Greedy Policies Based on Imperfect Value Functions, Technical Report NU-CCS-93-14, Northeastern University, 1993.
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Robust regression guards a linear model against errors in the data matrix. The observations $b \in \mathbb R^n$ are fitted by $Ax$, but the features (the columns $a_1,\dots,a_m$ of $A$) are only known up to a disturbance $\Delta A$ from an uncertainty set $\mathcal U$. The robust estimator minimizes the worst-case residual,

$$\min_{x \in \mathbb R^m}\ \max_{\Delta A \in \mathcal U} \|b - (A+\Delta A)x\| .$$

Xu, Caramanis and Mannor (arXiv:0811.1790v1; IEEE Trans. Inf. Theory 56(7), 2010) showed that when each column is perturbed independently within a Euclidean ball of radius $c_i$, this problem is exactly the weighted $\ell_1$-regularized problem $\min_x \|b - Ax\|_2 + \sum_i c_i|x_i|$, an un-squared Lasso (their Theorem 1, the subject of the first mission of this series). Robustness then explains regularization: the penalty is the price of the worst disturbance.

Section III of the paper asks which regularizers arise when the disturbances of different features are coupled, that is, when a single budget limits all columns jointly. The answer it gives is that every norm-based regularizer arises this way: a norm budget on the vector of column-disturbance sizes produces the dual norm as the penalty. This links robust optimization (Ben-Tal, El Ghaoui, Nemirovski 2009) and regularized estimation, and it recovers the robust least-squares formulation of El Ghaoui and Lebret (1997) as the Euclidean special case.

Setting

Fix $n \ge 1$, $m \ge 0$, and an arbitrary norm $\|\cdot\|_a$ on $\mathbb R^n$. The data are the columns $a_1,\dots,a_m \in \mathbb R^n$ of $A$ and the response $b \in \mathbb R^n$; for $x \in \mathbb R^m$, $Ax = \sum_i x_i a_i$. A disturbance is $\Delta A = (\delta_1,\dots,\delta_m)$ with $\delta_i \in \mathbb R^n$; the perturbed matrix $A + \Delta A$ has columns $a_i + \delta_i$. For an uncertainty set $\mathcal U$ the robust objective is

$$R_{\mathcal U}(x) = \sup_{\Delta A\in\mathcal U} \|b - (A+\Delta A)x\|_a \in [-\infty,+\infty].$$

Three families of uncertainty sets appear.

1. Feature-wise (Theorem 3): for budgets $c_i \ge 0$, $\mathcal U_a = \{(\delta_1,\dots,\delta_m) : \|\delta_i\|_a \le c_i\}$.
2. Coupled (p. 6): for functions $f_1,\dots,f_k:\mathbb R^m\to\mathbb R$, $\mathcal U' = \{(\delta_1,\dots,\delta_m) : f_j(\|\delta_1\|_a,\dots,\|\delta_m\|_a) \le 0,\ j=1,\dots,k\}$, with the budget set $\mathcal Z = \{z \in \mathbb R^m : f_j(z) \le 0\ \forall j,\ z \ge 0\}$.
3. Norm budget (Corollary 1): for a norm $\|\cdot\|_s$ on $\mathbb R^m$ and $l \ge 0$, $\mathcal U' = \{(\delta_1,\dots,\delta_m) : \|(\|\delta_1\|_a,\dots,\|\delta_m\|_a)\|_s \le l\}$. The dual norm is $\|y\|_s^* = \sup\{y^\top z : \|z\|_s \le 1\}$. A norm is absolute if $\|(|z_1|,\dots,|z_m|)\|_s = \|z\|_s$ for all $z$.

A fourth, polytope set, $\{(\delta_1,\dots,\delta_m) : \exists c \ge 0,\ Tc \le s,\ \|\delta_j\|_a \le c_j\}$ for $T \in \mathbb R^{k\times m}$, $s\in\mathbb R^k$, is the subject of Corollary 2. Write $|x| = (|x_1|,\dots,|x_m|)$.

Formalization targets

Goal: Corollary 1 (p. 7)

For an absolute norm $\|\cdot\|_s$ and $l \ge 0$, for every $x \in \mathbb R^m$ the worst case over the norm-budget set is attained and

$$\max_{\Delta A\in\mathcal U'} \|b-(A+\Delta A)x\|_a = \|b - Ax\|_a + l\,\|x\|_s^*,$$

and the robust problem and $\min_x \|b-Ax\|_a + l\|x\|_s^*$ have the same minimizers.

Milestone: Theorem 3 (p. 6)

For $c \ge 0$ and every $x$: $\max_{\Delta A\in\mathcal U_a}\|b-(A+\Delta A)x\|_a = \|b-Ax\|_a + \sum_i c_i|x_i|$, attained, with the same minimizers.

Milestone: Eq. (13) (proof of Theorem 4, Appendix B, p. 19)

For every $x$, in the extended reals,

$$\sup_{\Delta A\in\mathcal U'} \|b-(A+\Delta A)x\|_a = \|b-Ax\|_a + \sup_{c\in\mathcal Z} |x|^\top c .$$

Milestone: Corollary 2 (p. 7)

If some $c \ge 0$ has $Tc \le s$, then for every $x$ the worst case over the polytope set equals $\|b-Ax\|_a + \inf\{s^\top\lambda : x \le T^\top\lambda,\ -x\le T^\top\lambda,\ \lambda\ge0\}$ (both sides $+\infty$ when the constraints are infeasible), the infimum is attained when feasible, and robust minimizers are exactly the $x$-parts of optimal solutions of that linear program.

The paper's general result, Theorem 4 (p. 6), expresses the coupled robust problem through a Lagrangian function $v(\lambda,\kappa,x)$ under the assumption that $\mathcal Z$ has nonempty relative interior. The mission does not pose it: that assumption is not Slater's condition, and the statement fails without one (an explicit counterexample with $\mathcal Z = \{0\}\times[0,\infty)$ is recorded in the series plan). The mission poses the decomposition (13), on which Theorem 4 rests, and the two corollaries, which are true as stated under the readings below.

Significance

The result. Corollary 1 says that any norm penalty $l\|x\|_s^*$ is the worst-case cost of column disturbances whose sizes are jointly bounded in the dual norm. Taking $\|\cdot\|_s = \ell_\infty$ gives the $\ell_1$ penalty (budget per column), $\ell_1$ gives $\ell_\infty$ (a shared budget), and both Euclidean gives the Frobenius-ball model of robust least squares. Corollary 2 shows that polytope budgets keep the problem a linear program apart from the loss, which allows modeling, for instance, corruption of an unknown subset of features. Eq. (13) is the common reduction behind these: the coupled worst case is the uncoupled one maximized over the admissible budget vectors.

Formalizing it. None of these statements has a machine-checked proof. The mission makes precise two points the paper leaves implicit: which "symmetric" norms the corollary is true for, and in what sense "max" holds when the budget set is empty or unbounded. The finished development is a self-contained library of worst-case residual identities for arbitrary norms on finite-dimensional or general normed spaces. Related platform items, credited and not reused: SPOBounds.StronglyConvex.dual_norm_ball_max (maximum of a linear functional over a norm ball, with the continuous-dual norm), and RobustLS.Unstructured.worst_case_residual_closed_form (El Ghaoui–Lebret, which perturbs $[A\ b]$ in a Frobenius ball, a different set).

Difficulty

The upper bound of every identity is a triangle inequality. The content is in the matching lower bound: a disturbance must be exhibited that aligns all perturbed columns with the residual direction, and in (13) each column disturbance must have norm exactly $c_i$, including columns with $x_i = 0$, which is where $n \ge 1$ enters. The paper's first line of the proof of (13) rewrites $\mathcal U'$ as $\{\Delta A : \exists c \in \mathcal Z,\ \|\delta_i\|_a \le c_i\}$; that set identity is false unless $\mathcal Z$ is downward closed, so the obvious route through it does not work for (13) as stated. For Corollary 1 the remaining step is the identity $\sup\{|x|^\top c : c\ge0,\ \|c\|_s\le l\} = l\|x\|_s^*$, which needs the absolute property and fails for norms that are only permutation invariant. For Corollary 2 the remaining step is linear programming duality, which Mathlib does not yet provide in this form.

Formalization scope

$(\mathbb R^n, \|\cdot\|_a)$ is an arbitrary real normed space $E$ with Nontrivial E (the paper's implicit $n\ge1$); finite dimension is not imposed, a harmless generalization. Columns are a family a : Fin m → E, disturbances δ : Fin m → E, coefficients Fin m → ℝ, and $Ax = \sum_i x_i \cdot a_i$. Explicit readings:

1. The robust objective is a supremum over the uncertainty set, computed in EReal; it is never defined by its closed form. "Max" is stated as IsGreatest of the set of residual values (attained) in Theorem 3 and Corollary 1, where the maximum exists, and as an EReal supremum in (13) and Corollary 2, where it need not.
2. "Is equivalent to" / "the resulting regularized regression problem is" means: equal objectives at every $x$ and equal sets of minimizers. Existence of a minimizer is not claimed.
3. "Symmetric norm" is read as absolute; $\|\cdot\|_s$ is a Mathlib Seminorm on Fin m → ℝ with $N z = 0 \Rightarrow z = 0$ (the type already carries the sup norm, so the notation $\|\cdot\|$ is not used for it). The dual norm is a real sSup of $\{y^\top z : N z \le 1\}$, a nonempty set that is bounded above because $N$ is a norm on $\mathbb R^m$.
4. $l \ge 0$ is added to Corollary 1, and feasibility of $c\ge0$, $Tc\le s$ to Corollary 2; without them the sets are empty.
5. Eq. (13) is stated for $\mathcal U'$ as defined on p. 6 (not through the paper's set rewriting); the convexity of the $f_j$ is kept as the paper's standing assumption and is not used.

A trivializing formalization is ruled out: the robust objective is the EReal supremum (or the residual-value set) over the uncertainty set, so no identity holds by unfolding, and no real sSup junk value enters a robust objective. Welcome contributions: the explicit worst-case disturbance in an arbitrary normed space, the absolute-norm duality lemma, and a finite-dimensional LP strong duality theorem, each reusable beyond this mission.

Selected references

• H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Transactions on Information Theory 56(7):3561–3574, 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM Journal on Matrix Analysis and Applications 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• 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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Result 4

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

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

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

Milestones

1. The Derivation's derivatives:

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Result 3

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

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Theorem 5.2: WMC total loss

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

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

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

Supporting numbered results

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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