Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Machine Learning Markov Chain Reinforcement Learning·Captain: mikedeng1

Reinforcement Learning: An Introduction VII: The Error Reduction Property of n-step ReturnsTextbook

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

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$ .
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.
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)$ .
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]$ .
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).
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).

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory Machine Learning Mechanism Design·Captain: mikedeng1

How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design 2: Neutral Affine Maximizers Have Pseudo-Dimension at Least ⌊n/2⌋Research Paper

Motivation

In data-driven algorithm design, an algorithm or mechanism comes with a vector of tunable parameters $\rho$ , and the parameters are chosen by optimizing average performance over sample instances drawn from an unknown distribution. How many samples suffice for the empirical optimum to be near-optimal in expectation is governed by the pseudo-dimension of the class $\mathcal U=\{u_\rho\}$ of performance functions, where $u_\rho(x)$ is the performance of the parameter $\rho$ on instance $x$ . Balcan, DeBlasio, Dick, Kingsford, Sandholm and Vitercik (arXiv:1908.02894v4, 2021) give a general upper bound on $\mathrm{Pdim}(\mathcal U)$ for classes whose dual functions are piecewise structured (their Theorem 3.3, the subject of mission 1 of this series), and apply it across integer programming, computational biology, clustering and mechanism design.

A general upper bound raises the question of whether it can be improved. Section 5 of the paper answers it for one application: neutral affine maximizers (NAMs), a family of voting mechanisms studied by Roberts (1979), Mishra and Sen (2012) and Nath and Sandholm (2019). For NAMs with $n$ agents and $m$ alternatives the general theorem gives $\mathrm{Pdim}(\mathcal U)=O(n\ln m)$ , and Theorem 5.2 shows a lower bound linear in $n$ . So the sample complexity of tuning a NAM by sampling cannot be reduced below order $n$ by a sharper analysis, and the general bound is tight up to logarithmic factors.

Setting

There are $n$ agents and $m$ alternatives. Agent $i$ has a value $v_i(j)\in\mathbb R$ for each alternative $j\in[m]$ ; a valuation profile is $v=(v_1,\dots,v_n)\in\mathbb R^{nm}$ .

A NAM is specified by a weight vector $\rho=(\rho[1],\dots,\rho[n])\in\mathbb R^n_{\ge0}$ in which at least one agent has weight zero; an agent with $\rho[i]=0$ is a sink agent. The NAM's outcome on a profile $v$ is an alternative maximizing the weighted value,

\psi_\rho(v)\in\operatorname*{argmax}_{j\in[m]}\ \sum_{i=1}^n\rho[i]\,v_i(j).

Its utility is the social welfare of that outcome,

u_\rho(v)=\sum_{i=1}^n v_i\bigl(\psi_\rho(v)\bigr),

and the class studied is $\mathcal U=\{u_\rho \mid \rho\in\mathbb R^n_{\ge0},\ \{i\mid\rho[i]=0\}\ne\emptyset\}$ . NAMs also charge VCG-style payments that are redistributed to the sink agents; these do not enter $u_\rho$ .

A class $\mathcal H$ of real-valued functions on a set $Y$ shatters points $y_1,\dots,y_N$ if there are thresholds $z_1,\dots,z_N\in\mathbb R$ such that every pattern $b\in\{0,1\}^N$ is realized by some $h\in\mathcal H$ , in the sense that $h(y_\ell)>z_\ell$ exactly when $b_\ell=1$ . The pseudo-dimension $\mathrm{Pdim}(\mathcal H)$ is the largest $N$ for which some $N$ points are shattered. In Lean: a profile is v : Fin n → Fin m → ℝ, the outcome rule is ψ, the utility is welfare ψ ρ, the class is namClass ψ, and shattering is the published FoundationsML.Regression.Shatters.

Formalization targets

Goal: Theorem 5.2, corrected

For every $n\ge1$ , every $m\ge2$ and every tie-breaking rule,

\mathrm{Pdim}(\mathcal U)\ \ge\ \Bigl\lfloor\frac n2\Bigr\rfloor .

The printed statement reads $\mathrm{Pdim}(\mathcal U)\ge n/2$ ; see Formalization scope for why the floor is needed.

Milestones: the two claims of the proof (p. 24)

The proof fixes $N=\lfloor n/2\rfloor$ explicit profiles $v^{(1)},\dots,v^{(N)}$ and, for each bit vector $b\in\{0,1\}^N$ , an explicit weight vector $\rho\in\{0,1\}^n$ (both are definitions of this mission). The two milestones are the claims the proof makes about them: for every $\ell\in[N]$ and $\varepsilon\in(0,\tfrac12)$ ,

b_\ell=0\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=\varepsilon,\qquad b_\ell=1\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=1 .

Significance

The result. Theorem 5.2 is the paper's evidence that its main upper bound cannot be improved in general by more than logarithmic factors: for NAMs the upper bound is $O(n\ln m)$ and the lower bound is of order $n$ . Through the standard link between pseudo-dimension and uniform convergence, it also means that any learner choosing NAM weights from samples needs a number of samples growing with the number of agents, whatever tie-breaking rule the mechanism uses.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any pseudo-dimension lower bound for a mechanism class, was found on Prove2Me. This mission produces a Lean model of NAM outcomes and welfare that does not fix a tie-breaking rule, an explicit lower-bound construction stated as definitions, and a pseudo-dimension lower bound in the vocabulary of the published FoundationsML pseudo-dimension items. It complements mission 1, which formalizes the matching upper-bound machinery.

Difficulty

The mathematical content is a single explicit construction, and the work lies in stating and verifying it at full generality rather than in a deep argument. Three points make the naive transcription wrong. First, the printed bound $n/2$ is false at $n=1$ and is not what the proof establishes for odd $n$ ; the even- $n$ reduction must be replaced by a statement in $\lfloor n/2\rfloor$ . Second, the outcome $\psi_\rho(v)$ is defined by an argmax with unspecified tie-breaking, so the claims must hold for every maximizer; this requires showing the relevant maximizers are unique on the constructed profiles, not reading off a convenient one. Third, the construction embeds $\lfloor n/2\rfloor$ indices into the $n$ agents twice (as $\ell$ and $\lfloor n/2\rfloor+\ell$ ), and the printed index condition for the second alternative is a typo; an off-by-one in this embedding silently breaks both claims. Finally, every constructed $\rho$ must be admissible: it needs a sink agent, which holds only because $N\ge1$ or because $n$ is odd and the last agent keeps weight $0$ .

Formalization scope

Representation. Agents are Fin n, alternatives Fin m, profiles Fin n → Fin m → ℝ, all 0-based: the paper's agent $i$ is i - 1, and its first and second alternatives are 0 and 1. Bits are Bool with true for $1$ . An outcome rule is any ψ : (Fin n → ℝ) → (Fin n → Fin m → ℝ) → Fin m with IsArgmaxSelector ψ, which requires ψ ρ v to maximize ∑ i, ρ i * v i j for every ρ and v; the theorem and both claims are stated for every such ψ. " $\mathrm{Pdim}(\mathcal U)\ge N$ " is the existence of an $N$ -tuple of profiles shattered by namClass ψ in the sense of FoundationsML.Regression.Shatters, whose strict threshold t i < g (z i) shatters the same tuples as the paper's sign convention.

Corrections and readings of the printed text.

The bound is $\lfloor n/2\rfloor$ (natural-number division n / 2) instead of $n/2$ . The proof assumes $n$ even; at $n=1$ the only admissible $\rho$ is $0$ , so $\mathcal U$ is a single function and $\mathrm{Pdim}(\mathcal U)=0<\tfrac12$ .
The hypotheses $n\ge1$ and $m\ge2$ are explicit. For $n=0$ no weight vector has a zero coordinate and $\mathcal U=\emptyset$ ; for $m=1$ the class is a single function. The proof takes $m=2$ ; the statement is for every $m\ge2$ , with value $0$ on every further alternative in the constructed profiles.
The set-builder " $\{\rho[i]\mid i=0\}\ne\emptyset$ " in Theorem 5.2 is read as $\{i\mid\rho[i]=0\}\ne\emptyset$ , as written in Lemma 5.1.
The construction's condition " $\ell=n/2+i$ " for $v_i^{(\ell)}(2)=\varepsilon$ is read as $i=n/2+\ell$ , as the paper's own $n=6$ example shows. The milestone texts are verbatim and keep the printed " $v^{(\ell)}_{n/2+\ell}(1)$ ", which should read " $(2)$ ".

Ruled-out trivializations. Fixing one tie-breaking rule would state a special case and is excluded by quantifying over all argmax selectors. Dropping the sink-agent condition, or allowing $n=0$ or $m=1$ , would change the class or make the statement vacuous or false; the conventions above exclude all three.

Infrastructure. Only Mathlib finite sums over Fin and the published Shatters definition are needed. The NAM model (IsNAMParam, IsArgmaxSelector, welfare, namClass) is reusable for any further statement about learning NAM parameters, including the matching $O(n\ln m)$ upper bound once mission 1's general theorem is available. Proofs of the two claims, of the admissibility of the constructed weight vectors, and of the goal are all welcome.

Selected references

M.-F. Balcan, D. DeBlasio, T. Dick, C. Kingsford, T. Sandholm, E. Vitercik, How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design, arXiv:1908.02894v4, 2021. https://arxiv.org/abs/1908.02894v4
K. Roberts, The characterization of implementable social choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979 (reference [86] of the paper).
D. Mishra, A. Sen, Roberts' theorem with neutrality: a social welfare ordering approach, Games and Economic Behavior 75(1):283–298, 2012 (reference [74] of the paper).
S. Nath, T. Sandholm, Efficiency and budget balance in general quasi-linear domains, Games and Economic Behavior 113:673–693, 2019 (reference [78] of the paper).
D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (pseudo-dimension; reference [83] of the paper).

6 thms3 active usersReviewed

Completed

Combinatorics Computational Geometry Discrete Geometry+1·Captain: mikedeng1

A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension is Fixed: The Lattice-Point Count of an Integral Simplex Is a Short Signed Sum over Primitive ConesResearch Paper

Counting lattice points in fixed dimension

How many integral points does a polytope contain? The question arises in integer programming, where it measures the size of a feasible set, in combinatorics, where many enumeration problems are lattice-point counts in a polytope (contingency tables, magic squares, flows), in the representation theory of Lie groups, and in the analysis of loop nests in compilers. Counting is #P-hard when the dimension is part of the input, so the natural question is whether the count can be computed in polynomial time when the dimension $d$ is fixed.

Timeline:

1899. In dimension $2$ , Pick's formula leads to a polynomial algorithm.
1983. Lenstra shows that integer feasibility is decidable in polynomial time for fixed $d$ (Lenstra 1983). Deciding whether a lattice point exists does not count them.
1988, 1992. Brion proves that the exponential sum over the lattice points of a rational polytope is the sum of the exponential sums of its vertex cones.
1991. Dyer gives polynomial algorithms in dimensions $3$ and $4$ , based on Dedekind sums (Dyer 1991).
1994. Barvinok proves that for every fixed $d$ the number of lattice points of an integral simplex, and hence of a rational polyhedron, can be computed in polynomial time (Barvinok 1994). The algorithm was later implemented (LattE, barvinok) and is the standard method.

Setting

Points of $\mathbb{R}^d$ have real coordinates and $\langle c,x\rangle=\sum_l c_lx_l$ . For integral vectors $u_1,\dots,u_k\in\mathbb{Z}^d$ , the rational cone they generate is $\operatorname{co}\{u_1,\dots,u_k\}=\{\sum_i\lambda_iu_i:\lambda_i\ge0\}$ . The generators are simple if they are linearly independent, and primitive if moreover they form a basis of the lattice $\mathbb{Z}^d\cap\operatorname{Lin}\{u_1,\dots,u_k\}$ .

The index $\operatorname{Ind}K$ of the cone given by simple generators is the number of integral points in the semi-open parallelepiped $\Pi=\{\sum_i\alpha_iu_i:0\le\alpha_i<1\}$ . It equals $1$ exactly for primitive generators.

The exponential sum of $K$ is $\sigma(K;c)=\sum_{x\in K\cap\mathbb{Z}^d}e^{\langle c,x\rangle}$ . Where it converges it has the closed form

\sigma(K;c)=\Bigl(\sum_{x\in\Pi\cap\mathbb{Z}^d}e^{\langle c,x\rangle}\Bigr)\prod_{i=1}^k\frac{1}{1-e^{\langle c,u_i\rangle}},

and this closed form defines $\sigma$ at every regular point, i.e. every $c$ with $\langle c,u_i\rangle\ne0$ for all $i$ .

An integral simplex is $\Delta=\operatorname{conv}\{v_1,\dots,v_{k+1}\}$ with affinely independent $v_j\in\mathbb{Z}^d$ . Its supporting cone at a vertex $v$ is $K_v=\{u:v+\delta u\in\Delta\text{ for all sufficiently small }\delta>0\}$ . A signed decomposition $K=\sum_i\varepsilon_iK_i$ with integers $\varepsilon_i$ means $\chi_K=\sum_i\varepsilon_i\chi_{K_i}$ on all of $\mathbb{R}^d$ . The constant term of the Laurent expansion of $f$ at $t=0$ is the coefficient of $t^0$ in the expansion of $f$ around its pole at $0$ .

Formalization targets

Goal: the short signed formula (Theorem 1.2, mathematical content)

For $d\ge2$ and every integral simplex $\Delta\subseteq\mathbb{R}^d$ there are, for each vertex $v_j$ , primitive cones $K_{j,i}$ and integers $\varepsilon_{j,i}$ with $K_{v_j}=\sum_i\varepsilon_{j,i}K_{j,i}$ and at most $(2^d)^{T_j}$ terms. Here $T_j$ is the smallest integer

T_j\ge\frac{-\log\log1.9+\log\log\operatorname{Ind}_j}{\log d-\log(d-1)},

and $\operatorname{Ind}_j$ is the index of the edge vectors at $v_j$ . Moreover, for every $c$ orthogonal to no generator of any $K_{j,i}$ ,

\#(\Delta\cap\mathbb{Z}^d)=\sum_j\sum_i\varepsilon_{j,i}\,R(K_{j,i},v_j,c),

where $R(K,v,c)$ is the constant term at $t=0$ of $t\mapsto e^{t\langle c,v\rangle}\sigma(K;tc)$ .

Milestones

Proposition 2.4 with Remark 2.5: the closed form of $\sigma$ for simple cones.
Proposition 4.1: for primitive cones, $\sigma(K;c)=\prod_i(1-e^{\langle c,u_i\rangle})^{-1}$ .
Proposition 2.7 (Brion), for integral simplices.
Corollary 4.2: $R(K,v,c)=Q_k(x;y)\prod_ix_i^{-1}$ with $\deg Q_k\le k$ .
Primitive generators iff $\operatorname{Ind}K=1$ (§5).
Lemma 5.2: a short lattice vector $w$ with $\operatorname{Ind}K_j\le(\operatorname{Ind}K)^{(d-1)/d}$ .
Lemma 5.3: at most $2^d$ cones of smaller index, with signs $\pm1$ .
Theorem 5.4: decomposition into at most $(2^d)^T$ primitive cones.
The display in the proof of Theorem 5.4: $(2^d)^T\le C_1(d)(\log\operatorname{Ind}K)^{C_2(d)}$ .
Lemma 6.1: some $c(t)=(1,t,\dots,t^{d-1})$ , $t\in\{0,\dots,m(d-1)\}$ , is orthogonal to none of $m$ nonzero vectors.

Significance

The goal is the reason Barvinok's algorithm is polynomial. For fixed $d$ , the number of terms is bounded by a polynomial in $\log\operatorname{Ind}K$ , which is polynomial in the input size. Each term is an explicit rational function of inner products (Corollary 4.2). The identity therefore turns lattice-point counting into the evaluation of a short sum. Its consequences include polynomial-time counting for rational polyhedra in fixed dimension, polynomial-time computation of Ehrhart quasi-polynomials, and the theory of short rational generating functions (Barvinok–Woods), which underlies algorithms for parametric integer programming.

The result is proved and classical. As far as known it has not been machine-checked: Mathlib has convex cones, Minkowski's convex body theorem and lattices, but no signed cone decompositions, no generating functions of cones and no Brion identity. The mission produces a formal account of the algorithm's correctness and of the size of its output. Its milestones are statements of independent use: the closed form of cone generating functions, Brion's identity for simplices, and the index-reduction lemma.

Difficulty

The obvious approach is to triangulate the supporting cones into unimodular (primitive) cones. This fails: a cone of index $\operatorname{Ind}K$ may need about $\operatorname{Ind}K$ unimodular cones in any triangulation, which is exponential in the input size. The step that makes the count small is signed decomposition. Signed decomposition uses cones that are not contained in $K$ , combined with signs $\pm1$ , and controls the index through the geometry of numbers rather than through a subdivision of $K$ . The second difficulty is that $c=0$ , where the exponential sum equals the count, is a singular point of every $\sigma(K_i;\cdot)$ . The count is recovered as a constant term of a Laurent expansion, so every identity has to be valid as an identity of meromorphic functions on regular points, and not only where the series converge.

Formalization scope

Points of $\mathbb{R}^d$ are Fin d → ℝ, integral vectors Fin d → ℤ used through their real cast, and $\langle\cdot,\cdot\rangle$ is dotProduct. A cone is given by its generator list, because index, parallelepiped and the closed form of $\sigma$ depend on the generators. Logarithms are natural, and $|u|$ is the sup norm.
Theorem 1.2 is represented by its mathematical content. The paper's statement is "there exists a polynomial time algorithm". No machine model is formalized. The goal is the identity proved on p. 778, with the count of the proof of Theorem 5.4 (p. 777). The algorithmic clauses of Lemmas 5.2, 5.3, 6.1 and Theorem 5.4 are each replaced by the existence statement of the object the algorithm constructs. Lemma 5.3(c), whose constant is unquantified, is omitted.
Over $\mathbb{R}$ . The paper uses $c\in\mathbb{C}^d$ only to speak of meromorphic functions. Here $c$ is real, $\sigma$ is defined by its closed form, and regularity means $\langle c,u_i\rangle\ne0$ for every generator. The constant term is a predicate: $t^Nf(t)$ agrees near $0$ with a real-analytic function whose $N$ -th Taylor coefficient is the value.
Added hypotheses. These are $d\ge2$ wherever $T$ appears, $k\ge1$ in Lemma 5.2, $d\ge1$ in Lemma 5.3, $u_i\ne0$ in Lemma 6.1, and $\operatorname{Ind}K\ge2$ in the display bound. $T=0$ when the index is $1$ . Brion's identity is stated for integral simplices, the only case the proof uses.
Trivializations ruled out. $\sigma$ is never an infinite sum, which would take a junk value off its convergence region. "Primitive" means a lattice basis and not mere linear independence; with the weaker notion the decomposition is trivial. Decompositions hold for every $x\in\mathbb{R}^d$ , not only on $\mathbb{Z}^d$ . The halfspace of Lemma 5.2 is linear, since an affine one would make it vacuous.
Infrastructure. A complete development needs generating functions of simplicial cones, Brion's theorem for simplices, the identity theorem for rational functions in $e^{c_1},\dots,e^{c_d}$ , Minkowski's theorem on a sublattice, and inclusion–exclusion for triangulations. Each is reusable beyond this mission, and contributions of any of these pieces are welcome.

Selected references

A. I. Barvinok, A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed, Mathematics of Operations Research 19(4), 1994, 769–779. https://doi.org/10.1287/moor.19.4.769
M. Brion, Points entiers dans les polyèdres convexes, Annales scientifiques de l'École Normale Supérieure 21(4), 1988, 653–663. https://doi.org/10.24033/asens.1572
M. Dyer, On counting lattice points in polyhedra, SIAM Journal on Computing 20(4), 1991, 695–707. https://doi.org/10.1137/0220044
H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4), 1983, 538–548. https://doi.org/10.1287/moor.8.4.538
R. P. Stanley, Enumerative Combinatorics, Vol. 1, Wadsworth & Brooks/Cole, 1986, §4.6. https://doi.org/10.1007/978-1-4615-9763-6
A. Barvinok, K. Woods, Short rational generating functions for lattice point problems, Journal of the AMS 16(4), 2003, 957–979. https://doi.org/10.1090/S0894-0347-03-00428-4

16 thms3 active usersReviewed

Completed

Operations Research Probability Theoretical Computer Science·Captain: mikedeng1

Secretary Problems: Weights and Discounts 3: An O(log n)-Competitive Algorithm for the Discounted Secretary ProblemResearch Paper

Motivation

In the secretary problem, $n$ candidates with arbitrary values arrive one at a time in a uniformly random order, and an online decision maker must accept or reject each candidate on arrival, irrevocably, keeping at most one. The rule that observes the first $n/e$ candidates and then accepts the first one better than everything seen so far selects the best candidate with probability about $1/e$ (Dynkin, 1963). The problem is a basic model of online selection and, read economically, of posted-price mechanisms for agents who arrive in random order: a rule that compares each agent only against a threshold set by earlier agents is truthful.

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study a variant in which time costs value. Selecting the candidate who arrives at time $t$ earns that candidate's value multiplied by a discount $d(t)$ , for an arbitrary non-negative discount function $d$ known in advance. Earlier work treated only specific discount shapes, such as geometric discounting $d(t)=\beta^t$ (Rasmussen and Pliska, 1976). For a general $d$ the classical rule can fail badly: if all the discount mass sits in the first few time steps, a rule that waits through a sample of size $n/e$ earns nothing. The paper shows that the best competitive ratio for arbitrary discounts lies between $\Omega(\log n/\log\log n)$ (its Theorem 4.3) and $O(\log n)$ (its Theorem 4.4). This mission formalizes the upper bound.

Setting

There are $n\ge1$ elements, indexed $\{0,\dots,n-1\}$ , with values $v(e)\ge 0$ , and $n$ times with discounts $d(t)\ge0$ . A uniformly random permutation $\pi$ fixes the order of arrivals: element $\pi(t)$ arrives at time $t$ . An algorithm knows $d$ but not $v$ ; it sees each value on arrival and may select the current element, irrevocably, earning $d(t)\,v(\pi(t))$ . Expectations over $\pi$ are exact averages over the $n!$ orders.

The offline optimum on order $\pi$ is $\mathsf{OPT}(\pi)=\max_t d(t)\,v(\pi(t))$ ; it is a random variable, and the benchmark is its expectation $\mathbb E_\pi[\mathsf{OPT}]$ (p. 4 of the paper).

Let $d_{\max}=\max_t d(t)$ and $v_{\max}=\max_e v(e)$ . For $c\ge1$ the $c$ -th discount class is the set of times

P_c=\{\,i : 2^{-c}d_{\max}<d(i)\le 2^{-(c-1)}d_{\max}\,\}.

The quantity $\mathsf{OPT}_c$ is the part of $\mathbb E_\pi[\mathsf{OPT}]$ earned when the optimal time (the smallest time attaining the maximum) lies in $P_c$ .

The classical secretary rule on $m$ arrivals observes the first $\lfloor m/e\rfloor$ and then selects the first arrival that ranks above every earlier arrival. Ranks use a fixed tie-break order: larger value first, and smaller element index among equal values.

The algorithm $\mathcal A$ sets $M=3\lceil\log_2 n\rceil+2$ , draws $c\in\{1,\dots,M\}$ uniformly, and runs the classical rule on the subsequence of arrivals at the times of $P_c$ , ignoring all other arrivals.

Formalization targets

Goal: Theorem 4.4 with its explicit constant

\mathbb E_\pi[\mathsf{OPT}]\;\le\;4e\,\bigl(3\lceil\log_2 n\rceil+2\bigr)\;\mathbb E[\mathcal A]\qquad(n\ge1,\ d\ge0,\ v\ge0).

The paper states $\mathbb E[\mathsf{OPT}]/\mathbb E[\mathcal A]\le O(\log n)$ ; the constant $4e$ is the one its proof yields.

Milestones

The classical secretary rule selects the top-ranked of $m\ge1$ elements with probability at least $1/e$ (§2, p. 4).
$\mathsf{OPT}_1\ge v_{\max}d_{\max}/n$ (proof of Theorem 4.4, p. 7).
$\mathsf{OPT}_c\le 2^{-c}\,2n^2d_{\max}v_{\max}$ for every $c\ge1$ (p. 7).
$\sum_{c=1}^{3\lceil\log_2 n\rceil+1}\mathsf{OPT}_c\ge\tfrac12\mathbb E_\pi[\mathsf{OPT}]$ (p. 7).
$\mathbb E[\mathcal A_c]\ge\mathsf{OPT}_c/2e$ for every $c\ge1$ , where $\mathcal A_c$ is the classical rule on $P_c$ (p. 7).

Significance

The theorem shows that a general discount function costs only a logarithmic factor against the offline benchmark, and that one algorithm achieves this without any knowledge of the values. Together with the lower bound of Theorem 4.3 it pins the competitive ratio of the discounted secretary problem between $\log n/\log\log n$ and $\log n$ . The same scale-splitting idea, stated in the paper as Theorem 4.5 without full proof, extends the bound to the weighted discounted problem.

The result is proved in the paper; to our knowledge it has not been formalized. A complete development would also produce a machine-checked proof of the classical secretary guarantee for the rule with sample size exactly $\lfloor m/e\rfloor$ at every finite $m$ , with an explicit tie-break, which is reusable by every secretary-type mission. Milestone 1 is that statement. Sharper constants or a smaller class range are welcome as additional statements but do not replace the goal, which is about this algorithm with this $M$ .

Difficulty

The obvious argument, running the classical rule on all $n$ arrivals, fails because the discounts can be concentrated at times the rule spends sampling. Splitting by discount scale fixes this but creates two problems. First, there are unboundedly many scales, and one has to show that the offline optimum's mass outside the top $O(\log n)$ of them is negligible against $\mathbb E[\mathsf{OPT}]$ , a random quantity rather than a fixed maximum. Second, the classical rule on a class sees only a random subset of the elements, in random order, and the guarantee must be transferred to this subsequence, conditioning on which elements land in $P_c$ . Neither step is deep, but both require careful bookkeeping of permutations, and the classical $1/e$ bound at finite $m$ with a floor in the sample size is itself a nontrivial estimate.

Formalization scope

