Probability

Motivation

The conditional logit model is the workhorse of discrete choice analysis in econometrics, transportation planning, marketing and revenue management. An individual facing a finite set of alternatives picks alternative $i$ with probability proportional to $e^{z_i\theta}$, where $z_i$ is a vector of observed attributes and $\theta$ an unknown parameter vector. Daniel McFadden's 1974 chapter, Conditional Logit Analysis of Qualitative Choice Behavior, derived this model from a theory of random utility maximization and set out how to estimate $\theta$ by maximum likelihood. McFadden received the 2000 Nobel Memorial Prize in Economic Sciences for his development of theory and methods for analyzing discrete choice.

Every confidence interval and hypothesis test computed from a fitted logit model rests on the large-sample theory in §III of that chapter: the maximum likelihood estimator exists with probability tending to one, converges to the true parameter, and is approximately normal with covariance given by the inverse information matrix. This mission formalizes that theory, Lemmas 5 and 6 of the paper, as proved in its Appendix.

Setting

Observations are indexed serially, $m = 0, 1, 2, \dots$, as in the paper's Appendix ("Let m be a serial index of trials and repetitions"). Observation $m$ offers $J_m \ge 1$ alternatives, and alternative $i$ carries a vector $z_{im} \in \mathbb R^K$ of independent variables. For a parameter $\theta \in \mathbb R^K$ the selection probabilities are

$$P_{im}(\theta) = \frac{e^{z_{im}\theta}}{\sum_{j=1}^{J_m} e^{z_{jm}\theta}}, \qquad \bar z_m(\theta) = \sum_{i} P_{im}(\theta)\, z_{im}.$$

The data are generated at a true parameter $\theta^0$: the chosen alternatives $Y_0, Y_1, \dots$ are independent random variables with $\Pr(Y_m = i) = P_{im}(\theta^0)$. The log-likelihood of the first $q$ observations is $L^q(\theta) = \sum_{m<q}\log P_{Y_m m}(\theta)$. The moment matrix of observation $m$ is

$$\Omega_m = \sum_{i} P_{im}(\theta^0)\,(z_{im}-\bar z_m)(z_{im}-\bar z_m)', \qquad \bar z_m = \bar z_m(\theta^0).$$

Axiom 7 asks that $J_m \le J_*$ and $|z_{im}| \le M$ uniformly, and that $\frac1q\sum_{m<q}\Omega_m$ converge to a positive definite matrix $\Omega$. Axiom 6, for a given sample, asks that no nonzero $\gamma$ satisfy $(z_{jm} - z_{Y_m m})\gamma \le 0$ for all observed $m$ and all $j$. A maximum likelihood estimator $\hat\theta^q$ is a measurable choice of a maximizer of $L^q$, wherever one exists.

Formalization targets

Goal: Lemma 6

$$\hat\theta^q \xrightarrow{\Pr} \theta^0 \quad\text{and}\quad \sqrt q\,\Omega^{1/2}(\hat\theta^q - \theta^0) \xrightarrow{d} N(0, I_K) \qquad (q \to \infty).$$

Milestones

1. Axiom 7 implies Axiom 5 (the full-rank condition) in all sufficiently large samples.
2. Equation (42): $P_{im}(\theta) \ge 1/(J_* e^{2M|\theta|})$.
3. Lemma 5: $\Pr(\text{Axiom 6 holds and } L^q \text{ attains its maximum}) \to 1$.
4. Equation (43): the first three derivatives of $\log P_{im}$ are bounded by $2M$, $4M^2$, $8M^3$.
5. Equation (46): each score $\nabla\log P_{Y_m m}(\theta^0)$ has mean zero.
6. Equation (47): each expected Hessian equals $-\Omega_m$.
7. Consistency of $\hat\theta^q$.
8. Equation (58): $q^{-1/2}\,\Omega^{-1/2}\sum_{m<q}\nabla\log P_{Y_m m}(\theta^0) \xrightarrow{d} N(0, I_K)$.

Significance

The result. Lemma 6 is what licenses reading $\hat\theta^q$ as approximately $N(\theta^0, q^{-1}\Omega^{-1})$, so that the diagonal of the inverse information matrix estimates the sampling variances and $q(\hat\theta^q-\theta^0)'\Omega(\hat\theta^q-\theta^0)$ is asymptotically $\chi^2_K$. Lemma 5 complements it: in finite samples the likelihood can fail to have a maximum (the observations are then "explained" by a direction $\gamma$ of Axiom 6), and the lemma shows this failure is asymptotically negligible. The data are not identically distributed (each observation has its own alternatives), so the result is not an instance of the textbook i.i.d. maximum likelihood theorem.

Formalizing it. The results are proved in the paper, in outline. A machine-checked version adds: a complete proof of the existence part (Lemma 5), whose published argument is a sketch by induction over an infinite index set; a precise treatment of the estimator where no maximizer exists; the correction of two misprints in the published proof (the normalization $1/q$ in (58), which must be $1/\sqrt q$, and a constant in (51)); and a multivariate Lindeberg–Feller central limit theorem for bounded, independent, non-identically distributed vectors, which the proof invokes and which is reusable well beyond this paper. No machine-checked proof of these results is known.

Difficulty

