Machine Learning

Motivation

Many sequential decision problems have a combinatorial decision set and a linear cost: choosing a path in a graph whose edge delays change every day, choosing a binary search tree for a stream of requests, or choosing one of $n$ experts whose losses are revealed after each round. Classical weighted-majority algorithms keep one weight per decision, which is exponential in the size of a path or tree. Kalai and Vempala (J. Comput. System Sci. 71 (2005)) showed that one call per round to an offline optimiser, applied to the cumulative costs plus a random perturbation, already gives online guarantees comparable to those of the exponential-weights algorithms. The idea goes back to Hannan's perturbed algorithm (1957); the paper's contribution is a short, general analysis in the linear setting.

The paper proves two guarantees for Follow the Perturbed Leader. The additive one (Theorem 1.1(a), a sister mission) bounds the regret by a term growing like $\sqrt T$. This mission formalizes the multiplicative one, Theorem 1.1(b): for nonnegative costs, a variant with exponentially distributed perturbations pays at most a factor $1+\varepsilon$ more than the best fixed decision in hindsight, plus a term independent of the horizon. Such "small-loss" bounds matter when the best decision has small total cost, since the regret then scales with that cost rather than with $T$.

Setting

Fix a dimension $n$. A decision set $\mathcal D \subset \mathbb R^n$ and a state set $\mathcal S \subset \mathbb R^n$ are given; choosing $d\in\mathcal D$ in state $s\in\mathcal S$ costs $d\cdot s$. In this mission both sets are nonnegative: $\mathcal D, \mathcal S \subset \mathbb R^n_+$.

The decision set is accessed only through an argmin oracle $M:\mathbb R^n\to\mathcal D$ with

$$M(x)\cdot x \le d\cdot x \quad\text{for all } d\in\mathcal D,$$

i.e. $M(x)=\arg\min_{d\in\mathcal D} d\cdot x$ with arbitrary tie-breaking. For a state sequence $s_1,\dots,s_T\in\mathcal S$ write $s_{1:t}=s_1+\dots+s_t$; the benchmark is

$$\text{min-cost}_T=\min_{d\in\mathcal D}\sum_{t=1}^T d\cdot s_t = M(s_{1:T})\cdot s_{1:T}.$$

Two parameters measure the instance: the $\ell_1$-diameter $D\ge |d-d'|_1$ for $d,d'\in\mathcal D$, and the state size $A\ge |s|_1$ for $s\in\mathcal S$, where $|x|_1=\sum_i|x_i|$.

The algorithm FPL*($\varepsilon$) acts as follows on each period $t$: draw $p_t$ from the probability law $\mu_\varepsilon$ with density

$$\frac{d\mu_\varepsilon}{dx}(x)=\Big(\frac{\varepsilon}{2}\Big)^n e^{-\varepsilon|x|_1},$$

so each coordinate is $\pm r/\varepsilon$ with $r$ standard exponential, and play $M(s_{1:t-1}+p_t)$. Its expected cost against a fixed state sequence is

$$\mathbb E[\text{cost of FPL}^*(\varepsilon)]=\sum_{t=1}^T\int s_t\cdot M(s_{1:t-1}+p)\,d\mu_\varepsilon(p).$$

In Lean these are IsArgminOracle Dset M, laplaceLaw n ε and fplStarExpectedCost M s ε T; $s_{1:t}$ is the published OracleRO.ApproxFPL.prefixSum s t.

Formalization targets

Goal: Theorem 1.1(b)

For nonnegative $\mathcal D,\mathcal S$, $A>0$ and $0<\varepsilon\le 1$,

$$\mathbb E[\text{cost of FPL}^*(\varepsilon/2A)]\le(1+\varepsilon)\,\text{min-cost}_T+\frac{4AD(1+\ln n)}{\varepsilon}.$$

Intermediate statements (milestones, in attack order)

1. For any fixed $p_1$: $\sum_{t=1}^T M(s_{1:t}+p_1)\cdot s_t\le M(s_{1:T})\cdot s_{1:T}+D|p_1|_\infty$ (p. 303, by Lemma 3.1).
2. The expected maximum of $n$ independent standard exponentials is at most $\ln n+1$ (end of §2, p. 299).
3. $\mathbb E_{p\sim\mu_\varepsilon}|p|_\infty\le(1+\ln n)/\varepsilon$ (pp. 299, 303).
4. Equation (7): $\mathbb E[M(s_{1:t-1}+p)\cdot s_t]=\int (M(s_{1:t}+y)\cdot s_t)\,e^{-\varepsilon(|y+s_t|_1-|y|_1)}\,d\mu_\varepsilon(y)$.
5. Equation (6): $\mathbb E[M(s_{1:t-1}+p)\cdot s_t]\le e^{\varepsilon A}\,\mathbb E[M(s_{1:t}+p)\cdot s_t]$.
6. For $0<\varepsilon\le 1/A$: $e^{\varepsilon A}\le 1+2\varepsilon A$.
7. For $0<\varepsilon\le 1/A$: $\mathbb E[\text{cost of FPL}^*(\varepsilon)]\le(1+2\varepsilon A)\big(\text{min-cost}_T+D(1+\ln n)/\varepsilon\big)$.

