Probability

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.

Why finite-horizon reinforcement learning needs a variance-sensitive bound

An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.

Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.

The MDP, interaction, and algorithm

Let $\mathcal S$ and $\mathcal A$ be nonempty finite state and action sets with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ is a probability distribution on next states $y$ for every current state $x$ and action $a$. The reward $R(x,a)$ is deterministic, known to the learner, and lies in $[0,1]$. These are the conditions of Assumption 1 and §2. Episodes have $H\ge1$ steps; $K$ episodes comprise $T=KH$ interactions.

A policy $\pi$ chooses an action for each state and step. Its value $V_h^\pi(x)$ is the expected reward from step $h$ through the final step when the state at $h$ is $x$; the terminal value is $V_{H+1}^\pi=0$. The optimal value $V_h^*(x)=\sup_\pi V_h^\pi(x)$ ranges over all deterministic policies of this form. At the start of episode $k$, the environment may choose the initial state using the completed episodes. The learner then fixes a policy $\pi_k$, observes transitions during the episode, and updates counts for the next episode. Its regret is

$$\operatorname{Regret}(K)=\sum_{k=1}^{K}\bigl(V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})\bigr).$$

For each state-action pair, $N_k(x,a,y)$ counts transitions to $y$ in episodes before $k$, and $N_k(x,a)=\sum_yN_k(x,a,y)$. When the latter is positive, $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. The count $N'_{k,h}(y)$ records previous episodes whose state at step $h$ was $y$. Algorithms 2 and 4 compute optimistic $Q_{k,h}$ backward from zero terminal value, take a minimum with the previous episode's $Q$ estimate and with $H$, and choose a maximizing action at every state. Previously unseen pairs receive $Q_{k,h}=H$. The Bernstein–Freedman bonus uses the empirical variance of $V_{k,h+1}$ under $\widehat P_k$ and an additional term based on $N'_{k,h+1}$; the algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$.

Formalization targets

The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every $\delta>0$, write $L=\ln(5HSAT/\delta)$. The target is the exact bad-event form of the printed high-probability bound:

$$\Pr\!\left\{\operatorname{Regret}(K)>30HL\sqrt{SAK}+2500H^2S^2AL^2+4H^{3/2}\sqrt{KL}\right\}\le\delta.$$

The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's $\ell_1$ error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.

What the result and its formalization supply

The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in $K$ in the leading term, with explicit dependence on $S$, $A$, and $H$. The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.

A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.

Where the difficulty lies

The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.

Formalization scope and conventions

The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining $V^*$ ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.

Lean indexes the $H$ steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index $H+1$. At $N'_{k,h+1}(y)=0$, Algorithm 4's quotient is interpreted as infinite and the capped term is $H^2$; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$, while Theorem 2's bound uses $L=\ln(5HSAT/\delta)$. For Eq. (26), the appendix ends its sums at $H-1$ under a shifted terminal convention; the local statement includes all $H$ reward steps and the terminal value $V_{H+1}=0$ used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of $2$ under the square root present in that display.

Theorem 2 retains its printed $2500H^2S^2AL^2$ term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.

Selected references

• M. G. Azar, I. Osband, and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Preprint.

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing step sizes $\gamma_n$ and a noise term $U_{n+1}$. Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of $\dot x=F(x)$. In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process $X$. Under standard noise conditions, $X$ is almost surely an asymptotic pseudotrajectory of the flow of $F$, and its limit set is almost surely internally chain transitive.

That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.

Timeline.

• Kushner and Clark (1978) proved convergence statements for processes that visit a compact subset of the domain of attraction of an asymptotically stable equilibrium infinitely often.
• Arthur, Ermoliev and Kaniovski (1983) and Pemantle (1990) studied urn processes whose limit points depend on the trajectory.
• Benaïm (1997) and Duflo (1997, Random Iterative Models) developed the attainability argument for general stochastic approximation processes.
• Benaïm (1999) states it for arbitrary attractors of a semiflow on a locally compact metric space, under a single conditional shadowing condition (24).

