Optimization

Motivation

In an impulse control problem a controller does not steer a process continuously: at times of its choosing it shifts the state by a finite jump, paying a fixed cost plus a cost proportional to the jump. Such models describe central-bank interventions on an exchange rate, inventory replenishment and cash management. Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) study nonzero-sum games in which two players control the same diffusion by impulses. They prove a verification theorem for such games and apply it to a linear game whose Nash equilibria are explicit.

The paper's interpretation of the linear game is two central banks with different targets for an exchange rate. An explicit equilibrium gives explicit intervention thresholds, and Section 4.4 of the paper asks how these thresholds respond to the fixed cost of intervening. This mission formalizes that comparative-statics question: when intervening becomes more expensive, do the players intervene less?

Setting

The game of Section 4.1 has a discount rate $\rho > 0$, a volatility $\sigma > 0$, running payoffs $f_1(x) = x - s_1$ and $f_2(x) = s_2 - x$ with $s_1 < s_2$, and intervention costs: a player who shifts the state by $\delta$ pays $c + \lambda|\delta|$ and the opponent receives $\tilde c + \tilde\lambda|\delta|$. The standing assumptions of the section are

$$c \ge \tilde c \ge 0,\qquad \lambda \ge \tilde\lambda \ge 0,\qquad (c,\lambda) \ne (\tilde c,\tilde\lambda),\qquad 1 - \lambda\rho > 0 .$$

All parameters except the fixed cost $c$ are held fixed. Set $\theta = \sqrt{2\rho/\sigma^2}$ and $\eta = (1-\lambda\rho)/\rho$, both positive. For $c > 0$ the function

$$F_c(y) = 2y + \theta c - \eta\log\frac{\eta + y}{\eta - y},\qquad y \in (0,\eta),$$

has a unique zero $\xi(c) \in (0,\eta)$. With

$$\Gamma(c) = \frac{\theta(c-\tilde c)}{4\xi(c)} + \frac{\theta c(\lambda-\tilde\lambda)}{4\eta\,\xi(c)} + \frac{\lambda-\tilde\lambda}{2\eta}$$

and a parameter $\tilde s \in \mathbb R$, the paper's formulas (4.20) are

$$\bar x_i(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta+\xi}{\eta-\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],\qquad x_i^*(c) = \tilde s + \frac{(-1)^i}{\theta}\log\left[\sqrt{\frac{\eta-\xi}{\eta+\xi}}\bigl(\sqrt{\Gamma+1}+\sqrt\Gamma\bigr)\right],$$

for $i \in \{1,2\}$, with $\xi = \xi(c)$ and $\Gamma = \Gamma(c)$. In the Nash equilibrium of the paper's Proposition 4.7, player 1 intervenes when the state falls below $\bar x_1$ and moves it to $x_1^*$; player 2 intervenes above $\bar x_2$ and moves it to $x_2^*$. The interval $]\bar x_1(c), \bar x_2(c)[$ is the continuation region, where nobody intervenes. The equilibrium payoffs $V_1^c$, $V_2^c$ are explicit as well (4.27).

Formalization targets

Goal: Proposition 4.13

