Markov Chain

Motivation

Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.

Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served $K$-server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).

Setting

There are $I$ customer types and $J$ queues. Customers of type $i$ enter the system in a Poisson stream of rate $\nu(i)>0$ and visit the queues $r(i,1),r(i,2),\dots,r(i,S(i))$ in that order before leaving; two successive stages of a route are at different queues.

Queue $j$ holds its $n_j$ customers in positions $1,\dots,n_j$. Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate $\phi_j(n_j)$, with $\phi_j(n)>0$ for $n>0$; a proportion $\gamma_j(l,n_j)$ goes to the customer in position $l$. An arriving customer takes position $l$ with probability $\delta_j(l,n_j+1)$. For each $n\ge1$, $\gamma_j(\cdot,n)$ and $\delta_j(\cdot,n)$ are probability vectors on $\{1,\dots,n\}$.

The class of the customer in position $l$ of queue $j$ is $c_j(l)=(t_j(l),s_j(l))$, his type and the stage of his route. The state of queue $j$ is $\mathbf c_j=(c_j(1),\dots,c_j(n_j))$ and the state of the network is $\mathbf C=(\mathbf c_1,\dots,\mathbf c_J)$. Its transition rates $q(\mathbf C,\mathbf D)$, displays (3.1)–(3.6), are the sums of the intensities of all events taking $\mathbf C$ to $\mathbf D$: a departure from the system (intensity $\phi_j(n_j)\gamma_j(l,n_j)$), a move from position $l$ of queue $j$ to position $m$ of the next queue $k$ (intensity $\phi_j(n_j)\gamma_j(l,n_j)\delta_k(m,n_k+1)$), and an arrival into position $m$ of the first queue $k$ of a route (intensity $\nu(i)\delta_k(m,n_k+1)$).

With $\alpha_j(i,s)=\nu(i)$ if $r(i,s)=j$ and $0$ otherwise, set

$$a_j=\sum_{i,s}\alpha_j(i,s),\qquad b_j^{-1}=\sum_{n=0}^{\infty}\frac{a_j^n}{\prod_{l=1}^{n}\phi_j(l)},\qquad \pi_j(\mathbf c_j)=b_j\prod_{l=1}^{n_j}\frac{\alpha_j(t_j(l),s_j(l))}{\phi_j(l)}.$$

Formalization targets

Goal: Theorem 3.1 (p. 61)

If every series defining $b_j^{-1}$ converges, then

$$\pi(\mathbf C)=\prod_{j=1}^{J}\pi_j(\mathbf c_j)$$

is positive, sums to $1$ over all network states, and satisfies the equilibrium equations

$$\pi(\mathbf C)\sum_{\mathbf D}q(\mathbf C,\mathbf D)=\sum_{\mathbf D}\pi(\mathbf D)\,q(\mathbf D,\mathbf C)\quad\text{for every }\mathbf C.$$

Milestones

• Theorem 3.2 (p. 62). The time-reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$ are the rates of the reversed network: routes traversed backwards, $\gamma_j$ and $\delta_j$ interchanged.
• Corollary 3.4 (p. 63). Queue $j$ is independent of the rest of the network, is in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$, holds $n$ customers with probability $b_ja_j^n/\prod_{l=1}^n\phi_j(l)$ (3.7), and a customer in position $l$ is of class $(i,s)$ with probability $\alpha_j(i,s)/a_j$.
• Corollary 3.5 (p. 63). A type-$i$ customer reaching queue $j$ at stage $s$ finds it in state $\mathbf c_j$ with probability $\pi_j(\mathbf c_j)$.
• Lemma 3.13 (p. 89). For a multiclass queue with Poisson arrivals of rate $\nu(c)$ and departure intensities $\nu(c)\phi_c(\mathbf n)$: reversible $\Leftrightarrow$ quasi-reversible $\Leftrightarrow$ $\Phi(\mathbf n)=\phi_c(\mathbf n)\Phi(\mathbf n-\mathbf e_c)$ for some positive $\Phi$ (3.26).

Significance

Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate $a_j$, even though the actual arrival stream at queue $j$ is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).

The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.

Difficulty

The obvious first attempt, detailed balance, fails: $\pi(\mathbf C)q(\mathbf C,\mathbf D)$ and $\pi(\mathbf D)q(\mathbf D,\mathbf C)$ differ in general, because a customer's route cannot be run backwards inside the same network ($q(\mathbf D,\mathbf C)$ is usually $0$ when $q(\mathbf C,\mathbf D)>0$). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of $J$-tuples of lists, reorganized by queue length together with the identity $\sum_{\text{classes at } j}\alpha_j=a_j$.

Formalization scope

• Finite types and queues. Types are Fin I, queues Fin J; the book allows countably many types with $\sum_i\nu(i)<\infty$. A network state is a function assigning to each queue a list of classes $(i,s)$ with $r(i,s)=j$; the state space is countable and all sums over it are tsum/HasSum.
• Indexing. Stages and list positions are $0$-based in Lean; $\gamma_j(l,n)$ and $\delta_j(l,n)$ keep the book's $1$-based position argument.
• Rate level. Equilibrium means: positive, summing to $1$, and satisfying the equilibrium equations (the published KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates $\pi(\mathbf D)q(\mathbf D,\mathbf C)/\pi(\mathbf C)$; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).
• Normalizing constants. $b_j$ is defined through a tsum, which Lean sets to $0$ for a divergent series; every theorem assumes the series converges, the book's "none of $b_1,\dots,b_J$ is zero".
• No trivial instance. The goal holds for arbitrary $I$, $J$, $\nu$, routes, $\phi_j$, $\gamma_j$, $\delta_j$ subject only to the book's constraints; a proof for a single queue, or for fixed $\gamma=\delta$ disciplines, does not prove it. In Lemma 3.13 the function $\Phi$ is required to be positive, since $\Phi\equiv0$ satisfies (3.26) for every queue.

Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over $\prod_j \mathrm{List}(\cdot)$, and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://doi.org/10.2307/3212785
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887
• J. R. Jackson, Jobshop-like queueing systems, Management Science 10 (1963), 131–142. https://doi.org/10.1287/mnsc.10.1.131
• F. P. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781139565363

Why symmetric queues

