All missions

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

The traveling salesman problem is NP-hard in general, so special cost structures under which it can be solved exactly in polynomial time are of lasting interest in combinatorial optimization and scheduling. One of the earliest and most cited such cases comes from sequencing on a machine whose condition is described by a single real number: a furnace temperature, a knife setting, a fill level. Each job must start at a prescribed state and leaves the machine in another, and changing the state between consecutive jobs costs money or time. Finding the cheapest cyclic order of the jobs is a traveling salesman problem with asymmetric costs.

P. C. Gilmore and R. E. Gomory solved this problem exactly in 1964 (Oper. Res. 12(5), 655–679) with an algorithm of $O(N^2)$ simple steps. Their construction became the standard example of a solvable TSP case: it is the starting point of the survey literature on polynomially solvable TSPs (Gilmore, Lawler and Shmoys 1985; Burkard, Deineko, van Dal, van der Veen and Woeginger 1998), and it appears in the no-wait flow shop literature, where two-machine no-wait scheduling reduces to exactly this cost structure.

Setting

There are $N$ jobs $J_1,\dots,J_N$. Job $i$ must be started when the state of the machine is $A_i$ and leaves the machine in state $B_i$; the jobs are numbered so that $j>i$ implies $B_j\ge B_i$. Two cost densities $f,g:\mathbb R\to\mathbb R$ satisfy $f(x)+g(x)\ge0$: raising the state through $x$ costs $f(x)$ per unit, lowering it costs $g(x)$ per unit. The changeover cost of having job $j$ follow job $i$ is

$$c_{ij}=\begin{cases}\int_{B_i}^{A_j}f(x)\,dx & \text{if } A_j\ge B_i,\\ \int_{A_j}^{B_i}g(x)\,dx & \text{if } B_i>A_j.\end{cases}$$

A permutation $\psi$ of the jobs assigns to each job $i$ its successor $\psi(i)$ and has cost $c(\psi)=\sum_i c_{i\psi(i)}$. It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if it is a single cycle through all jobs.

A permutation $\varphi$ ranks the $A$ if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$. The interchange $\alpha_{ij}$ swaps $i$ and $j$; applying it to $\psi$ gives $\psi\alpha_{ij}$ (first $\alpha_{ij}$, then $\psi$), which exchanges the successors of $i$ and $j$, at cost $c_\psi(\alpha_{ij})=c(\psi\alpha_{ij})-c(\psi)$. The graph $G_\varphi$ links $i$ and $\varphi(i)$ for every $i$; a spanning tree of $G_\varphi$ is a minimal set of additional arcs $R_{ij}$ that makes it connected, with cost $\sum c_\varphi(\alpha_{ij})$. Node $q$ is of type 1 if $B_q\le A_{\varphi(q)}$ and of type 2 otherwise.

Given a minimal cost spanning tree $\tau$ of $G_\varphi$ made of arcs $R_{q,q+1}$, the tour $\psi^*$ is obtained from $\varphi$ by executing the interchanges $\alpha_{q,q+1}$, $R_{q,q+1}\in\tau$, first those of type 1 in decreasing order of $q$, then those of type 2 in increasing order of $q$.

Formalization targets

Goal: Theorem 5

$$\psi^*\ \text{is a tour, and}\quad c(\psi^*)\le c(\psi)\ \text{ for every tour }\psi.$$

This is the paper's main theorem. It fixes no constant and no special form of $f,g$; it asserts that the specific tour produced by the algorithm is optimal among all tours.

Milestones

In the order the proof uses them:

1. Theorem 1: $c(\varphi)=\min_\psi c(\psi)$ over all permutations.
2. Eq. (11): under $B_j\ge B_i$, $A_{\psi(j)}\ge A_{\psi(i)}$, the cost of $\alpha_{ij}$ is $\int_{[B_i,B_j]\cap[A_{\psi(i)},A_{\psi(j)}]}(f+g)$.
3. Lemma 1: an interchange between two different cycles merges them.
4. Theorem 2: the interchanges of a spanning tree, in any order, turn $\psi$ into a tour.
5. Lemma 2: some minimal cost spanning tree of $G_\varphi$ uses only arcs $R_{i,i+1}$.
6. Lemma 5: adjacent interchanges executed on $\varphi$ in the stated order have additive cost.
7. Theorem 3: $\psi^*$ is a tour of cost $c(\varphi)+c_\varphi(\tau)$.
8. Theorem 4: $c(\psi)\ge c(\varphi)+c^*(\psi)$ for every permutation, with the underestimate $c^*$ of (17).
9. Lemma 7: for a tour $\psi$ the graph $G_\psi^*$ is connected.
10. Lemma 8: conditions (22a) and (22b) hold for equally many indices.
11. Eq. (28): $c^*(\psi)\ge c_\varphi(\tau)$ for every tour $\psi$.

Off the goal's path: Theorem 7, a minimal tour for $(f,g)$ is minimal for $(f+g,0)$.

