Stochastic Systems

Motivation

Population models often allow each individual to produce a new individual or die at rates that change over time. Seasonal conditions, exposure to an epidemic, and changing conditions in a laboratory population all make a constant rate a restrictive assumption. In Kendall's 1948 paper, the question is how the entire distribution of the population size evolves when the per-individual birth and death rates are prescribed functions of time. The distribution matters even when its mean is known: a population can have a stable expected size while still having a substantial chance of extinction. Kendall presents the varying-rate model as a generalization of the constant-rate process discussed by Feller in 1939 (Kendall 1948, §1).

This mission concerns Kendall's solution for a population descended from one ancestor. It includes the explicit distribution, the forward equations that connect it to the birth and death model, and the formulas for its mean, variance, and chance of eventual extinction. The paper has no numbered theorems; its results are identified here by its equation numbers and printed pages.

Setting

At time $t\ge0$, let $n_t$ be the number of individuals. Each individual gives birth at instantaneous rate $\lambda(t)$ and dies at rate $\mu(t)$, so a population of size $n$ moves to $n+1$ at rate $n\lambda(t)$ and to $n-1$ at rate $n\mu(t)$. Both rates are nonnegative. The initial state is $n_0=1$. Write $P_n(t)$ for the probability that $n_t=n$. The forward equations in §2, (2)–(4), p. 2 are

$$P_0'(t)=\mu(t)P_1(t),\qquad P_n'(t)=(n+1)\mu(t)P_{n+1}(t)+(n-1)\lambda(t)P_{n-1}(t) -n(\lambda(t)+\mu(t))P_n(t)\quad(n\ge1).$$

The formula for $P_0'$ reflects that a population already at zero cannot reproduce. The $n-1$ term vanishes at $n=1$, as it must. The model is expressed through these real-valued probability functions; it does not require a sample-space construction of a stochastic process.

Define the integrated rate difference $\rho(t)$ and the function $W(t)$ by §2, (10a)–(11), p. 4:

$$\rho(t)=\int_0^t(\mu(\tau)-\lambda(\tau))\,d\tau,\qquad W(t)=e^{-\rho(t)}\left(1+\int_0^t e^{\rho(\tau)}\mu(\tau)\,d\tau\right).$$

Set $\xi_t=1-e^{-\rho(t)}/W(t)$ and $\eta_t=1-1/W(t)$. Kendall's modified-zero geometric law is $P_0(t)=\xi_t$ and $P_n(t)=(1-\xi_t)(1-\eta_t)\eta_t^{n-1}$ for $n\ge1$. The zero state has its own mass; the positive states form a geometric tail. For the nonnegative rates in this mission, $W(t)\ge1$ and $0\le\eta_t<1$ on $t\ge0$, so the displayed formulas have their ordinary probabilistic meaning.

Formalization targets

The geometric transient law

The goal is the full claim of §2, (8), (10a)–(12), pp. 3–4: the explicit $P_n(t)$ starts from one ancestor, is nonnegative and sums to one for every $t\ge0$, and satisfies the forward equations above. In symbols, the distribution part is

$$P_0(t)=\xi_t,\qquad P_n(t)=(1-\xi_t)(1-\eta_t)\eta_t^{n-1}\ (n\ge1),\qquad \sum_{n=0}^{\infty}P_n(t)=1.$$

The milestones record the paper's intermediate statements in reading order: the rational generating function $\phi(z,t)$ in (9); the pair of equations for $\xi$ and $\eta$ obtained from the generating-function equation (6); the equations for $U=1-\xi$ and $V=1-\eta$; the differential equation and integral representation of $W$; the alternate formulas (10b)–(10c); and the explicit expressions (12). Each is a statement made in the source, with the page and equation displayed beside its milestone.

Extinction and moments

The companion target from §3, (18)–(19), p. 6 writes $J(t)=\int_0^t e^{\rho(\tau)}\mu(\tau)\,d\tau$ and states

$$P_0(t)=\frac{J(t)}{1+J(t)},\qquad P_0(t)\longrightarrow1\ \Longleftrightarrow\ J(t)\longrightarrow+\infty.$$

When $J(t)$ has finite limit $I$, the limiting extinction chance is $I/(1+I)$. Companion statements also retain the mean $\bar n_t=e^{-\rho(t)}$, all three expressions for the variance in (14c), the criterion that extinction has zero chance exactly when $\mu$ vanishes identically, and the necessary divergence of $\int_0^\infty\mu$ for almost-sure extinction (Kendall 1948, pp. 4, 6–7).

Significance

The geometric law supplies every finite-time population probability from the rate functions. Its zero mass yields an extinction probability without taking limits of an unspecified process, while its first two moments quantify expected growth and fluctuations. The extinction criterion distinguishes a population that dies out with probability one from one that retains a positive chance of survival even when its eventual mean behavior is simple. The variance formulas give later sections of Kendall's paper a way to compare rate schedules with the same expected population (§§3, 6).

The result was proved in the 1948 paper. The work here is to state its model and conclusions precisely in Lean, preserving the initial condition, normalization, boundary state, and time-dependent rate conventions. The current files are theorem statements with proof placeholders; a successful build checks their syntax and types, not the mathematical proofs. Once proved, the definitions and the moment and extinction statements can also support formal work on time-dependent branching and population models.

Difficulty

Knowing the expected population is insufficient to determine the distribution. The forward equation for each $P_n$ couples it to both neighboring states, producing an infinite system. A direct finite truncation would change the birth rate at its upper boundary and would therefore no longer be Kendall's model. The zero state also behaves differently from positive states: a purely geometric law on all $n\ge0$ does not capture its mass. The generating function has a rational form, but its time dependence must still agree with the forward system for every state and with a normalized probability law. The extinction statement adds an improper integral, whose finite and divergent regimes require distinct limits.

Formalization scope

Lean represents $\lambda,\mu:\mathbb R\to\mathbb R$ as continuous functions that are nonnegative for $t\ge0$. The paper calls the rates specified functions and assumes their nonnegativity; global continuity is an explicit convenience for the two-sided derivatives and interval integrals. Only nonnegative time appears in the probabilistic statements. The oriented intervalIntegral from zero to $t$ represents every finite integral. HasDerivAt expresses each derivative, and HasSum expresses both normalization and the moment and generating-function series. The law lives on natural-number states, with $P_0$ handled separately. The coefficient at state $n=1$ is the real number $n-1$, not an implicit extension to a negative state.

The positivity of $W$ on nonnegative time must follow from the rates. The definitions are total Lean real functions, so a result that relies on a division states the hypotheses that keep its denominator nonzero. The limit $J(t)\to+\infty$ expresses divergence of the paper's improper integral. No uniqueness of solutions to the forward equations is included, because the cited passage does not establish that claim. The goal requires the explicit law to solve the forward equations and to be a probability law; merely expanding its generating function would leave the population model unformalized. Contributions that prove the formulas, establish the required positivity and convergence facts, or develop reusable lemmas for time-dependent linear birth and death equations all fit the scope.

