Operations Research

Completed

Linear Optimization Optimization·Captain: mikedeng1

Understanding and Using Linear Programming II: Optimal Basic Feasible Solutions and Vertices in Equational FormTextbook

Motivation

Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.

This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.

Setting

A linear program in equational form is

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

where $A$ is a real $m\times n$ matrix, $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ , and $x\ge 0$ means every coordinate of $x$ is nonnegative. A feasible solution is an $x\in\mathbb{R}^n$ satisfying both constraints; the set of them is $P$ . An optimal solution is a feasible $x$ with $c^{T}y\le c^{T}x$ for every feasible $y$ . The objective is bounded from above if some real $M$ satisfies $c^{T}x\le M$ for all feasible $x$ .

Throughout Section 4.2 the book assumes that $A$ has $n\ge m$ columns and rank $m$ (its rows are linearly independent). For $S\subseteq\{1,\dots,n\}$ , $A_S$ denotes the matrix formed by the columns of $A$ with indices in $S$ . A basis is an $m$ -element set $B$ for which $A_B$ is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible $x$ for which some basis $B$ has $x_j=0$ for every $j\notin B$ .

A point $v$ is a vertex of $P$ if $v\in P$ and some nonzero $c\in\mathbb{R}^n$ satisfies $c^{T}v>c^{T}y$ for every $y\in P\setminus\{v\}$ : $v$ is the unique maximizer over $P$ of a nonzero linear function.

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

For $A$ of rank $m$ with $n\ge m$ ,

\Bigl(P\neq\emptyset\ \wedge\ \exists M\ \forall x\in P,\ c^{T}x\le M\Bigr)\ \Longrightarrow\ \exists\,x^{*}\ \text{optimal},

\exists\,x^{*}\ \text{optimal}\ \Longrightarrow\ \exists\,\tilde x\ \text{optimal and basic feasible}.

Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.

Milestones

Lemma 4.2.1 (p. 45): a feasible $x$ is basic if and only if the columns of $A_K$ are linearly independent, where $K=\{j : x_j>0\}$ .
Proposition 4.2.2 (p. 45): for a basis $B$ there is at most one feasible solution vanishing outside $B$ .
The statement proved inside the proof of Theorem 4.2.3 (p. 47): if the objective is bounded above, every feasible $x_0$ is dominated by a basic feasible $\tilde x$ , $c^{T}\tilde x\ge c^{T}x_0$ .
Theorem 4.4.1 (p. 54): a point of $P$ is a vertex of $P$ if and only if it is a basic feasible solution.

Significance

Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most $\binom{n}{m}$ sets $B$ , solve $A_Bx_B=b$ , and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.

All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra $\{x : a_i^{T}x\ge b_i\}$ , extreme points, basic solutions as $n$ active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.

Difficulty

The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.

For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by $K$ must be completed to an $m$ -element basis, which requires the rank- $m$ assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.

Formalization scope

All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:

vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ are 0, …, n-1;
$Ax=b$ is A *ᵥ x = b, $x\ge 0$ is 0 ≤ x (pointwise), $c^{T}x$ is c ⬝ᵥ x;
a subset $B$ of indices is a Finset (Fin n); " $A_B$ nonsingular" is linear independence over $\mathbb{R}$ of the family of columns of $A$ indexed by the elements of $B$ , together with B.card = m;
the standing assumption of §4.2 is the pair of hypotheses m ≤ n and A.rank = m on every theorem;
"optimal" and "bounded from above" are stated against every feasible point. No real supremum over the feasible set appears anywhere, so an empty or unbounded feasible set cannot make a statement hold through a default value;
"vertex" is the book's unique-maximizer definition of p. 53, not Mathlib's Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;
Theorem 4.4.1 carries the extra hypothesis $n\ge 1$ : for $n=0$ there is no nonzero vector in $\mathbb{R}^0$ , the single feasible point $0$ is basic but not a vertex, and the book's equivalence fails.

A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.

Reusable infrastructure: the column-restriction and basis vocabulary, the support set $K$ , and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Universitext, Springer, 2007, Chapter 4, pp. 41–56. https://doi.org/10.1007/978-3-540-30717-4
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 2.
G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1

6 thms2 active usersReviewed

Markov Chain Probability Stochastic Systems·Captain: mikedeng1

Fundamentals of Queueing Theory I: Foster's Criterion for Positive RecurrenceTextbook

Motivation

Almost every model in queueing theory is analysed through a Markov chain. The number of customers in an M/M/c queue is a continuous-time birth–death chain; the number left behind by departing customers of an M/G/1 queue is a discrete-parameter chain on $\{0,1,2,\dots\}$ (the imbedded Markov chain); networks of queues are chains on vectors of queue lengths. Before any steady-state formula (Erlang's formulas, the Pollaczek–Khintchine formula, product forms) can be used, one has to know that the chain has a steady state at all: that it is positive recurrent, so that a stationary distribution exists and equals the limiting distribution.

Chapter 1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), collects the two ingredients the rest of the book stands on: the Poisson process with its exponential interarrival times (§§1.7–1.8), and the classification theory of discrete-parameter Markov chains (§1.9), ending with Foster's criterion (Theorem 1.2), a sufficient condition for positive recurrence in terms of a drift inequality. The criterion goes back to F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953) (DOI 10.1214/aoms/1177728976), and is the ancestor of the Foster–Lyapunov method used for stability of queueing networks and stochastic systems.

This mission is the first of a series formalizing the book chapter by chapter.

Setting

A homogeneous discrete-parameter Markov chain on $\{0,1,2,\dots\}$ is given by a transition matrix $P=\{p_{ij}\}$ with $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every $i$ . The $m$ -step transition probabilities $p_{ij}^{(m)}$ are the entries of $P^m$ .

The first-passage probability $f_{ij}^{(n)}$ is the probability that the chain started in $i$ enters $j$ for the first time at step $n\ge1$ ; for $i=j$ it is the probability of first return at step $n$ . The return probability is $f_{jj}=\sum_{n\ge1}f_{jj}^{(n)}$ and the mean recurrence time is $m_{jj}=\sum_{n\ge1}n f_{jj}^{(n)}\in[0,\infty]$ . A state is positive recurrent if $f_{jj}=1$ and $m_{jj}<\infty$ ; the chain is positive recurrent if every state is.

The chain is irreducible if for every pair of states $(i,j)$ some $p_{ij}^{(n)}$ is positive, and aperiodic if for every state $k$ the greatest common divisor of $\{n\ge1:p_{kk}^{(n)}>0\}$ is $1$ . A stationary distribution is a probability vector $\pi$ with $\pi=\pi P$ , i.e. $\pi_j=\sum_i\pi_i p_{ij}$ for every $j$ .

For the Poisson part, $T_0,T_1,\dots$ are independent interarrival times, each exponentially distributed with rate $\lambda>0$ ; the arrival epochs are $S_n=T_0+\dots+T_{n-1}$ , and $N(t)=\#\{n\ge1:S_n\le t\}$ counts the arrivals in $[0,t]$ .

Formalization targets

Goal: Theorem 1.2 (Foster's criterion)

An irreducible, aperiodic chain is positive recurrent if there exist $x_j\ge0$ with

\sum_{j=0}^\infty p_{ij}x_j\le x_i-1\quad(i\ne0),\qquad\sum_{j=0}^\infty p_{0j}x_j<\infty .

Milestones: the Markov chain theorems

Theorem 1.1(a). In an irreducible, positive recurrent chain, $\pi_j=1/m_{jj}$ is a stationary distribution, and it is the only one.
Theorem 1.1(c). If moreover the chain is aperiodic and all moments of $\pi$ are finite, then $\lim_{m\to\infty}p_{ij}^{(m)}=\pi_j$ for all $i,j$ .

Milestones: the Poisson process and the exponential distribution

Eqs. (1.11)–(1.14). The unique solution of $p_0'=-\lambda p_0$ , $p_n'=-\lambda p_n+\lambda p_{n-1}$ with $p_0(0)=1$ , $p_n(0)=0$ is $p_n(t)=(\lambda t)^n e^{-\lambda t}/n!$ .
Eq. (1.15). With exponential interarrival times,

\Pr\{N(t)\le n\}=\int_t^\infty\frac{\lambda(\lambda x)^n}{n!}e^{-\lambda x}dx=\sum_{i=0}^n\frac{(\lambda t)^ie^{-\lambda t}}{i!}.

Eq. (1.16). Given $N(L)=k$ , the arrival epochs have density $k!/L^k$ on $\{0<t_1<\dots<t_k<L\}$ .
Eq. (1.17) and its converse (p.21). The exponential law satisfies $\Pr\{T\le t_1\mid T\ge t_0\}=\Pr\{0\le T\le t_1-t_0\}$ , and it is the only continuous distribution on $[0,\infty)$ that does.
Nonhomogeneous Poisson law (p.22). With a continuous rate $\lambda(t)$ the forward equations have the unique solution $p_n(t)=e^{-m(t)}m(t)^n/n!$ , $m(t)=\int_0^t\lambda(s)\,ds$ .

Significance

Foster's criterion reduces positive recurrence, a statement about return times, to exhibiting one test function $x$ with negative drift outside a single state. In the book it is the tool that establishes the existence of steady state for imbedded chains of the M/G/1 and G/M/1 queues (Chapter 5); its generalizations are the standard stability proofs for queueing networks. Theorem 1.1 then supplies what positive recurrence buys: the stationary distribution exists, is unique, equals $1/m_{jj}$ , and is the limit of the transition probabilities. The Poisson results justify the "Markovian" arrivals and services of Chapters 2–4.

All of these results are classical and proved in the literature; the book states Theorems 1.1 and 1.2 without proof. The Prove2Me platform already holds machine-checked versions of related Markov chain theorems in other missions (Levin–Peres–Wilmer's and Durrett's countable-chain convergence theorems), stated with different definitions and hypotheses. What this mission adds is a formal development in the book's own terms — first-passage probabilities $f_{jj}^{(n)}$ , mean recurrence times $m_{jj}$ , gcd periodicity — on which the later missions of the series (imbedded chains, birth–death processes) can build, together with a formal proof of Foster's criterion, which is not on the platform.

Difficulty

For Foster's criterion the natural first step, taking expectations of the drift inequality along the chain, only shows that the expected value of $x$ decreases while the chain stays away from $0$ . Turning that into a bound on the expected return time to $0$ requires an optional-stopping or telescoping argument over a random time, with the value $x$ possibly unbounded, and a separate argument that positive recurrence of state $0$ propagates to all states of an irreducible chain. The book's hypotheses include aperiodicity, which the argument does not use.

For Theorem 1.1, identifying the stationary distribution with $1/m_{jj}$ requires relating the matrix powers $P^n$ to the first-passage probabilities (a renewal decomposition), and uniqueness over countably many states needs care with infinite sums. For the Poisson results, the difficulty is measure-theoretic: the distribution of the sum of $n+1$ exponential variables, and conditioning on the event $\{N(L)=k\}$ for the order-statistics property.

Formalization scope

States are natural numbers; the transition matrix is a real function $p:\mathbb N\times\mathbb N\to\mathbb R$ with nonnegative entries and rows summing to one (as a convergent series). The return probability and the mean recurrence time are valued in $[0,\infty]$ , so null recurrence ( $m_{jj}=\infty$ ) is representable. Irreducibility is the per-pair notion. Stationary equations are stated componentwise with convergent series.

In Foster's criterion the series $\sum_j p_{ij}x_j$ are required to converge for every $i$ , which is the book's condition $\sum_j p_{0j}x_j<\infty$ together with the finiteness implicit in the inequalities for $i\ne0$ ; $x$ is real-valued and nonnegative. Dropping the convergence requirement would let a divergent row series (whose Lean sum is $0$ ) satisfy the inequality vacuously; allowing $x_j=\infty$ would make the hypothesis trivially satisfiable. Neither is permitted.

The closed forms stated explicitly are: $\pi_j=1/m_{jj}$ (Theorem 1.1(a), with both existence and uniqueness), the Poisson probabilities $(\lambda t)^ne^{-\lambda t}/n!$ (1.14), the Erlang tail integral and the Poisson CDF (1.15), the density $k!/L^k$ (1.16), and $e^{-m(t)}m(t)^n/n!$ for the nonhomogeneous law. Equations (1.14) and the nonhomogeneous law are stated as "solves the equations with the initial conditions if and only if equals the closed form", so both existence and uniqueness are asserted.

The Poisson results use random variables on a probability space, with Mathlib's expMeasure for the exponential law and cond for conditional probability. The derivation of the forward equations from the $o(\Delta t)$ axioms of §1.7 is not formalized; the Poisson law is reached from the equations and, separately, from exponential interarrival times.

Not formalized: Theorem 1.1(b) and the word "ergodic" in 1.1(c), which rest on the book's informal notion of ergodicity; Theorem 1.3, whose phrase "for Theorem 1.1 to be valid" for a continuous-time chain is not pinned down.

The Markov chain definitions are reusable by every later mission that studies an imbedded chain. Contributions welcome: proofs of the milestones, and supporting lemmas (Chapman–Kolmogorov, renewal decomposition of $p_{jj}^{(n)}$ , class properties of recurrence).

Selected references

D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
F. G. Foster, On the stochastic matrices associated with certain queuing processes, Annals of Mathematical Statistics 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976

11 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Optimization+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design XI: Optimal Sequential Screening by Option ContractsTextbook

Motivation

Many sales are contracted before the buyer knows what the good is worth to her. An airline sells a ticket months before the trip, a hotel sells a refundable or non-refundable room before the traveller's plans are settled, and a supplier signs a capacity contract before demand is realised. At the time of contracting the buyer holds some private information about her future valuation (how likely she is to travel), and after contracting she learns more (whether she actually travels). Sequential screening is the mechanism design problem of a seller facing such a buyer.

The chapter formalized here, Daniel Krähmer and Roland Strausz's Dynamic Mechanism Design (Chapter 11 of Börgers' textbook), develops the problem along two lines. The first is dynamic private information: one sale, two rounds of private information. The second is dynamic allocations: repeated sales, one fixed valuation.

Timeline:

Baron and Besanko (1984) show that dynamic allocations with static information produce no real dynamics in the optimal mechanism.
Courty and Li (2000, Review of Economic Studies) solve the sequential screening problem and show that the optimal mechanism is a menu of option contracts.
Esö and Szentes (2007) decompose the buyer's information into initial and additional information, show that the seller can extract the additional information at no cost, and derive the optimal multi-buyer mechanism, the handicap auction.
Krähmer and Strausz (2011, 2014), cited in the chapter's problems (notes 2–3, p.237), show that the conclusions depend on the model's assumptions; with discrete ex ante types the privacy of the additional information can cost the seller (Problem 11.5(c), p.233).

Setting

A seller sells one indivisible good. Before contracting, the buyer privately observes her ex ante type $\tau\in[\underline\tau,\bar\tau]$ , with distribution function $G$ and density $g>0$ . After accepting the mechanism she privately observes her ex post type $\theta\in[\underline\theta,\bar\theta]$ , $0\le\underline\theta<\bar\theta$ , which is her valuation. Conditionally on $\tau$ it has distribution function $F(\theta\mid\tau)$ and density $f(\theta\mid\tau)>0$ . Both $F$ and $f$ are continuously differentiable in $\tau$ , $|\partial F/\partial\tau|<K$ , and higher $\tau$ is good news in the sense of first-order stochastic dominance: $\partial F(\theta\mid\tau)/\partial\tau<0$ for $\theta\in(\underline\theta,\bar\theta)$ .

A direct mechanism is a pair $q(\tau,\theta)\in[0,1]$ , $t(\tau,\theta)\in\mathbb R$ . The buyer first reports $\tau$ , then $\theta$ . Write $u(\tau,\theta)=\theta q(\tau,\theta)-t(\tau,\theta)$ , $\hat U(\tau'\mid\tau)=\int u(\tau',\hat\theta)f(\hat\theta\mid\tau)\,d\hat\theta$ and $U(\tau)=\hat U(\tau\mid\tau)$ . The mechanism is incentive-compatible if truth about $\theta$ is optimal after every report of $\tau$ , and truth about $\tau$ is optimal against every subsequent reporting function $\theta_r$ . It is individually rational if $U(\tau)\ge0$ for all $\tau$ . The seller maximizes expected revenue $\int\!\!\int t\,f\,g$ . The virtual valuation is

\psi(\tau,\theta)=\theta+\frac{1-G(\tau)}{g(\tau)}\,\frac{\partial F(\theta\mid\tau)/\partial\tau}{f(\theta\mid\tau)} ,

and Assumption 11.1 requires $\psi$ to be increasing in $\tau$ and $\theta$ . The exercise price is $p(\tau)=\min\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$ .

Formalization targets

Goal: Proposition 11.8 (optimal sequential screening)

Under Assumption 11.1 the optimal mechanism is

q^*(\tau,\theta)=\mathbf 1[\theta\ge p(\tau)],\qquad t^*(\tau,\theta)=t_0(\tau)+p(\tau)\,\mathbf 1[\theta\ge p(\tau)],

where $t_0$ is the expression of Proposition 11.5 for $q^*$ , and the lowest type pays

t(\underline\tau,\underline\theta)=\int_{p(\underline\tau)}^{\bar\theta}\hat\theta f(\hat\theta\mid\underline\tau)\,d\hat\theta-p(\underline\tau)\bigl[1-F(p(\underline\tau)\mid\underline\tau)\bigr]+\underline\theta q^*(\underline\tau,\underline\theta).

The goal asserts that this mechanism is incentive-compatible, individually rational and optimal. It also characterizes all optimal mechanisms: an incentive-compatible, individually rational mechanism is optimal if and only if $q=q^*$ almost everywhere off $\{\psi=0\}$ and $U(\underline\tau)=0$ . When $\{\psi=0\}$ is null, this becomes $q=q^*$ and $t=t^*$ almost everywhere.

Milestones

The path to the goal, in the book's order:

the dynamic revelation principle (Proposition 11.1);
the reduction of incentive compatibility to two families of inequalities (Proposition 11.2);
the ex post characterization (Proposition 11.3);
monotonicity and absolute continuity of $U$ (Lemma 11.1);
the envelope formula $U'(\tau)=-\int q(\tau,\hat\theta)\,\partial F(\hat\theta\mid\tau)/\partial\tau\,d\hat\theta$ (Proposition 11.4);
the transfer formula (Proposition 11.5);
sufficiency of monotone allocation rules (Proposition 11.6);
individual rationality at $\underline\tau$ (Proposition 11.7).

Three extensions follow. Propositions 11.9 and 11.10 show that the privacy of the additional information $\gamma=F(\theta\mid\tau)$ costs the seller nothing. Proposition 11.11 gives the optimal mechanism with several buyers. Proposition 11.12 shows that with dynamic allocations and a fixed valuation, repeating the static posted price is optimal.

Significance

The result gives a practical rule: sell an option. Ex ante type $\tau$ pays a fee $t_0(\tau)$ for the right to buy later at the exercise price $p(\tau)$ , and $p$ decreases in $\tau$ . This explains refund and cancellation menus in advance-purchase markets. Proposition 11.10 adds that information the buyer receives after contracting generates no rents under Assumption 11.1. A seller therefore gains from contracting early and from disclosing information after contracting. Proposition 11.12 shows that, under full commitment, a monopolist gains nothing from responding to past purchases.

On the formal side, the results are proved in the literature and in the book, but none of them is machine-checked. The mission produces a verified envelope theorem in a two-dimensional type space where incentive compatibility does not imply monotonicity. It also produces a verified revenue-equivalence formula for sequential mechanisms, and the first verified optimal-mechanism results with dynamic information.

Difficulty

The static argument of Chapter 2 does not carry over directly. Incentive compatibility with respect to $\tau$ does not make $q$ increasing in $\tau$ . The buyer's first-period utility is an expectation over a whole schedule $q(\tau',\cdot)$ , so single crossing has no bite. The characterization therefore splits into necessary conditions (the envelope formula in $\tau$ , which needs Lipschitz continuity of $U$ from the bound $K$ ) and a sufficient condition (monotonicity in both arguments, via first-order stochastic dominance), and the two meet only under Assumption 11.1.

Definition 11.2(ii) quantifies over all off-path reporting functions. The revelation principle does not remove them, so Proposition 11.2 is needed before any envelope argument applies.

Pointwise maximization of the virtual surplus pins down $q$ only where $\psi\ne0$ and only almost everywhere. The optimal mechanism is therefore not unique in the pointwise sense the page states.

Formalization scope

Representation. $F(\theta\mid\tau)$ is F θ τ and $q(\tau,\theta)$ is q τ θ. Functions are total on $\mathbb R$ or $\mathbb R^2$ , and conditions quantify over the type intervals only. $\partial F/\partial\tau$ and $\partial f/\partial\tau$ are fields pinned by HasDerivWithinAt on $[\underline\tau,\bar\tau]$ .
Measurability. The book omits all measurability. Here the densities are jointly measurable, mechanisms are admissible (measurable on the type rectangle, $q\in[0,1]$ ), and reporting functions are measurable. In the observable- $\gamma$ model each $\tilde t(\tau,\cdot)$ is integrable on $[0,1]$ , and in the several-buyer model each payment $t_i$ is integrable against the distribution of the type profile, so that expected utilities and expected revenue are genuine integrals.
Revenue and a.e. Revenue is the integral of $t$ against the joint law with density $g(\tau)f(\theta\mid\tau)$ , and "almost everywhere" refers to that law.
Corrected necessity. The page's pointwise "if and only if" in Propositions 11.8 and 11.11 is corrected. The explicit optimal mechanism is kept, with the formulas (11.10), (11.11), (11.12) and $t_0$ of Proposition 11.5. Necessity is stated almost everywhere and off $\{\psi=0\}$ , and, for several buyers, off ties between virtual valuations.
Regularity. Propositions 11.9 and 11.10 assume $f$ and $\partial F/\partial\tau$ continuous in $(\tau,\theta)$ , the regularity the book invokes on p.217 to differentiate $F^{-1}(\gamma\mid\tau)$ .
Exercise price. $p(\tau)$ is the infimum of $\{\hat\theta\mid\psi(\tau,\hat\theta)\ge0\}$ .

Ruled out. Stating only that the cutoff mechanism is incentive-compatible and individually rational, or only that it beats posted prices, would trivialize the goal. The goal asserts optimality among all admissible incentive-compatible, individually rational sequential mechanisms with randomized allocations, together with the explicit fee $t_0$ and (11.12).

Infrastructure. A complete development needs envelope theorems for suprema of equi-differentiable families, integration by parts with absolutely continuous functions, differentiation under the integral sign, and change of variables $\gamma=F(\theta\mid\tau)$ . The single-buyer lemmas (Propositions 11.2–11.7) are reusable for the multi-buyer case through the interim mechanism $(Q_i,T_i)$ . Proofs of any milestone, and sorry-free lemmas on the definitions, are welcome.

Selected references

D. Krähmer and R. Strausz, Dynamic Mechanism Design, Chapter 11 in T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
P. Courty and H. Li, Sequential Screening, Review of Economic Studies 67 (2000) 697–717. https://doi.org/10.1111/1467-937X.00150
P. Eső and B. Szentes, Optimal Information Disclosure in Auctions and the Handicap Auction, Review of Economic Studies 74 (2007) 705–731. https://doi.org/10.1111/j.1467-937X.2007.00438.x
D. P. Baron and D. Besanko, Regulation and Information in a Continuing Relationship, Information Economics and Policy 1 (1984) 267–302.

18 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Probability·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design X: Robust Mechanism Design — Belief Revelation on Finite Type SpacesTextbook

Motivation

Classical Bayesian mechanism design assumes that the designer knows the agents' beliefs about each other: typically a commonly known prior over independent private values. Wilson's critique (1987) observed that mechanisms tuned to such a prior can depend on details that no designer knows, and a literature on robust mechanism design replaced the fixed prior by a large family of possible beliefs. Chapter 10 of Börgers, An Introduction to the Theory of Mechanism Design (OUP 2015), develops this programme in the framework of Bergemann and Morris (2001, 2005): agents' information is described by a type space, the designer is uncertain which beliefs agents hold, and mechanisms are compared across all type profiles at once.

Timeline of the results formalized here:

1980: Hylland shows that strategy-proof random mechanisms satisfying unanimity conditions are random dictatorships; Dutta, Peters and Sen (2007, 2008) give and correct the cardinal version used in the chapter.
1985: Mertens and Zamir construct the universal type space of belief hierarchies; the space of finite types is emphasized by Dekel, Fudenberg and Morris (2006).
1988: Crémer and McLean show that with correlated types satisfying a spanning condition, beliefs can be elicited at no cost (Proposition 6.4 of the book).
2001–2005: Bergemann and Morris introduce payoff and belief types and prove that on finite type spaces only incentive constraints between types with the same beliefs matter (their Proposition 4.5, the goal of this mission).
2010–2014: Smith, Börgers and Smith study the ranking of mechanisms without a common prior; random dictatorship with compromise comes from Börgers and Smith (2012, 2014).

Setting

There are finitely many agents $i \in I$ , and agent $i$ has a set $\Theta_i$ of payoff types. An outcome $x$ gives agent $i$ the utility $u_i(x,\theta)$ , which may depend on all payoff types. A type space $\mathcal T = (T_i,\hat\theta_i,\hat\beta_i)_{i\in I}$ consists of nonempty sets $T_i$ of types, a payoff type map $\hat\theta_i : T_i \to \Theta_i$ and a belief map $\hat\beta_i : T_i \to \Delta(T_{-i})$ , where $T_{-i} = \prod_{j\ne i}T_j$ . Different types may share a payoff type and differ only in their beliefs, and vice versa. A common prior is a distribution $\mu$ on $T$ from which every type's belief is obtained by conditioning. A type space has a large variety of certainties if for every $\theta_i$ and $\theta_{-i}$ some type with payoff type $\theta_i$ is certain that the others' payoff types are $\theta_{-i}$ . The space of finite types $\mathcal T^+$ collects every infinite hierarchy of beliefs ("I believe that you believe that …") that is generated by a type of some finite type space.