Elements and times are Fin n, an order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and the paper's time $t=1,\dots,n$ is index $t-1$ . Values and discounts are Fin n → ℝ with non-negativity hypotheses. Every expectation is the finite average $\frac1{n!}\sum_\pi$ ; the algorithm's random class is the explicit average $\frac1M\sum_{c=1}^M$ . Maxima are suprema over the finite index set. The logarithm is base 2, $\lceil\log_2 n\rceil$ is Nat.clog 2 n, and the sample size is Nat.floor (m / Real.exp 1). Ties are broken by the order on Lex (ℝ × (Fin n)ᵒᵈ) (larger value, then smaller index); distinct values are not assumed. The optimal time is the smallest maximizing time, so that the $\mathsf{OPT}_c$ add up to $\mathbb E[\mathsf{OPT}]$ . Competitiveness is stated multiplicatively, never as a quotient, so $\mathbb E[\mathcal A]=0$ is not a loophole.

The goal is a statement about the specific algorithm $\mathcal A$ , not "there exists an algorithm": an existential over unrestricted algorithms is witnessed by a clairvoyant rule that reads the values in advance. $\mathcal A$ sees the values only through comparisons among arrivals that have already occurred, and $\mathbb E[\mathsf{OPT}]$ is the expected offline maximum over the same random order, not $d_{\max}v_{\max}$ .

Needed infrastructure: averages over permutations and the fact that the elements landing at a fixed set of times form a uniformly random subset in uniformly random order; the finite- $m$ analysis of the classical rule; and elementary estimates on geometric sums. Contributions of general lemmas about uniform permutations are welcome and reusable.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.139
E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Math. Doklady 4, 1963.
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493
L. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2, 1976. https://doi.org/10.1007/BF01458209
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007. https://dl.acm.org/doi/10.5555/1283383.1283429

9 thms3 active usersReviewed

Completed

Combinatorics Machine Learning Operations Research·Captain: mikedeng1

How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design 1: Pseudo-Dimension Bound from a Piecewise-Decomposable Dual ClassResearch Paper

Motivation

Many algorithms in operations research and computer science have tunable parameters: sequence-alignment weights, clustering linkage interpolations, branch-and-bound branching rules, auction reserve prices. In data-driven algorithm design the parameters are chosen by optimizing average performance over a training set of problem instances drawn from an unknown application-specific distribution. The question this mission is about is statistical: how many training instances suffice for the empirical average performance of every parameter setting to be close to its expected performance?

Classical learning theory answers this through the pseudo-dimension of the class of utility functions (Pollard, 1984): a bound on the pseudo-dimension gives a uniform convergence bound of order $H\sqrt{(\mathrm{Pdim} + \ln(1/\delta))/N}$ . The difficulty is that utility functions of combinatorial algorithms are wildly discontinuous in the parameters, so standard tools (Lipschitz arguments, linear classes) do not apply. Balcan, DeBlasio, Dick, Kingsford, Sandholm and Vitercik (arXiv:1908.02894v4, STOC 2021) observed that for a large family of algorithms the utility on each fixed instance is a piecewise-structured function of the parameters, and proved a single general theorem converting that structure into a pseudo-dimension bound. Earlier analyses (for example Gupta and Roughgarden 2017; Balcan, Nagarajan, Vitercik and White 2017) derived such bounds one algorithm family at a time; Theorem 3.3 unifies them.

Setting

Let $\mathcal X$ be a set of problem instances and $\mathcal U \subseteq \mathbb R^{\mathcal X}$ a class of utility functions; in the paper $\mathcal U = \{u_\rho : \rho \in \mathcal P\}$ for a parameter space $\mathcal P \subseteq \mathbb R^d$ , with $u_\rho(x)$ the performance of the algorithm with parameter $\rho$ on instance $x$ .

Pseudo-dimension. A class $\mathcal H$ of real functions on a domain $\mathcal Y$ shatters points $y_1, \dots, y_N$ if there are targets $z_1, \dots, z_N \in \mathbb R$ such that every one of the $2^N$ patterns of "above / not above $z_i$ " at the points $y_i$ is realized by some $h \in \mathcal H$ . The pseudo-dimension $\mathrm{Pdim}(\mathcal H)$ is the largest $N$ for which some $N$ points are shattered. For $\{0,1\}$ -valued classes it is the VC-dimension $\mathrm{VCdim}(\mathcal H)$ .

Dual class (Definition 3.1). For $\mathcal H \subseteq \mathbb R^{\mathcal Y}$ , each $y \in \mathcal Y$ gives an evaluation map $h^*_y : \mathcal H \to \mathbb R$ , $h^*_y(h) = h(y)$ , and $\mathcal H^* = \{h^*_y : y \in \mathcal Y\}$ . For utility functions, $u^*_x(u_\rho) = u_\rho(x)$ : the dual function of instance $x$ records performance on $x$ as the algorithm varies.

Piecewise decomposability (Definition 3.2). Given a class $\mathcal G \subseteq \{0,1\}^{\mathcal Y}$ of boundary functions, a class $\mathcal F \subseteq \mathbb R^{\mathcal Y}$ of piece functions and $k \in \mathbb N$ , a class $\mathcal H \subseteq \mathbb R^{\mathcal Y}$ is $(\mathcal F, \mathcal G, k)$ -piecewise decomposable if every $h \in \mathcal H$ admits $g^{(1)}, \dots, g^{(k)} \in \mathcal G$ and, for each bit vector $\boldsymbol b \in \{0,1\}^k$ , some $f_{\boldsymbol b} \in \mathcal F$ , with $h(y) = f_{\boldsymbol b_y}(y)$ where $\boldsymbol b_y = (g^{(1)}(y), \dots, g^{(k)}(y))$ . The theorem applies this to $\mathcal H = \mathcal U^*$ , so $\mathcal F \subseteq \mathbb R^{\mathcal U}$ and $\mathcal G \subseteq \{0,1\}^{\mathcal U}$ , and their duals $\mathcal F^*$ , $\mathcal G^*$ are classes of functions on $\mathcal F$ and $\mathcal G$ .

Formalization targets

Goal: Theorem 3.3, explicit form

Suppose $\mathcal U^*$ is $(\mathcal F, \mathcal G, k)$ -piecewise decomposable, $k \ge 1$ , $d_F = \mathrm{Pdim}(\mathcal F^*)$ , $d_G = \mathrm{VCdim}(\mathcal G^*)$ and $D = d_F + d_G$ . With $a = D/\ln 2$ and $b = (D + d_G\ln k)/\ln 2$ ,

\mathrm{Pdim}(\mathcal U) \le 4a\ln(2a) + 2b = O\bigl(D\ln D + d_G \ln k\bigr).

This is the explicit bound behind the printed $O(\cdot)$ ; it is what the paper's proof establishes.

Milestones, in the order the proof uses them

Lemma 3.4. For $h_1, \dots, h_N$ in a $\{0,1\}$ -valued class $\mathcal H$ ( $N \ge 1$ ),

|\{(h_1(y), \dots, h_N(y)) : y \in \mathcal Y\}| \le (eN)^{\mathrm{VCdim}(\mathcal H^*)}.

Claim 3.5. For instances $x_1, \dots, x_N$ , the class $\mathcal U$ splits into $M \le (ekN)^{d_G}$ cells (strictly fewer when $d_G \ge 1$ ) on each of which every $u^*_{x_i}$ coincides with one fixed piece function $f_i \in \mathcal F$ .
Eq. (7). On any cell, fixed piece functions $f_1, \dots, f_N$ realize at most $(eN)^{d_F}$ label vectors $(\mathbb 1[f_i(u) > z_i])_i$ .
Eq. (5). The whole class realizes at most $(ekN)^{d_G}(eN)^{d_F}$ label vectors $(\mathbb 1[u(x_i) > z_i])_i$ .
Shattering inequality. If $\mathcal U$ shatters $x_1, \dots, x_N$ ( $N \ge 1$ ), then $2^N \le (ekN)^{d_G}(eN)^{d_F}$ .
Lemma A.1. For $a \ge 1$ , $b > 0$ : $y < a\ln y + b$ implies $y < 4a\ln(2a) + 2b$ .

Significance

Theorem 3.3 is the engine behind every generalization guarantee in the paper. It is instantiated for piecewise-constant and piecewise-linear duals over $\mathbb R^d$ (Lemmas 3.8–3.10), and through them for sequence alignment, RNA folding, hierarchical clustering, integer programming (branch-and-bound), greedy algorithms and auction design. Combined with the classical uniform convergence bound, it says that $\tilde O(H^2(D + d_G\ln k)/\varepsilon^2)$ training instances suffice to tune any such algorithm to within $\varepsilon$ of its optimal expected performance. The matching lower bounds in the paper (Theorems 4.3 and 5.2) show that the bound is tight up to logarithmic factors.

The result is proved in the paper; to the best of available records it has not been machine-checked. The mission formalizes the known proof, including the dual-class version of Sauer's lemma and the counting argument over the partition induced by the boundary functions. The published Sauer's lemma FoundationsML.RademacherVC.sauer_lemma is included as a reference item, as it is the tool Lemma 3.4 cites.

Difficulty

The obvious approach, bounding the pseudo-dimension of $\mathcal U$ directly from the complexity of $\mathcal F$ and $\mathcal G$ , fails: the piecewise structure lives on the dual side, and nothing about $\mathcal F$ or $\mathcal G$ themselves controls how $\mathcal U$ labels instances. The bound has to pass through dual classes twice and through the dual of a dual once, and Sauer's lemma, which counts labelings of fixed points by varying functions, must be applied in the transposed direction. Formally, the counting step needs bookkeeping of label vectors under a partition indexed by $kN$ boundary functions, and a conversion from a pseudo-dimension bound on $\mathcal F^*$ to a VC-dimension bound on the thresholded class $\{(f, z) \mapsto \mathbb 1[f(u) > z]\}$ , which needs the observation that a shattered tuple of pairs has distinct first coordinates.

Formalization scope

Pseudo- and VC-dimension are the published FoundationsML predicates Shatters, PseudoDim, GrowthFunction, HasVCDim. The exact-value predicates fix finite dimensions $d_F$ , $d_G$ , which the paper's bound presupposes. " $\mathrm{Pdim}(\mathcal U) \le B$ " is stated as "every shattered tuple has length at most $B$ ". $\{0,1\}$ is Bool.
Sign convention. Shattering uses strict thresholds $u(x_i) > z_i$ ; the paper leaves $\mathrm{sign}(0)$ unspecified, and strict and non-strict thresholds shatter the same tuples, so the dimension is unchanged. Label vectors in the counting milestones use the same reading.
Domains. The dual classes are classes of functions on the subtype of the primal class. Parameters $\rho$ are indexed by the functions $u_\rho$ themselves, and Claim 3.5's partition of $\mathcal P$ becomes a partition of $\mathcal U$ ; nothing in the theorem depends on $\rho$ except through $u_\rho$ .
Corrections of the printed statements. (i) Theorem 3.3's $O(\cdot)$ is replaced by the explicit bound $4a\ln(2a) + 2b$ derived from the paper's own last step and Lemma A.1, with $k \ge 1$ added (the printed $\ln k$ is undefined at $k = 0$ ); the case $D = 0$ is covered, where the bound is $0$ . (ii) Lemma 3.4 and the counting milestones assume $N \ge 1$ ; at $N = 0$ the printed bounds read $1 \le 0$ . (iii) Claim 3.5's strict $M < (ekN)^{\mathrm{VCdim}(\mathcal G^*)}$ is kept for $\mathrm{VCdim}(\mathcal G^*) \ge 1$ and weakened to $\le$ only when $\mathrm{VCdim}(\mathcal G^*) = 0$ , where the strict form is false ( $M = 1$ ). The milestone texts are quoted verbatim.
Dropped hypothesis. The range $[0, H]$ of the utility functions is not used by the theorem or its proof and is omitted, which makes the statement more general.
Ruling out trivializations. The goal carries the explicit constant, never an $O(\cdot)$ with a constant chosen after the classes; the hypotheses are jointly satisfiable on a nontrivial example (one instance, $u_\rho(x) = \rho$ , $k = 1$ , $d_F = 1$ , $d_G = 0$ , in which $\mathcal U$ does shatter one point), checked by a sorry-free local verification file; all counts are of subsets of $\{0,1\}^N$ , so no cardinality silently defaults to zero.
Contributions welcome: proofs of each milestone; a dual-class Sauer lemma reusable for other data-driven design papers; the passage from pseudo-dimension of $\mathcal F^*$ to the VC-dimension of its thresholded class.

Selected references

M.-F. Balcan, D. DeBlasio, T. Dick, C. Kingsford, T. Sandholm, E. Vitercik, How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design, STOC 2021; arXiv:1908.02894v4, 2021. https://arxiv.org/abs/1908.02894
P. Assouad, Densité et dimension, Annales de l'Institut Fourier 33(3), 1983. https://doi.org/10.5802/aif.938
D. Pollard, Convergence of Stochastic Processes, Springer, 1984. https://doi.org/10.1007/978-1-4612-5254-2
N. Sauer, On the density of families of sets, Journal of Combinatorial Theory A 13(1), 1972. https://doi.org/10.1016/0097-3165(72)90019-2
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014. https://doi.org/10.1017/CBO9781107298019
R. Gupta, T. Roughgarden, A PAC approach to application-specific algorithm selection, SIAM Journal on Computing 46(3), 2017. https://doi.org/10.1137/15M1050276

14 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Sequencing with Earliness and Tardiness Penalties: With Due-Date Tolerances, the Least Optimal Common Due Date Puts One Job at an End of Its Tolerance WindowResearch Paper

Motivation

Earliness/tardiness (E/T) scheduling penalizes a job both for finishing late and for finishing early. It models just-in-time production, where an early job ties up inventory and a late one delays a customer. Baker and Scudder's review (Oper. Res. 38 (1990) 22–36) organized the single-machine E/T literature around a short list of structural properties of optimal schedules for a common due date shared by all jobs. For the problem without tolerances these properties go back to work the review surveys, beginning with Kanet (1981) for equal penalties.

The review then turns to due-date tolerances: a job pays nothing if it completes within a window around the due date, as in contracts that accept delivery within a few days of a target. Cheng (1988) studied a version in which the penalty is discontinuous at the window ends. Baker and Scudder state the continuous version and prove two generalized properties, III(G) and IV(G), in the paper's Appendix (pp. 34–35). They are the paper's own results; the rest of the review cites results proved elsewhere.

Setting

Fix $n \ge 1$ jobs, processed on one machine in a fixed order, one after another, starting at time $0$ with no idle time between them. The job in position $j$ has a processing time $p_j$ , so it completes at $C_j = p_1 + \dots + p_j$ . All jobs share a common due date $d \in \mathbb R$ , which is a decision variable. Job $j$ has tolerances $u_j, v_j \ge 0$ and is free of penalty when $C_j \in [d - u_j,\ d + v_j]$ . Outside its window it pays a unit earliness penalty $\alpha_j > 0$ or a unit tardiness penalty $\beta_j > 0$ :

E_j = (d - C_j - u_j)^+,\qquad T_j = (C_j - d - v_j)^+,\qquad f(d) = \sum_{j=1}^n \bigl(\alpha_j E_j + \beta_j T_j\bigr).

The tolerances are small compared with the processing times: $p_j - v_j - u_i > 0$ for distinct jobs $i \ne j$ . Under this condition at most one job can avoid penalty costs. A due date is optimal if it minimizes $f$ over $\mathbb R$ , and the least optimal due date is the smallest optimal one. The paper minimizes $d$ as a secondary criterion when there are alternative optima.

In Lean the model is BakerScudder1990.Tolerance.Instance n, with fields p u v α β : Fin n → ℝ, completion times I.C, earliness I.earliness d, tardiness I.tardiness d, total penalty I.cost d, and the predicates I.IsOptimalDueDate and I.IsLeastOptimalDueDate.

Formalization targets

Goal: Property IV(G)

Let $d$ be the least optimal due date and let $b$ be the number of jobs with $T_j = 0$ . Then a least optimal due date exists, and exactly one of the following holds:

\begin{aligned} C_b &= d + v_b \quad\text{with}\quad \textstyle\sum_{i<b}\alpha_i < \sum_{i\ge b}\beta_i,\ \ \sum_{i<b}\alpha_i \ge \sum_{i>b}\beta_i,\\ C_b &= d - u_b \quad\text{with}\quad \textstyle\sum_{i<b}\alpha_i < \sum_{i>b}\beta_i,\ \ \sum_{i\le b}\alpha_i \ge \sum_{i>b}\beta_i. \end{aligned}

The case labels follow the paper's proof. The printed statement swaps them (see Formalization scope).

Milestones

Case 1 of the proof of III(G). Between the window of job $j-1$ and the window of job $j$ , $f$ is affine with slope $\sum_{i<j}\alpha_i - \sum_{i\ge j}\beta_i$ . Before the first window and after the last, the slopes are $-\sum_i\beta_i$ and $\sum_i\alpha_i$ .
Case 2 of the proof of III(G). Inside the window of job $j$ , $f$ is affine with slope $\sum_{i<j}\alpha_i - \sum_{i>j}\beta_i$ .
Property III(G). A least optimal due date exists, and at it some job completes at $d - u_j$ or at $d + v_j$ .
The two optimality conditions. The first pair of inequalities above makes $C_j - v_j$ the least optimal due date, and the second pair makes $C_j + u_j$ the least optimal due date.

Significance

III(G) reduces the choice of an optimal common due date for a given sequence to $2n$ candidates. IV(G) goes further and names the candidate directly from prefix and suffix sums of the penalties. Baker and Scudder use this to say which V-shaped sequences remain candidates for optimality, so that an enumeration over sequences can discard the others. With $u_j = v_j = 0$ the two properties reduce to the classical common-due-date conditions: some job completes exactly at $d$ , and which one is fixed by a weighted-median condition.

The results are proved in the paper, so the formalization does not settle an open question. It produces a machine-checked version of the Appendix, with two printed errors corrected, and a reusable model of single-machine E/T costs with tolerance windows. No earliness/tardiness model or result was formalized on Prove2Me as of October 2026.

Difficulty

Each linear piece of $f$ is elementary. The work lies in showing that the pieces are the claimed ones: the tolerance condition must imply that a job before position $j$ is early, and a job after it tardy, throughout each gap and window. That needs the ordering $C_i + u_i < C_j - v_j$ for every $i < j$ , not only for consecutive jobs. The second point is the least optimal due date. Optimality alone does not determine $d$ on a flat stretch of $f$ , where every point is optimal and only the left end satisfies the strict inequalities. Existence of a least minimizer also has to be shown, from the two outer slopes and finitely many breakpoints. Finally, the count $b$ of jobs without tardiness must be matched to the position of the critical job at both kinds of breakpoint.

Formalization scope

Jobs are indexed by 0-based positions Fin n, so the paper's job $b$ is position $k = b - 1$ and the goal states the count of untardy jobs as $k+1$ . Data are real numbers. $(x)^+$ is max 0 x.
The sequence starts at time $0$ and $d$ ranges over all of $\mathbb R$ ; this is the unrestricted problem, which is the one where the paper asserts III(G) and IV(G). Shifting the start time is equivalent to shifting $d$ .
"In an optimal schedule" is read for a fixed sequence and its least optimal due date. If a sequence and due date are jointly optimal with $d$ least among such optima, then $d$ is the least optimal due date for that sequence, so this reading implies the paper's.
The tolerance condition is assumed only for distinct jobs. That is a weaker hypothesis than the literal "for all pairs $(i,j)$ ", so the theorems are stronger.
Errata, corrected and disclosed. (i) IV(G) is printed (p. 30 and p. 35) with its two case labels swapped relative to its own proof. One job with $u_1, v_1 > 0$ has least optimal due date $C_1 - v_1$ , so $C_1 = d + v_1$ while the first condition pair holds. (ii) In Cases 1 and 2 the identity is printed as $f(S) - f(S') = [\dots]\varepsilon$ ; the correct one is $f(S') - f(S) = [\dots]\varepsilon$ . The milestone texts are quoted as printed; the Lean states the corrected mathematics.
Existence of a least optimal due date is a conjunct of III(G) and of IV(G), and both assume $n \ge 1$ . A version quantifying only over least optimal due dates without existence would be vacuous. A version for every optimal due date would be false. Neither is acceptable.
The optimality conditions are stated as sufficient. Their converse fails when $u_j = v_j = 0$ .
Properties I and II (no inserted idle time, V-shaped sequences) are quoted in the paper, not proved there, and are not formalized. Optimization over sequences is out of scope.
Welcome contributions: proofs of the two slope identities (finite sums of max 0 terms with a sign determined on each piece), a general lemma that a convex piecewise-linear coercive function on $\mathbb R$ attains its least minimizer at a breakpoint, and the special cases $u = v = 0$ as corollaries.

Selected references

K. R. Baker and G. D. Scudder, Sequencing with earliness and tardiness penalties: a review, Operations Research 38(1) (1990) 22–36. https://doi.org/10.1287/opre.38.1.22
J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28 (1981) 643–651 (as cited in Baker and Scudder 1990).
U. Bagchi, R. S. Sullivan and Y.-L. Chang, Minimizing mean absolute deviation of completion times about a common due date, Naval Research Logistics Quarterly 33 (1986) 227–240 (as cited in Baker and Scudder 1990).
T. C. E. Cheng, Optimal common due date with limited completion time deviation, Computers & Operations Research 15 (1988) 91–96 (as cited in Baker and Scudder 1990).

6 thms3 active usersReviewed

Completed

Machine Learning Markov Chain Reinforcement Learning+1·Captain: mikedeng1

Reinforcement Learning: An Introduction VI: Batch TD(0) Converges to the Certainty-Equivalence EstimateTextbook

Why batch TD(0) and batch Monte Carlo disagree

Temporal-difference (TD) learning estimates the value of each state of a Markov reward process from observed experience, updating an estimate toward a target built from the next reward and the current estimate of the next state. Monte Carlo (MC) methods instead update toward the full observed return. Both are standard prediction methods in reinforcement learning, and their relationship is a recurring question of the field (Sutton 1988).

When only a finite amount of experience is available, a common practice is to present the same data repeatedly until the estimates stop changing. Chapter 6 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses this setting to explain why TD(0) is often faster: under such batch updating, both methods converge deterministically, but to different answers. Batch MC finds the least-squares fit to the observed returns; batch TD(0) finds the value function of the maximum-likelihood Markov model of the data, the certainty-equivalence estimate. The comparison appears in §6.3, Optimality of TD(0) (pp. 126–128), and is illustrated by Example 6.4, You are the Predictor. The book states these conclusions without proof. This mission formalizes them.

Setting

Let $\mathcal S$ be a finite set of nonterminal states and $\mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$ . An episode is a finite sequence $S_0, R_1, S_1, \dots, S_{T-1}, R_T, S_T$ with $S_0, \dots, S_{T-1} \in \mathcal S$ , real rewards $R_1, \dots, R_T$ , and $S_T$ terminal. A batch is a finite list of episodes. A visit of $s$ is an (episode, time $t < T$ ) pair with $S_t = s$ , and $n(s)$ counts all visits (every-visit counting).

A value array $V : \mathcal S \to \mathbb R$ is extended by $V(\text{terminal}) = 0$ . For a discount rate $\gamma \in [0,1]$ , the return is $G_t = \sum_{k=t+1}^{T}\gamma^{k-t-1}R_k$ and the TD error is $\delta_t = R_{t+1} + \gamma V(S_{t+1}) - V(S_t)$ .

Batch TD(0) with step size $\alpha$ computes the TD(0) increment for every visit in the batch and changes $V$ once, by their sum:

V_{m+1}(s) = V_m(s) + \alpha\sum_{\text{visits } t \text{ of } s}\big[R_{t+1} + \gamma V_m(S_{t+1}) - V_m(S_t)\big].

Batch constant- $\alpha$ MC is the same iteration with the increment $G_t - V_m(S_t)$ .

