Probability

Motivation

Many problems in statistics, signal processing and machine learning minimize an expected loss that is neither smooth nor convex: robust phase retrieval, blind deconvolution, covariance estimation with the $\ell_1$ loss, training of networks with ReLU activations, and composite problems $h(c(x))$ with convex $h$ and smooth $c$. A common structural feature of these objectives is weak convexity: adding a quadratic $\frac{\rho}{2}\|x\|^2$ makes the function convex. For such problems the classical stochastic algorithms — the stochastic proximal point method, the stochastic prox-linear method, and the stochastic proximal subgradient method — were used in practice long before any nonasymptotic complexity guarantee was available for them.

Damek Davis and Dmitriy Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) gave such guarantees for all of these methods at once. They abstract each method as minimization of a stochastic one-sided model of the objective, and prove that the expected squared gradient of the Moreau envelope at a randomly selected iterate decays at rate $O(1/\sqrt T)$, i.e. a sample complexity of $O(\varepsilon^{-4})$. This mission formalizes that main theorem (Theorem 4.3) and the lemmas its proof uses.

Timeline. Nurminskii (1973, 1974) showed that when the sample losses are $\rho$-weakly convex and there is no regularizer, the stochastic subgradient method converges subsequentially to stationary points almost surely; no rate was given. Ghadimi and Lan (2013) proved $O(\varepsilon^{-4})$ complexity for smooth nonconvex stochastic problems. Davis and Grimmer (arXiv:1707.03505, 2017) gave a rate for a proximally guided variant of the stochastic subgradient method on weakly convex problems. Davis and Drusvyatskiy (2018) obtained the $O(\varepsilon^{-4})$ complexity for the basic proximal stochastic subgradient method and, through the one-sided model framework, for the stochastic proximal point and prox-linear methods.

Setting

Work on $\mathbb R^d$ with the Euclidean norm. An extended-valued function $r:\mathbb R^d\to\mathbb R\cup\{\infty\}$ has domain $D=\operatorname{dom} r=\{x: r(x)<\infty\}$ and is closed when its epigraph is closed. A function $\psi$ is $\rho$-weakly convex when $x\mapsto\psi(x)+\frac{\rho}{2}\|x\|^2$ is convex. For $\lambda>0$ the Moreau envelope and proximal map are

$$\psi_\lambda(x)=\min_y\Big\{\psi(y)+\tfrac{1}{2\lambda}\|y-x\|^2\Big\},\qquad \operatorname{prox}_{\lambda\psi}(x)=\operatorname*{argmin}_y\Big\{\psi(y)+\tfrac{1}{2\lambda}\|y-x\|^2\Big\}.$$

The problem is $\min_x \varphi(x):=f(x)+r(x)$ with $r$ closed and $f$ locally Lipschitz, where $f$ is accessible only through a random model $f_x(y,\xi)$, $\xi\sim P$. Assumption B asks for constants $\tau,\eta,\mathsf L$, an open convex $U\supseteq D$ and a measurable $L:\Omega\to\mathbb R_+$ such that: $\mathbb E_\xi f_x(x,\xi)=f(x)$ and $\mathbb E_\xi[f_x(y,\xi)-f(y)]\le\frac\tau2\|y-x\|^2$ on $U$ (one-sided accuracy); $f_x(\cdot,\xi)+r$ is $\eta$-weakly convex for almost every $\xi$; $\sqrt{\mathbb E L(\xi)^2}\le\mathsf L$ and $f_x(x,\xi)-f_x(y,\xi)\le L(\xi)\|x-y\|$.

Algorithm 4.1 fixes $\bar\rho>\tau+\eta$ and parameters $\beta_t>\bar\rho$, draws i.i.d. samples $\xi_0,\dots,\xi_T$, and sets

$$x_{t+1}=\operatorname*{argmin}_x\Big\{r(x)+f_{x_t}(x,\xi_t)+\tfrac{\beta_t}{2}\|x-x_t\|^2\Big\}.$$

It returns $x_{t^*}$, with $t^*\in\{0,\dots,T\}$ drawn with $\mathbb P(t^*=t)\propto\frac{\bar\rho-\tau-\eta}{\beta_t-\eta}$. With $f_x(y,\xi)=f(y,\xi)$ it is the stochastic proximal point method; with a linearization it is the proximal stochastic subgradient method; with $h(c(x,\xi)+\nabla c(x,\xi)(y-x),\xi)$ it is the stochastic prox-linear method.

Formalization targets

Goal: Theorem 4.3, (4.15) and (4.16)

$$\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2\le\frac{\bar\rho(\varphi_{1/\bar\rho}(x_0)-\min\varphi)+2\bar\rho^2\mathsf L^2\sum_{t=0}^T\frac{1}{(\beta_t-\eta)(\beta_t-\bar\rho)}}{\sum_{t=0}^T\frac{\bar\rho-\tau-\eta}{2(\beta_t-\eta)}},$$

and for $\beta_t\equiv\bar\rho+\gamma^{-1}\sqrt{T+1}$ with $\gamma>0$,

$$\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2\le\frac{2(\bar\rho(\varphi_{1/\bar\rho}(x_0)-\min\varphi)+2\bar\rho^2\mathsf L^2\gamma^2)}{\bar\rho-\tau-\eta}\Big(\frac{\bar\rho-\eta}{T+1}+\frac{1}{\gamma\sqrt{T+1}}\Big).$$

Milestones, in the order the proof uses them

1. Lemma 4.1: $\varphi$ is $(\tau+\eta)$-weakly convex and $f$ is $\mathsf L$-Lipschitz on $U$.
2. Lemma 4.2, (4.7): $\mathbb E_t\|\hat x_t-x_{t+1}\|^2\le\|\hat x_t-x_t\|^2-\frac{\bar\rho-\tau-\eta}{\beta_t-\eta}\|\hat x_t-x_t\|^2+\frac{4\mathsf L^2}{(\beta_t-\eta)(\beta_t-\bar\rho)}$, with $\hat x_t=\operatorname{prox}_{\varphi/\bar\rho}(x_t)$.
3. Lemma 2.2: for $\rho$-weakly convex $\varphi$ and $\lambda\in(0,\rho^{-1})$, $\varphi_\lambda$ is $C^1$ with $\nabla\varphi_\lambda(x)=\lambda^{-1}(x-\operatorname{prox}_{\lambda\varphi}(x))$.
4. Theorem 4.3, (4.14): the one-step expected descent of $\varphi_{1/\bar\rho}$.

Significance

The result. By Lemma 2.2, $\|\nabla\varphi_{1/\bar\rho}(x)\|=\bar\rho\|x-\hat x\|$, and the proximal point $\hat x$ satisfies $\varphi(\hat x)\le\varphi(x)$ and $\operatorname{dist}(0,\partial\varphi(\hat x))\le\|\nabla\varphi_{1/\bar\rho}(x)\|$. A small envelope gradient therefore certifies that $x$ is close to a nearly stationary point. Theorem 4.3 gives this certificate, with explicit constants, for every algorithm fitting Assumption B, in particular the first complexity bounds for the stochastic proximal point and stochastic prox-linear methods on weakly convex problems. Companion results in the same paper (Theorems 4.1 and 4.2, separate missions) specialize to convex and strongly convex models.

Formalizing it. The theorem is proved on paper; no machine-checked version exists, on this platform or in Mathlib, of Theorem 4.3, of Lemma 2.2 for extended-valued weakly convex functions, or of the one-sided-model framework. A formalization yields a reusable Moreau-envelope library for weakly convex functions with constraints (via the domain of $r$), and a template for iterate-level stochastic analysis on product probability spaces.

