All missions

Motivation

Fractional Brownian motion (fBM) is the standard Gaussian model of long-range dependence and rough paths. It appears in network traffic, finance (rough volatility), hydrology and queueing, and it drives a class of stochastic differential equations whose solutions are defined pathwise by Young integration. Simulating such models needs sample paths of fBM, and an error guarantee in the strongest sense: a path that lies within a prescribed distance $\varepsilon$ of the true one, with probability one, on a finite computer. This guarantee is $\varepsilon$-strong simulation.

The concept was introduced for Brownian motion by Beskos, Peluchetti and Roberts (Bernoulli 2012) and extended to reflected Brownian motion by Blanchet and Chen (AAP 2015) and to multidimensional Brownian-driven SDEs by Blanchet, Chen and Dong (AAP 2017), whose "record-breaker" strategy this paper adopts. For $H\ne 1/2$ the coefficients of Lévy's midpoint-displacement expansion are correlated and the earlier arguments do not apply. Chen, Dong and Ni (arXiv:1902.07824, 2019; Mathematics of Operations Research, 2021) extend the method to fBM of every Hurst index. The central fact is that, along the dyadic midpoint-displacement expansion, only finitely many levels "break a record", the last such level has finite exponential moments, and beyond it the remaining error is controlled deterministically. This mission formalizes that fact.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathbb P)$ and a Hurst index $H\in(0,1)$. A fractional Brownian motion on $[0,1]$ is a family of random variables $\{B(t)\}_{t\in[0,1]}$ that is a centered Gaussian process with covariance (1.1)

$$r(s,t)=\mathbb E[B(s)B(t)]=\tfrac12\big(|s|^{2H}+|t|^{2H}-|s-t|^{2H}\big).$$

At $H=1/2$ this is $\min(s,t)$, Brownian motion.

The dyadic grid of level $n$ is $D_n=\{t^n_i=i/2^n:\ i=0,\dots,2^n\}$. The dyadic discretization $B_n$ is the piecewise-linear interpolation of the values $B(t^n_0),\dots,B(t^n_{2^n})$. Passing from level $k-1$ to level $k$ adds the midpoints $t^k_{2j+1}$, and the midpoint displacement at the new point is $a^k_j-b^k_j$, where (3.1)

$$a^k_j=B(t^k_{2j+1}),\qquad b^k_j=\tfrac12\big(B(t^{k-1}_j)+B(t^{k-1}_{j+1})\big),\qquad j=0,\dots,2^{k-1}-1 .$$

Fix $\delta\in(0,H)$ and $\rho>0$, and put $\ell_k=2^{-(H-\delta)k}$. A record is broken at level $k\ge1$ if (3.11)

$$\max_{0\le j\le 2^{k-1}-1}|a^k_j-b^k_j|\ \ge\ \rho\,\ell_k ,$$

and $N=\sup\{k\ge1:\text{a record is broken at level }k\}$ is the last record level ($\sup\emptyset=0$, and $N=\infty$ if records occur at infinitely many levels). Theorem 3.1 also uses $K(\nu)=\sup\{n\ge1:4\sqrt n>\nu\,2^{\delta n}\}$ (3.2).

Formalization targets

Goal: Theorem 3.6 (p. 12)

Assume the paths of $B$ are almost surely continuous on $[0,1]$. For every $\delta\in(0,H)$, $\rho>0$ and $t>0$,

$$\mathbb E\big[e^{tN}\big]<\infty,$$

and almost surely, for every $n>N$,

$$\sup_{s\in[0,1]}|B(s)-B_n(s)|\ \le\ \frac{\rho\cdot2^{-(H-\delta)(n+1)}}{1-2^{-(H-\delta)}} .$$

Milestones

1. Sup-norm identity (display after (3.1), p. 8): $\|B_k-B_{k-1}\|_\infty=\max_j|a^k_j-b^k_j|$, for every path.
2. Lemma 3.2 (p. 9): the conditional variance of $a^k_j$ given the values on $D_{k-1}$ is at most $2\cdot2^{-2kH}$.
3. Borell–TIS inequality (finite form, cited at (3.6), p. 9): for a centered Gaussian vector with coordinate variances $\le\sigma^2$, $\mathbb P(\max_i|X_i|-\mathbb E\max_i|X_i|>u)\le e^{-u^2/(2\sigma^2)}$.
4. Lemma 3.3 (p. 10): $\mathbb E[\max_{i\le n}|X_i|]\le2\sqrt{2\log(2n)}\,\sigma$ for centered Gaussians with variances $\le\sigma^2$.
5. Lemma 3.4 (p. 11): $\operatorname{Var}(c^k_j-b^k_j)\le2\cdot2^{-2kH}$, with $c^k_j=\mathbb E[a^k_j\mid B^H_{k-1}]$.
6. Theorem 3.1 (p. 8): for $\nu,\nu^*>0$, $\rho=2(\nu+\nu^*)$ and $k>K(\nu)$,

$$\mathbb P\Big(\max_j|a^k_j-b^k_j|\ge\rho\ell_k\Big)\le2\exp\{-\nu^{*2}\cdot2^{2k\delta-2}\}.$$

7. $N<\infty$ almost surely (proof of Theorem 3.5, pp. 11–12).
8. Theorem 3.5 (p. 11): $B_n$ converges almost surely, uniformly on $[0,1]$, to a continuous fBM that is a modification of $B$.

A companion statement after the goal records the truncation rule of Algorithm 1 (p. 14): with $N(\varepsilon)=\max\{N,\lceil\log_2(\rho(\varepsilon(1-2^{-(H-\delta)}))^{-1})/(H-\delta)\rceil\}$, $\|B-B_{N(\varepsilon)}\|_\infty\le\varepsilon$ almost surely.

Significance

The result. Theorem 3.6 supplies both conditions of the record-breaker scheme: the last record level is finite with a light tail (so an algorithm that searches for it terminates with finite expected effort), and beyond it the truncation error is bounded by an explicit, deterministic quantity. Together they give an exact $\varepsilon$-accurate path in finite time, the basis of the paper's simulation algorithm for fBM and, through the Hölder-norm analogue (Theorem 3.8), of its Euler scheme for fBM-driven Young SDEs and its unbiased multilevel Monte Carlo estimators. Theorem 3.5 is the almost-sure validity of Lévy's midpoint-displacement series for fBM with correlated coefficients.

Formalizing it. The results are proved in the paper; none of them is machine-checked. The mission produces a formal model of fBM on $[0,1]$, its dyadic discretizations and the record-breaker level, together with two general Gaussian tools that are absent from Mathlib: the Borell–TIS inequality for finitely many correlated Gaussians and an upper bound on the expected maximum of Gaussians. Both are reusable well beyond this paper (suprema of Gaussian processes, chaining, high-dimensional statistics).

Difficulty

For Brownian motion the midpoint displacements are independent of the coarser levels and of each other, and every step is a computation with independent normal variables. For $H\ne1/2$ that independence is lost: given the values on $D_{k-1}$, the new value $a^k_j$ is neither centered at $b^k_j$ nor independent of the other new values, and the bounds must hold for a maximum over $2^{k-1}$ correlated coordinates with constants uniform in $k$. Two ingredients carry the weight, and Mathlib has neither:

• Gaussian concentration of the maximum. The Borell–TIS inequality for correlated Gaussians, and the Gaussian log-Sobolev or Poincaré machinery that usually proves it.
• Gaussian conditioning. For $H\ne1/2$ the values at the new midpoints depend on all values at the previous level, not only on the two neighbours, so the conditional variance and the bias of Lemmas 3.2 and 3.4 are statements about Gaussian conditional expectations, for which Mathlib has no regression formula.

Beyond these, Theorem 3.5 requires constructing the limit process and identifying its finite-dimensional laws, and the exponential moment in Theorem 3.6 requires a tail for $N$ that decays faster than any exponential.

Formalization scope

