All missions

Dividends, reinsurance and a finite horizon

An insurer that pays dividends to its shareholders faces a trade-off studied since de Finetti (1957): paying out surplus early raises the discounted payout but brings ruin closer. Reinsurance changes the trade-off, because ceding part of each claim lowers the volatility of the surplus at the price of a reinsurance premium. When the insurer may choose both the dividend stream and, at every moment, an arbitrary reinsurance contract, the problem becomes a mixed singular–classical stochastic control problem. Most of the literature treats it on an infinite horizon, where the value function solves an ordinary differential equation. On a finite horizon $T$ the value function also depends on time to maturity, the Hamilton–Jacobi–Bellman (HJB) equation becomes a parabolic variational inequality with a gradient constraint, and neither its solvability nor the regularity of its solution is classical.

Guan, Xu and Zhou (arXiv:2008.00391v3, Mathematics of Operations Research, 2023) show by PDE methods that this variational inequality has a classical solution, identify it with the value function, and read the optimal reinsurance contract and dividend barrier off its derivatives. This mission formalizes the PDE part: Theorem 3.1 and the steps of Appendix A that lead to it.

Setting

Claims are nonnegative random variables with common distribution function $F$, $F(0-)=0$, possibly discontinuous. The paper assumes the tail condition

$$z^3\,(1-F(z))\ \text{is bounded on }[0,\infty), \tag{3.3}$$

so the moments $\mu_1=\int_0^\infty z\,dF(z)$ and $\mu_2=\int_0^\infty z^2\,dF(z)$ are finite. The other data are the net reinsurance loading $\gamma>0$, the discount factor $c>0$ and the horizon $T>0$; the mission assumes $\gamma<\mu_1$ throughout.

A reinsurance contract is described by the retained loss $H(z)$ the insurer keeps out of a claim of size $z$, with $0\le H(z)\le z$; $\mathcal H$ is the set of such functions. For a function $v(x,t)$ of the surplus $x$ and the time to maturity $t$ the operator

$$\mathcal Lv=\sup_{H\in\mathcal H}\Big(\frac{v_{xx}}2\int_0^\infty H(z)^2\,dF(z)+v_x\int_0^\infty H(z)\,dF(z)\Big)-\gamma v_x-cv \tag{3.2}$$

is the generator of the controlled diffusion approximation of the surplus. The HJB equation is the variational inequality, on $\mathcal Q_T=(0,\infty)\times(0,T]$,

$$\min\{v_t-\mathcal Lv,\ v_x-1\}=0,\qquad v(0,t)=0,\qquad v(x,0)=x. \tag{3.1}$$

The functions

$$A(y)=\int_0^{1/y}z(1-F(z))\,dz,\qquad B(y)=\int_0^{1/y}(1-F(z))\,dz\qquad(y>0),$$

with $A=\mu_2/2$ and $B=\mu_1$ for $y\le0$, compute the supremum in (3.2), and $f(y)=-yA(y)+B(y)-\gamma$ has a unique root $\lambda>0$. The penalized gradient problem (A.17) on $\mathcal Q_{L,T}=(0,L)\times(0,T]$ is

$$u_t-\mathcal Tu+\beta_\varepsilon(u-1)=0,\quad (\lambda u+u_x)(0,t)=f_\varepsilon(t),\quad u(L,t)=1,\quad u(x,0)=1,$$

with $\mathcal Tu=A(-u_x/u)u_{xx}+B(-u_x/u)u_x-\gamma u_x-cu$, a penalty function $\beta_\varepsilon$ and a boundary datum $f_\varepsilon$ that ramps from $\lambda$ down to $0$ on $[0,\varepsilon]$.

Formalization targets

Goal: Theorem 3.1

There is a unique $v\in C^{2,1}(\overline{\mathcal Q}_T\setminus\{(0,0)\})\cap C(\overline{\mathcal Q}_T)$ that solves (3.1) and satisfies

$$v_x\ge1,\quad v_t\ge0,\quad v_{xx}\le0,\quad v_{xxx}\ge0\ \text{(weakly)},\quad v_{xt}\ge0,\quad \lambda v_x+v_{xx}\ge0 .$$

Uniqueness is among solutions in the same class with the same six properties, as equality on $\overline{\mathcal Q}_T$.

Milestones

1. (A.7)–(A.9): $A$, $B$ are non-increasing, Lipschitz, bounded by $\tfrac12\min\{y^{-2},\mu_2\}$ and $\min\{y^{-1},\mu_1\}$, with $y^3A'=y^2B'=F(1/y)-1$.
2. (A.10): $\mathcal Lv=A(-v_{xx}/v_x)v_{xx}+B(-v_{xx}/v_x)v_x-\gamma v_x-cv$ when $v_x>0$.
3. (A.12)–(A.13): $f'=-A<0$ everywhere, and $f$ has a unique root, which is positive.
4. Lemma A.1: $A(-y/z)$ and $B(-y/z)$ are Lipschitz on $\mathbb R\times[1,\infty)$.
5. Lemma A.2: a comparison principle for (A.17) between functions $\ge1$.
6. Lemma A.3: (A.17) has a $C^{2,1}$ solution, and $1\le u^\varepsilon\le Ke^{\Lambda t}/(x+1/\lambda)$ for small $\varepsilon$, with $K=L+1/\lambda+1$, $\Lambda=\mu_2/\gamma^2+\gamma\lambda$.
7. Lemmas A.4–A.6: $u^\varepsilon_t\ge0$, $u^\varepsilon_x\le0$, $\lambda u^\varepsilon+u^\varepsilon_x\ge0$, $u^\varepsilon_{xx}\ge0$.

Significance

Theorem 3.1 is the analytic core of the paper. The verification theorem (Theorem 3.2) needs a classical solution that is increasing and concave in $x$, which Theorem 3.1 provides, and Section 4 derives the shape of the optimal policy from (3.4)–(3.9): the optimal retained loss is $\min\{z,\,-v_x/v_{xx}\}$, and (3.9) bounds the reinsurance barrier away from zero. Without the existence of a classical solution, the HJB equation could only be interpreted in the viscosity sense, whose uniqueness theory for this mixed singular–classical problem is not available, and the strategies would not be well defined.