The obvious route, "the log-likelihood is concave, so its maximizer converges", needs a maximizer to exist, and in a finite sample it may not; the estimator is defined only on an event whose probability must first be shown to tend to one. Consistency then needs a uniform law of large numbers for the gradient on a sphere around $\theta^0$, controlled by the third-derivative bound (43). Asymptotic normality needs a central limit theorem for independent but not identically distributed score vectors, with covariances $\Omega_m$ that converge only on average; the i.i.d. central limit theorem does not apply. Finally the random Hessian at an intermediate point must be shown to converge in probability, which ties the consistency result into the normality argument.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin K); $z\theta$ is the inner product, and all norms are Euclidean (footnote 11's sum-of-absolute-values norm is equivalent and gives the same qualitative axiom); derivative bounds use operator norms.
• The paper's $N$ trials with $R_n$ repetitions are the special case of the serial indexing in which consecutive observations repeat their data; the sample size $\sum_n R_n$ is $q$.
• Axiom 7's limit (27) is taken in its serial form (48), with $P$ evaluated at $\theta^0$.
• The estimator is any measurable selection that maximizes $L^q$ whenever $L^q$ has a maximum, and is unconstrained otherwise. Requiring a maximizer for every sample would be unsatisfiable, since Axiom 6 fails with positive probability, and would make the goal vacuous; this convention rules that out.
• Consistency is TendstoInMeasure. Asymptotic normality is TendstoInDistribution to a random vector whose law is stdGaussian. $\Omega^{1/2}$ is the positive semidefinite square root CFC.sqrt.
• Needed infrastructure: derivatives of log-sum-exp, a law of large numbers for bounded independent vectors, and a multivariate Lindeberg–Feller theorem. Mathlib provides the one-dimensional i.i.d. central limit theorem only. Contributions of these general results as separate theorems are welcome.

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966 (Lindeberg–Feller theorem, pp. 256–258).
• C. R. Rao, Linear Statistical Inference and Its Applications, Wiley (cited by McFadden as Rao (1968), pp. 347–351, for the asymptotic $\chi^2$ test).

Motivation

Neural-network classifiers can be made to change their output by perturbations of the input that are imperceptible to a person. A certified defense is a classifier together with a proof that its prediction at a point $x$ does not change for any perturbation $\delta$ in a stated set, typically an $\ell_2$ ball $\|\delta\|_2<R$. Randomized smoothing turns an arbitrary base classifier into one with such a certificate by classifying Gaussian-noised copies of the input and returning the most likely class. Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) gave the certified radius $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$ (their Theorem 1) and showed, in their Theorem 2, that this radius cannot be enlarged when only the two class-probability bounds are known about the base classifier. This mission formalizes Theorem 2. Theorem 1 is the subject of the companion mission of this series.

Earlier certificates for the same smoothed classifier, by Lecuyer et al. (2019) via differential privacy and Li et al. (2018) via Rényi divergence, gave smaller radii. Theorem 2 shows that no further analysis that uses only the class-probability bounds can improve on Theorem 1.

Setting

Inputs live in $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$; classes form a set $\mathcal Y$. A base classifier is a map $f:\mathbb R^d\to\mathcal Y$ with Borel decision regions. For a noise level $\sigma>0$, write $\mathcal N(x,\sigma^2I)$ for the isotropic Gaussian law of $x+\varepsilon$ with $\varepsilon\sim\mathcal N(0,\sigma^2I)$. The class probability of $c$ at $x$ is $\mathbb P(f(x+\varepsilon)=c)$, and the smoothed classifier is

$$g(x)=\arg\max_{c\in\mathcal Y}\ \mathbb P(f(x+\varepsilon)=c).$$

Let $\Phi$ be the standard Gaussian CDF and $\Phi^{-1}$ its inverse on $(0,1)$. A classifier $f$ is consistent with the observed class probabilities (6) for a top class $c_A$ and numbers $\underline{p_A}\ge\overline{p_B}$ if

$$\mathbb P(f(x+\varepsilon)=c_A)\ \ge\ \underline{p_A}\ \ge\ \overline{p_B}\ \ge\ \max_{c\ne c_A}\mathbb P(f(x+\varepsilon)=c).$$

The certified radius is $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$. In Lean these are gaussNoise x σ, classProb f σ x c, IsConsistent f σ x cA pA pB and radius σ pA pB in the namespace Cohen2019.Tight, with Phi and PhiInvReal from the series' shared module Cohen2019.Robust; the half-spaces $A=\{z:\delta^T(z-x)\le\sigma\|\delta\|\Phi^{-1}(\underline{p_A})\}$ and $B=\{z:\delta^T(z-x)\ge\sigma\|\delta\|\Phi^{-1}(1-\overline{p_B})\}$ of the paper's Appendix A are setA and setB.

Quotations write the paper's underlined lower bound as p̲A and its overlined upper bound as p̄B. The PDF has no printed page numbers; every page cited is the PDF page of arXiv:1902.02918v2.

Formalization targets

Goal: Theorem 2 (corrected)

Assume $0<\overline{p_B}\le\underline{p_A}<1$, $\underline{p_A}+\overline{p_B}\le1$, and that some finite set $s$ of classes other than $c_A$ satisfies $1\le\underline{p_A}+|s|\,\overline{p_B}$. Then for every $\delta$ with $\|\delta\|_2>R$ there is a base classifier $f^*$ consistent with (6) and a class $c\ne c_A$ with

$$\mathbb P(f^*(x+\delta+\varepsilon)=c_A)\ <\ \mathbb P(f^*(x+\delta+\varepsilon)=c),$$

so that $g(x+\delta)\ne c_A$ under any tie-breaking. The classifier may depend on $\delta$.

The class-capacity hypothesis is a correction. As printed, with only $\underline{p_A}+\overline{p_B}\le1$, the theorem fails for two classes: with $\mathcal Y=\{c_A,c_B\}$, $\underline{p_A}=0.6$, $\overline{p_B}=0.1$ and $\sigma=\|\delta\|_2=1$, one has $R\approx0.767<1$, yet every consistent $f$ gives $c_A$ probability at least $0.9$, and Theorem 1 then certifies radius $\Phi^{-1}(0.9)\approx1.28$.

Milestones

The milestones are the steps the paper itself states, in its order: the Claims $\mathbb P(X\in A)=\underline{p_A}$ and $\mathbb P(X\in B)=\overline{p_B}$ for $X\sim\mathcal N(x,\sigma^2I)$; the disjointness of $A$ and $B$ (corrected to "null" when $\underline{p_A}+\overline{p_B}=1$); equations (13) and (14) for $Y\sim\mathcal N(x+\delta,\sigma^2I)$,

$$\mathbb P(Y\in A)=\Phi\Big(\Phi^{-1}(\underline{p_A})-\tfrac{\|\delta\|}{\sigma}\Big),\qquad \mathbb P(Y\in B)=\Phi\Big(\Phi^{-1}(\overline{p_B})+\tfrac{\|\delta\|}{\sigma}\Big);$$

the equivalence $\mathbb P(Y\in A)<\mathbb P(Y\in B)\iff\|\delta\|_2>R$; and the existence of the worst-case classifier $f^*$ satisfying (6) with equalities.

Significance

Theorem 2 makes the guarantee of Theorem 1 exact: when only (6) is known about $f$, the set of perturbations under which the Gaussian-smoothed prediction is provably constant is exactly the open $\ell_2$ ball of radius $R$. It settles that improvements to Gaussian-smoothing certificates must use more information about the base classifier than the two bounds, as later work on higher-order and Lipschitz-based certificates does.

