Probability

Why average cost on finite state spaces

Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a $\limsup$ of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.

The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$, a finite nonempty action set $A_i$ in each state $i$, nonnegative finite costs $C(i,a)$, and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$. A policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$ that may depend on the whole history $h_t = (i_0,a_0,\ldots,i_t)$. A stationary policy $f$ always chooses a fixed action $f(i) \in A_i$ in state $i$.

With $X_t, A_t$ the state and action at time $t$ and $X_0 = i$, define

• the discounted cost $V_{\theta,\alpha}(i) = \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t)]$ for $0<\alpha<1$, and the discounted value function $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$;
• the $n$ horizon cost $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t)]$;
• the average cost $J_\theta(i) = \limsup_n v_{\theta,n}(i)/n$, its $\liminf$ version $J^*_\theta(i)$, and the minimum average cost $J(i) = \inf_\theta J_\theta(i)$.

All infima range over all general policies, and every quantity may equal $+\infty$. A policy is $\alpha$ discount optimal if $V_{\theta,\alpha} = V_\alpha$, and average cost optimal if $J_\theta = J$.

For a stationary policy $f$ on a finite state space, the induced Markov chain splits into positive recurrent classes $R_1,\ldots,R_K$ and transient states. With $p_k(i)$ the probability of reaching $R_k$ from $i$, distinguished states $z_k \in R_k$, and $W_\alpha(i) = \sum_k p_k(i) V_\alpha(z_k)$, the relative value function is $w_\alpha(i) = V_\alpha(i) - W_\alpha(i)$.

Formalization targets

Goal: Proposition 6.2.3

For an MDC with a finite state space there are $\alpha_0 \in (0,1)$ and one stationary policy $f$ such that $f$ is $\alpha$ discount optimal for every $\alpha \in (\alpha_0,1)$, $f$ is average cost optimal, and

$$J(i) = \lim_{\alpha\to 1^-} (1-\alpha) V_\alpha(i) = \lim_{n\to\infty} \frac{v_{f,n}(i)}{n}, \qquad i \in S.$$

Milestones

1. Proposition 4.5.3. For finite $S$ and stationary $e$, $\alpha \mapsto V_{e,\alpha}(i)$ is a finite, continuous, rational function on $(0,1)$.
2. Proposition 6.1.1. For every policy on a countable state space,

$$J^*_\theta(i) \le \liminf_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le \limsup_{\alpha\to1^-}(1-\alpha)V_{\theta,\alpha}(i) \le J_\theta(i),$$

with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite $S$ and stationary $e$, $J_e(i) = \lim_{\alpha\to1^-}(1-\alpha)V_{e,\alpha}(i) = \lim_n v_{e,n}(i)/n$. 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of $V_{\theta,\alpha}$ in $\alpha$; monotonicity and left continuity of $V_\alpha$; continuity under bounded costs. 5. Theorem 6.3.1. For the policy $f$ of the goal, $\lim_{\alpha \to 1^-} w_\alpha(i) = w(i)$ exists, and

$$J(i) + w(i) = C(i,f) + \sum_j P_{ij}(f) w(j) \ \ge\ \min_{a} \Big\{C(i,a) + \sum_j P_{ij}(a) w(j)\Big\},$$

together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. $V_\alpha(i) = J(i)/(1-\alpha) + w^*(i) + \varepsilon_\alpha(i)$ with $\varepsilon_\alpha(i) \to 0$ as $\alpha \to 1^-$.

Significance

The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.

The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.

Difficulty

The obvious argument picks, for each $\alpha$, a stationary discount optimal policy $f_\alpha$ and lets $\alpha \to 1$. Finiteness of the set of stationary policies gives one policy that is optimal along some sequence $\alpha_n \to 1$, but not on an interval. Excluding infinite switching between two policies requires the analytic structure of $\alpha \mapsto V_{f,\alpha}(i)$ (Proposition 4.5.3), which in turn rests on matrix inversion of $I - \alpha P$. Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.

Formalization scope

• States form a type S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.
• A general policy is a function of the list of past state-action pairs (most recent first) and the current state, giving a distribution on A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.
• $V_{\theta,\alpha}$, $V_\alpha$, $v_{\theta,n}$, $J_\theta$, $J^*_\theta$, $J$ are in ℝ≥0∞, so $+\infty$ is represented. $\alpha \to 1^-$ is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 ($w_\alpha$, $w$, $w^*$, equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.
• The objects of Section 6.3 ($p_k$, $m_{i|k}$, $c_{i|k}$, $\pi_s$, $W_\alpha$) are defined from $f$. The distinguished states are a hypothesis quantified over.
• A trivializing formalization would take the infimum over stationary policies only, let the optimal policy depend on $\alpha$, or state rationality as an equation p/q without requiring $q \ne 0$. Each is excluded here: $J$ and $V_\alpha$ are infima over all general policies, one pair $(\alpha_0,f)$ is quantified before all $\alpha$, and the denominator is required to be nonzero on $(0,1)$.

Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent $(I-\alpha P)^{-1}$ of a stochastic matrix, the Abelian inequality for $[0,\infty]$-valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
• D. Blackwell, "Discrete dynamic programming", Annals of Mathematical Statistics 33 (1962), 719–726. https://doi.org/10.1214/aoms/1177704593
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).

Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.

Timeline of the underlying theory:

• 1965. Blackwell (Ann. Math. Statist. 36) establishes the discounted theory with bounded rewards.
• 1966. Strauch (Ann. Math. Statist. 37) treats "negative" dynamic programming, the case of nonpositive rewards (equivalently nonnegative costs), with no boundedness assumption.
• 1977–1978. Bertsekas (SIAM J. Control Optim. 15) and Bertsekas and Shreve (Stochastic Optimal Control: The Discrete-Time Case) give the abstract monotone-mapping framework covering both cases.
• 1999. Sennott's text states the countable-state, finite-action, nonnegative-cost discounted theory in the form used for queueing control, with general history-dependent randomized policies.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$; for each state $i$ a finite nonempty action set $A_i$; for each $a \in A_i$ a nonnegative finite cost $C(i,a)$ and a probability distribution $(P_{ij}(a))_{j \in S}$ of the next state. A policy $\theta$ chooses the action at time $n$ at random from a distribution $\theta(\cdot \mid h_n)$ on $A_{i_n}$ that may depend on the entire history $h_n = (i_0, a_0, \dots, a_{n-1}, i_n)$. A stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$; for it one writes $C(i,f) = C(i,f(i))$ and $P_{ij}(f) = P_{ij}(f(i))$.