Setting

Let $(M,d)$ be a metric space and let $\Phi=(\Phi_t)_{t\ge0}$ be a semiflow on $M$: a continuous map $(t,x)\mapsto\Phi_t(x)$ with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$.

• A set $A$ is invariant if $\Phi_t(A)=A$ for all $t\ge0$, and positively invariant if $\Phi_t(A)\subset A$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly. Its basin $B(A)$ is the set of points $x$ with $\operatorname{dist}(\Phi_tx,A)\to0$.
• A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory if $\sup_{0\le h\le T}d(X(t+h),\Phi_h(X(t)))\to0$ as $t\to\infty$, for every $T>0$.
• The limit set of $X$ is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$.
• For $T>0$, $d_X(T)=\sup_{k\in\mathbb N}d(\Phi_T(X(kT)),X(kT+T))$.

Now let $X=(X(t))_{t\ge0}$ be a process on a probability space $(\Omega,\mathcal F,P)$ with continuous paths in $M$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$. The standing assumption of Section 7 is that for all $\delta>0$, $T>0$ and $t\ge0$,

$$P\Big(\sup_{s\ge t}\ \sup_{0\le h\le T}d\big(X(s+h),\Phi_h(X(s))\big)\ge\delta\ \Big|\ \mathcal F_t\Big)\le w(t,\delta,T)\tag{24}$$

for a function $w\ge0$ with $w(t,\delta,T)\downarrow0$ as $t\to\infty$.

A point $p$ is attainable if $P(\exists s\ge t: X(s)\in U)>0$ for every $t>0$ and every open neighbourhood $U$ of $p$. $\mathrm{Att}(X)$ is the set of attainable points.

Formalization targets

Goal: Theorem 7.3, first statement

If $M$ is locally compact, $A$ is an attractor of $\Phi$, and $\mathrm{Att}(X)\cap B(A)\neq\emptyset$, then

$$P\big(L(X)\subset A\big)>0 .$$

This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.

Theorem 7.3, second statement

If $U$ is open and relatively compact with $\overline U\subset B(A)$, there are $T,\delta>0$, depending only on $U$ (and on $\Phi$, $A$), such that for every process satisfying the standing assumption and every $t\ge0$

$$P\big(L(X)\subset A\big)\ge\big(1-w(t,\delta,T)\big)\,P\big(\exists s\ge t:\ X(s)\in U\big).$$

Milestones

• Lemma 6.8. For a nonempty compact $K\subset B(A)$ there are $T,\delta>0$ such that every asymptotic pseudotrajectory with $X(0)\in K$ and $d_X(T)<\delta$ has $L(X)\subset A$.
• Lemma 7.1, in three parts:
  • $\mathrm{Att}(X)$ is closed;
  • it is positively invariant;
  • it contains $L(X)$ almost surely.

Significance

The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.

Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:

• a precise reading of the conditional shadowing condition (24) as a conditional expectation of an indicator;
• the stopping-time decomposition of the event $\{\exists s\ge t: X(s)\in U\}$ over dyadic times;
• the deterministic Lemma 6.8, which rests on the limit set theorem for precompact asymptotic pseudotrajectories (Theorem 5.7 of the notes, the subject of mission 1 of this series).

Difficulty

The obvious argument says: once $X$ enters a compact part of the basin, the flow carries it into $A$. That fails because $X$ is not a trajectory of the flow. Each window of length $T$ adds an error, and errors over infinitely many windows can push the process out of the basin.

Two things are needed instead:

• A uniform version of the deterministic statement, with $T$ and $\delta$ fixed in advance from the compact set alone. This is Lemma 6.8, which needs local compactness of $M$ and the structure of limit sets of asymptotic pseudotrajectories.
• A probabilistic step that applies (24) at the random time when $X$ first enters $U$. That time is not a stopping time on a continuum, and conditioning at it needs care.

A naive union bound over all times is useless: it does not use the conditional form of (24).

Formalization scope