The maximum-likelihood model of the batch has transition probabilities $\hat p(j \mid i) = N(i,j)/n(i)$ , where $N(i,j)$ counts the observed transitions from $i$ to $j \in \mathcal S^+$ , and expected rewards $\hat r(i,j)$ equal to the average reward observed on those transitions. With $\hat P = (\hat p(s'\mid s))_{s,s'\in\mathcal S}$ and $\hat r(s) = \sum_j \hat p(j\mid s)\hat r(s,j)$ , the certainty-equivalence estimate is the value function of this Markov reward process,

\hat v(s) = \sum_{k\ge0}\gamma^k\big(\hat P^k\hat r\big)(s).

Formalization targets

Goal: batch TD(0) converges to the certainty-equivalence estimate

For every finite batch and every $\gamma \in [0,1]$ , the series defining $\hat v$ converges, and there is $\bar\alpha > 0$ such that for all $\alpha \in (0,\bar\alpha)$ and all initial arrays $V_0$ ,

\lim_{m\to\infty} V_m(s) = \hat v(s)\quad\text{for every visited } s, \qquad V_m(s) = V_0(s)\ \text{otherwise}.

The limit depends neither on $\alpha$ nor on $V_0$ at visited states.

Milestones

(6.6): with $V$ held fixed, $G_t - V(S_t) = \sum_{k=t}^{T-1}\gamma^{k-t}\delta_k$ .
Exercise 6.8: the same identity for action values, $\delta_t = R_{t+1} + \gamma Q(S_{t+1},A_{t+1}) - Q(S_t,A_t)$ .
Least squares: the sample averages $\bar G(s)$ of the returns after the visits to $s$ minimize $\sum_{\text{visits}}(G_t - V(S_t))^2$ over all arrays $V$ .
Batch MC: for small $\alpha$ , batch constant- $\alpha$ MC converges to $\bar G(s)$ at every visited $s$ .
Fixed points: the batch TD(0) increments vanish everywhere if and only if $V = \hat v$ on visited states.
Example 6.4: on the eight episodes $A,0,B,0$ ; $B,1$ (six times); $B,0$ with $\gamma = 1$ , the certainty-equivalence estimate is $\hat v(A) = \hat v(B) = 3/4$ and batch TD(0) converges to it, while batch MC converges to $V(A) = 0$ , $V(B) = 3/4$ .

Significance

The result explains the empirical observation of Figure 6.2 in the book: batch TD(0) has lower error than batch MC on Markov data, because it computes the certainty-equivalence estimate, while batch MC fits the training returns. It also gives a precise meaning to the claim that TD methods approximate the certainty-equivalence solution with memory linear in the number of states, where computing it directly needs a model of quadratic size and cubic time (p. 128). Identity (6.6) is the starting point of the $n$ -step and eligibility-trace methods of later chapters.

The comparison under repeated presentation of a finite training set goes back to Sutton 1988, but the textbook states the conclusions without proof, and no machine-checked version is known to exist. The formalization pins down every hypothesis the text leaves implicit: the step-size threshold, the treatment of unvisited states, every-visit counting, and the undiscounted case.

Difficulty

The fixed-point equation of batch TD(0) is $D(\hat r + \gamma\hat PV - V) = 0$ on visited states, with $D$ the diagonal of visit counts, and convergence of the iteration $V \mapsto V + \alpha D(\hat r + \gamma\hat P V - V)$ requires every eigenvalue of $D(I - \gamma\hat P)$ to have positive real part. For $\gamma < 1$ this follows from $\hat P$ being substochastic. For $\gamma = 1$ , the case of Example 6.4, $\hat P$ is only substochastic and the naive contraction argument fails: invertibility of $I - \hat P$ must be derived from the structure of the data, since every episode ends in the terminal state. The matrix $D(I - \gamma\hat P)$ is not symmetric, so symmetric positive-definiteness arguments do not apply. The same issue makes convergence of the series defining $\hat v$ nontrivial at $\gamma = 1$ .

Formalization scope

An episode is a Lean List (X × ℝ) of transitions $(S_t, R_{t+1})$ , with the terminal state represented by none : Option X; a batch is a list of episodes; states form a Fintype. Values at the terminal state are $0$ by definition. The certainty-equivalence estimate is defined from returns as the series $\sum_k\gamma^k\hat P^k\hat r$ , not as the solution of a Bellman equation, and its convergence is part of the goal, not assumed. "Sufficiently small $\alpha$ " is an existential threshold $\bar\alpha > 0$ quantified before $\alpha$ and $V_0$ ; a statement for one fixed $\alpha$ , or for some $\alpha$ , would be weaker than the book's and is ruled out. Unvisited states receive no increment and keep their initial value; the goal records this rather than claiming convergence to $\hat v$ there. The standing assumption $\gamma \in [0,1]$ includes $\gamma = 1$ . Every visit is counted in both the TD increments and the model; mixing first-visit and every-visit counts would make the goal false.

The mission needs only finite sums, matrix powers and limits of real sequences; Mathlib's Matrix and Filter.Tendsto suffice. A lemma that a nonnegative matrix whose rows reach an absorbing mass has spectral radius below one would be reusable beyond this mission, as would a convergence criterion for $V \mapsto V + \alpha(b - MV)$ when $M$ is a nonsingular M-matrix. Contributions of either kind, and of the elementary milestones 1–3, are welcome.

Selected references

Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §6.1 and §6.3, pp. 119–129. http://incompleteideas.net/book/the-book-2nd.html
Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 9–44, 1988. https://doi.org/10.1007/BF00115009

9 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time: Delayed SWPT Has Competitive Ratio 2Research Paper

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$ , needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$ ; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$ . Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$ ) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$ , and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$ -competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$ -competitive deterministic algorithm from an LP relaxation.
2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$ , integer processing times $p_j \ge 1$ and real weights $w_j > 0$ . A schedule assigns each job an integer start time $S_j$ . It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$ .

Delayed SWPT runs over unit time slots $[t, t+1)$ . When the machine is available at time $t$ , it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$ . Ties go to the smaller $p_j$ , then to the smaller index. If $p_j \le t$ , it starts $j$ at $t$ and the machine is busy until $t + p_j$ . Otherwise the machine stays idle and the rule is applied again at $t+1$ . The resulting schedule is written $\pi$ , or dswpt I in Lean. In particular no job starts before time $p_j$ .

The proof uses three auxiliary problems:

the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$ ;
the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$ , where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$ .

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$ .

Formalization targets

Goal: Theorem 8

\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

$\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
$\pi_E$ is feasible for (E) (§3.2).
Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$ .
Lemma 2. $\pi_E$ is optimal for (E).
Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}

then $C(\pi) \le 2\,C(S)$ for every feasible $S$ . 6. Inequality (1) holds for some feasible $\sigma_E$ , for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$ . The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

an executable, verified-terminating definition of an online scheduling rule;
the doubling lemma for release-date problems;
the optimality criterion behind Lemma 2;
the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$ .
Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$ . A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$ , and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

simulation invariants for the algorithm;
exchange and left-shift arguments for single-machine schedules;
the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106

11 thms3 active usersReviewed

Completed

Convex Optimization Numerical Analysis Optimization·Captain: mikedeng1

The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than 1/k^2 I: For α > 3, (Ψ + Φ)(x_k) − min(Ψ + Φ) = o(k⁻²) and ‖x_{k+1} − x_k‖ = o(k⁻¹)Research Paper

Motivation

Many problems in signal processing, statistics and machine learning take the form

\min_{x\in\mathcal H}\ \Psi(x)+\Phi(x),

where $\Phi$ is smooth and convex (a data-fit term) and $\Psi$ is convex but possibly nonsmooth or infinite-valued (an $\ell^1$ penalty, the indicator function of a constraint set). The forward-backward method alternates a gradient step on $\Phi$ with a proximal step on $\Psi$ and reduces the objective gap at rate $O(k^{-1})$ after $k$ iterations. Combining it with Nesterov's extrapolation scheme gives the accelerated forward-backward method, best known as FISTA, which improves the guaranteed rate to $O(k^{-2})$ . FISTA and its variants are standard solvers for sparse recovery and image reconstruction.

Timeline:

1983. Nesterov introduces the extrapolation scheme for smooth convex minimization, with an $O(k^{-2})$ rate for function values (Nesterov 1983).
2009. Beck and Teboulle extend it to the composite problem above (FISTA), with the $O(k^{-2})$ rate (doi:10.1137/080716542).
2014. Su, Boyd and Candès read the scheme as a discretization of the ODE $\ddot x+\frac{\alpha}{t}\dot x+\nabla\Theta(x)=0$ (arXiv:1503.01243).
2014–2015. Chambolle and Dossal (doi:10.1007/s10957-015-0746-4) and, independently, Attouch, Chbani, Peypouquet and Redont (arXiv:1507.04782) prove weak convergence of the iterates for the variant with parameter $\alpha>3$ . Before that, convergence of the iterates had been open for about two decades.
2015. May shows that for $\alpha>3$ the continuous-time gap is $o(t^{-2})$ (arXiv:1509.05598).
2016. Attouch and Peypouquet prove the discrete analogue: for $\alpha>3$ the function gap of the algorithm is $o(k^{-2})$ and the velocity is $o(k^{-1})$ (arXiv:1510.08740, SIAM J. Optim. 26(3):1824–1834).

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let:

$\Psi:\mathcal H\to\mathbb R\cup\{+\infty\}$ be proper (finite somewhere), lower semicontinuous and convex;
$\Phi:\mathcal H\to\mathbb R$ be convex and continuously differentiable, with gradient $\nabla\Phi$ Lipschitz continuous with constant $L$ ;
$\Theta=\Psi+\Phi$ , and assume the set of minimizers $S=\operatorname{argmin}\Theta$ is nonempty.

For $s>0$ , the proximal map $\operatorname{prox}_{s\Psi}(z)$ is the unique minimizer of $u\mapsto\Psi(u)+\frac1{2s}\|u-z\|^2$ . Given $\alpha>0$ , a step size $0<s<1/L$ and starting points $x_0,x_1$ , algorithm (2) generates

y_k=x_k+\frac{k-1}{k+\alpha-1}(x_k-x_{k-1}),\qquad x_{k+1}=\operatorname{prox}_{s\Psi}\big(y_k-s\nabla\Phi(y_k)\big),\qquad k\ge1.

The common choice is $\alpha=3$ ; this mission concerns $\alpha>3$ .

The proofs use the operator $G_s(y)=\frac1s\big(y-\operatorname{prox}_{s\Psi}(y-s\nabla\Phi(y))\big)$ , the sequence $z_k=x_k+\frac{k-1}{\alpha-1}(x_k-x_{k-1})$ , a minimizer $x^*$ , and the quantity

\mathcal E(k)=\frac{2s}{\alpha-1}(k+\alpha-2)^2\big(\Theta(x_k)-\Theta(x^*)\big)+(\alpha-1)\|z_k-x^*\|^2 .

Write $\theta_k=\Theta(x_k)-\Theta(x^*)$ and $d_k=\frac1{2s}\|x_{k+1}-x_k\|^2$ .

Formalization targets

Goal: Theorem 1 (p. 2)

For $\alpha>3$ and $0<s<1/L$ ,

\lim_{k\to\infty}k^2\big(\Theta(x_k)-\min\Theta\big)=0\qquad\text{and}\qquad\lim_{k\to\infty}k\,\|x_{k+1}-x_k\|=0.

The statement fixes no constants, so it is unaffected by later improvements of the explicit bounds below.

Milestones (in attack order)

(9), p. 2. If $sL\le1$ , then for all $x,y$ : $\Theta(y-sG_s(y))\le\Theta(x)+\langle G_s(y),y-x\rangle-\frac s2\|G_s(y)\|^2$ .
(13), p. 3. For $\alpha\ge3$ and $k\ge1$ : $\mathcal E(k+1)+2s\frac{\alpha-3}{\alpha-1}k\,\theta_k\le\mathcal E(k)$ .
Fact 1, p. 3. $(\mathcal E(k))$ is nonincreasing and has a finite limit.
Fact 2, p. 3. $\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(k+\alpha-2)^2}$ and $\|z_k-x^*\|^2\le\frac{\mathcal E(1)}{\alpha-1}$ for $k\ge1$ .
Fact 3, p. 3. For $\alpha>3$ : $\sum_{k\ge1}k\,\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(\alpha-3)}$ .
(14), p. 4. $\Theta(x_{k+1})+d_k\le\Theta(x_k)+\frac{(k-1)^2}{(k+\alpha-1)^2}d_{k-1}$ for $k\ge1$ .
Fact 4, p. 4. For $\alpha>3$ : $\sum_{k\ge1}k\,d_k\le\frac{\alpha(3\alpha-5)\mathcal E(1)}{4s(\alpha-1)(\alpha-3)}$ .
Lemma 2, p. 4. For $\alpha>3$ , $\lim_k\big[k^2d_k+(k+1)^2\theta_{k+1}\big]$ exists and is finite.

Significance

The result. The $O(k^{-2})$ rate of FISTA is often quoted as optimal for first-order methods. Theorem 1 shows that for $\alpha>3$ the worst-case rate along every single run is strictly better, $o(k^{-2})$ , and that the steps $\|x_{k+1}-x_k\|$ decay faster than $1/k$ . No better power is possible: by Attouch et al., Example 2.13 there is no $p>2$ with an $O(k^{-p})$ rate for every $\Phi$ and $\Psi$ . The intermediate estimates (Facts 2–4) give explicit, quantitative bounds that are reused in the analysis of inexact and perturbed variants (Theorem 4 of the paper) and in mission II of this series, which proves weak convergence of the iterates.

Formalizing it. The result is proved on paper. As far as we know, no machine-checked proof of the $O(k^{-2})$ rate of FISTA in this Hilbert-space, extended-valued setting exists in Mathlib or on this platform, and neither does the $o(k^{-2})$ refinement. A complete development would provide reusable statements about proximal-gradient steps for functions valued in $\mathbb R\cup\{+\infty\}$ . The page also has a factor slip in Fact 4 and Lemma 2 (see Formalization scope); checking it mechanically is one of the outputs.

Difficulty

The $O(k^{-2})$ bound follows from the monotonicity of $\mathcal E$ alone. That argument cannot give $o(k^{-2})$ : it controls $k^2\theta_k$ only by the constant $\mathcal E(1)$ , and summability of $k\theta_k$ (Fact 3) gives a decay of $k^2\theta_k$ only along a subsequence, not of the whole sequence. The missing ingredient is convergence of a weighted combination of function gaps and velocities, which is Lemma 2. The bookkeeping is delicate: every step carries explicit coefficients in $k$ and $\alpha$ , and the inequalities must hold in the extended reals because $\Psi$ may be $+\infty$ at the starting point.

Formalization scope

Space and functions. $\mathcal H$ is a real inner product space that is complete. $\Psi$ takes values in EReal and satisfies the published predicate IsProperClosedConvex (never $-\infty$ , finite somewhere, lower semicontinuous, convex epigraph). $\Phi:\mathcal H\to\mathbb R$ is ConvexOn and ContDiff ℝ 1, and gradient Φ is LipschitzWith L for some L : ℝ≥0.
Step size. $0<s<1/L$ is written 0 < s and s * L < 1, so that $L=0$ is allowed (s < 1 / L would be unsatisfiable when $L=0$ ). Display (9) uses the page's $s\le1/L$ , written s * L ≤ 1.
Proximal map. It is a map P with the published predicate IsProx s Ψ P, which determines $P=\operatorname{prox}_{s\Psi}$ for proper closed convex $\Psi$ and $s>0$ .
The run. It is required to follow (2) for every $k\ge1$ , with $x_0,x_1$ arbitrary; the coefficient of $x_0$ vanishes at $k=1$ .
Extended reals. $\Theta$ , $\mathcal E$ and the function-value statements live in EReal. No value is ever converted to $\mathbb R$ with toReal, which would turn $+\infty$ into $0$ . "The limit exists" (Fact 1, Lemma 2) means convergence to a real number, because in EReal every monotone sequence converges. Infinite series of nonnegative terms are stated as bounds on every partial sum. $\min\Theta$ in the goal is ⨅ y, Θ y together with the hypothesis that a minimizer exists.
Corrected slips. Fact 2 is stated with $\mathcal E(1)$ for $k\ge1$ ; the page writes $\mathcal E(0)$ for $k\ge0$ , which needs an iterate $x_{-1}$ . Fact 4 is stated for $\sum k\,d_k$ ; the page prints $\sum k\|x_{k+1}-x_k\|^2$ with the same constant, which is off by the factor $2s$ and false in general. Lemma 2 is stated for the bracket $k^2d_k+(k+1)^2\theta_{k+1}$ of its proof (16).
Ruled out. The goal assumes nothing about $\mathcal E$ , $z_k$ , $\theta_k$ or $d_k$ . A statement of the first limit for toReal values, or with an extended-real "limit exists", would be trivially weaker and is not what is asked.
Welcome contributions. Proofs of any milestone; general facts about proximal maps of EReal-valued convex functions and about the descent property of $L$ -smooth convex functions, which are reusable well beyond this mission.

Selected references

H. Attouch, J. Peypouquet, The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than $1/k^2$ , SIAM J. Optim. 26(3):1824–1834, 2016. arXiv:1510.08740v4, doi:10.1137/15M1046095
H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168:123–175, 2018. arXiv:1507.04782
A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2(1):183–202, 2009. doi:10.1137/080716542
A. Chambolle, C. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166:968–982, 2015. doi:10.1007/s10957-015-0746-4
R. May, Asymptotic for a second order evolution equation with convex potential and vanishing damping term, 2015. arXiv:1509.05598
Y. Nesterov, A method of solving a convex programming problem with convergence rate $O(1/k^2)$ , Soviet Math. Dokl. 27:372–376, 1983. mathnet
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17(153):1–43, 2016. arXiv:1503.01243

11 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Correlated Equilibrium as an Expression of Bayesian Rationality I: Bayes Rationality at Every State Yields Exactly the Correlated Equilibrium DistributionsResearch Paper

Motivation

Nash equilibrium is the standard solution concept for strategic games, but it is usually justified by appeal to what players "would" do once they somehow coordinate on a profile. Correlated equilibrium, introduced by Aumann (J. Math. Econ. 1, 1974), enlarges the set of outcomes by letting players condition their actions on correlated private signals. In Correlated Equilibrium as an Expression of Bayesian Rationality (Econometrica 55, 1987), Aumann gave the concept a decision-theoretic foundation: if the players share a common prior over the states of the world and each player maximizes expected utility given his information at every state, then what they play is a correlated equilibrium — and every correlated equilibrium arises this way. The result is a standard entry point to the epistemic foundations of game theory, and correlated equilibria are central in algorithmic game theory because no-swap-regret learning dynamics converge to them (Foster–Vohra 1997; Hart–Mas-Colell 2000).

Timeline:

1974, Aumann: correlated equilibrium defined, in a measure-theoretic model with subjective probabilities and information σ-fields.
1987, Aumann: the Main Theorem (Bayes rationality at every state under a common prior implies correlated equilibrium play) and its converse, in a finite model with information partitions.

Setting

A game $G$ in strategic form has players $i$ , action sets $S^i$ , action $n$ -tuples $s\in S=S^1\times\dots\times S^n$ , and payoffs $h^i(s)\in\mathbb R$ .

A correlated strategy $n$ -tuple is a function $f:\Gamma\to S$ on a finite probability space $(\Gamma,q)$ , with $q\ge 0$ and $\sum_\gamma q(\gamma)=1$ . Its expected payoff is $Eh^i(f)=\sum_\gamma q(\gamma)h^i(f(\gamma))$ . For $g^i:\Gamma\to S^i$ , the profile $(f^{-i},g^i)$ replaces player $i$ 's coordinate of $f$ by $g^i$ . The function $f$ is a correlated equilibrium (Definition 2.1) if

Eh^i(f)\ \ge\ Eh^i(f^{-i},g^i)\qquad(2.2)

for every player $i$ and every $g^i$ that is a function of $f^i$ (i.e. $g^i=\varphi\circ f^i$ ). The distribution of $f$ assigns to each $s\in S$ the number $q\{f^{-1}(s)\}$ , and a correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium.

An information system consists of a finite set $\Omega$ of states of the world, a common prior $p$ on $\Omega$ , an information partition $\mathcal P^i$ of $\Omega$ for each player, and action functions $\mathbf s^i:\Omega\to S^i$ with $\mathbf s=(\mathbf s^1,\dots,\mathbf s^n)$ , each $\mathbf s^i$ constant on the elements of $\mathcal P^i$ (each player knows his own action). For a random variable $x$ , $E(x\mid\mathcal P^i)(\omega)$ is the $p$ -average of $x$ over the element of $\mathcal P^i$ containing $\omega$ . Player $i$ is Bayes rational at $\omega$ if

E\big(h^i(\mathbf s)\mid\mathcal P^i\big)(\omega)\ \ge\ E\big(h^i(\mathbf s^{-i},a)\mid\mathcal P^i\big)(\omega)\quad\text{for every }a\in S^i .

Formalization targets

Goal: Main Theorem with its converse

Q\ \text{is a c.e.d. of }G\iff\exists\ \text{information system }(\Omega,p,(\mathcal P^i),\mathbf s):\ \text{every player is Bayes rational at every state, and } Q(a)=p\{\mathbf s=a\}\ \forall a.

This is the two-sided statement the paper announces in its introduction (p. 2) and closes in Sect. 4d (p. 11): "under Bayesian rationality, the set of all information systems corresponds precisely to the set of all correlated equilibria."

Milestones

Main Theorem, proof: summing the cell-wise inequalities over the partition, $Eh^i(\mathbf s^{-i},g^i)\le Eh^i(\mathbf s)$ for $g^i$ constant on the cells of $\mathcal P^i$ .
Main Theorem, proof: $\mathbf s$ itself is a correlated equilibrium on $(\Omega,p)$ .
Main Theorem (p. 7): the distribution of $\mathbf s$ is a c.e.d.
Sect. 4d: in the system generated by $f$ (partitions generated by $f^i$ ), Bayes rationality everywhere is equivalent to (2.2).
Sect. 4d: every correlated equilibrium is realized by a Bayes-rational information system with the same distribution.

The mission also states, as a supporting lemma without a milestone, the cell-wise step of the proof of the Main Theorem: Bayes rationality at every state gives $E(h^i(\mathbf s^{-i},g^i)\mid P)\le E(h^i(\mathbf s)\mid P)$ on every cell $P$ for $g^i$ constant on cells.

Significance

The theorem identifies correlated equilibrium as the outcome of individual Bayesian decision making under a common prior, without any assumption that players randomize or that their choices are independent. It shows that the Nash equilibrium's independence requirement is not implied by rationality alone, and it is the template for later epistemic characterizations of solution concepts. On the computational side, correlated equilibrium distributions form a polytope described by linear inequalities (the companion mission of this series), which is why they are the tractable equilibrium notion in algorithmic game theory.

The result is proved in the paper; it has no machine-checked formalization known to this mission. Formalizing it pins down the exact role of the standing assumptions — finiteness, a common prior, measurability of each player's action with respect to his own partition, rationality at every state — and of the conditional expectation on cells of probability zero. The definitions (information systems, Bayes rationality, correlated equilibria as functions on a finite probability space) are reusable for later formalizations of the paper's Sect. 5 (subjective correlated equilibrium) and of other epistemic results.

Difficulty

The mathematics is short; the difficulty lies in the bookkeeping that the paper's notation hides. The hypothesis is interim (a conditional inequality at each state), while Definition 2.1 is ex ante (an unconditional inequality). Passing between them requires the law of total expectation over a partition whose cells may have probability zero, where conditional expectations are undefined. Deviations in Definition 2.1 are functions of $f^i$ , not arbitrary maps, and must be shown constant on cells, which uses measurability of $\mathbf s^i$ . A tempting first idea — that rationality against every fixed action already gives rationality against every deviation — fails without measurability: a player who does not know his own action could be rational at each state against constant deviations while a deviation $\varphi\circ\mathbf s^i$ varies inside his cells. The converse direction needs an information system that satisfies every axiom of the goal's right-hand side, not just one that is Bayes rational.

Formalization scope

Players form a finite type ι with decidable equality; action sets S i are arbitrary types (the paper's finiteness of $S^i$ is not used); payoffs are h : ι → (∀ i, S i) → ℝ.
Probability spaces are finite types with a real weight vector satisfying AGT.IsLottery (from the published definition agt_games). State spaces and the witnessing probability spaces of a c.e.d. range over Type; for finite sets this loses nothing.
Partitions are Setoids. The Common Prior Assumption is built into the information system, which has a single prior. Measurability of each action function is a field of the structure.
Conditional expectation on a cell is a ratio of finite sums; on a cell of probability zero Lean returns $0$ , so Bayes rationality at such states holds vacuously. The prior is not required to have full support. This matches the paper, whose argument multiplies each cell inequality by the cell's probability.
Deviations in Definition 2.1 are exactly the compositions $\varphi\circ f^i$ ; neither all maps nor only constant maps. A c.e.d. requires a genuine probability vector, ruling out the trivializing reading in which the zero weight function witnesses every $Q$ .
Contributions welcome: proofs of the milestones, a general law-of-total-expectation lemma for finite partitions, and lemmas relating distr to sums over action profiles.

Selected references

R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), no. 1, 1–18. https://doi.org/10.2307/1911154
R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

9 thms3 active usersReviewed

Completed

Dynamic Programming Machine Learning Optimization+1·Captain: mikedeng1

Reinforcement Learning: An Introduction III: The Policy Improvement Theorem and Policy IterationTextbook

Why policy improvement matters

Reinforcement learning methods search for good behaviour by alternating two activities: estimating how good the current behaviour is, and changing the behaviour in the direction those estimates suggest. Sutton and Barto call this pattern generalized policy iteration and use it as the organizing idea of their textbook (Sutton & Barto 2018, §4.6). Its mathematical justification is a single result of Chapter 4, the policy improvement theorem (p. 78): a comparison made one step ahead, at each state separately, certifies that a changed policy is at least as good everywhere. Policy iteration, value iteration, Monte Carlo control with ε-greedy policies (Chapter 5), Sarsa and Q-learning are all motivated by it.

The chapter's results go back to the foundations of dynamic programming: the Bellman optimality equation (Bellman 1957), and policy iteration with its finite termination for discounted finite Markov decision processes (Howard 1960). Standard modern treatments are Puterman 1994, Ch. 6, and Bertsekas 2012, Vol. II, Ch. 1.

Setting

A finite Markov decision process has a finite state set $\mathcal S$ , a finite nonempty action set $\mathcal A$ , a finite reward set $\mathcal R\subset\mathbb R$ and dynamics $p(s', r\mid s, a)$ : for each state $s$ and action $a$ , a probability distribution over the next state $s'$ and reward $r$ (Eqs. (3.2)–(3.3)). A policy $\pi$ gives probabilities $\pi(a\mid s)$ of choosing each action in each state; a deterministic policy is a map $\pi:\mathcal S\to\mathcal A$ .

Fix a discount rate $0\le\gamma<1$ . The state-value function of $\pi$ is the expected discounted return

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

and the action-value function is defined from it by (4.6):

q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)\,\big[r+\gamma v_\pi(s')\big],

the value of taking $a$ once in $s$ and following $\pi$ afterwards. A policy is optimal if its value is at least that of every policy at every state, and the optimal value function is $v_*(s)=\max_\pi v_\pi(s)$ . A deterministic policy $\pi'$ is greedy with respect to $q_\pi$ if $\pi'(s)\in\operatorname{argmax}_a q_\pi(s,a)$ for all $s$ (4.9).

Formalization targets

Goal: the policy improvement theorem, (4.7)–(4.8), p. 78

For deterministic policies $\pi,\pi'$ ,

\big(\forall s,\ q_\pi(s,\pi'(s))\ge v_\pi(s)\big)\ \Longrightarrow\ \big(\forall s,\ v_{\pi'}(s)\ge v_\pi(s)\big),

and at every state where the hypothesis is strict, the conclusion is strict at that same state.

Milestones

Iterative policy evaluation (4.5), p. 74. From any $v_0$ , the iterates $v_{k+1}(s)=\sum_a\pi(a\mid s)\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_\pi$ .
Greedy improvement (4.9), p. 79. A greedy $\pi'$ with respect to $q_\pi$ satisfies (4.7), hence $v_{\pi'}\ge v_\pi$ .
The stochastic case, p. 79. For stochastic $\pi,\pi'$ , with $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ as in (5.2), the theorem holds as stated, strictness included.
Equality forces optimality, p. 79. If a greedy $\pi'$ has $v_{\pi'}=v_\pi$ , then $v_{\pi'}$ solves the Bellman optimality equation (4.1), $v_{\pi'}=v_*$ , and $\pi$ and $\pi'$ are optimal.
Policy iteration, p. 80. For every sequence of deterministic policies with $\pi_{k+1}$ greedy with respect to $q_{\pi_k}$ : each step is a strict improvement unless $\pi_k$ is optimal, and from some $K$ on every $\pi_k$ is optimal with $v_{\pi_k}=v_*$ .
Value iteration (4.10), p. 83. $v_*$ is attained by one policy at all states, and from any $v_0$ the iterates $v_{k+1}(s)=\max_a\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_*$ .

