Markov Chain

Motivation

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

Setting

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

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

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

Formalization targets

Characterization of admissible rates

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

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

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

Supporting claims

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

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

and the nonnegative normalized array relation

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

A finite Markov decision process may have several recurrent classes under one policy. In that setting, its long-run reward depends on the initial state, and a single stationary distribution does not describe the whole decision problem. Hordijk and Kallenberg developed a linear program with two families of variables to handle this multichain case. Their Theorem 8 relates policies to feasible points of that program in both directions: optimal stationary policies give optimal dual solutions, and every optimal dual solution gives an average optimal stationary policy. This relationship explains why the dual program represents the original sequential decision problem rather than merely bounding its value. Hordijk and Kallenberg (1979)

An earlier frequency formulation associated stationary randomized policies with one family of occupation variables in a more restricted Markov-chain setting. The present theorem uses both $x$ and $y$ variables, and its policy comparison covers history-dependent randomized decisions. The corresponding formalization therefore addresses the finite multichain model of the 1979 paper, with its own dual equations and representative map. Hordijk and Kallenberg (1979), §§1 and 3.3

Setting

Let $E$ be a nonempty finite set of states. At state $i$, an action $a$ is chosen from a nonempty finite set $A(i)$. It earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}$. The transition probabilities are nonnegative and sum to one over $j$. A general policy $R$ may randomize and use the complete past history. Its average reward $\phi_i(R)$ is the liminf, as the horizon grows, of expected total reward divided by the horizon when the initial state is $i$. The optimal value $\phi_i$ is the supremum of $\phi_i(R)$ over all such policies. A policy is average optimal when it attains that value at every state. These are the conventions of §2.1 of the paper. Hordijk and Kallenberg (1979), p. 353

A stationary randomized policy $\pi^\infty$ chooses each admissible action $a$ at state $i$ with a fixed probability $\pi_{ia}$, independently of the epoch and history. Its transition matrix is $P(\pi)_{ij}=\sum_{a\in A(i)}\pi_{ia}p_{iaj}$, and its reward vector is $r(\pi)_i=\sum_{a\in A(i)}\pi_{ia}r_{ia}$. The Cesàro limit matrix $P^*(\pi)$ and deviation matrix $D(\pi)$ describe the recurrent and transient behavior of this finite chain. In particular, $\phi(\pi^\infty)=P^*(\pi)r(\pi)$. Hordijk and Kallenberg (1979), p. 359

Fix positive state weights $\beta_j$ summing to one. The primal linear program minimizes $\sum_j\beta_j\widetilde\phi_j$ over pairs $(\widetilde\phi,\widetilde u)$ that are superharmonic: for every $i$ and $a\in A(i)$, the first vector dominates its one-step expected continuation, and the sum of the two vectors dominates one-step reward plus the continuation of the second. The dual linear program maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative $x_{ia}$ and $y_{ia}$ satisfying the two flow equations (3) and (4). Variables are present only for admissible state-action pairs. The set $E_x$ consists of states where $\sum_a x_{ia}>0$. Hordijk and Kallenberg (1979), pp. 356–357

For a feasible dual point $(x,y)$, the associated policy $\pi(x,y)$ normalizes the $x$ row at states in $E_x$ and the $y$ row at other states. Conversely, equation (6) constructs a representative $(x(\pi),y(\pi))$ of a stationary randomized policy. Its $x$ coordinates use $\beta^TP^*(\pi)$. Its $y$ coordinates use $\beta^TD(\pi)+\gamma^TP^*(\pi)$, where $\gamma$ is zero at transient states and is chosen separately on each recurrent class by a maximum formula. The formalization restricts that formula's denominator to the recurrent class, as required by the subsequent nonnegativity calculation; the printed unrestricted denominator has a two-state counterexample. Hordijk and Kallenberg (1979), pp. 359–360

Formalization targets

Optimality correspondence

The goal is Theorem 8, with both directions in one statement:

$$\pi^\infty\text{ average optimal}\ \Longrightarrow\ (x(\pi),y(\pi))\text{ dual optimal}, \qquad (x,y)\text{ dual optimal}\ \Longrightarrow\ \pi^\infty(x,y)\text{ average optimal}.$$

The second implication applies to every optimal dual point. It produces the stationary randomized policy given by the printed normalization rule, including its existence as a valid policy. The first implication uses the particular representative defined by equation (6). Neither direction imposes an extreme-point condition. Hordijk and Kallenberg (1979), Theorem 8, p. 360

