Combinatorics

Motivation

The chromatic number of the random graph $G(n,p)$ is one of the central random variables of probabilistic combinatorics. Its order of magnitude for constant $p$, $\chi(G(n,p)) \sim n/(2\log_{1/(1-p)} n)$, was settled by Bollobás ([B], 1988); the question that remains is how much $\chi$ fluctuates around its typical value. Shamir and Spencer ([S-S], 1987) used the edge- and vertex-exposure martingales to show that $\chi(G(n,p))$ lies, with high probability, in an interval of length about $\sqrt n$, and for sparse graphs $p = n^{-\alpha}$ in an interval of bounded length.

Chapter 9 of Talagrand's 1995 memoir revisits this question as an application of his convex-hull inequality (Theorem 4.1.1 of the paper, posed in a separate mission of this series). The author states the aim plainly: martingale methods require ingenuity on this problem, and the chapter shows that Theorem 4.1.1 gives somewhat better results "in a completely straightforward manner". The chapter also derives, from the same inequality, an upper bound on the probability that $G(n,p)$ has no independent set of a given size — the quantity that drives the greedy colouring bound, previously obtained by Bollobás with martingales and by Janson's correlation inequality.

Timeline. 1987: Shamir–Spencer, concentration of $\chi(G(n,p))$ by martingales. 1988: Bollobás, the asymptotic value of $\chi(G(n,p))$ for constant $p$, via a martingale bound on independent sets. 1990: Janson's inequality gives a simpler route to the same independent-set bound. 1995: Talagrand, Theorem 9.1 and Proposition 9.2, both from the convex-hull inequality.

Setting

A graph $G$ on the vertex set $V = \{1,\dots,n\}$ is a subset of $E_0 = \{(i,j);\ i<j\}$. A set $I \subseteq V$ is independent if no two of its points are joined by an edge. For $A \subseteq V$, the chromatic number $\chi(G,A)$ is the smallest number of independent sets that cover $A$, that is, the chromatic number of the subgraph induced on $A$; $\chi(G,\emptyset) = 0$. For an integer $m$,

$$\chi(G,m) = \inf\{\chi(G,A);\ \operatorname{card} A = m\}.$$

Given $0<p<1$, the random graph $G(n,p)$ contains each possible edge $(i,j)$ with probability $p$, independently. Concretely, $x = (x_e)_{e \in E_0} \in \{0,1\}^{E_0}$ carries the product of Bernoulli$(p)$ laws and $G(x)$ is the set of $e$ with $x_e = 1$.

The vertex-exposure space is $\Omega' = \prod_{j} \Omega_j$ with $\Omega_j = \{0,1\}^{j-1}$: the coordinate $\omega_j = (\omega_{i,j})_{i<j}$ lists the edges from $j$ to earlier vertices, and $G(\omega)$ contains $(i,j)$ iff $\omega_{i,j}=1$. Changing one coordinate of $\omega$ changes only edges at one vertex.

For an integer $r$ and $e = (i,j) \in E_0$, $N(G,e)$ denotes the number of independent sets of $G$ of size $r$ containing $i$ and $j$.

Formalization targets

Goal: Theorem 9.1

For $k \in \mathbb N$, $m \le n$ and $t>0$ there is an integer $a$ such that

$$P\big(\chi(G(n,p),m) \in [a-k,a]\big) \ \ge\ 1 - 2e^{-t^2/8} - P\big(\sup\{\chi(G(n,p),F);\ F\subset V,\ \operatorname{card}F \le t\sqrt m\} > k\big).$$

The integer $a$ depends on $n,p,m,k,t$. The last term is zero when $k > t\sqrt m$, so for such $k$ the chromatic number $\chi(G(n,p),m)$ sits in a window of $k+1$ values except on an event of probability $2e^{-t^2/8}$.

The deterministic step of the proof, Eq. (9.3)

With $A \subseteq \Omega'$ the set of $\omega$ with $\chi(G(\omega),m) \ge a$ and $\sup\{\chi(G(\omega),F);\ \operatorname{card}F \le t\sqrt m\} \le k$, and

$$B = \Big\{\omega;\ \forall (\alpha_j) \ge 0,\ \exists \omega' \in A;\ \sum_j \alpha_j 1_{\{\omega_j \ne \omega'_j\}} \le t\sqrt{\textstyle\sum_j \alpha_j^2}\Big\},$$

every $\omega \in B$ satisfies $\chi(G(\omega),m) \ge a-k$.

Proposition 9.2 and Eq. (9.7)

The double count $N = \big(r(r-1)/2\big)^{-1}\sum_{e\in E_0} N(G,e)$ of independent $r$-sets, and, for $u \ge 0$ and $r \ge 2$, if with probability greater than $1/2$ the graph $G(n,p)$ has an independent $r$-set and $u\sqrt{\sum_e N(G(n,p),e)^2} \le \sum_e N(G(n,p),e)$, then

$$P\big(G(n,p)\ \text{contains no independent set of size } r\big) \le 2\exp\Big(-\frac{u^2}{r^2(r-1)^2}\Big).$$

Significance

The results. Theorem 9.1 is a two-sided concentration statement for $\chi(G(n,p),m)$ with an explicit Gaussian error $2e^{-t^2/8}$ and no loss in the exponent from a martingale difference bound; for sparse $p = n^{-\alpha}$, where small vertex sets are sparse enough to be coloured with few colours, it localises $\chi$ to a bounded window. Proposition 9.2 is the independent-set estimate on which the greedy upper bound for $\chi(G(n,p))$ rests, obtained here with the same tool and constants $2$ and $r^2(r-1)^2$ stated on the page.

Formalizing them. All results are proved on paper; none of them, nor any concentration statement for $\chi(G(n,p))$, is formalized in Lean or on the platform. A formal development gives a machine-checked model of $G(n,p)$ both as an edge product and as a vertex-exposure product, a statement-level check of how the convex-hull inequality transfers to graph functionals, and a corrected form of Proposition 9.2 (see the scope section): the printed hypothesis (9.4) is satisfied vacuously by graphs without independent $r$-sets, and the formal statement records the hypothesis the proof uses.

Difficulty

The obvious encoding of $G(n,p)$ is the edge product $\{0,1\}^{E_0}$, and it is the wrong one for Theorem 9.1: changing the edges at one vertex changes up to $n-1$ coordinates, so a Hamming-type control of $\chi(G,m)$ in the edge coordinates gives fluctuations of order $\sqrt{n^2}$ instead of order $\sqrt m$. The statement is therefore tied to the vertex-exposure product $\Omega'$, and transporting the law of $G(n,p)$ to $\Omega'$ and handling the "largest integer $a$" with $P(\chi \ge a) \ge e^{-t^2/8} + b$ are further steps a formal proof must carry out. For Proposition 9.2 a plain Hamming-distance bound in the edge coordinates gives the wrong dependence on the number of independent sets: a graph with many independent $r$-sets is turned into one with none by adding an edge inside each of them, and since these sets overlap heavily, the Hamming distance to the graphs without independent $r$-sets is not determined by their number.