The paper's proof is complete in its main lines and has two gaps that this mission records and repairs: the printed statement omits a condition on the number of classes, and the claim $A\cap B=\emptyset$ fails at $\underline{p_A}+\overline{p_B}=1$. To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. Mathlib at the pinned revision has the multivariate standard Gaussian but no normal quantile function and no Gaussian half-space lemma; this mission adds statements for both kinds of fact.

Difficulty

Each step is elementary on paper but rests on facts about Gaussians that Mathlib does not package: the image of the standard Gaussian on $\mathbb R^d$ under a linear functional $z\mapsto\delta^T z$ is the one-dimensional Gaussian with variance $\|\delta\|^2$, and $\Phi$ is a continuous strictly increasing bijection $\mathbb R\to(0,1)$ with $\Phi^{-1}(1-p)=-\Phi^{-1}(p)$. The construction of $f^*$ has a further step the paper leaves informal: the region between $A$ and $B$, of mass $1-\underline{p_A}-\overline{p_B}$, must be shared among "other classes" with none exceeding $\overline{p_B}$, which is where the capacity hypothesis enters. Measurability of the constructed decision regions must be carried along.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $\mathcal N(x,\sigma^2I)$ is the pushforward of Mathlib's stdGaussian under $z\mapsto x+\sigma z$, with $\sigma>0$ a binder. $\Phi$ is cdf (gaussianReal 0 1); $\Phi^{-1}(p)$ is the generalized inverse $\inf\{t:p\le\Phi(t)\}$, which is the true inverse on $(0,1)$ and the junk value $0$ at the endpoints, so every statement that evaluates it assumes $0<p<1$; at $\overline{p_B}=0$ or $\underline{p_A}=1$ the paper's radius is infinite and Theorem 2 is vacuous. Class probabilities are real numbers. The base classifier in the conclusion is deterministic with Borel decision regions, which is the stronger existence statement. The conclusion is the strict inequality between class probabilities, not merely the failure of $c_A$ to be a strict unique argmax.

A formalization in which the junk endpoint value of $\Phi^{-1}$ makes $R$ negative, or in which the classifier's decision regions are non-measurable so that its class probabilities are default values, would make the goal trivial; the hypotheses above exclude both.

Reusable beyond this mission: the Gaussian half-space probabilities and the normal quantile on $(0,1)$. Contributions of general Mathlib-style lemmas (the law of $\delta^T X$ for $X\sim\mathcal N(x,\sigma^2I)$, properties of $\Phi^{-1}$) are welcome.

Selected references

• J. M. Cohen, E. Rosenfeld, J. Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML 2019; arXiv:1902.02918v2. https://arxiv.org/abs/1902.02918v2
• M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, S. Jana, Certified Robustness to Adversarial Examples with Differential Privacy, IEEE S&P 2019. https://arxiv.org/abs/1802.03471
• B. Li, C. Chen, W. Wang, L. Carin, Certified Adversarial Robustness with Additive Noise, NeurIPS 2019. https://arxiv.org/abs/1809.03113
• J. Neyman, E. S. Pearson, On the Problem of the Most Efficient Tests of Statistical Hypotheses, Phil. Trans. R. Soc. A 231, 1933. https://doi.org/10.1098/rsta.1933.0009

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$, each with a nonnegative value $v(e)$, and $K$ goods indexed in decreasing order of nonnegative weight:

$$w(1)\ge w(2)\ge\cdots\ge w(K)\ge0.$$

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$. Its value is $\sum_{k=1}^K v(s(k))w(k)$. Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$, chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$, assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$, the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$, observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$. A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$.

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$, which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$:

$$\mathrm{OPT}\le(8+3e)\,\mathbb E[A].$$

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$. Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class-$i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$, the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$. The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$. It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$. An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$, so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

• Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

Motivation

A martingale difference sequence is the standard model of a "fair" sequence of observations whose terms may depend on the past: each new term has conditional mean zero given everything observed before it. Laws of large numbers for such sequences underlie the analysis of stochastic approximation, sequential estimation and online learning, where the noise terms are dependent but conditionally centred.

Classical strong laws concern averages in which every observation keeps the same weight as the sample grows. Kazuoki Azuma's 1967 paper Weighted sums of certain dependent random variables (Tôhoku Math. J. 19) studies weighted sums of dependent variables, and is best known for the exponential moment bound that is now called the Azuma inequality (its display (2.4) together with Remark 1). Its Theorem 3 uses that bound to prove a strong law for weighted averages in which the weights are applied in reverse order, so that the oldest observation always receives the newest, largest weight.

Timeline:

• 1960s: Y. S. Chow (Ann. Math. Statist. 37, 1966) introduces a conditional exponential-moment condition close to Azuma's property [G] in a convergence theorem for independent variables.
• 1967: Azuma proves the moment bound (2.4) for conditionally sub-Gaussian martingale differences, a law of the iterated logarithm for direct weighted sums (Theorem 2), and the strong law for reversed weighted sums (Theorem 3), the subject of this mission.

Setting

Let $(\Omega,\mathfrak A,P)$ be a probability space and $(\mathfrak A_n)_{n\ge0}$ an increasing family of sub-$\sigma$-fields of $\mathfrak A$. A sequence $(x_n)_{n\ge1}$ of real random variables is a sequence of martingale differences if, for every $n\ge1$, $x_n$ is $\mathfrak A_n$-measurable and integrable and $E\{x_n\mid\mathfrak A_{n-1}\}=0$ almost surely. Theorem 3 assumes moreover $|x_n|\le1$ almost surely for every $n$.

Let $(a_n)_{n\ge1}$ be positive increasing weights: $a_n>0$ and $a_n\le a_{n+1}$. Put

$$A_n = a_1+a_2+\dots+a_n,\qquad \bar S_n = a_nx_1 + a_{n-1}x_2+\dots+a_1x_n=\sum_{j=1}^n a_{n-j+1}x_j .$$

The sums $\bar S_n$ are the reversed weighted sums. In passing from $\bar S_n$ to $\bar S_{n+1}$ every existing term changes its weight, so $(\bar S_n)$ is in general not a martingale. In the Lean development, $A_n$ is A a n, $\bar S_n(\omega)$ is Sbar a x n ω, and the martingale-difference property is IsMartingaleDiff μ ℱ x.

Formalization targets