The result is proved in the paper; nothing in it has been machine-checked. A formal development would produce, beyond the theorem, a reusable formal treatment of a parabolic obstacle problem with a Robin boundary condition through penalization, comparison principles for quasilinear parabolic equations, and the explicit reduction of a supremum over reinsurance contracts against an arbitrary claim distribution. The appendix lemmas (A.7)–(A.13) and Lemma A.1 are elementary real analysis and are self-contained targets.

Difficulty

The supremum in $\mathcal L$ is over a function space and $F$ may have atoms, so even the closed form (A.10) and the everywhere-differentiability of $f$ require care with one-sided derivatives at the jumps of $F$. The operator is fully nonlinear and degenerates as $-v_{xx}/v_x\to\infty$, since $A(y)\to0$. The inequality carries a gradient constraint $v_x\ge1$ rather than an obstacle, and the left boundary condition $(\lambda u+u_x)(0,t)=0$ is incompatible with the initial condition at the corner $(0,0)$, which is why the solution is only claimed to be $C^{2,1}$ away from that corner. The obvious route, solving (3.1) directly by a fixed-point argument, does not control $v_{xx}$; the paper differentiates in $x$ and works with the gradient $u=v_x$, which turns the gradient constraint into an obstacle but introduces the Robin condition with the wrong sign for a direct maximum principle. The passage $\varepsilon\to0$ needs $W^{2,1}_p$ and Hölder estimates uniform in $\varepsilon$, which are not in Mathlib.

Formalization scope

• Functions of $(x,t)$ are ℝ → ℝ → ℝ; $t$ is time to maturity. Partial derivatives are explicit functions $v_x, v_{xx}, v_t$ tied to $v$ by HasDerivAt on sections at interior points ($x>0$, $0<t<T$) and continuous on $\overline{\mathcal Q}_T\setminus\{(0,0)\}$; boundary values are these continuous extensions, and (3.1) holds at $t=T$ through them.
• The claim law is a probability measure on $\mathbb R$ with no mass on $(-\infty,0)$, and $F(z)=\mu((-\infty,z])$; no density is assumed. $\mathcal H$ consists of measurable $H$ with $0\le H(z)\le z$ for $z\ge0$, and $\mathcal L$ is defined by the supremum (3.2), not by (A.10).
• $0<\gamma<\mu_1$ is a standing hypothesis (the paper imposes it from Section 4; without it $f$ has no positive root and (3.9) is undefined).
• (3.7) is read as monotonicity of $x\mapsto v_{xx}(x,t)$, (3.8) as monotonicity of $t\mapsto v_x(x,t)$, (3.9) for every positive root of $f$.
• Uniqueness is equality on $\overline{\mathcal Q}_T$ within the class of solutions with (3.4)–(3.9). Uniqueness among all classical solutions is not posed: the paper's argument on an unbounded domain uses no growth condition.
• Penalty data are taken at one fixed $\varepsilon$; the limit $\varepsilon\to0$ of $\beta_\varepsilon$ is not part of the data. "Sufficiently small $\varepsilon$" is an $\varepsilon_0>0$ depending on the model and $L$.
• A formalization in which $\mathcal L$ is given by its closed form, the derivatives are deriv evaluated at boundary points, or uniqueness is stated as equality of functions on all of $\mathbb R^2$, would trivialize or falsify the goal; the statements avoid all three.

Needed infrastructure: interval integrals of monotone functions and their one-sided derivatives, maximum and comparison principles for linear and quasilinear parabolic equations in one space dimension, existence for quasilinear parabolic problems (Leray–Schauder with Schauder estimates), and compactness in Hölder and Sobolev spaces. The parabolic comparison principle and the penalization scheme are reusable well beyond this mission. Proofs of individual milestones, in particular the elementary ones (A.7)–(A.13) and Lemma A.1, are welcome independently.

Selected references

• C. Guan, Z. Q. Xu, R. Zhou, Dynamic optimal reinsurance and dividend-payout in finite time horizon, Mathematics of Operations Research, 2023; preprint arXiv:2008.00391v3. https://arxiv.org/abs/2008.00391
• B. de Finetti, Su un'impostazione alternativa della teoria collettiva del rischio, Transactions of the XVth International Congress of Actuaries, 1957.
• G. M. Lieberman, Second Order Parabolic Differential Equations, World Scientific, 1996. https://doi.org/10.1142/3302
• L. C. Evans, Partial Differential Equations, 2nd ed., American Mathematical Society, 2010. https://doi.org/10.1090/gsm/019

Motivation

An insurance company pays out dividends to its shareholders and buys reinsurance to limit its exposure to large claims. Both decisions are dynamic: the right amount to cede and the right moment to pay depend on the current surplus and on the time left until a fixed maturity $T$. Guan, Xu and Zhou (2023) solve the combined problem for a diffusion-approximated surplus with a general claim distribution, a general reinsurance contract (any retained-loss function $0\le H(z)\le z$), and a finite horizon. Their main structural output is a description of the optimal strategy by free boundaries in the surplus–time plane: a dividend barrier $d(\tau)$, and for each claim size $z$ a reinsurance barrier $K(z,\tau)$.

A companion mission formalizes the existence and uniqueness of the classical solution of the HJB variational inequality (Theorem 3.1 of the paper). This mission takes that solution as given and formalizes the shape of the boundaries (Section 4 of the paper), culminating in the description of the reinsurance boundaries for discrete claim distributions (Theorem 4.5).

Setting

Claims are i.i.d. copies of a nonnegative random variable $Z_1$ with distribution function $F$, satisfying the tail condition that $z^3(1-F(z))$ is bounded on $[0,\infty)$. Write $\mu_1=\int_0^\infty z\,dF(z)$ and $\mu_2=\int_0^\infty z^2\,dF(z)$. The reinsurance loading is $\gamma>0$, the discount rate $c>0$, the horizon $T>0$, and throughout $0<\gamma<\mu_1$ (for $\gamma\ge\mu_1$ the problem is trivial).

The value function $v(x,\tau)$, with $x\ge0$ the surplus and $\tau\in[0,T]$ the time to maturity, is the solution of the variational inequality