Difficulty

The algebra of each step is short; what is hard is making it rigorous. First, Lemma 2.2 must be proved for extended-valued closed functions: existence and uniqueness of the proximal point need strong convexity of the subproblem together with lower semicontinuity and a quadratic minorant, and differentiability of the envelope is not a consequence of a generic envelope theorem. Second, the conditional expectations $\mathbb E_t$ in Lemma 4.2 must be realized on the product space of samples, with integrability of $\|x_{t+1}-x_t\|^2$, $r(x_{t+1})$ and $\varphi_{1/\bar\rho}(x_t)$ established along the iterates rather than assumed; the paper takes all of these for granted. Third, Assumption B gives the Lipschitz bound (4.2) only in one direction and only almost surely, and the argmin of Algorithm 4.1 exists only almost surely, so every pointwise step must be carried through null sets that depend on the current iterate.

Formalization scope

• Carrier and encoding. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The extended-valued $r$ (and $\varphi$) is a pair $(D,\text{real values on }D)$; closedness, weak convexity, the envelope (an infimum over $D$) and proximal points are defined in this encoding. The envelope parameter $\lambda$ is written lam.
• Randomness. The samples $\xi_0,\dots,\xi_T$ are a point of $\Omega^{T+1}$ under the product measure, and $\mathbb E$ is the Bochner integral. In Lemma 4.2, $\mathbb E_t$ is the integral over one fresh sample with the current iterate fixed.
• The algorithm. The step is any jointly measurable selection that lies in $D$ and minimizes the subproblem for almost every sample; measurability is an added hypothesis.
• The output. $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2$ is the weighted average of $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_t)\|^2$ with weights $\frac{\bar\rho-\tau-\eta}{\beta_t-\eta}$, its exact value for $t^*$ drawn independently of the samples.
• $\min\varphi$ is any real lower bound of $\varphi$ on $D$; the bound is monotone in it.
• Added hypotheses, implicit in the paper: $\beta_t>\eta$ (the subproblem is $(\beta_t-\eta)$-strongly convex; Assumption B allows any real $\tau$, so this does not follow from $\beta_t>\bar\rho>\tau+\eta$), $\eta\le\bar\rho$ in (4.16) (its derivation from (4.15) needs it), $\bar\rho>0$, $x_0\in U$, and, in Lemma 2.2, that $\varphi$ is closed and proper.
• Typos. The statement of Theorem 4.3 twice says "Algorithm 3.1"; it means Algorithm 4.1. The constant in (4.16) is the printed one, which is valid (slightly weaker than what (4.15) yields). The proof's "Setting $\bar\rho=2\rho$" is a slip; (4.16) keeps $\bar\rho$.
• No trivialization. Every bounded expectation comes with an integrability conclusion (a Bochner integral of a non-integrable function is $0$), the update is constrained by the argmin property of Algorithm 4.1, and $\min\varphi$ is a genuine lower bound; the hypotheses are satisfiable (e.g. $r=0$, $f=0$, zero model).
• Contributions welcome: a general Moreau-envelope library for weakly convex extended-valued functions (Lemma 2.2), measurability of argmin selections, and the one-step analysis lemmas.

Selected references

• D. Davis, D. Drusvyatskiy, Stochastic Model-Based Minimization of Weakly Convex Functions, SIAM J. Optim. 29(1):207–239, 2019. arXiv:1803.06523
• D. Davis, B. Grimmer, Proximally Guided Stochastic Subgradient Method for Nonsmooth, Nonconvex Problems, SIAM J. Optim. 29(3), 2019. arXiv:1707.03505
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4):2341–2368, 2013. doi:10.1137/120880811
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. doi:10.1007/978-3-642-02431-3

Motivation

Bayesian inverse problems and conditioned diffusions lead to probability measures on function spaces, and these are sampled in practice through finite-dimensional approximations on $\mathbb R^m$ with $m$ large. A Markov chain Monte Carlo method is useful in this setting only if its convergence rate does not deteriorate as the discretisation is refined. Random walk Metropolis (RWM), the default Metropolis–Hastings algorithm, is known from diffusion-limit analyses to need step sizes of order $1/m$ for Gaussian-type targets (Roberts, Gelman and Gilks 1997; Beskos, Roberts and Stuart 2009). Those results describe a scaling limit of the chain in stationarity; they do not bound the speed of convergence of the chain itself.

Hairer, Stuart and Vollmer (arXiv:1112.1392v4, Ann. Appl. Probab. 2014) prove that the preconditioned Crank–Nicolson algorithm has a spectral gap bounded below uniformly in $m$, and in §2.4 they show by an explicit example that RWM does not: its $L^2$-spectral gap vanishes as $m\to\infty$, faster than any power of $m$ unless the step size decays at least like $1/m$. This mission formalizes that negative result.

Setting

Fix $m\ge1$. The target is the Gaussian measure

$$\gamma_m=\mathcal L\Bigl(\sum_{i=1}^m\tfrac1i\,\xi_i e_i\Bigr),\qquad \xi_i\ \text{i.i.d.}\ \mathcal N(0,1),$$

on $\mathbb R^m$: the coordinates $x_1,\dots,x_m$ are independent and $x_i\sim\mathcal N(0,1/i^2)$. Its covariance $C$ satisfies $\langle x,C^{-1}x\rangle=\sum_{i=1}^m i^2x_i^2$.

A Metropolis–Hastings kernel with proposal kernel $Q$ and acceptance probability $\alpha(x,y)\in[0,1]$ is

$$P(x,dz)=Q(x,dz)\,\alpha(x,z)+\delta_x(dz)\int\bigl(1-\alpha(x,u)\bigr)\,Q(x,du).$$

RWM with step size $\delta>0$ proposes $y=x+\sqrt{2\delta}\,\xi$ with $\xi\sim\gamma_m$ and accepts with probability $\alpha(x,y)=1\wedge\exp\bigl(\sum_{i=1}^m\frac{i^2}{2}(x_i^2-y_i^2)\bigr)$. The resulting kernel $P_m$ is reversible with respect to $\gamma_m$. The expected acceptance probability from $x$ is $\alpha(x)=\int\alpha(x,y)\,Q(x,dy)$.

For a Markov kernel $P$ with invariant probability measure $\mu$, write $(Pf)(x)=\int f(y)\,P(x,dy)$, $\mu(f)=\int f\,d\mu$ and

$$\beta=\|P\|_{L^2_0\to L^2_0}=\sup_{f\in L^2_\mu}\frac{\|Pf-\mu(f)\|_2}{\|f-\mu(f)\|_2};$$

$1-\beta$ is the $L^2_\mu$-spectral gap. The conductance is

$$\mathsf C=\inf_{0<\mu(A)\le1/2}\frac{\int_A P(x,A^c)\,d\mu(x)}{\mu(A)}.$$

The step size is scaled with the dimension as $\delta_m=s\,m^{-a}$ with $s>0$ and $a\ge0$; $\beta_m$ is $\beta$ for $P_m$ and $\mu=\gamma_m$.

Formalization targets

Goal: Theorem 2.17 (1)

For $a\in[0,1)$, $s>0$ and every $p$, there is a constant $K$, independent of $m$, such that

$$1-\beta_m\le K\,m^{-p}\qquad\text{for all } m\ge1 .$$

Companion: Theorem 2.17 (2)