Goal: Theorem 3, (4.9)–(4.10)

If $(x_n)$ is a sequence of martingale differences with $|x_n|\le1$ a.s., $(a_n)$ is positive and nondecreasing, and

$$\frac{a_n}{A_n}=o\Big(\frac{1}{\log\log A_n}\Big)\qquad(n\to\infty),\tag{4.9}$$

then

$$\frac{\bar S_n}{A_n}\longrightarrow0\quad\text{almost surely}.\tag{4.10}$$

Milestones

The milestones follow the paper's proof, in attack order.

1. Remark 1 (p. 358): if $|x_n|\le K_n$ a.s., then $E\{\exp(tx_n)\mid\mathfrak A_{n-1}\}\le\cosh(tK_n)\le\exp(t^2K_n^2/2)$ a.s.
2. The tail step of (4.16) (p. 366): for $|x_n|\le1$, real $c_1,\dots,c_N$ with $\sum c_j^2>0$ and $\lambda\ge0$,

$$P\Big\{\sum_{j=1}^Nc_jx_j>\lambda\Big\}\le\exp\Big(-\frac{\lambda^2}{2\sum_{j=1}^Nc_j^2}\Big).$$

3. The blocks (4.11)–(4.14) (pp. 364–365): for every $\varepsilon>0$ there are indices $n_1<n_2<\cdots$ with $A_{n_1}>2(3+\varepsilon)/(6+\varepsilon)$, $a_n/A_n<\varepsilon/(6+\varepsilon)$ and $a_n\log\log A_n/A_n<\varepsilon^2/64$ for $n>n_1$, and $A_{n_{k-1}}<A_{n_k}\le(1+\varepsilon/3)A_{n_{k-1}}<A_{n_k+1}$.
4. The maximal inequality (4.15) (p. 365): if $A_{N_1}\le(1+\varepsilon/3)A_{N_0}$ with $1\le N_0<N_1$, then

$$2P\{\bar S_{N_1}>(\varepsilon/2)A_{N_0}\}\ge P\Big\{\max_{N_0<n\le N_1}\bar S_n>\varepsilon A_{N_0}\Big\}.$$

5. Block growth (p. 366): (4.11), (4.12) and (4.14) give $A_{n_k}>(2(3+\varepsilon)/(6+\varepsilon))^{k-1}$.

Significance

The result. Theorem 3 shows that reversed weighting does not destroy the strong law, under a growth condition on the weights that is strictly weaker than the condition $a_n^2/\sum_{j\le n}a_j^2\to0$ of the paper's Theorem 2: the paper reproduces an example of T. Tsuchikura satisfying (4.9) but not that condition. The condition allows rapidly growing weights, provided no single weight carries more than an $o(1/\log\log A_n)$ share of the total. Milestone 2 is the one-sided Azuma inequality in the paper's conditional-expectation form, a tool used throughout probability, combinatorics and learning theory. Milestone 4 is a maximal inequality for a process that is not a martingale, where Doob's inequality cannot be used.

Formalizing it. The theorem is proved in the paper; this mission produces a machine-checked proof. Mathlib contains sub-Gaussian moment-generating-function bounds for martingale differences in a kernel formulation (HasCondSubgaussianMGF, which assumes a standard Borel space), and the Prove2Me platform has two-sided Azuma–Hoeffding inequalities under the same assumption. Neither states Remark 1 or the one-sided tail bound in the paper's conditional-expectation form on an arbitrary probability space, and no strong law for reversed weighted sums is formalized.

Difficulty

The obvious route to a strong law for a martingale, Doob's maximal inequality applied along a geometric subsequence, fails at the first step: $(\bar S_n)$ is not a martingale, because each new step reweights all earlier terms. The maximum of $\bar S_n$ over a block of indices therefore needs a separate maximal inequality, and it is there that the monotonicity of the weights is indispensable. A second difficulty is quantitative: the exponential tail bound must be summable over blocks whose growth is controlled only through (4.9), which is weaker than the variance-type condition of Theorem 2, so the block sizes and the constants $\varepsilon/(6+\varepsilon)$, $\varepsilon^2/64$ and $1+\varepsilon/3$ have to be chosen to fit together.

Formalization scope

Conventions committed to in Lean:

• Indices start at $1$: sums run over Finset.Icc 1 n, and $a_0$, $x_0$ are never used. Every hypothesis on $a$ and $x$ is quantified over $n\ge1$.
• The filtration is a Mathlib Filtration ℕ. Its first $\sigma$-field plays the role of $\mathfrak A_0$ and is arbitrary rather than trivial; the paper's $\mathfrak A_0=\{\emptyset,\Omega\}$ is a special case, so the formal statements are at least as general.
• "Positive increasing" is read as $a_n>0$ and $a_n\le a_{n+1}$ (nondecreasing), the weaker hypothesis.
• (4.9) is stated literally as a little-$o$ relation (IsLittleO along atTop). $A_n\to\infty$ is not a hypothesis, since it follows from positivity and monotonicity.
• The conclusion is convergence of the real sequence $\bar S_n(\omega)/A_n$ to $0$ for almost every $\omega$, which contains both the upper and the lower tail; a statement giving only $\limsup\le0$ is not the goal. No real-valued limsup is used anywhere.
• Probabilities are real-valued (μ.real); conditional expectations are Mathlib's μ[f | ℱ n].

A formalization of the goal that replaces $\bar S_n$ by the direct sums $a_1x_1+\dots+a_nx_n$, drops the monotonicity of the weights, or strengthens (4.9) to $a_n/A_n=o(1/\log A_n)$ or to $a_n^2/\sum_{j\le n}a_j^2\to0$ states a different theorem and does not count.

A complete development needs the Azuma moment bound in conditional-expectation form, conditional Chebyshev arguments on events, the Borel–Cantelli lemma (in Mathlib) and elementary real analysis of the blocks. The one-sided Azuma inequality and the maximal inequality (4.15) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. https://doi.org/10.2748/tmj/1178243286
• Y. S. Chow, Some convergence theorems for independent random variables, Annals of Mathematical Statistics 37 (1966), 1482–1493.
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

Motivation

The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form $P(x\mid s,B) = e^{v(s,x)}/\sum_{y\in B} e^{v(s,y)}$. Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.

That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" $v(s,x)$ shared by all alternative sets.

Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes $s$, the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.

Setting