Fix a discount factor $\alpha \in (0,1)$. For an initial state $i$ and a policy $\theta$, the $n$-horizon cost with terminal cost zero and the infinite horizon discounted cost are

$$v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i], \qquad V_{\theta,\alpha}(i) = \sum_{t=0}^{\infty} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i],$$

and the value functions are $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ and $V_\alpha(i) = \inf_\theta V_{\theta,\alpha}(i)$, infima over all policies. All of these lie in $[0,\infty]$. A policy is discount optimal if $V_{\theta,\alpha} = V_\alpha$. The discount optimality equation is

$$W(i) = \min_{a \in A_i} \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) W(j) \Big\}, \qquad i \in S. \tag{4.9}$$

With $W = V_\alpha$, $B_i(\alpha)$ denotes the set of actions attaining the minimum at $i$.

Formalization targets

Goal: Theorem 4.1.4

$V_\alpha$ solves (4.9); every $W : S \to [0,\infty]$ solving (4.9) satisfies $V_\alpha \le W$; and every stationary policy $f_\alpha$ with

$$C(i,f_\alpha) + \alpha \sum_j P_{ij}(f_\alpha) V_\alpha(j) = \min_a \Big\{ C(i,a) + \alpha \sum_j P_{ij}(a) V_\alpha(j) \Big\} \quad \text{for all } i$$

is discount optimal. No boundedness of costs and no finiteness of $V_\alpha$ is assumed.

Milestones

In attack order: Lemma 4.1.1 ($v_{\theta,\alpha,n} \uparrow V_{\theta,\alpha}$); Proposition 4.1.2 (a supersolution of the one-policy equation dominates $v_{e,\alpha,n} + \alpha^n E_e[W(X_n)]$ and $V_{e,\alpha}$); Corollary 4.1.3 (a supersolution of the optimality inequality dominates $V_{f,\alpha} \ge V_\alpha$); then, beyond the goal, Corollary 4.1.5 ($\alpha^n E_{f_\alpha}[V_\alpha(X_n) \mid X_0 = i] \to 0$ where $V_\alpha(i) < \infty$), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals $V_\alpha$), Proposition 4.3.1 ($v_{\alpha,n} \uparrow V_\alpha$, and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets $B_{i}(\alpha)$ along histories of positive probability).

Significance

Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies $V_\alpha$ among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting $\alpha \to 1$. Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.

These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.

Difficulty

The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and $V_\alpha$ can equal $+\infty$ at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in $[0,\infty]$, where finite-valued arguments do not transfer verbatim.

Formalization scope

The Lean development lives in the namespace SennottDP.Discounted. Conventions:

• The state space is a type S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.
• A history at time $n$ is a pair Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.
• All values ($v_{\theta,\alpha,n}$, $V_{\theta,\alpha}$, $v_{\alpha,n}$, $V_\alpha$, and the competing solutions $W$) are ℝ≥0∞-valued; $0 \cdot \infty = 0$. The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.
• $V_\alpha$ and $v_{\alpha,n}$ are infima over the type of all general policies. Defining them over stationary policies only would make the optimality of $f_\alpha$ a tautology; that formalization is ruled out.
• Proposition 4.4.1: the book states the equivalence without a finiteness assumption, but its necessity argument needs $V_\alpha < \infty$, and necessity fails otherwise. Sufficiency is stated in general and necessity under $V_\alpha < \infty$ everywhere.

Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation $E_f[W(X_{n+1})] = E_f[\sum_j P_{X_n j}(f) W(j)]$ for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999, Chapter 4. https://doi.org/10.1002/9780470317037
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM Journal on Control and Optimization 15 (1977), 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.

This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.

Setting

A Markov decision chain $\Delta$ has a countable state space $S$; for each $i \in S$ a finite nonempty action set $A_i$; a finite cost $C(i,a) \ge 0$; and for each $a \in A_i$ a transition distribution $(P_{ij}(a))_{j \in S}$. A history at time $t$ is $h_t = (i_0, a_0, \dots, i_{t-1}, a_{t-1}, i_t)$, and a general policy $\theta$ chooses the action at time $t$ from a distribution $\theta(\cdot \mid h_t)$ on $A_{i_t}$: it may use the whole history and may randomize. Stationary policies $f$ ($f(i) \in A_i$) and deterministic Markov policies (a stationary policy for each time) are special cases.

Fix a finite terminal cost $F \ge 0$ and a discount factor $0 < \alpha \le 1$ ($\alpha = 1$ is the undiscounted case). The $n$ horizon expected discounted cost of $\theta$ from initial state $i$ is

$$v_{\theta,\alpha,n}(i) = \sum_{t=0}^{n-1} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i] + \alpha^n E_\theta[F(X_n) \mid X_0 = i],$$

and the value function is $v_{\alpha,n}(i) = \inf_\theta v_{\theta,\alpha,n}(i)$ over all general policies. Both may be $+\infty$. A policy is optimal for the $n$ horizon if it attains $v_{\alpha,n}(i)$ at every $i$. For $n \ge 1$ put $u_{\alpha,n}(i,a) = C(i,a) + \alpha \sum_j P_{ij}(a) v_{\alpha,n-1}(j)$ and let $B_i(\alpha,n)$ be the set of $a \in A_i$ minimizing it.

