Operations Research

Computational Geometry Dynamic Programming Optimization·Captain: mikedeng1

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 1: The Threshold Rule on Efficient Periods Picks an Optimal Next Production PeriodResearch Paper

Motivation

Economic lot sizing asks how to meet a known sequence of demands while deciding when to set up production and how much to carry forward. It is a basic deterministic inventory problem: a setup has a fixed cost, production has a per-unit cost, and inventory may be held for later demand. Recomputing every possible next production period in the standard backward dynamic program takes a quadratic number of candidate comparisons. Wagelmans, Van Hoesel and Kolen use the geometry of cumulative-demand points to identify which candidates can affect the minimum. Their Section 2 gives the threshold rule targeted here. Wagelmans, Van Hoesel and Kolen (1992)

The paper notes independent related work by Aggarwal and Park and by Federgruen and Tzur. The published Prove2Me items for Federgruen and Tzur formalize a forward recursion and its minimal optimal predecessor lists. They address the same planning problem through different state variables; the backward value and efficient periods of this mission are new objects. Wagelmans, Van Hoesel and Kolen (1992), p. S145

Setting

A planning horizon consists of periods $1,\dots,n$ , with $n\ge1$ , and an extra terminal period $n+1$ . In period $i$ , a known demand $d_i\ge0$ must be met without backlogging. The final demand is positive, $d_n>0$ ; a trailing zero-demand period could otherwise be deleted. A production setup costs $f_i\ge0$ , and every unit produced in that period has a marginal cost $c_i\in\mathbb R$ . The sign of $c_i$ is unrestricted. Holding costs have been absorbed into these transformed marginal costs, as in Section 1 of the paper. Define the remaining demand $D(t)=\sum_{j=t}^{n}d_j$ , with $D(n+1)=0$ . If production at $i$ covers demand until the next production period $t$ , then $D(i)-D(t)$ units are produced. Wagelmans, Van Hoesel and Kolen (1992), pp. S146–S147

The backward value $G(t)$ starts at $G(n+1)=0$ and follows Equation (1). At positive demand, it minimizes $f_i+c_i[D(i)-D(t)]+G(t)$ over $i<t\le n+1$ . When $d_i=0$ , skipping setup and using $G(i+1)$ is an additional choice. The paper identifies $G(t)$ with the optimal cost from $t$ onward using the cited zero-inventory property. This mission takes Equation (1) as the definition of $G$ ; it does not formalize the separate equivalence with the original production-plan formulations. Wagelmans, Van Hoesel and Kolen (1992), p. S147

For a fixed $i$ , plot the finite points $(D(t),G(t))$ for $i<t\le n+1$ . Their lower convex envelope is a piecewise linear graph. Its endpoints and places where its slope changes are breakpoints; the corresponding period indexes form the efficient set $E_i$ . Write $\operatorname{succ}_i(t)$ for the next larger index in $E_i$ . The consecutive-point ratio is $r_i(t)=[G(t)-G(\operatorname{succ}_i(t))]/[D(t)-D(\operatorname{succ}_i(t))]$ . These objects have no optimization over production policies hidden in their definitions. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization targets

Efficient candidates

Proposition 1 says every candidate outside $E_i$ can be removed without changing the minimum:

\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=\min_{t\in E_i}\{c_i[D(i)-D(t)]+G(t)\}.

The endpoint and slope claims establish the geometry used in this reduction. Proposition 2 compares neighboring efficient periods using $r_i(t)$ and $c_i$ . Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S149

Threshold rule and backward value

The selected period is the first efficient index whose ratio falls below the current marginal cost, with the terminal period as fallback:

q(i)=\min\bigl(\{n+1\}\cup\{t\in E_i:t<n+1,\ r_i(t)<c_i\}\bigr).

The goal asserts that the full candidate minimum is attained there and that the algorithm's resulting assignment equals $G(i)$ :

\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=c_i[D(i)-D(q(i))]+G(q(i)),

G(i)=\begin{cases}f_i+c_i[D(i)-D(q(i))]+G(q(i)),&d_i>0,\\ \min\{G(i+1),f_i+c_i[D(i)-D(q(i))]+G(q(i))\},&d_i=0.\end{cases}

This states the mathematical choice and value; it does not assert a time bound. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S150

Significance

The result reduces a finite dynamic-programming minimum to the vertices of a lower envelope and gives an explicit threshold for choosing a minimizing vertex. It explains which future production period the backward recursion may select even when marginal costs are negative or some intermediate demands are zero. The paper uses ordered slopes to implement the selection efficiently; a solver proving the statements here establishes the mathematical correctness of that selection independently of a particular list representation. Wagelmans, Van Hoesel and Kolen (1992), pp. S148–S150

The paper's result is proved in print. The Lean statements are open proof obligations in this proposal. A complete development would add reusable finite lower-envelope facts, including vertex dominance and the order of adjacent slopes, as well as a machine-checked treatment of the zero-demand tie convention. The previously published forward-algorithm items do not supply these backward-recursion facts.

Difficulty

A candidate point can have a smaller value $G(t)$ than a neighboring point yet still fail to minimize $c_i[D(i)-D(t)]+G(t)$ for a given $c_i$ . Comparing raw values alone therefore cannot identify the selected period. The lower envelope must retain exactly the points that can support a line of slope $c_i$ , and their consecutive ratios must be ordered. Zero demand creates repeated abscissae; without a representative rule, a ratio may have denominator zero and the successor is ambiguous. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization scope

Periods are natural numbers starting at $1$ ; $n+1$ is the terminal sentinel. Demands, setup costs, marginal costs and values are real numbers. Finite minima use attained Finset.inf', with nonempty domains. The effective score omits the common setup cost $f_i$ . No sign restriction is imposed on $c_i$ . The efficient set is determined by a finite chord test for lower-envelope vertices: points on a chord are excluded, and at identical abscissa and height the earliest period is retained. This makes explicit the paper's zero-demand replacement convention on p. S150. The successor is used only on nonsentinel efficient periods; there its denominator is positive. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

The algorithm's printed Iterations use $d_{1n}$ where $d_{in}$ is required; the Lean statement uses $D(i)-D(q(i))=d_{i,q(i)-1}$ , matching the preceding display and the numerical table. The zero-demand branch explicitly includes skipping setup. The selector is the ratio-threshold rule, rather than an argmin, and the efficient set is the actual lower-envelope vertex set rather than all periods. A finite zero-demand example and Tables I–II are used as verification data. The paper's $O(n\log n)$ bound, the binary-search implementation, the amortized list updates, the $O(n)$ Wagner–Whitin specialization and the final production-plan construction are outside this mission: they require additional algorithm-state and cost-model statements. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S152

Selected references

A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1 (1992), S145–S156. DOI: 10.1287/opre.40.1.S145

8 thms2 active usersReviewed

Completed

Bandit Algorithms Dynamic Programming Probability·Captain: mikedeng1

Multi-armed Bandits and the Gittins Index: With Per-Project Horizons the Maximal M-Process Reward Is K − ∫_M^K ∏ᵢ ∂φᵢ/∂m dm and the Gittins Index Rule Attains ItResearch Paper

Motivation

The multi-armed bandit problem asks how to allocate effort sequentially among $N$ independent projects, only one of which can be worked on at a time, so as to maximise expected total discounted reward. It is the model behind research planning, clinical-trial allocation and job scheduling, and it is the prototypical example of a Markov decision problem whose state space grows exponentially in $N$ yet whose optimal policy is simple. Gittins and Jones (1974) and Gittins (1979) showed that each project can be given an index computed from that project alone, and that it is optimal always to engage a project of largest index. P. Whittle's 1980 paper gave a short proof of this theorem by attaching a retirement option to the process, and extended it to projects with individual horizons.

Timeline:

1974–1979. Gittins and Jones introduce the dynamic allocation index; Gittins (1979, JRSS B) proves its optimality by an interchange argument.
1980. Whittle (JRSS B 42, 143–149) introduces the $M$ -process, proves the finite-horizon formula (Theorem 1 below), derives the infinite-horizon identity (12), and extends the result to superprocesses (Theorem 2).
1980s–2010s. Weber (1992) and Tsitsiklis (1994) give further short proofs; the index theory is collected in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (Wiley, 2011).

Setting

There are $N$ projects. Project $i$ has a state $x_i$ in a measurable space $X_i$ . Engaging project $i$ in state $x_i$ earns the expected reward $R_i(x_i)$ and moves its state by a Markov kernel $P_i$ ; the other projects' states do not change. Rewards are discounted by $\beta$ , $0 \le \beta < 1$ , and bounded:

k(1-\beta) \le R_i(x_i) \le K(1-\beta). \qquad (1)

The operator $L_i\theta(x) = R_i(x_i) + \beta\,\mathbb E[\theta(x(t+1)) \mid x(t) = x, i(t) = i]$ evaluates engaging project $i$ for one step.

In the $M$ -process one may also retire at any time for the reward $M$ . Its value $F(x, M)$ solves $F = \max(M, \max_i L_i F)$ (4), and the value $\varphi_i(x_i, M)$ of the single-project $M$ -process solves $\varphi_i = \max(M, L_i\varphi_i)$ (9).

With per-project horizons, project $i$ may be operated at most $s_i$ more times. A project with $s_i > 0$ is active, and $D_i s$ lowers $s_i$ by one. The single-project value $\varphi_i(x_i, s_i, M)$ satisfies $\varphi_i(x_i, 0, M) = M$ and

\varphi_i(x_i, s_i, M) = \max\big[M,\ R_i(x_i) + \beta\,\mathbb E\,\varphi_i(x_i(t+1), s_i - 1, M)\big]. \qquad (14)

$F(x, s, M)$ is the maximal expected reward of the $M$ -process under these limits. The index $M_i(x_i, s_i)$ is the infimal $M$ with $\varphi_i(x_i, s_i, M) = M$ , and $v_i = (1-\beta)M_i$ is the Gittins index. Finally

\hat F(x, s, M) = K - \int_M^K \prod_i \frac{\partial \varphi_i(x_i, s_i, m)}{\partial m}\, dm. \qquad (13)

Formalization targets

Goal: Theorem 1 (p. 147)

F(x, s, M) = \hat F(x, s, M),

and $F$ is attained by the policy that, at $(x, s)$ , engages a project $i$ maximising $M_i(x_i, s_i)$ when this maximum exceeds $M$ , and otherwise retires. The Lean goal has three conjuncts: $F = \hat F$ , every measurable index rule (any tie-breaking) earns $F$ , and no feasible measurable Markov policy earns more than $F$ .

Milestones (the steps of the proof)

Lemma 1 (p. 144): $F(x, M)$ is non-decreasing and convex in $M$ , equals $\Phi(x)$ for $M \le k$ and $M$ for $M \ge K$ .
(18) (p. 147): $P_i(x,s,M) = \prod_{j \ne i}\partial\varphi_j/\partial M$ is a distribution function in $M$ , equal to $1$ for $M \ge M_{(i)} = \max_{j\ne i} M_j$ .
(19) (p. 147): $\hat F = \varphi_i P_i + \int_M^\infty \varphi_i\, d_m P_i$ .
(21) (p. 148): $\hat F \ge L_i\hat F$ , with equality if $M_i = \max_j M_j \ge M$ .
Retirement case (p. 148): if $\max_j M_j \le M$ then $\hat F = M$ .
(16) (p. 147): $\hat F = \max(M, \max_i L_i\hat F)$ and $\hat F(x, 0, M) = M$ .

Further item

Infinite horizon (p. 148, formula (12) of p. 146): $F(x, M) = K - \int_M^K \prod_i \partial\varphi_i(x_i, m)/\partial m\, dm$ , with the index rule optimal.

Significance

Theorem 1 reduces an $N$ -project problem, whose state space is a product, to $N$ one-dimensional retirement problems. The formula (13) shows more than optimality of the index rule: the derivative of the multi-project value in $M$ is the product of the single-project derivatives, so the multi-project value is computable from the projects separately. The finite-horizon version gives an inductive argument that avoids the interchange arguments of earlier proofs, and the infinite-horizon identity (12) follows from it.

The result is classical and proved. What this mission adds is a machine-checked version in a generality not yet on the platform: heterogeneous projects (each with its own kernel and reward on its own measurable space), a retirement option, and per-project horizons. The platform already has a proved index theorem for identical arms sharing one kernel and reward without retirement, BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári, Theorem 35.9), single-arm retirement values in charge form (GittinsFiniteRetirementValue), and open Beta–Bernoulli special cases from Bäuerle–Rieder (MDPFinance.InfiniteHorizonApplications.proposition_7_6_7, proposition_7_6_9, theorem_7_6_10). None of these states Theorem 1, formula (13) or formula (12).

Difficulty

The obvious approach, value iteration on the product state space, gives existence of an optimal policy but says nothing about its structure. The content of Theorem 1 lies in the identity of a multi-dimensional value with an integral of a product of one-dimensional derivatives. Verifying it requires differentiating single-project values in $M$ (they are convex, but have a kink exactly at the index, where the choice of one-sided derivative matters), an integration by parts against a Stieltjes measure in $M$ , and an exchange of the expectation over the next state with the $M$ -integral. The exhausted projects ( $s_i = 0$ ) and the boundary $M = M_i$ need separate care in every step.

Formalization scope

Projects are indexed by Fin N (0-based; the paper uses $1, \dots, N$ ). State spaces are arbitrary measurable spaces; no finiteness or countability is assumed. Kernels are Markov, rewards measurable and bounded as in (1), and $0 \le \beta < 1$ (β = 0 is allowed). $k$ and $K$ are any constants satisfying (1).
Budgets are s : Fin N → ℕ; $D_i s$ is Function.update s i (s i - 1) and is only applied to active projects.
$F(x, s, M)$ , the "maximal reward", is the backward-induction value: $F(x, 0, M) = M$ and $F = \max(M, \max_{i\ \text{active}} L_iF)$ , defined by recursion on $\sum_i s_i$ . It is not defined through $\hat F$ , the index, or a policy. $\varphi_i(x_i, s_i, M)$ is defined by (14) with $\varphi_i(x_i, 0, M) = M$ .
$\partial/\partial m$ is the right derivative. Since the $\varphi_i$ are convex in $m$ , this changes (13) at no point, and it makes (18) hold at the kink $M = M_{(i)}$ .
The index of an exhausted project is the paper's $-\infty$ . In Lean index takes the junk value 0 there; every use (the index rule, $M_{(i)}$ , $\max_j M_j$ ) ranges over active projects only.
Policies are Markov in $(x, s, M)$ , valued in Option (Fin N) (none = retire), feasible (they engage only active projects) and measurable (each decision set is measurable), so that their expected rewards are well defined. The index rule allows arbitrary tie-breaking; the goal quantifies over every such rule.
Infinite-horizon values (Lemma 1, the further item) are any bounded measurable solutions of (2), (4), (9); such solutions exist and are unique by the contraction property.
(19) uses the Stieltjes measure of any monotone right-continuous function agreeing with $P_i$ , and integrates over $m > M$ .
Trivializing formalizations are excluded: $F$ is not $\hat F$ by definition, exhausted projects cannot be engaged by the index rule, and maxima over $i$ are seeded with $M$ rather than taken as a junk real supremum.

A complete development needs measurability of the recursive values, convexity of $\varphi_i$ in $M$ with one-sided derivatives, Lebesgue–Stieltjes integration by parts, and Fubini for kernels. Convexity of finite-horizon retirement values and the integration-by-parts identity are reusable beyond this mission. Contributions to any milestone, and sorry-free lemmas on these ingredients, are welcome.

Selected references

P. Whittle, Multi-armed Bandits and the Gittins Index, J. R. Statist. Soc. B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, J. R. Statist. Soc. B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

An Introduction to Timetabling 3: Course Scheduling with Unavailabilities and Preassignments in p Periods Is Equivalent to p-Coloring the Nodes of a GraphResearch Paper

Motivation

Universities schedule lectures and examinations every term. When students choose their courses freely, with no fixed curriculum, the basic requirement is that no student is asked to attend two lectures at the same time. On top of this come local constraints: a course cannot take place at some periods (its teacher or a suitable room is unavailable), and some lectures are fixed in advance at a given period. D. de Werra's invited review An introduction to timetabling (Eur. J. Oper. Res. 19 (1985) 151–162) surveys the graph models of these problems. Its §3.1 shows that course scheduling, with unavailabilities and preassignments, is exactly a node colouring problem. This reduction is the standard starting point for graph colouring heuristics in timetabling, including the examination timetabling literature.

Setting

A course scheduling instance has $q$ courses $K_b$ , course $K_b$ consisting of $k_b$ lectures $l_a$ , and $r$ students; student $i$ takes a set $T_i$ of courses. There are $p$ periods.

The lecture graph $G$ has one lecture-node $m_{ab}$ for each lecture $l_a$ of each course $K_b$ . Two lecture-nodes of the same course are adjacent. Two lecture-nodes of distinct courses $K_b$ , $K_{\bar b}$ are adjacent whenever some student takes both courses.

A feasible course schedule in $p$ periods assigns a period $s(l) \in \{1,\dots,p\}$ to each lecture so that two lectures of one course are at different periods and no student has two lectures at the same period.

A course scheduling problem with unavailabilities and preassignments (CSUP) adds, for each course $K_b$ , a set $U_b$ of forbidden periods, and for some lectures $l$ a prescribed period $\bar k(l)$ . A solution is a feasible schedule with $s(l) \notin U_b$ for every lecture $l$ of $K_b$ and $s(l) = \bar k(l)$ for every preassigned lecture.

The graph $\hat G$ of a CSUP adds one period-node $k$ per period to $G$ . All pairs of period-nodes are adjacent. A lecture-node of $K_b$ is adjacent to period-node $k$ if $k \in U_b$ . A lecture-node of a lecture preassigned to $\bar k$ is adjacent to every period-node $k \neq \bar k$ .

A node colouring with $p$ colours assigns one of $p$ colours to each node so that adjacent nodes get different colours.

Formalization targets

Goal: Proposition 3.1

\text{the CSUP } P \text{ has a solution in } p \text{ periods} \iff \hat G(P) \text{ has a node colouring with } p \text{ colours.}

Milestones

§3.1 (p. 157). Without unavailabilities and preassignments, the feasible schedules in $p$ periods are exactly the node colourings of $G$ with $p$ colours.
Figure 4 (p. 157). For courses $K_1,K_2,K_3$ with $1,2,2$ lectures, student 1 taking $K_1,K_2$ and student 2 taking $K_2,K_3$ , the printed schedule in $4$ periods is feasible.
Proof of Proposition 3.1 (p. 158). Every colouring of $\hat G$ with $p$ colours gives a solution in which lecture $l_a$ of $K_b$ is at period $k$ exactly when $m_{ab}$ has the colour of period-node $k$ , and every solution arises in this way from some colouring.
Proposition 3.2 (p. 158). Let $H$ be a graph on lecture-nodes and a clique of $p$ period-nodes, with some lecture-nodes precoloured consistently with the colours of period-nodes. Removing the precoloured nodes and joining their neighbours to the matching period-nodes gives a graph $\hat G'$ with

H \text{ has a } p\text{-colouring respecting the precolouring} \iff \hat G' \text{ is } p\text{-colourable.}

Significance

The result. Proposition 3.1 turns a family of constrained timetabling problems into one well-studied problem. Any exact or heuristic method for node colouring (sequential colouring, DSATUR, implicit enumeration; §3.2 of the paper) applies directly to course scheduling with forbidden and fixed periods, and lower bounds on the chromatic number become lower bounds on the number of periods. Proposition 3.2 adds that preassignments cost nothing for node colouring: a precoloured instance is again a plain colouring instance. For edge colouring the paper contrasts this with the NP-completeness of precoloured edge colouring.

The formalization. The results are proved on the page in a few lines and are not machine-checked anywhere. This mission makes the reduction precise. It writes out the graph $\hat G$ as a definition, isolates the consistency condition that Proposition 3.2 needs, and states the correspondence between colourings and schedules in a form other formal timetabling and scheduling developments can use. The definitions of course instances, CSUP and $\hat G$ can serve formal work on examination timetabling and on the complexity of timetabling problems.

Difficulty

The forward direction of Proposition 3.1 is direct: colour each lecture-node with its period and each period-node with itself. The converse is where care is needed. A colouring of $\hat G$ need not give period-node $k$ the colour $k$ ; the colours of the period-nodes can be any permutation of the palette. The schedule must therefore be read through the colours of the period-nodes, and the fact that the $p$ period-nodes form a clique is what makes this well defined.

For Proposition 3.2, the obvious reading of the page is false. If two adjacent lecture-nodes are precoloured with the same colour, no colouring respects the precolouring, yet removing both nodes deletes the edge between them and the reduced graph may still be colourable. The same happens when a node is precoloured with the colour of a period-node it is adjacent to. The proposition therefore needs a consistency condition the page leaves implicit. The page's "1–1 correspondence" between colourings fails when precolours are fixed colours of the palette, since $\hat G'$ 's colourings can permute the colours of the period clique; the target is the equivalence of the proposition.

Formalization scope

Courses, students, lectures of a course and periods are indexed from $0$ (Fin q, Fin r, Fin (lectures b), Fin p). A lecture is a dependent pair Σ b, Fin (lectures b), and the nodes of $\hat G$ are Lecture ⊕ Fin p. Graphs and colourings are Mathlib's SimpleGraph, SimpleGraph.Coloring and SimpleGraph.Colorable. Unavailability is per course and preassignment per lecture, as on the page. The set-valued constraint of the Figure 5 example ("1 lecture of $K_3$ at period 1 or 2") is not modelled. Feasibility includes the clique on the lectures of each course even when no student takes the course, because the page's graph contains it. $p = 0$ is allowed.

The paper states Proposition 3.1 as "one can construct a graph $\hat G$ such that …". The existential form is trivially true (pick a complete graph on $p+1$ nodes or an edgeless graph according to the answer), so the goal is stated about the specific graph csupGraph P built in the proof.

Proposition 3.2 is stated for any graph whose period-nodes form a clique, with two disclosed consistency hypotheses: no precoloured node is adjacent to its own period-node, and no two adjacent nodes are precoloured with the same period-node's colour. A sanity file shows that the equivalence fails without them. "Precoloured" means "receives the colour of period-node $k$ ", the reading of the proof of Proposition 3.1.

Not targeted: the NP-completeness remarks (cited, not proved), the heuristics of §3.2–§3.4, and the hypergraph classroom model of §3.5, whose "1–1 correspondence" has the same palette-permutation issue as Proposition 3.2.

Contributions welcome: proofs of the milestones and the goal, and general lemmas about colourings of graphs containing a clique of size equal to the number of colours.

Selected references

D. de Werra, An introduction to timetabling, European Journal of Operational Research 19 (1985) 151–162. https://doi.org/10.1016/0377-2217(85)90167-5
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (NP-completeness of graph $p$ -colourability, reference [13] of the paper).
D. Brélaz, New methods to color the vertices of a graph, Communications of the ACM 22 (1979) 251–256. https://doi.org/10.1145/359094.359101

7 thms2 active usersReviewed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Negative Dynamic Programming IV: Switching at Each Stage to the Policy with the Better Continuation Return Does at Least as Well as Both PoliciesResearch Paper

Motivation

Policy improvement is one of the two classical ways of solving a Markov decision problem: start from a policy, compute its return, and change the decision wherever another action looks better against that return. Howard (1960, Dynamic Programming and Markov Processes) introduced it for finite state and action spaces, and Blackwell (1965) proved it for discounted problems on Borel spaces. A related routine combines two given policies instead of improving one: at each state, follow whichever policy has the larger return there. Eaton and Zadeh (1962, J. Basic Eng. Ser. D 84, 23–29) proved that this combination of two stationary policies is at least as good as both in the negative case with finite state and action spaces (as credited on p. 889 of Strauch's paper).

Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966) 871–890) treats the negative case: all one-stage returns are non-positive (costs) and there is no discounting. This case covers stochastic shortest-path and optimal-stopping problems with positive costs, where expected total returns may be $-\infty$ and the contraction arguments of the discounted case are not available. Section 9 of the paper shows that both improvement routines remain valid there, for arbitrary randomized history-dependent policies on Borel spaces, and that they fail in the positive case (Examples 4.2 and 9.1 of the paper).

Timeline:

1960, Howard: policy iteration for finite state and action spaces.
1962, Eaton and Zadeh: the two-policy combination for finite negative problems.
1965, Blackwell: both routines for discounted problems with Borel state and action spaces.
1966, Strauch, §9: Howard's routine (Theorem 9.2), the history-dependent switching theorem (Theorem 9.3) and its Markov and stationary forms (Corollaries 9.1, 9.2) in the negative case on Borel spaces.

Setting

