Machine Learning

Motivation

Classical generalization bounds for classifiers, built on the VC dimension, grow with the number of adjustable parameters. For neural networks this is at odds with practice: networks with many more weights than training examples often generalize well. Bartlett's 1998 paper (IEEE Trans. Inform. Theory 44(2), 525–536) explains part of this by measuring a real-valued classifier's confidence. If a hypothesis classifies most training examples correctly with a margin $\gamma$, its misclassification probability is controlled by a scale-sensitive dimension of the class at scale proportional to $\gamma$, not by its VC dimension. Later in the paper this yields bounds for networks with small weights that do not depend on the number of weights.

This mission formalizes the first of the paper's two main technical results, the margin bound of Theorem 2 (p. 527), together with the steps of its proof on pp. 527–528.

The fat-shattering dimension was introduced by Kearns and Schapire (JCSS 1994). Alon, Ben-David, Cesa-Bianchi and Haussler (J. ACM 1997) proved the scale-sensitive Sauer-type covering bound used here (Theorem 5 of the paper). Shawe-Taylor, Bartlett, Williamson and Anthony (IEEE Trans. Inform. Theory 1998) proved the zero-training-error version (Theorem 1 of the paper). Theorem 2 extends it to hypotheses that make margin errors on the training data.

Setting

Let $X$ be a set and $P$ a probability distribution on $X\times\{-1,1\}$. The threshold function is $\operatorname{sgn}(\alpha)=-1$ for $\alpha<0$ and $\operatorname{sgn}(\alpha)=1$ for $\alpha\ge0$. For a real-valued hypothesis $h$ on $X$, the misclassification probability is $\operatorname{er}_P(h)=P\{\operatorname{sgn}(h(x))\ne y\}$. For a sample $z=((x_1,y_1),\dots,(x_m,y_m))$ drawn independently from $P$ and $\gamma>0$, the margin error estimate is

$$\widehat{\operatorname{er}}{}^{\gamma}_z(h)=\tfrac1m\,|\{i : y_ih(x_i)<\gamma\}|.$$

Let $H$ be a class of real functions on $X$. Points $x_1,\dots,x_m$ are $\gamma$-shattered by $H$ if some $r\in\mathbb R^m$ has the following property: for every sign vector $b\in\{-1,1\}^m$, some $h\in H$ satisfies $(h(x_i)-r_i)b_i\ge\gamma$ for all $i$. The fat-shattering dimension $\operatorname{fat}_H(\gamma)$ is the largest such $m$, possibly $\infty$.

The proof uses the following objects:

• the squashing function $\pi_\gamma(\alpha)=\max(-\gamma,\min(\gamma,\alpha))$ and the class $\pi_\gamma(H)=\{\pi_\gamma\circ h:h\in H\}$;
• the sample $\ell_\infty$ pseudometric $d_{\ell_\infty(x)}(f,g)=\max_i|f(x_i)-g(x_i)|$;
• the covering number $\mathcal N_\infty(F,\epsilon,m)$, the largest over $x\in X^m$ of the size of the smallest $\epsilon$-cover (Definition 3), and the corresponding packing number $\mathcal M_\infty(F,\alpha,m)$;
• the quantization $Q_\alpha(x)=\lceil (x-\alpha/2)/\alpha\rceil\alpha$.

Formalization targets

Goal: Theorem 2

Assume $0<\delta<1/2$, $0<\gamma<1$, $m\ge1$, and $d=\operatorname{fat}_H(\gamma/16)$ finite with $d\le 34m$. With probability at least $1-\delta$ over $z$, every $h\in H$ satisfies

$$\operatorname{er}_P(h)<\widehat{\operatorname{er}}{}^{\gamma}_z(h)+\sqrt{\frac2m\Bigl(d\ln\frac{34em}{d}\log_2(578m)+\ln\frac4\delta\Bigr)} .$$

Milestones, in the order the proof uses them

1. Lemma 4. $\operatorname{er}_P(h)<\widehat{\operatorname{er}}{}^{\gamma}_z(h)+\sqrt{(2/m)\ln(2\mathcal N_\infty(\pi_\gamma(H),\gamma/2,2m)/\delta)}$ uniformly over $H$, with probability at least $1-\delta$.
2. Theorem 5 (Alon et al.). If $F:\{1,\dots,n\}\to\{1,\dots,b\}$ and $\operatorname{fat}_F(1)\le d$, then $\log_2\mathcal N_\infty(F,2,n)<1+\log_2(nb^2)\log_2\sum_{i\le d}\binom ni b^i$, provided $n$ is large enough.
3. Writing $F=Q_{\gamma/8}(\pi_\gamma(H))$: $\operatorname{fat}_F(\gamma/8)\le\operatorname{fat}_{\pi_\gamma(H)}(\gamma/16)$.
4. $\mathcal M_\infty(\pi_\gamma(H),\gamma/2,2m)\le\mathcal M_\infty(F,\gamma/2,2m)$.
5. $\mathcal N_\infty(\pi_\gamma(H),\gamma/2,2m)\le\mathcal N_\infty(F,\gamma/4,2m)$.
6. $\log_2\mathcal N_\infty(\pi_\gamma(H),\gamma/2,2m)<1+d\log_2(34em/d)\log_2(578m)$ when $1\le d\le 2m$ and $m\ge d\log_2(34em/d)+1$.
7. $\operatorname{fat}_{\pi_\gamma(H)}(\gamma/16)\le\operatorname{fat}_H(\gamma/16)$.

A further item, Proposition 8 (p. 529), is the probabilistic device the paper uses to make such bounds uniform over $\gamma$.

Significance

Theorem 2 is the bound behind the paper's main message. Corollary 9 makes it uniform over $\gamma$, and Theorem 28 combines it with fat-shattering estimates for networks with bounded weights. Together they show that a network classifying the training data with a large margin generalizes at a rate governed by the size of its weights, not by its number of weights. The same template, a margin error plus a capacity term at scale $\gamma$, underlies later margin analyses of support vector machines and boosting.

All results in this mission are proved in the literature; none is open. None is machine-checked on this platform: the platform has Rademacher-complexity margin bounds, but no statement about fat-shattering dimension or $\ell_\infty$ sample covering numbers of real-valued classes. A complete formalization would provide a reusable library of these objects, with their basic inequalities between squashing, quantization, packing and covering. It would also give a checked version of the explicit constants $34em/d$ and $578m$, which differ from those in later textbook treatments.

Difficulty

The bound is uniform over a possibly uncountable class $H$, so a union bound over hypotheses does not apply. The obvious replacement is a union bound over a cover of $H$. Two steps make it hard:

• Lemma 4. It needs a ghost-sample symmetrization and a random-swap argument, carried out with an $\ell_\infty$ cover of the squashed class on the double sample, so the cover depends on the data.
• Theorem 5. Bounding that covering number by the fat-shattering dimension is a combinatorial counting argument about strongly shattered pairs. It is the scale-sensitive analogue of the Sauer–Shelah lemma, and here the bookkeeping of constants is exact.

The quantization steps look routine but carry the factor-of-two losses that produce the constants $\gamma/16$, $17$ and $578$.

Formalization scope

The model is in the namespace BartlettNN.Margin.

