Probability

Motivation

Many limit theorems of probability in Banach spaces, among them the strong law of large numbers and the law of the iterated logarithm for vector-valued random variables, reduce to sharp estimates of the tail probability

$$P\Big(\Big\|\sum_{i\le N}X_i\Big\|\ge t\Big)$$

for independent random variables $X_i$ with values in a Banach space $W$. For many years these estimates were obtained with martingale methods, and they were not optimal. Chapter 13 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), explains how the isoperimetric inequalities of the earlier chapters, in particular control by $q$ points (Theorem 3.1.1), give such estimates with explicit constants.

Timeline. M. Ledoux observed (unpublished note on Gaussian randomization, reference [L] of the paper) that for Gaussian sums $\sum g_iX_i$ one may split $\|\sum g_iX_i\|$ into its conditional mean given $(X_i)$ plus a deviation, and that the conditional mean has a monotonicity property that replaces positivity arguments ([L], Eq. (13.1)–(13.2) of the paper). Ledoux and Talagrand used this to characterize the Banach-valued random variables satisfying the law of the iterated logarithm (1988). The resulting conviction that an isoperimetric principle was at work led to Talagrand's 1989 isoperimetric theorem (Ann. Probab. 17), superseded in the 1995 paper by Theorem 3.1.1. Ledoux–Talagrand, Probability in Banach Spaces (1991), Theorem 6.17, proves a variant of the bound formalized here that also allows truncation of the variables.

Setting

Let $W$ be a real Banach space with dual $W^*$, and let $X_1,\dots,X_N$ be independent (not necessarily identically distributed) $W$-valued random variables. Let $\varepsilon_1,\dots,\varepsilon_N$ be Rademacher signs: independent, independent of $(X_i)$, with $P(\varepsilon_i=1)=P(\varepsilon_i=-1)=1/2$. Following the paper, write

$$\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|=E_\varepsilon\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|+\Big(\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|-E_\varepsilon\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|\Big),$$

where $E_\varepsilon$ is expectation in the signs only. The conditional mean is $Z=E_\varepsilon\|\sum_i\varepsilon_iX_i\|$. The weak variance of a point $x=(x_i)\in W^N$ is

$$\sigma^2(x)=\sup\Big\{\sum_{i\le N}w^*(x_i)^2:\ w^*\in W^*,\ \|w^*\|\le1\Big\}.$$

The decreasing rearrangement $\|x_i\|^*=\sup\{t:\ \operatorname{card}\{j\le N:\|x_j\|\ge t\}\ge i\}$ is the $i$-th largest norm, and $\sum_{i\le k}\|x_i\|^*$ is the sum of the $k$ largest norms.

For sets $A_1,\dots,A_q\subseteq W^N$, the $q$-point distance of $x$ is

$$f(A_1,\dots,A_q,x)=\inf\big\{\operatorname{card}\{i\le N:\ x_i\notin\{y^1_i,\dots,y^q_i\}\}:\ y^l\in A_l\big\}.$$

For $b>0$ let $B=\{\sigma\le b\}$ and $k(x)=f(B,\dots,B,x)$ with $q$ copies of $B$.

Formalization targets

Goal: Theorem 13.4 (p. 200)

With $a=2E\|\sum_i\varepsilon_iX_i\|$ and $s^2=E\,\sigma^2(X)$, for all integers $q\ge2$, $k\ge0$ and $u,t>0$,

$$P\Big(\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|\ge 2aq+3t+u\Big)\le\frac{2^{q+1}}{q^{k+1}}+4\exp\Big(-\frac{u^2}{32qs^2}\Big)+2P\Big(\sum_{i\le k}\|X_i\|^*>t\Big).$$

Milestones

1. Proposition 13.1 (p. 197): for $a>0$, $P(Z\ge qa+t)\le q^{-k-1}P(Z\le a)^{-q}+P(\sum_{i\le k}\|X_i\|^*\ge t)$.
2. Proposition 13.3 (p. 199): for fixed $x\in W^N$ and $u>0$,

$$P_\varepsilon\Big(\Big\|\sum_i\varepsilon_ix_i\Big\|\ge2E_\varepsilon\Big\|\sum_i\varepsilon_ix_i\Big\|+u+\sum_{i\le k(x)}\|x_i\|^*\Big)\le4\exp\Big(-\frac{u^2}{16qb^2}\Big).$$

3. Eq. (13.14) (p. 200): the joint bound at level $2v+u+t$ combining the two.

The goal keeps the paper's explicit constants.

Significance

The result. Theorem 13.4 bounds the tail of a Rademacher sum in an arbitrary Banach space using three quantities only: the mean $E\|\sum\varepsilon_iX_i\|$, the weak variance $s^2$, and the law of the $k$ largest summands. No moment assumption on the $X_i$ beyond these is needed, and $q,k$ are free parameters to optimize. By symmetrization, such bounds are the main input for the law of large numbers and the law of the iterated logarithm in Banach spaces, for the integrability of sums, and for comparison of moments.

Formalizing it. The result is proved in the paper (and in a different form in Ledoux–Talagrand 1991). It is not formalized: Mathlib has independence, product measures and the dual of a normed space, but no Rademacher sums in Banach spaces and none of Talagrand's isoperimetric inequalities. The mission yields a machine-checked statement of the vector-valued tail bound with explicit constants, connected to the $q$-point inequality (Theorem 3.1.1, posed in mission IV of this series) and to the concentration of $\|\sum Y_iv_i\|$ for bounded $Y_i$ (Theorem 13.2, posed in mission IX).

Difficulty

The obvious approach controls $\|\sum_i\varepsilon_iX_i\|$ by its mean plus a concentration term. Bounded-difference (martingale) inequalities do not work here: the increments are $\|X_i\|$, which can be unbounded and heavy-tailed, so the resulting bound depends on $\sum\|X_i\|^2$ rather than on the much smaller weak variance $\sigma^2$. Concentration for the signs conditionally on $(X_i)$ (Theorem 13.2) gives the weak variance, but at scale $\sigma(X)$, a random quantity. The difficulty is to make both the conditional mean $Z$ and $\sigma(X)$ uniformly controlled on most of the space, at the cost of discarding only a few large summands; a single-point isoperimetric inequality does not supply this.

Formalization scope

