Probability

Motivation

Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate $\lambda$, how many servers $s$ are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule

$$s = \lambda + \gamma\sqrt{\lambda},$$

where the grade of service $\gamma > 0$ sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.

Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers $N$ in the IS model is Poisson with mean $\lambda$, its mean and variance are both $\lambda$, so the event "more than $s$ servers busy" has roughly constant probability when $s - \lambda$ is a fixed multiple of $\sqrt\lambda$. The Poisson law of $N$ is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean $1$ (M/G/∞ with finite support).

Timeline:

• The stationary number in system of M/G/∞ is classically known to be Poisson with mean $\lambda \cdot E[S]$ for general service-time laws (Palm's theorem; see Gross et al., Fundamentals of Queueing Theory).
• Halfin and Whitt (Operations Research 29, 1981) proved the heavy-traffic limit theorem that justifies square-root staffing for GI/M/s queues.
• Whitt (1992) gave the elementary IS derivation formalized here, with the finite-support M/G/∞ case argued through splitting a Poisson stream into independent class streams.

Setting

Time is measured in units of the mean service time. Let $T_0, T_1, T_2, \dots$ be i.i.d. exponential random variables with rate $\lambda > 0$, the interarrival times, and let $\tau_n = T_0 + \cdots + T_{n-1}$ be the $n$-th arrival epoch. The arrival counting process $A(t)$ is the number of $n \ge 1$ with $\tau_n \le t$, the number of arrivals in $(0, t]$. This is a Poisson process of rate $\lambda$.

Customers are numbered $k = 0, 1, 2, \dots$; customer $k$ arrives at $\tau_{k+1}$, is served at once, and has service time $D_k$. Following the paper (proof of Proposition 2.3, p. 712), an arrival at time $t$ is counted and a departure at time $t$ is not, so customer $k$ is present at $t$ iff $\tau_{k+1} \le t < \tau_{k+1} + D_k$. The number of busy servers is

$$N(t) = \#\{k : \tau_{k+1} \le t < \tau_{k+1} + D_k\}.$$

For the M/G/∞ case fix $m \ge 1$ classes with probabilities $p_1, \dots, p_m$ and values $d_1, \dots, d_m \ge 0$. Each customer carries a class label $J_k$, the labels are i.i.d. with $P(J_k = i) = p_i$ and independent of the interarrival times, and $D_k = d_{J_k}$. The class-$i$ busy count is $N_i(t) = \#\{k : J_k = i,\ \tau_{k+1} \le t < \tau_{k+1} + d_i\}$.

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

If $\sum_{i=1}^m p_i d_i = 1$ and $t > \max_i d_i$, then

$$P\big(N(t) = k\big) = e^{-\lambda}\frac{\lambda^k}{k!}, \qquad k = 0, 1, 2, \dots$$

The law depends on the service-time distribution only through its mean.

Milestones

1. Proposition 2.3 (p. 712): with unit service times, $N(t) = A(t) - A(t-1)$, pathwise.
2. Proof of Proposition 2.4 (p. 712): for $t \ge 1$, $A(t) - A(t-1)$ has the same law as $A(1)$.
3. Proposition 2.4 (p. 712): in M/D/∞ with unit service times, $N(t) \sim \mathrm{Poisson}(\lambda)$ for each $t > 1$.
4. §2.5, splitting (p. 713): the class-$i$ arrivals form independent Poisson streams of rates $\lambda p_i$; stated as independence and Poisson laws of the class counts in one window $(a_i, b_i]$ per class.
5. §2.5, "Hence" (p. 713): for $t > \max_i d_i$, the $N_i(t)$ are independent, $N_i(t) \sim \mathrm{Poisson}(\lambda p_i d_i)$, and $N(t) = \sum_i N_i(t)$ almost surely.

A companion item, Proposition 2.1 (p. 710), states that (2) implies $\lambda = s + \gamma^2/2 - \gamma\sqrt{s + \gamma^2/4}$ and $s - \gamma\sqrt s \le \lambda \le s - \gamma\sqrt s + \gamma^2/2$, connecting (2) to the utilization equation $\lambda = s - \gamma\sqrt s$.

Significance

The goal is the step that turns the IS heuristic from a special case into a statement about general service: since $N(t)$ is Poisson with mean $\lambda$ whatever the finite service-time law of mean $1$, the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that $s$-server congestion is nearly insensitive to the service distribution beyond its mean when $s$ is large.

The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:

• a Poisson process built from exponential interarrival times, with the stationary-increment property derived rather than assumed;
• Poisson splitting (thinning by i.i.d. labels) with independence of the class streams, a tool reused throughout queueing and inventory theory;
• the M/G/∞ Poisson law for discrete service times, complementing the open platform items ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.

The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law $A(t) \sim \mathrm{Poisson}(\lambda t)$) is related but distinct from milestone 2, which concerns the increment over $(t-1, t]$.

Difficulty

The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time $t - 1$: the residual time to the next arrival after $t-1$ must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by $t-1$), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows $(t - d_i, t]$ of different classes make this unavoidable.

Formalization scope

• The arrival process is the published definition QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.
• The model IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.
• Counts are Set.ncard, which is $0$ on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by $t$, and the decomposition $N(t) = \sum_i N_i(t)$ is stated almost surely. Poisson laws are stated pointwise, $P(X = k) = e^{-c}c^k/k!$, avoiding pushforwards of possibly non-measurable maps.
• Standing conventions: service rate $1$; the system starts empty at time $0$; arrival counted at $t$, departure not; "steady state" means the law at each fixed $t > \max_i d_i$, with no limit $t \to \infty$; the paper's $1 \le i \le n$ is Fin m. The constraint $\sum_i p_i d_i = 1$ forces $m \ge 1$, and the label law forces $p_i \ge 0$ and $\sum_i p_i = 1$. Added hypotheses: $d_i \ge 0$ (service times are nonnegative) and, in Proposition 2.1, $\gamma > 0$ (the paper's grade of service).
• Infrastructure welcome: memorylessness of the Poisson process at a fixed time, Poisson thinning with independent marks, and the finite-sum version of Mathlib's IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.

Selected references