• Model. $B:\mathbb R\to\Omega\to\mathbb R$, of which only the times in $[0,1]$ are constrained. The predicate "fBM with Hurst index $H$" requires each $B(t)$ to be measurable, $\{B(t)\}_{t\in[0,1]}$ to be a Gaussian process (Mathlib's IsGaussianProcess), $\mathbb E[B(t)]=0$ and $\operatorname{Cov}(B(s),B(t))=r(s,t)$ exactly as in (1.1). Everywhere $0<H<1$ and $0<\delta<H$.
• Continuity. The paper fixes the continuous modification of fBM once (p. 5). The goal and the companion assume almost-sure continuity of the paths on $[0,1]$; Theorem 3.5 assumes nothing about paths and constructs the continuous limit.
• The last record level is valued in $\mathbb N\cup\{\infty\}$, and $e^{tN}$ in $[0,\infty]$ with $e^{t\cdot\infty}=\infty$. A natural-number supremum, which Lean sets to $0$ on unbounded sets, would make the exponential moment trivially finite on exactly the bad paths; this encoding rules that out.
• $\rho$. Theorem 3.1 has $\rho=2(\nu+\nu^*)$; the goal admits every $\rho>0$, which is the same family.
• Conditioning on $B^H_{k-1}$ is conditioning on the $\sigma$-algebra generated by the values on $D_{k-1}$; Lemma 3.2 uses Mathlib's conditional variance (an almost-sure statement), and Lemma 3.4 states the diagonal of $\Sigma^{(k)}$ as $\operatorname{Var}(c^k_j-b^k_j)$, which is how p. 11 describes it.
• Sup norms are stated pointwise for every $s\in[0,1]$, or as an attained maximum, never as a real supremum.
• Printed constants are kept: $2\cdot2^{-2kH}$ (Lemmas 3.2, 3.4), $2\sqrt{2\log(2n)}\,\sigma$ (Lemma 3.3, natural logarithm), $2\exp\{-\nu^{*2}2^{2k\delta-2}\}$ (Theorem 3.1). The paper's display (3.6) contains a sign slip in the exponent; the Borell–TIS milestone states the inequality the citation names.

A formalization in which $N$ is defined as the level beyond which the error bound already holds, or in which the absence of records beyond $N$ is assumed, would make Theorem 3.6 definitional; $N$ here is computed from the path as the supremum of the record set.

Out of scope: the algorithms that sample $N$ (Algorithms 2–5, Theorems 4.6–4.8), the Hölder-norm results (Lemma 3.7, Theorem 3.8) and the SDE section. Contributions of general Gaussian infrastructure (Gaussian conditioning, Borell–TIS, expected-maximum bounds) are especially welcome.

Selected references

• Y. Chen, J. Dong, H. Ni, ε-Strong simulation of fractional Brownian motion and related stochastic differential equations, arXiv:1902.07824v1, 2019; Mathematics of Operations Research, 2021. https://arxiv.org/abs/1902.07824
• J. Blanchet, X. Chen, Steady-state simulation for reflected Brownian motion and related networks, Annals of Applied Probability 25(6), 2015. https://doi.org/10.1214/14-AAP1072
• A. Beskos, S. Peluchetti, G. Roberts, ε-Strong simulation of the Brownian path, Bernoulli 18(4), 2012. https://doi.org/10.3150/11-BEJ383
• J. Blanchet, X. Chen, J. Dong, ε-Strong simulation for multidimensional stochastic differential equations via rough path analysis, Annals of Applied Probability 27(1), 2017. https://doi.org/10.1214/16-AAP1214
• R. J. Adler, J. E. Taylor, Random Fields and Geometry, Springer, 2007 (Borell–TIS inequality, Theorem 2.1.1). https://doi.org/10.1007/978-0-387-48116-6
• B. B. Mandelbrot, J. W. Van Ness, Fractional Brownian motions, fractional noises and applications, SIAM Review 10(4), 1968. https://doi.org/10.1137/1010093

Motivation

Zero-sum stochastic games model two opponents who interact over a finite set of states, each state being a matrix game whose outcome also decides the next state. Since Shapley (1953), every such game with discount factor $\lambda\in(0,1]$ has a value $v_\lambda^k$ at each initial state $k$, characterised as the fixed point of a contraction. The value is the basic quantity of the theory, both for the discounted game and for its limits as $\lambda\to0$, and computing it, or describing what kind of number it is, is a long-standing question in game theory and operations research.

A short history of the algebraic side of the question:

• 1950: Shapley and Snow describe the extreme optimal strategies of a matrix game through square sub-matrices and their cofactors.
• 1953: Shapley proves existence of $v_\lambda$ as the unique fixed point of the Shapley operator.
• 1976: Bewley and Kohlberg use Tarski–Seidenberg to show that $\lambda\mapsto v_\lambda$ is semi-algebraic and admits a Puiseux expansion near $0$; the degree of the algebraic equation is not controlled.
• 2018: Attia and Oliu-Barton (A solution for stochastic games, arXiv e-print, reference [2] of the paper) characterise $v^k_\lambda$ as the unique zero of $w\mapsto\mathrm{val}((-1)^n(\Delta^k-w\Delta^0))$, with $n+1$ auxiliary matrices built from a Kronecker determinant.
• 2021: the present paper (arXiv:1810.08798v2, Mathematics of Operations Research 46(3)) refines this with Shapley–Snow kernels and the theory of multiparameter eigenvalue problems, and obtains an explicit univariate polynomial with $v^k_\lambda$ as a root, of degree bounded by a rank.

Setting

A stochastic game has states $K=\{1,\dots,n\}$, finite nonempty action sets $I_k$, $J_k$ at state $k$, a payoff $g(k,i,j)\in\mathbb R$, transition probabilities $q(\ell\mid k,i,j)\ge0$ with $\sum_\ell q(\ell\mid k,i,j)=1$, and a discount factor $\lambda\in(0,1]$.

A real matrix $A$ is a matrix game: the row player picks a mixed strategy $x$, the column player a mixed strategy $y$, and the row player receives ${}^txAy$. Its value $\mathrm{val}(A)$ is the number that each player can guarantee. For $z\in\mathbb R^n$, the local game $\mathcal G^k(\lambda,z)$ has entries $\lambda g(k,i,j)+(1-\lambda)\sum_\ell q(\ell\mid k,i,j)z^\ell$, and the discounted value $v_\lambda\in\mathbb R^n$ is the unique solution of $\mathrm{val}(\mathcal G^k(\lambda,v_\lambda))=v^k_\lambda$ for all $k$.

The data array $D(\lambda)$ is the $n\times(n+1)$ array of matrices $M^k_0=\lambda G^k$, $M^k_k=(1-\lambda)Q^k_k-U$ and $M^k_\ell=(1-\lambda)Q^k_\ell$ for $\ell\neq k$, where $G^k=(g(k,i,j))$, $Q^k_\ell=(q(\ell\mid k,i,j))$ and $U$ is a matrix of ones. The Kronecker determinant of an $n\times n$ array of matrices replaces products of scalars by Kronecker products; entrywise, its entry at rows $(i_1,\dots,i_n)$ and columns $(j_1,\dots,j_n)$ is $\det\big(A_{k\ell}^{i_kj_k}\big)_{k,\ell}$. The auxiliary matrices are $\Delta^\ell=(-1)^\ell\det_\otimes D^{(\ell)}(\lambda)$, where $D^{(\ell)}$ deletes column $\ell$, for $0\le\ell\le n$.

A Shapley–Snow kernel of a matrix game $G$ is a square sub-matrix $\dot G$ with $S(\mathrm{co}(\dot G))\neq0$ whose cofactor strategies $\mathrm{co}(\dot G)\mathbf 1/S(\mathrm{co}(\dot G))$ and ${}^t\mathrm{co}(\dot G)\mathbf 1/S(\mathrm{co}(\dot G))$, completed by zeros, are optimal in $G$; $\mathrm{co}$ is the cofactor matrix and $S$ the sum of entries. Choosing a kernel $\dot I_k\times\dot J_k$ of every local game $\mathcal G^k(\lambda,v_\lambda)$ and restricting each $M^k_\ell$ to it gives the reduced array $\dot D(\lambda)$, with square auxiliary matrices $\dot\Delta^0,\dots,\dot\Delta^n$.

Formalization targets

Goal: Theorem 3.4.2

For every state $k$ and every choice of kernels:

$$\text{(i) } v^k_\lambda \text{ is the unique } w\in\mathbb R \text{ with } \mathrm{val}(\dot\Delta^k-w\dot\Delta^0)=0;\qquad \text{(ii) } \mathrm{rank}(\dot\Delta^k-v^k_\lambda\dot\Delta^0)<\max_{w\in\mathbb R}\mathrm{rank}(\dot\Delta^k-w\dot\Delta^0);$$

(iii) some nonzero polynomial $P^k$ of degree at most $\mathrm{rank}(\dot\Delta^0)$, the determinant of a square sub-matrix of $\Delta^k-w\Delta^0$, vanishes at $v^k_\lambda$; (iv) if all entries of $D(\lambda)$ are rational, then

$$[\mathbb Q(v^k_\lambda):\mathbb Q]\le\mathrm{rank}(\dot\Delta^0).$$

Milestones

In attack order: Shapley's fixed-point theorem (§2.1); the sign of $\Delta^0$ (Lemma 2.2.3) and unique solvability of $\mathrm{val}(A-wB)=0$ (Remark 2.2.4); the Shapley–Snow theorem (Theorem 2.3.1) and existence of kernels (§3.1); the cofactor lemmas B1–B3 and Proposition 2.3.4 on the kernel of $\dot G-v\dot U$; the rank-drop criterion (Lemma C1), the tensor kernel vector (Lemma C2) and Proposition 2.4.4; Proposition 3.2.1 placing $v_\lambda$ in the reduced solution sets; Proposition 3.4.1, the characterising polynomial.

Significance

The result. Theorem 3.4.2 turns the computation of a discounted value into univariate root finding: $v^k_\lambda$ is a root of one of finitely many explicit polynomials, read off from $D(\lambda)$, of degree bounded by $\mathrm{rank}(\dot\Delta^0)\le\prod_k\min(|I_k|,|J_k|)$. Part (iv) gives an explicit bound on the algebraic degree of the value of a rational game, a quantity that the semi-algebraic approach leaves uncontrolled. The same polynomials yield, in §4 of the paper, the convergence of $v_\lambda$ as $\lambda\to0$ and a bound on its rate. These are not part of this mission.

Formalizing it. The theorem is proved in the paper; no part of it is machine-checked. A complete development formalizes the value of a matrix game on arbitrary finite action sets, Shapley's fixed point, the Shapley–Snow description of extreme optimal strategies, Kronecker determinants of arrays of matrices, and the singular multiparameter-eigenvalue lemmas of Muhič–Plestenjak and Atkinson. Each of these is reusable outside stochastic games.

Difficulty

The obvious route is Cramer's rule for the multiparameter system $\det(M^k_0+z^1M^k_1+\dots+z^nM^k_n)=0$: when $\Delta^0$ is invertible, the solutions are the eigenvalues of $\Delta^k(\Delta^0)^{-1}$. Here $\Delta^0$, and still more $\dot\Delta^0$, is in general singular, and the polynomials $\det(\dot\Delta^k-w\dot\Delta^0)$ may vanish identically, so the determinant equation carries no information. The value must instead be located through a rank drop of the pencil. Proving the rank drop requires nonzero left and right kernel vectors with ${}^tx\dot\Delta^0y\neq0$, which come from the sign of $\Delta^0$ (Lemma 2.2.3) and from nonnegative kernel strategies of the Shapley–Snow kernels transported through Kronecker products. Neither ingredient is available off the shelf.

A second obstacle is the paper's degree argument: it quotes the degree of $\det(A+wB)$ as equal to $\mathrm{rank}(B)$, which is false in general; only the inequality holds and is posed.

Formalization scope

• Model. States are Fin n with $n\ge1$. The action sets I k, J k are finite, nonempty and may depend on the state, as in §4, p. 20, where the paper extends its results "word for word" to that case. The transition probabilities are nonnegative and sum to one, and 0 < lam ≤ 1.
• Value. The value of a matrix game is the relation IsMatVal A w: optimal strategies of both players guarantee $w$. No supremum or infimum over strategy sets is taken. $v_\lambda$ is any $v$ with IsShapleyFixed g q lam v; the milestone shapley_fixed_point gives existence and uniqueness, so the goal is not vacuous.
• Kernels. A kernel is given by embeddings Fin s ↪ I, Fin s ↪ J. IsSSK requires $S(\mathrm{co}(\dot G))\neq0$ and optimality of the completed cofactor strategies. The paper also requires the pair to be basic, but by Theorem 2.3.1 this is equivalent.
• Linear algebra. co M is the transposed adjugate. The Kronecker determinant is defined through its entry formula (K5), and rows and columns of $\Delta^\ell$ are indexed by tuples instead of lexicographic integers. Column $0$ of the array is the paper's $\ell=0$, and the paper's $\Delta^k$ is Delta … k.succ. "$\max_w\mathrm{rank}$" means "some real $w$ gives larger rank". The sets $S^M,S^\Delta$ accept complex vectors in Lemma C2, as in §2.4; $S^R,T^M$ are used over $\mathbb R^n$ in the game results. Proposition 3.4.1 takes its polynomial from a determinant of a reduced-pencil submatrix, as the proof constructs.
• Conventions. Part (i) is the printed form, without the $(-1)^n$ of Result 1 (i); both hold for the square reduced matrices. Part (iv) is IsAlgebraic ℚ v ∧ (minpoly ℚ v).natDegree ≤ rank.

The goal ranges over Shapley–Snow kernels, not over arbitrary square sub-matrices, and $E^k$ is built from the full $\Delta^k-w\Delta^0$ with only its degree cap taken from $\dot\Delta^0$. A formalization in which kernels are arbitrary square sub-matrices, or in which $E^k$ is built from $\dot\Delta$, states a different theorem.

Contributions are welcome at every level. In particular: the value of a matrix game on Fintype index types with existence and uniqueness, Shapley's contraction, the Shapley–Snow theorem, the Kronecker determinant and its column-alternation property (K3), and the bound $\deg\det(A+wB)\le\mathrm{rank}(B)$.

Selected references

• L. Attia, M. Oliu-Barton, Shapley–Snow kernels, multiparameter eigenvalue problems and stochastic games, Mathematics of Operations Research 46(3), 2021; arXiv:1810.08798v2. https://arxiv.org/abs/1810.08798v2
• L. Attia, M. Oliu-Barton, A solution for stochastic games, arXiv e-print, 2018 (reference [2] of the paper).
• L. S. Shapley, Stochastic games, PNAS 39(10), 1953. https://doi.org/10.1073/pnas.39.10.1095
• L. S. Shapley, R. N. Snow, Basic solutions of discrete games, Contributions to the Theory of Games I (Annals of Mathematics Studies 24), 1950, pp. 27–35.
• T. Bewley, E. Kohlberg, The asymptotic theory of stochastic games, Mathematics of Operations Research 1(3), 1976. https://doi.org/10.1287/moor.1.3.197
• A. Muhič, B. Plestenjak, On the singular two-parameter eigenvalue problem, Electronic Journal of Linear Algebra 18, 2009, pp. 420–437.
• F. V. Atkinson, Multiparameter Eigenvalue Problems, vol. 1, Academic Press, 1972.
• J. W. Demmel, Applied Numerical Linear Algebra, SIAM, 1997 (cited for the degree of $\det(A+wB)$).

Motivation

When a bank or fund in distress must sell a large position, the price it receives depends on how much it sells: the market's capacity to absorb the sale is finite. Models of fire sales and systemic risk (for instance Cifuentes, Shin and Ferrucci and Amini, Filipović and Minca) encode this through an inverse demand function, the price per unit as a function of the quantity liquidated. In most of this literature the inverse demand function is postulated exogenously, typically linear or exponential.

Bichuch and Feinstein (arXiv:2012.08002v3, 2022; Operations Research) derive the inverse demand function endogenously, from the utility-maximising behaviour of the market participants who buy the liquidated assets. Their starting point is the classical risk-exchange equilibrium of Bühlmann (1980), whose pricing measure generalises the Esscher premium of actuarial science. The price of a liquidated claim then becomes the solution of a fixed-point equation, and the first question the paper answers is when that equation has exactly one solution, so that the market produces a well-defined clearing price.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathbb P)$. The market participants' utilities share a domain $\mathbb D$, either the real line $\mathbb R$ or the half line $\mathbb R_{++}=(0,\infty)$. The aggregate endowment $\mathcal X$ is an essentially bounded random variable with $\mathcal X\in\mathbb D$ almost surely and $\operatorname{ess\,inf}\mathcal X\in\mathbb D$ (Assumption 2.1).