The classical product-form results for queueing networks (Jackson, Kelly, Baskett–Chandy–Muntz–Palacios) assume exponentially distributed service requirements, because then the state of a queue need not record how much service each customer has received. Real service times are rarely exponential: telephone call lengths, job sizes in time-shared computers and web transfers are far from it. Symmetric queues, introduced in §3.3 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), form the class of single queues for which the stationary distribution of the number of customers, and of their classes, depends on the service requirement distribution only through its mean. This property, insensitivity, is what makes Erlang's loss formula valid for arbitrarily distributed call lengths (Kelly, p. 79), and it is the reason processor-sharing, last-come-first-served preemptive and infinite-server stations may appear with general service in product-form networks.

Timeline. Sevastyanov (1957) proved that Erlang's loss formula holds for arbitrarily distributed call lengths. Kelly (1975, 1976) introduced queues with customers of different types whose effort and arrival-position functions coincide, and showed product form for networks of them with non-exponential service built from exponential stages; Barbour (1976) extended the method of stages; Baskett, Chandy, Muntz and Palacios (1975) gave product form for networks containing processor-sharing, LCFS-preemptive and infinite-server stations with phase-type service. Kelly's 1979 book presents the symmetric queue in the form formalized here.

Setting

A symmetric queue holds customers in positions $1, 2, \dots, n$, where $n$ is the number present. It operates as follows (Kelly, p. 72):

1. the service requirement of a customer is a random variable whose distribution may depend on the class of the customer;
2. a total service effort is supplied at rate $\phi(n)$, with $\phi(n) > 0$ for $n > 0$;
3. a proportion $\gamma(l, n)$ of this effort, $\sum_{l=1}^n \gamma(l, n) = 1$, goes to the customer in position $l$; when he leaves, the customers in positions $l+1, \dots, n$ move down by one;
4. an arriving customer moves into position $l \in \{1, \dots, n+1\}$ with probability $\gamma(l, n+1)$ — the same function — and the customers in positions $l, \dots, n$ move up by one.

Server-sharing ($\gamma(l, n) = 1/n$), the stack ($\gamma(n, n) = 1$, last come first served preemptive), the queue with no waiting room and the infinite-server queue are examples (pp. 73–74).

Customers of class $c$ arrive in a Poisson stream of rate $\nu(c)$. On arrival a class-$c$ customer receives a refined class $(c, z)$ with probability $p(c, z)$, $\sum_z p(c, z) = 1$, and then needs $w(c, z) \ge 1$ independent stages of service, each exponentially distributed with mean $d(c, z) > 0$. The class-$c$ service requirement is therefore a mixture of gamma distributions with mean

$$a(c) = \sum_z p(c, z)\, w(c, z)\, d(c, z),$$

and the work arriving per unit time is $a = \sum_c \nu(c) a(c)$. The record of the customer in position $l$ is $\mathbf c(l) = (c(l), z(l), u(l))$, $u(l)$ the stage in progress, and $\mathbf c = (\mathbf c(1), \dots, \mathbf c(n))$ is a Markov process. Its transitions are: an arrival of class $(c,z)$ into position $l$ at stage $1$, at rate $\nu(c)p(c,z)\gamma(l, n+1)$; and, at rate $\phi(n)\gamma(l,n)/d(c(l),z(l))$, completion of the current stage of the customer in position $l$, which moves him to the next stage or, after stage $w(c(l), z(l))$, out of the queue. The normalizing constant is

$$b^{-1} = \sum_{n=0}^{\infty} \frac{a^n}{\prod_{l=1}^n \phi(l)}. \tag{3.15}$$

Formalization targets

Goal: Theorem 3.8

When (3.15) converges, the distribution

$$\pi(\mathbf c) = b \prod_{l=1}^n \frac{\nu(c(l))\, p(c(l), z(l))\, d(c(l), z(l))}{\phi(l)} \tag{3.18}$$

is the equilibrium distribution of $\mathbf c$, and under it

$$\mathbb P(n \text{ customers}) = \frac{b\,a^n}{\prod_{l=1}^n \phi(l)}, \qquad \mathbb P(\text{classes } c_1, \dots, c_n \mid n) = \prod_{l=1}^n \frac{\nu(c_l)\, a(c_l)}{a},$$

and the queue is quasi-reversible with respect to the classification $c$ and to $(c, z)$: from every state, the rate of arrivals of each class does not depend on the state, both for the process and its time reversal (relations (3.8) and (3.10) of p. 67).

Milestones

• Eqs. (3.14)–(3.15): the case of one refinement per class, $\pi(\mathbf c) = b\prod_l \nu(c(l))d(c(l))/\phi(l)$ with $a = \sum_c \nu(c)d(c)w(c)$.
• Eqs. (3.16)–(3.17): in that case, the law of $n$, and given $n$ independent positions of class $c$ with probability $\nu(c)d(c)w(c)/a$ and uniform stage.
• Eq. (3.18): the equilibrium distribution under gamma-mixture service.
• Lemma 3.9: mixtures of gamma distributions approximate, at continuity points, the distribution function of any positive random variable.

Significance

Theorem 3.8 gives the stationary law of a symmetric queue in closed form and shows that it depends on the service requirement distributions only through their means $a(c)$. Quasi-reversibility (part (iii)) is the property that lets symmetric queues be placed in networks: Kelly's §3.2 shows that a network of quasi-reversible queues has a product-form equilibrium, so Theorem 3.8 is the single-queue input to product-form networks with processor-sharing, LCFS-preemptive and infinite-server stations and class-dependent, non-exponential service. Lemma 3.9 is the approximation step behind the extension to arbitrary service distributions (Theorem 3.10).

These results are classical and proved in the book. To our knowledge none of them is machine-checked; Mathlib has the gamma distribution and distribution functions but no queueing theory. The mission produces a formal model of the symmetric queue as a countable-state Markov process, its equilibrium distribution, the insensitive marginals and the rate characterization of quasi-reversibility, all reusable by the chapter on networks of quasi-reversible queues.

Difficulty

The obvious first attempt, detailed balance, fails: the stage process is not reversible in general, since an intermediate stage completion has no transition back. The equilibrium equations must be verified in full, over a countable state space in which a single state is reached from infinitely many others. The symmetry condition $\gamma \equiv \delta$ is essential and must enter the argument: without it (for first-come-first-served, say) the distribution (3.18) is false for non-exponential service. Positions shift on every arrival and departure, so the bookkeeping of which list results from which event, including coincidences when neighbouring customers have identical records, is the main formal burden. The marginal computations sum (3.18) over lists of records, where convergence must be tracked, and Lemma 3.9 needs an explicit construction of approximating gamma mixtures.

Formalization scope