Formalization scope

Vertices are Fin n (0-based). $G(n,p)$ is graphOf x for $x : E_0 \to \mathrm{Bool}$ under gnp n p, the product (Measure.pi) of the law $p\,\delta_1 + (1-p)\,\delta_0$ on Bool, with $E_0$ the subtype $\{(i,j) : i<j\}$; all sets of this finite space are measurable. Probabilities are Measure.real, so right-hand sides may be negative, as on the page. $\chi(G,A)$ is Mathlib's chromaticNumber of the induced subgraph in ℕ∞; $\chi(G,m)$ is an infimum in ℕ∞, equal to $+\infty$ when $m>n$, and Theorem 9.1 carries $m \le n$, implicit on the page, without which it fails. Comparisons with integers are made in WithTop ℤ. The supremum over small sets $F$ is an ℕ∞ supremum over finsets with $\operatorname{card}F \le t\sqrt m$. The vertex-exposure space has a coordinate $\{0,1\}^j$ for every 0-based vertex $j$, the trivial one for $j=0$ included, as in the paper's $\prod_{j\le n}\Omega_j$; the weights in $B$ are nonnegative, the setting of Lemma 4.1.2.

Proposition 9.2 is stated with three explicit additions: $r \ge 2$, $u \ge 0$, and the event of (9.4) intersected with "$G(n,p)$ contains an independent set of size $r$". As printed, (9.4) holds for every $u$ whenever $G(n,p)$ almost surely has no independent $r$-set (both sums are zero), and the conclusion then fails; the proof selects a graph with $N>0$, which is exactly the added clause.

A formalization in which $\chi(G,m)$ is a real infimum (junk value $0$ on the empty family), in which the Bochner integral replaces probabilities, or in which the coloured set $A$ ranges over all vertices instead of $m$-subsets would trivialise or change Theorem 9.1; these are ruled out by the definitions above.

Theorem 4.1.1 (the convex-hull inequality) and Lemma 4.1.2 are posed in their own mission and are not repeated here; a complete development needs them on the finite product $\Omega'$, the identity in law between the edge and vertex-exposure models, and monotonicity and subadditivity of chromatic numbers of induced subgraphs. The vertex-exposure model and the independent-set counts are reusable for other random-graph functionals. Proofs of any milestone, and of the law identity between the two models, are welcome.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
• E. Shamir, J. Spencer, Sharp concentration of the chromatic number on random graphs $G_{n,p}$, Combinatorica 7 (1987), 121–129. https://doi.org/10.1007/BF02579208
• B. Bollobás, The chromatic number of random graphs, Combinatorica 8 (1988), 49–55. https://doi.org/10.1007/BF02122551
• S. Janson, Poisson approximation for large deviations, Random Structures & Algorithms 1 (1990), 221–229. https://doi.org/10.1002/rsa.3240010209
• N. Alon, J. Spencer, The Probabilistic Method, Wiley, 1992 ([A-S] in the paper). https://doi.org/10.1002/0471722154

Motivation

A product probability space $(\Omega^N, P)$, $P=\mu^{\otimes N}$, concentrates its mass: a set $A$ of non-negligible measure is "close" to most points. How closeness is measured decides what the statement can be used for. The Hamming distance (Chapter 2 of the paper) counts coordinates in which a point differs from $A$; it gives Gaussian concentration, but only for functions that are Lipschitz for one fixed weighting of the coordinates. Chapter 4 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), introduces the convex hull distance, which controls every weighted Hamming distance at once with weights chosen after seeing the point. This one inequality is what the second half of the paper uses for the longest increasing subsequence, bin packing, suprema of linear forms, the chromatic number of random graphs, the random assignment problem and the travelling salesman problem, and it is the form in which "Talagrand's inequality" is usually quoted in probability and combinatorics.

History (paper, p. 125). The author first proved the deviation inequality of Theorem 13.2 of the paper for symmetric $\pm1$ variables; W. B. Johnson and G. Schechtman extended it, and their one-dimensional lemma (Lemma 4.1.3 here) led to the abstract setting of Theorem 4.1.1. Section 4.2 sharpens the exponent $1/4$ by replacing $f_c^2/4$ with an exactly optimised penalty $f_\alpha$.

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer and $P=\mu^{\otimes N}$ on $\Omega^N$. For $A\subseteq\Omega^N$ and $x\in\Omega^N$ let

$$U_A(x)=\{(s_i)_{i\le N}\in\{0,1\}^N;\ \exists y\in A,\ s_i=0\Rightarrow x_i=y_i\},$$

the set of $0$–$1$ vectors marking a superset of the coordinates in which $x$ differs from some point of $A$. Let $V_A(x)$ be its convex hull in $\mathbb R^N$; it contains $0$ exactly when $x\in A$. The convex hull distance $f_c(A,x)$ is the Euclidean distance from $0$ to $V_A(x)$, and the enlargement of $A$ is

$$A_t^c=\{x\in\Omega^N;\ f_c(A,x)\le t\}$$

(the superscript $c$ stands for "convexity", not for a complement). For $\alpha\ge0$ and $u\in[0,1]$ put

$$\xi(\alpha,u)=\alpha(1-u)\log(1-u)-(\alpha+1-\alpha u)\log\Big(\frac{1+\alpha-\alpha u}{1+\alpha}\Big),$$

and let $f_\alpha(A,x)=\inf\{\sum_{i\le N}\xi(\alpha,s_i);\ s\in V_A(x)\}$; it plays the role of $f_c^2(A,x)$.

Formalization targets

Goal: Theorem 4.2.4

For $\alpha>0$ and every $A\subseteq\Omega^N$,

$$\int\exp f_\alpha(A,x)\,dP(x)\le\frac{1}{P(A)^{\alpha}}.$$

The constant is exact (no unspecified constants), and the statement holds for every probability space $\Omega$ and every $N$.

Milestones