The state space $S$ and the action space $A$ are non-empty Borel sets. The law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$ , and the return $r(s,a,t)$ is a Borel function with $-\infty<r\le 0$ whose one-step expectation $\int r(s,a,t)\,q(dt\mid s,a)$ is finite at every $(s,a)$ . There is no discounting ( $\beta=1$ ).

A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the $n$ -th action $a_n$ from a probability kernel $\pi_n(\cdot\mid h)$ that may depend on the whole history $h=(s_1,a_1,\dots,a_{n-1},s_n)$ . The expected return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\pi_1q\cdots\pi_nqr\,(s)\in[-\infty,0],

the sum of the expected one-stage returns. For a terminal reward $w\le 0$ that depends on the history $(s_1,a_1,\dots,s_{n+1})$ , $I_n(\pi,w)$ is the expected return of following $\pi$ for $n$ stages and then receiving $w$ .

Given two policies $\sigma$ and $\tau$ , their continuation returns at a history $h=(s_1,\dots,s_n)$ are

u_n(h)=\sum_{j=n}^{\infty}\sigma_nq\cdots\sigma_jqr\,(h),\qquad v_n(h)=\sum_{j=n}^{\infty}\tau_nq\cdots\tau_jqr\,(h),

the expected returns from stage $n$ on if $\sigma$ , respectively $\tau$ , is used from $h$ on with its own kernels fed the full history. The switching policy $\pi$ uses $\sigma_n$ on $B_n=\{u_n>v_n\}$ and $\tau_n$ on its complement. In Lean these objects are contReturn, IsSwitch, wmax (for $w_n=\max(u_n,v_n)$ ), InH (for $I_n(\pi,w)$ ) and I, in the namespace NegativeDP.Switching.

Formalization targets

Goal: Theorem 9.3 (negative case)

For all policies $\sigma,\tau$ , the switching rule defines a policy $\pi$ , and every such $\pi$ satisfies

I(\pi)\ge\max\big(I(\sigma),I(\tau)\big)\quad\text{at every initial state.}

Milestones (proof of Theorem 9.3, p. 888)

With $w_n=\max(u_n,v_n)$ and $\pi$ the switching policy:

I_0(\pi,w_1)=w_1=\max(I(\sigma),I(\tau)),

w_n=\pi_n(r+u_{n+1})\text{ on }B_n,\qquad w_n=\pi_n(r+v_{n+1})\text{ on }B_n^c,

w_n\le\pi_n(r+w_{n+1}),\qquad I_{n-1}(\pi,w_n)\le I_n(\pi,w_{n+1}),\qquad I_{n-1}(\pi,w_n)\ge\max(I(\sigma),I(\tau)).

Further results (not milestones)

Theorem 9.2 (Howard): if $I(f,\pi)\ge I(\pi)$ then $I(f^{(\infty)})\ge I(\pi)$ . Corollary 9.1: the switching theorem for Markov policies, comparing $I(^{n-1}\sigma)$ and $I(^{n-1}\tau)$ at the current state. Corollary 9.2 (Eaton–Zadeh): for stationary $f^{(\infty)},g^{(\infty)}$ , the rule $h=f$ where $I(f^{(\infty)})\ge I(g^{(\infty)})$ and $h=g$ elsewhere satisfies $I(h^{(\infty)})\ge\max(I(f^{(\infty)}),I(g^{(\infty)}))$ .

Significance

Theorem 9.3 yields an improvement step that needs only the returns of two policies, not an optimality equation or a value function. Its Markov and stationary forms give policy-combination results usable for stochastic shortest-path and positive-cost problems, and together with Theorem 9.2 they justify policy-iteration schemes in the negative case on general state spaces. Example 9.1 of the paper shows that no comparable routine exists in the positive case, so the sign assumption is essential.

The results are proved in the paper. No machine-checked version of any of them exists, for the negative case or on Borel spaces; the related items on Prove2Me treat finite or discounted models. This mission produces the statements in Lean over Blackwell's published model of history-dependent plans, a construction of continuation returns from an arbitrary history, and terminal rewards that depend on the whole history.

Difficulty

The argument of the discounted case, which passes to the limit through the vanishing tail $\beta^n w_n$ , is not available: with $\beta=1$ the terminal term does not vanish, and returns may be $-\infty$ . Comparing $u_n$ and $v_n$ at the current state only is not enough either: for history-dependent policies the continuation returns depend on the whole history, and the switching set $B_n$ must be shown to be Borel in the history before the switching rule is even a policy. The induction also requires integrating extended-real terminal rewards against the history law and identifying the integral of the one-step operator with the next-stage expected return.

Formalization scope

Borel sets are non-empty standard Borel types; Baire functions are measurable functions. Policies are Blackwell's DiscountedDP.Stationary.Plan (one Markov kernel per decision, on Hist S A n). Decisions are numbered from $0$ in Lean, so Lean's index $n$ is the paper's stage $n+1$ .
Only the negative case is formalized ( $r\le0$ real-valued, $q$ -integrable at every $(s,a)$ , $\beta=1$ ). The paper states Theorem 9.3 for the discounted and negative cases; the discounted case is not part of this mission.
Returns lie in $[-\infty,0]$ and are EReal values computed as minus the lintegral of the loss $-r$ ; Bochner integrals and toReal are never used, so a return of $-\infty$ is not silently turned into $0$ . $I(\pi)$ is the sum of stage expectations, equal to $e_\pi\rho$ by monotone convergence.
Terminal rewards are read through their negative parts; they are applied only to $w_n\le 0$ .
The switching policy is characterized by the predicate IsSwitch, not constructed. A statement "every switching policy satisfies the bound" would hold vacuously if no plan satisfied the rule; the goal therefore also asserts that a switching plan exists, which is the content of the paper's "define $\pi$ by". The same pattern is used in Corollaries 9.1 and 9.2 (the rule defines a measurable decision rule).
Ties $u_n=v_n$ go to $\tau$ in Theorem 9.3, and $I(^{n-1}\sigma)=I(^{n-1}\tau)$ to $g_n$ in Corollary 9.1 (strict $>$ as printed); in Corollary 9.2 ties go to $f$ (non-strict $\ge$ as printed).
Lemma 3.1 ( $I_n(\pi,0)\downarrow I(\pi)$ ), used in the last step of the proof, is posed in mission I of this series and not repeated here.

Contributions welcome: measurability of continuation returns in the history (needed for the existence part), the identification of the history law with the continuation law from the initial state, and a Chapman–Kolmogorov identity for the continuation kernels. These are reusable in any development on history-dependent policies over Borel spaces.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
J. H. Eaton and L. A. Zadeh, Optimal pursuit strategies in discrete-state probabilistic systems, J. Basic Eng. Ser. D 84 (1962) 23–29 (reference [7] of Strauch's paper).
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.

9 thms2 active usersReviewed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Negative Dynamic Programming I: With Non-Positive Rewards, If an Optimal Policy Exists Then an Optimal Stationary Policy ExistsResearch Paper

Motivation

Many sequential decision problems accumulate costs that are never recovered: inventory holding and shortage costs, waiting times, the expected number of steps until a target is reached. Written as rewards, these are non-positive rewards summed over an infinite horizon without discounting. Ralph Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966), doi:10.1214/aoms/1177699369) is the foundational treatment of this negative case on general Borel state and action spaces. It complements Blackwell's treatment of the discounted case (Blackwell 1965) and of the positive bounded case (Blackwell 1964, mimeographed), and it sets out which conclusions of the discounted theory survive when rewards are non-positive and undiscounted.

A central question in that theory is how simple an optimal policy can be taken to be. A policy may in principle randomize and consult the entire past history. Strauch showed that in the negative case, whenever an optimal policy exists, an optimal stationary one exists, using one measurable decision rule at every stage. This mission formalizes that result together with the reduction from general policies to semi-Markov ones on which its proof rests.

Timeline. Blackwell (1965) proved that in the discounted case a stationary optimal policy exists whenever an optimal policy does, and gave an example showing that Markov policies need not suffice on Borel spaces. Strauch (1966) proved the corresponding statement for the negative case and proved that semi-Markov policies, which remember the initial state as well as the current one, are enough.

Setting

A negative dynamic programming problem consists of non-empty Borel sets $S$ (states) and $A$ (actions), a law of motion $q(\cdot\mid s,a)$ , which is a probability kernel from $S\times A$ to $S$ , and a Borel return function $r(s,a,t)$ with

r\le 0,\qquad r>-\infty,\qquad \int r(s,a,t)\,dq(t\mid s,a)>-\infty\ \ \text{for all }(s,a).

There is no discounting. A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the action $a_n$ at stage $n$ from a probability kernel $\pi_n(\cdot\mid h_n)$ , where $h_n=(s_1,a_1,\dots,a_{n-1},s_n)$ is the history. A policy is Markov if $a_n=f_n(s_n)$ for Borel maps $f_n:S\to A$ , semi-Markov if $a_n=g_n(s_1,s_n)$ for Borel $g_n$ , and stationary, written $f^{(\infty)}$ , if $a_n=f(s_n)$ for one Borel rule $f$ . Random Markov and random semi-Markov policies draw $a_n$ from kernels in $s_n$ , respectively $(s_1,s_n)$ .

The expected total return from the initial state $s$ is

I(\pi)(s)=\sum_{n=1}^{\infty}\mathbb E^{\pi}_{s}\,r(s_n,a_n,s_{n+1})\in[-\infty,0],

the optimal return is $v^*(s)=\sup_\pi I(\pi)(s)$ over all policies, and $\pi^*$ is optimal if $I(\pi^*)(s)\ge v^*(s)$ for every $s$ . For a Borel rule $f$ , the operator $T$ acts on non-positive Borel functions $u$ by

Tu(s)=\int r(s,f(s),t)+u(t)\,dq(t\mid s,f(s)).

The namespace is NegativeDP.Stationary. The objects above are Problem, Plan, I, In, vstar, IsOptimal and T.

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

\big(\exists\,\pi^*\ \ I(\pi^*)\ge v^*\big)\ \Longrightarrow\ \exists\,f\ \text{Borel},\ \ I(f^{(\infty)})\ge v^* .

Milestones

Lemma 2.1: for a kernel $q(\cdot\mid x)$ and a Borel $u\le 0$ on $X\times Y$ there is a Borel $f$ with $u(x,f(x))\ge\int u(x,y)\,dq(y\mid x)$ .
Lemma 3.1 (N): $I_n(\pi)\downarrow I(\pi)$ .
Lemma 4.1 (a), (b): policies built from the conditional laws of $a_n$ given $(s_1,s_n)$ , respectively given $s_n$ under an initial law $p$ , reproduce the laws of $(s_1,s_n,a_n,s_{n+1})$ , respectively the $p$ -averaged laws of $(s_n,a_n,s_{n+1})$ .
Theorem 4.1: for every policy $\pi$ and initial law $p$ there are a random semi-Markov $\pi^*$ and a random Markov $\pi^{**}$ with $I(\pi)=I(\pi^*)$ and $pI(\pi)=pI(\pi^{**})$ for every return function.
Theorem 4.2 (N): if $I(\pi^n\sigma)\ge I(\sigma)$ for all large $n$ , then $I(\pi)\ge I(\sigma)$ .
Theorem 4.3 (N): a semi-Markov $\tau$ with $I(\tau)\ge I(\pi)$ and a Markov $\sigma$ with $pI(\sigma)\ge pI(\pi)$ .
Theorem 5.1 (N), parts (a)–(g): the properties of $T$ , including $TI(\pi)=I(f,\pi)$ , $TI(f^{(\infty)})=I(f^{(\infty)})=\lim_n T^n0$ and $I_n(\pi,v)=T_1\cdots T_nv$ for Markov $\pi$ .

Significance

Theorem 8.3 reduces a search over all randomized, history-dependent policies to a search over single measurable decision rules, whenever an optimal policy exists at all. It underlies policy iteration and the stationary-policy conclusions of the later negative-programming literature, and it shows that the negative case behaves like the discounted case on this point. In the positive case only a weaker statement holds. The reduction of §4 (Theorems 4.1–4.3) is reused throughout the paper: Theorem 8.1 on $(p,\varepsilon)$ -optimal Markov policies starts from Theorem 4.3, and the value-iteration results of §9 use Lemma 3.1 and Theorem 5.1.

All results in this mission are proved in the paper. None of them has a machine-checked proof that we know of. The closest formal result is part 2 of Bertsekas's Proposition 7, formalized in an abstract monotone-mapping model (MonotoneDP.Increase.prop7_optimal_stationary_criterion). There, policies are sequences of selectors, so it contains neither the measure-theoretic reduction from randomized history-dependent policies nor Borel state spaces. The formal work here is to build the law of the controlled process on Borel spaces, carry out the conditional-distribution argument of Theorem 4.1, and combine it with the operator calculus of §5.

Difficulty

The obvious argument starts from an optimal $\pi^*$ , takes its first decision rule $f$ , and shows that $f^{(\infty)}$ is optimal. That fails for a general $\pi^*$ , because its first action may be randomized and its later actions may depend on the entire history. One first needs Theorem 4.3, which says a non-random semi-Markov policy is at least as good. That theorem needs two things. One is Theorem 4.1, which replaces a history-dependent policy by one built from conditional distributions of actions, and this requires disintegration of measures on Borel spaces. The other is the measurable selection of Lemma 2.1, which the paper takes from Theorem 2 of Blackwell and Ryll-Nardzewski 1963, applied stage by stage, with Theorem 4.2 to pass to the limit. On Borel spaces Markov policies are not enough (Blackwell's example, Example 4.1 of the paper), so the semi-Markov step cannot be skipped. Returns can equal $-\infty$ , and every limit exchange has to respect that.

Formalization scope

Borel sets are non-empty standard Borel types and Baire functions are measurable functions. The return $r$ is real-valued, non-positive and integrable under $q(\cdot\mid s,a)$ for every $(s,a)$ . Returns live in the extended reals. $I(\pi)$ , $I_n(\pi,v)$ , $T$ and all integrals of non-positive functions are computed as minus lower Lebesgue integrals of the corresponding losses in $[0,\infty]$ , so a return of $-\infty$ is never collapsed to $0$ . $I(\pi)$ is the sum of stage expectations, which equals the paper's expectation of the total return by monotone convergence. $v^*$ is the supremum over every randomized history-dependent plan. Restricting it to Markov or stationary policies would make the goal weaker, and that encoding is ruled out. Only the negative case ( $r\le 0$ , $\beta=1$ ) is formalized. Results the paper labels "D, P, N" or "D, N" appear here in their N form.

Explicit choices:

Lean numbers decisions from $0$ . Hist S A n is the paper's $H_{n+1}$ and the plan's kernel κ n is $\pi_{n+1}$ .
The objects $\pi^*$ and $\pi^{**}$ of Lemma 4.1 are defined in the paper's proof as conditional distributions. Here their defining property is a hypothesis: for every initial state, or after averaging over $p$ , the joint law of $(s_n,a_n)$ is the law of $s_n$ followed by the kernel.
In Theorem 4.1, "for any return function $r$ " is a quantifier over every negative problem with the same law of motion, placed after the choice of $\pi^*$ and $\pi^{**}$ .
In Theorem 5.1 (b), $u+c$ is required to lie in $M(S)$ . In (d), the increasing part holds only on $\{\sup_jTu_j>-\infty\}$ .
In Theorem 5.1 (f), $T$ is applied to $I(\pi)$ for a general plan with no measurability hypothesis. The lower integral is defined for every function.

Infrastructure needed: the law of the controlled process (built here by iterated kernel composition, as in the published DiscountedDP.Stationary model), disintegration of kernels on standard Borel spaces, a measurable selection theorem of Blackwell–Ryll-Nardzewski type, and monotone convergence for lower integrals. The disintegration and selection results are reusable well beyond this paper. Contributions to Theorems 4.1 and 4.3 are especially welcome, since missions II–IV of this series build on them.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. Blackwell and C. Ryll-Nardzewski, Non-existence of everywhere proper conditional distributions, Ann. Math. Statist. 34(1) (1963) 223–225. https://doi.org/10.1214/aoms/1177704259

16 thms2 active usersReviewed

Completed

Analysis Optimization·Captain: mikedeng1

Vertical Integration and Antitrust Policy: Integrating Successive Monopolies Lowers the Final Price and Raises Output, Joint Profit and Consumer SurplusResearch Paper

Motivation

In 1950 the United States Supreme Court appeared to be moving toward treating corporate integration, horizontal or vertical, as illegal per se under the antitrust laws. Joseph J. Spengler's note in the Journal of Political Economy argued that this conflates two different things: horizontal integration can suppress competition, but vertical integration, the joining of successive stages of production under one owner, can lower prices when the stages are already imperfectly competitive. The note is the standard origin of what industrial organization now calls double marginalization: when a monopolist upstream sells to a monopolist downstream, each adds its own markup, and the final price is higher than a single integrated monopolist would charge.

The argument underlies the modern economics of vertical mergers and vertical restraints (resale price maintenance, two-part tariffs, franchise fees) and the supply-chain coordination literature in operations research, where a wholesale-price contract between a supplier and a retailer reproduces the same distortion.

A short timeline: Cournot (1838, Chapter IX) analysed complementary monopolists selling inputs to a common product; Spengler (1950) gave the successive-monopoly version and drew the antitrust conclusion; Tirole's textbook (1988, §4.2) made it the canonical example of vertical externalities; Cachon and Lariviere (2005) and the coordination literature studied the same inefficiency in newsvendor supply chains.

Setting

A product passes through three successive stages $A\to B\to C$ before reaching consumers. Production uses fixed proportions: one unit of stage A's product goes into one unit of B's, and one unit of B's into one unit of C's, so all stages handle the same quantity. Each stage has a constant unit variable cost $V_a,V_b,V_c$ (marginal cost equal to average variable cost at every relevant output).

Final demand is a function $D:\mathbb R\to\mathbb R$ : $D(p)$ units of $C$ are bought at price $p$ . A firm with constant unit cost $c$ that sells at price $p$ earns the profit (return above variable outlay)

\pi_c(p)=(p-c)\,D(p),

and $p$ is a profit-maximizing price at cost $c$ when $\pi_c(x)\le\pi_c(p)$ for every $x$ .

Unintegrated chain. Stage A sells to B at a transfer price $P_a$ , B sells to C at $P_b$ . Their per-unit profits are $R_a=P_a-V_a$ and $R_b=P_b-(V_b+P_a)$ ; horizontal integration within each stage lets these be positive "monopolistic surcharges". Stage C's unit cost is $C_c=V_c+P_b$ ; it charges a profit-maximizing price $P_c$ at that cost and sells $Q=D(P_c)$ . The chain's aggregate profit is $R_aQ+R_bQ+R_cQ$ with $R_c=P_c-(V_c+P_b)$ .

Integrated firm. One firm owns all three stages. Its unit cost is $C'_c=V_a+V_b+V_c$ ; it charges a profit-maximizing price $P'_c$ at that cost and sells $Q'=D(P'_c)$ , earning $(P'_c-C'_c)\,Q'$ .

The price elasticity of demand at $p$ is $e(p)=-p\,D'(p)/D(p)$ (positive for a downward-sloping curve) and the marginal revenue is $r(p)=p+D(p)/D'(p)$ . The consumers' surplus gained when the price falls from $P_c$ to $P'_c$ is $\int_{P'_c}^{P_c}D(x)\,dx$ .

Formalization targets

Goal: vertical integration benefits producer and consumer

For every non-increasing demand curve $D$ , all unit costs $V_a,V_b,V_c$ , and all transfer prices with $R_a>0$ , $R_b>0$ , if $P_c$ is profit-maximizing at cost $V_c+P_b$ , $P'_c$ is profit-maximizing at cost $V_a+V_b+V_c$ , $D$ is differentiable at $P_c$ and $Q=D(P_c)>0$ , then

P'_c<P_c,\qquad D(P_c)<D(P'_c),\qquad R_aQ+R_bQ+R_cQ<(P'_c-C'_c)\,Q',

