Markov Chain

Motivation

A finite Markov chain describes a system that changes state according to fixed transition probabilities. For a chain that settles toward an equilibrium distribution, a central question is how quickly the effect of its starting state disappears. The logarithmic Sobolev constant supplies quantitative control of this convergence and, through hypercontractive estimates, also governs how the continuous-time transition operator changes the size of functions measured in different norms. Diaconis and Saloff-Coste's 1996 paper develops these relations for finite chains and uses them to study mixing on graphs and product spaces.

The constant can be hard to calculate directly. Its definition is an infimum over all nonconstant functions, while a particular Markov semigroup may admit an accessible bound from $\ell^2$ to $\ell^q$ at one time. Theorem 3.9 turns such an operator estimate into a numerical lower bound for the log-Sobolev constant. This mission formalizes that result, including both finite $q$ and the supremum-norm endpoint.

Setting

Let $\mathcal X$ be a finite state space. A Markov kernel $K(x,y)$ is nonnegative, with $\sum_yK(x,y)=1$ for every $x$. A strictly positive stationary distribution $\pi$ satisfies $\sum_x\pi(x)K(x,y)=\pi(y)$ and $\sum_x\pi(x)=1$. The chain is reversible when $\pi(x)K(x,y)=\pi(y)K(y,x)$ for every pair of states. Its continuous-time heat semigroup is $H_t=e^{-t(I-K)}$, acting on a function $f$ by $H_tf$. These conventions follow §§2.1–2.3 of the source paper.

For a real function on $\mathcal X$, write $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$ when $p$ is finite, and $\|f\|_\infty=\max_x|f(x)|$. The Dirichlet form is $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$. The quadratic entropy functional is $\mathcal L(f)=\sum_x|f(x)|^2\log(|f(x)|^2/\|f\|_2^2)\pi(x)$, with a zero contribution where $f(x)=0$. Write $Ef=\sum_xf(x)\pi(x)$ and $\operatorname{Var}_\pi(f)=\|f-Ef\|_2^2$.

The spectral gap in this mission is the variational constant $\lambda=\inf_{\operatorname{Var}_\pi(f)\ne0}\mathcal E(f,f)/\operatorname{Var}_\pi(f)$, as in (2.4). The log-Sobolev constant is $\alpha=\inf_{\mathcal L(f)\ne0}\mathcal E(f,f)/\mathcal L(f)$, as in (3.1). These definitions specify the quantities that Theorem 3.9 relates; in particular, $\lambda$ is the paper's variational quantity, rather than an eigenvalue expression imported from a different convention.

Formalization targets

Theorem 3.9: a single heat-operator estimate bounds $\alpha$

Suppose $2<q<\infty$, $t_q>0$, and $M_q$ satisfy $\|H_{t_q}f\|_q\le M_q\|f\|_2$ for every function $f$. The paper's theorem asserts

$$\alpha\ge\frac{(1-2/q)\lambda}{2\left(\lambda t_q+\log M_q+(q-2)/q\right)}.$$

It also covers $q=\infty$: the hypothesis then uses $\|H_{t_q}f\|_\infty$, and the two fractions involving $q$ in the displayed bound become $1$.

Companion results

Theorem 3.10 replaces $H_{t_q}$ in the norm hypothesis with $H_{t_q}-E$, where $E$ sends a function to its constant mean. Corollary 3.11 relates $\alpha$ to $\tau$, the first time at which every heat-kernel density $h_t^x(y)=H_t(x,y)/\pi(y)$ is within $1/e$ of $1$ in $\ell^2(\pi)$:

$$\frac1{2\alpha}\le\tau\le\frac{4+\log\log(1/\pi_*)}{4\alpha}, \qquad \pi_*=\min_x\pi(x).$$

The three milestones reproduce the interpolation estimate (3.6), the resulting entropy inequality, and the centering inequality (3.7). Theorem 3.10's printed finite-$q$ denominator contains $(q-2)/2$; its displayed proof and the $q=\infty$ use in Corollary 3.11 require $(q-2)/q$. That proof also needs $\log M_q+(q-2)/q\ge0$, which the page does not state and without which the printed statement fails on a four-state product chain. The formal companion records both corrections, while the main goal follows the printed Theorem 3.9 exactly.

Significance

Theorem 3.9 makes a norm bound at a chosen time useful beyond that time: it yields a bound on a functional inequality that holds for every function on the state space. Thus estimates obtained from an explicit heat kernel or another analytic method can be compared across chains using the same constant $\alpha$. The centered version and the bound for $\tau$ connect this functional viewpoint back to convergence from a point mass, as the paper explains in §3.4.