• Lemma 4.1.2: $x\in A_t^c$ iff for every real $(\alpha_i)$ some $y\in A$ has $\sum\{\alpha_i;\ x_i\ne y_i\}\le t(\sum\alpha_i^2)^{1/2}$.
• Lemma 4.1.3: $\inf_{0\le\lambda\le1}r^{-\lambda}\exp\frac{(1-\lambda)^2}{4}\le2-r$ for $0\le r\le1$.
• Lemma 4.2.1: $\inf_{0\le\lambda\le1}r^{-\lambda\alpha}\exp\xi(\alpha,1-\lambda)=1+\alpha-\alpha r$ for $0<r<1$.
• Lemma 4.2.2: $\xi(\alpha,\cdot)$ is increasing and convex on $[0,1]$ and $\xi(\alpha,u)\ge\frac{\alpha}{2(\alpha+1)}u^2$.
• Lemma 4.2.3: $1+\alpha-\alpha a\le a^{-\alpha}$ and $a+(1-a)\exp\xi(\alpha,1)\le a^{-\alpha}$.
• Eq. (4.2.6): $P(A_t^c)\ge1-P(A)^{-\alpha}\exp\big(-\frac{\alpha t^2}{2(\alpha+1)}\big)$.
• Corollary 4.2.5: for $t\ge\sqrt{2\log(1/P(A))}$, $P(A_t^c)\ge1-\exp\big(-\frac12(t-\sqrt{2\log(1/P(A))})^2\big)$.
• Theorem 4.3.1 (two-point space, uniform $\mu$, $\alpha\ge1$): $\int\exp\big(\frac{\alpha}{\alpha+1}f_c^2(A,x)\big)\,dP(x)\le P(A)^{-\alpha}$.

Significance

The result. At $\alpha=1$, Lemma 4.2.2 gives $\xi(1,u)\ge u^2/4$, so the goal contains Theorem 4.1.1,

$$\int\exp\tfrac14f_c^2(A,x)\,dP(x)\le\frac1{P(A)},\qquad P(A_t^c)\ge1-\frac1{P(A)}e^{-t^2/4},$$

the convex distance inequality itself. For general $\alpha$ it improves the coefficient of $t^2$ from $1/4$ to the optimal $1/2$ (Corollary 4.2.5), and since $\xi(\alpha,1)=\log(1+\alpha)$ grows with $\alpha$, it simultaneously controls the number of coordinates in which $x$ must be changed to reach $A$, recovering features of the $q$-point inequalities of Chapter 3. Every Part II application of the paper rests on Theorem 4.1.1 or on this sharpening.