An approximating sequence $(\Delta_N)_{N \ge N_0}$ has finite nonempty state spaces $S_N$ increasing to $S$, the same actions and costs, and transition distributions $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$ as $N \to \infty$. Its value functions are $v^N_{\alpha,n}$. In an augmentation type approximating sequence, the probability $P_{ir}(a)$ of leaving $S_N$ to $r$ is redistributed over $S_N$ by an augmentation distribution $q_j(i,a,r,N)$. Assumption FH($\alpha$, $n$) requires $\limsup_N v^N_{\alpha,n}(i)$ to be finite and at most $v_{\alpha,n}(i)$ for every $i$. A stationary policy $e$ is a limit point of stationary policies $e^N$ if, along a subsequence, $e^{N_r}(i) = e(i)$ eventually for each $i$.

Formalization targets

Goal: Theorem 3.2.3

For fixed $n \ge 1$,

$$\Big(\forall i:\ \lim_{N\to\infty} v^N_{\alpha,n}(i) = v_{\alpha,n}(i) < \infty\Big) \iff \mathrm{FH}(\alpha,n),$$

and under either condition every limit point $e_n$ of stationary policies $e^N_n$ with $e^N_n(i) \in B^N_i(\alpha,n)$ satisfies $e_n(i) \in B_i(\alpha,n)$ for all $i \in S$.

Milestones

1. Proposition A.1.1: a probability average of $u$ is at least $\min u$, with equality iff the distribution is concentrated on the minimizers.
2. Theorem 3.1.2: the finite horizon optimality equation $v_{\alpha,n}(i) = \min_a u_{\alpha,n}(i,a)$, and the characterization of all optimal general policies.
3. Corollary 3.1.4: choosing $f_{n-t}(i) \in B_i(\alpha,n-t)$ yields an optimal deterministic Markov policy.
4. Proposition 2.5.6: the augmentation (2.19) defines an approximating distribution.
5. Lemma 3.2.2: $v^N_{\alpha,0} \to v_{\alpha,0}$ and $\liminf_N v^N_{\alpha,n} \ge v_{\alpha,n}$.
6. Propositions B.3 and B.5: sequences of stationary policies, for $\Delta$ or for $(\Delta_N)$, have limit points.
7. Propositions 3.3.1, 3.3.2 and 3.3.4: three sufficient conditions for FH($\alpha$, $n$), namely bounded costs, an augmentation sending excess probability to a finite set, and the augmentation inequality (3.20).

Significance

Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.

Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.

The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.

Difficulty

The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.

For approximating sequences, the natural idea is to pass to the limit in the optimality equation of $\Delta_N$. This fails in general. Example 3.2.1 of the book has $\lim_N v^N_{1,2}(0) = 2 > 1 = v_{1,2}(0)$, because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.

Formalization scope

The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities $\prod \theta(a_s \mid h_s) P_{i_s i_{s+1}}(a_s)$, which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies $0 < \alpha \le 1$ in every statement. An approximating sequence is indexed by $N \in \mathbb N$ with a start level $N_0$; its value functions are set to $0$ for the finitely many $N$ at which a given state is not yet in $S_N$, which does not affect limits.

The optimality equation must not be made definitional by defining $v_{\theta,\alpha,n}$ or $v_{\alpha,n}$ through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard $v_{\alpha,n}(i) < \infty$; the book omits it, and without it the "only if" direction is false (see the item's note).

A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance $v_{\theta,\alpha,0} = F$).

Selected references

• Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
• Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (the standard reference for finite horizon dynamic programming with history-dependent randomized policies).
• Richard Bellman, Dynamic Programming, Princeton University Press, 1957.

Motivation

Optimal transport asks for the cheapest way to move one distribution of mass onto another. Monge posed the problem in 1781 for maps; Kantorovich (1942) relaxed it to transference plans (couplings), turning it into an infinite-dimensional linear program with a dual: maximize the total revenue $\int\psi\,d\mu+\int\varphi\,d\nu$ of pickup and delivery prices that never exceed the cost, $\psi(x)+\varphi(y)\le c(x,y)$. The equality of the two values — Monge–Kantorovich duality — underlies much of modern optimal transport, with uses in economics (matching markets, principal–agent problems), probability, and PDE.

This mission formalizes the duality theorem and its proof as presented in Colin Yao, Monge–Kantorovich and Transportation Theory (paper dated September 10, 2023), whose proof follows Villani's Optimal Transport: Old and New and, for the weak inequality, Galichon's Optimal Transport Methods in Economics.

Setting

$X$ and $Y$ are Polish spaces (separable, completely metrizable) with their Borel σ-algebras; $\mu$ and $\nu$ are Borel probability measures on $X$ and $Y$; $c : X\times Y\to[0,\infty)$ is a continuous cost function.

• A transference plan is a probability measure $\pi$ on $X\times Y$ with marginals $\mu$ and $\nu$; $\Pi(\mu,\nu)$ denotes the set of such plans.
• The Kantorovich problem is $\min_{\pi\in\Pi(\mu,\nu)}\int c\,d\pi$.
• The dual problem is $\sup\{\int\psi\,d\mu+\int\varphi\,d\nu\}$ over bounded continuous $\psi,\varphi$ with $\psi(x)+\varphi(y)\le c(x,y)$ everywhere.
• A set $\Gamma\subseteq X\times Y$ is $c$-cyclically monotone if $\sum_{i=1}^N c(x_i,y_i)\le\sum_{i=1}^N c(x_i,y_{i+1})$ (with $y_{N+1}=y_1$) for all finite families of points of $\Gamma$; a plan is $c$-cyclically monotone if it is concentrated on such a set.
• The $c$-conjugate of $\psi$ is $\psi^c(y)=\inf_x(c(x,y)-\psi(x))$; $\psi$ is $c$-concave if $\psi(x)=\inf_y(c(x,y)-\varphi(y))$ for some $\varphi$; its $c$-subdifferential is $\partial_c\psi=\{(x,y):\psi^c(y)+\psi(x)=c(x,y)\}$.

Formalization targets

Goal (Theorem 4.1)