• The state is a List of customer records (class, refined class, stage); list index $i$ is position $l = i + 1$, and $\gamma(l, n)$, $\phi(n)$ keep the book's $1$-based indexing. The state space consists of the lists whose records have $\nu(c)p(c,z) > 0$ and $1 \le u \le w(c, z)$: records of a refined class arriving at rate zero are unreachable and excluded.
• Classes $\mathcal C$ and refinements $\mathcal Z$ are arbitrary countable types. All infinite sums are HasSum or tsum with explicit convergence hypotheses: $\sum_c \nu(c) < \infty$ (finite exit rates, the book's standing assumption of §1.1), convergence of $a(c)$, of $a$, and of (3.15). "Equilibrium distribution" means positive, summing to one, and satisfying the equilibrium equations with convergent series.
• The statement is rate level: (3.18) is shown to satisfy the equilibrium equations of the stage process, and quasi-reversibility is its rate characterization (3.8), (3.10). That these describe the stationary process and its time reversal is the book's Chapter 1 and is not reformalized.
• Trivializing readings ruled out: the goal keeps $p$, $w$ and $d$ general (not $w \equiv 1$, which would make the result Section 3.1's exponential case); the arrival position uses the same $\gamma$ as the service split; and in Lemma 3.9 the approximants must be genuine gamma mixtures with integer shapes, which a point mass is not.
• Not planned: Theorem 3.10 (arbitrary service distributions; only an outline of proof and a continuous state space the book does not construct) and Theorem 3.11 (reversibility of the number in queue, a non-Markov process).

Welcome contributions: proofs of the milestones, lemmas about List.insertIdx/List.eraseIdx bookkeeping for queues with positions, and summation over lists of records.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979, §3.3, pp. 72–82. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://www.jstor.org/journal/japplprob
• F. P. Kelly, Networks of queues, Advances in Applied Probability 8 (1976), 416–432. https://www.jstor.org/journal/advaapplprob
• A. D. Barbour, Networks of queues and the method of stages, Advances in Applied Probability 8 (1976), 584–591. https://www.jstor.org/journal/advaapplprob
• B. A. Sevastyanov, An ergodic theorem for Markov processes and its application to telephone systems with refusals, Theory of Probability and its Applications 2 (1957), 104–112.
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887

Motivation

A Markov decision problem models a system that is observed once per period and controlled by choosing an action: the action earns an immediate income and determines the probabilities of the next state. Inventory control, machine replacement, queue admission and many reinforcement-learning benchmarks are of this form. With future income discounted by a factor $\beta<1$, Howard (Dynamic Programming and Markov Processes, 1960) showed how to compute an optimal policy by policy improvement. The undiscounted problem ($\beta=1$) is harder, because total income is typically infinite.

David Blackwell's Discrete Dynamic Programming (Ann. Math. Statist. 33 (1962) 719–726) treats $\beta=1$ as a limit of $\beta<1$. Its Theorem 5 shows that some stationary policy is optimal simultaneously for all discount factors sufficiently close to $1$. Such policies are now called Blackwell optimal, and the result is the base of sensitive discount optimality (Veinott, 1969) and of the standard textbook treatment of average-reward problems (Puterman, Markov Decision Processes, 1994, Ch. 10).

Timeline. Howard (1960): policy iteration for discounted and average-reward finite problems. Blackwell (1962): Theorem 5 (Blackwell optimal stationary policies exist) and the characterization of nearly optimal stationary policies (Theorem 4, the subject of the companion mission). Miller and Veinott (Ann. Math. Statist. 40 (1969) 366–370), Veinott (Ann. Math. Statist. 40 (1969) 1635–1660): Laurent expansions of $V_\beta$ in $1-\beta$ and $n$-discount optimality.

Setting

There are finitely many states $s$ and a finite set $A$ of actions, every action available in every state. In state $s$, action $a$ yields income $i(s,a)\in\mathbb R$ (any sign) and moves the system to state $s'$ with probability $q(s'\mid s,a)$; each $q(\cdot\mid s,a)$ is a probability vector.

A decision rule is a function $f$ from states to actions; $F$ is the finite set of decision rules. A policy is a sequence $\pi=\{f_n,\ n=1,2,\dots\}$ in $F$: on day $n$, in state $s$, action $f_n(s)$ is used. Policies are deterministic and Markov but may change with time. The policy $(f,\pi)$ uses $f$ on day $1$ and then follows $\pi$; $f^{(\infty)}$ uses $f$ every day and is called stationary.

For $f\in F$, $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s'\mid s,f(s)))_{s,s'}$. With $Q_0(\pi)=I$ and $Q_n(\pi)=Q(f_1)\cdots Q(f_n)$, the return of $\pi$ at discount factor $0\le\beta<1$ is

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

a vector indexed by the initial state. Vectors are compared coordinatewise; $w_1>w_2$ means $w_1\ge w_2$ and $w_1\ne w_2$.

A policy $\pi^*$ is $\beta$-optimal if $V_\beta(\pi^*)\ge V_\beta(\pi)$ for every policy $\pi$. Following §4 of the paper, a policy is optimal if it is $\beta$-optimal for all $\beta$ sufficiently near $1$.

Formalization targets

Goal: Theorem 5

There exist a decision rule $f$ and $\beta_0<1$ such that

$$V_\beta(f^{(\infty)})\ \ge\ V_\beta(\pi)\qquad\text{for all }\beta\in(\beta_0,1)\text{ and all policies }\pi.$$

One $f$ and one $\beta_0$ serve every competing policy and every $\beta\in(\beta_0,1)$.

Milestones

1. The composition rule $V_\beta(f,\pi)=L(f)V_\beta(\pi)$, with $L(f)w=r(f)+\beta Q(f)w$, and its $N$-fold version (§2).
2. Theorem 1: if $V_\beta(f,\pi^*)\le V_\beta(\pi^*)$ for all $f\in F$, then $\pi^*$ is $\beta$-optimal.
3. Theorem 2: if $V_\beta(f,\pi)>V_\beta(\pi)$ then $V_\beta(f^{(\infty)})>V_\beta(\pi)$.
4. Theorem 3 (policy improvement): if no action improves $f^{(\infty)}$ by one step, $f^{(\infty)}$ is $\beta$-optimal; otherwise switching to improving actions gives $g^{(\infty)}>f^{(\infty)}$.
5. Corollary: for each fixed $\beta\in[0,1)$ some stationary policy is $\beta$-optimal.
6. Each coordinate of $V_\beta(f^{(\infty)})$ is a rational function of $\beta$ on $[0,1)$ with nonvanishing denominator.
7. Some $f^*$ is $\beta$-optimal for a set of $\beta$'s having $1$ as a limit point.
8. If $V_\beta(f^{*(\infty)})\ge V_\beta(g^{(\infty)})$ for a set of $\beta$'s accumulating at $1$, then it holds for all $\beta$ near $1$.