$$\min\{v_\tau-\mathcal Lv,\ v_x-1\}=0\ \text{on }(0,\infty)\times(0,T],\qquad v(0,\tau)=0,\qquad v(x,0)=x,$$

where

$$\mathcal Lv=\sup_{0\le H(z)\le z}\Bigl(\frac{v_{xx}}{2}\int_0^\infty H^2\,dF+v_x\int_0^\infty H\,dF\Bigr)-\gamma v_x-cv .$$

It is the unique function of class $C^{2,1}([0,\infty)\times[0,T]\setminus\{(0,0)\})\cap C([0,\infty)\times[0,T])$ that solves this inequality and satisfies $v_x\ge1$, $v_\tau\ge0$, $v_{xx}\le0$, $v_{xx}$ nondecreasing in $x$, $v_x$ nondecreasing in $\tau$, and $\lambda v_x+v_{xx}\ge0$. Here $\lambda$ is the unique positive root of

$$f(y)=-yA(y)+B(y)-\gamma,\qquad A(y)=\int_0^{1/y}z(1-F(z))\,dz,\quad B(y)=\int_0^{1/y}(1-F(z))\,dz\quad(y>0).$$

The no-dividend region is $\mathcal{ND}=\{(x,\tau): v_x(x,\tau)>1\}$, and the dividend boundary is

$$d(\tau)=\inf\{x\ge0: v_x(x,\tau)=1\}.$$

For a claim of size $z$ the optimal retained loss is $-v_x/v_{xx}$ if $-v_{xx}/v_x>1/z$ and $z$ otherwise, and the ceded loss $\hat I(z,x,\tau)$ is the difference from $z$. The reinsurance boundary is $K(z,\tau)=\sup\{x>0: -v_{xx}/v_x(x,\tau)>1/z\}$. For a discrete law $\mathbb P(Z_1=z_j)=p_j>0$ with $0<z_1<\dots<z_N$, the $j$-th reinsurance boundary is

$$K_j(\tau)=\inf\Bigl\{x>0: -\frac{v_{xx}}{v_x}(x,\tau)\le\frac1{z_j}\Bigr\}.$$

Formalization targets

Goal: Theorem 4.5

For a discrete claim law, every $K_j$ is continuously differentiable on $(0,T]$, and for every $\tau\in(0,T]$:

$$K_j(\tau)=0\ \text{ if }z_j\le\tfrac1\lambda;\qquad 0<K_{i_0}(\tau)<\frac{z_{i_0}-1/\lambda}{2c};\qquad 0<K_j(\tau)-K_{j-1}(\tau)<\frac{z_j-z_{j-1}}{2c}\ \ (j>i_0);\qquad \lim_{\tau\to0+}K_j(\tau)=0,$$

where $z_{i_0}$ is the smallest atom above $1/\lambda$.

Milestones

1. Theorem 4.2: $d$ is continuous and nondecreasing on $(0,T]$, and $d(0+)=0<d(\tau)\le\sqrt{(\mu_1+c\gamma)(c\mu_2+\gamma^2)/(\gamma c^3)}$.
2. Lemma 4.3: $v_x,v_\tau\in C^{2,1}$ in $\mathcal{ND}$, $v_{xx}<0$ in $\mathcal{ND}$, and $\hat I(z,x,\tau)=\max\{z+v_x/v_{xx},0\}$ there.
3. Lemma 4.4: $-v_x/v_{xx}=1/\lambda$ at $x=0$, $-v_x/v_{xx}>1/\lambda$ in $\mathcal{ND}$, and $\partial_x(-v_x/v_{xx})\ge2c$ in $\mathcal{ND}$.
4. Section 4.2, p. 18: for $z>1/\lambda$, $K(z,\tau)\le z/(2c)-1/(2c\lambda)$.

Significance

The theorems turn an existence result for a fully nonlinear variational inequality into a usable description of the optimal policy. Claims below $1/\lambda$ are never reinsured; a claim of size $z>1/\lambda$ is partly ceded only when the surplus lies below a barrier that starts at the origin at maturity, stays below $z/(2c)-1/(2c\lambda)$, and stays below the dividend barrier, which is itself bounded by an explicit constant independent of the horizon. For discrete claims the barriers are smooth, ordered, and separated by gaps of at most $(z_j-z_{j-1})/(2c)$. The quantity $-v_x/v_{xx}$, the optimal retention level, is shown to grow at rate at least $2c$ in the surplus; this single monotonicity estimate is what makes the regions of the surplus–time plane ordered and nonoverlapping.