Significance

The theorem shows that a traveling salesman problem whose costs come from a one-dimensional state is solved by three polynomial steps: sorting (an optimal assignment), a minimum spanning tree over $N-1$ candidate arcs, and a prescribed sequence of interchanges. It is the base case for a family of later results on solvable TSPs and for the two-machine no-wait flow shop, where it gives an exact polynomial algorithm.

The result has been proved since 1964. No machine-checked proof of it is known to exist. The proof in the paper argues largely from figures ("evident geometrically"), and its statement of Theorem 3 lists the interchanges in an order that contradicts its own proof: executed in the printed order, the paper's numerical example yields a tour of cost 39 instead of the optimum 34. A formal proof settles which order is correct and fills in the geometric steps. Partial contributions are useful: the permutation facts (Lemmas 1, 8 and Theorem 2) are independent of the cost model and reusable.

Difficulty

The obvious argument fails at two points. First, interchanges do not commute in cost: once one interchange is executed, the cost of the next one depends on the new successors, so the cost of $\psi^*$ is not simply $c(\varphi)$ plus the tree cost for an arbitrary execution order. Showing that the specific order of Lemma 5 avoids all interference requires tracking how type-1 and type-2 nodes behave as interchanges are applied. Second, optimality is not a local statement: an arbitrary tour is not reachable from $\varphi$ by tree interchanges, so the lower bound needs the separate underestimate $c^*$ and a counting argument relating every tour to a spanning tree of $G_\varphi$. Neither step follows from general minimum spanning tree theory.

Formalization scope

Jobs are Fin (n + 1) ($N=n+1\ge1$), so the paper's job $i$ is index $i-1$; the adjacent arc $R_{q,q+1}$ is indexed by q : Fin n and joins q.castSucc and q.succ. Permutations are Equiv.Perm (Fin (n + 1)), and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j (Mathlib's composition, "first $\alpha_{ij}$, then $\psi$"). Costs are real; (1) uses oriented interval integrals and (17) set integrals.

Explicit readings of the paper's loose phrases:

• "any integrable functions $f,g$" is read as local integrability on $\mathbb R$, with $f+g\ge0$ the only sign condition;
• "proper subsets $s$" in (4) are nonempty proper subsets;
• "a minimal set of additional arcs that connect" is minimal under inclusion; "minimal cost spanning tree" is minimal in cost among spanning trees made of adjacent arcs (by Lemma 2 the same minimum as over all trees);
• "minimal cost tour" means cost at most that of every tour, i.e. every permutation that is a single cycle;
• "obtained by executing the $\alpha$'s in a particular order" (Lemma 5) is the explicit order of its proof;
• ties among the $A$ leave $\varphi$ non-unique; every statement holds for every ranking $\varphi$.

The order of $\psi^*$ is that of the proof of Lemma 5 and of steps T2–T4 (p. 673), not the order printed in Theorem 3.

Trivializing formalizations are ruled out: the goal quantifies over all tours, not over permutations (that is Theorem 1) nor over tours reachable from $\varphi$; $\psi^*$ is constructed from $\varphi$ and $\tau$, not taken as an arbitrary tour of the right cost; $\tau$ is both inclusion-minimal and cost-minimal; and the costs keep both branches of (1) with general densities, not $c_{ij}=|A_j-B_i|$. The TSP items already on the platform concern symmetric or metric distances with tours as visiting orders, a different model, and are not reused.

Needed infrastructure: cycle structure of permutations under transpositions (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, interval integrals of locally integrable functions. Contributions to any milestone are welcome; the purely combinatorial ones (Lemmas 1, 8, Theorem 2, Lemma 7) are independent of the integrals.

Selected references

• P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5), 1964, 655–679. https://doi.org/10.1287/opre.12.5.655
• P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in The Traveling Salesman Problem (Lawler, Lenstra, Rinnooy Kan, Shmoys, eds.), Wiley, 1985, 87–143. ISBN 978-0-471-90413-7
• R. E. Burkard, V. G. Deineko, R. van Dal, J. A. A. van der Veen and G. J. Woeginger, Well-solvable special cases of the traveling salesman problem: a survey, SIAM Review 40(3), 1998, 496–546. https://doi.org/10.1137/S0036144596297514
• J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proc. AMS 7(1), 1956, 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7

Motivation

Freedman's inequality bounds the probability that a martingale with increments bounded above by $1$ reaches a level $a$ before its accumulated conditional variance exceeds $b$: the bound is $\exp[-a^2/2(a+b)]$ (D. A. Freedman, On Tail Probabilities for Martingales, Ann. Probab. 3 (1975) 100–118, Theorem (4.1), doi:10.1214/aop/1176996452). It is the standard tool for concentration of martingales whose variance is random, and it is used throughout online learning, bandit theory and the analysis of randomized algorithms.