• W. Whitt, Understanding the efficiency of multi-server service systems, Management Science 38(5):708–723, 1992. https://doi.org/10.1287/mnsc.38.5.708
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
• D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

Why the walk slows down

A random walk in a random environment uses transition probabilities selected once for each site, rather than probabilities resampled at every step. Even when the site environments are independent and identically distributed, the walker revisits the same local bias whenever it returns to a site. Its long-time motion can therefore differ sharply from that of a walk with a single averaged right-step probability. Solomon’s 1975 paper established the recurrence and speed classification for this one-dimensional model and then examined a two-value example in which some sites are one-way mirrors: the walker can pass through them to the right but cannot cross them to the left. The example isolates how a sequence of random intervals between mirrors produces slow growth and phase-dependent limit laws Solomon 1975, §2.

The present mission concerns §2 of that paper, pp. 10–20. Its central question is how far the walker has traveled after $n$ steps when the mean crossing time reaches or exceeds the critical threshold. At criticality, a logarithmic correction replaces ordinary linear speed. Above criticality, the paper gives limits along subsequences whose logarithmic fractional parts approach a fixed phase.

The walk and its mirror environment

Let $(\Omega,\mathcal F,P)$ be a probability space and let $\alpha_j$, $j\in\mathbb Z$, be independent, identically distributed random variables in $[0,1]$. The environment is the complete sequence $\alpha=(\alpha_j)_{j\in\mathbb Z}$. Conditional on a fixed environment, a nearest-neighbour walk starts at $X_0=0$ and, from site $j$, moves to $j+1$ with probability $\alpha_j$ and to $j-1$ with probability $1-\alpha_j$. The annealed probability $P$ averages the conditional path law over the environment. In Lean this joint law is specified on every finite path cylinder together with every measurable event of the whole environment, so it determines the dependence between $X$ and $\alpha$.

Fix $\theta>1$ and $0<\gamma<1$. Solomon’s example has $\alpha_j=1$ with probability $1-\gamma$ and $\alpha_j=(1+\theta)^{-1}$ with probability $\gamma$. Equivalently, the left-to-right odds ratio $\sigma_j=(1-\alpha_j)/\alpha_j$ takes values $0$ and $\theta$. A site with $\sigma_j=0$ is a one-way mirror. Write $V_0=0$ and let $V_n$ be the position of the $n$th mirror strictly to the right of zero. Let $T_j$ be the first time the walk reaches site $j$, with $T_j=\infty$ if it never does. For $b>0$, $\log_b x$ means the logarithm in base $b$, and $\{x\}=x-\lfloor x\rfloor$ is the fractional part.

The parameters used below are

$$\nu=\frac{2\theta}{(\theta-1)^2},\qquad K=\frac{1-\gamma}{\gamma}\nu,\qquad \rho=\log_{1/\gamma}\theta.$$

When $\gamma\theta>1$, the paper specifies a probability law $F_\varepsilon$ on $[0,\infty)$ by its Laplace transform

$$\int_0^\infty e^{-ux}\,dF_\varepsilon(x)=\exp\left[-Ku\sum_{j\in\mathbb Z}\frac{(\gamma\theta)^{j-\varepsilon}}{1+\nu u\theta^{j-\varepsilon}}\right],\qquad u>0.$$

Here $F_\varepsilon(t)$ also denotes that law’s distribution function at $t$. The bilateral series converges in the supercritical parameter range. The source’s notation uses the same letter for a distribution and its distribution function; the Lean development keeps these roles separate as a measure and its value on $(-\infty,t]$.

Formalization targets

The first clause of Theorem (2.20) is the critical growth law. If $\gamma\theta=1$, then

$$\frac{X_n}{n/\log_\theta n}\xrightarrow{P}\frac12.$$

The second clause describes the supercritical case. If $\gamma\theta>1$, $n_k\to\infty$, and $\{\log_\theta n_k\}\to\varepsilon$, then for each $x>0$,

$$P\!\left(n_k^{-1/\rho}X_{n_k}<x\right)\longrightarrow 1-F_{\lambda(x)}\!\left(((1-\gamma)x)^{-\rho}\right), \qquad \lambda(x)=\varepsilon+\log_{1/\gamma}((1-\gamma)x).$$

Both clauses are the goal. The milestones record the transform identity of Lemma (2.5), its approximation and scaling limits in Lemmas (2.6)–(2.7), the mirror passage-time limits of Lemma (2.10), and the ordinary passage-time limits of Theorem (2.18). The fractional part in the goal uses base $\theta$; the two passage-time results use base $1/\gamma$, exactly as printed Solomon 1975, pp. 12–19.

What the result gives

The critical law identifies the constant in the growth scale $n/\log_\theta n$. The supercritical law shows that a single power normalization $n^{1/\rho}$ does not erase the logarithmic phase of the environment: the limiting distribution depends on the phase approached by the chosen subsequence. These assertions describe the position $X_n$ itself, rather than only the time needed to reach a distant site. They complement the paper’s general speed theorem by resolving the zero-speed behavior in a concrete model Solomon 1975, Theorems (1.16) and (2.20).

The results are proved in the 1975 paper; the open work here is machine checking their definitions, statements, and proofs. The development also yields reusable interfaces for a nearest-neighbour chain specified by cylinder probabilities, first-passage times that can be infinite, and Laplace-transform arguments for random time changes. The mission’s statements currently compile locally with proof placeholders, so they are formalization targets rather than machine-checked theorems.

Where the difficulty lies

The one-way mirrors create independent, identically distributed blocks of crossing times, but those times have tails governed by the random spacing between mirrors. At $\gamma\theta=1$, their accumulation produces a logarithmic correction; at $\gamma\theta>1$, the underlying geometric scales preserve the fractional part of a logarithm. An ordinary law of large numbers for passage times therefore cannot supply both limits. Moreover, a limit for passage times to the random mirror positions $V_n$ does not immediately give a limit for passage times to deterministic sites, and converting a passage-time limit into a position limit requires control of the inverse time change. The source separates these tasks across the milestone results Solomon 1975, pp. 11–20.

Formalization scope