Formalizing it. All results here are proved in the paper (the goal's proof is "an obvious adaptation" of that of Theorem 4.1.1, by induction on $N$). None of them has a machine-checked proof for a general probability space. Theorem 4.1.1 itself is posed on the platform, still open, for finite alphabets and finite sets (Talagrand.Eexp_mul_mass_le_one, Talagrand.mass_mul_mass_le_exp); it is not posed again here. A proof of the goal settles it for arbitrary $\Omega$ and arbitrary measurable $A$.

Difficulty

The function $x\mapsto f_\alpha(A,x)$ is not a sum of one-coordinate terms, so no tensorization of a one-dimensional inequality applies directly. Bounding $f_\alpha(A,x)$ pointwise by the distance to a single nearby point of $A$ gives only Hamming-type bounds with a fixed weighting, which is exactly what the convex hull distance is designed to beat; the inequality has to hold for the infimum over the whole hull. The one-coordinate estimate the paper uses is the exact identity of Lemma 4.2.1, which leaves no slack. A further obstacle is analytic: $V_A(x)$ is a convex hull in $\mathbb R^N$ of a set indexed by the possibly uncountable set $A$, and its infima must be compared across dimensions $N$ and $N+1$.

Formalization scope

• $\Omega^N$ is Fin N → Ω; $P$ is Measure.pi (fun _ : Fin N => μ) with IsProbabilityMeasure μ.
• $U_A(x)$ is a set of Fin N → ℝ with values in $\{0,1\}$; $V_A(x)$ is convexHull ℝ (U A x). The $\ell^2$ norm is written out as $\sqrt{\sum_i s_i^2}$: Mathlib's norm on Fin N → ℝ is the sup norm.
• $f_c$ and $f_\alpha$ take values in $[0,\infty]$ (ℝ≥0∞); both are $+\infty$ when $A=\varnothing$. $\exp(+\infty)=+\infty$ (EReal.exp), $P(A)^{-\alpha}=+\infty$ when $P(A)=0$. No real-valued infimum or Bochner integral is used, so no junk value can make a bound hold for free.
• $\xi(\alpha,1)=\log(1+\alpha)$ relies on $0\cdot\log0=0$, which Mathlib's Real.log 0 = 0 provides.
• Measurability. The paper ignores measurability (pp. 81–82). Here $A$ and $x\mapsto f_\alpha(A,x)$ are assumed measurable (explicit hypotheses), integrals are ∫⁻, and $P(A_t^c)$ is the measure of an arbitrary set, i.e. its outer probability, as the paper prescribes.
• $\alpha>0$ in the goal; $t\ge0$ for the enlargement; $P(A)>0$ in Corollary 4.2.5, where the paper's hypothesis on $t$ is otherwise unsatisfiable. In §4.3, $\Omega=\{0,1\}$ is Bool with PMF.uniformOfFintype.
• A trivializing formalization is ruled out: restricting $\Omega$ to a finite type or $A$ to a finite set would give a strictly weaker statement (and the finite case of Theorem 4.1.1 is already posed elsewhere).
• Needed infrastructure: convex hulls of $0$–$1$ vectors and their behaviour under adding a coordinate, Hölder's inequality for ∫⁻, Fubini for Measure.pi on Fin (N+1), and the one-variable calculus of $\xi$. The definitions module is the substrate the Part II chapters of the paper use; proofs of the one-variable lemmas and of the induction step are welcome independently.
• Corollary 4.3.2 is not included: the paper derives it from Theorem 4.3.1 by optimising over $\alpha\ge1$, which only covers $t\ge2\sqrt{\log(1/P(A))}$, and the printed range $t\ge\sqrt{\log(1/P(A))}$ is not established on the page.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376

Motivation

Sequencing jobs on one machine to minimize the total weighted completion time $\sum_j w_jC_j$ is one of the basic problems of scheduling theory. Without precedence constraints it is solved by Smith's ratio rule (1956): sequence the jobs in nonincreasing order of $w_j/p_j$. With arbitrary precedence constraints the problem is NP-hard, as Lawler shows in the same report. Between these two extremes lies the class of series parallel precedence constraints, which covers chains, rooted trees and their nested combinations, and which is exactly the class that can be assembled from single jobs by "all of this before all of that" and "this independently of that".

Lawler's report (IRIA-LABORIA No. 205, 1976; Annals of Discrete Mathematics 2, 1978) gives an $O(n\log n)$ algorithm for this class, once a decomposition of the constraints is known. It is the standard reference for the polynomial case of $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$.

Timeline.

• 1956, Smith: the ratio rule, no precedence constraints.
• 1964, Conway, Maxwell and Miller: parallel chains with unit weights.
• 1971–1973, Baker, Horn, Adolphson and Hu: rooted trees, in $O(n\log n)$.
• 1975, Sidney: job modules and $\rho$-maximal initial sets, for arbitrary precedence constraints, without an efficient method to find them.
• 1976/1978, Lawler: series parallel constraints in $O(n\log n)$; NP-completeness for arbitrary constraints.

Setting

There are $n$ jobs, forming a finite set $N$, to be processed by a single machine. Precedence constraints are given by an acyclic digraph $G=(N,A)$: job $i$ must precede job $j$ if there is a directed path from $i$ to $j$. Job $j$ has a processing time $p_j>0$ and a real weight $w_j$ (of either sign). A feasible sequence lists every job once and never puts a job before one that must precede it. The machine starts at time $0$ without idle time, so the completion time $C_j$ of job $j$ is the sum of the processing times of $j$ and the jobs before it. The cost of a sequence is $\sum_{j\in N} w_jC_j$, and an optimal sequence is a feasible sequence of minimum cost.

A transitive series parallel digraph is built from single nodes by series composition $(N_1\cup N_2,\ A_1\cup A_2\cup N_1\times N_2)$ and parallel composition $(N_1\cup N_2,\ A_1\cup A_2)$ of digraphs on disjoint node sets. $G$ is series parallel if its transitive closure is transitive series parallel. A decomposition tree records such a construction: its leaves are the jobs, and its internal nodes are marked $S$ (left son before right son) or $P$.

Sidney's theory works with three notions. A nonempty $M\subseteq N$ is a module if every job outside $M$ must precede all of $M$, must follow all of $M$, or is unconstrained with respect to all of $M$. A subset $I\subseteq M$ is an initial set of $M$ if it contains, with each of its jobs, every job of $M$ that must precede it. With

$$\rho(I)=\frac{\sum_{j\in I}w_j}{\sum_{j\in I}p_j},$$

an initial set $I^*$ is $\rho$-maximal if $\rho(I^*)\ge\rho(I)$ for every initial set $I$ of $M$.

A composite job is a sequence of jobs treated as one job whose weight and processing time are the sums over its jobs. Lawler's algorithm works bottom-up on the decomposition tree and represents an optimal sequence for each node's module as a set of composite jobs: a leaf gives its job, a $P$-node the union of its sons' sets, and an $S$-node the output of the series procedure (Steps 1–3, p. 11), which absorbs elements of $M_1$ and $M_2$ into a composite job $k=(i,k)$ or $k=(k,j)$ until the ratios separate.

Formalization targets

Goal: the algorithm is correct

For a decomposition tree $T$ of $G$ and any run of the algorithm on $T$ producing the set $F$ of composite jobs, every arrangement $L$ of $F$ in nonincreasing ratio order, with each composite job expanded into its sequence, is an optimal sequence:

$$\operatorname{flatten}(L)\ \text{is an optimal sequence for } N .$$

Ties, both in the algorithm's choice of minimal and maximal elements and in the final sort, may be broken arbitrarily.

Milestones

1. Subtrees are modules (p. 7): the leaves of any subtree of a decomposition tree form a module.
2. Theorem 1 (p. 7): an optimal sequence for a module extends to an optimal sequence for $N$ in which the module's jobs keep their order.
3. Existence (Definition 3, p. 8): every module has a $\rho$-maximal initial set.
4. Theorem 2 (p. 8): for a $\rho$-maximal initial set $I$ of a module $M$, some optimal sequence for $N$ runs $I$ consecutively, before all other jobs of $M$.
5. Ratio order (p. 10): composite jobs in nonincreasing ratio order cost no more than in any other order.
6. Parallel composition (p. 10): the union of two representing sets represents the parallel composition.
7. Series composition, separated ratios (p. 10): if every ratio in $M_1$ exceeds every ratio in $M_2$, the union represents the series composition.
8. Series composition, Steps 1–3 (pp. 10–11): the output of the series procedure represents the series composition.

A companion theorem states that the algorithm always has a run.

Significance

The result places $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ with series parallel constraints in polynomial time. Sidney's module and $\rho$-maximal initial set machinery, which it uses, is the decomposition later used in approximation algorithms for general precedence constraints; Theorems 1 and 2 hold for arbitrary acyclic constraints.

The algorithm and Sidney's theorems are proved in the literature; none of them has a machine-checked proof. The report proves Theorems 1 and 2 by citation to Sidney's 25 lemmas and argues the algorithm's correctness informally in a few paragraphs. A formal development supplies the missing invariants (what exactly is preserved at each node of the tree) and checks that arbitrary tie-breaking is harmless.

Difficulty

The algorithm's correctness rests on an invariant the page states only in passing: that composite jobs behave as single jobs. Read literally, "nonincreasing ratio order is optimal for $M_1$ and for $M_2$" does not imply the same for their parallel composition. A composite job of two unconstrained jobs can be optimal on its own module yet blocks a better interleaving once another module is added. The invariant that makes the induction go through is that every composite job is a $\rho$-maximal initial set of itself, and the series procedure must be shown to preserve it while merging. The second difficulty is Theorems 1 and 2 themselves: exchange arguments over sequences of a whole module, with real weights of either sign, under arbitrary acyclic constraints.

Formalization scope

Jobs have a type $\iota$ with decidable equality; $N$ is a Finset ι; the arcs are a relation G : ι → ι → Prop with endpoints in $N$, acyclic in the sense that no job reaches itself by a path, and "must precede" is Relation.TransGen G. Processing times are positive on $N$, weights are arbitrary reals. The objective and optimality are the published SingleMachinePrec.Biclique.WeightedCompletion; feasibility is checked against the arcs of $G$, which for a sequence listing each job once is the same as against its paths. "Optimal for $M$" uses the job set $M$.

The decomposition tree is an inductive SPTree with leaves, $S$-nodes and $P$-nodes. It is tied to $G$ by three hypotheses: its leaves are distinct, they are exactly $N$, and on $N$ the transitive closure of $G$ equals the arc relation of the transitive series parallel digraph the tree builds. Composite jobs are lists of jobs, sets of composite jobs are lists of lists, and their ratio is $\sum w/\sum p$ over the list. The algorithm is an inductive relation (Run, SeriesMerge, SeriesLoop), so every tie-breaking is a run. The dummies of ratio $\pm\infty$ in Step 1 become vacuous conditions on empty sets.

Committed conventions and disclosed deviations:

• Lean evaluates $0/0=0$, so $\rho(\emptyset)=0$; $\rho$-maximality compares nonempty initial sets only and requires the maximal set to be nonempty, and composite jobs are nonempty.
• Modules use the disjunction of (4.1)–(4.3); for acyclic $G$ and nonempty $M$ this is the page's "exactly one".
• "Represents an optimal sequence" includes the composite invariant (every nonempty proper prefix has ratio at most the whole). Without it the parallel and series milestones are false.
• In the parallel and series milestones, $M_1$, $M_2$ and $M_1\cup M_2$ are assumed to be modules, as on the page (the sons of a node of the decomposition tree and the node itself). Without this, a path through a job outside $M_1\cup M_2$ could constrain two of its jobs while feasibility on $M_1\cup M_2$ does not see it, and the series milestone would be false.
• The introduction's "nondecreasing order of the ratios" (p. 1) is a slip for the nonincreasing order used in §5; the formalization uses nonincreasing.

The goal assumes nothing about modules, Theorem 2 or subtrees, only the tree, the data and a run, and the companion theorem shows that runs exist, so the goal is neither trivial nor vacuous.

Needed infrastructure: exchange arguments for $\sum w_jC_j$ on lists, restriction of sequences to modules, induction over decomposition trees. Theorems 1 and 2 and the ratio-order lemma are reusable in any $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ development. Proofs of any milestone, and of the goal from the milestones, are welcome.

Selected references

• E. L. Lawler, Sequencing jobs to minimize total weighted completion time subject to precedence constraints, IRIA-LABORIA Rapport de Recherche No. 205, December 1976. https://hal.science/hal-04716371v1. Journal version: Annals of Discrete Mathematics 2 (1978), 75–90. https://doi.org/10.1016/S0167-5060(08)70323-6
• J. B. Sidney, Decomposition algorithms for single-machine sequencing with precedence relations and deferral costs, Operations Research 23 (1975), 283–298. https://doi.org/10.1287/opre.23.2.283
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956), 59–66. https://doi.org/10.1002/nav.3800030106
• J. Valdes, R. E. Tarjan, E. L. Lawler, The recognition of series parallel digraphs, SIAM Journal on Computing 11 (1982), 298–313. https://doi.org/10.1137/0211023

