Probability

Motivation

A random walk on the integers in which the probability of stepping right depends on the current site is the simplest model of motion through a disordered medium: a particle diffusing in a crystal with impurities, a molecule moving along a heterogeneous polymer, or a gene frequency drifting under fluctuating selection. When the site-dependent probabilities are themselves drawn at random, the result is a random walk in a random environment (RWRE). Fred Solomon's 1975 paper [Solomon 1975] gave the first rigorous analysis of this model on $\mathbb Z$ with independent, identically distributed site probabilities, and its recurrence criterion opened the subject now surveyed in [Zeitouni 2004].

Timeline. Chung [Chung 1960, pp. 65–71] gave the hitting probabilities and the recurrence/transience criterion for a nearest-neighbour chain on $\mathbb Z$ with fixed, site-dependent transition probabilities. Fluctuation theory, as presented in Chung's A Course in Probability Theory [Chung 1968, Ch. 8], characterises when a sum of i.i.d. random variables drifts to $-\infty$, to $+\infty$, or oscillates, through the series $\sum\frac1nP(S_n>0)$ and $\sum\frac1nP(S_n<0)$. Solomon (1975) combined the two to classify the RWRE on $\mathbb Z$, and also computed its speed and exhibited sub-ballistic and non-Gaussian behaviour. Kesten, Kozlov and Spitzer (1975) [KKS 1975] identified stable limit laws in the transient sub-ballistic regime, and Sinai (1982) [Sinai 1982] found the $(\log n)^2$ scaling of the recurrent case.

Setting

Let $\alpha=(\alpha_n)_{n\in\mathbb Z}$ be independent, identically distributed random variables with values in $[0,1]$. Given a fixed sequence $a=(a_n)$ in $[0,1]$ (an environment), the chain $M_a$ on $\mathbb Z$ jumps from $n$ to $n+1$ with probability $a_n$ and to $n-1$ with probability $\beta_n=1-a_n$. The random walk in a random environment $(X_n)_{n\ge0}$ is the process obtained by first drawing $\alpha$ and then running $M_\alpha$ from $X_0=0$; jointly,

$$P(\alpha\in A,\ X_0=x_0,\dots,X_n=x_n)=\int_{\{\alpha\in A\}}\mathbf 1\{x_0=0\}\prod_{k<n}M_\alpha(x_k,x_{k+1})\,dP .$$

The walk is a Markov chain given the environment, but not after averaging over it. Define

$$\sigma_n=\frac{\beta_n}{\alpha_n}\in[0,\infty],\qquad \rho_n=\sigma_1\cdots\sigma_n\ (n\ge1),\qquad \rho_{-n}=\sigma_{-1}\cdots\sigma_{-n}\ (n\ge1),$$

and, for a fixed environment, the hitting probability $f_{ij}=P(X_n=j\text{ for some }n>0\mid X_0=i)$. The quantity $E(\ln\sigma)$ is defined when the expectation of the positive or of the negative part of $\ln\sigma\in[-\infty,\infty]$ is finite.

Formalization targets

Goal: Theorem (1.7)

Assume $\alpha_0$ is not almost surely constant and either $0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$. Then

$$\sum_{n\ge1}\tfrac1nP(\rho_n>1)<\infty\Rightarrow X_n\to+\infty,\qquad \sum_{n\ge1}\tfrac1nP(\rho_n<1)<\infty\Rightarrow X_n\to-\infty,$$

and if both series diverge, $-\infty=\liminf X_n<\limsup X_n=+\infty$, all almost surely. When $E(\ln\sigma)$ is defined, the three cases are exactly $E(\ln\sigma)<0$, $>0$, $=0$.

Milestones

Theorem (0.1): almost-sure properties of the walk in almost every fixed environment transfer to the RWRE. Lemma (1.1)(i)–(ii): the hitting probabilities $f_{ij}$ in a fixed environment with $0<a_n<1$, as ratios of series in $\sigma$. Lemma (1.5): in a fixed environment, $\sum(\rho_{-n})^{-1}$ and $\sum\rho_n$ decide transience to $+\infty$, to $-\infty$, or recurrence. Lemma (1.6): fluctuation theory for i.i.d. sums, including the summability of $e^{S_n}$. Two claims from the proof of (1.7) (p. 5): the boundary cases where $\alpha_n$ equals $1$ or $0$ with positive probability, and the equivalence $E(\ln\sigma)<0\iff S_n\to-\infty\iff\sum\frac1nP(\rho_n>1)<\infty$ for $S_n=\ln\sigma_1+\dots+\ln\sigma_n$. A companion item asserts that the RWRE exists for every law of $\alpha_0$ on $[0,1]$.

Significance

The theorem classifies the long-run behaviour of the RWRE on $\mathbb Z$ by a condition on the law of a single site variable, with no moment assumption. It shows that the averaged drift $E\alpha_0-E\beta_0$ is not the right quantity: a walk can be recurrent or transient to the left while its average step is positive, because the criterion involves $E\ln\sigma$, a geometric rather than arithmetic mean. The criterion is the starting point for the speed law (Theorem (1.16) of the same paper), for the limit laws of Kesten–Kozlov–Spitzer and Sinai, and for the large-deviation theory of RWRE.

Solomon's results are proved; none of them, nor the fixed-environment criterion of Chung, is formalized in Lean. This mission produces machine-checked statements of the full trichotomy including the boundary cases $\sigma\in\{0,\infty\}$, of the classical hitting-probability formulas for birth–death chains on $\mathbb Z$, and of the fluctuation-theory criterion with infinite-valued expectations allowed.

Difficulty

