Statistics

Motivation

Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order $\sqrt{1/n}$ whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order $\sqrt{\mathbb V Z/n} + 1/n$, but the variance $\mathbb V Z$ is unknown, so the bound cannot be evaluated from data.

Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger $1/n$ term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).

Setting

For a vector $x = (x_1,\dots,x_n)$ of reals, the sample mean and sample variance are

$$P_n(x) = \frac1n\sum_{i=1}^n x_i, \qquad V_n(x) = \frac{1}{n(n-1)}\sum_{i,j=1}^n\frac{(x_i-x_j)^2}{2}.$$

Let $\mu$ be a probability distribution on a set $\mathcal X$, and $\mathcal F$ a class of hypotheses (loss functions) $f:\mathcal X\to[0,1]$. For $f\in\mathcal F$, its risk is $P(f,\mu) = \mathbb E f(X)$ and its variance is $V(f,\mu)=\mathbb V f(X)$, with $X\sim\mu$. For a sample $\mathbf X = (X_1,\dots,X_n)\sim\mu^n$, $P_n(f,\mathbf X)$ and $V_n(f,\mathbf X)$ are $P_n$ and $V_n$ of the vector $(f(X_1),\dots,f(X_n))$.

The complexity of $\mathcal F$ enters through the growth function. For $x\in\mathcal X^m$ let $\mathcal F(x) = \{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}\subseteq\mathbb R^m$, and let $\mathcal N(\epsilon, A, \|\cdot\|_\infty)$ be the least number of sup-norm $\epsilon$-balls centred in $A$ that cover $A$. Then

$$\mathcal N_\infty(\epsilon,\mathcal F,m) = \sup_{x\in\mathcal X^m}\mathcal N(\epsilon,\mathcal F(x),\|\cdot\|_\infty), \qquad \mathcal M(n) = 10\,\mathcal N_\infty(1/n,\mathcal F,2n).$$

For $\lambda\ge0$, sample variance penalization selects

$$SVP_\lambda(\mathbf X) = \arg\min_{f\in\mathcal F}\; P_n(f,\mathbf X) + \lambda\sqrt{\frac{V_n(f,\mathbf X)}{n}}.$$

With $\lambda = 0$ it is empirical risk minimization.

Formalization targets

Goal: Theorem 15 (p. 6)

Fix $\delta\in(0,1)$, $n\ge2$, $\lambda = \sqrt{18\ln(3\mathcal M(n)/\delta)}$ and any $f^*\in\mathcal F$. With probability at least $1-\delta$ in $\mathbf X\sim\mu^n$,

$$P(SVP_\lambda(\mathbf X),\mu) - P(f^*,\mu) \le \sqrt{\frac{32\,V(f^*,\mu)\ln(3\mathcal M(n)/\delta)}{n}} + \frac{22\ln(3\mathcal M(n)/\delta)}{n-1}.$$

The constants are the paper's. The goal is stated for an arbitrary comparator $f^*$, so it covers an optimal one when one exists.

Milestones

In the order of the proof:

• the fourth-moment inequality (Lemma 8, Corollary 9);
• the self-bounding concentration inequality the paper cites (Theorem 7, lower and upper tails);
• the tails (5)–(6) of the sample variance and the standard-deviation bounds of Theorem 10;
• the comparison $W\le\mathbb EV_n$ of (7)–(9);
• Bennett's inequality for independent variables, together with the i.i.d. Theorem 3;
• the empirical Bernstein bounds (Theorem 4 for i.i.d. variables, Theorem 11 for independent ones);
• the Lipschitz properties of the confidence functionals $\Phi,\Psi$ (Lemma 12);
• the symmetrization lemma (Lemma 13) and the swap bound (Lemma 14);
• the uniform bound, Theorem 6:

$$\Pr\Big\{\exists f\in\mathcal F:\ P(f,\mu)-P_n(f,\mathbf X) > \sqrt{\tfrac{18V_n(f,\mathbf X)\ln(\mathcal M(n)/\delta)}{n}} + \tfrac{15\ln(\mathcal M(n)/\delta)}{n-1}\Big\}\le\delta \quad (n\ge16).$$