For $a\ge1$ and $s>0$ there is a constant $K$, independent of $m$, such that $1-\beta_m\le K\,m^{-a/2}$ for all $m\ge1$.

Milestones

1. Cheeger's inequality (2.7): $1-\beta\le2\mathsf C$ for a $\mu$-reversible Markov kernel (cited by the paper).
2. The conductance displays of p. 15: $\mathsf C\le\inf_A\int_A\alpha(x)\,\mu(dx)/\mu(A)$ and $\mathsf C\le\sup_{x\in B}\alpha(x)$ for $0<\mu(B)\le\frac12$.
3. Proposition 2.16: $1-\beta\le2\mathsf C\le2\sup_{x\in B}\alpha(x)$ (2.8) and $1-\beta\le2\mathsf C\le2\inf_A\int_AQ(x,A^c)\,d\mu/\mu(A)$ (2.9) for any Metropolis–Hastings kernel.
4. Proposition 2.16, second branch of (2.8): $1-\beta\le2\mathsf C\le2\,\mathbb E_\mu\alpha(x)$, for atomless $\mu$.
5. The acceptance bound of the proof of Theorem 2.17: for $\lambda\in[0,1]$, $\alpha(x)\le(1+2\lambda\delta)^{-m/2}\exp\bigl(\sum_{i=1}^m\delta\lambda^2i^2x_i^2/(2\delta\lambda+1)\bigr)$.
6. The half-space estimate for part (2): $A=\{x_1\ge0\}$ has $\gamma_m(A)=\frac12$ and $\int_AQ(x,A^c)\,\gamma_m(dx)\le c\sqrt{\delta/(\delta+1)}$ with $c$ independent of $m$ and $\delta$.
7. Theorem 2.17 (2).

Significance

The theorem separates two algorithms that differ only in their proposal. For the same Gaussian targets (the case $\Phi=0$ of the paper), the preconditioned Crank–Nicolson algorithm has an $L^2$-spectral gap bounded below uniformly in $m$, while RWM's gap collapses. For a reversible chain the spectral gap determines the worst-case asymptotic variance of ergodic averages over $L^2_\mu$ observables, so for RWM at a fixed step-size decay $a<1$ that worst case grows faster than any polynomial in $m$. Proposition 2.16 is reusable on its own: it bounds the spectral gap of every Metropolis–Hastings kernel by the acceptance probability or by the proposal's flow, on any measurable space. It also turns diffusion-limit statements about acceptance rates into bounds on the spectral gap.