A mechanism $(S_1,\dots,S_N,g)$ has strategy sets $S_i$ and an outcome rule $g : S \to \Delta(X)$ . Strategies $\sigma_i : T_i \to \Delta(S_i)$ form a Bayesian equilibrium if each type maximizes expected utility under its own belief; it is belief-independent if types with equal payoff types play alike, and ex post if each type's choice stays optimal when it becomes certain of the others' types. A direct mechanism asks agents for their types, a reduced direct mechanism only for their payoff types. In the quasi-linear case outcomes are $(a,t_1,\dots,t_N)$ and $u_i = v_i(a,\theta) - t_i$ , with $t_i$ paid by agent $i$ ; a direct mechanism is $(q,t)$ .

Formalization targets

Goal: belief revelation on finite type spaces (Proposition 10.6)

On a finite type space with quasi-linear utilities, suppose that for every agent no belief in $\{\hat\beta_i(\tau_i) : \tau_i\in T_i\}$ is a convex combination of the others, and that in the direct mechanism $(q,t)$ no type wants to imitate another type with the same belief. Then there is a direct mechanism $(\tilde q,\tilde t)$ in which truth telling is a Bayesian equilibrium, with

\tilde q(\tau) = q(\tau)\ \ \forall \tau\in T,\qquad \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\,\tilde t_i(\tau) = \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\, t_i(\tau)\ \ \forall i,\tau_i.

The goal fixes neither the transfers $\tilde t$ nor any bound on them; it asserts the existence of a truthful mechanism with the same alternatives and the same interim payments.

Milestones

The other fourteen numbered results of the chapter: conditional independence of payoff types under a full-support common prior (10.1); three revelation principles (10.2–10.4); existence of Bayesian equilibria of finite mechanisms on $\mathcal T^+$ (10.5); betting between agents with inconsistent beliefs (10.7); ex post implementation of unique equilibrium outcomes and alternatives (10.8, 10.9); emptiness of the set of undominated auctions under interim Pareto welfare and under ex post revenue (10.10, 10.11); Hylland's characterization of random dictatorship (10.12); and three comparisons of random dictatorship with random dictatorship with compromise (10.13–10.15).

Significance

Proposition 10.6 reduces the design problem on a finite type space to incentive constraints among types with the same beliefs: belief types can always be elicited by side payments that leave interim utilities unchanged. With a common prior and Proposition 10.1 this yields optimal mechanisms by solving an independent-types problem for each profile of belief types (§10.8; Farinha Luz 2013 carries this out for auctions). Proposition 10.7 and its consequences 10.10–10.11 show why the same construction cannot be used without a common prior: inconsistent beliefs allow unbounded bets, so interim or revenue criteria admit no undominated mechanism. Propositions 10.12–10.15 show that relaxing belief independence escapes Hylland's impossibility result in the voting problem.

None of these results is formalized elsewhere to our knowledge. The book proves only some of them (10.1, 10.5, 10.8, 10.9, 10.13–10.15 are proved or outlined; 10.6 is sketched; the proofs of 10.2–10.4 are omitted as standard; 10.7 and 10.10–10.12 are stated without proof), so formalization also produces complete proofs of results the book leaves informal. Two printed statements are corrected (see Formalization scope).

Difficulty

The obvious approach to Proposition 10.6 applies the Crémer–McLean construction type by type. This fails because several types may share a belief: a side payment that depends on the reported belief cannot separate them, and the convex-independence condition concerns the set of distinct beliefs rather than the indexed family of types.

For the results on $\mathcal T^+$ , a type is an infinite belief hierarchy, and a strategy must be one function on all finite types simultaneously. Existence (10.5) cannot be obtained by applying Nash's theorem to a single finite type space, because a type belongs to many finite type spaces and must play the same strategy in all of them. Hylland's theorem (10.12) requires a full characterization of strategy-proof random rules on a cardinal preference domain.

Formalization scope

Distributions $\Delta(X)$ are countably supported (PMF X); expected utilities are sums. The book leaves the measure structure of type spaces unspecified (p.179, note 3); finite type spaces, $\mathcal T^+$ and point beliefs are covered exactly. A Bayesian equilibrium requires every type's expected utility to exist (absolute summability) under every mixed strategy.
A type's belief is a distribution on $\prod_{j\ne i}T_j$ . Beliefs in Proposition 10.6 are vectors in $\mathbb R^{T_{-i}}$ , and condition (i) is stated with the convex hull of the other distinct beliefs.
Quasi-linear direct mechanisms are deterministic, $q : T\to A$ , $t_i : T\to\mathbb R$ . Mixed misreports are allowed in every equilibrium notion.
$\mathcal T^+$ is built from belief hierarchies encoded level by level ( $L_0 = \Theta_i$ , $L_{n+1} = \Theta_i\times\Delta(\prod_{j\ne i}L_{n,j})$ ) and the finite type spaces generating them. The universal type space (Definition 10.5) is not needed and not formalized.
§10.11: two agents Fin 2, candidates $\{a,b,c\}$ , strict private vNM utilities with every strict utility attained; mechanisms map to lotteries over candidates; rankings are bijections C ≃ Fin 3.
Corrections of the page: in Proposition 10.7 the signs of the transfers in (v) are reversed on the page relative to the bet described on p.186 and are stated as described; Proposition 10.9 is false under a large variety of certainties alone and is stated under the common-certainty condition that its proof uses, on type spaces whose beliefs have finite support (with countably supported beliefs the reduced mechanism's expected utilities need not exist). Both are explained in the item notes.
The goal is not trivialized by taking $(\tilde q,\tilde t) = (q,t)$ : condition (ii) constrains only types with the same belief, so the original mechanism is in general not incentive-compatible, and the conclusion demands full Bayesian incentive compatibility.

Welcome contributions: a finite Farkas/separation lemma in the form needed for 10.6 (the platform has Polyhedral.farkas_lemma), basic API for PMF-valued type spaces (products of mixed strategies, conditioning), and the hierarchy map of finite type spaces, which all $\mathcal T^+$ milestones share.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 10. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
D. Bergemann, S. Morris, Robust Mechanism Design, Cowles Foundation Discussion Paper 1421, 2001; Econometrica 73 (2005) 1771–1813. https://doi.org/10.1111/j.1468-0262.2005.00638.x
J. Crémer, R. McLean, Full Extraction of the Surplus in Bayesian and Dominant Strategy Auctions, Econometrica 56 (1988) 1247–1257. https://doi.org/10.2307/1913096
J.-F. Mertens, S. Zamir, Formulation of Bayesian Analysis for Games with Incomplete Information, International Journal of Game Theory 14 (1985) 1–29. https://doi.org/10.1007/BF01770224
B. Dutta, H. Peters, A. Sen, Strategy-Proof Cardinal Decision Schemes, Social Choice and Welfare 28 (2007) 163–179. https://doi.org/10.1007/s00355-006-0152-4
T. Börgers, D. Smith, Robust Mechanism Design and Dominant Strategy Voting Rules, Theoretical Economics 9 (2014) 339–360. https://doi.org/10.3982/TE1100

19 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design IX: Monotone Direct Mechanisms Are Dictatorial (Gibbard–Satterthwaite)Textbook

Motivation

Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.

This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.

Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.

Setting

There is a finite set $I=\{1,\dots,N\}$ of agents and a finite set $A$ of alternatives. Each agent $i$ has a preference relation $R_i$ over $A$ ; $a\,R_i\,b$ reads " $a$ is weakly preferred to $b$ ". Every $R_i$ is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is $P_i$ . The set of all linear orders over $A$ is $\mathcal R$ , and a profile is $R=(R_1,\dots,R_N)\in\mathcal R^N$ . $(R_i',R_{-i})$ is the profile obtained from $R$ by replacing agent $i$ 's preference with $R_i'$ .

A direct mechanism is a function $f:\mathcal R^N\to A$ (Definition 8.1). It is

dominant strategy incentive-compatible (DSIC) if $f(R_i,R_{-i})\,R_i\,f(R_i',R_{-i})$ for all $i$ , $R$ , $R_i'$ (Definition 8.2);
dictatorial if some agent $i$ satisfies $f(R)\,R_i\,a$ for all profiles $R$ and all $a\in A$ (Definition 8.3);
monotone if $f(R)=a$ and, for every $i$ , $a\,R_i\,b\Rightarrow a\,R_i'\,b$ for all $b$ , together imply $f(R')=a$ (Definition 8.4);
set-monotone if $f(R)\in B$ and, for every $i$ , $R_i'$ differs from $R_i$ only in the ranking of elements of $B$ , together imply $f(R')\in B$ (Definition 8.5);
unanimity-respecting if $f(R)=a$ whenever every agent ranks $a$ at the top (Definition 8.6).

"The range of $f$ is $A$ " means that every alternative is chosen at some profile.

For §8.3 the alternatives are labelled $1,\dots,K$ . A preference is single-peaked if it has a top alternative $k(i)$ and declines monotonically to the right and to the left of it. $\hat{\mathcal R}$ is the set of single-peaked preferences, and on the restricted domain $\hat{\mathcal R}^N$ DSIC and dictatorship are read with all profiles and deviations taken from $\hat{\mathcal R}$ .

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

|A|\ge 3,\quad f(\mathcal R^N)=A,\quad f\ \text{monotone}\ \Longrightarrow\ \exists\, i\in I\ \ \forall R\in\mathcal R^N\ \forall a\in A:\ f(R)\,R_i\,a.

This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.

Milestones

Proposition 8.2: DSIC $\Rightarrow$ monotone.
Proposition 8.3: monotone $\Rightarrow$ set-monotone.
Proposition 8.4: monotone and full range $\Rightarrow$ respects unanimity.
Proposition 8.1 (Gibbard–Satterthwaite): for $|A|\ge3$ and full range, $f$ is DSIC $\iff$ $f$ is dictatorial.
Proposition 8.6: for $|A|\ge3$ and at least two agents, there is a mechanism on $\hat{\mathcal R}^N$ with range $A$ that is DSIC on $\hat{\mathcal R}^N$ and not dictatorial on $\hat{\mathcal R}^N$ .

Significance

The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.

Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.

Difficulty

Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative $c$ in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses $|A|\ge3$ cannot succeed. Formally, each "move $b$ just below $a$ in agent $j$ 's ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.

Formalization scope

A linear order is the structure LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. $A$ is a Fintype. "The range of $f$ is $A$ " is Function.Surjective f, and $|A|\ge3$ is 3 ≤ Fintype.card A.
Monotonicity is the book's Definition 8.4 for arbitrary pairs of profiles, with the lower-contour condition required for each agent separately. Dictatorship is ∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.
§8.3: the labelling is lab : A ≃ Fin K (labels $0,\dots,K-1$ ). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.
Two corrections of the page. The left-hand clause of single-peakedness is printed as $(\ell-1)\,R_i\,\ell$ and is used as $\ell\,R_i\,(\ell-1)$ (the book's words "decline monotonically to the left"). Proposition 8.6 carries the added hypothesis $N\ge2$ , since with one agent every onto strategy-proof rule is dictatorial.
Proposition 8.6 is an existence statement. The median voting mechanism is the book's witness, but the statement does not fix it.
Reusable beyond this mission: the linear-order profile model, Maskin monotonicity and the restricted-domain notions, which apply to Arrow-type results, implementation theory and Moulin's characterization. Proofs of any milestone, or an independent formal proof of Proposition 8.5, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
A. Gibbard, "Manipulation of voting schemes: a general result", Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
M. A. Satterthwaite, "Strategy-proofness and Arrow's conditions", Journal of Economic Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
E. Muller and M. A. Satterthwaite, "The equivalence of strong positive association and strategy-proofness", Journal of Economic Theory 14 (1977) 412–418. https://doi.org/10.1016/0022-0531(77)90140-5
P. J. Reny, "Arrow's theorem and the Gibbard–Satterthwaite theorem: a unified approach", Economics Letters 70 (2001) 99–105. https://doi.org/10.1016/S0165-1765(00)00332-3
H. Moulin, "On strategy-proofness and single peakedness", Public Choice 35 (1980) 437–455. https://doi.org/10.1007/BF00128122
S. Barberà, "An introduction to strategy-proof social choice functions", Social Choice and Welfare 18 (2001) 619–653. https://doi.org/10.1007/s003550100151

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design VIII: Dominant-Strategy Implementation of Efficient Decision Rules Is VCGTextbook

Motivation

A group of agents must choose one alternative from a set $A$ (whether to build a public project, who receives an object, which of several policies to adopt). Each agent privately knows how much each alternative is worth to them, and money can be transferred. A designer who wants the welfare-maximizing alternative must ask the agents for their valuations, and must set payments so that no agent gains by misreporting, whatever the others report. This requirement, dominant strategy incentive compatibility, does not depend on what agents believe about one another, which is why it is the standard robustness benchmark in public economics, auction design and algorithmic game theory.

The Vickrey–Clarke–Groves (VCG) mechanisms solve this problem for every efficient decision rule. The central question of Chapter 7 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), is whether they are the only solution, and what can be implemented in dominant strategies at all.

Timeline:

1961–1973: Vickrey (1961), Clarke (1971) and Groves (1973) introduce the payments that make efficient decisions dominant-strategy incentive-compatible.
1977: Green and Laffont (Econometrica 45) show that, when valuations range over a sufficiently rich connected domain, every efficient dominant-strategy mechanism has the Groves form.
1979: Holmström (Econometrica 47) extends the uniqueness result to smoothly connected domains. Roberts (1979) characterizes decision rules with positive association of differences on unrestricted domains as weighted welfare maximizers.
1987: Rochet (J. Math. Econ. 16) characterizes implementable decision rules by cyclical monotonicity, with no structure on alternatives or types.
2001: Krishna and Maenner (Econometrica 69) prove payoff equivalence for convex type sets and utilities convex in the type.
2009: Lavi, Mu'alem and Nisan (Soc. Choice Welf. 32) give two short proofs of Roberts' theorem.

Setting

There is a finite set $I$ of agents and a set $A$ of alternatives. Agent $i$ has a type $\theta_i$ from an abstract set $\Theta_i$ . If alternative $a$ is chosen and agent $i$ pays $t_i$ , agent $i$ 's utility is $u_i(a,\theta_i) - t_i$ . A type vector is $\theta \in \Theta = \prod_i \Theta_i$ ; $\theta_{-i} \in \Theta_{-i} = \prod_{j \ne i}\Theta_j$ omits agent $i$ , and $(\theta_i', \theta_{-i})$ replaces agent $i$ 's type by $\theta_i'$ .

A direct mechanism $(q, t_1, \dots, t_N)$ consists of a decision rule $q : \Theta \to A$ and transfer rules $t_i : \Theta \to \mathbb R$ . It is dominant strategy incentive-compatible (DSIC) if for all $\theta$ , $i$ and $\theta_i'$ ,

u_i(q(\theta),\theta_i) - t_i(\theta) \ \ge\ u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i}).

A decision rule is efficient if $q(\theta)$ maximizes $\sum_i u_i(a,\theta_i)$ over $a \in A$ at every $\theta$ . A mechanism is VCG if $q$ is efficient and every agent's transfer has the form

t_i(\theta) = -\sum_{j \ne i} u_j(q(\theta),\theta_j) + \tau_i(\theta_{-i})

for some function $\tau_i$ of the other agents' types. The chapter also uses positive association of differences (PAD: if $q(\theta) = a$ and every agent's utility advantage of $a$ over every other alternative strictly increases from $\theta$ to $\theta'$ , then $q(\theta') = a$ ), flexibility (the range $q(\Theta)$ has at least three elements), ex post individual rationality and ex post budget balance ( $\sum_i t_i(\theta) = 0$ ).

Formalization targets

Goal: uniqueness of VCG (Corollary 7.1, Green–Laffont–Holmström)

If every $\Theta_i$ is a convex subset of a Euclidean space $\mathbb R^{d_i}$ and every $u_i(a,\cdot)$ is convex and continuous on $\Theta_i$ , then every DSIC mechanism $(q,t)$ with an efficient $q$ is a VCG mechanism: for each $i$ there is $\tau_i : \Theta_{-i} \to \mathbb R$ with

t_i(\theta) = -\sum_{j \ne i} u_j(q(\theta),\theta_j) + \tau_i(\theta_{-i}) \qquad \text{for all } \theta.

The goal leaves $A$ , the number of agents and the dimensions $d_i$ free; it asserts only the form of the transfers.

Milestones

Every numbered result of Chapter 7 except Proposition 7.6 (see Formalization scope):

Proposition 7.1: implementability iff cyclical monotonicity in each agent's type (Rochet).
Proposition 7.2: on bounded, one-dimensional type sets, implementability iff monotonicity.
Proposition 7.3: under the goal's convexity hypotheses, the transfers implementing a given $q$ are unique up to $\tau_i(\theta_{-i})$ .
Proposition 7.4: VCG mechanisms are DSIC.
Proposition 7.5: weak monotonicity in every $\theta_i$ implies PAD.
Proposition 7.7 (Roberts): on unrestricted domains with finite $A$ , a flexible $q$ with range $q(\Theta) = A$ satisfies PAD iff there are $k_i \ge 0$ , not all zero, and $F : A \to \mathbb R$ with $\sum_i k_i u_i(q(\theta),\theta_i) + F(q(\theta)) \ge \sum_i k_i u_i(a,\theta_i) + F(a)$ for all $a \in A$ .
Proposition 7.8: affine maximizers with all $k_i > 0$ are implementable.
Proposition 7.9: ex post individual rationality holds iff it holds at the lowest type $\underline\theta_i$ with outside option $\underline a_i$ .
Proposition 7.10: with $N \ge 2$ , a budget-balanced VCG mechanism for efficient $q$ exists iff $\sum_i u_i(q(\theta),\theta_i) = \sum_i f_i(\theta_{-i})$ for some $f_i : \Theta_{-i} \to \mathbb R$ .

Significance

Corollary 7.1 turns the VCG construction from one solution into the complete answer. Any question about efficient dominant-strategy mechanisms (revenue, budget balance, individual rationality) reduces to a question about the functions $\tau_i$ . With Proposition 7.10 it gives a necessary and sufficient condition for efficient, budget-balanced dominant-strategy implementation. That condition fails in bilateral trade, and the failure does not use individual rationality. Roberts' theorem plays the same role for inefficient rules: on unrestricted domains, weighted welfare maximization is essentially all that can be implemented.

All of these results are proved in the literature, and none is formalized. The platform has VCG incentive compatibility and weak monotonicity for valuation-based types (the Algorithmic Game Theory IV mission). It has no uniqueness theorem, no revenue equivalence for multidimensional convex types, no Rochet theorem and no Roberts theorem. The book proves Corollary 7.1 from Proposition 7.3, but proves 7.3 itself only by reference to Krishna and Maenner. It states Roberts' theorem without proof.

Difficulty

The uniqueness claim does not follow from incentive compatibility alone. With finitely many types it is false, because any transfers inside the gaps left by the incentive constraints work (Börgers §5.8). The work lies in showing that, along every segment in the convex type set, an agent's equilibrium utility is pinned down by the decision rule. The equilibrium utility is a pointwise supremum of convex functions, one for each report, and the chosen alternative can change at uncountably many points of the segment. A differentiable envelope argument is therefore not directly available. At the boundary of the type set, convexity alone does not prevent upward jumps, which is why continuity is part of the hypotheses. Roberts' theorem needs a separate, combinatorial analysis of the sets of utility differences at which each alternative is chosen, and flexibility is essential there.

Formalization scope