The same paper shows that the exponent $a^2/2b$ cannot be improved in general. For a martingale with increments bounded by $1$ in absolute value, Freedman's estimate (1.10) bounds from below the probability that level $a$ is crossed while the conditional variance used is still below $b$. The analytic core of that lower bound is isolated in the paper as Proposition (4.10), p. 109: a statement about a single nonnegative random variable whose Laplace transform is controlled from both sides. The paper calls its proof "disappointingly hard". This mission formalizes Proposition (4.10) and the steps of its proof.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. For real $\lambda$ put (Definition (1.2), p. 101)

$$e(\lambda)=e^{\lambda}-1-\lambda,\qquad f(\lambda)=e^{-\lambda}-1+\lambda .$$

Both are nonnegative and equal $\lambda^2/2+O(\lambda^3)$ near $0$. Fix $a>0$ and a nonnegative random variable $W$. The two Laplace-transform bounds are, for every $\lambda\ge0$,

$$\text{(4.11a)}\quad E\{\exp[-e(\lambda)W]\}\le\exp(-\lambda a),\qquad \text{(4.11b)}\quad E\{\exp[-f(\lambda)W]\}\ge\exp(-\lambda(a+1)).$$

In the paper $W=W_a$ is the conditional variance $\sum_{i\le\tau_a}\operatorname{Var}\{X_i\mid\mathcal F_{i-1}\}$ accumulated up to the first time $\tau_a$ the martingale reaches $a$; for that variable (4.11a) and (4.11b) are Theorems (1.12) and (1.8). Here $W$ is abstract. The hypotheses are consistent: the first-passage time of standard Brownian motion to level $a$ has $E e^{-sW}=e^{-a\sqrt{2s}}$, and since $f(\lambda)\le\lambda^2/2\le e(\lambda)$ for $\lambda\ge0$, it satisfies both bounds.

The parameter conditions (4.12) on positive reals $\delta,a,b$ are

$$\delta<\tfrac13,\qquad \frac ba>\frac{9}{\delta^2},\qquad \frac{a^2}{b}>\frac{16}{\delta^2}\log\frac{64}{\delta^2}.$$

The proof uses the notation (4.14): $\varphi(\lambda)=\lambda^2/2-\lambda^3/6$, $\lambda=(1+\delta)a/b$, $k=a^2/b$, $N=2/\delta^2$, the five intervals $I_1=[0,Na]$, $I_2=(Na,(1-2\delta)b]$, $I_3=(b,2b]$, $I_4=(2b,\infty)$, $I_5=((1-2\delta)b,b]$, and the terms

$$\eta_i=\varphi(\lambda)\int_{I_i}P\{W<x\}\,e^{-\varphi(\lambda)x}\,dx .$$

In Lean these objects are FreedmanTail.LowerTail.e, f, LaplaceUpper, LaplaceLower, ParamConditions, phi, lamStar, kStar, NStar, I1–I5 and eta.

Formalization targets

Goal: Proposition (4.10)

Under (4.11a)–(4.11b) for all $\lambda\ge0$ and (4.12a)–(4.12c),

$$P\{W<b\}>\tfrac12\exp\!\left[-\left(\tfrac12+2\delta\right)\frac{a^2}{b}\right].\qquad(4.13)$$

Milestones

In the order of the proof:

1. Lemma (4.9): $\alpha>0$, $x>2\log\alpha$ imply $e^x>\alpha x$.
2. (4.17): $\exp(-\delta^2k/8)<1/(8k)$ under (4.12).
3. (4.18): under (4.11a), $P\{W<x\}<\exp[-a^2/(2(a+x))]$ for $x\ge0$.
4. (4.15): under (4.11b) and (4.12), $\varphi(\lambda)\int_0^\infty P\{W<x\}e^{-\varphi(\lambda)x}\,dx>\exp[-\lambda(a+1)]$.
5. (4.19), with its exponent corrected: $P\{W<x\}<(\tfrac18-\tfrac1{50})\exp[-(1+\delta)k]$ for $0\le x\le Na$.
6. (4.16:1)–(4.16:4): $\eta_1<(\tfrac18-\tfrac1{50})e^{-(1+\delta)k}$ and $\eta_i<\tfrac18e^{-(1+\delta)k}$ for $i=2,3,4$.
7. (4.16:5): $\eta_5<P\{W<b\}\cdot\exp[(-\tfrac12+2\delta^2)k]$.

Significance

The result. Proposition (4.10) converts two-sided control of a Laplace transform into a lower bound for a left tail, with an explicit constant and an explicit range of validity. Applied to the crossing variance $W_a$ it gives Freedman's lower bound (1.10) for $P\{W_a<b\}$, which matches the exponent $a^2/(2b)$ of the upper bound of Theorem (4.1) up to the term $2\delta a^2/b$. That is the statement that Freedman's inequality is sharp in the regime $a^2/b\to\infty$, $b/a\to\infty$.