The results are proved in the paper (Cheeger's inequality is cited from Lawler and Sokal 1988 and Sinclair and Jerrum 1989). No part has a machine-checked proof. The prove2me library has Cheeger's inequality for finite-state reversible chains (MarkovMixing.cheeger_upper), not for kernels on general measurable spaces with the $L^2_0$ operator norm. A complete development would contain the first formal Cheeger upper bound in that generality, the Metropolis–Hastings conductance bounds, and an explicit Gaussian computation for RWM.

Difficulty

Three steps resist a direct transcription. First, Cheeger's inequality has to be stated and proved for the Markov operator on $L^2_\mu$ of a general measurable space: $Pf$ is a Bochner integral that is finite only $\mu$-almost everywhere, and every identity relating $\beta$ to the flow between sets passes through invariance and centring. Second, the acceptance bound is an exact Gaussian computation in $m$ dimensions with explicit constants, where an off-by-one in the coordinate weights changes the target. Third, the asymptotic step: the acceptance probability is small only on sets where the weighted quantity $\sum_i i^2x_i^2$ is controlled, but a typical draw from $\gamma_m$ has $\sum_i i^2x_i^2$ of order $m$. A bound on $\alpha(x)$ over all of $\mathbb R^m$, or over a Euclidean ball, gives no decay, and the set used in Proposition 2.16 must keep $\gamma_m$-mass bounded away from $0$ uniformly in $m$ while $\alpha$ decays on it faster than every power of $m$.

Formalization scope

• State space Fin m → ℝ. The Lean coordinate i : Fin m is the paper's $x_{i+1}$, with variance $1/(i+1)^2$ and weight $(i+1)^2$. The target is Measure.pi of gaussianReal 0 (1/(i+1)^2).
• Kernels. The Metropolis–Hastings kernel is Q.withDensity α + Kernel.id.withDensity (rejection mass), with α : X → X → ℝ≥0∞. Every statement assumes α ≤ 1 and joint measurability (without it withDensity is the zero kernel). The RWM acceptance probability is Algorithm 2's with $\Phi=0$, with the exponential (display (1.4) omits it, a misprint).
• $\beta$ is the real supremum of the ratios over measurable $f\in L^2_\mu$ with $\|f-\mu(f)\|_2\ne0$, norms via eLpNorm. For a $\mu$-invariant Markov kernel the ratio set is bounded by $1$, and for $\gamma_m$ with $m\ge1$ it is nonempty, so $\beta_m$ is not a junk value.
• Conductance is in $[0,\infty]$ with the infimum over measurable $A$ with $0<\mu(A)\le\frac12$. The condition $0<\mu(A)$ is added: with $0/0=0$ it would otherwise force $\mathsf C=0$. Cheeger's inequality and Proposition 2.16 are stated in $[0,\infty]$ with $\max(1-\beta,0)$ on the left.
• Added hypotheses and readings. "$\delta_m\sim m^{-a}$" is read as $\delta_m=s\,m^{-a}$ for a fixed $s>0$ (p. 14), and $K$ may depend on $s$. The bounds hold for all $m\ge1$, not only for large $m$. "Any $p$" is every real $p$. Proposition 2.16's "Metropolis–Hastings kernel for a target $\mu$" is formalized as reversibility of $P$ with respect to $\mu$. Its undefined middle term $1-\Lambda$ is dropped. Its $\mathbb E_\mu\alpha$ branch carries an added atomlessness hypothesis on $\mu$.
• Trivializations ruled out. No statement involves a Bochner integral of a possibly non-integrable function or a real supremum over a possibly empty or unbounded set at the relevant parameters. $K$ is quantified before $m$. The target is a probability measure by construction.
• Infrastructure. The development needs the Markov operator on $L^2_\mu$, Jensen's inequality for kernels, Gaussian integrals on $\mathbb R^m$ with explicit constants, and tail estimates for $\gamma_m$ in weighted norms. Cheeger's inequality and Proposition 2.16 are reusable beyond this mission. Contributions of any of the milestones, or of alternative proofs of the goal, are welcome.

Selected references

• M. Hairer, A. M. Stuart and S. J. Vollmer, Spectral gaps for a Metropolis–Hastings algorithm in infinite dimensions, Ann. Appl. Probab. 24(6) (2014) 2455–2490; arXiv:1112.1392v4. https://arxiv.org/abs/1112.1392
• G. F. Lawler and A. D. Sokal, Bounds on the $L^2$ spectrum for Markov chains and Markov processes: a generalization of Cheeger's inequality, Trans. Amer. Math. Soc. 309 (1988) 557–580. https://doi.org/10.1090/S0002-9947-1988-0930082-9
• A. Sinclair and M. Jerrum, Approximate counting, uniform generation and rapidly mixing Markov chains, Inform. and Comput. 82 (1989) 93–133. https://doi.org/10.1016/0890-5401(89)90067-9
• A. Beskos, G. Roberts and A. Stuart, Optimal scalings for local Metropolis–Hastings chains on nonproduct targets in high dimensions, Ann. Appl. Probab. 19(3) (2009) 863–898. https://doi.org/10.1214/08-AAP563
• G. O. Roberts, A. Gelman and W. R. Gilks, Weak convergence and optimal scaling of random walk Metropolis algorithms, Ann. Appl. Probab. 7(1) (1997) 110–120. https://doi.org/10.1214/aoap/1034625254

Motivation

A seller with several goods and a single buyer is the smallest setting in which multi-dimensional mechanism design differs from the one-good theory. For one good, Myerson's theorem (Myerson 1981) says the optimal mechanism posts a price. For two or more goods the optimal mechanism may use lotteries, may be non-monotone in the buyer's values, and is in general not known in closed form. Practitioners nevertheless use simple mechanisms, and the question that Hart and Nisan (arXiv:1204.1846v3) ask is quantitative: what fraction of the optimal revenue does a simple mechanism guarantee?

This mission concerns the simplest mechanism of all, bundling: one posted price for the set of all goods. When the goods are independent and identically distributed, bundling is known to become nearly optimal as the number of goods grows for a fixed distribution (Armstrong 1999; Bakos and Brynjolfsson 1999). That limit is not uniform over distributions. Theorem D of Hart and Nisan gives the uniform guarantee: for every $k\ge2$ and every distribution, bundling $k$ i.i.d. goods earns at least $c/\log k$ of the optimal revenue.

Timeline. Armstrong (1999) and Bakos–Brynjolfsson (1999) proved the asymptotic optimality of bundling for a fixed distribution. Hart and Nisan circulated the first version of this paper in 2012 (EC 2012), proving Theorems A–D; the version formalized here is arXiv:1204.1846v3 (2017), published in J. Econ. Theory 172 (2017). Li and Yao (2013) later improved separate selling for i.i.d. goods to $\Theta(1/\log k)$, and Babaioff, Immorlica, Lucier and Weinberg (2014) showed that the better of separate selling and bundling is a constant-factor approximation for independent goods.

Setting

There are $k$ goods and one buyer with additive valuation $x=(x_1,\dots,x_k)\in\mathbb R_+^k$, drawn from a known distribution. A mechanism $\mu=(q,s)$ assigns to every reported valuation $x$ an allocation vector $q(x)\in[0,1]^k$ (the probabilities of receiving each good) and a payment $s(x)\in\mathbb R$. The buyer's payoff is $b(x)=q(x)\cdot x-s(x)$. The mechanism is incentive compatible (IC) if $b(x)\ge q(\tilde x)\cdot x-s(\tilde x)$ for all $x,\tilde x$, and individually rational (IR) if $b(x)\ge0$ for all $x$. For a random valuation $X$, the expected revenue is $R(\mu;X)=\mathbb E[s(X)]$ and the optimal revenue is

$$\mathrm{Rev}(X)=\sup\{R(\mu;X):\ \mu\text{ IC and IR}\}\in[0,\infty].$$

For one good, $\mathrm{Rev}(X)=\sup_{p\ge0}p\cdot\mathbb P[X\ge p]$. The bundled revenue is the one-good revenue of the total value, $\mathrm{BRev}(X)=\mathrm{Rev}(X_1+\dots+X_k)$, and the separate revenue is $\mathrm{SRev}(X)=\sum_i\mathrm{Rev}(X_i)$.

"$k$ i.i.d. goods" means that $X_1,\dots,X_k$ are independent with a common law $\nu$ on $\mathbb R_+$. Write $R_k=\mathrm{Rev}(X_1,\dots,X_k)$ and $B_k=\mathrm{BRev}(X_1,\dots,X_k)$.

Two auxiliary objects appear in the milestones. A real random variable $X$ is stochastically dominated by $Y$ if $\mathbb P[X\ge p]\le\mathbb P[Y\ge p]$ for every $p$. The equal-revenue (ER) law is that of $V\ge1$ with $\mathbb P[V\ge p]=1/p$ for $p\ge1$. The constant $w\approx0.278$ is the unique real solution of $w\,e^{w+1}=1$.

Formalization targets

Goal: Theorem D (p. 7)

$$\exists\,c>0\ \ \forall k\ge2\ \ \forall\nu:\qquad \frac{c}{\log k}\,R_k\le B_k .$$

The constant is absolute: it is chosen before $k$ and before the distribution. This is the statement as printed; it fixes neither the constant nor the base of the logarithm.

Explicit form (proof of Theorem D, p. 27)

$$R_k\le 8(w+1)(\log_2k+2)\,B_k\qquad(k\ge2).$$

Milestones

The milestones follow the paper's proof: Myerson's formula (1); monotonicity of one-good revenue under domination (Proposition 11); the ER characterization (Lemma 20) and the tail of a weighted sum of two ER goods (Lemma 21); $\mathrm{BRev}(V_1,V_2)=2(w+1)$ (Proposition 24); $\mathrm{SRev}\ge\mathrm{BRev}/(w+1)$ for two independent goods (Proposition 13 (i)); $\mathrm{BRev}\ge\mathrm{SRev}/4$ for i.i.d. goods (Proposition 14 (ii)); the decomposition Theorem 7; the power-of-two bound $R_k\le4(\log_2k+1)B_k$; monotonicity of $R_k$ and $B_k$ in $k$; and the explicit bound above.

Significance

Theorem D says that for identically distributed goods the gap between the simplest mechanism and the optimal one grows at most logarithmically in the number of goods, uniformly over all distributions, including heavy-tailed ones with infinite mean. The i.i.d. hypothesis is essential: for independent goods with different distributions bundling can recover only a $1/k$ fraction (Example 27 of the paper). Together with Theorem C (separate selling, $c/\log^2k$) it places the two simple mechanisms on a common scale, and the decomposition Theorem 7 it rests on is a general tool for independent groups of goods.

The result is proved in the paper; no machine-checked version is known to exist. A formalization adds: a Lean model of multi-good mechanisms with IC, IR and expected revenue in the extended reals; a checked version of Myerson's one-good formula for arbitrary laws on $\mathbb R_+$; the equal-revenue law and its two-good convolution; and a checked reduction from the decomposition theorem to the logarithmic bundling guarantee. Shorter arguments or a better constant are also welcome.

Difficulty

The obvious argument fails at the first step: revenue is not monotone in the valuation for two or more goods (Hart and Reny 2015), so one cannot bound $R_k$ by replacing each good by a dominating ER good. Every comparison therefore has to pass through one-dimensional quantities, and the multi-good step (Theorem 7) is a statement about expectations of a mechanism's payments conditioned on an independent block of goods. Proposition 14 (ii) must handle distributions where no optimal one-good price exists and $\mathrm{Rev}(X_i)$ may be infinite (the paper's proof speaks of "an optimal price"). Proposition 24 is an exact evaluation whose answer is defined only implicitly, through $w\,e^{w+1}=1$. The induction itself must track how block sums of i.i.d. goods are again i.i.d.

Formalization scope

Valuations are laws: a $k$-good random valuation is a probability measure on Fin k → ℝ≥0, and $k$ i.i.d. goods with law $\nu$ form Measure.pi (fun _ : Fin k => ν). Two independent groups $Y,Z$ have the product law on the disjoint union of their index types (jointLaw); the two-good statement Proposition 13 (i) uses this encoding on Unit ⊕ Unit. A mechanism is a pair of functions; the admissible class requires $q\in[0,1]^k$, IC, IR, and a measurable payment rule, the last being the without-loss-of-generality pin of the paper's footnote 12. The expected revenue of one mechanism is an EReal difference of two lower integrals, never a Bochner integral (which would be $0$ for non-integrable payments). $\mathrm{Rev}$ is a supremum in ℝ≥0∞, so infinite revenues are represented. $w$ is a real parameter with the hypothesis $w\,e^{w+1}=1$, not a Lambert-$W$ value. Logarithms are natural in Theorem D and base 2 (Real.logb 2) in the proof's explicit bounds, as printed; every statement with a logarithm keeps $k\ge2$.