The mathematical results are proved in the 1996 paper. Here the remaining work is to give their finite-state objects, norm hypotheses, and constants machine-checked meanings, then formalize the proofs. The definition layer and the centering inequality have use beyond this mission: they can support other statements about entropy decay and heat-kernel convergence in the same paper.

Difficulty

A bound for $H_t$ in the same norm is too weak to recover the displayed lower bound: the information here is the change from an $\ell^2$ input to an $\ell^q$ output. The dependence of the exponent on time must retain the factors $(1-2/q)$ and $(q-2)/q$ exactly. The endpoint $q=\infty$ also requires a separate norm statement, since a real exponent cannot represent infinity. The centering inequality (3.7) is another substantial step; the paper points to earlier proofs rather than treating it as immediate.

Formalization scope

The state space is a finite Lean type, the kernel a real matrix, and the invariant law a positive real-valued probability vector. Reversibility is detailed balance, and irreducibility is retained from the standing setting of §3.1. The heat semigroup uses the already published Poissonized heat kernel. Operator norms are represented by inequalities quantified over every real function. The finite-$q$ and $q=\infty$ conclusions are separate clauses of the goal. Time is real; $t_q>0$ makes explicit the positive-time convention used in §3.4. Theorem 3.10 carries the condition $M_q\ge e^{-(q-2)/q}$ (and $M_\infty\ge e^{-1}$) described above; Corollary 3.11 is stated without any extra condition.

The variational constants are real infima, the logarithms and real powers use Lean's total operations, and the supremum norm is a supremum over the finite state space. The stationary probability hypothesis rules out an empty state space; the operator hypothesis on the constant function forces $M_q\ge1$ in Theorem 3.9. These facts prevent the bound from arising from a zero norm, an empty operator test, an invalid logarithm, or an eigenvalue convention different from (2.4). Useful contributions include finite-state entropy inequalities, interpolation machinery, estimates for the heat operator, and proofs of the three stated milestones.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Annals of Applied Probability 6 (1996), 695–750. DOI.

Motivation

In a wireless multihop network, a switch, or a parallel computer, transmissions interfere: two links that share a receiver, or two crossbar paths that share a port, cannot be active in the same time slot. The scheduler must choose, slot by slot, a set of links that may operate together and decide which traffic each one carries. The basic question is which arrival rates a network can sustain at all, and whether a single scheduling rule sustains every one of them without knowing the rates.

Tassiulas and Ephremides answered both questions in 1992 for a general slotted model with interference constraints, multihop routing and several traffic classes (IEEE Trans. Automat. Control 37(12):1936–1948). Their policy, here called $\pi_0$, weighs each link by the largest queue-length difference it can reduce and activates a maximum-weight feasible set. It is the origin of the max-weight and back-pressure scheduling rules that later became standard in switch scheduling (McKeown, Mekkittikul, Anantharam and Walrand, 1999) and in stochastic network optimization (Georgiadis, Neely and Tassiulas, 2006).

Setting

A constrained queueing network has $L$ nodes, $N$ servers (links) and $J$ customer classes. Server $i$ moves customers from its origin node $q(i)$ to its destination node $h(i)$. Class $j$ leaves the network on reaching a node of its destination set $V_j$; at every other node $l$ it has a queue $(l,j)$, whose length at the end of slot $t$ is $X_{lj}(t)\in\mathbb N$.

The constraint set $S$ is the family of sets of servers that may be active in the same slot. Assumption C.1 says that every subset of an activation set is an activation set. In each slot a stationary policy, given the state $x=X(t-1)$, chooses a set of servers in $S$ and the class each active server serves; an activation rule never activates more servers of queue $(l,j)$ than there are customers $x_{lj}$. The class of all such rules is $H$. An activated server $i$ completes its service with probability $m_i$, independently. New arrivals $A_{lj}(t)$ are i.i.d. over slots, independent across queues and of the services, with finite second moments and means $a_{lj}$. Under a stationary rule the vector $X(t)$ is a Markov chain on $\mathbb N^{\{\text{queues}\}}$.

The chain is stable (Definition 3.1) if, from every transient state, it enters a closed communicating class with probability one, and every state of a closed communicating class is positive recurrent. The stability region $C_\pi$ of a policy is the set of rate vectors $a$ for which the system is stable under $\pi$; the stability region of the system is $C=\bigcup_{\pi\in H}C_\pi$.