• $W$ is a real normed space with CompleteSpace W, MeasurableSpace W and BorelSpace W; $W^*$ is W →L[ℝ] ℝ with the operator norm. $\sigma^2$ is a real ⨆ over the dual unit ball, which is nonempty and bounded above by $\sum\|x_i\|^2$.
• The $X_i$ are realized canonically on $W^N$ = Fin N → W with $P$ = Measure.pi μ for laws μ i (independent, not identically distributed). Signs are Fin N → Bool under the platform's uniform measure Komlos.spMeasure N (referenced). The joint law is the product of the two. Coordinates are 0-based; the rearrangement index is 1-based as in the paper.
• $E_\varepsilon$ is the finite average over $2^N$ sign patterns. $a$ and $s^2$ are lower Lebesgue integrals (∫⁻) in $[0,\infty]$, so they need no integrability hypothesis, and $a=\infty$ makes the goal hold with an empty event. Probabilities are in $[0,\infty]$, so $P(B)=0$ or $P(Z\le a)=0$ makes the corresponding term $+\infty$.
• The paper ignores measurability (pp. 81–82). Here measurability of $x\mapsto\|\sum\varepsilon_ix_i\|$ (each sign pattern) and of $\sigma^2$ is an explicit hypothesis; it is automatic for separable $W$.
• The paper writes $q\in\mathbf N$; statements take $q\ge2$, the range of Theorem 3.1.1, and all bounds are trivial for $q\le1$.
• The paper calls $\|x_i\|^*$ the "non-decreasing rearrangement", but its formula gives the $i$-th largest norm; the formula is formalized.
• Trivializing formalizations are ruled out: $\sigma^2$ and $E_\varepsilon$ cannot take junk values (bounded nonempty supremum, finite average), the $q$-point distance is ℕ∞-valued, and no Bochner integral of a possibly non-integrable function appears.

Needed infrastructure: Rademacher sums in Banach spaces, order statistics of finitely many reals, the $q$-point inequality on general product spaces, and Theorem 13.2 for Bernoulli variables. The rearrangement and the $q$-point distance can be reused elsewhere. Contributions are welcome on any milestone, and on proving Proposition 13.3 from a stated form of Theorem 13.2.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
• M. Ledoux, M. Talagrand, Characterization of the law of the iterated logarithm in Banach spaces, Ann. Probab. 16 (1988), 1242–1264. https://doi.org/10.1214/aop/1176991688
• M. Ledoux, M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
• M. Talagrand, Isoperimetry and integrability of the sum of independent Banach-space valued random variables, Ann. Probab. 17 (1989), 1546–1570. https://doi.org/10.1214/aop/1176991174

Motivation

A random walk in a random environment on $\mathbb Z$ moves one step right with probability $\alpha_x$ and one step left with probability $1-\alpha_x$ from site $x$, where the $\alpha_x$ are themselves i.i.d. random variables. In his 1975 paper, F. Solomon (Ann. Probab. 3(1):1–31, DOI 10.1214/aop/1176996444) decided recurrence and transience of this walk and computed its speed. Section 4 of the paper isolates a piece of that analysis: the conditional mean time for the walk to cross one bond, given the environment.

Fix the environment, make $0$ reflecting, and let $\mu_n$ be the mean first-passage time from $n$ to $n+1$. Conditioning on the first step gives $\mu_n=\sigma_n\mu_{n-1}+(\sigma_n+1)$ with $\sigma_n=(1-\alpha_n)/\alpha_n$, and $Z_n=\tfrac12(\mu_n-1)$ satisfies a linear recursion with random coefficients (p. 28). The sum $Z_1+\dots+Z_n$ is, up to an affine change, the expected time to reach level $n$ in that environment. Recursions of the same form, $Z_n=A_nZ_{n-1}+B_n$ with i.i.d. coefficients, are the random difference equations studied by Kesten (Acta Math. 131, 1973) and Vervaat (Adv. Appl. Probab. 11, 1979); they recur in queueing (waiting-time recursions), insurance (discounted cash flows, "perpetuities") and the analysis of stochastic algorithms.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\sigma_1,\sigma_2,\dots$ independent, identically distributed, nonnegative real random variables. The system of difference equations (4.1) is

$$Z_0=0,\qquad Z_n=\sigma_n\,(1+Z_{n-1}),\quad n\ge1 .$$

In the Lean development Z σ n ω is defined by this recursion (module SolomonRWRE.DiffEq.System), so it is a function of $\sigma_1,\dots,\sigma_n$ and needs no existence hypothesis. Unfolding gives the closed form (4.3), $Z_n=\sum_{j=1}^n\sigma_j\cdots\sigma_n$.

The mean is $\nu=E(\sigma)=\int\sigma_1\,dP\in[0,\infty]$ (nu P σ); $\sigma$ need not be integrable, and $\nu=\infty$ is allowed. The products are $\rho_j=\sigma_1\cdots\sigma_j$ (rho), and the block sums of the proof are

$$Y_k^n=\sum_{j=1}^{n-k+1}\ \prod_{i=j}^{j+k-1}\sigma_i \qquad(\texttt{Y σ k n}),$$

the sums of the products of $k$ consecutive $\sigma$'s inside $\sigma_1,\dots,\sigma_n$. For one step of the proof the sequence is extended to a two-sided i.i.d. family $\{\sigma_j\}_{j\in\mathbb Z}$ (module TwoSided), with $S_n=\sum_{j=-\infty}^n\sigma_j\cdots\sigma_n\in[0,\infty]$.

Formalization targets

Goal: Theorem (4.4)

$$\lim_{n\to\infty}\frac{Z_1+\dots+Z_n}{n}=\begin{cases}\dfrac{\nu}{1-\nu}, & \nu<1,\\[2mm] \infty, & \nu\ge1,\end{cases}\qquad\text{almost surely.}$$

The goal fixes nothing beyond the paper's hypotheses: any law on $[0,\infty)$, integrable or not. Both cases are almost-sure limits.

Milestones, in the order of the proof (pp. 28–29)

1. The closed form (4.3), $Z_n=\sum_{j=1}^n\sigma_j\cdots\sigma_n$.
2. The regrouping $Z_1+\dots+Z_n=Y_1^n+\dots+Y_n^n$.
3. For fixed $k\ge1$, $Y_k^n/n\to\nu^k$ almost surely, in $[0,\infty]$.
4. $\liminf_n (Z_1+\dots+Z_n)/n\ge\sum_{k\ge1}\nu^k$ almost surely, which settles $\nu\ge1$.
5. For a two-sided family, $Z_n\le S_n$ pathwise, and $S_n<\infty$ almost surely when $\nu<1$.
6. For $\nu<1$, $\limsup_n\frac1n\sum_{k=1}^nZ_k\le\nu/(1-\nu)$ almost surely.