The market is summarised by one function $R:\mathbb D\to\mathbb R$, the integral of the absolute risk aversion of the harmonic representative agent. Assumption 3.1 requires $R$ to be strictly increasing, differentiable and concave. If $\mathbb D=\mathbb R_{++}$, $R(0)=\lim_{z\searrow0}R(z)$ in the broad sense, possibly $-\infty$.

A claim $Z\in L^\infty$ is liquidated. Its price $v$ must satisfy $v=H_Z(v)$, where

$$H_Z(v)=\frac{\mathbb E\big[Z\exp(-R(\mathcal X+Z-v))\big]}{\mathbb E\big[\exp(-R(\mathcal X+Z-v))\big]}.$$

For $\mathbb D=\mathbb R$ the domain $\operatorname{dom}H_Z$ is all of $\mathbb R$; for $\mathbb D=\mathbb R_{++}$ it consists of the $v$ with $\mathbb P(\mathcal X+Z\ge v)=1$ at which the denominator is finite. The set of clearing prices is

$$V(Z)=\{v\in\operatorname{dom}H_Z \mid v=H_Z(v)\}.$$

Write $e=\operatorname{ess\,inf}[\mathcal X+Z]$ for the worst-case aggregate wealth after the claim is added, and $\Theta_Z(v)=\mathbb E[(Z-v)\exp(-R(\mathcal X+Z-v))]$. The uniqueness conditions of Theorem 3.3 are: (a) $Z$ and $\mathcal X+Z$ are comonotonic; (b) $R$ is linear; (c) $z\in\mathbb R_{++}\mapsto z\exp(-R(\mathcal X+z))$ is almost surely non-decreasing; (d) the same map is almost surely concave.