The results are proved in the paper; none of them, nor Theorem 3.1 on which they rest, has a machine-checked proof. Formalizing them requires the parabolic regularity statements of Lemma 4.3 (the paper's proof invokes interior Schauder estimates) and the implicit function theorem in a form that gives one-variable $C^1$ dependence of a level set. Statements of the boundary properties in this mission are posed for any function with the properties of Theorem 3.1, so they can be proved independently of the companion mission.

Difficulty

Most of the elementary statements reduce to a sign or a monotonicity property of $-v_x/v_{xx}$, and the first idea is to differentiate the equation. That requires $v_{xxx}$ and $v_{x\tau}$ to exist as classical derivatives in $\mathcal{ND}$, which the class of Theorem 3.1 does not provide: it gives only two $x$-derivatives and one $\tau$-derivative, and a weak monotonicity of $v_{xx}$. Lemma 4.3's interior regularity is therefore not a formality but the gateway to Lemma 4.4, and its proof uses Hölder estimates for linear parabolic equations, which are not available in Mathlib.

The positivity $d(\tau)>0$ and the limit $d(0+)=0$ are statements about the free boundary itself, not about $v$ at fixed points, and need the uniqueness part of Theorem 3.1 or a comparison argument. The strict inequalities in (4.13)–(4.14) need more than the bound $\partial_x(-v_x/v_{xx})\ge2c$ as stated.

Formalization scope

All objects live in the namespace DynReinsDiv.Barriers. Conventions:

• The claim law is a probability measure μ on $\mathbb R$ with $\mu((-\infty,0))=0$; $F(z)=\mu((-\infty,z])$; no density is assumed. $\mu_1,\mu_2$ are Bochner integrals, finite under the tail condition. The standing hypothesis $0<\gamma<\mu_1$ is a field of the model.
• $v:\mathbb R\to\mathbb R\to\mathbb R$ takes $(x,\tau)$, and the derivatives vx vxx vt are explicit functions: they are HasDerivAt derivatives of the sections at interior points ($x>0$, $0<\tau<T$) and continuous on $[0,\infty)\times[0,T]\setminus\{(0,0)\}$; boundary values (at $x=0$ and $\tau=T$) are the continuous extensions. "$v_{xxx}\ge0$ in the weak sense" is monotonicity of $v_{xx}$ in $x$, "$v_{x\tau}\ge0$" is monotonicity of $v_x$ in $\tau$.
• The only hypothesis on $v$ is the conclusion of Theorem 3.1, bundled as IsTheorem31Solution. The milestone conclusions ($v_{xx}<0$, the bounds on $-v_x/v_{xx}$, $d(0+)=0$) are never hypotheses; with them as hypotheses Theorem 4.5 would be a short mean-value argument.
• $\mathcal L$ is the supremum over measurable retained-loss functions, not its closed form.
• Infima and suprema of empty sets are $0$ in Lean. Theorem 4.2 concludes that $\{x\ge0: v_x=1\}$ is nonempty; $K(z,\tau)$ uses $0$ for the empty set, as the paper does.
• Atoms are indexed by Fin N from $0$. The paper's index $i_0$ is replaced by conditions on $z_j$ and $z_{j-1}$, which also cover laws whose atoms all lie below $1/\lambda$.
• Not formalized: $d(\infty)$ (the horizon is finite; $d(\tau)\le x_2$ for every $\tau\le T$ and every $T$ carries the same content), the $C^\infty$ regularity of $d$ for bounded claims (only sketched in the paper), and the Verification Theorem 3.2.

Contributions welcome: the interior regularity of Lemma 4.3, the monotonicity estimate (4.10), and the derivation of Theorem 4.5 from the milestones.

Selected references

• Chonghu Guan, Zuo Quan Xu, Rui Zhou, Dynamic optimal reinsurance and dividend-payout in a finite time horizon, Mathematics of Operations Research, 2023; read as arXiv:2008.00391v3 (2022). https://arxiv.org/abs/2008.00391

Motivation

Quantum state tomography reconstructs an unknown $d$-dimensional quantum state from measurements on many copies of it. For $n$ qubits, $d = 2^n$, so the number of copies a tomography procedure needs grows exponentially in $n$, and lower bounds on that number decide how far experiments can scale. In many experiments the only measurements available are Pauli measurements: each qubit is measured in the eigenbasis of one of $\sigma_x, \sigma_y, \sigma_z$.

Flammia and Liu, Direct fidelity estimation from few Pauli measurements (arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011), show that the fidelity of an experimental state with a target pure state can be estimated with far fewer copies than full tomography needs. To make the comparison meaningful they also prove that full tomography of a pure state with Pauli measurements requires $\Omega(d^2/\log d)$ copies. That lower bound has two steps. The first builds a large family of nearly orthogonal pure states whose Pauli expectation values are all small, so that Pauli measurements extract little information about which state is present. Its engine is Lemma 1 of the paper (p. 7), the subject of this mission. The second step, an information-theoretic argument over a noisy classical channel, is not in scope.

Setting

Fix $n \ge 1$ qubits and put $d = 2^n$. States are unit vectors $\psi \in \mathbb C^d$, $\|\psi\|_2 = 1$; the overlap $\langle\varphi|\psi\rangle = \sum_x \overline{\varphi_x}\psi_x$ is conjugate-linear in $\varphi$.

The single-qubit Pauli matrices are $I$, $\sigma_x$, $\sigma_y$, $\sigma_z$. A Pauli label $k \in \{0,1,2,3\}^n$ determines the $n$-qubit Pauli operator $W_k = \sigma_{k_1}\otimes\cdots\otimes\sigma_{k_n}$ (with $\sigma_0 = I$). There are $d^2$ labels; the all-zero label gives $W_k = I$. Every $W_k$ is Hermitian and unitary, so the Pauli expectation $\langle\psi|W_k|\psi\rangle$ is a real number in $[-1, 1]$.

A Haar-random state is a vector $\psi$ drawn from the uniform (rotation-invariant) probability measure on the unit sphere of $\mathbb C^d$, a real sphere of dimension $2d - 1$. The constants of the lemma are

$$\varepsilon = \sqrt{9\pi^3(\log 2)\,c},\qquad \tau = \sqrt{72\pi^3},\qquad C_1 = \frac{2}{9\pi^3},$$

with $\log$ the natural logarithm and $c > 0$ a parameter.

Formalization targets

Goal: Lemma 1

Let $\varphi_1, \dots, \varphi_s \in \mathbb C^d$ be states with $s \le 2^{cd}$. Then there is a state $\psi \in \mathbb C^d$ with

$$|\langle\varphi_i|\psi\rangle| \le \varepsilon \quad (1 \le i \le s), \qquad |\langle\psi|W_k|\psi\rangle| \le \tau\sqrt{\log d}/\sqrt d \quad (W_k \ne I).$$

These are (31) and (32) of the paper. The goal is an existence statement with no measure in it.

Milestones (all p. 7)

1. (33): for a state $\varphi$, $|\langle\varphi|\psi\rangle - \langle\varphi|\psi'\rangle| \le \|\psi - \psi'\|_2$.
2. $\mathbb E\langle\varphi|\psi\rangle = 0$ for Haar-random $\psi$.
3. (34): $\Pr[|\langle\varphi|\psi\rangle| \ge \varepsilon] \le 4\exp(-C_1 d\varepsilon^2/\eta^2)$ with $\eta = 1$.
4. (35): $\Pr[(31)\text{ fails for some } i] \le 4\exp(cd\log 2 - C_1 d\varepsilon^2) = 4\cdot 2^{-cd}$.
5. (36): on unit vectors, $|\langle\psi|W_k|\psi\rangle - \langle\psi'|W_k|\psi'\rangle| \le 2\|\psi - \psi'\|_2$.
6. $\mathbb E\langle\psi|W_k|\psi\rangle = 0$ for $W_k \ne I$.
7. (37): $\Pr[|\langle\psi|W_k|\psi\rangle| \ge \tau\sqrt{\log d}/\sqrt d] \le 4\exp(-C_1\tau^2(\log d)/\eta^2)$ with $\eta = 2$.
8. (38): $\Pr[(32)\text{ fails for some } k] \le 4\exp(2\log d - C_1\tau^2(\log d)/4) = 4/d^2$.

Every constant is the paper's; none is replaced by an unspecified absolute constant.

Significance

The result. Lemma 1 is a packing statement: applied repeatedly, it yields $2^{\Omega(d)}$ states that are pairwise almost orthogonal and whose non-identity Pauli expectations are all $O(\sqrt{\log d/d})$. Such states are hard to tell apart with Pauli measurements, since each measurement outcome is nearly unbiased. The paper converts this into the $\Omega(d^2/\log d)$ copy lower bound for full tomography with Pauli measurements (pp. 3, 7–8). Since direct fidelity estimation of an arbitrary pure state uses $O(d)$ copies (for fixed accuracy and failure probability), the lower bound is what shows that the scheme beats tomography followed by a fidelity computation by a factor of about $d$.

Formalizing it. The lemma and its proof are published, but none of it is machine-checked: Mathlib has no Pauli operators, no concentration of measure on spheres with explicit constants, and no Levy lemma. A formal proof needs a concentration inequality on the complex unit sphere with the explicit constant $C_1 = 2/(9\pi^3)$ (or any sharper one), the vanishing of the means by symmetry, and the union bounds. Each milestone is a reusable fact about Haar-random states.

Difficulty

The two union bounds (35) and (38) and the Lipschitz estimates (33) and (36) are elementary. The central difficulty is the tail bounds (34) and (37). The paper obtains them from Levy's lemma, which it cites (P. Lévy, 1951) and does not prove; Levy's lemma rests on the isoperimetric inequality on the sphere, which Mathlib does not have, and (37) concerns a quadratic form of $\psi$ rather than a linear one. Both tail bounds also need a working theory of the uniform measure on the complex unit sphere (rotation invariance, the distribution of a coordinate), little of which exists in Lean today.

A second difficulty is that the printed proof does not cover every parameter. The union bound produces a good $\psi$ only when $4\cdot 2^{-cd} + 4/d^2 < 1$. For small $d$, or small $c$ with few given states, the goal is still true, but a complete proof must handle those cases separately; they are not in the paper.

Formalization scope

• Representation. Basis labels are Q n = Fin n → Fin 2, Pauli labels P n = Fin n → Fin 4, states live in EuclideanSpace ℂ (Q n), and $W_k$ is the entrywise product of single-qubit Pauli matrices (the Kronecker product). $d$ is the real number $2^n$; $\log$ is Real.log; ⟨φ|ψ⟩ is Mathlib's inner ℂ φ ψ.
• Measure. The uniform measure on the sphere is Mathlib's Measure.toSphere of an additive Haar measure on $\mathbb C^d$ (as a real vector space), normalised to total mass one. The paper's "Haar-random vector in $S^{d-1}$" is read as this measure on the unit sphere of $\mathbb C^d$.
• Added hypotheses, all disclosed. The goal assumes $n \ge 1$: at $n = 0$ ($d = 1$) and small $c$ the lemma is false, since every unit vector of $\mathbb C^1$ has overlap $1$ with $\varphi_1$. It assumes $c > 0$, under which $\varepsilon$ is defined. "States" means unit vectors, for the given $\varphi_i$ and for the produced $\psi$. The mean-zero statement for Pauli operators assumes $W_k \ne I$ (for $W_k = I$ the mean is $1$); the paper's "for each $k$" refers to the non-identity labels of (32). "$W_k \ne I$" is formalized as "the label $k$ is not all zeros".
• Non-trivialization. The produced $\psi$ must be a unit vector, so $\psi = 0$ does not satisfy the goal; the given states are unit vectors, so (31) is not trivially false; and the mean-zero milestones assert integrability together with the value of the integral, so they cannot hold merely because a non-integrable integral is $0$.
• Infrastructure needed. Facts about $n$-qubit Pauli operators (Hermitian, unitary, traceless for $W_k \ne I$); rotation invariance of the normalised sphere measure; a concentration inequality for Lipschitz functions on the complex unit sphere with an explicit constant. The concentration inequality and the sphere-measure facts are reusable well beyond this mission and are welcome as separate contributions.

Selected references

• S. T. Flammia and Y.-K. Liu, Direct fidelity estimation from few Pauli measurements, Phys. Rev. Lett. 106, 230501 (2011); arXiv:1104.4695v3. https://arxiv.org/abs/1104.4695
• P. Lévy, Problèmes concrets d'analyse fonctionnelle, Gauthier-Villars, Paris, 1951 (reference [10] of the paper; no stable online link).
• M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089
• P. Hayden, D. W. Leung and A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 95–117 (2006); arXiv:quant-ph/0407049. https://arxiv.org/abs/quant-ph/0407049

Motivation

Many service relationships are dynamic contracts in which the principal cannot observe the agent's effort, only its noisy consequences. Cao, Sun and Tian (Management Science, 2024) study such a relationship when the principal can suspend the agent and must pay a fixed switching cost to restart work. Suspension is a punishment that does not end the relationship, and it is used in practice for platform workers, contractors and franchisees. The paper shows that, when the switching cost and the revenue are low, the optimal contract has a control-band structure: the agent's promised utility is kept inside an interval, the agent is suspended when it falls below the lower end, and work resumes at the upper end. Two-threshold policies of this kind are standard in optimal switching problems with switching costs (Duckworth and Zervos, 2001; Vath and Pham, 2007), whose verification arguments the paper compares with its own.

This mission is the fourth of a series formalizing the analytic core of the paper. It covers the low-switching-cost region (Area III of the paper's Figure 2).

Setting

A Poisson process of arrivals brings revenue $R$ each. The base arrival rate is $\underline\mu\ge0$; if the agent works, at cost $b>0$ per unit of time, the rate becomes $\mu>\underline\mu$. Write $\Delta\mu=\mu-\underline\mu$. The principal's cost rate while the agent works is $c\ge b$, restarting work costs $K>0$, and the principal and the agent discount at rates $0<r\le\rho$. Assumption 1 is $R\Delta\mu>c$. The constants are

$$\beta=\frac b{\Delta\mu},\quad \bar w=\frac{\beta\mu}\rho,\quad \underline v=\frac{\underline\mu R}r,\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}r,\quad \bar V(w)=\frac{R\mu-c-(\rho-r)w}r .$$

The promised utility $w\ge0$ is the state. For a function $f$ on $\mathbb R_+$ with left derivative $f'$, the paper's operators are

$$(\mathcal A_If)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,$$ $$(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu,$$

for the working state $I$ and the suspended state $\emptyset$. A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if $\mathcal A_IV_I\ge0$, $\mathcal A_\emptyset V_\emptyset\ge0$, $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$.

Two families of functions enter. In the suspended state, $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24) solves $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$. In the working state, for $\tilde w<\bar w$, $V_{\tilde w}$ is the $C^1$ solution of the delay differential equation (25), in which $V(w)$ is coupled to the look-ahead value $V((w+\beta)\wedge\tilde w)$, with $V_{\tilde w}=\bar V(\tilde w)$ beyond $\tilde w$; $\mathcal V_{\tilde w}$ is its concavification (Lemma 2), linear below a threshold $\check w(\tilde w)$. Lemma 3's $\hat{\mathrm w}$ is the unique $\tilde w$ with $\mathcal V_{\tilde w}(0)=\underline v$ under Condition 1.

The parameter regions are Condition 1 ($\mu\ge\rho-r$ or $R<\hat R$), Condition 2 (its negation) and Condition 3: Condition 1 and $K<\bar K_1$, or Condition 2 and $K<\underline K$, with $\hat R$ (28), $\bar K_1$ (K1) and $\underline K$ (33) explicit thresholds.

The paper uses three different hats: Definition 1's payment threshold $\hat w$, Lemma 3's upright $\hat{\mathrm w}$, and Proposition 6's bold $\hat{\mathbf w}$, the upper end of the control band.

Formalization targets

Goal: Proposition 7, first claim

Under Condition 3 there are parameters $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ satisfying Proposition 6 such that

$$V_I(w)=\begin{cases}V_{\mathsf c}(w),&w<\underline\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w),&w\ge\underline\vartheta\end{cases},\qquad V_\emptyset(w)=\begin{cases}V_{\mathsf c}(w),&w<\bar\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w)-K,&w\ge\bar\vartheta\end{cases}\qquad(46)$$