0<\int_{P'_c}^{P_c}D(x)\,dx,\qquad Q\,(P_c-P'_c)\le\int_{P'_c}^{P_c}D(x)\,dx.

The goal fixes no functional form and no numbers; it is the general statement behind the paper's "under all cases conceivable … within the framework here employed".

Milestones

Footnote 6, equilibrium identities. At a profit-maximizing price, $r=c$ , $e=p/(p-r)=p/(p-c)$ , and $p=c\,e/(e-1)$ when $c\ne0$ .
Section III, unitary elasticity. At zero cost, $e=1$ ; at positive cost, $p>c$ and $e>1$ .
Section III, cost raises price. For $c_1<c_2$ , profit-maximizing prices satisfy $D(p_2)\le D(p_1)$ , and $p_1<p_2$ under the goal's regularity hypotheses.
Footnote 6, straight-line demand. For $D(p)=b(a-p)$ : $p^*(c)=(a+c)/2$ , $\Delta r=2\Delta p$ , $e(p^*(c))=(a+c)/(a-c)$ , the elasticity rises relatively more than the price, and the relative rise grows with $c$ .
Figure 1. With $D_c(p)=\tfrac85(140-p)$ and $V_a=V_b=V_c=20$ : $P_c=115$ , $Q=40$ , aggregate profit $2{,}200$ ; $P'_c=100$ , $Q'=64$ , profit $2{,}560$ ; consumers' surplus rises by $780$ .

Significance

The result. The theorem shows that removing an upstream markup can only lower the final price and raise output, so that producers and consumers gain together. This is the economic content of the rule that vertical integration is not anticompetitive as such, and it is the reason modern merger guidelines credit the "elimination of double marginalization" as an efficiency of vertical mergers. Milestone 3, monotonicity of the monopoly price in cost, is the general comparative-statics fact used in tax incidence and cost pass-through.

Formalizing it. The result is classical and proved in every industrial-organization textbook, usually for linear demand. The mission states it for an arbitrary non-increasing demand curve, without concavity, continuity or uniqueness of the profit maximizer, which makes explicit which hypotheses the strict conclusions actually need. Related items on the platform formalize double marginalization in a different model, the newsvendor wholesale-price contract of Cachon and Lariviere, where the supplier-induced order quantity falls short of the integrated one; this mission covers the price-setting, deterministic-demand version.

Difficulty

The weak inequalities ( $P'_c\le P_c$ , $Q\le Q'$ , profit $\le$ ) follow from comparing the two maximization problems (the price comparison also uses $Q>0$ : if $D\equiv 0$ , every price is profit-maximizing). The strict inequalities do not: a demand curve with a kink can have the same profit-maximizing price at two different costs, so integration need not change the price at all. The strict claims therefore need a first-order condition at $P_c$ , and the argument has to combine global optimality (all prices) with local information (a derivative at one point) without assuming the profit function is concave or the maximizer unique. The consumers'-surplus clause requires a lower bound on an integral of a monotone, possibly discontinuous function.

Formalization scope

Prices, costs and quantities are real numbers; maximization is over all prices $p\in\mathbb R$ . Demand is a function $D:\mathbb R\to\mathbb R$ ; the goal assumes only that it is non-increasing (Antitone D).
Profit-maximizing prices are hypotheses (IsProfitMax D c p), never closed forms; the closed form $(a+c)/2$ appears only for straight-line demand.
The transfer prices $P_a,P_b$ are arbitrary data with positive markups; they need not be profit-maximizing for $D_a,D_b$ , which the paper draws only in its figure.
Explicit readings of the paper's prose. "Benefits both producer and consumer" and "will lower the price" become the four strict inequalities of the goal. "Aggregate profit" is the sum over the three stages, $Q[P_c-(V_a+V_b+V_c)]$ , not stage C's profit alone. Consumers' surplus "in the Marshallian sense" is the interval integral of $D$ between the two prices; footnote 5's trapezoid formula is used only for the straight line of Figure 1. Elasticity is a positive number $-pD'(p)/D(p)$ . "Relatively greater increment in the elasticity" is made exact for straight-line demand as $e(p^*(c'))/e(p^*(c))>p^*(c')/p^*(c)$ ; the literal $\Delta e/e>\Delta c/c$ is false for small $c$ . Footnote 6's $e'=(p+\Delta p)/(p-2\Delta p)$ and "approximating $3\Delta p/p$ " are a printed slip; the exact $e(p^*(c))=(a+c)/(a-c)$ is stated instead, and no approximation is formalized. Figure 1's demand line $D_c(p)=\tfrac85(140-p)$ is the line through the three points the text gives.
Added hypotheses. Differentiability of $D$ at $P_c$ and $D(P_c)>0$ , which the paper's marginal-revenue reasoning presupposes. Every statement involving elasticity or marginal revenue carries differentiability and positive demand, because Lean's deriv and division return $0$ on bad input.
Ruled out. Formalizations that hard-code linear demand in the goal, compare the integrated profit with stage C's profit alone, or prove only the weak ( $\le$ ) inequalities do not capture the result.
Sections IV and the policy remarks of Section III (rent evasion, taxes, co-operatives) are not formalized.
Only Mathlib is needed: Fermat's rule (IsLocalMax.hasDerivAt_eq_zero), interval integrals of monotone functions, and real arithmetic. Proofs of the general milestones are reusable for any monopoly-pricing comparative statics.

Selected references

J. J. Spengler, Vertical integration and antitrust policy, Journal of Political Economy 58(4), 1950, 347–352. https://doi.org/10.1086/256964
A. A. Cournot, Recherches sur les principes mathématiques de la théorie des richesses, Hachette, 1838, Chapter IX.
J. Tirole, The Theory of Industrial Organization, MIT Press, 1988, §4.2.
G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

7 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics·Captain: mikedeng1

On Cores and Indivisibility 1: The Housing Market's Game Without Side Payments Is BalancedResearch Paper

Motivation

A market in which each trader owns one indivisible good has a basic coordination question: can all goods be reassigned so that no group of traders can withdraw its own goods and improve every member's outcome? Houses are the paper's running example. Monetary transfers and fractional houses are absent, so ordinary convex allocation arguments do not describe the setting. Shapley and Scarf use games without side payments to express what each coalition of owners can achieve, and identify a balance property of this game in their Section 4 theorem (Shapley and Scarf, 1974).

The paper states that a general balanced-game theorem gives a nonempty core once balance has been established. Its Section 4 contribution is the classification of this particular housing market game. The separate top-trading-cycles construction in Section 6 gives another route to a core allocation and is the subject of the second mission in this series (Shapley and Scarf, 1974).

Setting

Let $N$ be a nonempty finite set of traders. Trader $j$ brings one indivisible item $j$ . Trader $i$ 's ranking of item $j$ is represented by a real number $a_{ij}$ . Only comparisons within one trader's row matter: $a_{ij}>a_{ik}$ means that $i$ prefers $j$ to $k$ , while equality represents indifference. No strict-preference or positivity assumption is imposed on the preference matrix $A=(a_{ij})$ .

A coalition $S\subseteq N$ can redistribute the items brought by its members. Its allocation matrix $P$ has $P_{ij}=1$ when trader $i$ receives item $j$ , and zero otherwise. An $S$ -allocation puts exactly one 1 in each column indexed by $S$ and has zeros in rows and columns outside $S$ . An $S$ -permutation is an $S$ -allocation with row sums at most one, so every member of $S$ receives exactly one of the coalition's items. Rows index traders and columns index items.

For a proposed payoff vector $x\in\mathbb R^N$ , define the acceptability matrix

b_{S|ij}(x)= \begin{cases} 1,& i\in S\text{ and }x_i\le a_{ij},\\ 0,&\text{otherwise}. \end{cases}

The coalition payoff set is

V(S)=\{x\in\mathbb R^N:\text{some }S\text{-permutation }P \text{ satisfies }P_{ij}\le b_{S|ij}(x)\text{ for all }i,j\}.

Thus a coalition can reach a payoff threshold if it can give each member an item that member values at least as highly. The comparison is weak, so ties count as acceptable. This is the characteristic function used in the paper's Section 4 (Shapley and Scarf, 1974, pp. 109–110 of the source printing).

A balanced family $T$ is a family of nonempty coalitions with nonnegative real weights $\delta_S$ , zero outside $T$ , such that every trader has total covering weight one:

\sum_{\substack{S\in T\\j\in S}}\delta_S=1 \quad(j\in N).

The weights may be zero even for a coalition listed in $T$ . A balanced game is a game without side payments whose feasible payoff sets obey

\bigcap_{S\in T}V(S)\subseteq V(N)

for every balanced family $T$ . This includes overlapping families, not merely partitions (Shapley and Scarf, 1974, pp. 108–109).

Formalization targets

The goal is the paper's Section 4 theorem:

\text{For every finite nonempty }N\text{ and every }A:N\times N\to\mathbb R,\quad V_A\text{ is a balanced game}.

It contains four requirements. For each nonempty $S$ , $V_A(S)$ is closed; it is downward closed in the coordinates of $S$ ; and its payoff slice after removing the interiors of singleton payoff sets is bounded and nonempty. The fourth requirement is the balanced-family inclusion displayed above.

The milestones name the paper's intervening claims in their order: the three game conditions, the identity $B_N(x)=\sum_{S\in T}\delta_SB_S(x)$ , the doubly stochastic character of a balanced mixture $D=\sum_{S\in T}\delta_SP_S$ , and the existence of a grand-coalition permutation $P_N\le B_N(x)$ when $D\le B_N(x)$ . The final milestone states the matrix existence claim made at the end of Section 4, without committing the theorem statement to a particular construction.

Significance

The result establishes that the finite housing market falls under the paper's general balance framework. In the paper, the cited theorem that balanced games have nonempty cores then yields a core existence conclusion for this market. That general existence theorem is external to the Section 4 proof and is not asserted by this mission's goal (Shapley and Scarf, 1974, pp. 109–110).

The formal development supplies reusable definitions of games without side payments and balanced families alongside the market-specific allocation and acceptability matrices. It also gives precise targets for the matrix claims used in the paper. The source result is proved in print; these Lean statements are proposed formalization targets and their proof bodies remain open. Nearby platform items about transferable-utility games, including the Bondareva–Shapley goal, use a real value for each coalition and do not define this paper's payoff-set game. They are not substituted for these objects.

Difficulty

The challenge is the passage from coalition-wise feasibility to feasibility for all traders together. A balancing family can overlap: choosing one feasible permutation for each coalition does not immediately give a single permutation of $N$ . Their weighted mixture has fractional matrix entries. The condition $B_N(x)\ge D$ also has to survive the move from such a mixture to an actual zero-one permutation matrix. Without that last assertion, the balancing equations alone do not prove the inclusion $V(S)$ requires. Separately, the bounded nonempty payoff-slice condition must be checked for every nonempty coalition; merely proving closedness and downward closure would define a weaker class of games.

Formalization scope

Traders are an arbitrary finite nonempty Lean type, and payoffs live in $N\to\mathbb R$ . The paper's $E^S$ is encoded as the coordinate subspace of vectors zero outside $S$ ; interiors are taken in the product topology on $N\to\mathbb R$ . The boundedness and nonemptiness test applies to the intersection of that subspace with $V(S)$ after removing the singleton interiors. All conditions defining a game quantify over nonempty coalitions. The market formula is also defined at $S=\varnothing$ , where it yields all of $\mathbb R^N$ .

Allocation matrices are real zero-one matrices. An $S$ -permutation retains the paper's column, support, and row conditions; it is not replaced by an unconstrained permutation of all traders. The inequality between matrices is entrywise. The acceptability matrix has a 1 exactly when $i\in S$ and $x_i\le a_{ij}$ ; its columns are not independently restricted to $S$ . Balancing weights are nonnegative, may vanish inside the family, and cover every trader in $N$ . These choices exclude the trivializations $V(N)=\mathbb R^N$ , balance tested only on partitions, and coalitions using outsiders' items.

The definitions need finite-sum and matrix support from Mathlib, while the eventual proof can use Mathlib's doubly stochastic matrix and permutation-matrix library. Contributions that establish the stated game conditions or any of the four sourced matrix milestones are within scope. The paper's Section 8 counterexample and the optional superadditivity observation are outside this mission's attack path.

Selected references

Lloyd S. Shapley and Herbert Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974), 23–37. DOI: 10.1016/0304-4068(74)90033-0. The supplied scan has printed folios 104–123; Section 4 is on folios 109–111.

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Optimization·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research II: Equal Journey Times on Alternative Routes — Exactly the Routes with bᵢ < t Are Used, qᵢ = pᵢ(1 − bᵢ/t)Research Paper

Motivation

Planning a road improvement requires an estimate of how traffic will redistribute over the routes affected. Because speed falls as flow rises, sending every vehicle along the route that is quickest today changes which route is quickest. J. G. Wardrop posed the question in its simplest setting in 1952: a given flow $Q$ chooses among $D$ alternative routes between one origin and one destination, and the journey time on each route rises with the flow on it. He proposed two criteria for the resulting distribution. The first, equal journey times, became known as Wardrop's first principle or user equilibrium: "the journey times on all the routes actually used are equal, and less than those which would be experienced by a single vehicle on any unused route." It describes the state in which no driver can shorten their trip by switching routes, and it is the equilibrium notion behind traffic-assignment models and the theory of selfish routing.

Timeline:

1952. Wardrop states both criteria and, for parallel routes with journey times of the form (22), derives the closed-form equal-times split (23)–(24) (Wardrop 1952, p. 345).
1956. Beckmann, McGuire and Winsten show that, on general networks with increasing link costs, the equal-times conditions are the optimality conditions of a convex program, which gives existence and uniqueness of link flows (Beckmann et al. 1956).
2014. Kelly and Yudovina give a textbook treatment of the network case (Kelly–Yudovina 2014, ch. 4); its existence theorem is on Prove2Me for total, continuous, increasing delay functions.

Setting

There are $D$ routes, $i = 1, \dots, D$ . Route $i$ has two positive constants: $b_i$ , its journey time when no additional traffic uses it, and $p_i$ , the additional flow at which its speed would drop to zero. When an additional flow $x$ uses route $i$ , its journey time is

t_i(x) = \frac{b_i}{1 - x/p_i}, \qquad 0 \le x < p_i. \tag{22}

This form comes from a linear speed/flow relation on each route. A feasible split of the total flow $Q$ is a vector $q = (q_1, \dots, q_D)$ with $0 \le q_i < p_i$ and $\sum_i q_i = Q$ . A feasible split $q$ satisfies the equal-times criterion with common time $t$ when

every used route ( $q_i > 0$ ) has $t_i(q_i) = t$ , and
every unused route ( $q_i = 0$ ) has $t \le b_i$ , so a single vehicle could not do better than $t$ by moving to it.

Write $U(t) = \{ i : b_i < t \}$ for the routes whose empty-route time is below $t$ . In Lean these objects are routeTime b p i x, IsFeasible p Q q, IsEqualTimes b p Q q t and usedSet b t, all in the namespace WardropTraffic.EqualTimes.

Formalization targets

Goal: the closed form (23)–(24)

For every $Q$ , $t$ and $q$ , the split $q$ is feasible and satisfies the equal-times criterion with common time $t$ if and only if

q_i = \begin{cases} p_i\left(1 - \dfrac{b_i}{t}\right) & b_i < t,\\[4pt] 0 & \text{otherwise,}\end{cases} \qquad Q = \sum_{i \in U(t)} p_i - \frac{1}{t}\sum_{i \in U(t)} p_i b_i .

This states which routes are used, the flow on each, and the relation between the total flow and the common journey time. The milestones are the steps of Wardrop's derivation:

$t_i(x) \ge b_i$ for $0 \le x < p_i$ , with equality exactly when $x = 0$ ;
a route in use has $b_i < t$ ;
every route with $b_i < t$ is in use;
on a route in use, $q_i = p_i(1 - b_i/t)$ , equation (23).

Companion: the equal-times split exists and is unique

If $0 < Q < \sum_i p_i$ , there is exactly one pair $(q, t)$ satisfying the criterion. This formalizes the paper's closing sentence, that the solution is found "by picking out the value of $t$ which corresponds to the given $Q$ ".

Significance

The result. For parallel routes with journey times (22), the equilibrium is explicit. The common time $t$ is the root of a single scalar equation (24), and the flows follow from $t$ by (23). The derivation also shows a threshold structure: a route is used if and only if its empty-route time is below the equilibrium time. Adding flow raises $t$ , and the routes enter the set in use one at a time, in increasing order of $b_i$ . This structure is what the paper's second criterion (minimum average time, the next mission of this series) is compared with.

Formalizing it. The result is classical and its proof is elementary; it has not been machine-checked. The platform has the existence of a Wardrop equilibrium on general networks for delay functions that are total, continuous and increasing on $\mathbb R$ , with no closed form. That model excludes the vertical asymptote of (22) at $q_i = p_i$ and has no empty-route time $b_i$ . This mission adds the closed-form characterization for Wardrop's own model, both directions of it, and the existence and uniqueness of the split, including the corner cases that the printed criterion leaves open.

Difficulty

Each step is short. The difficulty is in the boundaries. The paper labels the routes so that $b_1 < \dots < b_D$ and speaks of "the first $j$ routes", with $b_j < t \not> b_{j+1}$ . A faithful formal version has to say what happens at $t = b_{j+1}$ , at ties among the $b_i$ , at $t \le \min_i b_i$ (no route is used), and at a route used near capacity. The printed criterion says "less than" for unused routes, yet the derivation's own case split allows equality. With the strict comparison, an equal-times split fails to exist at the values of $Q$ where $t$ coincides with some $b_k$ . The companion's uniqueness requires $Q > 0$ : at $Q = 0$ every $t \le \min_i b_i$ is a common time of the zero split. Existence requires a continuity and monotonicity argument for the right-hand side of (24) as a function of $t$ .

Formalization scope

Routes are indexed by Fin D, and all quantities are real.
The standing hypotheses are $b_i > 0$ and $p_i > 0$ for every $i$ . Feasibility includes $q_i < p_i$ , the range in which (22) is a positive finite journey time. Without it, Lean's $b_i/0 = 0$ would give a route at capacity journey time $0$ .
The criterion is formalized in the weak form $t \le b_i$ on unused routes, as the paper's derivation uses it. Every split satisfying the printed strict form satisfies it, and the definitions file records the implication. The goal under the weak form is therefore stronger than under the strict one.
The ordering $b_1 < \dots < b_D$ is not assumed. "The first $j$ routes" becomes the set $U(t) = \{i : b_i < t\}$ . This generalisation also covers ties.
No sign condition on $t$ or $Q$ is assumed in the goal. For $t \le \min_i b_i$ the term $1/t$ multiplies an empty sum, and both sides of the equivalence force $q = 0$ and $Q = 0$ .
The goal is a two-sided equivalence for arbitrary $(Q, q, t)$ . The companion requires $0 < Q < \sum_i p_i$ and asserts existence and uniqueness. Together they rule out a vacuous reading in which no split satisfies the criterion.

The development needs only the definitions above and basic real analysis (the intermediate value theorem for the companion). The model of a finite family of parallel routes with hyperbolic journey times is reusable for the minimum-average-time criterion. Proofs of the milestones, of the goal and of the companion are welcome.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Instn Civ. Engrs Part II 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
M. Beckmann, C. B. McGuire, C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956 (RAND RM-1488, 1955). https://www.rand.org/pubs/research_memoranda/RM1488.html
F. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, ch. 4. https://doi.org/10.1017/CBO9781139565363

6 thms2 active usersReviewed

Dynamic Programming Probability·Captain: mikedeng1

Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes I: Critical Rationing Levels z̄ₜ¹ ≥ ⋯ ≥ z̄ₜⁿ Give an Optimal Policy When Each aₜ Is 0 or 1Research Paper

Motivation

A firm that holds a single stock of a product often serves customers of different priority: military and civilian requisitions, contract and spot customers, emergency and routine orders for spare parts. When stock runs short, it must decide not only how much demand to satisfy but whose. Satisfying a low-priority order now may leave the firm unable to serve a high-priority order that arrives later in the same replenishment cycle. Inventory rationing asks for the optimal rule.

Veinott (Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13 (1965)) studied a model with $n$ demand classes, but fixed in advance the rule that a lower class is served only when every higher class has been served in full, and gave conditions on the costs under which that rule is optimal. Topkis (Management Science 15 (1968), 160–176) dropped the fixed rule and characterized the optimal rationing policy within a replenishment period. Theorem 1 of that paper is the target of this mission. It extends the author's earlier two-class analysis; the two-class case was later partly rediscovered by Evans and by Kaplan. Critical-level rationing policies of this kind are a standard object in the later literature on multi-class inventory systems.

Setting

A period between two replenishments is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so the period starts in interval $k$ and ends in interval $1$ . Demand comes in classes $1,\dots,n$ , with class $n$ the most important. At the start of interval $t$ the firm holds stock $z\ge0$ and faces the outstanding demand vector $B=(B^1,\dots,B^n)\ge0$ : the backlog $b$ carried in plus the new demand $d_t$ , whose law $\mu_t$ on $[0,\infty)^n$ has finite means. Demands of different intervals are independent.

The firm chooses the vector $u$ of demand left unsatisfied, with $0\le u\le B$ , so that $w=z-\mathbf 1\cdot(B-u)\ge0$ units remain in stock, where $\mathbf 1\cdot y=\sum_j y^j$ . It pays the penalty $p_t\cdot u$ and the holding cost $h_t(w)$ . A fraction $a_t\ge0$ of the unsatisfied demand is carried into the next interval: $b_{t-1}=a_tu$ , with $a_t=1$ meaning complete backlogging and $a_t=0$ lost sales. At the end of interval $1$ the salvage cost $v_1(z)+v_2(z-\mathbf 1\cdot b)$ is charged. The standing assumptions are:

(A) $h_t$ is convex and continuous on $[0,\infty)$ ;
(B) $v_1$ is convex and continuous on $[0,\infty)$ , $v_2$ is convex and continuous on $\mathbb R$ , and $D^+v_2$ is bounded below, where $D^+$ is the right derivative;
(C) $0\le p_t^1\le\cdots\le p_t^n$ .

The minimal expected cost $f_t$ of the last $t$ intervals and its expectation $g_t$ satisfy

f_t(z,B)=\inf_{\substack{0\le u\le B\\ w=z-\mathbf 1\cdot(B-u)\ge0}}\big[p_t\cdot u+h_t(w)+g_{t-1}(w,a_tu)\big],\qquad g_t(z,b)=\mathbb E\,f_t(z,b+d_t),

with $g_0(z,b)=v_1(z)+v_2(z-\mathbf 1\cdot b)$ .

For a class $j$ , with $\delta_j$ its unit vector, the critical rationing level $\bar z_t^j\in[0,+\infty]$ is $+\infty$ if $\varphi_t^j(w)=p_t^jw+h_t(w)+g_{t-1}(w,a_tw\delta_j)$ is strictly decreasing on $[0,\infty)$ , and is the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. With $B^{(j)}=\sum_{i\ge j}B^i$ , the rationing level policy leaves unsatisfied

u^j=\big(B^{(j)}-z+\bar z_t^j\big)^+\wedge B^j .

In words: going down from class $n$ , it serves as much of each class as it can without letting the stock fall below that class's critical level.

Formalization targets

Goal: Theorem 1

Suppose $a_i\in\{0,1\}$ for every $i\le t$ . Then

the rationing level policy attains $f_t(z,B)$ for every $z\ge0$ , $B\ge0$ ;
the critical levels are ordered as

\bar z_t^1\ge\bar z_t^2\ge\cdots\ge\bar z_t^n;

for $\varepsilon>0$ , the differences $f_t(z,B)-f_t(z+\varepsilon,B+\varepsilon\delta_j)$ and $g_t(z,b)-g_t(z+\varepsilon,b+\varepsilon\delta_j)$ do not depend on $B^1,\dots,B^j$ and $b^1,\dots,b^j$ .

Milestones

In attack order:

Lemma 1: the infimum of a convex function over one block of variables is convex.
Lemma 2: $g_t$ and $f_t$ are convex and continuous on the orthant, and the infimum in (1) is a minimum.
The critical levels exist, so they are well defined.
Lemma 3: moving $\varepsilon$ of demand from class $i$ to a less important class $j<i$ does not raise $f_t$ or $g_t$ .
(6): $f_t(z,B)=\min_wf_t(w;z,B)$ , where $f_t(w;z,B)$ is the cost of issuing exactly $z-w$ units.
Lemma 4: for each $w$ , serving the classes in order of importance is optimal.
Corollary 1: some optimal $u$ never serves a class before every more important class has been served in full.

A companion item states the paper's remark that with a linear ordering cost $c(y)=c\cdot y$ the optimal order is $y(z)=(y(0)-z)^+$ .

Significance

Theorem 1 reduces the $n$ -dimensional rationing decision in each interval to $n$ numbers, which are computed from one-dimensional convex minimizations. Under complete or no backlogging this is the structural result that the rest of the paper builds on: the monotonicity of the levels in time (Theorem 2), the reduction of the backlog case to a single-interval problem (Theorem 3), and the multi-period ordering policy (Theorem 4). The hypothesis on $a_i$ is sharp in the sense the paper shows: for $a_2\in(0,1)$ an example on pp. 165–166 has no optimal policy of this form.

The theorem is proved in the paper, but no part of it is machine-checked. A formal development would contribute a reusable treatment of finite-horizon dynamic programs whose value function is defined by an infimum and an expectation over an orthant, with convexity and continuity propagated through the recursion. It would also contribute the comparative statics of critical-level policies.

Difficulty

The obvious argument proves optimality of the rationing level policy by induction from convexity alone. That is not enough. Convexity gives a one-dimensional problem in $w$ (by (6) and Lemma 4). But identifying its minimizer with the class-wise critical levels requires the marginal value of class- $j$ demand to be independent of the demand of the less important classes, which is part (c). Part (c) is false when $0<a_t<1$ , so the induction must carry (a), (b) and (c) together and use $a_t\in\{0,1\}$ at every step. A second difficulty is analytic: $f_t$ is an infimum and $g_t$ an expectation, and before any structural argument starts the value functions must be shown to be finite, attained, continuous and integrable on the closed orthant (Lemma 2).

Formalization scope

Representation. Classes are Fin n; the paper's class $j$ is index $j-1$ , so class $n$ is the largest index and (b) is Antitone. Intervals are natural numbers counted backwards, as in the paper. Vectors are Fin n → ℝ with the pointwise order.
Value functions. $f_t$ is defined by the recursion (1) itself, with a real infimum (sInf), and $g_t$ by a Bochner integral against $\mu_t$ . Every statement about $f_t$ , $g_t$ is restricted to $z\ge0$ and $B\ge0$ (or $b\ge0$ ). Lemma 2's attainment and integrability conjuncts are what identify these values with the paper's.
Critical levels. The levels live in WithTop ℝ, with $\top=+\infty$ . They are specified by the predicate IsCriticalLevel: strictly decreasing for $+\infty$ , smallest minimizer otherwise. They are never computed by a real sInf, which would give the junk value $0$ when no minimizer exists.
Standing assumptions. (A)–(C) are imposed for $1\le t\le k$ . (B)'s limit condition is read as " $D^+v_2$ is bounded below". $D^+$ is an extended-real right Dini derivative. Assumption (D) on the ordering cost is not used.
Added hypothesis. Lemma 1 adds the hypothesis that the function is bounded below on every fibre, because a real infimum cannot be $-\infty$ .
Not stated. The paper's remark that Assumption (D) ensures an optimal order $y(z)$ exists for a general continuous $c$ is not formalized. With $n=k=1$ , $h_1(w)=w^2$ , $c(w)=w-w^2$ , $p_1=1$ , $v_1=v_2=0$ and demand $1$ with certainty, (D) holds but $c(y)+g_1(y,0)=1-y$ for $y\ge1$ , so no minimizer exists.
Ruled out. Theorem 1 is not proved by assuming Lemma 2, the shape of the optimal vector, or the paper's derivative formulas (8)–(9). Those appear only as milestones or not at all. Part (a) asserts optimality over all feasible $u$ , not among rationing level policies.
Contributions welcome. Proofs of the milestones, general lemmas on convexity of partial infima and on continuity of parametric minima over polytopes, and integrability of functions of linear growth against laws with finite means.

Selected references

D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (convexity of partial minima, Theorem 5.7). https://doi.org/10.1515/9781400873173

10 thms2 active usersReviewed

Completed

Statistics·Captain: mikedeng1

Some Theoretical Aspects of Road Traffic Research I: Time-Mean Speed Equals Space-Mean Speed plus σₛ²/v̄ₛ, so v̄ₜ ≥ v̄ₛ with Equality Only Without Speed VariationResearch Paper

Why two traffic speed averages differ

A speed recorded as a vehicle passes a fixed point and a speed recorded among vehicles occupying a road segment answer different questions. Fast vehicles pass a detector more often per unit time; slow vehicles remain visible along the segment for longer. Traffic studies therefore need to identify which distribution a measurement samples before comparing average speeds. J. G. Wardrop made this distinction explicit in his 1952 treatment of road traffic, then quantified it through the variance of the spatial speed distribution (Wardrop 1952, pp. 327–331 and Appendix II).

The result belongs to the paper's mathematical account of traffic flow. It is useful even when the subsidiary streams do not describe a random vehicle process: the identities concern finite positive flows and speeds. The paper also applies the same distributions to speed samples from radar and aerial photographs and to an idealized count of overtaking events (Wardrop 1952, pp. 330, 333–334).

Traffic streams and their two distributions