The naive approach applies the law of large numbers to $X_n$; it fails because the increments $X_{j}-X_{j-1}$ are neither independent nor stationary once the environment is averaged out. The argument must instead pass through a fixed environment, where the criterion of Lemma (1.5) involves the full random series $\sum\rho_n$ and $\sum\rho_{-n}^{-1}$, and then decide when these series converge almost surely. That step requires fluctuation theory for $\ln\rho_n=\sum_{k\le n}\ln\sigma_k$, a random walk whose steps may be infinite and may have no mean. In Lean, the main missing infrastructure is the fluctuation-theory criterion $\sum\frac1nP(S_n>0)<\infty\iff S_n\to-\infty$, which Mathlib does not have, and the transfer from quenched to annealed statements for a process defined only through its cylinder laws.

Formalization scope

Everything lives in the namespace SolomonRWRE.Recurrence. The fixed-environment chain is IsChainInEnv P a i X, specified by its cylinder probabilities. The RWRE is IsRWRE P α X on an arbitrary probability space: measurable $\alpha_n$ with values in $[0,1]$ at every outcome, iIndepFun α P, identically distributed, and the joint cylinder law above. $\sigma_n$, $\rho_n$, $f_{ij}$ and all series are in $[0,\infty]$ (ℝ≥0∞), so "$<\infty$" and "$=\infty$" are literal; series over $n\ge1$ are indexed by $n+1$ in Lean. $\ln\sigma$ and $S_n$ are extended reals, $E(\ln\sigma)$ is the difference of two lower Lebesgue integrals, and "defined" means one of them is finite. Recurrence is always stated in the paper's "in fact" form: $\liminf X_n=-\infty$ and $\limsup X_n=+\infty$. "Correspond respectively" is formalized as three equivalences between the series conditions and the sign conditions.

Two trivializing formalizations are ruled out. Without nondegeneracy ($\alpha\equiv\frac12$) both series vanish and (i), (ii) would contradict each other; the hypothesis is part of every statement that needs it. A cylinder law that cannot be met would make every theorem vacuous; a sorry-free check confirms that the environment $\alpha\equiv1$ with $X_n=n$ satisfies IsRWRE, and the companion item asserts existence for every law of $\alpha_0$. The page's alternative "$0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$" is kept, since a single range $[0,1]$ would let $0\cdot\infty=0$ change $\rho_n$.

Needed infrastructure: hitting probabilities of birth–death chains (reusable for any nearest-neighbour chain), the fluctuation-theory criterion for i.i.d. sums with extended values (reusable throughout applied probability), and a quenched-to-annealed transfer lemma. Contributions to any of these are welcome.

Selected references