Motivation

Ulam asked, in the early 1960s, how long the longest increasing subsequence of a random permutation typically is. The question is a test case for a whole class of problems in combinatorial probability: a quantity defined by an optimisation over exponentially many configurations (here, all subsequences) whose typical size has to be found without enumerating them. The same structure appears in last-passage percolation, in the patience-sorting card game, in sequence comparison, and in scheduling problems where the longest chain of a random partial order determines a makespan.

J. F. C. Kingman's IMS Special Invited Paper Subadditive ergodic theory (Ann. Probab. 1 (1973), 883–899) presents Ulam's problem in §2.4 as an application of the subadditive ergodic theorem, following J. M. Hammersley, and then proves explicit bounds on the limiting constant. This mission formalizes those bounds.

Timeline.

• Ulam (1961) raised the question and conjectured, from simulations, that the typical length grows like a constant times $\sqrt n$.
• Erdős and Szekeres (1935) had already shown deterministically that every permutation of $n$ elements has an increasing or a decreasing subsequence of length at least $\sqrt n$.
• Hammersley (A few seedlings of research, Proc. Sixth Berkeley Symp. 1 (1972), 345–394) proved, by embedding the permutation in a planar Poisson process and applying a subadditivity argument, that $n^{-1/2}$ times the length converges in probability to a constant $c$, and showed $\tfrac12\pi\le c\le e$.
• Kingman (1973), the paper of this mission, refined the bounds to $(8/\pi)^{1/2}\le c\le\delta^{1/2}+\delta^{-1/2}$, that is $1.59<c<2.49$.
• Logan and Shepp (1977) and Vershik and Kerov (1977) later identified the constant exactly. That later work is not part of this mission.

Setting

Let $\mathcal S_n$ be the group of permutations of $\{1,2,\dots,n\}$. For $\sigma\in\mathcal S_n$, a sequence of positions $1\le i_1<i_2<\dots<i_k\le n$ is ascending if $\sigma(i_1)<\sigma(i_2)<\dots<\sigma(i_k)$. The length of the longest ascending sequence, $l(\sigma)$, is the largest such $k$.

The uniform distribution on $\mathcal S_n$ gives each of the $n!$ permutations probability $1/n!$, so an event $A\subseteq\mathcal S_n$ has probability $P\{A\}=|A|/n!$. Let $\pi_n$ denote a permutation drawn from this distribution. The sequence $n^{-1/2}\,l(\pi_n)$ converges in probability to a real number $c$ if, for every $\varepsilon>0$,

$$P\{|n^{-1/2}\,l(\pi_n)-c|>\varepsilon\}\to0\qquad(n\to\infty).$$

For integers $k\ge1$, $\nu_k(\sigma)$ denotes the number of ascending sequences of length $k$ in $\sigma$. For $0<\alpha<b$ write

$$E(\alpha,b)=2\alpha+(b-\alpha)\log(b-\alpha)-\alpha\log\alpha-b\log b ,$$

the exponent appearing in Kingman's condition (2.4.8). (The paper calls the second variable $\beta$; in Lean it is $b$, because $\beta$ also names the constant below.)

Formalization targets

Goal: Theorem 8

Let $c$ be the limit in probability of $n^{-1/2}l(\pi_n)$. Let $\delta$ be the unique positive root of $\log(1+\delta)=2\delta/(1+\delta)$, and $\beta=\delta^{1/2}+\delta^{-1/2}$. Then

$$\Big(\frac8\pi\Big)^{1/2}\le c\le\beta \tag{2.4.4}$$

and hence

$$1.59<c<2.49. \tag{2.4.5}$$

Numerically $\delta\approx3.9216$ and $\beta\approx2.4853$. The goal states (2.4.4) and (2.4.5) as printed, together with the existence and uniqueness of $\delta$.

Milestones

1. Theorem 7 (Hammersley). There is an absolute constant $c$ such that $n^{-1/2}l(\pi_n)\to c$ in probability.
2. The double integral of the lower-bound argument: $\int_0^\infty\!\int_0^\infty x\,e^{-\frac12(x+y)^2}\,dx\,dy=(\pi/8)^{1/2}$.
3. First moment of $\nu$: for $k\ge1$, $E(\nu_k)=\binom nk(k!)^{-1}$.
4. Subsequence count: if $l(\sigma)\ge k$ then $\nu_k(\sigma)\ge\binom{l(\sigma)}k$.
5. (2.4.7): for $1\le k\le r$, $P\{l(\pi)\ge r\}\le\binom nk\big[k!\binom rk\big]^{-1}$.
6. (2.4.8): if $0<\alpha<b$ and $E(\alpha,b)<0$, then $P\{l(\pi)\ge b\,n^{1/2}\}\to0$.
7. The optimisation: $\inf\{b>0:\exists\alpha\in(0,b),\ E(\alpha,b)<0\}=\delta^{1/2}+\delta^{-1/2}$.

Significance

The result. Theorem 8 was, at the time, the sharpest rigorous information about Ulam's constant. Its upper bound comes from a first-moment computation that applies to any random structure in which long increasing chains can be counted; the same calculation bounds the longest chain in random partial orders and the height of random $k$-dimensional orders. The lower bound shows that a greedy path through a Poisson process already achieves a positive fraction of the optimum, an argument reused for last-passage percolation models.