Significance

Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as $\ln\mathcal M(n)/n$; for a finite class $\mathcal M(n)$ does not depend on $n$ and the rate is $1/n$. The paper gives a two-hypothesis example where empirical risk minimization cannot beat order $1/\sqrt n$ (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.

All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a $1/n$-normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.

Difficulty

Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for $V_n$ itself with the right dependence on $\mathbb EV_n$, and $V_n$ is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.

The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.

Formalization scope

Conventions:

• The source is arXiv:0907.3740v1. It has no printed page numbers, so every page cited is the PDF page.
• Indices $i=1,\dots,n$ are i : Fin n.
• A sample is a vector Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in $[0,1]$" have laws giving zero mass outside $[0,1]$.
• "With probability at least $1-\delta$, $A$" is written as $\mu^n\{\neg A\}\le\delta$. For a set that is not measurable this is the outer measure.
• $P_n$ is the published VarianceRegularization.Expansion.empMean. $V_n$ is a local sampleVar with the $1/(n(n-1))$ normalization. $V(f,\mu)$ is Mathlib's variance.
• The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in the set, values in $\mathbb N\cup\{\infty\}$).
• $\Pr_\sigma$ and $\mathbb E_\sigma$ are uniform averages over the $2^n$ sign vectors.
• $SVP_\lambda$ is an arbitrary selector that returns, for every sample, a minimizer in $\mathcal F$ of the penalized objective. Every minimizer is covered.

Added hypotheses and repaired statements, each disclosed in the item:

• The paper says "questions of measurability will be ignored throughout". This is made precise as follows:
  • Theorems 6 and 15: $\mathcal F$ is countable and its members are measurable.
  • Lemma 13: the function is measurable.
  • Theorem 7: $Z$ is measurable, integrable and nonnegative, and its coordinate-wise infima are measurable.
• Theorems 6 and 15 assume $\mathcal N_\infty(1/n,\mathcal F,2n)<\infty$. With an infinite value the printed bound is vacuous.
• Theorems 4 and 11 and Lemmas 12 and 14 add $n\ge2$. Theorem 3 and Bennett's display add $n\ge1$. Without these, Lean's convention $1/0=0$ makes the printed formulas false at the excluded $n$.
• Corollary 9's "set" $\{x_1,\dots,x_n\}$ is read as a list, so repetitions are allowed.

Ruled-out trivializations:

• SVP is not defined as the comparator $f^*$.
• $\lambda$ is pinned to $\sqrt{18\ln(3\mathcal M(n)/\delta)}$.
• $V_n$ is the sample variance, not the true variance.
• No measurability of the bad event or of the selector is assumed.

A complete development needs the following:

• the entropy method for self-bounding functions (Theorem 7);
• Bennett's inequality for independent non-identical bounded variables;
• product-measure symmetrization;
• covering-number bookkeeping.

The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.

Selected references

• A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009; arXiv:0907.3740v1, 2009. https://arxiv.org/abs/0907.3740
• A. Maurer, Concentration inequalities for functions of independent variables, Random Structures & Algorithms 29, 121–138, 2006. https://doi.org/10.1002/rsa.20105
• C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998.
• J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation trade-off using variance estimates in multi-armed bandits, Theoretical Computer Science 410(19), 2009. https://doi.org/10.1016/j.tcs.2009.01.016
• V. Mnih, Cs. Szepesvári, J.-Y. Audibert, Empirical Bernstein stopping, ICML 2008. https://doi.org/10.1145/1390156.1390241
• W. Hoeffding, Probability inequalities for sums of bounded random variables, JASA 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
• H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017; arXiv:1610.02581. https://arxiv.org/abs/1610.02581

Minimum discrimination information under moment constraints