Significance

The result. Theorem 5 shows that the infinitely many discounted problems near $\beta=1$ share a common optimal stationary policy. Such a policy is also optimal for the long-run average criterion, which settles the existence of average-optimal stationary policies in finite models without any recurrence assumption. It also justifies computing undiscounted solutions as limits of discounted ones, and it is the first case of the sensitive optimality criteria developed later.

Formalizing it. The theorem is classical and proved in the paper and in the textbooks; there is no machine-checked proof of it in Blackwell's model on the platform. A related open item, SennottDP.AvgFinite.prop_6_2_3_blackwell_optimal, states the textbook version for nonnegative costs and randomized history-dependent policies; the present mission is Blackwell's own formulation with incomes of either sign and deterministic Markov policies. A complete development also yields a verified policy improvement theorem (Theorem 3) and the rationality of discounted values in $\beta$, both reusable for any finite-state discounted model.

Difficulty

The Corollary gives, for each $\beta$, some optimal stationary policy, and $F$ is finite, so one $f^*$ is $\beta$-optimal for infinitely many $\beta$ accumulating at $1$. The obvious argument stops there: optimality on a sequence of $\beta$'s says nothing about the $\beta$'s in between, and a pointwise limit argument cannot produce a whole interval $(\beta_0,1)$. The step that fails is passing from "frequently" to "eventually", and it needs structural information about how $V_\beta$ depends on $\beta$, not just continuity. A second difficulty is the comparison class: optimality must hold against all time-dependent policies, not only the finitely many stationary ones, so the final step has to bring the Corollary back in for every $\beta$ near $1$.

Formalization scope

States and actions are finite nonempty Lean types St, Act; decision rules are functions St → Act and policies are sequences ℕ → St → Act, indexed from $0$ (π 0 is Blackwell's $f_1$). Incomes are real-valued with no sign restriction. The law of motion law s a s' $=q(s'\mid s,a)$ satisfies the published predicate IsTransitionKernel. $Q_n(\pi)$ is the ordered matrix product and $V_\beta(\pi)$ is the tsum of the series, which converges absolutely for $0\le\beta<1$; every statement at a fixed $\beta$ assumes $0\le\beta<1$, and nothing is stated for $\beta\ge1$. Vector inequalities are coordinatewise, and the strict order is "$\ge$ and $\ne$", not coordinatewise strict. "$\beta$ sufficiently near $1$" is "there is $\beta_0<1$ such that for every $\beta\in(\beta_0,1)$". The paper's §4 phrase $V_\beta(\pi)=U(\beta)$ is encoded as $\beta$-optimality, so no supremum over policies appears.

The word "optimal" has two meanings in the paper: at one fixed $\beta$ (§3, the Corollary) and for all $\beta$ near $1$ (§4, Theorem 5). The Lean development keeps them apart as IsBetaOptimal β and IsOptimal. A statement of Theorem 5 at a single $\beta$, with "there exists $\beta$", for a set of $\beta$'s accumulating at $1$, or against stationary policies only would be a different and weaker theorem; the goal rules all of these out.

Needed infrastructure: summation and shifting of the discounted series, Neumann series $(I-\beta Q)^{-1}=\sum_n\beta^nQ^n$ for stochastic $Q$, Cramer's rule to express $(I-\beta Q)^{-1}r$ as a ratio of polynomials in $\beta$, and the fact that a nonzero polynomial has finitely many roots. The policy improvement theorem and the rationality lemma are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. A. Howard, Dynamic Programming and Markov Processes, Technology Press and Wiley, 1960.
• A. F. Veinott Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, 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
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999 (Proposition 6.2.3, Blackwell optimality for finite models). https://doi.org/10.1002/9780470317037

Motivation

Reinforcement learning methods estimate the value function $v_\pi$ of a policy $\pi$: the expected discounted sum of future rewards from each state. When the state space is large, $v_\pi$ cannot be stored as a table and is approximated by a parametrized function. The most studied case is linear function approximation, where each state $s$ carries a feature vector $\mathbf x(s) \in \mathbb R^d$ and the estimate is $\hat v(s, \mathbf w) = \mathbf w^\top \mathbf x(s)$. Temporal-difference learning with this approximation, linear semi-gradient TD(0), is one of the basic algorithms of the field, and Chapter 9 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) presents its analysis: where the algorithm can converge, why that point exists, and how good it is.

The history is short. Sutton (1988, doi:10.1007/BF00115009) introduced TD learning and showed positive definiteness of the matrix governing its expected update. Dayan (1992, doi:10.1007/BF00992701) extended convergence to TD(λ). Tsitsiklis and Van Roy (1997, doi:10.1109/9.580874) proved convergence with probability one for linear TD(λ) under on-policy sampling and bounded the error of the limit. Bradtke and Barto (1996) introduced least-squares TD (LSTD), which computes the same limit directly.

Setting

A finite Markov decision process has finite sets of states $\mathcal S$, actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$, the probability of next state $s'$ and reward $r$ after action $a$ in state $s$. A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. It induces a Markov chain on states with transition matrix $\mathbf P$, $\mathbf P(s, s') = p(s' \mid s) = \sum_a \pi(a \mid s) \sum_r p(s', r \mid s, a)$, and expected one-step reward $r_\pi(s)$. For a discount rate $0 \le \gamma < 1$, the true value is $v_\pi(s) = \sum_{k \ge 0} \gamma^k (\mathbf P^k r_\pi)(s)$, the expected discounted return.

A state distribution $\mu$ is stationary if $\mu^\top \mathbf P = \mu^\top$; write $\mathbf D = \mathrm{diag}(\mu)$. The feature matrix $\mathbf X$ is the $|\mathcal S| \times d$ matrix with rows $\mathbf x(s)$. The mean square value error of a weight vector is

$$\overline{\mathrm{VE}}(\mathbf w) = \sum_{s} \mu(s)\,[v_\pi(s) - \mathbf w^\top \mathbf x(s)]^2 .$$

Linear semi-gradient TD(0) updates $\mathbf w_{t+1} = \mathbf w_t + \alpha(R_{t+1} + \gamma \mathbf w_t^\top \mathbf x_{t+1} - \mathbf w_t^\top \mathbf x_t)\mathbf x_t$. In steady state its expected update involves