• The semiflow is Mathlib's Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.
• The process is X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.
• Adaptedness is Borel measurability of $X(t)$ with respect to $\mathcal F_t$, for a Mathlib Filtration ℝ≥0. $P$ is a probability measure.
• The suprema in (24) and in $d_X(T)$ are computed in $[0,\infty]$ with the extended distance, so that "sup $\ge\delta$" and "sup $<\delta$" are exact even when the supremum is infinite or not attained.
• The conditional probability in (24) is the conditional expectation of the indicator of the event. The event is required to be measurable, so the condition cannot hold vacuously through a junk conditional expectation.
• $w$ is required to be both nonincreasing in $t$ and convergent to $0$.
• The events $\{L(X)\subset A\}$ and $\{\exists s\ge t: X(s)\in U\}$ are measured with $P$ as an outer measure, so no measurability hypothesis is added for them.
• In the second statement of Theorem 7.3, $T$ and $\delta$ are chosen before the probability space, the process, $w$ and $t$.
• Invariance in the definition of an attractor is the equality $\Phi_t(A)=A$, not inclusion.
• The almost-sure clause of Lemma 7.1 is stated for separable $M$. Without separability it cannot be proved in ordinary set theory.

These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants $T,\delta$ that depend on the process or on $t$, and a probability bound $w$ without monotonicity.

A complete development needs:

• limit sets of asymptotic pseudotrajectories and the fact that an internally chain transitive set meeting the basin of an attractor lies in the attractor (shared with missions 1 and 5 of this series);
• measurability of path functionals of continuous processes;
• conditioning on events of the form $\{\tau=t_n(k)\}$ at dyadic times.

The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, are welcome.

Selected references

• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Benaïm, Vertex-reinforced random walks and a conjecture of Pemantle, Annals of Probability 25 (1997), 361–392. https://doi.org/10.1214/aop/1024404292
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997. https://doi.org/10.1007/978-3-662-12880-0
• H. J. Kushner, D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8
• C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

Motivation

A manufacturer that makes one product to stock faces random demand, can produce at most $b$ units per period, and can store at most $U$ units. The classical result without the production limit is that a base-stock policy is optimal: raise inventory to a fixed level $\bar y$ each period. With a production limit, the natural modification is to produce up to $\bar y$ when that is possible and to produce at full capacity otherwise. Federgruen and Zipkin (1986) proved that this modified base-stock (critical-number) policy is optimal under the long-run average-cost criterion, for discrete demand with a general convex cost. Production-capacity models of this type are standard in operations management texts, and the result underlies the computational and comparative-static work that followed, starting with Part II of the same paper, which treats discounted costs.

Timeline.

• 1950s–60s: optimality of base-stock (critical-number) policies for uncapacitated periodic-review models; see Heyman and Sobel's Stochastic Models in Operations Research, Vol. II (1984).
• 1986: Federgruen and Zipkin, Part I (average cost, MOR 11(2):193–207) and Part II (discounted cost, MOR 11(2):208–215) establish the capacitated case. Part I handles the unbounded state space with a general average-cost theory for countable-state Markov decision processes by Federgruen, Schweitzer and Tijms (1983).

Setting

Time is divided into periods $t = 0, 1, \dots$. The demands $D_0, D_1, \dots$ are independent copies of a random variable $D$ with values in $\{0, 1, 2, \dots\}$ and probability mass function $p(j)$; write $\mu = E(D)$ and $P(j) = \Pr\{D \le j\}$. At the start of period $t$ the inventory is an integer $x_t$ (negative values are backorders). The decision maker raises it to

$$y_t \in Y(x_t) = \{y \in \mathbb Z : x_t \le y \le x_t + b,\ y \le U\},$$

pays the expected one-period cost $G(y_t)$, and demand is subtracted: $x_{t+1} = y_t - D_t$. The order cost per unit is set to zero, as in the paper; this loses no generality because every policy with finite average cost has the same average order cost.