Given a reference probability distribution $R$ and a set $\mathcal E$ of probability distributions, the minimum discrimination information problem asks for the member of $\mathcal E$ closest to $R$ in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations $\int f_i\,dP = a_i$, and the classical answer is that the minimizer is an exponential family member, with density $c\exp\sum_i t_i f_i$ with respect to $R$.

That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the $f_i$.

Timeline:

• 1959: Kullback formulates the minimum discrimination information theorem: an element of $\mathcal E$ of exponential form is the minimizer (a sufficient condition).
• 1966: Kullback and Khairat (Ann. Math. Statist. 37, 1966) refine the sufficient condition.
• 1972: Čencov proves existence of exponential-form minimizers under general conditions (Statistical Decision Rules and Optimal Inference, Theorem 23.1).
• 1975: Csiszár proves Theorem 3.3 by the minimizing-sequence method of his Theorem 2.1; a first version of the paper assumed $T_R = E^k$, weakened to "$T_R$ open" after Čencov's work.

Setting

All distributions (PD's) live on one measurable space $(X,\mathcal X)$. The I-divergence of $P$ from $Q$ is

$$I(P\|Q)=\int \log p_Q\,dP\ \text{ if } P\ll Q,\qquad I(P\|Q)=+\infty\ \text{ otherwise},$$

where $p_Q$ is the density of $P$ with respect to $Q$; it takes values in $[0,\infty]$ and vanishes only for $P=Q$. The variation distance is $|P-Q|=\int|p_R-q_R|\,dR$ for any PD $R$ dominating both. If $\mathcal E$ is a convex set of PD's containing some $P$ with $I(P\|R)<\infty$, a $Q\in\mathcal E$ with

$$I(Q\|R)=\min_{P\in\mathcal E} I(P\|R)$$

is the I-projection of $R$ on $\mathcal E$.

Fix real-valued measurable functions $f_1,\dots,f_k$ on $X$. For $a=(a_1,\dots,a_k)\in E^k$ (Euclidean $k$-space) the moment set $\mathcal E(a)$ is the set of PD's $P$ with $\int f_i\,dP=a_i$, $i=1,\dots,k$. Further:

• $A_R$ is the set of $a\in E^k$ for which $\mathcal E(a)$ contains some $P$ with $I(P\|R)<\infty$;
• $T_R=\{t\in E^k:\ \exp\sum_i t_i f_i \text{ is } R\text{-integrable}\}$, (3.16);
• $F(a)=\inf_{P\in\mathcal E(a)} I(P\|R)$, (3.18), the optimal value as a function of the constraint levels.

Formalization targets

Goal: Theorem 3.3

If $T_R$ is open in $E^k$, then for every point $a$ of the interior of $A_R$ the I-projection $Q$ of $R$ on $\mathcal E(a)$ exists and

$$q_R(x)=c\exp\sum_{i=1}^k t_i f_i(x)\qquad R\text{-a.e.},$$

for some constant $c$ and some $t\in E^k$.

Milestones

1. (2.2), the parallelogram identity: $I(P_m\|R)+I(P_n\|R)=2I(\tfrac{P_m+P_n}2\|R)+I(P_m\|\tfrac{P_m+P_n}2)+I(P_n\|\tfrac{P_m+P_n}2)$.
2. (2.4): a minimizing sequence $P_n$ in a convex set converges in variation to a PD $Q\ll R$ (closedness of the set is not used).
3. Lemma 3.1: if $e^{tf}$ is $Q$-integrable for small $|t|$, then $I(P_n\|Q)\to0$ implies $\int f\,dP_n\to\int f\,dQ$.
4. (3.18): $A_R$ is convex and $F$ is finite and convex on $A_R$.
5. (3.19): at an interior point $a$ of $A_R$ there is $t$ with $F(b)\ge F(a)+\sum_i t_i(b_i-a_i)$ for all $b\in A_R$.
6. Remark, p. 158: $F$ is differentiable at interior points of $A_R$, and $\operatorname{grad}F(a)=t$, the parameter vector of the I-projection.

Significance

Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.

The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).

Difficulty