$$\mathbf b = \mathbb E[R_{t+1}\mathbf x_t], \qquad \mathbf A = \mathbb E[\mathbf x_t(\mathbf x_t - \gamma \mathbf x_{t+1})^\top],$$

and the TD fixed point is $\mathbf w_{\mathrm{TD}} = \mathbf A^{-1}\mathbf b$. A real square matrix $M$, not necessarily symmetric, is positive definite if $y^\top M y > 0$ for every $y \ne 0$. The key matrix is $\mathbf D(\mathbf I - \gamma\mathbf P)$.

Formalization targets

Goal: the TD fixed point exists and its error bound (9.12), (9.14)

Under the hypotheses above, with every $\mu(s) > 0$ and linearly independent feature columns, $\mathbf A$ is invertible, $\mathbf b = \mathbf A \mathbf w_{\mathrm{TD}}$, and

$$\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}}) \le \frac{1}{1-\gamma}\min_{\mathbf w} \overline{\mathrm{VE}}(\mathbf w).$$

Milestones

1. The expected update (9.13): $\mathbb E[\mathbf w_{t+1} \mid \mathbf w_t] = (\mathbf I - \alpha \mathbf A)\mathbf w_t + \alpha \mathbf b$.
2. The matrix form $\mathbf A = \mathbf X^\top \mathbf D(\mathbf I - \gamma \mathbf P)\mathbf X$.
3. The criterion of Sutton (1988): positive diagonal, nonpositive off-diagonal entries, positive row sums and nonnegative column sums give positive definiteness.
4. The column sums of the key matrix, $\mathbf 1^\top \mathbf D(\mathbf I - \gamma \mathbf P) = (1-\gamma)\mu^\top$.
5. The key matrix and $\mathbf A$ are positive definite.
6. A positive definite $\mathbf A$ is invertible and $\mathbf A^{-1}\mathbf b$ is the unique solution of $\mathbf b = \mathbf A \mathbf w$ (9.12).
7. The Sherman–Morrison update (9.22) of the LSTD inverse $\hat{\mathbf A}_t^{-1}$.

Significance

Positive definiteness of $\mathbf A$ is the reason on-policy linear TD(0) is stable: it makes the expected iteration contract toward the fixed point for small step sizes, and it guarantees that the fixed point exists and is unique. The error bound (9.14) quantifies the price of bootstrapping: the limit of TD can be worse than the best linear approximation, but by at most the factor $1/(1-\gamma)$. The same objects $\mathbf A$, $\mathbf b$ and the key matrix reappear in LSTD, in the analysis of off-policy divergence (Chapter 11 of the book, where $\mathbf D$ is no longer the stationary distribution of $\mathbf P$ and positive definiteness fails), and in gradient-TD methods.

All results here are known. The book gives the positive definiteness argument in a box and cites (9.14) without proof. None of them has a machine-checked proof on the platform; the general Woodbury identity (FamousTheorems.woodbury_identity) is available, and (9.22) is its rank-one case written for the LSTD recursion. The mission produces a formal account of the finite-state theory of linear TD(0), with every hypothesis the book leaves implicit stated.

Difficulty

The key matrix $\mathbf D(\mathbf I - \gamma \mathbf P)$ is not symmetric, so the usual tools for symmetric positive definite matrices do not apply directly, and $\mathbf A$ is positive definite only because of the specific interplay between $\mathbf D$ and $\mathbf P$: if $\mu$ is replaced by a non-stationary distribution the claim is false (this is the off-policy counterexample of Chapter 11). The error bound (9.14) is not a consequence of positive definiteness alone. The TD fixed point is not the minimizer of $\overline{\mathrm{VE}}$, and $\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}})$ has to be compared with the error of the $\mu$-weighted projection of $v_\pi$, which requires controlling $\mathbf P$ in the $\mu$-weighted norm. The book gives no argument for this step.

Formalization scope

