All missions

Motivation

Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.

Timeline.

• 1989: Watkins' thesis introduces Q-learning and sketches a convergence argument.
• 1992: Watkins and Dayan publish the proof via the action-replay process, for bounded rewards, discount $0<\gamma<1$ and learning rates satisfying condition (3) at every state–action pair.
• 1994: Jaakkola, Jordan and Singh (Neural Computation 6) and Tsitsiklis (Machine Learning 16) give proofs through stochastic approximation for asynchronous iterations, with predictable random choices of state, action and step.
• Later work (Szepesvári 1997; Even-Dar and Mansour 2003) quantifies the convergence rate.

Setting

A finite controlled Markov process has a finite state set $X$, a finite nonempty action set $\mathfrak A$ (the same in every state), mean rewards $\mathcal R_x(a)$ and transition probabilities $P_{xy}[a]$. Rewards received $s$ steps later are discounted by $\gamma^s$ with $0<\gamma<1$. The optimal action-value function $Q^*$ is the unique solution of the Bellman optimality equation

$$Q^*(x,a)=\mathcal R_x(a)+\gamma\sum_y P_{xy}[a]\max_b Q^*(y,b).$$

In the $n$-th episode the agent observes a state $x_n$, performs an action $a_n$, observes the next state $y_n$ and a reward $r_n$ of mean $\mathcal R_{x_n}(a_n)$, and updates its table with a learning rate $\alpha_n$:

$$Q_n(x,a)=\begin{cases}(1-\alpha_n)Q_{n-1}(x,a)+\alpha_n\bigl[r_n+\gamma\max_b Q_{n-1}(y_n,b)\bigr]&(x,a)=(x_n,a_n),\\ Q_{n-1}(x,a)&\text{otherwise,}\end{cases}$$

from given initial values $Q_0$. Episodes need not form a single trajectory. Writing $n^i(x,a)$ for the episode of the $i$-th visit to $(x,a)$, the learning-rate condition is

$$\sum_{i=1}^\infty\alpha_{n^i(x,a)}=\infty,\qquad\sum_{i=1}^\infty\bigl[\alpha_{n^i(x,a)}\bigr]^2<\infty\qquad\forall x,a.\tag{3}$$

The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states $\langle x,n\rangle$ (a real state and a level $n$), in which taking $a$ at $\langle x,n\rangle$ replays a randomly chosen earlier episode that tried $a$ in $x$, emitting its reward and dropping to the level below that episode. Its expected one-step reward is $\mathcal R^{(n)}_x(a)$ and its aggregated transition probabilities are $P^{(n)}_{xy}[a]$.

Formalization targets

Goal: the Theorem (p. 282)

Given bounded rewards $|r_n|\le\mathcal R$, learning rates $0\le\alpha_n<1$ and (3),

$$Q_n(x,a)\to Q^*(x,a)\quad\text{as }n\to\infty,\ \forall x,a,\ \text{with probability }1.$$