Significance

The results. The policy improvement theorem turns a local test into a global guarantee: it is enough to check, state by state, that one step of the new policy followed by the old one does no worse than the old one. Combined with the finiteness of the set of deterministic policies, it yields the finite termination of policy iteration and, with the equality case, the existence of a deterministic optimal policy. The stochastic form is what Chapter 5 invokes for ε-greedy control. Value iteration is the other classical way to compute $v_*$ .

Formalizing them. All of these results are classical and proved in the literature cited above; they are not open. The textbook presents them informally ("we chose not to produce a rigorous formal treatment", p. xiii): the improvement theorem is argued by an unbounded chain of expansions, and the policy evaluation and value iteration convergence claims are stated without proof. The mission makes each claim precise with explicit hypotheses and asks for machine-checked proofs against the book's own model with four-argument dynamics and stochastic policies. Related platform results use different models (cost minimization with deterministic policies in Bertsekas's Dynamic Programming; an expected-reward kernel and an assumed fixed point in Foundations of Machine Learning), and none states the policy improvement theorem itself.

Difficulty

The book's proof expands $q_\pi$ with (4.6) and reapplies (4.7) indefinitely, ending with " $\le\cdots=v_{\pi'}(s)$ ". Made rigorous, the chain is an inequality between truncated returns plus a remainder $\gamma^n E_{\pi'}[v_\pi(S_{t+n})]$ , and the passage to the limit needs the remainder to vanish and the truncated returns to converge to $v_{\pi'}$ . Since $v_\pi$ is defined here as a series of expected rewards under the induced Markov chain, connecting it to the one-step quantities requires first establishing the Bellman equation for $v_\pi$ from that series. The strictness part does not follow from the weak inequality alone: strictness at one state must be shown to survive the averaging over later states, which requires tracking the contribution of the first step exactly. The policy iteration statement additionally requires handling ties: a greedy step taken from an optimal policy can move to a different optimal policy, so the sequence need not become constant.

Formalization scope

All objects live in the namespace SuttonBartoRL.DP. States and actions are finite types, actions nonempty where a maximum is taken; one action set serves all states (footnote 3, p. 48). Rewards form a finite set $\mathcal R\subset\mathbb R$ , and the dynamics are a function $p(s',r\mid s,a)$ whose values off $\mathcal R$ are never used. Policies are stochastic; deterministic policies are embedded as policies that choose one action with probability one.

Committed conventions:

Discount $0\le\gamma<1$ throughout. The book also allows $\gamma=1$ when "eventual termination is guaranteed" (p. 74) but never states that hypothesis precisely; the episodic case with a terminal state is out of scope. This is the only restriction relative to the text.
$v_\pi$ from returns. $v_\pi(s)=\sum_k\gamma^k(P_\pi^k r_\pi)(s)$ , with $P_\pi$ the state transition matrix of $\pi$ and $r_\pi$ its expected one-step reward. $q_\pi$ is defined by (4.6), as the book does. The Bellman equation (4.4) is not assumed. Defining $v_\pi$ as the fixed point of a Bellman operator would make the goal an order property of that operator and is excluded.
$v_*$ is the real supremum over all stochastic policies; the value iteration item also asserts it is attained. Optimality of a policy means dominance over all stochastic policies.
Greedy means $\pi'(s)$ is any maximizer of $q_\pi(s,\cdot)$ ; tie-breaking is arbitrary and may differ between iterations.
Stochastic case. The book only says the theorem "carries through as stated"; the meaning $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ is taken from the book's (5.2), p. 101.
Policy iteration is the idealized sequence with exact evaluation. The item does not claim that the boxed pseudocode on p. 80 stops, which it may fail to do under ties (Exercise 4.4, p. 82).
Convergence of iterates is in the product topology on $\mathbb R^{\mathcal S}$ , equivalent to the sup norm for finite $\mathcal S$ .

In-place (asynchronous) sweeps (§4.5) and truncated policy iteration are not formalized.

Needed infrastructure: summability of discounted series of bounded expected rewards, the Bellman equation for $v_\pi$ derived from the return definition, contraction arguments in the sup norm on $\mathbb R^{\mathcal S}$ , and finiteness of the set of deterministic policies. The definitions here duplicate those of the series' Chapter 3 mission and are intended to be merged with them; lemmas about $v_\pi$ , the Bellman equation and contraction are reusable by every later mission of the series, and contributions of such lemmas are welcome.

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 4. http://incompleteideas.net/book/the-book-2nd.html
R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/dynamic-programming-and-markov-processes/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012. http://www.athenasc.com/dpbook.html

9 thms3 active usersReviewed

Completed

Analysis Functional Analysis Machine Learning·Captain: mikedeng1

Theory of Reproducing Kernels III: The Product of Two Reproducing Kernels Is the Kernel of the Diagonal Restrictions of the Direct ProductResearch Paper

Motivation

A reproducing kernel is the function $K(x,y)$ that represents point evaluation in a Hilbert space of functions: $f(y) = (f, K(\cdot, y))$ . Kernels are combined all the time. In machine learning, a kernel on pairs of objects is routinely built as the pointwise product of two simpler kernels, and in complex analysis the product $|K(x,y)|^2 = K(x,y)K(y,x)$ of a kernel with its conjugate appears naturally. That the pointwise product of two positive matrices is again a positive matrix goes back to I. Schur (1911). What Schur's theorem does not say is which space of functions the product kernel belongs to and what its norm is.

N. Aronszajn answered this in §8 of Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, doi:10.1090/S0002-9947-1950-0051437-7), the paper that fixed the general theory of reproducing kernel Hilbert spaces. He notes (p. 358, footnote 7) that the idea of the proof was found independently by R. Godement, who applied it only to positive definite functions. The answer has three ingredients developed in the same paper: the functional completion of an incomplete class of functions (§4), the restriction of a kernel to a subset (§5), and the direct product $F_1 \otimes F_2$ of two classes of functions (§8).

Setting

Let $E$ be an arbitrary set. A class with a reproducing kernel is a complex Hilbert space $F$ of functions $f : E \to \mathbb{C}$ such that every point evaluation $f \mapsto f(y)$ is continuous. Its reproducing kernel $K : E \times E \to \mathbb{C}$ is characterized by: $K(\cdot, y) \in F$ for each $y$ , and $f(y) = (f, K(\cdot, y))$ for all $f \in F$ , where the scalar product $(f, g)$ is linear in $f$ and conjugate-linear in $g$ .

Functional completion. Suppose $F$ is a linear class of functions on $E$ with a scalar product satisfying every Hilbert-space axiom except completeness. A functional completion of $F$ is a Hilbert space of functions on $E$ , with continuous point evaluations, that contains $F$ isometrically as a dense subset.

Restriction. For $E_1 \subseteq E$ , the restriction of $f$ is $f|_{E_1}$ , and $F|_{E_1}$ is the class of all restrictions.

Direct product. Given classes $F_1$ , $F_2$ on $E$ with kernels $K_1$ , $K_2$ and norms $\|\cdot\|_1$ , $\|\cdot\|_2$ , consider on $E' = E \times E$ the functions

f'(x_1,x_2) = \sum_{k=1}^n f_1^{(k)}(x_1) f_2^{(k)}(x_2), \qquad f_1^{(k)} \in F_1,\ f_2^{(k)} \in F_2,

with scalar product $(f', g')' = \sum_{k,l} (f_1^{(k)}, g_1^{(l)})_1 (f_2^{(k)}, g_2^{(l)})_2$ . Their functional completion is the direct product $F' = F_1 \otimes F_2$ , with norm $\|\cdot\|'$ .

In Lean, kernelFn H x y is the scalar kernel $K(x,y)$ of a space H, IsFunctionalCompletion ι H says H is a functional completion of the class presented by ι, and IsDirectProduct H₁ H₂ H' says H' is $F_1 \otimes F_2$ .

Formalization targets

Goal: §8, Theorem II

The kernel $K(x,y) = K_1(x,y) K_2(x,y)$ is the reproducing kernel of the class $F$ of restrictions of the functions of $F_1 \otimes F_2$ to the diagonal $\{(x,x)\}$ , and

\|f\| = \min\{\|g'\|' : g' \in F_1 \otimes F_2,\ g'(x,x) = f(x)\ \forall x \in E\}.

Milestones

§4, Theorem. A functional completion of $F$ exists if and only if every evaluation $f \mapsto f(y)$ is bounded on $F$ and every Cauchy sequence $(f_m) \subset F$ with $f_m(y) \to 0$ for every $y$ satisfies $\|f_m\| \to 0$ ; the functional completion, when it exists, is unique.
§8, Theorem I. $F_1 \otimes F_2$ has reproducing kernel

K'(x_1,x_2,y_1,y_2) = K_1(x_1,y_1)\,K_2(x_2,y_2).

§5, Theorem. $K|_{E_1 \times E_1}$ is the reproducing kernel of $F|_{E_1}$ , with $\|f_1\|_1 = \min\{\|f\| : f|_{E_1} = f_1\}$ .
§8, Remark. For a complete orthonormal system $\{g_1^{(k)}\}$ of $F_1$ , every $f$ in the class of $K_1K_2$ is $f = \sum_k f_2^{(k)} g_1^{(k)}$ with $f_2^{(k)} \in F_2$ , $\sum_k \|f_2^{(k)}\|_2^2 < \infty$ ; exactly one such representation minimizes $\sum_k \|f_2^{(k)}\|_2^2$ , and the minimum is $\|f\|^2$ .

Significance

The result. Theorem II turns the Schur product theorem from a statement about matrices into a statement about function spaces: it says which functions the product kernel can represent and how their norms are computed, through a minimal decomposition. It is the standard description of the reproducing kernel Hilbert space of a product kernel, used to reason about which functions product kernels can express and with what norm, and the Remark gives a concrete series description of the same space. §5 (restriction) and §4 (functional completion) are general tools in their own right: restriction underlies every comparison of kernels on nested domains, and §4 is the criterion for when an incomplete space of functions can be completed without leaving the world of functions.

Formalizing it. All four results are classical and proved on paper. Mathlib has reproducing kernel Hilbert spaces (RKHS, RKHS.kernel, the construction RKHS.OfKernel from a positive semidefinite kernel) and Schur's product theorem (Matrix.PosSemidef.hadamard, for an arbitrary index type), but no restriction theorem, no functional completion and no tensor product of reproducing kernel Hilbert spaces. None of these statements has a machine-checked proof that the mission is aware of.

Difficulty

The kernel identity is the easy part: by Schur's theorem $K_1K_2$ is positive, so some space with kernel $K_1K_2$ exists. The content is the identification of that space and its norm. The direct product has to be constructed before anything can be said about it: the class of finite sums of products is not complete, the scalar product (2) must be shown independent of the representation and positive definite, and the completion must stay a class of functions, which is exactly the question §4 answers and which can fail (p. 349 gives a class satisfying the first condition but not the second). The norm formula is an attained minimum over an infinite-dimensional affine set of preimages, not merely an infimum.

Formalization scope

Scalars are complex throughout ("From now on … we shall consider only complex Hilbert spaces", p. 343). The underlying set $E$ is an arbitrary type X, with no topology, measure or nonemptiness assumption. A class with a reproducing kernel is a complex Hilbert space H with Mathlib's RKHS ℂ H X ℂ structure; its functions are the coercions ⇑f. The scalar kernel is kernelFn H x y = RKHS.kernel H x y 1. Mathlib's inner product $\langle u, v\rangle$ is conjugate-linear in $u$ , so Aronszajn's $(f,g)$ is $\langle g, f\rangle$ .

Conventions and reading decisions:

Statements of the form " $K$ is the reproducing kernel of the class $\mathcal{C}$ with norm $N$ " assert that a space with kernel $K$ exists and that every space with kernel $K$ has exactly the functions $\mathcal{C}$ and the norm $N$ . They never define the space as RKHS.OfKernel K, which would make the kernel identity true by construction.
The direct product is characterized by its elementary products $f_1(x_1)f_2(x_2)$ , the scalar product (2) on them, and density of their span (IsDirectProduct); it is never defined through its kernel. With that, Theorem I is not a definitional identity and Theorem II is not a restatement of §5.
"min" is an attained minimum (IsLeast). In Theorem II and §5 it is the minimum of the norm, not its square; in the Remark it is the minimum of the sum of squared norms, as printed.
The diagonal of $E\times E$ is identified with $E$ through $x \mapsto (x,x)$ , and the restriction of $g'$ is $x \mapsto g'(x,x)$ .
§4's "incomplete" Hilbert space is a complex inner product space, not assumed complete; completeness is not excluded either.
The complete orthonormal system of the Remark is a Mathlib HilbertBasis over an arbitrary index set, and the series converges unconditionally at each point.

Results already in Mathlib are not restated: Schur's product theorem (Matrix.PosSemidef.hadamard, the first sentence of §8 and the sentence after Theorem I), positivity of a kernel (RKHS.posSemidef_kernel) and existence of a space for a positive kernel (RKHS.OfKernel, RKHS.kernel_ofKernel).

A complete development needs a Hilbert tensor product of reproducing kernel Hilbert spaces realized as functions on $E\times E$ , the restriction construction (quotient by the subspace of functions vanishing on $E_1$ ), and uniqueness of a reproducing kernel Hilbert space with given kernel. The restriction theorem and the functional completion theorem are reusable well beyond this mission; contributions of either, or of a Hilbert tensor product for RKHS, are welcome.

Selected references

N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
I. Schur, Bemerkungen zur Theorie der beschränkten Bilinearformen mit unendlich vielen Veränderlichen, J. Reine Angew. Math. 140 (1911), 1–28. https://doi.org/10.1515/crll.1911.140.1
J. von Neumann and F. J. Murray, On rings of operators, Ann. of Math. 37 (1936), 116–229 (direct products of Hilbert spaces). https://doi.org/10.2307/1968693
V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge Univ. Press, 2016. https://doi.org/10.1017/CBO9781316219232

8 thms3 active usersReviewed

Completed

Analysis Functional Analysis Machine Learning·Captain: mikedeng1

Theory of Reproducing Kernels I: The Sum of Two Reproducing Kernels Is the Kernel of the Sum Class with the Minimal-Decomposition NormResearch Paper

Motivation

Reproducing kernel Hilbert spaces are Hilbert spaces of functions in which evaluation at a point is a continuous linear functional. They appear wherever a space of functions carries a natural quadratic norm: Bergman and Hardy spaces of analytic functions, spaces of harmonic functions and solutions of elliptic equations, Sobolev spaces in one dimension, and, since the 1990s, the hypothesis classes of kernel methods in machine learning (support vector machines, Gaussian process regression, kernel ridge regression). In all of these settings, kernels are routinely combined: a sum of kernels is used to model a function as a sum of components, and the question is which space of functions, and which norm, the combined kernel describes.

N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) organised the subject as a calculus of operations on kernels. Its §6 answers the question for sums.

Timeline. E. H. Moore (Bull. Amer. Math. Soc. 1916; General Analysis, 1935) introduced positive Hermitian matrices on arbitrary sets and their associated function classes. S. Bergman (1920s–1930s) studied the kernel of square-integrable analytic functions of a domain. R. Godement (C. R. Acad. Sci. Paris notes, 1945–1946) found the sum theorem for positive definite functions on a group (footnote 6 of the paper). Aronszajn (1950) proved it for arbitrary kernels on arbitrary sets, with the description of the norm as a minimum over decompositions.

Setting

Let $E$ be an arbitrary set. A class of functions $F$ on $E$ is a complex vector space of functions $f:E\to\mathbb C$ carrying a norm $\|\cdot\|$ that makes it a complex Hilbert space. A function $K:E\times E\to\mathbb C$ is the reproducing kernel (r.k.) of $F$ if, for every $y\in E$ , the function $K(\cdot,y)$ belongs to $F$ and

f(y)=(f,K(\cdot,y))\qquad\text{for every } f\in F,

where $(f,g)$ is the scalar product, linear in $f$ . A kernel exists exactly when every evaluation $f\mapsto f(y)$ is continuous.

A function $K:E\times E\to\mathbb C$ is a positive matrix if $\sum_{i,j=1}^n K(y_i,y_j)\bar\xi_i\xi_j\ge 0$ for all finite families of points $y_i\in E$ and complex numbers $\xi_i$ . Every reproducing kernel is a positive matrix.

A class $F_1$ is a subclass of $F_2$ if every function of $F_1$ belongs to $F_2$ , and a subspace if moreover the two norms agree on $F_1$ . Two classes $F_1$ , $F_2$ with kernels $K_1$ , $K_2$ have a sum class $F_1+F_2=\{f_1+f_2: f_i\in F_i\}$ , a set of functions; a function of it may have many decompositions $f=f_1+f_2$ , since $F_1$ and $F_2$ may share functions.

Formalization targets

Goal: the sum theorem (§6, Theorem, p. 353)

For complex Hilbert spaces $F_1$ , $F_2$ of functions on $E$ with kernels $K_1$ , $K_2$ : the kernel $K=K_1+K_2$ is the reproducing kernel of the class of all $f=f_1+f_2$ , with

\|f\|^2=\min\big[\|f_1\|_1^2+\|f_2\|_2^2\big],

the minimum taken over all decompositions $f=f_1+f_2$ , $f_i\in F_i$ . The goal asserts that a space with kernel $K_1+K_2$ exists, and that every such space consists exactly of the sums and has exactly this norm, the minimum being attained.

Milestones

§2 (4), Moore's theorem (p. 344): a positive matrix is the kernel of one and only one class of functions with a uniquely determined norm. This makes "the class with kernel $K_1+K_2$ " well defined.
§2 (7) (p. 345): every closed subspace $F'$ of $F$ has a kernel $K'$ , and for the orthogonal complement $F''$ , $K'+K''=K$ .
§3, Theorem (p. 347): $K$ is the kernel of a finite-dimensional class if and only if $K(x,y)=\sum_{i,j}\beta_{ij}w_i(x)\overline{w_j(y)}$ with $\{\beta_{ij}\}$ positive definite and the $w_k$ linearly independent; the class is then spanned by the $w_k$ , with norm given by the inverse of $\{\bar\beta_{ij}\}$ .
§6, p. 354, the disjoint case: when $F_1\cap F_2=\{0\}$ , $\|f\|^2=\|f_1\|_1^2+\|f_2\|_2^2$ , and this happens if and only if $F_1$ and $F_2$ are complementary closed subspaces of $F$ .
§6, p. 354, Eq. (1): the class of conjugates $\bar F$ has kernel $K(y,x)$ , and $\operatorname{Re}K=2^{-1}(K(x,y)+K(y,x))$ is the kernel of the class of all $f+\bar g$ , with $\|\varphi\|_0^2=2\min[\|f\|^2+\|g\|^2]$ .

Significance

The result itself. The sum theorem is the first operation of Aronszajn's calculus and the base of the next ones: the order $K_1\ll K$ between kernels and the inclusion theorem of §7 are derived from it, as are the kernel $\operatorname{Re}K$ of the class of all $f+\bar g$ and the characterisation of kernels of real spaces (§6, p. 354). In machine learning, it is the statement behind additive kernels and multiple-kernel learning: the hypothesis class of $K_1+K_2$ is the set of sums, and the regulariser is the infimal convolution of the two squared norms. In complex analysis, it describes the space attached to a sum of Bergman-type kernels.

Formalizing it. The results are classical and proved in the paper; none of them is formalized in Mathlib beyond the existence half of Moore's theorem. Mathlib (2026) has reproducing kernel Hilbert spaces with operator-valued kernels (RKHS, RKHS.kernel, RKHS.kerFun, RKHS.posSemidef_kernel) and the construction of a space from a positive semidefinite matrix (RKHS.OfKernel, RKHS.kernel_ofKernel). This mission adds uniqueness, the sum theorem, kernels of closed subspaces, the finite-dimensional case and the conjugate class.

Difficulty

The kernel $K_1+K_2$ is the kernel of some space by Moore's existence theorem, so the content is the identification of that space. The obvious candidate, the external direct sum $F_1\oplus F_2$ mapped to functions by $(f_1,f_2)\mapsto f_1+f_2$ , is not injective as soon as $F_1$ and $F_2$ share a nonzero function; the class of sums is the image of a quotient, and its norm is the norm of a minimal representative, which has to be shown to exist and to make the class complete. Proving that the resulting space has kernel $K_1+K_2$ and that every other space with this kernel coincides with it requires the uniqueness half of Moore's theorem, which is not in Mathlib. The disjoint case needs, in addition, that an isometric image of a complete space is closed, and the converse direction of its "only in this case".

Formalization scope

Scalars and sets. Complex scalars throughout (the paper's convention from §1 on). $E$ is an arbitrary type X with no topology, measure, or nonemptiness assumption.
Spaces. A class with a kernel is a Mathlib RKHS ℂ H X ℂ on a complex Hilbert space H; its functions are Set.range (⇑ : H → X → ℂ).
Kernel. The scalar kernel kernelFn H x y is RKHS.kernel H x y 1.
Scalar products. The paper's $(f,g)$ , linear in $f$ , is Mathlib's ⟪g, f⟫_ℂ.
Positivity. A positive matrix is (Matrix.of K).PosSemidef, and "positive definite" is Matrix.PosDef.
Decompositions are of functions: $f=f_1+f_2$ pointwise with $f_i$ in $F_i$ .
Minima. "min" is an attained minimum (IsLeast), never an infimum.
Quantification. Statements about "the" class with a given kernel quantify over every RKHS with that kernel, in any universe, and assert separately that one exists.

Reading decisions, recorded in the item notes:

In §2 (7), "complementary subspaces" means a closed subspace and its orthogonal complement, and the kernels of the two subspaces are any kernels with the reproducing property there, not projections of $K$ .
In §3, $\{\bar\beta_{ij}\}$ is the entrywise conjugate of $\{\beta_{ij}\}$ (consistent with §3 (5), $\sum_j\alpha_{ij}\bar\beta_{jk}=\delta_{ik}$ ), not its conjugate transpose.
In §6, p. 354, "subspace" is the paper's §1 notion (norms agree), and the scalar-product remark on $\bar F$ follows from the norm statement by polarization.

Trivialization ruled out. The goal does not define the sum class as RKHS.OfKernel (K₁ + K₂) and assert that its kernel is $K_1+K_2$ , which is Mathlib's kernel_ofKernel. Its content is the description of the functions (exactly the sums) and of the norm (the attained minimum) for every space with that kernel.

Infrastructure. A complete development needs:

uniqueness of an RKHS given its kernel (milestone 1);
orthogonal projections onto closed subspaces (Mathlib Submodule.starProjection);
quotients of Hilbert spaces by closed subspaces, or the orthogonal complement of the kernel of the sum map;
for §3, Gram matrices and their inverses.

Milestone 1 and the RKHS structure on a closed subspace are reusable beyond this mission and are natural Mathlib contributions. Independent proofs of any milestone are welcome.

Selected references

N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
E. H. Moore, General Analysis, Part I, Memoirs of the American Philosophical Society 1, 1935.
R. Godement, Sur les fonctions de type positif, C. R. Acad. Sci. Paris 221 (1945), 69; and further notes in vols. 221–222 (1945–1946), as cited by Aronszajn [Godement 1].
E. H. Moore, On properly positive Hermitian matrices, Bull. Amer. Math. Soc. 23 (1916), 59.
V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge Univ. Press, 2016. https://doi.org/10.1017/CBO9781316219232

8 thms3 active usersReviewed

Completed

Dynamic Programming Machine Learning Markov Chain+1·Captain: mikedeng1

Reinforcement Learning: An Introduction II: The Bellman Optimality Equation and the Existence of an Optimal PolicyTextbook

Motivation

Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) is the standard introductory text of the field. Its Chapter 3 sets up the model that the rest of Part I works in: the finite Markov decision process (MDP), the value functions of a policy, and the Bellman equations that relate the value of a state to the values of its successors. Section 3.6 then states the fact every planning and control method of the book relies on: in a finite MDP there is an optimal policy, its value is the unique solution of a system of nonlinear equations, and a policy that acts greedily with respect to that solution is optimal. Dynamic programming (Chapter 4), Monte Carlo control (Chapter 5), Sarsa and Q-learning (Chapter 6) are all methods for solving the Bellman optimality equation; their correctness statements presuppose that it has exactly one solution and that it identifies optimal behaviour.

The book is deliberately informal ("we chose not to produce a rigorous formal treatment", p. xiii): §3.6 asserts these facts without proof. The results themselves are classical, going back to Bellman (1957), Howard (1960) and Blackwell (1965); a textbook proof for discounted finite MDPs is in Puterman, Markov Decision Processes (Wiley, 1994), Chapter 6.

Setting

A finite MDP has a finite set of states $\mathcal S$ , a finite nonempty set of actions $\mathcal A$ , a finite set of rewards $\mathcal R \subset \mathbb R$ , and dynamics

p(s', r \mid s, a) = \Pr\{S_t = s', R_t = r \mid S_{t-1} = s, A_{t-1} = a\}, \qquad \sum_{s' \in \mathcal S}\sum_{r \in \mathcal R} p(s', r \mid s, a) = 1,

Eqs. (3.2)–(3.3). From $p$ one derives $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ and $r(s, a) = \sum_r r \sum_{s'} p(s', r \mid s, a)$ , Eqs. (3.4)–(3.5).

A policy $\pi$ gives a probability $\pi(a \mid s)$ of each action in each state. Fix a discount rate $0 \le \gamma < 1$ . The return of a reward sequence is $G_t = \sum_{k \ge 0} \gamma^k R_{t+k+1}$ (3.8). The state-value function and action-value function of $\pi$ are the expected returns

v_\pi(s) = \mathbb E_\pi[G_t \mid S_t = s], \qquad q_\pi(s, a) = \mathbb E_\pi[G_t \mid S_t = s, A_t = a] \qquad (3.12)\text{–}(3.13).