A road's traffic stream is divided into $C$ subsidiary streams, indexed by $i=1,\ldots,C$ . Stream $i$ has flow $q_i$ , the number of vehicles passing a point per unit time, and speed $v_i$ . Its concentration is $k_i=q_i/v_i$ , the number of vehicles occupying a unit road length. Total flow and concentration are $Q=\sum_i q_i$ and $K=\sum_i k_i$ . The time frequency $f_i=q_i/Q$ weights each stream by how often its vehicles pass a point. The space frequency $f'_i=k_i/K$ weights it by the fraction of vehicles present along the road.

The time-mean speed is $\bar v_t=\sum_i q_i v_i/Q=\sum_i f_i v_i$ . The space-mean speed is $\bar v_s=\sum_i k_i v_i/K=\sum_i f'_i v_i$ . Both are averages of the same speeds; the weights differ. Wardrop defines the space-distribution variance independently as $\sigma_s^2=\sum_i k_i(v_i-\bar v_s)^2/K$ , and the corresponding coefficient of variation as $c_s=\sigma_s/\bar v_s$ (equations (1)–(3), (7), pp. 328–331).

These are finite sums, not limits of a stochastic process. The model requires at least one subsidiary stream and positive flow and speed for each stream. Positive flows ensure that every speed in the equality criterion belongs to a present stream; positive speeds make concentration meaningful. The count $C$ is allowed to be one. In that case both means coincide and the variance is zero, as the formulas require.

Formalization targets

The main target is Wardrop's equation (6), together with its stated comparison and equality case (p. 330; Appendix II, p. 356):

\bar v_t=\bar v_s+\frac{\sigma_s^2}{\bar v_s},\qquad \bar v_s\le\bar v_t,\qquad \bar v_t=\bar v_s\iff v_i=v_j\text{ for every }i,j.