Formalizing it. The proposition is proved in the 1975 paper; no machine-checked proof is known. Mathlib contains Chernoff-type upper bounds and the layer-cake formula, but no lower tail bound derived from two-sided Laplace-transform control. The mission produces a self-contained, constant-explicit Tauberian-type lemma for nonnegative random variables, usable without any martingale structure. The companion missions of this series formalize Theorem (4.1) and the Laplace bound (1.8); together they would give the sharpness statement for martingales.

Difficulty

The obvious route is to invert the Laplace-transform bounds directly. A lower bound on $E\{e^{-sW}\}$ does not by itself bound $P\{W<b\}$ from below: the mass that makes the Laplace transform large could sit at small values of $W$ or be spread over a wide range. Without (4.11a) the conclusion fails, and with it every contribution from values of $W$ away from $b$ must be shown negligible at a precision of order $e^{-(1+\delta)k}$, where $k=a^2/b$ is large. The main term is smaller than the total by the factor $e^{-k/2}$, so every error term must be estimated with constants explicit enough to stay below it. The thresholds (4.12b)–(4.12c) are what make all of these comparisons hold at once.

Formalization scope

The probability space is a measurable space Ω with a measure P and [IsProbabilityMeasure P]. $W$ is a measurable function Ω → ℝ with W ω ≥ 0 for every ω. The expectations in (4.11) are Bochner integrals of $\exp[-e(\lambda)W]$ and $\exp[-f(\lambda)W]$; for $\lambda\ge0$ these integrands lie in $(0,1]$, so they are integrable and the integrals are genuine expectations. Probabilities are P.real {ω | W ω < x}, with the strict event as on the page. The integrals in $x$ are Lebesgue integrals over $[0,\infty)$ and over the intervals $I_i$; the integrand is a nondecreasing function of $x$ times $e^{-\varphi(\lambda)x}$, hence measurable and, as $\varphi(\lambda)>0$, integrable.

Conventions and corrections, each also disclosed in the items:

• The page says "for each $a>0$, let $W_a$ be a nonnegative random variable"; only the one variable at the one level $a$ of (4.12) enters, so the statement is made for a fixed $a$ and a single $W$.
• (4.14) prints $\varphi(\lambda)=\lambda^2/2>\lambda^3/6$; this is read as $\varphi(\lambda)=\lambda^2/2-\lambda^3/6$, as the rest of the proof requires.
• (4.19) prints $\theta=(\tfrac18-\tfrac1{50})\exp[-(1+\delta)]$; the milestone states $\theta=(\tfrac18-\tfrac1{50})\exp[-(1+\delta)k]$, which is what the page's argument proves and what (4.16:1) needs.
• (4.18) is stated for every $x\ge0$, the range on which it is used.
• The proof of (4.16:5) ends "This settles (3.16:5)", a misprint for (4.16:5).

A trivializing formalization is ruled out: the hypotheses are satisfied by the Brownian first-passage time above, the parameter conditions hold for instance at $\delta=0.3$, $a=10^6$, $b=2\cdot10^8$, and no integral in a hypothesis or conclusion can take a default value $0$.

Needed infrastructure: Markov's inequality and the layer-cake formula (both in Mathlib), the identity $E\{e^{-sW}\}=s\int_0^\infty P\{W<x\}e^{-sx}\,dx$ for $W\ge0$, and elementary estimates of $e^x$ and of the convex function $\theta(x)=\tfrac{\lambda^2}2x+\tfrac{N}{N+1}\tfrac{a^2}{2x}$ of (4.21). The layer-cake identity and the left-tail bound (4.18) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the unnumbered steps (4.20)–(4.30).

The source is the published article in The Annals of Probability (a scanned copy); page numbers are the journal's.

Selected references

• D. A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1) (1975) 100–118. doi:10.1214/aop/1176996452

Motivation

Many problems in mechanics and optimal control are posed as the minimization of a convex functional of the form $f(Av)-\langle b,v\rangle$, where $A$ is a differential operator and $f$ is non-smooth: an obstacle, a friction term, a plasticity threshold. Splitting the variable, $y=Av$, separates the linear operator from the non-smooth function, and a Lagrange multiplier for the constraint $Av-y=0$ turns the problem into a sequence of two simpler ones: a linear system in $v$ and a pointwise nonlinear problem in $y$. The scheme that alternates between the two and then updates the multiplier is now called the alternating direction method of multipliers (ADMM). It is one of the standard algorithms of large-scale convex optimization, statistics and imaging (Boyd, Parikh, Chu, Peleato and Eckstein, 2011).

Gabay and Mercier (IRIA report RR-126, 1975; Comput. Math. Appl., 1976) gave a convergence proof of this method in Hilbert space, for a stepsize $\rho$ anywhere in $(0,2r)$, where $r$ is the penalty parameter of the augmented Lagrangian.

Timeline.