$$c \mapsto \bar x_2(c)\ \text{is strictly increasing and}\ c \mapsto \bar x_1(c)\ \text{is strictly decreasing on}\ ]\tilde c, +\infty[ .$$

The continuation region therefore widens strictly as the fixed cost grows. The statement concerns the explicit functions (4.20); that they are equilibrium thresholds is mission 2 of this series.

Milestones

1. (4.17). For $c > 0$, $\xi(c)$ is the unique zero of $F_c$ in $(0,\eta)$.
2. (4.28). $\xi \in C^\infty(]0,\infty[)$ with $\xi' = \frac\theta2\frac{\eta^2-\xi^2}{\xi^2}$ and $\xi'' = -\theta\eta^2\frac{\xi'}{\xi^3} = -\frac{\theta^2\eta^2}{2}\frac{\eta^2-\xi^2}{\xi^5}$.
3. (4.29). $\xi$, $c/\xi$ and $c\,\xi'$ tend to $0$ as $c \to 0^+$; $c(\eta-\xi) \to 0$ and $\xi \to \eta$ as $c \to +\infty$.
4. Proposition 4.12. As $c \to +\infty$, $\bar x_2, x_1^* \to +\infty$, $\bar x_1, x_2^* \to -\infty$, and pointwise $V_1^c(x) \to (x-s_1)/\rho$, $V_2^c(x) \to (s_2-x)/\rho$.
5. Proposition 4.14 (with a corrected hypothesis, below). If $\tilde c = 0$, then $x_2^*$ is strictly decreasing and $x_1^*$ strictly increasing on $]0,\infty[$; if moreover $\lambda = \tilde\lambda$, then $x_2^*(c) < \tilde s < x_1^*(c)$ for all $c > 0$.

Significance

Proposition 4.13 is the rigorous form of the economic intuition that costlier intervention makes players more patient. Together with Proposition 4.12 it describes the whole range of costs: the region of inaction grows strictly and invades the real line as $c \to \infty$, where the payoffs converge to those of the uncontrolled Brownian motion. Proposition 4.14 adds that, when the fixed gain vanishes, the targets $x_i^*$ move away from the centre $\tilde s$. The paper's numerical section shows that without $\tilde c = 0$ the targets need not be monotone.

The results are proved in the paper, in a few lines each, by differentiating the implicit function $\xi(c)$. None of them is formalized. The mission produces a machine-checked treatment of a parametrised implicit function, $c \mapsto \xi(c)$ defined by a transcendental equation: smoothness, explicit derivatives, and the asymptotics at both ends. On top of it, it gives a fully verified comparative-statics result for an explicit game equilibrium.

Difficulty

The thresholds depend on $c$ only through $\xi(c)$, which has no closed form, and through $\Gamma(c)$, a sum of terms in $c/\xi(c)$ and $1/\xi(c)$. Monotonicity of $\xi$ alone does not settle the goal: $c/\xi(c)$ is a ratio of two increasing functions, and its direction is decided by how fast $\xi$ grows compared with $c$, uniformly on $]\tilde c,\infty[$, including near $c = 0$, where $F_0$ has no zero and $\xi$ degenerates. The limits as $c \to +\infty$ need more than $\xi(c) \to \eta$: $\Gamma(c)$ grows linearly in $c$, so the rate at which $\eta - \xi(c)$ decays decides whether the targets $x_i^*$ diverge and whether the payoff coefficients vanish.

Formalization scope

The parameters $\rho, \sigma, \lambda, \tilde\lambda, \tilde c, \tilde s, s_1, s_2$ are bundled in a structure, and the standing assumptions not involving $c$ in a predicate $\rho > 0$, $\sigma > 0$, $s_1 < s_2$, $\tilde c \ge 0$, $\lambda \ge \tilde\lambda \ge 0$, $1 - \lambda\rho > 0$. $\theta$ and $\eta$ are computed from $\rho, \sigma, \lambda$ as in (4.21), not taken as free parameters. All quantities are real numbers.

$\xi(c)$ is defined as $\sup\{y \in (0,\eta) : F_c(y) \ge 0\}$. Milestone 1 proves that this is the paper's unique zero for every $c > 0$. For $c \le 0$ the set is empty and the definition returns the placeholder $0$. Every statement therefore restricts $c$ to $c > 0$, to $c > \tilde c$, or to $c \to +\infty$, and no statement can be satisfied through a junk value. On $]\tilde c, \infty[$ one has $\Gamma > 0$, so the square roots in (4.20) are the paper's. "Increasing" and "decreasing" are read strictly, as the proofs give. $C^\infty$ is ContDiffOn ℝ ∞, and $\xi'$ is deriv ξ. Limits at $0^+$ use the right neighbourhood filter.

Two departures from the page are disclosed in the items:

• $c > 0$ in (4.17). The standing assumptions allow $c = 0$ when $\tilde c = 0$ and $\lambda > \tilde\lambda$, but then $F_0$ has no zero; the paper's argument uses $F(0^+) = \theta c > 0$.
• $\lambda = \tilde\lambda$ in the last sentence of Proposition 4.14. For $\lambda > \tilde\lambda$, Proposition 4.11 gives $x_2^*(0^+) > \tilde s$ and the inequality $x_2^* < \tilde s$ fails for small $c$. The monotonicity claims keep the hypothesis $\tilde c = 0$ alone.

A complete development needs the intermediate value theorem and strict monotonicity on an interval, a differentiable implicit (or inverse) function theorem in one variable, and asymptotic estimates of $\log\frac{\eta+y}{\eta-y}$ near $0$ and near $\eta$. These one-variable lemmas about implicitly defined functions are reusable beyond this mission. Proofs of the milestones in any order are welcome.

Selected references

• R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0989 — accepted manuscript arXiv:1605.00039v4, https://arxiv.org/abs/1605.00039

Motivation

Optimization over sets of matrices of fixed rank comes up in low-rank matrix completion, model reduction, and the low-rank approximation of solutions of large matrix equations. A standard approach treats the constraint set as a Riemannian manifold and runs gradient or Newton-type methods on it (Absil, Mahony & Sepulchre 2008). Each iteration takes a step in the tangent space and then has to return to the manifold. A map that does this to first order is called a retraction, and its cost is often what decides whether a manifold method is practical.

Absil and Malick (2012) study retractions defined by projection: step to $X+Z$ in the ambient space, then take the nearest point of the manifold. Their Proposition 3.2 shows that for any $C^k$ submanifold ($k\ge2$) this projective retraction is a retraction. Section 3.2 makes it explicit for the manifold of fixed-rank matrices: near any matrix of rank $r$, the nearest matrix of rank exactly $r$ is the truncated singular value decomposition (Proposition 3.3). Section 4.4 also gives a closed form for a second retraction on the same manifold, the orthographic retraction (Proposition 4.11).

Setting

Fix natural numbers $n$, $m$ and $r\ge1$. The space $\mathbb R^{n\times m}$ of real $n\times m$ matrices carries the Frobenius norm $\|X\|^2=\sum_{i,j}X_{ij}^2=\operatorname{trace}(X^\top X)$ (3.6). The fixed-rank set is

$$\mathcal R_r=\{X\in\mathbb R^{n\times m}:\ \operatorname{rank}(X)=r\},$$

a smooth submanifold of $\mathbb R^{n\times m}$. It is not closed: its closure is the set of matrices of rank at most $r$.

A singular value decomposition (3.5) of $X$ is a factorization $X=U\Sigma V^\top$ in which $U=[u_1,\dots,u_n]\in\mathbb R^{n\times n}$ and $V=[v_1,\dots,v_m]\in\mathbb R^{m\times m}$ are orthogonal and $\Sigma\in\mathbb R^{n\times m}$ is zero off its diagonal. The diagonal of $\Sigma$ holds the singular values of $X$ in nonincreasing order,

$$\sigma_1(X)\ge\sigma_2(X)\ge\cdots\ge\sigma_{\min\{n,m\}}(X)\ge0,$$

and $\sigma_i(X)=0$ for $i>\min\{n,m\}$. A matrix has rank $r$ exactly when $\sigma_r(X)>0=\sigma_{r+1}(X)$. The truncated SVD of rank $r$ is $\hat X=\sum_{i=1}^r\sigma_i(X)u_iv_i^\top$ (3.7).

For a set $Q$ and a point $X$, the projection $P_Q(X)$ is the set of nearest points: the $Y\in Q$ with $\|X-Y\|\le\|X-W\|$ for all $W\in Q$. For a set that is not closed, $P_Q(X)$ may be empty or contain several points.

Formalization targets

Goal: Proposition 3.3

Let $\bar X\in\mathcal R_r$. For every $X$ with $\|X-\bar X\|<\sigma_r(\bar X)/2$ and every singular value decomposition $X=U\Sigma V^\top$,

$$P_{\mathcal R_r}(X)=\Bigl\{\sum_{i=1}^r\sigma_i(X)\,u_iv_i^\top\Bigr\}.$$

The projection exists, is unique, and is the truncated SVD. The radius $\sigma_r(\bar X)/2$ and the strict inequality are those of the paper.

Milestones

The paper's proof goes through four claims, which are the milestones in attack order:

1. Weyl's bound (§3.2, proof of Proposition 3.3, citing Horn–Johnson 7.3.8): $|\sigma_i(\bar X)-\sigma_i(X)|\le\|X-\bar X\|$ for every $i\ge1$.
2. Eckart–Young (3.7): for every singular value decomposition of $X$, $\hat X$ is a nearest matrix to $X$ of rank at most $r$.
3. The gap (3.8): if $\operatorname{rank}\bar X=r$ and $\|X-\bar X\|<\sigma_r(\bar X)/2$, then $\sigma_{r+1}(X)<\sigma_r(\bar X)/2<\sigma_r(X)$.
4. Uniqueness under a gap (§3.2, proof of Proposition 3.3, citing Helmke–Moore): if $\sigma_r(X)>\sigma_{r+1}(X)$, then $\hat X$ is the only nearest matrix of rank at most $r$.

Further result: Proposition 4.11

Write $X=U\left[\begin{smallmatrix}\Sigma_0&0\\0&0\end{smallmatrix}\right]V^\top$ (4.7), with $\Sigma_0$ the positive diagonal of nonzero singular values, and a tangent vector $Z=U\left[\begin{smallmatrix}A&C\\B&0\end{smallmatrix}\right]V^\top$ (4.8). If $\Sigma_0+A$ is invertible, the orthographic retraction is

$$R(X,Z)=U\begin{bmatrix}\Sigma_0+A&C\\B&B(\Sigma_0+A)^{-1}C\end{bmatrix}V^\top .$$

Here $R(X,Z)$ is the nearest point to $X+Z$ of $\mathcal R_r\cap(X+Z+N_{\mathcal R_r}(X))$.

Significance

The result. Proposition 3.3 reduces the projective retraction on $\mathcal R_r$ to one truncated singular value decomposition. With Proposition 3.2 this gives an explicit, computable retraction for Riemannian optimization on fixed-rank matrices. It is used, for instance, in low-rank matrix completion algorithms. The point is local: $\mathcal R_r$ is not closed, so far from $\mathcal R_r$ the nearest matrix of rank exactly $r$ need not exist, and the proposition gives an explicit radius on which it does exist and is unique. Proposition 4.11 gives a second retraction that needs only products of matrices and one $r\times r$ inverse.

Formalizing it. All results here are proved, on paper. To the best of a search of Mathlib and the Prove2Me catalog, none is machine-checked. Mathlib has singular values of linear maps between finite-dimensional inner product spaces (LinearMap.singularValues), but no singular value decomposition in matrix form, no Weyl perturbation inequality for singular values, and no Eckart–Young theorem. A complete development would add these, and the Eckart–Young theorem with its uniqueness case is a standard result of numerical linear algebra in its own right.

Difficulty

The proof in the paper is short only because it cites three facts, and each of them is a real piece of matrix analysis.

• Weyl's bound needs the variational (min–max) description of singular values, which Mathlib does not have for singular values.
• Eckart–Young requires comparing $\|X-Y\|$ with the singular values of $X$ for every $Y$ of rank at most $r$, not only for those diagonal in the same bases. The obvious approach, writing $Y$ in the singular bases of $X$, fails because $Y$ need not be diagonal there.
• Uniqueness under the gap requires showing that every minimizer is diagonal in some singular bases of $X$ and then using the gap to fix its support. Without the gap uniqueness fails: for $X=I_2$ and $r=1$ every $uu^\top$ with $\|u\|=1$ is a nearest point.

A further subtlety: Proposition 3.3 must hold for any singular value decomposition of $X$. Singular vectors are not unique, so the proof has to show that the truncation does not depend on the choice under the gap (3.8).

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius). The projection is the published platform predicate RandomGradFree.Nonsmooth.IsMetricProjection, and $P_{\mathcal R_r}(X)$ is the set {Y | IsMetricProjection (rankSet r) X Y}. The set equality with a singleton states existence, uniqueness and the formula together.