satisfy (20)–(22).

Proposition 6

Under Condition 3 there is $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ with $\mathsf c>0$, $\underline\vartheta<\bar\vartheta<\hat{\mathbf w}$ and value matching and smooth pasting at both thresholds:

$$\mathcal V_{\hat{\mathbf w}}(\underline\vartheta)=V_{\mathsf c}(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}'(\underline\vartheta)=V_{\mathsf c}'(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}(\bar\vartheta)=V_{\mathsf c}(\bar\vartheta)+K,\quad \mathcal V_{\hat{\mathbf w}}'(\bar\vartheta)=V_{\mathsf c}'(\bar\vartheta)>1 .$$

Milestones

Lemma EC.4 (the first step of the EC.3.9 construction), Proposition 6, and the two hardest parts of (20) at the constructed tuple: Lemma EC.12 ($\mathcal A_\emptyset V_\emptyset\ge0$ on $[\bar\vartheta,\hat{\mathbf w})$) and Lemma EC.13 ($\mathcal A_IV_I\ge0$ below $\underline\vartheta$). The other steps of the construction are posed as further statements of the mission without milestone status: Lemma EC.7 (the root of $\psi=K$ under Condition 1), Lemma EC.8 and Lemma EC.11 (the Condition 2 counterparts of EC.4 and EC.7).