• Labels and samples. Labels are Bool, read as $\pm1$ through pm (true is $+1$). $\operatorname{sgn}(0)=1$. Samples are functions Fin m → X × Bool, indexed from $0$, with law Measure.pi (fun _ => P). The margin estimate uses the strict inequality $y_ih(x_i)<\gamma$, and shattering uses $\ge\gamma$.
• Fat-shattering dimension. $\operatorname{fat}$ is valued in ℕ∞. A ℕ-valued supremum would be $0$ on an unbounded set, so the goal assumes fat H (γ/16) = d with d : ℕ.
• Covering and packing numbers. Covers are finite and external (centres are arbitrary functions), the cover inequality is strict, and covering numbers are ⊤ when no finite cover exists. $\mathcal N_\infty$ and $\mathcal M_\infty$ are suprema over all samples, with repetitions allowed. "$\alpha$-separated", which the paper leaves undefined, is read as distance $\ge\alpha$.
• Logarithms. $\ln$ is Real.log, $\log_2$ is Real.logb 2, and $e$ is Real.exp 1.
• High probability. "With probability at least $1-\delta$, every $h$" bounds the measure of the event that some $h\in H$ violates the inequality. It is not a per-hypothesis statement.

Measurability. The paper states "we ignore issues of measurability, and assume that all sets considered are measurable" (p. 526). This is made explicit, not removed, through three hypotheses:

• every $h\in H$ is measurable;
• the bad events $\{z:\exists h\in H,\ \operatorname{er}_P(h)\ge\widehat{\operatorname{er}}{}^{\gamma}_z(h)+\epsilon\}$ are measurable;
• the double-sample events of display (1) are measurable.

Replacing these by countability of $H$ would weaken the theorem.

Corrections of the printed text.

• Theorem 2. The goal adds $d\le 34m$. Beyond $34m$ the term $d\ln(34em/d)$ decreases, vanishes at $d=34em$ and then turns negative, and the printed statement fails for rich classes. Within this range nothing is lost: the proof covers $d\le2m$, and for $2m<d\le34m$ the bound exceeds $1$.
• Milestone 6. It carries the hypothesis $d\le 2m$, the range of the binomial estimate behind $34em/d$.
• Milestone 3. Its printed justification $|Q_{\gamma/8}(a)-Q_{\gamma/8}(b)|<|a-b|+\gamma/16$ is false; the correct term is $\gamma/8$. The milestone's conclusion is true as printed, and only the conclusion is formalized.

Trivializing formalizations, ruled out. The following would each make the statements empty or different, and none is used:

• a ℕ-valued fat dimension or covering number;
• Real.sign in place of $\operatorname{sgn}$;
• a per-hypothesis probability bound;
• an unrestricted $d$, which makes $\sqrt{\cdot}$ of a negative number equal to $0$;
• a covering number that is $0$ on classes without finite covers.

Infrastructure that a complete development needs, and contributions that are welcome:

• product measures and Hoeffding's inequality, which Mathlib has;
• a symmetrization (ghost-sample) lemma for margin events;
• the combinatorics of Theorem 5;
• the elementary inequalities between packing and covering numbers.

The covering/packing and fat-shattering lemmas apply beyond this mission. Proofs of individual milestones, or of Theorem 5 in the generality of Alon et al., are useful contributions in their own right.

Selected references

• P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Trans. Inform. Theory 44(2), 525–536, 1998. https://doi.org/10.1109/18.661502
• N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, J. ACM 44(4), 615–631, 1997. https://doi.org/10.1145/263867.263927
• J. Shawe-Taylor, P. L. Bartlett, R. C. Williamson, M. Anthony, Structural risk minimization over data-dependent hierarchies, IEEE Trans. Inform. Theory 44(5), 1926–1940, 1998. https://doi.org/10.1109/18.705570
• M. J. Kearns, R. E. Schapire, Efficient distribution-free learning of probabilistic concepts, J. Comput. Syst. Sci. 48(3), 464–497, 1994. https://doi.org/10.1016/S0022-0000(05)80062-5
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory Probab. Appl. 16(2), 264–280, 1971. https://doi.org/10.1137/1116025

Motivation

In data-driven algorithm design, an algorithm or mechanism comes with a vector of tunable parameters $\rho$, and the parameters are chosen by optimizing average performance over sample instances drawn from an unknown distribution. How many samples suffice for the empirical optimum to be near-optimal in expectation is governed by the pseudo-dimension of the class $\mathcal U=\{u_\rho\}$ of performance functions, where $u_\rho(x)$ is the performance of the parameter $\rho$ on instance $x$. Balcan, DeBlasio, Dick, Kingsford, Sandholm and Vitercik (arXiv:1908.02894v4, 2021) give a general upper bound on $\mathrm{Pdim}(\mathcal U)$ for classes whose dual functions are piecewise structured (their Theorem 3.3, the subject of mission 1 of this series), and apply it across integer programming, computational biology, clustering and mechanism design.

A general upper bound raises the question of whether it can be improved. Section 5 of the paper answers it for one application: neutral affine maximizers (NAMs), a family of voting mechanisms studied by Roberts (1979), Mishra and Sen (2012) and Nath and Sandholm (2019). For NAMs with $n$ agents and $m$ alternatives the general theorem gives $\mathrm{Pdim}(\mathcal U)=O(n\ln m)$, and Theorem 5.2 shows a lower bound linear in $n$. So the sample complexity of tuning a NAM by sampling cannot be reduced below order $n$ by a sharper analysis, and the general bound is tight up to logarithmic factors.

Setting

There are $n$ agents and $m$ alternatives. Agent $i$ has a value $v_i(j)\in\mathbb R$ for each alternative $j\in[m]$; a valuation profile is $v=(v_1,\dots,v_n)\in\mathbb R^{nm}$.

A NAM is specified by a weight vector $\rho=(\rho[1],\dots,\rho[n])\in\mathbb R^n_{\ge0}$ in which at least one agent has weight zero; an agent with $\rho[i]=0$ is a sink agent. The NAM's outcome on a profile $v$ is an alternative maximizing the weighted value,

$$\psi_\rho(v)\in\operatorname*{argmax}_{j\in[m]}\ \sum_{i=1}^n\rho[i]\,v_i(j).$$

Its utility is the social welfare of that outcome,

$$u_\rho(v)=\sum_{i=1}^n v_i\bigl(\psi_\rho(v)\bigr),$$

and the class studied is $\mathcal U=\{u_\rho \mid \rho\in\mathbb R^n_{\ge0},\ \{i\mid\rho[i]=0\}\ne\emptyset\}$. NAMs also charge VCG-style payments that are redistributed to the sink agents; these do not enter $u_\rho$.

A class $\mathcal H$ of real-valued functions on a set $Y$ shatters points $y_1,\dots,y_N$ if there are thresholds $z_1,\dots,z_N\in\mathbb R$ such that every pattern $b\in\{0,1\}^N$ is realized by some $h\in\mathcal H$, in the sense that $h(y_\ell)>z_\ell$ exactly when $b_\ell=1$. The pseudo-dimension $\mathrm{Pdim}(\mathcal H)$ is the largest $N$ for which some $N$ points are shattered. In Lean: a profile is v : Fin n → Fin m → ℝ, the outcome rule is ψ, the utility is welfare ψ ρ, the class is namClass ψ, and shattering is the published FoundationsML.Regression.Shatters.