Let $X$ be the universe of objects of choice and $S$ the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set $B\subseteq X$; a designated family of finite sets is the family of possible alternative sets. The selection probability $P(x\mid s,B)$ is the probability that an individual drawn at random from the population, with attributes $s$ and facing $B$, chooses $x\in B$. For every $s$ and possible $B$, $x\mapsto P(x\mid s,B)$ is a probability vector on $B$. Whenever $x\neq y$ belong to a possible set, the pair $\{x,y\}$ is possible too, so binary choices are defined.

• Axiom 1 (IIA). For all possible $B$, all $s$ and all $x,y\in B$: $P(x\mid s,\{x,y\})P(y\mid s,B) = P(y\mid s,\{x,y\})P(x\mid s,B)$.
• Axiom 2 (Positivity). $P(x\mid s,B)>0$ for all possible $B$, all $s$, all $x\in B$.
• Binary probabilities. $p_{xy}=P(x\mid s,\{x,y\})$ for $x\neq y$, and $p_{xx}=\tfrac12$ by definition.
• The function $V$. $V(s,x,z)=\log(p_{xz}/p_{zx})$.
• Universal benchmark. An alternative $z$ such that $B\cup\{z\}$ is possible whenever $B$ is.

In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.

Formalization targets

Goal: footnote 3 with Equation (12)

Under Axioms 1 and 2 and a universal benchmark $z$, with $v(s,x)=V(s,x,z)$, for every $s$, every possible $B$ (containing $z$ or not) and every $x\in B$:

$$P(x\mid s,B) = \frac{e^{v(s,x)}}{\sum_{y\in B} e^{v(s,y)}}.$$

The function $v$ is the same for all alternative sets; this is what distinguishes the goal from Equation (10).

Milestones, in the paper's order

1. Equation (5): for $x\neq y$ in $B$ with $P(x\mid s,B)>0$, Axiom 1 gives $P(x\mid s,\{x,y\})>0$ and $\dfrac{P(y\mid s,\{x,y\})}{P(x\mid s,\{x,y\})}=\dfrac{P(y\mid s,B)}{P(x\mid s,B)}$.
2. Equations (6)–(7): $P(y\mid s,B)=\dfrac{p_{yx}}{p_{xy}}P(x\mid s,B)$ and $1=\Big(\sum_{y\in B}\dfrac{p_{yx}}{p_{xy}}\Big)P(x\mid s,B)$.
3. Equation (8): $P(x\mid s,B)=1\big/\sum_{y\in B}(p_{yx}/p_{xy})$.
4. Equation (9): $\dfrac{p_{yx}}{p_{xy}}=\dfrac{p_{yz}/p_{zy}}{p_{xz}/p_{zx}}$ for $x,y,z$ in a possible set.
5. Equation (10): for a benchmark $z\in B$, $P(x\mid s,B)=e^{V(s,x,z)}\big/\sum_{y\in B}e^{V(s,y,z)}$.

Significance

The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification $v(s,x)=\theta'z(s,x)$ estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.

Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.

Difficulty

The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick $z\in B$ as benchmark" produces a function $V(s,x,z)$ that depends on the set through the choice of $z$. The goal requires a single $v$ for all sets, including sets that do not contain $z$, where neither Equation (10) nor the axioms on $B$ alone say anything about $z$. A second subtlety is the diagonal: $\{x,x\}=\{x\}$, so $p_{xx}$ is set to $\tfrac12$ by definition rather than read off a singleton choice.

Formalization scope

Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.

The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit $v(s,x)=V(s,x,z)$, never as "for each $B$ there is a $v$", which would only restate (10).

Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
• R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, New York, 1959. https://doi.org/10.1037/14396-000

Motivation

Weighted sums of dependent random variables occur when the weights change with the observation horizon. Even if each random variable is bounded and centered, allowing the weights in row $n$ to be chosen anew makes an almost-sure statement about all large $n$ different from a bound on a single finite sum. Kazuo Azuma's 1967 paper treats this situation under a finite-product moment condition called class [M]. Its first main theorem bounds every row of an arbitrary real triangular array at the scale given by that row's Euclidean norm and $\log n$.

The condition is useful because it allows dependence. The paper notes that bounded martingale differences provide examples, but Theorem 1 is stated directly for class [M], without introducing a filtration in the result. The conclusion therefore records the property of the random variables actually used by this part of the paper, rather than restricting the mission to one familiar source of examples. Azuma, §1 and Theorem 1.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$. Let $x_1,x_2,\ldots$ be real measurable random variables. They form a bounded multiplicative system with unit bounds if $|x_k|\le1$ almost surely for every $k\ge1$, and

$$E\!\left[\prod_{k\in S}x_k\right]=0 \quad\text{for every nonempty finite }S\subseteq\{1,2,\ldots\}.$$

The indices in $S$ are distinct. Taking a singleton shows $E[x_k]=0$; taking sets of two, three, or more indices imposes the full condition used in the paper. Pairwise zero correlations by themselves do not state class [M]. All bounds and moment conditions are for the positive indices, so $x_0$ is outside the mathematical sequence. Azuma, p. 357, property [M].

For each $n\ge1$, choose real coefficients $a_{n1},\ldots,a_{nn}$. There is no relation required between different rows. Define the weighted sum $T_n$ and its weight norm $B_n$ by

$$T_n=\sum_{k=1}^{n}a_{nk}x_k, \qquad B_n=\left(\sum_{k=1}^{n}a_{nk}^{2}\right)^{1/2}.$$

Both definitions use the source's 1-based indices. A row of zero weights has $B_n=0$ and $T_n=0$ almost surely; such rows remain within the theorem. Azuma, p. 359, §3.

Formalization targets

The goal is Theorem 1, display (3.1): for every bounded multiplicative system and every real triangular array,

$$\limsup_{n\to\infty} \frac{|T_n|}{\sqrt{2B_n^2\log n}}\le1 \qquad P\text{-almost surely}.$$

The normalizing constant is exactly $2$, and the upper bound is exactly $1$. The mission does not assume that $B_n$ grows, converges, or stays positive. In Lean, the target is stated as the equivalent operational bound: for each $\delta>0$, almost every outcome eventually satisfies $|T_n|\le(1+\delta)\sqrt{2B_n^2\log n}$. This includes zero-weight rows without assigning a meaning to a real quotient $0/0$.