• F. Solomon, Random walks in a random environment, The Annals of Probability 3(1):1–31, 1975. https://doi.org/10.1214/aop/1176996444
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, Berlin, 1960 (pp. 65–71; reference [1] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
• K. L. Chung, A Course in Probability Theory, Harcourt, Brace and World, New York, 1968 (Ch. 8; reference [2] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
• H. Kesten, M. V. Kozlov, F. Spitzer, A limit law for random walk in a random environment, Compositio Mathematica 30(2):145–168, 1975. http://www.numdam.org/item/CM_1975__30_2_145_0/
• Ya. G. Sinai, The limiting behavior of a one-dimensional random walk in a random medium, Theory of Probability and its Applications 27(2):256–268, 1982. https://doi.org/10.1137/1127028
• O. Zeitouni, Random walks in random environment, Lectures on Probability Theory and Statistics (Saint-Flour 2001), Lecture Notes in Mathematics 1837, Springer, 2004. https://doi.org/10.1007/978-3-540-39874-5_2

Motivation

Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6

Setting

Fix a dimension $n$, an integer $d$ with $0\le d\le n$, and a vector $r\in\mathbb R^n$. Draw a random $d$-dimensional subspace $U$ from the distribution invariant under orthogonal transformations. Let $p$ be the Euclidean orthogonal projection of $r$ onto $U$, and put $q=r-p$, its projection onto $U^\perp$. The matrix $P=\operatorname{diag}(p)$ turns the vector $q$ into the coordinatewise product $Pq=(p_jq_j)_{j=1}^n$.

For a coordinate vector $z$, let $z^-=(\min\{z_j,0\})_{j=1}^n$ and $\|z\|^-_\infty=\|z^-\|_\infty$. Thus $\|Pq\|^-_\infty$ records the magnitude of the largest negative coordinate of $Pq$. An unsubscripted vector norm is always the Euclidean $\ell_2$ norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2

The formal model samples an $(n-d)\times n$ matrix $G$ with independent standard normal entries and sets $U=\ker G$. The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension $d$. The construction covers the endpoint cases $d=0$ and $d=n$ as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6

Formalization targets

Theorem 5

For arbitrary choices $r_n\in\mathbb R^n$ and $d_n\le n$ at each dimension, the central target is

$$\Pr\left\{\|P_nq_n\|^-_\infty\le \frac{\log n}{n}\|r_n\|_2^2\right\} \longrightarrow 1\qquad(n\longrightarrow\infty).$$

The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of $r_n$ and $d_n$ may change with $n$; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13

Source milestones

The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by $\sqrt{3\log n/n}$ with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6

Significance

The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7

The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.

Difficulty

A direct norm bound on $p$ and $q$ loses the coordinate information needed for the factor $\log n/n$. The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so $\|r\|$ is the $\ell_2$ norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated $d$-dimensional law almost surely.

Lemma 6 concerns $d,m\ge1$ and $n\ge2$, where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains $d=0$, $d=n$, and $r=0$. Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition $\varepsilon>0$. All limits are probabilities tending to one, never probability one at every finite $n$.

Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.

Selected references

• Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. DOI
• Sidney I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71, cited in the report for the Gaussian maximum estimate. DOI

Motivation

A prophet inequality compares two observers of a sequence of nonnegative random variables $X_1, \dots, X_n$. The prophet knows all values in advance and collects $X_n^* = \max(X_1, \dots, X_n)$. The gambler sees the values one at a time and must decide, irrevocably, when to stop and collect the current value. For independent variables the gambler's optimal value is at least half of $EX_n^*$, and the factor $2$ is sharp. Prophet inequalities are a basic tool in the analysis of online mechanisms, posted-price auctions and online selection problems, where the gambler's rule is a pricing policy and the prophet is the offline optimum.

Optimal stopping rules are often difficult to compute and to implement. A threshold rule, which stops at the first value at least $c$, is a posted price, and is the form used in applications. Samuel-Cahn (Ann. Probab. 12 (1984) 1213–1216) proved that a threshold rule alone attains the factor $2$: with $m$ a median of $X_n^*$, Theorem 1 of the paper gives $EX_n^* \le 2E^+X_{s(m)}$ or $EX_n^* \le 2E^+X_{t(m)}$. Mission I of this series formalizes that theorem.

Timeline (as recounted on p. 1213 of the paper).

• 1978: Krengel and Sucheston show $EX_n^* \le 2V_n(\underline X)$, where $V_n$ is the optimal stopping value, for independent $X_i \ge 0$; the constant $2$ cannot be improved for any $n \ge 2$.
• 1981: Hill and Kertz show that strict inequality holds in all but trivial cases.
• 1982: Hill and Kertz show that for i.i.d. $X_i$ the best constant $\alpha_n$ for optimal rules depends on $n$ and is bounded by $1.6$.
• 1983: Kertz (unpublished at the time) proves $\lim \alpha_n = 1 + a^* = 1.341\ldots$ for a constant $a^*$ given by an integral equation.
• 1984: Samuel-Cahn shows that a median threshold rule achieves the factor $2$ (Theorem 1), and that for threshold rules the factor $2$ cannot be lowered even for i.i.d. variables (Theorem 2). This mission is Theorem 2.

Setting

Fix $n \ge 1$ and a probability law $\mu$ on $[0, \infty)$. Let $X_1, \dots, X_n$ be independent with common law $\mu$, and $X_n^* = \max(X_1, \dots, X_n)$. For a constant $c \ge 0$ the threshold rules are

• $t(c)$: the smallest $i < n$ with $X_i \ge c$, and $t(c) = n$ otherwise;
• $s(c)$: the smallest $i < n$ with $X_i > c$, and $s(c) = n$ otherwise.

The stopped value is $X_{t(c)}$ or $X_{s(c)}$. The truncated expectations are $E^+X_{t(c)} = E[X_{t(c)} I(X_{t(c)} \ge c)]$ and $E^+X_{s(c)} = E[X_{s(c)} I(X_{s(c)} > c)]$: they discard the forced stop at time $n$ below the threshold. The class $T_n^*$ is the set of all $t(c)$ and $s(c)$ with $c \ge 0$.

The lower half of the theorem uses an explicit family. For $0 < a < 1$, $b > 0$, $c > 0$ and $n > b + c$, the variables $X_i^{(n)}$ take the values $0$, $a$, $1$ with probabilities $1 - (b+c)/n$, $c/n$, $b/n$. Two constants enter:

$$a^* = \frac{c(1 - e^{-b}) - b e^{-b}(1 - e^{-c})}{c(1 - e^{-b-c})}, \qquad Q(b, c) = 1 + \frac{e^{-b} - e^{-b-c}}{1 - e^{-b-c}} - \frac{b(e^{-b} - e^{-b-c})^2}{c(1 - e^{-b-c})(1 - e^{-b})}.$$

This $a^*$ is unrelated to the $a^*$ of the NOTE in §1 of the paper.

In Lean (SamuelCahnProphet.IID), a sample is x : Fin n → ℝ under iidLaw μ n, the product measure; tIdx x c and sIdx x c are $t(c)$ and $s(c)$; Emax, EstopT, EstopS, EplusT, EplusS are $EX_n^*$, $EX_{t(c)}$, $EX_{s(c)}$ and the $E^+$ terms; supE and supEplus are the two suprema over $T_n^*$; threePoint n a b c is the law of $X_i^{(n)}$; aStarIID and Q are the constants above.

Formalization targets

Goal: Theorem 2 (p. 1215)

$$\sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} E^+X_t}\right] = \sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} EX_t}\right] = 2,$$

over i.i.d. nonnegative $\underline X$. It is stated as three facts: $EX_n^* \le 2 \sup_{T_n^*} E^+X_t$ for every $n$ and law; $\sup_{T_n^*} E^+X_t \le \sup_{T_n^*} EX_t$; and for every $\varepsilon > 0$ some $n$ and law with $(2 - \varepsilon)\sup_{T_n^*} EX_t < EX_n^*$.

Milestones (proof of Theorem 2, p. 1215)

1. The upper bound $EX_n^* \le 2\sup_{T_n^*} E^+X_t$, attributed to Theorem 1.
2. $\lim_n EX_n^{(n)*} = 1 - e^{-b} + a\{e^{-b} - e^{-b-c}\}$.
3. For the three-point law, $\sup_{T_n^*} EX_t = \max\{EX_{t(a)}, EX_{t(1)}\}$.
4. $W(a) = \lim_n EX^{(n)}_{t(a)} = (1 - e^{-b-c})(b + ac)/(b + c)$.
5. $W(1) = \lim_n EX^{(n)}_{t(1)} = 1 - e^{-b}$.
6. $W(a^*) = W(1)$ and $0 < a^* < 1$.
7. With $a = a^*$, $\lim_n EX_n^{(n)*}/\sup_{T_n^*} EX_t^{(n)} = Q(b, c)$.
8. $Q(b, c) \to 2$ as $b \to 0^+$ and $c \to \infty$.