Formalization targets

Goal: Theorem 5.2, corrected

For every $n\ge1$, every $m\ge2$ and every tie-breaking rule,

$$\mathrm{Pdim}(\mathcal U)\ \ge\ \Bigl\lfloor\frac n2\Bigr\rfloor .$$

The printed statement reads $\mathrm{Pdim}(\mathcal U)\ge n/2$; see Formalization scope for why the floor is needed.

Milestones: the two claims of the proof (p. 24)

The proof fixes $N=\lfloor n/2\rfloor$ explicit profiles $v^{(1)},\dots,v^{(N)}$ and, for each bit vector $b\in\{0,1\}^N$, an explicit weight vector $\rho\in\{0,1\}^n$ (both are definitions of this mission). The two milestones are the claims the proof makes about them: for every $\ell\in[N]$ and $\varepsilon\in(0,\tfrac12)$,

$$b_\ell=0\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=\varepsilon,\qquad b_\ell=1\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=1 .$$

Significance

The result. Theorem 5.2 is the paper's evidence that its main upper bound cannot be improved in general by more than logarithmic factors: for NAMs the upper bound is $O(n\ln m)$ and the lower bound is of order $n$. Through the standard link between pseudo-dimension and uniform convergence, it also means that any learner choosing NAM weights from samples needs a number of samples growing with the number of agents, whatever tie-breaking rule the mechanism uses.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any pseudo-dimension lower bound for a mechanism class, was found on Prove2Me. This mission produces a Lean model of NAM outcomes and welfare that does not fix a tie-breaking rule, an explicit lower-bound construction stated as definitions, and a pseudo-dimension lower bound in the vocabulary of the published FoundationsML pseudo-dimension items. It complements mission 1, which formalizes the matching upper-bound machinery.

Difficulty

The mathematical content is a single explicit construction, and the work lies in stating and verifying it at full generality rather than in a deep argument. Three points make the naive transcription wrong. First, the printed bound $n/2$ is false at $n=1$ and is not what the proof establishes for odd $n$; the even-$n$ reduction must be replaced by a statement in $\lfloor n/2\rfloor$. Second, the outcome $\psi_\rho(v)$ is defined by an argmax with unspecified tie-breaking, so the claims must hold for every maximizer; this requires showing the relevant maximizers are unique on the constructed profiles, not reading off a convenient one. Third, the construction embeds $\lfloor n/2\rfloor$ indices into the $n$ agents twice (as $\ell$ and $\lfloor n/2\rfloor+\ell$), and the printed index condition for the second alternative is a typo; an off-by-one in this embedding silently breaks both claims. Finally, every constructed $\rho$ must be admissible: it needs a sink agent, which holds only because $N\ge1$ or because $n$ is odd and the last agent keeps weight $0$.

Formalization scope

Representation. Agents are Fin n, alternatives Fin m, profiles Fin n → Fin m → ℝ, all 0-based: the paper's agent $i$ is i - 1, and its first and second alternatives are 0 and 1. Bits are Bool with true for $1$. An outcome rule is any ψ : (Fin n → ℝ) → (Fin n → Fin m → ℝ) → Fin m with IsArgmaxSelector ψ, which requires ψ ρ v to maximize ∑ i, ρ i * v i j for every ρ and v; the theorem and both claims are stated for every such ψ. "$\mathrm{Pdim}(\mathcal U)\ge N$" is the existence of an $N$-tuple of profiles shattered by namClass ψ in the sense of FoundationsML.Regression.Shatters, whose strict threshold t i < g (z i) shatters the same tuples as the paper's sign convention.

Corrections and readings of the printed text.

1. The bound is $\lfloor n/2\rfloor$ (natural-number division n / 2) instead of $n/2$. The proof assumes $n$ even; at $n=1$ the only admissible $\rho$ is $0$, so $\mathcal U$ is a single function and $\mathrm{Pdim}(\mathcal U)=0<\tfrac12$.
2. The hypotheses $n\ge1$ and $m\ge2$ are explicit. For $n=0$ no weight vector has a zero coordinate and $\mathcal U=\emptyset$; for $m=1$ the class is a single function. The proof takes $m=2$; the statement is for every $m\ge2$, with value $0$ on every further alternative in the constructed profiles.
3. The set-builder "$\{\rho[i]\mid i=0\}\ne\emptyset$" in Theorem 5.2 is read as $\{i\mid\rho[i]=0\}\ne\emptyset$, as written in Lemma 5.1.
4. The construction's condition "$\ell=n/2+i$" for $v_i^{(\ell)}(2)=\varepsilon$ is read as $i=n/2+\ell$, as the paper's own $n=6$ example shows. The milestone texts are verbatim and keep the printed "$v^{(\ell)}_{n/2+\ell}(1)$", which should read "$(2)$".

Ruled-out trivializations. Fixing one tie-breaking rule would state a special case and is excluded by quantifying over all argmax selectors. Dropping the sink-agent condition, or allowing $n=0$ or $m=1$, would change the class or make the statement vacuous or false; the conventions above exclude all three.

Infrastructure. Only Mathlib finite sums over Fin and the published Shatters definition are needed. The NAM model (IsNAMParam, IsArgmaxSelector, welfare, namClass) is reusable for any further statement about learning NAM parameters, including the matching $O(n\ln m)$ upper bound once mission 1's general theorem is available. Proofs of the two claims, of the admissibility of the constructed weight vectors, and of the goal are all welcome.

Selected references

• M.-F. Balcan, D. DeBlasio, T. Dick, C. Kingsford, T. Sandholm, E. Vitercik, How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design, arXiv:1908.02894v4, 2021. https://arxiv.org/abs/1908.02894v4
• K. Roberts, The characterization of implementable social choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979 (reference [86] of the paper).
• D. Mishra, A. Sen, Roberts' theorem with neutrality: a social welfare ordering approach, Games and Economic Behavior 75(1):283–298, 2012 (reference [74] of the paper).
• S. Nath, T. Sandholm, Efficiency and budget balance in general quasi-linear domains, Games and Economic Behavior 113:673–693, 2019 (reference [78] of the paper).
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (pseudo-dimension; reference [83] of the paper).

Motivation

Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only $o(T)$ regret in time $T$ (Granmo 2010; May, Korda, Lee and Leslie 2011).

Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the $N$-armed bound, Theorem 2.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least $\big[\sum_i \Delta_i/D(\mu_i\|\mu^*)+o(1)\big]\ln T$. Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an $O(\sum_i \ln T/\Delta_i)$ finite-time bound. Agrawal and Goyal (2012) proved $O(\ln T/\Delta+1/\Delta^3)$ for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.

Setting

There are two arms. Arm $i\in\{1,2\}$ has a fixed, unknown reward distribution $D_i$ supported in $[0,1]$, with mean $\mu_i$. Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, $\mu_1>\mu_2$, and $\Delta=\mu_1-\mu_2$ is the gap.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$, a success count $S_i$ and a failure count $F_i$, both starting at $0$. In each round $t=1,2,\dots$ it