The milestone list follows results displayed in the paper: the corrected convexity inequality (2.2), Lemma 1's exponential moment estimate (2.1), the exponential estimate in the proof of Theorem 1 with its factor $2$, and the almost-sure finite exponential series on the next page. Lemma 1 gives, for arbitrary real $b_1,\ldots,b_n$ and $t\in\mathbb R$,

$$E\exp\!\left(t\sum_{k=1}^{n}b_kx_k\right) \le \exp\!\left(\frac{t^2}{2}\sum_{k=1}^{n}b_k^2\right).$$

The paper prints (2.2) with a missing factor $b_{nk}$ in its linear term. The mission records the printed text as provenance and states the corrected inequality in Lean; the printed version fails already when $b_{nk}=2$ and $x_k=t=1$. Azuma, pp. 357–360.

Significance

Theorem 1 turns an exponential moment bound for each finite weighted sum into a single almost-sure assertion along an entire triangular array. It gives a scale that adapts to the actual coefficients in each row: two arrays with different row norms receive different bounds, while no regularity across rows is required. The result is also the starting point for the weighted strong-law corollaries that follow it in the paper. Azuma, Theorem 1 and Corollary 1.

The mathematical theorem has been proved since 1967. This mission's remaining work is a machine-checked Lean proof of the exact theorem and its listed intermediate statements. A complete development would add reusable formal statements for bounded multiplicative systems and for their finite exponential moments. Those objects could support later work on dependent sums without importing a filtration or a stronger independence assumption. The proposal statements compile as open goals; compilation alone does not supply proofs.

Difficulty

The usual first step for independent bounded variables is to factor the exponential moment into one-variable expectations. Class [M] does not assume independence, so that factorization is unavailable. The condition controls every product with distinct indices, while allowing other dependence. The almost-sure conclusion must also hold when the coefficients change arbitrarily with $n$: bounds that depend on one fixed row do not by themselves settle what happens for all sufficiently large rows. Finally, rows with $B_n=0$ require a statement that preserves the theorem rather than excluding them by an added positivity hypothesis.

Formalization scope

The Lean development represents the probability law by a measure $\mu$ with IsProbabilityMeasure μ, and a random sequence by $x:\mathbb N\to\Omega\to\mathbb R$. It uses measurable variables and states the unit bound almost surely at every positive index. The class [M] predicate quantifies over every nonempty finite set of positive indices; no conditional expectations, filtration, symmetry, or independence hypotheses enter Theorem 1. Finite products and finite weighted sums use ordinary real multiplication and Finset.Icc 1 n. The triangular weights have type $\mathbb N\to\mathbb N\to\mathbb R$, and only entries with $1\le k\le n$ contribute.

The norm $B_n$ is the nonnegative real square root of the sum of squared weights. Real.log is zero at $n=0$ and $n=1$ in Lean, but the target is eventually quantified, so its asymptotic content concerns large $n$. The exponential estimate is stated for $n\ge1$. If $B_n=0$, Lean's total division returns zero in the exponent's quotient; all weights in that row are zero, making this extension valid. In the almost-sure series, the term at index zero is set to zero. The source's limsup is represented by eventual inequalities for every positive excess, avoiding a real-valued limsup default on unbounded sequences.

The definition of class [M] includes every finite product, including singletons; replacing it by pairwise orthogonality would change the theorem. Measurability and the almost-sure unit bounds ensure that the finite products and the exponential functions in Lemma 1 are integrable, so their Lean integrals represent expectations. Contributions toward proofs of the corrected convexity bound, the moment estimate, the exponential series, and the final almost-sure step are all within scope. The finite-product predicate and the exponential estimate are reusable beyond this mission.

Selected references

• Kazuo Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. DOI: 10.2748/tmj/1178243286.

Motivation

A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size $m$ changes the loss of the output at every point by at most $\beta$, the generalization error exceeds the empirical error by roughly $2\beta + (4m\beta + M)\sqrt{\ln(1/\delta)/(2m)}$ with probability $1-\delta$ (their Theorem 12). The bound is useful only when $\beta = O(1/m)$, and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.

Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate $1/(\lambda m)$. The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.

Setting

Let $\Theta$ be a measurable space with a reference measure $\nu$, and write $d\theta$ for integration against $\nu$. A base class $\mathcal H = \{h_\theta : \theta \in \Theta\}$ is indexed by $\Theta$, and $r(h_\theta, z) \in [0, M]$ is the loss of the base hypothesis $h_\theta$ at an example $z \in Z$.

The algorithm outputs a density $g$ with respect to $\nu$: a measurable, nonnegative, integrable $g : \Theta \to \mathbb R$ with $\int_\Theta g\,d\theta = 1$. $F$ denotes the set of all densities. A density is scored by the averaged loss

$$\ell(g, z) = \int_\Theta r(h_\theta, z)\, g(\theta)\, d\theta \qquad (28),$$

the expected loss of a randomized predictor that draws $h_\theta$ from $g$. The relative entropy of $g$ to $g'$ is

$$K(g, g') = \int_\Theta g(\theta) \ln \frac{g(\theta)}{g'(\theta)}\, d\theta \in [0, \infty],$$