$$\min_{\pi\in\Pi(\mu,\nu)}\int_{X\times Y}c\,d\pi=\sup_{\substack{\psi\in C_b(X),\ \varphi\in C_b(Y)\\ \psi(x)+\varphi(y)\le c(x,y)}}\Big(\int_X\psi\,d\mu+\int_Y\varphi\,d\nu\Big),$$

including existence of a minimizing plan; the common value may be $+\infty$.

Milestones (in the order of the source)

1. Weak duality, inequality (3.1): $\inf\ge\sup$.
2. Proposition 4.4: a $c$-cyclically monotone plan exists between uniform empirical measures.
3. Lemma 4.16: plans with marginals in tight families form a tight family.
4. Proposition 4.17: a $c$-cyclically monotone plan exists for general marginals.
5. Proposition 4.22: the support of a $c$-cyclically monotone plan lies in $\partial_c\psi$ for a $c$-concave $\psi$ (bounded $c$).
6. Theorem 4.25: $(\psi^c)^c=\psi$ for $c$-concave $\psi$.
7. Proposition 4.31: duality for bounded continuous $c$.
8. Theorem 4.32: $\int f\,d\mu=\int f\,d\pi$ for a plan with marginal $\mu$.

Significance

Duality converts a minimization over measures into a maximization over functions; it characterizes optimal plans by the complementary-slackness condition that they are concentrated on $\{\psi(x)+\varphi(y)=c(x,y)\}$, and it is the entry point to Brenier's theorem, the Kantorovich–Rubinstein formula for the Wasserstein-1 distance, and the economic applications discussed in Section 5 of the source. The result is classical and proved in the literature; the work here is to formalize the known proof and to supply reusable infrastructure (couplings, $c$-cyclical monotonicity, $c$-transforms) on top of Mathlib's measure theory.

Difficulty