The Lean environment is the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The position and environment are integer-indexed; time is natural-number-indexed. The one-way-mirror parameter range is $\theta>1$, $0<\gamma<1$, $\gamma\theta\ge1$. The strict bounds on $\gamma$ make both atom probabilities meaningful and the logarithm base $1/\gamma$ valid. The source uses these bounds implicitly. All probabilities concern the annealed joint law, not an arbitrary process with the same one-time marginals.

First-passage times are extended natural numbers, with infinity on paths that never hit the target. The real-valued limits convert finite passage times to real numbers; under the stated model, infinite passage times form a null event. The location of a nonexistent next mirror is assigned zero for a total Lean function, again only on a null event in this model. The Laplace transform of an infinite passage time is defined as zero. Convergence in probability uses TendstoInMeasure; convergence in law is expressed by convergence of distribution functions at continuity points. The limit-law family is constrained to probability measures supported on $[0,\infty)$ with the exact transform (2.12), preventing a degenerate or unrelated choice of $F$.

A complete proof needs measurable cylinder laws, independence of the mirror gaps, hitting-time and transform calculations, asymptotics of one-sided and bilateral series, distributional convergence from Laplace transforms, and inversion from passage time to position. Work on any of these components is in scope. The statement keeps both source regimes and every constant; replacing the joint walk law by independent marginals or choosing an arbitrary limit distribution would change the theorem.

Selected references

• Fred Solomon, Random Walks in a Random Environment, The Annals of Probability 3(1):1–31, 1975. DOI: 10.1214/aop/1176996444.

Motivation

Many quantities in queueing, inventory and reliability models are additive functionals of a regenerative process: the total work processed by a server up to time $t$, the cost accumulated by an inventory policy, the time a machine spends broken. Each such quantity grows by independent, identically distributed amounts over the cycles between successive regeneration points. W. L. Smith called these cumulative processes in Regenerative stochastic processes (Proc. R. Soc. Lond. A, 1955), the paper that introduced the term "regenerative process" and laid out its limit theory. Long-run averages of such quantities are estimated by simulation and by statistical observation of real systems. Confidence intervals for these estimates, and the regenerative method of simulation output analysis, rest on the central limit theorem for cumulative processes. When several quantities are estimated at once (a ratio of two rewards, a vector of costs), they rest on its joint version for several cumulative processes driven by the same regenerations.

Timeline:

• 1949. Feller proves the central limit theorem for the renewal counting process.
• 1952. Anscombe proves that a central limit theorem survives replacing the number of summands by a random index $m_t$ with $m_t/\psi(t)\to 1$ in probability, without independence between the index and the summands (Anscombe, Proc. Camb. Phil. Soc. 48, 1952).
• 1955. Smith extends Anscombe's theorem to random vectors and deduces the univariate (Theorem 9, Corollary 9·1) and multivariate (Theorem 10) central limit theorems for cumulative processes (Smith 1955).

Setting