• 1969: Hestenes and Powell introduce the augmented Lagrangian (method of multipliers).
• 1975: Glowinski and Marrocco propose the alternating scheme for nonlinear Dirichlet problems.
• 1975–76: Gabay and Mercier prove strong convergence of the primal iterates for $0<\rho<2r$ under strong monotonicity of $f_1'$ (this mission).
• 1983: Gabay identifies ADMM with Douglas–Rachford splitting applied to the dual.
• 1992: Eckstein and Bertsekas extend convergence to maximal monotone operators, without strong monotonicity, for $\rho=r$.

Setting

$V$ and $Y$ are real Hilbert spaces; $(\cdot,\cdot)$ and $|\cdot|$ are the inner product and norm of $Y$, $\|\cdot\|$ the norm of $V$. $A:V\to Y$ is a continuous linear operator and $b$ is a continuous linear functional on $V$, with value $\langle b,v\rangle$ at $v$. The dual of $Y$ is identified with $Y$. The function $f:Y\to(-\infty,+\infty]$ is a sum $f=f_1+f_2$ where

1. $f_1:Y\to\mathbb R$ is convex and continuously differentiable, and its gradient is strongly monotone: $(f_1'(y)-f_1'(z),y-z)\ge\gamma|y-z|^2$ for some $\gamma>0$ (2.3);
2. $f_2$ is proper (never $-\infty$, somewhere finite), convex and lower semicontinuous;
3. $|Av|^2\ge\alpha^2\|v\|^2$ for some $\alpha>0$ (2.5);
4. some $Av_0$ lies in the interior of $\operatorname{dom}f_2=\{y:f_2(y)<+\infty\}$ (qualification).

The problem is

$$(\mathcal P)\qquad \inf_{v\in V}\ f(Av)-\langle b,v\rangle ,$$

and a solution $v^*$ is a point where this value is finite and minimal. The Lagrangian and augmented Lagrangian are, for $\lambda\in Y$ and $r>0$,

$$\mathcal L(v,y;\lambda)=f(y)+(\lambda,Av-y)-\langle b,v\rangle,\qquad \mathcal L_r=\mathcal L+\frac r2|Av-y|^2 .$$

The modified dual algorithm (3.4) starts from any $(y^0,\lambda^0)\in Y\times Y$ and, for $n\ge0$,

1. finds $v^{n+1}$ with $r(Av^{n+1},Aw)=(ry^n-\lambda^n,Aw)+\langle b,w\rangle$ for all $w\in V$ (minimization of $\mathcal L_r$ in $v$);
2. finds $y^{n+1}$ with $\lambda^n+rAv^{n+1}-ry^{n+1}-f_1'(y^{n+1})\in\partial f_2(y^{n+1})$ (minimization of $\mathcal L_r$ in $y$);
3. sets $\lambda^{n+1}=\lambda^n+\rho(Av^{n+1}-y^{n+1})$.

$P$ denotes the orthogonal projection of $Y$ onto the range $R(A)$, which is closed by (2.5).

Formalization targets

Goal: Theorem 3.1

For $r>0$ and every stepsize with

$$0<\rho<2r,$$

every run of the algorithm satisfies

$$\|v^n-v^*\|\to0,\qquad |y^n-Av^*|\to0,\qquad \sup_n|\lambda^n|<\infty,$$

where $v^*$ is the unique solution of $(\mathcal P)$. The multipliers need not converge.

Milestones

1. Proposition 2.1: $(\mathcal P)$ has a unique solution.
2. Theorem 2.1: a saddle point $(v^*,y^*;\lambda^*)$ of $\mathcal L$ consists of the solution $v^*$, $y^*=Av^*$ and $\lambda^*\in\partial f(Av^*)$ with $A'\lambda^*=b$; and a saddle point exists.
3. Theorem 2.2: for $r>0$, $\mathcal L_r$ and $\mathcal L$ have the same saddle points.
4. (3.8)–(3.10): a saddle point is a fixed point of Steps 1–2.
5. (3.11)–(3.12): $A(v^{n+1}-v^*)=P(y^n-y^*)-\frac1rP(\lambda^n-\lambda^*)$.
6. (3.19)–(3.20): the energy estimate

$$\gamma|y^{n+1}-y^*|^2+\Bigl(r-\frac\rho2\Bigr)|(I-P)(y^{n+1}-y^*)|^2+\frac r2|P(y^{n+1}-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^{n+1}-\lambda^*)|^2\le\frac r2|P(y^n-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^n-\lambda^*)|^2$$

and its sum over $n=0,\dots,N$. 7. $y^n\to y^*$ for $0<\rho\le2r$. 8. (3.22)–(3.23): a contraction-plus-summable-forcing recursion for $|P(\lambda^n-\lambda^*)|^2$, and the scalar lemma that such recursions tend to $0$. 9. $P(\lambda^n-\lambda^*)\to0$ and $v^n\to v^*$ for $0<\rho<2r$.