Conventions committed to:

• sv X i is $\sigma_i(X)$, 1-based as on the page. It is Mathlib's 0-based singularValues of Matrix.toEuclideanLin X at i - 1, so the index $0$ is meaningless and every statement uses indices $\ge1$.
• IsSVD X U S V is the predicate of (3.5). The singular value decomposition is a hypothesis of the theorems, never a choice made inside them, so the theorems hold for every singular value decomposition.
• truncSVD r U S V is $\sum_{i\le r}\Sigma_{ii}u_iv_i^\top$, written with the diagonal of S. That these entries are the singular values $\sigma_i(X)$ is a fact to be proved, not part of the definition.
• The hypothesis $r\ge1$ is added, because $\sigma_r$ needs it (and $\mathcal R_0=\{0\}$). It is the only hypothesis of Proposition 3.3 not printed on the page.
• In Proposition 4.11, matrices use the block index types Fin r ⊕ Fin p and Fin r ⊕ Fin q. The tangent vector and the normal space are taken in the form the page gives, and invertibility of $\Sigma_0+A$ is an explicit hypothesis. In the paper's proof it comes from "$Z$ in a neighborhood of the origin".

A formalization in which the radius is replaced by a smaller one, the projection is taken onto the matrices of rank at most $r$, or the singular value decomposition is chosen inside the statement is a different theorem and is ruled out.