Formalizing it. All results here are proved in the literature; none is open. To the best of our knowledge none of them has been machine-checked. A complete development produces: an exact non-asymptotic tail bound on the longest increasing subsequence ((2.4.7)), useful on its own; a Stirling-type asymptotic for products of binomial coefficients at scale $\sqrt n$; and, through Theorem 7, a formal existence proof of the Ulam constant. Theorem 7 is the substantial piece: the paper's proof is a sketch through a continuous-parameter subadditive ergodic theorem and a planar Poisson process.

Difficulty

The upper bound needs care with asymptotics: (2.4.7) holds for each $n$, but the passage to (2.4.8) uses Stirling's formula with $k$ and $r$ integers tending to infinity at rate $\sqrt n$, and the infimum in milestone 7 is not attained (the admissible set is open), so the argument must produce, for every $b>\beta$, a suitable $\alpha$.

The lower bound is where the obvious approach fails. A first-moment or counting argument gives only upper bounds on $l$; a lower bound requires exhibiting long ascending sequences. The paper's argument does this with a greedy path in a planar Poisson process, which is not a statement about uniform permutations and needs the Poissonization of Theorem 7 to transfer back. Proving $c\ge(8/\pi)^{1/2}$ directly from the counting definition of $l$ is not available. Both bounds also need the existence of $c$, which is Theorem 7.

Formalization scope

• $\mathcal S_n$ is Equiv.Perm (Fin n); the permutation is named $\sigma$ in Lean because $\pi$ is Real.pi.
• $l(\sigma)$ is the largest cardinality of a finite set of positions on which $\sigma$ is strictly increasing; $\nu_k(\sigma)$ is the number of such sets with exactly $k$ elements.
• Probabilities under the uniform law are proportions $|A|/n!$. Convergence in probability depends only on the law of each $\pi_n$ (the paper notes this on p. 895), so no common probability space is introduced. Time is $n\in\mathbb N$, and at $n=0$ Lean reads $l/\sqrt0$ as $0$, which does not affect a limit.
• The constant of Theorem 8 enters as a hypothesis: the goal is stated for every real $c$ to which $n^{-1/2}l(\pi_n)$ converges in probability. Such a limit is unique, and Theorem 7 shows it exists. No sign or bound on $c$ is assumed. The goal and milestone 7 assert that the positive root $\delta$ exists and is unique, so the upper bound cannot hold vacuously for want of a root.
• The double integral is stated as a value only; the claim that it is the mean of i.i.d. increments of a Poisson greedy path is not formalized.

Needed infrastructure: counting arguments on Finset.powersetCard; Stirling's formula (Mathlib has Stirling.tendsto_stirlingSeq_sqrt_pi); elementary calculus for the root $\delta$; Gaussian-type integrals on the quadrant. Theorem 7 additionally needs Poisson point processes in the plane, which Mathlib lacks, or another route to the existence of the limit. Contributions of that infrastructure are welcome and reusable well beyond this mission. The counting bounds (milestones 3–5) are independent of Theorem 7 and are a natural first target.

Selected references

• J. F. C. Kingman, Subadditive ergodic theory, Annals of Probability 1(6) (1973), 883–899. https://doi.org/10.1214/aop/1176996798
• J. M. Hammersley, A few seedlings of research, Proc. Sixth Berkeley Symposium on Mathematical Statistics and Probability, Vol. 1 (1972), 345–394. https://projecteuclid.org/euclid.bsmsp/1200514101
• S. M. Ulam, Monte Carlo calculations in problems of mathematical physics, in Modern Mathematics for the Engineer, Second Series, McGraw-Hill (1961), 261–281.
• P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Mathematica 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/

Motivation

A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in which a task may be interrupted and resumed later on the same machine. For two machines the optimal finish time is computed by Johnson's rule, and preemption does not help. The paper shows that with three machines the preemptive problem is already NP-complete, and its second result, Theorem 2, strengthens this to NP-completeness in the strong sense: the problem stays hard even when the task times are written in unary.

Strong NP-completeness matters because it rules out a pseudo-polynomial algorithm, one whose running time is polynomial in the sum of the task lengths. The preemptive three-machine flow shop ($F3\mid pmtn\mid C_{\max}$ in later notation) is a standard entry in complexity classifications of scheduling problems, and Theorem 2 is the reference for its status. The paper notes that Garey and Johnson obtained a proof independently.

Timeline. Johnson (1954) solved the two-machine flow shop. Garey, Johnson and Sethi (1976) proved the non-preemptive three-machine flow shop NP-complete in the strong sense. Gonzalez and Sahni (1978) treated the preemptive case: Theorem 1 (ordinary NP-completeness via Partition) and Theorem 2 (strong NP-completeness via 3-Partition), the subject of this mission.

Setting

A flow shop has $m\ge 1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ runs on $P_j$ and takes time $t_{j,i}\ge 0$; zero times are allowed. For each job, task $j\ge 2$ can begin only after task $j-1$ has been completed, and schedules start at time $0$.

A preemptive schedule is given, as in the paper's footnote on p. 40, by finitely many pieces $(s,f)$ per task: the task is processed on its processor during $[s,f)$. Pieces have $0\le s<f$, pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$, and a piece of task $j'$ starts only after every piece of every earlier task $j<j'$ of the same job has ended. A task has no preemption when it is processed in at most one piece; a non-preemptive schedule has no preemption anywhere. The completion time of job $i$ is $f_i(S)$, the end of its last piece, and the finish time is $FT(S)=\max_i f_i(S)$.

3-Partition. An instance $C=(a_1,\dots,a_s,B)$, $s=3t$, consists of a positive integer $B$ and nonnegative integers $a_i$ with $\sum_i a_i=tB$ and $B/4<a_i<B/2$. It has a 3-partition if $\{1,\dots,s\}$ splits into $t$ disjoint sets $L_1,\dots,L_t$, each of three elements with $\sum_{j\in L_k}a_j=B$.

The instance FS. From $C$ the proof of Lemma 4 builds a three-processor flow shop with $s+t+2$ jobs:

• jobs $1,\dots,s$: times $(a_i,\,0,\,a_i)$ on $(P_1,P_2,P_3)$;
• job $s+1$: $(0,\,2B,\,B)$;
• jobs $s+i+1$, $1\le i\le t-2$: $(B,\,2B,\,B)$;
• job $s+t$: $(B,\,2B,\,0)$;
• job $s+t+1$: $(0,\,0,\,B)$;
• job $s+t+2$: $(B,\,0,\,0)$.

Each processor carries total work exactly $2tB$, and the threshold is $\tau=2tB$.

Formalization targets

Goal: Theorem 2, as Lemma 4's equivalence

For every 3-Partition instance $C$ with $t\ge 2$,

$$\exists\,S \text{ preemptive schedule of } FS:\ FT(S)\le 2tB \quad\Longleftrightarrow\quad C \text{ has a 3-partition},$$

and every task time of $FS$ satisfies $t_{j,i}\le 2B$. The second clause records that the instance's numbers are bounded by those of $C$, the reduction's contribution to "the problem size being measured as the sum of the length of the tasks".