Significance

Theorem 1 says a posted price recovers half of the prophet's value. Theorem 2 says this guarantee is tight within the class of threshold rules even under the most favourable independence structure, identical distributions. This matters because for optimal rules the i.i.d. constant is at most $1.6$ (Hill and Kertz 1982); the theorem separates threshold rules from optimal rules in the i.i.d. case and sets the benchmark that later single-threshold and order-selection analyses compare against.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces one: a formal model of threshold rules on an i.i.d. sample, exact asymptotics of the expected maximum and of two stopped values for a triangular array of three-point laws, the reduction of the class $T_n^*$ to two rules, and the two-parameter limit. The upper bound (milestone 1) is the i.i.d. case of mission I's goal, and may later be closed by reference to it.

Difficulty

The limits are "easily seen" on the page, but each requires controlling $(1 - x/n)^{n-1}$ uniformly with the exact law of a stopped index on a product space, including the forced stop at $n$ whose contribution vanishes only in the limit. Milestone 3 is a finite claim over an uncountable family of rules: every $t(c)$ and $s(c)$ with $c \ge 0$ must be shown to coincide almost surely with one of $t(0)$, $t(a)$, $t(1)$ or stopping at $n$, and the first and last must be shown dominated by $t(a)$ for every finite $n > b + c$, not only asymptotically. The final step is a joint limit in $(b, c)$, in which $b/(1 - e^{-b}) \to 1$ while the correction term vanishes like $1/c$; an iterated limit is not the statement.

Formalization scope

The i.i.d. variables are the coordinates of $\mathbb R^n$ under the product measure $\mu^{\otimes n}$; all quantities depend only on the joint law, so the supremum over $\underline X$ is a supremum over laws $\mu$ with $\mu((-\infty, 0)) = 0$. Indices are 0-based in Fin n with [NeZero n], the paper's index $n$ being ⊤. Expectations are lintegrals of ENNReal.ofReal in $[0, \infty]$: no integrability is assumed and $EX_n^* = \infty$ is allowed. The sup over $T_n^*$ ranges over $c \ge 0$ and over both families $t(c)$ and $s(c)$. Limits along the triangular array are indexed by $n = k + 1$ and taken in $\mathbb R$ after toReal; the early terms with $n \le b + c$, where the clipped weights of threePoint do not form a probability measure, do not affect any limit.

The page's ratios are not written literally: in $[0, \infty]$ the quotients $0/0$ and $\infty/\infty$ take junk values, so a literal supremum of ratios would be decided by degenerate laws. The goal's third fact uses a strict inequality and requires an explicit probability law on $[0, \infty)$, which rules out the Dirac mass at $0$ and sub-probability witnesses.

A complete development needs: the law of the first index of a product sample entering a set, expectations of finite-valued functions under Measure.pi, the limit $(1 - x/n)^n \to e^{-x}$ along a triangular array, and elementary bounds on the exponential. The first two are reusable for any threshold or secretary-type stopping problem on i.i.d. samples. Proofs of the milestones in any order are welcome, as is a proof of the upper bound that does not route through the median.

Selected references

• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12(4) (1984) 1213–1216. https://doi.org/10.1214/aop/1176993150
• U. Krengel and L. Sucheston, On semiamarts, amarts, and processes with finite value, in Probability on Banach Spaces, Adv. Probab. Related Topics 4, Dekker, New York (1978) 197–266.
• T. P. Hill and R. P. Kertz, Ratio comparisons of supremum and stop rule expectations, Z. Wahrsch. verw. Gebiete 56 (1981) 283–285. https://doi.org/10.1007/BF00536175
• T. P. Hill and R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Ann. Probab. 10(2) (1982) 336–345. https://doi.org/10.1214/aop/1176993861

Motivation

Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.

Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).

Setting

There are $m$ major players $M = \{1, \dots, m\}$ with weights $w_1, \dots, w_m \ge 0$, and $w(S) = \sum_{j \in S} w_j$. The ocean is the interval $I = [0,1]$ with Lebesgue measure, carrying total weight $\alpha > 0$. In the oceanic game $[c; w_1, \dots, w_m; \alpha]$ with quota $c$, a coalition wins when the weight of its major players plus $\alpha$ times its share of the ocean is at least $c$.

The random order is modelled by a uniform random point $x = (x_1, \dots, x_m)$ of the cube $I^m$: major player $j$ is inserted into the ocean at position $x_j$, and $P(t) = \{ j : x_j < t \}$ is the set of major players placed before position $t$. Player $i$ is pivotal when

$$w(P(x_i)) + \alpha x_i \le c \le w(P(x_i)) + w_i + \alpha x_i, \qquad (2.4)$$

and the value $\varphi_i$ of player $i$ is the probability of (2.4), i.e. the volume of the set $A_i \subseteq I^m$ where it holds. The combined value of the ocean is $\Phi = 1 - \sum_{i} \varphi_i$ (2.5).

With the quota $y$ as a variable, $\Gamma(y) = [y; w_1, \dots, w_m; \alpha]$ has values $\varphi_i(y)$, $\Phi(y)$, and the pivot location $F(y) = \inf\{t \ge 0 : w(P(t)) + \alpha t \ge y\}$ is a random, nondecreasing, piecewise linear function of $y$ with expectation $E\{F(y)\}$. Adding a major player $m+1$ of weight $w_{m+1}$ gives the game $\Gamma^+$.