1. samples, independently for each arm, $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$;
2. plays $i(t)=\arg\max_i\theta_i(t)$ and observes a reward $\tilde r_t\sim D_{i(t)}$;
3. performs a Bernoulli trial with success probability $\tilde r_t$, with outcome $r_t\in\{0,1\}$;
4. increments $S_{i(t)}$ if $r_t=1$ and $F_{i(t)}$ otherwise.

$k_i(t)$ is the number of plays of arm $i$ before round $t$. The expected regret in time $T$ is

$$\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu_1-\mu_{i(t)})\Big],$$

the expectation being over the rewards and the algorithm's randomness.

The analysis uses the Beta cdf $F^{beta}_{\alpha,\beta}$, the binomial cdf $F^B_{n,p}$, and the random variable $X(j,s,y)$: the number of independent $\mathrm{Beta}(s+1,j-s+1)$ draws made before one exceeds $y$.

Formalization targets

Goal: Theorem 1 (p. 3)

There is an absolute constant $C>0$ such that for every two-armed instance with rewards in $[0,1]$ and $\mu_1>\mu_2$, and every $T\ge 2$,

$$\mathbb E[\mathcal R(T)]\le C\Big(\frac{\ln T}{\Delta}+\frac1{\Delta^3}\Big).$$

The constant is not fixed numerically: the paper states the theorem in $O(\cdot)$ form (footnote 1), and the explicit display it reports on p. 8, $40\ln T/\Delta+48/\Delta^3+18\Delta$, is not the formal claim.

Milestones

• Fact 1 (p. 12): $F^{beta}_{\alpha,\beta}(y)=1-F^B_{\alpha+\beta-1,y}(\alpha-1)$ for positive integers $\alpha,\beta$.
• Lemma 1 (p. 6): $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$.
• Lemma 6 (p. 13): Hoeffding-type bounds (10)–(11) on binomial cdfs.
• Fact 2 (p. 13): every median of $\mathrm{Binomial}(n,p)$ is $\lfloor np\rfloor$ or $\lceil np\rceil$.
• Lemma 2 (p. 7): $\Pr(E_2(t))\ge 1-2/T^2$, where $E_2(t)=\{\theta_2(t)\le\mu_2+\Delta/2\ \text{or}\ k_2(t)<24\ln T/\Delta^2\}$.
• Lemma 3 (p. 7): a three-case bound on $\mathbb E\big[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]\big]$ for $s(j)\sim\mathrm{Binomial}(j,\mu_1)$.
• Eq. (1) (p. 7): $\mathbb E[k_2(T)]\le C(\ln T/\Delta^2+1/\Delta^4)$.

Significance

The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in $T$ on every two-armed instance, matching the order in $T$ of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.

Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on $[0,1]$-valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.

Difficulty

The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after $\Theta(\ln T/\Delta^2)$ plays. Under TS the optimal arm's sample $\theta_1(t)$ is random and, if the arm has been played rarely or its early rewards were poor, it falls below $\mu_2$ with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the $1/\Delta^3$ dependence enters.

Formalization scope

• Model. The instance is the platform's StochasticBandit 2 (a probability measure on $\mathbb R$ per arm, mean banditArmMean), with the hypothesis that each reward law gives mass $1$ to $[0,1]$. Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from $0$.
• Algorithm. Algorithm 2 is realized on one probability space with three independent i.i.d. tables: Beta draws $W(i,t,a,b)\sim\mathrm{Beta}(a+1,b+1)$, rewards $X(i,t)\sim D_i$, and uniforms $V(i,t)$. Round $t$ uses $\theta_i(t)=W(i,t,S_i(t),F_i(t))$, $\tilde r_t=X(i(t),t)$ and $r_t=\mathbf 1\{V(i(t),t)<\tilde r_t\}$. Ties in the arg max go to the smaller index (a null event).
• Values. Regret and expectations are lower Lebesgue integrals in $[0,\infty]$. $X(j,s,y)$ is $\mathbb N\cup\{\infty\}$-valued, so Lemma 1 at $y=1$ reads $\infty=\infty$, as in the paper.
• O(·). The paper's $O(\cdot)$ (footnote 1: $f\le cg$ for $n\ge n_0$) is stated with one universal constant $C>0$, quantified before the instance, the means and the horizon, for all $T\ge 2$. Eq. (1) is stated the same way, without its printed numerals.
• Not trivial. The goal is about Algorithm 2 itself, with fresh Beta samples, fresh rewards and the Bernoulli coin. A statement about "any policy satisfying Lemma 2's event bound", or one whose constant depends on $\Delta$, the reward laws or $T$, would not be Theorem 1.
• Edge cases. $\mu_1<1$ is assumed only in Lemma 3, where the paper's $R$ and $D$ require it. It is not a hypothesis of the goal.
• Infrastructure. A complete proof needs: inverse-transform or order-statistics facts for Beta laws (Fact 1); geometric expectations; Hoeffding's inequality for sums of Bernoulli variables (Mathlib has Hoeffding/Azuma); the binomial median theorem (Jogdeo–Samuels; Kaas–Buhrman); and the coupling from the reward tables to the per-arm i.i.d. output stacks the paper reasons with. Fact 1, Lemma 6 and Fact 2 are reusable beyond this mission. Contributions to any milestone are welcome, and so is a direct proof of the regret bound with an explicit constant.

Selected references

• S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3. https://arxiv.org/abs/1111.1797
• W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933) 285–294. https://doi.org/10.2307/2332286
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6 (1985) 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47 (2002) 235–256. https://doi.org/10.1023/A:1013689704352
• K. Jogdeo and S. M. Samuels, Monotone convergence of binomial probabilities and a generalization of Ramanujan's equation, Annals of Mathematical Statistics 39 (1968) 1191–1195. https://doi.org/10.1214/aoms/1177698243
• R. Kaas and J. M. Buhrman, Mean, median and mode in binomial distributions, Statistica Neerlandica 34 (1980) 13–18. https://doi.org/10.1111/j.1467-9574.1980.tb00681.x
• O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling

Motivation