The paper states Theorem D as a lower bound on an infimum of ratios $\mathrm{BRev}/\mathrm{Rev}$; the formal goal is the multiplicative inequality, which agrees with it wherever the ratio is defined and requires $\mathrm{BRev}=\infty$ when $\mathrm{Rev}=\infty$. A formalization in which $c$ may depend on $k$ or on the distribution, or in which $\mathrm{Rev}$ is computed with a Bochner integral, would trivialize the statement and is ruled out by the binder order and the definitions above.

The definitions are a mission-local copy of the model shared by this series (missions 1–5), so they can be merged later. Not posed here: Theorem C, Proposition 25, Corollary 23, Lemma 22, Example 32, the GFOR notation, and the asymptotic optimality of bundling (Appendix A.5). Proofs of any milestone are welcome, as are reusable lemmas on posted prices, stochastic domination of sums of independent variables, and binomial medians.

Selected references

• S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, J. Econ. Theory 172 (2017); preprint arXiv:1204.1846v3. https://arxiv.org/abs/1204.1846
• R. Myerson, Optimal Auction Design, Math. Oper. Res. 6 (1981) 58–73. https://doi.org/10.1287/moor.6.1.58
• M. Armstrong, Price Discrimination by a Many-Product Firm, Rev. Econ. Stud. 66 (1999) 151–168. https://doi.org/10.1111/1467-937X.00083
• Y. Bakos and E. Brynjolfsson, Bundling Information Goods: Pricing, Profits, and Efficiency, Management Sci. 45 (1999) 1613–1630. https://doi.org/10.1287/mnsc.45.12.1613
• S. Hart and P. Reny, Maximal Revenue with Multiple Goods: Nonmonotonicity and Other Observations, Theoretical Economics 10 (2015) 893–922. https://doi.org/10.3982/TE1517
• X. Li and A. C.-C. Yao, On Revenue Maximization for Selling Multiple Independently Distributed Items, PNAS 110 (2013) 11232–11237. https://doi.org/10.1073/pnas.1309533110
• M. Babaioff, N. Immorlica, B. Lucier and S. M. Weinberg, A Simple and Approximately Optimal Mechanism for an Additive Buyer, FOCS 2014. https://arxiv.org/abs/1405.6146

Why stochastic extinction matters

A population can disappear because its average growth rate is negative when it is rare, even if its deterministic dynamics would support coexistence. Interactions among several species make this harder to assess: a species may be rare while the remaining species fluctuate among several possible long-run configurations. Hening and Nguyen study this problem for nonlinear systems driven by correlated environmental Brownian noise. Their analysis treats the noncompact state space $[0,\infty)^n$, where population sizes have no fixed upper bound. The central result of this mission gives a quantitative form of approach to the boundary when one boundary community acts as a sink: the expected positive moment of the smallest population size tends to zero. The source is Hening and Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, arXiv:1704.06984v1, Theorems 1.2 and 5.1.

The population system and its boundary laws

There are $n\ge1$ species. Their abundances form $X(t)=(X_1(t),\ldots,X_n(t))\in\mathbb R^n_+=[0,\infty)^n$. Species $i$ has per capita drift $f_i(x)$ and environmental noise intensity $g_i(x)$ at state $x$. A matrix $\Gamma$ correlates the noise: $E=\Gamma^\top B$ for a vector $B$ of independent standard Brownian motions, and $\Sigma=\Gamma^\top\Gamma=(\sigma_{ij})$. The stochastic Kolmogorov system is

$$dX_i(t)=X_i(t)f_i(X(t))\,dt+X_i(t)g_i(X(t))\,dE_i(t),\qquad i=1,\ldots,n.$$

The factor $X_i$ makes the state $X_i=0$ absorbing in that coordinate. Consequently each collection of present species defines an invariant face of the orthant. The interior $\mathbb R^{n,\circ}_+=(0,\infty)^n$ consists of states where every species is present. The paper uses $\|x\|=\sum_i|x_i|$ throughout. Its standing Assumption 1.1 requires local Lipschitz coefficients, nondegenerate noise in each population subspace, and a negative large-state drift condition (1.2) expressed through positive $c_i$ and $\gamma_b$. These conditions place the same control on the unbounded part of the orthant in every theorem below. Source, §1.1, pp. 3–4.

A probability measure $\mu$ is invariant if the law of $X(t)$ remains $\mu$ when $X(0)$ has law $\mu$. It is ergodic if it is an extreme point of the invariant probability measures. Let $M$ contain the ergodic invariant measures supported on the boundary $\partial\mathbb R^n_+$. This set includes the Dirac law $\delta_*$ at zero. For any invariant $\mu$, the invasion rate of species $i$ is

$$\lambda_i(\mu)=\int\left(f_i(x)-\tfrac12\sigma_{ii}g_i(x)^2\right)\,\mu(dx).$$

The term $\sigma_{ii}g_i^2/2$ records the effect of environmental variation on logarithmic population growth. For $\mu\in M$, let $I_\mu$ be its present species and $\mathbb R^\mu_+$ its coordinate face. The set $M_\mu$ contains boundary ergodic measures supported on the boundary of that face. Assumption 1.3 requires $\lambda_i(\mu)<0$ for every $i\notin I_\mu$ and, when $I_\mu\ne\varnothing$, a positive invasion rate among $I_\mu$ for every finite convex combination of measures in $M_\mu$. Thus the missing species decline near $\mu$, while the community on its face resists collapse to a smaller face. Source, pp. 5–6.

Formalization targets

The goal is Theorem 1.2 in the explicit quantification of Theorem 5.1. Let $\delta_0>0$ satisfy the paper's bound (3.2). For every $0<\delta<\delta_0$ and every $x\in\mathbb R^{n,\circ}_+$,

$$\lim_{t\to\infty}\mathbb E_x\left(\min_{1\le i\le n}X_i(t)\right)^\delta=0.$$

This is the moment form of approach to the boundary. It does not specify which species tends to zero on a given path. The companion targets retain the paper's route: strong solutions and face invariance in Lemma 3.1, moment and Feller estimates in Lemma 3.2, zero resident invasion rates in Lemma 5.1, the weighted negative margin (5.1)–(5.2), the averaged drift bound in Lemma 5.2, local contraction in Proposition 5.1, global control in Lemma 5.3, the capped one-step bound (5.11)–(5.12), and transience in the interior. Source, §§3 and 5.

What the result gives

The conclusion detects extinction pressure without asking in advance which coordinate disappears. Since the minimum of the coordinates is small whenever the system is near any boundary face, it applies even when trajectories may approach different faces. The paper uses this result before its stronger classification theorem, which adds assumptions to determine the fate of particular species. Theorem 1.2 is proved in the cited paper; this mission seeks a machine-checked development of that known result and its supporting stochastic estimates. In particular, the formalization makes explicit how invariant measures on smaller faces control a statement about solutions starting in the full interior. Source, Theorems 1.2 and 1.3.

Where the difficulty lies