The weak inequality is a short integration argument; the reverse inequality is where the work lies. Finite-dimensional linear-programming duality does not pass to general measures directly: one must produce a cyclically monotone plan as a limit of discrete approximations (tightness and Prokhorov's theorem, closedness of the cyclic-monotonicity condition under weak convergence), build a potential $\psi$ from chains of cost differences, and control measurability and integrability of $\psi$ and $\psi^c$. Passing from bounded to unbounded nonnegative costs requires an additional approximation argument, which the source only sketches (Section 4.5).

Formalization scope

Lean namespace MongeKantorovichYao; one definition file provides transference plans, $c$-cyclical monotonicity, $c$-conjugates, $c$-concavity and $c$-subdifferentials. Conventions: marginals are pushforwards along the projections; $c$-conjugates are extended-real infima (no default values); the transport cost in the goal is the $[0,\infty]$-valued integral of the nonnegative cost, and both sides of the goal are compared in the extended reals, so the infinite-cost case is included and no integrability hypothesis is added. The dual side ranges over bounded continuous functions with the constraint imposed at every point. Proposition 4.22 is stated for bounded $c$ (as used in Proposition 4.31), since with unbounded costs a real-valued potential need not exist. Infrastructure that may be missing from Mathlib: Prokhorov-type compactness of tight families of probability measures, weak convergence of empirical measures, and lower semicontinuity of $\pi\mapsto\int c\,d\pi$.

Selected references

• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• A. Galichon, Optimal Transport Methods in Economics, Princeton University Press, 2016.
• L. V. Kantorovich, On the translocation of masses, Dokl. Akad. Nauk SSSR 37 (1942).

Motivation

Two-stage stochastic integer programs combine the two hardest features of mathematical programming: uncertainty in the data and integrality of the decisions. Even evaluating the objective of such a program at a single first-stage decision requires the expected optimal value of an NP-hard combinatorial problem. Chapter 8 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by A. H. G. Rinnooy Kan and L. Stougie, argues that for many such problems the way forward is probabilistic analysis: the random optimal value of the second-stage problem often converges, after normalization, to a simple function of the problem parameters, and that function can replace the intractable expectation.

The chapter illustrates this on the machine investment problem: first buy $m$ identical machines at cost $c$ each, knowing only the distribution of the processing times of $n$ jobs, then schedule the jobs once their processing times are revealed so as to minimize the makespan. This mission formalizes the chapter's analysis of that example: the almost sure asymptotics of the optimal makespan (8.13), its expectation version, and the asymptotic clairvoyance of the resulting two-stage heuristic.

Setting

Let $p_1, p_2, \dots$ be processing times: independent, identically distributed, nonnegative random variables on a probability space $(\Omega, \mathcal F, P)$ with mean $\mu = \mathbb E p_1 > 0$ and finite second moment $\mathbb E p_1^2 < \infty$. The instance with $n$ jobs uses the first $n$ of them.

An assignment of the $n$ jobs to $m \ge 1$ identical machines is a map $\sigma : \{1, \dots, n\} \to \{1, \dots, m\}$. The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ and the makespan of $\sigma$ is its largest load. The minimum makespan is

$$C^*_n(m) = \min_{\sigma} \max_{i=1,\dots,m} \sum_{j:\ \sigma(j) = i} p_j ,$$

and the machine investment problem is to minimize $Z_n(m) = cm + \mathbb E\, C^*_n(m)$ over integers $m$ (8.9).

List scheduling takes the jobs in the order $1, \dots, n$ and assigns each to the first available machine, a machine of least current load (lowest index on ties). Its makespan is $C^H_n(m)$. Write $S_n = \sum_{j=1}^n p_j$ and $p_{\max} = \max_{j \le n} p_j$.

For §8.3, the estimate $Z'_n(m) = cm + n\mu/m$ is minimized over integers by the heuristic first-stage decision $m^{H1}_n$, the better of $\lfloor\sqrt{n\mu/c}\rfloor$ and $\lceil\sqrt{n\mu/c}\rceil$. A clairvoyant decision maker who sees the processing times first chooses $m^\circ_n(\omega) \ge 1$ minimizing $cm + C^*_n(m)$.

Formalization targets

Goal: Eq. (8.13)

For machine counts $m = m(n) \ge 1$ with $m(n) = O(\sqrt n)$,

$$P\Bigl\{ \lim_{n\to\infty} \frac{C^*_n(m)}{n\mu/m} = 1 \Bigr\} = 1 .$$

The machine count is allowed to grow with $n$; this is the regime the first-stage heuristic lives in, since $m^{H1}_n$ is of exact order $\sqrt n$.

Milestones

1. Eq. (8.10): the deterministic sandwich $S_n/m \le C^*_n(m) \le C^H_n(m) \le S_n/m + p_{\max}$, divided by $n\mu/m$.
2. Eq. (8.11): the strong law of large numbers, $(S_n - n\mu)/(n\mu) \to 0$ almost surely (a published platform theorem).
3. Lemma 8.1 (i): $p_{\max}/\sqrt n \to 0$ almost surely.
4. Eq. (8.12): $m\, p_{\max}/(n\mu) \to 0$ almost surely when $m = O(\sqrt n)$.
5. Lemma 8.1 (ii): $\mathbb E\, p_{\max}/\sqrt n \to 0$.
6. p. 207: $\mathbb E\, C^*_n(m)/(n\mu/m) \to 1$ when $m = O(\sqrt n)$.
7. p. 211, asymptotic clairvoyance: almost surely

$$\lim_{n\to\infty} \frac{c\, m^{H1}_n + C^{H2}_n(m^{H1}_n)}{c\, m^\circ_n + C^*_n(m^\circ_n)} = 1 ,$$

where $C^{H2}_n$ is the list-scheduling makespan.

Significance

Result (8.13) says that the optimal value of an NP-hard problem, rescaled, is almost surely asymptotic to the elementary function $n\mu/m$ of the data and the first-stage decision. Its expectation version replaces the intractable term $\mathbb E\,C^*_n(m)$ in (8.9) by $n\mu/m$, and the clairvoyance statement shows that the heuristic built on that replacement loses asymptotically nothing, not even against a decision maker with full information. The chapter presents the example as the template for vehicle routing and location problems preceded by an investment decision.

All results here are classical and proved in the literature cited by the chapter (Lemma 8.1 is quoted from Feller without proof; the chapter refers to Dempster et al. for the asymptotic optimality of the two-stage heuristic and to Lenstra et al. for the notion of asymptotic clairvoyance). None of them has, to our knowledge, a machine-checked proof. The mission produces a formal model of identical-machine makespan scheduling and of list scheduling, the extreme-value estimates of Lemma 8.1 for square-integrable i.i.d. sequences, and the full chain from the strong law to (8.13).

Difficulty

The deterministic part is elementary on paper, but list scheduling is a recursively defined procedure, and its makespan bound has to be established for that recursion rather than for a picture like the chapter's Figure 8.3. The probabilistic core is Lemma 8.1: the strong law controls $S_n/n$, but the error term $m\, p_{\max}/(n\mu)$ is of order $p_{\max}/\sqrt n$ once $m$ grows like $\sqrt n$, and the strong law says nothing about maxima. With a fixed number of machines the whole statement would reduce to the strong law; the growth $m(n) = O(\sqrt n)$ is exactly where the second moment is needed. For the clairvoyance statement, the clairvoyant choice $m^\circ_n$ is a random, unstructured minimizer, so its value must be bounded below without knowing where the minimum is attained.

Formalization scope

Processing times are one sequence p : ℕ → Ω → ℝ, 0-based (the book's $p_j$ is p (j-1)), with each p j measurable, the family mutually independent (iIndepFun), identically distributed with p 0, pointwise nonnegative, p 0 ^ 2 integrable and ∫ p 0 = μ with μ > 0. Nonnegativity and $\mu > 0$ are not printed in the book; they are implicit in "processing times" and in the division by $n\mu$. Machines are Fin m; a schedule is an assignment Fin n → Fin m, which is faithful because jobs are non-preemptive, machines identical and there are no precedence constraints.

The book writes "$m = 0(\sqrt n)$"; this is read as $m$ a function of $n$ with $m(n) \ge 1$ and (fun n => (m n : ℝ)) =O[atTop] (fun n => √n). Stating (8.13) for a fixed $m$ would trivialize it into the strong law and is ruled out. "$\Pr\{\lim \dots = 1\} = 1$" means that almost surely the limit exists and equals $1$. Expectations are Bochner integrals of functions that are measurable and bounded by $S_n$, hence integrable. List scheduling uses the index order and breaks ties towards the lowest machine index; both are admissible instances of the book's "arbitrary fixed order" and "first available machine". In the clairvoyance statement the minimum is over $m \ge 1$ (the book writes $m \in \mathbb N$; no machine cannot process any job, and the Lean value $C^*_n(0)$ is an empty-infimum convention). No explicit constants replace an O(·): the statements are limits and the O-hypothesis is carried as stated.

Out of scope: (8.14) and the p. 210 expectation statement, which need a positive density at $0$ and whose proof the book calls "far from easy", and the dynamic programming recursion of §8.3.

Needed infrastructure: finite maxima and minima of measurable functions, extreme-value estimates for square-integrable i.i.d. sequences (Lemma 8.1), and Mathlib's strong law. The makespan and list-scheduling definitions are reusable for other identical-machine scheduling results; alternative proofs of Lemma 8.1 and sharper forms of the clairvoyance statement are welcome.

Selected references

• A. H. G. Rinnooy Kan, L. Stougie, "Stochastic Integer Programming", in Yu. Ermoliev, R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 8, pp. 201–213. https://doi.org/10.1007/978-3-642-61370-8
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, 3rd edition, Wiley, 1968 (cited by the chapter for Lemma 8.1).
• M. A. H. Dempster, M. L. Fisher, L. Jansen, B. J. Lageweg, J. K. Lenstra, A. H. G. Rinnooy Kan, "Analysis of heuristics for stochastic programming: results for hierarchical scheduling problems", Mathematics of Operations Research 8 (1983) 525–537. https://doi.org/10.1287/moor.8.4.525
• J. K. Lenstra, A. H. G. Rinnooy Kan, L. Stougie, "A framework for the design and analysis of hierarchical planning systems", Annals of Operations Research 1 (1984) 23–42. https://doi.org/10.1007/BF01874451
• R. L. Graham, "Bounds on multiprocessing timing anomalies", SIAM Journal on Applied Mathematics 17 (1969) 416–429. https://doi.org/10.1137/0117039

Motivation

Many optimization problems in operations research have an objective that is an expectation, $F^0(x)=E f^0(x,\omega)$, over a random parameter $\omega$ whose distribution is known only through samples or is too complex to integrate. Two-stage stochastic programs, inventory and reliability models, and simulation-based design all have this form. Neither $F^0$ nor its subgradients can be evaluated exactly, but a random vector whose conditional mean is close to a subgradient is often cheap to compute: a sample subgradient of $f^0(\cdot,\omega)$, or a finite-difference quotient of two sampled values.

Stochastic quasigradient (SQG) methods, developed by Ermoliev and co-workers in Kiev from the late 1960s, use such vectors in place of subgradients. They extend the stochastic approximation procedures of Robbins–Monro (1951) and Kiefer–Wolfowitz (1952) to nonsmooth convex objectives, general convex constraints, and directions whose conditional mean is biased by a vanishing amount. This mission formalizes the basic convergence theory of the simplest SQG method, the projection method, as presented by Yu. Ermoliev in Chapter 6 of the IIASA volume Numerical Techniques for Stochastic Optimization (Springer 1988).

Timeline (as cited in the chapter's bibliography).

• 1951–1954: Robbins and Monro, Kiefer and Wolfowitz, Dvoretzky and Blum prove convergence of stochastic approximation for unconstrained smooth problems.
• 1962–1967: Shor introduces the generalized gradient (subgradient) method; Ermoliev (Kibernetika 4, 1966) and Polyak (Soviet Math. Doklady 8, 1967) prove its convergence.
• 1967–1969: Ermoliev and Nekrylova introduce stochastic subgradients; Ermoliev ("On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2, 1969) introduces stochastic quasi-Féjer sequences.
• 1976: Ermoliev's monograph Stochastic Programming Methods (Nauka) contains the proof of Theorem 6.1 (p. 98).
• 1988: the survey chapter formalized here presents the projection method, Theorems 6.1 and 6.2, and an efficiency estimate for the averaged iterate.

Setting

Let $X\subseteq\mathbb R^n$ be a nonempty convex compact set and $F^0:\mathbb R^n\to\mathbb R$ convex and continuous on $X$. The optimal set is $X^*=\{x\in X: F^0(x)\le F^0(y)\ \forall y\in X\}$. The projection onto $X$ is $\pi_X(y)=\operatorname{argmin}\{\|y-x\|^2:x\in X\}$.

On a probability space, the stochastic quasigradient projection method produces random vectors $x^0,x^1,\dots$ by

$$x^{s+1}=\pi_X\big[x^s-\rho_s\,\xi^0(s)\big],\qquad s=0,1,\dots \tag{6.11}$$

where $\rho_s\ge0$ is a step size and $\xi^0(s)$ a random direction. Write $E\{\cdot\mid x^0,\dots,x^s\}$ for conditional expectation given the history $\sigma(x^0,\dots,x^s)$. The direction is a stochastic quasigradient if, for every $x^*\in X^*$,

$$F^0(x^*)-F^0(x^s)\ge\big\langle E\{\xi^0(s)\mid x^0,\dots,x^s\},\,x^*-x^s\big\rangle+\gamma_0(s)\quad\text{a.s.}, \tag{6.12}$$

where the error $\gamma_0(s)$ is a function of the history. If the conditional mean of $\xi^0(s)$ is a subgradient plus a bias $b^0(s)$, then (6.12) holds with $\gamma^0(s)=-\langle b^0(s),x^*-x^s\rangle$ (6.13).

A sequence of random vectors $z^0,z^1,\dots$ is a stochastic quasi-Féjer sequence for $Z\subseteq\mathbb R^n$ if $E\|z^0\|^2<\infty$ and there are random $r_s\ge0$ with $\sum_s E r_s<\infty$ such that for all $z\in Z$

$$E\{\|z-z^{s+1}\|^2\mid z^0,\dots,z^s\}\le\|z-z^s\|^2+r_s. \tag{6.14}$$

Formalization targets

Goal: Theorem 6.2

If, with probability 1, $\rho_s\ge0$ and $\sum_s\rho_s=\infty$, and

$$\sum_{s=0}^\infty E\{\rho_s|\gamma_0(s)|+\rho_s^2\|\xi^0(s)\|^2\}<\infty, \tag{6.15}$$

then with probability 1 the iterates converge and $\lim_s x^s\in X^*$.

Milestones

1. Theorem 6.1 (a)–(c). For a stochastic quasi-Féjer sequence for $Z$: $\|z-z^{s+1}\|^2$ converges a.s. and $E\|z-z^s\|^2$ is bounded, for each $z\in Z$; accumulation points exist a.s. (for $Z\ne\emptyset$); and a.s. $Z$ lies in the hyperplane equidistant from any two distinct accumulation points outside $Z$.
2. Eq. (6.13). Biased stochastic subgradients satisfy (6.12).
3. One-step inequality (p. 145): $E\{\|x^*-x^{s+1}\|^2\mid\cdot\}\le\|x^*-x^s\|^2+2\rho_s\langle E\{\xi^0(s)\mid\cdot\},x^*-x^s\rangle+E\{\rho_s^2\|\xi^0(s)\|^2\mid\cdot\}$ for $x^*\in X$.
4. Quasi-Féjer property (p. 145): the iterates of (6.11) form a stochastic quasi-Féjer sequence for $X^*$.
5. Efficiency estimate (p. 147), for deterministic $\rho_k$ and $\bar x^s=\sum_{k\le s}\rho_kx^k/\sum_{k\le s}\rho_k$:

$$E F^0(\bar x^s)-F^0(x^*)\le\Big(2\sum_{k=0}^s\rho_k\Big)^{-1}\Big[E\|x^*-x^0\|^2+\sum_{k=0}^s E\big(2\rho_k|\gamma_0(k)|+\rho_k^2\|\xi^0(k)\|^2\big)\Big].$$

Significance

Theorem 6.2 is the prototype convergence theorem for SQG methods. Its hypotheses allow random step sizes chosen from the history, nonsmooth objectives, and directions with a bias that vanishes fast enough; its conclusion is convergence of the iterates themselves to a single optimal point, not only convergence of function values or of $\operatorname{dist}(x^s,X^*)$. The later chapters of the same volume (adaptive step sizes, Chapters 17–18; nonstationary problems, §6.4) reuse the same framework. Theorem 6.1 isolates the probabilistic content in a form that applies to any algorithm with a quasi-Féjer inequality. The efficiency estimate gives a non-asymptotic accuracy bound for the averaged iterate.

The results are classical and proved in the literature: Theorem 6.1 in Ermoliev (1976, p. 98), Theorem 6.2 in this chapter (pp. 145–146). To our knowledge none of them has a machine-checked proof. Mathlib has conditional expectations and the a.s. martingale convergence theorem, but no Robbins–Siegmund-type almost-supermartingale lemma and no stochastic subgradient method. A formal proof of this mission would supply both.

Difficulty

The deterministic argument for projected subgradient methods compares $\|x^*-x^{s+1}\|$ with $\|x^*-x^s\|$ for a fixed $x^*$. In the stochastic setting this comparison holds only in conditional mean, with a perturbation $r_s$ that is random, and the distances converge only almost surely, with an exceptional null set that depends on $x^*$. Since $X^*$ is typically uncountable, "for every $x^*$, almost surely" does not immediately give "almost surely, for every $x^*$", and it is the second form that identifies a single limit. A second difficulty is that $\sum\rho_s(F^0(x^s)-F^0(x^*))<\infty$ only yields a subsequence along which $F^0$ approaches its minimum; passing from there to convergence of the whole sequence is exactly what part (c) of Theorem 6.1 is for.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The probability space is an arbitrary measurable space with a probability measure. $\pi_X$ is a chosen minimizer of $\|y-x\|^2$ over $X$ (unique for nonempty closed convex $X$). The history is the $\sigma$-algebra generated by $x^0,\dots,x^s$; $\rho_s$ and $\gamma_0(s)$ are measurable with respect to it.
• Directions $\xi^0(s)$ are integrable and random vectors are measurable; conditional expectations are Mathlib's condExp. The quasi-Féjer definition requires square integrability of every $z^s$ (implied by the book's definition when $Z\ne\emptyset$), so no conditional expectation is taken of a non-integrable function.
• $X\ne\emptyset$ and $x^0\in X$ are stated; $Z\ne\emptyset$ is added in Theorem 6.1 (b), which is false without it.
• $\gamma_0(s)$ does not depend on $x^*$; the $x^*$-dependent error of (6.13) is dominated on a bounded $X$ by $\|b^0(s)\|\operatorname{diam}X$.
• (6.15) keeps its mixed form: $\rho_s\ge0$ and $\sum\rho_s=\infty$ almost surely, and a deterministic sum of expectations (lower Lebesgue integrals) finite.
• Explicit constants. The book's "$C$" in the efficiency estimate is instantiated from its proof: $2$ on $\rho_k|\gamma_0(k)|$ and $1$ on $\rho_k^2\|\xi^0(k)\|^2$. The unspecified $C$ before the quasi-Féjer sentence is replaced by the existence of summable $r_s$.
• Typo corrections. The one-step inequality on p. 145 prints $\rho_sE\{\|\xi^0(s)\|^2\mid\cdot\}$; it is $\rho_s^2$. The efficiency estimate on p. 147 omits $E$ before the last sum; it is restored. "$\rho_k$ independent of $(x^0,\dots,x^k)$" is read as deterministic step sizes.
• A trivializing formalization is excluded: the goal does not replace $\xi^0(s)$ by an exact subgradient, does not set $\gamma_0\equiv0$, and concludes convergence of $x^s$ to a point of $X^*$ rather than $\operatorname{dist}(x^s,X^*)\to0$.
• Reusable infrastructure: a Robbins–Siegmund lemma for nonnegative almost-supermartingales, the nonexpansiveness of $\pi_X$, and Theorem 6.1 itself, which applies to any quasi-Féjer algorithm (Chapter 6 §6.4 and Chapters 17–18 of the same book). Contributions of these general lemmas are welcome.

Selected references

• Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, §6.1–6.2 (pp. 141–147). https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, "On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2 (1969) (in Russian; English translation in Cybernetics). Reference [3] of the chapter.
• Yu. Ermoliev, Stochastic Programming Methods, Nauka, Moscow, 1976 (in Russian); Theorem 6.1 is on p. 98. Reference [5] of the chapter.
• H. Robbins and D. Siegmund, "A convergence theorem for non negative almost supermartingales and some applications", in J. S. Rustagi (ed.), Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• H. Robbins and S. Monro, "A stochastic approximation method", Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an $n$-digit integer in time polynomial in $n$ (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given $x$ coprime to $n$, find the least $r \ge 1$ with $x^r \equiv 1 \pmod n$. The quantum part solves order finding.

This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads $r$ off the measured value. The paper's claim is that one run of this procedure returns $r$ with probability at least $\varphi(r)/3r$.

Timeline:

• 1976: Miller reduces factoring to order finding (with randomization).
• 1985–1994: Deutsch, Bernstein–Vazirani and Simon give the quantum Fourier sampling ideas the algorithm builds on.
• 1994: Shor's FOCS paper introduces the factoring and discrete logarithm algorithms.
• 1997: the SIAM J. Comput. version gives the analysis formalized here, with $q$ the power of $2$ in $[n^2, 2n^2)$.

Setting

Fix an integer $n \ge 2$ and an integer $x$ coprime to $n$. Its order $r$ is the least $r \ge 1$ with $x^r \equiv 1 \pmod n$; since $x$ is a unit, $r \le \varphi(n) < n$. Let $q = 2^l$ be the power of $2$ with $n^2 \le q < 2n^2$.

A quantum state on two registers, the first holding $0 \le a < q$ and the second a residue $y \in \mathbb{Z}/n$, is a complex vector $\psi(a, y)$ indexed by the basis states $|a, y\rangle$. Measuring it returns $|a, y\rangle$ with probability $|\psi(a, y)|^2$.

The Fourier matrix $A_q$ is the $q \times q$ matrix with entries $(A_q)_{a,c} = q^{-1/2}\exp(2\pi i a c/q)$, with rows indexing inputs and columns outputs. The algorithm

1. prepares $\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle$ (eq. (5.2)),
2. applies $A_q$ to the first register, obtaining $\frac1q\sum_{a,c}\exp(2\pi iac/q)|c\rangle|x^a \bmod n\rangle$ (eq. (5.4)),
3. measures, obtaining some $|c, y\rangle$,
4. rounds $c/q$ to the nearest fraction with denominator smaller than $n$.

The observed $c$ gives us $r$ if some fraction with lowest-terms denominator below $n$ is within $1/2q$ of $c/q$, and every such fraction has lowest-terms denominator exactly $r$. In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.

Formalization targets

Goal: success probability at least $\varphi(r)/3r$

For all sufficiently large $n$, with $x$, $r$ and $q$ as above,

$$\Pr\bigl[\text{the observed } c \text{ gives us } r\bigr] \;=\; \sum_{c\ \text{gives}\ r}\ \sum_{y \in \mathbb{Z}/n} |\Psi(c, y)|^2 \;\ge\; \frac{\varphi(r)}{3r},$$

where $\Psi$ is the state (5.4). The threshold on $n$ is uniform in $x$ and $q$; it is the paper's "for sufficiently large $n$" from the per-state bound.

Milestones

1. Eqs. (5.5)–(5.6). For $0 \le k < r$, the probability of $|c, x^k\rangle$ equals $\left|\frac1q\sum_{b=0}^{\lfloor (q-k-1)/r\rfloor}\exp(2\pi i(br+k)c/q)\right|^2$.
2. Eq. (5.11). For $n$ past a threshold, every $|c, x^k\rangle$ with $-r/2 \le rc - dq \le r/2$ for some integer $d$ has probability at least $1/3r^2$.
3. Eq. (5.13). If $n^2 \le q$, at most one fraction with denominator below $n$ lies within $1/2q$ of $c/q$.
4. p. 1500. Such a fraction is a convergent of the continued fraction of $c/q$.
5. p. 1501. At least $\varphi(r)$ values of $c$ are within $1/2q$ of some $d/r$ with $\gcd(d, r) = 1$; with the $r$ distinct values of $x^k$ this gives at least $r\varphi(r)$ states $|c, x^k\rangle$, and each such $c$ gives us $r$.

Significance

The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since $\varphi(r)/r \ge \delta/\log\log r$ for a constant $\delta$ (Hardy and Wright, Thm. 328), $O(\log\log r)$ repetitions find $r$ with high probability, and Miller's reduction then factors $n$. Without the bound, the algorithm is a procedure with no guarantee.

The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of $q$ and his constants, starting from the state built by applying $A_q$ to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where $r$ divides $q$ and the output is uniform on $r$ peaks, but that model removes the approximation that the $1/3r^2$ bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.

Difficulty

The obvious route is to compute the output distribution in closed form. That works only when $r$ divides $q$; here $q$ is a power of $2$ and $r$ is arbitrary, so the amplitudes are geometric sums of $\lfloor (q-k-1)/r\rfloor + 1$ terms whose phases do not cancel exactly. The per-state bound $1/3r^2$ requires a lower bound on such a sum that is uniform in $r$, $c$ and $k$, with error terms of order $1/q$ controlled against a main term of order $1/r^2$. The constant $1/3$ leaves only a small margin below the limiting value $4/\pi^2 \approx 0.405$, so the errors must be bounded explicitly, not merely shown to vanish.

The second difficulty is the counting: distinct coprime numerators $d$ must give distinct outcomes $c$ in $[0, q)$, and each good $c$ must determine $r$ uniquely, which uses $r < n$ and $n^2 \le q$.

Formalization scope

Conventions the statements commit to:

• States are functions Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying $A_q$ to the first register gives the amplitude $\sum_a \psi(a, y)(A_q)_{a,c}$ at $(c, y)$.
• The final state is built by applying $A_q$ to the state (5.2); the closed forms (5.5) and (5.6) are theorems, not definitions. No normalization hypothesis is assumed.
• Probabilities are squared moduli; the probability of the event "$c$ gives us $r$" sums over all $y \in \mathbb{Z}/n$, which is exact because $y$ that are not powers of $x$ have probability zero.
• $x$ is a natural number with $\gcd(x, n) = 1$; $r$ is orderOf (x : ZMod n). $q$ enters through the three hypotheses $q = 2^l$, $n^2 \le q$, $q < 2n^2$, not through a function of $n$.
• Fractions are rationals, and "in lowest terms" is Rat.den.
• Thresholds "for sufficiently large $n$" are $\exists N,\ \forall n \ge N$, with $N$ quantified before $x$, $q$, $c$ and $k$.
• Condition (5.11) is stated in its equivalent form (5.12), with an integer $d$.
• Printed slip. Eq. (5.13)'s justification says "Because $q > n^2$", but $q$ was chosen with $n^2 \le q$, and $q = n^2$ when $n$ is a power of $2$. The uniqueness claim holds under $n^2 \le q$, and that is what is stated.

Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.

Not stated: the polynomial running time of any step, the $O(\log\log r)$ repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod $n$ are reusable in the companion discrete logarithm mission.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
• P. W. Shor, Algorithms for quantum computation: discrete logarithms and factoring, Proc. 35th FOCS, 1994. https://doi.org/10.1109/SFCS.1994.365700
• G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford, 1979 (Ch. X, continued fractions; Thm. 328).
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge, 2000. https://doi.org/10.1017/CBO9780511976667