Agents form a finite type ι with decidable equality. Types are arbitrary types Θ i, and utilities are u : ∀ i, A → Θ i → ℝ. The profile $(\theta_i',\theta_{-i})$ is Function.update θ i θ'. $\Theta_{-i}$ is the product Others Θ i over j ≠ i, so each $\tau_i$ and $f_i$ is a function of the others' types only; a constant or a function of the full profile would change the theorem. In the goal and Proposition 7.3, $\Theta_i$ is a convex set S i in EuclideanSpace ℝ (Fin (d i)).

Deviations from the page, each forced by a counterexample recorded in the item's natural-language statement:

Corollary 7.1 and Proposition 7.3 add continuity of $u_i(a,\cdot)$ on $\Theta_i$ . With convexity alone, a utility with a jump at the endpoint of $[0,1]$ admits a non-VCG DSIC mechanism.
Proposition 7.7 is stated with $k_i \ge 0$ , not all zero, instead of $k_i > 0$ , and with the added hypothesis that $q$ is onto $A$ (the conclusion still ranges over all $a \in A$ , as on the page). Dictatorships and affine maximizers over a proper subset of $A$ are counterexamples to the printed version.
Proposition 7.6 (flexible PAD rules on unrestricted domains are implementable) is false as printed. It is not a milestone; the reason is in the mission's hard list.
Proposition 7.10 adds $N \ge 2$ , since its proof divides by $N-1$ .

The trivializing formalization to avoid is proving Proposition 7.4 (VCG $\Rightarrow$ DSIC) in place of the goal (DSIC $+$ efficient $\Rightarrow$ VCG). A development that proves the goal needs reusable infrastructure: convex functions restricted to segments, absolute continuity of continuous convex functions on compact intervals, and an envelope theorem for suprema of convex functions. Proofs of Rochet's and Roberts' theorems in this abstract setting are also welcome.

Selected references

T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 7. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11, 1971. https://doi.org/10.1007/BF01726210
T. Groves, Incentives in Teams, Econometrica 41, 1973. https://doi.org/10.2307/1914085
J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45, 1977. https://doi.org/10.2307/1911219
B. Holmström, Groves' Scheme on Restricted Domains, Econometrica 47, 1979. https://www.jstor.org/stable/1911954
K. Roberts, The Characterization of Implementable Choice Rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–348.
J.-C. Rochet, A Necessary and Sufficient Condition for Rationalizability in a Quasi-Linear Context, Journal of Mathematical Economics 16, 1987. https://doi.org/10.1016/0304-4068(87)90007-3
V. Krishna and E. Maenner, Convex Potentials with an Application to Mechanism Design, Econometrica 69, 2001. https://doi.org/10.1111/1468-0262.00233
R. Lavi, A. Mu'alem and N. Nisan, Two Simplified Proofs for Roberts' Theorem, Social Choice and Welfare 32, 2009. https://doi.org/10.1007/s00355-008-0333-3
P. Milgrom, Putting Auction Theory to Work, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511813825

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Mechanism Design·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design VI: Rochet's Theorem — Implementability Is Cyclical MonotonicityTextbook

Motivation

Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.

This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.

Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.

Setting

A designer and one agent choose an alternative $a$ from a set $A$ . The agent has a type $\theta$ in a nonempty set $\Theta$ . With utility function $u : A \times \Theta \to \mathbb R$ , her payoff from $a$ when she pays $t$ is $u(a,\theta) - t$ . Neither $A$ nor $\Theta$ carries any structure.

A direct mechanism is a decision rule $q : \Theta \to A$ and a transfer rule $t : \Theta \to \mathbb R$ . It is incentive-compatible if $u(q(\theta),\theta) - t(\theta) \ge u(q(\theta'),\theta) - t(\theta')$ for all $\theta,\theta'$ . A decision rule is implementable if some $t$ makes it incentive-compatible. It is weakly monotone if $u(q(\theta_1),\theta_1) - u(q(\theta_2),\theta_1) \ge u(q(\theta_1),\theta_2) - u(q(\theta_2),\theta_2)$ for all pairs of types. It is cyclically monotone if for every finite sequence of types $\theta^1,\dots,\theta^k$ with $\theta^k = \theta^1$ ,

\sum_{\kappa=1}^{k-1}\bigl(u(q(\theta^\kappa),\theta^{\kappa+1}) - u(q(\theta^\kappa),\theta^\kappa)\bigr) \le 0 .

A complete and transitive order $R$ of $A$ induces a partial order on types: $\theta \succ_R \theta'$ if $\theta$ values every $R$ -higher alternative strictly more, relative to an $R$ -lower one, than $\theta'$ does, and neither type distinguishes $R$ -indifferent alternatives. The type set is one-dimensional if any two distinct types are $\succ_R$ -comparable, and bounded if all utility differences lie in $(-c,c)$ for some $c > 0$ . It is rich if, for some reflexive and transitive relation $R$ , every function $v : A \to \mathbb R$ with $aRb \Rightarrow v(a) \ge v(b)$ is some type's utility function. A mechanism is individually rational with outside option $a$ if every type does at least as well as with $a$ and no payment.

Formalization targets

Goal: Proposition 5.2 (Rochet)

q \text{ implementable} \iff q \text{ cyclically monotone},

for arbitrary $A$ , nonempty $\Theta$ and $u$ .

Milestones

Proposition 5.1: implementable $\Rightarrow$ weakly monotone.
Proposition 5.3: for lotteries over finitely many outcomes, $\Theta \subseteq \mathbb R^\Omega$ convex and $u(p,\theta) = p\cdot\theta$ , $q$ is implementable iff there is a convex $U$ on $\Theta$ with $U(\theta') \ge U(\theta) + q(\theta)\cdot(\theta'-\theta)$ for all $\theta,\theta'$ .
Proposition 5.4: weakly monotone $\Rightarrow$ ( $\theta \succ_R \theta' \Rightarrow q(\theta)\,R\,q(\theta')$ ), for every complete transitive $R$ .
Proposition 5.5: on one-dimensional type sets, weak monotonicity $\iff$ monotonicity with respect to $R$ .
Proposition 5.6: $A$ finite, $\Theta$ bounded and one-dimensional: monotone with respect to $R$ $\Rightarrow$ implementable.
Proposition 5.7 (Bikhchandani et al.): $A$ finite, rich and consistent domain: weakly monotone $\Rightarrow$ implementable.
Proposition 5.8 (revenue equivalence): on convex $\Theta \subseteq \mathbb R^n$ with $u(a,\cdot)$ convex and continuous, if $(q,t)$ is incentive-compatible then $(q,t')$ is iff $t' = t + \tau$ for a constant $\tau$ .
Proposition 5.9: on one-dimensional type sets with a lowest type $\underline\theta$ and a worst alternative $\underline a$ , an incentive-compatible mechanism is individually rational with outside option $\underline a$ iff $u(q(\underline\theta),\underline\theta) - t(\underline\theta) \ge u(\underline a,\underline\theta)$ .

Significance

Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns $t(\theta)$ , into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.

All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations $A \to \mathbb R$ ), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.

Difficulty

Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in $\Theta$ without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.

Formalization scope

Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length $k = m+1$ is a map Fin (m+1) → Θ with equal first and last entries, and its $m$ summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.

The explicit statements are fixed as follows:

Proposition 5.8's conclusion is the exact translation form $t'(\theta) = t(\theta) + \tau$ for one $\tau$ and all $\theta$ .
Proposition 5.9's condition is the single inequality at $\underline\theta$ .
Boundedness in Proposition 5.6 is Definition 5.9's strict two-sided bound with some $c > 0$ .

Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:

Proposition 5.7 adds Bikhchandani et al.'s requirement that every type's utility respects $R$ .
Proposition 5.8 adds continuity of $u(a,\cdot)$ on $\Theta$ (automatic in the relative interior).

Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite $\Theta$ , finite $A$ or bounded utilities, is a different and much weaker theorem and does not close the goal.

The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 5. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context," Journal of Mathematical Economics 16 (1987) 191–200. https://doi.org/10.1016/0304-4068(87)90007-3
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 24.8.
V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design," Econometrica 69 (2001) 1113–1119. https://doi.org/10.1111/1468-0262.00233
S. Bikhchandani, S. Chatterji, R. Lavi, A. Mu'alem, N. Nisan and A. Sen, "Weak monotonicity characterizes deterministic dominant-strategy implementation," Econometrica 74 (2006) 1109–1132. https://doi.org/10.1111/j.1468-0262.2006.00695.x
M. Saks and L. Yu, "Weak monotonicity suffices for truthfulness on convex domains," Proceedings of the 6th ACM Conference on Electronic Commerce (2005) 286–293. https://doi.org/10.1145/1064009.1064039

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design V: Dominant-Strategy Public Goods Mechanisms for Two Agents Are Fixed Cost SharesTextbook

Motivation

Bayesian mechanism design assumes that the designer knows a common prior from which every agent's beliefs about the others are derived. Chapter 4 of Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, DOI 10.1093/acprof:oso/9780199734023.001.0001) drops that assumption. The designer is unwilling to rely on anything about what agents believe about each other, and therefore requires that truth telling be optimal for every type whatever the other agents report (dominant strategy incentive compatibility) and that participation be worthwhile after all reports are known (ex post individual rationality). The chapter revisits the three examples of Chapter 3 (single unit auctions, public goods, bilateral trade) and asks which mechanisms survive these requirements.

The answer differs sharply between examples. In auctions nothing is lost: an expected-revenue-maximizing auction can be implemented in dominant strategies. With a budget constraint, the class collapses. For a public good shared by two agents, the only dominant-strategy, ex post individually rational mechanisms that exactly balance the budget are fixed cost shares; in bilateral trade they are fixed-price mechanisms. These results go back to the dominant-strategy literature on public goods (Serizawa 1999, Econometrica) and on bilateral trade (Hagerty and Rogerson 1987, Journal of Economic Theory), as the book's §4.5 records (p.93), and they explain why simple posted-price and cost-sharing rules are common in practice.

Setting

Every agent $i$ has a type $\theta_i$ in an interval. In the auction and the public good examples the interval is $[\underline\theta,\bar\theta]$ with $0 \le \underline\theta < \bar\theta$ ; $\Theta = [\underline\theta,\bar\theta]^I$ is the set of type vectors, and $\theta_{-i}$ is $\theta$ without its $i$ -th entry. A direct mechanism asks every agent to report a type and maps the reports to an outcome.

Auction (§4.2). A seller has one good. The mechanism consists of allocation probabilities $q_i(\theta) \ge 0$ with $\sum_i q_i(\theta) \le 1$ and payments $t_i(\theta)$ ; buyer $i$ 's utility is $\theta_i q_i(\theta) - t_i(\theta)$ .
Public good (§4.3). A good costing $c > 0$ is produced ( $q(\theta) = 1$ ) or not ( $q(\theta) = 0$ ); agent $i$ pays $t_i(\theta)$ and has utility $\theta_i q(\theta) - t_i(\theta)$ . Ex post budget balance is the equality $\sum_i t_i(\theta) = c\,q(\theta)$ for every $\theta$ .
Bilateral trade (§4.4). A seller with type $\theta_S \in [\underline\theta_S,\bar\theta_S]$ and a buyer with type $\theta_B \in [\underline\theta_B,\bar\theta_B]$ ; trade takes place ( $q(\theta) = 1$ ) or not; the seller receives $t_S(\theta)$ and has utility $\theta_S(1-q(\theta)) + t_S(\theta)$ ; the buyer pays $t_B(\theta)$ and has utility $\theta_B q(\theta) - t_B(\theta)$ . Ex post exact budget balance is $t_B = t_S$ .

A mechanism is dominant strategy incentive-compatible if for every agent, every true type, every false report and every report profile of the others, truthful reporting yields at least as much utility. It is ex post individually rational if every type's utility at every type vector is at least its outside option: $0$ for buyers and public good agents, $\theta_S$ (keeping the good) for the seller. A canonical mechanism (Definitions 4.3–4.5) allocates according to strictly increasing continuous scores $\psi_i(\theta_i)$ and charges each agent the smallest report with which the outcome would have been the same.

Formalization targets

Goal: Proposition 4.8, fixed cost shares

For $N = 2$ and a decision rule whose production set $\{\theta \in \Theta \mid q(\theta) = 1\}$ is closed, a direct public good mechanism is dominant strategy incentive-compatible, ex post individually rational and ex post budget balanced if and only if there are $\tau_1, \tau_2 \in \mathbb R$ with $\tau_1 + \tau_2 = c$ and, for all $\theta \in \Theta$ ,

q(\theta) = 1,\ t_i(\theta) = \tau_i \ \text{ if } \theta_1 \ge \tau_1 \text{ and } \theta_2 \ge \tau_2; \qquad q(\theta) = 0,\ t_i(\theta) = 0 \ \text{ otherwise.}

Both directions are part of the goal; the "only if" direction is the content.

Milestones

The revelation principle for dominant strategies (Proposition 4.1).
Characterizations of dominant strategy incentive compatibility: monotone allocation with the envelope payment formula in auctions (Proposition 4.2), threshold rules with payment jump $\hat\tau_i - \tau_i = \hat\theta_i$ for public goods (Proposition 4.5) and bilateral trade (Proposition 4.9).
Ex post individual rationality reduces to the lowest type, or to the highest seller type (Propositions 4.3, 4.6, 4.10).
Canonical mechanisms are dominant strategy incentive-compatible and ex post individually rational, with zero rent for the lowest type (Propositions 4.4, 4.7, 4.11).
The bilateral trade analogue of the goal (Proposition 4.12): the only such mechanisms with $t_B = t_S$ and closed trade set are no trade, or trade at a fixed price $\hat\theta$ exactly when $\theta_S \le \hat\theta \le \theta_B$ .

Significance

Proposition 4.4 shows that the optimal auctions of Chapter 3 remain available without any assumption on beliefs, while Propositions 4.8 and 4.12 show that under exact budget balance, dominant strategy implementation forces rules that ignore reported valuations except through a yes/no participation decision. Together they mark the boundary between settings where the Bayesian and the belief-free approaches coincide and settings where the belief-free requirement is severe. This contrast motivates the robust mechanism design of Chapter 10.

These results are proved in the book: Propositions 4.5 and 4.8 in full, the others with proofs omitted or "analogous". No machine-checked proof of them appears on the platform or in Mathlib. The platform has a single-parameter characterization in a different model (AGT.single_parameter_characterization: valuation profiles, win sets, normalized losers' payments) and the second-price dominance fact; neither covers public goods, bilateral trade, budget balance or randomized allocations. The mission would add a machine-checked belief-free counterpart of Chapter 3, including the two characterization theorems whose printed proofs leave cases to the reader.

Difficulty

The characterizations (Propositions 4.2, 4.5, 4.9) are standard single-agent arguments applied to every profile of the others. The goal is harder. Proposition 4.5 describes each agent's incentives separately, for each report of the other agent, with thresholds and payments that may vary with that report. Budget balance couples the two agents' payments at every type vector. The step that fails when attempted naively is going from "a threshold for each $\theta_{-i}$ " to "one fixed threshold for each agent": the thresholds may lie outside the type interval, several degenerate configurations occur (an agent whose report never matters, a good that is always or never produced), and the printed proof treats the degenerate cases by assuming $\underline\theta = 0$ and leaves one of them "analogous". The closedness hypothesis is what makes the relevant minimal types exist; without it the boundary of the production set is not determined. Proposition 4.12 has the same structure with the seller's orientation reversed.

Formalization scope

Agents are a finite type with decidable equality (auctions, public goods), Fin 2 for the goal, and a pair (θS, θB) : ℝ × ℝ for bilateral trade. A deviation $(\theta_i', \theta_{-i})$ is Function.update θ i x for θ ∈ Θ; quantifying over θ ∈ Θ quantifies over $\theta_{-i}$ .
Decision and trading rules are real-valued and take values in $\{0,1\}$ on $\Theta$ ; auction allocations lie in $\Delta$ on $\Theta$ . Values outside $\Theta$ play no role.
Budget balance in §§4.3–4.4 is the equality $\sum_i t_i = c\,q$ (resp. $t_B = t_S$ ). The inequality of Definition 3.5 would make the goal false.
Explicit formulas stated as in the book: the payment identity of Proposition 4.2, the relation $\hat\tau_i - \tau_i = \hat\theta_i$ (Propositions 4.5, 4.9), the canonical payments of Definitions 4.3–4.5 (with the $1/n$ tie-splitting of Definition 4.3), the cost shares with $\tau_1 + \tau_2 = c$ (Proposition 4.8) and the fixed price $\hat\theta$ with trade iff $\theta_S \le \hat\theta \le \theta_B$ (Proposition 4.12). Minima and maxima in the canonical payments are written as sInf/sSup of sets that are nonempty and closed whenever they are used.
Thresholds $\hat\theta_i$ range over $\mathbb R$ and depend on $\theta_{-i}$ ; cost shares $\tau_i$ may be negative; the goal does not assume $\underline\theta = 0$ .
The general mechanism of Proposition 4.1 has arbitrary message sets and an outcome function to allocation probabilities and expected payments. Stating the revelation principle for a mechanism that is already direct would trivialize it and is ruled out.
The goal must not be weakened to one direction, to the existence of some fixed-share mechanism, or to budget balance as an inequality.

Contributions welcome: proofs of the characterization milestones (4.2, 4.5, 4.9), which the goal and Proposition 4.12 use; a proof of the goal covering the degenerate cases the book leaves to the reader; and the three-agent counterexample of p.90 as a separate statement.

Selected references

T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 4. DOI 10.1093/acprof:oso/9780199734023.001.0001
K. M. Hagerty and W. P. Rogerson, Robust trading mechanisms, Journal of Economic Theory 42 (1987) 94–107.
S. Serizawa, Strategy-proof and symmetric social choice functions for public good economies, Econometrica 67 (1999) 121–145.
D. Mookherjee and S. Reichelstein, Dominant strategy implementation of Bayesian incentive compatible allocation rules, Journal of Economic Theory 56 (1992) 378–399.

15 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Probability·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design IV: The Myerson–Satterthwaite TheoremTextbook

Motivation

Stock exchanges, commodity markets and trading platforms are institutions for trade between parties who each know something the other does not. The simplest version is bilateral trade: one seller, one buyer, one indivisible good, and each side privately knows its own value. The question is whether any trading institution can make the two trade exactly when trade is efficient, with both taking part voluntarily and without a subsidy from outside. Myerson and Satterthwaite (1983) showed that, apart from trivial cases, none can. The result is one of the basic impossibility theorems of economic theory. It explains why bargaining under private information is inefficient, and it is the benchmark every later analysis of double auctions and market design compares against.

This mission formalizes Section 3.4 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): the impossibility theorem, the pivot-mechanism argument that proves it, the second-best and profit-maximizing trading mechanisms, and the uniform example.

Timeline. Vickrey (1961) noted the tension between efficiency and budget balance in markets with private values. Chatterjee and Samuelson (1983) studied the sealed-offer double auction and its linear equilibrium for uniform values. Myerson and Satterthwaite (1983) proved the impossibility for general independent distributions with overlapping supports, and computed the second-best mechanism; for uniform values it coincides with the Chatterjee–Samuelson linear equilibrium. Börgers (2015) gives the pivot-mechanism proof formalized here.

Setting

A seller $S$ owns one indivisible good; a buyer $B$ may buy it. The seller's value $\theta_S$ has distribution $F_S$ with density $f_S > 0$ on $[\underline\theta_S, \overline\theta_S]$ ; the buyer's value $\theta_B$ has distribution $F_B$ with density $f_B > 0$ on $[\underline\theta_B, \overline\theta_B]$ . The two intervals are nondegenerate and may differ, and the values are independent. The seller's utility is $t$ if she sells for $t$ and $\theta_S + t$ if she keeps the good and receives $t$ ; the buyer's is $\theta_B - t$ if he buys and pays $t$ , and $-t$ otherwise.

A direct mechanism is a trading rule $q : \Theta \to \{0,1\}$ on $\Theta = [\underline\theta_S, \overline\theta_S] \times [\underline\theta_B, \overline\theta_B]$ and transfers $t_S$ (received by the seller) and $t_B$ (paid by the buyer). Conditioning on one agent's type gives the interim trade probabilities $Q_S, Q_B$ , the interim transfers $T_S, T_B$ , and the interim utilities $U_S(\theta_S) = T_S(\theta_S) + (1 - Q_S(\theta_S))\theta_S$ and $U_B(\theta_B) = Q_B(\theta_B)\theta_B - T_B(\theta_B)$ . The mechanism is incentive-compatible if truthful reporting is a Bayesian equilibrium, individually rational if $U_S(\theta_S) \ge \theta_S$ and $U_B(\theta_B) \ge 0$ for all types, ex post budget balanced if $t_S(\theta) = t_B(\theta)$ for every $\theta$ , and ex ante budget balanced if $\mathbb E[t_S] = \mathbb E[t_B]$ . A first-best trading rule trades when $\theta_B > \theta_S$ and not when $\theta_B < \theta_S$ , with any choice at ties. The seller's virtual cost is $\psi_S = \theta_S + F_S/f_S$ and the buyer's virtual valuation is $\psi_B = \theta_B - (1 - F_B)/f_B$ ; the distributions are regular if both are increasing.

Formalization targets

Goal: Proposition 3.12 (Myerson–Satterthwaite)

An incentive-compatible, individually rational and ex post budget balanced direct mechanism with a first-best trading rule exists if and only if

\underline\theta_B \ge \overline\theta_S \quad\text{or}\quad \underline\theta_S \ge \overline\theta_B .

Milestones

Lemmas 3.9–3.11. The pivot mechanism is incentive-compatible and individually rational. Among all such mechanisms that implement a first-best rule, it maximizes $\mathbb E[t_B - t_S]$ . That quantity is negative whenever $\underline\theta_B < \overline\theta_S$ and $\overline\theta_B > \underline\theta_S$ .
Proposition 3.13 (second best). With overlapping supports and regular distributions, the welfare-maximizing incentive-compatible, individually rational, ex ante budget balanced mechanisms are characterized by the trading rule

q(\theta) = 1 \iff \theta_B - \tfrac{\lambda}{1+\lambda}\tfrac{1 - F_B(\theta_B)}{f_B(\theta_B)} \ge \theta_S + \tfrac{\lambda}{1+\lambda}\tfrac{F_S(\theta_S)}{f_S(\theta_S)}

for some $\lambda > 0$ , exact budget balance $\int q\,(\psi_B - \psi_S)\,f = \overline\theta_S - \int \psi_S f$ , and the incentive-compatible payments with binding participation of $\overline\theta_S$ and $\underline\theta_B$ .

Proposition 3.14 (profit maximization). Profit $\mathbb E[t_B - t_S]$ is maximized by trading iff $\psi_B(\theta_B) > \psi_S(\theta_S)$ , with the same payment formulas.
Propositions 3.15–3.16 (uniform values on $[0,1]$ ). The second best trades iff $\theta_B - \theta_S > 1/4$ ; the profit maximizer trades iff $\theta_B - \theta_S > 1/2$ .

Significance

The theorem locates the source of inefficiency in bilateral bargaining in private information itself, not in any particular bargaining protocol: no mechanism, however clever, achieves efficient voluntary trade without a subsidy. It is the reason efficiency in markets is studied as a limit (large double auctions approach efficiency as the number of traders grows), and why a trading platform's fee structure is analyzed as a second-best problem. The pivot-mechanism argument is the same one that proves the impossibility of first-best public-goods provision (Proposition 3.7), so the two formalizations share their structure.

All results of this section are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no mechanism-design library. The platform has the Chatterjee–Samuelson linear equilibrium as an open statement about one particular game; this mission states results about all mechanisms. A complete development yields a reusable one-dimensional envelope/payoff-equivalence library for two agents with differently oriented types (the seller's incentive constraint runs from high types down), and the Lagrangian optimality argument for a linear objective under a single linear constraint.

Difficulty

The obvious attempt to prove impossibility looks for a contradiction between incentive compatibility and budget balance state by state. That fails: incentive compatibility and participation are interim constraints, so any single state admits budget-balanced transfers consistent with them, and the contradiction exists only after integrating over the prior. Two points need care. The seller's orientation is reversed: her trade probability is decreasing and her participation constraint binds at the highest type. And the deficit of the pivot mechanism must be shown to have positive probability, which uses that the supports overlap in a set with nonempty interior. The optimal-mechanism results additionally need that the trading rule implied by a Lagrange multiplier satisfies the monotonicity constraint, which is where regularity enters, and that a multiplier exists which makes the budget constraint bind.

Formalization scope

A type vector is a pair θ : ℝ × ℝ with θ.1 the seller's and θ.2 the buyer's value. The prior is Lebesgue measure on $\Theta$ with density $f_S(\theta_S) f_B(\theta_B)$ . Densities are measurable, strictly positive on the closed supports and integrate to one; nothing else, such as continuity, is assumed. The trading rule is real-valued with values in $\{0,1\}$ on $\Theta$ (deterministic, as in Definition 3.9). The measurability the book omits (Ch. 2 note 2) is built into the admissible class: $q$ , $t_S$ , $t_B$ are measurable with integrable transfers. "Increasing" is weak monotonicity, the book's convention.

Explicit formulas the statements carry: the first-best rule (3.61) with free tie rule, the pivot transfers of Definition 3.10, the rule (3.70) with parameter $\lambda > 0$ , the exact budget equation of Proposition 3.13 (ii), the payment formulas $T_B(\theta_B) = \theta_B Q_B(\theta_B) - \int_{\underline\theta_B}^{\theta_B} Q_B$ and $T_S(\theta_S) = \overline\theta_S - (1 - Q_S(\theta_S))\theta_S - \int_{\theta_S}^{\overline\theta_S}(1 - Q_S)$ , the profit rule $\psi_B > \psi_S$ , and the thresholds $1/4$ and $1/2$ .

The goal quantifies over every first-best trading rule and imposes budget balance as the ex post equality $t_S = t_B$ . Dropping budget balance, weakening it to $t_S \le t_B$ , or fixing one tie rule would give a different, and in the first case false, statement. The pointwise "if and only if … for all $\theta$ " characterizations of Propositions 3.13–3.16 are stated with necessity almost everywhere, since an optimal trading rule is determined only up to null sets. For Proposition 3.14 necessity is also restricted to $\{\psi_B \ne \psi_S\}$ : under weak regularity that tie set can have positive probability, and profit does not depend on the trading rule there.

Contributions welcome: proofs of the milestones, a two-agent payoff-equivalence lemma for the seller's reversed orientation, and a sorry-free construction of the pivot mechanism's integrability facts.

Selected references

R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
K. Chatterjee and W. Samuelson, Bargaining under incomplete information, Operations Research 31 (1983) 835–851. https://doi.org/10.1287/opre.31.5.835
W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.4. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Optimization+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design III: Impossibility of First-Best Public Goods ProvisionTextbook

Motivation

Whether a community can finance a shared project out of voluntary contributions, when each member knows only her own benefit from it, is one of the founding questions of mechanism design. Bayesian mechanism design began with mechanisms for the provision of public goods: d'Aspremont and Gérard-Varet (1979) and Arrow (1979) showed that the efficient decision can be made Bayesian incentive compatible with a budget that balances in every state, provided agents cannot opt out. Once participation is voluntary, this is no longer possible, and Güth and Hellwig (1986) studied the best mechanism under that constraint. The same tension between efficiency, incentives, voluntary participation and budget balance drives the Myerson–Satterthwaite theorem for bilateral trade, which the next mission of this series formalizes.

This mission formalizes Section 3.3 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), which treats the public goods problem in the independent private values model with a continuum of types. The section proves an impossibility theorem for first best provision and then characterizes the best mechanisms that respect the budget: the welfare-maximizing (second best) mechanism and the profit-maximizing one, with a worked two-agent uniform example.

Setting

A community of agents $I = \{1, \dots, N\}$ , $N \ge 2$ , decides whether to produce an indivisible, nonexcludable public good, $g \in \{0,1\}$ , at cost $c > 0$ . Agent $i$ pays a transfer $t_i$ and obtains utility $\theta_i g - t_i$ . Her type $\theta_i$ is private information, drawn independently across agents from a distribution $F_i$ with density $f_i$ , strictly positive on the common support $[\underline\theta, \bar\theta]$ , $0 \le \underline\theta < \bar\theta$ . The type space is $\Theta = [\underline\theta, \bar\theta]^N$ and $f(\theta) = \prod_i f_i(\theta_i)$ .

A direct mechanism is a decision rule $q : \Theta \to \{0,1\}$ and transfer rules $t_i : \Theta \to \mathbb R$ . For agent $i$ reporting $\theta_i$ , $Q_i(\theta_i)$ is the probability of production and $T_i(\theta_i)$ the expected transfer, taken over the other agents' types, and $U_i(\theta_i) = Q_i(\theta_i)\theta_i - T_i(\theta_i)$ . The mechanism is incentive compatible (IC) if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i, \theta_i, \theta_i'$ , and individually rational (IR) if $U_i(\theta_i) \ge 0$ for all $i, \theta_i$ . It is ex post budget balanced if $\sum_i t_i(\theta) \ge c\,q(\theta)$ for every $\theta$ , and ex ante budget balanced if this inequality holds after integrating both sides against $f$ .

Welfare is $(\sum_i \theta_i)\, g - \sum_i t_i$ . The first best decision rule is $q^*(\theta) = 1$ if $\sum_i \theta_i \ge c$ and $0$ otherwise; a first best mechanism uses $q^*$ and transfers that add up to exactly $c\,q^*(\theta)$ in every state. The pivot mechanism uses $q^*$ and

t_i(\theta) = \underline\theta\, q^*(\underline\theta,\theta_{-i}) + \big(q^*(\theta) - q^*(\underline\theta,\theta_{-i})\big)\Big(c - \sum_{j\ne i}\theta_j\Big).

The virtual valuation is $\psi_i(\theta_i) = \theta_i - (1-F_i(\theta_i))/f_i(\theta_i)$ , and $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Proposition 3.7

\exists\ \text{an IC and IR first best mechanism} \iff N\underline\theta \ge c \ \text{ or }\ N\bar\theta \le c .

In the two cases on the right, producing is efficient for every type vector or for none; in every other case efficient provision cannot be financed voluntarily.

Milestones

Proposition 3.6: every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
Lemma 3.6: the pivot mechanism is IC and IR.
Lemma 3.7: among IC and IR mechanisms with decision rule $q^*$ , the pivot mechanism has the largest expected budget surplus.
Lemma 3.8: if $N\underline\theta < c < N\bar\theta$ , the pivot mechanism's expected budget surplus is negative.
Proposition 3.8 (second best): under regularity and $N\underline\theta < c < N\bar\theta$ , an IC, IR, ex ante budget balanced mechanism maximizes expected welfare among such mechanisms iff for some $\lambda > 0$

q(\theta) = 1 \iff \sum_i \theta_i > c + \sum_i \frac{\lambda}{1+\lambda}\,\frac{1-F_i(\theta_i)}{f_i(\theta_i)},

the budget binds, $\int_\Theta q(\theta)\big[\sum_i \psi_i(\theta_i) - c\big] f(\theta)\,d\theta = 0$ , and $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$ . 6. Proposition 3.9 (profit maximization): under regularity, the profit-maximizing IC and IR mechanism produces iff $\sum_i \theta_i > c + \sum_i (1-F_i(\theta_i))/f_i(\theta_i)$ , with the same formula for $T_i$ . 7. Proposition 3.10 (Example 3.3: $N=2$ , uniform types on $[0,1]$ , $0<c<2$ ): the second best produces iff $\theta_1+\theta_2 > s$ , where $s$ is the unique root in $[0,1]$ of $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ if $c < 2/3$ , and $s = \tfrac12 + \tfrac34 c$ if $c \ge 2/3$ . 8. Proposition 3.11 (same example): the profit maximizer produces iff $\theta_1+\theta_2 > 1 + \tfrac12 c$ .

Significance

Proposition 3.7 says that with voluntary participation no mechanism both takes efficient production decisions and pays for them, outside the degenerate cases. It is the reason the rest of the section, and much of the applied literature on public goods, studies constrained optimum mechanisms: Proposition 3.8 describes what the best budget-respecting mechanism gives up (it undersupplies the good, producing only when valuations exceed a bound strictly above the cost), and Proposition 3.9 quantifies the further distortion under a monopoly supplier. The example makes the three thresholds explicit and comparable.

All results of the section are classical and proved in the book, several of them only sketched there (Proposition 3.9 is stated without proof; Proposition 3.8 invokes an infinite-dimensional Kuhn–Tucker theorem whose applicability is not checked). None of them is formalized in Lean. The mission produces a machine-checked account of the envelope and revenue-equivalence arguments with interim expectations over independent types, a checked pivot-mechanism deficit computation, and a checked Lagrangian characterization; the uniform example additionally certifies the book's arithmetic.

Difficulty

The naive argument for the goal fails at the first step: a mechanism that implements $q^*$ with a balanced budget in every state is not obviously comparable to one that is only IC and IR, because IC constrains interim expectations while budget balance is ex post. The impossibility needs a reduction of the whole class of IC, IR mechanisms with rule $q^*$ to a single extremal one, which requires the payoff equivalence formula for interim utilities and an exact integral identity for expected revenue in terms of virtual valuations. The strict deficit of the pivot mechanism then needs a case analysis over which agents are pivotal and a positive-probability argument. For Proposition 3.8, pointwise maximization of a Lagrangian is not enough: one must show the multiplier exists and is positive, that the maximizer satisfies the monotonicity constraint, and that uniqueness holds only up to null sets.

Formalization scope

Agents are Fin N with $N \ge 2$ ; types are vectors in Fin N → ℝ; the type distribution is the product of the marginal measures $f_i(x)\,dx$ on $[\underline\theta,\bar\theta]$ , which encodes independence. $Q_i$ and $T_i$ integrate the decision and transfer rules against this distribution with agent $i$ 's coordinate overwritten by her report. Decision rules are deterministic, with values in $\{0,1\}$ on $\Theta$ , as in Definition 3.4. Ties in the first best rule produce, as in the book's note 2 to Chapter 3; the second best and profit-maximizing rules use strict inequalities, as printed.

The book omits measurability and the existence of conditional expectations; the class of direct mechanisms here requires $q$ and each $t_i$ to be Borel measurable, each $t_i$ integrable, and each conditional expectation of $t_i$ given one agent's type to exist. The characterizations in Propositions 3.8–3.11 are stated in two directions: the stated rule, for every $\theta$ , is sufficient; necessity holds for almost every $\theta$ , since changing $q$ on a null set of type vectors changes nothing that is optimized. The explicit formulas the mission commits to are: the pivot transfers above; the second best rule with multiplier $\lambda > 0$ and the binding budget identity; $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i$ ; the cubic $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ for $c < 2/3$ ; $s = \tfrac12 + \tfrac34 c$ for $c \ge 2/3$ ; and $s = 1 + \tfrac12 c$ for the profit maximizer.

A trivializing formalization of the goal takes "first best" to mean only the decision rule $q^*$ ; the pivot mechanism would then be a witness in every case, so first best here also requires transfers adding up to exactly $c\,q^*(\theta)$ in every state.

Reusable infrastructure includes interim expectations over independent product distributions, the payoff and revenue equivalence lemmas for IC mechanisms, and the virtual-valuation identity for expected revenue; these are shared with the auction and bilateral trade chapters of the series. Contributions to any milestone, and to general lemmas about product measures with densities on boxes, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.3. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
C. d'Aspremont and L.-A. Gérard-Varet, Incentives and incomplete information, Journal of Public Economics 11 (1979) 25–45. https://doi.org/10.1016/0047-2727(79)90043-4
W. Güth and M. Hellwig, The private supply of a public good, Zeitschrift für Nationalökonomie, Supplement 5 (1986) 121–159.
R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969.

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Optimization+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design II: Myerson's Optimal Single-Unit AuctionTextbook

Why revenue-maximizing auctions matter

A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.

This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.

Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).

Setting

There are $N \ge 2$ potential buyers $i \in I = \{1,\dots,N\}$ . Buyer $i$ values the good at $\theta_i$ ; if he receives it and pays $t_i$ his utility is $\theta_i - t_i$ , and otherwise $-t_i$ . The seller's utility is $\sum_i t_i$ . The valuations $\theta_1,\dots,\theta_N$ are independent; $\theta_i$ has cumulative distribution function $F_i$ and density $f_i$ with $f_i(\theta_i) > 0$ on the common support $[\underline\theta, \bar\theta]$ , where $0 \le \underline\theta < \bar\theta$ . The type space is $\Theta = [\underline\theta,\bar\theta]^N$ and the joint density is $f(\theta) = \prod_i f_i(\theta_i)$ .

A direct mechanism asks buyers to report their types and consists of an allocation rule $q : \Theta \to \Delta$ , where $\Delta = \{(q_1,\dots,q_N) : 0 \le q_i \le 1,\ \sum_i q_i \le 1\}$ , and payment rules $t_i : \Theta \to \mathbb R$ . Its interim quantities are the expected allocation probability, payment and utility of buyer $i$ conditional on his own type:

Q_i(\theta_i) = \int_{\Theta_{-i}} q_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad T_i(\theta_i) = \int_{\Theta_{-i}} t_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad U_i = \theta_i Q_i - T_i.

The mechanism is incentive-compatible if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i,\theta_i,\theta_i'$ (truth-telling is a Bayesian Nash equilibrium) and individually rational if $U_i(\theta_i) \ge 0$ for all $i,\theta_i$ . The virtual valuation of buyer $i$ is

\psi_i(\theta_i) = \theta_i - \frac{1 - F_i(\theta_i)}{f_i(\theta_i)},

and the distribution $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Myerson's optimal auction (Proposition 3.4)

Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue $\mathbb E[\sum_i t_i(\theta)]$ exactly when, for every buyer $i$ ,

q_i(\theta) = \begin{cases}1 & \text{if } \psi_i(\theta_i) > 0 \text{ and } \psi_i(\theta_i) > \psi_j(\theta_j) \text{ for all } j \ne i,\\ 0&\text{otherwise,}\end{cases}\qquad T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx,

the allocation identity holding for almost every $\theta$ ; and such a mechanism exists.

Milestones

Proposition 3.1, the revelation principle: every Bayesian Nash equilibrium of every mechanism is replicated by truth-telling in an incentive-compatible direct mechanism.
Lemmas 3.1–3.4: incentive compatibility makes $Q_i$ increasing and $U_i$ convex with $U_i' = Q_i$ ; payoff equivalence $U_i(\theta_i) = U_i(\underline\theta) + \int_{\underline\theta}^{\theta_i} Q_i$ ; revenue equivalence for $T_i$ .
Proposition 3.2: incentive compatibility holds if and only if every $Q_i$ is increasing and the revenue-equivalence formula holds.
Proposition 3.3: under incentive compatibility, individual rationality is equivalent to $T_i(\underline\theta) \le \underline\theta Q_i(\underline\theta)$ .
Lemma 3.5: an optimal mechanism has $T_i(\underline\theta) = \underline\theta Q_i(\underline\theta)$ .
Eqs. (3.4)–(3.5): expected revenue equals expected virtual surplus $\sum_i \int_\Theta q_i(\theta)\psi_i(\theta_i) f(\theta)\,d\theta$ .
Proposition 3.5: a mechanism maximizes expected welfare $\mathbb E[\sum_i q_i(\theta)\theta_i]$ among incentive-compatible, individually rational mechanisms if and only if it gives the good to the highest value (almost everywhere) and $T_i(\theta_i) \le \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i}Q_i$ .