Companion: Lemma (4.2)(i)–(ii)

If $\sum_n n^{-1}P(\rho_n>1)<\infty$ then $\sum_j\rho_j<\infty$ a.s. and $Z_n$ converges in law to $\sum_j\rho_j$; if the series diverges, $Z_n\to\infty$ in probability; when $E(\ln\sigma)$ is defined, the two cases are $E(\ln\sigma)<0$ and $E(\ln\sigma)\ge0$.

Significance

The result. Theorem (4.4) gives the almost-sure growth rate of the cumulative mean passage time of a random walk in a random environment: linear with slope $\nu/(1-\nu)$ when $E(\sigma)<1$, superlinear otherwise. This is the averaged counterpart of the speed law of §1 of the paper (Theorem (1.16)), where the limiting speed $(1-E\sigma)/(1+E\sigma)$ is exactly the reciprocal of $1+2\nu/(1-\nu)$. The superlinear case $\nu\ge1$ is the starting point of the paper's §4 limit laws for $f(n)(Z_1+\dots+Z_n)$ (Lemma (4.5) to Theorem (4.9)), which are stated without proof. Lemma (4.2) concerns the single variable $Z_n$, and its dichotomy is a statement about perpetuities $\sum_j\sigma_1\cdots\sigma_j$.

Formalizing it. The theorem has been proved since 1975; what this mission adds is a machine-checked proof. No result about random difference equations, random products, or this paper is on the platform. The proof needs, for a nonnegative stationary ergodic sequence with possibly infinite mean, the almost-sure convergence of averages in $[0,\infty]$. That convergence is not in Mathlib in this form (Mathlib has the i.i.d. strong law for integrable variables, ProbabilityTheory.strong_law_ae), and Birkhoff's pointwise ergodic theorem is posed on the platform as an open item (Birkhoff1931.tendsto_birkhoffAverage_condExp). A completed mission therefore leaves behind a nonnegative, infinite-mean ergodic theorem for block products of i.i.d. sequences, which is reusable well beyond this paper.

Difficulty

The obvious argument fails at independence. $Z_n$ is a sum of products sharing the factor $\sigma_n$, so $Z_1,Z_2,\dots$ are neither independent nor stationary, and no law of large numbers applies to them directly. The regrouping into $Y_k^n$ produces sums of $k$-dependent block products, which are stationary but not independent, so the i.i.d. strong law does not apply either. Moreover there are $n$ such groups at time $n$, so letting $k$ and $n$ grow together needs a uniform argument: Fatou's lemma gives only the lower bound. The upper bound requires a different object, $S_n$, which is stationary because it looks infinitely far into the past, and it exists only because $\nu<1$ makes the backward series converge. A second trap is the infinite-mean case: $\sigma$ may be non-integrable, and every integrability-based ergodic or strong-law statement must be adapted to nonnegative variables with values in $[0,\infty]$.

Formalization scope

• Driving sequence. σ : ℕ → Ω → ℝ; the hypotheses (IsIIDNonneg) are on $\sigma_1,\sigma_2,\dots$ (the shifted family n ↦ σ (n + 1)): measurable, pointwise nonnegative, mutually independent (iIndepFun), and identically distributed with $\sigma_1$ (IdentDistrib). $\sigma_0$ is unused and unconstrained.
• Expectations are lower Lebesgue integrals in $[0,\infty]$ (∫⁻). A Bochner integral would return $0$ for a non-integrable $\sigma$, which would put $\nu=0<1$ and make the goal false; this trivializing reading is excluded by the definition of nu.
• Limits are taken in $[0,\infty]$: the averages are mapped there by ENNReal.ofReal, which loses nothing because $Z_k\ge0$. In the case $\nu<1$, $\nu/(1-\nu)$ is computed in $[0,\infty]$ and is finite.
• Indices. The sums start at $k=1$ (Finset.Icc 1 n); in $Y_k^n$ the upper limit $n+1-k$ uses natural-number subtraction, which gives the empty sum for $k>n$.
• Two-sided family. Milestone 5 is stated for a separate predicate IsIIDNonnegZ on σ : ℤ → Ω → ℝ; $Z_n$ is computed from its restriction to $\mathbb N$. This mirrors the page's "without loss of generality"; the goal keeps the one-sided family.
• Lemma (4.2). One hypothesis is added: $\sigma_1$ is not almost surely $1$. For $\sigma\equiv1$ the series $\sum n^{-1}P(\rho_n>1)$ vanishes while $\sum\rho_j=\infty$, so clause (i) fails as printed; the paper's proof cites its Lemma (1.6), which assumes nondegeneracy. "Converges in law" is Mathlib's TendstoInDistribution; "$p-\lim Z_n=\infty$" is $P(Z_n\le M)\to0$ for every $M$; $E(\ln\sigma)$ is the difference of the $[0,\infty]$-valued expectations of its positive and negative parts, required not to be both infinite, with $\ln0=-\infty$.

Contributions welcome beyond the milestones: an ergodic theorem for nonnegative stationary sequences with values in $[0,\infty]$; the identity $E(S_1)=\nu/(1-\nu)$; and the construction of a two-sided i.i.d. extension of a one-sided sequence, which turns milestone 5 into a statement about the goal's sequence.

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
• H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Mathematica 131:207–248, 1973. https://doi.org/10.1007/BF02392040
• W. Vervaat, On a stochastic difference equation and a representation of non-negative infinitely divisible random variables, Advances in Applied Probability 11(4):750–783, 1979. https://doi.org/10.2307/1426858
• G. D. Birkhoff, Proof of the ergodic theorem, Proceedings of the National Academy of Sciences 17(12):656–660, 1931. https://doi.org/10.1073/pnas.17.12.656

Motivation

Fitting a probability distribution to prescribed margins or moments is a basic task in statistics and information theory. Starting from a reference distribution, one can enforce one constraint at a time by choosing the closest distribution in I-divergence, then cycle through the constraints. In a contingency table this procedure is iterative proportional fitting. A single projection onto the intersection is the desired answer, but each step of the iteration sees only one constraint set. Csiszár's 1975 paper proves that cyclic I-projections converge to the joint I-projection when the underlying set is finite and the constraint sets are linear. This mission formalizes that result together with the geometric statements needed to identify its limit.

