All missions

Motivation

Belief propagation (BP) is the message-passing algorithm used throughout artificial intelligence, coding theory and statistical physics to approximate marginals of graphical models. On graphs with cycles it is a heuristic: it may fail to converge, and when it converges its output need not be the true marginal. Rigorous guarantees had mostly been confined to the high-temperature regime, as a consequence of a uniform decay of correlations (spatial mixing) under which any boundary condition is forgotten; see the works cited as [3, 23, 26] in §1 of the paper.

Dembo and Montanari (arXiv:0804.4726v3, Ann. Appl. Probab. 20 (2010)) proved that for the ferromagnetic Ising model with a positive external field, BP converges exponentially fast on every graph of bounded degree, at every temperature, and that on locally tree-like graphs its fixed point computes local marginals accurately. The low-temperature regime, where the Gibbs measure on the limiting infinite tree is not unique, is the point: the field breaks the $\pm$ symmetry, and monotonicity replaces spatial mixing.

Setting

Let $G=(V,E)$ be a finite graph in which every vertex has at most $\Delta$ neighbours, $\beta\ge0$ an inverse temperature and $B$ a magnetic field. The Ising model on $G$ is the distribution on spin configurations $\underline x\in\{+1,-1\}^V$

$$\mu(\underline x)=\frac1{Z(\beta,B)}\exp\Big\{\beta\sum_{(i,j)\in E}x_ix_j+B\sum_{i\in V}x_i\Big\}.$$

More generally one allows a field $B_i$ at each vertex, and $B_i=+\infty$ (a vertex pinned to $+1$).

A message $\nu_{i\to j}$ is a distribution on $x_i\in\{+1,-1\}$ attached to the directed edge $i\to j$. The BP iteration is

$$\nu^{(t+1)}_{i\to j}(x_i)=\frac1{z^{(t)}_{i\to j}}\,e^{Bx_i}\prod_{l\in\partial i\setminus j}\ \sum_{x_l}e^{\beta x_ix_l}\,\nu^{(t)}_{l\to i}(x_l),$$

with $\partial i$ the neighbours of $i$ and $z^{(t)}_{i\to j}$ a normalization. An initial condition is positive if $\nu^{(0)}_{i\to j}(+1)\ge\nu^{(0)}_{i\to j}(-1)$ on every directed edge. Distances between distributions are in total variation, $\|p-q\|_{\mathrm{TV}}=\tfrac12\sum_x|p(x)-q(x)|$.

For $i_*\in V$, $U=\mathsf B_{i_*}(r)$ is the ball of radius $r$, $\partial U$ its vertices at distance exactly $r$, and $j(i)$ a neighbour in $U$ of each $i\in\partial U$. Given a BP fixed point $\nu^*$, the BP estimate of the marginal on $U$ is

$$\nu_U(\underline x_U)=\frac1{z_U}\exp\Big\{\beta\sum_{(i,j)\in E_U}x_ix_j+B\sum_{i\in U\setminus\partial U}x_i\Big\}\prod_{i\in\partial U}\nu^*_{i\to j(i)}(x_i).$$

The proofs run through Ising models on rooted trees $\mathsf T$: $\mathsf T(\ell)$ is the tree of the first $\ell$ generations, $\partial\mathsf T(\ell)$ the $\ell$-th generation, and $\mu^{\ell,0}$, $\mu^{\ell,+}$ the Ising models on $\mathsf T(\ell)$ with free and plus boundary conditions (the latter pins $\partial\mathsf T(\ell)$ to $+1$). A random tree is conditionally independent with average offspring bounded by $\Delta$ if, given the first $k$ generations, the offspring numbers of generation $k$ are independent with conditional means at most $\Delta$ (Definition 2.5).

Formalization targets

Goal: Theorem 2.6

For $\beta\ge0$, $B>0$ and $\Delta$, there are $A<\infty$ and $\lambda>0$ depending only on $(\beta,B,\Delta)$ such that every finite graph of maximal degree $\Delta$ has a BP fixed point $\nu^*$ with

$$\sup_{(i,j)\in E}\big\|\nu^{(t)}_{i\to j}-\nu^*_{i\to j}\big\|_{\mathrm{TV}}\le A\exp(-\lambda t)$$

for every positive initial condition and every $t\ge0$. The constants are uniform over graphs; this uniformity is the content of the theorem.

Companion: Theorem 2.7

With $c=c(\beta,B,\Delta)$ and $\lambda>0$: if $\mathsf B_{i_*}(t)$ is a tree, then $\|\mu_U-\nu_U\|_{\mathrm{TV}}\le\exp\{c^{r+1}-\lambda(t-r)\}$.

Milestones

The tree estimates of §3–§4, in the order the proofs use them: Griffiths' inequality (Theorem 3.1); the GHS inequality (Theorem 3.2); the reweighting bound in total variation (Lemma 3.3); marginals on subtrees (Lemma 4.1); the $M/\ell$ bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le M/\ell$ on root magnetizations (Lemma 4.3); its extension to marginals near the root (Theorem 4.2); a Simon-type factorization of tree correlations (Lemma 4.4); and Corollary 4.5: exponential decay of correlations (4.13), Theorem 4.2 with rate $Ae^{-\lambda t}$, and the root-magnetization bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le Ae^{-\lambda\ell}$.

Significance

The theorem gives an unconditional convergence guarantee for BP on a nontrivial class of models with cycles, valid deep in the low-temperature phase, with a rate independent of the number of vertices. Theorem 2.7 adds that the fixed point is accurate on locally tree-like graphs such as random regular graphs and sparse Erdős–Rényi graphs, so BP is a polynomial-time algorithm for local marginals there. The tree estimates of §4, in particular the insensitivity of the root to plus versus free boundary conditions on conditionally independent trees, are also the engine of the free-entropy theorem of the same paper (mission 1 of this series).

The results are proved in the paper; none of them, nor Griffiths' or the GHS inequality, has a machine-checked proof known to this mission. Formalizing them produces a reusable library for ferromagnetic Ising models on finite graphs and trees (correlation inequalities, pinned boundary conditions, marginals on subtrees) and a formal account of BP as an operator on message families.

Difficulty

The obvious argument is a contraction: show that one BP step shrinks the distance between message families, uniformly over the graph. At low temperature this fails: the BP map is not a contraction, the infinite-tree Ising model has several Gibbs measures, and without a field BP has several fixed points. Uniform decay of correlations, the tool behind high-temperature results, is false in this regime. What has to be controlled instead is a single, weaker quantity: how much the root of a tree of depth $t$ feels a plus boundary condition compared with a free one, with a bound that is uniform over all trees of bounded average offspring and over all depths. The difficulty is concentrated in that estimate (Lemma 4.3), and in upgrading its $1/\ell$ rate to an exponential one (Corollary 4.5), which is where the positive field enters quantitatively.

Formalization scope

