Probability

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.

Motivation

Reliability theory classifies life distributions by how they age. The IHRA class (increasing hazard rate average) is the smallest class of life distributions that contains the exponential distributions and is closed under forming coherent systems and taking limits in distribution (Birnbaum, Esary and Marshall 1966). It is therefore the natural class for the lifetime of a system built from components that wear out. A distribution belongs to it when its survival function $\bar F$ satisfies: $[\bar F(t)]^{1/t}$ is decreasing in $t > 0$.

Esary, Marshall and Proschan (Ann. Probability 1 (1973) 627–649) asked where such ageing comes from physically. Their answer is a shock model: a device receives shocks at the epochs of a Poisson process, each shock does random damage, and the device fails when the accumulated damage exceeds its capacity. The central result of their §4, formalized in this mission, is that this model always produces an IHRA life, whatever the damage distribution. In the authors' words, "the IHRA property has been obtained … as an implication of a natural physical model. The only hypothesis imposed upon $F$ is that it be the distribution of a nonnegative random variable." The paper is a standard reference of reliability theory and the source of the cumulative damage model used across maintenance and insurance applications.

Setting

Shocks arrive according to a Poisson process with rate $\lambda > 0$. Write $\bar P_k$ for the probability that the device survives the first $k$ shocks; then $1 \ge \bar P_0 \ge \bar P_1 \ge \dots \ge 0$ (display (2.2)). Conditioning on the number of shocks in $[0, t]$ gives the shock survival function (2.1):

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

with $\bar H(t) = 1$ for $t < 0$. The weights $K(k,t) = e^{-\lambda t}(\lambda t)^k/k!$ are the Poisson probabilities.

In the cumulative damage model the $i$th shock causes a damage $X_i \ge 0$, the damages are independent with common distribution function $F$ (so $F(z) = 0$ for $z < 0$), and the device survives $k$ shocks when $X_1 + \dots + X_k \le x$, for a fixed threshold $x$. Hence (4.1)

$$\bar P_k = F^{(k)}(x), \qquad k = 0, 1, \dots,$$

where $F^{(k)}$ is the $k$-fold convolution of $F$ and $F^{(0)}$ is degenerate at $0$. A distribution with survival function $\bar F$ is IHRA if $[\bar F(t)]^{1/t}$ is decreasing in $t > 0$; throughout, "decreasing" means non-increasing.

Formalization targets

Goal: Corollary 4.2, display (4.7)

For every distribution $F$ on $[0,\infty)$, every $\lambda > 0$ and every threshold $x$,

$$\bar H(t) = \sum_{k=0}^\infty e^{-\lambda t}\frac{(\lambda t)^k}{k!} F^{(k)}(x) \quad \text{is IHRA.}$$

This is the first of the three statements of Corollary 4.2; the second ((4.7a), independent damages $F_i$ that worsen with $i$) is an extra item of this mission, and the third ((4.7b), dependent damages satisfying (4.3)–(4.5)) belongs to mission III of this series.

Milestones

1. (2.6): $\bar H(t) \ge \bar H(0)e^{-\lambda t}$ for $t \ge 0$.
2. Theorem 3.1 (3.4) through the three claims of its proof (p. 633): if $1 = \bar P_0 \ge \bar P_1 \ge \dots$ and $\bar P_k^{1/k}$ is decreasing in $k \ge 1$, then $\bar P_k - \zeta^k$ ($0 \le \zeta \le 1$) has at most one sign change, from $+$ to $-$; this property passes to $\bar H(t) - e^{-(1-\zeta)\lambda t}$ on $t \ge 0$; hence $\bar H(t) - e^{-\theta t}$ has at most one sign change for every $\theta > 0$; and $H$ is IHRA.
3. Lemma 4.1: for $F$ on $[0,\infty)$, $[F^{(k)}(x)]^{1/k}$ is decreasing in $k = 1, 2, \dots$.

Further items

Lemma 4.1a and Corollary 4.2 (4.7a); Theorem 4.4 ($[F^{(k)}(x)]^{1/k}$ is constant in $k$ iff $F$ has no mass in $(0,x]$); Corollary 4.5 ((4.7) is exponential iff $F$ has no mass in $(0,x]$); Corollary 4.11 ($[P\{N(x) \ge k\}]^{1/k}$ is decreasing for the count $N(x)$ of an ordinary renewal process).

Significance

The goal turns a modelling assumption into a theorem: anyone who models failure as accumulated nonnegative damage under Poisson shocks obtains, without further checks, every consequence of IHRA proved in reliability theory, including the closure of the class under the formation of coherent systems. Theorem 3.1 (3.4) is reusable on its own: it reduces the IHRA property of any Poisson mixture to a discrete condition on the $\bar P_k$, and the same scheme drives the first passage result for wear processes (Theorem 4.10, mission III). Lemma 4.1, applied to renewal processes, gives Corollary 4.11, a statement about renewal counts with no shock model in sight.