A family $f=(f_{ij})\ge0$ is an $a$-admissible flow if it satisfies flow conservation, $a_{lj}=\sum_{q(i)=l}f_{ij}-\sum_{h(i)=l}f_{ij}$ at every queue; $\hat f_i=\sum_jf_{ij}$ is its total flow through server $i$. With $\mathrm{co}(S)$ the convex hull of the indicator vectors of the activation sets,

$$C'=\{a\ge0:\ \exists f\in F_a,\ c\in\mathrm{co}(S),\ m_i^{-1}\hat f_i<c_i\text{ if }\hat f_i>0,\ \hat f_i=0\text{ if }c_i=0\}.$$

Formalization targets

Goal: Theorem 3.2

$$C'\subset C\subset\bar C',\qquad C'\subset C_{\pi_0}\subset C\subset\bar C_{\pi_0}.$$

The system stability region is pinned between $C'$ and its closure, and policy $\pi_0$, whatever its tie-breaking, stabilizes every rate vector in $C'$. Inclusions are not strict.

Milestones

1. Lemma A.1: $\mathrm{co}(S)$ is closed under $0\le a\le c$ (under C.1).
2. Lemma 3.1: $\bar C'=\{a:\exists f\in F_a,\ c\in\mathrm{co}(S),\ M^{-1}\hat f\le c\}$.
3. Theorem 3.1: a function bounded below with drift $\le-\epsilon$ outside a finite set, and finite conditional expectation on it, makes a countable chain stable in the sense of Definition 3.1.
4. (A.6)–(A.7): for $V(x)=\sum_{l,j}x_{lj}^2$, the one-step drift under $\pi_0$ is finite everywhere and below $-\epsilon$ once $V(x)\ge b$.
5. Lemma 3.2: $C'\subset C_{\pi_0}$.
6. Lemma 3.3: for $a\notin\bar C'$, the system is unstable under every policy in $H$.

An optional item states the claim of Remark 1: if $a\in\bar C'\setminus C'$, then $\delta a\notin\bar C'$ for every $\delta>1$.

Significance

Theorem 3.2 shows that a throughput-optimal stationary policy exists, which is not obvious: stability regions of different policies need not be nested, so a policy whose region contains all the others has to be exhibited. It also describes the system stability region by a deterministic flow condition, $C'$, which can be checked without simulating any policy. The same drift argument underlies the stability proofs of max-weight switch schedulers, back-pressure routing and the drift-plus-penalty method.

The result is proved in the paper, with a proof sketched in places (Theorem 3.1 is called "a trivial extension of Foster's criteria", Lemma A.1 is omitted, Lemma 3.3 is argued by ergodicity in a paragraph). As far as a search of the platform shows, none of these statements has a machine-checked proof: Foster's criterion is posed on the platform only for irreducible chains on $\mathbb N$, and the back-pressure results already posed concern fluid models of other networks. A complete formal development would supply the reducible-chain Foster criterion, the convex-geometry lemma on $\mathrm{co}(S)$, the quadratic drift computation and the ergodic converse.

Difficulty

The obvious argument is a quadratic Lyapunov drift bound, but it does not go through as is in three places. First, the drift bound needs a direction of decrease from every large state: the largest queue must be connected to a destination through servers that can actually be activated, which is where assumption C.2 and the topology of $S$ enter (A.21)–(A.24). Second, stage 3 of $\pi_0$ defers some activations to respect the rule "no service for nonexisting customers", so the chosen schedule is not exactly maximum-weight and the loss has to be bounded uniformly. Third, the chain is in general reducible, so Foster's criterion for irreducible chains does not apply; the extension must show that every closed class meets the finite exceptional set and that transient states are left almost surely. The converse, Lemma 3.3, needs a law-of-large-numbers argument for an arbitrary stationary rule on a positive recurrent class, together with compactness of acyclic flows (Lemma 3.1).

Formalization scope

Nodes, servers and classes are Fin L, Fin N, Fin J (0-based). $S$ is a Set (Finset (Fin N)); a queue is a pair $(l,j)$ with $l\notin V_j$, and a state is a function from queues to $\mathbb N$. A multiclass activation vector assigns to each server an optional class. The transition matrix of the queue-length chain is written out explicitly as a sum over arrival vectors and Bernoulli service outcomes; Definition 3.1 is stated through this matrix (first-entry probabilities, essential states, positive recurrence), with values in $[0,\infty]$.

Conventions committed to, and hypotheses added relative to the page:

• Standing assumptions of the goal: C.1; $\emptyset\in S$ (the idle schedule is always allowed); $0<m_i\le1$; and C.2 in a topological form, a chain of servers from every non-destination node of class $j$ to $V_j$ (stronger than the printed sentence, which covers only nodes that class $j$ can reach).
• Every single server is an activation set, $\{i\}\in S$. The proof of Lemma 3.2 uses this at (A.24) without stating it; without it a server that can never be activated breaks the drift bound and Lemma 3.2.
• Stability regions quantify over laws. $C_\pi$ is the set of nonnegative rate vectors for which the chain is stable for every arrival law with finite second moments and those means. $C'$ is intersected with $a\ge0$.
• $\pi_0$ is a family. Statements hold for every rule satisfying the three stages, with arbitrary tie-breaking.
• Expectations of unbounded functions are real series with explicit summability, so a divergent expectation is never read as $0$.

A formalization in which $C_\pi$ asks for stability under one convenient arrival law, or in which negative rates are admitted, or in which $\pi_0$ is one fixed tie-break, would be a different theorem; the definitions rule each of these out.

Infrastructure needed: hitting probabilities and positive recurrence for countable chains (reusable beyond this mission), convex hulls of finite point sets, a cycle-cancelling bound for multicommodity flows, and the ergodic theorem for positive recurrent chains. Proofs of any milestone, and reusable lemmas on countable Markov chains, are welcome.

Selected references

• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Trans. Automat. Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24(3):355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• N. McKeown, A. Mekkittikul, V. Anantharam and J. Walrand, Achieving 100% throughput in an input-queued switch, IEEE Trans. Commun. 47(8):1260–1267, 1999. https://doi.org/10.1109/26.780463
• L. Georgiadis, M. J. Neely and L. Tassiulas, Resource allocation and cross-layer control in wireless networks, Found. Trends Netw. 1(1):1–144, 2006. https://doi.org/10.1561/1300000001

Why the walk slows down

A random walk in a random environment uses transition probabilities selected once for each site, rather than probabilities resampled at every step. Even when the site environments are independent and identically distributed, the walker revisits the same local bias whenever it returns to a site. Its long-time motion can therefore differ sharply from that of a walk with a single averaged right-step probability. Solomon’s 1975 paper established the recurrence and speed classification for this one-dimensional model and then examined a two-value example in which some sites are one-way mirrors: the walker can pass through them to the right but cannot cross them to the left. The example isolates how a sequence of random intervals between mirrors produces slow growth and phase-dependent limit laws Solomon 1975, §2.

The present mission concerns §2 of that paper, pp. 10–20. Its central question is how far the walker has traveled after $n$ steps when the mean crossing time reaches or exceeds the critical threshold. At criticality, a logarithmic correction replaces ordinary linear speed. Above criticality, the paper gives limits along subsequences whose logarithmic fractional parts approach a fixed phase.

The walk and its mirror environment

Let $(\Omega,\mathcal F,P)$ be a probability space and let $\alpha_j$, $j\in\mathbb Z$, be independent, identically distributed random variables in $[0,1]$. The environment is the complete sequence $\alpha=(\alpha_j)_{j\in\mathbb Z}$. Conditional on a fixed environment, a nearest-neighbour walk starts at $X_0=0$ and, from site $j$, moves to $j+1$ with probability $\alpha_j$ and to $j-1$ with probability $1-\alpha_j$. The annealed probability $P$ averages the conditional path law over the environment. In Lean this joint law is specified on every finite path cylinder together with every measurable event of the whole environment, so it determines the dependence between $X$ and $\alpha$.

Fix $\theta>1$ and $0<\gamma<1$. Solomon’s example has $\alpha_j=1$ with probability $1-\gamma$ and $\alpha_j=(1+\theta)^{-1}$ with probability $\gamma$. Equivalently, the left-to-right odds ratio $\sigma_j=(1-\alpha_j)/\alpha_j$ takes values $0$ and $\theta$. A site with $\sigma_j=0$ is a one-way mirror. Write $V_0=0$ and let $V_n$ be the position of the $n$th mirror strictly to the right of zero. Let $T_j$ be the first time the walk reaches site $j$, with $T_j=\infty$ if it never does. For $b>0$, $\log_b x$ means the logarithm in base $b$, and $\{x\}=x-\lfloor x\rfloor$ is the fractional part.

The parameters used below are

$$\nu=\frac{2\theta}{(\theta-1)^2},\qquad K=\frac{1-\gamma}{\gamma}\nu,\qquad \rho=\log_{1/\gamma}\theta.$$

When $\gamma\theta>1$, the paper specifies a probability law $F_\varepsilon$ on $[0,\infty)$ by its Laplace transform