Statement 7 is the bound for an arbitrary parameter; the goal is its evaluation at $\varepsilon/2A$.

Significance

The result is the first multiplicative guarantee for a perturbation algorithm that needs only an offline linear optimiser. With $\varepsilon$ tuned to $\text{min-cost}_T$ it gives $\mathbb E[\text{cost}]\le\text{min-cost}_T+4\sqrt{\text{min-cost}_T\,AD(1+\ln n)}+4AD(1+\ln n)$ (p. 294). The paper applies it to online shortest paths, to the tree-update problem (giving the first efficient $(1+\varepsilon)$-competitive algorithm there), and to adaptive Huffman coding. The lazy variant FLL* of the same paper, whose per-period behaviour coincides with FPL*, inherits the bound; that is the third mission of this series.

The theorem is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces a formal proof of Theorem 1.1(b) as printed, together with the reusable ingredients: the multivariate Laplace law with its normalisation, its translation identity (7), and the expected maximum of i.i.d. exponentials. The paper's argument has small gaps that a formalization must close, notably the condition $\varepsilon\le 1$, which (b) omits but its proof uses.

Difficulty

The deterministic part is the be-the-leader argument with a shared perturbation; it is a finite-sum induction. The probabilistic part is where the work is. The obvious approach, bounding the difference between following and being the perturbed leader by the measure of a symmetric difference of translated sets as in the additive case, gives an additive term proportional to $T$ and cannot give a multiplicative factor. Instead (6) needs the density ratio of $\mu_\varepsilon$ under translation by $s_t$, which requires a change of variables against a density on $\mathbb R^n$, together with the nonnegativity of the integrand; without nonnegativity the inequality fails. The bound on $\mathbb E|p|_\infty$ requires the expected maximum of $n$ exponentials, which is not in Mathlib, and the identification of the coordinates of $\mu_\varepsilon$ as independent scaled Laplace variables, which requires factoring a product density.

Formalization scope

Vectors are Fin n → ℝ; $d\cdot s$ is ⬝ᵥ; $|x|_1$ is written $\sum_i|x_i|$; $|x|_\infty$ is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The decision set is Dset, the diameter Ddiam. States are indexed from $1$; s 0 is unused. The oracle is a hypothesis IsArgminOracle Dset M on an arbitrary function, so the theorems hold for every tie-breaking rule. The paper's parameters are hypotheses ∀ d d' ∈ Dset, ∑ i, |d i - d' i| ≤ Ddiam and ∀ x ∈ S, ∑ i, |x i| ≤ A. The bound $R\ge|d\cdot s|$ of the paper is not used by part (b) and is omitted.

Hypotheses added to the page, each necessary: measurability of $M$ (the expectations presuppose it); $\varepsilon>0$; $A>0$ (the parameter $\varepsilon/2A$ presupposes it); $\varepsilon\le1$ in the goal (used by the proof, p. 303); and $n\ge1$ only in the statement about a maximum over $n$ variables. Two printed slips are corrected, not copied: "exponential distributions with mean $\varepsilon$" (rate $\varepsilon$ is meant) and "$|p_1|_\infty\le(1+\ln n)/\varepsilon$" (an expectation is meant).

Trivializing formalizations are ruled out as follows. The law $\mu_\varepsilon$ carries its normalising constant $(\varepsilon/2)^n$ and is shown to be a probability measure in a sorry-free sanity file; it is not the uniform law of FPL. The cost uses $M(s_{1:t-1}+p)$, not the be-the-leader $M(s_{1:t}+p)$. The oracle is not built with Classical.epsilon. All integrands are measurable and bounded (because $\mathcal D$ has finite diameter), so no integral vanishes for lack of integrability; the sanity file checks this on a two-expert instance that satisfies every hypothesis.

A complete development needs Lebesgue change of variables under translation for densities on Fin n → ℝ, Fubini for product densities, the tail-integral formula for expectations, and a union bound. The Laplace law, its translation identity, and the expected maximum of exponentials are reusable beyond this mission; contributions of those as standalone lemmas are welcome.

Selected references