All results are proved in the paper; none has a machine-checked proof that we know of. The Mathlib library has the Poisson distribution and the convolution of measures, but no reliability classes, no total positivity and no variation diminishing property. The mission's output is a formal proof of the paper's chain of results and, along the way, reusable statements about Poisson mixtures and convolution powers.

Difficulty

Two steps resist a direct argument. The first is the transfer from sequences to functions: knowing that $\bar P_k - \zeta^k$ changes sign at most once says nothing pointwise about the series $\sum_k(\bar P_k - \zeta^k)K(k,t)$. The paper invokes the variation diminishing property of the totally positive Poisson kernel (Karlin, Total Positivity, 1968), which is not in Mathlib. The second is Lemma 4.1, an inequality between convolution powers of an arbitrary law: no density, moments or continuity may be assumed, atoms at $0$ and at $x$ are allowed, so any argument through densities or Laplace transforms loses generality. A further subtlety is the passage from "one sign change of $\bar H(t) - e^{-\theta t}$ for every $\theta$" to the monotonicity of $[\bar H(t)]^{1/t}$, which needs care where $\bar H$ vanishes.

Formalization scope

• A distribution $F$ with $F(z) = 0$ for $z < 0$ is a probability measure $\mu$ on $\mathbb R$ with $\mu(-\infty,0) = 0$; nothing else is assumed. $F^{(k)}$ is the $k$-fold additive convolution of $\mu$ (Mathlib's Measure.conv) starting from the point mass at $0$, and $F^{(k)}(x)$ is the real number $F^{(k)}(-\infty,x]$.
• $\bar H$ is the series (2.1) as a function on $\mathbb R$, equal to $1$ on $t < 0$. It is never defined through a constructed random failure time, and IHRA is never encoded through a condition on the $\bar P_k$: the goal concludes that $[\bar H(t)]^{1/t}$ is decreasing on $t > 0$ for the series itself. This rules out the trivializing reading in which the goal unfolds to Lemma 4.1.
• Powers $[\bar H(t)]^{1/t}$ and $\bar P_k^{1/k}$ are real powers with exponent $1/t$, $1/k$ in $\mathbb R$.
• Hypotheses the paper leaves implicit and the Lean statements make explicit: $\lambda > 0$; $\bar P_k \ge 0$ (the $\bar P_k$ are probabilities); in Corollary 4.5, $x \ge 0$ (the threshold is a capacity), and "exponential" includes the degenerate rate $0$.
• Sign change statements about $\bar H$ hold on $t \ge 0$, where the series defines it.
• The threshold $x$ in the goal ranges over all reals, as printed.
• In Corollary 4.11 the renewal process is given by independent measurable interarrival times with common law $\mu$, and $N(x) = \#\{k \ge 1 : X_1 + \dots + X_k \le x\}$ takes values in $\{0, 1, \dots, \infty\}$.

A complete development needs: the variation diminishing property of the Poisson kernel (reusable for every Poisson mixture), monotonicity of $[F^{(k)}(x)]^{1/k}$ via convolution integrals, and elementary facts about real powers and sign changes. Proofs of any milestone or extra item, and general total positivity lemmas, are welcome.

Selected references

• J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, The Annals of 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, The Annals of Mathematical Statistics 37 (1966) 816–825. https://doi.org/10.1214/aoms/1177699362
• S. Karlin, Total Positivity, Vol. I, Stanford University Press, 1968.
• R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965. https://doi.org/10.1137/1.9781611971194

Motivation

Reflected Brownian motion on the orthant is the diffusion that arises as the heavy-traffic limit of open networks of queues. In a $K$-station network the scaled queue-length vector lives in the nonnegative orthant $\mathbb R^K_+$; in the interior it moves like a Brownian motion, and when a station empties the process is pushed back into the orthant in a direction determined by the routing of customers between stations. Harrison (1978) obtained such a limit for two queues in tandem, and Reiman (Open Queueing Networks in Heavy Traffic, Math. Oper. Res. 9 (1984)) showed that general $K$-station open networks lead exactly to the class of processes studied here.

Classical constructions of reflected diffusions (Stroock and Varadhan 1971, Watanabe 1971) require a smooth boundary and a reflection direction varying continuously on it. The orthant has corners and the reflection direction jumps between faces, so those results do not apply. Harrison and Reiman (Reflected Brownian Motion on an Orthant, Ann. Probab. 9 (1981)) construct the process pathwise, following Skorokhod's one-dimensional approach, and derive its Markov property from the construction. The process has since become the standard object in the diffusion approximation of queueing networks.

Setting

Fix a positive integer $K$. Vectors in $\mathbb R^K$ are row vectors, indexed by $j=1,\dots,K$. Let $A$ be a $K\times K$ covariance matrix (symmetric, nonnegative definite), $b\in\mathbb R^K$ a drift vector, and $Q=(q_{ij})$ a nonnegative $K\times K$ matrix with zeros on the diagonal and spectral radius strictly less than one. $S=\mathbb R^K_+$ is the nonnegative orthant.

Let $C$ be the space of continuous paths $x:[0,\infty)\to\mathbb R^K$ with the topology of uniform convergence on compact intervals, and $C_S$ the paths with $x(0)\in S$. For $x\in C_S$, the Skorokhod problem asks for $y,z\in C$ with, for every $j$,

$$z_j(t)=x_j(t)+y_j(t)-\sum_{i=1}^K q_{ij}\,y_i(t),\qquad z_j(t)\ge 0,\qquad t\ge0, \tag{5–6}$$

$y_j$ nondecreasing with $y_j(0)=0$ (7), and $y_j$ increasing only at times $t$ where $z_j(t)=0$ (8). In matrix form, $z=x+y(I-Q)$. Theorem 1 of the paper shows there is exactly one such pair, written $y=\psi(x)$, $z=\phi(x)$.

The process is obtained by feeding a Brownian path into this map. On a probability space $(\Omega,\mathcal F,P)$ let $X$ be a $K$-dimensional Brownian motion with covariance matrix $A$, drift $b$ and $X(0)\in S$ almost surely, with $X(0)$ independent of the increments of $X$. Let $\mathcal F_t=\mathcal F(X(s);0\le s\le t)$. Set $Y=\psi(X)$ and $Z=\phi(X)$ where $X\in C_S$, and $Y=Z=0$ on the exceptional null set. $Z$ is reflected Brownian motion on $S$ with reflection matrix $I-Q$.

Formalization targets

Goal: Corollary 1

There is a family $(\kappa_t)$ of Markov transition kernels on $\mathbb R^K$, depending only on $(Q,A,b)$, such that for every such $X$, $Y$, $Z$:

$$\text{(a)}\quad Y(t),\ Z(t)\ \text{are } \mathcal F_t\text{-measurable},\ t\ge0;$$ $$\text{(b)}\quad (Y,Z)\ \text{satisfies (1)–(4) a.s., and any pair satisfying (1)–(4) a.s. equals } (Y,Z) \text{ a.s.};$$ $$\text{(c)}\quad P\big[Z(s+t)\in B \mid \mathcal F_s\big]=\kappa_t\big(Z(s),B\big)\ \text{a.s.},\qquad s,t\ge0,\ B \text{ Borel}.$$

Here (1)–(4) are (5)–(8) for the paths of $X$, $Y$, $Z$. The kernel is chosen before the probability space and the initial law, which is what "stationary transition probabilities" means.

Milestones

The milestones follow the proof of Theorem 1 on pp. 304–305:

1. a positive diagonal $\Lambda$ with $\|\Lambda^{-1}Q\Lambda\|<1$ (Veinott scaling);
2. (5)–(8) are invariant under $(Q,x,y,z)\mapsto(\Lambda^{-1}Q\Lambda,x\Lambda,y\Lambda,z\Lambda)$;
3. the key observation that (5)–(8) are equivalent to $y\in C_0$, the fixed-point equation $y=\pi(y)$ with $\pi(y)(t)=\sup_{0\le s\le t}[y(s)Q-x(s)]^+$, and $z=x+y(I-Q)$;
4. the contraction $\|\pi(y)-\pi(y')\|\le\alpha\|y-y'\|$ on $[0,T]$;
5. convergence of the Picard iterates $y^{n+1}=\pi(y^n)$, $y^0\equiv0$;
6. the Lipschitz bound $\|\psi(x)-\psi(x')\|\le\|x-x'\|/(1-\alpha)$;
7. Theorem 1 itself: existence and uniqueness, non-anticipation (9), continuity (10);
8. the regeneration property (11): with $x^*(t)=z(T)+x(T+t)-x(T)$, $y^*(t)=y(T+t)-y(T)$, $z^*(t)=z(T+t)$, one has $y^*=\psi(x^*)$, $z^*=\phi(x^*)$.

Milestone 7 is the platform theorem Reiman84.QueueLength.lemma_1, posed as an open target by an earlier mission (Reiman 1984 cites it as its Lemma 1). It is referenced here and not posed again.

Significance

Corollary 1 is what makes $Z$ a usable stochastic process: adaptedness and almost-sure uniqueness say $Z$ is determined by the driving Brownian motion in a non-anticipating way, and the Markov property with time-homogeneous kernels is the starting point for the change-of-variable formula of §3, for generators, for stationary distributions, and for the heavy-traffic limit theorems in which $Z$ appears as the limit. The pathwise map $\phi$ and its Lipschitz continuity are reused throughout queueing theory: the continuous-mapping argument for heavy-traffic limits rests on exactly the continuity (10) established here.

The results are classical, with complete published proofs. None of them has a machine-checked proof. Mathlib has the measure-theoretic layer (kernels, conditional expectation, independence) but no reflection maps, no construction of multidimensional Brownian motion with drift, and no Markov-process theory in continuous time. This mission provides a formal statement of the pathwise reflection theory and its probabilistic consequence on which such a development can build.

Difficulty

The pathwise part is a contraction argument, but the contraction is not in the original norm: the map $y\mapsto yQ$ need not be a contraction for any standard norm when only the spectral radius of $Q$ is below one. The proof first changes coordinates by a positive diagonal matrix, and the right norm must be matched to the row-vector convention. The fixed-point characterization also has to be shown equivalent to the complementarity condition (8), which is where the zero diagonal of $Q$ enters.

For Corollary 1, the difficulty is measure-theoretic. Adaptedness requires measurability of a path functional with respect to the uncompleted natural filtration, which uses (9) and (10) and the fact that continuous paths are determined by countably many coordinates. The Markov property requires the regeneration identity (11) together with independence of the post-$s$ increments of $X$ from $\mathcal F_s$, and a kernel that is jointly measurable and independent of the initial law. Conditioning on $\mathcal F_s$ alone, without identifying the future as a fixed functional of $Z(s)$ and an independent Brownian motion, does not give a kernel that is the same for all $s$.

Formalization scope

• $\mathbb R^K$ is Fin K → ℝ (paper index $j$ = Lean index $j-1$), with $K\ge1$; row vector times matrix is Matrix.vecMul. Paths are functions ℝ → Fin K → ℝ; only times $t\ge0$ are constrained.
• Spectral radius $<1$ is rendered as $Q^m\to0$, the rendering of Reiman84.QueueLength.lemma_1. $A$ is PosSemidef.
• (5)–(8) are the published Reiman84.QueueLength.IsReflectionPair; (8) reads "$y_j$ is constant on every interval $[s,t]\subseteq[0,\infty)$ on which $z_j>0$". $C_S$ is IsCPlus; uniform convergence on compacts is UocTendsto; Brownian motion from $0$ with drift and covariance is IsDriftedBM.
• The norm on $C[0,T]$ is $\sup_{0\le t\le T}\|y(t)\|_\infty$. The suprema in $\pi$ and in the norm are real suprema, honest only for continuous paths, and every statement using them assumes continuity.
• The paper's $\|P\|$ is printed as the maximal row sum. Under the row-vector convention the contraction, Picard and Lipschitz steps need the maximal column sum; with the printed reading the contraction inequality is false (a nilpotent $3\times3$ counterexample is recorded in those items). Veinott scaling is stated as printed; applying it to $Q^\top$ gives the column version.
• The Brownian motion is $X=X_0+\xi$ with $\xi$ a drifted Brownian motion from $0$ and $X_0\ge0$ a.s. independent of the whole process $\xi$. $\mathcal F_t$ is the uncompleted σ-algebra generated by $X(s)$, $0\le s\le t$.
• $Y$ and $Z$ enter Corollary 1 as hypotheses: a solution of (5)–(8) on $\{X\in C_S\}$, zero elsewhere. That such processes exist is the existence part of Theorem 1, the referenced open item.
• The kernel family is quantified before the probability space, so it cannot depend on $s$, on $\Omega$ or on the law of $X(0)$. A version of (c) with a kernel depending on these, with the completed or full σ-algebra in place of $\mathcal F_s$, or with one-dimensional marginals only, is a different and weaker statement and is ruled out.

Out of scope: Theorem 2 (the change-of-variable formula, which needs stochastic integration), the necessity of spectral radius $<1$, and §§3–4. Useful contributions beyond the milestones include a construction of multidimensional Brownian motion with drift in Mathlib, the Skorokhod map as a function on $C_S$, and general lemmas on measurability of continuous path functionals.

Selected references

• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9(2), 302–308, 1981. https://doi.org/10.1214/aop/1176994471
• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3), 441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• A. F. Veinott, Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Annals of Mathematical Statistics 40(5), 1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• A. V. Skorokhod, Stochastic Equations for Diffusion Processes in a Bounded Region, Theory of Probability and Its Applications 6(3), 264–274, 1961. https://doi.org/10.1137/1106035
• D. W. Stroock and S. R. S. Varadhan, Diffusion Processes with Boundary Conditions, Communications on Pure and Applied Mathematics 24, 147–225, 1971. https://doi.org/10.1002/cpa.3160240206