The standing assumptions are: $G \ge 0$ is convex and $G(y) \to \infty$ as $|y| \to \infty$ (Assumption 1); the characteristic function of $D$ is analytic at the origin (Assumption 2), and $0 < \mu$; $G(y) \le A + B|y|^\rho$ for some positive integer $\rho$ (Assumption 3); $b > \mu$ and $P(b) < 1$ (Assumption 4). The smallest global minimizer of $G$ is $\bar y^\infty$, and $U \ge \bar y^\infty$.

A Markov policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of maps with $\pi_t(x) \in Y(x)$. The critical-number policy with critical number $\bar y$ is $\delta[\bar y](x) = \max(x, \min(\bar y, x + b))$. A stationary policy $\delta$ is strongly optimal with average cost $g$ if, from every initial state $x \le U$, its average cost $t^{-1}E\{\sum_{i<t} G(y_i)\}$ converges to $g$, while every Markov policy has lim-inf average cost at least $g$ from every initial state.

The analysis uses the operators $Rv(y) = G(y) + E\,v(y - D)$ and $Sv(x) = \min_{y \in Y(x)} Rv(y)$, and the optimality equation

$$g + v(x) = Sv(x),\qquad x \le U. \tag{6}$$

For an interval $\iota = [l, u]$, $H_\iota v(x)$ is the largest expected sum of $v(y_t)$, over policies forced to produce at capacity below $l$ and to produce nothing above $u$, until the inventory first returns to $\iota$.

Formalization targets

Goal: Theorem 1 (p. 202)

There exist $g^*$, $v^*$ and $y^* \ge \bar y^\infty$ such that $(g^*, v^*)$ solves (6), $v^*$ is convex with global minimizer $y^*$, and

$$\delta^* = \delta[y^*] \text{ is strongly optimal with average cost } g^*.$$

The $y^*$ in the optimality claim is the minimizer constructed in part (a).

Milestones

• Lemma 2(a)–(c) (pp. 196–197): a normal-tail inequality and two series estimates.
• Lemma 3 (p. 198): if $v(x) = O(|x|^q)$ then $H_\iota v(x) = O(|x|^{q+3})$.
• Corollary 1 (p. 200): $H_\iota 1 = O(|x|^3)$ and $H_\iota G = O(|x|^{\rho+3})$, both finite.
• Corollary 2 (p. 201): $(t+1)^{-1}P[\delta_{0t}]\cdots P[\delta_{tt}](H_\iota 1 + H_\iota G)(x) \to 0$.
• Lemma 4 (p. 201): reachability of every state in $[L, U - D_-]$ under some policy that produces at capacity below $L$.
• Lemma 5 (p. 202): $S$ and $Q$ preserve the class $V$ of convex functions of growth $O(|x|^{\rho+3})$ that are nonincreasing below $\bar y^\infty$.

Significance

The result. Theorem 1 reduces an infinite-state average-cost control problem to a one-parameter search over critical numbers. The paper then evaluates the average cost of $\delta[\bar y]$ by a renewal formula, proves it convex in $\bar y$ (Theorem 2), and in §5 extends optimality to unlimited storage. The strong form of optimality matters: it compares with every Markov policy from every starting state, and it compares lim-infs, not only lim-sups.

Formalizing it. The theorem has a published proof, but no machine-checked one, and its proof relies on external results that are themselves unformalized: the countable-state average-cost theory of Federgruen, Schweitzer and Tijms, a fixed-point theorem on a compact convex subset of a product space, and a large-deviation estimate quoted from Feller. A formal development produces reusable infrastructure: expected first-passage sums for integer-valued random walks with a reflecting control, polynomial moment bounds for them, and the convexity-preservation argument for capacitated value iteration.

Difficulty

The state space is unbounded below, so the finite-state theory of average-cost Markov decision processes does not apply, and the one-period cost is unbounded. The obvious approach, letting the discount factor tend to one in the discounted problem, needs uniform bounds on relative value functions. Those bounds come from the expected cost until the inventory returns to a fixed interval, and with capacity limits that expectation must be controlled with growth $O(|x|^{\rho+3})$ uniformly over a class of policies. This is the content of Lemma 3, whose proof combines a large-deviation estimate for the demand sums with a renewal-type recursion. A second obstacle is strong optimality: comparing with policies whose lim-inf average cost is smaller requires that the relative value function grows sublinearly along every admissible trajectory (Corollary 2).