The game is interior when

$$w(M) \le c \le \alpha,$$

that is, the ocean alone wins and the major players together lose. With $\bar w_j = \alpha - w_j$, define $\pi(S) = \prod_{j \in S} \tfrac{w_j}{\alpha} \prod_{j \in M - S} \tfrac{\bar w_j}{\alpha}$ for $S \subseteq M$, the analogous product $\pi_i(S)$ over $M - \{i\}$ for $S \subseteq M - \{i\}$, and the integers $a_0 = 1$, $a_n = 1 - n a_{n-1}$, i.e. $1, 0, 1, -2, 9, -44, \dots$

Formalization targets

Goal: Theorem 6 (p. 20)

In an interior game, with $s = |S|$,

$$\varphi_i = \frac{w_i}{\alpha} \sum_{S \subseteq M - \{i\}} a_s \, \pi_i(S), \qquad \Phi = \sum_{S \subseteq M} a_s \, \pi(S).$$

Both identities are part of the goal. The values do not depend on $c$ within the interior range.

Milestones

1. §2, p. 5: the pivot sets $A_1, \dots, A_m$ overlap only in measure zero.
2. (4.3): $\varphi_i(y) = \operatorname{Prob}\{F(y) = x_i\}$ for $0 \le y \le w(M) + \alpha$.
3. (4.4)–(4.5): for $0 < y < w(M) + \alpha$, $F$ is differentiable at $y$ almost surely, $\sum_i \varphi_i(y) = \operatorname{Prob}\{F'(y) = 0\}$ and $\Phi(y) = \operatorname{Prob}\{F'(y) = 1/\alpha\}$.
4. Theorem 2, (4.7): $\Phi(y) = \alpha \, \frac{d}{dy} E\{F(y)\}$.
5. Lemma, (4.12)–(4.13): $\varphi^+_{m+1}(z) = \frac{1}{\alpha} \int_{t_1}^{t_2} \Phi(y)\, dy$ with $t_1 = \max(z - w_{m+1}, 0)$, $t_2 = \min(z, w(M) + \alpha)$.
6. Theorem 5, (5.4): if $[c; w_1, \dots, w_m; \alpha]$ and $[d; w_1, \dots, w_{m+1}; \alpha]$ are both interior, $\varphi^+_{m+1} = \frac{1}{\alpha} \Phi w_{m+1}$.
7. Proof of Theorem 6, p. 21: the right-hand sides above add up to 1, an identity valid for all real $w_j$ and $\alpha \ne 0$.

Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ($|a_n|$ is the nearest integer to $n!/e$ and counts derangements).

Significance

Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios $w_j/\alpha$. Table 1 of the memorandum lists the cases $m \le 3$, and the theorem gives every $m$. Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.

The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.

Difficulty

The values are volumes of regions of $I^m$ cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into $m!$ order cells, with the quota $c$ entering each. The paper's route avoids this by passing through the random function $F$, Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in $y$, with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of $[0, w(M) + \alpha]$. Theorem 6 is then an induction on $m$ that uses Theorem 5 for every player in turn, so it also needs the invariance of $\varphi_i$ under a relabelling of the major players.

Formalization scope

• Major players are Fin m ($m = 0$ is allowed; then $\Phi = 1$). The probability of an event is the Lebesgue volume of its intersection with $[0,1]^m$; no probability space is built.
• $P(t)$ uses the strict inequality $x_j < t$, as printed.
• $\varphi_i$ is defined as the volume of the pivot set (2.4), for every real quota. $\Phi$ is defined by (2.5), as the paper allows ("We might equally well take (2.5) as the definition of $\Phi$"). Neither is defined through the formulas of Theorem 6 or through $F$; defining them that way would make the goal an unfolding, and is ruled out.
• The paper writes (4.2) as a minimum $F(y) = \min\{x \mid w(P(x)) + \alpha x \ge y\}$, which need not be attained; $F$ is the infimum over $t \ge 0$, the value shown in its Fig. 3.
• The standing assumptions $w_j \ge 0$ and $\alpha > 0$ (§2) are explicit hypotheses. The p. 5 footnote's $0 \le c \le w(M)+\alpha$ applies to the pivot-set milestone. Other quota ranges are explicit: $0 \le y \le w(M) + \alpha$ for (4.3) and Theorem 2 (one-sided derivatives at the ends), the open interval for (4.4)–(4.5) (two-sided derivatives, stated with HasDerivAt), and $0 \le z \le w(M) + w_{m+1} + \alpha$ for the Lemma, as on p. 14.
• The added player is appended with Fin.snoc as index Fin.last m.
• Corollary (5.5) assumes $w_i > 0$, since it divides by $w_i$. Theorem 4, stated in the paper "in the general oceanic game", is false at quota $0$ and when the limit game has no winning coalition; it is stated for $0 < c \le w(M - \{i\}) + \alpha$.
• The identity of milestone 7 is pure algebra and is stated for all real weights and $\alpha \ne 0$.

A complete development needs: measurability of the pivot sets and of $F$ in $x$, the structure of $F$ as a piecewise linear function of $y$, differentiation of $E\{F\}$, and invariance of the values under permutations of the major players. The pivot-set and $F$ infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.

Selected references

• J. W. Milnor and L. S. Shapley, Values of Large Games, II: Oceanic Games, The RAND Corporation, Research Memorandum RM-2649, February 1961. https://www.rand.org/pubs/research_memoranda/RM2649.html
• J. W. Milnor and L. S. Shapley, Values of Large Games II: Oceanic Games, Mathematics of Operations Research 3(4):290–307, 1978. https://doi.org/10.1287/moor.3.4.290
• L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, 307–317. https://doi.org/10.1515/9781400881970-018
• L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, The RAND Corporation, Research Memorandum RM-2648, November 1960.
• R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080