with $K(g, g') = +\infty$ when $g\,\nu$ is not absolutely continuous with respect to $g'\,\nu$ or the integrand is not integrable.

Fix a prior $f_0 \in F$, a parameter $\lambda > 0$, and a training set $S = (z_1, \dots, z_m)$. The algorithm returns a minimizer over $F$ of

$$R_r(g) = \frac1m \sum_{j=1}^m \ell(g, z_j) + \lambda K(g, f_0) \qquad (29).$$

For an index $i$, the truncated objective is $R_r^{\setminus i}(g) = \frac1m \sum_{j \ne i} \ell(g, z_j) + \lambda K(g, f_0)$, and $f^{\setminus i}$ denotes one of its minimizers over $F$.

Formalization targets

Goal: Theorem 24

For every minimizer $f$ of (29), every minimizer $f^{\setminus i}$ of the truncated objective, and every example $z$,

$$|\ell(f, z) - \ell(f^{\setminus i}, z)| \le \frac{M^2}{\lambda m}.$$

Milestones

1. $M$-admissibility of (28) (§5.2.3, p. 518): $|\ell(g,z) - \ell(g',z)| \le M \int_\Theta |g - g'|\,d\theta$.
2. Pinsker's inequality, $L^1$ form (proof of Theorem 24): $\tfrac12 \bigl(\int_\Theta |g - g'|\,d\theta\bigr)^2 \le K(g, g')$ for densities $g, g'$.
3. Lemma 21 (p. 513): for a differentiable convex regularizer $N$ on a vector space and a $\sigma$-admissible loss,

$$d_N(f, f^{\setminus i}) + d_N(f^{\setminus i}, f) \le \frac{1}{\lambda m}\Bigl(\ell(f^{\setminus i}, z_i) - \ell(f, z_i) - d_{\ell(\cdot, z_i)}(f^{\setminus i}, f)\Bigr) \le \frac{\sigma}{\lambda m}|\Delta f(x_i)|.$$

4. Bregman divergence of the relative entropy (proof of Theorem 24): $d_{K(\cdot, f_0)}(g, g') = K(g, g')$.
5. $L^1$ displacement bound (proof of Theorem 24):

$$\int_\Theta |f - f^{\setminus i}|\,d\theta \le \frac{M}{\lambda m}.$$

Significance

Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order $M^2/(\lambda m) + (M^2/\lambda + M)\sqrt{\ln(1/\delta)/m}$. The proof also yields the $L^1$ bound $\int |f - f^{\setminus i}| \le M/(\lambda m)$, which by itself gives classification stability $M/(\lambda m)$ for base hypotheses with values in $\{-1, 1\}$ (remark after Theorem 24, p. 518).

The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in $L^1$ form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.

Difficulty

The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy $K(\cdot, f_0)$ is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity $d_{K(\cdot,f_0)} = K$ needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the $+\infty$ values of $K$. Pinsker's inequality itself requires a separate argument at the level of general measures.

Formalization scope

• Densities are IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral $d\theta$ is always against ν, never Lebesgue measure.
• The base loss is r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).
• $K$ is InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts $K$ to a real number with toReal would send $K = +\infty$ to $0$ and make the worst densities minimizers; that reading is excluded.
• The minimizers are given as hypotheses: f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.
• Corrected reading of the algorithm on $S^{\setminus i}$. The goal is stated in the pairwise form of the paper's proof: $f^{\setminus i}$ minimizes the truncated objective with factor $1/m$, the analogue of (20), not (29) run on the $m-1$ points of $S^{\setminus i}$ with factor $1/(m-1)$.
• Corrected display. The objective displayed before Theorem 24 has $\ell(g, z)$ inside the sum; (29) has $\ell(g, z_i)$, which is used.
• Lemma 21 is stated as printed, in its differentiable case, on a real normed space whose elements act as functions on $X$ through a linear map; the goal does not instantiate it. The Bregman identity is stated with the explicit gradient $\ln(g'/f_0) + 1$, for $f_0, g' > 0$, finite $K(g, f_0)$, $K(g', f_0)$, and integrable $g \ln(g'/f_0)$.

Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (Pinsker's inequality). https://doi.org/10.1002/0471200611
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Bregman divergences, Appendix C of the paper). https://doi.org/10.1515/9781400873173

Motivation

A learning algorithm is judged by its generalization error: the expected loss of the hypothesis it outputs on a fresh example. That quantity depends on an unknown distribution, so it is estimated from the training data, by the empirical error (the average loss on the training set) or the leave-one-out error (the average loss on each training point of the hypothesis trained without it). Classical learning theory controls the gap between these estimates and the true error uniformly over a hypothesis class, through its VC dimension or covering numbers. Such bounds say nothing useful about algorithms that search very large or infinite-dimensional spaces, such as support vector machines and regularization networks in a reproducing kernel Hilbert space.

Bousquet and Elisseeff (JMLR 2 (2002) 499–526) replaced the capacity of the class by a property of the algorithm, its stability: how much its output changes when one training example is removed. Their exponential bound for uniformly stable algorithms is the starting point of the stability approach to generalization, which was later used for stochastic gradient descent (Hardt, Recht and Singer, 2016) and differential privacy, and sharpened by Feldman and Vondrák (2019) and Bousquet, Klochkov and Zhivotovskiy (2020).

Timeline. Rogers and Wagner (1978) and Devroye and Wagner (1979) bounded the leave-one-out error of local rules such as k-nearest neighbours through their stability. McDiarmid (1989) proved the bounded-differences inequality. Lugosi and Pawlak (1994) combined it with smoothed error estimates. Kearns and Ron (1999) named hypothesis and error stability and related them to the VC dimension. Bousquet and Elisseeff (2002) introduced uniform stability and proved the exponential bounds this mission formalizes.

Setting

Let $Z = X \times Y$ be a measurable space of labelled examples with an unknown probability distribution $D$. A training set $S = (z_1, \dots, z_m)$ is drawn from $D^m$. A learning algorithm $A$ maps a training set to a hypothesis $A_S : X \to Y'$. It is deterministic and symmetric: it depends on the training set only as a multiset, so it is a function Multiset (X × Y) → (X → Y'), defined for training sets of every size. For a cost $c$, the loss of a hypothesis $f$ at $z = (x, y)$ is $\ell(f, z) = c(f(x), y)$.

Given $S$, write $S^{\setminus i}$ for $S$ with its $i$-th example removed, and $S^i$ for $S$ with $z_i$ replaced by an independent draw $z_i' \sim D$. The three errors are

$$R = \mathbb E_{z \sim D}[\ell(A_S, z)], \qquad R_{\mathrm{emp}} = \frac1m \sum_{i=1}^m \ell(A_S, z_i), \qquad R_{\mathrm{loo}} = \frac1m \sum_{i=1}^m \ell(A_{S^{\setminus i}}, z_i).$$

An algorithm has uniform stability $\beta$ at sample size $m$ (Definition 6) if for every $S \in Z^m$, every $i$ and every $z \in Z$,

$$|\ell(A_S, z) - \ell(A_{S^{\setminus i}}, z)| \le \beta .$$

As a function of the sample size this constant is written $\beta_m$.

Formalization targets

Goal: Theorem 12

If $A$ has uniform stability $\beta$ and $0 \le \ell(A_S, z) \le M$ for all $z$ and all training sets $S$, then for every $m \ge 1$ and $\delta \in (0,1)$, each of the following holds, separately, with probability at least $1 - \delta$ over $S \sim D^m$:

$$R \le R_{\mathrm{emp}} + 2\beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}, \qquad (11)$$ $$R \le R_{\mathrm{loo}} + \beta + (4m\beta + M)\sqrt{\frac{\ln(1/\delta)}{2m}}. \qquad (12)$$