A negative invasion rate at one boundary law does not by itself control the whole trajectory. The surviving species can fluctuate toward a still smaller face, where a missing species may have a different growth rate. Assumption 1.3 excludes that obstruction by quantifying over boundary ergodic laws of the selected face. Another obstacle is unbounded population size: a local bound near the face cannot alone give convergence of expected moments. The paper combines face-specific estimates with global moment control; encoding both regimes faithfully is the main mathematical burden. The compact-state intuition cited in the paper does not immediately apply to the noncompact orthant. Source, Remark 1.6 and §5.

Formalization scope

Lean represents $\mathbb R^n$ by the published EthierKurtz.SDEState n, with coordinates indexed by Fin n from zero to $n-1$. The SDE uses the published strong Brownian solution interface; a common probability space, Brownian motion, and solution family replace the paper's notation $\mathbb P_x$ and $\mathbb E_x$. The model reads coefficients at the componentwise positive part off the orthant, where the source never evaluates them. Assumption 1.1(3)'s strict limit superior becomes an equivalent eventual negative $\varepsilon$ bound. Ergodicity is extremality. The index set $I_\mu$ is defined through positive $\mu$-mass of $x_i>0$. Finite convex combinations, rather than a closure of their hull, implement the paper's $\operatorname{Conv}$.

The stated goal requires $n\ge1$ and $\delta>0$; $\delta=0$ would make the displayed expectation equal to one. Theorem 5.1 suppresses the latter restriction, while Theorem 1.2 states it. Lemma 5.2's displayed average divides by $T$, so its $T_e$ is positive, as its proof says, despite the printed $T_e\ge0$. The weights, time threshold, and contraction exponent are chosen before the points and times over which their bounds hold. Boundary ergodic measures are not assumed to be absent; the explicit $\delta_*\in M$ target records nonemptiness. The definitions of $U_\theta$, invariant measures and invasion rates, together with finite-dimensional stochastic integration and moment estimates, are reusable beyond this mission. Contributions that establish these interfaces or prove the listed paper statements are in scope.

The radius $M$ of (3.1) is positive. The freely chosen $\delta_0$ is below one, as Appendix A uses, and the extinction weights are selected with $\sum_{i\in I_\mu}\widehat p_i\le\delta_0$. Scaling all positive weights and the margin preserves (5.2) and makes the paper's $C_U$ finite. Bounds involving real expectations explicitly include integrability, so Lean's value for a nonintegrable integral cannot satisfy them by default. The transience target applies to each compact interior set with nonempty interior, as the proof on p. 24 does.

Selected references

• Alexandru Hening and Dang H. Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, Annals of Applied Probability 28(3), 2018. Formalization uses arXiv:1704.06984v1, 23 April 2017, especially pp. 3–7, 13–14, and 20–24.

Motivation

Ecologists model interacting populations — competitors, predators and prey, food chains — by Kolmogorov systems, in which the growth of each species is proportional to its current abundance. Environmental fluctuations turn these into stochastic differential equations, and the basic question becomes which species persist and which go extinct. Hening and Nguyen (arXiv:1704.06984, Ann. Appl. Probab. 28(3), 2018) gave sharp answers for a general class of such systems on the non-compact state space $[0,\infty)^n$, extending the compact-simplex theory of Schreiber, Benaïm and Atchadé (SBA11).

The paper has three main results: persistence when every boundary ergodic measure repels (Theorem 1.1), extinction in mean when one boundary measure attracts (Theorem 1.2), and a classification of which species die out (Theorem 1.3). This mission formalizes the third. When the community does not persist, Theorem 1.3 says that each path settles near exactly one "sink" measure on the boundary, and identifies the species that vanish and their rates of decay.

Timeline: Schreiber, Benaïm and Atchadé (2011) proved persistence criteria for stochastic population models on the simplex $\{y \in \mathbb R^n_+ : y_1 + \dots + y_n = 1\}$. Evans, Hening and Schreiber (EHS15, 2015), studying patch-selection strategies in stochastic environments, extended the limit theorem for occupation measures to locally compact state spaces. Hening and Nguyen (2017/2018) proved persistence with exponential convergence and the extinction classification for general Kolmogorov systems.

Setting

Let $n \ge 1$, $\mathbb R^n_+ = [0,\infty)^n$, $\mathbb R^{n,\circ}_+ = (0,\infty)^n$, $\partial\mathbb R^n_+ = \mathbb R^n_+\setminus\mathbb R^{n,\circ}_+$, and $\|x\| = \sum_i |x_i|$. The abundances $X = (X_1,\dots,X_n)$ solve

$$dX_i(t) = X_i(t)f_i(X(t))\,dt + X_i(t)g_i(X(t))\,dE_i(t),\qquad i = 1,\dots,n,$$

where $E = \Gamma^\top B$ for an $n$-dimensional standard Brownian motion $B$, and $\Sigma = \Gamma^\top\Gamma = (\sigma_{ij})$. Assumption 1.1 asks that $(g_ig_j\sigma_{ij})$ be positive definite, that $f_i, g_i$ be locally Lipschitz, and that a dissipativity condition (1.2) with a vector $c > 0$ and a constant $\gamma_b > 0$ hold at infinity.

An invariant probability measure $\mu$ is one with $\int P(t,x,A)\,\mu(dx) = \mu(A)$ for all $t$; it is ergodic if it is an extreme point of the invariant probability measures. $\mathcal M$ is the set of ergodic invariant probability measures supported on $\partial\mathbb R^n_+$; it contains the Dirac mass $\delta^*$ at the origin. For $\mu \in \mathcal M$, $I_\mu$ is the set of species charged by $\mu$ and $I^c_\mu$ its complement. The Lyapunov exponent of species $i$ at $\mu$ is

$$\lambda_i(\mu) = \int\Big(f_i(x) - \frac{\sigma_{ii}g_i^2(x)}{2}\Big)\mu(dx).$$

A measure $\mu \in \mathcal M$ is a sink (Assumption 1.3) if $\lambda_i(\mu) < 0$ for all $i \in I^c_\mu$ and, if $I_\mu \ne \emptyset$, every finite convex combination $\nu$ of ergodic measures living on the relative boundary of the face of $\mu$ has $\max_{i\in I_\mu}\lambda_i(\nu) > 0$. $\mathcal M^1$ is the set of sinks and $\mathcal M^2 = \mathcal M\setminus\mathcal M^1$.

The occupation measures of a path are $\widetilde\Pi_t = \frac1t\int_0^t\mathbf 1_{\{X(s)\in\cdot\}}ds$, and $\mathcal U(\omega)$ is the set of weak limits of $\widetilde\Pi_t(\omega)$ as $t\to\infty$. Assumption 1.4 asks that $\|x\|^{\delta_1}\sum_ig_i^2/(1+\sum_i(|f_i|+g_i^2)) \to 0$ for some $\delta_1 > 0$; Assumption 1.5 asks that $\mathcal M^2 = \emptyset$ or that every finite convex combination $\nu$ of measures of $\mathcal M^2$ has $\max_i\lambda_i(\nu) > 0$.

Formalization targets

Goal: Theorem 1.3

Under Assumptions 1.1, 1.4, 1.5 and $\mathcal M^1 \ne \emptyset$, for every $x \in \mathbb R^{n,\circ}_+$,

$$\sum_{\mu\in\mathcal M^1} P^\mu_x = 1,\qquad P^\mu_x := \mathbb P_x\Big\{\mathcal U(\omega) = \{\mu\},\ \lim_{t\to\infty}\frac{\ln X_i(t)}{t} = \lambda_i(\mu) < 0,\ i\in I^c_\mu\Big\} > 0 .$$