The obvious argument fails at the first step: the moment set $\mathcal E(a)$ is convex but not closed in variation when the $f_i$ are unbounded, since $\int f_i\,dP$ is not continuous in variation. A minimizing sequence therefore converges in variation to some $Q$ (as in Theorem 2.1), but nothing places $Q$ in $\mathcal E(a)$: mass can escape to where $|f_i|$ is large. Ruling this out needs quantitative control of $I(P_n\|Q)$, which in turn requires knowing the form of $Q$ before knowing $Q$ is feasible; the interplay with the convexity of $F$ and the openness of $T_R$ is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.

Formalization scope

• Probability distributions are Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions $\log 0=-\infty$, $\log\frac a0=+\infty$, $0\cdot(\pm\infty)=0$.
• The variation distance uses $P+Q$ as dominating measure (the page allows any dominating PD; the value is the same).
• The I-projection carries $I(Q\|R)<\infty$ explicitly: the page defines it only when $\mathcal E$ meets $\{P: I(P\|R)<\infty\}$.
• $\mathcal E(a)$ requires $P$-integrability of every $f_i$, so the constraint integrals are genuine. $E^k$ is Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. $k=0$ is allowed.
• $F$ is an infimum in $[0,\infty]$ (equal to $\infty$ outside $A_R$); statements use its real value only on $A_R$, where it is finite. (3.18) prints $I(P\|Q)$; the reference measure is $R$, as the definition of $A_R$ and the proof show. (3.16) prints $(t_1,\dots,t_n)$ for $(t_1,\dots,t_k)$.
• Densities are Radon–Nikodym derivatives and the form (3.2) is an $R$-almost-everywhere identity with no exceptional set of positive measure.
• Lemma 3.1 asserts that $f$ is $P_n$-integrable for large $n$ as well as the convergence, so that $\int f\,dP_n$ is not a default value.
• Trivializing readings are excluded: the goal asserts existence of the I-projection rather than assuming it, $T_R$ is an integrability set (not a set where a junk integral is finite), and the infimum is never a real sInf over a possibly empty set.

A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) $I(P\|R)-I(P\|Q)=\int\log q_R\,dP$), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.

Selected references

• I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probab. 3(1), 146–158, 1975. https://doi.org/10.1214/aop/1176996454
• S. Kullback, Information Theory and Statistics, Wiley, 1959.
• S. Kullback and M. A. Khairat, A note on minimum discrimination information, Ann. Math. Statist. 37, 279–280, 1966.
• E. T. Jaynes, Information theory and statistical mechanics, Phys. Rev. 106, 620–630, 1957. https://doi.org/10.1103/PhysRev.106.620
• N. N. Čencov, Statistical Decision Rules and Optimal Inference (Russian), Nauka, 1972; English translation, American Mathematical Society, 1982.
• I. N. Sanov, On the probability of large deviations of random variables (Russian), Mat. Sbornik 42, 11–44, 1957.

Motivation

In 1952 Herbert Robbins asked how a statistician should draw a sample sequentially from two populations when the goal is the largest possible expected total, not a test or an estimate after the fact (Robbins 1952). This is the problem now called the two-armed bandit, and Robbins' paper is the usual starting point of the multi-armed bandit literature that underlies clinical-trial allocation, adaptive experimentation and online recommendation (Lattimore and Szepesvári 2020).

Robbins illustrated the problem with two coins. His first concrete rule, "stay on heads, switch on tails" (later known as win-stay, lose-shift or play the winner), uses only the outcome of the last toss, yet its long-run loss relative to an observer who knows the better coin is at most $3-2^{3/2}\approx 0.172$ per toss, against $1/2$ for a rule that ignores the outcomes. The same rule was studied again in clinical-trial design as "play the winner" (Zelen 1969).

Timeline. 1952: Robbins computes the operating characteristics of the stay-or-switch rule $R_1$ and of the outcome-blind rule $R_0$ for two coins, and shows that a greedy rule with sparse forced sampling attains $\max(\alpha,\beta)$ for arbitrary populations with finite means (Section 2). 1969: Zelen proposes the play-the-winner rule for clinical trials. 1985: Lai and Robbins give the logarithmic lower bound on regret and rules that attain it (Lai and Robbins 1985).