Supporting results

The milestones state the least-superharmonic characterization of $\phi$; the positivity that makes the dual-to-policy normalization meaningful; the stationary gain identity; feasibility and objective value of the representative; and Propositions 4 and 5, which describe tight actions and identify $E_x$ with the recurrent states of $P(\pi(x,y))$. Each is a statement about the same finite model and the same primal–dual pair. Hordijk and Kallenberg (1979), pp. 356–361

Significance

The theorem establishes an exact relation between two ways of expressing average optimality. The LP direction turns an optimal stationary policy into a dual optimum with a concrete state-action representation. The converse says an arbitrary optimal dual point can be read as an average optimal policy, even when its $x$ coordinates vanish at some states. Proposition 5 specifies what those vanishing coordinates mean for the induced chain: those states are transient. These statements permit optimization over a finite LP while preserving the policy interpretation of its solutions. Hordijk and Kallenberg (1979), Theorem 8 and Proposition 5

The result was proved in 1979; this mission asks for a machine-checked proof of its precise finite-state statement. The shared MDP model and the limit and deviation matrix definitions already exist as published formal objects. The new work is the correspondence for Hordijk and Kallenberg's dual equations, with the representative, its class-wise correction, and the connection to liminf average reward. The definitions of stationary policy mixtures, admissible-pair LP coordinates, and finite-chain recurrence can support later results about average-reward optimization.

Difficulty

Normalizing $x$ alone does not define a policy at every state: its row sum can be zero. The dual program's second variable $y$ supplies the action weights there, and the feasibility equations must ensure its row sum is positive. In the other direction, the natural $\beta^TD(\pi)$ term in $y(\pi)$ need not be nonnegative. The correction $\gamma$ is chosen by a maximum over each recurrent class, while transient states require a different case. These issues remain in a multichain process even though the state and action sets are finite. Hordijk and Kallenberg (1979), pp. 359–361

Formalization scope

Lean uses finite types for states and actions, a nonempty state type, and a nonempty admissible action set at every state. The published StationaryMDP definition provides real rewards and stochastic transition rows. General policies are its history-dependent randomized AvgHRPolicy values; average reward is its liminf reward, and optimal gain is the supremum over that entire policy class. The mission defines its own average-optimality predicate because the published Puterman predicate uses a stronger limsup comparison. For finite rewards, the liminf gains and their supremum are bounded real numbers.

Stationary randomized weights are nonnegative, sum to one on each $A(i)$, and vanish outside $A(i)$. The dual variables are functions on the subtype of admissible state-action pairs. The primal and dual optima mean feasible points attaining the relevant objective against every other feasible point. The paper's positive, normalized $\beta$ remains explicit. The raw formula for $\pi(x,y)$ is used only with a feasible dual point, and the policy-well-definedness milestone supplies its nonzero denominators. The representative uses a maximum over the ergodic class of each recurrent state, with the class-restricted denominator needed by the paper's proof; replacing $\gamma$ by zero or by one global maximum would change the target.

The known matrix objects $P^*$ and $D$ are imported from the published Blackwell development. Their convergence and identities are theorem obligations, not assumptions hidden in definitions. Contributions proving the finite-chain identities, representative feasibility, complementary slackness, and the final policy comparison are within scope. A statement restricted to a unichain model, an extreme dual point, or a pure selected action would not establish this theorem.

Selected references

• A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. DOI: 10.1287/mnsc.25.4.352.

Motivation

A controller observes a finite system period after period, chooses an action in each state, earns an income and moves the system at random. When future income is not discounted, the natural criterion is the average return per unit time (the gain), but many policies share the maximal gain while differing in their transient income. Blackwell (1962) showed that the policies that are optimal as the discount factor tends to one, the 1-optimal policies, are exactly the stationary policies that first maximize the gain and then, among those, the bias. He gave no finite procedure for the second maximization. Veinott (1966) supplied one: an extension of Howard's policy improvement method in which a second improvement test, on the bias, is run after the gain test is exhausted, with a third vector $z(f)$ guaranteeing termination. The method and its sensitivity hierarchy became the starting point of the $n$-discount optimality theory developed by Veinott (1969) and treated in Puterman's Markov Decision Processes (1994), Chapter 10.

Timeline:

• 1960: Howard, Dynamic Programming and Markov Processes: policy improvement for the discounted and the average-return problems.
• 1962: Blackwell, Discrete Dynamic Programming: existence of stationary policies optimal for all discount factors near one; the expansion $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+o(1)$; nearly optimal (1-optimal) policies characterized by lexicographic maximization of $(x,y)$.
• 1966: Veinott, this paper: the extended policy improvement method that finds a 1-optimal stationary policy in finitely many steps (Theorem 6), and a finite-horizon characterization of the same policies (Theorem 7).
• 1969: Veinott, Discount optimality and sensitive optimality: the full hierarchy of $n$-discount optimal policies and the corresponding nested improvement method.

Setting

There are finitely many states $s$ and a finite set of actions. Choosing action $a$ in state $s$ earns the income $i(s,a)$ and moves the system to state $s'$ with probability $q(s'\mid s,a)$. A decision rule $f\in F$ picks an action $f(s)$ in each state; $r(f)$ is the vector with entries $i(s,f(s))$ and $Q(f)$ the stochastic matrix with entries $q(s'\mid s,f(s))$. A policy is a sequence $(f_1,f_2,\dots)$ of decision rules, $f^\infty=(f,f,\dots)$ is a stationary policy, and for $0\le\beta<1$

$$V_\beta(\pi)=\sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\,r(f_{n+1})$$

is the vector of expected discounted returns. For vectors, $u\ge v$ is coordinatewise and $u>v$ means $u\ge v$ and $u\ne v$.

Let $Q^*(f)$ be the Cesàro limit of the powers of $Q(f)$. The gain $x(f)$ and the bias $y(f)$ are the unique solutions of

$$[I-Q(f)]x=0,\quad Q^*(f)x=Q^*(f)r(f);\qquad [I-Q(f)]y=r(f)-x(f),\quad Q^*(f)y=0,$$

and $z(f)$ is the unique solution of $[I-Q(f)]z=-y(f)$, $Q^*(f)z=0$. Write $F'$ for the decision rules of maximal gain and $F''\subset F'$ for those of maximal bias within $F'$.

The two improvement sets compare $f$ with a decision rule $g$ through the state-by-state tests

$$\text{(i) } [Q(g)x(f)]_s\ge[x(f)]_s,\qquad \text{(ii) } [r(g)+Q(g)y(f)]_s\ge[x(f)+y(f)]_s .$$

$G(f)$ consists of the $g$ for which (i) holds everywhere, (ii) holds wherever (i) is an equality, some inequality is strict, and $g(s)=f(s)$ wherever both are equalities. $E(f)$ consists of the $g$ for which (i) and (ii) are equalities at every state. For $g\in E(f)$,

$$\text{(iii) } [-y(f)+Q(g)z(f)]_s\ge[z(f)]_s,$$

and $H(f)$ consists of the $g\in E(f)$ for which (iii) holds everywhere, strictly somewhere, with $g(s)=f(s)$ wherever it is an equality.

Formalization targets

Goal: Theorem 6 (p. 1290)

For every $f\in F$:

1. $G(f)=\varnothing\ \Rightarrow\ f\in F'$;
2. $G(f)\cup H(f)=\varnothing\ \Rightarrow\ f\in F''$;
3. $g\in G(f)\ \Rightarrow\ x(g)>x(f)$, or $x(g)=x(f)$ and $y(g)>y(f)$;
4. $g\in H(f)\ \Rightarrow\ x(g)=x(f)$, and $y(g)>y(f)$, or $y(g)=y(f)$ and $z(g)>z(f)$.

Part 2 is the stopping certificate and parts 3 and 4 are the progress guarantee; together they say that the extended method raises $(x,y,z)$ lexicographically and stops at a decision rule in $F''$.

Milestones

• Theorem 3 (Blackwell): $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\epsilon(\beta,f)$ with $\epsilon(\beta,f)\to0$ as $\beta\to1^-$, and the unique-solution characterizations of $x(f)$, $y(f)$ (already posed on the platform, referenced).
• Lemma 1 (Blackwell): $g\in E(f)\Rightarrow x(g)=x(f)$, and $y(g)=y(f)$ if moreover $Q^*(g)Q^*(f)=Q^*(g)$ (referenced).
• Theorem 1: for fixed $0\le\beta<1$, exactly one of "$f^\infty$ has no one-step improvement and is $\beta$-optimal" and "some $g$ gives $V_\beta(g,f^\infty)>V_\beta(f^\infty)$ and $V_\beta(g^\infty)>V_\beta(f^\infty)$".
• Theorem 4: $F''$ is the nonempty set of $f$ with $f^\infty$ 1-optimal.
• Theorem 5 and Corollary 1: $G(f)=\varnothing\Rightarrow f\in F'$; $g\in G(f)\Rightarrow V_\beta(g^\infty)>V_\beta(f^\infty)$ for $\beta$ near one, hence the lexicographic increase of $(x,y)$.
• Lemma 4: for $g\in E(f)$, $y(g)=y(f)+w(g)$, where $w(g)$ is the unique solution of $[I-Q(g)]w=0$, $Q^*(g)w=Q^*(g)(-y(f))$.
• (12): $z(f)$ is the unique solution of its system.
• Lemma 5: $G(f)=\varnothing$ and $y(f)\ge y(g)$ for all $g\in E(f)$ imply $f\in F''$.
• Two steps of the proof of Theorem 6: $H(f)=\varnothing\Rightarrow y(g)\le y(f)$ on $E(f)$; and $g\in H(f)\Rightarrow w(g)>w(f)=0$, or $w(g)=w(f)=0$ and $z(g)>z(f)$.

Significance

Theorem 6 turns Blackwell's existence result into an algorithm. Blackwell's characterization requires maximizing the bias over $F'$, a set with no explicit description; Lemma 5 shows that maximizing over the explicitly available set $E(f)$ suffices, and Lemma 4 shows that this maximization has the same form as the original gain maximization, so the familiar policy improvement machinery applies a second time. The same mechanism, iterated, gives the $n$-discount optimal policies of the later sensitivity theory and the lexicographic policy improvement algorithms in standard texts.

The results are proved in the paper (with a correction to the proof of Lemma 5 credited to Bruce Miller). They are not formalized in any proof assistant known to the mission. A complete development yields machine-checked policy improvement for average and bias optimality on top of the published Blackwell model, including the convergence-free closed forms of gain, bias and $z$ and the facts about the limit matrix $Q^*$ and the deviation matrix they rest on.

Difficulty

Parts 1 and 3 are Blackwell's policy improvement for the gain, transported to Veinott's set $G(f)$. The new content is in parts 2 and 4, and in both the obvious argument fails at the same place: the bias of $g\in E(f)$ cannot be compared with the bias of $f$ by a state-by-state test in the original problem, because $E(f)$ is a product of action sets $E(s,f)$ different from the original ones, and Blackwell's comparison works only after a reduction to a problem in which the reward is $-y(f)$ and the role of the gain is played by $w(g)$. A second difficulty is Lemma 5: $E(f)$ may be a proper subset of $F'$ (Example 3 of the paper), so maximizing the bias over $E(f)$ does not obviously maximize it over $F'$. The certificate does not follow from the gain and bias tests at $f$ alone, and the paper's original proof of it contained an error (corrected, as the paper records, by Bruce Miller).

Formalization scope

Everything is built on the published Blackwell definitions (BlackwellDiscreteDP.NearOne.Model, LimitMatrix, GainBias): one finite action type available in every state (Veinott's $A_s$ are all equal to it), decision rules St → Act, policies indexed from $0$ (π 0 is $f_1$), real vectors St → ℝ with the pointwise order, and VecGt for the paper's $>$ (not coordinatewise strict). $Q^*(f)$ is the published Cesàro limit $\lim (N+1)^{-1}\sum_{i=0}^N Q(f)^i$, the same limit as Veinott's $N^{-1}\sum_{i=0}^{N-1}$. The gain and bias are the published closed forms $x(f)=Q^*(f)r(f)$ and $y(f)=H(f)r(f)$ with the deviation matrix $H(f)$; the new vectors are closed forms too: $w(g)=Q^*(g)(-y(f))$ and $z(f)=H(f)(-y(f))$, and their characterizations by (10) and (12) are milestones. 1-optimality is the published IsNearlyOptimal, which compares against every policy. Veinott's set $H(f)$ is HSet, to keep it apart from the deviation matrix Hf.

$G(f)$ and $H(f)$ are defined literally from the paper's inequalities, including the clauses "at least one strict" and "$g(s)=f(s)$ where the tests are equalities". Dropping either clause makes parts 3 and 4 false (a $g$ that only reshuffles ties would count as an improvement); replacing $F''$ or $G(f)$ by a set defined through the conclusion of the theorem would make the goal trivial. Neither is acceptable.

The reduction "replace $A_s$ by $E(s,f)$ and $r(g)$ by $-y(f)$" is not instantiated, since the published model has a single action set; its two uses in the proof of Theorem 6 are milestones stated in the original model. A development of the general model with state-dependent action sets, and of the limit-matrix identities $Q^*Q=QQ^*=Q^*Q^*=Q^*$, $(I-Q)H=I-Q^*$, $Q^*H=0$, would be reusable well beyond this mission. Proofs of any milestone are welcome, as is a proof of the published Theorem 3 and Lemma 1, on which most of the mission rests.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• A. F. Veinott, Jr., On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, Ann. Math. Statist. 37(5):1284–1294, 1966. https://doi.org/10.1214/aoms/1177699272
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• A. F. Veinott, Jr., Discount Optimality and Sensitive Optimality, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A random walk on the integers in which the probability of stepping right depends on the current site is the simplest model of motion through a disordered medium: a particle diffusing in a crystal with impurities, a molecule moving along a heterogeneous polymer, or a gene frequency drifting under fluctuating selection. When the site-dependent probabilities are themselves drawn at random, the result is a random walk in a random environment (RWRE). Fred Solomon's 1975 paper [Solomon 1975] gave the first rigorous analysis of this model on $\mathbb Z$ with independent, identically distributed site probabilities, and its recurrence criterion opened the subject now surveyed in [Zeitouni 2004].

Timeline. Chung [Chung 1960, pp. 65–71] gave the hitting probabilities and the recurrence/transience criterion for a nearest-neighbour chain on $\mathbb Z$ with fixed, site-dependent transition probabilities. Fluctuation theory, as presented in Chung's A Course in Probability Theory [Chung 1968, Ch. 8], characterises when a sum of i.i.d. random variables drifts to $-\infty$, to $+\infty$, or oscillates, through the series $\sum\frac1nP(S_n>0)$ and $\sum\frac1nP(S_n<0)$. Solomon (1975) combined the two to classify the RWRE on $\mathbb Z$, and also computed its speed and exhibited sub-ballistic and non-Gaussian behaviour. Kesten, Kozlov and Spitzer (1975) [KKS 1975] identified stable limit laws in the transient sub-ballistic regime, and Sinai (1982) [Sinai 1982] found the $(\log n)^2$ scaling of the recurrent case.

Setting

Let $\alpha=(\alpha_n)_{n\in\mathbb Z}$ be independent, identically distributed random variables with values in $[0,1]$. Given a fixed sequence $a=(a_n)$ in $[0,1]$ (an environment), the chain $M_a$ on $\mathbb Z$ jumps from $n$ to $n+1$ with probability $a_n$ and to $n-1$ with probability $\beta_n=1-a_n$. The random walk in a random environment $(X_n)_{n\ge0}$ is the process obtained by first drawing $\alpha$ and then running $M_\alpha$ from $X_0=0$; jointly,

$$P(\alpha\in A,\ X_0=x_0,\dots,X_n=x_n)=\int_{\{\alpha\in A\}}\mathbf 1\{x_0=0\}\prod_{k<n}M_\alpha(x_k,x_{k+1})\,dP .$$

The walk is a Markov chain given the environment, but not after averaging over it. Define

$$\sigma_n=\frac{\beta_n}{\alpha_n}\in[0,\infty],\qquad \rho_n=\sigma_1\cdots\sigma_n\ (n\ge1),\qquad \rho_{-n}=\sigma_{-1}\cdots\sigma_{-n}\ (n\ge1),$$

and, for a fixed environment, the hitting probability $f_{ij}=P(X_n=j\text{ for some }n>0\mid X_0=i)$. The quantity $E(\ln\sigma)$ is defined when the expectation of the positive or of the negative part of $\ln\sigma\in[-\infty,\infty]$ is finite.

Formalization targets

Goal: Theorem (1.7)

Assume $\alpha_0$ is not almost surely constant and either $0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$. Then

$$\sum_{n\ge1}\tfrac1nP(\rho_n>1)<\infty\Rightarrow X_n\to+\infty,\qquad \sum_{n\ge1}\tfrac1nP(\rho_n<1)<\infty\Rightarrow X_n\to-\infty,$$

and if both series diverge, $-\infty=\liminf X_n<\limsup X_n=+\infty$, all almost surely. When $E(\ln\sigma)$ is defined, the three cases are exactly $E(\ln\sigma)<0$, $>0$, $=0$.

Milestones

Theorem (0.1): almost-sure properties of the walk in almost every fixed environment transfer to the RWRE. Lemma (1.1)(i)–(ii): the hitting probabilities $f_{ij}$ in a fixed environment with $0<a_n<1$, as ratios of series in $\sigma$. Lemma (1.5): in a fixed environment, $\sum(\rho_{-n})^{-1}$ and $\sum\rho_n$ decide transience to $+\infty$, to $-\infty$, or recurrence. Lemma (1.6): fluctuation theory for i.i.d. sums, including the summability of $e^{S_n}$. Two claims from the proof of (1.7) (p. 5): the boundary cases where $\alpha_n$ equals $1$ or $0$ with positive probability, and the equivalence $E(\ln\sigma)<0\iff S_n\to-\infty\iff\sum\frac1nP(\rho_n>1)<\infty$ for $S_n=\ln\sigma_1+\dots+\ln\sigma_n$. A companion item asserts that the RWRE exists for every law of $\alpha_0$ on $[0,1]$.

Significance

The theorem classifies the long-run behaviour of the RWRE on $\mathbb Z$ by a condition on the law of a single site variable, with no moment assumption. It shows that the averaged drift $E\alpha_0-E\beta_0$ is not the right quantity: a walk can be recurrent or transient to the left while its average step is positive, because the criterion involves $E\ln\sigma$, a geometric rather than arithmetic mean. The criterion is the starting point for the speed law (Theorem (1.16) of the same paper), for the limit laws of Kesten–Kozlov–Spitzer and Sinai, and for the large-deviation theory of RWRE.

Solomon's results are proved; none of them, nor the fixed-environment criterion of Chung, is formalized in Lean. This mission produces machine-checked statements of the full trichotomy including the boundary cases $\sigma\in\{0,\infty\}$, of the classical hitting-probability formulas for birth–death chains on $\mathbb Z$, and of the fluctuation-theory criterion with infinite-valued expectations allowed.

Difficulty

The naive approach applies the law of large numbers to $X_n$; it fails because the increments $X_{j}-X_{j-1}$ are neither independent nor stationary once the environment is averaged out. The argument must instead pass through a fixed environment, where the criterion of Lemma (1.5) involves the full random series $\sum\rho_n$ and $\sum\rho_{-n}^{-1}$, and then decide when these series converge almost surely. That step requires fluctuation theory for $\ln\rho_n=\sum_{k\le n}\ln\sigma_k$, a random walk whose steps may be infinite and may have no mean. In Lean, the main missing infrastructure is the fluctuation-theory criterion $\sum\frac1nP(S_n>0)<\infty\iff S_n\to-\infty$, which Mathlib does not have, and the transfer from quenched to annealed statements for a process defined only through its cylinder laws.

Formalization scope

Everything lives in the namespace SolomonRWRE.Recurrence. The fixed-environment chain is IsChainInEnv P a i X, specified by its cylinder probabilities. The RWRE is IsRWRE P α X on an arbitrary probability space: measurable $\alpha_n$ with values in $[0,1]$ at every outcome, iIndepFun α P, identically distributed, and the joint cylinder law above. $\sigma_n$, $\rho_n$, $f_{ij}$ and all series are in $[0,\infty]$ (ℝ≥0∞), so "$<\infty$" and "$=\infty$" are literal; series over $n\ge1$ are indexed by $n+1$ in Lean. $\ln\sigma$ and $S_n$ are extended reals, $E(\ln\sigma)$ is the difference of two lower Lebesgue integrals, and "defined" means one of them is finite. Recurrence is always stated in the paper's "in fact" form: $\liminf X_n=-\infty$ and $\limsup X_n=+\infty$. "Correspond respectively" is formalized as three equivalences between the series conditions and the sign conditions.

Two trivializing formalizations are ruled out. Without nondegeneracy ($\alpha\equiv\frac12$) both series vanish and (i), (ii) would contradict each other; the hypothesis is part of every statement that needs it. A cylinder law that cannot be met would make every theorem vacuous; a sorry-free check confirms that the environment $\alpha\equiv1$ with $X_n=n$ satisfies IsRWRE, and the companion item asserts existence for every law of $\alpha_0$. The page's alternative "$0\le\alpha_n<1$ for all $n$ or $0<\alpha_n\le1$ for all $n$" is kept, since a single range $[0,1]$ would let $0\cdot\infty=0$ change $\rho_n$.

Needed infrastructure: hitting probabilities of birth–death chains (reusable for any nearest-neighbour chain), the fluctuation-theory criterion for i.i.d. sums with extended values (reusable throughout applied probability), and a quenched-to-annealed transfer lemma. Contributions to any of these are welcome.

Selected references

• F. Solomon, Random walks in a random environment, The Annals of Probability 3(1):1–31, 1975. https://doi.org/10.1214/aop/1176996444
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, Berlin, 1960 (pp. 65–71; reference [1] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
• K. L. Chung, A Course in Probability Theory, Harcourt, Brace and World, New York, 1968 (Ch. 8; reference [2] of Solomon 1975, https://doi.org/10.1214/aop/1176996444).
• H. Kesten, M. V. Kozlov, F. Spitzer, A limit law for random walk in a random environment, Compositio Mathematica 30(2):145–168, 1975. http://www.numdam.org/item/CM_1975__30_2_145_0/
• Ya. G. Sinai, The limiting behavior of a one-dimensional random walk in a random medium, Theory of Probability and its Applications 27(2):256–268, 1982. https://doi.org/10.1137/1127028
• O. Zeitouni, Random walks in random environment, Lectures on Probability Theory and Statistics (Saint-Flour 2001), Lecture Notes in Mathematics 1837, Springer, 2004. https://doi.org/10.1007/978-3-540-39874-5_2

Motivation

Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.

Timeline of the LP approach to average-cost problems:

• 1960 — Manne: the inventory model as a linear program in the joint probabilities of (stock level, production quantity); mixed strategies allowed; the decision rule is read off as a conditional probability.
• 1960 — H. M. Wagner, in a companion note in the same issue, shows that an optimal solution consisting of pure strategies exists.
• 1962 — C. Derman (Management Science 9(1), 1962) gives the general finite-state, finite-action version, assuming every stationary randomized rule yields an irreducible chain.
• 1960 — F. d'Epenoux (Revue Française de Recherche Opérationnelle 4, No. 14; English translation 1963) treats the discounted criterion by linear programming, as Manne's closing note records.

Setting

A positive integer $T$ bounds inventory accumulation; the stock levels are $0,1,\dots,T$. At the start of a month the initial stock $i$ is observed and a production quantity $j$ is chosen; the available stock is $k=i+j$. The month's demand $n\in\{0,1,2,\dots\}$ is independent of everything else and has law $p_n$. Backlogs are excluded, so the terminal stock is $t=\max(0,k-n)$, which becomes the next initial stock. A finite set $A$ of admissible pairs $(i,j)$, all with $i+j\le T$ and containing $(i,0)$ for every $i\le T$, lists the decisions available at each stock level. Costs are three arbitrary real functions: $C_1(i)$ of the initial stock, $C_2(j)$ of the production quantity, and $C_3(n-k)$ of the shortage level.

A stationary randomized decision rule $q(j\mid i)$ is a conditional probability of producing $j$ at stock $i$, supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of $q$ is a stationary distribution $y=(y_0,\dots,y_T)$ of that chain: the law $y'$ of the terminal stock equals the law $y$ of the initial stock, (2). The expected monthly cost (1) of $q$ in the equilibrium $y$ is

$$\mathcal EC_1(i)+\mathcal EC_2(j)+\mathcal EC_3(n-k),$$

the expectation taken under the joint law $y_i\,q(j\mid i)\,p_n$ of (initial stock, production, demand).

The linear program has one unknown $x_{ij}$ per admissible pair, the joint probability of (initial stock $i$, production $j$). Its constraints are $x_{ij}\ge0$, (4) $\sum_{i,j}x_{ij}=1$, and the equilibrium equations

$$\text{(8.t)}\qquad \sum_j x_{tj}=\sum_{\substack{i,j,n:\\ i+j-n=t}}p_nx_{ij}\qquad(t=1,\dots,T),$$

and its objective (9) is $\sum_{i,j}c_{ij}x_{ij}$ with the cost coefficients (10)

$$c_{ij}=C_1(i)+C_2(j)+\sum_np_nC_3(n-i-j).$$

The companion equation (8.0) for $t=0$ has right-hand side $\sum_{i+j-n\le0}p_nx_{ij}$ and is omitted from the constraints. A feasible $x$ is decoded into $y_i=\sum_jx_{ij}$ and $q(j\mid i)=x_{ij}/y_i$.

Formalization targets

The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.

Goal: an LP optimum gives an optimal stationary rule

Assume $\sum_np_n|C_3(n-i-j)|<\infty$ for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution $x^*$, with decoding $(q^*,y^*)$, $q^*$ is a stationary randomized rule, $y^*$ is a statistical equilibrium of $q^*$, and

$$\mathrm{Cost}(q^*,y^*)=\sum_{i,j}c_{ij}x^*_{ij}\le \mathrm{Cost}(q,y)$$

for every stationary randomized rule $q$ and every statistical equilibrium $y$ of $q$.

Milestones

1. (7): under a rule in a distribution $y$, the law of the terminal stock is the right-hand side of (7)/(8) evaluated at $x_{ij}=y_iq(j\mid i)$.
2. (8.0)–(8.T): a rule in statistical equilibrium yields a point satisfying $x\ge0$, (4) and all of (8.0)–(8.T).
3. (8.0) is redundant: (4) and (8.1)–(8.T) imply (8.0).
4. §3, N.B.: every feasible $x$ equals $y_iq(j\mid i)$ for its decoding $(q,y)$, with $y$ an equilibrium of $q$.
5. (10): the expected monthly cost (1) under the joint law $x_{ij}p_n$ equals $\sum c_{ij}x_{ij}$.
6. Table 1: the cost coefficients of the §6 example ($T=3$, $p=(2/3,0,1/3)$, $C_1(i)=i$, $C_2(j)=3j$, $C_3(m)=\max[0,6m]$, $j\in\{0,1\}$) are $4,5,3,4,2,5,3$.
7. Table 2, footnote 3: $x_{01}=1/3$, $x_{11}=2/9$, $x_{20}=4/9$ is optimal with cost $31/9$; the do-nothing solution costs $4$.
8. Footnote 5: the implicit prices $-7/3,-13/3,-11/3$ of (8.1)–(8.3), with $31/9$ on (4), are an optimal dual solution.

Significance

The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.

The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient $x_{ij}/\sum_jx_{ij}$ is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.

Difficulty

Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over $(i,j,n)$ with conditions $i+j-n\le0$ and $i+j-n=t$, and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and $\sum_np_n=1$. The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level $0$ must be recovered from (4) and the bound $i+j\le T$. And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.

Formalization scope

All statements live in the namespace ManneLP.Equilibrium. Conventions:

• Stock levels and production quantities are natural numbers; a model carries $T>0$, the admissible set $A$ (a Finset (ℕ × ℕ) with $i+j\le T$ and every $(i,0)\in A$), a demand law $p:\mathbb N\to\mathbb R$ with $p_n\ge0$ and HasSum p 1, and costs $C_1,C_2:\mathbb N\to\mathbb R$, $C_3:\mathbb Z\to\mathbb R$. The shortage level $n-i-j$ is an integer; no convexity, sign or monotonicity of the costs is assumed.
• The admissible set is a parameter: §6 imposes a capacity limit $j\le1$. Reading of the page: $i+j\le T$ is how §2's requirement $\max(0,k-n)\le T$ holds whatever the demand; $(i,0)\in A$ (producing nothing is possible) is implicit in §2.
• The terminal stock is computed by truncated subtraction in $\mathbb N$, which equals $\max(0,k-n)$. Sums over demands are tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.
• A statistical equilibrium is a stationary distribution of the chain of the rule, defined from the transition probabilities, not from (8). The expected monthly cost is defined from the joint law of (stock, production, demand), not as $\sum c_{ij}x_{ij}$. The LP constraint set omits (8.0), exactly as the page does.
• The decoded rule uses the default action $j=0$ at stock levels with $\sum_jx_{ij}=0$; any admissible default would do.
• Table 2's $x_{30}=\varepsilon$ is the paper's device against degeneracy; the example's solution has $x_{30}=0$. Footnote 5 prints no price for (4); $31/9$ is the price forced by equal objectives, and the dual optimum is not claimed unique.

Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as $\sum c_{ij}x_{ij}$ (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.

Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.

Selected references

• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963 (translation of the 1960 French paper). https://doi.org/10.1287/mnsc.10.1.98

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