Optimization

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.

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

1. Proposition 3.6: every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
2. Lemma 3.6: the pivot mechanism is IC and IR.
3. Lemma 3.7: among IC and IR mechanisms with decision rule $q^*$, the pivot mechanism has the largest expected budget surplus.
4. Lemma 3.8: if $N\underline\theta < c < N\bar\theta$, the pivot mechanism's expected budget surplus is negative.
5. 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.

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

1. Proposition 3.1, the revelation principle: every Bayesian Nash equilibrium of every mechanism is replicated by truth-telling in an incentive-compatible direct mechanism.
2. 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$.
3. Proposition 3.2: incentive compatibility holds if and only if every $Q_i$ is increasing and the revenue-equivalence formula holds.
4. Proposition 3.3: under incentive compatibility, individual rationality is equivalent to $T_i(\underline\theta) \le \underline\theta Q_i(\underline\theta)$.
5. Lemma 3.5: an optimal mechanism has $T_i(\underline\theta) = \underline\theta Q_i(\underline\theta)$.
6. 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$.
7. 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

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

1. Proposition 2.1: every mechanism and optimal buyer strategy can be replaced by a truthful direct mechanism with the same outcomes.
2. 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.$$

3. 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)$.
4. 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.
5. 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.

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:

1. for every $y$ and every row the maximum of $\sum_j a_{ij}(q_i) y_j$ over $S_i$ is attained;
2. $0 < a_{ij}(q) \le m < \infty$ on $S$;
3. $\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

1. § 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]$.
2. 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.
3. 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$.
4. 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]$.
5. 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

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

1. 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}'$.
2. § 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]$.
3. Eq. (12.13): $|J(\varphi) - J_N(\{\varphi_k\}, n)| \le B'/n$ for step controls.
4. Eq. (12.14): $f(c, T, n) \le f(c, T) + B'/n$ for all $n \ge 1$.
5. 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