Formalization targets

Goal: Corollary 3.4

Let $\mathbb D=\mathbb R_{++}$ and assume any of (a)–(d). Then

$$|V(Z)|=1\iff\Big(e\in\operatorname{dom}H_Z,\ H_Z(e)\le e\Big)\ \text{or}\ \Big(e\notin\operatorname{dom}H_Z,\ \liminf_{v\nearrow e}H_Z(v)<e\Big),$$

and every clearing price satisfies $v\le e$. Both directions of the equivalence, both branches of the case split, and the bound are part of the goal.

Milestones

1. Proposition D.1: monotonicity or concavity of $z\mapsto z\exp(-R(x+z))$ on $\mathbb R_{++}$ extends to $\mathbb D-x$.
2. Continuity of $H_Z$ on $\operatorname{dom}H_Z$, and the bounds $\operatorname{ess\,inf}Z\le H_Z(v)\le\operatorname{ess\,sup}Z\vee e$ (proof of Theorem 3.2).
3. Theorem 3.2: $V(Z)\ne\emptyset$ if $\mathbb D=\mathbb R$, or if $\mathbb D=\mathbb R_{++}$ and $H_Z(v_0)\le v_0$ for some $v_0\in\operatorname{dom}H_Z$, which holds under either branch of the goal's right-hand side; $V(Z)$ is compact.
4. Under (a) or (b), $H_Z$ is non-increasing; $v=H_Z(v)$ iff $\Theta_Z(v)=0$; under (c) or (d), $\Theta_Z<0$ beyond any root (proof of Theorem 3.3).
5. Theorem 3.3: under any of (a)–(d), $|V(Z)|\le1$.
6. Corollary 3.5: if $\mathbb D=\mathbb R_{++}$ and $\mathbb E[\exp(-R(\mathcal X+Z-e))]=\infty$, then $V(Z)\ne\emptyset$.
7. The necessity step of Corollary 3.4: if $e\in\operatorname{dom}H_Z$ and $H_Z(e)>e$, then $\Theta_Z>0$ on $[\operatorname{ess\,inf}Z,e]$.

Significance

Corollary 3.4 turns the existence of a unique clearing price into a check of one number: the value of $H_Z$ at $e$, or its limit inferior from the left when the denominator blows up there. It is the basis for the rest of the paper: the pricing function $V$, its extension $\bar V$ to claims without a clearing price, and the endogenous inverse demand functions $f^q$ and $\bar f^q$ of a liquidated portfolio $q$ (Lemmas 3.9–3.10) are defined through the unique solution of (3.1). Without uniqueness the inverse demand function is not a function. The exponential- and power-utility special cases of Section 4 rely on the same statements.

The results are proved in the paper, with the proofs in its Online Appendix D. They have no machine-checked proof. Formalizing them produces a verified existence-and-uniqueness theory for Bühlmann-type pricing fixed points on both utility domains. It also records precisely how the broad-sense convention $R(0)=-\infty$ and an infinite denominator enter, which the printed definitions leave implicit.

Difficulty

$H_Z$ is a ratio of two expectations that both depend on the price $v$. Continuity together with the bounds gives existence on $\mathbb R$ almost directly, but uniqueness does not follow from continuity: Example C.1 of the paper exhibits three clearing prices. Each uniqueness condition controls a different object. Conditions (a) and (b) control the sign of a covariance-type double integral, so that $H_Z$ is non-increasing. Conditions (c) and (d) control the shape of $\Theta_Z$, and do so only for positive arguments, so Proposition D.1 is needed to reach the negative arguments $Z-v$ that actually occur.

On $\mathbb R_{++}$ the domain of $H_Z$ ends at $e$, and $e$ may or may not belong to it. When $\mathbb E[\exp(-R(\mathcal X+Z-e))]=\infty$, $H_Z(e)$ has no value and only the left limit inferior is available. Both sides of that limit, an expectation that becomes infinite and a ratio whose numerator and denominator diverge together, must be handled by monotone convergence and truncation. The naive approach of evaluating $H_Z$ at $e$ as a real number fails exactly in this branch.

Formalization scope

Everything is defined in the namespace EndoInvDemand.Clearing. The probability space is a measure P with IsProbabilityMeasure P. Only the aggregate $\mathcal X$ is modelled, since $H_Z$ sees the individual endowments only through their sum. Assumption 2.1 is stated for it with MemLp X ⊤ P. The domain is a two-valued flag Dom (real, pos). $R$ is a function ℝ → ℝ of which only the restriction to $\mathbb D$ is constrained and read.

The weight $\exp(-R(y))$ is valued in ℝ≥0∞. For $\mathbb D=\mathbb R_{++}$ its value at $y=0$ is $\sup_{z>0}\exp(-R(z))$, which encodes $R(0)$ in the broad sense and is $+\infty$ exactly when $R(0)=-\infty$. The denominator of $H_Z$ is a lower Lebesgue integral and may be $+\infty$; the numerator and $\Theta_Z$ are Bochner integrals.

The printed $\operatorname{dom}H_Z$ for $\mathbb R_{++}$ asks the denominator to be "$>0$", which always holds. The formalization asks it to be finite, the reading the proof of Corollary 3.5 uses, because the ratio has no value otherwise. "Linear" means affine on $\mathbb D$. Comonotonicity is the $\mathbb P\otimes\mathbb P$-almost-everywhere form. $|V(Z)|=1$ is ∃!, $|V(Z)|\le1$ is Set.Subsingleton, and $\liminf_{v\nearrow e}$ is Filter.liminf along 𝓝[<] e. The paper's derivative statements $H_Z'\le0$ and $\partial_v\Theta_Z<0$ are formalized as the monotonicity statements they are used for.