The subsidiary targets follow the paper's order. Equation (4) says $k_i v_i=q_i$ for each stream, giving equation (5), $Q=K\bar v_s$ . Appendix II then uses the centered identity $\sum_i f'_i(v_i-\bar v_s)=0$ and rewrites the time mean as $\bar v_t=(\sum_i f'_i v_i^2)/\bar v_s$ . These three claims are the mission milestones. Equation (8) is included as a companion formulation:

\bar v_t=\bar v_s(1+c_s^2).

The mission also records the paper's formulas for equally weighted time and space speed samples and the equivalent space- and time-frequency formulas for the idealized overtaking count. These companions use the same definitions without changing the main target (pp. 330–334).

What the result supplies

The identity gives an exact size and direction for the difference between the two averages. Since the variance is nonnegative and $\bar v_s$ is positive, the time mean cannot fall below the space mean. If all constituent speeds are equal, the difference vanishes; if any two present streams have different speeds, the difference is positive. The formula therefore lets a reader decide whether two reported speed averages can be compared directly, and it identifies the spatial variance as the quantity needed to convert between them.

The sample formulas sharpen that interpretation. Equal weights among vehicles passing a point make the time mean the arithmetic mean of the sampled speeds and the space mean their harmonic mean. Equal concentrations reverse which mean is arithmetic; the time mean becomes $\sum_i v_i^2/\sum_i v_i$ . The overtaking formulas express a single pairwise count using either frequency system, provided the speeds are ordered and the paper's assumption of no interference with overtaking is used (Wardrop 1952, pp. 330, 333–334).

Wardrop proved these formulas in print. The remaining work in this mission is a machine-checked proof of the finite-sum identities and their strict equality case. The proposal supplies typed statements and definitions, but the theorem proofs are open. The resulting concentration and frequency definitions are reusable in other traffic-flow formalizations; the statements also provide small algebraic interfaces for testing more elaborate traffic models.

Where the formal proof needs care

The relation looks like a routine identity for weighted means, but the two weight systems are coupled through $k_i=q_i/v_i$ . One cannot treat the time and space frequencies as independent arbitrary probability vectors and still obtain equation (6). The strict case needs more than nonnegativity of the variance: it needs the fact that every space weight is positive, so zero variance forces every constituent speed to equal the mean. The single-stream case and every denominator need the same attention.

The overtaking statement has a separate modelling boundary. Its algebraic equalities use a rate defined by pairwise speed differences. Wardrop's physical interpretation of that rate assumes that overtaking does not interfere with other overtaking. The mission records the identities for that idealized rate, without claiming that a measured road necessarily meets the physical assumption.

Formalization scope

Lean uses Fin C for the streams and real numbers for $q_i$ , $v_i$ , $k_i$ , both means, the variance, and the overtaking rate. Finite sums are taken over all streams. The theorem hypotheses require $0<C$ , $0<q_i$ , and $0<v_i$ for every $i$ . These requirements make $Q$ , $K$ , and $\bar v_s$ positive; Lean's total division would otherwise assign a zero value at a zero denominator that has no meaning in the paper's model. For the overtaking identity, StrictMono v retains Wardrop's ordering $v_1<\cdots<v_C$ .

The variance is defined from equation (7), $\sum_i k_i(v_i-\bar v_s)^2/K$ . Defining it by rearranging equation (6) would make the target true by definition and would erase the mathematical claim. The standard deviation uses the real square root of that variance. An observation in the sample companion is represented as one subsidiary stream of equal time or space weight; this is the formal reading of the paper's sampling paragraphs. No probability-measure library is needed, since $f_i$ and $f'_i$ are explicit finite weights.

A complete proof needs finite-sum rearrangements, elementary real division under positive denominators, nonnegative weighted squares, and the equality case of a positive weighted sum of squares. The definitions and the mean identities are welcome as separate reusable contributions. The mission does not include the paper's normal approximation for overtaking density in equation (11), which Wardrop presents as an approximation rather than an exact finite-sum theorem.

Selected references

J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II 1 (1952), 325–362. DOI: 10.1680/ipeds.1952.11259.

5 thms2 active usersReviewed

Dynamic Programming Markov Chain·Captain: mikedeng1

On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting 1: If G(f) ∪ H(f) Is Empty, f Maximizes the Gain and Then the Bias, and Each Improvement Step Raises (x, y, z)Research Paper

Motivation

A controller observes a finite system period after period, chooses an action in each state, earns an income and moves the system at random. When future income is not discounted, the natural criterion is the average return per unit time (the gain), but many policies share the maximal gain while differing in their transient income. Blackwell (1962) showed that the policies that are optimal as the discount factor tends to one, the 1-optimal policies, are exactly the stationary policies that first maximize the gain and then, among those, the bias. He gave no finite procedure for the second maximization. Veinott (1966) supplied one: an extension of Howard's policy improvement method in which a second improvement test, on the bias, is run after the gain test is exhausted, with a third vector $z(f)$ guaranteeing termination. The method and its sensitivity hierarchy became the starting point of the $n$ -discount optimality theory developed by Veinott (1969) and treated in Puterman's Markov Decision Processes (1994), Chapter 10.

Timeline:

1960: Howard, Dynamic Programming and Markov Processes: policy improvement for the discounted and the average-return problems.
1962: Blackwell, Discrete Dynamic Programming: existence of stationary policies optimal for all discount factors near one; the expansion $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+o(1)$ ; nearly optimal (1-optimal) policies characterized by lexicographic maximization of $(x,y)$ .
1966: Veinott, this paper: the extended policy improvement method that finds a 1-optimal stationary policy in finitely many steps (Theorem 6), and a finite-horizon characterization of the same policies (Theorem 7).
1969: Veinott, Discount optimality and sensitive optimality: the full hierarchy of $n$ -discount optimal policies and the corresponding nested improvement method.

Setting

There are finitely many states $s$ and a finite set of actions. Choosing action $a$ in state $s$ earns the income $i(s,a)$ and moves the system to state $s'$ with probability $q(s'\mid s,a)$ . A decision rule $f\in F$ picks an action $f(s)$ in each state; $r(f)$ is the vector with entries $i(s,f(s))$ and $Q(f)$ the stochastic matrix with entries $q(s'\mid s,f(s))$ . A policy is a sequence $(f_1,f_2,\dots)$ of decision rules, $f^\infty=(f,f,\dots)$ is a stationary policy, and for $0\le\beta<1$

V_\beta(\pi)=\sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\,r(f_{n+1})

is the vector of expected discounted returns. For vectors, $u\ge v$ is coordinatewise and $u>v$ means $u\ge v$ and $u\ne v$ .

Let $Q^*(f)$ be the Cesàro limit of the powers of $Q(f)$ . The gain $x(f)$ and the bias $y(f)$ are the unique solutions of

[I-Q(f)]x=0,\quad Q^*(f)x=Q^*(f)r(f);\qquad [I-Q(f)]y=r(f)-x(f),\quad Q^*(f)y=0,

and $z(f)$ is the unique solution of $[I-Q(f)]z=-y(f)$ , $Q^*(f)z=0$ . Write $F'$ for the decision rules of maximal gain and $F''\subset F'$ for those of maximal bias within $F'$ .

The two improvement sets compare $f$ with a decision rule $g$ through the state-by-state tests

\text{(i) } [Q(g)x(f)]_s\ge[x(f)]_s,\qquad \text{(ii) } [r(g)+Q(g)y(f)]_s\ge[x(f)+y(f)]_s .

$G(f)$ consists of the $g$ for which (i) holds everywhere, (ii) holds wherever (i) is an equality, some inequality is strict, and $g(s)=f(s)$ wherever both are equalities. $E(f)$ consists of the $g$ for which (i) and (ii) are equalities at every state. For $g\in E(f)$ ,

\text{(iii) } [-y(f)+Q(g)z(f)]_s\ge[z(f)]_s,

and $H(f)$ consists of the $g\in E(f)$ for which (iii) holds everywhere, strictly somewhere, with $g(s)=f(s)$ wherever it is an equality.

Formalization targets

Goal: Theorem 6 (p. 1290)

For every $f\in F$ :

$G(f)=\varnothing\ \Rightarrow\ f\in F'$ ;
$G(f)\cup H(f)=\varnothing\ \Rightarrow\ f\in F''$ ;
$g\in G(f)\ \Rightarrow\ x(g)>x(f)$ , or $x(g)=x(f)$ and $y(g)>y(f)$ ;
$g\in H(f)\ \Rightarrow\ x(g)=x(f)$ , and $y(g)>y(f)$ , or $y(g)=y(f)$ and $z(g)>z(f)$ .

Part 2 is the stopping certificate and parts 3 and 4 are the progress guarantee; together they say that the extended method raises $(x,y,z)$ lexicographically and stops at a decision rule in $F''$ .

Milestones

Theorem 3 (Blackwell): $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\epsilon(\beta,f)$ with $\epsilon(\beta,f)\to0$ as $\beta\to1^-$ , and the unique-solution characterizations of $x(f)$ , $y(f)$ (already posed on the platform, referenced).
Lemma 1 (Blackwell): $g\in E(f)\Rightarrow x(g)=x(f)$ , and $y(g)=y(f)$ if moreover $Q^*(g)Q^*(f)=Q^*(g)$ (referenced).
Theorem 1: for fixed $0\le\beta<1$ , exactly one of " $f^\infty$ has no one-step improvement and is $\beta$ -optimal" and "some $g$ gives $V_\beta(g,f^\infty)>V_\beta(f^\infty)$ and $V_\beta(g^\infty)>V_\beta(f^\infty)$ ".
Theorem 4: $F''$ is the nonempty set of $f$ with $f^\infty$ 1-optimal.
Theorem 5 and Corollary 1: $G(f)=\varnothing\Rightarrow f\in F'$ ; $g\in G(f)\Rightarrow V_\beta(g^\infty)>V_\beta(f^\infty)$ for $\beta$ near one, hence the lexicographic increase of $(x,y)$ .
Lemma 4: for $g\in E(f)$ , $y(g)=y(f)+w(g)$ , where $w(g)$ is the unique solution of $[I-Q(g)]w=0$ , $Q^*(g)w=Q^*(g)(-y(f))$ .
(12): $z(f)$ is the unique solution of its system.
Lemma 5: $G(f)=\varnothing$ and $y(f)\ge y(g)$ for all $g\in E(f)$ imply $f\in F''$ .
Two steps of the proof of Theorem 6: $H(f)=\varnothing\Rightarrow y(g)\le y(f)$ on $E(f)$ ; and $g\in H(f)\Rightarrow w(g)>w(f)=0$ , or $w(g)=w(f)=0$ and $z(g)>z(f)$ .

Significance

Theorem 6 turns Blackwell's existence result into an algorithm. Blackwell's characterization requires maximizing the bias over $F'$ , a set with no explicit description; Lemma 5 shows that maximizing over the explicitly available set $E(f)$ suffices, and Lemma 4 shows that this maximization has the same form as the original gain maximization, so the familiar policy improvement machinery applies a second time. The same mechanism, iterated, gives the $n$ -discount optimal policies of the later sensitivity theory and the lexicographic policy improvement algorithms in standard texts.

The results are proved in the paper (with a correction to the proof of Lemma 5 credited to Bruce Miller). They are not formalized in any proof assistant known to the mission. A complete development yields machine-checked policy improvement for average and bias optimality on top of the published Blackwell model, including the convergence-free closed forms of gain, bias and $z$ and the facts about the limit matrix $Q^*$ and the deviation matrix they rest on.

Difficulty

Parts 1 and 3 are Blackwell's policy improvement for the gain, transported to Veinott's set $G(f)$ . The new content is in parts 2 and 4, and in both the obvious argument fails at the same place: the bias of $g\in E(f)$ cannot be compared with the bias of $f$ by a state-by-state test in the original problem, because $E(f)$ is a product of action sets $E(s,f)$ different from the original ones, and Blackwell's comparison works only after a reduction to a problem in which the reward is $-y(f)$ and the role of the gain is played by $w(g)$ . A second difficulty is Lemma 5: $E(f)$ may be a proper subset of $F'$ (Example 3 of the paper), so maximizing the bias over $E(f)$ does not obviously maximize it over $F'$ . The certificate does not follow from the gain and bias tests at $f$ alone, and the paper's original proof of it contained an error (corrected, as the paper records, by Bruce Miller).

Formalization scope

Everything is built on the published Blackwell definitions (BlackwellDiscreteDP.NearOne.Model, LimitMatrix, GainBias): one finite action type available in every state (Veinott's $A_s$ are all equal to it), decision rules St → Act, policies indexed from $0$ (π 0 is $f_1$ ), real vectors St → ℝ with the pointwise order, and VecGt for the paper's $>$ (not coordinatewise strict). $Q^*(f)$ is the published Cesàro limit $\lim (N+1)^{-1}\sum_{i=0}^N Q(f)^i$ , the same limit as Veinott's $N^{-1}\sum_{i=0}^{N-1}$ . The gain and bias are the published closed forms $x(f)=Q^*(f)r(f)$ and $y(f)=H(f)r(f)$ with the deviation matrix $H(f)$ ; the new vectors are closed forms too: $w(g)=Q^*(g)(-y(f))$ and $z(f)=H(f)(-y(f))$ , and their characterizations by (10) and (12) are milestones. 1-optimality is the published IsNearlyOptimal, which compares against every policy. Veinott's set $H(f)$ is HSet, to keep it apart from the deviation matrix Hf.

$G(f)$ and $H(f)$ are defined literally from the paper's inequalities, including the clauses "at least one strict" and " $g(s)=f(s)$ where the tests are equalities". Dropping either clause makes parts 3 and 4 false (a $g$ that only reshuffles ties would count as an improvement); replacing $F''$ or $G(f)$ by a set defined through the conclusion of the theorem would make the goal trivial. Neither is acceptable.

The reduction "replace $A_s$ by $E(s,f)$ and $r(g)$ by $-y(f)$ " is not instantiated, since the published model has a single action set; its two uses in the proof of Theorem 6 are milestones stated in the original model. A development of the general model with state-dependent action sets, and of the limit-matrix identities $Q^*Q=QQ^*=Q^*Q^*=Q^*$ , $(I-Q)H=I-Q^*$ , $Q^*H=0$ , would be reusable well beyond this mission. Proofs of any milestone are welcome, as is a proof of the published Theorem 3 and Lemma 1, on which most of the mission rests.

Selected references

D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
A. F. Veinott, Jr., On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, Ann. Math. Statist. 37(5):1284–1294, 1966. https://doi.org/10.1214/aoms/1177699272
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
A. F. Veinott, Jr., Discount Optimality and Sensitive Optimality, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

16 thms2 active usersReviewed

Convex Optimization Functional Analysis Optimization·Captain: mikedeng1

Duality and Stability in Extremum Problems Involving Convex Functions 3: If f Is Finite at x and g Is Finite and Continuous at Ax, Then (P) Is Stably Set and inf (P(z)) Is Continuous Near z = 0Research Paper

Motivation

A convex program is useful in practice only if its optimal value responds reasonably to small changes in the data. Lagrangian and Fenchel duality theory makes this precise: the dual problem attains its optimum and has no duality gap exactly when the primal value function does not fall off infinitely steeply under small perturbations. A constraint qualification is a checkable condition on the data that guarantees this good behaviour; Slater's condition (a strictly feasible point) is the best-known example in finite dimensions.

R. T. Rockafellar's 1967 paper Duality and Stability in Extremum Problems Involving Convex Functions (Pacific J. Math. 21 (1967) 167–187) develops Fenchel-type duality for the problem of minimizing $f(x) - g(Ax)$ in general locally convex spaces. It introduces the notion of a stably set problem, shows that stability is equivalent to strong duality with an attained dual optimum (its Theorem 3), and gives in Theorem 1 a general sufficient condition for stability. Theorem 1 is the infinite-dimensional analogue of Slater's condition and is the form in which the result is usually applied: one exhibits a single point where $f$ is finite and $g$ is finite and continuous.

Timeline. Fenchel (1951) proved the duality theorem for $A = I$ in $\mathbb{R}^n$ under relative-interior conditions. Brøndsted (1964) and Moreau (1966–67) extended conjugate duality to paired locally convex spaces. Rockafellar's 1967 paper (this mission) added the linear map $A$ , the perturbation function $h$ , the notion of stability, and Theorem 1. The perturbational approach was later systematized in Rockafellar's Conjugate Duality and Optimization (SIAM, 1974).

Setting

Let $E$ and $F$ be real locally convex Hausdorff topological vector spaces and $A : E \to F$ a continuous linear map. Let $f : E \to [-\infty, +\infty]$ and $g : F \to [-\infty, +\infty]$ .

$f$ is convex if its epigraph $\{(x, \mu) \mid x \in E, \mu \in \mathbb{R}, \mu \ge f(x)\}$ is a convex subset of $E \times \mathbb{R}$ ; it is proper if $f(x) > -\infty$ for all $x$ and $f(x) < +\infty$ for some $x$ . $g$ is concave if $-g$ is convex, and proper concave if $g < +\infty$ everywhere and $g > -\infty$ somewhere.
Throughout, $f$ is lower semicontinuous proper convex and $g$ is upper semicontinuous proper concave. Their effective domains are $C = \{x \mid f(x) < +\infty\}$ and $D = \{y \mid g(y) > -\infty\}$ .
The primal problem is

(P) \qquad \text{minimize } f(x) - g(Ax) \text{ over } x \in E,

and its perturbations are $(P(z))$ : minimize $f(x) - g(Ax - z)$ , for $z \in F$ . The perturbation function is $h(z) = \inf (P(z)) = \inf_x \{ f(x) - g(Ax - z) \} \in [-\infty, +\infty]$ , so $h(0) = \inf (P)$ . $(P)$ is consistent if $h(0) < +\infty$ .

When $h(0)$ is finite, the directional derivative is $h'(0; z) = \lim_{\varepsilon \downarrow 0} [h(\varepsilon z) - h(0)]/\varepsilon$ .
$(P)$ is unstably set if $h(0)$ is finite and every neighbourhood of $0$ contains vectors $z$ with $h'(0; z)$ a negative number of arbitrarily large magnitude ( $-\infty$ included). $(P)$ is stably set if it is consistent but not unstably set.

Formalization targets

Goal: Theorem 1 (p. 175)

Suppose there exists $x \in E$ such that $f$ is finite at $x$ and $g$ is finite and continuous at $Ax$ . Then

(P) \text{ is stably set} \quad\text{and}\quad \text{there is a neighbourhood } U \text{ of } 0 \text{ on which } z \mapsto \inf (P(z)) \text{ is continuous}.

The neighbourhood $U$ is left unspecified, as in the paper.

Milestones (in the order the proof uses them)

(4.4) $\{z \mid h(z) < +\infty\} = \{Ax - y \mid f(x) < +\infty,\ g(y) > -\infty\} = A(C) - D$ .
(4.5) $A(C)$ meets $\operatorname{int} D$ , and $0 \in A(C) - \operatorname{int} D \subseteq \operatorname{int}(A(C) - D)$ .
Epigraph of $h$ has interior (p. 176): the hypograph $G = \{(y, \mu) \mid g(y) \ge \mu > -\infty\}$ has nonempty interior, $(Ax, \lambda) - G$ lies in the epigraph of $h$ for every $(x, \lambda)$ in the epigraph of $f$ , and so the epigraph of $h$ has nonempty interior.
Continuity on the interior of the domain (p. 176): $0 \in \operatorname{int}\{h < +\infty\}$ and $h$ is continuous there.
(4.6) For a convex $h$ with $h(0)$ finite: $h(z) \ge h(0) + h'(0; z)$ and $h'(0; z) \ge -h'(0; -z)$ for all $z$ .

Significance

The result. Combined with the paper's Theorem 3, Theorem 1 yields: if $f$ is finite at some $x$ where $g$ is finite and continuous at $Ax$ , then $\inf (P) = \max (P^*)$ , with the dual maximum attained. This is the standard sufficient condition for Fenchel–Rockafellar duality in infinite dimensions, used in calculus of variations, optimal control, and the convex analysis of integral functionals. The continuity half of Theorem 1 says that the optimal value depends continuously on translations of the constraint data near the unperturbed problem, a basic sensitivity statement.

Formalizing it. The theorem is proved (1967) and appears in many textbooks, but there is no machine-checked version on this platform. Mathlib contains continuity criteria for real-valued convex functions on open sets of normed or finite-dimensional spaces (ConvexOn.continuousOn_tfae, ConvexOn.continuousOn_interior), but nothing for extended-real-valued convex functions on general topological vector spaces, no perturbation function, and no notion of a stably set problem. A complete development would provide reusable infrastructure: the epigraph-interior continuity criterion for $[-\infty, +\infty]$ -valued convex functions and the elementary calculus of one-sided directional derivatives.

Difficulty

The obvious argument says: $g$ is continuous at $Ax$ , so $h(z) \le f(x) - g(Ax - z)$ is bounded above near $0$ , hence $h$ is continuous at $0$ and its directional derivatives are bounded. Two steps of this fail without care. First, the passage from "bounded above near a point" to "continuous" requires convexity of $h$ (Lemma 2 of the paper, proved in the companion mission) and a continuity criterion valid in an arbitrary topological vector space, with values in $[-\infty, +\infty]$ ; the normed-space proofs in Mathlib do not apply. Second, $h$ may take the value $-\infty$ , and the derivative may be $-\infty$ in some directions; the bookkeeping of extended-real arithmetic (where $(+\infty) + (-\infty)$ is not defined mathematically and is given a junk value in Lean) has to be done honestly. Finally, upper bounds on $h'(0;\cdot)$ must be converted into lower bounds, which is where the second inequality of (4.6) enters; an upper bound alone does not give stability.

Formalization scope

All values are in Lean's EReal. Convexity is convexity of the epigraph with real second coordinate (the paper's definition, p. 170); concavity is convexity of $-g$ . Properness is stated as in the paper. The perturbation function is the EReal infimum ⨅ x, f x - g (A x - z); under properness the undefined form $(+\infty) - (+\infty)$ never arises. The directional derivative (4.3) is the lower limit of the difference quotient along $\varepsilon \to 0^+$ , which equals the paper's limit whenever it exists (always, for convex $h$ with $h(0)$ finite). "Unstably set" quantifies over all neighbourhoods of $0$ and all real $M$ , with $h'(0;z) < -M$ allowing $-\infty$ . "Stably set" is $h(0) < +\infty$ together with "not unstably set", so $\inf (P) = -\infty$ is stably set, as the paper says on p. 176. Continuity is with respect to the order topology of EReal, and "continuous at $Ax$ " is continuity of $g$ itself at that point, not of its restriction to $D$ .

The paper's standing setting (§3) includes dual spaces $E^*, F^*$ , the adjoint $A^*$ and the conjugates $f^*, g^*$ . Neither Theorem 1 nor its proof uses them, so they are omitted and the theorem is stated for every pair of real locally convex Hausdorff spaces, which includes every paired setting. The lower and upper semicontinuity of $f$ and $g$ are standing hypotheses of the paper and are kept, although the proof does not use them. Inequality (4.6) is stated for an arbitrary convex function finite at $0$ , the generality in which the paper invokes it. No statement was repaired.

A definition of "stably set" that already presumed finiteness or continuity of $h$ near $0$ , or that tested the derivative only in a fixed set of directions, would make the first conclusion of Theorem 1 trivial; the definition used here is the paper's p. 175 definition verbatim, applied to an arbitrary function $h$ . The definitions are local to this mission; the companion missions on Theorem 3 and Theorem 6 of the same paper define the same objects in their own namespaces. Contributions are welcome on the milestones in any order, and in particular on a general continuity criterion for extended-real-valued convex functions on topological vector spaces, which is reusable well beyond this mission.

Selected references

R. T. Rockafellar, Duality and stability in extremum problems involving convex functions, Pacific J. Math. 21 (1967) 167–187. https://doi.org/10.2140/pjm.1967.21.167
A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat.-Fys. Medd. Dansk. Vid. Selsk. 34 (1964), no. 2.
W. Fenchel, Convex Cones, Sets and Functions, lecture notes, Princeton University, 1951.
J. J. Moreau, Fonctionnelles convexes, Séminaire Leray, Collège de France, 1966–67.
R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Optimization·Captain: mikedeng1

An Iterative Method of Solving a Game: For Every Vector System, min U(t)/t and max V(t)/t Converge to the Value of the GameResearch Paper

Motivation

A finite two-person zero-sum game is given by a real pay-off matrix, and its value can be computed by linear programming. In 1949 George W. Brown proposed a much simpler procedure, now called fictitious play: each player in turn plays a best pure reply to the accumulated play of the opponent so far, and the running averages are read off as estimates of the value (Brown, RAND P-78, 1949). Brown conjectured that both estimates converge to the value. Julia Robinson proved the conjecture in An Iterative Method of Solving a Game, Annals of Mathematics 54 (1951).

The result is the starting point of the theory of learning in games. Fictitious play is the basic model of boundedly rational players who best-respond to empirical frequencies, and the question "for which classes of games does it converge?" has driven a long line of work.

Timeline.

1949–1951: Brown proposes the method and conjectures convergence for zero-sum games.
1951: Robinson proves it for every vector system of every zero-sum matrix game; the statement contains no rate.
1958: Shapiro extracts from Robinson's argument a rate: the gap $(\max V(t) - \min U(t))/t$ is $O(t^{-1/(m+n-2)})$ (doi:10.1002/cpa.3160110408).
1964: Shapley gives a 3 × 3 bimatrix (non-zero-sum) game in which fictitious play does not converge (doi:10.1515/9781400882014-002).
1996: Monderer and Shapley prove convergence for games with identical interests (doi:10.1006/jeth.1996.0014).
2014: Daskalakis and Pan show that with adversarial tie-breaking the convergence can be much slower than the rate $t^{-1/2}$ conjectured by Karlin (arXiv:1412.4840).

Setting

Let $A = (a_{ij})$ be a real $m \times n$ matrix, $m, n \ge 1$ . The first player chooses a row $i$ , the second a column $j$ , and the second pays the first $a_{ij}$ . A mixed strategy is a probability vector $x = (x_1, \dots, x_m)$ for the first player, or $y = (y_1, \dots, y_n)$ for the second. For all mixed strategies,

\min_j \sum_i a_{ij} x_i \le \max_i \sum_j a_{ij} y_j. \tag{1}

A pair $(X, Y)$ for which equality holds is a solution, and the common number $v$ is the value of the game. The minimax theorem says that a solution exists.

Write $A_{i\cdot}$ for the $i$ -th row, $A_{\cdot j}$ for the $j$ -th column, and $\max W$ , $\min W$ for the largest and smallest component of a vector $W$ . A vector system for $A$ is a pair of sequences $U(0), U(1), \dots$ of $n$ -vectors and $V(0), V(1), \dots$ of $m$ -vectors with $\min U(0) = \max V(0)$ and

U(t+1) = U(t) + A_{i\cdot}, \qquad V(t+1) = V(t) + A_{\cdot j},

where $v_i(t) = \max V(t)$ and $u_j(t) = \min U(t)$ . In the alternate vector system the column satisfies $u_j(t+1) = \min U(t+1)$ instead. A row $i$ is eligible in the interval $(t, t')$ if $v_i(t_1) = \max V(t_1)$ for some $t \le t_1 \le t'$ , and similarly a column $j$ if $u_j(t_2) = \min U(t_2)$ for some $t \le t_2 \le t'$ .

With $U(0) = V(0) = 0$ , $U(t)/t$ is the payoff vector of the first player's empirical mixed strategy against each column, and $V(t)/t$ that of the second player's against each row. In the Lean development these objects are vmax, vmin, IsVectorSystem, IsAltVectorSystem, RowEligible, ColEligible and IsSolution, in the namespace RobinsonFP.Convergence.

Formalization targets

Goal: the Theorem (p. 297)

For every vector system $(U, V)$ for $A$ , and $v$ the value of the game,

\lim_{t\to\infty} \frac{\min U(t)}{t} = \lim_{t\to\infty} \frac{\max V(t)}{t} = v.

The statement holds for arbitrary initial vectors with $\min U(0) = \max V(0)$ and for every way of breaking ties.

Milestones, in the order of the proof

Inequality (1).
Lemma 1: $\liminf_{t\to\infty} (\max V(t) - \min U(t))/t \ge 0$ .
Lemma 2: if every row and column is eligible in $(s, s+t)$ , then $\max U(s+t) - \min U(s+t) \le 2at$ and $\max V(s+t) - \min V(s+t) \le 2at$ , where $a = \max_{i,j}|a_{ij}|$ .
Lemma 3: under the same hypothesis, $\max V(s+t) - \min U(s+t) \le 4at$ .
Display (3) of the proof of Lemma 4: if some row or column is not eligible in $(s, s+t^*)$ , the gap $\max V - \min U$ grows by less than $\tfrac12 \varepsilon t^*$ over that window, given the bound $\tfrac12\varepsilon t$ for the vector systems of the submatrices.
Lemma 4: for every $\varepsilon > 0$ there is $t_0$ , uniform over all vector systems for $A$ , with $\max V(t) - \min U(t) < \varepsilon t$ for $t \ge t_0$ .
$(\max V(t) - \min U(t))/t \to 0$ .
$\limsup \min U(t)/t \le v$ and $\liminf \max V(t)/t \ge v$ .

Two further items are not milestones: the Theorem for the alternate vector system, which the paper says follows by the same proofs, and the bracketing $\min U(t)/t \le v \le \max V(t')/t'$ when $U(0) = V(0) = 0$ (p. 297).

Significance

The Theorem shows that a payoff-based procedure with no linear algebra finds the value of every zero-sum matrix game. It was one of the first iterative methods for linear programs with a convergence proof, and it is the base case for every later convergence result about fictitious play: potential games, games with identical interests, $2\times n$ games, and continuous-time best-response dynamics.

The result is proved, and its proof is short. To our knowledge it has no machine-checked proof. The mission produces a Lean proof of the Theorem and its four lemmas, together with reusable definitions of vector systems and eligibility. A statement with an explicit rate, such as Shapiro's, or a proof for the alternate system, is a natural extension.

Difficulty

Lemmas 1–3 are elementary estimates. The difficulty is Lemma 4. The obvious approach follows a single run of the iteration and tries to show that the gap $\max V(t) - \min U(t)$ grows sublinearly. This fails because a run can spend arbitrarily long windows in which some row or column is never a best reply, and nothing about one fixed run controls the gap over such a window. What is needed is a bound that is uniform over all vector systems, whatever their initial vectors and tie-breaking, which is why $t_0$ in Lemma 4 comes before the vector system, and why display (3) quantifies over every vector system of the smaller matrices. In Lean, this uniformity has to range over matrices of every smaller size, so the statements must be general in the index types.

Formalization scope

Rows and columns are indexed by finite nonempty types ι, κ (the paper's $m, n \ge 1$ ); Fin m, Fin n is a special case. The matrix is Matrix ι κ ℝ.
$\max W$ , $\min W$ are Finset.sup' and Finset.inf' over all indices, hence attained.
A vector system allows any maximizing row and minimizing column at each step (an existential per step). No tie-breaking rule is fixed, and the initial vectors are arbitrary subject to $\min U(0) = \max V(0)$ . The case $U(0) = V(0) = 0$ is not imposed.
Time is a natural number. Limits are Tendsto … atTop (𝓝 ·); lim inf and lim sup of real sequences are stated in $\varepsilon$ -form (for every $\varepsilon > 0$ , eventually), with no boundedness side conditions.
The value $v$ is given by a solution: every statement about $v$ assumes IsSolution A x y v, i.e. probability vectors $x$ , $y$ with $\min_j \sum_i a_{ij} x_i = v = \max_i \sum_j a_{ij} y_j$ . Such a solution exists by the minimax theorem, which is proved on the platform as MatousekLP.ZeroSum.minimax_equality in a different encoding. A statement with $v$ free, or with "there exists $v$ ", would be false or would lose the identification with the value; neither is used.
In Lemmas 2 and 3, $a$ is any upper bound on the $|a_{ij}|$ . This is equivalent to the paper's $a = \max_{i,j}|a_{ij}|$ .
In display (3), the bound for submatrices is assumed only for the submatrices that delete one row or one column, which makes the statement at least as strong as the paper's.
The paper's closing display on p. 301 prints $\lim \min V(t)/t$ for $\lim \min U(t)/t$ . The goal follows the statement of the Theorem on p. 297.

A general "restriction of a vector system to a submatrix" lemma would be reusable for later work on fictitious play. Proofs of any milestone are welcome, as are proofs of the two extra items.

Selected references

J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54(2), 296–301, 1951. https://doi.org/10.2307/1969530
G. W. Brown, Some notes on computation of games solutions, RAND Report P-78, 1949. https://www.rand.org/pubs/papers/P78.html
H. N. Shapiro, Note on a computation method in the theory of games, Communications on Pure and Applied Mathematics 11(4), 587–593, 1958. https://doi.org/10.1002/cpa.3160110408
L. S. Shapley, Some topics in two-person games, Advances in Game Theory, Annals of Mathematics Studies 52, 1964. https://doi.org/10.1515/9781400882014-002
D. Monderer, L. S. Shapley, Fictitious play property for games with identical interests, Journal of Economic Theory 68, 258–265, 1996. https://doi.org/10.1006/jeth.1996.0014
C. Daskalakis, Q. Pan, A counter-example to Karlin's strong conjecture for fictitious play, FOCS 2014. https://arxiv.org/abs/1412.4840

10 thms2 active usersReviewed

Bandit Algorithms Probability Statistics·Captain: mikedeng1

Some Aspects of the Sequential Design of Experiments I: Greedy Sampling with Density-Zero Forced Draws Earns max(α, β) per Draw from Any Two Populations with Finite MeansResearch Paper

Motivation

An experimenter can draw observations from two populations $A$ and $B$ , one at a time, and wants the sum of the observations to be as large as possible. The populations might be two treatments, two seed varieties or two manufacturing processes; their means are unknown. Each draw both earns a reward and tells the experimenter something about the population it came from. This is the two-armed bandit problem. Herbert Robbins posed it in its modern form in his 1952 address to the American Mathematical Society, Some aspects of the sequential design of experiments, the paper usually credited with founding the field.

Section 2 of that paper asks a basic question (display (12), p. 532): is there any sampling rule whose average reward per draw approaches the larger of the two means, whatever the populations are? Robbins answers yes, for any two populations with finite means, using one explicit rule: forced sampling along a sparse schedule, greedy choice otherwise. This mission formalizes that answer.

Timeline:

1933. Thompson proposes a randomized rule for choosing between two treatments (Biometrika 25).
1952. Robbins states the problem for general populations and gives the rule $\bar R$ with $\lim_n L_n(A,B,\bar R) = 0$ for any two populations with finite means. The argument is only indicated ("it can be shown").
1985. Lai and Robbins replace $o(n)$ loss by the optimal logarithmic regret for parametric families (Adv. Appl. Math. 6).
2020. Lattimore and Szepesvári give the textbook account of explore-then-commit and $\varepsilon$ -greedy rules, which descend from forced sampling (Bandit Algorithms).

Setting

Population $A$ has distribution function $F$ and population $B$ has $G$ , with expectations

\alpha = \int_{-\infty}^{\infty} x\,dF(x), \qquad \beta = \int_{-\infty}^{\infty} x\,dG(x),

assumed to exist, i.e. to be finite (display (1), p. 529). Nothing else is assumed about $F$ and $G$ .

A sampling rule $R$ draws $x_1, x_2, \dots$ one at a time; the population of the $i$ -th draw may depend on $x_1, \dots, x_{i-1}$ , and given that choice $x_i$ is a fresh draw from the chosen population. Write $S_n = x_1 + \cdots + x_n$ . The loss of $R$ after $n$ draws (display (9), p. 531) is

L_n(A, B, R) = \max(\alpha, \beta) - E\!\left(\frac{S_n}{n}\right),

the average shortfall per draw compared with someone who knows the better population and samples only from it.

The forcing schedule (display (13), p. 532) is a pair of disjoint, strictly increasing sequences of positive integers

1 = a_1 < a_2 < \cdots, \qquad 2 = b_1 < b_2 < \cdots

of density zero: the fraction of the integers $1, \dots, n$ that are an $a$ or a $b$ tends to $0$ .

The rule $\bar R$ : at draw $i$ , sample $A$ if $i$ is an $a$ , sample $B$ if $i$ is a $b$ , and otherwise sample $A$ if the mean of the previous observations from $A$ is strictly larger than the mean of the previous observations from $B$ , and $B$ if it is not (a tie goes to $B$ ).

Formalization targets

Goal: Section 2, Eq. (16)

For every pair of populations with finite means and every forcing schedule,

\lim_{n\to\infty} L_n(A, B, \bar R) = 0.

The goal is about the specific rule $\bar R$ and every schedule, not about the mere existence of a rule. It contains no rate and no constant, so it stays valid when the rule is analysed more finely.

Milestone: Eq. (14), almost-sure average

\lim_{n\to\infty} \frac{S_n}{n} = \max(\alpha, \beta) \quad\text{with probability } 1.

Milestone: Eq. (15), expected average

\lim_{n\to\infty} E\!\left(\frac{S_n}{n}\right) = \max(\alpha, \beta).

The goal follows from (15) by the definition (9); the paper's chain is (14) ⇒ (15) ⇒ (16).

Significance

The result. The theorem answers question (12) and shows that "learning while earning" costs nothing in the long run, per draw, under no assumption beyond finite means: no bounded support, no variance, no parametric family. It is the first consistency result for an adaptive allocation rule, and it fixes the benchmark later refined by logarithmic-regret theory. In modern terms, a forced-exploration greedy policy has regret $o(n)$ on every two-armed bandit with integrable rewards.

Formalizing it. The paper gives no proof; it says the results "can be shown". A machine-checked proof records the argument in full. The platform already has finite-horizon regret bounds for $\varepsilon$ -greedy with bounded rewards (FoundationsRL.Bandits.epsilon_greedy_regret_bound), consistency in the stronger Lai–Robbins sense as a definition (ConsistentBanditPolicy), and a forced-sample tail bound for the Lasso bandit (BastaniBayati.LassoBandit.forced_sample_estimator_tail). None of these covers a deterministic greedy rule, almost-sure convergence, or unbounded rewards with only a first moment, and none of them proves (14)–(16).

Difficulty

The obvious argument is: each population is sampled infinitely often because of the forced draws, so each running mean converges by the strong law, so greedy eventually picks the better population, and the forced draws are negligible. Two steps are not routine.

First, the strong law applies to i.i.d. sequences, while the observations from $A$ arrive at random, history-dependent times. The values seen from $A$ have to be identified, in law, with an i.i.d. sequence that is independent of the times at which they are used.

Second, passing from (14) to (15) needs uniform integrability of $S_n/n$ , and only first moments are available. No second moment is assumed, so variance bounds are not available.

When $\alpha = \beta$ greedy need not settle on either population; the statement must hold anyway, and an argument that waits for greedy to "lock in" does not cover this case.

Formalization scope

The populations are a published two-armed BanditAlgorithm.StochasticBandit 2. $A$ is arm 0 and $B$ is arm 1; $\alpha$ and $\beta$ are banditArmMean. A rule is a published BanditPolicy 2, and $E$ is the integral against the published infinite-horizon law banditTrajMeasure, whose coordinate $t$ is the paper's draw $t+1$ . Explicit readings of the paper's phrases:

"the expectations exist" means both reward laws are Integrable. This is the only assumption on the populations: the class $D$ of the paper is left arbitrary, and $\alpha = \beta$ is allowed.
"density 0" means #({1,…,n} ∩ (range a ∪ range b)) / n → 0 in $\mathbb R$ . The sequences are infinite and 0-indexed (a 0 = 1, b 0 = 2).
"according as … exceeds or does not exceed": $A$ exactly when mean $_A$ > mean $_B$ , so ties go to $B$ .
"with probability 1" is ∀ᵐ under the trajectory law, and "lim" is Tendsto … atTop along $n \in \mathbb N$ .
$S_n/n$ uses real division; its value at $n = 0$ plays no role.

Trivializing formalizations are excluded. Without integrability the means and expectations are junk zeros; this is ruled out by the integrability hypothesis. Replacing $\bar R$ by "there exists a rule" would weaken the goal to (12). Finite forcing sets would make the statement false.

The needed infrastructure is a representation of the adaptive sampling process by per-population i.i.d. reward sequences, the strong law along random subsequences, and a uniform-integrability argument for averages under only a first moment. All three are reusable for other forced-exploration and greedy policies. Contributions of these general lemmas as separate theorems are welcome.

Selected references

H. Robbins, Some aspects of the sequential design of experiments, Bull. Amer. Math. Soc. 58(5) (1952), 527–535. https://doi.org/10.1090/S0002-9904-1952-09620-8
W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933), 285–294. https://doi.org/10.2307/2332286
T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Adv. Appl. Math. 6 (1985), 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
T. Lattimore and Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

8 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming: The Set-Inclusive LP Has the Same Feasible Set as the LP of Support FunctionalsResearch Paper

Motivation

A linear program $\max c\cdot x$ subject to $Ax\le b$ , $x\ge 0$ assumes that the constraint matrix $A$ is known exactly. In practice the columns of $A$ — the activity vectors, describing how much of each resource one unit of activity $j$ consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision $x$ should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.

The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.

Setting

Fix integers $m,n\ge0$ . Vectors in $\mathbb R^m$ are compared componentwise. For a set $S\subseteq\mathbb R^m$ and a scalar $t$ , $tS=\{ta: a\in S\}$ , and the sum of sets is Minkowski addition, $S+T=\{s+t: s\in S,\ t\in T\}$ .

Let $K_1,\dots,K_n\subseteq\mathbb R^m$ be nonempty convex activity sets and $K\subseteq\mathbb R^m$ a nonempty convex resource set. Problem (I) is

\sup\ c\cdot x\quad\text{subject to}\quad x_1K_1+x_2K_2+\cdots+x_nK_n\subseteq K,\quad x_j\ge0,

and $X\subseteq\mathbb R^n$ denotes its set of feasible $x$ . Problem (Ib) is the special case $K=K(b)=\{y\in\mathbb R^m: y\le b\}$ for a right-hand side $b\in\mathbb R^m$ .

The support functional of a set $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y\cdot a$ , a value in $[-\infty,+\infty]$ . With $e_i$ the $i$ -th unit vector, the auxiliary matrix $\bar A$ is the $m\times n$ matrix with entries

\bar a_{ij}=\delta^*(e_i\mid K_j)=\sup_{a_j\in K_j}a_{ij},

defined when all of these are finite, and LP $(\bar A)$ is the linear program $\max c\cdot x$ subject to $\bar Ax\le b$ , $x\ge0$ . Finally $M$ is the set of $m\times n$ matrices $(a_1,\dots,a_n)$ whose $j$ -th column lies in $K_j$ .

In the application, the activity sets are Euclidean balls $K_j=\{a\in\mathbb R^m:\|a-a_j\|_2\le\rho_j\}$ around nominal columns $a_j$ of a matrix $A_0$ , with radii $\rho_j\ge0$ .

Formalization targets

Goal: the THEOREM (p. 1156)

Assume every $K_j$ is nonempty and convex and $\delta^*(e_i\mid K_j)<\infty$ for all $i,j$ . Then

\{x : x\ \text{feasible for (Ib)}\}=\{x : \bar Ax\le b,\ x\ge 0\},

and for every objective $c$ , the optimal solutions of (Ib) and of LP $(\bar A)$ coincide.

Milestones

Feasibility for (I) is equivalent to $x\ge0$ and $\sum_j x_ja_j\in K$ for every choice $a_j\in K_j$ (p. 1154).
LEMMA (p. 1155): $X$ is convex.
If $\delta^*(e_i\mid K_j)=\infty$ for some $i$ , every feasible $x$ of (Ib) has $x_j=0$ (p. 1155).
Compact activity sets have $\delta^*(e_i\mid K_j)<\infty$ (p. 1156).
$x$ is feasible for (Ib) iff $Ax\le b$ for every $A\in M$ and $x\ge0$ (p. 1156).
Every $A\in M$ satisfies $A\le\bar A$ entrywise (proof of THEOREM).
Feasible for LP $(\bar A)$ implies feasible for (Ib) (proof of THEOREM).
Feasible for (Ib) implies $\sum_j x_j\sup_{a_j\in K_j}a_{ij}\le b_i$ for every $i$ , i.e. feasible for LP $(\bar A)$ (proof of THEOREM).
For Euclidean balls, $\delta^*(e_i\mid K_j)=a_{ij}+\rho_j$ , so $\bar a_j=a_j+\rho_je$ with $e$ the all-ones vector (p. 1157).
Inexact LP over balls: (Ib) has the same feasible and optimal solutions as $\max c\cdot x$ subject to $\sum_j x_j(a_j+\rho_je)\le b$ , $x\ge0$ (p. 1157).

Significance

The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in $M$ , of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column $j$ is inflated by the full radius $\rho_j$ , which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.

The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.

Difficulty

The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every $A\in M$ " to $\bar A$ uses that the supremum of a sum of independent terms is the sum of suprema, which needs every $K_j$ nonempty and the scalars $x_j$ nonnegative; with an empty activity set the Minkowski sum is empty and every $x\ge0$ becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.

Formalization scope

Vectors are Fin m → ℝ and Fin n → ℝ, with indices $0,\dots,m-1$ in place of $1,\dots,m$ ; the order on vectors is componentwise.
Feasibility of (I) is the Minkowski-sum inclusion (∑ j, x j • K j) ⊆ R (pointwise set operations) together with $x\ge0$ . It is not defined as "for every choice $a_j\in K_j$ ", which would make milestones 1 and 5 trivial, and $\bar A$ is constructed from the $K_j$ , not an arbitrary matrix dominating $M$ , which would make the goal trivial.
$\delta^*$ is valued in EReal. The entries of $\bar A$ are its real conversions, so every statement mentioning $\bar A$ assumes $K_j\neq\emptyset$ and $\delta^*(e_i\mid K_j)<\infty$ , the paper's standing assumptions (pp. 1154–1156). Convexity of the $K_j$ is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of $K$ ).
An optimal solution is a feasible point attaining the maximum of $c\cdot x$ ; the paper writes $\sup$ and does not discuss attainment. Because the goal identifies the feasible sets, the two problems also have equal suprema.
Hyperspheres use the Euclidean norm (EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii $\rho_j\ge0$ .
The support functional restates the published FenchelRobust.Counterpart.supportFun with the same body.
Not formalized: Magnanti's extension to $\ge$ and $=$ rows (p. 1156), and the remarks on (GLP) and stochastic programming. Contributions of proofs of any milestone, and of an EReal statement equating the optimal values, are welcome.

Selected references

A. L. Soyster, Convex Programming with Set-Inclusive Constraints and Applications to Inexact Linear Programming, Operations Research 21(5), 1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Mathematics of Operations Research 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal and A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Mathematical Programming 88, 411–424, 2000. https://doi.org/10.1007/PL00011380
D. Bertsimas and M. Sim, The Price of Robustness, Operations Research 52(1), 35–53, 2004. https://doi.org/10.1287/opre.1030.0065

12 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 1: The State Probabilities of an Aperiodic Equilibrium Process Converge to (1/μ₁)∫φ_A(v){1 − F(v)}dvResearch Paper

Motivation

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

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

Timeline.

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 2

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

10 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 3: A Cumulative Process Has Mean (κ₁/μ₁)t + o(t) and Variance (t/μ₁){σ₂² − 2ρσ₁σ₂κ₁/μ₁ + σ₁²(κ₁/μ₁)²} + o(t)Research Paper

Why cumulative-process moments matter

Many stochastic systems accumulate a real-valued quantity while repeatedly returning to a state at which a new cycle begins. A queue may accumulate work or cost, a component may accumulate wear, and a recurrent system may accumulate time in a state. The observations at a fixed clock time usually cut through a cycle. This makes the moments of the observed process different from the moments of a sum stopped exactly at a regeneration epoch. W. L. Smith introduced cumulative processes to state mean, variance, ergodic, and central limit results for this setting in a common language (Smith 1955, §5).

The mean growth rate describes the long-run reward per unit time. The variance growth rate also records the dependence between a cycle's length and its reward. That dependence matters in systems where unusually long cycles tend to accumulate unusually large rewards; assuming the two are independent would erase a term in Smith's formula (Smith 1955, Theorem 8). This mission targets the exact first-order mean and variance asymptotics, along with the source results Smith uses to pass from completed cycles to observations at ordinary times.

Renewal and cumulative-process setting

Work on one probability space $(\Omega,P)$ . The cycle lengths $t_1,t_2,\ldots$ are nonnegative, independent, identically distributed random variables whose common law is not concentrated at zero. Set $T_0=0$ and $T_n=t_1+\cdots+t_n$ for $n\geq1$ . Thus $T_n$ is the $n$ th renewal epoch after the initial renewal at time zero. For $t\geq0$ , $n_t$ counts the epochs $T_k\leq t$ , including $T_0$ . The corresponding renewal function is $H_U(t)=\mathbb E[n_t]$ , where $U=\delta_0$ is Smith's zero-delay law. These conventions come from §2·1 and §5·2 of the paper (Smith 1955, pp. 9 and 23).

A cumulative process $w_t$ is real valued, starts at $w_0=0$ , and has almost surely bounded variation on each finite nonnegative time interval. The cycle reward is $y_n=w_{T_n}-w_{T_{n-1}}$ . Write $\tilde w_t$ for the total variation of the path on $[0,t]$ and $\tilde y_n$ for its variation on $[T_{n-1},T_n]$ . For the moment results, the cycle vectors $(t_n,y_n,\tilde y_n)$ are independent and identically distributed across $n$ . Their coordinates within one cycle may be dependent. This joint-cycle interpretation is required by Smith's common joint distribution for $(t_i,y_i)$ in the proof of Lemma 5 (Smith 1955, pp. 23–24).

Let $\mu_r=\mathbb E[t_1^r]$ , $\kappa_r=\mathbb E[y_1^r]$ , and $\tilde\kappa_r=\mathbb E[\tilde y_1^r]$ when the moments exist. Put $\sigma_1^2=\operatorname{var}(t_1)$ , $\sigma_2^2=\operatorname{var}(y_1)$ , and $c=\operatorname{cov}(t_1,y_1)$ . Smith writes $c=\rho\sigma_1\sigma_2$ , with $\rho$ the cycle length–reward correlation. The covariance remains defined when either variance is zero. The auxiliary sum $Y_t=\sum_{i=1}^{n_t+1}y_i$ includes a reward beyond the cycles completed by time $t$ , exactly as in (5·2·1) (Smith 1955, p. 23).

Formalization targets

The first target is the mean part of Theorem 8. If $\mu_1$ and $\tilde\kappa_1$ are finite, then

\mathbb E w_t=\frac{\kappa_1}{\mu_1}t+o(t)\qquad(t\to\infty).

The goal includes the variance part under the additional assumptions $\mu_2<\infty$ and $\tilde\kappa_2<\infty$ :

\operatorname{var}(w_t)=\frac{t}{\mu_1} \left\{\sigma_2^2-2c\frac{\kappa_1}{\mu_1} +\sigma_1^2\left(\frac{\kappa_1}{\mu_1}\right)^2\right\}+o(t).

Both limits are along real time, and neither assumes that a cycle's length and reward are independent. The milestone list contains the mean and variance limits for $Y_t$ , the cycle-moment estimate used for the incomplete cycle, and Theorem 8(i) as the explicit mean target (Smith 1955, Lemmas 4, 5, 9 and Theorem 8).

What the result supplies

The theorem gives a linear approximation to the process's expected value and variance, with errors smaller than the observation horizon. The leading variance coefficient separates reward variability, cycle-length variability, and their covariance. It can therefore be used without a false independence assumption when the duration of a cycle affects the amount accumulated during it. The formulas are first-order statements; they do not claim a bounded error or a limiting distribution (Smith 1955, (5·3·6)–(5·3·7)).

Formalizing these statements requires reusable definitions of renewal counts, path variation, random-cycle rewards, and the moment conditions that make expectations and variances genuine. The statement is a draft target, not a claim that Smith's proof already has a machine-checked reconstruction. A completed development would also give formal tools for other regenerative reward models whose observations occur between renewal epochs.

Main mathematical difficulty

The auxiliary sum $Y_t$ is sampled at a random index, while $w_t$ is observed at a deterministic clock time. They differ by part of a cycle that crosses $t$ . Ordinary laws for sums of a fixed number of independent rewards do not directly control either this random index or the crossing-cycle contribution. At second order, a bound on the mean difference alone does not determine the variance difference. The length–reward covariance must also survive the passage from completed cycles to the continuous-time process (Smith 1955, pp. 24–28).

Formalization scope and conventions

Lean uses real time and real-valued paths. Cycle laws are represented by random variables on one probability space; the renewal at zero is explicit. The renewal count takes the value zero on a path with infinitely many renewals before a finite time, a null event under the nondegenerate i.i.d. length law. Variation is represented by Mathlib's extended nonnegative eVariationOn and converted to a real number only under the almost-sure bounded-variation condition. The theorem states integrability of $w_t$ and its square as consequences of the cycle-moment assumptions, avoiding default values for divergent real integrals or variance. A finite $r$ th moment is an integrability condition, not a comparison between a real number and infinity.

The paper's exact identity (5·2·2) is off by one under its own definitions of $n_t$ and $Y_t$ ; the mission targets its valid asymptotic consequence (5·2·3). The last variance in the printed Lemma 5 coefficient is $\sigma_2^2$ , while Theorem 8 and the calculation require $\sigma_1^2$ . Milestone provenance retains the printed text; the Lean statements use the corrected coefficient. Lemma 9 is formalized for the absolute $p$ th moment $\mathbb E|y_1|^p$ of the cycle increment, which is the printed statement for a nonnegative cycle quantity such as the variation $\tilde y_n$ to which Theorem 8 applies it. Solvers may contribute the renewal and random-index estimates needed for the listed targets. A definition that makes rewards independent of cycle lengths would remove the covariance term and would not represent this mission's model.

Selected references

W. L. Smith, Regenerative stochastic processes, Proceedings of the Royal Society of London, Series A 232(1188):6–31, 1955. DOI: 10.1098/rspa.1955.0198.

7 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Renewal Theory and Its Ramifications: The Elementary Renewal Theorem H(t)/t → 1/μ₁ as t → ∞, Including the Case μ₁ = ∞Research Paper

Motivation

A renewal process models the successive replacements of an article that fails and is replaced at once: light bulbs, machine components, the inter-arrival times of a queue. The central quantity is the renewal function $H(t)$ , the expected number of replacements up to time $t$ . Long-run average costs of maintenance and inventory policies, the throughput of regenerative systems and the rates in renewal–reward arguments are all read off the growth of $H(t)$ . W. L. Smith's survey Renewal Theory and Its Ramifications (J. R. Statist. Soc. B, 1958) organized the field around this function and opened with its oldest general limit result, the elementary renewal theorem, proved in full in §1.2 (pp. 245–247).

Timeline.

1941 — W. Feller gives the first rigorous proof of the elementary renewal theorem, through a Tauberian theorem for Laplace integrals.
1946 — C. Stein proves, for general sequential sampling procedures, that the stopping index has a finite exponential moment; for renewal processes this gives finite moments of all orders of the count $N_t$ .
1948 — J. L. Doob gives a purely probabilistic proof, through the strong law of large numbers.
1958 — Smith presents Doob's proof in modified form: an identity for the residual lifetime gives the lower bound, and a truncation of the lifetimes gives the upper bound, also when the mean lifetime is infinite.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1, X_2, \dots$ real random variables that are mutually independent, identically distributed, non-negative, and not almost surely zero: $P(X_i = 0) < 1$ . Lifetimes equal to zero with positive probability are allowed.

The renewal epochs are $S_0 = 0$ and $S_n = X_1 + \dots + X_n$ .
The counting variable $N_t$ is the number of $n \ge 1$ with $S_n \le t$ , the number of renewals in $[0,t]$ ; for $t \ge 0$ it is the largest $n$ with $S_n \le t$ .
The renewal function is $H(t) = \mathbb E N_t$ and the mean lifetime is $\mu_1 = \mathbb E X_i \in (0,\infty]$ .
The residual lifetime $\zeta_t$ is defined by $S_{N_t+1} = t + \zeta_t$ .
For $\Delta > 0$ the truncated process is $X_i^\dagger = \min(X_i,\Delta)$ , with associated $S_n^\dagger$ , $N_t^\dagger$ , $H^\dagger$ , $\mu_1^\dagger$ , $\zeta_t^\dagger$ .

In Lean these are IsRenewalProcess P X, S X n, N X t, H X P t, mu1 X P, zeta X t and trunc Δ X in the namespace SmithRenewal.Elementary.

Formalization targets

Goal: the elementary renewal theorem (§1.2, p. 246)

\frac{H(t)}{t} \longrightarrow \mu_1^{-1} \qquad (t \to \infty),

with $\mu_1 \le \infty$ and $\mu_1^{-1} = 0$ when $\mu_1 = \infty$ . No moment beyond the first is assumed, and not even the first: the infinite-mean case is part of the goal.

Milestones, in the order of the paper's argument

Stein's result (p. 245). There is $\theta_0 > 0$ with $\mathbb E e^{\theta N_t} < \infty$ for every real $\theta \le \theta_0$ ; hence $N_t$ has finite moments of all orders and $H(t) < \infty$ .
Equation (1.1) (p. 246). If $\mu_1 < \infty$ , then for $t \ge 0$

t + \mathbb E\zeta_t = \mu_1\{1 + H(t)\}.

Lower bound (p. 246). If $\mu_1 < \infty$ , $\liminf_{t\to\infty} H(t)/t \ge \mu_1^{-1}$ .
Truncation (p. 246). $(X_i^\dagger)$ is a renewal process, $S_n^\dagger \le S_n$ , $N_t^\dagger \ge N_t$ , $H^\dagger(t) \ge H(t)$ and $\zeta_t^\dagger \le \Delta$ .
Upper bound (p. 246). For every $\Delta > 0$ ,

\limsup_{t\to\infty}\frac{H(t)}{t} \le \limsup_{t\to\infty}\frac{H^\dagger(t)}{t} \le \{\mu_1^\dagger\}^{-1}.

Letting $\Delta \to \infty$ (p. 247). $\mu_1^\dagger \to \mu_1$ in $[0,\infty]$ .

Significance

The result. The elementary renewal theorem is the law of large numbers for the renewal function: in the long run renewals occur at mean rate $1/\mu_1$ . It is the basis of the renewal–reward theorem, of long-run average cost formulas for replacement, maintenance and $(s,S)$ inventory policies, and of rate computations for regenerative queues. The sharper results of Smith's survey — Blackwell's theorem (1.2) and the key renewal theorem (1.3) — refine it and reduce to it on averaging.

Formalizing it. The theorem has been proved since 1941; what this mission adds is a machine-checked development of the continuous-time, real-valued renewal process in Lean, which Mathlib does not contain. Mathlib has the strong law of large numbers, independence and identical distribution, but no renewal counting process, no Wald identity and no renewal function. The platform holds a proved discrete Erdős–Feller–Pollard theorem for integer renewal sequences, a different statement about a different object; to the curators' knowledge the elementary renewal theorem for general non-negative lifetimes has not been formalized.

Difficulty

The almost-sure statement $N_t/t \to 1/\mu_1$ is close to the strong law, since $S_{N_t} \le t < S_{N_t+1}$ . The obvious next step, taking expectations, fails: almost-sure convergence does not imply convergence of means, and $N_t/t$ has no evident integrable dominating function. The exact relation (1.1) involves a sum with a random number of terms stopped at $N_t + 1$ , and by itself it bounds $H(t)/t$ from one side only, because the residual lifetime $\zeta_t$ can have infinite mean. When $\mu_1 = \infty$ the relation is unavailable altogether, yet the theorem still claims a limit. Throughout, $N_t$ is a priori allowed to be infinite on a null set and $H(t)$ to be infinite, so finiteness itself is part of what must be established.

Formalization scope

Representation. Lifetimes are X : ℕ → Ω → ℝ, with the paper's $X_1, X_2, \dots$ as X 0, X 1, …. IsRenewalProcess P X bundles measurability, mutual independence (iIndepFun), IdentDistrib (X i) (X 0), non-negativity at every sample point, and P {X 0 = 0} < 1. Strict positivity is not assumed.
Counting. $N_t$ is the cardinality in ℕ∞ of $\{n \ge 1 : S_n \le t\}$ ; it is $0$ for $t < 0$ and may be $\infty$ on a null set.
Expectations. $H(t)$ , $\mu_1$ and $\mathbb E\zeta_t$ are lower Lebesgue integrals with values in $[0,\infty]$ . No finiteness is presupposed; finiteness of $H(t)$ is milestone 1.
Ratios and limits. $H(t)/t$ is formed in $[0,\infty]$ and limits are taken as $t \to \infty$ along the reals; $\mu_1^{-1}$ is the inverse in $[0,\infty]$ , so $\infty^{-1} = 0$ is the paper's convention.
Residual lifetime. $\zeta_t = S_{N_t+1} - t$ , reading $N_t$ through ENat.toNat; on the null event $N_t = \infty$ this is $S_1 - t$ , which never affects an expectation.
Truncation. $H^\dagger$ , $\mu_1^\dagger$ , $\zeta_t^\dagger$ are the same definitions applied to trunc Δ X, never separate formulas.

Ruled out. A goal restricted to $\mu_1 < \infty$ , a renewal function defined through $\sum_r P(S_r \le t)$ or the renewal equation, or a real-valued ratio with $1/\mu_1$ in $\mathbb R$ (where $1/0 = 0$ and an infinite integral becomes $0$ ) would each be a different, weaker or trivially true statement; none of them is the goal.

Needed infrastructure and welcome contributions. A Wald identity for stopping indices of i.i.d. sums with values in $[0,\infty]$ ; the comparison of a renewal count with a negative binomial count; uniform-in- $t$ moment bounds for $N_t$ ; and the lim inf/lim sup squeeze in $[0,\infty]$ . The renewal process definitions and the Wald identity are reusable for Blackwell's theorem, the key renewal theorem and renewal–reward arguments. Alternative proofs of the goal (Feller's Tauberian route, a uniform-integrability argument) are welcome as long as they prove the stated goal.

Selected references

W. L. Smith, Renewal Theory and Its Ramifications, J. R. Statist. Soc. B 20(2):243–283, 1958. https://doi.org/10.1111/j.2517-6161.1958.tb00294.x
W. Feller, On the integral equation of renewal theory, Ann. Math. Statist. 12(3):243–267, 1941. https://doi.org/10.1214/aoms/1177731708
C. Stein, A note on cumulative sums, Ann. Math. Statist. 17(4):498–499, 1946. https://doi.org/10.1214/aoms/1177730890
J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63(3):422–438, 1948. https://doi.org/10.1090/S0002-9947-1948-0025098-8

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Graph Theory·Captain: mikedeng1

Graphs and Cooperation in Games: The Unique Fair Allocation Rule, the Shapley Value of the Graph-Restricted Game, Is Totally Stable for Superadditive GamesResearch Paper

Motivation

Classical cooperative game theory assumes that any coalition of players can form and coordinate. In many settings cooperation is mediated by pairwise relationships: communication lines, contracts, alliances, or trade links. Roger Myerson's discussion paper Graphs and Cooperation in Games (Northwestern University, 1976; published in Mathematics of Operations Research 2(3), 1977, doi:10.1287/moor.2.3.225) models such a cooperation structure as a graph on the set of players and asks how the players should share the worth of the game when only linked players can coordinate directly.

The answer, now called the Myerson value, is the starting point of the literature on communication situations and network games. It underlies later work on network formation (Jackson and Wolinsky, A strategic model of social and economic networks, JET 1996) and on allocation rules for networks, and it is a standard textbook example of an axiomatic solution concept.

Timeline:

1953. Shapley defines the Shapley value $\varphi$ for transferable-utility games by efficiency, symmetry, a carrier axiom and additivity (Shapley 1953).
1976–1977. Myerson introduces cooperation graphs, the fairness (equal gains from each link) condition, proves existence and uniqueness of the fair allocation rule, identifies it as the Shapley value of the graph-restricted game, proves its total stability for superadditive games, and extends existence and uniqueness to games without transferable utility in graph function form.

Setting

Let $N$ be a nonempty finite set of players and $CL$ the set of nonempty coalitions $S\subseteq N$ . A game in characteristic function form is a vector $v\in\mathbb R^{CL}$ ; $v_S$ is the transferable wealth coalition $S$ can divide.

A link $n{:}m$ is an unordered pair of distinct players and a graph $g$ is a set of links; $GR$ is the set of all graphs, $\bar g^N$ the complete graph, $g\setminus n{:}m$ the graph with one link removed, and $|g|$ the number of links. Players $a,b$ are connected in $S$ by $g$ if $a=b\in S$ or a path of links of $g$ joins them through players of $S$ only; the classes form the partition $S/g$ of $S$ , and $N/g$ is the set of connected components of $g$ . The graph-restricted game is

(v/g)_S=\sum_{T\in S/g}v_T .

An allocation rule is a function $Y:GR\to\mathbb R^N$ , with $Y_n(g)$ the payoff of player $n$ under cooperation structure $g$ . It is a fair allocation rule for $v$ if

(efficiency, (7)) $\sum_{n\in S}Y_n(g)=v_S$ for every $g$ and every component $S\in N/g$ , and
(equity, (10)) $Y_n(g)-Y_n(g\setminus n{:}m)=Y_m(g)-Y_m(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$ .

$Y$ is totally stable if $Y_n(g)\ge Y_n(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$ , and $v$ is superadditive if $v_{S\cup T}\ge v_S+v_T$ for disjoint $S,T\in CL$ .

A game in graph function form assigns to every pair $(S,g)$ with $S\in N/g$ a closed, comprehensive (closed under decreasing coordinates), proper ( $\emptyset\ne W\ne\mathbb R^S$ ) set $w(S,g)\subseteq\mathbb R^S$ of feasible payoffs; its fair allocation rule replaces (7) by (14), $(Y_n(g))_{n\in S}\in\partial w(S,g)$ .

Formalization targets

Goal: Theorem 3 (p. 8)

If $v$ is superadditive, then the fair allocation rule $Y$ for $v$ is totally stable:

Y_n(g)\ge Y_n(g\setminus n{:}m)\qquad\text{for all } g\in GR,\ n{:}m\in g .

Theorem 1 (p. 7) and Theorem 4 (p. 10)

Every $v\in\mathbb R^{CL}$ has a unique fair allocation rule; every game $w$ in graph function form has a unique $Y$ satisfying (14) and (10).

Theorem 2 (p. 8)

The fair allocation rule is

Y(g)=\varphi(v/g)\quad\text{for all }g\in GR,\qquad\text{in particular } Y(\bar g^N)=\varphi(v).

The milestones follow the paper's Section 7: the steps of the proof of Theorem 4 (displays (15)–(17)), Theorem 4, Theorem 1, the decomposition of $v/g$ and the efficiency and equity of $\varphi(v/g)$ (proof of Theorem 2), Theorem 2, and the monotonicity of $v/g$ and $\varphi(v/g)$ in a link (proof of Theorem 3). Theorem 3 is the goal because its proof uses the formula of Theorem 2, whose proof uses the uniqueness of Theorem 1, which is the transferable-utility case of Theorem 4: all four numbered results lie on one path.

Significance

The theorems give an axiomatic foundation for allocation in networks: two natural requirements, component-wise efficiency and equal gains from each link, single out one rule, and that rule is an explicit formula built from the Shapley value. At the complete graph it recovers the Shapley value itself, so the result is also a new characterization of the Shapley value. Total stability says that, for superadditive games, no player has an incentive to break a link, which connects the allocation rule to the question of which networks form.

The results are proved in the paper. A search of the platform found no formalization of cooperation graphs, the graph-restricted game, the Myerson value or total stability; the Shapley value is available as a platform definition and is reused. This mission produces machine-checked statements of all four theorems and of the intermediate steps of their proofs, together with a reusable definition layer for communication situations.

Difficulty

The equity condition (10) relates the payoff at a graph to the payoff at a graph with one fewer link, and it constrains only pairs of linked players; it is not evident that these conditions, together with efficiency on components, determine the rule at every graph, nor that they are consistent. Uniqueness and existence must hold simultaneously for all $2^{|\bar g^N|}$ graphs, and the constraints couple each graph to all of its subgraphs and each player to every other player of its component. In the graph function form, efficiency becomes a boundary condition on a closed comprehensive set, and the existence and uniqueness of the relevant extremal point depend on all three properties of $w(S,g)$ .

Identifying the rule with $\varphi(v/g)$ requires the efficiency of the Shapley value on each component of $g$ , which is not the efficiency of $\varphi$ on $N$ , and equity requires tracking how the partitions $S/g$ change when a link is removed. Total stability is false for general games: without superadditivity a player can gain by cutting a link, so the hypothesis cannot be dropped.

Formalization scope

Players are Fin n, with $0<n$ in every theorem as the paper assumes $N$ nonempty; the paper's player $k$ is index $k-1$ . The general game carrier has its own definition module, and the graph-specific definitions build on it. Graphs are SimpleGraph (Fin n): $\bar g^N$ is ⊤, the empty graph ⊥, $h\subseteq g$ is h ≤ g and $h\subset g$ is h < g. A game is a function Finset (Fin n) → ℝ; its value at $\emptyset$ is a junk coordinate that no definition reads, and no theorem assumes $v_\emptyset=0$ . Superadditivity quantifies over nonempty coalitions only. The Shapley value is the platform definition Supermodularity.Cooperative.ShapleyValue, applied after resetting the value at $\emptyset$ to $0$ . $\mathbb R^S$ is ↥S → ℝ with the product topology, and $\partial$ is the topological frontier.

Explicit readings of the typescript:

The printed definition of "connected in $S$ by $g$ " (p. 3) asks $n^i\in S$ only for $i\ge1$ ; the formalization requires every vertex of the path, including the start, to lie in $S$ , which makes $S/g$ the partition of $S$ the paper describes.
Comprehensiveness (p. 10) prints " $\forall n\in N$ " for coordinates of vectors in $\mathbb R^S$ ; read as $n\in S$ .
Display (17) writes $Y_n(h)$ under the index $m\in S$ ; read as $Y_m(h)$ , as in (18b).
The proof headed "PROOF OF THEOREM 4." on p. 13 is the proof of Theorem 3.
"The unique fair allocation rule" in Theorems 2 and 3 is stated for every fair allocation rule; existence and uniqueness are Theorem 1.
The paper's $N$ is nonempty; every theorem carries the corresponding hypothesis $0<n$ .

The equity and stability conditions quantify over links of $g$ only. Quantifying over all pairs of players would make Theorem 1 false and the goal vacuous, so that reading is ruled out. Likewise (14) is boundary membership, not membership in $w(S,g)$ .

Contributions welcome: general lemmas on the partitions $S/g$ (refinement under link deletion, restriction to components), Möbius inversion over the subgraph lattice of a finite simple graph, the carrier and null-player properties of the Shapley value, and the extremal-point lemma for closed comprehensive sets. These are reusable beyond this mission.

Selected references

R. B. Myerson, Graphs and Cooperation in Games, Discussion Paper No. 246, CMS-EMS, Northwestern University, September 1976; published in Mathematics of Operations Research 2(3):225–229, 1977. https://doi.org/10.1287/moor.2.3.225
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, pp. 307–317. https://doi.org/10.1515/9781400881970-018
M. O. Jackson and A. Wolinsky, A Strategic Model of Social and Economic Networks, Journal of Economic Theory 71(1):44–74, 1996. https://doi.org/10.1006/jeth.1996.0108

18 thms2 active usersReviewed

Linear Optimization Optimization Probability+1·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 4: For a Random Subspace, ‖Pq‖⁻∞ ≤ (log n/n)‖r‖² with Probability Tending to OneResearch Paper

Motivation

Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6

Setting

Fix a dimension $n$ , an integer $d$ with $0\le d\le n$ , and a vector $r\in\mathbb R^n$ . Draw a random $d$ -dimensional subspace $U$ from the distribution invariant under orthogonal transformations. Let $p$ be the Euclidean orthogonal projection of $r$ onto $U$ , and put $q=r-p$ , its projection onto $U^\perp$ . The matrix $P=\operatorname{diag}(p)$ turns the vector $q$ into the coordinatewise product $Pq=(p_jq_j)_{j=1}^n$ .

For a coordinate vector $z$ , let $z^-=(\min\{z_j,0\})_{j=1}^n$ and $\|z\|^-_\infty=\|z^-\|_\infty$ . Thus $\|Pq\|^-_\infty$ records the magnitude of the largest negative coordinate of $Pq$ . An unsubscripted vector norm is always the Euclidean $\ell_2$ norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2

The formal model samples an $(n-d)\times n$ matrix $G$ with independent standard normal entries and sets $U=\ker G$ . The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension $d$ . The construction covers the endpoint cases $d=0$ and $d=n$ as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6

Formalization targets

Theorem 5

For arbitrary choices $r_n\in\mathbb R^n$ and $d_n\le n$ at each dimension, the central target is

\Pr\left\{\|P_nq_n\|^-_\infty\le \frac{\log n}{n}\|r_n\|_2^2\right\} \longrightarrow 1\qquad(n\longrightarrow\infty).

The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of $r_n$ and $d_n$ may change with $n$ ; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13

Source milestones

The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by $\sqrt{3\log n/n}$ with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6

Significance

The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7

The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.

Difficulty

A direct norm bound on $p$ and $q$ loses the coordinate information needed for the factor $\log n/n$ . The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so $\|r\|$ is the $\ell_2$ norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated $d$ -dimensional law almost surely.

Lemma 6 concerns $d,m\ge1$ and $n\ge2$ , where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains $d=0$ , $d=n$ , and $r=0$ . Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition $\varepsilon>0$ . All limits are probabilities tending to one, never probability one at every finite $n$ .

Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.

Selected references

Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. DOI
Sidney I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71, cited in the report for the Gaussian maximum estimate. DOI

7 thms2 active usersReviewed

Completed

Dynamic Programming Markov Chain Stochastic Systems·Captain: mikedeng1

Quality Control under Markovian Deterioration 1: A Discounted-Optimal Policy Produces, Inspects, Produces Again and Revises on Successive Intervals of the BeliefResearch Paper

Motivation

A production process deteriorates over time, and the state it is in cannot be observed directly. Each period the operator chooses among three actions: produce without looking, produce and inspect the item (which reveals the current state at a cost), or revise the process back to its good state. This is one of the earliest partially observed Markov decision problems with a costly observation action, and it is the prototype of the inspection and machine-replacement models that followed in operations research and maintenance theory. Ross (Management Science 17(9), 1971) set it up for a countable state space, reduced it to a fully observed problem on beliefs, and determined the structure of an optimal policy for two states.

Intuition suggests a three-region policy for two states: produce while the probability of the bad state is small, inspect at intermediate probabilities, revise when it is large. Ross showed that the true structure has up to four regions: produce, inspect, produce again, revise. This mission formalizes that structure theorem and the general results it rests on.

Setting

The underlying process has a countable set of states $0,1,2,\dots$ , with transition probabilities $P_{ij}$ from state $i$ at the end of a period to state $j$ at the beginning of the next. In state $i$ , producing without inspection costs $C_i$ , producing with inspection costs $I_i$ , and revising costs $R_i$ ; costs are bounded, and future costs are discounted by $\beta\in(0,1)$ . A revision puts the process in state $0$ .

The decision maker tracks a belief $P=(P_0,P_1,\dots)$ , a probability vector on the states, ranging over

S=\Big\{P: P_i\ge0,\ \sum_iP_i=1\Big\}.

Producing without inspection moves the belief to $TP$ , with $(TP)_i=\sum_jP_jP_{ji}$ . Inspecting reveals the state; if it is $i$ , the next belief is the row $e^i=(P_{i0},P_{i1},\dots)$ . Revising leads to $e^0$ .

The $\beta$ -discounted optimal cost $V_\beta$ is the limit of value iteration: $V^0=0$ and

V^{n+1}(P)=\min\Big\{\sum_iP_iC_i+\beta V^n(TP);\ \sum_iP_iI_i+\beta\sum_iP_iV^n(e^i);\ \sum_iP_iR_i+\beta V^n(e^0)\Big\}.

The three terms with $V^n$ replaced by $V_\beta$ form the right side of the optimality equation (1). The $\beta$ -optimal produce, inspect and revise regions are the sets of beliefs at which the corresponding term equals $V_\beta(P)$ , and a stationary rule is $\beta$ -optimal when it always selects an action attaining the minimum.

In the two-state process of §3, state $0$ is good and state $1$ is bad: $P_{00}=1-\pi$ , $P_{11}=1$ , $C_0=0$ , $C_1=C$ , $I_0=I_1=I$ , $R_0=R_1=R$ , with $C<I<R$ . The belief is a number $P\in[0,1]$ , the probability of the bad state, $TP=P+\pi-\pi P$ , and the optimality equation becomes

V_\beta(P)=\min\{CP+\beta V_\beta(TP);\ I+\beta PV_\beta(1)+\beta(1-P)V_\beta(\pi);\ R+\beta V_\beta(\pi)\}.\tag{3}

Formalization targets

Goal: Theorem 3.3, the four-region structure

There are thresholds $\pi\le P_1\le P_2\le P_3$ with $P_2\le1$ such that the rule

\text{produce on }[0,P_1),\quad\text{inspect on }[P_1,P_2),\quad\text{produce on }[P_2,P_3),\quad\text{revise on }[P_3,1]

is $\beta$ -optimal, and $P_3\le1$ whenever revising is $\beta$ -optimal at some belief. Degenerate thresholds (empty intervals) are allowed, so the statement fixes only the order of the regions, not their number.

Milestones

(1): value iteration converges on $S$ , $V_\beta$ is bounded, solves (1), and is its unique bounded solution.
Lemma 2.1: $V_\beta$ is concave on $S$ .
Theorem 2.2: the $\beta$ -optimal inspect and revise regions are convex.
(3): the two-state optimality equation, as an instance of (1).
Lemma 3.1: in the two-state model $V_\beta$ is nondecreasing on $[0,1]$ .
Lemma 3.2: for $0\le P\le\pi$ , producing is strictly better than inspecting and than revising.

Significance

Theorem 3.3 reduces the search for an optimal policy in the two-state problem to the choice of three numbers, and it fixes the order of the regions: there is never a revise region below an inspect region, and inspection never occurs below the deterioration probability $\pi$ . Together with Theorems 3.4 and 3.7 of the same paper (separate missions in this series), it is the basis for computing optimal inspection policies by searching over thresholds. Theorem 2.2 holds for any countable state space and is the general form of the observation that, in partially observed problems with linear-in-belief action costs, the regions of the "information" and "reset" actions are convex while the region of the passive action need not be.

The results are proved in the paper. As far as a search of the Prove2Me library shows (October 2026), none of them is formalized. Related formal work treats other models: belief-state reductions of finite POMDPs, and abstract contraction models for discounted dynamic programming. The mission produces machine-checked versions of the general model's optimality equation, the concavity of its value function, the convexity of two of its regions, and the two-state structure theorem.

Difficulty

The paper's proofs are short and lean on facts quoted from the literature. Theorem 3.3's proof is two sentences long. Filling it in requires several facts that the paper leaves implicit. The revise region of the two-state model is a closed right-hand interval. The inspect region meets $[0,1]$ in an interval, through the affine embedding $P\mapsto(1-P,P)$ of $[0,1]$ into $S$ . The half-open endpoints of the rule select optimal actions. That last point needs continuity of $V_\beta$ inside $(0,1)$ , a consequence of concavity, and Lemma 3.2 at the left end. The naive reading of the printed theorem, with all three thresholds in $[0,1]$ , is false in general (see below), so the threshold bookkeeping cannot be skipped.

On the general side, the optimality equation (1) is quoted from Blackwell. Here it must be proved for value iteration on the belief simplex of a countable state space, where the inspect term is an infinite series of values at the rows $e^i$ . Its convergence and the contraction estimates use the boundedness of the costs.

Formalization scope

The general model is a structure over a type ι with [Countable ι], a distinguished state i₀, a transition matrix Pm, costs C I R : ι → ℝ and β. A separate predicate Model.Valid requires nonnegative entries, rows with HasSum (Pm i) 1, bounded costs and 0 < β < 1. The simplex uses HasSum P 1, never tsum, so it consists of genuine probability vectors. $V_\beta$ is defined as limUnder atTop of value iteration from $V^0=0$ , which is the paper's own characterization in the proof of Lemma 2.1. It is not an arbitrary function assumed to satisfy (1). The paper's definition as an infimum over measurable policies is not formalized; the policy class would be a separate mission. Regions are subsets of $S$ .

The two-state model is the instance ι = Fin 2 with $P_{00}=1-\pi$ , $P_{01}=\pi$ , $P_{10}=0$ , $P_{11}=1$ , and its value at the scalar belief $P$ is the general $V_\beta$ at $(1-P,P)$ . The general Lemma 2.1 and Theorem 2.2 therefore apply to it without restatement. Standing hypotheses of §3 are $0<\beta<1$ , $0\le\pi\le1$ and $0<C<I<R$ . $0<C$ is implicit in the paper, where the good state costs $0$ and the bad state $C$ . " $\beta$ -optimal rule" means a rule selecting a minimizer of the right side of (3) at every $P\in[0,1]$ , the criterion the paper quotes on p. 588. "Every $\beta$ -optimal policy produces" (Lemma 3.2) means that producing is the unique minimizer.

Threshold repair. The paper prints $\pi\le P_1\le P_2\le P_3\le1$ . This is false when revising is never optimal, for instance when $R>C/(1-\beta(1-\pi))$ : then always producing is optimal and revising at $P=1$ is strictly worse, so no rule revising on a nonempty $[P_3,1]$ is optimal. The goal keeps $P_3\le1$ exactly when the $\beta$ -optimal revise region is nonempty and otherwise allows $P_3>1$ ; the rest of the printed chain, $\pi\le P_1\le P_2\le1$ , is kept. Adding the hypothesis $R<C/(1-\beta(1-\pi))$ instead would drop a case the paper covers.

The statement admits no trivializing reading. The thresholds are quantified existentially, but the rule must be optimal at every belief in $[0,1]$ , $V_\beta$ is pinned down by its definition, and the paper's numbers ( $C=4$ , $\pi=0.1$ , $I=6$ , $R=10$ , $\beta=0.9$ ) satisfy all hypotheses.

Infrastructure needed: tsum manipulations on the belief simplex (linearity of $T$ , summability of $\sum_iP_iV(e^i)$ for bounded $V$ ), a sup-norm contraction argument for value iteration, and closure of concavity under minima and pointwise limits. The value-iteration and contraction lemmas are reusable for any discounted model with bounded costs. Contributions of intermediate lemmas, such as continuity of the two-state $V_\beta$ on $(0,1]$ or the bridge identities $T(1-P,P)=(1-TP,TP)$ , are welcome.

Selected references

S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9):587–596, 1971. https://doi.org/10.1287/mnsc.17.9.587
D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1):226–235, 1965. https://doi.org/10.1214/aoms/1177700285
K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X

9 thms2 active usersReviewed

Algorithmic Game Theory Probability·Captain: mikedeng1

Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables II: For I.I.D. Variables the Constant 2 Is Best Possible over Threshold RulesResearch Paper

Motivation

A prophet inequality compares two observers of a sequence of nonnegative random variables $X_1, \dots, X_n$ . The prophet knows all values in advance and collects $X_n^* = \max(X_1, \dots, X_n)$ . The gambler sees the values one at a time and must decide, irrevocably, when to stop and collect the current value. For independent variables the gambler's optimal value is at least half of $EX_n^*$ , and the factor $2$ is sharp. Prophet inequalities are a basic tool in the analysis of online mechanisms, posted-price auctions and online selection problems, where the gambler's rule is a pricing policy and the prophet is the offline optimum.

Optimal stopping rules are often difficult to compute and to implement. A threshold rule, which stops at the first value at least $c$ , is a posted price, and is the form used in applications. Samuel-Cahn (Ann. Probab. 12 (1984) 1213–1216) proved that a threshold rule alone attains the factor $2$ : with $m$ a median of $X_n^*$ , Theorem 1 of the paper gives $EX_n^* \le 2E^+X_{s(m)}$ or $EX_n^* \le 2E^+X_{t(m)}$ . Mission I of this series formalizes that theorem.

Timeline (as recounted on p. 1213 of the paper).

1978: Krengel and Sucheston show $EX_n^* \le 2V_n(\underline X)$ , where $V_n$ is the optimal stopping value, for independent $X_i \ge 0$ ; the constant $2$ cannot be improved for any $n \ge 2$ .
1981: Hill and Kertz show that strict inequality holds in all but trivial cases.
1982: Hill and Kertz show that for i.i.d. $X_i$ the best constant $\alpha_n$ for optimal rules depends on $n$ and is bounded by $1.6$ .
1983: Kertz (unpublished at the time) proves $\lim \alpha_n = 1 + a^* = 1.341\ldots$ for a constant $a^*$ given by an integral equation.
1984: Samuel-Cahn shows that a median threshold rule achieves the factor $2$ (Theorem 1), and that for threshold rules the factor $2$ cannot be lowered even for i.i.d. variables (Theorem 2). This mission is Theorem 2.

Setting

Fix $n \ge 1$ and a probability law $\mu$ on $[0, \infty)$ . Let $X_1, \dots, X_n$ be independent with common law $\mu$ , and $X_n^* = \max(X_1, \dots, X_n)$ . For a constant $c \ge 0$ the threshold rules are

$t(c)$ : the smallest $i < n$ with $X_i \ge c$ , and $t(c) = n$ otherwise;
$s(c)$ : the smallest $i < n$ with $X_i > c$ , and $s(c) = n$ otherwise.

The stopped value is $X_{t(c)}$ or $X_{s(c)}$ . The truncated expectations are $E^+X_{t(c)} = E[X_{t(c)} I(X_{t(c)} \ge c)]$ and $E^+X_{s(c)} = E[X_{s(c)} I(X_{s(c)} > c)]$ : they discard the forced stop at time $n$ below the threshold. The class $T_n^*$ is the set of all $t(c)$ and $s(c)$ with $c \ge 0$ .

The lower half of the theorem uses an explicit family. For $0 < a < 1$ , $b > 0$ , $c > 0$ and $n > b + c$ , the variables $X_i^{(n)}$ take the values $0$ , $a$ , $1$ with probabilities $1 - (b+c)/n$ , $c/n$ , $b/n$ . Two constants enter:

a^* = \frac{c(1 - e^{-b}) - b e^{-b}(1 - e^{-c})}{c(1 - e^{-b-c})}, \qquad Q(b, c) = 1 + \frac{e^{-b} - e^{-b-c}}{1 - e^{-b-c}} - \frac{b(e^{-b} - e^{-b-c})^2}{c(1 - e^{-b-c})(1 - e^{-b})}.

This $a^*$ is unrelated to the $a^*$ of the NOTE in §1 of the paper.

In Lean (SamuelCahnProphet.IID), a sample is x : Fin n → ℝ under iidLaw μ n, the product measure; tIdx x c and sIdx x c are $t(c)$ and $s(c)$ ; Emax, EstopT, EstopS, EplusT, EplusS are $EX_n^*$ , $EX_{t(c)}$ , $EX_{s(c)}$ and the $E^+$ terms; supE and supEplus are the two suprema over $T_n^*$ ; threePoint n a b c is the law of $X_i^{(n)}$ ; aStarIID and Q are the constants above.

Formalization targets

Goal: Theorem 2 (p. 1215)

\sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} E^+X_t}\right] = \sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} EX_t}\right] = 2,