Wanted contributions, all reusable beyond this mission:

• existence of a singular value decomposition in matrix form, and the identification of its diagonal with singularValues;
• Weyl's inequality for singular values;
• the Eckart–Young theorem and its uniqueness case;
• the Schur-complement rank formula for $2\times2$ block matrices, used for Proposition 4.11.

Selected references

• P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version HAL hal-00651608v2: https://hal.science/hal-00651608v2)
• P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
• C. Eckart and G. Young, The approximation of one matrix by another of lower rank, Psychometrika 1(3):211–218, 1936. https://doi.org/10.1007/BF02288367
• R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (§7.3, §7.4). https://doi.org/10.1017/CBO9780511810817
• U. Helmke and J. B. Moore, Optimization and Dynamical Systems, Springer, 1994 (Ch. 5). https://doi.org/10.1007/978-1-4471-3467-1

Motivation

Riemannian optimization algorithms move along a manifold by taking a step in a tangent direction and then coming back to the manifold. The map that does the coming back is a retraction, and the most natural candidate on a submanifold of a Euclidean space is the projective retraction: add the tangent step, then take the nearest point of the manifold. Its practical value depends on whether that nearest point can be computed.

For many manifolds of symmetric matrices the defining property is a property of the eigenvalues: matrices whose largest eigenvalue has multiplicity $p$, matrices with prescribed spectrum, and similar sets that arise in eigenvalue optimization and in alternating projection methods (Lewis and Malick 2008). Daniilidis, Malick and Sendov (reference [8] of the paper) showed that such a spectral set is a smooth manifold when the underlying set of eigenvalue vectors is a smooth, locally symmetric manifold. P.-A. Absil and J. Malick (SIAM J. Optim. 2012; authors' version hal-00651608v2) then showed that, close to such a manifold, the metric projection onto it has a closed form: one eigendecomposition and one projection in $\mathbb R^n$. This mission formalizes that result, Theorem 3.9 of the paper.

Setting

Write $\mathbf S_n$ for the real symmetric $n \times n$ matrices with the Frobenius norm $\|X\|^2 = \sum_{i,j} X_{ij}^2$, $\mathbf O_n$ for the orthogonal matrices, and $\mathbf \Sigma_n$ for the permutation matrices, which act on $\mathbb R^n$ (with the Euclidean norm) by permuting coordinates. Let

$$\mathbb R^n_\downarrow = \{x \in \mathbb R^n : x_1 \ge x_2 \ge \cdots \ge x_n\}.$$

For $X \in \mathbf S_n$, $\lambda(X) \in \mathbb R^n_\downarrow$ is the vector of its eigenvalues, with multiplicity, in nonincreasing order; every $X$ has an eigendecomposition $X = U \operatorname{Diag}(\lambda(X)) U^\top$ with $U \in \mathbf O_n$. For $M \subseteq \mathbb R^n$ the spectral set of $M$ is

$$\lambda^{-1}(M) = \{X \in \mathbf S_n : \lambda(X) \in M\}.$$

For a set $Q$ and a point $y$, $P_Q(y)$ is the set of nearest points of $Q$ to $y$ (it may be empty or contain several points).

Let $\mathcal M$ be a $C^2$ submanifold of $\mathbb R^n$: around each of its points it is a coordinate slice of a $C^2$ chart with $C^2$ inverse. Let $\mathcal S = \lambda^{-1}(\mathcal M \cap \mathbb R^n_\downarrow)$, let $\bar X \in \mathcal S$ and $\bar x = \lambda(\bar X)$. The set $\mathcal M \cap B(\bar x, \delta)$ (open ball) is strongly locally symmetric if for every $x \in \mathcal M \cap B(\bar x, \delta)$ and every $P \in \mathbf \Sigma_n$ with $Px = x$,

$$P\big(\mathcal M \cap B(\bar x, \delta)\big) = \mathcal M \cap B(\bar x, \delta). \qquad (3.15)$$

Formalization targets

Goal: Theorem 3.9 (projection onto spectral manifolds)

Assume $\mathcal M$ is a $C^2$ submanifold of $\mathbb R^n$, $\bar X \in \mathcal S$, $\delta > 0$ and (3.15). Then there is $\delta_0 \in (0, \delta]$ such that for every $X \in \mathbf S_n$ with $\|X - \bar X\| \le \delta_0/2$, the set $P_{\mathcal M}(\lambda(X))$ is a single point $p$, and for every $U \in \mathbf O_n$ with $X = U \operatorname{Diag}(\lambda(X)) U^\top$,

$$P_{\mathcal S}(X) = \{\, U \operatorname{Diag}(p)\, U^\top \,\}.$$

The goal fixes no constant: $\delta_0$ is only asserted to exist, as the paper's proof restricts $\delta$ to make the local uniqueness of $P_{\mathcal M}$ and Lemma 3.8 apply.

Milestones

1. (3.11): $\|\lambda(X) - \lambda(Y)\| \le \|X - Y\|$ for $X, Y \in \mathbf S_n$.
2. Lemma 3.7: for closed $M \subseteq \mathbb R^n_\downarrow$, an eigendecomposition $X = U\operatorname{Diag}(\lambda(X))U^\top$ and sorted $z$, $U \operatorname{Diag}(z) U^\top \in P_{\lambda^{-1}(M)}(X) \iff z \in P_M(\lambda(X))$.
3. Lemma 3.8: for $\bar x \in \mathbb R^n_\downarrow$ and all small $\delta > 0$, for $y \in B(\bar x, \delta)$ and sorted $x \in B(\bar x, \delta)$, the maximum of $x^\top P y$ over permutations fixing $\bar x$ is attained at some $P$ with $Py$ sorted.
4. (3.20): under (3.15) and for small $\delta$, the distance from a sorted $x \in B(\bar x, \delta)$ to $\mathcal M \cap B(\bar x, \delta)$ is attained up to equality on sorted points.

Significance

The theorem turns the projective retraction on a spectral manifold, an optimization problem over $n \times n$ matrices, into a projection in $\mathbb R^n$ onto $\mathcal M$ plus one eigendecomposition. For the matrices whose largest eigenvalue has multiplicity $p$, the projection onto $\mathcal M_p$ is an explicit averaging of the top $p$ eigenvalues (Example 3.10 of the paper), which completes a partial result of Oustry (reference [29, Th. 13] of the paper). Together with Theorem 3.5, it is what makes the projective retraction a practical alternative on manifolds where the Riemannian exponential has no known efficient formula.

The result is proved in the paper; to our knowledge none of it is formalized. The mission produces a machine-checked version of the theorem and of the spectral-set toolkit beneath it: the Lipschitz property of sorted eigenvalues, the reduction of projections onto spectral sets to projections onto sets of vectors, and the permutation rearrangement lemma. The formalization also corrects a misstatement: Lemma 3.7 as printed quantifies over all $z \in \mathbb R^n$, and its direction "$\Rightarrow$" fails for unsorted $z$ (for $n = 2$, $M = \{(2, 0)\}$, $X = U = I$, $z = (0, 2)$). The mission states it for $z \in \mathbb R^n_\downarrow$, which is the only case Theorem 3.9 uses.

Difficulty

The obvious argument shows only half of the goal. Lemma 3.7 characterizes the nearest points of $\mathcal S$ that share the eigenvectors $U$ of $X$; it does not exclude a nearest point with other eigenvectors, and the goal asserts that $P_{\mathcal S}(X)$ is a single point. Excluding the others needs the equality case of the trace inequality $\operatorname{trace}(XY) \le \lambda(X)^\top \lambda(Y)$ (3.10), which the paper quotes from the literature without proof, and the fact that the projection $p$ inherits the ties of $\lambda(X)$, which comes from strong local symmetry and uniqueness of $P_{\mathcal M}$.

The local uniqueness of $P_{\mathcal M}$ near a point of a $C^2$ submanifold (Lemma 3.1 of the paper) is itself a tubular-neighbourhood argument through the inverse function theorem. Mathlib has no metric projection onto embedded submanifolds, no von Neumann trace inequality for sorted eigenvalues, and no Hoffman–Wielandt inequality. Finally, the radii interact: the restriction $\delta_0$ must make Lemma 3.1, Lemma 3.8 and the ball inclusion $P_{\mathcal M}(x) \in B(\bar x, \delta)$ all hold at once.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin n), with the Euclidean norm (not the sup norm of Fin n → ℝ). Matrices are Matrix (Fin n) (Fin n) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius); $\mathbf S_n$ is IsHermitian (symmetry over $\mathbb R$) and $\mathbf O_n$ is Matrix.orthogonalGroup.
• $\lambda(X)$ is eig X, built from Mathlib's sorted IsHermitian.eigenvalues₀; on a non-symmetric matrix it returns $0$, and every statement assumes symmetry. $\mathbb R^n_\downarrow$ is sortedDesc n, spectral sets are specSet, permutations act by permAct (an isometry), and (3.15) is IsStronglyLocallySymmetric on the open ball.
• Nearest points are the platform predicate RandomGradFree.Nonsmooth.IsMetricProjection; $P_Q(y)$ is {z | IsMetricProjection Q y z}.
• The submanifold hypothesis is a local slice-chart predicate IsSubmanifold 2 d M. The paper allows $k = 2$ or $\infty$; $k = 2$ covers both. Only the hypotheses of Theorem 3.5 (cited from Daniilidis–Malick–Sendov without proof) are assumed, not its conclusion that $\mathcal S$ is a manifold.
• "For $\delta$ small enough" is $\exists \delta_1 > 0, \forall \delta \in (0, \delta_1]$; the radius of Theorem 3.9 is an existential $\delta_0 \le \delta$, with the paper's non-strict $\|X - \bar X\| \le \delta_0/2$.
• Both singleton claims of Theorem 3.9 are part of the conclusion. A version proving only $\subseteq$ would be satisfied by the empty set, and a version that assumes $P_{\mathcal M}(\lambda(X))$ is a singleton would delete the theorem's local-uniqueness content; neither is the target.