Motivation

Many problems in statistics and engineering ask for the level $\theta$ at which an unknown function takes a prescribed value $\alpha$: the dose at which a fraction $\alpha$ of subjects respond, the setting at which a noisy device reaches a target output, the $\alpha$-quantile of a distribution that can only be probed by yes/no experiments. When the function can only be observed through noisy measurements, classical root-finding does not apply. Robbins and Monro (Ann. Math. Statist. 22 (1951) 400–407) proposed a recursive procedure that uses one noisy observation per step and proved that it converges in mean square. The paper started the field of stochastic approximation, which today underlies stochastic gradient descent, temporal-difference learning and adaptive control.

Timeline. Robbins and Monro (1951) prove mean-square convergence for bounded responses under conditions (5′) or (33)–(35). Kiefer and Wolfowitz (1952) adapt the scheme to finding a maximum. Blum (1954) proves almost-sure convergence under weaker moment conditions. Dvoretzky (1956) gives a general convergence theorem covering both schemes. Later work (Robbins and Siegmund, 1971; Ljung, 1977; Kushner and Clark, 1978; Benaïm, 1999) develops the supermartingale and ODE methods.

Setting

To each real level $x$ corresponds a random response $Y(x)$ with distribution function $H(y \mid x)$, and the regression function is

$$M(x) = \int_{-\infty}^{\infty} y \, dH(y \mid x).$$

The responses are bounded: there is $C > 0$ with $\Pr[|Y(x)| \le C] = 1$ for all $x$ (condition (4)). Fix constants $\alpha, \theta$ and positive step sizes $a_n$. The Robbins–Monro process starts at an arbitrary constant $x_1$ and sets

$$x_{n+1} - x_n = a_n(\alpha - y_n), \qquad \Pr[y_n \le y \mid x_n] = H(y \mid x_n),$$

so $y_n$ is a fresh response observed at the current level $x_n$. The quantity of interest is the mean squared error $b_n = E(x_n - \theta)^2$.

A sequence $\{a_n\}$ is of type $1/n$ if

$$\sum_{n=1}^{\infty} a_n^2 < \infty \quad (6), \qquad \sum_{n=2}^{\infty} \frac{a_n}{a_1 + \cdots + a_{n-1}} = \infty \quad (26);$$

$a_n = 1/n$ is the standard example. The proof also uses $d_n = E[(x_n-\theta)(M(x_n)-\alpha)]$, $e_n = E[\int (y-\alpha)^2\,dH(y\mid x_n)]$ and $A_n = |x_1 - \theta| + [C+|\alpha|](a_1 + \cdots + a_{n-1})$.

Formalization targets

Goal: Theorem 2 (p. 405)

If $\{a_n\}$ is of type $1/n$, (4) holds, and $M$ is nondecreasing with $M(\theta) = \alpha$ and $M'(\theta) > 0$, then, whatever $x_1$,

$$\lim_{n \to \infty} E(x_n - \theta)^2 = 0.$$

Milestones

1. The one-step identity (14): $b_{n+1} - b_n = a_n^2 e_n - 2a_n d_n$.
2. The signs and bound after (14): $d_n \ge 0$ and $0 \le e_n \le [C+|\alpha|]^2$.
3. (17)–(18): $\sum a_n^2e_n$ and $\sum a_n d_n$ converge, and $b = \lim b_n = b_1 + \sum a_n^2e_n - 2\sum a_nd_n$ exists with $b \ge 0$.
4. Lemma 1: if $d_n \ge k_n b_n$ with $k_n \ge 0$ and $\sum a_n k_n = \infty$, then $b = 0$.
5. (22): $\Pr[|x_n - \theta| \le A_n] = 1$.
6. (24): $d_n \ge \bar k_n b_n$, where $\bar k_n$ is the infimum of $(M(x)-\alpha)/(x-\theta)$ over $0 < |x-\theta| \le A_n$.
7. (27): (26) implies $\sum a_n = \infty$.
8. Lemma 2: if $\bar k_n \ge K/A_n$ for some $K > 0$ and large $n$, and (26) holds, then $b = 0$.
9. (42): under (33)–(35), $(M(x)-\alpha)/(x-\theta) \ge \delta M'(\theta)/2A_n$ on $0 < |x-\theta| \le A_n$.

Companion results

Theorem 1 (p. 404: the same conclusion under (5′), $M(x) \le \alpha - \delta$ for $x < \theta$ and $M(x) \ge \alpha + \delta$ for $x > \theta$); convergence in probability under the hypotheses of Theorem 2 (p. 401); the quantile estimator of §4, (48); and (30), that $c'/n \le a_n \le c''/n$ gives a sequence of type $1/n$.

Significance

Theorem 2 is the first convergence theorem for a recursive root-finding procedure under noise. It shows that a procedure using no knowledge of $M$ or of the noise distribution, beyond a monotone crossing and a positive slope at the root, is consistent. Section 4 turns it into a distribution-free consistent estimator of a quantile from response/nonresponse data, the up-and-down designs of bioassay and sensitivity testing. Its step-size conditions, $\sum a_n^2 < \infty$ with a divergence condition, remain the standard conditions for stochastic gradient methods.

The theorem has been proved since 1951 and strengthened many times. As far as is known it has no machine-checked proof, and Mathlib has no stochastic approximation theory. Formalizing it requires conditional laws given by Markov kernels, integration against a composition of a measure with a kernel, and deterministic series arguments. A finished formalization would be a base for formalizing the almost-sure theorems (Blum, Robbins–Siegmund) and the ODE method.