$$\int_0^\infty e^{-ux}\,dF_\varepsilon(x)=\exp\left[-Ku\sum_{j\in\mathbb Z}\frac{(\gamma\theta)^{j-\varepsilon}}{1+\nu u\theta^{j-\varepsilon}}\right],\qquad u>0.$$

Here $F_\varepsilon(t)$ also denotes that law’s distribution function at $t$. The bilateral series converges in the supercritical parameter range. The source’s notation uses the same letter for a distribution and its distribution function; the Lean development keeps these roles separate as a measure and its value on $(-\infty,t]$.

Formalization targets

The first clause of Theorem (2.20) is the critical growth law. If $\gamma\theta=1$, then

$$\frac{X_n}{n/\log_\theta n}\xrightarrow{P}\frac12.$$

The second clause describes the supercritical case. If $\gamma\theta>1$, $n_k\to\infty$, and $\{\log_\theta n_k\}\to\varepsilon$, then for each $x>0$,

$$P\!\left(n_k^{-1/\rho}X_{n_k}<x\right)\longrightarrow 1-F_{\lambda(x)}\!\left(((1-\gamma)x)^{-\rho}\right), \qquad \lambda(x)=\varepsilon+\log_{1/\gamma}((1-\gamma)x).$$

Both clauses are the goal. The milestones record the transform identity of Lemma (2.5), its approximation and scaling limits in Lemmas (2.6)–(2.7), the mirror passage-time limits of Lemma (2.10), and the ordinary passage-time limits of Theorem (2.18). The fractional part in the goal uses base $\theta$; the two passage-time results use base $1/\gamma$, exactly as printed Solomon 1975, pp. 12–19.

What the result gives

The critical law identifies the constant in the growth scale $n/\log_\theta n$. The supercritical law shows that a single power normalization $n^{1/\rho}$ does not erase the logarithmic phase of the environment: the limiting distribution depends on the phase approached by the chosen subsequence. These assertions describe the position $X_n$ itself, rather than only the time needed to reach a distant site. They complement the paper’s general speed theorem by resolving the zero-speed behavior in a concrete model Solomon 1975, Theorems (1.16) and (2.20).

The results are proved in the 1975 paper; the open work here is machine checking their definitions, statements, and proofs. The development also yields reusable interfaces for a nearest-neighbour chain specified by cylinder probabilities, first-passage times that can be infinite, and Laplace-transform arguments for random time changes. The mission’s statements currently compile locally with proof placeholders, so they are formalization targets rather than machine-checked theorems.

Where the difficulty lies

The one-way mirrors create independent, identically distributed blocks of crossing times, but those times have tails governed by the random spacing between mirrors. At $\gamma\theta=1$, their accumulation produces a logarithmic correction; at $\gamma\theta>1$, the underlying geometric scales preserve the fractional part of a logarithm. An ordinary law of large numbers for passage times therefore cannot supply both limits. Moreover, a limit for passage times to the random mirror positions $V_n$ does not immediately give a limit for passage times to deterministic sites, and converting a passage-time limit into a position limit requires control of the inverse time change. The source separates these tasks across the milestone results Solomon 1975, pp. 11–20.

Formalization scope

The Lean environment is the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The position and environment are integer-indexed; time is natural-number-indexed. The one-way-mirror parameter range is $\theta>1$, $0<\gamma<1$, $\gamma\theta\ge1$. The strict bounds on $\gamma$ make both atom probabilities meaningful and the logarithm base $1/\gamma$ valid. The source uses these bounds implicitly. All probabilities concern the annealed joint law, not an arbitrary process with the same one-time marginals.

First-passage times are extended natural numbers, with infinity on paths that never hit the target. The real-valued limits convert finite passage times to real numbers; under the stated model, infinite passage times form a null event. The location of a nonexistent next mirror is assigned zero for a total Lean function, again only on a null event in this model. The Laplace transform of an infinite passage time is defined as zero. Convergence in probability uses TendstoInMeasure; convergence in law is expressed by convergence of distribution functions at continuity points. The limit-law family is constrained to probability measures supported on $[0,\infty)$ with the exact transform (2.12), preventing a degenerate or unrelated choice of $F$.

A complete proof needs measurable cylinder laws, independence of the mirror gaps, hitting-time and transform calculations, asymptotics of one-sided and bilateral series, distributional convergence from Laplace transforms, and inversion from passage time to position. Work on any of these components is in scope. The statement keeps both source regimes and every constant; replacing the joint walk law by independent marginals or choosing an arbitrary limit distribution would change the theorem.

Selected references

• Fred Solomon, Random Walks in a Random Environment, The Annals of Probability 3(1):1–31, 1975. DOI: 10.1214/aop/1176996444.

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