Milestones

1. Lemma 3 (p. 40). For a flow shop with $m\ge 1$ processors, every preemptive schedule $S$ can be replaced by a schedule $S'$ with no preemptions on $P_1$ and on $P_m$ and $FT(S')=FT(S)$.
2. Lemma 4(a) (p. 41). If $C$ has a 3-partition, $FS$ has a non-preemptive schedule with $FT\le 2tB$.
3. First step of Lemma 4(b) (pp. 41–42). In every preemptive schedule of $FS$ with $FT\le 2tB$, the jobs among $1,\dots,s$ whose $P_1$ task is completed by time $2B$ have $\sum t_{1,i}=B$.
4. Lemma 4(b) (pp. 41–42). If $C$ has no 3-partition, every preemptive schedule of $FS$ has $FT>2tB$.

Significance

The result. Theorem 2 places the preemptive three-machine flow shop among the strongly NP-hard scheduling problems, so no algorithm polynomial in the number of jobs and the total processing time exists unless P = NP. It also shows that allowing preemption, which makes several single-stage problems (such as $P\mid pmtn\mid C_{\max}$) easy, does not help for three-stage flow shops. Lemma 3, that preemptions on the first and last machines can be removed without changing the finish time, holds for any number of machines and is a reusable structural fact about flow-shop schedules.

Formalizing it. The result is proved on paper, and its proof of the "only if" direction is an informal busy-processor argument repeated window by window. As far as is known, no part of it has a machine-checked proof. A formal development has to make the interval accounting rigorous: why each processor is busy throughout $[0,2tB]$, why exactly $B$ units of element jobs end on $P_1$ by $2B$, and how the argument restarts on $[2B,2tB]$. Lemma 3 needs an exchange argument on piece representations. Both are new for the platform.

Difficulty

The direction "3-partition $\Rightarrow$ schedule" is a direct construction. The hard direction is the converse. Preemption lets any task be split across many intervals, so the usual non-preemptive arguments, which reason about the order in which whole tasks run, do not apply directly. The paper's argument that the window $[0,2B]$ must contain exactly three element jobs of total $B$ on $P_1$ depends on every processor being continuously busy, and turning "otherwise there is idle time" into a precise statement requires a careful account of which jobs are available to each processor at each moment. The induction on windows is then not a literal restriction of the schedule to a smaller instance, because pieces may cross the boundary at $2B$.

Formalization scope

• Times are real numbers; the 3-Partition data are natural numbers cast to $\mathbb R$. Processors are Fin m with $P_1=$ 0; in $FS$, $P_1,P_2,P_3$ are 0, 1, 2.
• The 3-Partition instance is the published ResourceScheduling.Chain.ThreePartition (0-based indices, t parts, b $=B$, Valid, HasSolution), whose definition is the paper's p. 37 problem.
• Preemptive schedules are finite sets of pieces per task; precedence is required between every pair of tasks $j<j'$ of a job, so a zero task occupies no time and does not break the job's order. Finish time is a maximum over jobs with baseline $0$, never an unattained supremum.
• "No preemptions on $P_j$" means at most one piece per task on $P_j$.
• Not formalized: "NP-complete", the reduction symbol $\propto$, "the problem size being measured as the sum of the length of the tasks", and Lemma 2 (membership in NP). The goal states the equivalence Lemma 4 proves for the constructed instance, plus the bound $t_{j,i}\le 2B$ on its task times.
• Added hypothesis: $t\ge 2$. For $t<2$ the paper's job indices $s+1$ and $s+t$ coincide with conflicting times, so the construction is undefined there.
• The first step of Lemma 4(b) is read as: the sum of $t_{1,i}$ over element jobs whose $P_1$ task has completed by time $2B$ equals $B$.
• A trivializing formalization is ruled out: the schedules quantified over are all preemptive schedules of the specific instance $FS(C)$, the threshold $2tB$ is explicit, and the validity conditions $B/4<a_i<B/2$ are kept, so the schedule side cannot match the weaker "partition into $t$ groups of sum $B$".

Contributions welcome: the interval-accounting lemmas (busy processors, work available before a time), Lemma 3's exchange argument, and the schedule of Figure 2.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1):36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, "Strong" NP-Completeness Results: Motivation, Examples, and Implications, Journal of the ACM 25(3):499–508, 1978. https://doi.org/10.1145/322077.322090

Motivation

A birth-and-death process describes a population in which each individual independently gives birth and dies at given rates. Kendall's 1948 paper (doi:10.1214/aoms/1177730285) solved the process with arbitrary time-dependent rates and, in its §4, introduced a second random variable alongside the population size: the cumulative population $M_t$, the number of individuals that have ever been alive up to time $t$. Kendall gives two readings. If $n_t$ is the number of current cases of a disease, $M_t$ is the total number of cases recorded so far, and for an epidemic that is almost certain to die out, $M_\infty$ measures its overall severity. If $n_t$ is the viable count of a bacterial population, $M_t$ is the total count, in which living and dead organisms are not distinguished.

The question of this mission is the exact distribution of $M_\infty$ for the simplest transient process, with constant rates. Kendall answers it in §5 by solving a first-order partial differential equation for the joint generating function of $(n_t, M_t)$. The resulting law involves central binomial coefficients, the same numbers that count the total progeny of a critical binary branching process.

Setting

Let $\lambda_0 > 0$ and $\mu_0 > 0$ be constants. In the simple birth-and-death process with these rates, a population of size $n$ moves to $n + 1$ at rate $\lambda_0 n$ and to $n - 1$ at rate $\mu_0 n$. It starts from one ancestor, $n_0 = 1$. The cumulative population $M_t$ starts at $M_0 = n_0 = 1$ and shares all the positive jumps of $n_t$, so it never decreases. The process is transient (dies out with probability one) when $\lambda_0 \le \mu_0$.

Write $P_{n,M}(t)$ for the joint law of $(n_t, M_t)$ and

$$\psi(z, w, t) = \sum_{n=0}^\infty\sum_{M=0}^\infty P_{n,M}(t)\,z^n w^M$$

for its generating function (30). Kendall shows that $\psi$ satisfies

$$\frac{\partial\psi}{\partial t} = \{\lambda_0 w z^2 - (\lambda_0 + \mu_0) z + \mu_0\}\frac{\partial\psi}{\partial z}, \qquad \psi(z, w, 0) = zw, \tag{31–32}$$

and solves it with the roots $\alpha < \beta$ of the quadratic (49), $\lambda_0 w z^2 - (\lambda_0 + \mu_0) z + \mu_0 = 0$:

$$\psi(z, w, t) = w\,\frac{\alpha(\beta - z) + \beta(z - \alpha)e^{-\lambda_0 w(\beta - \alpha)t}}{(\beta - z) + (z - \alpha)e^{-\lambda_0 w(\beta - \alpha)t}}. \tag{50}$$