• A. Kalai and S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71(3):291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
• J. Hannan, Approximation to Bayes risk in repeated plays, in Contributions to the Theory of Games III, Ann. of Math. Studies 39, Princeton University Press, 1957, pp. 97–139 (reference [14] of Kalai and Vempala).

Motivation

In the local model of differential privacy, no trusted curator ever sees the raw data: each individual randomizes their own record before handing it to the analyst. This is how private telemetry is collected in practice (randomized response and its descendants), and it raises a basic question: which learning tasks remain possible when the learner only sees locally randomized records?

Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith answered it in What Can We Learn Privately? (arXiv:0803.0924v3, the accepted version of SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are the arXiv v3's). They showed that local private learning is equivalent, up to polynomial factors, to learning in Kearns' statistical query (SQ) model (Kearns 1998), where an algorithm sees a distribution only through approximate expectations. This mission formalizes one direction of that equivalence: every SQ algorithm can be run by a local algorithm (§5.1.1, Theorem 5.7). The other direction (Lemma 5.8) is a separate mission of this series.

Timeline. Blum, Dwork, McSherry and Nissim (PODS 2005) observed that SQ algorithms can be simulated by a trusted curator adding noise to sums. Dwork, McSherry, Nissim and Smith (TCC 2006) introduced the Laplace mechanism. Kasiviswanathan et al. (FOCS 2008; journal version 2011) showed the simulation works even in the local model, with each record entering a single randomizer.

Setting

A database is a vector $z=(z_1,\dots,z_n)\in D^n$; two databases are neighbors if they differ in exactly one entry. A randomized algorithm $A$ is $\varepsilon$-differentially private if $\Pr[A(z)\in S]\le e^{\varepsilon}\Pr[A(z')\in S]$ for all neighbors $z,z'$ and all measurable sets $S$ of outputs. An $\varepsilon$-local randomizer is an $\varepsilon$-differentially private map applied to a single record: $\Pr[R(u)\in S]\le e^{\varepsilon}\Pr[R(u')\in S]$ for all $u,u'$.

The Laplace distribution $\mathrm{Lap}(s)$ has density $\frac1{2s}e^{-|x|/s}$.

An SQ oracle $SQ_P$ for a distribution $P$ on $D$ receives a query $g:D\to[-b,b]$ and a tolerance $\tau$, and may return any $v$ with $|v-\mathbb E_{u\sim P}[g(u)]|\le\tau$. An SQ algorithm with $t$ queries asks $(g_0,\tau_0),\dots,(g_{t-1},\tau_{t-1})$, where $(g_k,\tau_k)$ may depend on the earlier answers $a_0,\dots,a_{k-1}$ (adaptive), and outputs a function of all answers. A vector $a$ is a valid transcript against $SQ_P$ if every $a_k$ is within $\tau_k$ of the true mean of the query $g_k$ asked at that point.

For one query $g$, the randomizer $R_g(u)=g(u)+\eta$ with $\eta\sim\mathrm{Lap}(2b/\varepsilon)$ is applied to each record, and the local algorithm $\mathcal A_g$ outputs the average $\frac1n\sum_i(g(z_i)+\eta_i)$. The simulation of an SQ algorithm answers its $k$-th query $g_k$ by running $\mathcal A_{g_k}$ on the $k$-th block of $m$ fresh entries $z_{km},\dots,z_{km+m-1}$ and finally outputs what the SQ algorithm outputs on these answers.

Formalization targets

Goal: Theorem 5.7 (local simulation of SQ)

There is an absolute constant $c>0$ such that, for every SQ algorithm with $t$ queries into $[-b,b]$, and every $\varepsilon>0$; the accuracy claim further takes every tolerance at least $\tau$, $\varepsilon\le1$, $\varepsilon\tau\le4b$ and $0<\beta<1$:

$$\text{the simulation is }\varepsilon\text{-differentially private for every block size }m\text{ and every }n\ge tm,$$ $$m\ \ge\ c\,\frac{\ln(t/\beta)\,b^2}{\varepsilon^2\tau^2},\ z\sim P^n\ \Longrightarrow\ \Pr\bigl[\text{the simulated answers are a valid transcript against }SQ_P\bigr]\ \ge\ 1-\beta .$$

On that event the simulation outputs exactly what the SQ algorithm outputs against a valid oracle. The constant is left unspecified, as in the paper.

Milestones

1. $R_g$ is an $\varepsilon$-local randomizer; $\mathcal A_g$ is $\varepsilon$-differentially private (p. 20).
2. Hoeffding's bound for the empirical mean of $g$: $\Pr[|\frac1n\sum g(u_i)-v|\ge\tau/2]\le2e^{-\tau^2n/(8b^2)}$.
3. The average of $n$ i.i.d. $\mathrm{Lap}(2b/\varepsilon)$ variables lies in $[-\tau/2,\tau/2]$ with probability at least $1-\beta/2$ once $n\ge c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$.
4. Lemma 5.6: $\mathcal A_g$ approximates $\mathbb E_P[g]$ within $\pm\tau$ with probability $1-\beta$ from $n\ge c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$ samples.

Significance

Theorem 5.7 is the inclusion "SQ ⊆ local" in the paper's characterization of local private learning: every concept class learnable with statistical queries is learnable by an $\varepsilon$-local algorithm, with sample size growing like $t\log(t/\beta)b^2/(\varepsilon^2\tau^2)$. Combined with the converse simulation (Lemma 5.8), it identifies local private learnability with SQ learnability (Theorem 5.14). It thereby transfers the known SQ lower bounds, such as the one for parity, to the local model. It also shows that nonadaptive SQ algorithms become noninteractive local protocols.

The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization fixes what "the simulation gives the same output" means against an adversarial oracle and an adaptive algorithm. It also supplies reusable Lean objects for local differential privacy, Laplace noise and SQ algorithms.

Difficulty

The privacy half is the easy-looking part, but it is adaptive: the query asked in block $k$ depends on the noisy answers from blocks $0,\dots,k-1$. A database change in block $k$ therefore changes the law of all later answers, not only $a_k$. The argument must use that every entry enters exactly one randomizer and compose along the adaptive transcript.

The accuracy half has the same adaptivity issue: the union bound over queries needs, for each $k$, the failure probability of block $k$ conditioned on everything before it. That is where the fresh blocks and measurability are used. The concentration step for Laplace averages is sub-exponential, not sub-Gaussian. The naive use of the paper's appendix lemma (A.3) fails: it is stated as an equality for every deviation $\delta>0$, but its proof only covers deviations of order the Laplace scale.

Formalization scope

Databases are Fin n → D (0-based). Randomized algorithms are identified with the laws of their outputs (Measure); differential privacy is required on all measurable sets. An SQ algorithm is a deterministic adaptive strategy (SQAlg): a randomized one is a mixture over its coins, to which the result transfers. "At most $t$ queries" is "exactly $t$" after padding with dummy queries. Queries are real valued with $|g|\le b$, as the paper allows after Definition 5.4. Block $k$ consists of the database indices $km,\dots,km+m-1$, so the blocks are disjoint by construction, and the simulated answers are a deterministic function of the database and the $t\times m$ noise array. The natural logarithm replaces the paper's base 2, which only changes $c$. Constants are existential and quantified before everything else.

Explicit choices, each recorded in the item that makes it:

• $\varepsilon\tau\le4b$ in Lemma 5.6, the Laplace step and Theorem 5.7. Without it the printed statements are false: for $\varepsilon\tau/b$ large a single sample is allowed, and its Laplace noise exceeds $\tau$ too often.
• $\varepsilon\le1$ in Lemma 5.6 and in the accuracy half of Theorem 5.7 (the privacy half holds for every $\varepsilon>0$). Without it the threshold $c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$ can be smaller than the sample size needed to estimate $\mathbb E[g]$ at all. The paper's own remark about an $O(\varepsilon^{-2})$ factor presumes $\varepsilon=O(1)$.
• $\beta\le1/2$ in the Laplace step, which is false for $\beta$ near $1$.
• Each query is jointly measurable in (earlier answers, record), and the output map is measurable for the privacy claim.
• "Gives the same output as $\mathcal A_{SQ}$" is "the simulated answers are a valid transcript against $SQ_P$". Accuracy bounds the measure of the failure event by $\beta$.
• "Noninteractive if nonadaptive" and "efficient" are not formalized.

A trivializing formalization is ruled out: the oracle is not replaced by the exact expectation, accuracy is required for every query actually asked (not only the first), privacy holds for every database (not only i.i.d. samples), and the constant $c$ cannot depend on $t$, $\beta$, $\varepsilon$, $\tau$, $b$ or the algorithm.

Needed infrastructure: the Laplace distribution as a probability measure and its moment generating function, a Hoeffding bound for bounded i.i.d. variables, the Laplace mechanism, and adaptive composition along a transcript. All of these are reusable beyond this mission. Proofs of the milestones, of standalone Laplace and composition lemmas, and of the goal are welcome.

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, https://arxiv.org/abs/0803.0924 ; DOI https://doi.org/10.1137/090756090
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. https://doi.org/10.1145/293347.293351
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating noise to sensitivity in private data analysis, TCC 2006, LNCS 3876, 265–284. https://doi.org/10.1007/11681878_14
• A. Blum, C. Dwork, F. McSherry, K. Nissim, Practical privacy: the SuLQ framework, PODS 2005, 128–138. https://doi.org/10.1145/1065167.1065184
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

Noisy low-rank matrix completion asks to reconstruct an $m_1\times m_2$ matrix $A_0$ from $n$ noisy observations of randomly chosen entries. It is the statistical model behind collaborative filtering (recommender systems), sensor localization and system identification, and the nuclear-norm penalized least-squares estimator is its standard convex method. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4, Ann. Statist. 2011) proved sharp oracle inequalities for this estimator and showed that its Frobenius error is of order $\operatorname{rank}(A_0)(m_1\vee m_2)\log(m_1+m_2)/n$ up to normalization, which matches the minimax lower bound up to a logarithmic factor.

An upper bound alone does not say whether the estimator really attains this rate on a given matrix, nor whether it reports the correct rank. Section 5.1 of the paper answers both questions with a single deterministic theorem, Theorem 8: with a slightly inflated regularization parameter the estimator never overestimates the rank of $A_0$; if the nonzero singular values of $A_0$ are separated from zero it recovers the rank exactly, and its error is then bounded below by a quantity of the same order as the upper bounds. Rank recovery is the property practitioners rely on when they use the estimator for model selection (choosing the number of latent factors). This mission formalizes Theorem 8 and the steps of its proof.

Setting

Fix integers $m_1,m_2,n\ge1$. The matrix completion basis is $\mathcal X=\{e_j(m_1)e_k(m_2)^\top\}$, the $m_1m_2$ matrices with a single entry equal to $1$. A sample consists of $n$ pairs $(X_i,Y_i)$ with $X_i\in\mathcal X$ (an observed position $(j_i,k_i)$) and $Y_i\in\mathbb R$ (a noisy observation of the corresponding entry of the unknown matrix $A_0$). Write $\langle A,B\rangle=\operatorname{tr}(A^\top B)$, $\|A\|_2$ for the Frobenius norm, $\|A\|_1$ for the nuclear norm (the sum of the singular values) and $\|A\|_\infty$ for the operator norm (the largest singular value). The singular values of $B$ are $\sigma_1(B)\ge\sigma_2(B)\ge\dots\ge\sigma_{m_1\wedge m_2}(B)\ge0$.

From the sample form

$$\mathbf X=\frac{m_1m_2}{n}\sum_{i=1}^nY_iX_i,\qquad \mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).$$

In the paper's model $\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle$ with $X_i$ uniform on $\mathcal X$, so $\mathbb E(Y_iX_i)=A_0/(m_1m_2)$ and $\mathbf X-A_0=m_1m_2\mathbf M$: the matrix $\mathbf M$ is the stochastic error. For $\lambda>0$ the estimator (3.1) is

$$\hat A^\lambda=\operatorname{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1\Big).$$

The objective is strictly convex, so the minimizer is unique; by (3.2) it is obtained from a singular value decomposition of $\mathbf X$ by soft thresholding every singular value at level $\lambda m_1m_2/2$.

Formalization targets

Goal: Theorem 8 (p. 20)

Let $\lambda\ge2\|\mathbf M\|_\infty$, $0<\delta<1$ and $\lambda'=\lambda/(1-\delta)$, and put $\hat r=\operatorname{rank}(\hat A^{\lambda'})$. Then

$$\hat r\le\operatorname{rank}(A_0).\tag{5.1}$$

If in addition $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$, then

$$\hat r\ge\operatorname{rank}(A_0)\tag{5.2}$$

and

$$\|\hat A^{\lambda'}-A_0\|_2^2\ge\frac{\delta^2}{4(1-\delta)^2}\operatorname{rank}(A_0)\,(\lambda m_1m_2)^2.\tag{5.3}$$

Milestones

The milestones follow the proof on p. 20 in order:

1. the singular value perturbation display $|\sigma_j(\mathbf X)-\sigma_j(A_0)|\le\sigma_1(\mathbf X-A_0)=m_1m_2\|\mathbf M\|_\infty\le\lambda m_1m_2/2$;
2. the rank of $\hat A^\lambda$ equals the number of singular values of $\mathbf X$ above $\lambda m_1m_2/2$ (the consequence of (3.2) the proof uses);
3. (5.1);
4. (5.2);
5. $\|\mathcal P(\hat A^{\lambda'}-\mathbf X)\|_2=\sqrt r\,\lambda'm_1m_2/2$ when $\hat r=r$, for the projector $\mathcal P$ onto the span of the top $r$ singular pairs $u_j(\mathbf X)v_j(\mathbf X)^\top$;
6. $\|\mathcal P(\mathbf X-A_0)\|_2\le\sqrt r\|\mathbf M\|_\infty m_1m_2\le\sqrt r\lambda m_1m_2/2$.

Significance

The result. Theorem 8 turns the paper's upper bounds into two-sided statements. Combined with a probability bound for $\|\mathbf M\|_\infty$ (Corollary 3 of the paper), it shows that with high probability the estimator selects the true rank and that its error on well-conditioned low-rank matrices is not smaller than the rate of the upper bounds, so those bounds cannot be improved for this estimator. Because the theorem is deterministic given the event $\lambda\ge2\|\mathbf M\|_\infty$, it applies unchanged to any noise model for which such a bound on the stochastic error is available.

Formalizing it. The theorem is proved in the paper; nothing in it is open. The mission produces a machine-checked version and, along the way, reusable linear algebra that is not on the platform in this form: Weyl's perturbation inequality for singular values in operator norm, the rank of a nuclear-norm proximal point, and the Frobenius norm of a projection onto a span of orthonormal rank-one matrices. The soft-thresholding representation (3.2) itself is the open platform item CaiCandesShen.Convergence.shrink_eq_prox (Cai–Candès–Shen, Theorem 2.1, after halving the objective); this mission references it rather than posing it again, and a proof of it would serve both missions.

Difficulty

The arithmetic of the proof is three lines; the content is in two facts about singular values that the paper takes from the literature. The first is Weyl's inequality $|\sigma_j(B)-\sigma_j(C)|\le\|B-C\|_\infty$, which needs the min–max (Courant–Fischer) characterization of singular values; Mathlib defines singular values through the eigenvalues of $T^*T$ but has neither the min–max principle for them nor this inequality. The second is the description of the minimizer of $\|A-\mathbf X\|_2^2+\lambda m_1m_2\|A\|_1$: one needs the subdifferential of the nuclear norm (2.1), or an equivalent von Neumann trace inequality, to show that soft thresholding is optimal, and then that its rank and its projection onto the top singular pairs are what the formula suggests. A naive approach that compares the estimator with $\mathbf X$ entrywise gives nothing about the rank; the proof needs the spectral structure.

Formalization scope

Matrices are MatrixCompletion.RealMatrix m₁ m₂ (Matrix (Fin m₁) (Fin m₂) ℝ) with the published norms frobeniusNormSq, frobeniusNorm, nuclearNorm, spectralNorm and SVD data SVD. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin, 0-based: the Lean singularValue B j is the paper's $\sigma_{j+1}(B)$. The conventions committed to:

• The statements are realization-wise: positions idx : Fin n → Fin m₁ × Fin m₂ and responses y : Fin n → ℝ are fixed, and every theorem holds for every data set satisfying $\lambda\ge2\|\mathbf M\|_\infty$. The matrix $\mathbf M$ is written as $\frac1n\sum_iY_iX_i-A_0/(m_1m_2)$, which is (2.2) under the model (1.1) and the uniform design; this is the paper's "Note that $\mathbf X-A_0=m_1m_2\mathbf M$". The probabilistic hypotheses are used for nothing else.
• $n,m_1,m_2\ge1$ and $\lambda>0$ are assumed, as in the paper.
• The estimator is any minimizer of (3.1) over all matrices, never the soft-thresholding formula; replacing the minimizer by formula (3.2) would assume the open Cai–Candès–Shen item.
• $\min_{j:\sigma_j(A_0)\ne0}\sigma_j(A_0)\ge\lambda'm_1m_2$ is written "for every $j$ with $\sigma_j(A_0)\ne0$"; for $A_0=0$ it is vacuous, as on the page. No real infimum over a possibly empty set is used.
• The projector $\mathcal P$ is built from a singular value decomposition of $\mathbf X$ carried as data, with decreasing singular values, from its first $r$ pairs.

No printed slip was found in Theorem 8 or its proof; no hypothesis beyond the above is added.

Contributions welcome: Weyl's inequality for singular values (generally useful), the rank and top-$r$ projection of the nuclear-norm proximal point, and a proof of CaiCandesShen.Convergence.shrink_eq_prox.

The source is the arXiv preprint arXiv:1011.6256v4; all page and display numbers refer to it.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
• J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://doi.org/10.1137/080738970
• G. W. Stewart, J.-G. Sun, Matrix Perturbation Theory, Academic Press, 1990 (reference [25] of the paper, p. 203).
• E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 2010. https://doi.org/10.1109/JPROC.2009.2035722

Motivation

Binary classification asks for a rule that predicts a label $Y\in\{0,1\}$ from a feature vector $X\in\mathbb R^d$, given $n$ labelled examples. A classical way to measure how hard this is, due to Mammen and Tsybakov (1999), treats classification as the estimation of a set, the region where label $1$ is more likely, and asks how fast the excess misclassification risk of a data-driven classifier can tend to zero. The answer depends on two parameters: the complexity $\rho$ of the class of candidate sets, measured by entropy with bracketing, and the margin parameter $\kappa$, which measures how sharply the conditional probability of label $1$ moves away from $1/2$ near the decision boundary.

Tsybakov (2004) showed that empirical risk minimization over a suitable net attains the rate $n^{-\kappa/(2\kappa+\rho-1)}$, which approaches $n^{-1}$ ("fast rates") for favourable margins and simple classes, and that this rate is minimax optimal. In practice neither $\rho$ nor $\kappa$ is known. The main result of the paper, Theorem 3, constructs a single classifier that adapts to both and attains the optimal rate up to a logarithmic factor simultaneously over a whole family of classes. The margin condition introduced here, often called the Tsybakov margin (or noise) condition, became a standard assumption of statistical learning theory, used for instance in the analysis of support vector machines and of plug-in rules (Audibert and Tsybakov 2007).

Setting

Observations are i.i.d. pairs $(X_1,Y_1),\dots,(X_n,Y_n)$ with law $\pi$. Write $P_X$ for the law of $X$ and $\eta(x)=P(Y=1\mid X=x)$ for the regression function. A classifier is a Borel set $G\subseteq\mathbb R^d$, predicting $1$ on $G$. The Bayes classifier is $G^*=\{x:\eta(x)\ge1/2\}$, and the excess risk of $G$ is

$$d(G,G^*)=\int_{G\triangle G^*}|2\eta(x)-1|\,P_X(dx)=R(G)-R(G^*),$$

where $R(G)=P(Y\ne I(X\in G))$. Two pseudodistances between sets are used: $d_\triangle(G,G')=P_X(G\triangle G')$ and its empirical analogue $d_{\triangle,e}(G,G')=\frac1n\sum_iI(X_i\in G\triangle G')$. The empirical risk is $R_n(G)=\frac1n\sum_i(Y_i-I(X_i\in G))^2$.

A class $\mathcal G$ of sets has complexity bound $\rho>0$ if its $\delta$-entropy with bracketing for $d_\triangle$ is at most $A\delta^{-\rho}$ for $0<\delta\le1$. The margin assumption (A1) requires $d(G,G^*)\ge c_0\,d_\triangle^\kappa(G,G^*)$ whenever $d_\triangle(G,G^*)\le\varepsilon_0$, with $\kappa\ge1$. A class $\mathcal P$ of distributions is a $(\mathcal G^*,\kappa,\rho)$-class if every $\pi\in\mathcal P$ has $G^*_\pi\in\mathcal G^*$, satisfies (A1), and $\mathcal G^*$ has complexity bound $\rho<1$ (Definition 4).

Aggregation. Given classes $\mathcal G_1,\dots,\mathcal G_N$ with complexities $\rho_1\le\dots\le\rho_N$ and nested approximating sets $\mathcal N_1\subseteq\dots\subseteq\mathcal N_N$, let $G_{nk}$ minimize $R_n$ over $\mathcal N_k$. With the thresholds

$$T_{nk}(G,G')=(\log^2n)\max\Big\{n^{-1/(1+\rho_k)},\ \tfrac1{\sqrt n}d_{\triangle,e}^{(1-\rho_k)/2}(G,G')\Big\},$$

an index $j$ is admissible if, for every $k\ge j$, some $G\in\mathcal N_j$ has $|R_n(G)-R_n(G_{nk})|\le T_{nk}(G,G_{nk})$. The adaptive classifier is $G^*_n=G_{n\hat j}$ with $\hat j$ the smallest admissible index.

Formalization targets

Goal: Theorem 3

Under assumptions (A3)–(A4), with $\mathcal P_j$ a $(\mathcal G_j,\kappa,\rho_j)$-class for each $j$, $N=O(n^\beta)$, and $\rho_1=\rho_{\min}$, $\rho_N=\rho_{\max}$ fixed, there is $C<\infty$ such that for all $n>1$ and every $j$,

$$\sup_{\pi\in\mathcal P_j}E_{\pi,n}\,d(G^*_n,G^*)\le C\left(\frac{\log^4n}{n}\right)^{\kappa/(2\kappa+\rho_j-1)}.$$

Milestones

1. Appendix, Lemmas 7–11: exponential tail bounds for suprema of ratio-type empirical processes over a class with complexity bound $\rho$.
2. Theorem 1: ERM over an $an^{-1/(1+\rho)}$-net of $\mathcal G^*$ attains $\sup_{\pi}E\,d(\hat G_n,G^*)=O(n^{-\kappa/(2\kappa+\rho-1)})$.
3. Lemma 2: the deterministic comparison inequalities (27)–(28) for an admissible index.
4. Lemma 1: $\sup_\pi P(\hat j>j^*)=o(1/n)$.
5. Lemmas 3, 5, 6, 4: the moment and probability bounds that combine into Theorem 3.

Significance

Theorem 3 says that a procedure which knows neither the class containing $G^*$ nor the margin parameter loses at most a factor $(\log n)^{4\kappa/(2\kappa+\rho_j-1)}$ against the optimal rate on every class at once; combined with the lower bound of Theorem 2 it identifies the optimal adaptive rate up to logarithms. Corollary 1 extends it to a continuum of classes $\{\mathcal G_\rho\}_{\rho\in[\rho_{\min},\rho_{\max}]}$. The selection rule is a Lepski-type pairwise comparison of empirical risks, and the analysis is one of the early results on adaptation to the margin.

The result is proved in the paper, with an Appendix that derives the empirical-process inequalities from van de Geer (2000). No part of it is known to have a machine-checked proof. A formalization would produce reusable infrastructure: entropy with bracketing for classes of sets, ratio-type deviation inequalities for empirical processes, and the excess-risk identity for 0–1 loss.

Difficulty

The obvious argument controls each $G_{nk}$ separately and takes a union bound over $k$. That fails: the bound for $G_{nk}$ at a class $\mathcal G_k$ that does not contain $G^*$ says nothing about $d(G_{nk},G^*)$, and the adaptive rule compares classifiers from different classes through random thresholds that depend on the empirical distance $d_{\triangle,e}$. The central steps are to show that the true index $j^*$ is admissible with probability $1-o(1/n)$ uniformly over a polynomially growing number of classes, and to replace $d_{\triangle,e}$ by $d_\triangle$ inside the thresholds at a constant-factor cost. Both rest on exponential, ratio-type deviation bounds for suprema over classes of infinite entropy, which are not in Mathlib.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, labels are Bool with true ↔ 1, and a distribution is a pair $(P_X,\eta)$ with $P_X$ a probability measure and $\eta$ measurable with values in $[0,1]$; the law of a pair is the published UnderstandingML.condLaw ($X\sim P_X$, then $Y\sim\mathrm{Bernoulli}(\eta(X))$). Classifiers are sets, risk is measured by $d$ via identity (2), and the complexity bound is stated as "some bracketing with $\log m\le A\delta^{-\rho}$ exists".

The Section 3 data ($N_n$, classes, nets, complexities, distribution classes) are indexed by $n$. The formalization commits to the following readings of the page, all disclosed in the items:

• one constant $A$, $c_0$, $\varepsilon_0$ for all classes;
• condition (7) uniformly over the whole family unless $\varepsilon_0=1$;
• complexity bounds for the design law of every distribution in the family;
• constants in Theorem 3 and Lemmas 1, 3–6 uniform in the class index $j$;
• "arg min" as any minimizer;
• the pseudoclassifier $G_{nkj}$ extended by its fallback branch to $j>k$;
• Lemmas 8–10 stated for every $c_1$ (or $c_2$), with constants that may depend on it.

Expectations are Lebesgue integrals over the sample, so each one carries the hypothesis that the data-dependent set is jointly measurable in (sample, point). This rules out the trivializing formalization in which a non-measurable classifier has integral $0$ and every rate bound holds for free. Probabilities of events involving suprema over uncountable classes are outer measures. Appendix suprema are real suprema over index sets bounded above. The goal is not vacuous: a solution-folder check exhibits a setup satisfying all hypotheses with $\hat j=1$.

Contributions welcome: bracketing-entropy chaining bounds, the van de Geer inequalities (5.42)–(5.43), and the Appendix lemmas as standalone results.

Selected references

• A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Ann. Statist. 32(1), 135–166, 2004. https://doi.org/10.1214/aos/1079120131
• E. Mammen and A. B. Tsybakov, Smooth discrimination analysis, Ann. Statist. 27(6), 1808–1829, 1999. https://doi.org/10.1214/aos/1017939240
• S. van de Geer, Empirical Processes in M-Estimation, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511802256
• J.-Y. Audibert and A. B. Tsybakov, Fast learning rates for plug-in classifiers, Ann. Statist. 35(2), 608–633, 2007. https://doi.org/10.1214/009053606000001217
• L. Devroye, L. Györfi and G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. https://doi.org/10.1007/978-1-4612-0711-5

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Corollary 3, Eq. (8)

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

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

Milestones (Appendix D)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

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

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

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

Milestones

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

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

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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