Formalization scope

All objects are in the namespace FedergruenZipkin.AvgCost, defined in one file. States $x, y$ and the capacity $U$ are integers; demands are natural numbers with a real probability mass function p; $b$ is a positive natural number. Convexity on $\mathbb Z$ is the second-difference inequality. Expectations of a real function are series $\sum_j p(j)\,v(y-j)$; expected policy costs and hitting sums are $[0,\infty]$-valued and need no integrability side condition. Feasibility and all properties of value functions are required only on states $x \le U$, which are the only states visited. Assumption 2 is stated literally, as real-analyticity of $\theta \mapsto \sum_j p(j)e^{i\theta j}$ at $0$. The order cost is zero, as in the paper. $\bar y^\infty$ is a parameter characterised as the least minimizer of $G$, not an infimum.

"Strongly optimal" has no displayed definition in the paper; it is read from eq. (7) in the proof of Theorem 1(b): convergence of the average cost of $\delta^*$ to $g^*$ from every state, together with a lim-inf lower bound for every Markov (memoryless, possibly nonstationary) policy from every state. The class is neither widened to history-dependent policies nor narrowed to stationary ones. The goal additionally records that $E\,v^*(y-D)$ converges, that $v^*$ has growth $O(|x|^{\rho+3})$, and that $g^* \ge 0$; all three follow from the paper's proof.

A trivializing reading is ruled out: the existence of $g$, $v$ and $y^*$ is one existential, so $y^*$ cannot be decoupled from the solution of (6), and strong optimality includes the convergence of $\delta^*$'s own average cost to $g^*$, so $g = 0$ does not satisfy it vacuously.

Not posed: Lemma 1 (quoted from Feller, and replaceable by a Chernoff bound); the renewal formulas (10)–(11) and Theorem 2; and §5 (unlimited storage). Useful contributions include a formal theory of expected hitting sums for skip-free-upward random walks, and a proof of Lemma 3 by any route.

Selected references

• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands I. The Average-Cost Criterion, Mathematics of Operations Research 11(2):193–207, 1986. https://doi.org/10.1287/moor.11.2.193
• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands II. The Discounted-Cost Criterion, Mathematics of Operations Research 11(2):208–215, 1986. https://doi.org/10.1287/moor.11.2.208
• A. Federgruen, P. J. Schweitzer and H. C. Tijms, Denumerable Undiscounted Semi-Markov Decision Processes with Unbounded Rewards, Mathematics of Operations Research 8(2):298–314, 1983. https://doi.org/10.1287/moor.8.2.298
• D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.

The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.

Setting

A linear program is specified by vectors $a_1,\ldots,a_n\in\mathbb R^d$, right-hand sides $y_1,\ldots,y_n\in\mathbb R$, and an objective vector $z\in\mathbb R^d$:

$$\max_x\langle z,x\rangle\quad\text{subject to}\quad \langle a_i,x\rangle\le y_i\qquad(1\le i\le n).$$

The paper’s two-phase shadow-vertex method first draws a collection $\mathcal I$ of $d$-element subsets of $[n]$ and chooses one whose constraint matrix $A_I$ has the largest smallest singular value. It sets a power-of-two scale $M$ from the input norm and a power-of-two scale $\kappa$ from that singular value. These determine positive relaxed right-hand sides $y'_i$: $M$ for $i\in I$ and $\sqrt d M^2/(4\kappa)$ otherwise. A coefficient vector $\alpha$ is chosen uniformly from $A_{1/d^2}=\{\alpha:\sum_{i\in I}\alpha_i=1,\ \alpha_i\ge1/d^2\}$. The first phase solves the relaxed program LP′ from the objective $A_I\alpha$.