Spins are Booleans (true $=+1$); the edge sum counts each unordered edge once; a field $+\infty$ is a pinned vertex, never a large real number. Graphs are finite (Fintype V) with all degrees at most $\Delta$. Messages are functions on ordered vertex pairs whose values on directed edges are distributions on $\{+1,-1\}$; the BP iterates are computed from the update, not posited. Total variation is $\tfrac12\ell^1$. Trees are encoded by offspring functions on finite words (Ulam–Harris), random trees by probability measures on offspring functions with the product $\sigma$-algebra; conditional independence uses Mathlib's iCondIndepFun, with integrable offspring numbers. Fields on trees are nonrandom functions of the vertex. Expectations that may be infinite, such as $\mathbb E\{C^{|\mathsf T(r)|}\}$, are lower Lebesgue integrals in $[0,\infty]$, and every expectation of a tree functional comes with a measurability conclusion, so that no integral can take a junk value. Constants are quantified before the graph, the tree law and the field, and, where the paper names their dependence (Theorem 4.2's $M(\beta_{\max},B_{\min},\Delta)$ and $C(\beta_{\max},B_{\max})$), as functions of exactly those parameters.

Two readings are fixed explicitly. Theorem 2.7 is stated for every positive BP fixed point, which by Theorem 2.6 is the paper's fixed point. Corollary 4.5's clause (4.13) carries the hypotheses of Theorem 4.2 ($B_i\le B_{\max}$ on $\mathsf T(r-1)$). A fixed point that is not a family of distributions, a "zero message" family, or a bound that holds only because an integral defaults to $0$ does not satisfy these statements.

The computation tree of §5, through which the paper derives Theorems 2.6–2.7 from Corollary 4.5, is a proof device and is not part of any statement; building it is welcome as supporting work. Proofs of the classical inequalities (Griffiths, GHS) are independently reusable.

Selected references

• A. Dembo, A. Montanari, Ising models on locally tree-like graphs, Ann. Appl. Probab. 20(2) (2010) 565–592. arXiv:0804.4726v3, doi:10.1214/09-AAP627
• R. B. Griffiths, C. A. Hurst, S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970) 790–795. MR0266507
• T. M. Liggett, Interacting Particle Systems, Grundlehren 276, Springer, 1985 (Theorem IV.1.21, Griffiths' inequality). MR776231
• B. Simon, Correlation inequalities and the decay of correlations in ferromagnets, Comm. Math. Phys. 77 (1980) 111–126. MR589426

Motivation

At a busy airport the runway is the bottleneck, and the order in which aircraft land or take off determines how much of its capacity is used. Wake turbulence forces a minimum time between consecutive operations that depends on the weight classes of the leading and trailing aircraft, so reordering a first-come-first-served (FCFS) queue can increase throughput or reduce delay. Controllers cannot reorder freely: constrained position shifting (CPS), introduced by Dear (1976, MIT Flight Transportation Laboratory Report R76-9), allows each aircraft to move at most $k$ positions from its FCFS position, which keeps the sequence fair and predictable.

Balakrishnan and Chandran (Oper. Res. 58(6), 2010) cast CPS scheduling as dynamic programming on a layered network whose paths are the admissible sequences. For makespan and total delay the separations are assumed to satisfy the triangle inequality, which holds for arrivals only or departures only. When arrivals and departures share a runway it fails: in the separation table of the paper, a heavy arrival followed by a departure and then a small arrival needs only $75+60=135$ seconds through the departure, while the direct requirement is $196$ seconds. Section 6.2 of the paper handles this case for arbitrary per-aircraft cost functions, by expanding the network state. This mission formalizes that construction and its correctness.

Setting

Time is discrete: all data are integer multiples of one period. There are $n$ aircraft labelled in FCFS order, a maximum shift $k$, a minimum separation $\delta_{ab}\in\mathbb N$ between a leading aircraft $a$ and a trailing aircraft $b$, a time window $[e_a,l_a]$ for each aircraft, a finite set of precedence pairs $(x,y)$ ($x$ lands before $y$), and a cost $c_a(t)$ of landing aircraft $a$ at period $t$.

A $k$-CPS sequence is a bijection $\sigma$ from positions to aircraft with $|\sigma(p)-p|\le k$. A feasible schedule is a $k$-CPS sequence with integer landing times $t_p$ such that precedence pairs are respected, $e_{\sigma(p)}\le t_p\le l_{\sigma(p)}$, and

$$t_q-t_p\ \ge\ \delta_{\sigma(p)\sigma(q)}\qquad\text{for all positions } p<q .$$

Its cost is $\sum_p c_{\sigma(p)}(t_p)$.

The CPS network has stages $1,\dots,n$. A node of stage $p$ is a list of $\min\{2k+1,p\}$ distinct aircraft that may occupy positions $p-\min\{2k+1,p\}+1,\dots,p$; its last aircraft is the final aircraft $\mathrm{fin}(i)$. An arc joins consecutive stages when the lists overlap. Removing the nodes that violate a precedence pair gives the network $G$. For a node $i$, $\Gamma(i)$ is the set of integer times in the window of $\mathrm{fin}(i)$.

The modified network of §6.2 has nodes $(i,t,d)$: a node $i$ of $G$, a time $t\in\Gamma(i)$, and a lower bound $d$ on the separation between $\mathrm{fin}(i)$ and its predecessor, with $d=0$ at stage $1$ and otherwise $d^{\min}_i\le d\le d^{\max}_i$, where, for the penultimate and final aircraft $a,b$ of $i$,

$$d^{\min}_i=\delta_{ab},\qquad d^{\max}_i=\max\Big\{\max_{j:\,i\in P(j)}\big(\delta_{a,\mathrm{fin}(j)}-\delta_{b,\mathrm{fin}(j)}\big),\ d^{\min}_i\Big\}.$$

An arc $(i,t',d')\to(j,t'',d'')$ requires an arc $(i,j)$ of $G$, $t''-t'\ge d^{\min}_j$, $d''=\min\{t''-t',d^{\max}_j\}$, and $d'+t''-t'$ at least the separation between the penultimate aircraft of $i$ and $\mathrm{fin}(j)$. Arcs entering $(i,t,d)$ cost $c_{\mathrm{fin}(i)}(t)$.

Formalization targets

Goal: minimum-cost paths are optimal schedules

Under $k\ge 1$, positive costs, and the polygon inequalities of three or more hops (below):

1. a feasible schedule exists if and only if the modified network has a source-sink path;

$$\min_{(\sigma,t)\ \text{feasible}}\ \sum_p c_{\sigma(p)}(t_p)\;=\;\min_{\text{paths}}\ \sum_{p=1}^n c_{\mathrm{fin}(i_p)}(t_p),$$

each minimum existing exactly when the other does; 3. every minimum-cost path represents a feasible, optimal schedule.

Milestones

• Theorem 1 (with §3.1): the $k$-CPS sequences respecting precedence are exactly the sequences of source-sink paths of $G$.
• Lemma 5: every source-sink path of the modified network represents a feasible schedule.
• Lemma 6: every feasible schedule (in particular an optimal one) is represented by a source-sink path.
• Remark 1: under the triangle inequality, $d^{\min}_i=d^{\max}_i=\delta_{ab}$.
• Lemma 4: under the triangle inequality, a feasible schedule exists if and only if the simpler discrete-time network of §6.1.2, with nodes $(i,t)$, has a source-sink path.

Significance