Neither side of the goal's equivalence can be satisfied by a degenerate encoding. $V(Z)$ is the fixed-point set of the explicit ratio $H_Z$ on its explicit domain; $H_Z$ never takes a junk value on that domain, because the denominator is finite and positive there; and $H_Z$ is bounded to the left of $e$, so the limit inferior is genuine. Both branches of the case split occur: $R=\log$ puts $e$ outside the domain and $R(z)=z$ puts it inside.

A complete development needs dominated and monotone convergence for parametric integrals, the intermediate value theorem, and a Chebyshev-type covariance inequality for comonotonic variables under $\mathbb P\otimes\mathbb P$. The covariance lemma and the treatment of $[0,\infty]$-valued weights with a broad-sense boundary value are reusable beyond this mission. Proofs of any milestone are welcome, including ones that route around the paper's derivative computations.

Selected references

• M. Bichuch and Z. Feinstein, Endogenous Inverse Demand Functions, arXiv:2012.08002v3, 2022; Operations Research. https://arxiv.org/abs/2012.08002
• H. Bühlmann, An economic premium principle, ASTIN Bulletin 11(1), 1980. https://doi.org/10.1017/s0515036100006619
• K. K. Aase, Equilibrium in a reinsurance syndicate; existence, uniqueness and characterization, ASTIN Bulletin 23(2), 1993. https://doi.org/10.2143/ast.23.2.2005091
• H. Amini, D. Filipović and A. Minca, Uniqueness of equilibrium in a payment system with liquidation costs, Operations Research Letters 44(1), 2016. https://doi.org/10.1016/j.orl.2015.10.005
• R. Cifuentes, H. S. Shin and G. Ferrucci, Liquidity risk and contagion, Journal of the European Economic Association 3(2–3), 2005. https://doi.org/10.1162/jeea.2005.3.2-3.556

Motivation

Many stochastic systems switch among a finite set of states at rates that vary with calendar time. A service system may face changing demand through the day; a reliability model may have components whose failure rates change with age. Time-inhomogeneous Markov jump processes describe such changes, but their transition probabilities generally involve product integrals rather than the matrix exponentials available for constant-rate models. Bladt and Peralta study a coupled approximation whose observations can instead be placed on a homogeneous Poisson grid. Their result addresses whole sample paths, including the times of jumps, rather than only a distribution at one fixed time. The paper develops this construction and its applications to phase-type models, ruin probabilities, and density evaluation (Bladt and Peralta, 2023, pp. 1–3).

The convergence target is the Skorokhod $J_1$ topology. It permits a small shift of jump times while requiring the sequence of state paths to match after that shift. For jump processes this distinction matters: even two paths with identical successive states can differ at every time near a jump when their jump epochs do not coincide. The source paper provides a quantitative rate for a specific common-space construction, followed by almost-sure convergence (Theorem 3, p. 9).

Setting

Let $\mathcal E$ be a nonempty finite state set. An intensity matrix function $\Lambda(t)$ has measurable, locally integrable entries for $t\ge0$; its off-diagonal entries are nonnegative, diagonal entries are nonpositive, and each row sum is nonpositive. A negative row sum allows termination into a cemetery state $\star$. Condition 1 bounds all diagonal rates uniformly. With an initial distribution $\alpha$ on $\mathcal E$, set

$$\lambda_0=\left\lceil\sup_{i\in\mathcal E,\,t\ge0} |\Lambda_{ii}(t)|\right\rceil .$$

The paper's uniformization construction uses a Poisson clock $\mathcal N$ of rate $\lambda_0$. At one of its arrival times $\chi_\ell$, a uniform random variable selects the next state with weight $\delta_{ij}+\lambda_0^{-1}\Lambda_{ij}(\chi_\ell)$; any leftover mass selects $\star$, which is absorbing. This constructs a path $\mathcal J$. Independent unit-rate clocks added to $\mathcal N$ create a denser inspection grid $\chi^{(n)}$ of rate $n$. A second, independent family creates an observation grid $\theta^{(n)}$ of the same rate. The approximation $J^{(n)}$ takes the observed value $\mathcal J(\chi^{(n)}_\ell)$ and holds it on $[\theta^{(n)}_\ell,\theta^{(n)}_{\ell+1})$ (Step (1), pp. 5–6).

For a sequence $c_k\to\infty$, the distance $d_{J_1}$ compares two state paths by taking the infimum over homeomorphisms $\Delta$ of nonnegative time. For each $\Delta$, it takes the larger of two terms: a geometrically weighted sum of the largest state mismatches on $[0,c_k]$, and the largest displacement $|\Delta(s)-s|$. The state space uses the discrete metric, including $\star$ (equation (3), p. 5, and Step (2), p. 8).

Formalization targets

For every $q>0$ and $0<\varepsilon<1$, Theorem 3 asks for a nonnegative sequence $c_k\to\infty$ such that, with $\kappa(q,\varepsilon)=4e^{1/2+\varepsilon/2+2q}$,

$$\mathbb P\!\left( d_{J_1}(J^{(n)},\mathcal J) \ge 3\kappa(q,\varepsilon)(\log n)n^{-1/2+\varepsilon/2} \right)=o(n^{-q}), \qquad d_{J_1}(J^{(n)},\mathcal J)\longrightarrow0 \quad\text{almost surely}.$$

The same $c_k$ supplies the metric in both clauses. Eight milestones cover the source's stated path toward this target: the rate-$n$ superpositions in Step (1); the Doob and Erlang moment estimates and bounds (16)–(17) in the proof of Lemma 1; the grid-discrepancy estimate of Lemma 1; the almost-sure time change and path equality in (12)–(13); and the maximal time-distortion identity (14). Each is part of the paper's construction or convergence argument (pp. 6, 8–9).

Significance

Theorem 3 supplies a common probability space on which the approximation and target can be compared path by path. Its probability estimate gives a rate for discrepancies in both the states and their jump times. Almost-sure convergence also supports the later distributional and functional consequences developed in the paper; the paper states a Prokhorov-distance consequence as Corollary 1 and then studies functionals of termination times (pp. 10, 13–24).

The result is proved in the source paper. This mission asks for a machine-checked Lean proof of its precise coupled-process statement. The formalized model would also supply reusable definitions for Poisson superposition, sampled jump paths, finite-state termination, and a $J_1$ distance on nonnegative time. The draft theorem declarations compile as statements with proof holes; they are not yet machine-checked proofs.

Difficulty

The two Poisson grids have the same rate but independent jump epochs. Direct pointwise comparison therefore fails near jumps even when the sequence of visited states agrees. The $J_1$ distance allows a time change, yet controlling it requires both the grid knots and the interpolation between them, as well as the probability of the largest discrepancy among roughly $n^{1+\varepsilon}$ arrivals. A bound at one fixed arrival cannot give the required maximum or the $o(n^{-q})$ tail. The source's formulas (12)–(14) and Lemma 1 isolate these distinct claims (p. 8).

Formalization scope

The state type is Fin p, with $p\ge1$, and termination is none in Option (Fin p). Paths are functions from nonnegative reals to this state type. The metric takes values in extended nonnegative reals so unbounded suprema retain their value, and its infimum ranges over every homeomorphism of nonnegative time. The setup records the laws and mutual independence of precisely the base clocks, the extra clocks with indices above $\lambda_0$, and the uniforms. Both $\mathcal J$ and $J^{(n)}$ are constructed from these ingredients; in particular, $J^{(n)}$ is defined by observations at $\chi^{(n)}$ placed on $\theta^{(n)}$, without assuming the path-alignment identity.