The second phase uses a lifted program LP⁺ in $\mathbb R^{d+1}$. For each original constraint it forms $a_i^+=((y'_i-y_i)/2,a_i)$ and $y_i^+=(y'_i+y_i)/2$, together with two artificial constraints at first coordinates $1$ and $-1$. LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of $(0,z)$ and $z^+=(1,0,\ldots,0)$.

For positive right-hand sides, an optimal polar simplex is a $d$-subset of constraints whose scaled vectors $a_i/y_i$ form a facet of $\operatorname{ConvHull}(0,a_1/y_1,\ldots,a_n/y_n)$ and whose unscaled cone contains an objective $q$. The shadow for objectives $t,z$ is the union of these simplices over all $q$ in $\operatorname{Span}(t,z)$. Its size bounds the number of polar pivots. In Section 5 the paper writes $S'_z$ for the first-phase shadow size and $S_z^+$ for the second-phase shadow size without the two artificial pivots.

The input is perturbed by independent Gaussians: each coordinate of $a_i$ and each $y_i$ has its prescribed center and common standard deviation $\sigma R$, where $R=\max_i\|(\bar y_i,\bar a_i)\|_2$. The algorithm has separate random choices of $\mathcal I$ and $\alpha$.

Formalization targets

The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for $S'_z$ and Lemma 5.3.1 gives one for $S_z^+$. Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.

The goal is the shape of Theorem 5.0.1. With $C(A,y,z)=\mathbb E_{\mathcal I,\alpha}(S'_z+S_z^++2)$, there are a single polynomial $\mathcal P$ and a positive constant $\sigma_0$ such that, for all $n>d\ge3$ and all centers and objectives,

$$\mathbb E_{A,y}C(A,y,z)\le \min\left\{\mathcal P\left(d,n,\frac1{\min(\sigma,\sigma_0)}\right), \binom nd+\binom n{d+1}+2\right\}.$$

The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on $C$ implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale $R$, the case in which the paper’s Gaussian rescaling applies.

Significance

The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.

Difficulty

The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective $A_I\alpha$ uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors $a_i^+/y_i^+$ are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make $y'$ very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s $[n]$ starts at one; Fin n starts at zero. The Gaussian constructor receives variance $\sigma^2$, not standard deviation $\sigma$. The $3nd\ln n$ draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on $A_\delta$ is represented by normalized independent exponential weights followed by the affine shift that imposes $\alpha_i\ge\delta$.

The Lean definition of $C$ is exactly the Section 5 shadow-size upper bound $\mathbb E(S'_z+S_z^++2)$, computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.

For LP⁺ the vectors live in $\mathbb R^{d+1}$, so the two LP⁺ milestone bounds use $\mathcal D(n,d+1,\cdot)$. The preprint prints $d$ in those calls even though the preceding extension theorem would be applied in dimension $d+1$. Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.

Selected references

• Daniel A. Spielman and Shang-Hua Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003, preprint. The PDF used here is the 96-page version with printed and PDF page numbers aligned.

Motivation

Reinforcement learning methods must explore in order to find good behaviour, yet the quantity they usually want to evaluate is the value of a different, often deterministic, policy. Off-policy prediction separates the two roles: episodes are generated by a behaviour policy $b$, and the goal is the value function $v_\pi$ of a target policy $\pi$. Almost every off-policy method in Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), and in the literature that follows it, rests on importance sampling: a return observed under $b$ is reweighted by the relative probability of its trajectory under $\pi$ and $b$. Section 5.5 of the book introduces the idea for Monte Carlo prediction, §5.6 gives the incremental form of the weighted estimator, and §§5.8–5.9 refine the weights using the internal structure of the return: discounting-aware importance sampling, after Sutton, Mahmood, Precup and van Hasselt (2014), and per-decision importance sampling, introduced by Precup, Sutton and Singh (2000). The book's remarks on the variance of the two estimators (p. 105) cite Precup, Sutton and Dasgupta (2001). Later chapters (7, 11, 12) reuse the same ratios for $n$-step, gradient-TD and eligibility-trace methods.

This mission is the fifth in a series formalizing the book's central mathematical claims. It covers §§5.5–5.9 (pp. 103–115).

Setting

A finite Markov decision process has finite sets of states $\mathcal S$ (terminal states included), actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$: for each $(s, a)$ a probability distribution over next state and reward. The state-transition probability is $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$. A policy $\mu$ gives a distribution $\mu(\cdot \mid s)$ over actions in every state.

An episode from a start state $s$ is a sequence $S_0 = s, A_0, R_1, S_1, \dots, A_{T-1}, R_T, S_T$ in which $S_0, \dots, S_{T-1}$ are nonterminal and $S_T$ is terminal. Under $\mu$ it has probability $\prod_{k=0}^{T-1} \mu(A_k \mid S_k)\, p(S_{k+1}, R_{k+1} \mid S_k, A_k)$. The return is $G_0 = \sum_{k=0}^{T-1} \gamma^k R_{k+1}$ with discount rate $\gamma \in [0, 1]$, and the value $v_\pi(s)$ is the expected return of an episode generated by $\pi$ from $s$.

The behaviour policy covers the target policy if $\pi(a \mid s) > 0$ implies $b(a \mid s) > 0$. The importance-sampling ratio of decisions $0, \dots, j$ is

$$\rho_{0:j} = \prod_{k=0}^{j} \frac{\pi(A_k \mid S_k)}{b(A_k \mid S_k)},$$

and the per-decision return weights each reward only by the ratio of the decisions that precede it:

$$\tilde G_0 = \rho_{0:0} R_1 + \gamma \rho_{0:1} R_2 + \dots + \gamma^{T-1} \rho_{0:T-1} R_T .$$

The book writes these objects at a general time $t$ and conditions on $S_t = s$; by the Markov property this is the same as starting the episode at $s$, which is what the formal statements do.

Formalization targets

Goal: unbiasedness of ordinary and per-decision importance sampling

For episodes generated by $b$ from $s$,

$$\mathbb E_b\bigl[\rho_{0:T-1} G_0 \mid S_0 = s\bigr] = v_\pi(s) = \mathbb E_b\bigl[\tilde G_0 \mid S_0 = s\bigr].$$

The first equality is Eq. (5.4) (p. 104); the second is the statement $\mathbb E[\rho_{t:T-1}G_t] = \mathbb E[\tilde G_t]$ of §5.9 (p. 114).

Milestones

1. (5.3): the trajectory probability is a product, and the ratio of trajectory probabilities under $\pi$ and $b$ is $\rho_{0:T-1}$, independent of the dynamics.
2. (5.4) alone.
3. (5.13): $\sum_a b(a \mid x)\, \pi(a \mid x)/b(a \mid x) = \sum_a \pi(a \mid x) = 1$ under coverage.
4. (5.14) and its $k$-th form: $\mathbb E_b[\rho_{0:T-1} R_k] = \mathbb E_b[\rho_{0:k-1} R_k]$ for every $k \ge 1$ (Exercise 5.13).
5. Example 5.5: in a one-state MDP with a loop, $v_\pi(s) = 1$ and $\mathbb E_b[\rho_{0:T-1}G_0] = 1$, yet $\mathbb E_b[(\rho_{0:T-1}G_0)^2] = \infty$.
6. (5.7)–(5.8): the incremental rule $V_{n+1} = V_n + (W_n/C_n)(G_n - V_n)$ computes the weighted average $\sum_{k<n} W_k G_k / \sum_{k<n} W_k$ (Exercise 5.10).
7. §5.8: $G_t = (1-\gamma)\sum_{h=t+1}^{T-1}\gamma^{h-t-1}\bar G_{t:h} + \gamma^{T-t-1}\bar G_{t:T}$ with flat partial returns $\bar G_{t:h} = R_{t+1} + \dots + R_h$.

Significance

Eq. (5.4) is the reason the first-visit ordinary importance-sampling estimator (5.5) is unbiased, and it is the template for every importance-sampling correction in the rest of the book. The per-decision identity shows that an estimator with fewer ratio factors per reward, (5.15), has the same expectation, which is the starting point for per-decision and control-variate methods for multi-step off-policy learning (Precup, Sutton and Singh 2000). Example 5.5 shows that unbiasedness says nothing about variance: the ordinary estimator can have infinite variance on a two-action problem, which motivates weighted importance sampling and the incremental weighted update of §5.6.

The results of these sections are classical and proved informally in the book, partly as exercises (5.10, 5.13) left without solution. No machine-checked version exists on the platform: a search for importance sampling, off-policy and per-decision returned no statements. The mission produces a formal trajectory model of an episodic MDP under two policies, which later missions on $n$-step off-policy returns and off-policy traces can reuse.

Difficulty

Eq. (5.4) itself is a termwise identity: for every episode, $\Pr_b(\text{episode})\,\rho_{0:T-1} = \Pr_\pi(\text{episode})$ under coverage. The per-decision identity is not termwise. The later factors of $\rho_{0:T-1}$ multiply a reward that was received before the corresponding decisions, and removing them requires summing over all continuations of an episode prefix, of every remaining length, and using that each factor has conditional expectation one (5.13) and that the continuation terminates with probability one. The obvious attempt, cancelling the factors episode by episode, fails: on a single episode $\rho_{0:T-1}R_1$ and $\rho_{0:0}R_1$ differ.

In Example 5.5 the episodes have no length bound, so the expected square is an infinite series over episode lengths whose divergence must be shown directly.

Formalization scope

• States, actions and rewards are finite types; the terminal states are a finite subset of the state type. Policies are stochastic, one action set is used in every state, and $v_\pi$ is defined as an expected return, never as the solution of a Bellman equation.
• Expectations are series over episode lengths of finite sums over episodes. Lean assigns $0$ to a divergent series, so the goal and milestones 2 and 4 assume that under $b$ every episode from $s$ terminates within a fixed number $H$ of steps with probability one. The book leaves termination implicit; this bounded-horizon hypothesis is a restriction relative to the book's episodic setting and is stated as such. Example 5.5, whose episodes are unbounded, is stated without it, with the expected square in $[0, \infty]$.
• The discount rate is kept general in $[0, 1]$.
• The importance-sampling ratio uses real division; a factor with $b(A_k \mid S_k) = 0$ evaluates to $0$ in Lean, but such episodes have probability $0$ under $b$.
• The flat-partial-return decomposition is an algebraic identity and is stated for every real $\gamma$, which is more general than the book's "for any $\gamma \in [0,1)$".
• The incremental weighted update is stated with nonnegative weights and $W_1 > 0$. The book's $C_0 = 0$ makes (5.8) divide by zero at $n = 1$ when $W_1 = 0$; the hypothesis excludes that case.
• A trivializing formalization is ruled out: $v_\pi$ is the expected return of $\pi$'s own episodes, the ratio is computed from the episode, and the per-decision identity, which carries the chapter's content beyond (5.4), is part of the goal.
• Not stated: the bias and variance comparisons of ordinary and weighted importance sampling (p. 105) and the discounting-aware estimators (5.9)–(5.10) as estimators; these are statistical claims about estimators over a random number of visits that the book does not make precise.

Contributions welcome: proofs of the milestones, a general measure-theoretic version of the trajectory model without the bounded-horizon hypothesis, and variants for action values $q_\pi$ (Exercise 5.6).

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§5.5–5.9, pp. 103–115. http://incompleteideas.net/book/the-book-2nd.html
• D. Precup, R. S. Sutton and S. Singh, Eligibility Traces for Off-Policy Policy Evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (cited in the book's bibliography).
• D. Precup, R. S. Sutton and S. Dasgupta, Off-Policy Temporal-Difference Learning with Function Approximation, Proceedings of the 18th International Conference on Machine Learning (ICML), 2001, pp. 417–424 (cited in the book, p. 105).