On a probability space $(\Omega, P)$, let $t_1, t_2, \dots$ be independent, identically distributed, non-negative random variables with $P\{t_1 = 0\} < 1$ (a renewal process), and $t_0 = 0$. The regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ ($k \ge 0$), and $n_t$ is the number of epochs in $[0,t]$ (in Smith's words, the greatest $k$ with $T_{k-1} \le t$, where $T_{-1} = 0$). Write $\mu_r = E t_1^r$.

A real process $w_t$ with $w_0 = 0$ is a cumulative process if (C1) its cycle increments $y_n = \Delta_n w_t = w_{T_n} - w_{T_{n-1}}$, $n \ge 1$, are i.i.d., and (C2) with probability one its paths have bounded variation on every finite interval. The variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ has increments $\tilde y_n = \Delta_n \tilde w_t$. Moments are written $\kappa_r = E y_n^r$ and $\tilde\kappa_r = E \tilde y_n^{\,r}$.

$M$ cumulative processes $w^{(1)}_t, \dots, w^{(M)}_t$ are based on the same sequence of regeneration points when the cycle vectors $(t_n, y^{(1)}_n, \dots, y^{(M)}_n, \tilde y^{(1)}_n, \dots, \tilde y^{(M)}_n)$ are i.i.d. in $n$. Put $\kappa^{(i)}_1 = E y^{(i)}_1$. The covariance matrices are

$$a_{kl} = \operatorname{cov}(y^{(k)}_1, y^{(l)}_1), \qquad b_{kl} = \operatorname{cov}\Big(y^{(k)}_1 - \tfrac{\kappa^{(k)}_1}{\mu_1} t_1,\; y^{(l)}_1 - \tfrac{\kappa^{(l)}_1}{\mu_1} t_1\Big).$$

Formalization targets

Goal: Theorem 10

If $\mu_1 < \infty$ and $E(\tilde y^{(i)}_1)^2 < \infty$ for every $i$, then as $t \to \infty$

$$\left(\frac{w^{(i)}_t - \kappa^{(i)}_1 n_t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, a),$$

and if in addition $\mu_2 < \infty$,

$$\left(\frac{w^{(i)}_t - (\kappa^{(i)}_1/\mu_1)\,t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, b).$$

Milestones

• The renewal strong law $n_t/t \to 1/\mu_1$ almost surely (§5·3).
• Lemma 8: if $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$, then $(w_{t+Z_t} - w_t)/t^{1/p} \to 0$ almost surely, where $Z_t = \sum_1^{n_t+1} t_i - t$.
• Theorem B (Anscombe): $P\{\sum_1^{m_t} y_i/(\sigma\psi(t)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ for i.i.d. centred $y_i$ with variance $\sigma^2 > 0$ and $m_t/\psi(t) \to 1$ in probability.
• Its $M$-dimensional form (§5·4): $\psi(t)^{-1/2}\sum_1^{m_t} \mathbf y_j \xrightarrow{d} \mathcal N(0, a)$ for i.i.d. centred random vectors.
• Theorem 9: if $E y_1 = 0$ and $\operatorname{var} y_1 = \sigma^2 > 0$, then $P\{w_t/(\sigma(t/\mu_1)^{1/2}) \le \alpha\} \to \Phi(\alpha)$.
• Corollary 9·1: the univariate forms of both assertions of the goal, with normalisations $\sigma = (\kappa_2 - \kappa_1^2)^{1/2}$ and $\gamma = \operatorname{var}(y_1 - (\kappa_1/\mu_1)t_1)$.

Significance

Theorem 10 is the multivariate central limit theorem for regenerative processes. Its second assertion with $M = 2$ and the delta method gives the asymptotic normality of ratio estimators $w^{(1)}_t / w^{(2)}_t$, the basis of the regenerative method of simulation output analysis. With $w_t = n_t$, Corollary 9·1 recovers Feller's central limit theorem for renewal processes, which Smith points out (p. 9). The first assertion, with the random centring $\kappa_1 n_t$, needs only $\mu_1 < \infty$, which matters for heavy-tailed cycle lengths.

The results are classical and proved, and none of them is formalized. Mathlib has the central limit theorem for i.i.d. real sums with a deterministic number of terms and multivariate Gaussian laws, but no random-index central limit theorem, no renewal counting process and no regenerative process. A formal development would supply Anscombe's theorem (useful well beyond renewal theory, for sequential analysis and random sums), the renewal strong law and a reusable model of cumulative processes.

Difficulty

The obvious argument writes $w_t$ as the sum of the first $n_t$ cycle increments plus a remainder and applies the classical central limit theorem. This fails at two points. First, the number of summands $n_t$ is random and depends on the summands themselves (cycle lengths and rewards are typically dependent), so the classical theorem with a deterministic index does not apply and conditioning on $n_t$ destroys the i.i.d. structure. Anscombe's theorem is needed exactly for this; it requires control of the partial sums uniformly over a window of indices around $t/\mu_1$, not at a single index. Second, the remainder over the incomplete cycle at time $t$ must be shown negligible on the scale $\sqrt t$ using only a second moment of the cycle variation; Lemma 8 does this almost surely. For the vector statement, the scalar theorem must be lifted to convergence in distribution in $\mathbb R^M$ with a possibly degenerate covariance matrix, where the scalar theorem's hypothesis $\sigma > 0$ can fail along some directions.

Formalization scope

• Time is real; every limit is along $t \to \infty$ in $\mathbb R$. Processes are functions $w : \mathbb R \to \Omega \to \mathbb R$ (or a family indexed by Fin M); cycle lengths are a sequence $\mathbb N \to \Omega \to \mathbb R$ with $t_0 = 0$.
• $n_t$ is a natural number, the number of epochs $T_j \le t$; on the null event where infinitely many epochs are $\le t$ it is $0$. Finiteness is never assumed.
• $\tilde w_t$ is the total variation (eVariationOn) of the path on $[0,t]$, set to $0$ for all $t$ on paths of infinite variation, as Smith allows.
• Condition (C1) is read for the whole cycle vector $(t_n, y_n, \tilde y_n)$. No independence between components is assumed. Assuming the cycle length independent of the rewards, or the components independent, would make $a$ diagonal or force $b$ into a special form; that trivialization is ruled out.
• "Jointly normally distributed with covariance matrix $a$" is TendstoInDistribution to multivariateGaussian 0 a on EuclideanSpace ℝ (Fin M). The matrices $a$ and $b$ are defined as covariance matrices, hence positive semidefinite, so the limit is a genuine (possibly degenerate) Gaussian law and not Mathlib's Dirac fallback for non-PSD input.
• The scalar statements keep the paper's form: convergence of $P\{\cdot \le \alpha\}$ to $\Phi(\alpha) =$ cdf (gaussianReal 0 1) α for every real $\alpha$. The paper's implicit $\sigma > 0$ and $\gamma > 0$ are explicit hypotheses; without them the quotients are $0$ in Lean and the statements would be false.
• $\mu_1 < \infty$, $\mu_2 < \infty$ and $E\tilde y^2 < \infty$ are Integrable hypotheses, never encoded through the value of an integral.

Contributions welcome: a proof of Anscombe's theorem from Mathlib's central limit theorem; the renewal strong law from strong_law_ae; measurability lemmas for $n_t$ and $\tilde w_t$; the Cramér–Wold step.

Selected references

• W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
• F. J. Anscombe, Large-sample theory of sequential estimation, Proc. Cambridge Philos. Soc. 48, 600, 1952 (cited in Smith 1955, p. 31).
• W. Feller, Fluctuation theory of recurrent events, Trans. Amer. Math. Soc. 67, 98, 1949 (cited in Smith 1955, p. 31).
• J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63, 422, 1948 (cited in Smith 1955, p. 31).

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 15 (p. 6)

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

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

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

Milestones

In the order of the proof:

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

Conventions:

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

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

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

Ruled-out trivializations:

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

A complete development needs the following:

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

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

Selected references

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

Motivation

Inventory systems in which unmet demand is lost, not backlogged, are the norm in retail: a customer who finds an empty shelf buys elsewhere. With a positive lead time $L$ between ordering and delivery, the optimal policy for such a system depends on the entire pipeline of outstanding orders, so dynamic programming is intractable beyond small $L$. Optimal policies are not of base-stock type, and for decades no policy with a provable guarantee on its expected cost was known for this model.

Levi, Janakiraman and Nagarajan (Math. Oper. Res. 33(2), 2008) gave the first such guarantee. Their dual-balancing policy balances, in every period, the expected holding cost against the expected lost-sales penalty of the units ordered now, and it costs at most twice as much as an optimal policy.

Timeline.

• 2007. Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2)) introduce marginal cost accounting and the dual-balancing policy for the backlogging model, with a worst-case guarantee of 2.
• 2008. Levi, Janakiraman and Nagarajan extend the guarantee to lost sales (this mission). In their model the truncated inventory positions of the two policies can cross back and forth inside a lead time, which the backlogging argument never meets.
• 2009. Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science, 2009) prove that order-up-to policies are asymptotically optimal in the lost-sales model as the penalty cost grows.
• 2021 onward. Xin (Oper. Res., 2021; SSRN 7134538) analyses capped base-stock policies for i.i.d. lost-sales demand, culminating in a 2.33-approximation guarantee for that policy class, whose main theorem is proved on Prove2Me.

Page and display numbers in this mission refer to the authors' accepted manuscript (28 pages, pp. 1–28), not to the journal's pages 351–374.

Setting

Periods are $t=1,\dots,T$. An order $Q_s\ge0$ placed in period $s$ arrives at the start of period $s+L$, where $L\ge1$ is an integer. Before the horizon there are $x_0\ge0$ units on hand and pipeline orders $Q_j=q_j\ge0$ for $1-L\le j\le0$. Demands $D_1,\dots,D_T\ge0$ have finite means. The information $\mathcal F_s$ available at the start of period $s$ contains $D_1,\dots,D_{s-1}$ and possibly more. A feasible policy chooses $Q_s$ as an $\mathcal F_s$-measurable quantity.

The on-hand inventory $I_t$ at the start of period $t$, after the arrival, satisfies $I_1=x_0+Q_{1-L}$ and

$$I_{t+1}=(I_t-D_t)^+ + Q_{t+1-L}.$$

Demand $(D_t-I_t)^+$ is lost. Costs are a holding rate $h_t\ge0$, a lost-sales penalty $p_t\ge0$ and an ordering cost $c_t\ge0$ per unit, where $p_t$ and $c_t$ are non-increasing in $t$.

Marginal cost accounting. Under first-ordered-first-consumed bookkeeping, $H_s$ is the ordering cost $c_sQ_s$ plus the holding cost that the $Q_s$ units incur until the end of the horizon, and $\Pi_s=p_{s+L}(D_{s+L}-I_{s+L})^+$ is the lost-sales penalty in the period in which they arrive. The cost of a policy $P$ is

$$\mathcal C(P)=\sum_{s=1}^{T-L}\bigl(H^P_s+\Pi^P_s\bigr).$$

It omits only costs that are the same for every policy.

The truncated inventory position of period $s$ with respect to $t\le s$ is $Y_{st}=I_s+\sum_{j=s+1-L}^{t}Q_j$. For two policies $B$ and $P$, the set $\mathcal T_H$ holds the periods $t\le T-L$ with $Y^B_{st}<Y^P_{st}$ for every $s\in[t,t+L]$, and $\mathcal T_\Pi$ holds the remaining periods $t\le T-L$.

A dual-balancing policy $B$ orders, in each period $t\le T-L$, the amount that equalises the two conditional expectations

$$E[H^B_t\mid\mathcal F_t]=E[\Pi^B_t\mid\mathcal F_t]=:Z_t.$$

Formalization targets

Goal: Theorem 3.1

If demands are independent, then for every feasible policy $P$

$$E[\mathcal C(B)]\le 2\,E[\mathcal C(P)].$$

Comparing with every feasible $P$, rather than with an optimal policy, gives the guarantee without assuming that an optimum is attained.

Milestones, in attack order

1. (11) For $t\le s\le t+L$, $I_{t+L}=Y_{st}-D_{[s,t+L)}+\sum_{r=s}^{t+L-1}(D_r-I_r)^+$.
2. Lemma 3.2. On every sample path, $\sum_{t\in\mathcal T_H}H^B_t\le\sum_{t}H^P_t$.
3. Lemma 3.3. On every sample path, $\sum_{t\in\mathcal T_\Pi}\Pi^B_t\le\sum_{t}\Pi^P_t$.
4. (14) $E[\mathcal C(P)]\ge E\bigl[\sum_t(\mathbb 1_{t\in\mathcal T_H}H^B_t+\mathbb 1_{t\in\mathcal T_\Pi}\Pi^B_t)\bigr]$.
5. Lemma 3.1. $E[\mathcal C(B)]=2\sum_{t=1}^{T-L}E[Z_t]$.
6. Lemma 3.4. This lemma characterises the crossing events $A_{st}=[Y^B_{st}<Y^P_{st}]\cap[Y^B_{s+1,t}\ge Y^P_{s+1,t}]$.
7. Lemmas 3.5 and 3.6. Under independence, conditioning on $t\in\mathcal T_H$ (respectively $t\in\mathcal T_\Pi$) does not lower the conditional expected holding (respectively lost-sales) cost of $B$ below $Z_t$.

Significance

The result. The theorem gives a constant-factor guarantee for a lost-sales system with lead times, for arbitrary independent and non-identical demand distributions. The policy is computed online, one period at a time, from one-dimensional conditional expectations, which an optimal policy cannot be. The guarantee holds with time-dependent holding costs and with non-increasing ordering and penalty costs. Section 5 of the paper extends it to correlated demand structures, which are out of this mission's scope.

Formalizing it. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The mission produces the lost-sales dynamics, the truncated inventory position, marginal cost accounting and the sample-path amortization lemmas as reusable Lean objects. It also produces a formal treatment of the conditional-expectation step under independence, which the backlogging analysis does not need. The sibling mission on the backlogging model, LeviBalancing.DualBalancing, provides the shared instance and policy definitions that are reused here.

Difficulty

In the backlogging model, $t\in\mathcal T_H$ is decided by information available at time $t$, so the cost comparison can be made period by period after conditioning on $\mathcal F_t$. With lost sales this fails: the truncated positions of $B$ and of the benchmark can cross from below to above and back inside the window $[t,t+L]$. Whether $t\in\mathcal T_H$ is therefore not known at time $t$, and conditioning on that event moves the conditional expectations of $H^B_t$ and $\Pi^B_t$ away from $Z_t$. A newcomer's first idea, to reuse the backlogging argument with $\mathcal F_t$-measurable indicators, does not apply. The lost-sales penalty also cannot be charged period by period: Lemma 3.3 is a global amortization over intervals. The non-increasing penalties are what make that amortization possible when $p_t$ varies.

Formalization scope

• Periods are integers. The pipeline $Q_j$, $j\le0$, is shared by every policy through the published order. Instance, cumDemand, order, DemandProcess and IsFeasiblePolicy are reused from LeviBalancing.DualBalancing. The new layer is one definition file, LostSalesBalancing.DualBalancing.Model.
• Orders and demands are real (fractional orders, as in §3.1). The randomized integral-order variant is out of scope.
• Cost generality is that of Theorem 3.1. Rates are only required to be $\ge0$, which strengthens the paper's stationary $h,p>0$. Accordingly (11) is stated in lost units, and Lemma 3.4(iv) is stated as positive lost demand, not positive penalty.
• Independence. The paper assumes independent demands but lets $\mathcal F_s$ hold more than past demands. The formalization requires $\mathcal F_t$ to be independent of $(D_t,\dots,D_T)$ for every $t$, which for the natural filtration is exactly mutual independence. Finite means are integrability.
• "OPT" becomes every feasible policy in Theorem 3.1, (14) and Lemmas 3.5–3.6. In the sample-path statements, (11) and Lemmas 3.2–3.4, it becomes every nonnegative order sequence.
• Conditional events. $\Pr(A\mid\mathcal F)\,E[X\mid\mathcal F,A]$ is written $E[\mathbb 1_AX\mid\mathcal F]$, which never divides by a zero probability.
• Expected costs are lower Lebesgue integrals in $[0,\infty]$. The dual-balancing predicate requires $H^B_t$ and $\Pi^B_t$ to be integrable, so no conditional expectation takes Mathlib's default value $0$.
• Lemma 3.4(iii) is stated with $D_s\ge I^P_s-\Delta Q_s$. The printed strict inequality excludes a tie at which the event $A_{st}$ does occur.
• A trivializing formalization is ruled out: the dual-balancing predicate and the independence hypothesis are jointly satisfiable with $T>L$ (checked locally on an explicit instance), and no statement is meaningful only when $T\le L$, the case in which every cost is zero.

Contributions welcome: proofs of the sample-path lemmas, which need only finite sums and the recursion; the conditional-expectation lemmas, which need a Harris-type argument for independent coordinates; and the existence of a measurable balancing order, which this mission does not pose.

Selected references

• R. Levi, G. Janakiraman, M. Nagarajan, A 2-Approximation Algorithm for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research 33(2), 351–374, 2008. https://doi.org/10.1287/moor.1070.0285
• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2), 284–302, 2007. https://doi.org/10.1287/moor.1060.0205
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science, 2009. https://doi.org/10.1287/mnsc.1080.0945
• L. Xin, capped base-stock policies in lost-sales inventory models, Operations Research, 2021. https://doi.org/10.1287/opre.2020.2019
• L. Xin, Capped Base-Stock Policies: A 2.33-Approximation, SSRN working paper 7134538, 2026. https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538

Motivation

A coalescent models a collection of ancestral lineages merging as time runs backward. If every event joins exactly two lineages, a single pairwise merger rate describes the finite system. Pitman’s 1999 paper asks which rates permit an event to join any number of blocks, while still giving one process on partitions of all positive integers. This matters when a sample of any finite size must be a restriction of the same population model: specifying a chain separately at every sample size is insufficient unless the chains agree when labels are removed. The paper supplies an exact answer in terms of a finite measure on the unit interval. See Pitman (1999), Theorem 1 and §3.1.

Setting

Let $\mathcal P_n$ be the partitions of $[n]=\{1,\ldots,n\}$ and $\mathcal P_\infty$ the partitions of the positive integers. A partition records which labels belong to the same block. The map $R_n$ restricts a partition to $[n]$. A partition $\pi$ refines $\pi'$ when every block of $\pi$ is contained in a block of $\pi'$. Thus blocks can merge as time grows, but never split.

A $\mathcal P_\infty$-valued process is a coalescent here when its paths refine with time and each finite restriction $R_n$ has right-continuous step-function paths. For a partition of $[n]$ with $b$ blocks, each unordered choice of $k$ blocks, $2\le k\le b$, merges into one block at rate $\lambda_{b,k}$. Different choices are different possible transitions, each with that rate; the rate is not multiplied by the number of choices. The finite chain’s generator $Q_n$ records these transition rates, with each diagonal entry the negative sum of the other entries in its row. Its transition matrix after time $t$ is $\exp(tQ_n)$.

An array $(\lambda_{b,k})$ is consistent when, for every $n<m$ and every initial partition of $[m]$, restricting the $m$-label chain to $[n]$ gives the same process law as the $n$-label chain started at the restricted partition. A finite nonnegative Borel measure $\Lambda$ on $[0,1]$ supplies a rate array through an integral. The point mass at zero is included: because $0^0=1$ for natural powers, it gives pairwise mergers while higher-order merger rates vanish. These definitions follow Pitman (1999), pp. 1871–1872 and Lemma 18.

Formalization targets

Characterization of admissible rates

The goal is the existence-and-rates part of Theorem 1. For every nonnegative array $(\lambda_{b,k}:2\le k\le b)$, a coalescent with these finite-chain merger rates exists from every $\pi\in\mathcal P_\infty$ if and only if there is a finite nonnegative measure $\Lambda$ on $[0,1]$ such that

$$\lambda_{b,k}=\int_{[0,1]}x^{k-2}(1-x)^{b-k}\,\Lambda(dx) \qquad(2\le k\le b).$$

The statement asks for one measure representing every rate in the infinite array, and a process from every initial partition. It fixes neither a particular measure nor a sample size. This is Theorem 1, equation (1).

Supporting claims

The milestone list follows §3.1: adjacent-size restrictions suffice to check consistency; consistency is equivalent to

$$\lambda_{b,k}=\lambda_{b+1,k}+\lambda_{b+1,k+1} \qquad(2\le k\le b);$$

and the nonnegative normalized array relation

$$\mu_{i,j}=\mu_{i+1,j}+\mu_{i,j+1},\qquad \mu_{0,0}=1,$$

is equivalent to a representation $\mu_{i,j}=\mathbb E[X^i(1-X)^j]$ for $X\in[0,1]$. The final milestone states the uniqueness as well as the existence of the representing measure: equation (1) is a bijection between consistent arrays and finite measures. These are the claims in Lemma 18 and its proof, p. 1882.

Significance

The characterization turns an infinite family of nonnegative rates into one finite measure, and says exactly when finite chains at different sample sizes can be restrictions of a common partition process. The bijection also makes the measure identifiable from the rates. Without consistency, a chain specified at one size can change its law when an unobserved extra label is added; there would be no single process on $\mathcal P_\infty$ with those restrictions.

Pitman proved these results in 1999. The mission concerns machine-checking their statements and, eventually, their proofs. The current Lean items are open theorems with compiled statements; they do not yet have machine-checked proofs. The reusable part of a complete development would include finite partition generators, restriction of continuous-time Markov chains, and the moment representation for normalized nonnegative arrays. These tools also apply to other consistent families of random combinatorial structures.

Difficulty

Checking that each $Q_n$ defines a finite-state chain does not by itself construct a process on partitions of all integers. Deleting one label can change which apparent merger occurs in the smaller chain, so the rates must satisfy a precise identity across adjacent sizes. Even once those identities hold, the conclusion requires one joint law whose finite restrictions agree for all sizes and times, with right-continuous paths. The representation step must recover a genuine finite measure, including possible mass at zero, and must prove uniqueness; a mere numerical fit for finitely many entries cannot establish the theorem.

Formalization scope

The Lean partition type is Setoid (Fin n) at finite size and a type synonym of Setoid ℕ at infinite size. The paper’s positive labels are shifted to zero-based labels, preserving their order. The measurable structure on infinite partitions is generated by pairwise equivalence coordinates, equivalently by finite restrictions; finite partition spaces use the discrete measurable structure. The process path predicate requires refinement at every pair of ordered times and right continuity of every finite restriction. Finite-chain laws are specified at all finite collections of times through $\exp(tQ_n)$, so a process cannot qualify merely by having the right initial state or a single marginal.

The measure is represented on $\mathbb R$ with zero mass outside $[0,1]`; integrals are over$[0,1]$. Finiteness is explicit, preventing a nonintegrable Bochner integral from acquiring Lean’s default value. Natural-number exponents retain$x^0=1$at$x=0$. The rate array is read only for$2\le k\le b$, and the zero measure is allowed. The Fin 0 restriction is an additional tautological boundary case introduced by Lean’s natural numbers. The process sample space is a small Lean type, and the law is a probability measure on it.

Only the characterization sentence of Theorem 1 is targeted. Its later assertions about the strong Markov property, Feller semigroup, Skorohod path-space law, and weak continuity of the law map are outside this mission. Contributions toward those properties would need further path-space infrastructure. The formalized foundations and milestones can also support the paper’s Poisson construction and its later results, but those are separate targets.

Selected references

• Jim Pitman, Coalescents with multiple collisions, Annals of Probability 27(4), 1870–1902, 1999. DOI: 10.1214/aop/1022874819.

Motivation

A random discrete distribution is a random sequence of nonnegative numbers summing to $1$. Ranked in decreasing order, $V_1\ge V_2\ge\cdots$, such sequences model the relative sizes of species in a population, of cycles of a random permutation, of excursion intervals of a Markov process, and of atoms of random measures used as priors in Bayesian nonparametrics. The two-parameter Poisson–Dirichlet family $\mathrm{PD}(\alpha,\theta)$ is the main family of such laws; Pitman and Yor (Ann. Probab. 1997) derived its properties from a stable subordinator.

The special case $\mathrm{PD}(\alpha,0)$, $0<\alpha<1$, describes the ranked lengths of the excursion intervals of a stable($\alpha$) subordinator's range, or of a Bessel process away from zero, up to time $1$. A basic question about it is the law of a single ranked term $V_n$. The answer goes through the Laplace transform of $1/V_n$:

• Darling (1952) found the characteristic function of the limit of $S_n/X_{(n,1)}$ (sum over maximum of i.i.d. heavy-tailed variables), which is that of $1/V_1$.
• Lamperti (1961) derived the corresponding Laplace transform from renewal theory, for $n=1$.
• Wendel (1964) obtained the transform for every $n\ge2$ from the range of a stable subordinator.
• Pitman and Yor (1997), Proposition 11, explained the formula through an exact decomposition of $1/V_n$ into independent, infinitely divisible pieces.

Setting

Fix $0<\alpha<1$. Let $\tilde Y_1,\tilde Y_2,\dots$ be independent, with $\tilde Y_n$ having the beta distribution $\mathrm{beta}(1-\alpha,n\alpha)$ on $(0,1)$. Form the stick-breaking sequence $\tilde V_1=\tilde Y_1$ and $\tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$ for $n\ge2$, and let $V_1\ge V_2\ge\cdots$ be its terms in decreasing order. The law of $(V_n)$ is $\mathrm{PD}(\alpha,0)$ (Definition 1 of the paper, with $\theta=0$).

From $(V_n)$ define $R_n=V_{n+1}/V_n$, $A_0=0$ and, for $n\ge1$,

$$A_n=\frac{V_1+\cdots+V_n}{V_{n+1}},\qquad \Sigma_n=\frac{V_{n+1}+V_{n+2}+\cdots}{V_n}.$$

For $\lambda\ge0$ the paper's two Laplace exponents are

$$\phi_\alpha(\lambda)=\alpha\int_1^\infty e^{-\lambda x}x^{-\alpha-1}\,dx,\qquad \psi_\alpha(\lambda)=1+\alpha\int_0^1\left(1-e^{-\lambda x}\right)x^{-\alpha-1}\,dx,$$

and $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$.

The proof represents $(V_n)$ through a Poisson random measure (PRM) $\Lambda_\alpha$ on $(0,\infty)$ with $\Lambda_\alpha(x,\infty)=Cx^{-\alpha}$: its ranked points $\Delta_1>\Delta_2>\cdots$ satisfy $X_n:=C\Delta_n^{-\alpha}=\varepsilon_1+\cdots+\varepsilon_n$ with $\varepsilon_i$ i.i.d. standard exponential, and $V_n=\Delta_n/\sum_m\Delta_m$.

Formalization targets

Goal: Proposition 11

For every $n\ge1$,

$$\frac1{V_n}=1+A_{n-1}+\Sigma_n\quad\text{a.s.},$$

where (i) $A_{n-1}$ is distributed as the sum of $n-1$ independent copies of $A_1$, with $E[e^{-\lambda A_{n-1}}]=\phi_\alpha(\lambda)^{n-1}$; (ii) $\Sigma_n$ is distributed as the sum of $n$ independent copies of $\Sigma_1$, with $E[e^{-\lambda\Sigma_n}]=\psi_\alpha(\lambda)^{-n}$; (iii) $A_{n-1}$ and $\Sigma_n$ are independent.

Milestones

• Proposition 10 (iii): $X_n=LV_n^{-\alpha}$, with $L=\lim nV_n^\alpha$, are the arrival times of a unit Poisson process, and $V_n=X_n^{-1/\alpha}/\sum_mX_m^{-1/\alpha}$.
• Lemma 24 (i)–(ii): $C\Delta_n^{-\alpha}$ is gamma$(n)$; the ratios $\Delta_i/\Delta_n$, $i<n$, are the order statistics of $n-1$ i.i.d. variables of density $\alpha x^{-\alpha-1}$ on $(1,\infty)$, independent of $(\Delta_n,\Delta_{n+1},\dots)$.
• (66): $P(A_1\in dx)=\alpha x^{-\alpha-1}dx\,1(x>1)$.
• (67): $E[e^{-\lambda\Sigma_n}\mid\Delta_1,\dots,\Delta_n]=\exp\left(-\Delta_n^{-\alpha}\int_0^1(1-e^{-\lambda u})\Lambda_\alpha(du)\right)$.
• Proposition 8: the $R_n$ are independent and $R_n\sim\mathrm{beta}(n\alpha,1)$.
• (34): $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$.

Consequence: Corollary 12 (Wendel's formula)

$$E\left[\exp(-\lambda/V_n)\right]=e^{-\lambda}\,\phi_\alpha(\lambda)^{n-1}\,\psi_\alpha(\lambda)^{-n}\qquad(\lambda\ge0).$$

Significance

The result. Proposition 11 turns $1/V_n$ into the sum of the constant $1$ and two independent variables, each a sum of i.i.d. pieces with explicit Laplace exponents. Wendel's formula (38) is a one-line consequence, and since $1/V_n>0$ it determines the law of $V_n$. The same decomposition is reused later in the paper: Proposition 26 combines (35) and (67) into a conditional form of (38) given $R_1,\dots,R_{n-1}$ and $X_n$, which the paper uses in later calculations.

Formalizing it. All results here are proved in the paper; none is machine-checked. A formal proof needs the Poisson representation of $\mathrm{PD}(\alpha,0)$ (Proposition 10, itself resting on Perman–Pitman–Yor 1992), elementary but non-trivial facts about Poisson arrival times (gamma laws, order statistics, independence of ratios), and a conditional Laplace functional of a Poisson process. Each milestone is a self-contained target; Lemma 24 and (67) are statements about Poisson arrival times only and do not mention Poisson–Dirichlet laws.

Difficulty

The identity $1/V_n=1+A_{n-1}+\Sigma_n$ is algebra once $\sum_mV_m=1$. The content is in the laws. On the stick-breaking side, the $V_n$ are the order statistics of a dependent sequence, and neither $A_{n-1}$ nor $\Sigma_n$ has an evident structure: the ranking destroys the independence of the $\tilde Y_n$. The proof passes to the Poisson side, where the ranked points of a PRM have tractable conditional laws, and then must transport the conclusions back through a representation that holds only in distribution. Part (ii) requires a conditional computation (67) given $n$ points, followed by integration against a gamma law; part (iii) requires the mutual independence of all the ratios $R_n$, an infinite family.

Formalization scope

The Lean development lives in namespace PoissonDirichlet.Wendel; its definitions file contains every object above.

• Sequences are 0-based: V ω k is $V_{k+1}$, Aseq (V ω) k is $A_k$, Sigseq (V ω) k is $\Sigma_{k+1}$, ratio (V ω) k is $R_{k+1}$. Exponents $n-1$ and $n$ become k and k + 1.
• $\mathrm{PD}(\alpha,0)$ is Definition 1 with $\theta=0$. The law of $(\tilde Y_n)$ is a probability measure on sequences with independent coordinates of the stated beta laws. "$V$ has law $\mathrm{PD}(\alpha,0)$" means $P(V\in s)$ equals the mass of the preimage of $s$ under the ranked stick-breaking map, for every measurable $s$. Ranked values are defined with the extended cardinal Set.encard.
• $A_n$ and $\Sigma_n$ are the $V$-quotients of (31)–(32), not the $R$-expressions; $\phi_\alpha,\psi_\alpha$ are the integrals (33)–(34), not Laplace transforms.
• "Distributed as the sum of $m$ independent copies of $X$" is equality with the $m$-fold convolution power of the law of $X$, the Dirac mass at $0$ when $m=0$.
• Every statement carries $0<\alpha<1$ except Lemma 24, which holds for all $\alpha>0$.
• The local time $L$ of (24) is a random variable with the hypothesis that $nV_n^\alpha\to L$ almost surely; this is its definition.
• The PRM is used only through its ranked points, encoded by arrival times: $\Delta_n=(C/X_n)^{1/\alpha}$ with $X_n=\varepsilon_1+\cdots+\varepsilon_n$, $\varepsilon_i$ i.i.d. standard exponential. This is the paper's own (27)–(28). In (67) the $\varepsilon_i$ are also assumed measurable, so that the conditioning $\sigma$-algebra is a sub-$\sigma$-algebra.
• Lemma 24 (iii) is not stated; its only use is (67), which is stated. Corollary 12 states only the formula (38).

The formalization does not use Measure.map of a possibly non-measurable map in any definition: every equality of laws for such maps is stated through preimages. It does not use Set.ncard or limUnder. Every Laplace transform is the integral of a function with values in $(0,1]$, and both exponent integrals are integrable under the stated parameter range, so no statement holds because an integral takes the junk value $0$.

Useful infrastructure beyond this mission: arrival times of a Poisson process and their gamma and order-statistic laws; convolution powers of measures on $\mathbb R$; the Laplace functional of a Poisson random measure. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
• M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992.
• J. G. Wendel, Zero-free intervals of semi-stable Markov processes, Math. Scand. 14:21–34, 1964.
• J. Lamperti, A contribution to renewal theory, Proc. Amer. Math. Soc. 12:724–731, 1961.
• D. A. Darling, The influence of the maximum term in the addition of independent random variables, Trans. Amer. Math. Soc. 73:95–107, 1952.