Milestones

In the order the proof uses them: $\delta^* \in \mathcal M$; Lemma 3.3 (moment bound and a zero-mean identity for invariant measures); Lemma 5.1 ($\lambda_i(\mu) = 0$ for $i \in I_\mu$); Lemma 5.4 (bounded weighted time averages and a strong law for the stochastic integral); Lemma 5.5 (time spent in a compact set, and staying away from a face on a finite horizon); Lemma 5.6 (convergence of unbounded time averages); Lemma 5.7 ($\mathcal U(\omega)$ consists of invariant measures); Lemma 5.8 (a limit set inside the face of a sink is that sink); Lemma 5.9 (sinks attract nearby paths with high probability); and the case $\mathcal M^2 = \emptyset$, where $\mathcal M = \mathcal M^1 = \{\delta^*\}$.

Significance

Theorem 1.3 turns local information — the signs of finitely many Lyapunov exponents at boundary ergodic measures — into a global almost-sure description of long-run behaviour: the community converges, in the sense of empirical distributions, to one of the sinks, each sink is reached with positive probability, and the species absent from it decay exponentially at explicit rates. In the applications of §2 of the paper (competitive Lotka–Volterra systems, food chains) this answers which species survive.

The theorem is proved on paper. No part of it is machine-checked. A formalization would produce a checked interface between Itô calculus for multidimensional SDEs, ergodic theory of Feller processes (occupation measures, invariant and ergodic measures), and the stochastic-persistence framework; the statements of Lemmas 5.4–5.7 are reusable for other SDE models with a Lyapunov-type condition.

Difficulty

The obvious argument — the occupation measures converge to some invariant measure, and the Lyapunov exponents at that measure decide the fate of each species — breaks down at two points. First, the state space is not compact and the functions $f_i - \sigma_{ii}g_i^2/2$ are unbounded, so weak convergence of occupation measures does not by itself give convergence of time averages of these functions; a pathwise uniform-integrability bound (Lemmas 5.4 and 5.6) is required, and this is where Assumption 1.4 enters. Second, a limit point of occupation measures is in general a mixture of ergodic measures, possibly including repellers; ruling out every mixture that is not a single sink requires the separate arguments of Lemma 5.8 and of the $\mathcal M^2$ step, together with a supermartingale built from a Lyapunov function near each sink (Lemma 5.9).

Formalization scope

The state space is EuclideanSpace ℝ (Fin n) with the published Ethier–Kurtz strong-SDE layer; coordinates are indexed by Fin n, the norm in every assumption is the $\ell^1$ norm, and $n \ge 1$ is a hypothesis. The process is a family of strong solutions $X^x$, one from each $x \in \mathbb R^n_+$, driven by one Brownian motion on one probability space. The coefficients are read at the positive part of the state, which is the state itself on $\mathbb R^n_+$. Ergodic means extremal among invariant probability measures, $I_\mu$ is the set of coordinates that are not $\mu$-a.s. zero, $\mathrm{Conv}$ means finite convex combinations with positive weights (as on p. 5), and weak limits are taken along sequences, tested against bounded continuous functions. The sum in (1.11) is an unconditional sum in $[0,\infty]$ over the set $\mathcal M^1$, with no finiteness assumption.

Deviations from the page, each disclosed in the item: (5.19) is stated for every finite horizon rather than for $n_eT_e$, which is undefined under the lemma's hypotheses; Lemma 5.9 takes $k \ge 1$; the convention $\delta_1 \le \delta_0$ of Assumption 1.4 is an explicit hypothesis where the exponent $\delta_1$ appears; integrability claims that the paper treats as automatic are part of the conclusions; and (5.17) is stated for every continuous version of the Itô integral. Lemma 5.6 is stated for each path that stays in the orthant, which the solution does almost surely. The proof's claim "$\mathcal U(\omega) \subset \mathrm{Conv}(\mathcal M)\setminus\mathrm{Conv}(\mathcal M^2)$" is left as source context: its inclusion in the finite convex hull of $\mathcal M$ requires an additional argument when $\mathcal M$ is infinite.

The statements cannot be made vacuous by the definitions: $\delta^* \in \mathcal M$ is itself a milestone, so $\mathcal M$ is never empty, and the occupation measures are probability measures for $t > 0$; every constant ($\widehat K$, $\widehat K_1$, $\beta$, $\Delta$) is chosen before the points it must be uniform in.

A complete development needs Itô's formula for $\ln X_i$, the strong law for continuous martingales with bounded quadratic-variation growth, Prokhorov's theorem and lower semicontinuity of integrals under weak convergence, and the Feller and strong Markov properties of (1.1). Contributions of any of these, and of the milestones in any order, are welcome.

Selected references

• A. Hening, D. H. Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, Ann. Appl. Probab. 28(3), 2018, DOI 10.1214/17-AAP1347; arXiv:1704.06984v1. https://arxiv.org/abs/1704.06984
• S. J. Schreiber, M. Benaïm, K. A. S. Atchadé, Persistence in fluctuating environments, J. Math. Biol. 62(5), 655–683, 2011. MR 2786721, https://mathscinet.ams.org/mathscinet-getitem?mr=2786721
• S. N. Evans, A. Hening, S. J. Schreiber, Protected polymorphisms and evolutionary stability of patch-selection strategies in stochastic environments, J. Math. Biol. 71(2), 325–359, 2015. MR 3367678, https://mathscinet.ams.org/mathscinet-getitem?mr=3367678
• R. Khasminskii, Stochastic Stability of Differential Equations, 2nd ed., Springer, 2012. MR 2894052, https://mathscinet.ams.org/mathscinet-getitem?mr=2894052

Motivation

A seller who owns several goods and faces buyers with private values must decide how to sell them. The revenue-maximizing mechanism is known in closed form only for one good: for a single buyer it is a posted price, and for several buyers it is Myerson's optimal auction (Myerson 1981). With two or more goods the optimal mechanism may use lotteries, may be impossible to describe compactly, and may behave non-monotonically in the value distribution. This makes simple mechanisms with provable revenue guarantees the practical question: how much of the optimal revenue does a seller lose by selling each good separately with its own optimal one-good mechanism?

Hart and Nisan (arXiv:1204.1846v3) answer this for one buyer and two independent goods (their Theorem A): selling separately earns at least half of the optimal revenue. Their Theorem 18 (p. 29), proved in Appendix A.7 as Theorems 33 and 34, extends the factor $\tfrac12$ to any number $n$ of buyers. This mission formalizes the dominant-strategy half, Theorem 33, in which the buyers may be arbitrarily correlated with one another, as long as the two goods are independent.

Setting

One seller sells $k$ goods to $n \ge 1$ buyers. Buyer $j$'s value for good $i$ is a number $x^j_i \ge 0$; a valuation profile is $x = (x^j_i) \in \mathbb R^{kn}_+$, and $x^j = (x^j_i)_i$ is buyer $j$'s valuation vector. The profile is random, $X$, with a commonly known joint law.

A mechanism $\mu = (q^j, s^j)_{j=1,\dots,n}$ gives each buyer $j$ an allocation $q^j(x) \in [0,1]^k$ (the probability that $j$ receives each good) and a payment $s^j(x) \in \mathbb R$, as functions of the reported profile, subject to feasibility: $\sum_j q^j_i(x) \le 1$ for every good $i$. Buyer $j$'s payoff is $b^j(x) = q^j(x)\cdot x^j - s^j(x)$, and the seller's revenue is $S(x) = \sum_j s^j(x)$.