Significance

The theorem says that ADMM converges without any step-size tuning beyond $\rho<2r$, and that the primal iterates converge in norm in infinite dimension, which is what makes the method usable for finite element discretizations of variational problems (the companion mission on internal approximations treats the discretization). It covers obstacle problems, Bingham fluids and elasto-plastic torsion, where $f_2$ is an indicator or a non-differentiable norm.

The result is proved in the 1975 report. To our knowledge it has no machine-checked proof. Formalizing it adds a library-level convergence theorem for ADMM in Hilbert space with $\mathrm{EReal}$-valued convex functions, a saddle-point existence theorem for linearly constrained convex problems, and the energy estimate (3.19) as a reusable lemma. The formalization also fixes two defects of the printed text (see Formalization scope): a sign in Step 1 and a qualification hypothesis that is too weak.

Difficulty

The energy estimate (3.19) only controls the multiplier through its component in $R(A)^\perp$, and only the $y$-error through $\gamma>0$. The natural first idea, a Lyapunov function in $|\lambda^n-\lambda^*|^2$ alone that decreases at each step, does not work for $\rho\ne r$: the component $P(\lambda^n-\lambda^*)$ obeys a separate recursion whose contraction factor $|1-\rho/r|$ is below one only for $0<\rho<2r$, and whose forcing term must be shown summable from the $y$-estimate. The existence of a multiplier, i.e. of a saddle point, is a separate difficulty: it needs the subdifferential chain rule $\partial(f\circ A)=A'\partial f(A\,\cdot)$ in infinite dimension, under a constraint qualification.

Formalization scope

Lean conventions:

• $V$, $Y$ are InnerProductSpace ℝ with CompleteSpace; multipliers are elements of $Y$; $b$ is a StrongDual ℝ V.
• $f_1:Y\to\mathbb R$ (a Gateaux-differentiable function is finite), with a gradient f₁' at every point (HasGradientAt) that is continuous; "weakly continuous on finite-dimensional subspaces" is then automatic.
• $f_2:Y\to$ EReal, with IsProperFn, IsConvexFn, IsSubgradient from the published InertialFB.IFB.ConvexAnalysis and Mathlib's LowerSemicontinuous. No subtraction in EReal occurs: the variational inequalities (3.6), (3.9) are stated as subgradient inclusions, and the Lagrangians as a real part plus $f_2(y)$.
• A solution of $(\mathcal P)$ has finite value. A run is any triple of sequences indexed by $\mathbb N$ satisfying Steps 1–3 for every $n$; the start is arbitrary, and the well-posedness of the steps is not assumed or used.
• $P$ is the orthogonal projection onto the closure of $R(A)$, equal to $R(A)$ under (2.5).
• Strong convergence is convergence in norm; "bounded" is Bornology.IsBounded (Set.range λ).

Corrections to the printed text, each explained in the item's statement:

• Step 1 (3.5) and (3.8) carry $+\langle b,v\rangle$. The paper prints $-\langle b,v\rangle$ there and in Remark 1 of p. 15, which is inconsistent with $\mathcal L$ and $(\mathcal P)$: with the printed sign the iteration solves the problem with $-b$.
• The qualification (2.4), "$\operatorname{int}\operatorname{dom}f_2\ne\emptyset$", is strengthened to $\operatorname{int}\operatorname{dom}f_2\cap R(A)\ne\emptyset$. With (2.4) alone, Theorem 2.1's saddle point need not exist and the multipliers of Theorem 3.1 need not be bounded: $V=\mathbb R$, $Y=\mathbb R^2$, $Av=(v,0)$, $f_1=|\cdot|^2/2$, $f_2$ the indicator of the disc of centre $(0,1)$ and radius $1$, $\langle b,v\rangle=v$.
• Proposition 2.1 assumes that $f_2\circ A$ is somewhere finite, which its proof requires.

Ruled out: the solution $v^*$ is a hypothesis of the goal, so the hypotheses must not be contradictory. They are met by $V=Y=\mathbb R$, $A=\mathrm{id}$, $f_1(y)=y^2/2$, $f_2=0$, $b=0$, and a proper $f_2$ excludes the degenerate reading in which every point "solves" $(\mathcal P)$ with value $+\infty$.

A complete development needs: existence of minimizers of coercive convex l.s.c. functions on a Hilbert space; the subdifferential sum and chain rules under a continuity qualification; orthogonal projections onto closed ranges; and elementary facts about summable sequences. The saddle-point theory (Theorems 2.1–2.2) and the scalar lemma (3.23) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal by a different route.

Selected references