The result turns a scheduling problem with arbitrary separable costs, time windows, precedence and non-metric separations into a shortest-path problem whose size is polynomial in $n$ for fixed $k$ and in the number of periods. It covers mixed arrival–departure operations, where the triangle inequality genuinely fails, and it is the basis of the paper's §7.1 algorithm for coupled arrivals and departures.

The paper proves Lemmas 5 and 6 in a few paragraphs and omits the proof of Lemma 4. No machine-checked version of the CPS network or of these lemmas exists. A formal development pins down the boundary cases the prose passes over (the first two stages, the last stage where $d^{\max}$ has no successors), and it makes explicit an assumption the prose leaves unstated: Lemma 5 needs the polygon inequalities, not only the two-step check in its proof.

Difficulty

The obvious argument checks separations only between consecutive aircraft, which is what the network of §6.1.2 does. Without the triangle inequality this misses aircraft two positions apart. The state $d$ repairs that but is capped at $d^{\max}$, so one must show that the cap loses nothing: a capped value still certifies the separation to the next aircraft. That uses the definition of $d^{\max}$ over the successors of a node in $G$, so the proof depends on how the network is pruned. Separations three or more positions apart are not tracked at all and rely on the polygon inequalities. Relating network paths to sequences (Theorem 1) requires reasoning about overlapping windows of the sequence and about the precedence pruning rule.

Formalization scope

Aircraft and positions are $0$-based (Fin n), stages $1$-based, and $n\ge 1$ (NeZero n). Times, windows and separations are natural numbers (periods); $d$, $d^{\min}$, $d^{\max}$ and time differences are integers, since $d^{\max}$ involves differences of separations that can be negative. Separation is required for all pairs of aircraft, not only consecutive ones. Minima are stated with IsLeast on sets of costs, never with a real infimum.

The following readings of the paper are committed:

• Polygon inequalities. Lemma 5 and the goal assume that for every chain $x_0,\dots,x_m$ of $m\ge 3$ hops between distinct aircraft, $\delta_{x_0x_m}\le\sum_i\delta_{x_ix_{i+1}}$. Without this hypothesis Lemma 5 is false: there are small instances violating the quadrilateral inequality whose minimum-cost path is infeasible. §7 of the paper asserts these inequalities for mixed operations; this mission states them as a hypothesis and makes no claim about the paper's Table 1.
• $\Gamma(i)$ is the full time window, not the narrowed set of §6.1.3, whose justification needs nondecreasing costs. With the full window Lemma 6 holds for every feasible schedule and arbitrary costs; it is stated in that stronger form.
• $k\ge 1$, so that every node beyond stage $1$ has a penultimate aircraft. Arc condition 4 is not imposed on arcs leaving stage $1$.
• Arc cost $c(i,t)$ of the paper is read as $c_{\mathrm{fin}(i)}(t)$.
• Precedence pruning uses the printed rule of §3.1; nodes unreachable from the source or the sink are not removed (this does not change the set of source-sink paths).
• Running times (§6.1.4, §6.3) and the bound $\lambda$ of recursion (4) are not formalized.

A trivializing formalization is ruled out: the networks are concrete definitions computed from the instance, not arbitrary graphs pinned by hypotheses, and the goal compares two independently defined minima, so it cannot hold by an empty feasible set or an unconstrained optimum.

A complete development needs basic list combinatorics (windows of a sequence, overlap of consecutive windows), the correspondence between bijections and paths, and finite minimization. The CPS network layer is shared with the other missions of this series and is reusable for any CPS scheduling result. Contributions on Theorem 1 alone are welcome, as it is independent of the time-expanded networks.

Selected references

• H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
• R. G. Dear, The Dynamic Scheduling of Aircraft in the Near Terminal Area, MIT Flight Transportation Laboratory Report R76-9, Massachusetts Institute of Technology, 1976 (as cited in the paper above).
• H. Lee, Tradeoff Evaluation of Scheduling Algorithms for Terminal-Area Air Traffic Control, Master's thesis, Massachusetts Institute of Technology, 2008 (source of the separation table; as cited in the paper above).

Motivation

Linear decision rules are a standard device for making multistage optimization under uncertainty computationally tractable: a recourse decision is restricted to be an affine function of the uncertain data observed so far. Their weakness is that a recourse variable that must stay nonnegative forces the rule to be very conservative. Goh and Sim, Distributionally Robust Optimization and Its Tractable Approximations (Operations Research, 2010), repair this with deflected linear decision rules, in which the violated part of an affine rule is corrected and paid for. The cost of the correction is the expected positive part $\mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ of an affine function of the uncertainty.

The distribution $\mathbb P$ is not known. The paper assumes only partial distributional information (a support set, a set containing the mean, a covariance, directional deviations) and bounds the worst case of this expectation over every distribution consistent with that information. Such worst-case bounds go back to Scarf's 1958 mean–variance newsvendor bound and form the core of distributionally robust optimization. This mission formalizes the first bound of §5, which uses support and mean information only.

Setting

Let $\tilde\zeta$ be a random vector in $\mathbb R^{n}$ (in the paper, the segregated uncertainty vector of dimension $n = N_E$). Two sets describe what is known about it:

• a support set $\mathcal V \subseteq \mathbb R^n$ with $\mathbb P(\tilde\zeta \in \mathcal V) = 1$;
• a mean set $\widehat{\mathcal V} \subseteq \mathbb R^n$ containing the mean $\hat\zeta = \mathbb E_{\mathbb P}(\tilde\zeta)$. A known mean is the case where $\widehat{\mathcal V}$ is a single point.

The family of distributions consistent with this information is

$$\mathbb F_1 = \{\mathbb P : \hat\zeta = \mathbb E_{\mathbb P}(\tilde\zeta) \in \widehat{\mathcal V},\ \mathbb P(\tilde\zeta \in \mathcal V) = 1\}.$$

For data $r^0 \in \mathbb R$ and $r \in \mathbb R^n$ the worst-case value is $\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$, with $x^+ = \max\{x, 0\}$. The paper's candidate for this value is the deterministic quantity of (21),

$$\pi^1(r^0, r) = \inf_{s \in \mathbb R^{n}} \Phi(s), \qquad \Phi(s) = \sup_{\hat\zeta \in \widehat{\mathcal V}} \{s'\hat\zeta\} + \sup_{\zeta \in \mathcal V} \max\{r^0 + r'\zeta - s'\zeta,\ -s'\zeta\}.$$

Both quantities live in the extended reals: following the paper (p. 909), an infeasible maximization has value $-\infty$ and an infeasible minimization $+\infty$.

Formalization targets

Goal: Theorem 1 (p. 909)

For closed convex $\mathcal V, \widehat{\mathcal V}$ with $\widehat{\mathcal V} \cap \operatorname{int} \mathcal V \neq \emptyset$, and all $r^0, r$,

$$\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big) = \pi^1(r^0, r).$$

Milestones