Selected references

• D. G. Kendall, On the generalized “birth-and-death” process, Annals of Mathematical Statistics 19(1), 1–15, 1948. DOI: 10.1214/aoms/1177730285.

Motivation

Telephone and data networks are often fully connected at the core: every pair of switching centres has a direct trunk group, and a call that finds its direct trunk full may be alternatively routed over a two-link path through a third, tandem centre. Whether such a network can absorb fluctuations of demand without losing traffic depends on how the spare capacity of lightly loaded links can be borrowed by heavily loaded ones. F. P. Kelly's survey Loss networks (Ann. Appl. Probab., 1991, doi:10.1214/aoap/1177005872) studies this question in §4.6, "Results respecting graph structure", by looking at a static snapshot of the network: random loads on the edges of a complete graph, and the question whether they can all be carried at once.

Timeline:

• Hajek (1986, personal communication cited as [21] in the survey) considered edges coloured independently red (a pair that needs twice an edge's capacity) or white (an idle edge), and proved that for red probability $p<1/3$ all red pairs can be served over white two-edge paths with probability tending to one (Theorem 4.40, p. 357).
• Hajek (1987, [22]) showed the same threshold for routing each red pair on a single two-edge path (Theorem 4.43, quoted, p. 358).
• Kelly (1991, Theorem 4.45, p. 358) extended Theorem 4.40 from two-valued loads to general i.i.d. loads with an exponential moment, under the condition $2\,\mathbb E(X-C)^+<\mathbb E(C-X)^+$. The survey gives the proof in full on p. 359.

Setting

Let $K\ge 1$ and consider the complete graph on the nodes $\{0,\dots,K-1\}$: every unordered pair $e=\{a,b\}$ of distinct nodes is an edge, and there are $\tfrac12K(K-1)$ edges. Every edge has capacity $C$.

An offered load $x_e\ge 0$ is attached to every edge $e$. The load of $e=\{a,b\}$ may be carried on its direct edge, or on a two-edge route $a-k-b$ through a tandem node $k\notin e$; such a route uses the two edges $\{a,k\}$ and $\{b,k\}$. Loads are divisible. The loads are routable with capacity $C$ if there are flows $f_{e,k}\ge 0$ (zero when $k\in e$) with $\sum_k f_{e,k}\le x_e$ such that on every edge $g$

$$\Big(x_g-\sum_k f_{g,k}\Big)+\sum_{(e,k):\ g \text{ on the route of } e \text{ via } k} f_{e,k}\le C,$$

i.e. the directly carried part of $g$'s own load plus all two-edge traffic passing through $g$ is at most $C$.

The loads are random: $X$ is a nonnegative real random variable with law $\mu$, and the loads $(x_e)$ are independent, each distributed as $X$. Let

$$P(K)=\mathbb P\{\text{the loads on the complete graph on } K \text{ nodes are routable}\}.$$

Write $\mathbb E(X-C)^+$ for the mean excess of a load over the capacity and $\mathbb E(C-X)^+$ for the mean spare capacity.

Formalization targets

Goal: Theorem 4.45

If $\mathbb E\,e^{\lambda X}<\infty$ for some $\lambda>0$ and

$$2\,\mathbb E(X-C)^+<\mathbb E(C-X)^+ \tag{4.46}$$

then

$$P(K)\to 1 \qquad (K\to\infty).$$

Milestones (in the order of the proof on pp. 358–359)

With $m=\mathbb E(C-X)^+$ and $0<\varepsilon<m^2$:

1. In each triangle the cyclic reservations $(x_e-C)^+(C-x_{ak})^+(C-x_{bk})^+/((K-2)(m^2-\varepsilon))$ are positive at most once, and only for an overloaded edge routed through two underloaded ones.
2. If every overloaded edge's reservations cover its excess and no underloaded edge has more reserved through it than it has spare, the loads are routable.
3. $\mathbb E\,Y=m^2/(m^2-\varepsilon)>1$ for $Y=(C-X_2)^+(C-X_3)^+/(m^2-\varepsilon)$.
4. $\mathbb E\,Z=2\,\mathbb E(X-C)^+\,m/(m^2-\varepsilon)<1$ for small $\varepsilon$, for $Z=\big((X_1-C)^+(C-X_2)^++(X_2-C)^+(C-X_1)^+\big)/(m^2-\varepsilon)$.
5. (4.48): $\mathbb P\{\sum_{i\le n} n^{-1}Y_i<1\}\le e^{-nI_1}$ for some $I_1>0$ and all $n\ge 1$.
6. (4.49): $\mathbb P\{\sum_{i\le n} n^{-1}Z_i>1\}\le e^{-nI_2}$ for some $I_2>0$ and all $n\ge 1$, when $X$ has an exponential moment.
7. $1-P(K)\le\tfrac12K(K-1)\,(P_1(K-2)+P_2(K-2))$.

Significance

The result. Theorem 4.45 says that in a large fully connected network, a load distribution whose mean overload is less than half its mean spare capacity can be served, with probability tending to one, using only direct and two-link routes. The factor $2$ reflects that each unit of overflow occupies two edges. The condition is explicit and depends on the load law only through two expectations, which makes it a design rule: capacity $C$ suffices for large networks as soon as (4.46) holds. Comment 4.47 (p. 358) observes that the two-valued law $\mathbb P\{X=2\}=p$, $\mathbb P\{X=0\}=1-p$ with $C=1$ turns (4.46) into Hajek's threshold $p<1/3$.

Formalizing it. The theorem is proved, in full, on one page; nothing here is open. The mission produces a machine-checked version of that proof: a precise routing event on the complete graph, the deterministic reservation argument, two Cramér–Chernoff tail bounds with rates uniform in the network size, and the union bound over edges. To our knowledge none of these steps is formalized anywhere, and no routing-feasibility event on a complete graph exists in Mathlib or on the platform.

Difficulty

The obvious approach is to fix an overloaded edge and argue that, among its $K-2$ two-edge routes, enough pass through two underloaded edges. That count is binomial and concentrates, but it does not prove the theorem: the same underloaded edge sits on two-edge routes of many overloaded pairs, so the reservations of different pairs compete for its spare capacity, and the routing decisions of different pairs are dependent. Any argument has to control, simultaneously at every edge, both the flow an overloaded edge can shed and the flow an underloaded edge is asked to absorb, with exponential rates uniform in $K$ so that a union bound over $\tfrac12K(K-1)$ edges survives; this is the central difficulty. On the upper side the variables are unbounded, so the exponential moment of $X$ has to be carried over to the reserved flows.

Formalization scope

The Lean development lives in the namespace KellyLossNetworks.Routing.

• Edges are {e : Sym2 (Fin K) // ¬ e.IsDiag}; loads are functions Edge K → ℝ.
• The routing event Feasible C x lets each pair split its load arbitrarily over its direct edge and all its two-edge routes, charges a two-edge flow to both edges of its route, requires the flow sent away from a pair not to exceed its load, and imposes the capacity constraint on every edge, including overloaded ones. Flows are real (divisible loads); integer routing is a different problem.
• "Independent and identically distributed" is the product measure Measure.pi (fun _ : Edge K => μ), with μ a probability measure on ℝ and X ≥ 0 almost surely. $P(K)$ is the measure of the routing event; no measurability of that event is presupposed.
• Expectations are Bochner integrals. The exponential moment is integrability of $t\mapsto e^{\theta t}$ for some $\theta>0$; it implies that $(X-C)^+$ is integrable, so (4.46) compares genuine expectations.
• The limit is along $K\in\mathbb N$ with no lower bound on $K$; for $K\le 2$ there are no two-edge routes, which does not affect the limit.
• The rates $I_1,I_2$ in (4.48) and (4.49) are quantified before $n$ and may not depend on it.

A trivializing formalization is ruled out: an event that allows only direct routing, ignores the capacity of the edges a detour passes through, or lets a pair send away more than its load would make the statement false or empty, and the routing event here does none of these.

A complete development needs Fubini on product measures, the Cramér–Chernoff method for averages of i.i.d. variables (both tails, with the lower tail for a bounded nonnegative variable and the upper tail under an exponential moment), measure-preserving projections of Measure.pi, and combinatorics of the triangles through an edge of the complete graph. The Cramér–Chernoff bounds with rates uniform in $n$ are reusable well beyond this mission. Contributions to any milestone are welcome; the deterministic milestones 1–2 and the expectation computations 3–4 are independent of the tail bounds and of each other.

Selected references

• F. P. Kelly, Loss networks, Annals of Applied Probability 1(3):319–378, 1991. doi:10.1214/aoap/1177005872
• B. Hajek, Average case analysis of greedy algorithms for Kelly's triangle problem and the independent set problem, 26th IEEE Conference on Decision and Control, 1987 (reference [22] of the survey; the source of Theorem 4.43).
• H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations, Annals of Mathematical Statistics 23(4):493–507, 1952. doi:10.1214/aoms/1177729330

Motivation

Reliability theory classifies life distributions by how they age. A device whose failure rate tends to increase over time is "wearing out", and the class of distributions with increasing hazard rate average (IHRA) is the one that is closed under forming coherent systems of independent components (Birnbaum, Esary and Marshall, 1966). This makes IHRA the natural ageing class for systems. It also raises a question: which physical failure mechanisms produce IHRA lives?

Esary, Marshall and Proschan's paper Shock Models and Wear Processes (Ann. Probability 1, 1973) answers this for two kinds of mechanism. In the first, damage arrives in discrete amounts at the epochs of a Poisson process of shocks. In the second, damage accumulates continuously. In both, the device fails when the accumulated damage first exceeds a fixed capacity. This mission covers the second kind: a wear process $\{Z(t), t \ge 0\}$ and its first passage time above a level. The paper shows that the first passage time is IHRA under three qualitative conditions: wear starts at zero and only grows, the process is Markov, and accumulated wear and age make further wear more likely. Nothing else is assumed about the law of the wear.

A short timeline. Birnbaum, Esary and Marshall (1966) introduced the IHRA class and proved it is closed under coherent systems. Morey (1965) studied first passage times of wear processes under an extra monotonicity assumption. Esary, Marshall and Proschan (1973), §4, proved the IHRA property first for Poisson shocks with i.i.d. damages (Corollary 4.2, (4.7)), then for dependent damages (Lemma 4.1b, (4.7b)), and finally for continuous wear (Theorem 4.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space. "Decreasing" means non-increasing throughout.

A survival function $\bar F$ is IHRA if $t \mapsto [\bar F(t)]^{1/t}$ is decreasing on $t > 0$ (p. 631). For an exponential life, $[\bar F(t)]^{1/t}$ is constant. IHRA says the average failure rate over $[0, t]$ never decreases.

Dependent damages. Let $X_1, X_2, \dots$ be nonnegative random variables, the damages caused by successive shocks, and let $Z_0 = 0$ and $Z_k = X_1 + \dots + X_k$. The paper's conditions (p. 636) are:

• (4.3) the conditional law of $X_k$ given $X_1, \dots, X_{k-1}$ depends only on $Z_{k-1}$;
• (4.4) $P\{X_k \le u \mid Z_{k-1} = z\}$ is decreasing in $z \ge 0$ (accumulated damage lowers resistance);
• (4.5) $P\{X_k \le u \mid Z_{k-1} = z\} \ge P\{X_{k+1} \le u \mid Z_k = z\}$ for $z \ge 0$ (later shocks are more severe).

Wear process. $Z(t)$ is the wear accumulated in $[0, t]$. The conditions (pp. 640–641) are:

• (4.8) $Z(0) = 0$ and $Z(t + \Delta) - Z(t) \ge 0$ for all $t, \Delta \ge 0$, with probability one;
• (4.9) $\{Z(t), t \ge 0\}$ is a Markov process;
• (4.10) $P\{Z(t + \Delta) - Z(t) \le u \mid Z(t) = z\}$ is decreasing in both $z$ and $t$ in the region $t \ge 0$, $z \ge 0$, $\Delta \ge 0$.

The first passage time above a level $x$ is $T_x = \inf\{t : Z(t) > x\}$. Its survival function is $\bar H_x(t) = P\{T_x > t\}$, and $F_t(x) = P\{Z(t) \le x\}$ is the distribution function of the wear at time $t$.

Formalization targets

Goal: Theorem 4.10 (p. 641)

If $\{Z(t), t \ge 0\}$ satisfies (4.8), (4.9) and (4.10), then for every level $x$

$$t \longmapsto \big[\bar H_x(t)\big]^{1/t} \text{ is decreasing on } t > 0,$$

that is, $T_x$ has an IHRA distribution.

Milestones

1. Lemma 4.1b (p. 637): under (4.3)–(4.5), $[P\{X_1 + \dots + X_k \le x\}]^{1/k}$ is decreasing in $k = 1, 2, \dots$.
2. Proof of Theorem 4.10, first claim (a): for $\Delta > 0$, the grid increments $X_i = Z(i\Delta) - Z((i-1)\Delta)$ satisfy (4.3)–(4.5).
3. Proof of Theorem 4.10, first claim (b): $[F_{k\Delta}(x)]^{1/(k\Delta)}$ is decreasing in $k = 1, 2, \dots$.
4. Proof of Theorem 4.10, second claim: $[F_s(x)]^{1/s} \ge [F_t(x)]^{1/t}$ whenever $0 < s \le t$.
5. Proof of Theorem 4.10, third claim: $\bar H_x(t) = \lim_{\varepsilon \downarrow 0} F_{t+\varepsilon}(x)$, under (4.8) alone.

An optional extra item states Corollary 4.2 (4.7b): Poisson shocks of rate $\lambda > 0$ with damages satisfying (4.3)–(4.5) give an IHRA life $\bar H(t) = \sum_k e^{-\lambda t} (\lambda t)^k / k! \cdot P\{Z_k \le x\}$.

Significance

The result. Theorem 4.10 derives an ageing property of a failure time from qualitative properties of the damage process alone: no distributional form, no stationarity and no independence of increments is assumed. Together with the closure of IHRA under coherent systems, this lets a reliability engineer conclude that a system built from components failing by wear has an IHRA life. Examples include processes with nonnegative stationary independent increments started at the origin, such as compound Poisson processes and infinitesimal renewal processes (p. 641). Lemma 4.1b is the discrete analogue: a sequence of probabilities $\bar P_k$ with $\bar P_k^{1/k}$ decreasing is what Theorem 3.1 (3.4) needs to give an IHRA life under Poisson shocks.

Formalizing it. The results are proved in the paper. As far as we know none of them has been machine-checked. The formalization needs, and would make reusable, a statement of the Markov property for a continuous-time real process in terms of Mathlib's conditional expectation, versions of conditional distributions with monotonicity constraints, and the passage from a discrete-time grid to continuous time for first passage times. Each of these is a step a probabilist writes in one line and a proof assistant does not.

Difficulty

The paper's proof is short, but every sentence hides a measure-theoretic step. The first claim, that the grid increments satisfy (4.3)–(4.5), requires turning the Markov property and the monotonicity of the increment law into conditional laws of $X_{k+1}$ given $(X_1, \dots, X_k)$. Those conditional laws are defined only almost everywhere, and the monotonicity must be preserved along the way. Lemma 4.1b itself is an induction that integrates the monotonicity conditions against the law of $Z_k$. The extension from rational to arbitrary ratios $s/t$ uses the monotonicity of paths. The identification of $\bar H_x(t)$ as a right limit of $F_{t+\varepsilon}(x)$ needs the pathwise reading of (4.8). The natural first idea, approximating $Z$ by a compound Poisson process, would add hypotheses the theorem does not have.

Formalization scope

All objects sit in the namespace ShockWear.WearProcess, in one definition file. The committed conventions:

• Probability space. A measure pr with IsProbabilityMeasure. Time is $\mathbb R_{\ge 0}$; $Z : \mathbb R_{\ge0} \to \Omega \to \mathbb R$ with every $Z(t)$ measurable.
• (4.8) is read pathwise. Almost every path has $Z(0) = 0$ and is nondecreasing. The paper's "for all $t, \Delta \ge 0$ with probability one" is ambiguous in quantifier order; this reading is the one used by the proof's equivalence "$T_x > t$ iff $Z(t+\varepsilon) \le x$ for some $\varepsilon > 0$".
• (4.9) is the Markov property for the natural filtration $\sigma(Z(r), r \le s)$: $P(Z(t) \in B \mid \mathcal F_s) = P(Z(t) \in B \mid Z(s))$ a.s. for $s \le t$ and Borel $B$.
• Conditional probabilities are explicit versions. $P\{X_{k+1} \le u \mid Z_k = z\}$ and $P\{Z(t+\Delta) - Z(t) \le u \mid Z(t) = z\}$ are the values on $(-\infty, u]$ of Markov kernels $\kappa$ that agree almost everywhere with Mathlib's condDistrib. The monotonicity conditions (4.4), (4.5), (4.10) are imposed on these versions, on the paper's regions $z \ge 0$, $t \ge 0$. "Is decreasing in $z$" is read as "has a version decreasing in $z$".
• Nonnegativity of damages is almost sure.
• Index base. Lean's X i is the paper's $X_{i+1}$, and the kernel κ k describes $X_{k+1}$ given $Z_k$.
• First passage time $T_x$ takes values in $[0, \infty]$ and may be infinite with positive probability; it is not assumed finite. $\bar H_x(t) = 1$ for $t < 0$. The level $x$ ranges over all reals.
• Powers $[\,\cdot\,]^{1/t}$, $[\,\cdot\,]^{1/k}$, $[\,\cdot\,]^{1/(k\Delta)}$ are real powers with real exponents.

Trivializing formalizations are ruled out: (4.9) and (4.10) are not replaced by independence or stationarity of increments, nor by a compound Poisson model. Those are examples (p. 641), not hypotheses. Monotonicity is never imposed on Mathlib's condDistrib itself, whose values off the support of $Z(t)$ are unconstrained. A sorry-free local check confirms the hypotheses are satisfiable: the deterministic process $Z(t) = t$ satisfies (4.8)–(4.10), and constant damages satisfy (4.3)–(4.5).

Contributions are welcome on any milestone. The reduction (milestone 2) and the induction of Lemma 4.1b are the substantial parts. Lemmas about versions of conditional distributions under Markov processes would be reusable well beyond this mission.

Selected references

• J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, Ann. Probability 1(4) (1973) 627–649. https://doi.org/10.1214/aop/1176996891
• Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-out for Components and Systems, Ann. Math. Statist. 37 (1966) 816–825. https://doi.org/10.1214/aoms/1177699362
• R. C. Morey, Stochastic Wear Processes, Technical Report ORC 65-16, Operations Research Center, University of California, Berkeley, 1965 (cited on p. 640 of Esary, Marshall and Proschan).
• R. E. Barlow and F. Proschan, Statistical Theory of Reliability and Life Testing, Holt, Rinehart and Winston, 1975.

Motivation

Reliability theory classifies life distributions by how they age. A device whose remaining life, once it has survived to age $t$, is stochastically shorter than the life of a new device is called new better than used (NBU). The NBU class, together with the classes IHR (increasing hazard rate) and IHRA (increasing hazard rate average), organizes much of the theory of maintenance and replacement: Marshall and Proschan showed that the NBU property is what makes certain replacement policies beneficial, and Barlow and Proschan's monographs build the statistical theory of reliability on these classes.

A question that runs through this literature is where such ageing properties come from physically. Esary, Marshall and Proschan (Ann. Probability 1973) answer it for shock models: a device is hit by shocks arriving in time as a Poisson process, each shock adds a random amount of damage, and the device fails when the accumulated damage exceeds its threshold. Section 4 of their paper treats a fixed threshold and shows that the life is IHRA for every damage law. Section 5, the subject of this mission, lets the threshold itself be random, which models the variation between individual items of a production lot. It then asks which ageing properties of the threshold law are inherited by the life distribution, and which are forced if the inheritance is to hold whatever the damage law.

Setting

All distributions are laws of non-negative random variables. For a distribution $F$ on $\mathbb R$ with $F(z) = 0$ for $z < 0$ (a damage law), $F^{(k)}$ denotes the $k$-fold convolution of $F$, with $F^{(0)}$ the point mass at $0$; thus $F^{(k)}(x) = P\{X_1 + \cdots + X_k \le x\}$ for independent $X_i \sim F$.

A threshold law is a distribution $G$ with $G(z) = 0$ for $z < 0$; write $\bar G = 1 - G$ for its survival function. If the threshold $Y \sim G$ is independent of the damages, the probability of surviving $k$ shocks is

$$\bar P_k = \int_0^\infty F^{(k)}(x)\, dG(x) = P\{X_1 + \cdots + X_k \le Y\}, \qquad k = 0, 1, \dots \tag{5.1}$$

If shocks arrive as a Poisson process of rate $\lambda > 0$, the device's life distribution $H$ has survival function

$$\bar H(t) = \sum_{k=0}^\infty e^{-\lambda t}\frac{(\lambda t)^k}{k!}\,\bar P_k, \qquad t \ge 0. \tag{5.2}$$

A survival function $\bar F$ is NBU if $\bar F(t + x) \le \bar F(x)\bar F(t)$ for all $x, t \ge 0$; it is IHR if $\bar F(x + t)/\bar F(t)$ is non-increasing in $t$ for each $x > 0$, and IHRA if $[\bar F(t)]^{1/t}$ is non-increasing in $t > 0$. The discrete analogue of NBU for the sequence $\bar P_k$ is submultiplicativity, $\bar P_{j+k} \le \bar P_j \bar P_k$.

Formalization targets

Goal: Theorem 5.3

For a threshold law $G$ with $G(z) = 0$ for $z < 0$:

$$\Big(\forall F:\ \bar P_{j+k} \le \bar P_j\,\bar P_k \ \ \forall j,k \ge 0\Big) \iff \bar G \text{ is NBU},$$

the quantifier ranging over every damage law $F$; and if $G$ is NBU, then for every damage law $F$ and every $\lambda > 0$ the life distribution $H$ of (5.2) is NBU.

Milestones

1. Theorem 3.1 (3.5). For any sequence $1 = \bar P_0 \ge \bar P_1 \ge \cdots \ge 0$ and $\lambda > 0$: if $\bar P_j \bar P_k \ge \bar P_{j+k}$ for all $j, k$, then $H$ of (2.1) is NBU.
2. First display of the proof of Theorem 5.3. If $G$ is NBU, then $\bar P_{j+k} \le \bar P_j \bar P_k$ for each damage law $F$.
3. Second display of the proof of Theorem 5.3. If submultiplicativity holds for every $F$, then $\bar G(s + j x_k) \le \bar G(s)\,\bar G(j x_k)$ for $s > 0$, $x_k = s/k$, $j = 0, 1, \dots$.

Further items (not milestones)

Theorem 5.1 (the life is exponential for every $F$ iff $G$ is exponential) and Theorem 5.2 (b), (c) (an IHR threshold makes $\bar P_k^{1/k}$ non-increasing for every $F$; non-increasing $\bar P_k^{1/k}$ for every $F$ forces $G$ to be IHRA) are posed as companion statements from the same section.

Significance

Theorem 5.3 is a characterization: the NBU class is exactly the class of threshold laws for which the cumulative-damage mechanism preserves the discrete NBU property under every damage law. Combined with Theorem 3.1 (3.5), it gives a physical derivation of NBU life distributions: an item with an NBU random strength, subject to Poisson shocks with arbitrary i.i.d. non-negative damage, has an NBU life. Theorems 5.1 and 5.2 place the exponential and the IHR/IHRA classes in the same framework, and the authors record that whether an IHRA threshold suffices in Theorem 5.2 (b) is left unresolved.

The results are proved in the paper. No machine-checked version is known to exist; this mission produces one. A complete development also supplies reusable infrastructure: convolution powers of laws on $[0, \infty)$ as Mathlib measures, Poisson mixtures of a sequence, and the ageing classes of p. 631 as predicates on survival functions.

Difficulty

The equivalence couples a property of one function, $\bar G$, to a family of inequalities indexed by every damage law, and the left side is about convolutions while the right side is pointwise. Two points make the statement harder than it looks. First, (5.1) as printed is $P\{X_1 + \cdots + X_k \le Y\}$, whereas the paper's proof works with $E\bar G(X_1 + \cdots + X_k) = P\{X_1 + \cdots + X_k < Y\}$; the two agree only when $F^{(k)}$ and $G$ have no common discontinuities, and they can disagree as soon as $F^{(k)}$ has an atom where $G$ has one, a case the left side of the equivalence includes. A formal proof cannot invoke that convention. Second, the second sentence of the theorem passes through a Poisson series (5.2) whose terms involve the whole sequence $\bar P_k$, so the NBU property of $H$ is a statement about a power series in $t$, not about any single $\bar P_k$.

Formalization scope

• A distribution is a probability measure on $\mathbb R$; "$F(z) = 0$ for $z < 0$" is mass $0$ on $(-\infty, 0)$, and "$G(0) = 0$" (Theorems 5.1, 5.2) is mass $0$ on $(-\infty, 0]$. $F^{(k)}$ is the $k$-fold Measure.conv power with $F^{(0)} = \delta_0$, and $F^{(k)}(x)$ is the mass of $(-\infty, x]$.
• $\bar P_k$ is (5.1) as printed, $\int F^{(k)}(x)\,dG(x)$ over $\mathbb R$; since $G$ is carried by $[0, \infty)$ this is $\int_0^\infty$ including an atom of $G$ at $0$, which Theorem 5.3 allows. The paper's convention that $F^{(k)}$ and $G$ have no common discontinuities is not added as a hypothesis: the statements hold for (5.1) without it. The integrand is monotone with values in $[0,1]$, so the Bochner integral is a genuine expectation.
• "For all $F$" sits inside the equivalence of Theorem 5.3 and ranges over every probability measure on $[0, \infty)$. Submultiplicativity for one fixed $F$ is a different, weaker statement.
• NBU and IHR are cross-multiplied, agreeing with the paper's ratio form wherever denominators are positive (the paper restricts variables to avoid zero denominators). NBU is on $x, t \ge 0$ exactly as in definition (v). Powers $[\bar G(t)]^{1/t}$ and $\bar P_k^{1/k}$ are real powers. "Decreasing" means non-increasing.
• $H$ is the series (2.1) as a function on $\mathbb R$, equal to $1$ on $(-\infty, 0)$; $\lambda > 0$ as in (1.1). In Theorem 3.1 (3.5) the non-negativity $\bar P_k \ge 0$ is stated explicitly.
• In Theorem 5.1 "exponential" allows rate $0$ for $H$ (the damage law $\delta_0$ gives $\bar H \equiv 1$) and requires a positive rate for $G$ ($G(0) = 0$ rules out the degenerate case $\bar G = 0$ on $(0,\infty)$).
• A trivializing formalization is ruled out: the threshold-law quantifier is not restricted to a class where both sides are automatic, the integral cannot collapse to a default value, and the NBU predicate is the paper's on $[0, \infty)$, not on $(0, \infty)$ or a vacuous domain.

Contributions welcome: proofs of the milestones, a library for Poisson mixtures and convolution powers of laws on $[0,\infty)$, and the extra items of §5.

Selected references

• J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, The Annals of Probability 1(4), 627–649, 1973. https://doi.org/10.1214/aop/1176996891
• R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965; reprinted SIAM Classics in Applied Mathematics, 1996. https://doi.org/10.1137/1.9781611971194
• Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-Out for Components and Systems, The Annals of Mathematical Statistics 37(4), 816–825, 1966. https://doi.org/10.1214/aoms/1177699362

Motivation

Many models in probability, statistical physics and the theory of stochastic networks are interacting particle systems: infinitely many sites, each in state 0 or 1, each updating at random according to the states of a few other sites. A basic question about such a system is ergodicity: does it have a unique stationary distribution, and does its law converge to it from every initial configuration? For infinite systems the question is hard, because the state space $\{0,1\}^I$ is uncountable and standard Markov chain arguments do not apply.

Holley and Liggett (Ann. Probab. 3 (1975), 643–663) introduced a class of such systems, the proximity processes, which arise from a coupling of more general weakly interacting systems (the settings of Vasershtein (1969), Dobrushin (1971) and Chover (1974)), and showed that each proximity process is dual to a process of finite sets, the branching process with interference. Duality turns a question about an infinite-dimensional process into a question about a process whose states are finite sets. The paper uses it to give short proofs of ergodicity criteria and, in its §5, to study the invariant measures of the voter model. Duality of this kind became one of the main tools of the field; see Liggett, Interacting Particle Systems (Springer, 1985).

This mission formalizes the discrete-time half of the paper: the duality theorem (1.6) and its first applications, Corollary (3.1) and Corollary (4.1).

Setting

Let $I$ be a countable set of sites and $S=\{0,1\}^I$ the set of configurations $\eta:I\to\{0,1\}$, with the product $\sigma$-algebra. For $\eta\in S$, $C(\eta)=\{i\in I:\eta(i)=1\}$ is the set of occupied sites.

The data of the model are, for each site $i$, a sequence $N_{i,0}=\emptyset,N_{i,1},N_{i,2},\dots$ of finite subsets of $I$ and a probability distribution $f_i$ on $\{0,1,2,\dots\}$.

The proximity process $\eta_n$ is the Markov chain on $S$ whose transition function is the product measure

$$Q(\eta,\cdot)=\prod_{i\in I}\nu_{\alpha(i,\eta),i},\qquad \alpha(i,\eta)=\sum_{k:\,N_{i,k}\cap C(\eta)\neq\emptyset}f_i(k),$$

where $\nu_{\rho,i}$ puts mass $\rho$ on $1$. In words: each site $i$ independently picks an index $k$ with probability $f_i(k)$ and becomes $1$ exactly when the set $N_{i,k}$ contains an occupied site. $P_\eta(\eta_n\in\cdot)$ denotes the law at time $n$ started from $\eta$.

The branching process with interference (b.p.i.) $A_n$ is the Markov chain on the collection $\mathcal T$ of finite subsets of $I$ with transition function

$$\tilde Q(A,B)=\sum{}'\prod_{i\in A}f_i(k_i),$$

the sum over all sequences $(k_i)_{i\in A}$ with $\bigcup_{i\in A}N_{i,k_i}=B$: each particle at $i$ splits into particles on $N_{i,k}$ with probability $f_i(k)$, and particles landing on the same site merge. $P_F$ denotes probabilities for the chain started at $F$.

For $F\in\mathcal T$, $B(F)=\{\eta\in S:\eta(i)=0\ \text{for all } i\in F\}$.

Formalization targets

Goal: Theorem (1.6)

For all $n\ge0$, $\eta\in S$ and $F\in\mathcal T$,

$$P_\eta(\eta_n\in B(F))=P_F(A_n\cap C(\eta)=\emptyset).$$

Milestones

The proof is an induction on $n$ whose steps are four displayed identities on p. 647:

1. (2.3) the one-step law of the proximity process on $B(F)$: $P_\eta(\eta_1\in B(F))=\sum'\prod_{i\in F}f_i(k_i)$, the sum over sequences with $N_{i,k_i}\cap C(\eta)=\emptyset$ for all $i\in F$;
2. (2.4) the same expression for $P_F(A_1\cap C(\eta)=\emptyset)$;
3. (2.5) the first-step decomposition $P_F(A_{n+1}\cap C(\eta)=\emptyset)=\sum_{(k_i)}P_{\bigcup_{i\in F}N_{i,k_i}}(A_n\cap C(\eta)=\emptyset)\prod_{i\in F}f_i(k_i)$;
4. (2.8) the last-step decomposition $P_\eta(\eta_{n+1}\in B(F))=\sum_{(k_i)}P_\eta(\eta_n\in B(\bigcup_{i\in F}N_{i,k_i}))\prod_{i\in F}f_i(k_i)$.

Applications

• Corollary (3.1): if $\sum_k|N_{i,k}|f_i(k)\le\lambda<1$ for all $i$, then

$$P_\eta(\eta_n\in B(F))\ge1-\lambda^n|F|,$$

and the point mass on the all-zero configuration is the only stationary distribution; along the way, (3.5): $P_F(A_n\neq\emptyset)\le E_F|A_n|\le\lambda^n|F|$.

• (4.5): for the §4 model on $\mathbb Z$, $P_{F\cup G}(A_t\neq\emptyset)\le P_F(A_t\neq\emptyset)+P_G(A_t\neq\emptyset)-P_{F\cap G}(A_t\neq\emptyset)$.
• Corollary (4.1): on $I=\mathbb Z$ with $N_{i,1}=\{i-1,i+1\}$, $f_i(0)=1-\lambda$, $f_i(1)=\lambda$, and $h(\lambda)=2\lambda+2\lambda^2-7\lambda^3+5\lambda^4-\lambda^5$,

$$P_\eta(\eta_t\in B(F))\ge1-[h(\lambda)]^{(t-1)/2}|F|\qquad(t\ge1).$$

Significance

The duality identity expresses every finite-dimensional "all vacant" probability of the proximity process, which determine its law, through a chain on finite sets. Consequences in the paper: a sufficient condition for convergence to the all-zero configuration (Corollary (3.1)), which in the nearest-neighbour example on $\mathbb Z$ gives $\lambda<\tfrac12$; the sharper range $h(\lambda)<1$, i.e. $\lambda<0.6527$, for that example (Corollary (4.1)), which the interference term makes possible; and, in continuous time, the analysis of the invariant measures of the voter model.

The results are classical and proved; a search of Prove2Me and Mathlib found no machine-checked proof of any of them. A formalization contributes a Lean model of an infinite-product Markov kernel on $\{0,1\}^I$ with its $n$-step laws, a model of a set-valued branching chain, and the duality between them, which are reusable for other duality arguments (contact process, voter model, coalescing random walks).

Difficulty

The two sides of (1.7) are defined independently and live on different spaces. The left side is the time-$n$ law of a chain on the uncountable space $\{0,1\}^I$, obtained by iterating an infinite product kernel; the right side comes from a transition matrix on the countable set of finite subsets of $I$, whose entries are themselves infinite sums over sequences indexed by a finite set. Neither side can be computed in closed form beyond $n=1$, so no direct evaluation proves the identity for general $n$.

Two technical points stand in the way of a naive argument. Evaluating a product kernel on a cylinder event and integrating it against a previous law requires the kernel to be measurable in $\eta$, a statement about cylinder sets of an infinite product that a hand proof passes over. And the natural recursion for $n$-step probabilities of the b.p.i. adds the new step at the end, while the comparison with the proximity process needs information about the first step; the two orders agree only by a Chapman–Kolmogorov argument over a countable state space with $[0,\infty]$-valued sums. Corollary (4.1) further needs quantitative estimates of survival probabilities for specific initial sets on $\mathbb Z$.

Formalization scope

All objects are in the namespace HolleyLiggett.Duality, in one definitions file.

• $\{0,1\}$ is Bool (true = 1), $S$ is Config I := I → Bool with the product $\sigma$-algebra, $\mathcal T$ is Finset I.
• Standing assumptions on every theorem: [Countable I], N : I → ℕ → Finset I (finite sets) with N i 0 = ∅, and f : I → PMF ℕ (probability distributions). A finite collection $N_{i,0},\dots,N_{i,m}$ is the case $f_i(k)=0$ for $k>m$.
• The kernel (1.1) is Measure.infinitePi of the two-point measures; the $n$-step law is proxLaw, iterating Measure.bind from the point mass at $\eta$. Measurability of the kernel is a true fact that solvers must prove; it is not assumed.
• The b.p.i. $n$-step probabilities bpiProb follow the last-step recursion $P_F(A_{n+1}=B)=\sum_GP_F(A_n=G)\tilde Q(G,B)$. All probabilities are in ℝ≥0∞, and each $\sum'$ over sequences is an unconditional sum over ↥F → ℕ.
• The page's "$\eta(1)=1$" in (1.2) is read as $\eta(i)=1$. Corollary (4.1) carries the added hypothesis $t\ge1$: at $t=0$ the printed bound fails when $h(\lambda)>1$, and the proof starts at $t=1$. Inequality (4.5) uses the §4 model on $\mathbb Z$, with the subtracted term moved across.
• The goal relates the two chains defined by (1.1) and (1.4). A statement through the coupling $X_{i,n}$ of the proof, about an arbitrary process with the right one-step behaviour, or for $n=1$ only, is not the theorem.

The continuous-time duality (Theorem (2.12)), Corollaries (3.9) and (4.15) and the voter model of §5 are out of scope. Contributions welcome: the measurability and probability facts for proxStep, Chapman–Kolmogorov for bpiProb, and proofs of the milestones.

Selected references

• R. A. Holley and T. M. Liggett, Ergodic theorems for weakly interacting infinite systems and the voter model, Ann. Probab. 3(4) (1975), 643–663. https://doi.org/10.1214/aop/1176996306
• T. M. Liggett, Interacting Particle Systems, Grundlehren der mathematischen Wissenschaften 276, Springer, 1985. https://doi.org/10.1007/978-1-4613-8542-4
• R. L. Dobrushin, Markov processes with a large number of locally interacting components (Russian), Problems of Information Transmission 7(2) (1971), 70–87 (as cited by Holley and Liggett).
• O. N. Stavskaya and I. I. Pyatetskii-Shapiro, On homogeneous nets of spontaneously active elements, Systems Theory Research 20 (1971), 75–88 (as cited by Holley and Liggett).
• L. N. Vasershtein, Processes over denumerable products of spaces, describing large systems, Problems of Information Transmission 3 (1969), 47–52 (as cited by Holley and Liggett).

Motivation

Little's law $L = \lambda W$ says that the long-run average number of customers in a system equals the arrival rate times the average time a customer spends there. It is one of the most used identities in queueing theory, and it holds on individual sample paths under weak conditions (Little 1961; Stidham 1974). Many quantities of interest are not head counts, however: the work in the system, the cost accumulated by customers in progress, the number of tokens a customer holds in some state. For these a more general relation is needed, between a time average $H$ and a customer average $G$, of the form $H = \lambda G$.

Heyman and Stidham (Oper. Res. 28 (1980)) prove such a relation on each sample path, for an arbitrary real-valued function attached to each customer, under a support condition that is much weaker than the continuous-sojourn assumption of the $L = \lambda W$ theorem. They then show by a counterexample that the support condition cannot simply be dropped, even when every customer function is an indicator.

Timeline.

• 1961: Little proves $L = \lambda W$ under stationarity assumptions (Little 1961).
• 1971: Brumelle proves $H = \lambda G$ under conditions (v.a), (v.b) on the tails of the $f_n$ (J. Appl. Prob. 8, 508–520).
• 1972: Stidham gives a new proof of $L = \lambda W$, including the lemma relating $N(t)/t$ and $t_n/n$ (Stidham 1972).
• 1974: Stidham proves $L = \lambda W$ on each sample path, assuming each sojourn is one uninterrupted interval (Stidham 1974).
• 1980: Heyman and Stidham prove $H = \lambda G$ on every sample path under the support condition below, and give the counterexample. The paper notes that its Theorem 1 is weaker than the sample-path version of Brumelle's theorem, with hypotheses stated directly on the sample path.

Setting

Fix one sample path. Customers $n = 1, 2, \ldots$ arrive at epochs $0 \le t_1 \le t_2 \le \cdots$; ties are allowed. The arrival count $N(t)$ is the number of $n$ with $t_n \le t$, and the arrival rate is $\lambda = \lim_{t\to\infty} N(t)/t$ when the limit exists.

Customer $n$ carries a real-valued function $f_n$ on $[0,\infty)$. Its total is $g_n = \int_0^\infty f_n(t)\,dt$, and the rate is $h(t) = \sum_{n=1}^\infty f_n(t)$. The customer average and time average are

$$G = \lim_{N\to\infty} \frac1N \sum_{n=1}^N g_n, \qquad H = \lim_{T\to\infty} \frac1T \int_0^T h(t)\,dt .$$

When $f_n$ is the indicator of $[t_n, t_n + W_n)$, $g_n = W_n$ is the sojourn time and $h(t)$ is the number in system, so $H = \lambda G$ is $L = \lambda W$.

The ASSUMPTION of the paper is that for each $n$ there is $s_n \in [0,\infty)$ with

1. (i) $f_n(t) = 0$ for $t \notin [t_n, t_n + s_n]$;
2. (ii) $s_n / n \to 0$.

For signed $f_n$ write $f_n^+ = \max[0, f_n]$, $f_n^- = \max[0, -f_n]$, and let $g_n^\pm$, $h^\pm$, $G^\pm$, $H^\pm$ be the corresponding totals, rates and averages.

Formalization targets

Goal: Theorem 2 (p. 986)

Assume (i), (ii) and (v) $\int_0^\infty |f_n(t)|\,dt < \infty$ for every $n$. If $\lambda$, $G^+$ and $G^-$ exist with $0 < \lambda < \infty$ and $G^\pm < \infty$, then $G$ exists, equals $G^+ - G^-$, $H$ exists, and

$$H = \lambda G. \tag{1}$$

Milestones

• (2): for $0 < \lambda < \infty$, $N(t)/t \to \lambda$ if and only if $t_n / n \to \lambda^{-1}$.
• (3): for $f_n \ge 0$, $V(T) \le \int_0^T h(t)\,dt \le U(T)$, where $U(T)$ sums $g_n$ over arrived customers and $V(T)$ over customers with $t_n + s_n \le T$.
• (4): $\lambda G = \lim_{t\to\infty} U(t)/t$.
• $s_n / t_n \to 0$, and $\lim U(t)/t = \lim V(t)/t$.
• Theorem 1 (p. 985): for $f_n \ge 0$ under (i)–(iv), $H = \lambda G$.
• The identity $\int_0^T h^+ - \int_0^T h^- = \int_0^T h$ and (6): $G = G^+ - G^-$, $H = H^+ - H^-$.

Companion results

• The §3 counterexample: $t_n = n$, indicator $f_n$ with $g_n = 1$, so $\lambda = G = 1$, but $H = \log 2$; its support span $s_n = n$ satisfies (i) and fails (ii).
• Corollary 3 (p. 988): if $\lambda(\omega) = \lambda$ is constant, the ensemble averages satisfy $\int H\,dP = \lambda \int G\,dP$.
• $G = W < \infty$ implies $W_n / n \to 0$ (p. 986), the step by which Theorem 1 contains $L = \lambda W$.

Significance

The result. $H = \lambda G$ converts between a time average, which is what a system designer measures, and a customer average, which is what a customer experiences. Applied to different $f_n$ it yields $L = \lambda W$, the relation between average work in system and average customer work, and relations between time-stationary and embedded-chain probabilities; §2 of the paper derives the GI/M/c/K relation this way. Because the support condition (i)–(ii) allows a customer's contribution to be interrupted (leaving and re-entering the system), it covers preemptive priority queues and nodes of networks, which the continuous-sojourn $L = \lambda W$ theorem does not. The counterexample marks the boundary: with interrupted sojourns, indicator functions and finite $\lambda$, $G$ alone do not suffice.

Formalizing it. The result is proved on paper, with two steps delegated to earlier work "by mimicking" Lemma 1 and Theorem 2 of Stidham 1974. The indicator special case $L = \lambda W$ (with strictly increasing arrivals) is already proved on Prove2Me as queueing_general_littles_law (wenxinzhang). This mission asks for the general, signed, pathwise statement and its proof steps, a counterexample with an exactly computed time average $\log 2$, and the ensemble corollary.

Difficulty

The obvious argument, exchanging the time integral of $h$ with the sum over customers, gives $\int_0^T h = \sum_n \int_0^T f_n$, but a customer that has arrived by $T$ may contribute only part of its total $g_n$ by $T$. The sandwich $V(T) \le \int_0^T h \le U(T)$ only bounds this loss; the hard step is showing that $U(t)/t$ and $V(t)/t$ have the same limit, which needs $s_n / t_n \to 0$ to compare $V$ at time $t$ with $U$ at a slightly earlier time. Without (ii) this fails, as the counterexample shows: customers there remain "open" for a window proportional to their index.

For signed $f_n$ the sandwich is not available directly, and the proof splits $f_n$ into positive and negative parts; the exchange of sum and integral then needs the finiteness of the parts on every $[0,T]$.

Formalization scope

All statements except Corollary 3 are about one fixed sample path; the paper's "with probability one" is the pathwise statement applied to almost every path, and Corollary 3 states this explicitly with a probability measure and almost-sure hypotheses.

Conventions:

• Customers are indexed from $0$ in Lean; index $n$ is the paper's customer $n+1$, so $s_n/n \to 0$ is written $s_n/(n+1) \to 0$.
• Arrival epochs are Monotone with $t_0 \ge 0$; ties are allowed.
• $f_n : \mathbb R \to \mathbb R$, but only values on $[0,\infty)$ enter: (i) is required only for $t \ge 0$, $g_n$ integrates over $[0,\infty)$, and time averages integrate over $[0,T]$.
• (iv) and (v) are stated as integrability of $f_n$ on $[0,\infty)$; the page prints (iv) as "$\le \infty$", a misprint for "$< \infty$".
• $N(t)$ is the cardinality of $\{n : t_n \le t\}$; $h$, $U$, $V$ are infinite sums over all customers.
• "$H$ exists" includes integrability of $h$ on every $[0,T]$.
• The page prints (6) as "$G = G^+ - G^+$"; the stated identity is $G = G^+ - G^-$, as the proof shows.

Added hypotheses: milestones (3), the $h^\pm$ identity and (6) assume $t_n \to \infty$, which the paper derives from (2); Corollary 3 assumes $G(\omega)$ is integrable, which its definition of the ensemble average presupposes.

A formalization in which $h$ sums only over arrived customers, or in which a non-integrable $h$ or $f_n$ has integral $0$, would make the statements trivial or different; the definitions rule this out by summing over all customers and requiring integrability.

Needed infrastructure: Cesàro averages and counting functions of nondecreasing sequences, interchange of countable sums and integrals for locally finite families, and harmonic sums $\sum_{m=\lceil (k+1)/2\rceil}^{k} 1/m \to \log 2$. The counting-function lemma (2) and the squeeze for $U$ and $V$ are reusable well beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• D. P. Heyman and S. Stidham, Jr., The relation between customer and time averages in queues, Operations Research 28(4):983–994, 1980. https://doi.org/10.1287/opre.28.4.983
• J. D. C. Little, A proof for the queuing formula: L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
• S. Stidham, Jr., L = λW: a discounted analogue and a new proof, Operations Research 20(6):1115–1126, 1972. https://doi.org/10.1287/opre.20.6.1115
• S. Stidham, Jr., A last word on L = λW, Operations Research 22(2):417–421, 1974. https://doi.org/10.1287/opre.22.2.417
• S. L. Brumelle, On the relation between customer and time averages in queues, Journal of Applied Probability 8:508–520, 1971.