Infrastructure that a full development needs and that is reusable beyond this mission: the von Neumann/Fan trace inequality and its equality case for real symmetric matrices, the Hoffman–Wielandt inequality (3.11), the rearrangement inequality over permutations fixing a vector, and the local existence and uniqueness of metric projections onto $C^2$ submanifolds. Useful platform items: RHLinalg.vonNeumann_trace_ineq (the trace inequality for Hermitian matrices), RHLinalg.bilinear_doublyStochastic_le_of_monovary (the rearrangement step), and Bhatia.trace_mul_perm_bounds (trace pairings between permutation pairings of unsorted spectra). Contributions of these lemmas, of alternative proofs of (3.11), and of the equality case of (3.10) are welcome.

Selected references

• P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529; authors' version https://hal.science/hal-00651608v2
• A. Daniilidis, J. Malick and H. Sendov, Locally symmetric submanifolds lift up to spectral manifolds, preprint, 2009 (reference [8] of the paper; the source of Theorem 3.5).
• A. S. Lewis and J. Malick, Alternating projections on manifolds, Math. Oper. Res. 33(1):216–234, 2008. https://doi.org/10.1287/moor.1070.0291
• F. Oustry, A second-order bundle method to minimize the maximum eigenvalue function, Math. Program. 89:1–34, 2000 (reference [29] of the paper).
• A. S. Lewis, Convex analysis on the Hermitian matrices, SIAM J. Optim. 6(1):164–177, 1996. https://doi.org/10.1137/0806009