Significance

The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price $\psi^{-1}(0)$ when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.

The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end $\underline\theta \ge 0$ , Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on $[0,\bar v]$ .

Difficulty

The obvious argument maximizes the virtual surplus $\sum_i q_i(\theta)\psi_i(\theta_i)$ pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every $Q_i$ ; the pointwise maximizer is feasible only because regularity makes $\psi_i$ increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every $\psi_i$ and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of $U_i$ , with care at the endpoints of the type interval.

Formalization scope

Buyers form a finite type with at least two elements. The prior is the measure on $\mathbb R^N$ with density $\prod_i f_i(\theta_i)$ on $\Theta$ and no mass outside it; each $f_i$ is measurable, strictly positive on $[\underline\theta,\bar\theta]$ and integrates to $1$ ; $F_i(\theta_i) = \int_{\underline\theta}^{\theta_i} f_i$ . Allocation and payment rules are total functions whose values on $\Theta$ are constrained, and $Q_i$ , $T_i$ are prior expectations with the $i$ -th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of $\psi_i$ on $[\underline\theta,\bar\theta]$ (Assumption 3.1).

The following conventions are committed to:

Measurability. The book omits measurability throughout. The comparison class for optimality consists of mechanisms with measurable $q_i, t_i$ , integrable $t_i$ , and integrable sections $\theta_{-i}\mapsto t_i(\theta_i,\theta_{-i})$ . Without these hypotheses the Lean integrals would be $0$ and revenue comparisons would be meaningless.
Almost-everywhere characterizations. Propositions 3.4 and 3.5 are printed with "for all $\theta \in \Theta$ ". Changing $q$ on a null set of type vectors changes neither incentives nor revenue nor welfare, so the "only if" directions hold only almost everywhere; they are stated for almost every $\theta$ , and the existence of a mechanism satisfying the allocation rule at every $\theta$ is stated separately. The payment conditions hold for every $\theta_i$ .
Explicit formulas. The goal states Myerson's allocation rule and the payment formula $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$ explicitly. Proposition 3.5 states the efficient rule $q_i(\theta) = 1$ iff $\theta_i > \theta_j$ for all $j \ne i$ , and the payment inequality. A statement asserting only that some optimal mechanism exists, or only that the optimal auction is efficient, would not be this theorem.
Revelation principle. A general mechanism has arbitrary measurable message sets and an outcome function giving allocation probabilities in $\Delta$ and expected transfers; equilibria are in pure type-contingent strategies. A version in which the mechanism is already direct would be trivial and is not the statement.
Interim constraints. Incentive compatibility and individual rationality are Bayesian and interim, not dominant-strategy or ex post; the latter are the subject of a later mission.
Endpoints in Lemma 3.2. Differentiability of $U_i$ and $U_i' = Q_i$ are stated at interior points of $[\underline\theta,\bar\theta]$ .

The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.

Selected references

Tilman Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.2, pp. 31–45. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
John G. Riley and William F. Samuelson, Optimal Auctions, American Economic Review 71(3), 381–392, 1981. https://www.jstor.org/stable/1802786
William Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1), 8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
Partha Dasgupta, Peter Hammond and Eric Maskin, The Implementation of Social Choice Rules: Some General Results on Incentive Compatibility, Review of Economic Studies 46(2), 185–216, 1979. https://doi.org/10.2307/2297045

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Functional Analysis Mechanism Design+1·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design I: Screening and the Optimality of a Posted PriceTextbook

Motivation

A seller with one good and one buyer whose valuation she does not know faces the simplest problem of mechanism design: choose a selling procedure, anticipating that the buyer will act in his own interest given what he knows. The textbook answer, "post the monopoly price", is usually derived by optimizing over prices alone. The question that opens Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, doi:10.1093/acprof:oso/9780199734023.001.0001) is whether the seller could do better with anything else: negotiation, lotteries, menus of price–probability pairs, or any extensive game she can commit to.

Chapter 2 answers this for one buyer, and in doing so introduces the tools the rest of the book, and most of auction theory, reuse: the revelation principle, the envelope characterization of incentive compatibility, payoff and revenue equivalence, and the virtual valuation. The book's exposition of §2.2 follows Manelli and Vincent (2007), and the nonlinear pricing model of §2.3 is due to Mussa and Rosen (1978, doi:10.1016/0022-0531(78)90085-6); both attributions are the book's own (§2.5, p.29).

Setting

The buyer's type $\theta$ is his valuation for the good. His utility is $\theta-t$ if he receives the good and pays $t$ , and $-t$ if he only pays $t$ . The seller's belief about $\theta$ is a cumulative distribution function $F$ with density $f$ on an interval $[\underline\theta,\bar\theta]$ , $0\le\underline\theta<\bar\theta$ , with $f(\theta)>0$ throughout and $F(\theta)=\int_{\underline\theta}^{\theta}f(x)\,dx$ .

A direct mechanism is a pair $q:[\underline\theta,\bar\theta]\to[0,1]$ , $t:[\underline\theta,\bar\theta]\to\mathbb R$ : the buyer reports a type $\theta'$ , receives the good with probability $q(\theta')$ and pays $t(\theta')$ . Write $u(\theta)=\theta q(\theta)-t(\theta)$ . The mechanism is incentive-compatible if $u(\theta)\ge\theta q(\theta')-t(\theta')$ for all $\theta,\theta'$ , and individually rational if $u(\theta)\ge 0$ for all $\theta$ . The seller's expected revenue is $\int_{\underline\theta}^{\bar\theta}t(\theta)f(\theta)\,d\theta$ .

For the extreme-point argument, $\mathcal F$ denotes the space of functions on $[\underline\theta,\bar\theta]$ with the $L^1$ norm, and $M\subset\mathcal F$ the set of increasing functions with values in $[0,1]$ . A point $x$ of a convex set $C$ is an extreme point if for every $y\neq 0$ at least one of $x+y$ , $x-y$ lies outside $C$ .

In the nonlinear pricing model of §2.3 the good is divisible, quantity $q\ge 0$ costs the seller $cq$ with $c>0$ , and the buyer's utility is $\theta\nu(q)-t$ , with $\nu(0)=0$ , $\nu'>0$ , $\nu''<0$ , $\bar\theta\nu'(0)>c$ and $\lim_{q\to\infty}\bar\theta\nu'(q)<c$ . The seller maximizes expected profit $\int(t-cq)f$ . The distribution $F$ is regular if the virtual valuation $\theta-(1-F(\theta))/f(\theta)$ is increasing.

Formalization targets

Goal: Proposition 2.5, a posted price is optimal

If $p^*\in\arg\max_{p\in[\underline\theta,\bar\theta]}p(1-F(p))$ , then the mechanism

q(\theta)=\begin{cases}1&\theta>p^*\\0&\theta<p^*\end{cases},\qquad t(\theta)=\begin{cases}p^*&\theta>p^*\\0&\theta<p^*\end{cases}

maximizes expected revenue among all incentive-compatible, individually rational direct mechanisms. The comparison class contains every randomized rule $q$ with values in $[0,1]$ ; the statement fixes no distribution and no constant.

Milestones on the way

Proposition 2.1: every mechanism and optimal buyer strategy can be replaced by a truthful direct mechanism with the same outcomes.
Lemmas 2.1–2.4: incentive compatibility forces $q$ increasing, $u$ increasing and convex with $u'=q$ , and

u(\theta)=u(\underline\theta)+\int_{\underline\theta}^{\theta}q(x)\,dx,\qquad t(\theta)=t(\underline\theta)+\big(\theta q(\theta)-\underline\theta q(\underline\theta)\big)-\int_{\underline\theta}^{\theta}q(x)\,dx.

Propositions 2.2–2.3 and Lemma 2.5: these conditions characterize incentive compatibility; individual rationality reduces to $u(\underline\theta)\ge0$ ; at the optimum $t(\underline\theta)=\underline\theta q(\underline\theta)$ .
Lemma 2.6, Proposition 2.4, Lemma 2.7: $M$ is compact and convex, a linear function continuous on a compact convex set attains its maximum at an extreme point, and the extreme points of $M$ are the $\{0,1\}$ -valued functions.
Proposition 2.6: under regularity, $q(\theta)=0$ when $\nu'(0)\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)\le c$ , otherwise $\nu'(q(\theta))\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)=c$ , with $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$ , maximizes expected profit.

Significance

Proposition 2.5 says that the elementary monopoly price is not a restriction of the seller's options but the solution of the unrestricted design problem, including every lottery and every indirect procedure. Its one-buyer argument is the template for Myerson's optimal auction (Chapter 3 of the book), whose revenue formula is the multi-buyer form of Lemma 2.4. Proposition 2.6 exhibits the two standard features of screening, no distortion at the top and downward distortion below, which recur in regulation, insurance and contract theory.