1. Upper-bound part of Theorem 1. $\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+) \le \pi^1(r^0, r)$, for arbitrary sets $\mathcal V, \widehat{\mathcal V}$.
2. Remark after Theorem 1, first case (p. 910). If $\widehat{\mathcal V} \subseteq \mathcal V$ is nonempty and $r^0 + r'\zeta \ge 0$ on $\mathcal V$, then the worst-case value equals $r^0 + \sup_{\hat\zeta \in \widehat{\mathcal V}} r'\hat\zeta$, and $\Phi(r) = \pi^1(r^0, r)$.
3. Remark after Theorem 1, second case (p. 910). If $\widehat{\mathcal V} \subseteq \mathcal V$ is nonempty and $r^0 + r'\zeta \le 0$ on $\mathcal V$, then the worst-case value is $0$, and $\Phi(0) = \pi^1(r^0, r) = 0$.
4. Tightness part of Theorem 1. Under the goal's hypotheses, $\pi^1(r^0, r) \le \sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$.

Significance

The result itself. Theorem 1 converts an optimization over an infinite-dimensional set of probability measures into a finite-dimensional convex program over the given sets. When $\mathcal V$ and $\widehat{\mathcal V}$ are representable by linear and second-order cone constraints, the epigraph of $\pi^1$ is a pair of robust constraints over those sets and is again tractable (Remark, p. 910). The bound is tight, so no better bound can be built from support and mean information alone. In the paper, $\pi^1$ is one of three building blocks; their infimal convolution (Theorem 4) prices the deflection in the deflected linear decision rules of §6, and the experiments there compare these rules against plain linear decision rules.

Formalizing it. The proof of Theorem 1 is in the paper's online appendix, not in the main text. A search of the Prove2Me library (October 2026) found no formal statement of this or any other mean-and-support bound. A formal proof has to settle the extended-real bookkeeping (empty families, unbounded suprema) and the exact hypotheses under which tightness holds. As printed, the theorem omits a condition: with no constraint qualification it fails when $\mathbb F_1$ is empty, which can happen for disjoint closed convex sets. This mission states the corrected version.

Difficulty

The upper-bound part is weak duality and needs no structure on the sets. The difficulty is tightness. It amounts to a strong-duality statement between the worst case over distributions and the infimum over the multiplier $s$, and strong duality for convex problems over unbounded sets needs a constraint qualification. Two obvious approaches fail. The first is to search for a single worst-case distribution: for unbounded $\mathcal V$ the supremum over $\mathbb F_1$ is generally not attained, and it may be $+\infty$. The second is to restrict to compact $\mathcal V$, which excludes the paper's main use, a segregation of an unbounded support such as $(-\infty, -1] \cup [-1, 1] \cup [1, \infty)$. Mathlib has separating-hyperplane theorems but no Fenchel duality theorem, so this duality has to be built.

Formalization scope

• A distribution is a measure $P$ on Fin n → ℝ with IsProbabilityMeasure P, and the random vector is the identity map. Every coordinate is required to be $P$-integrable, so the mean is a genuine expectation; the mean is MomentDRO.Conf.meanVec from the published definition MomentDRO_Conf_Setting.
• $\mathbb P(\tilde\zeta \in \mathcal V) = 1$ is the almost-everywhere statement ∀ᵐ ζ ∂P, ζ ∈ V, which needs no measurability of $\mathcal V$.
• The positive part is max (r0 + r ⬝ᵥ ζ) 0.
• The worst-case value, both suprema and the infimum in (21) are taken in EReal. An empty supremum is $-\infty$, an empty infimum $+\infty$, and an unbounded supremum $+\infty$. The paper's "inf" is ⨅; attainment is claimed only where the Remark claims it, via the objective $\Phi$ (pi1Obj) at $s = r$ and $s = 0$.
• The paper's tractable conic representable sets are modelled as closed and convex sets. The goal and its tightness part also assume $\widehat{\mathcal V} \cap \operatorname{int}\mathcal V \ne \emptyset$. This condition is not on the page; it is consistent with the paper's full-dimensionality assumptions (pp. 905–906), and it implies $\mathbb F_1 \neq \emptyset$.
• The Remark's two cases assume $\widehat{\mathcal V} \subseteq \mathcal V$ and $\widehat{\mathcal V} \ne \emptyset$. The paper's construction of $\mathcal V, \widehat{\mathcal V}$ from one set $\mathcal H$ (§4.5) gives the inclusion, and without it the first case is false.
• The segregation map, the matrices $F$, $g$ and the set $\mathcal H$ of §4 are context only and are not formalized: the theorem is stated for an arbitrary random vector with the listed properties.
• A real-valued supremum, a family without integrability (for which the mean would be a junk value), or a $\pi^1$ defined through the worst case would each trivialize the statement; the definitions avoid all three, and $\pi^1$ is defined directly from the sets.

Needed infrastructure: finite mixtures of Dirac masses as members of $\mathbb F_1$, integration of almost-surely bounded functions, separation of convex sets in $\mathbb R^n$, and a Fenchel-type duality for a concave function over a closed convex set under an interior-point condition. The duality and the concave-envelope facts are reusable well beyond this mission, including for Theorems 2–4 of the same paper. Proofs of any milestone, and reusable lemmas on extended-real suprema of integrals, are welcome.

Selected references

• J. Goh and M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4, Part 1 of 2):902–917, 2010. https://doi.org/10.1287/opre.1090.0795
• H. Scarf, A Min–Max Solution of an Inventory Problem, in K. Arrow, ed., Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958, 201–209.
• W. Chen and M. Sim, Goal-Driven Optimization, Operations Research 57(2):342–357, 2009 (cited by the paper for the infimal convolution of bounds).
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorem 31.1, Fenchel duality). https://doi.org/10.1515/9781400873173

Motivation

Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time is a basic model of machine scheduling: each job may take a different time on each machine, and a job becomes available on a machine only at a machine-dependent release date. In the three-field notation the problem is $R \mid r_{ij} \mid \sum w_jC_j$. Already the sequencing problem on a single machine with release dates is strongly NP-hard, so the question is how well it can be approximated in polynomial time.

Timeline (as surveyed in §1 of the paper):

• Phillips, Stein and Wein gave a performance guarantee of $O(\log^2 n)$ for a network-scheduling generalization.
• Hall, Shmoys and Wein (1996/1997) gave the first constant factor, $16/3$, from an interval-indexed linear programming relaxation (Math. Oper. Res. 22, 1997).
• Schulz and Skutella (1997–1999) gave a randomized $(2+\varepsilon)$-approximation from a time-indexed linear programming relaxation in intervals of geometrically increasing length; its size depends on $p_{\max}$ and on $\varepsilon$.
• Skutella (J. ACM 48, 2001) replaced the linear program by a convex quadratic program in assignment variables of strongly polynomial size and showed, in §3, that randomized rounding of it is a $2$-approximation.

This mission formalizes that last result.

Setting

There are $n$ jobs $J$ and $m$ machines. Job $j$ has a weight $w_j \ge 0$; on machine $i$ it has a processing time $p_{ij} > 0$ and a release date $r_{ij} \ge 0$. A nonpreemptive schedule runs every job without interruption on one machine, starting no earlier than its release date there, and each machine processes at most one job at a time. With completion times $C_j$, the objective is $\sum_j w_jC_j$.

Smith's order on machine $i$: $j \prec_i k$ if $w_j/p_{ij} > w_k/p_{ik}$, or the ratios are equal and $j < k$.