Learning an unknown quantum state is expensive. Full quantum state tomography of a $D$-dimensional mixed state $\rho$ to accuracy $\varepsilon$ in trace distance needs on the order of $D^2/\varepsilon^2$ copies of $\rho$ (O'Donnell–Wright 2016; Haah et al. 2017), and this is optimal. For a system of $n$ qubits, $D = 2^n$, so full tomography is out of reach beyond a few dozen qubits.

Often one does not need the whole density matrix, only the behaviour of $\rho$ on a fixed list of tests: acceptance probabilities of verification circuits, expectation values of observables, or the answers a piece of quantum advice gives to a set of questions. Aaronson (arXiv:1711.01053, STOC 2018) named this task shadow tomography and asked whether the number of copies can be polylogarithmic in both the dimension and the number of tests. Measuring each test on separate copies costs $\tilde O(M/\varepsilon^2)$ copies, which is linear in $M$.

Timeline.

• 2016: the question was posed at a mini-course without a name (Aaronson, The Complexity of Quantum States and Transformations, §8.3.1).
• 2016: Harrow, Lin and Montanaro gave a correct "quantum OR" test, repairing an earlier flawed claim (arXiv:1607.03236, Corollary 11).
• 2017–2018: Aaronson proved the first polylogarithmic bound, the theorem of this mission.
• Later work improved the exponents, notably Bădescu–O'Donnell 2021, and introduced the related "classical shadows" of Huang–Kueng–Preskill 2020.

Setting

A mixed state of dimension $D$ is a $D\times D$ Hermitian positive semidefinite matrix $\rho$ with $\mathrm{Tr}\,\rho = 1$. A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with all eigenvalues in $[0,1]$. Equivalently, $0 \preceq E \preceq \mathbb 1$. It accepts $\rho$ with probability $\mathrm{Tr}(E\rho)$.

The state $\rho^{\otimes k}$ consists of $k$ independent copies of $\rho$. A measurement of $\rho^{\otimes k}$ with classical output is a POVM: a finite family of positive semidefinite matrices $P_\omega$ on the $k$-register space with $\sum_\omega P_\omega = \mathbb 1$. Outcome $\omega$ occurs with probability $\mathrm{Tr}(P_\omega\rho^{\otimes k})$. An adaptive procedure that measures the copies one after another is described by one such POVM.

Problem 1 (shadow tomography). Given an unknown $\rho$ and known two-outcome measurements $E_1,\dots,E_M$, output numbers $b_1,\dots,b_M\in[0,1]$ with $|b_i-\mathrm{Tr}(E_i\rho)|\le\varepsilon$ for all $i$, with success probability at least $1-\delta$. The output must come from a measurement of $\rho^{\otimes k}$, with $k=k(D,M,\varepsilon,\delta)$ as small as possible. The measurement may depend on the $E_i$, but not on $\rho$.

Formalization targets

Goal: Theorem 2, in the explicit form proved in §5

There is a universal constant $C$ such that, for $M\ge2$ and $0<\varepsilon,\delta\le 1/2$, Problem 1 is solvable with

$$k \le C\,\frac{\log D}{\varepsilon}\Big(\frac{\log\log D+\log\frac1\varepsilon}{\varepsilon^{2}}\Big)^{2}\log^4 M\Big(\log\log M+\log\log D+\log\frac1\varepsilon+\log\frac1\delta\Big) = \tilde O\Big(\frac{\log 1/\delta}{\varepsilon^5}\log^4 M\log D\Big)$$

copies. This is the last display of the proof (p. 19). The goal fixes no constant, so any improvement of $C$ remains consistent with it.

Milestones

• Theorem 13 (Harrow–Lin–Montanaro). A one-copy test that accepts with probability at least $(1-\epsilon)^2/7$ if some $\mathrm{Tr}(E_i\rho)\ge1-\epsilon$, and at most $4\Delta M$ if $\sum_i\mathrm{Tr}(E_i\rho)\le\Delta M$.
• Lemma 14 (Quantum OR Bound). Deciding whether $\max_i\mathrm{Tr}(E_i\rho)\ge c$ or $\le c-\varepsilon$ with $O(\log(1/\delta)\log M/\varepsilon^2)$ copies, independent of $D$.
• Lemma 15 (Gentle Search). Finding $j$ with $\mathrm{Tr}(E_j\rho)\ge c-\varepsilon$ with $O(\frac{\log^4M}{\varepsilon^2}(\log\log M+\log\frac1\delta))$ copies.
• Amplification claims (p. 16). The threshold tests $E^*_{i,t,\pm}$ on $\rho^{\otimes q}$ accept with probability at least $5/6$ when the hypothesis is off by $\varepsilon$, and at most $1/3$ when it is within $\varepsilon/2$.
• Markov claim (p. 17). The postselection test $F_t$ on an arbitrary, possibly entangled, $q$-register state accepts with probability at most $\frac{a q}{(a+\varepsilon/4)q}$.
• Lemma 12 (Quantum Union Bound, probability part). Measurements each accepting with probability at least $1-\varepsilon$ all accept in succession with probability at least $1-2M\sqrt\varepsilon$.
• Chernoff claim (p. 18). $1-\mathrm{Tr}(F_t\rho^{\otimes q})\le\varepsilon^4/\log^2D$.
• Proposition 20. Promise-gap thresholds for all $i$ at once can be decided with $O(\log(M/\delta)/\varepsilon^2)$ copies.

Significance

The result. Theorem 2 shows that a state of exponential dimension can be learned "for all practical purposes" on exponentially many tests from polynomially many copies. Applications in the paper include a bound on quantum advice and one-way communication, and implications for quantum money and copy-protection. It also shows that the information needed to predict many measurement outcomes is far smaller than the description of $\rho$.

Formalizing it. The theorem is proved in the paper, and later work improves its exponents. As far as is known it has not been machine-checked. A complete development formalizes the gentle-measurement toolkit (Lemma 12, Lemma 14, Lemma 15), the amplification of two-outcome measurements on tensor powers, and the postselection argument. These are standard tools of quantum learning theory and quantum complexity with no formal counterpart yet. Lemma 14 and Lemma 15 are reusable beyond this mission.

Difficulty

The naive approach measures the $E_i$ directly on shared copies. A measurement that is likely to reject disturbs the state, so later measurements see a damaged state, and separate copies per measurement cost $M$ copies.

The proof needs three ingredients:

• a gentle search that finds a measurement on which the current hypothesis is wrong while damaging the copies only slightly;
• a potential argument showing that postselection cannot happen too often;
• a uniform control of the damage.

The potential argument has to hold for the state after postselection, which is correlated or entangled across registers. Independence-based concentration fails there, which is why the Markov claim, not a Chernoff bound, governs that step. Theorem 13 itself rests on a delicate ancilla-based procedure of Harrow, Lin and Montanaro, and the mission cites it as a milestone without its proof.

Formalization scope

• Representation.
  • Operators are complex matrices over a finite index type, and states use the published WildeQIT.IsDensityOperator (positive semidefinite, trace one).
  • A two-outcome measurement is IsEffect E: both $E$ and $\mathbb 1-E$ are positive semidefinite.
  • $\rho^{\otimes k}$ is a matrix indexed by $k$-tuples Fin k → n.
  • A measurement with output is a POVM structure with a finite outcome type. Probabilities are real parts of traces.
• Quantifier order of the goal. $\exists C$, then for all $D,M,\varepsilon,\delta$ there is $k$; then for all $E_i$ there are a POVM and outputs $b$; then for all $\rho$. Choosing the measurement after $\rho$ would make the goal trivial (output the true values with $k=0$), and this order rules that out.
• Disclosed hypotheses.
  • Theorem 2 assumes $M\ge2$, $\varepsilon\le1/2$ and $\delta\le1/2$. These keep the logarithmic factors positive; at $M=1$ the bound would force $k=0$.
  • Lemma 14 assumes $M\ge2$, and Lemmas 14 and 15 bound $\delta$.
  • Theorem 13 assumes $\epsilon\le1/2$, as in Harrow–Lin–Montanaro's Corollary 11.
  • The Chernoff claim assumes $D\ge2$.
• Conventions.
  • All logarithms are natural, including inside $\log\log$.
  • Amplified tests use real thresholds.
  • "Applied in succession" in Lemma 12 uses Lüders instruments ($\sqrt{E}$ Kraus operators), in the order $E_1,E_2,\dots$.
  • The hypothesis $\rho_t$ enters the amplification claims only as the number $a=\mathrm{Tr}(E\rho_t)$.
• Printed steps not drafted.
  • The printed $\varepsilon^{-4}$ form of Theorem 2 relies on an external online-learning algorithm that is only sketched.
  • The halting rule of §5 is unspecified, because Lemma 15 always returns an index.
  • The asymptotic claims $p_t\ge0.9/D^q$ for $t=o(\log^2D/\varepsilon^4)$ and $t=O(q\log D/\varepsilon)$ use a circular $o(\cdot)$.
  • The trace-distance part of Lemma 12 has an unquantified $O(\cdot)$.
  • Lemma 12's printed bound $1-2M\sqrt\varepsilon$ is weaker than its use on p. 18. It is stated as printed. The proof of the goal must retune constants or use Wilde's stronger $1-2\sqrt{M\varepsilon}$-type bound.
• Contributions welcome. Proofs of any milestone; a formal Hoeffding bound for binomial counts of product effects; the gentle measurement lemma for Lüders instruments; Naimark dilation for effects.

Selected references

• S. Aaronson, Shadow Tomography of Quantum States, STOC 2018; arXiv:1711.01053v2, 2018. https://arxiv.org/abs/1711.01053
• A. W. Harrow, C. Y.-Y. Lin, A. Montanaro, Sequential measurements, disturbance and property testing, SODA 2017. https://arxiv.org/abs/1607.03236
• M. M. Wilde, Sequential decoding of a general classical-quantum channel, Proc. R. Soc. A, 2013. https://arxiv.org/abs/1303.0808
• R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
• J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory, 2017. https://arxiv.org/abs/1508.01797
• C. Bădescu, R. O'Donnell, Improved quantum data analysis, STOC 2021. https://arxiv.org/abs/2011.10908
• H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics, 2020. https://arxiv.org/abs/2002.08953

Motivation

A correlated equilibrium (Aumann, 1974) is a joint distribution over the players' strategy profiles from which no player gains by deviating from a recommended strategy. A central question of learning in games is which equilibria repeated play of simple, myopic rules can reach. Foster and Vohra (1997) answered it for calibrated forecasting: if each player forecasts the opponent with a calibrated rule and best-responds to the forecast, the empirical distribution of play approaches the set of correlated equilibria (their Theorem 1). That result has become a basic reference point for no-regret and calibration-based learning in games (Hart and Mas-Colell, 2000).

This mission formalizes the paper's converse. Theorem 1 says calibrated learning ends up in the correlated equilibria; the converse says it can end up at any of them, for almost every game. Together the two results characterize exactly which long-run outcomes calibrated learning with best responses can produce.

Setting

Two players choose strategies from finite sets $S(1)$ with $m$ elements and $S(2)$ with $n$ elements; player $i$ receives payoff $u_i(x,y)\in\mathbb{R}$ and maximizes it. A game $G=(u_1,u_2)$ is a pair of real $m\times n$ matrices, that is, a point of $\mathbb{R}^{2mn}$; a set of games has measure zero if it is Lebesgue-null in $\mathbb{R}^{2mn}$.

A joint distribution $D$ on $S(1)\times S(2)$ is a correlated equilibrium if for every map $\Phi:S(1)\to S(1)$, $\sum_{x,y}D(x,y)u_1(\Phi(x),y)\le\sum_{x,y}D(x,y)u_1(x,y)$, and symmetrically for player 2. $\pi(G)$ is the set of correlated equilibria.

Play is repeated in rounds $t=0,1,2,\dots$. Before each round, player 1 issues a forecast $f_1(t)$, a probability vector over $S(2)$, produced by a deterministic forecasting rule from the history of play so far; player 2 likewise forecasts player 1. For a forecast sequence $f$ and the opponent's plays $z$, let $N(p,t)$ be the number of the first $t$ rounds with forecast $p$, and $\rho(p,j,t)$ the fraction of those rounds in which the opponent played $j$ (zero if $N(p,t)=0$). The forecasts are calibrated if for every $j$

$$\sum_p |\rho(p,j,t)-p_j|\,\frac{N(p,t)}{t}\ \longrightarrow\ 0 \qquad (t\to\infty).$$

Each player then plays $R_i$ of its forecast, where the best-reply function $R_i$ picks a best response to every forecast and does not depend on the round. $D_t(x,y)$ is the fraction of the first $t$ rounds in which $(x,y)$ was played.

$\lambda(G)$, the set of limit points of calibrated forecasts, consists of the $D$ for which some best-reply functions $R_1,R_2$ and some calibrated forecasting rules make $D_t(x,y)\to D(x,y)$ for all $(x,y)$.

Formalization targets

Goal: Theorem 2 (p. 47)

$$\text{for Lebesgue-almost every } G\in\mathbb{R}^{2mn}:\qquad \lambda(G)=\pi(G).$$

Milestones

1. $\lambda(G)\subseteq\pi(G)$ for every game (Theorem 1 restated, p. 46).
2. Every joint distribution $D$ is the limiting empirical distribution of a deterministic play sequence supported on $\{D>0\}$ (p. 47).
3. Along such a sequence the conditional forecasts $p_{1,t}=D(x_t,\cdot)/\sum_yD(x_t,y)$ and $p_{2,t}=D(\cdot,y_t)/\sum_xD(x,y_t)$ are calibrated (p. 47).
4. In a correlated equilibrium each recommended strategy is a best response to its conditional forecast (p. 47).
5. For almost every payoff matrix, each set $M_b(x)$ of forecasts to which $x$ is a best response is either empty or contains a forecast in the open simplex at which $x$ is the unique best response (p. 47).
6. The perturbed forecasts $p_i=(1-1/i)p^*+(1/i)q$ converge to $p^*$ and keep a unique best reply (p. 48).
7. For the $3\times3$ game of p. 48, a correlated equilibrium lies outside $\lambda(G)$, and $\lambda(G)$ is the single point mass on $(C,2)$.

Significance

Theorem 1 by itself leaves open whether calibration selects among correlated equilibria, for instance toward Nash equilibria or toward particular payoffs. Theorem 2 closes that question negatively for generic games: every correlated equilibrium is the genuine limit, not merely an accumulation point, of calibrated play with stationary best replies. As the paper notes, adding the assumption that the limit exists therefore does not refine the equilibrium reached, in contrast with Fudenberg and Kreps's result for asymptotically myopic Bayesian play. The $3\times3$ example shows that the genericity hypothesis cannot be dropped.

The results are proved in the 1997 paper; none is formalized. A complete development produces a reusable layer for repeated two-player games (calibration, empirical distributions, best-reply maps, correlated equilibria), a genericity lemma for best-response regions that is useful beyond this paper, and a machine-checked version of an argument that the paper gives only in outline.

Difficulty

The natural construction takes a correlated equilibrium $D$, a play sequence realizing $D$, and forecasts equal to the conditional distributions of $D$. The forecasts are then calibrated and each played strategy is a best response. What fails is the best-reply function: two strategies $x'\ne x''$ can have the same conditional forecast $p^*$, while a stationary $R_1$ maps $p^*$ to only one strategy. Separating them needs forecasts near $p^*$ at which each is the unique best response, and that exists only when the best-response regions have nonempty relative interior, a property that fails on a null set of games (the $3\times3$ example) and whose genericity must be proved. The perturbed forecasts are no longer exactly equal to the conditional frequencies, so calibration has to be re-established with errors that vanish along the sequence.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; players maximize. A game is a point of (Fin m → Fin n → ℝ) × (Fin m → Fin n → ℝ) with Mathlib's volume (Lebesgue measure on $\mathbb{R}^{2mn}$), and "almost every" is ∀ᵐ.
• A correlated equilibrium is the joint-distribution form of p. 44 (a joint distribution with the two deviation inequalities).
• Forecasting rules map finite histories to probability vectors; the play is generated recursively from the rules and the best-reply functions. Best-reply functions are arbitrary stationary selections of a best response at every probability vector; they may not depend on the round, since round-dependent tie-breaking enlarges $\lambda(G)$ (the matching pennies example of p. 46).
• Rounds are $0,\dots,t-1$; $D_0=0$. The calibration sum runs over the forecasts issued so far, which is the paper's sum over all $p$ since the other terms vanish.
• $\lambda(G)$ requires convergence of $D_t$, not a subsequence. Replacing the limit by a limit point, or stating only $\pi(G)\subseteq\lambda(G)$, does not formalize the theorem.
• The page's sentence "Almost every game has the property that all the sets $M_b(x)$ have non-empty interior" is false for dominated strategies ($M_b(x)=\emptyset$ on an open set of games). Milestone 5 states the dichotomy the page's argument proves: empty or with relative interior.
• The page prints the denominator of $p_{2,t}$ as $\sum_{x}D(x_t,y)$; the mission uses $\sum_xD(x,y_t)$.

The theorems are stated from the mission's own definitions of the game, calibration and $\lambda(G)$; no statement is vacuous: at $m=0$ or $n=0$ both sides of the goal are empty, and the $3\times3$ example exercises every definition. Contributions welcome: proofs of the milestones in any order, the genericity lemma (Lebesgue-null sets of linear degeneracies), and the calibration estimates for the perturbed forecasts.

Selected references

• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982), 605–610. https://doi.org/10.1080/01621459.1982.10477856
• D. Fudenberg and D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5 (1993), 320–367. https://doi.org/10.1006/game.1993.1021
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