• IC-DS (dominant-strategy incentive compatibility): $b^j(x) \ge q^j(\tilde x^j, x^{-j})\cdot x^j - s^j(\tilde x^j, x^{-j})$ for every buyer $j$, every profile $x$ and every report $\tilde x^j$, where $(\tilde x^j, x^{-j})$ replaces $j$'s vector in $x$ by $\tilde x^j$.
• IR-DS: $b^j(x) \ge 0$ for every $j$ and $x$.
• NPT (no positive transfer): $s^j \ge 0$.

The expected revenue is $R(\mu; X) = \mathbb E[S(X)]$, and

$$\mathrm{Rev}^{DS}(X) = \sup\{R(\mu;X) : \mu \text{ feasible, IC-DS and IR-DS}\} \in [0, \infty].$$

For two goods write $Y = X_1 = (X^j_1)_j$ and $Z = X_2 = (X^j_2)_j$ for the vectors of the buyers' values for good 1 and good 2, so $X = (Y, Z)$. $\mathrm{Rev}^{DS}(Y)$ is the optimal dominant-strategy revenue from good 1 alone, sold to the same $n$ buyers. Finally $a^{(1)} = \max_j a^j$.

Formalization targets

Goal: Theorem 33 (p. 49)

If $Y$ and $Z$ are independent, then

$$\mathrm{Rev}^{DS}(X_1) + \mathrm{Rev}^{DS}(X_2) \ge \tfrac12\,\mathrm{Rev}^{DS}(X_1, X_2).$$

No independence among buyers is assumed: the values $X^1_i, \dots, X^n_i$ for the same good may have any joint law.

Milestones (the steps of the paper's proof)

1. Remark (b) of A.7 (p. 48): an IC-DS, IR-DS mechanism is NPT iff $s^j(0, x^{-j}) = 0$ for all $j$, $x^{-j}$, and NPT is without loss of generality for $\mathrm{Rev}^{DS}$.
2. Remark (b), subdomain property (p. 48): $\mathbb E[\sum_j s^j(X)\mathbf 1_{X\in A}] \le \mathrm{Rev}^{DS}(X\mathbf 1_{X\in A}) \le \mathrm{Rev}^{DS}(X)$.
3. Display (21) (p. 50): $z^{(1)}\,\mathbb P[Y^{(1)} \ge z^{(1)}] \le \mathrm{Rev}^{DS}(Y)$.
4. The marginal mechanism (p. 50): for fixed second-good values $z$, $\hat q^j(y) = q^j_1(y,z)$, $\hat s^j(y) = s^j(y,z) - q^j_2(y,z)z^j$ is feasible, IC-DS and IR-DS.
5. Display (19) (p. 49): $\mathbb E[S(Y,Z)\mathbf 1_{Y^{(1)} \ge Z^{(1)}}] \le 2\,\mathrm{Rev}^{DS}(Y)$ for an NPT, IC-DS, IR-DS mechanism.

Companion: Theorem 34 (p. 49)

With $n$ independent buyers and two independent goods, so that all $2n$ values are independent (footnote 27), the same inequality holds for Bayesian Nash implementation: $\mathrm{Rev}^{BN}(X_1) + \mathrm{Rev}^{BN}(X_2) \ge \tfrac12\mathrm{Rev}^{BN}(X_1, X_2)$.

Significance

The result. Theorem 33 shows that the factor-$\tfrac12$ guarantee of separate selling does not depend on there being a single buyer, nor on the buyers being independent, provided incentive compatibility is required in dominant strategies. It reduces a two-good, $n$-buyer design problem, whose optimum is not characterized, to two one-good problems, each of which can be handled by known single-good auction theory. Remark (a) on p. 29 records that the dominant-strategy statement holds for correlated buyers, while Remark (b) there explains, via Crémer and McLean (1988), why the Bayesian Nash analogue cannot be extended to correlated buyers.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. A formal proof requires multi-agent mechanisms on $\mathbb R^{kn}_+$, the Lebesgue integral of a possibly non-integrable revenue, conditioning on an independent coordinate of a product law, and the subdomain property of Remark (b). The definitions here (feasible multi-buyer mechanisms, IC-DS, IR-DS, $\mathrm{Rev}^{DS}$, and the Bayesian Nash counterparts) are reusable for any multi-buyer revenue-maximization result.

Difficulty

The obvious first idea is to apply the one-buyer Theorem A buyer by buyer. It fails: the feasibility constraint $\sum_j q^j_i \le 1$ couples the buyers, so a multi-buyer mechanism does not decompose into single-buyer mechanisms, and the revenue extracted from one buyer depends on the reports of all the others. Any reduction to one-good problems must produce, from a two-good mechanism, one-good mechanisms that remain feasible and dominant-strategy incentive compatible for every buyer at once. On the measure-theoretic side, payments of an incentive compatible mechanism may be negative and non-integrable, so expectations must be handled in the extended reals, and the passage from bounds that hold for each fixed value of one good to a bound in expectation needs the product structure of the law of $(Y, Z)$.

Formalization scope

• A profile is x : Fin n → ι → ℝ≥0 (x j i $= x^j_i$); a random profile is given by its law, a probability measure on that space. One good is ι = Unit, two goods are ι = Fin 2 (good 1 is index 0). The law of two independent goods is twoGoodsN μY μZ, the image of the product law $\mu_Y\otimes\mu_Z$; μY and μZ are arbitrary probability laws on $\mathbb R^n_+$, so correlation among buyers is allowed.
• $(\tilde x^j, x^{-j})$ is Function.update x j x'. Feasibility $\sum_j q^j_i \le 1$ is part of admissibility; without it a mechanism could sell each good to every buyer.
• Payments are required measurable (the paper's footnote 12). $R(\mu;X)$ is the EReal difference of the integrals of $S^+$ and $S^-$, never a Bochner integral, which would vanish on non-integrable revenues. $\mathrm{Rev}^{DS}$ takes values in $[0,\infty]$.
• The subdomain property requires the set $A$ to be measurable, so that the law of $X\mathbf 1_{X\in A}$ is defined. It also requires the signed expectation on $A$ to be defined: at least one of its positive and negative part integrals must be finite. The hypothesis $n \ge 1$ is the paper's.
• For Theorem 34, buyers are independent with laws $\rho_j$; interim payoffs integrate over the others' product law, and allocations as well as payments are required measurable.
• The constant $\tfrac12$ is stated exactly as printed. A statement over an arbitrary joint law with given marginals, or with the feasibility constraint dropped, would be a different (and false, or trivial) theorem.

Contributions of every kind are welcome: proofs of the milestones, of Theorem 34, and general lemmas on multi-buyer mechanisms.

Selected references

• S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, arXiv:1204.1846v3, 2017; J. Economic Theory 172 (2017). https://arxiv.org/abs/1204.1846
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6 (1981), 58–73. https://doi.org/10.1287/moor.6.1.58
• J. Crémer and R. P. McLean, Full Extraction of the Surplus in Bayesian and Dominant Strategy Auctions, Econometrica 56 (1988), 1247–1257. https://doi.org/10.2307/1913096
• S. Hart and P. J. Reny, Maximal Revenue with Multiple Goods: Nonmonotonicity and Other Observations, Theoretical Economics 10 (2015), 893–922. https://doi.org/10.3982/TE1517