• D. Gabay and B. Mercier, A dual algorithm for the solution of non linear variational problems via finite element approximation, IRIA Rapport de Recherche 126, 1975. https://hal.science/hal-04716124v1 ; journal version: Computers & Mathematics with Applications 2 (1976) 17–40, https://doi.org/10.1016/0898-1221(76)90003-1
• R. Glowinski and A. Marrocco, Sur l'approximation, par éléments finis d'ordre un, et la résolution, par pénalisation-dualité, d'une classe de problèmes de Dirichlet non linéaires, RAIRO Analyse Numérique 9 (1975) 41–76. https://doi.org/10.1051/m2an/197509R200411
• M. R. Hestenes, Multiplier and gradient methods, J. Optim. Theory Appl. 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• I. Ekeland and R. Temam, Analyse convexe et problèmes variationnels, Dunod, 1974 (the paper's [E]).
• J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Math. Programming 55 (1992) 293–318. https://doi.org/10.1007/BF01581204
• S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3 (2011) 1–122. https://doi.org/10.1561/2200000016

Motivation

For sums of independent bounded random variables, the inequalities of Bernstein and Bennett bound the probability of a large deviation by an exponential in the deviation and the variance (Bennett 1962; Hoeffding 1963). Many processes met in probability, statistics and learning theory are not sums of independent terms but martingales or supermartingales: sequential estimators, stochastic approximation iterates, the regret of an online algorithm. For them the relevant scale is not a fixed variance but the conditional variance accumulated along the path, which is itself random.

David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) extended the Bernstein–Bennett inequality to this dependent case, with the conditional variance in place of the variance and with a bound that holds simultaneously for all times. The result, now called Freedman's inequality, is the standard tool for martingale concentration with variance-sensitive rates and is used throughout bandit and reinforcement-learning analyses, random-graph arguments and stochastic optimization. This mission formalizes that theorem, (4.1) of the paper, together with the chain of lemmas the paper uses to prove it.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal F_0\subset\mathcal F_1\subset\mathcal F_2\subset\cdots$ an increasing sequence of sub-$\sigma$-fields of $\mathcal F$ (a filtration). Let $X_1,X_2,\dots$ be real random variables with $X_n$ measurable with respect to $\mathcal F_n$. Define

• the partial sums $S_n=X_1+\cdots+X_n$, with $S_0=0$;
• the conditional variances $V_n=\operatorname{Var}\{X_n\mid\mathcal F_{n-1}\}$;
• the intrinsic time $T_n=V_1+\cdots+V_n$, with $T_0=0$.

Freedman treats $T_n$ as an intrinsic clock: read at time $T_n$ rather than $n$, the process $S_n$ resembles Brownian motion. The paper's condition (3.4) is

$$X_n\le1\ \text{a.e.}\qquad\text{and}\qquad E\{X_n\mid\mathcal F_{n-1}\}\le0\ \text{a.e.}\qquad\text{for all }n\ge1,$$

so $(S_n)$ is a supermartingale whose increments are bounded above by $1$; no lower bound is assumed. The auxiliary functions are $e(\lambda)=e^\lambda-1-\lambda$ and $Q_\lambda(v,y)=\exp\{\lambda y-e(\lambda)v\}$, with time first and position second. A stopping time $\sigma$ takes values in $\{0,1,2,\dots,\infty\}$ with $\{\sigma\le n\}\in\mathcal F_n$, and $P\{\sigma=\infty\}>0$ is allowed.