Significance

Proposition 7 is the analytic certificate behind the paper's Theorem 5: combined with the verification Theorem 1, it shows that the control-band contract is optimal in the low-cost region, and that the principal's value is $V_\emptyset(w)-w$. Without it the third case of the paper's main Theorem 2 is unproved. The construction of Proposition 6 also gives a computable description of the band, which the paper uses for its numerical illustrations.

The results are proved in the paper's e-companion; none of them has a machine-checked proof. This mission states the analytic part as Lean targets. The delay-ODE layer (existence, uniqueness and shape of $V_{\tilde w}$) is shared with the first mission of the series, and Proposition 7's proof depends on it. The stochastic contract model, the verification theorem and the optimality Theorems 1–5 are not formalized in this series.

Difficulty

Each piece of (20)–(22) is a one-variable inequality, but the functions are not explicit. $\mathcal V_{\hat{\mathbf w}}$ is defined through a delay equation, and the band's endpoints are defined implicitly through four nested steps: matching at $\underline\theta$, a range bound $\underline\theta^0$, an upper threshold $\bar\theta(\underline\theta)$ and a root of a gap function $\psi$. The natural argument, convexity or concavity of $\mathcal A_IV_I$ on the suspension region, fails: on $[0,\underline\vartheta)$ the function $\mathcal A_IV_I$ mixes $V_{\mathsf c}$ with the look-ahead value $V_I(w+\beta)$ and is not convex (p. 28), so the convexity arguments of the switching literature do not apply. The paper's proof of this single inequality occupies EC.3.12, with eight auxiliary lemmas.

Formalization scope

Functions are ℝ → ℝ and every statement quantifies over $w\ge0$. The standing assumptions are $0\le\underline\mu<\mu$, $0<b\le c$, $K>0$, $0<r\le\rho$ and Assumption 1; $\underline\mu\ge0$ and $b>0$ are disclosed additions. Conventions:

• $f'$ in $\mathcal A_I,\mathcal A_\emptyset$ is the left derivative; derivatives of $V_{\tilde w}$, $\mathcal V_{\tilde w}$ are taken within $\mathbb R_+$.
• (20) is posed for $w>0$: at $0$ the left derivative does not exist and $V_{\mathsf c}'(0^+)=+\infty$.
• $V_{\tilde w}$ is a solution of (25)–(26) chosen when one exists; $\check w$, $\hat{\mathrm w}$, $\bar K_1$, $\underline\theta^0$, $\bar\theta$ are infima or suprema of sets the paper describes; $\tilde w(\underline\theta)$, $C(\underline\theta)$ are chosen matching pairs.
• "Increasing/decreasing" is strict.
• $\underline K$ (33) uses the corrected bracket $((\rho-\mu)/\rho)\beta$ in place of the printed $(r/\rho)\beta$; the printed form contradicts the proof's (EC.69).
• Proposition 6's "$\hat{\mathbf w}<\hat{\mathrm w}$" is read as $\hat{\mathbf w}<\bar w$ in the Condition 2 case, where $\hat{\mathrm w}$ does not exist; $0<\underline\vartheta$ is stated.
• The goal is existential over Proposition 6 tuples. Lemmas EC.12 and EC.13 are stated at the tuple constructed in EC.3.9, in both cases of Condition 3; EC.13 is posed on $(0,\underline\vartheta)$.
• Lemma EC.11's second limit is printed at $0$; it is stated at $\breve{\underline\theta}$, as the proof computes it.

The tuple is never defined by the property that (46) satisfies (20)–(22); the construction definitions are Steps 1–4 of EC.3.9 only, and the goal requires all of Proposition 6's conclusions. The second claim of Proposition 7, (48) on the contract's utility, is out of scope.

A complete development needs existence, uniqueness and regularity for the linear delay equation (25) (reusable for other delay problems), implicit-function arguments for $\tilde w(\underline\theta)$, and the sign analysis of EC.3.12. Proofs of single milestones, and of the delay-ODE lemmas of the series' first mission, are welcome.

Selected references

• P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
• K. Duckworth, M. Zervos, A model for investment decisions with switching costs, Annals of Applied Probability 11(1), 2001. https://doi.org/10.1214/aoap/998926992
• V. L. Vath, H. Pham, Explicit solution to an optimal switching problem in the two-regime case, SIAM Journal on Control and Optimization 46(2), 2007. https://doi.org/10.1137/050638783

Motivation

Centralized matching markets (kidney exchange, ride hailing, freight and labor platforms) repeatedly decide which waiting participants to match now and which to hold for a better opportunity later. Matching early collects value sooner; waiting lets the platform see more arrivals and avoid matches that later turn out to be wasteful. A natural yardstick is the best set of matches that could have been made with hindsight from all arrivals up to a given time, and the question is how far an online policy, which cannot see the future, must fall behind that yardstick.

Kerimov, Ashlagi and Gurvich (SSRN 3824407, September 2022; Management Science 2023, doi:10.1287/mnsc.2021.01215) answer this for multi-way matching networks with patient agents. They identify a single parameter of the fluid relaxation, the general position gap $\epsilon$, and show that the regret against the hindsight benchmark can be kept at order $\epsilon^{-1}$ at all times, and that no policy does better in order on non-trivial networks. This mission formalizes the upper bound. The paper places itself next to constant-regret results for online packing (Bumpensanti and Wang 2020; Vera and Banerjee 2021), where resolving a linear program at each arrival achieves bounded regret.

Setting

There are $n$ agent types and $d$ matches. Match $m$ is a set $\mathcal A(m)$ of at least two types, every type belongs to some match, and the matching matrix $M\in\{0,1\}^{n\times d}$ has $M_{im}=1$ iff $i\in\mathcal A(m)$. Performing match $m$ uses one agent of each type in $\mathcal A(m)$ and earns $r_m>0$. Time is discrete; at each time $t=1,2,\dots$ one agent arrives, of type $i$ with probability $\lambda_i>0$, $\sum_i\lambda_i=1$, independently over time. $A^t_i$ counts the type-$i$ arrivals by time $t$.

A matching policy records $D^t_m$, the number of times match $m$ has been performed by time $t$. It is admissible when it is non-anticipative and only matches agents present: $MD^t\le A^t$. The pre-match queue is $Q^t=A^t-MD^{t-1}$, the value collected is $\mathcal R^{D,t}=\mathbb E[r\cdot D^t]$, and the hindsight benchmark is

$$\mathcal R^{*,t}=\mathbb E\big[\max\{r\cdot y: My\le A^t,\ y\in\mathbb Z^d_{\ge0}\}\big].$$

The static-planning problem is the linear program

$$\text{(SPP)}\qquad \max\ r\cdot z\quad\text{s.t.}\quad Mz+s=\lambda,\ z\ge0,\ s\ge0.$$

For an optimal $(z^*,s^*)$ let $\mathcal M_+=\{m:z^*_m>0\}$ (active matches), $\mathcal M_0$ the rest (redundant matches), $\mathcal Q_+=\{j:s^*_j>0\}$ (under-demanded types) and $\mathcal Q_0$ the rest (over-demanded types). The network satisfies general position (GP) if (SPP) has a unique optimal solution and it is non-degenerate, $|\mathcal M_+|+|\mathcal Q_+|=n$. The general position gap is the smallest positive basic value,

$$\epsilon=\min_{m\in\mathcal M_+}z^*_m\ \wedge\ \min_{j\in\mathcal Q_+}s^*_j .$$

The exhaustive resolving policy with inter-action delay $\tau$ acts only at the epochs $t_k=k\tau$. There it performs an optimal solution of the integer program $\max\{r\cdot z: Mz\le Q^{t_k},\ z\in\mathbb Z^d_{\ge0}\}$ with the redundant matches removed, and then discards the leftover agents of the under-demanded types.

Formalization targets

Goal: Theorem 3.1 (Upper bound), p. 14

There are constants $\kappa,\Gamma>0$ depending only on $n,d,M,r$ such that, under GP, the exhaustive resolving policy with $\tau=\lceil\kappa\epsilon^{-1}\rceil$ (any tie-breaking) is admissible and

$$\mathcal R^{*,t}-\mathcal R^{D,t}\le\Gamma\,\epsilon^{-1}\qquad\text{for all }t\ge1 .$$

The constants are not fixed, so the goal survives any improvement of them.

Milestones