Many data sets are large matrices of which only a small fraction of the entries is observed, and of which the underlying object is believed to have low rank: user–item rating tables in collaborative filtering, distance matrices in sensor-network localization, and measurement matrices in structure-from-motion. Matrix completion asks when the missing entries can be recovered exactly. Rank minimization subject to the observed entries is intractable in general. Its convex relaxation, nuclear-norm minimization, is a semidefinite program, and the question is how many randomly placed entries it needs.

Timeline:

• 2008–2009. Candès and Recht (arXiv:0805.4471) proved that nuclear-norm minimization recovers an incoherent $n\times n$ matrix of rank $r$ from about $\mu_0 n^{6/5} r\log n$ uniformly sampled entries, and from $n^{5/4}$ in the low-rank regime. They also showed that about $\mu_0 nr\log n$ entries are necessary for any method.
• 2010. Candès and Tao (doi:10.1109/TIT.2010.2044061), the source of this mission, closed most of the gap. Under a strong incoherence assumption, $C\mu^2 nr\log^6 n$ entries suffice (Theorem 1.2), within a polylogarithmic factor of the information-theoretic limit, which the same paper sharpens (Theorem 1.7).
• 2009–2011. Keshavan, Montanari and Oh (arXiv:0901.3150) obtained comparable bounds for a non-convex method. Gross (arXiv:0910.1879) and Recht (arXiv:0910.0651) later gave much shorter proofs of an $O(\mu_0 nr\log^2 n)$ bound under a different incoherence condition, using matrix Bernstein inequalities and a "golfing" construction of the dual certificate.