Setting

Let $(X,\mathcal X)$ be a measurable space. A probability distribution (PD) is a probability measure on it. For PDs $P$ and $Q$, the I-divergence $I(P\|Q)$ is the Kullback–Leibler divergence: integrate the logarithm of the density of $P$ relative to $Q$ against $P$, with value $+\infty$ when $P$ is not absolutely continuous with respect to $Q$ or the integral diverges. It takes values in $[0,+\infty]$ and vanishes exactly when $P=Q$. The logarithmic conventions are $\log0=-\infty$ and $0\cdot(\pm\infty)=0$ (Csiszár 1975, (1.1)–(1.3)).

Given a PD $R$ and a set $\mathcal E$ of PDs that contains at least one $P$ with finite $I(P\|R)$, an I-projection $Q$ of $R$ onto $\mathcal E$ minimizes $I(P\|R)$ over $P\in\mathcal E$ and itself has finite divergence. The variation distance is the $L^1$ distance between the densities of two PDs relative to a common dominating measure. A set of PDs is linear here when every real affine combination of two members that is still a PD also belongs to the set. This includes distributions satisfying fixed linear moment constraints (Csiszár 1975, pp. 147 and 150–151).

For the goal, $X$ is finite. Choose $k\ge1$ linear sets $\mathcal E_1,\ldots,\mathcal E_k$, and write $\mathcal E=\bigcap_{i=1}^k\mathcal E_i$. Beginning with $Q_0=R$, let $Q_n$ be the I-projection of $Q_{n-1}$ onto $\mathcal E_i$ when $n=mk+i$ and $1\le i\le k$. The common feasible set is assumed nonempty and contains a PD absolutely continuous with respect to $R$. These assumptions ensure that the intended finite-divergence projection problem is present (Csiszár 1975, Theorem 3.2).

Formalization targets

The goal is the convergence statement of Theorem 3.2:

$$\forall x\in X,\qquad Q_n(\{x\})\longrightarrow Q(\{x\}), \quad Q=\operatorname{proj}^{I}_{\mathcal E}(R).$$

The goal also asserts existence of the cyclic sequence. On finite $X$, convergence of every point mass is equivalent to convergence in variation distance. The target fixes no rate. Its milestones include existence on variation-closed convex sets (Theorem 2.1), the identity (2.6) and the tangent-hyperplane Lemma 2.1, the Pythagorean characterization and transitivity of I-projections (Theorems 2.2–2.3), the density form under general linear constraints (Theorem 3.1) and the finite-moment exponential-density characterization (Corollary 3.1(A)), and the finite-space identity used in Theorem 3.2's proof. The two displayed identities in that proof are also targets:

$$I(Q\|R)=I(Q\|Q_n)+\sum_{i=1}^{n}I(Q_i\|Q_{i-1}),\qquad I(P\|Q_n)=I(P\|Q)+I(Q\|Q_n)\quad(P\in\mathcal E).$$

They specify the divergence relationships that the eventual convergence theorem must preserve (Csiszár 1975, (3.14)–(3.15)).

Significance

The theorem justifies enforcing finitely many linear distribution constraints one at a time while still obtaining the same I-projection as a simultaneous minimization. It gives a precise limit for the iterative proportional fitting procedure discussed by Csiszár, including cases in which the initial distribution has zero probabilities; strict positivity of $R$ is not required (Csiszár 1975, p. 155). The accompanying identities make the relation between a partial iterate and the final solution explicit. The result was proved in 1975. The work here is to provide machine-checked proofs of that known result and its supporting geometry, while keeping the source's extended-value and boundary conventions visible.

Difficulty

Successive projections minimize divergence over different sets. Minimization for one set by itself does not identify the minimizer over their intersection, and ordinary metric projection facts do not directly apply because I-divergence is asymmetric and can be infinite. The paper's statements need to handle zero densities and feasible distributions at infinite divergence without turning extended-real expressions into default values. On the finite space, convergence of a subsequence is available, but the formal claim must still identify every possible limit as the joint I-projection. These are the mathematical and representation difficulties faced by a complete proof (Csiszár 1975, §§2–3).

Formalization scope

Lean uses Measure X and Mathlib's InformationTheory.klDiv : ℝ≥0∞ for $I(P\|Q)$. A projection is a finite-divergence minimizer over the stated feasible set; no real-valued infimum or implicit arbitrary witness replaces it. Variation distance uses the densities relative to $P+Q$, which dominates both PDs and gives the value of (1.6). Variation closure is expressed by sequential convergence in this distance. The integral $\int\log q_R\,dP$ is represented in extended reals using positive and negative logarithmic parts and ENNReal.log; the theorem hypotheses keep the indeterminate $+\infty-(+\infty)$ case out. Density equations are $R$-almost everywhere, and a claim that $Q$ has an $R$-density explicitly includes $Q\ll R$.

For moment constraints, every integral is accompanied by integrability. Real affine combinations are tested through their values on measurable sets; the candidate combination must be a PD. The goal assumes a finite carrier with measurable singleton sets and $k\ge1$. Lean indexes the sets by Fin k from zero, so Qs (n+1) is projected onto the set at n % k; this is the paper's rule (3.13) shifted by one. The goal asserts existence of a recursive sequence before speaking about every such sequence, and the required feasible witness has $P\ll R$. These choices rule out an empty cyclic schedule, junk integrals, and a vacuous convergence assertion. Reusable contributions include the variation-distance and I-projection interfaces, their Pythagorean geometry, and the finite-moment density characterization; the mission's main closure remains Theorem 3.2.

Selected references

• I. Csiszár, I-Divergence Geometry of Probability Distributions and Minimization Problems, The Annals of Probability 3(1), 146–158 (1975). DOI: 10.1214/aop/1176996454.

Motivation

Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has a perfect matching, a fixed greedy priority can leave many girls unmatched. The paper introduced RANKING, which randomly chooses the boys' priority order once and then uses that order for every arrival.

The question is quantitative: how many pairs does RANKING guarantee in expectation against a graph and an arrival order chosen before its random ranking? The paper's target is a fraction approaching $1-1/e$ of the $n$ pairs in a perfect matching. Its printed Theorem 1 concerns an auxiliary algorithm called EARLY; the RANKING statement follows the intended chain through Lemmas 3 and 5. The original EARLY analysis has a gap for general upper-triangular matrices, so this mission states the RANKING target and the earlier, unaffected lemmas separately. This distinction matters because an assertion about EARLY would be a different formalization target.