All results of the chapter are classical and proved in the book. None of them is formalized on Prove2Me, and Mathlib has neither the revelation principle, the envelope lemma for incentive-compatible mechanisms, nor a maximum principle for linear functions on compact convex sets (Mathlib has the Krein–Milman lemma, IsCompact.extremePoints_nonempty, but not Bauer's maximum principle). The mission therefore produces the first machine-checked foundation for the one-agent screening model on which chapters 3, 4 and 11 of the book build.

Difficulty

The obvious argument for the goal compares the posted price with other posted prices; that comparison is one line and is not the theorem. The content is the comparison with randomized mechanisms: an arbitrary increasing $q$ with values in $[0,1]$ may do better than every deterministic threshold rule unless one shows that expected revenue is linear in $q$ and that its maximum over the infinite-dimensional set $M$ is attained at an extreme point. That step needs compactness of $M$ in $L^1$ and a maximum principle on compact convex sets in a normed space, neither of which is finite-dimensional linear programming. The envelope step (Lemma 2.3) needs absolute continuity of a convex function on a closed interval, including its endpoints, where $u$ need not be differentiable. For Proposition 2.6 the pointwise maximizer of the virtual surplus must be shown to be monotone and to satisfy incentive compatibility, which is where regularity enters.

Formalization scope

Types are real numbers; every function of the type is a total function $\mathbb R\to\mathbb R$ and every condition quantifies over $[\underline\theta,\bar\theta]$ only. "Increasing" means weakly increasing (the book's note 3). The distribution is a structure carrying the density $f$ , positive and integrable on $[\underline\theta,\bar\theta]$ with total mass $1$ , and $F$ tied to it by $F(\theta)=\int_{\underline\theta}^{\theta}f$ . No measurability or integrability hypothesis is placed on mechanisms: incentive compatibility makes $q$ monotone and $t$ bounded and measurable, so every expected revenue is a genuine integral.

The explicit formulas are part of the statements: the posted-price mechanism of Proposition 2.5 with $p^*\in\arg\max p(1-F(p))$ ; the payment formulas of Lemmas 2.3–2.4 and Proposition 2.2; $t(\underline\theta)=\underline\theta q(\underline\theta)$ in Lemma 2.5; and in Proposition 2.6 the two-case rule for $q$ and the payment $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$ . The goal fixes $q(p^*)=1$ , $t(p^*)=p^*$ for existence and quantifies over every incentive-compatible, individually rational completion at the tie.

The space $\mathcal F$ is $L^1([\underline\theta,\bar\theta])$ of almost-everywhere classes, because the book's $L^1$ "norm" on bounded functions vanishes on null functions; $M$ is the set of classes with an increasing $[0,1]$ -valued representative, and Lemma 2.7 is an almost-everywhere statement, as the book's notes 4–6 already indicate. Proposition 2.4 is stated for a nonempty compact convex set in a real normed space and a linear map continuous on that set. The revelation principle models a general mechanism as the buyer's reduced strategy set, an arbitrary type, with a purchase probability and an expected payment for each strategy.

A goal that compared the posted price only with other posted prices, or only with deterministic mechanisms, would be trivial and is excluded: the competitors range over all incentive-compatible, individually rational direct mechanisms with $q$ valued in $[0,1]$ .

Reusable beyond this mission: the one-agent envelope and revenue-equivalence lemmas (needed again in Chapters 3, 4 and 11), compactness of monotone functions in $L^1$ , and the maximum principle for linear functions on compact convex sets. Contributions to any of these are welcome.

Selected references

T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. doi:10.1093/acprof:oso/9780199734023.001.0001
M. Mussa and S. Rosen, "Monopoly and product quality", Journal of Economic Theory 18(2), 1978. doi:10.1016/0022-0531(78)90085-6
E. A. Ok, Real Analysis with Economic Applications, Princeton University Press, 2007 (Extreme Point Theorem, p.658), cited by the book at p.16.

16 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Linear algebra+2·Captain: mikedeng1

Bellman's Dynamic Programming IX: Markovian Decision Processes and the Maximal Perron RootTextbook

Motivation

Chapter XI of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; DOI 10.2307/j.ctv1nxcw0f) studies decision processes whose state is a vector of nonnegative quantities, for example the probabilities that a system is in each of $N$ states, or the stocks of $N$ commodities, and whose transitions are linear maps chosen stage by stage by a controller. Maximizing a linear functional of the state at every stage leads to the nonlinear difference equation

x_i(n+1) = \max_q \sum_{j=1}^N a_{ij}(q)\, x_j(n), \qquad x_i(0) = c_i,

and, in the limit of small time steps, to differential equations of the form $dx/dt = \max_q [A(q,t)x + b(q,t)]$ and, when two opposing controllers act, $dx/dt = \max_p \min_q[\dots]$ .

These equations are the multiplicative counterpart of the additive Bellman equation. Their growth rate is the natural object for controlled population models, controlled Markov chains observed through their unnormalized state vectors, and economic growth models with a choice of technology. Bellman announced the discrete results in "A Markovian decision process" (J. Math. Mech. 6, 1957) the same year as the book, and R. A. Howard's Dynamic Programming and Markov Processes (MIT Press, 1960) developed policy iteration for the related average-reward problem. The central discrete result of the chapter, Theorem 2, is an early instance of what is now called nonlinear Perron–Frobenius theory (Lemmens and Nussbaum, 2012).

Setting

Fix $N \ge 1$ . Row $i$ of the matrix carries its own control $q_i$ , ranging over a set $S_i$ ; the joint control is $q = (q_1, \dots, q_N)$ in $S = S_1 \times \dots \times S_N$ , and $A(q) = (a_{ij}(q_i))$ . Bellman insists on this row-wise structure (§ 3): "the set of q's for each row is distinct from the corresponding set for any other row ... so that there is no interaction between the various maximizations". The maximum of a vector over $q$ is then taken row by row.

The Perron root $\varphi(q)$ is the characteristic root of $A(q)$ of largest absolute value, the spectral radius of $A(q)$ as a complex matrix. The conditions (10.3) of the chapter are:

for every $y$ and every row the maximum of $\sum_j a_{ij}(q_i) y_j$ over $S_i$ is attained;
$0 < a_{ij}(q) \le m < \infty$ on $S$ ;
$\varphi$ attains its maximum on $S$ .

For the continuous processes, $\|x\| = \sum_i |x_i|$ and $\|A\| = \sum_{i,j}|a_{ij}|$ , and a solution of $dx/dt = F(t,x)$ , $x(0)=c$ , on $[0,T]$ is a continuous $x$ with $x(t) = c + \int_0^t F(s, x(s))\,ds$ , which is the book's "satisfying the equation almost everywhere". The successive approximations are $x_0 = c$ , $x_{n+1}(t) = c + \int_0^t F(s, x_n(s))\,ds$ .

Formalization targets

Goal: Chapter XI, Theorem 2

Under (10.3) there is exactly one $\lambda > 0$ for which

\lambda y_i = \max_q \sum_{j=1}^N a_{ij}(q)\, y_j, \qquad i = 1,\dots,N,

has a solution with all $y_i > 0$ . That solution is unique up to a positive factor, and

\lambda = \max_{q \in S} \varphi(q).

Milestones

§ 4, Lemma. For row-wise maximized operators $T_1(x) = \max_q[b_1(q,t) + \int_0^t A(q,s)x\,ds]$ and $T_2(y)$ likewise, $\|T_1(x) - T_2(y)\| \le \max_q[\|b_1 - b_2\| + \int_0^t \|A(q,s)\|\,\|x-y\|\,ds]$ .
Theorem 1. If $\|A(q,t)\|, \|b(q,t)\| \le f(t)$ with $f$ locally integrable and the maximum is attained, then $dx/dt = \max_q[A(q,t)x + b(q,t)]$ , $x(0) = c$ , has a unique solution, the uniform limit of the successive approximations.
Theorem 3 (corrected). If moreover $\varphi$ has a unique maximizer on $S$ and $c \ge 0$ , $c \ne 0$ , then the recurrence satisfies $x_i(n) \sim a\,y_i\,\lambda^n$ with $a = a(c) > 0$ .
Theorem 4. The same well-posedness for $dx/dt = \max_p\min_q[A(p,q,t)x + b(p,q,t)] = \min_q\max_p[\dots]$ on $[0,T]$ .
Theorem 5. If $(Bp,q) \ge d > 0$ on probability vectors, the solution of $du/dt = \max_p\min_q[(Ap,q) - (Bp,q)u]$ satisfies

\lim_{t\to\infty} u(t) = \max_p \min_q \frac{(Ap,q)}{(Bp,q)} = \min_q \max_p \frac{(Ap,q)}{(Bp,q)} .

Significance

Theorem 2 identifies the optimal long-run growth rate of a controlled multiplicative process with the largest Perron root among the admissible matrices, and shows that the optimal process has a single positive stationary direction. Theorem 3 turns this into the asymptotics of the value iteration $x(n+1) = \max_q A(q)x(n)$ : after normalization by $\lambda^n$ the iterates converge to a multiple of the eigenvector. Theorems 1 and 4 are the existence and uniqueness results that justify defining continuous-time controlled processes and differential games by these equations. Theorem 5 recovers the min-max theorem for ratios of bilinear forms (Chapter X) as the long-run limit of a scalar differential game.

The results are classical, and none of them is formalized. Mathlib has the spectral radius and irreducible matrices but no Perron–Frobenius theorem and no Brouwer fixed point theorem; the platform has a statement of the Perron theorem for a single positive matrix (ClassicalGaps.perron_positive_matrix). A formal proof of the goal therefore also produces a reusable monotone, positively homogeneous eigenvector theorem on the positive orthant.

Difficulty

The map $y \mapsto \max_q A(q)y$ is not linear, so the linear-algebra proof of the Perron theorem through the characteristic polynomial does not apply. Existence of a positive eigenvector needs a fixed point argument for a nonlinear map of the simplex (Bellman uses Brouwer's theorem). The identification $\lambda = \max_q \varphi(q)$ must connect the nonlinear eigenvalue with the spectra of the individual matrices, which requires the Perron theory of each $A(q)$ , including the fact that the Perron root dominates every complex eigenvalue in modulus. For Theorem 3, the iterates may switch controls infinitely often when $S$ is infinite, so an argument that the optimal control is eventually constant does not settle convergence. For Theorems 1 and 4, the right-hand side is only measurable in $t$ and Lipschitz in $x$ with an integrable constant, so the classical Picard–Lindelöf theorem with a continuous right-hand side does not apply directly.

Formalization scope

Everything lives in the namespace BellmanDP.Markovian. Vectors are Fin N → ℝ and matrices are Matrix (Fin N) (Fin N) ℝ. Row $i$ 's control type is Q i with admissible set S i, and the joint admissible set is Set.pi Set.univ S. The Perron root is (spectralRadius ℂ (A.map (algebraMap ℝ ℂ))).toReal, the largest modulus of a complex eigenvalue; it is not defined as a positive eigenvalue with a positive eigenvector, which would make the Perron–Frobenius content of the goal definitional. The maximized eigen-equation is stated with IsGreatest, so the maxima are attained. The goal and Theorem 3 assume $N \ge 1$ ; for $N = 0$ every $\lambda$ would qualify.

Conventions and repairs:

Theorem 3 prints "a unique q for which the maximum value of q is assumed". A control has no maximum value; the proof uses " $q^*$ ... the value of $q$ for which $\lambda = \varphi(q^*)$ ", so the hypothesis is uniqueness of the maximizer of $\varphi$ . For $c = 0$ the iterates vanish and $x_i(n) \sim a y_i\lambda^n$ fails, so $c \ne 0$ is assumed (the proof takes $c > 0$ "without loss of generality"). The asymptotic is stated as $x_i(n)/\lambda^n \to a y_i$ with $a > 0$ .
Theorems 1 and 4: the book's controls are functions of $t$ with the maximum outside the integral; since the maximization is pointwise (§ 4), the statements use pointwise sets and the integral of the pointwise maximum. Measurability of $t \mapsto F(t,x)$ is not stated in the book and is assumed. In Theorem 4 the max-min is taken row by row, and (2a) is encoded as the existence of a saddle point in each row.
§ 4 Lemma: " $\le \max_q[\dots]$ " is stated as " $\le [\dots]$ at some admissible joint $q$ ".
Theorem 5: the right-hand side is the max-min form; the equality of the two ratio values is part of the conclusion.

Degenerate readings are ruled out: the maxima are attained or taken over nonempty compact sets, never Lean's junk sSup of an unbounded set, and the Perron root is spectral rather than defined through the conclusion. Contributions welcome: a proof of the single-matrix Perron theorem in the form needed here, a Brouwer or Kakutani fixed point theorem for the simplex, and a Carathéodory existence theorem for $dx/dt = F(t,x)$ with an integrable Lipschitz constant, each reusable well beyond this mission.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter XI. https://doi.org/10.2307/j.ctv1nxcw0f
R. Bellman, "A Markovian decision process", Journal of Mathematics and Mechanics 6 (1957), 679–684.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
O. Perron, "Zur Theorie der Matrices", Mathematische Annalen 64 (1907), 248–263. https://doi.org/10.1007/BF01449896
B. Lemmens and R. Nussbaum, Nonlinear Perron–Frobenius Theory, Cambridge University Press, 2012. https://doi.org/10.1017/CBO9781139026079

9 thms2 active usersReviewed

Calculus of Variations Control Theory Dynamic Programming+2·Captain: mikedeng1

Bellman's Dynamic Programming VII: Convergence of Discrete Approximations in the Calculus of VariationsTextbook

Motivation

Chapter IX of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) recasts problems of the calculus of variations with constraints as dynamic programming processes. A variational problem with an inequality constraint on the control, such as $0 \le y \le x$ , is awkward for the classical Euler–Lagrange theory: the optimal control switches between the constraint boundary and the interior, and the number and location of the switches are unknown in advance. Bellman's proposal is to replace the continuous problem by a discrete-time one and to solve that by the recurrence relations of dynamic programming, a procedure he describes as the more reliable computational one "in cases treated to date" (§ 11, p. 260).

That proposal is sound only if the discrete values converge to the continuous value as the time step goes to zero. Chapter IX states one such convergence result, Theorem 2 of § 12, and proves it through an Euler-scheme error estimate. The same chapter works through an example (§§ 10–11) whose discrete version is described by Theorem 1. Both are the subject of this mission. The convergence of time-discretized dynamic programming to the continuous value function has since become a standard topic of numerical optimal control (for example the semi-Lagrangian schemes analysed by Capuzzo-Dolcetta and Falcone), and Bellman's § 12 is an early rigorous instance of it.

Setting

A state $x(t) \ge 0$ evolves on a horizon $[0, T]$ under a control $y(t)$ with $0 \le y \le x$ , a running reward $F(x, y)$ and dynamics

\frac{dx}{dt} = G(x, y), \qquad x(0) = c .

Writing $y = \varphi x$ with a fractional control $0 \le \varphi \le 1$ turns $F$ and $G$ into $\tilde F(x, \varphi) = F(x, \varphi x)$ and $\tilde G(x, \varphi) = G(x, \varphi x)$ (phiForm). The continuous value is

f(c, T) = \sup_{\varphi} \int_0^T \tilde F(x(t), \varphi(t))\, dt,

over measurable $\varphi$ with values in $[0, 1]$ , where $x$ solves $x(t) = c + \int_0^t \tilde G(x(s), \varphi(s))\,ds$ on $[0, T]$ (IsTrajectory, contValue).

For $n = 1, 2, \dots$ the discrete problem uses step $1/n$ and $N = \lfloor Tn \rfloor$ steps (horizonSteps): for $\varphi_0, \dots, \varphi_N \in [0, 1]$ ,

x_0 = c, \quad x_{k+1} = x_k + \frac{\tilde G(x_k, \varphi_k)}{n}, \qquad J_N(\{\varphi_k\}, n) = \sum_{k=0}^{N} \frac{\tilde F(x_k, \varphi_k)}{n},

and $f(c, T, n) = \max J_N$ (eulerTraj, discretePayoff, discreteValue). A discrete control defines the step control $\varphi(t) = \varphi_k$ on $k/n \le t < (k+1)/n$ (stepControl).

The example of §§ 10–11 has a gain function $b$ with $b(0) = 0$ , $b'(0) = \infty$ , $b' > 0$ , $b'(y) \to 0$ as $y \to \infty$ , $b'' < 0$ (IsGainFunction; $b(y) = y^{1/2}$ is one), and value functions (uSeq)

u_0(c) = c, \qquad u_{N+1}(c) = \max_{0 \le v \le c}\,\bigl[c - v + u_N(c + b(v))\bigr].

Formalization targets

Goal: Chapter IX, Theorem 2 (corrected)

Assume (11): (a) $F$ and $G$ have continuous second partial derivatives; (b) $px \le G(x, y) \le qx + r$ for $x > 0$ , $0 \le y \le x$ ; (c) $G_y > 0$ throughout that region, or $G_y < 0$ throughout. Then for all $c \ge 0$ , $T > 0$ , the set of continuous payoffs is nonempty and bounded above, and

\lim_{n \to \infty} f(c, T, n) = f(c, T).

Milestones

Chapter IX, Theorem 1: the structure of $u_N$ . There are $v_N(c)$ and thresholds $c_N$ with $v_N$ decreasing in $c$ , $v_{N+1} > v_N$ , $c_N$ the unique fixed point of $v_N$ with $c_{N+1} > c_N$ , $u_N(c) = u_{N-1}(c + b(c))$ for $c \le c_N$ , $u_N(c) = c - v_N(c) + u_{N-1}(c + b(v_N(c)))$ for $c \ge c_N$ , and $u_N' \ge u_{N-1}'$ .
§ 12, Lemma (corrected): for $G$ Lipschitz on $[m, M] \times [0, 1]$ , the Euler states with a step control are within $\kappa / n$ of the exact solution on $[0, T]$ .
Eq. (12.13): $|J(\varphi) - J_N(\{\varphi_k\}, n)| \le B'/n$ for step controls.
Eq. (12.14): $f(c, T, n) \le f(c, T) + B'/n$ for all $n \ge 1$ .
Eq. (12.17): $f(c, T) \le \liminf_{n \to \infty} f(c, T, n)$ .

Milestones 3–5 are stated for $c > 0$ , as in the book's proof ("Given $c > 0$ and $T > 0$ "); the goal is stated for $c \ge 0$ , as in the theorem.

Significance

Theorem 2 says that the value of a constrained continuous-time control problem can be computed, to any accuracy, by the finite recurrence of dynamic programming on a time grid. Its upper half (12.14) gives a rate: the discrete value never exceeds the continuous one by more than $B'/n$ . The lower half (12.17) needs no rate and holds because measurable controls are approximated by step controls. Theorem 1 is a discrete counterpart of the transition curve computed in § 10: below the threshold $c_N$ the whole state is invested, above it an interior amount, and the thresholds increase with the number of remaining stages.

As far as the mission's author could establish, none of these results has a machine-checked proof. The Euler error estimate is classical and has a Gronwall-type proof; Mathlib contains Gronwall's inequality (Analysis/ODE/Gronwall) and Picard–Lindelöf for continuous right-hand sides, but no convergence theory for the value of discretized control problems. The book leaves the proof of Theorem 1 to the reader.

Difficulty

The upper bound (12.14) follows from the Lemma once the continuous and the discrete trajectories are known to stay in a common bounded strip $m \le x \le M$ ; that uniform bound is what assumption (11b) provides and must be established first. The lower bound is where the obvious argument fails: an arbitrary measurable control is not a step control on the grid $k/n$ , and passing to a step control changes the trajectory, so the payoff must be shown continuous under almost-everywhere convergence of controls. This uses the trajectory's dependence on the control in $L^1$ , not only on the initial value. Solutions exist in the Carathéodory sense only, so the integral form of the equation is required. For Theorem 1 the induction must carry concavity of $u_N$ and a strict comparison of marginal values across $N$ , and $u_N$ is not differentiable at $c = 0$ , where $b'(0) = \infty$ .

Formalization scope

States, controls and rewards are real; $F, G, b : \mathbb R \to \mathbb R$ (or $\mathbb R \to \mathbb R \to \mathbb R$ ), with the hypotheses imposed where the book imposes them. The conventions:

Misprint in (12.5). The print sets $N = [T/n]$ while using the step $1/n$ in (12.6) and the intervals $k/n \le t < (k+1)/n$ in the Lemma. Under the literal reading the discrete horizon $N/n$ tends to $0$ and Theorem 2 is false: for $F \equiv 1$ , $G(x, y) = y$ (which satisfies (11) with $p = 0$ , $q = 1$ , $r = 0$ , $G_y = 1$ ) and $T = 1$ , $f(c, 1) = 1$ but $f(c, 1, n) = 1/n$ for $n \ge 2$ . The mission uses $N = \lfloor Tn \rfloor$ and keeps the book's sum $\sum_{k=0}^{N}$ ; the range " $k = 0, \dots, n - 1$ " in (12.6) is read as $k = 0, \dots, N - 1$ .
Lemma. Its range " $0 \le t \le N$ " is read as $0 \le t \le T$ . The bounds $m \le x \le M$ are required of the solution $x(t)$ as well as of the sequence $x_k$ , since a Lipschitz condition on the strip says nothing about $G$ outside it; the proof of Theorem 2 supplies both bounds. The constant may depend on $m$ , $M$ and the Lipschitz constant.
Assumptions (11) are on the original $F(x, y)$ , $G(x, y)$ , with (11a) read as $C^2$ on $\mathbb R^2$ ; the problem is posed through $y = \varphi x$ .
"Max" over measurable controls is a supremum (the proof picks $\varepsilon$ -optimal controls). The goal asserts that the set of payoffs is nonempty and bounded above, so the Lean supremum cannot take its default value $0$ . Trajectories satisfy the integral equation with integrable right-hand side, and the reward is required integrable, so the Bochner integral's default $0$ cannot enter either.
Theorem 1. (5a) is read as non-strict monotonicity: for $N = 1$ the interior optimum solves $b'(v) = 1$ and is constant in $c$ . $v_N(c) \ge 0$ is required for $c \ge c_N$ , so that $v_N(c)$ is a feasible choice. (5f) presupposes differentiability and is stated where both derivatives exist.

A trivializing formalization is ruled out: the discrete and continuous values are defined from $F$ and $G$ by the book's recursions and integrals, not assumed as hypotheses, and the corrected step count is not a free parameter.

Needed infrastructure: Carathéodory existence and uniqueness for Lipschitz right-hand sides with measurable controls, Gronwall estimates for the Euler scheme, and approximation of measurable controls by step functions. All three are reusable beyond this mission, and contributions of any of them are welcome.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter IX, §§ 10–12, pp. 256–263. DOI 10.2307/j.ctv1nxcw0f
I. Capuzzo-Dolcetta, On a discrete approximation of the Hamilton–Jacobi equation of dynamic programming, Applied Mathematics and Optimization 10 (1983) 367–377. DOI 10.1007/BF01448394
M. Bardi and I. Capuzzo-Dolcetta, Optimal Control and Viscosity Solutions of Hamilton–Jacobi–Bellman Equations, Birkhäuser, 1997. DOI 10.1007/978-0-8176-4755-1

8 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Optimization+1·Captain: mikedeng1

Bellman's Dynamic Programming VI: Optimal Policies for the Continuous Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.

It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.

Setting

Mine A holds $x_0 \ge 0$ units of gold and mine B holds $y_0 \ge 0$ . At time $t$ a proportion $\varphi_1(t) \in [0,1]$ of the machine's effort goes to A and $\varphi_2(t) = 1 - \varphi_1(t)$ to B (Eq. (7.3)). With $x(t), y(t)$ the gold remaining, $p(t)$ the probability that the machine still works and $f(t)$ the expected gold mined, the process is defined by Eq. (7.2):

\frac{dx}{dt} = -\varphi_1 r_1 x,\qquad \frac{dy}{dt} = -\varphi_2 r_2 y,\qquad \frac{dp}{dt} = -p\,(\varphi_1 q_1 + \varphi_2 q_2),\qquad \frac{df}{dt} = p\,(\varphi_1 r_1 x + \varphi_2 r_2 y),

with $x(0) = x_0$ , $y(0) = y_0$ , $p(0) = 1$ , $f(0) = 0$ . The mining rates $r_1, r_2$ and the failure rates $q_1, q_2$ are positive. The objective is the expected total gold $f(\infty) = \int_0^\infty f'(t)\,dt$ .

In the three-choice problem (§ 12) a third decision $C$ removes gold from A at rate $r_3$ and from B at rate $r_4$ , and fails at rate $q_3$ . A control is a triple $\varphi_1, \varphi_2, \varphi_3 \ge 0$ with $\varphi_1 + \varphi_2 + \varphi_3 = 1$ (Eq. (12.2)). For a horizon $T$ , the switching functions $K_1, K_2, K_3$ of Eq. (12.5) are computed along a control. For instance,

K_1(t) = -q_1\int_t^T f'(s)\,ds + r_1\,p(T)\,x(T) - r_1\int_t^T p'(s)\,x(s)\,ds.

They measure the first-order gain from shifting effort towards each decision at time $t$ . The linear forms

C_1 = q_1 r_2 y - q_2 r_1 x,\qquad C_2 = q_1 r_4 y - (q_3 r_1 - q_1 r_3)x,\qquad C_3 = (q_3 r_2 - q_2 r_4) y - q_2 r_3 x

and the quantity $D = q_1 r_2 r_3 + q_2 r_1 r_4 - q_3 r_1 r_2$ (Eqs. (13.2)–(13.3)) organize the analysis.

Formalization targets

Goal: Chapter VIII, Theorem 1

For the two-choice process, the maximum of $f(\infty)$ is attained by the policy

\varphi_1 = 1 \text{ for } q_1 r_2 y < q_2 r_1 x,\qquad \varphi_2 = 1 \text{ for } q_1 r_2 y > q_2 r_1 x,\qquad \varphi_1 = \tfrac{r_2}{r_1+r_2},\ \varphi_2 = \tfrac{r_1}{r_1+r_2} \text{ for } q_1 r_2 y = q_2 r_1 x.

The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes $f(\infty)$ over all measurable controls with values in $[0,1]$ .

Milestones

Eq. (10.1): $f_A(\infty) = r_1 x_0/(q_1 + r_1)$ and $f_B(\infty) = r_2 y_0/(q_2 + r_2)$ for the pure policies.
Lemmas 1–3 (§ 13): for a control that maximizes $f(T)$ , almost everywhere, $K_i > K_j$ forces $\varphi_i = 1$ or $\varphi_j = 0$ ; a strictly largest $K_i$ forces $\varphi_i = 1$ ; a strictly beaten $K_i$ forces $\varphi_i = 0$ .
Lemma 4 (§ 14): if $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant and $D \ne 0$ , no optimal control mixes $A$ , $B$ and $C$ on an interval.
Lemma 5 (§ 14): a mixture of exactly two decisions on an interval keeps the state on $C_1 = 0$ , $C_2 = 0$ or $C_3 = 0$ respectively, with the proportions that hold $y/x$ fixed.
§ 15, Eq. (1) (corrected): $f_C(\infty) = r_3 x_0/(q_3 + r_3) + r_4 y_0/(q_3 + r_4)$ .
"Theorem 8" (§ 16, the chapter's third theorem): if $D < 0$ (with $r_3 > r_4$ and $x_0, y_0 > 0$ ), the three-choice problem is solved by the two-choice rule of Theorem 1, and every optimal control has $\varphi_3 = 0$ almost everywhere.

Significance

Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope $y/x$ , and on the line $q_1 r_2 y = q_2 r_1 x$ it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: $D < 0$ means that $C$ removes gold at a higher failure cost than an equivalent mixture of $A$ and $B$ .

On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.

Difficulty

The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and $B$ is preferred near the $y$ -axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let $\varphi$ be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into " $C_k = 0$ on the interval".

Formalization scope

Process by closed forms. No differential equations are formalized. With $\Phi_i(t) = \int_0^t \varphi_i$ , the definitions are $x = x_0 e^{-r_1\Phi_1 - r_3\Phi_3}$ , $y = y_0 e^{-r_2\Phi_2 - r_4\Phi_3}$ , $p = e^{-\sum_i q_i\Phi_i}$ , $f(T) = \int_0^T f'$ . These are the unique absolutely continuous solutions of (7.2) and (12.1). The two-choice process is the three-choice one with $\varphi_3 = 0$ .
Controls are open-loop and measurable, with $\varphi_i \ge 0$ and $\sum_i \varphi_i = 1$ . Decisions are indexed 0, 1, 2 for $A, B, C$ .
$f(\infty)$ is a lower Lebesgue integral with values in $[0,\infty]$ . It has no junk value, and optimality is compared in $[0,\infty]$ .
Theorem 1's feedback rule is encoded as a predicate on open-loop controls: the rule holds along the control's own trajectory for almost every $t \ge 0$ . The goal also asserts that such a control exists, which rules out the trivializing reading in which no control satisfies the rule and the optimality claim is vacuous.
Horizon of Lemmas 1–5. § 12 considers only $T = \infty$ , but the variation (12.4) and the switching functions (12.5) are written for a general $T$ . Each lemma is formalized for both: every finite horizon $T$ , with $K_i$ built from that horizon, and $T = \infty$ , with $K_i$ given by (12.5) at $T = \infty$ (boundary term $0$ ).
Implicit ranges. All rates $q_1, q_2, q_3, r_1, \dots, r_4$ are taken positive, and $x_0, y_0 \ge 0$ . Lemmas 4–5 and "Theorem 8" take $x_0, y_0 > 0$ , the open quadrant the book analyses. Lemma 4 carries the book's assumption that $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant ( $q_1 r_3 < q_3 r_1$ , $q_2 r_4 < q_3 r_2$ ). "Theorem 8" carries the standing assumption $r_3 > r_4$ of § 15.
Misprint corrected. The value of the pure $C$ -policy in the proof of Lemma 6 (§ 15, Eq. (1), p. 237) is printed $r_3 x_0/(q_2 + r_3) + r_4 y_0/(q_3 + r_4)$ . The first denominator must be $q_3 + r_3$ : for $x_0 = 1$ , $y_0 = 0$ , $q_2 = 1$ , $q_3 = 2$ , $r_3 = 1$ the process yields $1/3$ , not $1/2$ . The corrected identity is stated.
Numbering. The third theorem of the chapter is printed "Theorem 8" and is cited that way.
Left out. Theorem 2 ( $D > 0$ ) specifies its solution only through Fig. 7 and an unspecified line $L$ . Lemmas 6–8, 11 and the two Lemmas 12 describe regions of figures. The finite-horizon analysis of § 11 has no numbered result, and neither does the nonlinear utility of § 18.

Useful infrastructure: the derivative formulas (13.1) for the $K_i$ , a first-variation lemma for $f(T)$ under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter VIII, pp. 222–244. https://doi.org/10.2307/j.ctv1nxcw0f
L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Bellman's Dynamic Programming V: Optimality of a Constant Stock Level for the Optimal Inventory EquationTextbook

Motivation

The optimal inventory problem asks how much of an item to stock when demand is random, ordering costs money, and running short costs more. Arrow, Harris and Marschak formulated it as a sequential decision problem in 1951 (Optimal inventory policy, Econometrica 19), and Dvoretzky, Kiefer and Wolfowitz studied its structure in 1952–53. Chapter V of Richard Bellman's Dynamic Programming (1957) treats the problem through a single functional equation for the minimal expected discounted cost. It shows that when ordering and shortage costs are proportional to quantity, the optimal policy is described by one number, a constant stock level $\bar x$ , computed from the demand distribution alone.

This result is an early form of the base-stock (order-up-to) policy. Base-stock policies are the standard structure in periodic-review inventory theory: Karlin (1958), Scarf's $(s,S)$ theorem (1960) and Veinott (1965) extend it. Chapter V is also a worked example of a point the book makes throughout: the method of successive approximations determines the shape of an optimal policy, and not only its existence.

Setting

A single item is stocked over an unbounded sequence of periods. At the start of a period the stock is $x \ge 0$ . The decision maker orders up to a level $y \ge x$ , at cost $k(y-x)$ with $k > 0$ . A demand $s \ge 0$ then arrives, with probability density $\varphi$ : $\varphi(s) > 0$ for $s > 0$ , $\int_0^\infty \varphi(s)\,ds = 1$ , and $\int_0^\infty s\,\varphi(s)\,ds < \infty$ . If $s \le y$ , the next period starts with stock $y - s$ . If $s > y$ , the excess $s - y$ is bought at the penalty rate $p > 0$ and the next period starts with stock $0$ . Costs one period ahead are multiplied by a discount factor $0 < a < 1$ .

Write $f(x)$ for the minimal expected discounted cost from stock $x$ . Enumerating the cases gives Bellman's equation (5.1):

f(x) = \min_{y \ge x} T(y,x,f),

T(y,x,f) = k(y-x) + a\Big[\int_y^\infty p(s-y)\varphi(s)\,ds + f(0)\int_y^\infty \varphi(s)\,ds + \int_0^y f(y-s)\varphi(s)\,ds\Big].

A policy assigns an order-up-to level $y(x) \ge x$ to each stock $x$ . It is optimal when $y(x)$ attains the minimum. The mission takes the equation itself as the model; no stochastic process is built.

Formalization targets

Goal: Chapter V, Theorem 1 (with (4b) corrected)

The equation has exactly one solution $f$ among measurable functions bounded on $[0,\infty)$ . If $ap > k$ , the equation

k = ap\int_{\bar x}^\infty \varphi(s)\,ds + ak\int_0^{\bar x}\varphi(s)\,ds

has exactly one root $\bar x \ge 0$ , and for every $x \ge 0$ the minimum is attained at

y(x) = \max(x, \bar x).

If $ap \le k$ , the minimum is attained at $y(x) = x$ : never order.

Milestones

Chapter IV, Theorem 6 (proportional costs): existence and uniqueness of a solution bounded on every finite interval, its continuity, and convergence of $f_{n+1}(x) = \min_{y\ge x} T(y,x,f_n)$ from any non-negative continuous $f_0$ .
Eq. (5.8): $\bar x$ is the unique root of $\int_0^{y}\varphi(s)\,ds = (ap-k)/a(p-k)$ .
Appendix, Theorem 9: the renewal equation $u(x) = f(x) + \int_0^x u(x-s)\varphi(s)\,ds$ with $\int_0^\infty|\varphi| < 1$ has a unique locally bounded solution. The solution is the limit of successive approximations, satisfies a derivative identity, and is non-negative when $f, \varphi \ge 0$ .
Theorem 3: in the undiscounted $n$ -stage process with $p > k$ , the optimal policy at each horizon is a constant stock level $\bar x_n$ , and $\bar x_n$ increases with $n$ .
Theorem 4: with a fixed stock-out charge $q$ added to the penalty, the constant-stock-level policy is still optimal when the last minimum of

\psi(y) = ky + a\Big[\int_y^\infty [p(s-y)+q]\varphi(s)\,ds - k\int_0^y (y-s)\varphi(s)\,ds\Big]

is its absolute minimum.

Significance

The theorem reduces an infinite-horizon stochastic control problem to a scalar equation. Rewriting it as $\int_0^{\bar x}\varphi = (ap-k)/a(p-k)$ gives the critical-fractile form familiar from the newsvendor problem, with the discount factor entering the fractile. The level depends on the demand law only through its distribution function, and the policy does not depend on the current stock except through $\max(x,\bar x)$ . This is what makes the policy implementable and its parameters estimable from data, the point Bellman makes in § 1. Theorem 3 shows the same structure over a finite horizon, with levels that rise as more periods remain. Theorem 4 marks where the structure starts to depend on the demand density.

As far as a search of the platform shows (queries recorded in the mission files), none of these results has a machine-checked proof. Base-stock theorems on the platform, Veinott's multi-product theorem and Gallego–Özer's advance-demand model, use discrete periods, different excess-demand conventions and different state spaces. They do not cover a continuous-demand, lost-sales-at-penalty, discounted functional equation. Formalizing Chapter V would produce an explicit solution of a nonlinear integral equation of renewal type, a uniqueness theorem for that equation, and a Lean treatment of the renewal equation that other applied-probability missions can reuse.

Difficulty

Two steps resist the obvious argument. First, the minimization is over the unbounded set $y \ge x$ , and the unknown $f$ enters through a convolution with $\varphi$ . The operator $f \mapsto \min_{y\ge x}T(y,x,f)$ is a contraction on bounded functions, which settles uniqueness in the bounded class. Uniqueness among functions bounded only on finite intervals (Chapter IV's class) is not a contraction statement, because the minimization reaches arbitrarily far to the right. Second, optimality of $\max(x,\bar x)$ for $x > \bar x$ requires $f(y) + ky$ to be nondecreasing on $[\bar x,\infty)$ . There $f$ is defined only implicitly, as the solution of a renewal-type equation, and this monotonicity is a positivity statement about that solution, not a consequence of the first-order condition. Checking that the first-order condition holds at $\bar x$ is not enough, and neither is checking that the candidate function satisfies the equation at the single level $\bar x$ .

Formalization scope

Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter. Integrals over $(y,\infty)$ are Lebesgue integrals and $\int_0^y$ are interval integrals. The equation is stated with an infimum (IsGLB), as Chapter IV writes it, and every policy statement asserts that the minimum is attained (IsLeast) at the stated level. Uniqueness is asserted on $[0,\infty)$ (Set.EqOn … (Set.Ici 0)). Solution classes require measurability. This is the standing convention that makes $\int_0^y f(y-s)\varphi(s)\,ds$ meaningful; without it a non-measurable function would make the integral default to $0$ . " $\varphi(s) > 0$ " is read as positivity on $(0,\infty)$ .

Conventions and corrections, each stated in the items:

Theorem 1, (4b) is printed "for $x \ge \bar x$ , $y = \bar x$ ". Read literally, a stock $x > \bar x$ would be "ordered down" to $\bar x < x$ , which violates $y \ge x$ . The proof (p. 163, "the minimum occurs at $y = x$ ") and Theorem 4's (7) give $y = x$ , which is what the goal states. The printed text reads: "(4) a. for 0 ≤ x ≤ x̄, y = x̄, b. for x ≥ x̄, y = x̄."
The goal's uniqueness class is "uniformly bounded functions over $x \ge 0$ " (p. 164). Chapter IV, Theorem 6 is stated in its own larger class.
Theorem 4 gives no range for $q$ ; $q \ge 0$ is assumed. Its phrase "the last minimum of $\psi$ is the absolute minimum" is read as: $\bar x$ minimizes $\psi$ on $[0,\infty)$ and $\psi$ is nondecreasing on $[\bar x,\infty)$ . The bracket of (6), unbalanced in print, is closed at the end.
Theorem 3 assumes " $p > k$ "; $k > 0$ and the density conditions of Theorem 1 are carried over.
Theorem 9's derivative clause assumes $f$ continuously differentiable, where the book says "differentiable". The derivative identity is asserted for $x > 0$ .

A trivializing formalization is ruled out. The goal does not assume the stated policy is optimal, does not assume $f$ is given, and does not take $\bar x$ as a hypothesis. It asserts the existence of the root, the existence and uniqueness of the solution, and attainment of the minimum at $\max(x,\bar x)$ for every $x \ge 0$ .

Theorems 2 (two items, joint density), 5 (one-period delivery lag) and 6 (strictly convex ordering cost) are not part of this mission. Theorem 2 is printed with a sign error in (6) and garbled marginals. Theorem 5 states no hypotheses. Theorem 6's (9b) contradicts itself at $x = \bar x$ . Welcome contributions include a Lean library for the renewal equation (existence by successive approximation, positivity, differentiation under the convolution), which Theorem 9 needs and which is independent of inventory theory, and the contraction estimate for $\min_{y\ge x}T(y,x,\cdot)$ on bounded measurable functions.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter V and Chapter IV § 9. https://doi.org/10.2307/j.ctv1nxcw0f
R. Bellman, I. Glicksberg, O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
K. J. Arrow, T. Harris, J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906813
A. Dvoretzky, J. Kiefer, J. Wolfowitz, The inventory problem: I. Case of known distributions of demand, Econometrica 20(2), 1952, 187–222. https://doi.org/10.2307/1907847
A. F. Veinott, Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206

7 thms2 active usersReviewed

Completed

Dynamic Programming Functional Analysis Optimization·Captain: mikedeng1

Bellman's Dynamic Programming IV: Existence and Uniqueness for Functional Equations of Types One, Two and ThreeTextbook

Motivation

A multi-stage decision process is summarized by its optimal return function $f$ , which satisfies a functional equation. In Chapters I and II of Dynamic Programming (Princeton University Press, 1957), Richard Bellman proves existence and uniqueness for particular processes: allocation of resources, gold mining. Chapter IV abstracts these arguments into theorems about whole classes of equations. The same scheme reappears in later chapters (multi-stage games, the calculus of variations) and in every later treatment of dynamic programming.

Two points explain why the chapter is still worth formalizing. First, uniqueness is always claimed within a stated function class, and the choice of class is part of the theorem: an equation of this kind can have many solutions, and only one of them lies in the class that the process singles out. Second, the chapter covers equations that are not contractions in the supremum norm, in particular Type One, where the shrinking happens in the state rather than in the function values.

Setting

Let $D \subseteq \mathbb{R}^N$ carry the Euclidean norm $\|p\|$ , let $S$ be a nonempty set of decisions, and let $g, h : D \times S \to \mathbb{R}$ and $T : D \times S \to D$ . The general equation (1.1) is

f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big].

Here $g$ is the one-stage return, $T(p,q)$ the next state and $h(p,q)$ a multiplier: a discount factor or a survival probability.

An equation is of Type One with constant $0 \le a < 1$ under the following conditions. $D$ contains the null vector $\theta$ . $g$ is bounded on bounded parts of $D$ , uniformly in $q$ , and $g(\theta, q) = 0$ . $|h| \le 1$ . $\|T(p,q)\| \le a\|p\|$ . Finally, with $v(c) = \sup_{\|p\| \le c}\sup_q |g(p,q)|$ , the series $\sum_{n \ge 0} v(a^n c)$ converges for every $c$ .

It is of Type Two under the following conditions. $g$ is bounded on bounded parts of $D$ . On each bounded part, $|h| \le a < 1$ for some $a$ . $T$ maps $D$ into $D$ , and either $\|T(p,q)\| \le \|p\|$ or $D$ is bounded.

The successive approximations are $f_0(p) = \sup_q g(p,q)$ and $f_{n+1}(p) = \sup_q[g(p,q) + h(p,q) f_n(T(p,q))]$ .

The equation of the third type of § 8 lives on the probability simplex $\Delta$ of distributions $p = (p_0, \dots, p_n)$ , with vertices $x_k$ . It reads

f(p) = \min\Big[\,1 + \sum_{k=0}^{n} p_k f(x_k),\ \min_{1 \le l \le M}\big[1 + f(T_l p)\big]\Big] \quad (p \ne x_0), \qquad f(x_0) = 0.

Each $T_l$ maps $\Delta$ into itself, and the $0$ -th coordinate of $T_l p$ is never $1$ . $f(p)$ is the minimal expected time to drive a system into state $0$ with certainty, by observing the state (cost $1$ , then continuing from the observed vertex) or by applying one of the operations $T_l$ (cost $1$ ).

Formalization targets

Goal: Chapter IV, Theorem 1

For a Type One equation there is exactly one solution on $D$ , among functions continuous at $\theta$ and zero there, of

f(p) = \sup_{q \in S}\big[g(p,q) + h(p,q)\,f(T(p,q))\big] \ (p \ne \theta), \qquad f(\theta) = 0.

It is the pointwise limit of the successive approximations from $f_0 = \sup_q g$ , and also from any $f_0$ that is continuous and zero at $\theta$ and bounded on bounded parts of $D$ . If $g$ , $h$ and $T$ are continuous in $p$ on bounded portions of $D$ , uniformly in $q$ , the solution is continuous on every bounded portion of $D$ .

Milestones

Lemma 1 (the fundamental inequality): for nonnegative measures $dG$ ,

|f_2(p) - F_2(p)| \le \sup_q\Big[\,|g - h| + \int_{D} |f_1 - F_1|\,dG\Big].

Theorem 2: a Type Two equation has a unique solution bounded in every finite part of $D$ , obtained by successive approximations and continuous under the same conditions as in Theorem 1.
Theorem 3 (stability, Type One): $\sup_{\|p\| \le c} |F - f| \le \sum_{n \ge 0} u(a^n c)$ , where $u(c) = \sup_{\|p\| \le c}\sup_q |G - g|$ .
Theorem 4 (stability, Type Two, corrected): $\sup_{\|p\| \le c} |F - f| \le u(c)/(1-a)$ .
Lemma 2: two bounded solutions of the third-type equation satisfy $\sup_{p} |f(p) - g(p)| = \max_k |f(x_k) - g(x_k)|$ .
Theorem 5: if $\sum_{k=1}^n (T_l p)_k \le c_1 < 1$ for every $l$ and $p$ , the third-type equation has a unique bounded solution, and it is positive off $x_0$ .

Significance

Theorem 1 guarantees that the optimal return of a process whose decisions shrink the state is well defined and computable by iteration. It applies without assuming that the supremum over decisions is attained and without regularity of the maximizing decision. Theorems 3 and 4 give quantitative continuous dependence of the solution on the reward. This is what justifies approximating a process by a simpler one. Theorem 5 is a uniqueness result for an undiscounted minimum-time problem, where no contraction in the supremum norm is available.

All of these results are classical and proved in the book. None is formalized: the platform's related statements treat finite state spaces with a fixed policy (FoundationsML.ReinforcementLearning.bellman_equations_unique_solution), or Karlin's compact-decision-set setting with nonnegative rewards and an explicit vanishing-tail hypothesis (KarlinDP.Deterministic.unique_solution_of_vanishing_tail), or finite-state stochastic shortest paths (BertsekasDP.ssp_main_theorem). This mission adds machine-checked versions over a continuum of states and an arbitrary decision set, with the function classes stated exactly.

Difficulty

For Type One, the natural idea is to apply the Banach fixed-point theorem in the space of bounded functions. That fails: $|h| \le 1$ allows no contraction in the supremum norm, and the solution need not be bounded on $D$ . Contraction happens only along trajectories, $\|T(p,q)\| \le a\|p\|$ , so every estimate must be localized to balls $\|p\| \le c$ and summed along radii $a^n c$ . Uniqueness then rests on continuity at $\theta$ rather than on a global norm.

The suprema over an arbitrary, possibly infinite, decision set are not attained in general, so no argument may select a maximizing decision. For the third-type equation, neither a contraction nor a shrinking of the state is available: the operations $T_l$ need not move $p$ towards $x_0$ . Uniqueness among bounded solutions requires controlling how long a solution can keep choosing an operation other than observation.

Formalization scope

The state space is EuclideanSpace ℝ (Fin N), $D$ is a Set, the decision set is a nonempty type S, and functions are total, EuclideanSpace ℝ (Fin N) → ℝ. Only their values on $D$ matter, and uniqueness is asserted on $D$ . The equation is encoded with IsLUB, so the supremum is genuine and has no junk value. The successive approximations and the radii $v(c)$ , $u(c)$ use real iSup/sSup, evaluated only where the book's boundedness conditions hold. "Continuous at $\theta$ " is continuity within $D$ .

Conventions and corrections:

In Type One the book writes "for some $a < 1$ ". The formalization takes $0 \le a < 1$ , which loses no generality.
Condition (1a) of both types is read for every radius $c_1$ .
"Continuous in $p$ in any bounded portion of $D$ , uniformly for all $q$ " is read as uniform equicontinuity on each $\{p \in D : \|p\| \le c\}$ . For closed $D$ this is the pointwise reading.
Theorem 4 is printed with " $|F(p) - (p)|$ ", a misprint for $|F(p) - f(p)|$ . As printed, it is also false under the bounded-domain alternative of Type Two. Take $N = 1$ , $D = [-2,2]$ , $T \equiv 2$ , $h \equiv \tfrac12$ , $g \equiv 0$ , and $G = 1$ at $p = 2$ , $G = 0$ elsewhere. Then $|F(0) - f(0)| = 1$ while $u(1)/(1-a) = 0$ . The formal statement adds that $T$ maps $\{p \in D : \|p\| \le c\}$ into the ball of radius $c$ . This holds for every $c$ under the first alternative, where the statement is the book's.
Lemma 1 is stated for nonnegative measures $dG(p,q,\cdot)$ on $\mathbb{R}^N$ , integrated over $D$ . The right-hand supremum may be infinite, so it is expressed through its real upper bounds.
In § 8 the number of states is written both $N+1$ and $n+1$ ; the formalization uses $n+1$ , with $M \ge 1$ transformations indexed by Fin M.

A trivializing formalization would state uniqueness among all solutions of the equation, which is false because constants solve it when $g = 0$ and $h = 1$ . Equally trivializing would be to encode the supremum with a junk-valued sSup, so that unbounded return sets pass for solutions. Both are excluded: the class is part of each statement, and the equation is an IsLUB.

Theorem 6 of the chapter (the optimal inventory equation) is not part of this mission; it is treated in the inventory mission of the series. Welcome contributions include a reusable library for localized successive approximations and the equicontinuity lemmas that the continuity statements need.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010, Chapter IV. https://doi.org/10.2307/j.ctv1nxcw0f
S. Karlin, "The structure of dynamic programming models", Naval Research Logistics Quarterly 2 (1955), 285–294. https://doi.org/10.1002/nav.3800020408
D. P. Bertsekas and J. N. Tsitsiklis, "An analysis of stochastic shortest path problems", Mathematics of Operations Research 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580

10 thms2 active usersReviewed

Completed

Dynamic Programming Optimization Probability·Captain: mikedeng1

Bellman's Dynamic Programming III: Index Rules for the Stochastic Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.

Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.

Setting

Two mines, Anaconda and Bonanza, hold amounts of gold $x \ge 0$ and $y \ge 0$ . A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction $r_1$ of the gold there and stays in working order with probability $p_1$ , or is destroyed without mining anything with probability $1 - p_1$ . Bonanza has the corresponding data $p_2$ and $r_2$ . Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.

The expected return $f(x, y)$ under an optimal policy satisfies the functional equation

f(x,y) = \max\Big[\,A_f(x,y),\; B_f(x,y)\,\Big], \qquad x, y \ge 0, \tag{5.1}

where $A_f(x,y) = p_1\big[r_1x + f((1-r_1)x,\,y)\big]$ is the return of an A-choice followed by optimal continuation and $B_f(x,y) = p_2\big[r_2y + f(x,\,(1-r_2)y)\big]$ that of a B-choice. The $N$ -stage returns are $f_1(x,y) = \max(p_1r_1x,\ p_2r_2y)$ and $f_{N+1} = \max(A_{f_N}, B_{f_N})$ . The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.

In the generalization, a use of mine $i$ has $K$ outcomes: outcome $k$ occurs with probability $p_{ik}$ , yields $c_{ik}x_i$ and leaves $c'_{ik}x_i = (1-c_{ik})x_i$ in the mine, and $1 - \sum_k p_{ik}$ is the probability that the machine is destroyed. With $n$ mines the equation is

f(x_1,\dots,x_n) = \max_i \sum_{k=1}^{K} p_{ik}\big[c_{ik}x_i + f(x_1,\dots,c'_{ik}x_i,\dots,x_n)\big]. \tag{4}

"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle $0 \le x \le \bar X$ , $0 \le y \le \bar Y$ (or every box $0 \le x_i \le \bar X_i$ ), per Bellman's footnote 7.

Formalization targets

Goal: Chapter II, Theorem 4 (the index rule for $n$ mines)

Under $p_{ik} \ge 0$ , $\sum_k p_{ik} < 1$ , $0 \le c_{ik} \le 1$ , $c_{ik} + c'_{ik} = 1$ , equation (4) has a unique solution bounded on boxes, and at every state $x$ any index maximizing

D_i(x) = \frac{\sum_{k} p_{ik}c_{ik}}{1-\sum_{k} p_{ik}}\;x_i

attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.

Milestones

Theorem 1: for $|p_i| < 1$ and $0 \le r_i < 1$ , (5.1) has a unique solution bounded in every rectangle, and it is continuous on the closed quadrant.
Theorem 2: for $0 \le p_i < 1$ , $0 \le r_i \le 1$ , the solution takes the A-branch when $p_1r_1x/(1-p_1) > p_2r_2y/(1-p_2)$ , the B-branch when the reverse inequality holds, and both on equality.
Theorem 3: the same rule for two mines with $K$ outcomes per use.
Theorem 5: for each $N$ , the $N$ -stage process has exactly two decision regions: a sector along the $x$ -axis where A is optimal and a sector along the $y$ -axis where B is optimal, separated by a ray through the origin.
Theorem 6: as $N$ grows, the regions of $f_N$ move monotonically, and from some $N_0$ on they coincide with those of $f$ .
Theorem 7: if $g$ solves (5.1) with an added term $h$ , then $|f - g| \le \max_R|h|/q$ on every rectangle $R$ , where $q = \min(1-p_1, 1-p_2)$ .

Significance

The index rule reduces the choice among $n$ mines to computing $n$ numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the $N$ -stage process is a word in $n$ letters whose number of candidates grows like $n^N$ . The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite $N_0$ , and the stability theorem bounds how much the solution moves when the equation is perturbed.

Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The $n$ -mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.

Difficulty

The equation for the boundary between the regions involves the unknown function $f$ , so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of $f_N$ generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.

Formalization scope

Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with $n \ge 1$ added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's $N$ ). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most $f(x)$ and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for $n$ mines it is BoundedOnBoxes. The $N$ -stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's $f_1$ .

Choices made explicit:

Theorem 1 keeps the book's signed range $|p_i| < 1$ (footnote 2), while Theorems 2, 5, 6 and 7 use the range of § 8 and Theorem 2, $0 \le p_i < 1$ , $0 \le r_i \le 1$ .
The goal asserts existence and uniqueness of the bounded solution of (4) together with the index rule. This is how "the solution" is meant in the book; the extension of Theorem 1 to (4) is not a separate numbered result.
The goal's conclusion is the book's: a maximizer of $D$ is optimal. It does not also assert that the other indices are suboptimal.
Theorem 5's printed statement is only "there are two decision regions". It is formalized as the ray-separation statement its proof establishes, and is titled as the precise reading. Theorem 6's "converge in a monotone fashion" is formalized as monotonicity of the regions as sets, in one of the two directions.
Theorem 7 adds the hypothesis that $h$ is bounded in every rectangle, which is what gives the perturbed equation a solution in the class. $\max_R|h|$ is expressed through any bound $M$ of $|h|$ on $R$ .

A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).

Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.

Selected references

Richard Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter II, pp. 61–80. https://doi.org/10.2307/j.ctv1nxcw0f
Richard Bellman, The theory of dynamic programming, Bulletin of the American Mathematical Society 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society, Series B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

Bellman's Dynamic Programming II: Fibonacci Search for the Maximum of a Unimodal FunctionTextbook

Motivation

Many optimization routines contain an inner step that maximizes a function of one variable whose values are expensive to compute: a line search inside a multivariate method, a tuning parameter chosen by simulation, a stage of a dynamic program in which each evaluation requires solving a subproblem. When the only structural information is that the function has a single peak, the natural question is how to place the evaluations so that the peak is pinned down as tightly as possible with a fixed budget. Richard Bellman's Dynamic Programming (1957) takes up this question in Chapter I, § 22, as an illustration of the functional-equation method, and answers it with the Fibonacci numbers.

Timeline.

1953. J. Kiefer, Sequential minimax search for a maximum (Proc. Amer. Math. Soc. 4, 502–506), proves that Fibonacci search is minimax optimal among sequential procedures for a unimodal function on an interval. doi:10.1090/S0002-9939-1953-0055639-3
1957. Bellman, Dynamic Programming, Chapter I, § 22 (pp. 34–36), recasts the result in the language of the principle of optimality: Theorem 11 for the continuous problem and Theorem 12 for its discrete version.

Setting

Let $L > 0$ . A function $f : [0, L] \to \mathbb R$ is strictly unimodal with maximum at $m \in [0, L]$ if $f$ is strictly increasing on $[0, m]$ and strictly decreasing on $[m, L]$ . No continuity is assumed, and the peak may sit at an endpoint. The point $m$ is then the unique maximizer of $f$ .

A search procedure is a finite decision tree. At each internal node it names a point $x$ at which $f$ is evaluated and moves to a subtree chosen by the observed value $f(x)$ ; at a leaf it announces a closed interval $[a, b]$ . The $k$ -th evaluation point may depend on all values seen so far, but on nothing else about $f$ . The cost of the procedure on $f$ is the number of evaluations along the path that $f$ determines.

The procedure locates the maximum on $[0, L]$ within unit length using at most $n$ values if, for every strictly unimodal $f$ on $[0, L]$ with maximum at $m$ , it evaluates $f$ at most $n$ times and announces $[a, b]$ with $b - a \le 1$ and $m \in [a, b]$ . Write $\mathcal L_n$ for the set of lengths $L > 0$ for which such a procedure exists, and following Bellman's Eq. (22.1),

F_n = \sup \mathcal L_n .

The book's Fibonacci numbers are $F_0 = F_1 = 1$ , $F_n = F_{n-1} + F_{n-2}$ for $n \ge 2$ (in Lean, bookFib).

In the discrete version, $f$ is defined on the points $0, 1, \dots, N-1$ , strictly increasing up to its maximizer $m$ and strictly decreasing after it. $K_n$ is the largest $N$ for which some procedure evaluates at most $n$ values and then names $m$ exactly, for every such $f$ .

Formalization targets

Goal: Chapter I, Theorem 11

\sup \mathcal L_n = F_n \qquad \text{for every } n \ge 0 .

The supremum is not attained once $n \ge 2$ (with two evaluations every length $2 - \varepsilon$ is searchable, the length $2$ is not), which is why the statement is about the supremum rather than a maximum.

Milestones

$\sup \mathcal L_1 = 1$ : one value carries no information (proof of Theorem 11, p. 34).
$\sup \mathcal L_2 = 2$ (p. 35).
Eq. (22.3): for $n \ge 2$ every $L \in \mathcal L_n$ satisfies $L < F_{n-1} + F_{n-2}$ .
For $n \ge 2$ every $0 < L < F_{n-1} + F_{n-2}$ lies in $\mathcal L_n$ (p. 36).
Eq. (22.4): $F_{20} > 10{,}000$ , hence for every $L > 0$ twenty evaluations locate the maximum within an interval of length $10^{-4} L$ .
Eqs. (22.5)–(22.6): with $r_{1,2} = (1 \pm \sqrt5)/2$ ,

F_n = \frac{r_2 - 1}{r_2 - r_1} r_1^{\,n} + \frac{1 - r_1}{r_2 - r_1} r_2^{\,n}, \qquad \frac{F_{n+1}}{F_n} \to r_1 .

Theorem 12, corrected: $K_0 = K_1 = 1$ , $K_2 = 2$ , $K_3 = 4$ , and

K_n = F_{n+1} - 1 \qquad (n \ge 3).

Significance

The result. Theorem 11 is an exact minimax statement: $n$ evaluations shrink the interval of uncertainty for the peak of a unimodal function by a factor of at most $F_n \approx r_1^{\,n}/\sqrt5$ , and no adaptive rule, however clever, does better. It certifies Fibonacci search as optimal and golden-section search as asymptotically optimal, which is the reason these methods are the default line searches when derivatives are unavailable. Eq. (22.4) quantifies the rate: twenty evaluations give four decimal digits.

Formalizing it. The theorem has been proved since 1953; the work here is a machine-checked proof of the full minimax statement over all adaptive procedures, including the lower bound. That half is a statement about every decision tree and requires an adversary argument, which is exactly the kind of reasoning that is informal in the book and easy to get wrong. The discrete Theorem 12 is misprinted in the book (see below), so a formal proof also settles the correct values. We are not aware of an existing formalization of the optimality of Fibonacci search in Lean or another proof assistant. The Binet formula and the ratio limit are in Mathlib for Mathlib's indexing (Real.coe_fib_eq, tendsto_fib_succ_div_fib_atTop); milestone 6 only transfers them to the book's indexing.

Difficulty

The upper bound $L < F_{n-1} + F_{n-2}$ must hold for every procedure, not only for procedures that follow the "compare two points, discard a piece, keep the surviving point" pattern of the book's figures. A procedure may place its second point depending on the first value, may re-evaluate points, may evaluate outside $[0, L]$ , and may branch on the exact values rather than on their order. The book's argument tacitly restricts to that pattern, so the lower bound has to be established for arbitrary trees, where the information carried by exact values, repeated or wasted evaluations and branch-dependent placements all have to be accounted for. The bookkeeping is delicate because the surviving sets are half-open or open intervals, and whether the endpoints are included decides that the supremum is not attained.

The naive attempt of proving a bound only for "one new point per step inside the current bracket" procedures does not prove the goal: the goal quantifies over all decision trees.

Formalization scope

Model fixed. Deterministic adaptive procedures (decision trees branching on the exact real value observed), exact function values, cost equal to the number of evaluations; this is one of the models that Bellman's footnote 8 alludes to ("It is actually not easy to specify precisely what we mean by an optimal search procedure"). Functions are ℝ → ℝ, constrained only on $[0, L]$ ; evaluations outside $[0, L]$ are allowed and useless.
Output. A closed interval $[a, b]$ with $a \le b$ , $b - a \le 1$ containing the maximizer. It need not lie inside $[0, L]$ or have length exactly one; for $L \ge 1$ this is equivalent to Bellman's "sub-interval of unit length".
Indexing. The book's $F_n$ is a separate definition bookFib with $F_0 = F_1 = 1$ ; in Mathlib's indexing $F_n$ is Nat.fib (n + 1). The goal is stated for every $n \ge 0$ ; the book calls $F_0$ a convention, and in this model $\sup \mathcal L_0 = 1$ agrees with it.
Sup, not max. Theorem 11 is stated with IsLUB, never as "a procedure exists for $L = F_n$ ", which is false for $n \ge 2$ . Theorem 12 is stated with IsGreatest, which asserts that the maximum exists.
Implicit ranges. Eq. (22.3) is stated unconditionally for all $n \ge 2$ (the book proves it under the induction hypothesis). "Within $10^{-4}$ of the original interval length" is read as an interval of length at most $10^{-4} L$ .
Misprint corrected. Theorem 12 prints $K_n = 1 + F_n$ for $n \ge 3$ . On seven points, four evaluations suffice: evaluate points 3 and 5; if $f(3) > f(5)$ the peak is among points 1–4 with $f(3)$ known, and evaluating point 2 and then point 1 or 4 finds it; the case $f(5) > f(3)$ is symmetric, and $f(3) = f(5)$ forces the peak at point 4. So $K_4 \ge 7 > 6 = 1 + F_4$ . The mission states $K_n = F_{n+1} - 1$ for $n \ge 3$ , which agrees with the printed $K_3 = 4$ and keeps all printed initial values. The printed text is kept verbatim in the milestone.
Ruling out trivializations. The procedure never sees $f$ except through the values it requests, and it must succeed for every strictly unimodal $f$ with one fixed tree; "some interval of length one contains the maximizer" with no procedure, or a procedure allowed to depend on $f$ , would make the problem trivial and is not what is stated.
Contributions welcome. A reusable decision-tree framework for query-complexity lower bounds, lemmas about which finite sets of observed values are consistent with a strictly unimodal function, and the Fibonacci search tree itself as a construction.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter I, § 22, pp. 34–36. doi:10.2307/j.ctv1nxcw0f
J. Kiefer, Sequential minimax search for a maximum, Proceedings of the American Mathematical Society 4 (1953), 502–506. doi:10.1090/S0002-9939-1953-0055639-3

9 thms2 active usersReviewed

Completed

Dynamic Programming Optimization·Captain: mikedeng1

Bellman's Dynamic Programming I: Existence and Uniqueness for the Multi-Stage Allocation EquationTextbook

Motivation

Chapter I of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) opens the book with a multi-stage allocation process: a resource is divided, stage after stage, between two activities, each of which yields an immediate return and leaves behind a depleted remainder that is re-divided at the next stage. The chapter uses this process as its prototype for "a number of multi-stage processes, of diverse origin, but similar analytic structure" (§ 8, p. 11), and the techniques it introduces here — the functional equation of the infinite process, successive approximations, approximation in policy space, transfer of convexity and concavity through the recurrence, and a stability estimate — reappear throughout the book and in the later theory of Markov decision processes.

When the number of stages is large, Bellman replaces the finite sequence of recurrences by a single equation for the infinite process. As the book stresses (p. 11), this replacement is only useful once one knows that the equation has a solution and possesses "no extraneous solutions". This mission formalizes that existence and uniqueness theorem and the chapter's main structural results that rest on it.

Setting

A quantity $x \ge 0$ is split into $y \in [0,x]$ , assigned to a first activity with return $g(y)$ , and $x - y$ , assigned to a second activity with return $h(x-y)$ . After the stage the first allocation has been reduced to $ay$ and the second to $b(x-y)$ , and the process continues with the quantity $ay + b(x-y)$ . Writing

T(f,y) = g(y) + h(x-y) + f\big(ay + b(x-y)\big),

the total return $f(x)$ of the infinite process satisfies the allocation equation (Bellman's (8.1))

f(x) = \max_{0 \le y \le x} T(f,y), \qquad x \ge 0.

The standing hypotheses of Chapter I, Theorem 1 are:

$g$ and $h$ are continuous on $[0,\infty)$ and $g(0) = h(0) = 0$ ;
with $m(x) = \max_{0 \le y \le x} \max(|g(y)|, |h(y)|)$ and $c = \max(a,b)$ , the series $\sum_{n=0}^\infty m(c^n x)$ converges for every $x \ge 0$ ;
$0 \le a < 1$ and $0 \le b < 1$ .

The successive approximations from an initial function $f_0$ are $f_{N+1}(x) = \max_{0 \le y \le x} T(f_N, y)$ . A policy is a function $y_0(x)$ with $0 \le y_0(x) \le x$ ; its return is the total of the stage returns obtained by using $y_0$ at every stage.

In Lean all objects live in the namespace BellmanDP.Allocation: allocT is $T$ , allocM is $m$ , AllocationHyp g h a b bundles the three hypotheses, IsAllocationSolution g h a b f is the equation with the maximum attained, allocIter is the sequence $f_N$ , and policyReturn is the return of a policy.

Formalization targets

Goal: Chapter I, Theorem 1

Under the three hypotheses, there is a function $f$ with

f(x) = \max_{0 \le y \le x}\big[g(y) + h(x-y) + f(ay + b(x-y))\big] \quad (x \ge 0), \qquad f(0) = 0,\ f \text{ continuous at } 0,

this $f$ is continuous on $[0,\infty)$ , and every solution continuous at $0$ with value $0$ there coincides with $f$ on $[0,\infty)$ .

Milestones

Theorem 2 — from any $f_0$ continuous on $[0,\infty)$ with $f_0(0) = 0$ , the successive approximations converge to $f$ uniformly on every finite interval.
Theorem 3 — started from the return of a continuous policy, the successive approximations increase monotonically and converge to $f$ uniformly on every finite interval.
Lemma 1 — if $G(x,y)$ is jointly concave on $x,y \ge 0$ , then $x \mapsto \max_{0 \le y \le x} G(x,y)$ is concave.
Theorem 4 — if $g$ and $h$ are convex, $f$ is convex and for each $x$ the maximum is attained at $y = 0$ or $y = x$ .
Theorem 5 — if $g$ and $h$ are strictly concave, $f$ is strictly concave and the maximizing $y$ is unique for every $x$ .
Theorem 9 — for the general equation $f(x) = \max_{0\le y\le x}[u(x,y) + f(ay+b(x-y))]$ , the continuous solutions for returns $u$ and $v$ satisfy $|f(x) - F(x)| \le \sum_{n \ge 0} D(c^n x)$ , where $D(z)$ is the maximum of $|u - v|$ over $0 \le y \le x \le z$ .

Significance

Theorem 1 is what gives meaning to "the solution" of the allocation equation, which every later result of the chapter refers to. Without the side condition at $0$ uniqueness fails: when $g = h = 0$ , every constant function and the indicator of $(0,\infty)$ solve the equation. Theorems 2 and 3 turn the existence proof into computational procedures (value iteration and policy improvement), and Theorem 3's monotonicity is the prototype of the policy-improvement property. Theorems 4 and 5 are the first structural results on optimal policies — all-or-nothing allocation under convex returns, a unique interior-or-boundary allocation under strictly concave returns — and Theorem 9 bounds the error made by replacing a return function with a simpler approximation.

These are classical results with published proofs in the book. No machine-checked version of any of them is known to this mission; the work is to formalize the proofs, building reusable infrastructure for functional equations of the form $f(x) = \max_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with a contracting transition $\tau$ .

Difficulty

The equation is not a contraction in the supremum norm on $[0,\infty)$ : $g$ and $h$ may be unbounded, so no global Banach fixed-point argument applies. Control comes instead from the shrinking of the argument, $ay + b(x-y) \le cx$ , which propagates a local estimate near $0$ out to every finite interval, and the summability hypothesis (1b) is what makes the resulting series converge uniformly on bounded sets. Uniqueness cannot come from a norm estimate either; it rests on continuity at $0$ alone. The maximum in the equation must be shown to be attained, which requires continuity of the limit function; the book notes (p. 13) that the monotone argument for nonnegative $g,h$ gives only a supremum. For Theorems 4 and 5, convexity and concavity must be carried through each approximation and preserved in the limit, and strict concavity must be recovered for the limit, where a pointwise limit of strictly concave functions is only concave.

Formalization scope

Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter any hypothesis or conclusion. Continuity at $0$ is one-sided (ContinuousWithinAt f (Set.Ici 0) 0), and uniqueness is equality on $[0,\infty)$ .
The maximum in the equation is encoded as IsGreatest of $\{T(f,y) : 0 \le y \le x\}$ , so a solution attains its maximum at every $x \ge 0$ . The maxima inside definitions ( $m$ , $f_{N+1}$ , the triangle maximum of Theorem 9) are real suprema (sSup) of images of compact nonempty sets of continuous functions, which equal the book's maxima under the stated hypotheses.
The later theorems refer to "the solution" of Theorem 1 by quantifying over solutions that are continuous at $0$ and vanish there; they never quantify over arbitrary solutions of the equation, for which the conclusions are false.
Theorem 3's "converges uniformly" is stated uniformly on every finite interval $[0,R]$ , the sense in which Theorem 2 and the series (11.10) used in its proof converge. Its initial function is defined explicitly as the series of stage returns along the trajectory of the policy.
Theorem 4's " $y$ will equal $0$ or $x$ " is stated as: an endpoint is a maximizer. It does not say every maximizer is an endpoint, which fails for $g = h = 0$ .
Each theorem carries its own parameter range as printed: $0 \le a, b < 1$ for Theorems 1–5, $0 < a, b < 1$ for Theorem 9.
Not included: Theorem 6 (the policy structure under strict concavity, which uses $f'$ without a hypothesis making $f$ differentiable), Theorems 7 and 8 (explicit solutions), Theorem 10 (the multi-dimensional process), and Theorems 11–12 on Fibonacci search, which form a separate mission.

Welcome contributions: a general existence-and-uniqueness theorem for equations $f(x) = \sup_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with $\|\tau(x,y)\| \le c\|x\|$ , and a lemma that parametric maxima over $[0,x]$ of continuous functions are continuous in $x$ .

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. https://doi.org/10.2307/j.ctv1nxcw0f — Chapter I, §§ 8–14 and 18, pp. 11–29.
R. Bellman, "On the theory of dynamic programming", Proceedings of the National Academy of Sciences 38 (1952), 716–719. https://doi.org/10.1073/pnas.38.8.716

10 thms2 active usersReviewed

Numerical Analysis Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions VIII: Quadratic Convergence of the Gradient Orthogonalization Method for Nonlinear EquationsTextbook

Motivation

Solving a square system of nonlinear equations $\psi_i(x) = 0$ , $i = 1, \dots, n$ , $x \in \mathbb{R}^n$ , is one of the oldest tasks of numerical analysis. It appears whenever optimality conditions, equilibrium conditions or discretized differential equations have to be solved. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński) treats such a system as the nonsmooth minimization problem

\min_{x \in E_n} f(x), \qquad f(x) = \max_{1 \le i \le n} |\psi_i(x)|,

whose optimal value is $0$ exactly when the system is consistent. Section 3.5 of the book applies the subgradient method with space dilation to this problem. At each iteration that method needs the gradient of one of the $\psi_i$ , not all $n$ of them. Taking the dilation coefficient to its extreme value ( $\beta = 0$ ) turns the method into a gradient orthogonalization method. The book shows that this method converges at a quadratic rate near a regular solution, like Newton's method, although it never forms or factorizes the Jacobian.

This mission is the eighth in a series formalizing Shor's book. It covers Sections 3.5–3.6 (printed pp. 62–71).

Setting

$E_n$ is the $n$ -dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$ . The data are functions $\psi_1, \dots, \psi_n : E_n \to \mathbb{R}$ with gradients $g_{\psi_i}(x)$ , and the max-residual function is $f(x) = \max_i |\psi_i(x)|$ (3.24). The Jacobian is the matrix $J(x) = \{\partial\psi_i/\partial t_j\}_{i,j=1}^n$ of partial derivatives with respect to the coordinates $x = \{t_1, \dots, t_n\}$ .

An almost-gradient of a function $f$ at $x_0$ is an accumulation point of a sequence of gradients $\nabla f(x_k)$ , where $x_k \to x_0$ and $f$ is differentiable at every $x_k$ (p. 18).

The regular case (p. 63) is the situation in which $f^* = \min f = 0$ is attained at a point $x^*$ , the $\psi_i$ are continuously differentiable near $x^*$ , and $J(x^*)$ is nonsingular.

The gradient orthogonalization method (3.27) runs in stages of $n$ steps. A stage starting at $x_0$ produces $x_1, \dots, x_n$ as follows. At step $k+1$ , $0 \le k < n$ , the gradient $g_{\psi_{k+1}}(x_k)$ is projected on the subspace orthogonal to the gradients $g_{\psi_1}(x_0), \dots, g_{\psi_k}(x_{k-1})$ used earlier in the stage. Call the result $\varphi_{k+1}$ . The step is

x_{k+1} = x_k - \frac{\psi_{k+1}(x_k)}{\|\varphi_{k+1}\|^2}\, \varphi_{k+1}.

For $k = 0$ there is nothing to project, so $\varphi_1 = g_{\psi_1}(x_0)$ . The next stage starts at $x_n$ .

Formalization targets

Goal: Theorem 3.9, one stage squares the error

Let $x^* = 0$ solve the system, let the $\psi_i$ be continuously differentiable with gradients Lipschitz with constant $L$ on a ball $S_\delta = \{x : \|x\| < \delta\}$ (3.28), and let $g_{\psi_1}(0), \dots, g_{\psi_n}(0)$ be linearly independent. Then there exist $\varepsilon > 0$ and $c > 0$ such that every stage with $\|x_0\| \le \varepsilon$ satisfies

\|x_n\| \le c\, \|x_0\|^2 .

Milestones inside the proof

The proof of Theorem 3.9 passes through these displayed results, stated here in attack order:

Eq. (3.29): near the solution, the orthogonalized gradients satisfy $\|\varphi_{k+1}\| > b > 0$ , with $b$ uniform over stages.
Eq. (3.33): after step $k+1$ , $|\psi_{k+1}(x_{k+1})| \le (L/b^2)\, \psi_{k+1}^2(x_k)$ .
Lemma 3.1: a step of length $h$ in a unit direction orthogonal to $g_{\psi_i}(x_1)$ changes $\psi_i$ by at most $L h (h + \|x_1 - x_2\|)$ .
Eqs. (3.36)–(3.37): within a stage, $\max_k \|x_k\| \le c_1 \|x_0\|$ , and at the end point $f(x_n) \ge c_2 \|x_n\|$ .

Companion result: Theorem 3.8

In the regular case, for every $\delta > 0$ there is a neighborhood of $x^*$ in which every almost-gradient satisfies

(1-\delta) f(x) \le (g_f(x), x - x^*) \le (1+\delta) f(x).

Significance

Theorem 3.9 says that a method which evaluates one equation and one gradient per step, and never solves a linear system, has the local quadratic rate of Newton's method on a regular system. The stages combine: once one stage starts close enough to the solution, the errors of later stages satisfy $\|x_0^{(r+1)}\| \le c\|x_0^{(r)}\|^2$ . Theorem 3.8 describes the geometry of $f$ near a regular solution. The ratio of $(g_f(x), x - x^*)$ to $f(x)$ tends to $1$ , which is what allows the dilation parameters of the book's Theorem 3.3 to approach their extreme values near the solution. Both results connect the nonsmooth space-dilation methods of Chapter 3 to classical Newton-type theory.

All results of this mission are proved in the book. None of them has, to our knowledge, a machine-checked proof: the platform has local quadratic convergence results for cubic-regularized Newton, proximal Newton and semismooth Newton, but not for this method. The work is formalizing Shor's proof. This includes building the Gram-determinant argument behind (3.29) and the second-order estimates, which are reusable for other projection-based solvers of Kaczmarz type.

Difficulty

A naive argument analyses each step as a Newton step for one equation and stops there. That shows each equation $\psi_{k+1}$ is small right after its own step, but the theorem needs all equations to be small at the end of the stage. Later steps move the point and can undo the progress on earlier equations. The step directions are orthogonal to the earlier gradients, but those gradients were taken at earlier points, not at the current one. Controlling this drift needs Lemma 3.1 together with the bound (3.36), which says that the whole stage stays within a multiple of $\|x_0\|$ .

A second difficulty is that the method is only defined near the solution. The step divides by $\|\varphi_{k+1}\|^2$ , and a uniform positive lower bound on these norms comes from the nonvanishing of a Gram determinant evaluated at $n$ different points. The final passage from small residuals to a small error needs the growth bound (3.37), which uses the nonsingularity of the Jacobian once more.

Formalization scope

Representation. $E_n$ is EuclideanSpace ℝ (Fin n). The equations are a family ψ : Fin n → E_n → ℝ indexed from $0$ , so ψ k is the book's $\psi_{k+1}$ . Gradients are Mathlib's gradient, and $S_\delta$ is the open ball Metric.ball 0 δ. Continuous differentiability is ContDiff ℝ 1; in Theorem 3.8 it is ContDiffOn ℝ 1 on a neighborhood of $x^*$ .
The stage. A stage is a predicate IsOrthStage ψ x on a sequence $x : \mathbb{N} \to E_n$ , which fixes $x_1, \dots, x_n$ from $x_0$ . The projection is starProjection onto the orthogonal complement of the span of the earlier gradients.
Corrected misprint. The printed Step 1, (3.27a), divides by $\|g_{\psi_1}(x_0)\|$ rather than its square. The formalization uses the square, which is what (3.27b) and the proof's (3.31)–(3.33) require at $k = 0$ .
Division by zero. The book gives no rule for $\varphi_{k+1} = 0$ ; Lean's $t/0 = 0$ would leave the point unchanged. All statements apply the method only near the solution, where (3.29) bounds $\|\varphi_{k+1}\|$ away from zero.
Quantifier order. In Theorem 3.9 and in (3.29), (3.36)–(3.37), the constants ( $\varepsilon$ , $c$ , $\delta'$ , $b$ , $\varepsilon_0$ , $c_1$ , $c_2$ ) are existentials placed before the stage. They depend only on the data $\psi, \delta, L$ . A statement with $c$ chosen after $x_0$ would be trivial, with $c = \|x_n\|/\|x_0\|^2$ , and is ruled out.
Nonsingularity. In Theorem 3.9 it is the linear independence of $g_{\psi_i}(0)$ , the book's primary hypothesis. In Theorem 3.8 it is $\det J(x^*) \ne 0$ , with $J$ defined by coordinate partial derivatives.
Almost-gradients. They are quantified universally: Theorem 3.8 holds for every almost-gradient, not for one chosen one.

Not formalized: Theorem 3.10 (pp. 70–71), the $n$ -step quadratic convergence of the $\beta = 0$ r-algorithm with resetting. Its directional minimization rule is not pinned down on the page. The algorithm says "determined by minimizing", while the proof uses "the smallest positive root" of a stationarity equation. A contribution that fixes this rule and states the theorem is welcome as a follow-up.

Contributions of any of the five milestones are welcome independently. The Gram-determinant lower bound (3.29) and Lemma 3.1 are general facts about orthogonalization and Lipschitz gradients, and are useful beyond this mission.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§3.5–3.6, pp. 62–71. https://doi.org/10.1007/978-3-642-82118-9
J. M. Ortega and W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970. https://doi.org/10.1137/1.9780898719468

10 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions IV: Linear Convergence of the Subgradient Method under Level-Set Shape ConditionsTextbook

Motivation

The subgradient method minimizes a convex function $f$ on $\mathbb{R}^n$ that need not be differentiable, by stepping against an arbitrary subgradient. With stepsizes $h_k \to 0$ , $\sum h_k = \infty$ it converges (Shor, Theorem 2.2), but in general only slowly: no stepsize rule that ignores the structure of $f$ gives a geometric rate. Section 2.3 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) identifies geometric conditions on $f$ under which a simple geometric stepsize rule does give linear convergence — convergence with the speed of a geometric progression — and computes the rate explicitly.

The results are the origin of what is now studied as sharpness or error-bound conditions for nonsmooth optimization. Their practical content is that nonsmooth problems whose level sets are not too elongated near the minimum (piecewise-linear functions, maxima of finitely many well-conditioned pieces, positive definite quadratics) can be solved by the subgradient method at a linear rate, with a stepsize rule that needs only one or two scalar parameters.

Timeline. Shor proposed the subgradient method in 1962. The book presents the geometric stepsize rule under an angle condition (Theorem 2.7) and its level-surface form (Theorem 2.8), and attributes the block-halving rule of Theorem 2.9 to its reference [94]. Goffin (Math. Programming 13, 1977) gave the sharp rate in terms of a condition number of the level sets. The book compares the quadratic case with L. V. Kantorovich's rate for steepest descent.

Setting

Let $E_n$ be the $n$ -dimensional Euclidean space with inner product $(x, y)$ and $f : E_n \to \mathbb{R}$ convex. A vector $g$ is a subgradient of $f$ at $x$ if $f(y) - f(x) \ge (g, y - x)$ for all $y$ ; $g_f(x)$ denotes an arbitrary subgradient at $x$ , chosen once for each $x$ . Let $M^*$ be the set of minimum points of $f$ , assumed nonempty; for $x \in E_n$ , $x^*(x)$ is the point of $M^*$ nearest to $x$ .

Given a starting point $x_0$ and positive stepsizes $h_1, h_2, \dots$ , the normalized subgradient method is

x_{k+1} = x_k - h_{k+1}\frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, 2, \dots,

stopped when $g_f(x_k) = 0$ (then $x_k \in M^*$ ).

Two shape conditions are used. The angle condition (2.12) with angle $0 \le \varphi < \pi/2$ asks that every subgradient make an angle at most $\varphi$ with the direction to the nearest minimum point:

(g_f(x), x - x^*(x)) \ge \cos\varphi\,\|g_f(x)\|\,\|x - x^*(x)\|.

The level-surface ratio condition (2.20), for a function with unique minimum point $x^*$ , asks that on a ball $Y$ around $x^*$ any two points $x, z$ on a common level surface $f(x) = f(z) \ne f(x^*)$ satisfy $\|x - x^*\| \le \sigma\|z - x^*\|$ .

Formalization targets

Goal: Theorem 2.8 (p. 32)

If $f$ has a unique minimum point $x^*$ , $\sigma \ge \sqrt2$ , $h_1 \ge \|x_0 - x^*\|/\sigma$ , and (2.20) holds on $Y = \{y : \|y - x^*\| \le \sigma h_1\}$ , then with $h_{k+1} = h_k\sqrt{\sigma^2-1}/\sigma$

\|x_k - x^*\| \le h_{k+1}\,\sigma, \qquad k = 0, 1, 2, \dots

Milestones

Theorem 2.7 (pp. 30–31): under (2.12) and the geometric rule $h_{k+1} = h_k r(\varphi)$ with $r(\varphi) = \sin\varphi$ for $\varphi \ge \pi/4$ and $r(\varphi) = 1/(2\cos\varphi)$ for $\varphi < \pi/4$ ,

\|x_k - x^*(x_k)\| \le h_{k+1}/\cos\varphi \quad\text{resp.}\quad 2h_{k+1}\cos\varphi .

Remark after Theorem 2.7 (p. 32): the same conclusion when (2.12) holds only at the iterates.
Inequality (2.22) (p. 33): (2.20) on $Y$ implies $(g, x - x^*) \ge \sigma^{-1}\|g\|\,\|x - x^*\|$ for every $x \in Y$ and every subgradient $g$ at $x$ .
Example (p. 33): for $A$ symmetric positive definite with extreme eigenvalues $\lambda \le \mu$ ,

\min_{x \ne 0}\frac{(Ax, x)}{\|Ax\|\,\|x\|} = \frac{2\sqrt{\lambda\mu}}{\lambda + \mu},

attained at $x = \sqrt{\mu/(\lambda+\mu)}\,s_1 + \sqrt{\lambda/(\lambda+\mu)}\,s_2$ . 5. Theorem 2.9 (p. 34): under the assumptions of Theorem 2.8 with $\sigma \ge 2$ , the rule $h_{k+1} = h_0 2^{-[(k+1)/N]}$ with $N \ge 3\sigma^2 + 1$ gives $\|x_k - x^*\| \le 2\sigma h_{k+1}$ .

Significance

The results. Theorem 2.7 shows that the subgradient method, often dismissed as sublinear, converges linearly once the geometry of $f$ is controlled and the stepsizes decrease geometrically at the right ratio; the rate $r(\varphi)$ depends only on the angle. Theorem 2.8 restates the hypothesis in terms of the shape of level surfaces, a condition that can be checked for concrete functions, and gives rate $\sqrt{\sigma^2-1}/\sigma$ . The Example computes the angle for positive definite quadratics, yielding rate $(\varrho - 1)/(\varrho + 1)$ with $\varrho = \mu/\lambda$ the condition number — the same rate as steepest descent with exact line search in Kantorovich's analysis, obtained with less storage. Theorem 2.9 removes the need to know $\sigma$ exactly in the stepsize ratio.

Formalizing them. All five results are proved in the book; none is formalized, and no linear-rate result for a nonsmooth first-order method is on the platform. The formalization pins the constants (2.13)–(2.19), the stepsize indexing, and the treatment of the stopped iteration; the Example is a Kantorovich-type inequality for symmetric operators that is reusable beyond this mission.

Difficulty

The obvious one-step estimate $\|x_{k+1} - x^*\|^2 = \|x_k - x^*\|^2 - 2h_{k+1}(g, x_k - x^*)/\|g\| + h_{k+1}^2$ alone does not contract: the step length is fixed in advance and does not shrink with the distance, so a step may overshoot the minimum. The rate argument has to track the ratio between the current distance and the current stepsize, and the admissible ratio of stepsizes is dictated by the worst case of this quadratic in the distance; in the two regimes $\varphi \ge \pi/4$ and $\varphi < \pi/4$ the worst case sits at different ends. For Theorem 2.8, the shape condition is only assumed on the ball $Y$ , so the iterates must be shown to stay in $Y$ , and the passage from level surfaces to subgradients needs the distance from $x^*$ to a level surface, which is not a quantity the iteration computes. Theorem 2.9's constant stepsize blocks are not monotone in distance at all, and the count $3\sigma^2 + 1$ must be matched against a worst-case phase.

Formalization scope

The space $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued and ConvexOn ℝ Set.univ. A subgradient selection is an arbitrary function g with g x a subgradient at every x, quantified universally. Stepsizes are h : ℕ → ℝ with h (k+1) used at step k; the recursions $h_{k+1} = h_k r$ are imposed for $k \ge 1$ , $h_1$ being the chosen initial step (the book's " $k = 0, 1, 2, \dots$ " in Theorem 2.8 is read this way). The iteration stops at $g_f(x_k) = 0$ by an explicit branch that repeats $x_k$ , never through $x/0 = 0$ ; the bounds are asserted for every $k$ , which implies the book's "either the method stops or …" form. $x^*(x)$ is a definition (the nearest point of the set of minima), and the set of minima is assumed nonempty. Unique minimum is stated as $M^* = \{x^*\}$ . The ball $Y$ is closed, and (2.20) is assumed only for pairs in $Y$ with a common value different from $f(x^*)$ . In (2.16) the ratio is $1/(2\cos\varphi)$ , as the proof requires, where the page prints "1/2 cos φ". In Theorem 2.9, "the assumptions of Theorem 2.8" are taken with $h_1 = h_0$ , which fixes $h_0 \ge \|x_0 - x^*\|/\sigma$ and $Y$ of radius $\sigma h_0$ . In the Example, the extreme eigenvalues are pinned by $\lambda\|x\|^2 \le (Ax,x) \le \mu\|x\|^2$ together with unit eigenvectors, and the minimum is stated with IsLeast.

A statement in which the stepsizes or the bound constants could be chosen after the iterates, or in which the shape condition quantified over an empty set of pairs, would be trivially true; here every constant is fixed by the hypotheses before the sequence is generated, and the conditions are the book's.

Needed infrastructure: the subgradient inequality, continuity of convex functions on $\mathbb{R}^n$ , nearest points of closed convex sets, and elementary trigonometry. The nearest-point map and the stepsize ratio are defined within the mission; the subgradient inequality, the set of minima and the iteration come from the series' shared definitions. Contributions welcome: proofs of the milestones, and a reusable Kantorovich-type cosine bound for symmetric positive definite operators.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §2.3, pp. 30–36. https://doi.org/10.1007/978-3-642-82118-9
J.-L. Goffin, On convergence rates of subgradient optimization methods, Mathematical Programming 13 (1977) 329–347. https://doi.org/10.1007/BF01584346
L. V. Kantorovich, Functional analysis and applied mathematics, Uspekhi Mat. Nauk 3 (1948) 89–185 (steepest descent rate for quadratics, cited by Shor as [45]).

9 thms2 active usersReviewed

Dynamic Programming Markov Chain Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VII: The (BOR) Assumptions and Positive Recurrence of Optimal PoliciesTextbook

Motivation

Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.

Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.

According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).

Setting

A Markov decision chain consists of a countable state space $S$ , finite nonempty action sets $A_i$ , nonnegative finite costs $C(i,a)$ and transition probabilities $P_{ij}(a)$ . A policy $\theta$ may use the whole history and randomize. For $\alpha\in(0,1)$ the discount value function is $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$ , the infimum of $\sum_t\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i]$ ; the average cost of $\theta$ is $J_\theta(i)=\limsup_n\frac1nE_\theta[\sum_{t<n}C(X_t,A_t)\mid X_0=i]$ and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)$ . All of these lie in $[0,\infty]$ .

For a distinguished state $z$ the relative value is $h_\alpha(i)=V_\alpha(i)-V_\alpha(z)$ . The (SEN) assumptions are: (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded on $(0,1)$ ; (SEN2) $h_\alpha\le M$ for a finite function $M\ge0$ ; (SEN3) $h_\alpha\ge-L$ for a finite constant $L\ge0$ . Under (SEN), $J=\lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ is a finite constant, and a limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some $\beta_n\to1^-$ . The ACOI and ACOE read

J+h(i)\ \ge\ (\text{resp. }=)\ \min_{a\in A_i}\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\qquad i\in S.

For a nonempty set $G$ the first passage time is $T=\min\{n\ge1:X_n\in G\}$ . The class $\Re(i,G)$ consists of the policies that, from $i$ , enter $G$ with probability one in finite expected time $m_{iG}(\theta)$ ; $\Re^*(i,G)$ adds a finite expected first passage cost $c_{iG}(\theta)=E_\theta[\sum_{t<T}C(X_t,A_t)]$ . A (randomized) stationary policy $d$ is $z$ standard if the Markov chain it induces has $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$ ; it then has a single positive recurrent class $R_d\ni z$ and a finite constant average cost $J_d$ .

Formalization targets

Goal: Theorem 7.5.6

Assume (BOR): (BOR1) a $z$ standard policy $d$ exists; (BOR2) for some $\varepsilon>0$ the set $D=\{i: C(i,a)\le J_d+\varepsilon\text{ for some }a\}$ is finite; (BOR3) every $i\in D-R_d$ can be reached from $z$ by some $\theta_i\in\Re^*(z,i)$ . Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy $e$ has a positive recurrent state in

D(e)=\{i: C(i,e)\le J+\varepsilon\},

at most $|D(e)|$ positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies $e\in\Re^*(i,D(e)\cap R(e))$ for every $i$ .

Milestones

Lemma 7.4.1: $h_\alpha(i)\le c_{iz}(\theta_i)$ for $\theta_i\in\Re^*(i,z)$ , hence (SEN2).
Lemma 7.4.2: $h(i)\le c_{iG}(\theta)-Jm_{iG}(\theta)+E_\theta[h(X_T)]$ for $\theta\in\Re(i,G)$ under an integrability condition.
Theorem 7.4.3: four sufficient conditions for equality in the ACOI at a state.
Lemma 7.5.2: $J_d=(1-\alpha)\sum_{i\in R}\pi_i(d)V_{d,\alpha}(i)$ for a $z$ standard $d$ .
Proposition 7.5.3: a $z$ standard policy gives (SEN1–2).
Corollary 7.5.4: on $S=\{0,1,\dots\}$ , increasing $V_\alpha$ plus a $0$ standard policy gives (SEN), with nonnegative increasing limit functions.
Proposition 7.5.5: an optimal stationary policy has a positive recurrent state of cost at most $J+\varepsilon$ , reachable from $i$ , when (7.33) holds.
Corollaries 7.5.9 and 7.5.10: the (CAV) and (CAV*) conditions imply (BOR).

Significance

Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.

The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.

Difficulty

The obvious approach to the ACOE is to pass to the limit $\alpha\to1^-$ in the discount optimality equation. Exchanging this limit with $\sum_jP_{ij}(a)h_\alpha(j)$ requires a dominating function, and (SEN2) only gives a pointwise bound $M$ whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy $\Phi$ vanishes along them, which in turn needs finiteness of $c_{iG}$ that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set $D$ is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.

Formalization scope

States form a countable type $S$ ; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, $m_{iG}$ , $c_{iG}$ , $P_\theta(X_T=j)$ , $Q^{(n)}_{ij}$ ) are computed from the history probabilities of the process. $V_\alpha$ , $J_\theta$ , $m_{iG}$ and $c_{iG}$ take values in $[0,\infty]$ ; $m_{iG}=\infty$ when $G$ is missed with positive probability; the first passage time satisfies $T\ge1$ . $h_\alpha$ and $\sum_jP_{ij}(a)h(j)$ are in the extended reals, with the book's convention that a function bounded below has an expectation in $(-\infty,+\infty]$ . Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities $\pi_j=(m_{jj})^{-1}$ are the notions for the chain induced by a (randomized) stationary policy. $J_d$ is the average cost of $d$ from $z$ .

A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which $|D(e)|$ is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.

A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at $T$ ); Abelian limits of $\sum_t\alpha^tP(T=t)$ ; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. doi:10.1002/9780470317037
V. S. Borkar, "On minimum cost per unit time control of Markov chains", SIAM J. Control Optim. 22 (1984), 965–978.
V. S. Borkar, "Control of Markov chains with long-run average cost criterion: the dynamic programming equations", SIAM J. Control Optim. 27 (1989), 642–657.
V. S. Borkar, Topics in Controlled Markov Chains, Pitman Research Notes in Mathematics 240, Longman, 1991.
R. Cavazos-Cadena, "Weak conditions for the existence of optimal stationary policies in average Markov decision chains with unbounded costs", Kybernetika 25 (1989), 145–156.
R. Cavazos-Cadena and L. I. Sennott, "Comparing recent assumptions for the existence of average optimal stationary policies", Oper. Res. Letters 11 (1992), 33–37.
L. I. Sennott, "The average cost optimality equation and critical number policies", Prob. Eng. Inform. Sci. 7 (1993).
L. I. Sennott, "Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs", Operations Research 37 (1989), 626–633. doi:10.1287/opre.37.4.626
K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967.