over i.i.d. nonnegative $\underline X$ . It is stated as three facts: $EX_n^* \le 2 \sup_{T_n^*} E^+X_t$ for every $n$ and law; $\sup_{T_n^*} E^+X_t \le \sup_{T_n^*} EX_t$ ; and for every $\varepsilon > 0$ some $n$ and law with $(2 - \varepsilon)\sup_{T_n^*} EX_t < EX_n^*$ .

Milestones (proof of Theorem 2, p. 1215)

The upper bound $EX_n^* \le 2\sup_{T_n^*} E^+X_t$ , attributed to Theorem 1.
$\lim_n EX_n^{(n)*} = 1 - e^{-b} + a\{e^{-b} - e^{-b-c}\}$ .
For the three-point law, $\sup_{T_n^*} EX_t = \max\{EX_{t(a)}, EX_{t(1)}\}$ .
$W(a) = \lim_n EX^{(n)}_{t(a)} = (1 - e^{-b-c})(b + ac)/(b + c)$ .
$W(1) = \lim_n EX^{(n)}_{t(1)} = 1 - e^{-b}$ .
$W(a^*) = W(1)$ and $0 < a^* < 1$ .
With $a = a^*$ , $\lim_n EX_n^{(n)*}/\sup_{T_n^*} EX_t^{(n)} = Q(b, c)$ .
$Q(b, c) \to 2$ as $b \to 0^+$ and $c \to \infty$ .