Milestones (the paper's appendix, in attack order)

• Lemma A (p. 288): $Q_n(x,a)=Q^*_{\mathrm{ARP}}(\langle x,n\rangle,a)$ for all $a,x$ and $n\ge0$.
• Lemma B.1 (p. 289): the values of $s$ actions with and without a continuation policy differ by at most $\gamma^s\mathcal R/(1-\gamma)$.
• Lemma B.2 (p. 289): started high enough, the ARP strays below any level $l$ within $s$ actions with arbitrarily small probability.
• The stochastic-convergence theorem quoted in the proof of B.3 (p. 290): $X_{n+1}=X_n+\beta_n(\xi_n-X_n)$ with $\sum\beta_n=\infty$, $\sum\beta_n^2<\infty$ and bounded $\xi_n$ of mean $\Xi$ converges to $\Xi$ almost surely.
• Lemma B.3 (p. 290): almost surely $P^{(n)}_{xy}[a]\to P_{xy}[a]$ and $\mathcal R^{(n)}_x(a)\to\mathcal R_x(a)$.
• Lemma B.4 (p. 291): rewards within $\eta$ and transition rows within $\eta/\mathcal R$ give values of $s$ actions within $\eta s(s+1)/2$.

A further item states that the optimality equation has exactly one solution for $0\le\gamma<1$.

Significance

The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD($\lambda$), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.

Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.

Difficulty

The update touches one table entry at a time, at random times chosen by the agent, and its target $r_n+\gamma\max_b Q_{n-1}(y_n,b)$ depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize $Q_n$ as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.

Formalization scope

Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:

• $X$ and $\mathfrak A$ are Fintypes with decidable equality, $\mathfrak A$ is nonempty, and $\max_b$ is Finset.sup'. The process is a structure with R x a $=\mathcal R_x(a)$ and P x a y $=P_{xy}[a]$, rows nonnegative and summing to $1$.
• $Q^*$ enters the goal through the predicate IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.
• Lean index $n$ is the paper's episode $n\ge1$; index $0$ of the episode data is unused and qIter … 0 $=Q_0$.
• Condition (3) is written over episodes: the learning rate charged to $(x,a)$ at episode $n$ is $\alpha_n$ if $(x_n,a_n)=(x,a)$ and $0$ otherwise; its partial sums tend to $+\infty$ and its squares are summable. This equals (3) and forces infinitely many visits.
• Probability model (pinned). The paper describes it in words only. On a filtered probability space, $x_n,a_n,\alpha_n$ are $\mathcal F_{n-1}$-measurable, $y_n,r_n$ are $\mathcal F_n$-measurable, $\Pr[y_n=y\mid\mathcal F_{n-1}]=P_{x_ny}[a_n]$, $\mathbb E[r_n\mid\mathcal F_{n-1}]=\mathcal R_{x_n}(a_n)$, $|r_n|\le\mathcal R$, $0\le\alpha_n<1$, and (3) holds almost surely. Fixed episode schedules with independent outcomes are a special case.
• The ARP deck at level $n$ includes card $n$ (as in the card game and Lemma A's proof); $P^{(n)}$ keeps the printed range of levels $1,\dots,n-1$; ARP optimality is over deterministic Markov policies of the ARP. Finite action sequences are lists of actions with $0$ terminal reward.
• Corrections disclosed in the items. B.1 is stated with $\le$ (the page's strict inequalities fail for a constant reward). B.4 assumes closeness of transition rows in $\ell^1$ and $s\ge1$: with the page's entrywise closeness the printed constant is false once $|X|\ge4$. The stochastic-convergence theorem is read with conditional mean $\Xi$ and adapted steps.

Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.

The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.

Selected references

• C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292. https://doi.org/10.1023/A:1022676722315
• C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989.
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994), 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. https://doi.org/10.1007/BF00993306
• H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8

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

The Sherrington–Kirkpatrick model assigns random interactions to every pair of spins in a system. Its partition function aggregates the weights of all spin configurations, and the logarithm of that partition function is the free energy. For a finite system, the free energy is a random quantity because the interactions are random. A useful question is therefore how far it can move from a deterministic high-temperature scale. Aizenman, Lebowitz and Ruelle (1987), and Comets and Neveu (1995) for Gaussian couplings, proved that for $\beta<1$ the variable $\log Z_N-\beta^2N/4$ converges in law to a normal random variable ALR 1987; Talagrand asks instead for tail estimates valid for every $N$. Talagrand's Chapter 12 gives a finite-size tail bound and a bound on the expected free energy per site under explicit moment conditions on the interaction law Talagrand 1995.

The chapter belongs to a larger study of concentration inequalities on product spaces. Its relevance to the spin model is concrete: each pair interaction is an independent coordinate, while every spin configuration uses all those coordinates. The number of coordinates grows quadratically with the number of spins. A uniform estimate must respect both this growing dimension and the normalization in the energy Talagrand 1995, pp. 191–195.

Setting

Fix an integer $N\ge1$. A spin configuration is a vector $\varepsilon=(\varepsilon_i)_{1\le i\le N}$ with each $\varepsilon_i\in\{-1,1\}$. Each unordered pair of sites $i<j$ has a real coupling $h_{ij}$. For an inverse temperature $\beta>0$, the normalized partition function is

$$Z_N(h)=2^{-N}\sum_{\varepsilon\in\{-1,1\}^N} \exp\left(\frac{\beta}{\sqrt N}\sum_{1\le i<j\le N} h_{ij}\varepsilon_i\varepsilon_j\right).$$

Write $F_N(h)=\log Z_N(h)$. The factor $2^{-N}$ averages over configurations. Since every summand is positive, $Z_N(h)>0$ for every array $h$, so this logarithm is defined without excluding any coupling array.

The couplings are independent with a common probability law $\nu$ on $\mathbb R$; their joint law is $P_N=\nu^{\otimes\binom N2}$. Under $\nu$, a single coupling $H$ satisfies $\mathbb EH=\mathbb EH^3=0$ and $\mathbb EH^2=1$. The chapter also assumes $\mathbb E e^{\alpha|H|}<\infty$ for some $\alpha>0$. Its main theorem adds $\mathbb Ee^H<2$ and $\mathbb Ee^{-H}<2$. These inequalities describe a class of interaction laws rather than one chosen distribution. A median $M_N$ of $F_N$ means that both $P_N(F_N\le M_N)$ and $P_N(F_N\ge M_N)$ are at least $1/2$ Talagrand 1995, pp. 191–193.

Formalization targets

The goal is Theorem 12.1. There is one absolute constant $K>0$ such that, for $0<\beta<1$ and $0<t<N/K$,

$$P_N\left(\left|F_N-\frac{\beta^2N}{4}\right|\ge K\left(t+\sqrt{\log\frac K{1-\beta^2}}\right)\sqrt N\right) \le 2e^{-t^2},$$

and the same constant satisfies

$$-\frac K{\sqrt N}\sqrt{\log\frac2{1-\beta^2}} \le \frac1N\mathbb EF_N-\frac{\beta^2}{4} \le \frac KN.$$

The first formula controls deviations at finite $N$; the second locates the expected free energy per site. The theorem leaves the absolute value of $K$ unspecified, as the source does Talagrand 1995, Theorem 12.1.

Four numbered displays form the supporting targets. Equation (12.6) bounds the change in $F_N$ when all couplings are changed. Equation (12.5) bounds deviations about any median. Equations (12.7) and (12.8) give first- and second-moment estimates for $Z_N$. Together these specify the deterministic regularity and probabilistic estimates used by the chapter Talagrand 1995, pp. 192–195.

Significance

The theorem gives a nonasymptotic probability estimate, valid for each finite size and each law meeting the stated conditions. It also bounds the difference between the mean free energy per site and $\beta^2/4$ as $N$ grows, for fixed $\beta<1$. The moment estimates separately describe the scale of the partition function and limit its relative second moment. These conclusions keep the coupling law general within the stated moment class Talagrand 1995, Theorem 12.1 and Eqs. (12.7)–(12.8).

The result is proved in the cited paper; the open work here is its Lean formalization. A completed development would connect product-measure concentration, finite spin sums, exponential-moment bounds, and real-valued expectations in one reusable interface. The coupling product space and median conventions can also serve other finite random-interaction models. No machine-checked proof of this chapter's target is claimed by this proposal.

Difficulty

A direct bounded-differences estimate cannot be applied to this model as stated: the couplings are real and may be unbounded. An estimate that handles each coordinate must account for the law's exponential moments while still retaining the $N$ and $\beta$ factors in the chapter's explicit bounds. The normalization by $\sqrt N$ makes a single coupling's influence small, but there are $\binom N2$ couplings, so treating the total sensitivity as dimension-free would lose the scale of the theorem. The first moment alone also does not control the lower tail of $Z_N$; this is why the second-moment target is present Talagrand 1995, pp. 192–195.

Formalization scope

Lean indexes sites by Fin N and interactions by pairs with $i<j$. A spin is a Boolean choice interpreted as $-1$ or $1$, and the configuration sum is normalized by $2^N$. The coupling array is a function on the pair type, carrying the finite product measure of the common law $\nu$. The theorem uses $N\ge1$, $0<\beta<1$, and exactly the common-law moment assumptions above; the median deviation milestone uses $N\ge2$ because its denominator contains $N-1$. The main theorem places its single universal $K$ before every size, temperature, law, and deviation level.

Expectations are Bochner integrals, so integrability is explicit in the law predicates or in each conclusion that needs it. Probability expressions are real values of measurable events under the product measure. This avoids relying on Lean's default value for a nonintegrable integral. The model retains the entire real coupling law and does not replace it with a finite alphabet or a Gaussian special case. The partition function is built from the couplings and spins, rather than supplied as an unconstrained variable.

The source's displayed (12.5) omits $\beta$, whereas the derivation following (12.6) gives, for each tail separately, the range $0<t\le4\beta\sqrt N(N-1)$ and the exponent $-t^2/(32\beta^2(N-1))$ with the factor $2$. The formal milestone states exactly these two one-sided bounds, while its milestone text preserves the printed display verbatim. The first- and second-moment displays are kept with an absolute constant; the second-moment target uses the proof's $N\ge8$ range, since for smaller sizes the chapter's interaction-law assumptions do not ensure that $Z_N^2$ is integrable. Integrability of $F_N$ is a conclusion of the main theorem, never a hypothesis, and the median is quantified universally, so neither the expectation in (12.4) nor the deviation bound can hold by a default value of an undefined integral or by an unsatisfiable hypothesis; the Rademacher law $\nu=\frac12(\delta_{-1}+\delta_1)$ satisfies every assumption. Reusable contributions include integrability and measurability of $Z_N$ and $F_N$, product-law estimates, and the source's numbered inequalities.

Selected references

• Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.
• Michael Aizenman, Joel L. Lebowitz, David Ruelle, Some rigorous results on the Sherrington–Kirkpatrick spin glass model, Communications in Mathematical Physics 112 (1987), 3–20. DOI: 10.1007/BF01217677.
• Francis Comets, Jacques Neveu, The Sherrington–Kirkpatrick model of spin glasses and stochastic calculus: the high temperature case, Communications in Mathematical Physics 166 (1995), 549–564. DOI: 10.1007/BF02099887.

Motivation

Constrained convex programs are routinely solved by turning them into a sequence of unconstrained problems. The classical route is the ordinary Lagrangian $L_0(x, y) = f_0(x) + \sum_i y_i f_i(x)$, whose dual function $g_0$ is in general nonsmooth and equal to $-\infty$ off the orthant $y \ge 0$, so maximizing it requires a constrained, nonsmooth method. In 1969 Hestenes (JOTA 4, 1969) and Powell (in Optimization, ed. Fletcher, Academic Press, 1969) proposed the method of multipliers for equality constraints, which adds a quadratic penalty to the Lagrangian. Rockafellar's paper (Math. Programming 5, 1973) gives the inequality-constrained version, the penalty Lagrangian $L_r$, and shows that for convex programs its dual is a smooth, unconstrained, concave maximization problem with the same solutions and value as the ordinary dual. The method of multipliers built on this Lagrangian, now called the augmented Lagrangian method, underlies ADMM and many large-scale solvers.

Timeline. Hestenes and Powell (1969): multiplier method for equality constraints. Rockafellar (1973, this paper; and JOTA 12, 1973): the inequality-constrained penalty Lagrangian, its duality theory, and convergence of the multiplier method for convex programs. Rockafellar (Math. Oper. Res. 1, 1976): the method of multipliers identified as the proximal point algorithm applied to the dual. Bertsekas (Constrained Optimization and Lagrange Multiplier Methods, 1982): the general nonconvex theory.

This mission covers the first half of the paper: the duality theory of $L_r$ (§3) and the theorem that maximizing the penalty dual yields asymptotically optimal primal sequences (§4, Theorem 4.1).

Setting

Let $X$ be a nonempty convex subset of a real vector space $E$ and $f_0, f_1, \dots, f_m$ convex real functions on $X$. The problem is

$$\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \text{ subject to } f_i(x) \le 0,\ i = 1, \dots, m.$$

Multipliers $y$ range over $\mathbb R^m$, with Euclidean norm $|\cdot|$ and inner product $u \cdot y$. With $\theta(t) = \max\{0, t\}$ and a parameter $r > 0$, the penalty Lagrangian is

$$L_r(x, y) = f_0(x) + \frac{1}{4r} \sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big],$$

defined for all $y \in \mathbb R^m$ with no sign restriction. The dual function is $g_r(y) = \inf_{x \in X} L_r(x, y)$, and the dual problem $(D_r)$ maximizes $g_r$ over $\mathbb R^m$; $g_0$ and $(D_0)$ are the same with $L_0$, and $\sup g_0$ is the dual optimal value. In Lean these objects are Lr, L0, gr, g0, dualValue, and Fr is the perturbed objective $F_r(x, u) = f_0(x) + r|u|^2$ if $u \ge f(x)$, $+\infty$ otherwise.

A sequence $\{x^k\}$ in $X$ is asymptotically feasible if $\limsup_k f_i(x^k) \le 0$ for every $i$. The asymptotic optimal value (asympValue) is the infimum of $\limsup_k f_0(x^k)$ over asymptotically feasible sequences, and a sequence attaining it is asymptotically minimizing (IsAsympMinimizing). A maximizing sequence for $(D_r)$ is a sequence $\{y^k\}$ with $g_r(y^k) \to \sup g_r$.

Formalization targets

Goal: Theorem 4.1

Suppose the asymptotic optimal value in (P) is finite, $r > 0$, $\{y^k\}$ is a bounded maximizing sequence for $(D_r)$, and $x^k \in X$ satisfies

$$L_r(x^k, y^k) - g_r(y^k) \le \alpha_k, \qquad \alpha_k \to 0.$$

Then $\{x^k\}$ is asymptotically minimizing for (P).

Milestones

1. Theorem 3.1: $L_r(x, y) = \min_u \{F_r(x, u) + u \cdot y\}$; $L_r$ is convex in $x$ and concave in $y$.
2. Theorem 3.2: $g_r(y) = \max_z \{g_0(z) - \frac{1}{4r}|z - y|^2\}$; $(D_r)$ and $(D_0)$ have the same supremum and optimal solutions; if $g_0 \not\equiv -\infty$, $g_r$ is finite and $C^1$ with $\partial g_r/\partial y_i = \max\{-y_i/2r, f_i(x)\}$ at any $x$ attaining $g_r(y)$.
3. Corollary 3.3: $g_r(y) + (y' - y)\cdot\nabla g_r(y) \ge g_r(y') \ge g_r(y) + (y'-y)\cdot\nabla g_r(y) - \frac{1}{4r}|y'-y|^2$.
4. §4 (p. 364): the asymptotic optimal value equals the dual optimal value when the latter is not $-\infty$ or asymptotically feasible sequences exist.
5. Lemmas 4.2 and 4.3: $r|\nabla g_r(y)|^2 \le \sup g_r - g_r(y)$, and $r|\nabla_y L_r(x, y) - \nabla g_r(y)|^2 \le \alpha$ under (4.7).
6. (4.9)–(4.11): $u \mapsto F_0(x, u) + u \cdot y + r|u|^2$ has the unique minimizer $\nabla_y L_r(x, y)$.

Significance

Theorem 4.1 says that any procedure that drives the smooth, unconstrained dual $g_r$ to its supremum, while computing $L_r(\cdot, y^k)$-minimizers only approximately, produces an asymptotically optimal primal sequence. It needs no constraint qualification, no existence of a dual or primal optimal solution, and not even feasibility of (P): only that the asymptotic optimal value is finite. Together with Theorem 3.2 it justifies the multiplier method as a dual ascent on a $C^1$ concave function with Lipschitz gradient, and it is the starting point of the convergence theory of augmented Lagrangian methods.

None of these statements is formalized on Prove2Me or in Mathlib, which has Lagrangian duality only in special forms and no theory of the penalty Lagrangian or of asymptotic optimal values. The Qi–Sun augmented Lagrangian items on the platform (NonsmoothNewton.AugLagrangian.*) use the $(r/2)$-scaled function on $\mathbb R^n$ and concern smoothness in $(x, y)$, not the dual function. The results of this paper are classical and proved; this mission formalizes them.

Difficulty

The obvious argument compares the primal iterates with a saddle point: if $\bar y$ is a dual optimal solution and (P) is normal, approximate minimizers of $L_r(\cdot, \bar y)$ are approximately optimal. Theorem 4.1 assumes neither. The function $g_r$ need not attain its supremum, (P) need not be normal or even feasible, and there may be no Kuhn–Tucker vector, so there is no saddle point to compare with; the only data are the dual values $g_r(y^k)$, the boundedness of $\{y^k\}$ and the tolerances $\alpha_k$. The difficulty is to obtain primal feasibility and optimality information from dual convergence alone, measured against the asymptotic optimal value rather than the infimum in (P). Every ingredient is extended-real-valued: $g_0$ is $-\infty$ off the orthant, $g_r$ may be identically $-\infty$, and the asymptotic optimal value may be $\pm\infty$. Mathlib does not package this part of convex analysis (partial conjugates, envelopes of extended-real concave functions, the asymptotic duality theorem).

Formalization scope

$E$ is a bare real vector space (AddCommGroup E, Module ℝ E) with no topology, as in the paper. The functions $f_i$ are total functions $E \to \mathbb R$ assumed convex on $X$; only their values on $X$ enter. Constraint indices are Fin m (0-based) and $f_0$ is a separate argument. Multipliers live in EuclideanSpace ℝ (Fin m). The standing assumption of §3 ($X$ nonempty convex, all $f_i$ convex) is a hypothesis of every theorem.

Explicit choices:

• $g_r$, $g_0$, the dual value, the asymptotic optimal value and every $\limsup$ are computed in EReal, so $\pm\infty$ are represented and no infimum is replaced by a junk real value.
• $r > 0$ is an explicit hypothesis wherever $L_r$ is used; $L_0$ is a separate definition.
• (4.7) is written $L_r(x^k, y^k) \le g_r(y^k) + \alpha_k$ in EReal, equivalent to the printed difference; only $\alpha_k \to 0$ is assumed.
• Concavity or convexity of extended-real functions is stated through convex hypographs and epigraphs; "max" in (3.5) is attainment of the greatest value.
• Gradients are taken of the real coercion of $g_r$, and only under hypotheses that make $g_r$ finite.
• Dual optimal solutions do not exist when $g_r \equiv -\infty$ (the paper's convention, p. 361).
• Lemmas 4.2, 4.3 and (4.9)–(4.11) are stated for one point rather than along a sequence; the paper's statements are their instances.
• Misprints: "concave in $y \in Y$" (Theorem 3.1) reads $\mathbb R^m$; the lost minus sign in Lemma 4.2 is restored.

The goal must not be replaced by "$f_0(x^k) \to \inf\text{(P)}$ and $\limsup f_i(x^k) \le 0$": that is the special case of normal problems with feasible solutions. Nor may it assume a Slater point, a Kuhn–Tucker vector, or feasibility of (P), each of which makes it a special case.

A complete development needs extended-real convex analysis on $\mathbb R^m$ (partial conjugates, Moreau envelopes of concave functions, the asymptotic duality theorem), which is reusable beyond this mission. Contributions proving any milestone, or general lemmas on Moreau envelopes of extended-real concave functions, are welcome.

Selected references

• R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
• M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
• R. T. Rockafellar, The multiplier method of Hestenes and Powell applied to convex programming, Journal of Optimization Theory and Applications 12 (1973) 555–562. https://doi.org/10.1007/BF00934777
• R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1 (1976) 97–116. https://doi.org/10.1287/moor.1.2.97
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982.

Motivation

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

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 9.1

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

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

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

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

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

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

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

Proposition 9.2 and Eq. (9.7)

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Many stochastic systems studied in operations research "start afresh" at certain random instants: a single-server queue each time a customer arrives to find the server idle, an inventory system each time stock is replenished to its order level, a reliability system each time a failed unit is replaced. Between such instants the system may evolve in a complicated way, but its future after one of them does not depend on its past. W. L. Smith's 1955 paper Regenerative stochastic processes made this idea into a general theory. Its first main result, Theorem 2, says that the state probabilities of such a process converge as time grows, and gives the limit explicitly in terms of the behaviour of the process within one cycle and the law of the cycle length.

This limit theorem is the standard way of proving that a queue, an inventory or a reliability model has a limiting distribution and of computing it: one exhibits regeneration points and evaluates one cycle.

Timeline.

• 1948: Blackwell proves that the renewal function of a non-lattice renewal process has increments $H(t+h) - H(t) \to h/\mu_1$ (Duke Math. J. 15).
• 1949: Erdős, Feller and Pollard prove the discrete (lattice) renewal theorem.
• 1954: Smith proves the key renewal theorem for bounded, non-increasing, integrable kernels, and a version for kernels tending to zero when some convolution power of the cycle law has an absolutely continuous part (Proc. Roy. Soc. Edinburgh A 64).
• 1955: Smith introduces regenerative and equilibrium processes and proves Theorem 2 (this paper).

Setting

A general renewal process is a sequence $t_0, t_1, t_2, \dots$ of independent non-negative random variables in which $t_1, t_2, \dots$ have a common law $F$, not concentrated at $0$, with mean $\mu_1 = \int x\,dF(x) \in (0,\infty]$, and the delay $t_0$ has a law $K$. The regeneration epochs are $T_k = t_0 + \dots + t_k$, and $n_t$ is the number of epochs in $[0,t]$. The renewal measure is

$$H_K = \sum_{n \ge 0} K * F^{*n},$$

so that $H_K([0,t]) = \mathbb E\, n_t$. The law $F$ is periodic with period $\varpi > 0$ if all its mass sits on $\{0, \varpi, 2\varpi, \dots\}$; otherwise $\varpi = 0$ and $F$ is aperiodic. $F$ belongs to the class $\mathfrak S$ if some convolution power $F^{*k}$, $k \ge 1$, has a non-zero absolutely continuous component.

An equilibrium process $\mathcal E(\mathfrak z, \mathcal A, \{t_i\})$ consists of a process $x_t$ on a measurable state space $\mathfrak X$, a class $\mathcal A$ of measurable sets of states, a family of probability measures $P\{\cdot \mid z\}$ indexed by boundary conditions $z \in \mathfrak z$, and under each of them a general renewal process whose cycle law $F$ does not depend on $z$ and whose delay has law $K_z$. For each $A \in \mathcal A$ there is a measurable function $\varphi_A$, depending on $A$ only, such that

$$P\{x_t \in A \mid z;\ n_t > 0;\ L_t\} = \varphi_A(t - L_t),$$

where $L_t$ is the epoch of the last regeneration at or before $t$. In words: once a regeneration has occurred, the chance of being in $A$ at time $t$ depends only on the time elapsed since the last one.

Formalization targets

Goal: Theorem 2

If the process is aperiodic ($\varpi = 0$) and the regeneration event is certain ($K_z(+\infty) = 1$), then for every $z$ and every $A \in \mathcal A$ satisfying one of the regularity conditions (iv)$'$ ($\varphi_A\{1-F\}$ integrable and monotonic), (iv)$''_a$ ($\mu_1 < \infty$ and $\varphi_A\{1-F\}$ of locally bounded variation) or (iv)$''_b$ ($\mu_1 < \infty$ and $F \in \mathfrak S$),

$$\lim_{t\to\infty} P\{x_t \in A \mid z\} = \frac{1}{\mu_1} \int_0^\infty \varphi_A(v)\{1 - F(v)\}\,dv,$$

the limit being $0$ when $\mu_1 = \infty$.

Milestones

1. Theorem A(a), the key renewal theorem: for bounded, non-increasing, integrable $\Psi$ and aperiodic $F$, $\int_0^t \Psi(t-t')\,dH_K(t') \to (K(+\infty)/\mu_1)\int_0^\infty \Psi$.
2. Lemma A: for $F \in \mathfrak S$, $(1 - G^*(s))/(1 - F^*(s))$ is the Laplace–Stieltjes transform of a function of bounded variation with net variation $\lambda_1/\mu_1$.
3. Theorem 1: the same limit for bounded integrable $\Psi \to 0$ when $F \in \mathfrak S$ and $\mu_1 < \infty$.
4. (3·4·3): $P\{x_t \in A \mid z\} = P\{x_t \in A, t_0 > t \mid z\} + \int_0^t \varphi_A(t-\tau)\{1-F(t-\tau)\}\,dH_{K_z}(\tau)$.
5. (3·4·5): $\int_{t-\Delta}^t g(t-v)\,dH_K(v) \to \mu_1^{-1}\int_0^\Delta g$ for the page's kernel $g=\varphi_A(1-F)$ of locally bounded variation.
6. (3·4·7): $\int_0^{t-\Delta}\{1-F(t-v)\}\,dH(v) \to \mu_1^{-1}\int_\Delta^\infty\{1-F\}$; the limit is at most $\varepsilon$ for large enough $\Delta$.

Significance

The result. Theorem 2 reduces the long-run behaviour of a regenerative system to a one-cycle computation: the limiting probability of $A$ is the expected time spent in $A$ during a cycle divided by the expected cycle length. It underlies the existence of limiting distributions for the waiting time in the GI/G/1 queue, the number in system in many queueing networks, inventory levels under $(s,S)$ policies and the availability of repairable systems, and it is the continuous-time counterpart of the ergodic theorem for positive recurrent Markov chains. The paper's later sections apply it to semi-Markov processes.

Formalizing it. The results here are classical and proved; none is machine-checked. Mathlib has measure convolution and the strong law of large numbers but no renewal measure, no Blackwell or key renewal theorem, and no regenerative process. On Prove2Me only the discrete Erdős–Feller–Pollard renewal theorem for renewal sequences is proved. A completed mission supplies the continuous-time key renewal theorem in two forms, a reusable renewal-measure interface, and a general limit theorem for regenerative processes on which queueing and inventory results can be built.

Difficulty

The decomposition (3·4·3) is a direct consequence of independence and the renewal structure. The difficulty is the key renewal theorem. Blackwell's theorem controls $H_K$ on intervals of fixed length; passing from intervals to a general kernel requires the kernel to be directly Riemann integrable, which is why Theorem A asks for monotonicity and Theorem 2 lists three alternative regularity conditions. A merely integrable kernel tending to zero is not enough for a general aperiodic $F$: $H_K$ may concentrate on a set where the kernel has tall narrow spikes. Theorem 1 removes monotonicity only for $F \in \mathfrak S$, through a Laplace-transform argument that needs Lemma A, the uniqueness theorem for Laplace transforms and the fact that the singular part of $H_K$ contributes nothing in the limit. Blackwell's theorem itself, for a non-lattice law with possibly infinite mean, is not in any library and is a substantial development of its own.

Formalization scope

Laws are measures on $\mathbb R$ carried by $[0,\infty)$; the distribution function is $F(t) = F((-\infty,t])$ and $1 - F(v) = F((v,\infty))$. The mean $\mu_1$ is an extended non-negative real, so $\mu_1 = \infty$ is a value; every statement with a $1/\mu_1$ treats $\mu_1 = \infty$ and $\mu_1 < \infty$ as separate cases rather than relying on a default value of division. Stieltjes integrals $\int_0^t \cdots dH_K$ are integrals against the renewal measure over the closed interval $[0,t]$. Aperiodicity is the lattice condition on $F$, not a density condition. The delay law $K$ in Theorem A and Theorem 1 may have mass below one.

In the equilibrium process the conditional-probability representation is stated as the defining identity of conditional probability for every Borel set of last-regeneration epochs, every $t \ge 0$, every $z$ and every $A \in \mathcal A$. The paper writes $T_{n_t}$ for the last regeneration epoch, although under its own indexing that symbol is the first epoch after $t$; the formalization uses the last epoch at or before $t$. The delay $t_0$ is real-valued, so the regeneration event is certain (hypothesis (iii)); improper delays and cycles, which §3 of the paper also allows, are outside this mission.

A trivializing formalization would condition only on $\{n_t > 0\}$ rather than on the epoch of the last regeneration, or fix $\mu_1 < \infty$ globally; both are ruled out, and hypothesis (iv) is imposed separately for the one set $A$ of the conclusion.

Infrastructure needed: Blackwell's renewal theorem (non-lattice, finite or infinite mean), direct Riemann integrability, Laplace–Stieltjes transforms of functions of bounded variation and their uniqueness. All of these are reusable well beyond this paper; contributions of any of them are welcome. The convolution power and the Laplace–Stieltjes transform are taken from the published definition QueueingFundamentals.MG1.transforms.

Selected references

• W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232 (1955), 6–31. https://doi.org/10.1098/rspa.1955.0198
• W. L. Smith, Asymptotic renewal theorems, Proc. Roy. Soc. Edinburgh A 64 (1954), 9–48. https://doi.org/10.1017/S0080454100007482
• D. Blackwell, A renewal theorem, Duke Math. J. 15 (1948), 145–150. https://doi.org/10.1215/S0012-7094-48-01568-3
• P. Erdős, W. Feller, H. Pollard, A property of power series with positive coefficients, Bull. Amer. Math. Soc. 55 (1949), 201–204. https://doi.org/10.1090/S0002-9904-1949-09203-0
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Ch. V–VI. https://doi.org/10.1007/b97236