The Lean development lives in the namespace SuttonBartoRL.LinearTD. The MDP has four-argument dynamics $p(s', r \mid s, a)$ with a finite reward set and one action set for all states; policies are stochastic. $v_\pi$ is defined from expected discounted returns as the series $\sum_k \gamma^k \mathbf P^k r_\pi$, never from a Bellman equation or from $\mathbf w_{\mathrm{TD}}$. $\mathbf A$ and $\mathbf b$ are defined as the book's steady-state expectations (9.11), as finite sums over $\mu$, $\pi$ and $p$; the matrix form is a milestone, not a definition. Features are a matrix Matrix S (Fin d) ℝ with rows $\mathbf x(s)$; linear independence of its columns is LinearIndependent ℝ Xᵀ. Positive definiteness is a custom predicate $\forall y \ne 0,\ 0 < y^\top M y$, not Mathlib's Matrix.PosDef, which requires symmetry. The minimum in (9.14) is expressed by quantifying over every $\mathbf w$. The matrix inverse is Mathlib's, which is zero on singular matrices; the goal therefore asserts invertibility of $\mathbf A$ explicitly.

Hypotheses the book leaves implicit and the statements make explicit: $0 \le \gamma < 1$ (the continuing case); $\mu$ a stationary distribution of the chain induced by $\pi$ with $\mu(s) > 0$ for every $s$ (otherwise the key matrix is only positive semidefinite); linearly independent feature columns (the book's "degenerate cases", p. 205). The box calls the off-diagonal entries of the key matrix "negative"; they are zero wherever $p(s' \mid s) = 0$, so the criterion is stated with nonpositive entries. The book's sentence that $\varepsilon\mathbf I$ "ensures that $\hat{\mathbf A}_t$ is always invertible" (p. 229) is false in general, because the summands $\mathbf x_k(\mathbf x_k - \gamma \mathbf x_{k+1})^\top$ are not positive semidefinite: with $d = 1$, $\varepsilon = 1/10$, $\gamma = 1/2$, $\mathbf x_0 = 1$, $\mathbf x_1 = 11/5$ one gets $\hat{\mathbf A}_1 = 0$. It is not stated; (9.22) carries invertibility of $\hat{\mathbf A}_{t-1}$ and a nonzero denominator as hypotheses.

A statement in which $v_\pi$ is defined as the solution of the projected equation, or in which $\mathbf A$ is assumed invertible or positive definite, would make the goal trivial or empty; neither is done. Convergence of the stochastic algorithm with probability one is not stated, since the book says it needs conditions and a step-size schedule it does not give. The bound for the episodic case and for other bootstrapping methods (p. 208) is stated only by reference in the book and is not a target.

Useful infrastructure: the $\mu$-weighted inner product and orthogonal projection onto the column space of $\mathbf X$, the non-expansiveness of a stochastic matrix in the norm of its stationary distribution, and the positive definiteness criterion for non-symmetric matrices. All of these are reusable in the off-policy and average-reward chapters of the book. Contributions of these lemmas, and of alternative proofs of the milestones, are welcome.

Selected references

• Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§9.2, 9.4, 9.8.
• Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 1988. doi:10.1007/BF00115009
• John N. Tsitsiklis and Benjamin Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 1997. doi:10.1109/9.580874
• Steven J. Bradtke and Andrew G. Barto, Linear least-squares algorithms for temporal difference learning, Machine Learning 22, 1996. doi:10.1007/BF00114723
• Richard S. Varga, Matrix Iterative Analysis, Prentice-Hall, 1962.

Motivation

A manufacturer that makes one product to stock faces random demand, can produce at most $b$ units per period, and can store at most $U$ units. The classical result without the production limit is that a base-stock policy is optimal: raise inventory to a fixed level $\bar y$ each period. With a production limit, the natural modification is to produce up to $\bar y$ when that is possible and to produce at full capacity otherwise. Federgruen and Zipkin (1986) proved that this modified base-stock (critical-number) policy is optimal under the long-run average-cost criterion, for discrete demand with a general convex cost. Production-capacity models of this type are standard in operations management texts, and the result underlies the computational and comparative-static work that followed, starting with Part II of the same paper, which treats discounted costs.

Timeline.

• 1950s–60s: optimality of base-stock (critical-number) policies for uncapacitated periodic-review models; see Heyman and Sobel's Stochastic Models in Operations Research, Vol. II (1984).
• 1986: Federgruen and Zipkin, Part I (average cost, MOR 11(2):193–207) and Part II (discounted cost, MOR 11(2):208–215) establish the capacitated case. Part I handles the unbounded state space with a general average-cost theory for countable-state Markov decision processes by Federgruen, Schweitzer and Tijms (1983).

Setting

Time is divided into periods $t = 0, 1, \dots$. The demands $D_0, D_1, \dots$ are independent copies of a random variable $D$ with values in $\{0, 1, 2, \dots\}$ and probability mass function $p(j)$; write $\mu = E(D)$ and $P(j) = \Pr\{D \le j\}$. At the start of period $t$ the inventory is an integer $x_t$ (negative values are backorders). The decision maker raises it to

$$y_t \in Y(x_t) = \{y \in \mathbb Z : x_t \le y \le x_t + b,\ y \le U\},$$

pays the expected one-period cost $G(y_t)$, and demand is subtracted: $x_{t+1} = y_t - D_t$. The order cost per unit is set to zero, as in the paper; this loses no generality because every policy with finite average cost has the same average order cost.

The standing assumptions are: $G \ge 0$ is convex and $G(y) \to \infty$ as $|y| \to \infty$ (Assumption 1); the characteristic function of $D$ is analytic at the origin (Assumption 2), and $0 < \mu$; $G(y) \le A + B|y|^\rho$ for some positive integer $\rho$ (Assumption 3); $b > \mu$ and $P(b) < 1$ (Assumption 4). The smallest global minimizer of $G$ is $\bar y^\infty$, and $U \ge \bar y^\infty$.

A Markov policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of maps with $\pi_t(x) \in Y(x)$. The critical-number policy with critical number $\bar y$ is $\delta[\bar y](x) = \max(x, \min(\bar y, x + b))$. A stationary policy $\delta$ is strongly optimal with average cost $g$ if, from every initial state $x \le U$, its average cost $t^{-1}E\{\sum_{i<t} G(y_i)\}$ converges to $g$, while every Markov policy has lim-inf average cost at least $g$ from every initial state.

The analysis uses the operators $Rv(y) = G(y) + E\,v(y - D)$ and $Sv(x) = \min_{y \in Y(x)} Rv(y)$, and the optimality equation

$$g + v(x) = Sv(x),\qquad x \le U. \tag{6}$$

For an interval $\iota = [l, u]$, $H_\iota v(x)$ is the largest expected sum of $v(y_t)$, over policies forced to produce at capacity below $l$ and to produce nothing above $u$, until the inventory first returns to $\iota$.

Formalization targets

Goal: Theorem 1 (p. 202)

There exist $g^*$, $v^*$ and $y^* \ge \bar y^\infty$ such that $(g^*, v^*)$ solves (6), $v^*$ is convex with global minimizer $y^*$, and

$$\delta^* = \delta[y^*] \text{ is strongly optimal with average cost } g^*.$$

The $y^*$ in the optimality claim is the minimizer constructed in part (a).

Milestones

• Lemma 2(a)–(c) (pp. 196–197): a normal-tail inequality and two series estimates.
• Lemma 3 (p. 198): if $v(x) = O(|x|^q)$ then $H_\iota v(x) = O(|x|^{q+3})$.
• Corollary 1 (p. 200): $H_\iota 1 = O(|x|^3)$ and $H_\iota G = O(|x|^{\rho+3})$, both finite.
• Corollary 2 (p. 201): $(t+1)^{-1}P[\delta_{0t}]\cdots P[\delta_{tt}](H_\iota 1 + H_\iota G)(x) \to 0$.
• Lemma 4 (p. 201): reachability of every state in $[L, U - D_-]$ under some policy that produces at capacity below $L$.
• Lemma 5 (p. 202): $S$ and $Q$ preserve the class $V$ of convex functions of growth $O(|x|^{\rho+3})$ that are nonincreasing below $\bar y^\infty$.

Significance

The result. Theorem 1 reduces an infinite-state average-cost control problem to a one-parameter search over critical numbers. The paper then evaluates the average cost of $\delta[\bar y]$ by a renewal formula, proves it convex in $\bar y$ (Theorem 2), and in §5 extends optimality to unlimited storage. The strong form of optimality matters: it compares with every Markov policy from every starting state, and it compares lim-infs, not only lim-sups.

Formalizing it. The theorem has a published proof, but no machine-checked one, and its proof relies on external results that are themselves unformalized: the countable-state average-cost theory of Federgruen, Schweitzer and Tijms, a fixed-point theorem on a compact convex subset of a product space, and a large-deviation estimate quoted from Feller. A formal development produces reusable infrastructure: expected first-passage sums for integer-valued random walks with a reflecting control, polynomial moment bounds for them, and the convexity-preservation argument for capacitated value iteration.

Difficulty

The state space is unbounded below, so the finite-state theory of average-cost Markov decision processes does not apply, and the one-period cost is unbounded. The obvious approach, letting the discount factor tend to one in the discounted problem, needs uniform bounds on relative value functions. Those bounds come from the expected cost until the inventory returns to a fixed interval, and with capacity limits that expectation must be controlled with growth $O(|x|^{\rho+3})$ uniformly over a class of policies. This is the content of Lemma 3, whose proof combines a large-deviation estimate for the demand sums with a renewal-type recursion. A second obstacle is strong optimality: comparing with policies whose lim-inf average cost is smaller requires that the relative value function grows sublinearly along every admissible trajectory (Corollary 2).

Formalization scope

All objects are in the namespace FedergruenZipkin.AvgCost, defined in one file. States $x, y$ and the capacity $U$ are integers; demands are natural numbers with a real probability mass function p; $b$ is a positive natural number. Convexity on $\mathbb Z$ is the second-difference inequality. Expectations of a real function are series $\sum_j p(j)\,v(y-j)$; expected policy costs and hitting sums are $[0,\infty]$-valued and need no integrability side condition. Feasibility and all properties of value functions are required only on states $x \le U$, which are the only states visited. Assumption 2 is stated literally, as real-analyticity of $\theta \mapsto \sum_j p(j)e^{i\theta j}$ at $0$. The order cost is zero, as in the paper. $\bar y^\infty$ is a parameter characterised as the least minimizer of $G$, not an infimum.

"Strongly optimal" has no displayed definition in the paper; it is read from eq. (7) in the proof of Theorem 1(b): convergence of the average cost of $\delta^*$ to $g^*$ from every state, together with a lim-inf lower bound for every Markov (memoryless, possibly nonstationary) policy from every state. The class is neither widened to history-dependent policies nor narrowed to stationary ones. The goal additionally records that $E\,v^*(y-D)$ converges, that $v^*$ has growth $O(|x|^{\rho+3})$, and that $g^* \ge 0$; all three follow from the paper's proof.

A trivializing reading is ruled out: the existence of $g$, $v$ and $y^*$ is one existential, so $y^*$ cannot be decoupled from the solution of (6), and strong optimality includes the convergence of $\delta^*$'s own average cost to $g^*$, so $g = 0$ does not satisfy it vacuously.

Not posed: Lemma 1 (quoted from Feller, and replaceable by a Chernoff bound); the renewal formulas (10)–(11) and Theorem 2; and §5 (unlimited storage). Useful contributions include a formal theory of expected hitting sums for skip-free-upward random walks, and a proof of Lemma 3 by any route.

Selected references

• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands I. The Average-Cost Criterion, Mathematics of Operations Research 11(2):193–207, 1986. https://doi.org/10.1287/moor.11.2.193
• A. Federgruen and P. Zipkin, An Inventory Model with Limited Production Capacity and Uncertain Demands II. The Discounted-Cost Criterion, Mathematics of Operations Research 11(2):208–215, 1986. https://doi.org/10.1287/moor.11.2.208
• A. Federgruen, P. J. Schweitzer and H. C. Tijms, Denumerable Undiscounted Semi-Markov Decision Processes with Unbounded Rewards, Mathematics of Operations Research 8(2):298–314, 1983. https://doi.org/10.1287/moor.8.2.298
• D. P. Heyman and M. J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

Temporal-difference (TD) learning estimates the value of a policy by moving a current estimate toward a target built from observed rewards and from the estimate itself. Chapter 7 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) interpolates between the two extreme targets of the preceding chapters: the one-step TD target, which uses one reward and then bootstraps, and the Monte Carlo target, which uses every reward until the end of the episode. The intermediate target, the $n$-step return, uses $n$ rewards and then bootstraps from the current estimate. The family underlies $n$-step TD, $n$-step Sarsa, the off-policy per-decision methods and the tree-backup algorithm, and it is the introduction to eligibility traces (Chapter 12).