The formal statement adds $\sup_{i,t\ge0}|\Lambda_{ii}(t)|>0$. This excludes $\lambda_0=0$, where the paper's division by $\lambda_0$ and rate-$\lambda_0$ exponential gaps are undefined. It reads the printed initial-state and transition intervals as the intended inverse-CDF intervals, correcting their one-state index shift. The time-change assertions hold almost surely; probabilities of events whose measurability the paper does not establish are evaluated as outer measures. Set.ncard gives zero for an infinite arrival set, a null-path placeholder under the clock laws. For $n<\lambda_0$ the superposition has a placeholder value; finite-$n$ statements assume $n\ge\lambda_0$, and the asymptotic statements concern eventually larger $n$. The maximum over an empty initial index range is likewise zero, affecting only exceptional small $n$. The natural logarithm is used throughout. Lemma 1 prints an existential constant $\kappa(q,\varepsilon)>0$; the formal statement uses the value its proof fixes, $\kappa(q,\varepsilon)=4e^{1/2+\varepsilon/2+2q}$, which is the constant Theorem 3's threshold $3\kappa(q,\varepsilon)$ refers to. The Doob, Erlang and (16) milestones are stated for any sequence of independent exponential gaps of rate $n$, the role $\theta^{(n)}$ plays by the superposition milestone.

The theorem cannot be satisfied by defining $J^{(n)}$ through the time change or by assuming the grid discrepancy or path alignment: those are the results to establish. A complete development needs the Poisson superposition law, maximal inequalities and Erlang moments, pathwise grid bookkeeping, and asymptotic probability estimates. Theorem 1, Theorem 2, Corollary 1, Theorem 4, and the Section 3 applications remain outside this mission.

Selected references

• Martin Bladt and Oscar Peralta, Strongly convergent homogeneous approximations to inhomogeneous Markov jump processes and applications, arXiv:2204.02954v3, 2023; published in Mathematics of Operations Research, 2025. arXiv version used for all page and equation references.
• Giang T. Nguyen and Oscar Peralta, Rate of strong convergence to Markov-modulated Brownian motion, Journal of Applied Probability, 2022 (reference [45] of the source; its Lemma A.1 is the cited Erlang central-moment bound). https://arxiv.org/abs/1908.11075

Why dynamic double auctions matter

A platform that matches one seller with several buyers can trade an item whenever a buyer values it more than the seller does. That allocation maximizes the value created by trade in a single period. A platform seeking revenue also has to respect what privately informed agents are willing to report and accept. In a repeated market, it can distribute utility across periods through promises about future payoffs. The question is how closely a feasible dynamic mechanism can approach the welfare available from efficient trade. Balseiro, Mirrokni, Paes Leme, and Zuo study this question for repeated double auctions with a single seller, multiple buyers, and independent draws across periods in Dynamic Double Auctions: Towards First Best, §2 and §5.

The result formalized here is Theorem 5.3 of the November 15, 2018 SSRN version. Its central claim is that the paper's specified mechanism earns expected platform profit within order $\sqrt{T\log T}$ of the first-best benchmark over $T$ periods, under the paper's distributional and reserve-price assumptions. The same theorem states that the ratio of profit to that benchmark tends to one as the horizon grows. The 2022 journal title uses “Toward” rather than “Towards”; all theorem numbers and pages in this mission refer to the pinned SSRN preprint.

Market and mechanism

There are $n\ge1$ buyers and one seller. In every period $t=1,\ldots,T$, the seller's private opportunity cost is $v_0^t$ and buyer $i$'s private value is $v_i^t$. The vector $v^t$ has a common distribution $F$ on $[0,\bar v]^{n+1}$. Draws in different periods are independent; the seller's and buyers' values within one period may be correlated. A trade creates surplus $(\max_{i\ge1}v_i^t-v_0^t)^+$, where $x^+=\max(x,0)$. Write $\underline w_0=\mathbb E_F[(\max_{i\ge1}v_i-v_0)^+]$ for its expected value. Over $T$ periods, the first-best profit benchmark is $\Pi^{\mathrm{FB}}=T\underline w_0$.

The promised utility $w_i^t$ is the expected current utility plus the continuation utility owed to agent $i$ at the start of period $t$. An allocation $q_i^t$ is a probability of receiving the item, and $z_i^t$ is an expected transfer: buyers pay $z_i^t$ to the platform, while the platform pays $z_0^t$ to the seller. The platform's expected profit $\Pi$ is the expectation of the sum of buyer payments minus seller payments. The mechanism sets next period's promise to its current continuation utility. Promise keeping, dynamic incentive compatibility, participation, and nonnegative transfers are the relevant constraints. In the boundary regimes, the paper uses a weak supply balance inequality $q_0^t\ge\sum_{i=1}^n q_i^t$.

Assumption 5.1 supplies a reserve price $r\in[0,\bar v]$ and buyer weights $\alpha_i\in[0,1]$ with $\sum_i\alpha_i\le1$. Put $\mu=\mathbb E_F[(r-v_0)^+]$. The weights satisfy $\alpha_i\mathbb E_F[v_i\mathbf1_{\{v_0\le r\}}]=\mu$ for every buyer, and $0<\mu\le\underline w_0$. The upper promise at period $t$ is $\bar w^t=(T-t+1)\mu$. In the medium region, the mechanism sells to the highest buyer using lexicographic ties; the winner pays their value and the seller receives their cost. In the low and high regions, it uses the reserve price and buyer weights, with each agent's allocation throttled by $p_i^t=\min(1,w_i^t/\mu)$. The definition of the mechanism follows the formulas on printed p. 25 of the preprint.

Formalization targets

The goal is the two-part assertion of Theorem 5.3. Every agent starts with the same promise

$$w^1=\underline w_0+\bar v\sqrt{8T\log T}.$$

Whenever $w^1\le\bar w^1-\bar v(1+\sqrt{8T\log T})$, a constant $C$ independent of $T$ satisfies

$$\Pi\ge\Pi^{\mathrm{FB}}-C\sqrt{T\log T}.$$

For the same market and mechanism, the theorem also asserts

$$\frac{\Pi}{\Pi^{\mathrm{FB}}}\longrightarrow1\qquad(T\longrightarrow\infty).$$

The lower bound is stated for integer horizons $T\ge2$, and $C$ may depend on the fixed market data. The ratio statement is a limit over natural-number horizons. The mission's milestones record Lemma 5.2's feasibility claims, the welfare identity and loss bound, and the exit-time estimates used in Theorem 5.3. The exit-loss milestone keeps the constant displayed on printed p. 30.

What the result provides

The mechanism combines a period-by-period allocation rule with explicit continuation promises. Theorem 5.3 shows that a single feasible rule has sublinear expected profit loss relative to $T\underline w_0$, while Lemma 5.2 states the incentive and participation guarantees that make the profit comparison meaningful. The ratio result turns the additive estimate into asymptotic first-best performance because $\underline w_0\ge\mu>0$. These statements are proved in the cited paper; the open work here is a machine-checked formalization of its model, feasibility lemma, exit estimates, and profit theorem.

The resulting Lean definitions would also provide a reusable representation of expected allocations and transfers in a finite-horizon, privately informed market with correlated values within each period. The stopping-time and concentration parts can be useful in other repeated-mechanism arguments, although no such extension is asserted by this mission.

Main difficulty

The medium-region allocation extracts realized surplus but does not by itself meet the dynamic incentive constraints throughout the horizon. The low and high regimes change the allocation and transfers to keep promised utilities feasible. The analysis must account for the periods after the state first reaches either boundary. An estimate at one fixed period is insufficient: the relevant event is the first entry into a boundary region at any earlier period, and the upper boundary moves as the horizon runs down. The paper's martingale concentration argument supplies the needed control of that first-exit event.

Formalization scope

Lean represents agents by Fin (n+1), with zero reserved for the seller, and periods by natural numbers. The state before period $t$ has index $t-1$. A probability measure on the infinite sequence of period-value vectors represents independent draws from $F$ across time; all quantities for horizon $T$ use only its first $T$ coordinates. Allocations remain real-valued probabilities, with no separate randomization device. The rule uses the least-index buyer among those tied at the top. Boundary equality is assigned to the low or high rule, as in the paper's exit-time definitions. Each agent has its own throttle in the rule; on reachable coupled states these throttles agree. The positive part is max · 0, and $\log$ and square root are the real functions in Mathlib.