Significance

Theorem 1 says a posted price recovers half of the prophet's value. Theorem 2 says this guarantee is tight within the class of threshold rules even under the most favourable independence structure, identical distributions. This matters because for optimal rules the i.i.d. constant is at most $1.6$ (Hill and Kertz 1982); the theorem separates threshold rules from optimal rules in the i.i.d. case and sets the benchmark that later single-threshold and order-selection analyses compare against.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces one: a formal model of threshold rules on an i.i.d. sample, exact asymptotics of the expected maximum and of two stopped values for a triangular array of three-point laws, the reduction of the class $T_n^*$ to two rules, and the two-parameter limit. The upper bound (milestone 1) is the i.i.d. case of mission I's goal, and may later be closed by reference to it.

Difficulty

The limits are "easily seen" on the page, but each requires controlling $(1 - x/n)^{n-1}$ uniformly with the exact law of a stopped index on a product space, including the forced stop at $n$ whose contribution vanishes only in the limit. Milestone 3 is a finite claim over an uncountable family of rules: every $t(c)$ and $s(c)$ with $c \ge 0$ must be shown to coincide almost surely with one of $t(0)$ , $t(a)$ , $t(1)$ or stopping at $n$ , and the first and last must be shown dominated by $t(a)$ for every finite $n > b + c$ , not only asymptotically. The final step is a joint limit in $(b, c)$ , in which $b/(1 - e^{-b}) \to 1$ while the correction term vanishes like $1/c$ ; an iterated limit is not the statement.

Formalization scope

The i.i.d. variables are the coordinates of $\mathbb R^n$ under the product measure $\mu^{\otimes n}$ ; all quantities depend only on the joint law, so the supremum over $\underline X$ is a supremum over laws $\mu$ with $\mu((-\infty, 0)) = 0$ . Indices are 0-based in Fin n with [NeZero n], the paper's index $n$ being ⊤. Expectations are lintegrals of ENNReal.ofReal in $[0, \infty]$ : no integrability is assumed and $EX_n^* = \infty$ is allowed. The sup over $T_n^*$ ranges over $c \ge 0$ and over both families $t(c)$ and $s(c)$ . Limits along the triangular array are indexed by $n = k + 1$ and taken in $\mathbb R$ after toReal; the early terms with $n \le b + c$ , where the clipped weights of threePoint do not form a probability measure, do not affect any limit.

The page's ratios are not written literally: in $[0, \infty]$ the quotients $0/0$ and $\infty/\infty$ take junk values, so a literal supremum of ratios would be decided by degenerate laws. The goal's third fact uses a strict inequality and requires an explicit probability law on $[0, \infty)$ , which rules out the Dirac mass at $0$ and sub-probability witnesses.

A complete development needs: the law of the first index of a product sample entering a set, expectations of finite-valued functions under Measure.pi, the limit $(1 - x/n)^n \to e^{-x}$ along a triangular array, and elementary bounds on the exponential. The first two are reusable for any threshold or secretary-type stopping problem on i.i.d. samples. Proofs of the milestones in any order are welcome, as is a proof of the upper bound that does not route through the median.

Selected references

E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12(4) (1984) 1213–1216. https://doi.org/10.1214/aop/1176993150
U. Krengel and L. Sucheston, On semiamarts, amarts, and processes with finite value, in Probability on Banach Spaces, Adv. Probab. Related Topics 4, Dekker, New York (1978) 197–266.
T. P. Hill and R. P. Kertz, Ratio comparisons of supremum and stop rule expectations, Z. Wahrsch. verw. Gebiete 56 (1981) 283–285. https://doi.org/10.1007/BF00536175
T. P. Hill and R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Ann. Probab. 10(2) (1982) 336–345. https://doi.org/10.1214/aop/1176993861

10 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

Zur allgemeinen Kurventheorie I: Menger's Theorem for Finite Graphs, If No Fewer Than n Points Separate Two Finite Sets P and Q, Then n Disjoint Paths Join P to QResearch Paper

Motivation

Menger's theorem is the oldest of the min–max theorems of combinatorial optimization. It says that the largest number of disjoint paths joining two sets of vertices of a finite graph equals the smallest number of vertices whose removal disconnects them. The max-flow/min-cut theorem of Ford and Fulkerson (1956), the Kőnig–Egerváry theorem on bipartite matchings (1931), Whitney's characterization of $k$ -connected graphs (1932) and the integrality of network-flow polytopes all belong to its family. In operations research it underlies network reliability (how many vertex failures a network survives) and disjoint routing.

Karl Menger proved it in 1927, in a paper on curves. In Zur allgemeinen Kurventheorie (Fund. Math. 10, pp. 96–115) the graph statement is a lemma, Satz δ (p. 101), on the way to characterizing the order of a point of a regular curve by the number of arcs ending there (the subject of mission II of this series).

Timeline.

1927. Menger states Satz β for compact regular one-dimensional spaces and proves its finite case, Satz δ, for finite unions of arcs, by induction on the number of arcs (Menger 1927).
1931. Kőnig observes that one step of the induction, called "offenbar" on p. 102, is in the bipartite case exactly his matching theorem, and supplies it (Kőnig 1931, see the references). Kőnig's 1936 book gives the first complete graph-theoretic proof.
1932. Whitney derives the two-vertex form for $k$ -connected graphs.
1956. Ford and Fulkerson's max-flow/min-cut theorem gives the flow-theoretic proof; Dantzig and Fulkerson connect it to LP duality.

Setting

Let $G$ be a finite simple graph on a vertex set $V$ , and let $P, Q \subseteq V$ be disjoint sets of vertices.

A set $S \subseteq V$ separates $P$ and $Q$ if every walk of $G$ from a vertex of $P$ to a vertex of $Q$ passes through a vertex of $S$ . The set $S$ may contain vertices of $P$ and of $Q$ ; in particular $S = P$ always separates.

$G$ is $n$ -point connected between $P$ and $Q$ ("n-punktig zusammenhängend", p. 100) if no set of fewer than $n$ vertices separates $P$ and $Q$ :

|S| \ge n \quad\text{for every } S \text{ separating } P \text{ and } Q .

A family of $n$ disjoint $P$ – $Q$ paths consists of paths $W_1, \dots, W_n$ of $G$ , each from a vertex of $P$ to a vertex of $Q$ , whose vertex sets are pairwise disjoint, end vertices included.

The degree (Grad) of $G$ is its number of edges. A part of $G$ is a spanning subgraph $H \le G$ ; it is proper if it lacks an edge of $G$ . $G$ is irreducibly $n$ -point connected between $P$ and $Q$ if it is $n$ -point connected and no proper part is. For a separating set $S$ , the side $K_1$ of $S$ towards $P$ is formed by the components of $G - S$ that meet $P - S$ , together with their edges to $S - P$ ; the side $K_2$ towards $Q$ is defined symmetrically.

In Lean these are Menger27.Graphs.Separates, NPointConnected, HasDisjointPaths, IrreduciblyNPointConnected and sidePart.

Formalization targets

Goal: Satz δ (p. 101)

G \text{ is } n\text{-point connected between disjoint } P \text{ and } Q \quad\Longrightarrow\quad G \text{ contains } n \text{ disjoint } P\text{–}Q \text{ paths.}

This is the direction Menger states; the converse (disjoint paths force every separator to be large) is immediate and is not part of the mission.

Milestones: the proof of Satz δ, in the paper's order (pp. 101–102)