Setting $z = 1$ forgets $n_t$, so $\psi(1, w, t)$ generates the law of $M_t$. Finally

$$x = \frac{4\lambda_0\mu_0}{(\lambda_0 + \mu_0)^2}, \qquad Q_M = \frac{\lambda_0 + \mu_0}{2\lambda_0}\,\frac{(2M)!}{2^{2M}(M!)^2}\,\frac{x^M}{2M - 1}\quad(M = 1, 2, 3, \dots). \tag{52–53}$$

The Lean names are disc, alpha, beta, psi, x, Q and SolvesPDE, in the namespace KendallBD.Cumul.

Formalization targets

Goal: the law of the cumulative population (§5, (50)–(53), p. 11)

For $0 < \lambda_0 \le \mu_0$:

1. for every $w \in (0, 1)$, $\psi$ of (50) satisfies (31) at every $z \in [0, 1]$, $t \ge 0$, and $\psi(z, w, 0) = zw$;
2. for every $w \in (0, 1)$,

$$\lim_{t\to\infty}\psi(1, w, t) = \sum_{M \ge 1} Q_M w^M;$$

3. $Q_M \ge 0$ and $\sum_{M\ge1} Q_M = 1$.

Milestones (pp. 10–11)

• (49): for $0 < w < 1$ the roots satisfy $0 < \alpha < 1 < \beta$.
• (50): $\psi$ solves (31) with the boundary condition (32).
• (51): $\psi(1, w, \infty) = w\alpha = [\lambda_0 + \mu_0 - \sqrt{(\lambda_0 + \mu_0)^2 - 4\lambda_0\mu_0 w}]/(2\lambda_0)$.

Companions

• (54): $(Q_1, Q_2, Q_3, Q_4) = \frac{\mu_0}{\lambda_0 + \mu_0}(1, \frac14 x, \frac18 x^2, \frac{5}{64}x^3)$.
• (48): for $\lambda_0 < \mu_0$ the law has mean $\mu_0/(\mu_0 - \lambda_0)$ and variance $\lambda_0\mu_0(\lambda_0 + \mu_0)/(\mu_0 - \lambda_0)^3$.
• The balanced case $\lambda_0 = \mu_0$: $x = 1$, $Q_M$ decays like $M^{-3/2}$, and the mean of $M_\infty$ is infinite.

Significance

The result. The law (52) gives the full distribution of the total size of a transient linear birth-and-death population, not only its moments: the probability $Q_1 = \mu_0/(\lambda_0 + \mu_0)$ that the ancestor dies childless, the tail behaviour, and the dichotomy between the subcritical case (finite mean $\mu_0/(\mu_0 - \lambda_0)$, geometric-type tail with ratio $x < 1$) and the critical case (heavy $M^{-3/2}$ tail, infinite mean). In the epidemic reading this is the distribution of the final size of a minor outbreak; it is also the total-progeny law of the embedded binary Galton–Watson tree (Harris 1963).

Formalizing it. The result is classical and proved, but it is not formalized anywhere known to this mission. A formal proof would combine three separate pieces: the explicit solution of a first-order PDE by characteristics, checked as a classical solution on the region where a probability generating function lives; a limit $t \to \infty$ that selects one root of a quadratic; and the binomial series of $1 - \sqrt{1 - y}$ together with its boundary value at $y = 1$. The companions make the moments (48), which §4 derives by a separate route, a consequence of the law.

Difficulty

Checking that (50) satisfies (31) is calculus once the derivatives exist. The obstacles are elsewhere. First, the roots must be ordered as $0 < \alpha < 1 < \beta$, which fails at $w = 1$ when $\lambda_0 < \mu_0$ (the roots are then $1$ and $\mu_0/\lambda_0$): every statement about $\alpha$, $\beta$, $\psi$ has to be made for $0 < w < 1$, and the law is identified from the power series on that interval. Second, the normalization $\sum Q_M = 1$ is a statement at the boundary $y = xw = x$ of the series for $1 - \sqrt{1 - y}$; at $\lambda_0 = \mu_0$ this is $y = 1$, the edge of the disc of convergence, where convergence of the series is not automatic and where the value $\sqrt{1 - x} = (\mu_0 - \lambda_0)/(\lambda_0 + \mu_0)$ uses $\lambda_0 \le \mu_0$. For $\lambda_0 > \mu_0$ the same series sums to $\mu_0/\lambda_0 < 1$, so the hypothesis is essential. Third, the asymptotic $M^{-3/2}$ in the balanced case needs the asymptotics of central binomial coefficients.

Formalization scope

All objects are real functions; the process and the joint law $P_{n,M}(t)$ are not constructed, exactly as in the paper. "The law of $M_\infty$" is read, as on p. 11, as the coefficients of the generating function $\lim_{t\to\infty}\psi(1, w, t)$, and $\psi$ is tied to the process through the equation (31) and the boundary condition (32). The committed conventions are:

• constant rates $0 < \lambda_0 \le \mu_0$ (strict $\lambda_0 < \mu_0$ for the moment companion, $\lambda_0 = \mu_0$ for the balanced companion);
• $\alpha$ and $\beta$ are given by the quadratic formula, $\alpha$ with the minus sign, Real.sqrt the nonnegative root;
• statements about $\alpha$, $\beta$, $\psi$ hold for $w \in (0, 1)$; (31) is asserted for $z \in [0, 1]$, $t \ge 0$, and the boundary condition for every real $z$;
• (31) is SolvesPDE: both partial derivatives exist as HasDerivAt facts and satisfy the equation, never an equation between deriv values;
• $Q_0 = 0$ (since $M_\infty \ge M_0 = 1$), and $Q_M$ keeps the printed shape $(2M)!/(2^{2M}(M!)^2)$ with $2M - 1$ in the reals;
• "infinite mean" is non-summability of $\sum M Q_M$; the variance is stated through the second moment.

A goal that only asserted the power series identity $1 - \sqrt{1 - y} = \sum_{M\ge1}\frac{(2M)!}{2^{2M}(M!)^2(2M-1)}y^M$ would be a different and easier theorem with no birth-and-death content; the goal therefore ties $Q_M$ to $\psi$ of (50) and $\psi$ to the equation (31)–(32).

A complete development needs the binomial series for $\sqrt{1 - y}$ with real coefficients (Mathlib has Nat.centralBinom and general binomial series, and the platform has the generating function of the central binomial coefficients as a proof tool), the boundary behaviour of a power series with nonnegative coefficients, and Stirling-type asymptotics of $\binom{2M}{M}4^{-M}$. These are reusable well beyond this mission. Contributions proving any milestone or companion, or the series lemma on its own, are welcome.

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
• T. E. Harris, The Theory of Branching Processes, Springer, 1963. doi:10.1007/978-3-642-51866-9