The goal refers to the integral of transfers generated by the stated recursive mechanism under this product law, with the first-best value computed from the same distribution. It does not take profit or the benchmark as free variables. The distribution is supported in the bounded value box, and Assumption 5.1 is part of every theorem's standing data. The finite value range matters both for the mechanism's feasibility and for the real-valued expectations. Solvers may contribute probability, stopping-time, and finite-allocation lemmas needed to close these statements; the main profit theorem and its stated constants remain the fixed targets.

Selected references

• Santiago R. Balseiro, Vahab Mirrokni, Renato Paes Leme, and Song Zuo, Dynamic Double Auctions: Towards First Best, SSRN 3213460, November 15, 2018, especially §2 and §5. SSRN preprint.

Motivation

A bank's failure can make its creditors fail, and those failures can cause further defaults. The final number of failures depends on the network of exposures as well as on each bank's ability to absorb losses. Amini, Cao and Sulem study this question in a directed random network whose banks may have different degrees and different default thresholds. Their limit theorems separate the case in which nearly every bank eventually defaults from the case in which the final counts have Gaussian fluctuations around explicit deterministic values. Those distinctions matter when a systemic-risk calculation depends on the distribution of a cascade's final size, rather than only on its expected size (Amini, Cao and Sulem, arXiv:2104.00248v1, §§2–4).

The paper was first available as the pinned 2021 preprint used here and was published in Mathematics of Operations Research in 2024. This mission follows the preprint's section, page and theorem numbering throughout. Its target is Theorem 3.7 on preprint page 13.

Setting

An economy has $n$ banks, each assigned a characteristic $x$ from a countable set $X$. A type $x$ specifies an incoming degree $d_x^+$, an outgoing degree $d_x^-$, and a default threshold $\Theta_i^{(n)}$. The threshold is the number of defaulted incoming counterparties that bank $i$ can tolerate before it becomes insolvent. For a bank of type $x$, $\Theta_i^{(n)}$ has probability law $q_x^{(n)}$ on $\{0,\ldots,d_x^+\}$. The fraction of banks of type $x$ is $\mu_x^{(n)}$. As the economies grow, the type fractions and threshold laws approach $\mu_x$ and $q_x$.

The paper represents exposures as incoming and outgoing half-edges. Its balls-and-bins death process gives every incoming ball an independent exponential lifetime of mean one. A bank is solvent at time $t$ while fewer than $\Theta_i^{(n)}$ of its incoming balls have died. Threshold-zero banks are therefore defaulted at the start. The process tracks five quantities: solvent banks $S_n(t)$, defaulted banks $D_n(t)$, alive incoming balls of solvent banks $H_n^+(t)$, alive incoming balls of defaulted banks $I_n^+(t)$, and white infected outgoing balls $W_n(t)$. If $L_n(t)$ is the total number of alive incoming balls and $H_n^-(t)$ the outgoing balls of solvent banks, the paper's initial recolouring convention gives $W_n(t)=L_n(t)-H_n^-(t)-1$. The final time $\tau_n^*$ is the first nonnegative time at which $W_n$ becomes negative (§2.4, pp. 8–9).

For $z\in[0,1]$, let $b(d,z,\ell)$ be a binomial probability and $\beta(d,z,\ell)$ its upper tail. The paper's functions $f_S,f_D,f_{H^+},f_{I^+},f_W$ describe the deterministic scale of the five counts at time $t$ after setting $z=e^{-t}$. Write $\boldsymbol f(z)$ for their vector, and $\boldsymbol f^{(n)}(z)$ for the same formulas with finite-economy parameters. The final-size parameter is the largest zero

$$z^*=\sup\{z\in[0,1]:f_W(z)=0\},$$

and $\widehat z_n$ is the corresponding largest zero of $f_W^{(n)}$. A zero is stable when $\alpha=f_W'(z^*)>0$. The class count $S_{x,\theta,\ell}^{(n)}(t)$ records solvent banks of type $x$, threshold $\theta$, and $\ell$ dead incoming balls, with $0\le\ell<\theta\le d_x^+$ (§3, pp. 9–13).

Formalization targets

Final-size law

The goal is both parts of Theorem 3.7. If $z^*=0$, the final default fraction tends to one in probability:

$$D_n(\tau_n^*)/n\xrightarrow{p}1.$$

If $0<z^*\le1$ and $\alpha>0$, then $\widehat z_n\to z^*$ and the five final counts converge jointly:

$$n^{-1/2}\bigl(\boldsymbol\clubsuit_n(\tau_n^*)-n\boldsymbol f^{(n)}(\widehat z_n)\bigr) \Rightarrow N_5\!\left(0,J C(z^*)J^{\mathsf T}\right), \qquad J=I-\alpha^{-1}\boldsymbol f'(z^*)e_W^{\mathsf T}.$$

Here $C(y)$ is an explicit covariance formed by drawing a threshold and an independent binomial number of surviving incoming balls for each type. The theorem also gives a one-dimensional Gaussian limit for every admissible $S_{x,\theta,\ell}^{(n)}(\tau_n^*)$, centred at its finite-economy value. The milestones are Lemma A.4, the largest-zero claim in the proof of Theorem 3.7, and the process limits Theorems 3.5 and 3.6. They cover uniform derivatives, zero location and the Gaussian process limits in the stronger moment regime of Assumption 3b. The paper's Theorem 3.1, Lemma 3.2 and Theorem 3.3 are omitted as milestones because their printed weaker Assumption 3a allows outgoing degree mass to escape to rarer types; the formalization notes give a counterexample.

Significance

The stable regime supplies a distributional approximation for the final number of solvent and defaulted banks and for the numbers of healthy and infected links. It also quantifies fluctuations of a specified type-threshold class. The degenerate regime identifies a qualitatively different outcome: almost all banks default. The paper uses these counts as inputs to systemic-risk aggregates in its following section (§4, pp. 13–15).

The results are proved in the paper, but the goal and its four curated source results were not found as matching formal statements in the Prove2Me catalog during preparation. Formalizing them would provide reusable statements about first-passage times, countably typed death processes and vector-valued process limits. The cited Glivenko–Cantelli theorem is already proved on the platform, while a general martingale functional central limit theorem is posed there as an open goal; neither is substituted for a paper-specific milestone. Solvers can contribute the probability infrastructure as well as proofs of the listed statements.

Difficulty

The fixed-time counts are sums over many bank types, but the type space can be infinite and degrees need not be uniformly bounded. Pointwise convergence for each type does not by itself control the total process or all derivatives of its fluid functions. More importantly, the cascade ends at the random time $\tau_n^*$, while the process limit is indexed by deterministic time. Substituting $t^*=-\log z^*$ directly into a fixed-time Gaussian limit loses the fluctuation of the stopping time and produces the wrong final covariance. A proof must retain the joint process fluctuations and the behaviour of the largest finite-economy zero near the stable limit.

Formalization scope

Lean uses Fin n for banks, a countable type space $X$, real time $t\ge0$, and a single probability space for the sequence of economies; no dependence across different $n$ is assumed. It orders the five coordinates as $S,D,H^+,I^+,W$, represents each in-ball by an index $k<d_x^+$, and uses ordinary real derivatives. The threshold laws are supported on $\{0,\ldots,d_x^+\}$, thresholds and actual in-ball lifetimes are jointly independent within each economy, and the incoming and outgoing degree sums agree for every $n$. These conditions make explicit requirements used by the paper's formulas and proofs. The finite $I^+$ and $W$ fluid functions use $\lambda^{(n)}$, the finite mean degree, where the preprint prints $\lambda$ (p. 12).

The printed lifetime variance in equations (24) and (39) is too small by a factor of two. The limit here uses the corrected per-bank covariance $C(y)$; for a single incoming ball the Bernoulli variance is $y(1-y)$, rather than $[y-y^2]/2$. The statement concerns the balls-and-bins death process of §2.4, on which the paper's §3 states its theorems; the equivalence with the default cascade on the configuration model, asserted in §2.4, is not formalized.