15 thms2 active usersReviewed

Dynamic Programming Probability Stochastic Systems·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems VI: The (SEN) Assumptions and the Average Cost Optimality InequalityTextbook

Motivation

Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.

Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ , for each state $i$ a finite nonempty action set $A_i$ , a nonnegative finite cost $C(i,a)$ , and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$ . A policy $\theta$ chooses the action at time $n$ at random according to a distribution that may depend on the whole history $(X_0, A_0, \dots, X_n)$ ; a stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$ .

For an initial state $i$ , the $n$ -horizon cost is $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t) \mid X_0 = i]$ , the average cost is $J_\theta(i) = \limsup_{n} v_{\theta,n}(i)/n$ , and the minimum average cost is $J(i) = \inf_\theta J_\theta(i)$ over all policies. A policy is average cost optimal if $J_\theta \equiv J$ . For $\alpha \in (0,1)$ the discounted value function is $V_\alpha(i) = \inf_\theta \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i]$ . All these quantities lie in $[0,\infty]$ .

Fix a distinguished state $z$ and put $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ . The (SEN) assumptions are:

(SEN1) $(1-\alpha)V_\alpha(z)$ is bounded for $\alpha \in (0,1)$ ;
(SEN2) there is a nonnegative finite function $M$ with $h_\alpha(i) \le M(i)$ for all $i$ and $\alpha$ ;
(SEN3) there is a nonnegative finite constant $L$ with $-L \le h_\alpha(i)$ for all $i$ and $\alpha$ .

A limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some sequence $\beta_n \to 1^-$ . If $f_\alpha$ is a stationary policy realizing the discount optimality equation $V_\alpha(i) = \min_a \{C(i,a) + \alpha\sum_j P_{ij}(a)V_\alpha(j)\}$ , a limit point $f$ is a stationary policy with $f_{\beta_n}(i) = f(i)$ for large $n$ , for each $i$ , along some $\beta_n \to 1^-$ .

Formalization targets

Goal: Theorem 7.2.3

Under (SEN), there is a finite constant $J = \lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ independent of $i$ ; limit functions exist, satisfy $-L \le h \le M$ and the average cost optimality inequality (ACOI)

J + h(i) \ge \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)h(j)\Big\}, \qquad i \in S;

every stationary policy realizing the minimum is average cost optimal with $J_e \equiv J$ and $E_e[h(X_n)]/n \to 0$ ; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.

Milestones

Proposition 7.1.1: finitely many initial transitions with finite cost do not change $J_\theta$ .
Lemma 7.2.1: a bounded-below solution $(J,h)$ of the ACOI inequality for a stationary $e$ gives $J_e \le J$ .
Proposition B.6: a sequence of functions squeezed between $-L$ and $M$ on a countable set has a pointwise convergent subsequence.
Proposition 7.2.4: (SEN) does not depend on the choice of $z$ .
Proposition 7.7.1: (SEN) $\Rightarrow$ (H*) $\Rightarrow$ (H).
Proposition 7.7.2: the conclusions of Theorem 7.2.3 hold under (H), with a state-dependent lower bound $L(i)$ .