Motivation

Resource-constrained project scheduling with minimum and maximum time lags is the model behind make-to-order production, process-industry batch planning and large engineering projects. When the objective is the project duration or another regular function (nondecreasing in every start time), an optimum can be found among schedules that cannot be shifted to the left. Many objectives in practice are nonregular: net present value, earliness–tardiness costs, resource levelling and resource investment. For these, delaying an activity can pay, and "shift as far left as possible" no longer identifies a finite set of candidate schedules.

Neumann, Nübel and Schwindt (Math. Methods Oper. Res. 52, 2000) answered this with classes of schedules defined by the absence of pairs of opposite shifts: stable, semistable, pseudostable and quasistable schedules, the mirror image of active, semiactive, pseudoactive and quasiactive schedules. Section 3.2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), shows that these classes are exactly the extreme points of the feasible region and of its natural convex pieces. The classification of objective functions in §3.3, and every enumeration scheme of the later chapter, rests on that correspondence.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$. Activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. The project network $N$ has node set $V$ and arcs $\langle i,j\rangle\in E$ with integer weights $\delta_{ij}$, each encoding a temporal constraint $S_j-S_i\ge\delta_{ij}$. A prescribed deadline $\bar d\in\mathbb N$ is included as the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$. Renewable resources $k$ have capacities $R_k$, and activity $i$ uses $r_{ik}\le R_k$ units while it runs.