In the Lean development these are stateValue M γ π s and actionValue M γ π s a, computed as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ from the transition matrix $P_\pi(s, s') = \sum_a \pi(a \mid s)\,p(s' \mid s, a)$ and the expected reward $r_\pi(s) = \sum_a \pi(a \mid s)\,r(s, a)$ of the Markov chain the policy induces. A policy $\pi$ is optimal (IsOptimalPolicy) if $v_\pi(s) \ge v_{\pi'}(s)$ for every policy $\pi'$ and every state $s$ . The optimal value functions are

v_*(s) = \max_\pi v_\pi(s) \quad (3.15), \qquad q_*(s, a) = \max_\pi q_\pi(s, a) \quad (3.16),

optimalValue and optimalActionValue, with the maximum over all stochastic policies.

Formalization targets

Goal: the Bellman optimality equation and optimal policies (§3.6, pp. 62–64)

For every finite MDP and $0 \le \gamma < 1$ :

the maximum in (3.15) is attained at every state;
an optimal policy exists;
$v_*$ satisfies the Bellman optimality equation

v_*(s) = \max_{a} \sum_{s', r} p(s', r \mid s, a)\big[r + \gamma v_*(s')\big] \quad \text{for all } s; \qquad (3.19)

$v_*$ is the only function on $\mathcal S$ satisfying (3.19);
every policy that assigns positive probability only to actions attaining the maximum in (3.19) is optimal.

Milestones

(3.9) $G_t = R_{t+1} + \gamma G_{t+1}$ for bounded rewards, with the series convergent.
(3.14) the Bellman equation $v_\pi(s) = \sum_a \pi(a \mid s) \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_\pi(s')]$ , and (p. 60) its uniqueness: $v_\pi$ is its only solution.
Exercise 3.15 adding a constant $c$ to all rewards adds $v_c = c/(1-\gamma)$ to every value.
Exercises 3.18 and 3.19 $v_\pi(s) = \sum_a \pi(a \mid s)\,q_\pi(s, a)$ and $q_\pi(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_\pi(s')]$ .
(3.16)–(3.17) the maximum defining $q_*$ is attained and $q_*(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_*(s')]$ .
(3.20) the Bellman optimality equation for action values, $q_*(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma \max_{a'} q_*(s', a')]$ .

Significance

The goal is what turns "find a good policy" into "solve a system of equations". Parts 3 and 4 identify $v_*$ with the unique solution of (3.19), so any procedure that finds a solution of (3.19) has found $v_*$ ; part 5 converts $v_*$ into an optimal policy by a one-step search. Parts 1 and 2 say that the book's definition (3.15) makes sense: a single policy is simultaneously best at every state, so "the optimal value function" is well defined and shared by all optimal policies. Chapter 4's policy iteration and value iteration, and the fixed points of Q-learning, are statements about this equation. Exercises 3.18 and 3.19 are used, by number, in the proof of the policy gradient theorem (p. 325).

The mathematics is classical and proved in many texts; what is missing is a machine-checked version in the book's own model. Platform relatives exist in different models: FoundationsML.ReinforcementLearning.bellman_equations_unique_solution (uniqueness for a fixed policy, with an expected-reward kernel instead of $p(s', r \mid s, a)$ ), BertsekasDP.discounted_main_theorem (cost minimization over deterministic stationary policies), BanditAlgorithm.mdp_discounted_bellman_solution (existence of a solution with a greedy deterministic policy, rewards in $[0,1]$ ) and FoundationsRL.RLBasics.bellman_optimality (finite horizon). None of them states the book's result: the four-argument dynamics, stochastic policies, the maximum over all of them, uniqueness of the solution of (3.19), and optimality of every policy supported on greedy actions. This mission produces that statement and, with it, a vocabulary of finite-MDP definitions that the later missions of the series reuse.

Difficulty

The book's derivation of (3.19) (p. 63) starts from $v_*(s) = \max_a q_{\pi_*}(s, a)$ with a policy $\pi_*$ that is optimal at every state at once. The existence of such a policy is the substance of the goal, and it does not follow from the definition: (3.15) takes a separate maximum at each state, and a priori the maximizing policy could depend on the state. Uniqueness for (3.19) is likewise not a consequence of linear algebra, as it is for (3.14): the equation is nonlinear because of the maximum. The fixed point must be related to the value of an actual policy, and every policy's value must be bounded above by it.

Formalization scope

Model. S and A are finite types with A nonempty (without an action, $\max_a$ is undefined). One action set serves every state, as the book's footnote 3 (p. 48) allows. Rewards form a finite set M.R : Finset ℝ and the dynamics are the four-argument M.p s a s' r with the normalization (3.3).
Discounting. All statements assume $0 \le \gamma < 1$ (the continuing discounted case of §3.3). The episodic case with $\gamma = 1$ is not covered: the book's uniqueness claims then need every episode to terminate under every policy, which the chapter never states, and without it (3.19) can have many solutions (a state that loops to itself with reward $0$ satisfies $v(s) = v(s)$ for any value).
Value functions from returns. $v_\pi$ and $q_\pi$ are expected discounted returns, computed from the Markov chain the policy induces. They are not defined as solutions of the Bellman equations, and $v_*$ is not defined as a solution of (3.19): either would make the goal true by definition. The Bellman equations are theorems.
Maxima. $v_*$ and $q_*$ are real suprema over the type of stochastic policies (Lean gives a supremum that does not exist the value $0$ ); the goal and milestone (3.17) assert that these suprema are attained, so they are the book's maxima.
Conditional expectations. (3.17), (3.18) and (3.20) are stated in their finite-sum form over $(s', r)$ .
Exercises. Exercises 3.15, 3.18 and 3.19 have no printed solutions; the statements give the formalization's answers ( $v_c = c/(1-\gamma)$ and the two displayed identities).
Reusable infrastructure. The definitions (MDP, Policy, trans, expReward, policyTrans, policyReward, stateValue, actionValue, optimalValue, optimalActionValue, IsOptimalPolicy) follow the conventions shared by the whole series and are meant to be merged with the finite-MDP layers of the later chapters. Lemmas on summability of the value series, the Bellman operator as a $\gamma$ -contraction in the sup norm, and the Markov-chain identities for $P_\pi^k$ are welcome as separate contributions.

Selected references

R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 3. http://incompleteideas.net/book/the-book-2nd.html
R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://doi.org/10.2307/j.ctv1nxcw0f
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
D. Blackwell, "Discounted dynamic programming", Annals of Mathematical Statistics 36(1), 1965, 226–235. https://doi.org/10.1214/aoms/1177700285
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources IV: Every Feasible Schedule Obeys a Minimal Delaying Mode of Each Forbidden SetTextbook

Motivation

Resource-constrained project scheduling with general temporal constraints, written $PS|temp|C_{\max}$ , asks for start times of the activities of a project that respect minimum and maximum time lags between activities and the capacities of renewable resources (staff, machines, reactors), and that minimize the project duration. Deciding whether a feasible schedule exists at all is already NP-complete (Bartusch, Möhring and Radermacher, 1988), so exact methods are branch-and-bound procedures. The dominant family, going back to De Reyck and Herroelen (1998) and presented in Chapter 2 of Neumann, Schwindt and Zimmermann's monograph, branches on resource conflicts: whenever the currently computed schedule overloads a resource at some time $t$ , the set of activities in progress at $t$ is a forbidden set, and the node is split into children, each of which adds precedence constraints that resolve the conflict.

Such a scheme is only correct if the children together retain every feasible schedule. Theorem 2.5.7 of the book is exactly this completeness guarantee, and it is the reason the enumeration can be restricted to the small family of minimal delaying modes instead of arbitrary ways of breaking up a conflict. The same section also contains the preprocessing results (§2.5.2) that exploit two-element forbidden sets before any branching happens. This mission formalizes both.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$ ; activity $0$ is the project beginning and $n+1$ the project completion, both of duration $0$ , and every real activity $i\in\{1,\dots,n\}$ has an integer duration $p_i>0$ . The project network $N$ has arc set $E$ and integer arc weights $\delta_{ij}$ ; the arc $\langle i,j\rangle$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ . A finite set $\mathcal R$ of renewable resources is given; resource $k$ has capacity $R_k\in\mathbb N$ and activity $i$ uses $r_{ik}\in\mathbb Z_{\ge0}$ units of it, with $r_{ik}\le R_k$ and $r_{0k}=r_{n+1,k}=0$ .

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge0$ . The active set at time $t$ is $\mathcal A(S,t)=\{i\in V\mid S_i\le t<S_i+p_i\}$ . The schedule is time-feasible if it satisfies all temporal constraints, resource-feasible if

\sum_{i\in\mathcal A(S,t)}r_{ik}\le R_k\qquad(k\in\mathcal R,\ t\ge0),

and feasible if it is both; $\mathcal S$ denotes the set of feasible schedules.

A set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$ , a feasible set otherwise, and minimal forbidden if no proper subset is forbidden. For a forbidden $F$ , a set $B\subseteq F$ is a delaying alternative if $F\setminus B$ is feasible, and a minimal delaying alternative if no proper subset of $B$ is one. A minimal delaying mode for $F$ is a pair $(i,B)$ with $B$ a minimal delaying alternative for $F$ and $i\in F\setminus B$ .

For §2.5.2, fix an integer upper bound $UB$ on the project duration. The temporal scheduling network $N^+$ adds to $N$ the arc $\langle n+1,0\rangle$ with weight $\delta_{n+1,0}=-UB$ , and $d_{ij}$ is the longest path length from $i$ to $j$ in $N^+$ ( $-\infty$ if there is no path, $d_{ii}=0$ ).

Formalization targets

Goal: Theorem 2.5.7 (p. 49)

For every forbidden set $F$ and every feasible schedule $S\in\mathcal S$ there is a minimal delaying mode $(i,B)$ for $F$ with

S_j\ge S_i+p_i\qquad(j\in B).

$F$ is arbitrary (not necessarily minimal); $B$ must be a minimal delaying alternative and $i$ must lie outside $B$ .

Milestones

Eqs. (2.5.2)–(2.5.3), p. 46. $B$ is a minimal delaying alternative for a forbidden $F$ iff $F\setminus B$ is a maximal feasible subset of $F$ , iff $B\subseteq F$ ,

\sum_{i\in F\setminus B}r_{ik}\le R_k\ (k\in\mathcal R)\quad\text{and}\quad\forall j\in B\ \exists k:\ \sum_{i\in F\setminus B}r_{ik}+r_{jk}>R_k.

Bartusch et al.'s criterion (proof of Theorem 2.3.10, p. 35). A schedule is resource-feasible iff every minimal forbidden set $F$ contains distinct $i,j$ with $S_j\ge S_i+p_i$ .
Lemma 2.5.5, p. 49. A minimal delaying alternative for $F$ is an inclusion-minimal set meeting every minimal forbidden $F'\subseteq F$ .
Theorem 2.5.11, p. 55. If $\{i,j\}$ is a two-element forbidden set with $d_{ij}<p_i$ and $d_{ij}>-p_j$ , then every feasible $S$ with $S_{n+1}\le UB$ satisfies $S_j\ge S_i+p_i$ .
Eq. (2.5.7), p. 55. If for a two-element forbidden set $\{i,j\}$ neither $d_{ij}>-p_j$ nor $d_{ji}>-p_i$ holds, then for all $h,l\in V$ and every feasible $S$ with $S_{n+1}\le UB$ ,

S_l\ge S_h+\min\bigl(d_{hi}+p_i+d_{jl},\ d_{hj}+p_j+d_{il}\bigr).

Significance

The result. Theorem 2.5.7 is the completeness statement of the De Reyck–Herroelen enumeration scheme (Algorithm 2.5.8): if every child of a conflict node imposes the precedence constraints $i\to j$ ( $j\in B$ ) of one minimal delaying mode $(i,B)$ , the children's order polyhedra together contain all feasible schedules of the parent. Proposition 2.5.9(a), the correctness of the whole branch-and-bound procedure, rests on it. Because the objective does not enter, the book reuses the theorem for the regular and nonregular objectives of Chapter 3. Theorem 2.5.11 and inequality (2.5.7) are the preprocessing rules that shrink the time-feasible region before enumeration: each adds temporal constraints that every feasible schedule within the bound already satisfies, which raises the lower bound $ES_{n+1}$ and prunes the enumeration.

Formalizing it. All statements are proved in the book (Bartusch et al.'s criterion is quoted from their 1988 paper with the necessity argument sketched). None of them has a machine-checked proof; the Prove2Me catalog contains precedence-only scheduling models (Brucker–Knust) and acyclic event networks (Kelley–Walker) but no model with time windows and forbidden sets. The mission produces a reusable library of forbidden sets, delaying alternatives and longest-path distances in networks with maximum time lags.

Difficulty

The obvious idea — pick any two overlapping activities and delay one — does not give a minimal delaying alternative with a single delaying activity $i$ common to all of $B$ . The proof has to pass from the pairwise separations that resource-feasibility guarantees in each minimal forbidden subset to a set $B$ that is simultaneously minimal as a delaying alternative and ordered behind one activity outside $B$ . This needs the correspondence between delaying alternatives and hitting sets of the minimal forbidden subsets (Lemma 2.5.5) and the positivity of real durations to keep $i$ outside $B$ . For the preprocessing results, the delicate part is relating longest paths in $N^+$ , including the backward arc carrying $-UB$ , to the start-time differences of every feasible schedule within the bound.

Formalization scope

Activities are Fin (n + 2), with $n+1$ as Fin.last (n + 1). Start times are real; durations, capacities, requirements and time lags are integers (natural numbers where the book says so). The standing assumptions of the book (at least one real activity, zero-duration dummies, positive durations of real activities, no loops, $r_{0k}=r_{n+1,k}=0$ , $r_{ik}\le R_k$ , and paths in $N$ from $0$ to every node and from every node to $n+1$ ) are one hypothesis P.StandingAssumptions of every theorem.

Resource constraints are imposed for every $t\ge0$ , not only for $0\le t\le\bar d$ as (2.1.4) literally writes. The book's proofs and Remark 2.3.11 use the $t\ge0$ reading; with the literal cut-off, schedules running past $\bar d$ could violate capacities after $\bar d$ , and Bartusch et al.'s criterion would fail.

Longest path lengths are maxima over simple paths, with values in WithBot ℝ (⊥ for $-\infty$ ). If $N^+$ has a cycle of positive length, no schedule satisfies the temporal constraints with $S_{n+1}\le UB$ , and the statements using $d_{ij}$ are vacuous, as in the book. The arc $\langle n+1,0\rangle$ of $N^+$ has weight $-UB$ , or $\max(\delta_{n+1,0},-UB)$ if $N$ already has such an arc. $UB$ is an integer.

The goal is not trivial: it quantifies over minimal delaying modes only. A variant without the minimality of $B$ , or allowing $i\in B$ , would be nearly empty (take $B=F\setminus\{i\}$ ), and the statement here rules both out. Maximality in milestone 1 is taken among subsets of $F$ .

Welcome contributions: the hitting-set correspondence between delaying alternatives and minimal forbidden subsets, the telescoping bound $S_j-S_i\ge d_{ij}$ for feasible schedules, and proofs of any milestone. The definitions restate the setup of the series' earlier missions (II: order polyhedra) locally, because those are still drafts.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.5. https://doi.org/10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988) 201–240. https://doi.org/10.1007/BF02283745
B. De Reyck, W. Herroelen, A branch-and-bound procedure for the resource-constrained project scheduling problem with generalized precedence relations, European Journal of Operational Research 111 (1998) 152–174. https://doi.org/10.1016/S0377-2217(97)00305-6

8 thms3 active usersReviewed

Completed

Operations Research Probability Statistics+1·Captain: mikedeng1

Fundamentals of Queueing Theory VIII: Lindley's Integral Equation for the G/G/1 QueueTextbook

Why the G/G/1 queue

The single-server queue with general interarrival times and general service times, written G/G/1 in Kendall's notation, is the model left when every distributional assumption is removed from the classical single-server queue. Customers arrive one at a time, wait in line in first-come, first-served order, and are served one at a time. Almost nothing about it can be computed in closed form. What survives is a recursion for the waiting times of successive customers and the integral equation of its steady state, due to Lindley (Lindley, 1952). Every exact and approximate treatment of the G/G/1 waiting time, including the bounds of the next chapter of the book, starts from that equation.

This mission is the eighth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651). It covers Chapter 6, "General Models and Theoretical Topics". The chapter also treats the G/E_k/1 characteristic equation (§6.1), the M/D/c queue (§6.3) and maximum-likelihood estimation for M/M/1 (§6.7), which appear here as further milestones.

Timeline. Lindley (1952) derived the recursion and the integral equation and showed that a limiting waiting-time distribution exists when the mean service time is smaller than the mean interarrival time. Loynes (1962) gave the stationary solution as a supremum over the past of a random walk, for stationary rather than independent inputs. Clarke (1957) derived the maximum-likelihood estimators for M/M/1, and Crommelin (1932) the M/D/c generating function. Chaudhry, Harris and Marchal (1990) located the roots of the G/E_k/1 characteristic equation.

Setting

The interarrival times $T^{(n)}$ are independent with common distribution $A$ , the service times $S^{(n)}$ are independent with common distribution $B$ , and the two sequences are independent. Both $A$ and $B$ are lifetime laws: probability distributions on $[0,\infty)$ . The means are $\mathrm E[T]=1/\lambda$ and $\mathrm E[S]=1/\mu$ , and the traffic intensity is $\rho=\lambda/\mu=\mathrm E[S]/\mathrm E[T]$ .

The line delay $W_q^{(n)}$ of the $n$ th customer satisfies Lindley's recursion

W_q^{(n+1)}=\max\bigl(0,\;W_q^{(n)}+S^{(n)}-T^{(n)}\bigr).

Write $U$ for the distribution of $S-T$ with $S\sim B$ and $T\sim A$ independent. Since $W_q^{(n)}$ is independent of $(S^{(n)},T^{(n)})$ , one step of the recursion sends the distribution $\nu$ of $W_q^{(n)}$ to the distribution of $\max(0,W+U)$ with $W\sim\nu$ independent of $U$ . A stationary delay distribution is a probability distribution $\nu$ that this step maps to itself; its CDF is $W_q(t)=\nu((-\infty,t])$ .

Formalization targets

Goal: Lindley's equation (6.8)

If $\mathrm E[T]$ and $\mathrm E[S]$ are finite and $\rho<1$ , then a stationary delay distribution exists, and the CDF of every stationary delay distribution satisfies

W_q(t)=\begin{cases}\displaystyle\int_{-\infty}^{t}W_q(t-x)\,dU(x) & (0\le t<\infty),\\ 0 & (t<0),\end{cases} \qquad U(x)=\int_{\max(0,x)}^{\infty}B(y)\,dA(y-x).

The goal consists of the existence statement and the equation together. The equation alone is close to unfolding one step of the recursion. Existence is what ties it to a queue in steady state.

Milestones

(6.9), the CDF of $U=S-T$ as a convolution of $B$ and $A$ .
The one-step convolution (p.285): $W_q^{(n+1)}(t)=\int_{-\infty}^{t}W_q^{(n)}(t-x)\,dU(x)$ for $t\ge0$ .
(6.10)–(6.12), the Wiener–Hopf form: $W_q^-(t)+W_q(t)=\int_{-\infty}^t W_q(t-x)\,dU(x)$ for all $t$ , and $\bar W_q(s)=\bar W_q^-(s)/(A^*(-s)B^*(s)-1)$ for two-sided Laplace transforms.
The G/E_k/1 root result (p.278): the characteristic equation $z^k=A^*[k\mu(1-z)]$ has exactly one root in $(0,1)$ , one in $(-1,0)$ exactly when $k$ is even, and, when $A^*=[A_1^*]^k$ , exactly $k$ distinct roots in the open unit disk.
(6.18)–(6.20), the M/D/c generating function and $p_0$ in terms of the roots of $z^c=e^{-\lambda(1-z)}$ .
(6.33), the maximum-likelihood estimators $\hat\lambda=n_a/t$ , $\hat\mu=n_c/t_b$ for M/M/1.

Significance

Lindley's equation characterizes the stationary G/G/1 waiting time without any distributional assumption. The M/M/1, M/G/1 and G/M/1 waiting-time distributions of earlier chapters are its special cases. The transform relation (6.12) reduces the G/G/1 delay to a factorization problem for $A^*(-s)B^*(s)-1$ . The recursion and the equation are the starting point of Kingman's bound, of heavy-traffic approximations and of simulation of single-server systems.

All of these results are classical and proved. As far as a search of the platform shows, none of them is formalized. The platform's forward-coupling mission proves convergence to a stationary workload of a continuous-time queue that it assumes to exist. It proves neither the existence of a stationary law of Lindley's discrete recursion nor Lindley's equation. The mission therefore produces a machine-checked account of the G/G/1 recursion on distributions, a Loynes-type existence theorem for it, and the Wiener–Hopf transform identity. Its definitions (lifetime laws, the law of $S-T$ , the law map of the recursion, two-sided transforms) are reusable for Kingman's bound in the next mission of the series.

Difficulty

The obvious route to existence is to iterate the recursion from $W_q^{(0)}=0$ and take a limit. The distributions of $W_q^{(n)}$ from zero increase stochastically, but a limit of CDFs need not be a probability distribution: mass can escape to infinity, and it does when $\rho>1$ . Ruling this out under $\rho<1$ is the whole content of the existence half. It is a statement about the entire past of the input sequences, not about one step of the recursion, and the book asserts it without argument ("In the steady state ( $\rho<1$ ) …", p.285).

The transform identity (6.12) needs the right strip of convergence, which the book does not state. $A^*(-s)$ is finite only where the interarrival time has an exponential moment.

Formalization scope

Distributions are Mathlib measures on $\mathbb R$ . $A$ and $B$ are probability measures with no mass on $(-\infty,0)$ , with integrable identity where means are used. $\rho<1$ is stated as $\mathrm E[S]/\mathrm E[T]<1$ with $\mathrm E[T]>0$ . Independence is encoded by product measures: $U$ is the image of $B\otimes A$ under $(s,t)\mapsto s-t$ , and one step of the recursion is the image of $\nu\otimes U$ under $(w,u)\mapsto\max(0,w+u)$ . Stieltjes integrals over $(-\infty,t]$ are Lebesgue integrals over the closed half-line, so the atom $W_q(0)=q_0$ is counted. Transforms take complex arguments.

The closed forms carried by the statements are the following.

(6.8), in both of the book's forms, $\int_{-\infty}^t W_q(t-x)\,dU(x)$ and $-\int_0^\infty W_q(y)\,dU(t-y)$ .
(6.9) as an integral against the law of $T+x$ .
$U^*(s)=A^*(-s)B^*(s)$ and (6.12), for $0<\operatorname{Re}s$ with $\int e^{(\operatorname{Re}s)x}\,dA(x)<\infty$ . The division is stated only where $A^*(-s)B^*(s)\ne1$ .
(6.18) and (6.19) with the denominator $1-z^ce^{\lambda(1-z)}$ cleared on $|z|\le1$ , and (6.20) for $c\ge2$ . The roots $z_1,\dots,z_{c-1}$ are hypotheses: distinct, $\ne1$ , and exhausting the roots in the closed disk.
(6.33) as the unique maximizer of $-\lambda t-\mu t_b+n_a\ln\lambda+n_c\ln\mu$ over $\lambda,\mu>0$ .

A stationary delay distribution is a fixed point of the law map of the recursion, not an arbitrary CDF assumed to satisfy (6.8). A statement of (6.8) for "any CDF with $W_q=W_q*U$ on $[0,\infty)$ " would assume its own conclusion, and is excluded. The statement for M/D/c includes existence of a steady state under $\lambda<c$ as well as the formula for every steady state.

Not formalized: §6.1.1–6.1.2 (G/PH_k/1, quasi-birth–death processes), §6.4 (semi-Markov processes, whose limit theorems the book quotes without hypotheses), §6.5 (random-order and last-come service, series representations), §6.6 (design and control), and the rest of §6.7.

Contributions are welcome on the random-walk representation of the recursion, on the existence theorem under $\rho<1$ , and on the transform identities. The first two are reusable for any single-server or storage model driven by a reflected random walk.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
D. V. Lindley, "The theory of queues with a single server", Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 1952. https://doi.org/10.1017/S0305004100027638
R. M. Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 1962. https://doi.org/10.1017/S0305004100036094
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.
A. B. Clarke, "Maximum likelihood estimates in a simple queue", Annals of Mathematical Statistics 28(4), 1957. https://doi.org/10.1214/aoms/1177706796
M. L. Chaudhry, C. M. Harris, W. G. Marchal, "Robustness of rootfinding in single-server queueing models", ORSA Journal on Computing 2(3), 1990. https://doi.org/10.1287/ijoc.2.3.273

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization IV: Nonstationary Optimization and a Convergence Criterion for Nonmonotone SequencesTextbook

Motivation

Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective $f^0$ directly: $f^0$ may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces $f^0$ by a sequence of "good" approximations $F^0(\cdot, s)$ (smoothed versions, sample averages, perturbations) that converge to $f^0$ , and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective $F^0(\cdot, s)$ and the feasible set $X_s$ change with the iteration number $s$ , and the iterates $x^s$ are required to follow the time path of the optimal solutions,

\lim_{s\to\infty}\bigl[F^0(x^s, s) - \min\{F^0(x, s) \mid x \in X_s\}\bigr] = 0 .

Such procedures are essentially nonmonotone: a step on $F^0(\cdot, s)$ gives no guarantee of decrease of $F^0(\cdot, t)$ for $t \ge s+1$ , nor of $f^0$ . Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).

Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which $F^0(\cdot, s)$ and $X_s$ both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.

Setting

Throughout, points are vectors of $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$ .

The projection onto a nonempty closed convex set $X \subseteq \mathbb R^n$ is $\pi_X(y) = \arg\min\{\|y - x\|^2 : x \in X\}$ , the unique nearest point of $X$ to $y$ .
A subgradient of a convex function $F : \mathbb R^n \to \mathbb R$ at $x$ is a vector $g$ with $F(y) \ge F(x) + \langle g, y - x\rangle$ for all $y$ . The book writes $F^0_x(x, s)$ for a subgradient of $F^0(\cdot, s)$ at $x$ .
The nonstationary projected subgradient method (6.41) starts from any $x^0 \in \mathbb R^n$ and sets

x^{s+1} = \pi_X\bigl[x^s - \rho_s g_s\bigr], \qquad g_s \text{ a subgradient of } F^0(\cdot, s) \text{ at } x^s,\quad s = 0, 1, \dots

with step sizes $\rho_s \ge 0$ .

For a closed set $X^*$ (in the application, the set of minimizers of $f^0$ on $X$ ) and a sequence $(x^s)$ , the exit time from the $\varepsilon$ -ball around $x^{s_k}$ is $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ .
The Lyapunov function of the proof is $V(x) = \min_{x^* \in X^*}\|x^* - x\|^2$ , the squared distance to $X^*$ .

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Let $F^0(\cdot, s)$ and $f^0$ be convex continuous on $\mathbb R^n$ , $X$ a nonempty convex compact set, $F^0(\cdot, s) \to f^0$ uniformly on $X$ , $\|g_s\| \le C$ , $\rho_s \ge 0$ , $\rho_s \to 0$ and $\sum_s \rho_s = \infty$ . Then the iterates of (6.41) satisfy

F^0(x^s, s) \longrightarrow \min\{f^0(x) \mid x \in X\} \qquad (s \to \infty).

The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.

Milestones

p. 155 — the one-step recursion $V(x^{s+1}) \le V(x^s) + 2\rho_s\langle g_s, x^*(s) - x^s\rangle + \rho_s^2\|g_s\|^2$ , with $x^*(s)$ a point of $X^*$ nearest to $x^s$ .
p. 156 — the travel bound $\|x^b - x^a\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s$ along (6.41) once $x^a \in X$ .
p. 155 — conditions (1) and (2)(a) of Theorem 6.4 for (6.41): the iterates stay in a compact set and $\|x^{s+1} - x^s\| \to 0$ .
Theorem 6.4 (p. 155) — if $X^*$ is closed, $(x^s)$ lies in a compact set, steps vanish along subsequences converging into $X^*$ , the sequence leaves every small ball around a subsequential limit outside $X^*$ , and it leaves with a strictly lower value of a continuous $V$ that takes countably many values on $X^*$ , then $V(x^s)$ converges and all accumulation points lie in $X^*$ .
pp. 155–156 — conditions (2)(b) and (3) of Theorem 6.4 for (6.41) with $X^* = \arg\min_X f^0$ and $V = \operatorname{dist}(\cdot, X^*)^2$ :

\limsup_{k\to\infty} V(x^{\tau_k}) < \lim_{k\to\infty} V(x^{s_k}).

Significance

Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which $f^0$ is replaced by $F^0(x, s) = \mathbb E f^0(x + h(s))$ with a vanishing perturbation $h(s)$ (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.

Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.

Difficulty

The obvious argument for projected subgradient methods tracks $V(x^s) = \operatorname{dist}(x^s, X^*)^2$ and shows that it decreases whenever $x^s$ is far from $X^*$ . Here that argument fails at two points. First, the subgradient is taken on $F^0(\cdot, s)$ , not on $f^0$ , so the decrease of $V$ holds only up to an error controlled by $\sup_X|F^0(\cdot, s) - f^0|$ , and only while the iterate stays away from $X^*$ ; near $X^*$ , $V$ may increase. Second, a decrease of $V$ over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point $x' \notin X^*$ infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that $V$ takes only countably many values on $X^*$ is what separates it from a monotone-descent statement.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from $s = 0$ as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of $\mathbb R^n$ , and $F^0(\cdot, s)$ , $f^0$ are convex and continuous on all of $\mathbb R^n$ .
projX X y is a minimizer of $\|y - x\|^2$ over $X$ (junk value $y$ when none exists; every statement assumes $X$ nonempty, closed and convex). optimalSet f X is the set of minimizers of $f$ on $X$ ; $V$ is Metric.infDist · X* ^ 2.
Added hypotheses the page does not print: $\rho_s \ge 0$ (step sizes are nonnegative throughout the chapter) and $X \ne \varnothing$ (the minimum over $X$ must exist). The limit $\min_X f^0$ is written sInf (f '' X); $\sum_s\rho_s = \infty$ is divergence of the partial sums.
Constants. The only unspecified constant is the $C$ of the travel bound on p. 156 ("where $C$ is a constant"); the proof yields $C$ = the bound of hypothesis (d), $\|g_s\| \le C$ , and that is the constant in milestone 2. All other results are qualitative.
Corrections of the page. (i) Theorem 6.4 (2)(b) is printed as " $\tau_k = \min\{s \mid s \ge s_k, \|x^{s_k} - x^s\| < \varepsilon\} > \infty$ ", which no sequence satisfies; following the proof of Theorem 6.3 it is read as: $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ is finite. "For $\varepsilon$ sufficiently small and for any $s_k$ " is read as "there is $\varepsilon_0 > 0$ such that for all $\varepsilon \in (0,\varepsilon_0)$ and all $k$ ", and condition (3) is imposed for the same $\varepsilon$ . (ii) The left limit in (3) is read as $\limsup$ (the proof prints $\overline{\lim}$ ); the right limit is $V(x')$ . (iii) The display on p. 155 prints " $=$ " where the projection gives " $\le$ ". (iv) The proof on p. 155 prints " $x^{s_k} \to x' \in X^*$ " where $x' \notin X^*$ is meant.
Theorem 6.5 (the stochastic version, p. 156) is not formalized: the chapter states it without proof, citing [19], its moment hypothesis $E\|\xi^0(s)\| < \mathrm{const}$ and the measurability of the random step sizes $\rho_s$ are not pinned down on the page, and it is not used by Theorem 6.3.
A trivializing formalization is ruled out: the goal is about the iteration (6.41) itself, not a statement that assumes $x^s \to X^*$ and derives the limit of the values, and no hypothesis forces the sequence or the functions to be constant.
Contributions welcome: properties of projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.

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, pp. 141–185 (§6.4, pp. 152–156). https://doi.org/10.1007/978-3-642-61370-8
Yu. M. Ermoliev, Stochastic Programming Methods (in Russian), Nauka, Moscow, 1976 (the chapter's [5]; Theorem 6.4 is on p. 181).
Yu. M. Ermoliev and E. A. Nurminski, "Limit extremal problems", Kibernetika 1 (1973) (the chapter's [14]).
E. A. Nurminski, "Convergence conditions of algorithms of stochastic programming", Kibernetika 3 (1973) (the chapter's [11]).
E. A. Nurminski, "The problem of nonstationary optimization", Kibernetika 2 (1977) (the chapter's [16]).
A. A. Gaivoronski, "Nonstationary stochastic programming problems", Kibernetika 4 (1978) (the chapter's [19]).
W. I. Zangwill, Nonlinear Programming: A Unified Approach, Prentice-Hall, 1969.

8 thms3 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research+1·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources I: A Time-Feasible Schedule Exists iff the Project Network Has No Cycle of Positive LengthTextbook

Motivation

Project scheduling assigns start times to the activities of a project subject to constraints between them. The classical critical path method (CPM) of Kelley and Walker (1959) and the program evaluation and review technique (PERT) allow only minimum time lags: activity $j$ may start no earlier than a given time after activity $i$ starts. Practice also needs maximum time lags: activity $j$ must start no later than a given time after $i$ . These express deadlines, release dates, time windows and "no wait" couplings. Once maximum time lags are allowed, the project network has cycles and negative arc weights, and even the existence of a schedule is no longer automatic.

This mission is the first of a series on Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), a standard reference for resource-constrained project scheduling with general temporal constraints. Chapter 1 contains the temporal part of the theory: feasibility, earliest and latest schedules, floats, and the distance order. Every later chapter adds resource constraints on top of this layer.

Timeline. Roy (1964) introduced the Metra Potential Method, which is scheduling on activity-on-node networks with minimum time lags. Neumann (1975, Sect. 6.4) treated time windows through potentials on networks with arbitrary arc weights. Bartusch, Möhring and Radermacher (1988, Annals of Operations Research 16) developed the general theory of scheduling project networks with resource constraints and time windows, including the feasibility criterion stated below. The book collects these results in Chapter 1.

Setting

A project consists of $n\ge 1$ real activities $1,\dots,n$ and two fictitious activities, $0$ (project beginning) and $n+1$ (project completion), so the node set is $V=\{0,1,\dots,n+1\}$ . Each activity $i$ has an integer duration $p_i$ , with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities.

A minimum time lag $d^{\min}_{ij}$ between two different activities becomes an arc $\langle i,j\rangle$ of weight $\delta_{ij}=d^{\min}_{ij}$ . A maximum time lag $d^{\max}_{ij}$ becomes a backward arc $\langle j,i\rangle$ of weight $\delta_{ji}=-d^{\max}_{ij}$ . There is at most one arc per ordered pair, keeping the tightest lag. The result is the activity-on-node (AoN) network $N=(V,E,\delta)$ , whose integer weights may be positive, negative or zero and which in general contains cycles. The book establishes that for every node $i$ there is a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$ (p. 8, from Definition 1.1.1 and Remarks 1.1.2). This is the standing assumption of the chapter.

A schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ and $S_i\ge 0$ . It is time-feasible if it satisfies the temporal constraints

S_j-S_i\ \ge\ \delta_{ij}\qquad(\langle i,j\rangle\in E),

and $\mathcal S_T$ is the set of time-feasible schedules. A time-feasible schedule minimizing the project duration $S_{n+1}$ is time-optimal.

The length of a path or cycle is the sum of its arc weights. For an integer $L=LS_{n+1}$ , which is either a prescribed maximum project duration $\bar d$ or the shortest project duration, the temporal scheduling network $N^+$ adds the backward arc $\langle n+1,0\rangle$ with weight $-L$ . The distance $d_{ij}$ is the length of a longest path from $i$ to $j$ in $N^+$ , with $d_{ii}=0$ . The earliest and latest start times are $ES_i=d_{0i}$ and $LS_i=-d_{i0}$ , the earliest completion time is $EC_i=ES_i+p_i$ , and the total float is $TF_i=LS_i-ES_i$ . The distance order $\prec_D$ is defined for $i\ne j$ by: $i\prec_D j$ if $d_{ij}>0$ , or $d_{ij}=0$ and $d_{ji}<0$ .

Formalization targets

Goal: Theorem 1.3.3 (p. 10)

\mathcal S_T\ne\emptyset\quad\Longleftrightarrow\quad N\ \text{contains no cycle of positive length}.

The statement contains no constants. It is the consistency criterion for the temporal constraints and the entry condition for everything else in the book.

Milestones

Distances, §1.3, p. 11, Eq. (1.3.3). If $N^+$ has no cycle of positive length, then $d$ satisfies $d_{ij}\ge\delta_{ij}$ on $E^+$ and the triangle inequality $d_{ij}\ge d_{ih}+d_{hj}$ , and it is the smallest family that does.
Earliest and latest schedules, §1.3, p. 12. Under the same hypothesis and the standing assumption, $ES=(d_{0i})_i$ is time-feasible and lies below every time-feasible schedule. $LS=(-d_{i0})_i$ is time-feasible, satisfies $LS_{n+1}\le L$ , and lies above every time-feasible schedule $S$ with $S_{n+1}\le L$ .
Remark 1.3.2 (p. 10). If $\mathcal S_T\ne\emptyset$ , there is an integer-valued time-optimal schedule.
Proposition 1.3.8 (p. 15). For a real activity $i$ , $[LS_i,EC_i[\ne\emptyset$ if and only if $i$ is critical ( $TF_i=0$ ) or near-critical ( $0<TF_i<p_i$ ). A further item of the mission, not a milestone, states the claim of §1.4, p. 17 (after Definition 1.4.3): if $N^+$ has no cycle of positive length, $\prec_D$ is a strict order on $V$ .

Significance

The result itself. Theorem 1.3.3 tells when the temporal constraints of a project can be met at all. Milestones 1 and 2 identify the earliest and latest schedules with longest path lengths, which makes temporal scheduling a pair of longest-path computations (a forward pass from $0$ and a backward pass to $0$ ). Remark 1.3.2 justifies working in integer time. The distance order and the base time intervals $[LS_i,EC_i[$ are the inputs of the resource-constrained methods in Chapters 2 and 3: priority rules schedule along $\prec_D$ , and base time intervals give lower bounds on resource usage.

Formalizing it. These results are classical and proved, but the book does not prove Theorem 1.3.3; it points to Neumann (1975) and Bartusch et al. (1988). To our knowledge they have no machine-checked form in this generality, with arbitrary integer weights, cycles, fictitious start and end nodes, and the backward arc of $N^+$ . The CPM results for acyclic event networks with nonnegative durations already on Prove2Me are a special case. The definitions of this mission (project, AoN network, schedule, $N^+$ , distances) are intended as the shared substrate for the later missions of the series, which add renewable and cumulative resources.

Difficulty

The necessity direction of the goal is a telescoping sum around a cycle. The sufficiency direction needs a schedule, and the natural candidate $S_i=d_{0i}$ requires three things: longest path lengths must be well defined, they must be finite, and they must satisfy the temporal constraints. With negative weights and cycles, the maximum over walks is unbounded when a positive cycle exists, and a walk-based definition gives nothing. A path-based definition gives a finite maximum but loses the concatenation property, so the triangle inequality becomes a statement about removing nonpositive cycles from walks. $S_0=0$ and $S_i\ge 0$ further depend on the standing assumption: without it, an arc $\langle i,0\rangle$ with positive weight makes $\mathcal S_T$ empty although no cycle is positive. The same combinatorics of walks, paths and cycles is behind milestones 1 and 2 and the distance-order item.

Formalization scope

Nodes are Fin (n + 2): $0$ is the project beginning and Fin.last (n + 1) the project completion. The field one_le_n records $n\ge 1$ . Durations are natural numbers with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities. Arc weights are arbitrary integers on a loop-free Finset of ordered pairs, so parallel arcs cannot occur. Start times are real; integrality appears only as Remark 1.3.2.

Walks are functions Fin (m + 1) → Fin (n + 2). A path is an injective walk, and a cycle is a closed walk with at least one arc and distinct nodes apart from the repeated endpoint. Distances are maxima over the finitely many paths, valued in WithBot ℤ with $\bot=-\infty$ for unreachable pairs. No supremum over an unbounded set is taken. $ES_i$ and $LS_i$ convert these to integers with junk value $0$ for $-\infty$ , and every milestone that uses them carries the hypotheses under which the distances are finite. The backward arc of $N^+$ has weight $-L$ for an integer parameter $L$ . If $N$ already contains an arc $\langle n+1,0\rangle$ , the two arcs merge into one carrying the larger weight, as in the book's convention for parallel lags. The standing assumption of p. 8 is a named predicate and a hypothesis of the goal and of milestones 2 and 4.

A trivializing formalization is ruled out: weights are signed integers and cycles are allowed, so the no-positive-cycle condition is not vacuous, and the standing assumption is satisfiable by projects with maximum time lags.

A complete development needs cycle removal from closed walks, the Bellman-type characterization of longest paths without positive cycles, and total unimodularity or a direct integrality argument for Remark 1.3.2. The walk, path and distance layer is reusable for any difference-constraint system. Proofs of milestones and lemmas on walk decomposition are welcome.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, "Scheduling project networks with resource constraints and time windows", Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745
K. Neumann, Operations Research Verfahren, Band III, Hanser, 1975, Sect. 6.4.
B. Roy, Les problèmes d'ordonnancement: applications et méthodes, Dunod, 1964.
J. E. Kelley, M. R. Walker, "Critical-path planning and scheduling", Proceedings of the Eastern Joint Computer Conference, 1959, 160–173. https://doi.org/10.1145/1460299.1460318
R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993, Sect. 5.4 and 5.6.

8 thms3 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+1·Captain: mikedeng1

Understanding and Using Linear Programming V: The Primal–Dual Central Path and the Self-Dual EmbeddingTextbook

Motivation

Interior point methods solve linear programs in a number of iterations polynomial in the input size, and in practice they compete with the simplex method on large instances. Their modern form goes back to Karmarkar's projective algorithm (Karmarkar 1984); the primal–dual path-following variant analysed in textbooks follows a curve, the central path, defined by a perturbed system of optimality conditions. Two facts make the method well defined. First, the central path exists and is unique whenever the primal and dual programs have strictly feasible points. Second, an arbitrary linear program, possibly infeasible or unbounded, can be embedded in an auxiliary program that has an explicit starting point on its own central path and whose suitable optimal solutions either solve the original program or certify that it has no optimum.

Chapter 7, §7.2 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer 2007), presents both facts in elementary form, following Terlaky (2001). This mission formalizes its three numbered lemmas.

Timeline. The homogeneous system bearing their names is due to Goldman and Tucker (1956), in the study of the structure of optimal solution sets; the self-dual embedding for interior point methods was introduced by Ye, Todd and Mizuno (1994), and the book's presentation follows the skew-symmetric form in Roos, Terlaky and Vial (2005).

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ . The linear program in equational form (7.2) is

\text{maximize } c^{T}x \text{ subject to } Ax=b,\ x\ge 0,

where $A$ has rank $m$ ; its dual (7.5) is: minimize $b^{T}y$ subject to $A^{T}y\ge c$ , $y\in\mathbb{R}^m$ . The notation $x>0$ means that all coordinates of $x$ are strictly positive. For $\mu>0$ the barrier function is $f_\mu(x)=c^{T}x+\mu\sum_{j=1}^n\ln x_j$ , defined for $x>0$ . The central-path system (7.4), in unknowns $x,s\in\mathbb{R}^n$ and $y\in\mathbb{R}^m$ , is

Ax=b,\qquad A^{T}y-s=c,\qquad (s_1x_1,\dots,s_nx_n)=\mu\mathbf 1,\qquad x,s\ge 0 .

For the embedding, the book switches to the inequality form (7.7): maximize $c^{T}x$ subject to $Ax\le b$ , $x\ge 0$ , with dual: minimize $b^{T}y$ subject to $A^{T}y\ge c$ , $y\ge 0$ . The Goldman–Tucker system (GTS) is

Ax-\tau b\le 0,\qquad -A^{T}y+\tau c\le 0,\qquad b^{T}y-c^{T}x\le 0,\qquad x,y\ge 0,\ \tau\ge 0,

and $\rho=\rho(x,y)=c^{T}x-b^{T}y$ is the slack of its last inequality. With $u=(y,x,\tau)\in\mathbb{R}^k$ , $k=n+m+1$ , (GTS) reads $M_0u\le 0$ , $u\ge 0$ for the skew-symmetric matrix

M_0=\begin{pmatrix}0&A&-b\\-A^{T}&0&c\\b^{T}&-c^{T}&0\end{pmatrix}.

Put $r=\mathbf 1+M_0\mathbf 1$ , $M=\begin{pmatrix}M_0&-r\\r^{T}&0\end{pmatrix}$ and $q=(0,\dots,0,k+1)\in\mathbb{R}^{k+1}$ . The self-dual program (SD) in $v=(u,\vartheta)$ is: maximize $-q^{T}v$ subject to $Mv\le q$ , $v\ge 0$ . Its slacks are $z=q-Mv$ , and a feasible $v$ is strictly complementary if $v_j>0$ or $z_j>0$ for every $j=1,\dots,k+1$ .

Formalization targets

Goal: Lemma 7.2.1 (p. 121)

If (7.2) has a feasible $\tilde x>0$ and (7.5) has a feasible $\tilde y$ with $\tilde s=A^{T}\tilde y-c>0$ , then for every $\mu>0$

\exists!\,(x^*,y^*,s^*)\ \text{solving (7.4)},\qquad x^*=\arg\max\{f_\mu(x): Ax=b,\ x>0\}\ \text{(uniquely)}.

Milestones

Claim in the proof of Lemma 7.2.1 (p. 121): under the lemma's assumptions and for fixed $\mu>0$ , the set $Q=\{x: Ax=b,\ x>0,\ f_\mu(x)\ge f_\mu(\tilde x)\}$ is bounded.
Lemma 7.2.2 (p. 126): no solution of (GTS) has $\tau\ne 0$ and $\rho\ne 0$ ; exactly one of "a solution with $\tau>0$ " and "a solution with $\rho>0$ " exists; in the first case $\frac1\tau x$ and $\frac1\tau y$ are optimal for (7.7) and its dual; in the second, (7.7) is infeasible or unbounded.
Lemma 7.2.3 (p. 128): (SD) is feasible and bounded, every optimal solution has $\vartheta=0$ and its $u$ -part solves (GTS), and every strictly complementary optimal solution gives a solution of (GTS) with $\tau>0$ or $\rho>0$ .

Significance

Lemma 7.2.1 is what makes "the central path" a well-defined object: without existence, a path-following method has nothing to follow, and without uniqueness the point $x^*(\mu)$ that the algorithm approximates is not determined. It also identifies the barrier maximizer with the solution of the Lagrange system (7.4), which is the system the Newton steps of the algorithm linearize. Lemmas 7.2.2 and 7.2.3 remove the need for an interior starting point and for knowing in advance that the program has an optimum: every linear program reduces to computing a strictly complementary optimal solution of a program with a known interior point on its central path.

The three lemmas are classical and proved in the book (7.2.2 as a sketch). Formalizing them adds a machine-checked account of the central path in equational form, and of the Goldman–Tucker and self-dual constructions with explicit block matrices, reusable by any later formalization of interior point complexity bounds. As far as a search of the platform shows, no formal statement of the Goldman–Tucker system or of the self-dual embedding exists there; the nearest item, Lemma 9.5 of Introduction to Linear Optimization XII (Bertsimas–Tsitsiklis), characterizes the central path by KKT conditions and is not linked to a formal statement.

Difficulty

For Lemma 7.2.1, uniqueness of a maximizer follows from strict concavity, but existence does not: the feasible region $\{Ax=b,\ x>0\}$ is open relative to its affine hull and typically unbounded, and $f_\mu$ need not attain its supremum on such a set. The interior dual point is what rules out escape to infinity; the primal interior point is what rules out escape to the boundary. Identifying the maximizer with the unique solution of (7.4) further needs the Lagrange multiplier rule on an open set and the full row rank of $A$ to determine $y$ from $s$ .

For Lemma 7.2.2 the exclusivity and the optimality statements are weak-duality arguments, but existence of a solution with $\rho>0$ when (7.7) is infeasible or unbounded requires a Farkas-type alternative for both the primal and the dual, and the case split in the book's sketch ("the dual case is analogous") must be carried out. Lemma 7.2.3 requires bookkeeping with the block structure of $M$ and the skew-symmetry of $M_0$ .

Formalization scope

Vectors are functions Fin n → ℝ and Fin m → ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Matrices are Matrix (Fin m) (Fin n) ℝ, inequalities between vectors are componentwise, $x>0$ is ∀ j, 0 < x j. The rank condition of (7.2) is the hypothesis A.rank = m. Optimal solutions and unboundedness are expressed against every feasible point, never through a real supremum. The vector $u=(y,x,\tau)$ is indexed by Fin m ⊕ Fin n ⊕ Unit and $v=(u,\vartheta)$ by (Fin m ⊕ Fin n ⊕ Unit) ⊕ Unit; $M_0$ , $r$ , $M$ and $q$ are defined entrywise on these index types, with the last entry of $q$ equal to $k+1=n+m+2$ . "Exactly one" in Lemma 7.2.2 is Xor.

Lean's Real.log returns $0$ for nonpositive arguments, so a statement comparing $f_\mu$ over $\{Ax=b\}$ or $\{Ax=b,\ x\ge 0\}$ would be a different, and generally false or trivial, claim; every comparison of barrier values is restricted to points with all coordinates strictly positive. The unique solution of (7.4) is stated as existence plus equality of every solution with it, not as existence of some solution.

Useful infrastructure: strict concavity of sums of logarithms, the Lagrange multiplier rule for affine constraints (Mathlib's IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt or a direct orthogonality argument), compactness of closed bounded sets in Fin n → ℝ, and Farkas' lemma in the forms of Proposition 6.4.1 of the book. Proofs of the milestones, alternative arguments, and general lemmas about skew-symmetric linear programs are all welcome.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §7.2. https://doi.org/10.1007/978-3-540-30717-4
T. Terlaky, An easy way to teach interior-point methods, European Journal of Operational Research 130(1), 2001, 1–19.
C. Roos, T. Terlaky, J.-P. Vial, Interior Point Methods for Linear Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/b100325
A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt{n}L)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 1994, 53–67. https://doi.org/10.1287/moor.19.1.53
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, 373–395. https://doi.org/10.1007/BF02579150
F. A. Potra, S. J. Wright, Interior-point methods, Journal of Computational and Applied Mathematics 124, 2000, 281–302.

6 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+2·Captain: mikedeng1

Understanding and Using Linear Programming I: Integral Bipartite Matchings, Total Unimodularity and König's TheoremTextbook

Motivation

Many combinatorial optimization problems are integer programs: linear objectives and linear constraints, with the extra requirement that the variables be integers. Dropping that requirement gives the LP relaxation, which is solvable efficiently but in general only bounds the integer optimum. For a small but important class of problems the relaxation loses nothing: its optimum is attained at an integral point, so linear programming solves the combinatorial problem exactly. Bipartite matching is the standard example, and the job-assignment problem that opens Chapter 3 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) is a maximum-weight perfect matching problem in a bipartite graph.

The same phenomenon, combined with linear programming duality, produces combinatorial min–max theorems. The oldest of them is König's theorem (1931) on matchings and vertex covers in bipartite graphs; Hall's marriage theorem (1935) follows from it. This mission formalizes the book's treatment of both strands: the integrality of the bipartite matching LP (Section 3.2), total unimodularity and König's theorem (Section 8.2), and, on the same objects for general graphs, the LP-rounding 2-approximation for vertex cover (Section 3.3).

Setting

Let $G = (V, E)$ be a finite simple graph. A bipartition of $G$ is a pair of disjoint sets $X, Y$ with $X \cup Y = V$ such that every edge joins a vertex of $X$ to a vertex of $Y$ ; $G$ is bipartite if it has one. A matching is a set $M \subseteq E$ in which each vertex is incident to at most one edge; a vertex cover is a set $C \subseteq V$ containing at least one end-vertex of every edge. A matching is maximum if no matching has more edges; a vertex cover is minimum if no vertex cover has fewer vertices.

The incidence matrix of $G$ has a row for each vertex and a column for each edge, with entry $1$ when the vertex lies on the edge and $0$ otherwise. A real matrix is totally unimodular if every square submatrix, obtained by deleting some rows and some columns, has determinant $0$ , $1$ or $-1$ .

Given real edge weights $w_e$ , the integer program (3.1) maximizes $\sum_{e} w_e x_e$ subject to $\sum_{e \ni v} x_e = 1$ for every vertex $v$ and $x_e \in \{0,1\}$ ; its 0/1 solutions are the perfect matchings. Its LP relaxation replaces $x_e \in \{0,1\}$ by $0 \le x_e \le 1$ . The vertex-cover relaxation (3.3) minimizes $\sum_v x_v$ subject to $x_u + x_v \ge 1$ for every edge $\{u,v\}$ and $0 \le x_v \le 1$ .

Formalization targets

Goal: König's theorem (Theorem 8.2.2)

For every finite bipartite graph $G$ ,

\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{|C| : C \text{ a vertex cover of } G\}.

Total unimodularity (Lemmas 8.2.3–8.2.5)

A \text{ TU} \;\Rightarrow\; (A \mid e_i) \text{ TU}; \qquad A \text{ TU},\ b \in \mathbb{Z}^m,\ \max\{c^Tx : Ax \le b,\ x \ge 0\} \text{ attained} \;\Rightarrow\; \text{attained at some } x^* \in \mathbb{Z}^n;

and the incidence matrix of a bipartite graph is totally unimodular.

Integrality of the perfect-matching relaxation (Theorem 3.2.1)

If the LP relaxation of (3.1) for a bipartite graph with real weights is feasible, it has an optimal solution with all $x_e \in \{0,1\}$ , which is also optimal for (3.1).

Consequences on the same objects

Hall's theorem (Theorem 8.2.1): if $|N(T)| \ge |T|$ for every $T \subseteq X$ , where $N(T) \subseteq Y$ is the set of neighbours of $T$ , then some matching covers every vertex of $X$ . And for an arbitrary graph, with $x^*$ optimal for (3.3), $S_{LP} = \{v : x^*_v \ge \tfrac12\}$ and $S_{OPT}$ a minimum vertex cover (§3.3, p. 38):

S_{LP} \text{ is a vertex cover and } |S_{LP}| \le 2\,|S_{OPT}| .

Significance

König's theorem says that for bipartite graphs the two natural certificates, a matching (a lower bound on any vertex cover) and a vertex cover (an upper bound on any matching), always meet. It makes maximum matchings and minimum vertex covers computable by linear programming, whereas minimum vertex cover in general graphs is NP-hard; Section 3.3's rounding bound quantifies what the LP still gives in that general case. Lemma 8.2.4 is the general tool behind this and behind the max-flow min-cut theorem that the book mentions on p. 148: any integer program with a totally unimodular constraint matrix and integral right-hand side can be solved as a linear program.

All results here are classical and proved. The formalization work is to connect them: Mathlib already has the definition of total unimodularity (Matrix.IsTotallyUnimodular), closure under appending unit-like rows, and Hall's theorem in the form of Finset.all_card_le_biUnion_card_iff_exists_injective. To the best of the drafting survey, neither König's theorem nor the total unimodularity of bipartite incidence matrices nor the integrality lemma 8.2.4 is in Mathlib, and no König statement was found among the platform's missions. The mission produces these in a form that later chapters on network flows and combinatorial duality can import.

Difficulty

The inequality "maximum matching $\le$ minimum vertex cover" is immediate, since each edge of a matching needs its own cover vertex. The difficulty is the reverse inequality, and it is exactly where bipartiteness is needed: the triangle has maximum matching $1$ and minimum vertex cover $2$ . Along the book's route, the obstacle is that LP duality equates the optima of the two relaxations, which are real numbers; one must show that both relaxations already have integral optimal solutions, which is the content of total unimodularity and Lemma 8.2.4. Theorem 3.2.1 is a separate integrality statement with equality constraints and weights of arbitrary sign; it is not a consequence of the Birkhoff–von Neumann theorem unless the graph is complete bipartite with equal sides.

Formalization scope

Graphs are SimpleGraph V on a Fintype vertex type with decidable equality; edges are elements of Sym2 V, and a matching is a Finset (Sym2 V) of edges. Bipartiteness is the existence of finite sets $X, Y$ forming a bipartition; the empty graph and the empty vertex type are allowed and the statements remain the book's there. Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Matrices are real; LP vectors are Fin n → ℝ (0-based indices) or indexed by the edge set or the vertices. An "optimal solution" is always a feasible point that is at least as good as every feasible point: no supremum or infimum over a possibly empty or unbounded set is used, and König's theorem asserts that both a maximum matching and a minimum vertex cover exist and have equal size. Lemma 8.2.4 takes $b \in \mathbb{Z}^m$ and allows real $c$ ; its conclusion is an integral optimal solution, not merely an integral feasible one. Theorem 3.2.1 is the perfect-matching version with equality constraints, not the " $\le 1$ " matching version discussed in the book's remarks.

A formalization in which König's theorem compares a supremum and an infimum of possibly empty sets, or in which "optimal" is not tied to feasibility, would be trivializing and is ruled out by these conventions.

Useful infrastructure, reusable beyond this mission: Laplace expansion arguments for totally unimodular matrices, the equivalence of the inequality form with the equational form, existence of optimal basic feasible solutions, and LP duality in inequality form (the platform's LinearOptimization.lp_strong_duality states duality for a general-form LP). Combinatorial proofs of König and Hall are equally welcome; only the statements are fixed.

Selected references

J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §3.2–3.3 and §8.2. https://doi.org/10.1007/978-3-540-30717-4
D. Kőnig, "Gráfok és mátrixok", Matematikai és Fizikai Lapok 38 (1931), 116–119.
P. Hall, "On representatives of subsets", Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
A. J. Hoffman, J. B. Kruskal, "Integral boundary points of convex polyhedra", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton, 1956, 223–246. https://doi.org/10.1515/9781400881987-014
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, Chapter 19.

14 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Fundamentals of Queueing Theory VII: The Geometric Arrival-Point Law of the G/M/1 QueueTextbook

Motivation

Most queueing models with a closed-form answer assume Poisson arrivals. In practice the times between arrivals are often far from exponential: scheduled appointments, batch releases from an upstream process, or arrivals timed by a machine cycle. The G/M/1 queue keeps the service side exponential and makes no assumption about the arrival stream beyond independent, identically distributed interarrival times. It is the standard counterpart of the M/G/1 queue, and its solution is the one used in teaching and in practice whenever the input is not Poisson (Gross, Shortle, Thompson & Harris, Fundamentals of Queueing Theory, 4th ed., Wiley 2008, §5.3.1, DOI 10.1002/9781118625651).

The answer has an unusually clean form. The number of customers that an arriving customer finds in the system is geometric, exactly as in the M/M/1 queue, with the traffic intensity $\rho$ replaced by a number $r_0$ that depends on the whole interarrival distribution through a single scalar equation. This mission is the seventh of a series formalizing the book chapter by chapter; it covers the G/M/1 half of §5.3 (printed pp.259–263).

Setting

Customers arrive at a single server. The interarrival times are independent with common law $A$ , a probability distribution on $[0,\infty)$ with CDF $A(t)$ and finite mean $E[T] = 1/\lambda$ , $\lambda > 0$ . Service times are independent exponential random variables with rate $\mu > 0$ , and the discipline is first come, first served.

Let $X_n$ be the number of customers in the system just before the $n$ th arrival. Between two arrivals the server completes a Poisson number of services (truncated by the number present), so $\{X_n\}$ is a Markov chain on $\{0,1,2,\dots\}$ . Its transition probabilities are built from

b_k = \int_0^\infty \frac{e^{-\mu t}(\mu t)^k}{k!}\,dA(t) \qquad (k \ge 0),

the probability of exactly $k$ completions during one interarrival time (Eq. (5.50)): $p_{i0} = 1 - \sum_{k=0}^{i} b_k$ , $p_{ij} = b_{i+1-j}$ for $1 \le j \le i+1$ , and $p_{ij} = 0$ otherwise (Eq. (5.51)). A stationary arrival-point distribution is a probability vector $q = \{q_n\}$ with $qP = q$ and $qe = 1$ (Eq. (5.52)); $q_n$ is the long-run probability that an arrival finds $n$ customers present.

The characteristic equation of the chain is

z = \beta(z), \qquad \beta(z) = \sum_{n \ge 0} b_n z^n ,

where $\beta$ is the probability generating function of $\{b_n\}$ (Eq. (5.55)). Equivalently $z = A^*[\mu(1-z)]$ (Eq. (5.56)), where $A^*(s) = \int_0^\infty e^{-sx}\,dA(x)$ is the Laplace–Stieltjes transform of the interarrival law. The traffic intensity is $\rho = \lambda/\mu$ .

Formalization targets

Goal: Eq. (5.60), the geometric arrival-point law

If $\rho = \lambda/\mu < 1$ , there is a number $r_0$ with $0 < r_0 < 1$ and $r_0 = \beta(r_0)$ , it is the only complex root of $z = \beta(z)$ in the open unit disk, and

q_n = (1 - r_0)\, r_0^{\,n} \qquad (n \ge 0)

is a stationary arrival-point distribution and the only one. The root is part of the conclusion, not an assumption.

Milestones

Eqs. (5.51)–(5.53): for a probability vector $q$ , $qP = q$ is equivalent to $q_i = \sum_{k\ge0} q_{i+k-1}b_k$ ( $i \ge 1$ ) and $q_0 = \sum_{j\ge0} q_j\bigl(1 - \sum_{k=0}^{j} b_k\bigr)$ .
p.261: $0 < b_0 < 1$ , $b_n > 0$ for all $n$ , $\beta(1) = 1$ , and $\beta'(1) = \sum_n n b_n = \mu/\lambda$ .
Eq. (5.56): $\beta(z) = A^*[\mu(1-z)]$ for $|z| \le 1$ .
Eq. (5.58), Figure 5.2: $z = \beta(z)$ has at most one root in $(0,1)$ , and one exists if and only if $\lambda/\mu < 1$ .
p.262: when $\lambda/\mu < 1$ , $z = \beta(z)$ has exactly one root with $|z| < 1$ .
Eq. (5.59): successive substitution $z^{(k+1)} = \beta(z^{(k)})$ from any $0 < z^{(0)} < 1$ converges to $r_0$ .
Eq. (5.61): $L^{(A)} = r_0/(1-r_0)$ and $L_q^{(A)} = r_0^2/(1-r_0)$ .
Eq. (5.62): $W_q(t) = 1 - r_0 e^{-\mu(1-r_0)t}$ and $W(t) = 1 - e^{-\mu(1-r_0)t}$ for $t \ge 0$ .
Eq. (5.63): $W_q = r_0/(\mu(1-r_0))$ and $W = 1/(\mu(1-r_0))$ .

Significance

The result. Equation (5.60) reduces the analysis of a queue with arbitrary renewal input to one scalar root. Every arrival-point performance measure of the M/M/1 queue then carries over with $\rho$ replaced by $r_0$ : the mean number found by an arrival, the mean queue found by an arrival, and the full distributions of line delay and system time seen by arrivals (Eqs. (5.61)–(5.63)). The same root drives the multiserver G/M/c analysis later in §5.3 and the relation between arrival-point and time-average probabilities in §6.3. The result also illustrates a point the book stresses: $q_n$ is the distribution seen by arrivals, and it equals the time-average distribution $p_n$ only when the input is Poisson.

Formalizing it. The mathematics is classical (the embedded-chain method goes back to Kendall, 1953) and fully proved in the textbook literature; nothing here is open. To our knowledge none of it has a machine-checked proof: the platform had no G/M/1, embedded-chain, or Rouché-type statement when this mission was drafted. The work is to formalize the known argument, which touches analytic facts about power series with nonnegative coefficients, a mixture-of-Poisson computation, a counting of roots in the unit disk, and the uniqueness of the stationary law of an irreducible countable chain.

Difficulty

Locating a real root in $(0,1)$ is a one-variable question. The hard step is excluding every other complex root inside the unit disk: a real-variable argument says nothing about complex roots, and the book's route relies on Rouché's theorem, which Mathlib does not have. A second point is uniqueness of the stationary vector: showing that the geometric vector solves $qP = q$ does not show that no other probability vector does, and the goal asserts both. Computing $\sum_n n b_n = \mu/\lambda$ requires interchanging a sum with the integral against $A$ , which is where the finite mean of the interarrival law enters.

Formalization scope

The interarrival law is a measure A : Measure ℝ with IsProbabilityMeasure A, A (Set.Iio 0) = 0, integrable identity, and ∫ x ∂A = 1/λ (the structure IsInterarrivalLaw). Every theorem also assumes $\lambda > 0$ and $\mu > 0$ . The integrals defining $b_k$ and $A^*$ are over $[0,\infty)$ , closed at $0$ . The generating function $\beta$ takes complex arguments; real roots are written with the real-to-complex coercion. A stationary vector is a function q : ℕ → ℝ with $q_n \ge 0$ , HasSum q 1, and HasSum (fun i => q i * p i j) (q j) for every $j$ .

The explicit closed forms the statements carry are: the transition matrix (5.51); the equations (5.53); $\beta(z) = A^*[\mu(1-z)]$ (5.56); $\beta'(1) = \mu/\lambda$ ; $q_n = (1-r_0)r_0^n$ (5.60); $r_0/(1-r_0)$ and $r_0^2/(1-r_0)$ (5.61); $1 - r_0e^{-\mu(1-r_0)t}$ and $1 - e^{-\mu(1-r_0)t}$ (5.62); $r_0/(\mu(1-r_0))$ and $1/(\mu(1-r_0))$ (5.63). The waiting-time CDFs are defined as in §2.2.5 of the book: $W_q(t) = q_0 + \sum_{n\ge1} q_n \Pr\{n \text{ completions in} \le t\}$ with the Erlang type- $n$ CDF, and $W(t)$ likewise with $n+1$ completions. The means in (5.63) are $\int_0^\infty [1 - W_q(t)]\,dt$ and $\int_0^\infty [1 - W(t)]\,dt$ .

A trivializing formalization would take " $r_0 \in (0,1)$ solves $z = \beta(z)$ " as a hypothesis of the goal, which turns (5.60) into a geometric-series check; here existence, location and uniqueness of the root, and uniqueness of the stationary vector, are all conclusions.

Out of scope for this mission: the M/G/c and M/G/∞ results of §5.2 and the multiserver G/M/c analysis of §5.3.2. Reusable pieces include a Rouché-type or fixed-point counting lemma for power series with nonnegative coefficients summing to one, and the uniqueness of stationary laws for irreducible chains on $\mathbb N$ . Contributions of either kind are welcome.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.3.1, pp.259–263. https://doi.org/10.1002/9781118625651
D. G. Kendall, "Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain", Annals of Mathematical Statistics 24(3), 1953, 338–354. https://doi.org/10.1214/aoms/1177728975

12 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Fundamentals of Queueing Theory VI: The Pollaczek–Khintchine Transform for the M/G/1 QueueTextbook

Motivation

The M/G/1 queue is the single-server queue with Poisson arrivals and an arbitrary service-time distribution. It is the first queueing model beyond the birth–death family in which exact formulas survive. It is also the model a practitioner reaches for when service times are measured and visibly not exponential: repair times, transmission times of variable-length packets, machining times. Its central result is the Pollaczek–Khintchine formula, first obtained by Pollaczek (1930) and Khintchine (1932). It expresses the stationary queue in terms of the service distribution, and it shows that the mean wait grows linearly in the squared coefficient of variation of service. That makes variability, and not only load, a measurable driver of congestion.

The textbook treatment followed here is Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory, 4th ed. (Wiley 2008), §5.1. It derives the result through Kendall's (1953) imbedded Markov chain of system sizes at departure epochs. It then obtains the transforms of the waiting times and the busy-period functional equation of Takács (1962).

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$ . Service times $S$ are independent with distribution $B$ , a probability distribution on $[0,\infty)$ with mean $\mathrm E[S]$ , and the discipline is first-come first-served. The traffic intensity is $\rho = \lambda\,\mathrm E[S]$ .

Let $X_n$ be the number of customers the $n$ th departing customer leaves behind. The number of arrivals during one service time equals $i$ with probability

k_i = \int_0^\infty \frac{e^{-\lambda t}(\lambda t)^i}{i!}\,dB(t),

and $(X_n)$ is a Markov chain on $\{0,1,2,\dots\}$ whose transition matrix $P$ has first row $(k_0,k_1,k_2,\dots)$ and, for $i \ge 1$ , entries $p_{ij} = k_{j-i+1}$ for $j \ge i-1$ and $0$ otherwise. A stationary distribution is a probability vector $\pi$ with $\pi P = \pi$ . Its generating function is $\Pi(z) = \sum_i \pi_i z^i$ , and that of the arrivals per service is $K(z) = \sum_i k_i z^i$ , for complex $|z| \le 1$ . The Laplace–Stieltjes transform of a distribution $F$ on $[0,\infty)$ is $F^*(s) = \int_0^\infty e^{-st}\,dF(t)$ . In the Lean development these are arrivalProb, transitionMatrix, IsStationaryDist, pgf, utilization and lst in the namespace QueueingFundamentals.MG1.

Formalization targets

Goal: the Pollaczek–Khintchine transform formula (5.15)–(5.16)

If $\mathrm E[S] < \infty$ and $\rho < 1$ , the chain has a stationary distribution, and every stationary distribution satisfies $\pi_0 = 1-\rho$ and

\Pi(z) = \frac{(1-\rho)(1-z)K(z)}{K(z)-z}, \qquad |z| \le 1,\ z \ne 1,

with $K(z) \ne z$ at each such $z$ . It leaves the service distribution completely general.

Milestones

The stationary equations (5.12): $\pi_i = \pi_0 k_i + \sum_{j=1}^{i+1}\pi_j k_{i-j+1}$ .
The transform (5.14), $\Pi(z) = \pi_0(1-z)K(z)/(K(z)-z)$ , with $\pi_0$ free and no condition on $\rho$ .
Ergodicity (§5.1.4): a unique stationary distribution exists if and only if $\rho < 1$ .
The departure-point mean (5.7): $L^{(D)} = \rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$ .
$K(z) = B^*[\lambda(1-z)]$ (5.32).
The system-wait transform (5.29), (5.33): $\Pi(z) = W^*[\lambda(1-z)]$ and $W^*(s) = (1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$ .
The line-wait transform (5.34): $W_q^*(s) = (1-\rho)s/(s-\lambda[1-B^*(s)])$ .
The busy-period equation (5.37): $G^*(s) = B^*[s+\lambda-\lambda G^*(s)]$ .
The mean busy period: $\mathrm E[X] = 1/(\mu-\lambda)$ with $\mu = 1/\mathrm E[S]$ .

Significance

The transform formula determines the whole stationary departure-point distribution from the service distribution. Its derivatives at $z = 1$ give every moment of the system size, including the mean-value formula (5.7). Combined with the transform identity (5.32), it gives the waiting-time transforms (5.33)–(5.34). Those in turn give the classical geometric-series representation of the line-wait distribution through the residual service time. The busy-period equation is the starting point for busy-period moments and for the M/G/1 analysis of priority and vacation models later in the book.

All results here are classical and proved in the literature. As far as a search of the platform shows (2026-09-28), none is machine-checked: there is no M/G/1 queue, imbedded departure-point chain, Laplace–Stieltjes transform of a service distribution, or busy-period equation on Prove2Me. Mathlib has Poisson distributions and measure convolution but no generating-function theory for countable Markov chains, no Laplace–Stieltjes transform, and no identity theorem in the form these statements need. The mission produces a checked statement of the Pollaczek–Khintchine formulas that later queueing developments (vacations, priorities, M/G/1-type chains) can build on.

Difficulty

Turning the stationary equations into (5.14) is formal power-series algebra. The difficulties lie elsewhere. First, the formula must hold for complex $z$ on the closed disk, which needs the non-vanishing of $K(z)-z$ away from $z = 1$ . That fact fails for $\rho > 1$ , where $K$ has a fixed point inside the disk. Second, (5.15) evaluates $\pi_0$ from $\Pi(1) = 1$ by a limit at the point where the formula is $0/0$ , and this uses $K'(1) = \rho$ , an interchange of sum and integral. Third, the existence half of the goal requires positive recurrence of a chain with unbounded jumps. The book obtains it from Foster's criterion, which is not in Mathlib. Fourth, the waiting-time and busy-period transforms are stated for all real $s > 0$ , while the generating-function route reaches only $s = \lambda(1-z) \in (0, 2\lambda]$ . Extending the identity requires either analyticity arguments or a direct derivation. A formal proof of (5.14) alone does not touch any of these.

Formalization scope

The service distribution is a Measure ℝ with IsProbabilityMeasure B and B (Set.Iio 0) = 0; no density is assumed. The arrival rate is lam : ℝ with 0 < lam. Stationarity is IsStationaryDist P π: nonnegative entries, HasSum π 1, and HasSum (fun i => π i * P i j) (π j) for every j. That is global balance on ℕ, as the book writes it. Generating functions take a complex argument with ‖z‖ ≤ 1; transforms take a complex argument, and the waiting-time and busy-period statements use real s. The mean and variance of B are Bochner integrals, and every statement that uses them assumes Integrable. The mean busy period assumes 0 < E[S], so that $\mu = 1/\mathrm E[S]$ is the book's service rate.

Closed forms carried by the statements: $\pi_0 = 1-\rho$ (5.15); $(1-\rho)(1-z)K(z)/(K(z)-z)$ (5.16); $\pi_0(1-z)K(z)/(K(z)-z)$ (5.14); $\rho + (\rho^2+\lambda^2\sigma_B^2)/(2(1-\rho))$ (5.7); $B^*[\lambda(1-z)]$ (5.32); $(1-\rho)sB^*(s)/(s-\lambda[1-B^*(s)])$ (5.33); $(1-\rho)s/(s-\lambda[1-B^*(s)])$ (5.34); $B^*[s+\lambda-\lambda G^*(s)]$ (5.37); $1/(\mu-\lambda)$ for the mean busy period.

The waiting-time distribution $W$ enters through the book's FCFS relation $\pi_n = \frac1{n!}\int(\lambda t)^n e^{-\lambda t}\,dW(t)$ , and $W_q$ through $W = W_q * B$ ; both are hypotheses, as in the book. The busy-period distribution $G$ enters through the equation (5.36) in CDF form, with $n$ -fold convolutions built from Mathlib's Measure.conv.

The goal is not the algebraic consequence of (5.12) for an arbitrary sequence: $\pi$ must be a probability vector, $\pi_0$ is determined as $1-\rho$ , and the existence of a stationary distribution is part of the conclusion, so the statement cannot hold vacuously. The departure-point/time-average equality (§5.1.3, via PASTA) is not formalized.

Useful infrastructure, reusable beyond this mission: generating functions of stationary distributions on ℕ, Poisson mixtures, Laplace–Stieltjes transforms of measures on $[0,\infty)$ , and a Foster-type drift criterion for countable chains. Contributions proving any milestone, or those tools, are welcome.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §5.1. https://doi.org/10.1002/9781118625651
D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Annals of Mathematical Statistics 24 (1953) 338–354. https://doi.org/10.1214/aoms/1177728975
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953) 355–360. https://doi.org/10.1214/aoms/1177728976
L. Takács, Introduction to the Theory of Queues, Oxford University Press, 1962.
F. Pollaczek, Über eine Aufgabe der Wahrscheinlichkeitstheorie, Mathematische Zeitschrift 32 (1930) 64–100. https://doi.org/10.1007/BF01194620

12 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Fundamentals of Queueing Theory V: Closed Jackson Networks and the Mean-Value RecursionTextbook

Motivation

Networks of queues model systems in which a job visits several service stations in turn: jobs in a computer system alternating between CPU and disks, machines cycling between operation and repair, parts routed through a job shop. In a closed network no job enters or leaves; a fixed population of $N$ customers circulates among $k$ nodes. Closed networks are the standard model of multiprogrammed computer systems and of machine-repair and finite-source systems, and they are the setting of chapter 4 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, doi:10.1002/9781118625651).

The chapter's results form a short line of computational ideas:

Jackson (1957, 1963) showed that open networks of exponential servers with Markovian routing have a product-form steady state; Gordon and Newell (1967) gave the closed-network version, (4.15)–(4.18) of the book.
Buzen (1973) gave a convolution recursion for the normalizing constant $G(N)$ and for marginal distributions, (4.19)–(4.22).
Reiser and Lavenberg (1980) introduced mean-value analysis (MVA), which computes mean queue lengths, waiting times and throughputs population by population without ever forming $G(N)$ , (4.23)–(4.25); the book presents it following Bruell and Balbo (1980).
The book closes the section with a recursion for the full marginal distributions, (4.26), which it proves from the product form (pp.207–209).

This mission formalizes that line, ending at (4.26).

Setting

A closed Jackson network has nodes $i = 1, \dots, k$ , each with a single server whose service times are exponential with rate $\mu_i > 0$ . A customer finishing service at node $i$ moves to node $j$ with probability $r_{ij}$ ; the routing matrix $R = (r_{ij})$ has nonnegative entries and rows summing to one, and it is irreducible: every node can be reached from every other. The state is $\bar n = (n_1, \dots, n_k)$ , the number of customers at each node, with $n_1 + \cdots + n_k = N$ ; this state space is finite.

The steady-state distribution $p_{\bar n}$ is the probability vector on the state space that solves the flow-balance equations (4.14),

\sum_{j=1}^{k}\sum_{\substack{i=1\\ i\ne j}}^{k} \mu_i r_{ij}\, p_{\bar n;i^+j^-} = \sum_{i=1}^{k}\mu_i(1-r_{ii})\,p_{\bar n},

where $\bar n;i^+j^-$ has one more customer at $i$ and one fewer at $j$ , and terms with a negative subscript or with $\mu_i$ at an empty node vanish. The traffic equations (4.16) are $\mu_i\rho_i = \sum_j \mu_j r_{ji}\rho_j$ ; they determine $\rho = (\rho_1, \dots, \rho_k)$ up to a positive factor. The normalizing constant is

G(N) = \sum_{n_1+\cdots+n_k=N}\rho_1^{n_1}\cdots\rho_k^{n_k},

and more generally, with $f_i(n) = \rho_i^{\,n}/a_i(n)$ for $c_i$ -server nodes ((4.13)), $G(N) = \sum \prod_i f_i(n_i)$ and Buzen's function $g_m(n) = \sum_{n_1+\cdots+n_m=n}\prod_{i\le m} f_i(n_i)$ .

For each population $N$ write $p_i(n, N) = \Pr\{N_i = n\}$ for the marginal distribution at node $i$ , $\bar P_i(n; N) = \Pr\{N_i \ge n\}$ , $L_i(N)$ for the mean number at node $i$ , and

\lambda_i(N) = \Pr\{\text{server busy at node } i\}\cdot\mu_i

for the throughput of node $i$ .

Formalization targets

Goal: the marginal recursion (4.26)

For every node $i$ ,

p_i(0,0) = 1, \qquad p_i(n, N) = \frac{\lambda_i(N)}{\mu_i}\,p_i(n-1, N-1) \quad (n, N \ge 1).

It involves only the steady-state distributions and quantities computed from them; it holds for every irreducible routing matrix and every choice of rates.

Milestones

Product form (4.14)–(4.16). For any positive solution $\rho$ of (4.16), a probability distribution solves (4.14) if and only if $p_{\bar n} = G(N)^{-1}\rho_1^{n_1}\cdots\rho_k^{n_k}$ .
Buzen's algorithm (4.19)–(4.21). $G(N) = g_k(N)$ , $g_m(n) = \sum_{i=0}^{n} f_m(i)\,g_{m-1}(n-i)$ , $g_1 = f_1$ , $g_m(0) = 1$ .
Marginal at the last node (4.22). $p_k(n) = f_k(n)\,g_{k-1}(N-n)/G(N)$ for $0 \le n \le N$ .
Complementary marginal (p.208). $\bar P_i(n_i; N) = \rho_i^{\,n_i}G(N-n_i)/G(N)$ .
Mean-value analysis (4.23)–(4.25). $L_i(0) = 0$ ; $L_i(N) = \lambda_i(N)W_i(N)$ with $W_i(N) = (1 + L_i(N-1))/\mu_i$ ; and for $v$ solving $v_i = \sum_j v_j r_{ji}$ with $v_l = 1$ , $\lambda_l(N) = N/\sum_i v_iW_i(N)$ and $\lambda_i(N) = \lambda_l(N)v_i$ .

Significance

The product form reduces a $\binom{N+k-1}{N}$ -state Markov chain to the constants $G(0), \dots, G(N)$ , and Buzen's recursion computes them in $O(kN^2)$ operations. Mean-value analysis goes further and avoids $G(N)$ , whose magnitude can overflow or underflow for large populations; it is the method used in capacity planning of computer systems. The recursion (4.26) extends MVA from means to full marginal distributions, so a single pass over $N$ yields every nodal distribution.

All of these results are classical and proved in the literature; the book proves (4.26) itself. What the mission adds is a machine-checked development of them from the global balance equations: the product form with its uniqueness, the convolution identities, the marginal formulas, and the correctness of the MVA iteration as stated by the book, all over one shared definition layer. A search of the platform on 2026-09-28 found no formal statement of Buzen's algorithm or of MVA. The platform has Kelly's closed migration process theorem (KellyStochasticNetworks.closed_migration_equilibrium), which shows that the unnormalized product form satisfies the equilibrium equations under Kelly's conventions; the normalization, uniqueness and everything downstream of the product form are new here.

Difficulty

The combinatorial identities (Buzen's recursion, the tail marginal) are reindexings of finite sums over compositions of $N$ ; in Lean the work is in bijections between the state spaces $\{n_1+\cdots+n_k = N\}$ for different $k$ and $N$ . The substantive step is uniqueness in the product-form theorem: the global balance equations have a one-dimensional solution space only because the chain on the $N$ -customer states is irreducible on the population level, which is a property of the network chain and not of the routing matrix alone. The goal and MVA also need a positive solution of the traffic equations, which is not among the hypotheses and has to come from irreducibility of $R$ . The book's own intuitive derivation of MVA via the arrival theorem is not the route the statements require; they are stated in terms of the steady-state distributions alone.

Formalization scope

Nodes are Fin k (book node $i$ is index $i-1$ ); states are n : Fin k → ℕ with ∑ i, n i = N, collected in a Finset, and all sums are finite. A distribution is a real function on $\mathbb N^k$ that is nonnegative, vanishes off the $N$ -customer states and sums to one there. The balance equations are (4.14) verbatim with the book's boundary convention (p.188), not detailed balance. All results except Buzen's algorithm and (4.22) are for single-server nodes, as in the book; (4.13)'s multiserver factor $a_i(n)$ enters only (4.19)–(4.22).

Closed forms instantiated in the statements: the product form $G(N)^{-1}\prod_i\rho_i^{n_i}$ ((4.15)); $G(N)$ as the explicit sum (4.18)/(4.19); $a_i(n)$ from (4.13); $g_m$ from (4.20); $p_k(n) = f_k(n)g_{k-1}(N-n)/G(N)$ ((4.22)); $\bar P_i(n;N) = \rho_i^nG(N-n)/G(N)$ (p.208); $W_i(N) = (1+L_i(N-1))/\mu_i$ ((4.23)); $\lambda_l(N) = N/\sum_i v_iW_i(N)$ (MVA step (iii)(b)).

Two trivializing formalizations are ruled out: $\lambda_i(N)$ in (4.26) and (4.24) is the throughput computed from the steady-state distribution, not a free constant (which would make (4.26) a definition); and $g_m$ is defined by the sum (4.20), so the recursion (4.21) is a theorem rather than rfl. The product-form statement is an equivalence, so it asserts both that the product form is a steady state and that it is the only one.

Needed infrastructure: bijections between compositions of $N$ into $k$ and $k-1$ parts, uniqueness of stationary distributions of irreducible finite continuous-time chains (stated directly via the balance equations), and existence of positive solutions of $v = vR$ for irreducible stochastic $R$ . The last two are reusable beyond this mission. Contributions welcome: proofs of the milestones in any order, and helper lemmas on these three points.

Not formalized: open Jackson networks (4.11) and Burke's theorem (4.5)–(4.6), multiclass networks (§4.2.1), the multiserver recursion (4.27) and cyclic queues (§4.4).

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §4.3, pp.195–209. https://doi.org/10.1002/9781118625651
J. R. Jackson, "Jobshop-like queueing systems", Management Science 10(1), 1963. https://doi.org/10.1287/mnsc.10.1.131
W. J. Gordon, G. F. Newell, "Closed queuing systems with exponential servers", Operations Research 15(2), 1967. https://doi.org/10.1287/opre.15.2.254
J. P. Buzen, "Computational algorithms for closed queueing networks with exponential servers", Communications of the ACM 16(9), 1973. https://doi.org/10.1145/362342.362345
M. Reiser, S. S. Lavenberg, "Mean-value analysis of closed multichain queuing networks", Journal of the ACM 27(2), 1980. https://doi.org/10.1145/322186.322195
S. C. Bruell, G. Balbo, Computational Algorithms for Closed Queueing Networks, North-Holland, 1980.

7 thms3 active usersReviewed

Completed

Markov Chain Operations Research Probability+1·Captain: mikedeng1

Fundamentals of Queueing Theory IV: The Stationary Distribution of the M/M/1 Retrial QueueTextbook

Motivation

In many service systems a customer who finds every server busy does not join a queue. A caller who hears a busy signal hangs up and redials later; a request rejected by a saturated server is resent after a timeout; an aircraft that cannot land circles and tries again. These retrial queues are the subject of a substantial literature in telephone traffic engineering, computer networks and call-centre design, surveyed in the monograph of Falin and Templeton (1997) and the bibliography of Artalejo (1999). Their analysis is harder than that of ordinary queues: the blocked customers form an orbit whose size is part of the state, so even the simplest model is a two-dimensional Markov chain, and explicit stationary distributions are rare.

This mission is the fourth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008). Its goal is the explicit stationary distribution of the single-server retrial queue, Eq. (3.57) of §3.5.1, one of the few retrial models solvable in closed form. Chapter 3 of the book treats Markovian queues that are not birth–death processes: bulk arrivals, bulk service, Erlang phases, priority disciplines and retrials. The milestones also collect three capstone formulas from the chapter's other sections: the bulk-input queue, the partial-batch bulk-service queue, and Cobham's formula for nonpreemptive priorities (Cobham, 1954).

Setting

In the $M/M/1$ retrial queue customers arrive according to a Poisson process with rate $\lambda$ and are served one at a time by a single server, with exponential service times of mean $1/\mu$ . An arrival that finds the server busy enters the orbit and stays there for an exponential time with mean $1/\gamma$ , after which it tries again; each customer in orbit retries independently. No customer leaves because of impatience. With $N_s(t) \in \{0,1\}$ the number in service and $N_o(t)$ the number in orbit, the pair is a continuous-time Markov chain on states $\{i, n\}$ , $i \in \{0,1\}$ , $n \in \{0,1,2,\dots\}$ . Writing $p_{i,n}$ for the steady-state probability of $\{i,n\}$ , the rate-balance equations are

\begin{aligned} (\lambda + n\gamma)p_{0,n} &= \mu p_{1,n}, && n \ge 0, && (3.47)\\ (\lambda+\mu)p_{1,n} &= \lambda p_{0,n} + (n+1)\gamma p_{0,n+1} + \lambda p_{1,n-1}, && n \ge 1, && (3.48)\\ (\lambda+\mu)p_{1,0} &= \lambda p_{0,0} + \gamma p_{0,1}. && && (3.49) \end{aligned}

Following the book's convention (§1.9, and the footnote on p.118), a steady-state solution is a nonnegative solution of these equations whose total mass $\sum_n (p_{0,n} + p_{1,n})$ equals $1$ . The traffic intensity is $\rho = \lambda/\mu$ , and the partial generating functions are $P_0(z) = \sum_n z^n p_{0,n}$ and $P_1(z) = \sum_n z^n p_{1,n}$ .

The other models of the mission use the same convention. In the bulk-input queue $M^{[X]}/M/1$ , batches arrive at rate $\lambda$ with batch-size probabilities $c_n = \Pr\{X = n\}$ , $n \ge 1$ , and batch-size generating function $C(z) = \sum_n c_n z^n$ . In the partial-batch bulk-service queue $M/M^{[K]}/1$ , single arrivals come at rate $\lambda$ and the server serves up to $K$ customers together in an exponential time of mean $1/\mu$ . In the nonpreemptive priority queue there are $r$ classes with rates $\lambda_k$ and $\mu_k$ , loads $\rho_k = \lambda_k/\mu_k$ and cumulative loads $\sigma_k = \rho_1 + \cdots + \rho_k$ .

Formalization targets

Goal: the stationary distribution (3.57)

For $\lambda, \mu, \gamma > 0$ and $\rho < 1$ , the numbers

p_{0,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^n}{n!\,\gamma^n}\prod_{i=0}^{n-1}(\lambda+i\gamma), \qquad p_{1,n} = (1-\rho)^{(\lambda/\gamma)+1}\frac{\rho^{n+1}}{n!\,\gamma^n}\prod_{i=1}^{n}(\lambda+i\gamma)

form a steady-state solution of (3.47)–(3.49), and every steady-state solution equals them.

Milestones on the retrial queue

The generating functions satisfy (3.50)–(3.52) on $(-1,1)$ , including the separable equation

P_0'(z) = \frac{\lambda\rho}{\gamma(1-\rho z)}P_0(z),

their closed form is (3.55),

P_0(z) = (1-\rho z)\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1}, \qquad P_1(z) = \rho\left(\frac{1-\rho}{1-\rho z}\right)^{(\lambda/\gamma)+1},

and the mean orbit size is (3.58), $L_o = \frac{\rho^2}{1-\rho}\cdot\frac{\mu+\gamma}{\gamma}$ .

Milestones from the rest of Chapter 3

The bulk-input generating function (3.3), $p_0 = 1 - \rho$ with $\rho = \lambda\mathrm E[X]/\mu$ , and the mean (3.4); the unique root $r_0 \in (0,1)$ of $\mu r^{K+1} - (\lambda+\mu)r + \lambda = 0$ and the geometric law $p_n = (1-r_0)r_0^n$ (3.9); and Cobham's formula (3.41)/(3.43), the unique solution of the linear system (3.40).

Significance

The closed form (3.57) makes every performance measure of the $M/M/1$ retrial queue explicit. The server is busy a fraction $\rho$ of the time, exactly as without retrials. The mean orbit size (3.58) is the $M/M/1$ mean queue length multiplied by $(\mu+\gamma)/\gamma$ , and the mean time in orbit (3.59) follows from Little's law. These formulas quantify the cost of retrials against an ordinary queue and are the reference case against which approximations for multi-server retrial systems are checked.

The results are classical and proved in the book, partly through exercises (Problems 3.39–3.41). None of them is formalized in any proof assistant, as far as the platform's catalogue shows: there is no retrial, bulk or priority queue on Prove2Me. The mission produces machine-checked statements and, once solved, proofs of the chapter's main closed forms. It also produces a small reusable layer: generating functions of probability sequences on the closed unit disc, and the "probability solution of the balance equations" pattern for chains with countable state spaces.

Difficulty

The derivation in the book is formal. It differentiates power series term by term, divides by $1 - z$ , integrates $\ln P_0$ , and fixes the constant by setting $z = 1$ , without justifying any of these steps. A formal proof has to show that the series converge and are differentiable on $(-1,1)$ , that the differential equation determines $P_0$ up to a constant, and that the values at $z = 1$ are the limits of the values inside the disc (Abel's theorem). The uniqueness half of the goal is the hardest part. The book never proves it; it follows from the ODE argument only once every step is shown to hold for an arbitrary probability solution. Verifying that (3.57) solves (3.47)–(3.49) is only the easy half. The same pattern recurs in the bulk-input queue, where $z = 1$ is a removable singularity of (3.3). In the bulk-service queue the root $r_0$ is only characterized as the unique root in $(0,1)$ , so existence and uniqueness of the root are part of the claim.

Formalization scope

A steady-state solution is a pair p0 p1 : ℕ → ℝ (resp. one sequence p : ℕ → ℝ) that is pointwise nonnegative, has total mass $1$ as a HasSum, and solves the book's balance equations exactly as printed, global balance and not detailed balance. Every "the steady-state solution is X" is stated with both halves: X is a steady-state solution, and every steady-state solution equals X. Stating only that (3.57) solves (3.47)–(3.49), without normalization or uniqueness, would be a trivializing formalization. So would taking $r_0$ as a given root in (3.9), or taking the $W_q^{(i)}$ in (3.41) as numbers assumed to satisfy it. None of these is used. The closed forms instantiated are (3.52), (3.55), (3.57), (3.58), (3.3), (3.4), (3.9), (3.41) and (3.43), each written out in full, with the real power $(1-\rho)^{(\lambda/\gamma)+1}$ as Real.rpow.

The conventions are as follows. The retrial generating functions take real arguments, on $(-1,1)$ for the differential equations and on $[-1,1]$ for the closed form. The bulk-input generating function takes complex arguments with $|z| \le 1$ , $z \ne 1$ , because (3.3) is $0/0$ at $z = 1$ . The condition $\rho < 1$ is a hypothesis of every retrial statement. For the bulk-service queue the book's unnamed condition is stated as $\lambda < K\mu$ . For bulk input, $\mathrm E[X] < \infty$ is assumed throughout, and the mean (3.4) is asserted under the further condition $\mathrm E[X^2] < \infty$ , which it requires. For Cobham's formula only the algebraic content is formalized; the mean-value argument that yields (3.40) and (3.42) is not.

Needed infrastructure: power series of summable nonnegative sequences on the closed unit disc (convergence, term-by-term differentiation, Abel continuity), the binomial series $(1 - x)^{-a} = \sum_n \frac{a(a+1)\cdots(a+n-1)}{n!}x^n$ for real $a$ , and uniqueness of invariant probability vectors for irreducible chains. All of this is reusable beyond the mission. Proofs of any milestone, of the easy half of the goal, or of the needed series facts are welcome contributions.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§3.1, 3.2.0.1, 3.4.2, 3.5.1. https://doi.org/10.1002/9781118625651
G. I. Falin, J. G. C. Templeton, Retrial Queues, Chapman & Hall, 1997. https://doi.org/10.1007/978-1-4899-2977-8
J. R. Artalejo, Accessible bibliography on retrial queues, Mathematical and Computer Modelling 30 (1999) 1–6. https://doi.org/10.1016/S0895-7177(99)00128-4
A. Cobham, Priority assignment in waiting line problems, Journal of the Operations Research Society of America 2 (1954) 70–76. https://doi.org/10.1287/opre.2.1.70

10 thms3 active usersReviewed

Completed

Analysis Markov Chain Operations Research+2·Captain: mikedeng1

Fundamentals of Queueing Theory III: The Transient M/M/1 Queue via Modified Bessel FunctionsTextbook

Motivation

Steady-state formulas describe a queue that has been running forever. Many practical questions are about a queue that has not: a call centre just after opening, a server just after a reset, a system under a burst of load. For these, the relevant quantity is the transient distribution $p_n(t) = \Pr\{N(t) = n\}$ of the number $N(t)$ in the system at a finite time $t$ . It is also what determines how fast the steady state is approached, and it is needed for the busy period: the length of time a server stays busy once a customer arrives at an idle server.

For the single-server Markovian queue M/M/1 the transient distribution has an explicit closed form in modified Bessel functions. Its history is short and well documented. Ledermann and Reuter (1954) obtained it by spectral analysis of the birth–death process. Bailey (1954) found it by generating functions and Laplace transforms, and Champernowne (1956) by combinatorial methods. Bailey's route is the standard textbook derivation, and it is the one Gross, Shortle, Thompson and Harris outline in §2.11 of Fundamentals of Queueing Theory (4th ed., 2008). Abate and Whitt (1989) showed that computing with the resulting series is numerically delicate, which is one reason for having the formula pinned down exactly.

This mission formalizes §§2.11–2.12 of that book: the transient laws of M/M/1/1, M/M/1 and M/M/∞, and the M/M/1 busy period.

Setting

Customers arrive in a Poisson stream of rate $\lambda > 0$ . Each service takes an exponential time of rate $\mu > 0$ , and $\rho = \lambda/\mu$ . The number in the system is a continuous-time Markov chain on $\{0, 1, 2, \dots\}$ , and its state probabilities $p_n(t)$ satisfy the forward (differential–difference) equations. For M/M/1 started with $N(0) = i$ they are, for $t \ge 0$ ,

p_n'(t) = -(\lambda+\mu)p_n(t) + \lambda p_{n-1}(t) + \mu p_{n+1}(t)\ (n > 0), \qquad p_0'(t) = -\lambda p_0(t) + \mu p_1(t), \tag{2.72}

with $p_n(0) = 1$ if $n = i$ and $0$ otherwise. The other systems are variants:

M/M/1/1, no waiting room: two states and equations (2.70).
M/M/∞, ample service: the death rate in state $n$ is $n\mu$ , giving (2.76).
The busy-period system: (2.72) with $0$ made absorbing ( $\lambda_0 = 0$ ) and $N(0) = 1$ . Its $p_0(t)$ is the distribution function of the busy period $T_{bp}$ .

A family $(p_n)$ solves a system on $[0,\infty)$ when each $p_n$ has, at every $t \ge 0$ , the prescribed derivative (a right derivative at $t = 0$ ). It is a probability solution when $p_n(t) \ge 0$ and $\sum_n p_n(t) = 1$ for every $t \ge 0$ . The modified Bessel function of the first kind is

I_n(y) = \sum_{k=0}^{\infty} \frac{(y/2)^{n+2k}}{k!\,(n+k)!}, \qquad I_{-n} = I_n,

and the Laplace transform of $f$ is $\bar f(s) = \int_0^\infty e^{-st} f(t)\,dt$ for $\operatorname{Re} s > 0$ .

Formalization targets

Goal: the transient M/M/1 law, (2.75)

With $y = 2t\sqrt{\lambda\mu}$ ,

p_n(t) = e^{-(\lambda+\mu)t}\Big[\rho^{(n-i)/2} I_{n-i}(y) + \rho^{(n-i-1)/2} I_{n+i+1}(y) + (1-\rho)\rho^n \sum_{j=n+i+2}^{\infty} \rho^{-j/2} I_j(y)\Big].

The goal asserts five things for every $\lambda, \mu > 0$ and every $i$ , with no restriction on $\rho$ :

the series converges;
these functions solve (2.72);
they meet the initial condition;
they form a probability distribution at every $t$ ;
they are the only probability solution.

Milestones

(2.71): the M/M/1/1 solution $p_1(t) = \frac{\lambda}{\lambda+\mu}(1-e^{-(\lambda+\mu)t}) + p_1(0)e^{-(\lambda+\mu)t}$ , and the matching formula for $p_0$ .
(2.74) and Rouché's theorem: for $\operatorname{Re} s > 0$ , the quadratic $(\lambda+\mu+s)z - \mu - \lambda z^2$ has exactly one zero in $|z| < 1$ , namely $z_1 = (\lambda+\mu+s-\sqrt{(\lambda+\mu+s)^2-4\lambda\mu})/(2\lambda)$ .
The transform of $p_0$ : $\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$ .
The limit of (2.75): $p_n(t) \to (1-\rho)\rho^n$ if $\rho < 1$ , and $p_n(t) \to 0$ if $\rho \ge 1$ .
(2.77), M/M/∞: started empty, $p_n(t) = a(t)^n e^{-a(t)}/n!$ with $a(t) = (1-e^{-\mu t})\lambda/\mu$ . The statement says that this family solves (2.76), is the unique probability solution, and has generating function $\exp((z-1)a(t))$ .
The busy-period transform: $\bar p_0(s) = 2\mu/(s[\lambda+\mu+s+\sqrt{(\lambda+\mu+s)^2-4\lambda\mu}])$ .
The busy-period density: $p_0'(t) = \sqrt{\mu/\lambda}\,e^{-(\lambda+\mu)t} I_1(2\sqrt{\lambda\mu}\,t)/t$ .
(2.79): for $\lambda < \mu$ , $E[T_{bp}] = 1/(\mu-\lambda)$ and $E[T_{bc}] = 1/\lambda + 1/(\mu-\lambda)$ .

Significance

The formula (2.75) is the exact finite-time law of the most basic queue. It gives the rate at which M/M/1 approaches equilibrium, and it gives the distribution of the queue under overload ( $\rho \ge 1$ ), where no steady state exists. It is the reference against which numerical transient methods, such as the uniformization of Chapter 8 of the same book, are checked. The busy-period density and its mean (2.79) enter server-utilisation and vacation models, and the Laplace-transform method used here recurs in the M/G/1 analysis of Chapter 5.

All of these results are classical and proved in the literature. None of them is machine-checked, as far as the platform's catalogue and Mathlib show. The chain from a countable system of linear ODEs, through generating functions and a root-location argument, to a Bessel series is a standard pattern in applied probability, and a formal version of it is what this mission adds. The formal statements also make explicit what the book leaves implicit: the sense in which the equations hold at $t = 0$ , and the class in which the solution is unique.

Difficulty

The forward equations (2.72) form an infinite linear system. The obvious approach is to treat it like a finite system of ODEs, whose solution is a matrix exponential, and read off (2.75). That fails for two reasons. The generator is an infinite matrix, so its exponential needs a functional-analytic setting. And uniqueness is not automatic for infinite systems: it needs a class, such as probability solutions, and an argument that works in that class.

The Bessel form is a second, independent difficulty. The transform $\bar p_0(s)$ is fixed by a root-location argument in the complex plane. Inverting the transform, or verifying (2.75) directly, requires manipulating the three-term Bessel recurrence and exchanging infinite sums. The tail sum $\sum_{j} \rho^{-j/2} I_j$ has to be controlled uniformly enough to be differentiated term by term. For $\rho \ge 1$ the factor $(1-\rho)$ is non-positive, so the nonnegativity of $p_n(t)$ is not visible from the formula.

Formalization scope

Conventions committed to:

Parameters. Rates are real with $\lambda, \mu > 0$ , and $\rho = \lambda/\mu$ . States are ℕ (Fin 2 for M/M/1/1).
Solutions. "Solves on $[0,\infty)$ " is HasDerivWithinAt on Set.Ici 0 at every $t \ge 0$ . Uniqueness is asserted among solutions that are probability distributions at every time.
Special functions. Half-integer powers of $\rho$ are real powers, and $I_{-m} = I_m$ is part of the definition. Laplace transforms are complex Bochner integrals over $(0,\infty)$ , and each statement also asserts the integrability it needs. Square roots with positive real part are hypotheses $r^2 = (\lambda+\mu+s)^2 - 4\lambda\mu$ , $\operatorname{Re} r > 0$ .

The closed forms stated exactly as in the book are:

(2.71);
$z_1$ and $z_2$ of (2.74);
$\bar p_0(s) = z_1^{i+1}/(\mu(1-z_1))$ ;
(2.75), with the Bessel series of p.101;
the M/M/∞ law and (2.77);
the busy-period transform and density of p.102;
(2.79).

The book derives (2.79) by a steady-state ratio argument valid for M/G/1. Here it is stated for M/M/1, as the mean of the explicit density.

A statement of (2.75) that only asserts the right-hand side is well defined, or checks only $n = 0$ , is ruled out: the goal requires the ODE system, the initial condition, the probability property and uniqueness. For the same reason, the M/M/∞ law is tied to the system (2.76) and does not reduce to a Taylor expansion.

Needed infrastructure that Mathlib lacks:

modified Bessel functions of integer order;
Laplace transforms;
a Rouché-type zero count or a direct root-location lemma;
uniqueness for countable linear ODE systems with bounded or linearly growing rates.

The Bessel and Laplace definitions, and the uniqueness lemma for birth–death forward equations, are reusable beyond this mission. Contributions of those as separate lemmas are welcome.

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§2.11–2.12, pp.97–103. https://doi.org/10.1002/9781118625651
N. T. J. Bailey, "A continuous time treatment of a simple queue using generating functions", J. Royal Statistical Society B 16 (1954) 288–291. https://doi.org/10.1111/j.2517-6161.1954.tb00172.x
W. Ledermann, G. E. H. Reuter, "Spectral theory for the differential equations of simple birth and death processes", Phil. Trans. Royal Society A 246 (1954) 321–369. https://doi.org/10.1098/rsta.1954.0001
D. G. Champernowne, "An elementary method of solution of the queueing problem with a single server and constant parameters", J. Royal Statistical Society B 18 (1956) 125–128. https://doi.org/10.1111/j.2517-6161.1956.tb00217.x
J. Abate, W. Whitt, "Calculating time-dependent performance measures for the M/M/1 queue", IEEE Trans. Communications 37 (1989) 1102–1104. https://doi.org/10.1109/26.41165

15 thms3 active usersReviewed