A graph $n$ -point connected between $P$ and $Q$ has at least $n$ edges.
If it has exactly $n$ edges, it consists of $n$ disjoint $P$ – $Q$ paths.
It contains an irreducibly $n$ -point connected part $K'$ .
If $K'$ is irreducible and has more than $n$ edges, it has a vertex $s \notin P \cup Q$ on one of its edges.
Through such an $s$ passes a set $S$ of exactly $n$ vertices separating $P$ and $Q$ in $K'$ .
For an $n$ -vertex separating set $S$ with $|S \cap P| = p$ , the side $K_1$ is $(n-p)$ -point connected between $P - S$ and $S - P$ .
$n - p$ disjoint paths in $K_1$ and $n - q$ disjoint paths in $K_2$ (with $q = |S \cap Q|$ ) combine into $n$ disjoint $P$ – $Q$ paths in $G$ .

Significance

The result. Satz δ is the vertex form of Menger's theorem for two sets, from which the other standard forms follow: the two-vertex form, Whitney's theorem, the edge form (through line graphs), Kőnig's theorem (for bipartite $G$ with $P$ , $Q$ the two sides) and, through a standard reduction, integral max-flow/min-cut for unit capacities. Menger used it as the finite step of his theorem on $n$ -legs at points of regular curves.

Formalizing it. The theorem is proved, with many published proofs. Mathlib at the pinned revision has edge connectivity of simple graphs but no vertex separators between sets and no form of Menger's theorem; nothing on Prove2Me states it in set form. The mission produces a statement of Satz δ about Mathlib's SimpleGraph, together with the intermediate claims of Menger's own induction, so that the original argument, including the step Kőnig completed, can be checked. Related posed items on the platform are the two-vertex Whitney theorem Balinski61.Whitney.whitney_theorem (internally disjoint paths between two vertices) and Kőnig's theorem MatousekLP.Integrality.konig; neither is the set form stated here, and neither is proved yet.

Difficulty

The obvious argument, choosing disjoint paths one at a time, fails: a first path chosen badly can block every completion, so the paths must be chosen together. Menger's induction avoids this by passing to an irreducible part and cutting it at an $n$ -vertex separator, but it needs a vertex outside $P \cup Q$ to cut at (milestone 4). When every vertex of the irreducible part lies in $P \cup Q$ the part is bipartite between $P$ and $Q$ , and the claim is then Kőnig's matching theorem rather than an observation; this is the gap of 1927. The gluing step (milestone 7) is also more delicate than on the page: the paths of the two sides must meet the separator only at their ends, which depends on how the sides are cut out.

Formalization scope

Representation. Menger's gewöhnlich eindimensionaler Raum, a finite union of arcs meeting at most in end points, is read as a finite simple graph G : SimpleGraph V with [Fintype V]; $P$ and $Q$ are Finset V. Vertices are the points of $P \cup Q$ and the end and branch points (Menger's punktförmige Stücke); edges are the arcs between them, subdivided so that there are no loops or parallel edges. Subdivision changes neither separation nor the number of disjoint paths, and a separating point inside an arc can be moved to an end of the arc. Menger's degree (the number of arcs between consecutive punktförmige Stücke) becomes the number of edges, which a subdivision only increases; every milestone stays true.

Conventions and explicit readings of the paper's phrases.

Separation is phrased through walks: every walk from $P$ to $Q$ meets $S$ . Separators may meet $P$ and $Q$ .
Disjointness of $P$ and $Q$ ("fremden", p. 100) is a hypothesis of every theorem, not part of the definition. Paths are disjoint including their end points; with $P \cap Q = \emptyset$ every path has an edge.
"Teil" is a spanning subgraph H ≤ G; "echter Teil" is H < G.
"Offenbar enthält K′ ein punktförmiges Stück s …" (p. 102) is read as: a vertex $s \notin P \cup Q$ lying on an edge of $K'$ .
"In K′ − s sind n − 1 Punkte … so dass … S = {s, s₂, … sₙ}" is read as: a separating set of exactly $n$ vertices containing $s$ .
"Besteht aus n Bögen" (milestone 2) is read as: $n$ disjoint $P$ – $Q$ paths covering every edge.
The side $K_1$ is constructed from $G$ , $P$ and $S$ (sidePart G P S), not quantified over; it has no edges at the vertices of $S \cap P$ , matching Menger's $K_1 \subseteq K' - S$ considered between $P - S\cdot P$ and $S - S\cdot P$ .
The subtractions $n - p$ and $n - q$ are exact, since $|S| = n$ .
On p. 101 the induction hypothesis is printed as "Satz γ"; it is Satz δ.

Trivializations ruled out. Forcing separators to avoid $P \cup Q$ , counting internally disjoint or edge-disjoint paths, or allowing two paths to share an end vertex would each change the theorem; none is done. No hypothesis restricts $n$ , and $n = 0$ is the trivial case, not an excluded one.

Needed infrastructure. Walk surgery (prefixes up to the first visit of a set, concatenation, conversion of walks to paths), transfer of walks along SimpleGraph inclusions, and well-founded induction on the number of edges. Separators and disjoint path families between sets are reusable beyond this mission, for Whitney's theorem, Kőnig's theorem and flow integrality. Proofs by any method are welcome, including a proof of the goal through max-flow/min-cut or an independent argument (Göring's) bypassing the milestones.

Selected references

K. Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115
D. Kőnig, Gráfok és mátrixok, Matematikai és Fizikai Lapok 38 (1931), 116–119 (no DOI; English discussion in Diestel, Graph Theory, §2.1 and §3.3).
H. Whitney, Congruent graphs and the connectivity of graphs, American Journal of Mathematics 54 (1932), 150–168. https://doi.org/10.2307/2371086
L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
F. Göring, Short proof of Menger's theorem, Discrete Mathematics 219 (2000), 295–296. https://doi.org/10.1016/S0012-365X(00)00088-1
R. Diestel, Graph Theory, 5th ed., Springer, 2017, §3.3. https://doi.org/10.1007/978-3-662-53622-3

10 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

Integer Programming Formulation of Traveling Salesman Problems: The Miller–Tucker–Zemlin Constraints Exactly Describe the Itineraries with at Most p Cities per TourResearch Paper

Why this formulation matters

The traveling salesman problem asks for a shortest closed route through a set of cities. Writing it as an integer program requires linear constraints whose integer solutions are exactly the routes. The assignment constraints (each city entered once and left once) are not enough: their integer solutions include collections of disjoint cycles, called subtours, that never pass through the starting city. Some extra family of constraints must rule these out.

In 1960 C. E. Miller, A. W. Tucker and R. A. Zemlin gave such a family using one auxiliary real variable per city (J. ACM 7(4), 326–329). Their MTZ constraints have polynomially many rows, $n^2-n$ for $n$ cities, whereas the subtour elimination constraints of Dantzig, Fulkerson and Johnson (1954) (Oper. Res. 2(4)) have one row per subset of cities. They also handle a generalization: a salesman who returns to base several times, visiting at most $p$ cities per trip. This is the basic form of a capacitated vehicle routing problem. MTZ-type constraints remain standard in vehicle routing models and in textbook formulations of the TSP. Their linear relaxations are known to be weaker than those of the subtour elimination formulation (Padberg and Sung, 1991).

The paper attributes the model to Tucker and reports five machine experiments with Gomory's all-integer algorithm. The computational part is outside this mission.

Setting

There are $n$ cities $1,\dots,n$ and a base city $0$ . A tour is a succession of visits to cities without stopping at city $0$ . In problem (1) the salesman leaves $0$ , visits each of the $n$ cities exactly once and returns to $0$ , possibly several times, with at most $p$ cities per tour. Formally, an itinerary is a list $I=(T_1,\dots,T_t)$ of tours. Each tour is a nonempty list of cities other than $0$ of length at most $p$ , and each city $1,\dots,n$ occurs exactly once in the concatenation of the tours. The number $t$ of tours is the number of returns to $0$ . Tour $(c_1,\dots,c_k)$ travels the arcs $(0,c_1),(c_1,c_2),\dots,(c_k,0)$ . $a_{ij}(I)$ denotes the number of times $I$ travels the arc $(i,j)$ . For real distances $d_{ij}$ , the length of $I$ is the sum of $d_{ij}$ over the arcs it travels.

Problem (2) has non-negative integer variables $x_{ij}$ ( $0\le i\ne j\le n$ ) and real variables $u_1,\dots,u_n$ :

\min \sum\sum_{0\le i\ne j\le n} d_{ij}x_{ij}\quad\text{s.t.}\quad \sum_{\substack{i=0\\ i\ne j}}^{n} x_{ij}=1\ (j\ge1),\quad \sum_{\substack{j=0\\ j\ne i}}^{n} x_{ij}=1\ (i\ge1),\quad u_i-u_j+p\,x_{ij}\le p-1\ (1\le i\ne j\le n).

When the number of tours $t$ is fixed, the relation $\sum_{i=1}^n x_{i0}=t$ is added. With $t=1$ and $p\ge n$ , (1) is the standard traveling salesman problem.

Formalization targets

Goal: the equivalence of (1) and (2)

For every $n\ge0$ and every $p\ge1$ :

\{\,x : \exists u,\ (x,u)\ \text{feasible for (2)}\,\} \;=\; \{\,a(I) : I \text{ a legitimate itinerary of (1)}\,\},

with $\sum_{i=1}^n x_{i0}$ equal to the number of tours $t(I)$ , and with the $u_i$ in the converse taken to be non-negative integers. In addition, $\sum\sum_{i\ne j} d_{ij}\,a_{ij}(I)$ equals the length of $I$ for all real $d$ . The paper says that (2) "will be shown to be equivalent to (1)". Its "burden of proof" is that the two feasible sets correspond and the two objectives agree, and the goal states exactly that.

Milestones, in the order of the paper's proof

The constraints of (2) force $x_{ij}\in\{0,1\}$ (p. 327).
Along a path $r_0,\dots,r_m$ of non-base cities with all $x_{r_kr_{k+1}}=1$ , $u_{r_0}-u_{r_m}\le-m$ (p. 328).
A feasible $x$ has no cycle that avoids city $0$ , so all tours include city 0 (pp. 327–328).
For $p\ge1$ , no tour of a feasible $x$ visits more than $p$ cities (p. 328).
The converse: $u_i=$ the position of city $i$ in its tour makes $(a(I),u)$ feasible, with $1\le u_i\le p$ (p. 328).
Under $x=a(I)$ the objective of (2) is the distance travelled in (1) (p. 327).
An itinerary with $t$ tours of at most $p$ cities requires $tp\ge n$ (p. 326).

Significance

The result. The theorem justifies using (2) in place of (1). Because the feasible sets match and the objectives agree, an optimal solution of (2) is an optimal itinerary of (1), and the same holds with the number of tours fixed. It also shows that a compact, polynomial-size family of linear inequalities in auxiliary potentials excludes every subtour. The same idea, with the $u_i$ read as loads or arrival times, underlies the standard capacity and time-window constraints of vehicle routing.

Formalizing it. The result is classical and its proof is short, but the paper argues informally. It follows successor chains, treats "a tour" without defining an itinerary, and leaves several steps implicit, including the hypothesis $p\ge1$ and the distinctness of $r_{p+1}$ and $r_1$ . No machine-checked statement of the MTZ equivalence is recorded on the platform. The remaining work is the whole formal proof: the combinatorics that turns a 0/1 matrix with unit row and column sums and no subtours into a list of tours, the converse labelling, and the bookkeeping identity between the two objectives.

Difficulty

The inequalities themselves are elementary. Each milestone about (2) is a short computation with the potentials $u_i$ . The work is in the passage from a feasible matrix $x$ to an itinerary. The successor walk from city $0$ must be shown to terminate at $0$ and to cover every arc of $x$ . The resulting tours must be listed so that their arc counts reproduce $x$ exactly, including the number of arcs leaving $0$ . That number is not constrained directly in (2). It equals $\sum_{i}x_{i0}$ only through a counting argument on the row and column sums. A proof that only shows some itinerary exists does not establish the correspondence the paper claims.

Formalization scope

Cities are Fin (n + 1) with 0 the base city, which is the paper's indexing. The commitments, each also stated in the items' Formalization Notes, are:

An itinerary is a List of tours, each tour a List of cities. The paper's "legitimate itinerary" is read as: every tour nonempty, free of 0, of length at most $p$ ; the concatenation duplicate-free; every city $1,\dots,n$ present.
"A feasible solution to (2) has $x_{ij}$ which do define a legitimate itinerary" is read as $x=a(I)$ , the arc counts of $I$ , together with $\sum_{i=1}^n x_{i0}=t(I)$ ("The number of returns to city 0 is given by $\sum x_{i0}$ "). Arc counts are counts, so $x_{ij}\in\{0,1\}$ is a theorem, not an encoding choice.
"Together with appropriate $u_i$ " is made explicit as the existence of natural-number $u_i$ , following the paper's remark that the $u_i$ may be taken non-negative integers. The labelling $u_i=j$ is a definition.
Problem (2) has no variables $x_{ii}$ . The matrix $x$ is indexed by all pairs and the clause $x_{ii}=0$ encodes their absence. $u_0$ exists in the encoding but appears in no constraint.
$x_{ij}\in\mathbb N$ ("non-negative integers"), $u_i\in\mathbb R$ ("arbitrary real numbers"), and $p-1$ and $p\,x_{ij}$ are computed in $\mathbb R$ .
Added hypothesis $p\ge1$ in the goal and in milestone 4. The paper does not state it, and the claim is false without it: for $n=1$ , $p=0$ , $x_{01}=x_{10}=1$ is feasible for (2) but no itinerary exists.
The distances $d_{ij}$ are arbitrary reals, with no sign, symmetry or triangle condition, as on the page.
Milestone 2 states the exact summed bound $-m$ . The page prints the weaker $j+1-k$ .
Milestone 3 excludes every cycle of $x$ avoiding $0$ . The page argues for the cycle met while following successors from $0$ , by an argument that applies to any such cycle.

Not formalized: the constraint and variable counts and the elimination of $x_{i0},x_{0j}$ "to produce an equivalent problem with $n^2+n$ inequalities and $n^2$ variables" (p. 328), which the paper does not make precise, and the machine experiments (pp. 328–329).

Trivializing readings are ruled out. The goal identifies $x$ with the arc counts of an itinerary, not merely the existence of some itinerary. The hypotheses are satisfiable: for $n=3$ , $p=2$ , the itinerary $[[1,2],[3]]$ with $u=(1,2,1)$ is feasible for (2), while the subtour $x_{01}=x_{10}=x_{23}=x_{32}=1$ is not, for any $u$ . Contributions welcome: proofs of the milestones, a reusable library of "functional digraph with unit in- and out-degree" decompositions, and the optimization corollary (equal optimal values of (1) and (2)).

Selected references

C. E. Miller, A. W. Tucker, R. A. Zemlin, Integer Programming Formulation of Traveling Salesman Problems, Journal of the ACM 7(4), 326–329, 1960. https://doi.org/10.1145/321043.321046
G. Dantzig, R. Fulkerson, S. Johnson, Solution of a Large-Scale Traveling-Salesman Problem, Operations Research 2(4), 393–410, 1954. https://doi.org/10.1287/opre.2.4.393
M. Padberg, T.-Y. Sung, An analytical comparison of different formulations of the travelling salesman problem, Mathematical Programming 52, 315–357, 1991. https://doi.org/10.1007/BF01582894
R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bulletin of the AMS 64(5), 275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4

9 thms2 active usersReviewed

Algorithmic Game Theory Analysis Probability·Captain: mikedeng1

Values of Large Games II: Oceanic Games 1: Closed-Form Values of Interior Oceanic GamesResearch Paper

Motivation

Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.

Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).

Setting

There are $m$ major players $M = \{1, \dots, m\}$ with weights $w_1, \dots, w_m \ge 0$ , and $w(S) = \sum_{j \in S} w_j$ . The ocean is the interval $I = [0,1]$ with Lebesgue measure, carrying total weight $\alpha > 0$ . In the oceanic game $[c; w_1, \dots, w_m; \alpha]$ with quota $c$ , a coalition wins when the weight of its major players plus $\alpha$ times its share of the ocean is at least $c$ .

The random order is modelled by a uniform random point $x = (x_1, \dots, x_m)$ of the cube $I^m$ : major player $j$ is inserted into the ocean at position $x_j$ , and $P(t) = \{ j : x_j < t \}$ is the set of major players placed before position $t$ . Player $i$ is pivotal when

w(P(x_i)) + \alpha x_i \le c \le w(P(x_i)) + w_i + \alpha x_i, \qquad (2.4)

and the value $\varphi_i$ of player $i$ is the probability of (2.4), i.e. the volume of the set $A_i \subseteq I^m$ where it holds. The combined value of the ocean is $\Phi = 1 - \sum_{i} \varphi_i$ (2.5).

With the quota $y$ as a variable, $\Gamma(y) = [y; w_1, \dots, w_m; \alpha]$ has values $\varphi_i(y)$ , $\Phi(y)$ , and the pivot location $F(y) = \inf\{t \ge 0 : w(P(t)) + \alpha t \ge y\}$ is a random, nondecreasing, piecewise linear function of $y$ with expectation $E\{F(y)\}$ . Adding a major player $m+1$ of weight $w_{m+1}$ gives the game $\Gamma^+$ .

The game is interior when

w(M) \le c \le \alpha,

that is, the ocean alone wins and the major players together lose. With $\bar w_j = \alpha - w_j$ , define $\pi(S) = \prod_{j \in S} \tfrac{w_j}{\alpha} \prod_{j \in M - S} \tfrac{\bar w_j}{\alpha}$ for $S \subseteq M$ , the analogous product $\pi_i(S)$ over $M - \{i\}$ for $S \subseteq M - \{i\}$ , and the integers $a_0 = 1$ , $a_n = 1 - n a_{n-1}$ , i.e. $1, 0, 1, -2, 9, -44, \dots$

Formalization targets

Goal: Theorem 6 (p. 20)

In an interior game, with $s = |S|$ ,

\varphi_i = \frac{w_i}{\alpha} \sum_{S \subseteq M - \{i\}} a_s \, \pi_i(S), \qquad \Phi = \sum_{S \subseteq M} a_s \, \pi(S).

Both identities are part of the goal. The values do not depend on $c$ within the interior range.

Milestones

§2, p. 5: the pivot sets $A_1, \dots, A_m$ overlap only in measure zero.
(4.3): $\varphi_i(y) = \operatorname{Prob}\{F(y) = x_i\}$ for $0 \le y \le w(M) + \alpha$ .
(4.4)–(4.5): for $0 < y < w(M) + \alpha$ , $F$ is differentiable at $y$ almost surely, $\sum_i \varphi_i(y) = \operatorname{Prob}\{F'(y) = 0\}$ and $\Phi(y) = \operatorname{Prob}\{F'(y) = 1/\alpha\}$ .
Theorem 2, (4.7): $\Phi(y) = \alpha \, \frac{d}{dy} E\{F(y)\}$ .
Lemma, (4.12)–(4.13): $\varphi^+_{m+1}(z) = \frac{1}{\alpha} \int_{t_1}^{t_2} \Phi(y)\, dy$ with $t_1 = \max(z - w_{m+1}, 0)$ , $t_2 = \min(z, w(M) + \alpha)$ .
Theorem 5, (5.4): if $[c; w_1, \dots, w_m; \alpha]$ and $[d; w_1, \dots, w_{m+1}; \alpha]$ are both interior, $\varphi^+_{m+1} = \frac{1}{\alpha} \Phi w_{m+1}$ .
Proof of Theorem 6, p. 21: the right-hand sides above add up to 1, an identity valid for all real $w_j$ and $\alpha \ne 0$ .

Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ( $|a_n|$ is the nearest integer to $n!/e$ and counts derangements).

Significance

Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios $w_j/\alpha$ . Table 1 of the memorandum lists the cases $m \le 3$ , and the theorem gives every $m$ . Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.

The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.

Difficulty

The values are volumes of regions of $I^m$ cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into $m!$ order cells, with the quota $c$ entering each. The paper's route avoids this by passing through the random function $F$ , Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in $y$ , with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of $[0, w(M) + \alpha]$ . Theorem 6 is then an induction on $m$ that uses Theorem 5 for every player in turn, so it also needs the invariance of $\varphi_i$ under a relabelling of the major players.

Formalization scope

Major players are Fin m ( $m = 0$ is allowed; then $\Phi = 1$ ). The probability of an event is the Lebesgue volume of its intersection with $[0,1]^m$ ; no probability space is built.
$P(t)$ uses the strict inequality $x_j < t$ , as printed.
$\varphi_i$ is defined as the volume of the pivot set (2.4), for every real quota. $\Phi$ is defined by (2.5), as the paper allows ("We might equally well take (2.5) as the definition of $\Phi$ "). Neither is defined through the formulas of Theorem 6 or through $F$ ; defining them that way would make the goal an unfolding, and is ruled out.
The paper writes (4.2) as a minimum $F(y) = \min\{x \mid w(P(x)) + \alpha x \ge y\}$ , which need not be attained; $F$ is the infimum over $t \ge 0$ , the value shown in its Fig. 3.
The standing assumptions $w_j \ge 0$ and $\alpha > 0$ (§2) are explicit hypotheses. The p. 5 footnote's $0 \le c \le w(M)+\alpha$ applies to the pivot-set milestone. Other quota ranges are explicit: $0 \le y \le w(M) + \alpha$ for (4.3) and Theorem 2 (one-sided derivatives at the ends), the open interval for (4.4)–(4.5) (two-sided derivatives, stated with HasDerivAt), and $0 \le z \le w(M) + w_{m+1} + \alpha$ for the Lemma, as on p. 14.
The added player is appended with Fin.snoc as index Fin.last m.
Corollary (5.5) assumes $w_i > 0$ , since it divides by $w_i$ . Theorem 4, stated in the paper "in the general oceanic game", is false at quota $0$ and when the limit game has no winning coalition; it is stated for $0 < c \le w(M - \{i\}) + \alpha$ .
The identity of milestone 7 is pure algebra and is stated for all real weights and $\alpha \ne 0$ .

A complete development needs: measurability of the pivot sets and of $F$ in $x$ , the structure of $F$ as a piecewise linear function of $y$ , differentiation of $E\{F\}$ , and invariance of the values under permutations of the major players. The pivot-set and $F$ infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.

Selected references

J. W. Milnor and L. S. Shapley, Values of Large Games, II: Oceanic Games, The RAND Corporation, Research Memorandum RM-2649, February 1961. https://www.rand.org/pubs/research_memoranda/RM2649.html
J. W. Milnor and L. S. Shapley, Values of Large Games II: Oceanic Games, Mathematics of Operations Research 3(4):290–307, 1978. https://doi.org/10.1287/moor.3.4.290
L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, 307–317. https://doi.org/10.1515/9781400881970-018
L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, The RAND Corporation, Research Memorandum RM-2648, November 1960.
R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080

9 thms2 active usersReviewed

Operations Research

Missions

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 1: The Threshold Rule on Efficient Periods Picks an Optimal Next Production PeriodResearch Paper

Motivation

Setting

Formalization targets

Efficient candidates

Threshold rule and backward value

Significance

Difficulty

Formalization scope

Selected references

Multi-armed Bandits and the Gittins Index: With Per-Project Horizons the Maximal M-Process Reward Is K − ∫_M^K ∏ᵢ ∂φᵢ/∂m dm and the Gittins Index Rule Attains ItResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 147)

Milestones (the steps of the proof)

Further item

Significance

Difficulty

Formalization scope

Selected references

An Introduction to Timetabling 3: Course Scheduling with Unavailabilities and Preassignments in p Periods Is Equivalent to p-Coloring the Nodes of a GraphResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Negative Dynamic Programming IV: Switching at Each Stage to the Policy with the Better Continuation Return Does at Least as Well as Both PoliciesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 9.3 (negative case)

Milestones (proof of Theorem 9.3, p. 888)

Further results (not milestones)

Significance

Difficulty

Formalization scope

Selected references

Negative Dynamic Programming I: With Non-Positive Rewards, If an Optimal Policy Exists Then an Optimal Stationary Policy ExistsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

Milestones

Significance

Difficulty

Formalization scope

Selected references

Vertical Integration and Antitrust Policy: Integrating Successive Monopolies Lowers the Final Price and Raises Output, Joint Profit and Consumer SurplusResearch Paper

Motivation

Setting

Formalization targets

Goal: vertical integration benefits producer and consumer

Milestones

Significance

Difficulty

Formalization scope

Selected references

On Cores and Indivisibility 1: The Housing Market's Game Without Side Payments Is BalancedResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Some Theoretical Aspects of Road Traffic Research II: Equal Journey Times on Alternative Routes — Exactly the Routes with bᵢ < t Are Used, qᵢ = pᵢ(1 − bᵢ/t)Research Paper

Motivation

Setting

Formalization targets

Goal: the closed form (23)–(24)

Companion: the equal-times split exists and is unique

Significance

Difficulty