Milestones

1. McDiarmid's inequality (Theorem 2): for measurable $F : Z^m \to \mathbb R$ with $|F(S) - F(S^i)| \le c_i$, $P_S[F - \mathbb E_S F \ge \epsilon] \le e^{-2\epsilon^2/\sum_i c_i^2}$.
2. Uniform stability $\beta$ implies $|\ell(A_S, z) - \ell(A_{S^i}, z)| \le 2\beta$ (p. 504).
3. Lemma 7: the bias identities for $\mathbb E_S[R - R_{\mathrm{emp}}]$, $\mathbb E_S[R(A,S^{\setminus i}) - R_{\mathrm{loo}}]$ and $\mathbb E_S[R - R_{\mathrm{loo}}]$.
4. $R - R_{\mathrm{emp}}$ and $R - R_{\mathrm{loo}}$ have bounded differences $c_i = 4\beta + M/m$.
5. $\mathbb E_S[R - R_{\mathrm{emp}}] \le 2\beta$ and $\mathbb E_S[R - R_{\mathrm{loo}}] \le \beta$.
6. The tail bounds $P_S[R - R_{\mathrm{emp}} > \epsilon + 2\beta] \le \exp(-2m\epsilon^2/(4m\beta+M)^2)$ and the leave-one-out analogue.

Significance

When $\beta = O(1/m)$ both bounds are $O(1/\sqrt m)$, with constants that do not depend on any capacity of the hypothesis space. Later sections of the paper show that Tikhonov regularization in a reproducing kernel Hilbert space has $\beta = O(1/(\lambda m))$, so the theorem gives generalization bounds for support vector regression, kernel ridge regression and, through a smoothed loss, soft-margin classification. The theorem is also the template for later stability bounds: the decomposition into a bias term controlled by stability and a deviation term controlled by a concentration inequality recurs throughout the literature.

The result has been proved since 2002, and replace-one variants appear in textbooks (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Theorem 14.2; Shalev-Shwartz and Ben-David, Chapter 13). On Prove2Me the replace-one textbook version is not formalized, and Mathlib at the platform's environment has no McDiarmid inequality. This mission asks for a machine-checked proof of the paper's remove-one version with its exact constants, and a reusable McDiarmid inequality with per-coordinate constants.

Difficulty

The deterministic steps (the bias identity and the bounded-differences estimates) are short on paper. The central difficulty is McDiarmid's inequality itself: it needs a martingale argument along the coordinates of a product measure, or an equivalent tensorization of conditional sub-Gaussian bounds, with the Doob martingale $\mathbb E[F \mid z_1, \dots, z_k]$ expressed through partial integration over Measure.pi. Hoeffding's inequality for sums, which Mathlib has, does not apply directly: $R - R_{\mathrm{emp}}$ is not a sum of independent terms. A second, bookkeeping difficulty is Lemma 7: the identities rest on exchanging $z_i$ with $z_i'$ and on the symmetry of $A$, which in Lean means measure-preserving coordinate permutations of $D^m \otimes D$ and multiset equalities such as $S^{i\,\setminus i} = S^{\setminus i}$.

Formalization scope

Conventions committed to by the Lean statements:

• An algorithm is a function of a multiset; this is how symmetry is encoded. Samples are Fin m → X × Y, and $S^i$ is Function.update.
• The law of $S$ is Measure.pi (fun _ => D) with D a probability measure; $z_i'$ and $z$ are independent draws, integrated against the product (Measure.pi fun _ => D).prod D.
• The paper's standing assumption that all functions are measurable is one hypothesis: $(S, z) \mapsto \ell(A_S, z)$ is measurable for every sample size. With the bound $0 \le \ell(A_T, z) \le M$ for training sets $T$ of every size, every expectation is a genuine integral, so no bound can hold because a non-integrable expectation defaults to $0$.
• Uniform stability quantifies over every sample, every index and every point, not almost every one.
• "With probability at least $1 - \delta$" means the $D^m$-measure of the failure set is at most $\delta$. The two bounds (11) and (12) are separate statements, joined by a conjunction; they are not claimed for one joint event.
• The paper assumes $\beta_m$ is non-increasing in $m$ and bounds $\beta_{m-1}$ by $\beta_m$ (p. 504). The leave-one-out bound (12) and its milestones carry the explicit hypothesis of uniform stability $\beta$ at size $m-1$; the empirical bound (11) does not.
• McDiarmid's inequality sums $c_i^2$ over $i = 1, \dots, m$; the paper's printed upper index $n$ is a slip.
• When a displayed tail bound has a zero denominator, its formal statement uses the limiting bound $0$. In McDiarmid's inequality this is the constant-function case; in the stability tails the loss is identically zero.

The stability notion is the paper's remove-one notion. A formalization with replace-one stability would prove a different theorem with different constants, and the published FoundationsML_Stability_UniformlyStable (replace-one) is therefore not used.

The development needs the published loss, empirical-error and generalization-error definitions from Foundations of Machine Learning, a McDiarmid inequality on product measures (reusable for any bounded-differences argument), and the coordinate-exchange lemmas for Measure.pi behind Lemma 7. Contributions of a general McDiarmid inequality, of exchangeability lemmas for product measures, and of proofs of any milestone are welcome.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141 (1989) 148–188. https://doi.org/10.1017/CBO9781107359949.008
• L. Devroye and T. Wagner, Distribution-free performance bounds for potential function rules, IEEE Trans. Inform. Theory 25 (1979) 601–604. https://doi.org/10.1109/TIT.1979.1056087
• M. Kearns and D. Ron, Algorithmic stability and sanity-check bounds for leave-one-out cross-validation, Neural Computation 11 (1999) 1427–1453. https://doi.org/10.1162/089976699300016304
• M. Hardt, B. Recht and Y. Singer, Train faster, generalize better: stability of stochastic gradient descent, ICML 2016. https://arxiv.org/abs/1509.01240
• V. Feldman and J. Vondrák, High probability generalization bounds for uniformly stable algorithms with nearly optimal rate, COLT 2019. https://arxiv.org/abs/1902.10710
• O. Bousquet, Y. Klochkov and N. Zhivotovskiy, Sharper bounds for uniformly stable algorithms, COLT 2020. https://arxiv.org/abs/1910.07833
• M. Mohri, A. Rostamizadeh and A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 14.