Setting

Two coins $A$ and $B$ have unknown head probabilities $\alpha$ and $\beta$, with $0\le\alpha,\beta\le1$. A head pays \1$, a tail pays nothing. If$x_i\in{0,1}$is the payoff of the$i$-th toss,$S_n=x_1+\dots+x_n$is the total received after$n$tosses. In the formal development the pair of coins is a **two-armed stochastic bandit**: arm$0$is coin$A$, with payoff law$(1-\alpha)\delta_0+\alpha\delta_1$, and arm$1$is coin$B$, with payoff law$(1-\beta)\delta_0+\beta\delta_1$.

A sampling rule chooses the coin for each toss from the outcomes of the earlier tosses. Two rules are studied.

• Rule $R_1$. For the first toss choose $A$ or $B$ at random. Then, for $i=1,2,\dots$, if the $i$-th toss results in heads, use the same coin for the $(i+1)$-th toss; if it results in tails, switch to the other coin.
• Rule $R_0$. Choose one of the two coins at random and then use it for every toss.

Write $p_i$ for the probability of heads on the $i$-th toss under the rule in use, and $\mathrm E(S_n/n)$ for the expected average payoff of the first $n$ tosses. The paper's two parameters are

$$\gamma=\frac{\alpha+\beta}{2},\qquad \delta=\frac{|\alpha-\beta|}{2},$$

so that $\max(\alpha,\beta)=\gamma+\delta$ is the expected payoff per toss of an observer who knows the better coin. Following the paper, $\alpha$ and $\beta$ are assumed not both $0$ and not both $1$; then $|\alpha+\beta-1|<1$.

Formalization targets

Goal: the asymptotic loss of $R_1$ and its maximum

Under $R_1$,

$$\lim_{n\to\infty}\mathrm E\!\left(\frac{S_n}{n}\right)=\gamma+\frac{\delta^2}{1-\gamma}, \qquad L(A,B,R_1)=\lim_{n\to\infty}\left[\max(\alpha,\beta)-\mathrm E\!\left(\frac{S_n}{n}\right)\right]=\delta\left[1-\frac{\delta}{1-\gamma}\right],$$

and for every admissible pair of coins

$$0\le L(A,B,R_1)\le M_1=3-2^{3/2},$$

with equality at $\alpha=0,\ \beta=2-2^{1/2}$ and at $\alpha=2-2^{1/2},\ \beta=0$ (Eqs. (6), (8) and the text after (8), p. 531).

Milestones, in the order of the argument

1. Eq. (2): $p_{i+1}=(\alpha+\beta-1)p_i+(\alpha+\beta-2\alpha\beta)$ for $i\ge1$.
2. Eq. (3): the closed form $p_i=(\alpha+\beta-1)^{i-1}\bigl[p_1-c\bigr]+c$ with $c=(\alpha+\beta-2\alpha\beta)/(2-(\alpha+\beta))$.
3. Eqs. (4)–(5): $\lim_i p_i=c=\gamma+\delta^2/(1-\gamma)$.
4. Eq. (6): both $\mathrm E(S_n/n)$ and $(p_1+\dots+p_n)/n$ have the stated limit.
5. Eqs. (7)–(8) and $M_1$: $\max(\alpha,\beta)=\gamma+\delta$ and $0\le\delta[1-\delta/(1-\gamma)]\le 3-2^{3/2}$, with the two maximizers.
6. Rule $R_0$: $L(A,B,R_0)=\delta$, whose maximum over the admissible pairs is $M_0=1/2$, at $(0,1)$ and $(1,0)$.

Significance

The result. The goal quantifies how much an extremely simple adaptive rule recovers. A rule blind to outcomes loses up to half a dollar per toss; one bit of memory cuts the worst case to about $0.172$. Robbins used this comparison to argue that the sequential design problem has nontrivial, computable answers, and to motivate the forced-sampling rule $\bar R$ of the same section, whose loss tends to $0$. The closed forms (3)–(6) are the exact operating characteristics of the four-state Markov chain $(\text{coin},\text{outcome})$ that $R_1$ generates.