1. §2, p. 8: $\mathcal R^{*,t}=\max_{D}\mathcal R^{D,t}$, attained by the ultimate batching policy.
2. §4.2, (4), p. 20: under GP the optimal basis $\mathcal B$ is invertible, $(z^*_{\mathcal M_+},s^*_{\mathcal Q_+})=\mathcal B^{-1}\lambda$, and the entries of $\mathcal B^{-1}$ are bounded by a constant of the topology.
3. §4.2, p. 20: $\theta=\sum_{m\in\mathcal M_+}r_my^m$ is the optimal dual of (SPP), $\theta\ge0$, and $\theta_i>0$ on $\mathcal Q_0$.
4. Lemma 4.1, p. 19 (optimality test): a policy without redundant matches whose over-demanded queues have mean $O(\epsilon^{-1})$ has regret $O(\epsilon^{-1})$.
5. Lemma 4.2, p. 21: a Foster–Lyapunov drift condition bounds stationary means (Glynn and Zeevi 2008).
6. (11), p. 23: $\mathbb E_\pi[h^*(Q^0)]=O(\epsilon^{-1})$ for the stationary law of the epoch chain.
7. App. D, p. 49: $\mathbb E_{\mathbf 0}[h^*(Q^{t_k})]=O(\epsilon^{-1})$ for all $k\ge1$.

Here $h^*(u)$ is the $\theta$-weighted leftover in $\mathcal Q_0$ after an optimal integer matching of $u$ (display (7)).

Significance

The upper bound says that, under GP, hindsight-optimal performance up to an additive constant is achievable at every time simultaneously, not just at a known horizon. Long-run average optimality and near-optimality under discounting follow (Remark 2.1). The bound also quantifies the cost of acting often: the delay $\tau$ and the regret both scale with $\epsilon^{-1}$, so networks close to degeneracy force batching. Combined with the paper's lower bound, $\epsilon^{-1}$ is the right order on non-trivial networks.

The result has a printed proof (§4, Appendices B and D) but no machine-checked one. Several intermediate statements of the printed proof do not hold as stated and are not posed here. The goal and the stated displays (11) and App. D are posed as the paper states them, so a formal proof requires a correct argument for the uniform-in-$\lambda$ bound on the over-demanded queues. Lemma 4.1, the basis and duality facts and Lemma 4.2 are self-contained and checkable on their own.

Difficulty

The obvious approach compares the policy's realized matches with the fluid optimum $t\,z^*$ and controls the deviation with concentration bounds. That gives errors of order $\sqrt t$, not a constant. The constant comes from showing that the over-demanded queues stay of order $\epsilon^{-1}$ uniformly in time and in $\lambda$. Between epochs these queues behave like a multidimensional reflected random walk whose drift toward zero is only of order $\epsilon\tau$, while its fluctuations over an epoch are of order $\sqrt\tau$. The delay $\tau\asymp\epsilon^{-1}$ balances the two, but the queue state enters through the integer program (3), whose solution changes discontinuously with the queues, and the quantities that measure the drift are signed combinations of arrival counts, to which the usual one-sided concentration bounds for nonnegative sums do not apply. On top of this every constant must be independent of $\lambda$.

Formalization scope

• Types are Fin n and matches Fin d (0-based); the topology with its two standing assumptions ($|\mathcal A(m)|\ge2$, every type in a match) is a structure, and $\lambda>0$ with $\sum\lambda_i=1$ and $r>0$ are hypotheses.
• Time is $\mathbb N$; "for all $t>0$" is $t\ge1$. The arrival at time $s+1$ is the $s$-th entry of a path $\omega:\mathbb N\to$ Fin n. Expectations at horizon $t$ are finite sums over the first $t$ arrivals weighted by $\prod\lambda_{\omega_s}$, so no expectation is a default value.
• Admissible policies are non-anticipative cumulative counts with $MD^t\le A^t$ and no rejections. The resolving policy's removal of under-demanded leftovers acts on its own virtual queue, which agrees with the actual queue on $\mathcal Q_0$; its matches are feasible without removals, so it is admissible.
• (3) is solved with the redundant matches set to zero, and statements quantify over every tie-breaking selection. A selection exists (a sanity file exhibits one), so these statements are not vacuous.
• GP is a hypothesis on an explicit pair $(z^*,s^*)$; $\epsilon$ is the minimum of the positive basic values. The basis inverse is never a matrix-inverse function: statements assert the existence of a two-sided inverse.
• $h^*$ is defined in the form $\min\{\sum_{\mathcal Q_0}\theta_is_i: Mz+s=u,\ z_{\mathcal M_0}=0\}$, equivalent to (7) under the paper's reduction $\mathcal M_0=\emptyset$; $\theta$ is any solution of the complementary-slackness system, which is unique under GP.
• Every $O(\cdot)$ is an explicit constant, quantified after the topology and $r$ and before $\lambda$. Placing it after $\lambda$ would turn the theorem into a per-instance boundedness statement and is ruled out.
• A trivializing formalization (some unspecified policy, a $\tau$ independent of $\epsilon$, or GP replaced by an unsatisfiable condition) is ruled out: the policy is constructed, $\tau=\lceil\kappa/\epsilon\rceil$, and a sanity file proves GP for the Figure 1 network with $\epsilon=1/5$.
• Not posed: the lower bound of Theorem 3.1, Proposition 4.1 (8)–(9), Lemmas B.1–B.2, Proposition B.1 and displays (21)–(22), which do not hold as printed; Theorem 5.2 and §6.

Contributions welcome: proofs of the LP facts (milestones 2–3) and Lemma 4.1, a Mathlib-ready proof of Lemma 4.2, and any correct argument for the epoch bounds.

Selected references

• S. Kerimov, I. Ashlagi, I. Gurvich, Dynamic Matching: Characterizing and Achieving Constant Regret, SSRN 3824407 (version of Sep 14, 2022); Management Science, 2023. https://ssrn.com/abstract=3824407, https://doi.org/10.1287/mnsc.2021.01215
• P. W. Glynn, A. Zeevi, Bounding stationary expectations of Markov processes, in Markov Processes and Related Topics, IMS Collections 4, 2008. https://doi.org/10.1214/074921708000000381
• P. Bumpensanti, H. Wang, A re-solving heuristic with uniformly bounded loss for network revenue management, Management Science 66, 2020. https://doi.org/10.1287/mnsc.2019.3365
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997.