Setting

A bipartite graph has a boy side $U$ and a girl side $V$, each with $n$ vertices. An edge $(u,v)$ means that boy $u$ may be paired with girl $v$. A matching is a collection of edges in which no boy or girl occurs twice. The standing hypothesis for the performance guarantee is that the graph has a perfect matching: some bijection from boys to girls selects an edge for every boy. The graph is otherwise arbitrary.

Girls arrive in a predetermined order. When girl $v$ arrives, only her incident edges are revealed. RANKING first chooses a uniformly random permutation $\pi$ of the boys. For each arriving girl, it selects the highest-ranked adjacent boy who is still unmatched, if one exists. Write $M_{\mathrm R}(G,\pi)$ for the final matching. The expected size is the finite average over all $n!$ rankings. The guarantee must hold for every graph and every predetermined arrival order; relabeling girls lets the formal statement fix their order to $n,n-1,\ldots,1$.

The paper also uses a dual rows-arrive view. Boys arrive in an order and choose among eligible girls, whose priority order is fixed. This is the same greedy rule with the sides exchanged. For its triangular reduction, the columns are numbered $1,\ldots,n$ and column $n$ has highest priority. An upper-triangular matrix with unit diagonal is a graph with every edge $(i,i)$ and with an edge $(i,j)$ only when $i\le j$. On such a graph, the auxiliary algorithm EARLY declines to match row $i$ if column $i$ is already covered by EARLY's own matching. For any matching $M$, $D(M)$ denotes the indices for which both row $i$ and column $i$ are covered.

Formalization targets

RANKING guarantee

For every $\varepsilon>0$, one threshold $N$ must work for every size $n\ge N$ and every graph $G$ with a perfect matching:

$$\mathbb E_{\pi\sim\mathrm{Unif}(S_n)}|M_{\mathrm R}(G,\pi)| \ge (1-e^{-1}-\varepsilon)n.$$

This is the uniform lower-bound reading of the paper's $n(1-1/e)-o(n)$ target. It does not prescribe a finite-$n$ additive constant. The mission goal is the RANKING assertion drawn from the paper's Theorem 1 and Lemmas 3 and 5. The six milestones formalize the paper's Lemmas 1–5 and the corollary to Lemma 4, in their source order. They cover the side-exchange identity, arbitrary refusal algorithms, the triangular reduction, the matching-count identity, its expected form, and the pointwise comparison with EARLY.

Significance

The guarantee gives a concrete worst-case floor for a simple randomized allocation rule: as the graph size grows, RANKING matches at least an asymptotic $1-1/e$ fraction of the pairs available in a perfect matching, in expectation. The order is selected before the random permutation, matching the paper's performance measure. The lower bound remains meaningful on sparse graphs and does not rely on a density assumption. The original paper also studies the limit on what any randomized online algorithm can guarantee; that upper-bound result is treated in a separate mission.

A formal development here would provide reusable finite definitions for online greedy matching, arbitrary state-dependent refusal, fixed-order duality, and uniform expectation over permutations. The goal is a theorem statement awaiting a machine-checked proof; compiling the draft declarations verifies their Lean syntax and types, not their truth. The local mission separates the valid early structural statements from later statements whose published EARLY argument does not justify them on general upper-triangular graphs.

Difficulty

The random permutation does not make the fate of different vertices independent. Matching one girl removes a boy who might be essential to a later girl, so a per-arrival probability estimate cannot simply be added across all arrivals. The dual and triangular views capture useful structure, but turning that structure into a uniform bound for every graph is the main obstacle. In particular, reasoning about EARLY as if its matched-column set had the same monotonicity as unrestricted RANKING fails on some upper-triangular matrices. A proof of the goal must establish the RANKING guarantee without treating those later EARLY statements as available facts.

Formalization scope

Boys and girls are both Fin n; an adjacency matrix is a relation between them. A published predicate represents a perfect matching as an edge-preserving bijection. The generic greedy run processes arrival times in increasing order and interprets a smaller priority index as higher rank. It makes a new matching decision only from the current matching and the arriving vertex. RANKING's returned edges are consistently ordered as (boy, girl), even though girls arrive. The dual run has rows arriving in an arbitrary permutation and takes column $n-1$ as highest priority in Lean's zero-based numbering. EARLY's refusal test consults the matching constructed by EARLY itself.

All expectations are finite averages over Equiv.Perm (Fin n), scaled by $1/n!$. The formal $o(n)$ claim is $\forall\varepsilon>0,\ \exists N,\ \forall n\ge N,\ \forall G$ with a perfect matching, the displayed lower bound. Placing $N$ before $G$ preserves the worst-case meaning. The perfect-matching condition is essential: the empty graph cannot satisfy a positive linear guarantee. The triangular matrix in Lemma 3 retains every diagonal edge, so a zero matrix cannot witness the reduction. These conventions rule out vacuous versions of the goal and reduction.

The definitions of partial matching, covered vertices, greedy run, RANKING, EARLY, and uniform average are part of the mission. A complete proof may build further finite counting and permutation machinery; such lemmas can be shared beyond this paper. Contributions toward the six milestone statements, the goal, and faithful supporting results are in scope. Lemmas 6–12 and the printed EARLY Theorem 1 are outside this mission because their analysis depends on claims that fail for some matrices allowed by their surrounding assumptions.

Selected references

• Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, 1990, pp. 352–358. DOI: 10.1145/100216.100262.

Why competing retailers change the contracting problem

A supplier who sells through a single newsvendor retailer faces double marginalization: the retailer bears the whole cost of leftover stock but earns only the retail margin, so under a plain wholesale-price contract he orders less than the integrated supply chain would. The literature reviewed in G. P. Cachon's chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) shows that buy-back, revenue-sharing and related contracts correct this distortion. Section 6.5 asks what happens when the supplier sells through several retailers who compete for the same customers.

Competition can push in the opposite direction. When customers buy wherever stock is available, a retailer who stocks more also takes demand from his rivals, and he does not count that loss as a cost. This demand-stealing effect pushes the retailers towards over-ordering, which offsets double marginalization. §6.5.1 makes this precise in the proportional allocation model, in which total demand is split among the retailers in proportion to their inventories. The model goes back to the deterministic version of Wang and Gerchak (2001); related allocation models are those of Lippman and McCardle (1997) and Anupindi and Bassok (1999), and Mahajan and van Ryzin (2001) observe the same mitigation of the need for coordinating contracts.