Formalizing it. The results are classical and elementary on paper, but none of them has a machine-checked proof. The mission produces a verified chain from the canonical bandit measure to an explicit long-run payoff: the head probability of a fixed toss is computed from the law of the whole trajectory, the recursion is derived from the rule's kernels, and the Cesàro limit closes the argument. The same pattern applies to any finite-memory bandit rule, and the coin bandit and the two rules are reusable test cases for the platform's bandit library. No platform theorem states $R_1$, its recursion or its loss; other two-state models on the platform (a Markov-renewal gain rate, an MDP gadget) are different objects.

Difficulty

The recursion (2) is a statement about the trajectory law, not about a Markov chain given in advance: the chain $(\text{coin}_i,x_i)$ has to be extracted from the Ionescu–Tulcea construction of the bandit measure, where the coin of toss $i+1$ is a deterministic function of toss $i$ and the payoff is drawn from the chosen coin's law. The head probability alone is not a Markov chain: $p_{i+1}$ depends on the joint law of coin and outcome at toss $i$, so a naive one-step argument on $p_i$ does not apply, and the affine form of (2) is a property of this particular rule. The maximization in (8) is over a two-dimensional region whose maximizers lie on the boundary $\alpha=0$ or $\beta=0$, and the excluded corners are exactly where the formula $\delta/(1-\gamma)$ breaks down.

Formalization scope

The bandit is the published BanditAlgorithm.StochasticBandit 2; the rules are policies of the published type BanditPolicy 2, and probabilities and expectations are taken under the published infinite-horizon measure banditTrajMeasure, whose coordinate $t$ is toss $t+1$. Head probabilities are elements of unitInterval. The conventions committed to are:

• "At random" for the first coin of $R_1$ and $R_0$ is the fair choice, probability $1/2$ each.
• Heads is the payoff value $1$; $p_i$ is defined for $i\ge1$ and every statement quantifies over $i\ge1$ or $n\ge1$.
• "Not both $0$ or both $1$" is the hypothesis $\neg(\alpha=0\wedge\beta=0)\wedge\neg(\alpha=1\wedge\beta=1)$, never $0<\alpha$ or $\alpha<1$, which would remove the maximizer $\alpha=0$. Robbins states it immediately before Eq. (2), and the Lean carries it through the probability and loss results.
• The paper's "$\lim E(S_n/n)=\lim (p_1+\dots+p_n)/n$" is stated as convergence of both sequences to the same value.
• "$L(A,B,R_1)$ has its maximum value $M_1$ when …" is read as: $L\le M_1$ for every admissible $(\alpha,\beta)$, and $L=M_1$ at both named points ("or vice versa").
• $2^{3/2}$ is written $2\sqrt2$. The numerical asides ($\approx .172$, $\approx .586$, "17.2 cents") are not formalized, nor is the "tossing the two coins alternately" variant of $R_0$.

The asymptotic loss is stated as the limit of $\max(\alpha,\beta)-\mathrm E(S_n/n)$; defining $L$ by its closed form would make the goal a tautology. Likewise, the head probabilities are computed from the law of the rule on the coins: positing a sequence that satisfies (2) would drop the probabilistic content.

A complete development needs: the one-dimensional marginals of banditTrajMeasure (the law of coordinate $t+1$ given the prefix), the joint law of (coin, payoff) at each toss, linearity of expectation for bounded payoffs, a Cesàro-mean lemma, and a short two-variable optimization. The trajectory-marginal lemmas are reusable for every bandit mission on the platform; contributions that prove them in general are welcome.

Selected references

• H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58(5) (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
• M. Zelen, Play the winner rule and the controlled clinical trial, J. Amer. Statist. Assoc. 64 (1969), 131–146. https://doi.org/10.1080/01621459.1969.10500959
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6 (1985), 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401