Significance

Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.

The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.

Difficulty

On a finite state space the relative value functions are bounded and the Abelian limit $(1-\alpha)V_\alpha$ can be controlled directly. Here $h_\alpha$ is bounded above only by a function $M$ that may be unbounded, so passing to the limit in the discounted optimality equation $\sum_j P_{ij}(a)h_\alpha(j)$ cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of $E_e[h(X_n)]/n$ for a function $h$ that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.

Formalization scope

The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost $0$ , as the chapter prescribes.

The relative value $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ is computed in EReal, never through a truncated real subtraction: a state with $V_\alpha(i) = \infty$ gives $h_\alpha(i) = +\infty$ , so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces $V_\alpha(z) < \infty$ . Sums $\sum_j P_{ij}(a)h(j)$ and expectations $E[h(X_n)]$ of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to $0$ when not summable. The limit $\alpha \to 1^-$ is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences $\alpha_n \to 1^-$ in $(0,1)$ , and the (SEN), (H), (H*) sets are predicates carrying their witnesses $M$ and $L$ .

A development that bounds only $h_\alpha$ as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in $J(i)$ , proves a different and weaker theorem and does not count.

Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality $\limsup(1-\alpha)\sum\alpha^t c_t \le \limsup \frac1n\sum_{t<n}c_t$ (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Chapter 7 (pp. 127–166) and Appendix B. https://doi.org/10.1002/9780470317037
L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37 (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
L. I. Sennott, The average cost optimality equation and critical number policies, Probability in the Engineering and Informational Sciences 7 (1993). (Cited in the book's bibliography, p. 321.)
L. I. Sennott, Another set of conditions for average optimality in Markov control processes, Systems & Control Letters 24 (1995) 147–151. (Cited in the book's bibliography.)
R. Cavazos-Cadena, A counterexample on the optimality equation in Markov decision chains with the average cost criterion, Systems & Control Letters 16 (1991) 387–392. (Cited in the book's bibliography.)
S. M. Ross, Non-discounted denumerable Markovian decision models, Annals of Mathematical Statistics 39 (1968) 412–423. (Cited in the book's bibliography.)
H. M. Taylor, Markovian sequential replacement processes, Annals of Mathematical Statistics 36 (1965) 1677–1694. (Cited in the book's bibliography.)
E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control; formalized on Prove2Me in the mission of the same name (Borel state spaces, a different model).

12 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains VII: Palm's Theorem for Nonstationary DemandTextbook

Motivation

Spare-parts inventory models for repairable items rest on Palm's theorem: if demands arrive as a Poisson process with constant rate $\lambda$ and each demanded unit spends an independent, identically distributed resupply time with mean $\bar\tau$ in the pipeline, the number of units in resupply is Poisson with mean $\lambda\bar\tau$ in steady state. Stock levels, backorders and fill rates are all computed from that distribution.

Both assumptions fail in practice. Military flying programmes ramp up and down within weeks, repair shops close for periods, and commercial parts distribution centres see demand that varies by day of the week. Chapter 9 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) extends Palm's theorem to a nonstationary Poisson demand process with time-dependent resupply-time distributions, gives the compound (multi-unit order) version, and uses the result to compute, at any time $t$ , the distribution of units in repair at the depot of a two-echelon system.

Timeline: Palm (1938) proved the stationary result for telephone traffic; Feeney and Sherbrooke (1966) extended it to compound Poisson demand; Hillestad and Carrillo (RAND, 1980) and Crawford (RAND, 1981) developed the time-dependent extensions, summarized by Carrillo (RAND, 1989). The chapter presents these results.

Setting

A single item is stocked at one location, and every demand is for one unit.

Demand rate $\lambda(s) \ge 0$ , integrable on bounded intervals, with mean function $m(t) = \int_0^t \lambda(s)\,ds$ .
Demand process: a nonstationary Poisson process with mean function $m$ , with $N(0) = 0$ . $N(t)$ counts demands in $[0,t]$ and $T_0 < T_1 < \cdots$ are the demand epochs.
Resupply times: a unit demanded at time $s$ is resupplied within $w$ time units with probability $G_s(w)$ . Resupply times are nonnegative, have finite expectations, are independent from unit to unit, and are independent of the demand process.
$X(t)$ is the number of units in resupply at time $t$ : demands in $[0,t]$ whose resupply is not complete at $t$ .

The mean of $X(t)$ is

\alpha(t) = \int_0^t \bigl(1 - G_s(t-s)\bigr)\lambda(s)\,ds.

In the compound version (Section 9.2), orders arrive as above and each order is for $Q \ge 1$ units, with a time-stationary law $u_j = P(Q = j)$ . All units of an order share its resupply time, $Y(t)$ counts units demanded in $[0,t]$ , and $u^{(n)}_k$ is the $n$ -fold convolution of $(u_j)$ .

In the two-echelon version (Section 9.3), base $i$ has failure rate $\lambda_i$ . A failure is repaired at the base with probability $r_i$ and at the depot otherwise. Depot repair of a failure occurring at time $u$ takes a deterministic time $D(u)$ with $D(t) + t \ge D(s) + s$ for $s < t$ (no crossing). Write $\tilde t = \inf\{u \ge 0 : D(u) + u > t\}$ .

Formalization targets

Goal: Theorem 13 (p. 216)

For every $t \ge 0$ ,

P\{X(t) = k\} = e^{-\alpha(t)}\frac{\alpha(t)^k}{k!}, \qquad k = 0,1,2,\dots

This is an exact statement at each finite time, not a limit. With constant $\lambda$ and $G_s = G$ it reduces to the finite-time step of Palm's theorem.

Milestones

$E[N(t)] = m(t)$ (Section 9.1, p. 216).
Theorem 12 (p. 216): given $N(t) = n$ , the epochs $T_0, \dots, T_{n-1}$ are distributed as the order statistics of $n$ i.i.d. variables with distribution function $F(x) = m(x)/m(t)$ on $[0,t)$ .
The binomial step of the proof of Theorem 13 (pp. 216–217): $P\{X(t) = k \mid N(t) = n\} = \binom nk p^k(1-p)^{n-k}$ , with $p = \int_0^t (1 - G_s(t-s))\lambda(s)/m(t)\,ds$ .
Section 9.2 (p. 218): $E[Y(t)] = m(t)E[Q]$ and $\operatorname{Var}[Y(t)] = m(t)E[Q^2]$ .
Theorem 14 (p. 218): $P[X(t) = k] = \sum_{n\ge1} u^{(n)}_k e^{-\alpha(t)}\alpha(t)^n/n!$ for $k \ge 1$ , and $e^{-\alpha(t)}$ at $k = 0$ .
Section 9.3.2 (p. 221): $P\{X_0(t) = k\} = e^{-m_0(\tilde t,t)} m_0(\tilde t,t)^k/k!$ with $m_0(\tilde t,t) = \int_{\tilde t}^t \sum_i \lambda_i(u)(1-r_i)\,du$ .

A plain supporting item states that $N(t)$ is Poisson with mean $m(t)$ , the factor the proof of Theorem 13 uses.

Significance

Theorem 13 gives the full distribution of the pipeline at every instant. Time-dependent expected backorders, $\sum_{x > s(t)} (x - s(t)) P\{X(t) = x\}$ , and fill rates $P\{X(t) < s(t)\}$ follow from it, so stock levels can be planned against a surge or a repair outage without a steady-state approximation. Theorem 14 does the same for multi-unit orders. The depot result feeds the base-level convolution of Section 9.3.3, which in turn gives time-dependent performance measures for a two-echelon system.

These results are proved in the literature, and the chapter reproduces the proofs of Theorems 13 and 14. It cites Theorem 12 without proof ("similar to the one given in Chapter 3"). No machine-checked version of any of them is known, and neither Mathlib nor this platform has a Poisson process, stationary or not, a thinning theorem, or an order-statistics theorem. The formal content of this mission therefore includes the construction and the first distributional facts of the nonstationary Poisson process.

Difficulty

The algebra of the proof is a Poisson mixture of binomials and is short. The difficulty is Theorem 12 and its use. The obvious argument treats "the $n$ demands in $[0,t]$ " as $n$ independent draws from $F$ and assigns each an independent resupply time with law $G_{\text{draw}}$ . Making this rigorous requires identifying the conditional joint law of the epochs given $N(t) = n$ . The resupply time of the $j$ -th demand is not independent of its epoch: its law depends on the epoch. So it must be shown that, after conditioning, the marks attached to sorted epochs behave like marks attached to unsorted i.i.d. draws. The book's constant-rate argument (Chapter 3) uses the uniform density $n!/t^n$ on the simplex. Here the density involves $\lambda$ , which may vanish on intervals, and $m$ need not be invertible.

Formalization scope

Demand process. The nonstationary Poisson process is constructed, not postulated. With i.i.d. exponential(1) gaps and unit-rate points $\Gamma_k = A_0 + \cdots + A_k$ , the $k$ -th demand occurs at $T_k = \inf\{s \ge 0 : m(s) \ge \Gamma_k\}$ , and $N(t) = \#\{k : \Gamma_k \le m(t)\}$ .
Resupply times. Resupply times are $\rho(T_k, U_k)$ for a jointly measurable $\rho \ge 0$ and i.i.d. marks $U_k$ independent of the gaps, with $G_s(w) = \nu\{\rho(s,\cdot) \le w\}$ . Every measurable family $G_s$ arises this way, and joint measurability makes $\alpha(t)$ a genuine integral. Independence of resupply times from the demand process is not written in Theorem 12 or 13 but is used in the proof; it is part of the model.
Pinnings and conventions.
- " $\lambda$ integrable" is read as integrable on bounded intervals.
- Time is $t \ge 0$ .
- Theorem 12 assumes $m(t) > 0$ , since $F$ is $0/0$ otherwise, and sets $F = 0$ on $(-\infty,0)$ .
- Conditional probabilities are written as joint probabilities.
- $E[Y(t)]$ is stated in $[0,\infty]$ ; the variance identity assumes $E[Q^2] < \infty$ .
- $\tilde t$ is an infimum over $u \ge 0$ , and $D \ge 0$ .
- Counts are cardinalities, and are $0$ on the null event where they would be infinite.
Corrections. Theorem 14's printed sum starts at $n = 1$ , which gives $P[X(t) = 0] = 0$ . The statement keeps the book's formula for $k \ge 1$ and adds $P[X(t) = 0] = e^{-\alpha(t)}$ . The depot's Poisson demand stream with rate $\sum_i \lambda_i(1-r_i)$ is generated from the bases' processes and independent repair-location choices, not assumed.
Not stated.
- Eqs. (9.1)–(9.2), the FCFS depot backorders owed to base $i$ : the derivation on p. 221 is informal, and (9.1) prints the exponent $s_0(t-1)$ for $s_0(t)-1$ .
- The base analysis of Section 9.3.3.
- The compound law of $Y(t)$ on p. 217, which has the same $n = 0$ omission.
Trivialization ruled out. $X(t)$ is computed from the demand epochs and resupply times, not defined by its law, and resupply times cannot depend on the demand epochs except through the prescribed $G_s$ . Either shortcut would make the goal empty or false.
Infrastructure. The time-changed Poisson construction, its count law, the order-statistics property and marked thinning are reusable well beyond this chapter: in queueing ( $M_t/G_t/\infty$ ), in reliability, and in the stationary Palm mission of this series. Contributions of these general lemmas are welcome.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer, 2005, Chapter 9, pp. 215–222. https://doi.org/10.1007/b138879
C. Palm, "Analysis of the Erlang traffic formulae for busy-signal arrangements", Ericsson Technics 5, 1938, 39–58.
G. J. Feeney and C. C. Sherbrooke, "The (s−1, s) inventory policy under compound Poisson demand", Management Science 12(5), 1966, 391–411. https://doi.org/10.1287/mnsc.12.5.391
R. J. Hillestad and M. J. Carrillo, Models and techniques for recoverable item stockage when demand and the repair processes are nonstationary — Part I: Performance measurement, Report N-1482-AF, RAND Corporation, 1980.
G. B. Crawford, Palm's theorem for nonstationary processes, Report R-2750-RC, RAND Corporation, 1981.
M. J. Carrillo, Generalizations of Palm's theorem and Dyna-METRIC's demand and pipeline variability, Report R-3698-AF, RAND Corporation, 1989.

11 thms2 active usersReviewed

Operations Research

Missions

Understanding and Using Linear Programming II: Optimal Basic Feasible Solutions and Vertices in Equational FormTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Fundamentals of Queueing Theory I: Foster's Criterion for Positive RecurrenceTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 1.2 (Foster's criterion)

Milestones: the Markov chain theorems

Milestones: the Poisson process and the exponential distribution

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design XI: Optimal Sequential Screening by Option ContractsTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 11.8 (optimal sequential screening)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design X: Robust Mechanism Design — Belief Revelation on Finite Type SpacesTextbook

Motivation

Setting

Formalization targets

Goal: belief revelation on finite type spaces (Proposition 10.6)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design IX: Monotone Direct Mechanisms Are Dictatorial (Gibbard–Satterthwaite)Textbook

Motivation

Setting

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design VIII: Dominant-Strategy Implementation of Efficient Decision Rules Is VCGTextbook

Motivation

Setting

Formalization targets

Goal: uniqueness of VCG (Corollary 7.1, Green–Laffont–Holmström)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design VI: Rochet's Theorem — Implementability Is Cyclical MonotonicityTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 5.2 (Rochet)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design V: Dominant-Strategy Public Goods Mechanisms for Two Agents Are Fixed Cost SharesTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 4.8, fixed cost shares

Milestones

Significance