In Lean these are FreedmanTail.Bernstein.S, V, T (on Filtration ℕ m, with V given by Mathlib's condVar) and FreedmanTail.Bernstein.e, Q.

Formalization targets

Goal: (4.1) Theorem

Under (3.4), for all $a>0$ and $b>0$,

$$P\{S_n\ge a\ \text{and}\ T_n\le b\ \text{for some } n=1,2,\dots\}\le\Bigl(\frac{b}{a+b}\Bigr)^{a+b}e^{a}\le\exp\Bigl[-\frac{a^{2}}{2(a+b)}\Bigr].$$

The first bound is of Bennett type, the second of Bernstein type. The event is a union over all times; the bound does not depend on any horizon.

Milestones

In the order the paper's proof uses them:

1. (3.1) Lemma: $g(0)=\tfrac12$, $g(x)=(e^x-1-x)/x^2$ for $x\ne0$, is increasing.
2. (3.2) Corollary: $\exp(\lambda x)\le1+\lambda x+x^2e(\lambda)$ for $\lambda\ge0$, $x\le1$.
3. (3.5): $E\{\exp(\lambda X)\}\le1+e(\lambda)\operatorname{Var}X\le\exp[e(\lambda)\operatorname{Var}X]$ for $\lambda\ge0$, $X\le1$, $E(X)\le0$.
4. Proof of (3.3): $\{Q_\lambda(T_n,S_n),\mathcal F_n\}$ is a supermartingale for $\lambda\ge0$.
5. (3.3) Proposition: $\int_{\{\sigma<\infty\}}Q_\lambda(T_\sigma,S_\sigma)\,dP\le1$ for every stopping time $\sigma$ and $\lambda\ge0$.
6. Proof of (4.1): $P\{A\}\le\exp[-\lambda a+e(\lambda)b]$ for every $\lambda\ge0$, where $A$ is the event of the goal.
7. Proof of (4.1): $\lambda_0=\log[(a+b)/b]$ minimizes this bound, with value $(b/(a+b))^{a+b}e^a$.
8. Proof of (4.1): $(b/(a+b))^{a+b}e^a\le\exp[-a^2/(2(a+b))]$.

Significance

The inequality bounds the probability that a supermartingale ever reaches level $a$ before its accumulated conditional variance exceeds $b$. Since it holds for all times at once, fixed-horizon versions follow immediately, as do versions with stopping times, and with a peeling argument over $b$ it gives the variance-adaptive confidence sequences used in sequential testing and in the analysis of algorithms. Freedman's paper uses it to derive the law of the iterated logarithm for martingales; later work uses it wherever a martingale's conditional variance is much smaller than the square of its increment bound.

The theorem has been proved for fifty years. What this mission adds is a machine-checked statement and proof of the full infinite-horizon form under the one-sided hypothesis (3.4), together with the exponential supermartingale and the optional-stopping bound (3.3) as reusable lemmas. Prove2Me already has fixed-horizon Bernstein-form consequences for martingale differences; the infinite-horizon Bennett form under (3.4) does not appear in Mathlib or on the platform.

Difficulty

The naive route of applying Markov's inequality to $\exp(\lambda S_n)$ at a fixed $n$ gives a bound for one time only and requires a deterministic bound on $T_n$. Taking a union over all $n$ loses everything. The content of the theorem is that the random clock $T_n$ and the supremum over time can both be absorbed, which requires an exponential process compensated by the random $T_n$ and an optional-stopping bound for stopping times that may be infinite with positive probability. The process need not be uniformly integrable, and the increments have no lower bound. A second, smaller, difficulty is the variance form of (3.5): the bound uses $\operatorname{Var}X$ rather than $E(X^2)$, which is strictly sharper when $E(X)<0$ and is needed to compensate with conditional variances.

Formalization scope

Lean conventions this mission commits to:

• Increments are a sequence X : ℕ → Ω → ℝ used from index $1$ (X 0 is never read), so $S_n$, $T_n$ and $V_n$ carry the paper's indices. The filtration is Mathlib's Filtration ℕ m, and "$X_n$ is $\mathcal F_n$-measurable" is StronglyMeasurable[ℱ n] (X n) for $n\ge1$.
• $V_n$ is Mathlib's condVar (ℱ (n - 1)) (X n) P. Mathlib sets a conditional expectation of a non-integrable function to $0$, so every increment is assumed square integrable (MemLp (X n) 2 P). This is the one hypothesis added to the page. Under (3.4) the page also allows increments of infinite variance, for which its $T_n$ is $+\infty$; the formalization narrows the class of processes and leaves every conclusion as printed. Milestone (3.5) likewise assumes $E(X^2)<\infty$, which is the case the page reduces to.
• "Expectation-decreasing martingale" is Mathlib's Supermartingale.
• Stopping times are Ω → WithTop ℕ with IsStoppingTime; $\top$ is $\infty$. In (3.3) the integral over $\{\sigma<\infty\}$ is a lower Lebesgue integral in $[0,\infty]$, so the bound does not presuppose integrability, and $S_\sigma$, $T_\sigma$ are read only on $\{\sigma\ne\infty\}$.
• The probability of the event "for some $n$" is the measure of $\{\omega:\exists n\ge1,\ S_n(\omega)\ge a,\ T_n(\omega)\le b\}$. $(b/(a+b))^{a+b}$ is a real power.
• (3.1) is stated as strict monotonicity, which its proof ($g'(x)>0$ for $x\ne0$) establishes.

A fixed-horizon statement ($n=N$, or $n\le N$), a martingale hypothesis $E\{X_n\mid\mathcal F_{n-1}\}=0$, or a two-sided bound $|X_n|\le1$ would each be a strictly weaker theorem than (4.1) and is not an acceptable formalization of the goal.

The development needs exponential supermartingales compensated by conditional variance, optional stopping for stopping times that may be infinite, and elementary real analysis of $e^x$. The real-analysis milestones (3.1), (3.2) and the two calculus steps are independent and reusable; (3.5) is a self-contained moment-generating-function bound; the supermartingale and (3.3) are reusable for every exponential-supermartingale argument. Contributions to any milestone, and alternative proofs of the goal, are welcome.

Selected references

• David A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1) (1975), 100–118. https://doi.org/10.1214/aop/1176996452 (source of this mission; a scanned copy of the published article, cited by printed page)
• George Bennett, Probability Inequalities for the Sum of Independent Random Variables, Journal of the American Statistical Association 57 (1962), 33–45. https://doi.org/10.1080/01621459.1962.10482149
• Wassily Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963), 13–30. https://doi.org/10.1080/01621459.1963.10500830

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