Setting

Fix $M \in \mathbb{R}^{n\times n}$ of rank $r$ with singular value decomposition $M = \sum_{k=1}^r\sigma_k u_kv_k^*$, where $\sigma_k>0$ and $\{u_k\}$, $\{v_k\}$ are orthonormal. Let $P_U = \sum_k u_ku_k^*$, $P_V = \sum_k v_kv_k^*$, and let $E = \sum_k u_kv_k^*$ be the sign matrix. The tangent space $T$ at $M$ is the image of the projection

$$\mathcal{P}_T(X) = P_UX + XP_V - P_UXP_V,$$

and $\mathcal{P}_{T^\perp} = \mathcal{I} - \mathcal{P}_T$.

$M$ obeys the strong incoherence property with parameter $\mu$ if every entry of $P_U$ and $P_V$ is within $\mu\sqrt r/n$ of the corresponding entry of $(r/n)I$, and every entry of $E$ is at most $\mu\sqrt r/n$ in absolute value.

An observation set $\Omega \subseteq [n]\times[n]$ is either a uniformly random $m$-subset (the uniform model) or contains each entry independently with probability $p = m/n^2$ (the Bernoulli model). $\mathcal{P}_\Omega$ keeps the entries in $\Omega$ and zeroes the rest. The program is

$$\text{minimize } \|X\|_* \text{ subject to } \mathcal{P}_\Omega(X) = \mathcal{P}_\Omega(M), \qquad \text{(I.3)}$$

where $\|X\|_*$ is the sum of the singular values.

The analysis uses the centered operators $\mathcal{Q}_\Omega = p^{-1}\mathcal{P}_\Omega - \mathcal{I}$ and $\mathcal{Q}_T = \mathcal{P}_T - \rho'\mathcal{I}$, where $\rho = r/n$ and $\rho' = 2\rho-\rho^2$. It also uses the random matrices $(\mathcal{Q}_\Omega\mathcal{Q}_T)^k\mathcal{Q}_\Omega(E)$, where the operator is applied to $E$ from the right. $\|\cdot\|$ denotes the spectral norm.

Formalization targets

Goal: Theorem 1.2 (Matrix Completion II)

There is an absolute constant $C>0$ such that, for every fixed $M$ as above and $m \le n^2$ uniformly sampled entries,

$$m \ge C\mu^2 nr\log^6 n \implies \Pr\bigl[M \text{ is the unique solution of (I.3)}\bigr] \ge 1 - n^{-3}.$$

The constant $C$ is not fixed; the goal asserts only its existence.

Milestones (in attack order)

1. Lemma 3.1. A dual certificate $Y$ with $\mathcal{P}_\Omega(Y)=Y$, $\mathcal{P}_T(Y)=E$, $\|\mathcal{P}_{T^\perp}(Y)\|<1$, together with injectivity of $\mathcal{P}_\Omega$ on $T$, implies unique recovery. This is already proved on the platform.
2. Theorem 3.2 (Rudelson selection estimate). With probability at least $1-3n^{-\beta}$,

$$p^{-1}\|\mathcal{P}_T\mathcal{P}_\Omega\mathcal{P}_T - p\mathcal{P}_T\| \le C_R\sqrt{\mu_0nr\beta\log n/m},$$