Time slots. Sort the release dates on machine $i$ as $\rho_{i_1} \le \dots \le \rho_{i_n}$ and set $\rho_{i_{n+1}} = \infty$. The $k$-th time slot $i_k$ holds the jobs started on machine $i$ within $[\rho_{i_k}, \rho_{i_{k+1}})$. An assignment of jobs to slots is feasible if job $j$ goes to a slot $i_k$ with $\rho_{i_k} \ge r_{ij}$. For assignment variables $a_{i_kj}$, the slot starts are

$$s_{i_1} = \rho_{i_1}, \qquad s_{i_{k+1}} = \max\Big\{\rho_{i_{k+1}},\ s_{i_k} + \sum_j a_{i_kj}p_{ij}\Big\},$$

and for a 0/1 assignment the completion time of $j \in i_k$ is $C_j = s_{i_k} + p_{ij} + \sum_{j' \prec_i j,\ j' \in i_k} p_{ij'}$ (17).

(CQP). Minimize $Z_{CQP}(a) = \sum_j w_j \bar C_j(a)$ with

$$\bar C_j(a) = \sum_{i,k} a_{i_kj}\Big(\rho_{i_k} + \frac{1 + a_{i_kj}}{2}\,p_{ij} + \sum_{j' \prec_i j} a_{i_kj'}p_{ij'}\Big)$$

subject to $\sum_{i,k} a_{i_kj} = 1$ (14), $a_{i_kj} = 0$ if $\rho_{i_k} < r_{ij}$ (18), $a \ge 0$ (20), and $\sum_j a_{i_kj}p_{ij} \le \rho_{i_{k+1}} - \rho_{i_k}$ (21). In matrix form the objective is $b^Ta + \tfrac12 c^Ta + \tfrac12 a^T(D + \mathrm{diag}(c))a$, which is convex.

Randomized rounding. Each job $j$ is put into exactly one slot $i_k$, with probability $a_{i_kj}$, the choices being pairwise independent across jobs. The resulting slot assignment is turned into a schedule by (15)–(17).

Formalization targets

Goal: Theorem 3.4 (pp. 19–20), formal core

For every instance with $p > 0$, $w \ge 0$, $r \ge 0$:

1. every feasible slot assignment yields a feasible schedule with completion times (17);
2. for every (CQP)-feasible $a$ and every pairwise independent rounding $\mu$ of $a$,

$$E_\mu\Big[\sum_j w_jC_j\Big] \le 2\,Z_{CQP}(a);$$

3. every feasible schedule $S$ admits a (CQP)-feasible $a$ with $Z_{CQP}(a) \le \sum_j w_jC_j(S)$.

The bound is stated for every feasible $a$, so it needs no optimum of (CQP), and with (3) it gives the positive half of Corollary 3.6.

Milestones

• Lemma 3.1 (p. 15): an optimal schedule exists whose slots are sequenced by $\prec_i$ without interruption.
• p. 16: the schedule built from a feasible slot assignment is feasible, with completion times (17).
• Lemma 3.2 (p. 16): rebuilding such a schedule from its slot assignment gives a feasible schedule with the same property that completes no job later.
• p. 17: for 0/1 assignments the relaxed completion times (19) equal (17).
• Lemma 3.3 (p. 18): the quadratic programming relaxation has an optimal solution with $s_{i_k} = \rho_{i_k}$ for all $i, k$.
• Proof of Lemma 3.5 (p. 20): $E_{j \mapsto i_k}[s_{i_k}] \le 2\rho_{i_k}$.
• Lemma 3.5 (p. 20): $E[C_j] \le 2\bar C_j(a)$ for every job.

Significance

The result gives a $2$-approximation for $R \mid r_{ij} \mid \sum w_jC_j$ from a program of polynomial size, with a short analysis that holds job by job. The relaxation (CQP) is also the basis of §4, where the same rounding compares nonpreemptive with preemptive schedules, and its relaxation property bounds the optimum of (CQP) against the optimal schedule within a factor $2$.

The result is proved in the paper; none of it is formalized. A formal development adds a checked model of release-date schedules and time slots on unrelated machines, the exchange argument behind Smith's rule in the presence of release dates, and a measure-free treatment of pairwise independent rounding. These pieces are reusable for other slot-based relaxations.

Difficulty

The analysis of Lemma 3.5 is short; the work lies in the reduction to slot assignments. Lemma 3.1 is an exchange argument, but swapping two jobs can push a job into a different time slot, so the naive bubble sort within a slot does not obviously terminate in a slot-sequenced schedule. Lemma 3.2 needs an induction across slots that accounts for empty slots and ties $\rho_{i_k} = \rho_{i_{k+1}}$. Lemma 3.3 is a shifting argument on fractional solutions whose objective change is a quadratic computation, and the step size printed on p. 18 must be divided by $p_{i\hat\jmath}$ to land exactly on $s_{i_k} = \rho_{i_k}$. The relaxation conjunct of the goal chains Lemmas 3.1, 3.2, 3.3 and the p. 17 identity.

Formalization scope

Jobs are Fin n, machines Fin m, and slots Fin m × Fin n, all 0-based. $\prec_i$ is cross-multiplied, which equals the page's ratio order because $p > 0$. $\rho$ is the sorted tuple of release dates; $\rho_{i_{n+1}} = \infty$ is never represented by a real number. Constraint (21) is imposed only for slots before the last, and a job's slot is the largest $k$ with $\rho_{i_k} \le S_j$. Schedules are a machine and a real start time per job; two jobs on one machine must satisfy $C_j \le S_k$ or $C_k \le S_j$. Randomized rounding is a probability weight on slot assignments with marginals $a_{i_kj}$ and product joint probabilities for distinct jobs; full independence is not required, and the product weight is one instance. The standing assumptions $p_{ij} > 0$, $w_j \ge 0$, $r_{ij} \ge 0$ of p. 2 are hypotheses of every theorem; Lemmas 3.1 and 3.3, which assert existence, also assume $m \ge 1$.

A statement of the bound alone, $E \le 2 Z_{CQP}(a)$, would say nothing about schedules: conjuncts 1 and 3 of the goal are what tie it to the scheduling problem, and neither may be dropped.

Not formalized: polynomial-time solvability of (CQP), the running time of the algorithm, the tightness half of Corollary 3.6, and the first sentence of Lemma 3.1 as a statement about every optimal schedule (false when some $w_j = 0$).

Contributions welcome: proofs of any milestone; a general library of time-slot schedules; and the convexity of (22) (positive semidefiniteness of $D + \mathrm{diag}(c)$), which is not a milestone here.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• 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), 1997. https://doi.org/10.1287/moor.22.3.513
• A. S. Schulz and M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM Journal on Discrete Mathematics 15(4), 2002. https://doi.org/10.1137/S0895480199357078
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106

Motivation

In a road or communication network where each unit of traffic picks its own route, the outcome is a Nash flow (Wardrop equilibrium): no traffic can lower its own latency by switching paths. It is well known since Pigou (1920) that such selfish routing can be inefficient: the total latency of a Nash flow may exceed that of the best centrally planned flow. The ratio between the two, maximized over a family of instances, is the price of anarchy. Network designers, transportation economists and computer scientists use it to decide when central coordination (tolls, routing protocols) is worth its cost.

Timeline:

• 1920–1956. Pigou's two-road example shows inefficiency; Wardrop (1952) and Beckmann, McGuire and Winsten (1956) formalize equilibrium flows and characterize optimal flows by marginal costs.
• 2002. Roughgarden and Tardos (J. ACM 49(2), 2002) prove that with affine latencies $\ell(x)=ax+b$ the price of anarchy is exactly $4/3$ in every network.
• 2002–2003. Roughgarden (STOC 2002; journal version J. Comput. Syst. Sci. 67(2), 2003) shows that for any class of latency functions satisfying mild conditions the price of anarchy does not depend on the network: two parallel links are already worst possible. This mission formalizes that paper.
• 2004. Correa, Schulz and Stier-Moses (Math. Oper. Res. 29(4), 2004) give a geometric proof of the same bound and extend it to capacitated networks.

Setting

A network is a finite directed multigraph $G=(V,E)$; parallel edges are allowed. There are $k$ commodities; commodity $i$ has a source $s_i$, a sink $t_i$, a rate $r_i>0$, and at least one simple $s_i$–$t_i$ path. A flow $f$ assigns a nonnegative amount $f^i_P$ to each simple $s_i$–$t_i$ path $P$; it is feasible if $\sum_P f^i_P=r_i$ for every $i$. The edge flow is $f_e=\sum_i\sum_{P\ni e}f^i_P$.

Each edge carries a latency function $\ell_e:[0,\infty)\to\mathbb R$, nonnegative, differentiable and nondecreasing. The latency of a path is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$ and the cost of a flow is $C(f)=\sum_i\sum_P\ell_P(f)f^i_P$. A feasible flow of least cost is optimal. A flow is a Nash flow (Definition 2.1) if moving any amount $\delta\in(0,f^i_{P_1}]$ of commodity $i$ from a used path $P_1$ to another path $P_2$ yields a flow $\tilde f$ with $\ell_{P_1}(f)\le\ell_{P_2}(\tilde f)$. The ratio between the cost of a Nash flow and of an optimal flow is $\rho(G,r,\ell)$.

A latency function is standard if $x\,\ell(x)$ is convex on $[0,\infty)$; its marginal cost is $\ell^*(x)=\frac{d}{dx}(x\,\ell(x))$. A class $\mathcal L$ of latency functions is standard if it contains a nonzero function and all its members are standard. The anarchy value of a standard $\ell$ is

$$\alpha(\ell)=\sup_{r>0:\ \ell(r)>0}\bigl[\lambda\mu+(1-\lambda)\bigr]^{-1},\qquad \ell^*(\lambda r)=\ell(r),\ \lambda\in[0,1],\ \mu=\frac{\ell(\lambda r)}{\ell(r)},$$

and $\alpha(\mathcal L)=\sup_{0\neq\ell\in\mathcal L}\alpha(\ell)\in[1,\infty]$. It is the worst ratio in a Pigou-type network: two parallel links, one with a constant latency and one with $\ell$. Finally, $G_2$ is the network with one source, one sink and two edges from source to sink.

Formalization targets

Goal: Theorem 4.2

For a standard class $\mathcal L$ that contains the constant functions $\ell(x)=c$, $c>0$, with $\mathcal I$ the set of all instances with latencies in $\mathcal L$ and $\mathcal I_2\subseteq\mathcal I$ the single-commodity instances on $G_2$,

$$\sup_{(G_2,r,\ell)\in\mathcal I_2}\rho(G_2,r,\ell)=\alpha(\mathcal L)=\sup_{(G,r,\ell)\in\mathcal I}\rho(G,r,\ell).$$

It is stated as two parts: every ratio $C(f)/C(f^*)$ of a feasible Nash flow to a feasible flow of positive cost, in any network with any number of commodities, is at most $\alpha(\mathcal L)$; and every value below $\alpha(\mathcal L)$ is exceeded by such a ratio on $G_2$.

Milestones

The milestones follow the paper's proof: the edge form of the cost (§2.1), the shortest-path characterization of Nash flows (Proposition 2.2), the cost of a Nash flow (Proposition 2.3), monotonicity and continuity of marginal costs (§2.3), existence of $\lambda$ (§3.1), Lemmas 3.5–3.7, the upper bound $\rho\le\alpha(\mathcal L)$ (Theorem 3.8) and the two-link lower bound (Lemma 4.1).

Companion results

Lemma 4.4 and Theorem 4.5 replace "contains the constants" by diversity (for each $c>0$ some $\ell\in\mathcal L$ has $\ell(0)=c$) and show that networks of parallel links are worst possible among single-commodity instances. Proposition 5.1 computes the price of anarchy of polynomials of degree at most $p$ with nonnegative coefficients:

$$\sup_{\mathcal I_p}\rho=\bigl[1-p\,(p+1)^{-(p+1)/p}\bigr]^{-1}=\Theta\!\left(\frac{p}{\ln p}\right).$$

Significance

The theorem reduces a combinatorial question (the worst instance over all networks and all commodity structures) to a one-dimensional calculus problem: computing $\alpha(\ell)$ for the steepest functions of the class. It yields exact prices of anarchy for polynomial latencies (Proposition 5.1), for M/M/1 delay functions and others, and it shows that the inefficiency of selfish routing is never caused by the interaction of commodities or by network structure: Pigou's two-link example already captures it. The bound has become a standard reference point for later work on smoothness arguments, tolls and Stackelberg routing.

The result is proved; it has not been formalized. This mission produces a machine-checked model of nonatomic multicommodity routing on directed multigraphs (simple paths, path flows, Nash flows in the paper's own definition, marginal costs), the general upper bound for an arbitrary standard class, and the matching lower bound in two-link and parallel-link networks. Alternative arguments, such as the variational-inequality proof of Correa, Schulz and Stier-Moses, are equally welcome as proofs of the same statements.

Difficulty

The obvious approach, following Roughgarden–Tardos for affine latencies, scales the Nash flow down by a constant factor and shows the result is optimal for reduced rates. For nonlinear latencies no single factor works. The paper's proof scales each edge by its own factor $\lambda_e$, which produces a pseudoflow that obeys no conservation constraints, and the augmentation from it to an optimal flow must then be priced edge by edge. Formally, the scaling factors are solutions of $\ell_e^*(\lambda_e f_e)=\ell_e(f_e)$ that need not be unique, marginal costs are one-sided derivatives at $0$, and the anarchy value may be infinite, so every comparison has to be valid in the extended reals.

Formalization scope

All declarations live in PoAIndep.Topology. A network is a pair of finite types with endpoint maps src tgt : E → V; parallel edges are free. Simple paths are nonempty edge lists with a repetition-free vertex sequence, so commodities with $s_i=t_i$ are excluded. A flow stores one finitely supported path flow per commodity. Latency functions are maps $\mathbb R\to\mathbb R$ whose properties (nonnegative, differentiable, nondecreasing; for standard ones, $x\ell(x)$ convex) are required on $[0,\infty)$ only, and $\ell^*$ is the derivative within $[0,\infty)$. The standing assumptions of §2.1 ($r_i>0$, $\mathcal P_i\neq\emptyset$, latency properties) are fields of the Instance structure; standardness of the latencies enters through the class $\mathcal L$.

The anarchy values live in $[0,\infty]$; $\alpha(\ell)$ is the supremum over all admissible pairs $(r,\lambda)$, which equals the page's value because the expression does not depend on the choice of $\lambda$. Instead of $\rho$, which presupposes existence and uniqueness of the Nash cost (Proposition 2.4, cited by the paper), statements bound $C(f)/C(f^*)$ for every feasible Nash flow $f$ and every feasible $f^*$ with $C(f^*)>0$. The networks $G_2$ and $G_m$ are instances of the general model, so $\mathcal I_2\subseteq\mathcal I$ holds literally.

The Nash condition is Definition 2.1, not the shortest-path characterization, and the cost is the path sum, not the edge sum; both alternatives would make milestones trivial. The goal is not satisfied by the two-link lower bound alone: its upper part quantifies over every network and every number of commodities.

Reusable beyond this mission: the routing model, Nash flows, marginal costs and the anarchy value, which also underlie the companion paper on the $4/3$ bound and later work on tolls and Stackelberg strategies. Proofs of any milestone, and supporting lemmas about convex functions with one-sided derivatives, are welcome.

Selected references

• T. Roughgarden, The price of anarchy is independent of the network topology, STOC 2002, pp. 428–437; journal version J. Comput. Syst. Sci. 67(2):341–364, 2003. https://doi.org/10.1145/509967.509971
• T. Roughgarden and É. Tardos, How bad is selfish routing?, J. ACM 49(2):236–259, 2002. https://doi.org/10.1145/506147.506153
• J. R. Correa, A. S. Schulz and N. E. Stier-Moses, Selfish routing in capacitated networks, Math. Oper. Res. 29(4):961–976, 2004. https://doi.org/10.1287/moor.1040.0098
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Inst. Civil Engineers, Part II, 1:325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259

Motivation

A Markov decision process (MDP) is evaluated by solving a linear fixed-point equation built from its transition probabilities. In practice those probabilities are rarely known exactly: they are estimated from data, elicited from experts, or obtained by aggregating the states of a larger model, and each estimate comes with an error band. Givan, Leach and Dean (Bounded-parameter Markov decision processes, Artificial Intelligence, 2000) replace each transition probability by a closed interval and ask what can still be said about the value of a policy. Their answer for a fixed policy is an interval value: at each state, the smallest and the largest expected discounted reward the policy can obtain over all exact MDPs consistent with the intervals.

The same model reappears under other names. Robust MDPs with rectangular uncertainty sets (Nilim and El Ghaoui, Operations Research, 2005; Iyengar, Mathematics of Operations Research, 2005) take the pessimistic end of the interval, and optimistic model-based reinforcement learning (for example UCRL-type algorithms) takes the optimistic end over a confidence set. Interval transition models are also used to bound the error of state aggregation. In all of these, the basic computational question is how to evaluate a fixed policy against a whole family of MDPs at once.

Setting

Fix a finite set $Q$ of states and a finite nonempty set $A$ of actions. An exact MDP $M=\langle Q,A,F,R\rangle$ has transition probabilities $F_{pq}(\alpha)$, each row $q\mapsto F_{pq}(\alpha)$ a probability distribution, a reward $R(q)\in\mathbb R$ per state, and a discount rate $0\le\gamma<1$. A policy is a map $\pi:Q\to A$. Its value function $V_{M,\pi}$ is the expected discounted cumulative reward of the Markov chain with transition matrix $F_{pq}(\pi(p))$:

$$V_{M,\pi}(p)=\sum_{t\ge0}\gamma^t\,(P_\pi^tR)(p),\qquad P_\pi(p,q)=F_{pq}(\pi(p)).$$

On the space $\overline V$ of value functions $v:Q\to\mathbb R$, with the sup norm $\|v\|=\max_q|v(q)|$, the value-iteration operator is $VI_{M,\pi}(v)(p)=R(p)+\gamma\sum_{q}F_{pq}(\pi(p))\,v(q)$, and $VI_{M,\alpha}$ is the same with the action $\alpha$ in place of $\pi(p)$. An operator $T$ on $\overline V$ is a contraction mapping if $\|Tv-Tu\|\le\lambda\|v-u\|$ for all $u,v$ and some $0\le\lambda<1$.

A bounded-parameter MDP (BMDP) $M_\updownarrow$ gives intervals $[F_{\downarrow pq}(\alpha),F_{\uparrow pq}(\alpha)]\subseteq[0,1]$ with $\sum_qF_{\downarrow pq}(\alpha)\le1\le\sum_qF_{\uparrow pq}(\alpha)$, a reward $R$ and a discount rate $\gamma$. An exact MDP belongs to $M_\updownarrow$ if it has the same $R$ and $\gamma$ and every transition probability lies in its interval. The interval value of a policy $\pi$ (Definition 3) is

$$V_{\updownarrow\pi}(q)=\Big[V_{\downarrow\pi}(q),V_{\uparrow\pi}(q)\Big]=\Big[\min_{M\in M_\updownarrow}V_{M,\pi}(q),\ \max_{M\in M_\updownarrow}V_{M,\pi}(q)\Big].$$

Interval policy evaluation acts on an interval value function $V_\updownarrow=[V_\downarrow,V_\uparrow]$ by

$$IVI_{\updownarrow\pi}(V_\updownarrow)(p)=\Big[\min_{M\in M_\updownarrow}VI_{M,\pi}(V_\downarrow)(p),\ \max_{M\in M_\updownarrow}VI_{M,\pi}(V_\uparrow)(p)\Big],$$

with lower and upper bound maps $IVI_{\downarrow\pi},IVI_{\uparrow\pi}:\overline V\to\overline V$.

For the optional part, interval value iteration adds a maximization over actions: $IVI_{\updownarrow opt}$ and $IVI_{\updownarrow pes}$ take, at each state, the largest of the candidate intervals $\big[\min_MVI_{M,\alpha}(V_\downarrow)(p),\max_MVI_{M,\alpha}(V_\uparrow)(p)\big]$ for the lexicographic orders $\le_{opt}$ (upper end first) and $\le_{pes}$ (lower end first). For a value function $V$, $\rho_V(p)$ and $\sigma_V(p)$ are the actions maximizing $\max_MVI_{M,\alpha}(V)(p)$ and $\min_MVI_{M,\alpha}(V)(p)$, and $IVI_{\downarrow opt,V}(V')=IVI_{\downarrow opt}([V',V])$, $IVI_{\uparrow pes,V}(V')=IVI_{\uparrow pes}([V,V'])$.

Formalization targets

Goal: convergence of interval policy evaluation (Section 5.1, p. 22)

For every BMDP, every policy $\pi$, and every interval value function $V_{\updownarrow0}=[V_{\downarrow0},V_{\uparrow0}]$ with $V_{\downarrow0}\le V_{\uparrow0}$,

$$\lim_{n\to\infty}IVI_{\updownarrow\pi}^{\,n}(V_{\updownarrow0})=V_{\updownarrow\pi}.$$

The limit is the interval value of Definition 3, an extremum over infinitely many MDPs; nothing about the starting point is assumed beyond its being an interval value function.

Milestones on the goal's path

• Theorem 10 (p. 21): $IVI_{\downarrow\pi}$ and $IVI_{\uparrow\pi}$ are contraction mappings on $\overline V$.
• Theorem 11 (p. 22): $IVI_{\downarrow\pi}(V_{\downarrow\pi})=V_{\downarrow\pi}$, $IVI_{\uparrow\pi}(V_{\uparrow\pi})=V_{\uparrow\pi}$, and hence $IVI_{\updownarrow\pi}(V_{\updownarrow\pi})=V_{\updownarrow\pi}$.

Further results on interval value iteration (Section 5.2)

• Lemma 4 (p. 25): $IVI_{\downarrow opt,V}(V')(p)=\max_{\alpha\in\rho_V(p)}\min_{M}VI_{M,\alpha}(V')(p)$ and $IVI_{\uparrow pes,V}(V')(p)=\max_{\alpha\in\sigma_V(p)}\max_{M}VI_{M,\alpha}(V')(p)$.
• Theorem 13(a) (p. 25): $IVI_{\uparrow opt}$ and $IVI_{\downarrow pes}$ are contraction mappings.
• Theorem 13(b) (p. 25): for every value function $V$, $IVI_{\downarrow opt,V}$ and $IVI_{\uparrow pes,V}$ are contraction mappings.

Significance

The result. The interval value is defined as a minimum and a maximum over a continuum of MDPs, and there is no a priori reason it should be computable by a dynamic program. The goal says it is: one operator, whose per-state step is a small linear program over a box intersected with a simplex, iterated from any start, converges to both ends of the interval simultaneously. The pessimistic end is the robust value of the policy under rectangular uncertainty, so the goal is also a policy-evaluation theorem for interval-rectangular robust MDPs; the optimistic end is the value used by optimism-based exploration. Theorem 11 is the bridge between the "game" definition (nature picks the MDP) and the fixed-point characterization; Theorem 13 is the corresponding first step for the optimal interval values of the companion mission.

Formalizing it. The results are proved in the paper (2000), with Theorem 11 relying on the existence of a single member MDP that is $\pi$-minimizing at every state simultaneously (the paper's Theorem 7). No machine-checked version of the BMDP model or of these results is known. Nearby statements formalized elsewhere concern other models: robust MDPs with costs and general row sets, and optimistic Bellman equations over compact confidence sets. This mission produces the BMDP model and its interval operators, the contraction and fixed-point theorems, and the convergence theorem, all stated against the member-MDP definition of $V_{\updownarrow\pi}$.

Difficulty

The contraction estimates (Theorems 10 and 13) follow the familiar pattern for Bellman operators, with the extra point that the minimum or maximum over the infinite family $M_\updownarrow$ must be attained. The real difficulty is Theorem 11. The obvious argument compares $V_{\downarrow\pi}(q)$ with $VI_{M,\pi}(V_{\downarrow\pi})(q)$ state by state; but $V_{\downarrow\pi}(q)$ is a minimum taken separately at each state, possibly by a different MDP at each state, and $V_{\downarrow\pi}$ need not a priori be the value function of any single member MDP. Without a member MDP that is minimizing at all states at once, the inequality $IVI_{\downarrow\pi}(V_{\downarrow\pi})\ge V_{\downarrow\pi}$ does not follow. Establishing that simultaneous minimizer is the central step.

Formalization scope

All statements live in the namespace BoundedParamMDP.IntervalEval. The exact MDP, the BMDP, its member MDPs, $V_{M,\pi}$, $VI_{M,\pi}$, $VI_{M,\alpha}$ and Definition 3's $V_{\downarrow\pi}$, $V_{\uparrow\pi}$ are the shared definitions BoundedParamMDP.Optimal.MDP and BoundedParamMDP.Optimal.BMDP used by the companion mission, so its theorems apply to the same objects. Conventions:

• $Q$ and $A$ are finite types, $A$ is nonempty; $Q$ may be empty (every statement then holds for the paper's own reasons). Policies are deterministic and stationary, Q → A.
• An exact MDP is a structure with F p α q $=F_{pq}(\alpha)$, rows nonnegative and summing to $1$, a state reward R, and the discount rate $0\le\gamma<1$ as a field. Rewards are tight (the paper's footnote 3): members share the BMDP's R and γ.
• $V_{M,\pi}$ is the discounted series $\sum_t\gamma^t P_\pi^tR$, not a solution chosen from the Bellman equation.
• Minima and maxima over $M_\updownarrow$ are the real infimum and supremum over the nonempty subtype Member B; all quantities are bounded, so these are the genuine values (and attained, by the paper's Lemma 1).
• An interval value function is a pair (V↓, V↑) of functions Q → ℝ. The operators are defined on all pairs; the goal assumes $V_{\downarrow0}\le V_{\uparrow0}$ as the paper's interval notion, though the conclusion does not need it.
• The norm is Mathlib's norm on Q → ℝ (the sup norm (4)); convergence of pairs is in the product topology. A contraction mapping is "there exists $\lambda\in[0,1)$", as on p. 6; the modulus is not fixed to $\gamma$.
• $\max_{\alpha,\le_{opt}}$ is the supremum over the finite action set in the lexicographic order on (upper end, lower end); $\le_{pes}$ uses (lower end, upper end). $\rho_V(p)$, $\sigma_V(p)$ are sets of actions.
• Theorem 13(a) is stated for $IVI_{\uparrow opt}$ as the upper end of $IVI_{\updownarrow opt}$ with arbitrary lower inputs on both sides: the bound by $\lambda\|U'-U\|$ includes the independence from the lower input that the paper uses (p. 23) to regard $IVI_{\uparrow opt}$ as a map on $\overline V$.
• Lemma 4's second line is printed with $\min_{M}$; the evident reading $\max_M$ (eq. (29), proof of Theorem 13(b), p. 47) is stated.

A trivializing formalization is excluded: the limit in the goal is Definition 3's infimum and supremum over member MDPs, not the fixed point of $IVI_{\updownarrow\pi}$, so the goal is not Banach's theorem alone; and the member type is nonempty for every BMDP, so the infima and suprema are not the junk value $0$.

The proof of Theorem 11 uses the paper's Lemma 1 (attainment in the order-maximizing family), Theorem 3 ($V_{M,\pi}$ is the unique fixed point of $VI_{M,\pi}$), Theorem 6 (comparison principle) and Theorem 7 (existence of $\pi$-minimizing and $\pi$-maximizing MDPs). These are milestones of the companion mission Bounded-parameter Markov Decision Processes 1 and are not restated here. The Banach fixed-point theorem is Mathlib's ContractingWith. Contributions welcome: proofs of the milestones, a reusable lemma on the attained minimum of a linear function over a box intersected with the simplex, and the order-maximizing construction itself.

Selected references

• R. Givan, S. Leach, T. Dean, Bounded-parameter Markov decision processes, Artificial Intelligence 122 (2000). https://doi.org/10.1016/S0004-3702(00)00047-3
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887