Difficulty

The obvious argument fails at one step. Monotonicity of $M$ and a positive derivative at $\theta$ do not give a uniform positive lower bound on the slope $(M(x)-\alpha)/(x-\theta)$: away from $\theta$ the slope can decay to $0$, for example when $M$ is bounded, as (4) forces. So the drift towards $\theta$ is not uniformly strong, and the newcomer's first idea, a uniform contraction $b_{n+1} \le (1 - c\,a_n) b_n + O(a_n^2)$, is not available under (33)–(35). This is why the theorem needs the divergence condition (26), which is stronger than $\sum a_n = \infty$, and not only (6). On the formal side, the expectations come from integrating against the joint law of $(x_n, y_n)$, and they need integrability bounds before any identity can be used.

Formalization scope

Everything is in the namespace RobbinsMonroSA.Conv, over a probability space $(\Omega, P)$ with IsProbabilityMeasure P. Indices are 0-based: Lean's x 0, a 0 are the paper's $x_1$, $a_1$, and Lean's bigA … n is the paper's $A_{n+1}$. The committed conventions are:

• $H$ is a Kernel ℝ ℝ with IsMarkovKernel H (each $H(\cdot\mid x)$ is a probability law, measurable in $x$).
• (4) is 0 < C ∧ ∀ x, H x [-C, C] = 1. It is a hypothesis of every item that mentions an expectation, and it is what keeps the Bochner integrals defining $b_n$, $d_n$, $e_n$ and $M$ from defaulting to $0$.
• (8) is the joint-law equation: the law of $(x_n, y_n)$ is the law of $x_n$ composed with $H$. (7) holds surely, and $x_n$, $y_n$ are measurable. No Markov property or filtration beyond (8) is assumed.
• Every "$= \infty$" for a series ((19), (26), (27)) is divergence of partial sums to $+\infty$. "$b = 0$" is $b_n \to 0$.
• $M'(\theta) > 0$ is HasDerivAt M M' θ with 0 < M'.
• The infimum $\bar k_n$ of (23) is never formed. (24) and (25) are stated with lower bounds on $(M(z)-\alpha)/(z-\theta)$ over $0<|z-\theta|\le A_n$. This avoids the junk value $0$ that Lean's real infimum gives on the empty range ($A_n = 0$), where the paper's infimum is $+\infty$.

The standing assumptions of §3, (4), (5) and (6), are hypotheses of Lemma 1, Lemma 2 and the displays of §3 whose proofs use them. In Theorems 1 and 2, (5) follows from (5′) or from (33)–(34), and (6) is part of "type $1/n$".

The goal cannot be trivialized. It mentions neither $d_n$, $e_n$, $A_n$ nor any constant, and the process must satisfy (8) for every $n$. Without (8), $y_n$ would be arbitrary and the statement false; with $y_n = M(x_n)$ it would be deterministic.

Contributions welcome: proofs of the milestones, reusable lemmas on integrating against μ ⊗ₘ κ, and a proof that $a_n = 1/n$ satisfies (26).

Selected references

• H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
• J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23 (1952), 462–466. https://doi.org/10.1214/aoms/1177729392
• J. R. Blum, Approximation methods which converge with probability one, Ann. Math. Statist. 25 (1954), 382–386. https://doi.org/10.1214/aoms/1177728794
• A. Dvoretzky, On stochastic approximation, Proc. Third Berkeley Symp. Math. Statist. Prob. 1 (1956), 39–55. https://projecteuclid.org/euclid.bsmsp/1200501645
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics (1971), 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709 (1999), 1–68. https://doi.org/10.1007/BFb0096509

Motivation

The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every $n$, not just in the limit.

Timeline.

• 1933–1944. Kolmogorov and Smirnov introduce the statistics, prove that their laws do not depend on the continuous distribution, and find the limit laws, e.g. $\lim_n P(D_n^->\lambda)=\exp(-2\lambda^2)$. Smirnov (1944) also gives the exact law of the one-sided statistic and the expansion $P(D_n^->\lambda)=\exp(-2\lambda^2)\bigl(1-\frac{2\lambda}{3\sqrt n}+O(n^{-1})\bigr)$.
• 1956. Dvoretzky, Kiefer and Wolfowitz prove $P(D_n^->\lambda)\le C\exp(-2\lambda^2)$ for every $n$, with an unspecified constant $C$ (Ann. Math. Statist. 27).
• 1958. Birnbaum and McCarty conjecture that $C=1$ is admissible.
• 1979–1985. Explicit constants: $C\le306$ (Devroye and Wise), $C\le29$ (Shorack and Wellner), $C\le2\sqrt2$ (Hu).
• 1990. Massart proves the conjecture under a mild lower bound on $\lambda$, and deduces the two-sided bound with the optimal constant $2$ (Ann. Probab. 18).

Setting

Let $x_1,\dots,x_n$ ($n\ge1$) be independent, identically distributed real random variables with a continuous distribution function $F$. The empirical distribution function is

$$\hat F_n(x)=\frac1n\sum_{i=1}^n\mathbb 1_{(x_i\le x)},$$

and the centred, normalised empirical process is $Z_n=\sqrt n(\hat F_n-F)$. The statistics are

$$D_n^+=\sup_{x\in\mathbb R}Z_n(x),\qquad D_n^-=\sup_{x\in\mathbb R}\bigl(-Z_n(x)\bigr),\qquad D_n=\sup_{x\in\mathbb R}|Z_n(x)|.$$

In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), $F$ is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter $\lambda$ is written l.