This mission formalizes §6.5.1 of the chapter's January 2003 third draft, pp. 48–53.

The proportional allocation model

There are $n \ge 2$ retailers and one supplier. Total retail demand $D \ge 0$ is random, with distribution function $F$ that is differentiable on $(0,\infty)$ with density $f$, strictly increasing on $[0,\infty)$, and satisfies $F(0)=0$. The retail price is $p$ and the supplier's unit production cost is $c$, with $0 < c < p$. Goodwill costs, the salvage value and the retailers' handling cost are zero.

Retailer $i$ orders $q_i \ge 0$. Write $q = \sum_j q_j$ and $q_{-i} = q - q_i$. Retailer $i$ receives the demand $D_i = (q_i/q)D$. Under a buy-back contract $(w, b)$ he pays $w$ per unit ordered and is refunded $b$ per unit left over; $b = 0$ is the wholesale-price contract. His expected profit is

$$\pi_i(q_i, q_{-i}) = \mathbb E\big[p\min(q_i, D_i) + b(q_i - D_i)^+\big] - wq_i = (p-w)q_i - (p-b)\frac{q_i}{q}\int_0^q F(x)\,dx .$$

Because total sales $\min(q, D)$ depend only on the total stock, the integrated chain earns $\Pi(q) = pS(q) - cq$ with $S(q) = \mathbb E[\min(q,D)]$, and its optimal stock $q^o$ solves the newsvendor equation $F(q^o) = (p-c)/p$, Eq. (20). A Nash equilibrium is a profile of orders in which each $q^*_i$ maximizes $\pi_i(\cdot, q^*_{-i})$ over all orders $x \ge 0$. A contract coordinates the chain when its equilibrium total order is $q^o$.

Two contract prices appear on p. 52: the wholesale price $\widehat w(q) = p\big(1 - \tfrac1n F(q) - \tfrac{n-1}{n}\cdot\tfrac1q\int_0^qF\big)$ that induces total stock $q$, and the buy-back wholesale price

$$w_b(b) = p - (p-b)\left[\frac1n\cdot\frac{p-c}{p} + \frac{n-1}{n}\cdot\frac{1}{q^o}\int_0^{q^o}F(x)\,dx\right].$$

Formalization targets

Goal: the coordinating buy-back contract (pp. 51–53)

For $n \ge 2$, $b < p$ and $q^o$ solving (20), with $w = w_b(b)$: $q^o$ maximizes $\Pi$; $b < w_b(b) < p$; the profile in which every retailer orders $q^o/n$ is the unique Nash equilibrium; and at that equilibrium

$$\pi_i = \frac{p-b}{pn^2}\,\Pi(q^o), \qquad \pi_s = wq^o - cq^o - b\,\mathbb E[(q^o-D)^+] = \frac{p(n-1)+b}{pn}\,\Pi(q^o).$$

Milestones

The milestones are the section's own claims, in attack order: the newsvendor characterization (20); the inequality $\frac1q\int_0^qF < F(q)$; the closed form of $\pi_i$ and its strict concavity in the retailer's own order (p. 50); the first-order condition and Eq. (21); the monotonicity and limits of the left side $L_n$ of Eq. (22), giving a unique root for $b < w < p$; the unique, symmetric Nash equilibrium for every $b < w < p$; the increase of the equilibrium total in $n$; that $\widehat w(q)$ induces $q$, that $\widehat w(q^o) > c$, and that the supplier's profit under wholesale pricing has negative slope at $q^o$; the coordinating price $w_b(b)$ with $w_b(b) > \widehat w(q^o)$ for $b > 0$; and the ratio $\pi_s(q^o, w_b(0), 0)/\Pi(q^o) = (n-1)/n$ (p. 53). A companion item states the endpoint $b = p$, at which the supplier takes all of $\Pi(q^o)$.

Significance

The section answers two questions. First, with competing retailers a plain wholesale-price contract can coordinate the chain and still leave the supplier a positive margin, which a single retailer never allows. Second, that contract is not the supplier's best wholesale price, and it fixes a single division of profit. Buy-back contracts remove both limitations: the family $(w_b(b), b)$ coordinates for every $b < p$ and moves the supplier's share continuously from $(n-1)/n$ to all of $\Pi(q^o)$. The ratio $(n-1)/n$ also measures how little a coordinating contract adds when many retailers compete (80% of the optimal profit at $n = 5$).

The results are proved in the chapter, mostly by short computations, and none of them has been machine-checked. The formalization makes explicit what the page leaves implicit: that no equilibrium has a retailer ordering zero, the limits behind "from 0 to 1", and the density condition behind the strict sign on p. 52. It also produces a reusable proportional-allocation game and a Nash-equilibrium predicate for nonnegative real strategies.

Difficulty

The algebraic identities (the profits at the coordinating contract, the ratio $(n-1)/n$, the derivative at $q^o$) are routine once $\pi_i$ has its closed form. The closed form itself requires computing the expectation with proportional shares and identifying $\mathbb E[\min(q,D)]$ with $q - \int_0^q F$.

The real obstacle is the uniqueness of the equilibrium. The page argues from first-order conditions, which describe only interior best responses. A complete proof must show that each retailer's profit is strictly concave in his own order, that no retailer orders zero in equilibrium, and that the all-zero profile (where $\pi_i$ has $q = 0$ in a denominator) is not an equilibrium. Strict concavity is the delicate step. The second derivative mixes the density with the term $\frac{2q_{-i}}{q^3}\big(qF(q) - \int_0^qF\big)$, and concavity has to be established on the closed half-line, including the boundary $q_i = 0$.

Formalization scope