The book justifies the whole family with one inequality, the error reduction property (7.3), p. 144: the expected $n$-step return is closer to the true value than the estimate it bootstraps from, by a factor $\gamma^n$ in the worst state. It is the reason given for calling $n$-step TD methods "sound". The same chapter states, mostly as exercises without solutions, a series of exact identities that rewrite each kind of $n$-step return as a sum of one-step TD errors.

Setting

A finite Markov decision process has finite state and action sets $\mathcal S$, $\mathcal A$, a finite reward set $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$, the probability of next state $s'$ and reward $r$ after action $a$ in state $s$ (Eqs. (3.2)–(3.3)). A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. Following $\pi$ from $S_t = s$ produces a random trajectory $A_t, R_{t+1}, S_{t+1}, A_{t+1}, R_{t+2}, \dots$ For a discount factor $0 \le \gamma < 1$ the state-value function is the expected discounted return (3.12),

$$v_\pi(s) = \mathbb E_\pi\Big[\sum_{k=0}^{\infty} \gamma^k R_{t+k+1} \,\Big|\, S_t = s\Big].$$

Given any function $V : \mathcal S \to \mathbb R$ (an estimate of $v_\pi$), the $n$-step return (7.1) is

$$G_{t:t+n} = R_{t+1} + \gamma R_{t+2} + \cdots + \gamma^{n-1} R_{t+n} + \gamma^n V(S_{t+n}).$$

In an episode that terminates at time $T$ it is replaced by the complete return $G_t$ when $t + n \ge T$. The TD error (6.5) is $\delta_k = R_{k+1} + \gamma V(S_{k+1}) - V(S_k)$. Off-policy variants use a behavior policy $b$ that generates the data, the per-decision ratio $\rho_t = \pi(A_t \mid S_t)/b(A_t \mid S_t)$, and the return with control variate (7.13), $G_{t:h} = \rho_t(R_{t+1} + \gamma G_{t+1:h}) + (1-\rho_t) V(S_t)$, $G_{h:h} = V(S_h)$. The tree-backup return (7.15)–(7.16) uses action values $Q$ and the expected approximate value $\bar V(s) = \sum_a \pi(a \mid s) Q(s, a)$ (7.8).

Formalization targets

Goal: the error reduction property (7.3)

For a finite MDP, a policy $\pi$, $0 \le \gamma < 1$, any $V : \mathcal S \to \mathbb R$ and every $n \ge 1$,

$$\max_s \big|\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s)\big| \le \gamma^n \max_s \big|V(s) - v_\pi(s)\big|.$$