The explicit covariance, the joint five-coordinate law, and evaluation at the random $\tau_n^*$ rule out an unspecified or existential covariance, separate marginal limits, and substitution of the deterministic $t^*$. The degree moment and probability assumptions exclude junk Gaussian, derivative and infinite-sum values. The model definitions, the corrected covariance and the path-convergence reference are reusable beyond this mission. Theorem 4.1 and later systemic-risk aggregates are outside this final-size target.

Selected references

• H. Amini, Z. Cao and A. Sulem, Limit Theorems for Default Contagion and Systemic Risk, Mathematics of Operations Research, 2024; pinned preprint arXiv:2104.00248v1, 2021. Preprint.

Motivation

A seller who can inspect a buyer's true value after receiving a bid can use the bid as a refundable deposit. A truthful buyer may receive a reward, while a buyer whose report is false forfeits the deposit. This changes the incentive constraint: a buyer who considers reporting $w$ compares her truthful utility with $v x(w)-w$, not with the payoff from a conventional payment schedule at the false report. Alaei, Belloni, Makhdoumi, and Malekian study the revenue-maximizing design for this setting in Optimal Auction Design with Deferred Inspection and Reward, §§2–3.

The single-agent problem is a useful test of how inspection affects mechanism design. The paper gives an explicit bid function, allocation rule, and payment rule for a general positive differentiable value density. The mission asks for a formal statement and proof of that characterization, including the claim that the proposed auction is optimal among every feasible deferred-inspection mechanism. The source used here is the SSRN copy dated 2022-03-22; all page and result numbers refer to that copy.

Setting

The buyer has a private value $v$ in $V=[0,1]$. Its density $f$ is differentiable and strictly positive on $V$, and integrates to one. The seller allocates one object with probability $x(w)\in[0,1]$ after report $w$. The buyer pays the report as a deposit. After inspection reveals the true value, a truthful report may earn a nonnegative reward; a false report earns none. Write $p(v)$ for the seller's net payment when the buyer reports truthfully.

A pair $(x,p)$ is incentive compatible and individually rational when, for every $v,w\in V$,

$$v x(v)-p(v)\ge v x(w)-w, \qquad v x(v)-p(v)\ge0.$$

The first inequality includes the forfeited deposit $w$. Expected revenue is $R_f(x,p)=\int_0^1 p(v)f(v)\,dv$. Feasibility also requires $p(v)f(v)$ to be integrable, so this real-valued objective represents an expectation. These are Problem (7)–(9) on p. 7 of the source.

For a fixed allocation, (10) defines its greatest compatible payment

$$p_x(v)=\inf_{0\le w\le v}\{v(x(v)-x(w))+w\}.$$

The best-alternative bid $b_x(v)$ is the largest report attaining that minimum, when an attaining report exists. The paper also considers allocations that are strictly concave and differentiable up to a threshold $\bar v$ and equal to one thereafter. It calls this class SCD. Those concepts are represented directly in the mission's definition module.

Formalization targets

The goal is Theorem 2 on p. 12. Put

$$G(t)=\int_0^t yf(y)\,dy, \qquad b(v)= \begin{cases} 0,&v\le\underline v,\\ G^{-1}(G(v)-G(\underline v)),&v>\underline v. \end{cases}$$

The theorem asserts that thresholds $\underline v,\bar v$ exist with $\bar v=b(1)$ and with the integral branch of the proposed allocation reaching one at $\bar v$. The allocation is $x(v)=1$ above $\bar v$ and

$$x(v)=\int_{\underline v}^{b^{-1}(v)}\frac{b'(t)}{t}\,dt \qquad(v<\bar v),$$

where $b^{-1}(v)=G^{-1}(G(v)+G(\underline v))$. Its payment is $v x(v)$ at or below $\underline v$, $v(x(v)-x(b(v)))+b(v)$ between the thresholds, and $v(1-x(b(v)))+b(v)$ at or above $\bar v$. The formal goal says this explicit pair is feasible and that $R_f(x',p')\le R_f(x,p)$ for every feasible pair $(x',p')$. It also asserts that a threshold pair exists.

The milestones follow the paper's route: Proposition 2 identifies $p_x$; Lemma 1 records payment improvements from removing allocation decreases, changing endpoints, and taking the concave hull; Lemma 2 supplies smooth strictly concave approximations with convergent revenue; and the sound part of Proposition 3 concerns best-alternative bids. The final two targets are the differential identity for $b$ in the proof of Theorem 2 and the threshold equation (15). Their source wording, page, and PDF hash are attached to each milestone.

Why the result matters

The result replaces an optimization over pairs of functions subject to all pairwise incentive inequalities with explicit rules calculated from the value density. It determines both the allocation probabilities and the payments in the inspection model. For the uniform density, Example 2 on pp. 13–14 gives a continuous allocation and revenue about $0.3808$, compared with $0.25$ for the standard no-inspection benchmark in that example; see the source. The difference comes from the seller's ability to retain the deposit after a false report.

The paper has a published mathematical argument, but these exact statements have no machine-checked proofs in this mission. A completed formalization would provide reusable definitions for truthful reporting with forfeited deposits, the optimal-payment operator, and the inverse weighted distribution $G$. It would also resolve proof gaps visible in the source rather than silently taking them as assumptions. Theorem 1 of the SSRN copy is false as printed for its stated bid class and is deliberately absent from the formal targets; the mission's goal is Theorem 2 itself.

Difficulty

The main obstacle is global optimality. Checking a derivative or a local incentive condition does not compare the proposed auction against every feasible mechanism. Every type can contemplate every false report, so a local condition alone does not settle incentive compatibility. The appendix derives the proposed bid through variations of an allocation-dependent functional, including Dirac-delta perturbations and an unconstrained reformulation in Theorem 1. Its admissible bids do not all correspond to feasible allocations satisfying the endpoint condition. A proof of Theorem 2 must establish the global revenue comparison without treating that reformulation as an already valid equivalence.

The boundary is also mathematically delicate. The derivative $b'(v)$ becomes singular as $v$ approaches $\underline v$ from above, although the allocation integral remains meaningful for the intended positive threshold. Formula (15) must have a genuine solution; merely quantifying over thresholds satisfying an equation would make the optimality clause empty if no such pair existed.

Formalization scope

Lean represents values by real numbers and restricts every value and report quantifier to $[0,1]$. The density carries exactly Assumption 1's differentiability, positivity, and unit integral; the absence of point masses follows from the density representation. Allocation and payment functions are total real functions whose values outside the value interval have no economic role. Expected payment is a real interval integral, and feasible mechanisms require integrability of $pf$.

The inverse $G^{-1}$ is the lower inverse on $[0,1]$, formed with a real infimum. Its intended calls are within the range of $G$. The displayed allocation uses the ordinary derivative of the explicit bid on its open differentiability interval; the singular endpoint does not affect the integral. The equation $x(\bar v)=1$ is read through the integral branch, not through the constant-one branch, because it determines the threshold by continuity. The goal states existence of thresholds and optimality over all feasible mechanisms. In particular, the incentive condition is not replaced by the classical $v x(w)-p(w)$, and comparison is not restricted to SCD, concave, or monotone allocations.

Proposition 2 and Lemma 1 are expressed as payment-improvement statements, since pointwise assertions about every revenue optimum fail after null-set changes. Proposition 3 keeps the unique minimizer and monotonicity claims but narrows strict increase to the region before the bid reaches $\bar v$; the printed full-interval claim admits a flat segment. The derivative identity is stated on $(\underline v,1)$, where its terms are defined. Contributions that prove these precise statements, construct the threshold solution, or establish the final global comparison are within scope.

Selected references

• Saeed Alaei, Alexandre Belloni, Azar Makhdoumi, and Ali Malekian, Optimal Auction Design with Deferred Inspection and Reward, SSRN preprint 3700525, version dated 2022-03-22; published in Operations Research, 2024. SSRN copy; journal DOI.