Retailers are indexed by Fin n with $n \ge 2$ (the page's $n > 1$). The comparison in $n$ also allows a single retailer, as the page does. Orders are real numbers $q_i \ge 0$, and best responses range over all $x \ge 0$. The demand law is a probability measure on $\mathbb R$ carried by $[0,\infty)$ with finite mean, $F$ is its cdf, and $f$ is a field with HasDerivAt F (f y) y for $y > 0$. These are the chapter's standing assumptions (p. 7). The condition $c > 0$ is needed for (20) to have a solution. The integrated optimum $q^o$ enters each theorem through the hypothesis $F(q^o) = (p-c)/p$, which determines it uniquely. Transfers run from the retailers to the supplier.

Added or made explicit relative to the page: $b < p$ in the concavity claim (at $b = p$ the profit is linear); $f(q^o) > 0$ for the strict sign of the supplier's marginal profit; positivity of the total order wherever $\frac1q\int_0^qF$ appears. The page's printed slips (the first-order condition rescaled by $q^*/(p-b)$, "$F(q^o) = (p-c)/c$", "$w(b)$") are corrected in the statements and kept in the milestone quotes.

Ruled out as trivializing: $\widehat w$ and $w_b$ are the printed formulas, not "the price at which $q^o$ is an equilibrium"; the supplier's profit is computed from the transfers, not as $\Pi$ minus the retailers' profits; the equilibrium statement quantifies over all nonnegative deviations, so restricting attention to interior or symmetric profiles is not an option.

A complete development needs interval integrals of a cdf, the fundamental theorem of calculus for $q \mapsto \int_0^qF$, and strict concavity from a strictly decreasing derivative. The proportional-allocation game and the Nash predicate are reusable for the other allocation models of §6.5. No platform item is referenced: the competing-retailer game of Cachon and Lariviere (2005), RevShareCoord.Competing.*, uses deterministic revenue functions and is a different model.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; read in the author's 3rd draft (Jan. 2003), §6.5.1. https://doi.org/10.1016/S0927-0507(03)11006-7
• Y. Wang and Y. Gerchak, Supply chain coordination when demand is shelf-space dependent, Manufacturing & Service Operations Management 3(1), 2001, 82–87. https://doi.org/10.1287/msom.3.1.82.9998
• S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 1997, 54–65. https://doi.org/10.1287/opre.45.1.54
• S. Mahajan and G. van Ryzin, Inventory competition under dynamic consumer choice, Operations Research 49(5), 2001, 646–657. https://doi.org/10.1287/opre.49.5.646.10603
• G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

Motivation

Many counting problems in probability, combinatorics and statistics ask for the law of the number of occurrences of rare, weakly dependent events: long head runs in coin tossing, matching segments between two DNA sequences, isolated vertices or small subgraphs in a random graph, clusters of points in a scan statistic. Chen's 1975 adaptation of Stein's method gives an explicit error bound for approximating such a count by a Poisson law. Arratia, Goldstein and Gordon (Ann. Probab. 17 (1989) 9–25) recast it in terms of a neighbourhood of dependence for each event. In this form the error bound needs only the first two moments of the indicators whenever each event is independent of the events outside its neighbourhood. The paper's examples (head runs, DNA sequence matching, birthday-type problems) made this form standard in applied probability.

The paper has two main results. Theorem 1 bounds the distance between the law of the total count and a Poisson law; it is essentially contained in Chen (1975). Theorem 2, which the authors describe as new, is a process version. It compares the joint law of all the indicators, that is, where the events occur, with a Poisson process. Theorem 3, a corollary, compares a dependent family of events with an independent family having the same marginal probabilities. This mission formalizes Theorem 2, the finite-dimensional bound it is derived from, the steps of its proof in §6, and Theorem 3.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $I$ an index set. For $\alpha\in I$ let $X_\alpha$ be a Bernoulli random variable, $X_\alpha\in\{0,1\}$, with

$$p_\alpha=P(X_\alpha=1)>0,\qquad \lambda=\sum_{\alpha\in I}p_\alpha\in(0,\infty).$$

For each $\alpha$ fix a set $B_\alpha\subseteq I$ with $\alpha\in B_\alpha$, the neighbourhood of dependence of $\alpha$. Put $p_{\alpha\beta}=E(X_\alpha X_\beta)$ and

$$b_1=\sum_{\alpha\in I}\sum_{\beta\in B_\alpha}p_\alpha p_\beta,\qquad b_2=\sum_{\alpha\in I}\sum_{\alpha\neq\beta\in B_\alpha}p_{\alpha\beta},\qquad b_3=\sum_{\alpha\in I}E\bigl|E\{X_\alpha-p_\alpha\mid\sigma(X_\beta:\beta\in I-B_\alpha)\}\bigr|.$$

Roughly, $b_1$ measures the size of the neighbourhoods, $b_2$ the expected number of neighbours of an occurrence, and $b_3$ the dependence between an event and the events outside its neighbourhood. In many applications $X_\alpha$ is independent of $\sigma(X_\beta:\beta\notin B_\alpha)$, so $b_3=0$.

The dependent Bernoulli process is $\mathbf X=(X_\alpha)_{\alpha\in I}$, a random element of $\mathbb Z_+^I$. The Poisson process on $I$ with intensity $p_{(\cdot)}$ is $\mathbf Y=(Y_\alpha)_{\alpha\in I}$ with the $Y_\alpha$ mutually independent and $Y_\alpha$ Poisson with mean $p_\alpha$.

Distances are measured in the paper's total variation norm,

$$\|\mathcal L(U)-\mathcal L(V)\|=\sup_{\|h\|=1}|Eh(U)-Eh(V)|=2\sup_A|P(U\in A)-P(V\in A)|,$$

which is twice the usual total variation distance.

Formalization targets

Goal: Theorem 2

$$\|\mathcal L(\mathbf X)-\mathcal L(\mathbf Y)\|\le2(2b_1+2b_2+b_3).$$

The bound has no dependence on $\lambda$ and no assumption on $I$ beyond countability (which the setting forces).

Milestones, in attack order

1. $T_iS_ih=h$ (§6, p. 22). For functions on $\mathbb Z_+^d$, the coordinatewise Stein operators $(T_if)(j)=j_if(j)-\lambda_if(j+e_i)$ and $(S_ih)(j+e_i)=-(\lambda_iP(Z_i=j_i))^{-1}E\{h(j_1,\dots,Z_i,\dots,j_d)1(Z_i\le j_i)\}$ satisfy $T_iS_ih=h$.
2. Bounds on $f_i=S_i(h-P_ih)$ (§6, p. 22), where $P_ih$ averages $h$ over a Poisson($\lambda_i$) $i$-th coordinate. For $\|h\|\le1$, $\|f_i\|<2(1\wedge1.4\lambda_i^{-1/2})$ and $\|\Delta_kf_i\|<4(1\wedge1.4\lambda_i^{-1/2})$.
3. Display (15) (p. 24). $E\{(X_\alpha-p_\alpha)(f(U+X_\beta e_k)-f(U))\}\le2\|f\|(p_{\alpha\beta}+p_\alpha p_\beta)$ for any random $U$.
4. Displays (13)–(14), the step $i=1$ (p. 23). With $W_j=\sum_{\alpha\in I(j)}X_\alpha$ the block sums of a partition and $Z_1$ an independent Poisson($\lambda_1$),

$$|Eh(W_1,\dots,W_d)-Eh(Z_1,W_2,\dots,W_d)|\le2\|f_1\|\sum_{I(1)}p_\alpha^2+2\|f_1\|\sum_{I(1)}\sum_{\alpha\ne\beta\in B_\alpha}(p_{\alpha\beta}+p_\alpha p_\beta)+\|f_1\|\sum_{I(1)}s_\alpha.$$

5. The finite-dimensional bound (Theorem 2, p. 11). For a partition of $I$ into nonempty blocks $I(1),\dots,I(d)$ with $W_j=\sum_{I(j)}X_\alpha$, $Z_j=\sum_{I(j)}Y_\alpha$ and $\lambda_j=EW_j$:

$$\|\mathcal L((W_1,\dots,W_d))-\mathcal L((Z_1,\dots,Z_d))\|\le2\bigl(1\wedge1.4(\min_i\lambda_i)^{-1/2}\bigr)(2b_1+2b_2+b_3).$$

Companion results

• Theorem 3 (p. 12). For an independent Bernoulli process $\mathbf X'$ with the same marginals as $\mathbf X$, $\|\mathcal L(\mathbf X)-\mathcal L(\mathbf X')\|\le2(2b_1+2b_2+b_3)+4\sum p_\alpha^2$.
• The remark after Theorem 3. $\|\mathcal L(\mathbf X')-\mathcal L(\mathbf Y)\|\le2\sum p_\alpha^2$, so $4\sum p_\alpha^2$ in Theorem 3 can be replaced by $2\sum p_\alpha^2$.

Significance

The result. Theorem 2 says that when $b_1$, $b_2$, $b_3$ are small, the set of indices at which the dependent events occur is close in law to a Poisson process with the same intensity. The bound covers every event about the locations, not just the total count. It is in the strong total variation norm and needs only moment information when $b_3=0$. Theorem 3 turns this into a decoupling statement: a dependent family of rare events is almost indistinguishable from an independent family with the same marginals. The process bound is the form used when the positions of rare events matter, for example in the distribution of the location of the longest match in sequence comparison and in scan statistics.

Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would give a Lean statement and proof of a Chen–Stein bound with explicit constants, for countable index sets and arbitrary dependence. It would also include the coordinatewise Stein operators on $\mathbb Z_+^d$ and the bounds on their solutions, which are reusable for other multivariate Poisson approximations. A companion mission formalizes Theorem 1, including Lemma 1 (the bounds on the one-variable Stein solution) on which milestone 2 rests.

Difficulty

The total variation distance between two laws on $\mathbb Z_+^I$ cannot be bounded coordinate by coordinate, because the $X_\alpha$ are dependent. The one-variable Stein equation controls only the law of a single integer-valued statistic. The paper passes through finite-dimensional block sums and replaces the coordinates one at a time. At each replacement the error has to be charged to the terms of $b_1,b_2,b_3$ indexed by the current block, so that the total over all blocks reproduces $2b_1+2b_2+b_3$ without a factor $d$. Two further points need care. First, the bound $\|\Delta_kf_1\|\le2\|f_1\|$ is the only one available for differences in a coordinate other than the one being replaced; this is why the constants are larger than in Theorem 1. Second, the infinite index set requires a limiting argument from finitely many blocks to the full process.

Formalization scope

• The index set is a countable type. The page says "arbitrary index set", but $p_\alpha>0$ and $\sum p_\alpha<\infty$ force countability; the assumption also makes $\mathbf X$ measurable as a map into $\mathbb N^I$ with the product σ-algebra.
• The $X_\alpha$ are measurable, $\mathbb N$-valued and bounded by $1$. $p_\alpha$ is $P(X_\alpha=1)$. The standing hypotheses $p_\alpha>0$, $\sum p_\alpha=\lambda$ and $\lambda>0$ are explicit.
• $b_1,b_2,b_3$ and $s_\alpha$ are $[0,\infty]$-valued, and every bound is an inequality in $[0,\infty]$, so a divergent series is never read as $0$. The conditional expectation in $s_\alpha$ is taken with respect to a σ-algebra generated by measurable maps, hence a genuine sub-σ-algebra.
• The norm $\|\mathcal L(U)-\mathcal L(V)\|$ is twice the published definition MarkovChainCLT.tvDist (supremum over measurable sets of $|\mu(A)-\nu(A)|$). Dropping the factor $2$ would make the goal twice as strong and false in general.
• $\mathbf Y$ (and $\mathbf X'$ in Theorem 3) lives on its own probability space. Mutual independence of the $Y_\alpha$ and of the $X'_\alpha$ is a hypothesis. Without it the law of the process is not determined by the marginals and the statements are false.
• Block sums $W_j$ are $\mathbb N$-valued tsums, equal to the true sums almost surely. A partition is a surjection $I\to\{1,\dots,d\}$ (Fin d), so Lean's coordinate 0 is the paper's coordinate $1$.
• $(S_ih)(j)$ is set to $0$ when $j_i=0$, as for $S$ in §4. The strict inequalities in milestone 2 use the actual sup norms over $\mathbb Z_+^d$.

Needed infrastructure: product measures and independence on $\mathbb N^I$, Poisson laws (Mathlib's poissonMeasure), conditional expectation, and a one-variable Stein bound (Lemma 1). Contributions of proofs of any milestone, of the general step $i$ of §6, and of the one-dimensional Lemma 1 are welcome.

Selected references

• R. Arratia, L. Goldstein, L. Gordon, Two moments suffice for Poisson approximations: the Chen-Stein method, Ann. Probab. 17(1) (1989) 9–25. https://doi.org/10.1214/aop/1176991491
• L. H. Y. Chen, Poisson approximation for dependent trials, Ann. Probab. 3(3) (1975) 534–545. https://doi.org/10.1214/aop/1176996359
• A. D. Barbour, G. K. Eagleson, Poisson approximation for some statistics based on exchangeable trials, Adv. Appl. Probab. 15(3) (1983) 585–600. https://doi.org/10.2307/1426620
• A. D. Barbour, L. Holst, S. Janson, Poisson Approximation, Oxford University Press, 1992. https://global.oup.com/academic/product/poisson-approximation-9780198522355