The proof works with Smirnov's point probabilities $p_{\lambda,n}(j)=\lambda\sqrt n\,(j+\lambda\sqrt n)^{j-1}(n-j-\lambda\sqrt n)^{n-j}n^{-n}\binom nj$, whose sum over $0\le j<n-\lambda\sqrt n$ is $P(D_n^->\lambda)$, with Csáki's density $f_\lambda(s)=\frac{\lambda}{\sqrt{2\pi}}s^{-3/2}(1-s)^{-1/2}\exp\bigl(-\frac{\lambda^2}{2s(1-s)}\bigr)$ of the first passage of a Brownian bridge at level $\lambda$, and with the ratio $C_{\lambda,n}=\exp(2\lambda^2)P(D_n^->\lambda)$.

Formalization targets

Goal: Theorem 1

For every $n\ge1$ and every $\lambda\ge\sqrt{\log(2)/2}\wedge\gamma n^{-1/6}$, with $\gamma=1.0841$,

$$P(D_n^->\lambda)\le\exp(-2\lambda^2).$$

Here $\wedge$ is the minimum. The constant $1$ in front of the exponential is the point of the theorem; the threshold on $\lambda$ is the paper's.

Milestones

The milestones follow the proof in the paper's order of attack:

1. the reduction to the uniform law, and Smirnov's exact formula (2.3);
2. the identity $\int_0^1f_\lambda=\exp(-2\lambda^2)$ (2.4);
3. the local comparison of $p_{\lambda,n}(j)$ with $f_\lambda$: (2.7), Lemma 2, Claims 1–3, and Proposition 1;
4. the midpoint bound for log-convex integrands (Lemma 3) and the closed forms of Lemma 4;
5. the nonasymptotic expansion (2.11), the negativity of its right side $\eta_n$, and with them Theorem 1 for $n\ge39$, $\lambda\le\sqrt n/2$;
6. Proposition 2 on the slope of $C_{\lambda,n}$, the crude bounds (2.13)–(2.14), and the finite grid check (2.15) for $n\le38$.

Companions

The equality in law of $D_n^+$ and $D_n^-$, Comment 1 ((1.4) whenever $\exp(-2\lambda^2)\le1/2$), the reduction $P(D_n>\lambda)\le2P(D_n^->\lambda)$, and Corollary 1:

$$P(D_n>\lambda)\le2\exp(-2\lambda^2)\qquad(\lambda>0).$$

Significance

The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, $1$ and $2$, which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.

Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified $C$. The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, $\eta_{39}$); turning those into checked certificates is part of the work.

Difficulty

The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison $P(\tau_n=t)\le\frac1nf_\lambda(t-\varepsilon/3)$ is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time $t$ is close to $\varepsilon=\lambda/\sqrt n$. Controlling that factor uniformly in $j$ while keeping the leading constant exactly $1$ is what forces the delicate constants ($\theta=0.4833$, $\beta=0.826$, $\mu=0.4345$, $\gamma=1.0841$). For small $n$ the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on $\lambda\mapsto C_{\lambda,n}$ plus a finite numerical check over a grid; neither half suffices alone.

Formalization scope

Conventions:

• $n\ge1$; the sample is indexed by Fin n; $F$ is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.
• Probabilities are measures of events in $[0,\infty]$ and are compared with ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in $[-1,1]$, hence a genuine real supremum.
• $p_{\lambda,n}(j)$ uses an integer power at $j-1$, so that $p_{\lambda,n}(0)=(1-\varepsilon)^n$. $C_{\lambda,n}$ is defined from the exact formula (2.3); it equals $\exp(2\lambda^2)P(D_n^->\lambda)$ by the (2.3) milestone, so the analytic milestones carry no probability.
• Statements that the page gives through derivatives of $C_{\lambda,n}$ (Proposition 2(i), (iii)) are stated as monotonicity and as an increment bound, because $C_{\lambda,n}$ has kinks.

Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of $j$), (2.8) (swapped numerators) and Proposition 2(i) ("$\ge0$" for nonincreasing) are corrected; Claim 2 carries the hypothesis $\varepsilon\le3s'$, without which the corrected claim is false; Lemma 3 uses strict inequalities $\delta<s<1-\delta$; Comment 1 makes the implicit $\lambda>0$ explicit; (2.14) carries Proposition 2's standing range $n\ge2$, $0<\lambda<\sqrt n$.

The goal does not mention $p_{\lambda,n}$, $f_\lambda$, $C_{\lambda,n}$, the case split at $n=39$, or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.

Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on $]0,1[$; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.

Selected references

• P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Ann. Probab. 18(3):1269–1283, 1990. https://doi.org/10.1214/aop/1176990746
• A. Dvoretzky, J. Kiefer, J. Wolfowitz, Asymptotic minimax character of the sample distribution function and of the classical multinomial estimator, Ann. Math. Statist. 27:642–669, 1956. https://doi.org/10.1214/aoms/1177728174
• Z. W. Birnbaum, R. C. McCarty, A distribution-free upper confidence bound for P(Y<X), based on independent samples of X and Y, Ann. Math. Statist. 29:558–562, 1958.
• N. V. Smirnov, Approximate laws of distribution of random variables from empirical data, Uspekhi Mat. Nauk 10:179–206, 1944.
• E. Csáki, Investigations concerning the empirical distribution function, Magyar Tud. Akad. Mat. Fiz. Oszt. Közl. 23:239–327, 1974; English translation in Selected Transl. Math. Statist. Probab. 15:229–317, 1981.
• G. R. Shorack, J. A. Wellner, Empirical Processes with Applications to Statistics, Wiley, 1986.