provided the right-hand side is below $1$. 3. Lemma 8.1. An exact expansion of $(\mathcal{Q}_\Omega\mathcal{P}_T)^k\mathcal{Q}_\Omega$ in powers of $\mathcal{Q}_\Omega\mathcal{Q}_T$ with explicit recursive coefficients. 4. Lemma 8.2. The coefficients are at most $\lambda^{\lceil (k-j)/2\rceil}4^k$, with $\lambda = \rho'/p$. 5. Lemma 3.3. On the event $\|(\mathcal{Q}_\Omega\mathcal{Q}_T)^k\mathcal{Q}_\Omega(E)\| \le \sigma^{(k+1)/2}$, the same terms with $\mathcal{P}_T$ obey the bound with an extra factor $1+4^{k+1}$. 6. Theorem 3.6 (Moment bound II). Let $A = (\mathcal{Q}_\Omega\mathcal{Q}_T)^k\mathcal{Q}_\Omega(E)$ and $r_\mu = \mu^2 r$. Then

$$\mathbb{E}\operatorname{trace}\bigl((A^*A)^j\bigr) \le n\bigl(C(j(k+1))^6nr_\mu/m\bigr)^{j(k+1)}.$$

7. Corollary 3.7. Under (I.12), with probability at least $1-n^{-3}$ the certificate (III.10) exists and has $\|\mathcal{P}_{T^\perp}(Y)\|\le 1/2$.

Significance

Theorem 1.2 shows that a polynomial-time convex program recovers an incoherent low-rank matrix from a number of entries that is linear in $nr$ and within a polylogarithmic factor of what any method requires. It turned nuclear-norm minimization from a heuristic into a method with near-optimal guarantees, and much of the later work on low-rank recovery, robust PCA and phase retrieval uses its framework of dual certificates, tangent spaces and incoherence.

The theorem is proved; formalizing it is the remaining work here. None of these results has a machine-checked proof. The platform already has the Candès–Recht definitions (nuclear norm, SVD data, Bernoulli model, tangent projection), the deterministic Lemma 3.1, and the Bernoulli-to-uniform transfer. This mission adds:

• the trace-moment bound, which is the combinatorial core of the paper;
• the deterministic operator algebra of Appendix A;
• the assembly into the main theorem.

Shorter later proofs (Gross, Recht) use a different incoherence condition. A formal proof of the goal along either route is welcome, provided it proves the statement as given.

Difficulty

The obvious approach bounds each term $\|(\mathcal{Q}_\Omega\mathcal{P}_T)^k\mathcal{Q}_\Omega(E)\|$ of the Neumann series for the certificate separately, using noncommutative Khintchine inequalities and decoupling. This is what Candès and Recht did, and it fails beyond small $k$: the entries of these matrices are coupled through the same random indicators, and the bounds degrade with $k$. That is where their $n^{6/5}$ comes from.

The moment method avoids this but has its own obstruction. Taking absolute values inside the expansion of $\mathbb{E}\operatorname{trace}(A^*A)^j$ loses a factor of $r$, which gives the quadratic dependence of Theorem 1.1. The linear bound needs sign cancellations among the coefficients of $\mathcal{Q}_T$ to be tracked through a nested induction over "generalized spider" configurations (Section VI). Replacing $\mathcal{P}_T$ by $\mathcal{Q}_T$ (Lemma 3.3) is necessary for those cancellations. Without it the diagonal coefficients are of size $r/n$ instead of $\sqrt r/n$.

Formalization scope

• Objects. Matrices are Matrix (Fin n) (Fin n) ℝ (MatrixCompletion.RealMatrix). The SVD is the platform structure SVD M r. Logarithms are natural. Probabilities are the platform's finite sums: successProb (uniform $m$-subsets), bernoulliEventProb and bernoulliExpectation. The spectral norm is spectralNorm. The definitions of matrix_completion_{basic,svd,bernoulli,tangent} are reused, not restated.
• Square case. Theorem 1.2 is printed "under the same hypotheses as in Theorem 1.1", for $n_1\times n_2$ matrices. The paper proves only $n_1=n_2=n$ (Section I-H), and the goal and milestones 3–7 are square. Theorem 3.2 is quoted from Candès–Recht and is stated rectangular, as printed.
• Rank. "The same hypotheses" is read as the matrix hypotheses (fixed $M$, strong incoherence, uniform sampling), not as $r = O(1)$: (I.12) carries $r$, the paper calls the result general and nonasymptotic, and Section VI never uses bounded rank. The goal holds for every $r$.
• Constants. Every "numerical constant" ($C$, $C_R$, $c_0$) and every $O(\cdot)$ is an existential absolute constant quantified before all other variables. The goal's $C$ absorbs the standing assumptions $n \ge C'$ and $m\ge 2nr$. Where a milestone needs (I.22), $2nr\le m$ is an explicit hypothesis, and $m\le n^2$ is explicit wherever a probability or $p\le 1$ appears.
• Correction of Theorem 3.6. The printed bound (III.27) omits the factor $n$ and the $O(1)^{j(k+1)}$ constant of the paper's own final display (p. 2070), and as printed it is false: for $k=0$, $j=1$ and a flat rank-one matrix, the left side exceeds the right by the factor $n(1-p)$. The formal statement is the bound the paper derives, $n\,(C(j(k+1))^6nr_\mu/m)^{j(k+1)}$, under $nr_\mu\le m$, which that derivation uses and which (I.12) implies. The milestone text is kept verbatim.
• Deterministic lemmas. Lemmas 3.3, 8.1 and 8.2 hold for every fixed $\Omega$. The event (III.18) is a hypothesis, not a probability.
• Certificate. $Y$ of (III.10) exists only when $\mathcal{P}_\Omega$ is injective on $T$, so Corollary 3.7's event includes injectivity. $Y$ is characterized as the minimum-Frobenius-norm solution of $\mathcal{P}_\Omega(Y)=Y$, $\mathcal{P}_T(Y)=E$ (p. 2061).
• Ruling out trivialization. The hypothesis $m\le n^2$ is there only because successProb is $0$ for $m>n^2$; it does not exclude any case the paper covers. The failure probability stays $n^{-3}$ and is not traded for a constant. The constant $C$ may not depend on $n$, $r$, $\mu$ or $M$, so it cannot be chosen to make (I.12) unsatisfiable. For fixed $C$, (I.12) is satisfiable with $m \le n^2$ for every large $n$ and every $r \le n/(C\mu^2\log^6 n)$.
• Not covered. Proposition 6.1 (the summand bound on generalized spiders) is the heart of Theorem 3.6. It needs the admissible-quadruplet combinatorics of Sections IV–VI as definitions, and is left to solvers as a lemma of their own. Contributions formalizing Sections IV–VI (the moment expansion (IV.10), admissible pairs, the cancellation identities (VI.1)–(VI.4)) are welcome and reusable for mission I of this series.

Selected references

• E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Trans. Inf. Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
• E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9:717–772, 2009. https://arxiv.org/abs/0805.4471
• R. H. Keshavan, A. Montanari and S. Oh, Matrix Completion from a Few Entries, IEEE Trans. Inf. Theory 56(6):2980–2998, 2010. https://arxiv.org/abs/0901.3150
• D. Gross, Recovering Low-Rank Matrices from Few Coefficients in Any Basis, IEEE Trans. Inf. Theory 57(3):1548–1566, 2011. https://arxiv.org/abs/0910.1879
• B. Recht, A Simpler Approach to Matrix Completion, J. Mach. Learn. Res. 12:3413–3430, 2011. https://arxiv.org/abs/0910.0651