Milestones, in the book's order

1. Exercise 7.1, p. 143: with $V$ fixed and $V(S_T) = 0$, $G_{t:t+n} - V(S_t) = \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}\delta_k$.
2. Exercise 7.4, Eq. (7.6), p. 148: the $n$-step Sarsa return equals $Q_{t-1}(S_t, A_t) + \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}[R_{k+1} + \gamma Q_k(S_{k+1}, A_{k+1}) - Q_{k-1}(S_k, A_k)]$, with estimates changing from step to step.
3. Eq. (7.12), p. 150: $G_{t:h} = R_{t+1} + \gamma G_{t+1:h}$ for $t < h < T$, $G_{h:h} = V(S_h)$.
4. Exercise 7.6, p. 151, for (7.13): under coverage, $\mathbb E_b$ of the control-variate return equals $\mathbb E_b$ of the same return without the control variate, and both equal $\mathbb E_\pi[G_{t:t+n} \mid S_t = s]$.
5. Exercise 7.8, p. 151: $G_{t:h} - V(S_t) = \sum_{k=t}^{h-1} \gamma^{k-t} \big(\prod_{i=t}^{k}\rho_i\big) \delta_k$ for the return (7.13).
6. Exercise 7.11, p. 153: the tree-backup return equals $Q(S_t, A_t) + \sum_{k=t}^{\min(t+n-1,T-1)} \delta_k \prod_{i=t+1}^{k} \gamma\pi(A_i \mid S_i)$ with the expectation-based TD error $\delta_k = R_{k+1} + \gamma\bar V(S_{k+1}) - Q(S_k, A_k)$.

Significance

The result. The error reduction property makes the expected $n$-step target a $\gamma^n$-contraction toward $v_\pi$ in the sup norm, uniformly over the estimate it starts from. It is the one-line reason the book offers for the soundness of every $n$-step TD method, and the same contraction is what the $\lambda$-return of Chapter 12 averages over $n$. The TD-error identities are the algebra behind implementations that accumulate TD errors instead of storing returns, and behind the forward/backward-view equivalences of Chapter 12. Exercise 7.6 is the unbiasedness of the control-variate return, which is what allows (7.13) to replace plain importance weighting without changing the expected update.

Formalizing it. All results are elementary and well known, but the book gives no proofs: (7.3) is asserted, and the identities are exercises without published solutions. None is formalized on Prove2Me. The mission produces machine-checked versions with every hypothesis explicit (discounting, the fixed estimate, terminal values, coverage), and a trajectory-level expectation for finite MDPs that other chapters of the series can reuse.

Difficulty

The obvious proof of (7.3) is a matrix computation: $\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s) = \gamma^n (P_\pi^n (V - v_\pi))(s)$, and a stochastic matrix does not increase the sup norm. The difficulty lies in the step before it. The left side is an expectation over trajectories, and $v_\pi$ is an infinite discounted series; neither is a matrix power by definition. Connecting them requires a Chapman–Kolmogorov identity for the finite-trajectory distribution induced by $\pi$ and $p(s', r \mid s, a)$, the splitting of $v_\pi$ at time $n$, and summability of the discounted series. Defining the expected $n$-step return as the matrix expression would reduce the goal to the last line and remove its content; that shortcut is ruled out below.

The TD-error identities are telescoping sums, but each has its own boundary: termination inside the $n$ steps, the convention that terminal states have value zero, the index $Q_{-1}$ at $t = 0$ in (7.6), the special case $G_{T-1:t+n} = R_T$ of the tree backup, and ratios with vanishing denominators in (7.13).

Formalization scope

• Model. The finite MDP, policies and $v_\pi$ follow the series conventions: dynamics $p(s', r \mid s, a)$ over a finite reward set, one action set for all states, $v_\pi(s) = \sum_k \gamma^k (P_\pi^k r_\pi)(s)$ computed from expected rewards and never defined as a Bellman solution.
• Expectations are over trajectories. $\mathbb E_\pi[\,\cdot \mid S_t = s]$ is the finite sum over $n$-step segments $(A_{t+k}, S_{t+k+1}, R_{t+k+1})_{k<n}$ weighted by $\prod_k \pi(A_{t+k}\mid S_{t+k})\,p(S_{t+k+1}, R_{t+k+1}\mid S_{t+k}, A_{t+k})$. The expected $n$-step return is not defined as $\sum_{k<n}\gamma^k P_\pi^k r_\pi + \gamma^n P_\pi^n V$, which would make the goal a two-line matrix inequality.
• The estimate is fixed. In the algorithm, $V_{t+n-1}$ is the current random estimate. Every statement takes a fixed function $V$ (or $Q$), which is the book's own reading ("if the value estimates don't change"). The only exception is Exercise 7.4, whose estimates $Q_k$ are indexed by time $k \in \mathbb Z$ exactly as in (7.6).
• Discounting. The goal assumes $0 \le \gamma < 1$ and takes the maximum over all states. Episodic tasks enter through absorbing zero-reward terminal states. The undiscounted episodic case $\gamma = 1$ is not stated.
• Episodes. Sample-path identities use sequences $S_k, A_k, R_k$ and a termination time $T$. The book's convention that terminal states have value $0$ is a hypothesis ($V(S_T) = 0$, $Q(S_T, \cdot) = 0$).
• Exercise 7.6 is stated for the state-value return (7.13) of p. 150, although the exercise follows the action-value return (7.14). Its conclusion includes, besides the literal "does not change the expected value", equality with the on-policy expected return, the property the book states on p. 150. Coverage ($\pi(a\mid s) > 0 \Rightarrow b(a\mid s) > 0$) is assumed.
• Not stated. The convergence of $n$-step TD methods "under appropriate technical conditions" (p. 144), and the programming exercises.

Needed infrastructure: finite sums over function types, Chapman–Kolmogorov for the segment distribution, summability of $\sum_k \gamma^k P_\pi^k r_\pi$. The trajectory layer is reusable for the importance-sampling and eligibility-trace chapters. Alternative proofs of the goal, and proofs of the undiscounted episodic version as a separate theorem, are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 7, pp. 141–158. http://incompleteideas.net/book/the-book-2nd.html
• C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989 (the $n$-step return and its error reduction property, as credited on p. 158 of the book). https://www.cs.rhul.ac.uk/~chrisw/new_thesis.pdf
• D. Precup, R. S. Sutton and S. Singh, Eligibility traces for off-policy policy evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (the tree-backup algorithm, as credited on p. 158 of the book; no DOI).