A schedule is a vector $S\in\mathbb R^{n+2}$ of start times. The time-feasible region $\mathcal S_T$ collects the schedules with $S_0=0$, $S\ge0$ and $S_j-S_i\ge\delta_{ij}$ on every arc; it is a polyhedron, and a polytope when every activity precedes $n+1$ as in Remarks 1.1.2. A schedule is resource-feasible if at every time $t\ge0$ the running activities $\mathcal A(S,t)=\{i\mid S_i\le t<S_i+p_i\}$ use at most $R_k$ units of every resource. The feasible region is $\mathcal S=\mathcal S_T\cap\mathcal S_R$. It is in general neither convex nor connected.

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$. For a strict order $O$, the order polytope is $\mathcal S_T(O)=\{S\in\mathcal S_T\mid S_j\ge S_i+p_i\ ((i,j)\in O)\}$. The order $O$ is feasible if $\emptyset\ne\mathcal S_T(O)\subseteq\mathcal S$. The schedule polytope of $S$ is $\mathcal S_T(O(S))$.

A shift moves a schedule $S$ to $S'\neq S$. It is global if both are feasible, local if in addition a continuous path inside $\mathcal S$ joins them, order-preserving if $O(S)\subseteq O(S')$, and order-monotone if $O(S)$ and $O(S')$ are comparable. Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$. A feasible schedule is stable, semistable, pseudostable or quasistable if no pair of opposite global, local, order-monotone or order-preserving shifts, respectively, starts at it. It is antiactive if no global right-shift starts at it.

Formalization targets

Goal: Theorem 3.2.10

For every feasible schedule $S$:

$$\begin{aligned} &\text{(a) } S\text{ antiactive}\iff S\text{ maximal in }\mathcal S, \qquad \text{(b) } S\text{ stable}\iff S\in\operatorname{ext}\mathcal S,\\ &\text{(c) } S\text{ semistable}\iff S\in\operatorname{ext}C_S,\ C_S\text{ the component of }\mathcal S\text{ containing }S,\\ &\text{(d) } S\text{ pseudostable}\iff S\in\operatorname{ext}\mathcal S_T(O)\ \text{for all feasible }O\subseteq O(S),\\ &\text{(e) } S\text{ quasistable}\iff S\in\operatorname{ext}\mathcal S_T(O(S)). \end{aligned}$$

Milestones

• Lemma 3.2.4: opposite order-preserving or order-monotone shifts can be taken uniform (all moved activities move by one common amount).
• Lemma 3.2.8: pseudostable schedules are the local extreme points of $\mathcal S$, the points on no segment that lies entirely in $\mathcal S$.
• Lemma 3.2.9: when $S$ is not pseudostable, a segment through $S$ can be found inside one order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$ feasible.
• Proposition 3.2.13: the quasistable schedules, and every class below them in Fig. 3.2.6, form finite sets.
• Proposition 3.2.16: every vertex of $\mathcal S_T$ is the unique solution of $S_0=0$, $S_j-S_i=\delta_{ij}$ on the arcs of a spanning tree of $N$; for the minimal point, an outtree rooted at $0$.
• Theorem 3.2.18: $S$ is quasistable iff it is the unique solution of such a tree system in the schedule network $N(O(S))$.
• Remark 3.2.7: every activity of a quasistable schedule is tied to another one by a tight duration or time lag, so quasistable schedules are integer-valued.

Significance

The theorem makes four shift-defined classes computable objects: extreme points of explicit polytopes, or of a finite union of them. Together with Proposition 3.2.13, it gives each class of nonregular objective functions in §3.3 a finite candidate set of schedules among which an optimum can be sought (§3.2, p. 207). Theorem 3.2.18 gives the certificate for quasistable schedules: a spanning tree of the schedule network, which the later sections use to enumerate vertices.

The results are proved in the book, except Lemma 3.2.9, whose proof is cited to Neumann, Nübel and Schwindt (2000). As far as a search of the platform shows, none of them has been formalized. A formalization supplies the missing details, among them that connected and path components of $\mathcal S$ coincide and the degenerate vertices behind the tree description. It also produces a reusable library of schedule classes on real-valued start times.

Difficulty

Part (b) is close to the definition, since a pair of opposite global shifts is a segment through $S$ with feasible endpoints. The content is elsewhere. In (c) the definition speaks of continuous trajectories and the right-hand side of connected components, so the proof needs local path-connectedness of a finite union of polytopes. In (d) the feasible region is not convex: an order-monotone shift keeps $S$ and $S'$ in a common order polytope, but $S'$ and $S''$ may lie in different ones. The segment through $S$ has to be moved into a single order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$, and that is Lemma 3.2.9. Proposition 3.2.16 and Theorem 3.2.18 need the passage from $n+2$ linearly independent tight constraints to a spanning tree. They must allow degenerate vertices, where several trees describe the same point, and must represent the nonnegativity constraints $S_i\ge0$ by arcs of the network.

Formalization scope

Activities are Fin (n + 2); start times are real vectors Fin (n + 2) → ℝ with the pointwise order. Durations, capacities and requirements are natural numbers, and time lags integers. The deadline is the arc $\langle n+1,0\rangle$ of weight $-\bar d$, which is always present, as §3.1 prescribes. Resource constraints are imposed for every $t\ge0$, not only for $0\le t\le\bar d$ as (3.1.2) writes; the proofs use the first reading. Extreme points are Mathlib's Set.extremePoints ℝ, maximal points are Maximal for the pointwise order, and components are connectedComponentIn. A local shift carries an explicit continuous map from unitInterval into $\mathcal S$. Strict orders are asymmetric, transitive relations on $V$. A spanning tree is an arc set of size $n+1$ whose underlying simple graph is connected. Its arcs must be arcs of $N$, resp. of $N(O(S))$, with their network weights, so an arbitrary equation system does not count.

The schedule classes are defined through shifts and nothing else. Defining "stable" as "extreme point", or "pseudostable" as "local extreme point", would make the goal and Lemma 3.2.8 tautologies, and such encodings are ruled out. Proposition 3.2.16 carries the book's standing convention (§1.2, p. 8) that every node is reached from $0$ by a walk of nonnegative length. Without it the statement is false.

The definitions duplicate, under this mission's namespace, the model of the book's Chapter 2 missions (order polytopes, shifts, active classes). They are written to be merged with those once published. Contributions on the geometry of finite unions of polytopes, and on spanning-tree bases of difference constraint systems, are reusable beyond this mission.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1–3.2. https://doi.org/10.1007/978-3-540-24800-2
• K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), 441–465. https://doi.org/10.1007/s001860000092
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 199–240. https://doi.org/10.1007/BF02283745

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.