Probability

Motivation

Scheduling jobs whose processing times are not known in advance is a basic problem of production planning, project management and computing systems. In the stochastic machine scheduling model only the distribution of each processing time is known beforehand; the actual duration of a job is revealed when the job completes. A solution is then not a schedule but a scheduling policy, which decides at every point in time what to start next on the basis of what has been observed so far.

For precedence-constrained problems, constant-factor guarantees for policies were long unavailable. Möhring, Schulz and Uetz (J. ACM 1999) introduced LP relaxations with load inequalities for stochastic scheduling and obtained the first constant-factor policies for independent jobs. In the deterministic setting, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 2001) gave a list scheduling algorithm with deliberate idle times for $\mathrm P\,|\,r_j,\mathit{prec}\,|\sum w_jC_j$. Skutella and Uetz (SIAM J. Comput. 2005) combined the two and gave the first constant-factor approximation for stochastic scheduling with precedence constraints and release dates. This mission formalizes that result.

Setting

A finite set $V$ of jobs is to be scheduled on $m\ge1$ identical parallel machines, nonpreemptively. Precedence constraints are the arcs $A$ of an acyclic digraph: an arc $(i,j)$ requires $j$ to start no earlier than $i$ completes, and $i$ is a predecessor of $j$ if a directed path leads from $i$ to $j$. Job $j$ has a release date $r_j\ge0$, before which it must not start, and a weight $w_j\ge0$. Following §2 of the paper, release dates are assumed to respect the precedence constraints (Assumption 2.1: $r_i\le r_j$ whenever $i$ is a predecessor of $j$).

The processing time of job $j$ is a random variable $P_j\ge0$ with finite mean $\mathrm E[P_j]$; the $P_j$ are stochastically independent. For a realization $p$ of the processing times, a feasible schedule assigns start times $S_j\ge r_j$ such that $S_i+p_i\le S_j$ for every arc and at most $m$ jobs are in process at any time. A policy $\Pi$ maps realizations to feasible schedules; it is nonanticipatory if what it has started by time $t$ depends only on what has been observed by $t$. The completion time of $j$ under $\Pi$ is $C^\Pi_j(P)=S^\Pi_j(P)+P_j$.

The coefficient of variation is $\mathrm{CV}[P_j]=\sqrt{\mathrm{Var}[P_j]}/\mathrm E[P_j]$; the mission assumes $\mathrm{CV}[P_j]\le\sqrt\Delta$ for all $j$ and some $\Delta\ge0$. With $\mu_j=\mathrm E[P_j]$, the set function

$$f(W)=\frac1{2m}\Big(\big(\textstyle\sum_{j\in W}\mu_j\big)^2+\sum_{j\in W}\mu_j^2\Big)-\frac{(m-1)(\Delta-1)}{2m}\sum_{j\in W}\mu_j^2$$

defines the LP relaxation: minimize $\sum_jw_jC^{\mathrm{LP}}_j$ subject to $\sum_{j\in W}\mu_jC^{\mathrm{LP}}_j\ge f(W)$ for all $W\subseteq V$, $C^{\mathrm{LP}}_j\ge C^{\mathrm{LP}}_i+\mu_j$ for $(i,j)\in A$, and $C^{\mathrm{LP}}_j\ge\mu_j$.

Algorithm CMNS takes a priority list $L$ and a parameter $\beta$. Whenever a machine is idle and the first job of the residual list (the jobs not yet scheduled) is available, it is scheduled. Otherwise the first available job $j$ of the residual list is deliberately delayed; idle machines accumulate deliberate idle time charged to $j$, and once $j$ has been charged $\beta\,\mathrm E[P_j]$ it is scheduled out of order. The critical chain of a job $j$ is traced backwards through critical predecessors (those completing last, after $r_j$); its length is $\ell_j(p)$.

Formalization targets

Goal: Theorem 4.1

If $C^{\mathrm{LP}}$ is an optimal LP solution, $L$ orders the jobs by nondecreasing $C^{\mathrm{LP}}_j$ and $\beta>0$, then for every feasible nonanticipatory policy $\Pi$

$$\mathrm E\Big[\sum_jw_jC^{\mathrm{CMNS}}_j(P)\Big]\le(1+\beta)\Big(1+\frac1\beta+\max\Big\{1,\frac{m-1}m\Delta\Big\}\Big)\,\mathrm E\Big[\sum_jw_jC^\Pi_j(P)\Big].$$

Milestones

1. Observation 2.4: each job is charged at most $\beta\,\mathrm E[P_j]$; idle time while $j$ waits is charged to jobs before $j$; no deliberate idle time is uncharged.
2. Lemma 2.5: the per-realization bound $C_j(p)\le\frac{m-1}m\ell_j(p)+\frac1mr_j+\frac1m\big(\sum_{i\in B_j}(p_i+\beta\mathrm E[P_i])+\sum_{i\in O_j(p)}p_i\big)$.
3. Lemma 2.6: $\mathrm E[\sum_{i\in O_j(P)}P_i]=\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]$.
4. Lemma 2.7: $\frac1m\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]\le\frac1\beta\mathrm E[\ell_j(P)]$.
5. Theorem 2.8: $\mathrm E[C_j(P)]\le\big(\frac{m-1}m+\frac1\beta\big)\mathrm E[\ell_j(P)]+\frac{1+\beta}m\sum_{i\in B_j}\mathrm E[P_i]+\frac1mr_j$.
6. Theorem 3.1: the load inequalities $\sum_{j\in W}\mathrm E[P_j]\mathrm E[C^\Pi_j(P)]\ge f(W)$.
7. §3: expected completion times of any policy are LP-feasible, so the LP optimum is a lower bound.
8. Lemma 3.3: $\frac1m\sum_{k\le j}\mathrm E[P_k]\le\big(1+\max\{1,\frac{m-1}m\Delta\}\big)C^{\mathrm{LP}}_j$ along the LP order.
9. §4: $\ell_j(p)\le C_j(p)$ in any feasible schedule, so $\mathrm E[\ell_j(P)]$ is a lower bound for every policy.

Significance

The theorem gives a policy with a performance guarantee independent of the number of jobs for $\mathrm P\,|\,r_j,\mathit{prec}\,|\,\mathrm E[\sum w_jC_j]$, using only the expected processing times and a bound on their coefficients of variation. For NBUE distributions ($\Delta=1$) and $\beta=1/\sqrt2$ it yields $3+2\sqrt2\approx5.83$, matching the deterministic guarantee of Chekuri et al. The analysis separates cleanly into an algorithmic half (Theorem 2.8, valid for arbitrary distributions) and a polyhedral half (load inequalities and Lemma 3.3), both reused for the in-forest results of the same paper and in later work on stochastic scheduling.

The result is proved in the paper; it has no machine-checked proof. Formalizing it produces a precise definition of nonanticipatory policies and of a list scheduling algorithm with deliberate idle times in continuous time, a formal proof of the Möhring–Schulz–Uetz load inequalities, and a verified approximation guarantee for a stochastic scheduling policy.

Difficulty

Lemma 2.6 is the step where the stochastic setting departs from the deterministic one: the set $O_j(P)$ of out-of-order jobs is random and correlated with the schedule, and the identity holds only because the decision to start a job out of order is taken before its processing time is revealed. Making this rigorous requires a formal notion of nonanticipation and an independence argument over a random set. On the algorithmic side, the bookkeeping of deliberate idle time, which accumulates at a rate equal to the number of idle machines, must be made precise at instants where several jobs start, including jobs of length zero. The load inequalities compare every nonanticipatory policy at once and involve second moments of the processing times, so they cannot be checked policy by policy.

Formalization scope

Jobs form a finite type; arcs are a relation whose transitive closure is irreflexive; machine capacity is the counting condition "at most $m$ jobs in process", with half-open processing intervals. Processing times may be zero. The CV bound is encoded as finite second moments, positive means and $\mathrm{Var}[P_j]\le\Delta\,\mathrm E[P_j]^2$.

Algorithm CMNS is characterized by its rules: a decision order nondecreasing in time, the scheduling rule at each decision, and the condition that after the decisions at any time nothing remains to be done. A CMNS policy is a map $\sigma$ with this property for every realization. Nonanticipation and measurability of $\sigma$, which the paper asserts without proof (p. 795; §5), are hypotheses. Critical chains use a fixed tie-breaking order.

Standing assumptions and added hypotheses: independence, Assumption 2.1, $r_j\ge0$, $w_j\ge0$ and finite means appear in every statement where they are used. $\beta>0$ is assumed wherever $1/\beta$ appears (Lemma 2.7, Theorem 2.8), where the page allows $\beta\ge0$ with $1/0=\infty$. Lemma 2.6 assumes that $L$ is a linear extension, as in the surrounding Lemma 2.5 and Theorem 2.8; with zero processing times it fails otherwise. Comparator policies have integrable completion times and, like $\sigma$, are measurable for the law of $P$, which §5's requirement that every policy be universally measurable implies.

The goal is not trivialized: comparators range over every feasible nonanticipatory policy, not over list policies or the algorithm itself; $C^{\mathrm{LP}}$ is optimal over all $W\subseteq V$, not merely feasible; and the expected cost of CMNS is asserted to be finite, so neither side can collapse to a default integral value.

Contributions welcome: proofs of any milestone, in particular Theorem 3.1 and Lemma 3.3, which are reusable for the companion in-forest mission, and a proof that the CMNS rules determine a unique, nonanticipatory, measurable policy.

Selected references

• M. Skutella, M. Uetz, Stochastic machine scheduling with precedence constraints, SIAM J. Comput. 34(4) (2005) 788–802. https://doi.org/10.1137/S0097539702415007
• R. H. Möhring, A. S. Schulz, M. Uetz, Approximation in stochastic scheduling: the power of LP-based priority policies, J. ACM 46(6) (1999) 924–942. https://doi.org/10.1145/331524.331530
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1) (2001) 146–166. https://doi.org/10.1137/S0097539797327180
• R. H. Möhring, F. J. Radermacher, G. Weiss, Stochastic scheduling problems I: General strategies, Z. Oper. Res. 28 (1984) 193–260. https://doi.org/10.1007/BF01919323

Motivation

Linear stochastic programs with recourse model decisions that are taken after an uncertain parameter $\xi$ has been observed: the decision is a decision rule $x(\xi)$, a function of the data. Computing the optimal value exactly is intractable in general. Dyer and Stougie showed that already two-stage linear stochastic programs are #P-hard (Math. Program. 2006), and the same holds for the one-stage problem $\mathcal{SP}$ below even when $\mathbb P$ is uniform on a cube.

A widely used remedy restricts decision rules to be linear in $\xi$. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduced this restriction in robust optimization (Math. Program. 2004); Shapiro and Nemirovski (2005) and Chen, Sim, Sun and Zhang (Oper. Res. 2008) carried it into stochastic programming. The restriction yields an upper bound, but on its own it says nothing about how much optimality is lost. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; published in Math. Program. 2011) also apply the linear restriction to the dual multipliers. This gives a lower bound, so the gap between the two computable bounds estimates the approximation error. This mission formalizes the paper's model result for the case of fixed recourse and polyhedral support (§2, Theorem 1).

Setting

Uncertainty is a probability measure $\mathbb P$ on $(\mathbb R^k, \mathfrak B(\mathbb R^k))$. The support $\Xi$ of $\mathbb P$ is the smallest closed set of probability one. A decision rule is an element of $\mathcal L^2_{k,n}$, the Borel measurable, square-integrable functions $\mathbb R^k \to \mathbb R^n$. Inequalities between vectors and matrices are componentwise.

The data are a fixed recourse matrix $A \in \mathbb R^{m\times n}$, matrices $C \in \mathbb R^{n\times k}$ and $B \in \mathbb R^{m\times k}$ giving the costs $c(\xi) = C\xi$ and right-hand sides $b(\xi) = B\xi$, and $W \in \mathbb R^{l\times k}$, $h \in \mathbb R^l$. The stochastic program is

$$\mathcal{SP}:\quad \min_{x \in \mathcal L^2_{k,n}} \ \mathbb E\big(c(\xi)^\top x(\xi)\big) \quad\text{s.t.}\quad Ax(\xi) \le b(\xi)\ \ \mathbb P\text{-a.s.}$$

The standing assumptions of §2 are:

• the support is the nonempty bounded polyhedron $\Xi = \{\xi : W\xi \ge h\}$ (2.1a);
• (2.1b) holds: the first two rows of $W$ are $e_1^\top$ and $-e_1^\top$, the remaining rows form $\widehat W$, and $h = (1,-1,0,\dots,0)$, so that $\xi_1 = 1$ on $\Xi$;
• $\Xi$ spans $\mathbb R^k$.

The second-order moment matrix is $M = \mathbb E(\xi\xi^\top)$. $\mathcal{SP}$ is strictly feasible (2.9) if some $\bar x \in \mathcal L^2_{k,n}$, $\bar s \in \mathcal L^2_{k,m}$ and $\varepsilon > 0$ satisfy $A\bar x(\xi) + \bar s(\xi) = b(\xi)$ and $\bar s(\xi) \ge \varepsilon e$ almost surely.

The two approximations are as follows.

• Primal linear decision rules, $\mathcal{SP}^u$: minimize $\operatorname{Tr}(MC^\top X)$ over $X \in \mathbb R^{n\times k}$, $S \in \mathbb R^{m\times k}$ with $AX\xi + S\xi = B\xi$ and $S\xi \ge 0$ almost surely.
• Dual linear decision rules, $\mathcal{SP}^l$: minimize $\mathbb E(c(\xi)^\top x(\xi))$ over $x \in \mathcal L^2_{k,n}$, $s \in \mathcal L^2_{k,m}$ with $\mathbb E\big([Ax(\xi)+s(\xi)-b(\xi)]\xi^\top\big) = 0$ and $s \ge 0$ almost surely.

Formalization targets

Goal: Theorem 1 (p. 10)

Under the standing assumptions, $\widehat W \ne 0$ (see Formalization scope) and strict feasibility,

$$\operatorname{val}\mathcal{SP}^u = \operatorname{val}(2.3) \quad\text{and}\quad \operatorname{val}\mathcal{SP}^l = \operatorname{val}(2.8),$$

where (2.3) and (2.8) are the linear programs

$$(2.3)\quad \min_{X,\Lambda}\ \operatorname{Tr}(MC^\top X)\ \text{ s.t. }\ AX + \Lambda W = B,\ \Lambda h \ge 0,\ \Lambda \ge 0,$$ $$(2.8)\quad \min_{X,S}\ \operatorname{Tr}(MC^\top X)\ \text{ s.t. }\ AX + S = B,\ (W - he_1^\top)MS^\top \ge 0.$$

Milestones, in the order the proof uses them

1. §2.2 (p. 5). The almost-sure constraints of $\mathcal{SP}^u$ hold on all of $\Xi$, and $AX\xi + S\xi = B\xi$ a.s. is equivalent to $AX + S = B$.
2. Proposition 1 (p. 5). If $\Xi$ is nonempty, then $z^\top\xi \ge 0$ on $\Xi$ if and only if $z = W^\top\lambda$ for some $\lambda \ge 0$ with $h^\top\lambda \ge 0$.
3. Proposition 2 (p. 7). $M$ is positive definite and invertible.
4. §2.4 (p. 7). $\operatorname{val}\mathcal{SP}^l$ equals the optimal value of the moment problem (2.6).
5. Proposition 3 (p. 7). If $\widehat W \ne 0$, then $\emptyset \ne \operatorname{int}\mathcal K \subseteq \mathcal K_{\mathbb P} \subseteq \mathcal K$, for the polyhedral cone $\mathcal K = \{z : (W-he_1^\top)z \ge 0\}$ and the moment cone $\mathcal K_{\mathbb P} = \{\mathbb E(s(\xi)\xi) : s \in \mathcal L^2_{k,1},\ s \ge 0\}$.
6. Proposition 4 (p. 9). Under strict feasibility and $\widehat W \ne 0$, (2.6) and (2.8) have the same optimal value.

Significance

Because $\mathcal{SP}^u \ge \mathcal{SP} \ge \mathcal{SP}^l$, Theorem 1 brackets the value of an intractable stochastic program between two explicit linear programs. The sizes of these programs are polynomial in $k, l, m, n$. They depend on $\mathbb P$ only through its support and its second-order moment matrix. The difference $\operatorname{val}(2.3) - \operatorname{val}(2.8)$ is therefore a computable certificate of how much the linear-decision-rule restriction can lose. Sections 3 and 4 of the paper extend the same scheme to random recourse (semidefinite programs) and to multistage problems; they are the subjects of the companion missions 2 and 3.

The theorem is proved in the paper. As far as a search of the platform shows, none of the statements above has a machine-checked proof. A formal proof would check the measure-theoretic steps that the paper passes over quickly. These are the passage from "almost surely" to "on the support", the density argument behind $\operatorname{int}\mathcal K \subseteq \mathcal K_{\mathbb P}$, and the approximation argument of Proposition 4. A formal proof would also produce reusable results on robust counterparts of polyhedral constraints and on moment cones.

Difficulty

The primal half is robust-optimization duality. Its only delicate point is that almost-sure constraints become constraints on all of $\Xi$, which uses the fact that every point of the support is charged. The dual half is harder. The constraint "$SM$ has rows in $\mathcal K_{\mathbb P}$" is a family of moment problems over nonnegative square-integrable densities, and $\mathcal K_{\mathbb P}$ is in general not closed. Replacing it by the polyhedral cone $\mathcal K$ is exact only up to the boundary, and it is strict feasibility that removes the boundary effect. Without strict feasibility the optimal values of (2.6) and (2.8) are only known to bracket each other. The proof of Proposition 3 also needs a description of the closed cone generated by $\Xi$, and this description uses (2.1b).

Formalization scope

Vectors in $\mathbb R^k$ are Fin k → ℝ and matrices are Matrix (Fin m) (Fin k) ℝ. The paper's 1-based indices are 0-based in Lean, so $e_1$ is index 0 and the rows of (2.1b) are rows 0 and 1. The data form a structure Setting, and the standing assumptions form one predicate Standing. The support is encoded by three conditions on $\Xi$: it is closed, $\mathbb P(\Xi^c) = 0$, and every ball centred in $\Xi$ has positive mass. This is equivalent to "smallest closed set of probability one"; $\mathbb P(\Xi) = 1$ alone would not be enough. Decision rules are measurable functions with MemLp x 2 P. Expectations of vector- and matrix-valued quantities are written entrywise as Bochner integrals. Under the standing assumptions $\xi$ is bounded almost surely, so every integrand involved is integrable and no integral defaults to $0$.

"Equivalent" means equal optimal values. Each optimal value is the infimum of the objective over the feasible set in EReal: $+\infty$ if the problem is infeasible and $-\infty$ if it is unbounded below. A one-sided inequality between the values, or the bare statement that the problems are linear programs, is not Theorem 1 and does not close the goal. Strict feasibility is a hypothesis of both equalities, as printed. Proposition 1 is stated for any $W, h$ with a nonempty polyhedron, since nonemptiness is the only property of $\Xi$ it uses. Proposition 3, Proposition 4 and Theorem 1 carry one hypothesis the paper does not state, $\widehat W \ne 0$ (some row of $W$ below the first two is nonzero). The printed statements are false without it: for $k = 1$, $W = (1,-1)^\top$, $h = (1,-1)^\top$, $\mathbb P = \delta_1$ every assumption holds, $W - he_1^\top = 0$, so $\mathcal K = \mathbb R$ while $\mathcal K_{\mathbb P} = [0,\infty)$, and (2.8) loses the sign constraint $S \ge 0$ that (2.6) keeps. Under the standing assumptions the hypothesis is automatic whenever $k \ge 2$. Theorem 1's closing sentence ("the sizes of these linear programs are polynomial … efficiently solvable") is informal and is not formalized.

A complete development needs strong LP duality or Farkas' lemma for inequality systems, the support of a measure in $\mathbb R^k$, density of $L^2$-densities in nonnegative measures, and basic facts on interiors of polyhedral cones. The Farkas lemma is on the platform (LinearOptimization.farkas_lemma). Proofs of the milestones are welcome independently. Proposition 1 and Proposition 3 are reusable outside this paper.

Selected references

• D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online 2009/02/2218 (2009); Math. Program. 130 (2011) 177–209. https://doi.org/10.1007/s10107-009-0331-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
• X. Chen, M. Sim, P. Sun, J. Zhang, A linear decision-based approximation approach to stochastic programming, Oper. Res. 56 (2008) 344–357. https://doi.org/10.1287/opre.1070.0441
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0
• A. Shapiro, A. Nemirovski, On complexity of stochastic programming problems, in Continuous Optimization, Springer (2005) 111–144. https://doi.org/10.1007/0-387-26771-9_4

Motivation

An investor who trades in a market with fewer stocks than sources of randomness cannot hedge every risk: the market is incomplete. If the investor also faces a liability $F$ due at the horizon $T$ and has to respect trading constraints (no short sales, limits on positions in certain stocks, a ban on trading some assets altogether), the question of how to trade optimally becomes a constrained stochastic control problem. With exponential utility $U(x)=-\exp(-\alpha x)$, its value function gives the investor's utility indifference price of $F$, a standard pricing rule in incomplete markets.

Earlier treatments needed convexity. Cvitanić and Karatzas (Ann. Appl. Probab. 2 (1992)) proved existence and uniqueness for utility maximization in a Brownian filtration with convex constraints, by convex duality. Delbaen, Grandits, Rheinländer, Samperi, Schweizer and Stricker (Math. Finance 12 (2002)) related exponential utility maximization to the martingale measure of minimal relative entropy. El Karoui and Rouge (Math. Finance 10 (2000)) computed the value function and optimal strategy for exponential utility by backward stochastic differential equations (BSDEs), for strategies confined to a convex cone; Sekine (preprint, 2002) obtained the same BSDE from the Cvitanić–Karatzas duality. Hu, Imkeller and Müller (Ann. Appl. Probab. 15 (2005)) gave a direct BSDE solution that works for closed, possibly nonconvex constraint sets, with a bounded liability. The tool is a BSDE whose driver grows quadratically in the control variable, whose solvability rests on Kobylanski's existence theorem for quadratic BSDEs (Ann. Probab. 28 (2000)).

Setting

Fix $T>0$ and an $m$-dimensional Brownian motion $W$ on a probability space $(\Omega,\mathcal F,P)$, and let $\mathbb F=(\mathcal F_t)$ be the $P$-augmentation of the filtration generated by $W$. There are $d\le m$ stocks with prices $dS^i_t/S^i_t=b^i_t\,dt+\sigma^i_t\,dW_t$; the drift $b$ and the $d\times m$ volatility matrix $\sigma$ are predictable and uniformly bounded, and $KI_d\ge\sigma\sigma^{\mathrm{tr}}\ge\varepsilon I_d$ for constants $K>\varepsilon>0$. The market price of risk is $\theta_t=\sigma^{\mathrm{tr}}_t(\sigma_t\sigma^{\mathrm{tr}}_t)^{-1}b_t\in\mathbb R^m$.

A strategy is an $\mathbb R^{1\times m}$-valued predictable process $p_t=\pi_t\sigma_t$, where $\pi_t$ is the vector of amounts held in the stocks. Its wealth from initial capital $x$ is

$$X^{(p)}_t=x+\int_0^tp_u\,(dW_u+\theta_u\,du).$$

The constraint is a closed set $\tilde C\subseteq\mathbb R^{1\times d}$, not necessarily convex; in terms of $p$ it reads $p_t\in C_t:=\tilde C\sigma_t$. A strategy is admissible, $p\in\mathcal A$, when $E\int_0^T|p_t|^2dt<\infty$, $p_t\in C_t$ for $\lambda\otimes P$-a.e. $(t,\omega)$, and $\{\exp(-\alpha X^{(p)}_\tau):\tau\le T\text{ a stopping time}\}$ is uniformly integrable. The value function is

$$V(x)=\sup_{p\in\mathcal A}E\Big[-\exp\Big(-\alpha\big(X^{(p)}_T-F\big)\Big)\Big],$$

with $\alpha>0$ and a bounded $\mathcal F_T$-measurable liability $F$. For a closed set $C$, $\operatorname{dist}_C(a)=\min_{b\in C}|a-b|$ and $\Pi_C(a)=\{b\in C:|a-b|=\operatorname{dist}_C(a)\}$ is the set of nearest points.

Formalization targets

Goal: Theorem 7

Let $f(t,z)=-\frac\alpha2\operatorname{dist}^2\big(z+\frac1\alpha\theta_t,C_t\big)+z\theta_t+\frac1{2\alpha}|\theta_t|^2$. The BSDE

$$Y_t=F-\int_t^TZ_s\,dW_s-\int_t^Tf(s,Z_s)\,ds,\qquad t\in[0,T],$$

has a unique solution $(Y,Z)\in\mathcal H^\infty(\mathbb R)\times\mathcal H^2(\mathbb R^m)$, the value function is

$$V(x)=-\exp\big(-\alpha(x-Y_0)\big),$$

and there is an optimal strategy $p^*\in\mathcal A$ with $p^*_t\in\Pi_{C_t}\big(Z_t+\frac1\alpha\theta_t\big)$.

Milestones

In the order of the proof: the bound (4) on $C_t$ and its closedness; the measurable selection Lemma 11 (a), (b); the identity on p. 8 that dictates $f$; the growth bound (9) and the local Lipschitz estimate of $f$; existence and uniqueness for (7); the BMO property of Lemma 12; admissibility and optimality of any predictable selection $p^*$; and the comparison $E[-\exp(-\alpha(X^{(p)}_T-F))]\le-\exp(-\alpha(x-Y_0))$ for every $p\in\mathcal A$.

Significance

The theorem reduces a constrained, nonconvex control problem to a single quadratic BSDE: the value is read off the initial value $Y_0$, and the optimal strategy is a pointwise nearest-point selection from the constraint set. It requires neither convexity nor duality, and it exhibits non-uniqueness of the optimal strategy when $\Pi_{C_t}$ has several points. It is the starting point of the quadratic-BSDE approach to utility maximization, indifference pricing and related equilibrium problems.

The result is proved in the paper; nothing in it is open. As far as is known, none of it is formalized: Mathlib has no stochastic integral against Brownian motion, no BSDE theory and no BMO martingales. A complete development would be the first machine-checked solution of a continuous-time portfolio optimization problem by BSDE methods, and its intermediate results (measurable selection of nearest points, the BMO bound for quadratic BSDEs, the verification argument) are reusable.

Difficulty

The deterministic steps (the identity behind the choice of $f$, the growth and Lipschitz bounds) are short. The hard steps are elsewhere. Existence rests on Kobylanski's theorem for BSDEs with quadratic growth, whose proof is a monotone approximation argument with exponential transforms; the Lipschitz theory of Pardoux–Peng does not apply. Uniqueness and the optimality of $p^*$ need the BMO property of $\int Z\,dW$ and a Girsanov change of measure with a stochastic exponential of a BMO martingale. The selection Lemma 11 (b) cannot use a projection map because $\tilde C$ is not convex; a measurable choice from a possibly multivalued nearest-point set is required. Finally the verification argument is a localization: $R^{(p)}$ is only a local supermartingale, and passing to the limit uses the uniform integrability built into admissibility.

Formalization scope

Time is $\mathbb R_{\ge0}$ with $T>0$; row vectors of $\mathbb R^{1\times m}$ are EuclideanSpace ℝ (Fin m) (so $|\cdot|$ is Euclidean) and products such as $z\theta$ are inner products. The Brownian motion is the published EthierKurtz.IsStandardBrownian; the filtration and the stochastic integral come from the published module CvitanicKaratzas92_Optimality_Market (IsAugmentedBrownianFiltration, lebP for $\lambda\otimes P$, and an Itô-integral operator I). Predictability is measurability for Mathlib's Filtration.predictable. The market price of risk $\theta$ and the wealth $X^{(p)}$ are computed from the data, not assumed.

Expectations of $-\exp(\cdot)$ are minus lower integrals in $[0,\infty]$, and $V(x)$ is an extended real: a Bochner expectation would assign the junk value $0$ to non-integrable strategies and make them optimal, which is the trivializing formalization to avoid. Existence and uniqueness of the BSDE solution are part of the goal, not hypotheses, and the optimal strategy is a predictable selection of the nearest-point set, not of a choice function.

Disclosed readings: $\tilde C\neq\emptyset$ is assumed (otherwise $\mathcal A=\emptyset$); constraints and (8) are read $\lambda\otimes P$-a.e.; ellipticity holds for $P$-a.e. $\omega$ and all $t\le T$; $Y_0$ is a.s. constant and the value identity holds a.s.; uniqueness is in $Y_t$ a.s. for each $t$ and $Z$ $\lambda\otimes P$-a.e.; "$p^*$ given by Lemma 11" is read as any predictable selection; Lemma 11 (b) assumes full rank of $\sigma_t(\omega)$. The equivalence of the $\pi$- and $p$-formulations (Remark 5), the dynamic principle (Proposition 9) and Remarks 2–10 are out of scope.

Needed infrastructure: Itô calculus for continuous semimartingales, stochastic exponentials, BMO martingales and Kazamaki's criterion, Girsanov's theorem, quadratic BSDEs, and measurable selection. Contributions to any of these are welcome; they serve the companion power-utility mission (Theorem 14) as well.

Selected references

• Y. Hu, P. Imkeller, M. Müller, Utility maximization in incomplete markets, Ann. Appl. Probab. 15(3), 1691–1712, 2005. https://doi.org/10.1214/105051605000000188 (arXiv: https://arxiv.org/abs/math/0508448)
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 558–602, 2000. https://doi.org/10.1214/aop/1019160253
• J. Cvitanić, I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4), 767–818, 1992. https://doi.org/10.1214/aoap/1177005576
• E. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14(1), 55–61, 1990. https://doi.org/10.1016/0167-6911(90)90082-6
• N. El Karoui, R. Rouge, Pricing via utility maximization and entropy, Math. Finance 10(2), 259–276, 2000. https://doi.org/10.1111/1467-9965.00093
• F. Delbaen, P. Grandits, T. Rheinländer, D. Samperi, M. Schweizer, C. Stricker, Exponential hedging and entropic penalties, Math. Finance 12(2), 99–123, 2002. https://doi.org/10.1111/1467-9965.02001
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585

Motivation

Risk measures quantify the danger of an uncertain cost $X$ by a single number. The axiomatic theory of coherent and convex risk measures (Artzner, Delbaen, Eber and Heath, Coherent measures of risk, 1999; Föllmer and Schied, Convex measures of risk and trading constraints, 2002) is static: the risk is evaluated once, with no information beyond what is known at time zero. Multistage stochastic optimization and dynamic risk management need risk evaluated conditionally: at time 1 part of the uncertainty has been resolved, and the risk of a time-2 cost should be a function of what is known at time 1.

Ruszczyński and Shapiro, in Conditional risk mappings (preprint of February 21, 2004; journal version Mathematics of Operations Research 31(3), 2006), extend their earlier static theory (Optimization of convex risk functions, Math. Oper. Res. 31(3), 2006) to this conditional setting. They define conditional risk mappings by three axioms, derive a pointwise conjugate duality, and show that positively homogeneous conditional risk mappings are, under regularity conditions, suprema of countably many conditional expectations. The last result explains the word conditional: the conditional expectation is the prototype, and every positively homogeneous conditional risk mapping is a worst case over a countable family of them.

Setting

Let $\Omega$ be a set with $\sigma$-algebras $\mathcal F_1\subset\mathcal F_2$; $\mathcal F_1$ is the information available when risk is evaluated. Let $\mathcal X_2$ be a real vector space of $\mathcal F_2$-measurable functions $X:\Omega\to\mathbb R$, and $\mathcal X_1\subset\mathcal X_2$ a subspace of $\mathcal F_1$-measurable ones. Let $\mathcal Y_2$ be a real vector space of finite signed measures on $(\Omega,\mathcal F_2)$ with $\int|X|\,d|\mu|<\infty$, and pair them by

$$\langle\mu,X\rangle=\int_\Omega X\,d\mu .$$

Both spaces carry locally convex topologies that are compatible with this pairing: the continuous linear functionals on each space are exactly the pairings with elements of the other. Two standing conditions hold throughout: (C) if $\mu\in\mathcal Y_2$ is not a nonnegative measure, some nonnegative $X\in\mathcal X_2$ has $\langle\mu,X\rangle<0$; (C′) $\mathbb 1_B\in\mathcal X_1$ for every $B\in\mathcal F_1$.

A conditional risk mapping is a map $\rho:\mathcal X_2\to\mathcal X_1$ with, writing $\rho_\omega(X)=[\rho(X)](\omega)$:

• (A1) convexity: $\rho_\omega(tX+(1-t)Y)\le t\rho_\omega(X)+(1-t)\rho_\omega(Y)$ for $t\in[0,1]$;
• (A2) monotonicity: $Y(\omega')\ge X(\omega')$ for all $\omega'$ implies $\rho_\omega(Y)\ge\rho_\omega(X)$;
• (A3) translation equivariance: $\rho(X+Y)=\rho(X)+Y$ for every $Y\in\mathcal X_1$.

Costs are minimised: smaller $X$ is better. All inequalities hold at every $\omega\in\Omega$, not almost surely. $\rho$ is positively homogeneous if $\rho(tX)=t\rho(X)$ for $t>0$, and lower semicontinuous if each $\rho_\omega$ is.

The conjugate is $\rho^*(\mu,\omega)=\sup_{X}\{\langle\mu,X\rangle-\rho_\omega(X)\}\in\overline{\mathbb R}$ and the risk envelope is $\mathcal A(\omega)=\{\mu:\rho^*(\mu,\omega)<\infty\}$. $\mathcal P_{\mathcal Y_2}$ denotes the probability measures in $\mathcal Y_2$, and $\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ those $\nu$ with $\nu(B)=\mathbb 1_B(\omega)$ for all $B\in\mathcal F_1$. A map $\omega\mapsto\mu_\omega$ is weakly* $\mathcal F_1$-measurable if every $\omega\mapsto\langle\mu_\omega,X\rangle$ is $\mathcal F_1$-measurable. For such a selection of $\mathcal A$, the operator $[\mathbb Q_\mu(\nu)](A)=\int\mu_\omega(A)\,d\nu(\omega)$ acts on $\mathcal Y_2$. Assumption (K): $\mathcal P_{\mathcal Y_2}$ is compact, and every such $\mathbb Q_\mu$ maps $\mathcal P_{\mathcal Y_2}$ into itself with a closed graph. Finally, $\mu(\cdot)$ is the conditional probability of $\nu$ given $\mathcal F_1$ if each $\omega\mapsto\mu_\omega(A)$ is $\mathcal F_1$-measurable and $\int_S\mu_\omega(A)\,d\nu=\nu(A\cap S)$ for $S\in\mathcal F_1$, $A\in\mathcal F_2$; then $\mathbb E_\nu[X|\mathcal F_1](\omega)=\langle\mu_\omega,X\rangle$.

Formalization targets

Goal: Theorem 2 (p. 11)

If $\mathcal X_2$ is separable, (K) holds and $\rho$ is a positively homogeneous, lower semicontinuous conditional risk mapping, then there are probability measures $\nu^i\in\mathcal P_{\mathcal Y_2}$, $i\in\mathbb N$, with

$$\rho_\omega(X)=\sup_{i\in\mathbb N}\mathbb E_{\nu^i}[X|\mathcal F_1](\omega)\qquad\text{for all }X\in\mathcal X_2,\ \omega\in\Omega,$$

each conditional expectation being the integral against a weakly* $\mathcal F_1$-measurable conditional probability of $\nu^i$.

Milestones

1. $\operatorname{dom}\rho^*(\cdot,\omega)\subseteq\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)$ (proof of Theorem 1, pp. 5–6).
2. Theorem 1 (p. 5): $\rho_\omega(X)=\sup_{\mu\in\mathcal P_{\mathcal Y_2|\mathcal F_1}(\omega)}\{\langle\mu,X\rangle-\rho^*(\mu,\omega)\}$, and its converse.
3. (3.8) (p. 6): for positively homogeneous $\rho$, $\rho^*(\cdot,\omega)$ is the indicator of a closed convex $\mathcal A(\omega)$ and $\rho_\omega(X)=\sup_{\mu\in\mathcal A(\omega)}\langle\mu,X\rangle$.
4. Lemma 1 (p. 11): for separable $\mathcal X_2$, countably many weakly* measurable selections of $\mathcal A$ suffice.
5. Under (K), each $\mathbb Q_\mu$ has a fixed point in $\mathcal P_{\mathcal Y_2}$ (p. 10).
6. Proposition 3 (p. 9): a fixed point $\bar\nu$ of $\mathbb Q_\mu$ has $\mu$ as its conditional probability given $\mathcal F_1$.

Corollary 1 (p. 10, singleton envelopes give a conditional expectation) and Proposition 2 (p. 7, $\rho(YX)=Y\rho(X)$ for nonnegative $\mathcal F_1$-step functions $Y$) are included as further statements.

Significance

Theorem 2 identifies the positively homogeneous conditional risk mappings with suprema of conditional expectations. It is the conditional analogue of the representation of a coherent risk measure as a worst-case expectation over a set of probability measures. It shows that the axioms (A1)–(A3), stated at every $\omega$, are the right abstraction of "conditional": nothing beyond conditional expectations and a supremum is needed to generate them. Theorem 1, the pointwise duality on which it rests, is what makes conditional risk mappings usable in multistage problems. Its envelope form (3.8) is what the paper's composition results and dynamic programming equations in §5–§7 manipulate.

The results are proved in the paper, partly by reference: the duality of Theorem 1 by applying the authors' earlier unconditional theorem "verbatim" at each $\omega$, Lemma 1 through a measurable-selection theorem, and Theorem 2 through Kakutani's fixed-point theorem. None of them is formalized. A formalization would check these deferred steps. In particular the passage, in the proof of Lemma 1, from a dense subset of $\mathcal X_2$ to all of $\mathcal X_2$ uses only lower semicontinuity of $\rho_\omega$, and whether that suffices in every separable paired space is open to scrutiny.

Difficulty

Theorem 1 needs the Fenchel–Moreau theorem in a general locally convex space, paired through integrals against signed measures. Mathlib's convex duality is mostly finite-dimensional or normed, and the extended-real bookkeeping of conjugates is delicate. The main obstacle is Lemma 1. The envelope $\mathcal A(\omega)$ can be uncountable, and choosing countably many selections that are simultaneously measurable in $\omega$ and exhaust the supremum for every $X$ requires a measurable-selection theorem for multifunctions with values in $\mathcal Y_2$, a space that need not be metrizable. The obvious argument fixes a dense sequence $X_n$, picks $\varepsilon$-optimal measures for each $X_n$, and passes to general $X$ by semicontinuity. As written, that last step appears to need more than the proof supplies: approximation of $\langle\mu,X\rangle$ by $\langle\mu,X_n\rangle$ uniformly over the chosen $\mu$ needs more than lower semicontinuity of $\rho_\omega$. The fixed-point step needs a Kakutani-type theorem in a locally convex space, which Mathlib does not provide.

Formalization scope

$\mathcal X_2$ and $\mathcal Y_2$ are abstract real vector spaces with their own topologies (instances of IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ), realised by injective linear maps into $\Omega\to\mathbb R$ and into Mathlib's SignedMeasure Ω. They are not subspaces of $\Omega\to\mathbb R$ with the pointwise topology. The ambient MeasurableSpace Ω is $\mathcal F_2$; $\mathcal F_1\le\mathcal F_2$ is a structure field. The pairing is $\int X\,d\mu^+-\int X\,d\mu^-$, and integrability against $|\mu|$ is a field, so no integral takes a junk value. Compatibility includes continuity of both pairings as well as the representation of continuous functionals. The paper's space $\mathcal Y_1$ is not modelled; no statement uses it.

Committed conventions:

• every statement holds at every $\omega$; there are no a.e. classes;
• the conjugate and the supremum in (3.6) are in EReal;
• suprema of real numbers ((3.8), (4.7), (4.9)) are least upper bounds (IsLUB), never sSup on $\mathbb R$;
• (K) is taken in its closed-graph form and quantifies over every weakly* measurable selection;
• separability is that of the topology of $\mathcal X_2$.

Two hypotheses are added where the page relies on them implicitly. $\Omega$ is nonempty in the goal, Corollary 1 and the fixed-point milestone. $\mathbb 1_A\in\mathcal X_2$ for every $A\in\mathcal F_2$ is assumed in the goal, Proposition 3 and Corollary 1, because the paper derives measurability of $\omega\mapsto\mu_\omega(A)$ from weak* measurability.

The goal cannot be satisfied by an almost-everywhere version of a conditional expectation chosen separately for each $X$, which would allow $\rho$ itself as a "version". Each $\mathbb E_{\nu^i}[\cdot|\mathcal F_1]$ is integration against one kernel $\kappa^i$ that is a conditional probability of $\nu^i$. The goal mentions no selection, fixed point or Kakutani; $\mathbb Q_\mu$ appears only inside (K).

Contributions are welcome on all of the following:

• Fenchel–Moreau duality for paired locally convex spaces;
• measurable selections of weakly* measurable multifunctions;
• a Kakutani–Fan–Glicksberg or Schauder–Tychonoff fixed-point theorem.

All three are reusable beyond this mission.

Selected references

• A. Ruszczyński, A. Shapiro, Conditional risk mappings, preprint dated February 21, 2004; Mathematics of Operations Research 31(3):544–561, 2006. https://doi.org/10.1287/moor.1060.0204
• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• P. Billingsley, Probability and Measure, 3rd ed., Wiley, 1995 (conditional probability, pp. 430–431).

Motivation

Stochastic models of covariance matrices need processes that stay in the cone of positive semidefinite matrices. Wishart processes (Bru, 1991) and their extensions underlie multivariate stochastic-volatility and term-structure models in finance (see §1 of Cuchiero et al. for the literature). They are used because their Laplace transforms are explicit: they are exponential-affine in the initial state, and their exponents solve matrix Riccati equations. Cuchiero, Filipović, Mayerhofer and Teichmann (arXiv:0910.0137, Ann. Appl. Probab. 2011) classify all such affine processes on the cone. Theorem 2.4 of that paper says that affine processes on $S_d^+$ correspond one-to-one to admissible parameter sets. This mission formalizes the converse direction of that correspondence: every admissible parameter set is realized by exactly one affine process.

Timeline:

• Bru (1991, MR1132135) constructs Wishart processes for specific parameters.
• Duffie, Filipović and Schachermayer (Ann. Appl. Probab. 2003, MR1994043) characterize affine processes on the canonical state space $\mathbb R_+^m\times\mathbb R^n$, with existence through the martingale problem.
• Cuchiero et al. (2011) give the full characterization on $S_d^+$. The necessity of admissibility and the existence-and-uniqueness converse are proved in separate sections (§4 and §5).

Setting

Let $S_d$ be the real symmetric $d\times d$ matrices with $\langle x,y\rangle=\operatorname{Tr}(xy)$, let $S_d^+$ be the positive semidefinite cone, and let $S_d^{++}$ be its interior. Write $x\preceq y$ when $y-x\in S_d^+$. A time-homogeneous, possibly killed Markov process on $S_d^+$ with transition kernels $p_t(x,d\xi)$ is affine if it is stochastically continuous and

$$\int_{S_d^+}e^{-\langle u,\xi\rangle}p_t(x,d\xi)=e^{-\varphi(t,u)-\langle\psi(t,u),x\rangle},\qquad t\ge0,\ u,x\in S_d^+,$$

for functions $\varphi\ge0$ and $\psi\in S_d^+$.

An admissible parameter set $(\alpha,b,\beta^{ij},c,\gamma,m,\mu)$ (Definition 2.3) consists of the following:

• a diffusion matrix $\alpha\in S_d^+$;
• a drift $b\succeq(d-1)\alpha$;
• killing rates $c\ge0$ and $\gamma\in S_d^+$;
• a jump measure $m$ with $\int(\|\xi\|\wedge1)\,m(d\xi)<\infty$;
• a matrix of finite measures $\mu$, which gives the state-dependent jump kernel $M(x,d\xi)=\langle x,\mu(d\xi)\rangle/(\|\xi\|^2\wedge1)$;
• linear drift coefficients $\beta^{ij}$, with the inward-pointing conditions (2.9) and (2.11) on $\partial S_d^+$.

These data define the operator (2.12),

$$\mathcal Af(x)=\tfrac12\sum A_{ijkl}(x)\partial^2_{ij,kl}f+\sum(b_{ij}+B_{ij}(x))\partial_{ij}f-(c+\langle\gamma,x\rangle)f+\int(f(x+\xi)-f(x))m(d\xi)+\int(f(x+\xi)-f(x)-\langle\chi(\xi),\nabla f\rangle)M(x,d\xi),$$

with $A_{ijkl}(x)=x_{ik}\alpha_{jl}+x_{il}\alpha_{jk}+x_{jk}\alpha_{il}+x_{jl}\alpha_{ik}$. They also define the functions $F(u)$ and $R(u)$ of (2.16)–(2.17), which drive the generalized Riccati equations $\partial_t\varphi=F(\psi)$, $\varphi(0,u)=0$ and $\partial_t\psi=R(\psi)$, $\psi(0,u)=u$.

Formalization targets

Goal: Theorem 2.4, second part (= Proposition 5.9)

For every admissible parameter set there is a transition family $(p_t)$ and there are exponents $(\varphi,\psi)$ such that:

$$\text{(i) } p \text{ is affine with exponents } (\varphi,\psi);\quad\text{(ii) } \mathcal S_+\subset D(\mathcal A_p),\ \mathcal A_pf=\text{(2.12)};\quad\text{(iii) } (\varphi,\psi) \text{ solves (2.14)–(2.15)};$$ $$\text{(iv) every affine } p' \text{ whose generator equals (2.12) on } \mathcal S_+ \text{ satisfies } p'_t=p_t \text{ for } t\ge0.$$

Milestones, in attack order

1. Theorem 4.8: a comparison theorem for matrix ODEs whose vector field is quasi-monotone increasing (Volkmann).
2. Lemma 5.1: $R$ is analytic on $S_d^{++}$ and quasi-monotone increasing on $S_d^+$.
3. Lemma 5.2: the growth bound $\langle u,R(u)\rangle\le\frac K2(\|u\|^2+1)$.
4. Proposition 5.3: unique global $\mathbb R_+\times S_d^{++}$-valued Riccati solutions, analytic in $(t,u)$.
5. Lemma 5.5: the regularized operators $\mathcal A^{\varepsilon,\delta,n}$ converge to $\mathcal A$ uniformly on $\mathcal S_+$.
6. Lemma 5.7 (second part): the boundary condition $\langle b-\frac12\sum D\sigma^{kl}\sigma^{kl},u\rangle\ge0$ on $\partial S_d^+$.
7. Lemma 5.6: the regularized martingale problems have $S_d^+$-valued càdlàg solutions.
8. Lemma 5.8: the martingale problem for $\mathcal A$ has an $S_d^+\cup\{\Delta\}$-valued càdlàg solution.

Significance

Together with the necessity direction (companion mission I in this series), the goal makes admissibility an exact characterization. Every admissible parameter set, including those with jumps of infinite activity and state-dependent killing, defines a well-posed Markov model on $S_d^+$. Its Laplace transform is then given by the Riccati flow, which is what makes the model computationally tractable. The intermediate results are reusable on their own:

• the matrix comparison theorem applies to any ODE on symmetric matrices;
• the Riccati well-posedness on $S_d^{++}$ holds for vector fields that need not be Lipschitz at $\partial S_d^+$;
• the martingale-problem framework on a one-point compactification is used beyond this paper.

The theorem is proved in the paper; it is not formalized anywhere. No formal library contains affine processes, generalized Riccati equations on matrix cones, quasi-monotone comparison theorems or martingale problems with jumps. Formalizing them requires all of that infrastructure.

Difficulty

The obvious route is to solve the Riccati equation (2.15) on $S_d^+$ by Picard iteration and to show invariance of the cone from the inward-pointing condition. That route fails because $R$ need not be Lipschitz at $\partial S_d^+$: the integral term can have unbounded derivative there (Remark 5.4). Standard invariance theorems therefore do not apply. Instead, quasi-monotonicity keeps the solution away from the boundary.

The obvious construction of the process is also blocked. Stroock's existence and uniqueness theory for martingale problems needs $\mathbb R^n$ and a uniformly elliptic diffusion part, and neither holds on the cone, where the diffusion degenerates at the boundary. Existence must go through regularized operators with bounded smooth coefficients, then tightness in the Skorokhod space of $S_d^+\cup\{\Delta\}$ and a limit. Uniqueness in law comes from the Riccati solutions. The killing terms $c$ and $\gamma$ are added last.

Formalization scope

Conventions committed to in Lean:

• $M_d$ is the function type Fin d → Fin d → ℝ, with $\langle x,y\rangle=\sum_{ij}x_{ij}y_{ji}$ and its norm.
• $S_d^+$ is the subtype of positive semidefinite matrices, with the subspace topology and Borel structure.
• Partial derivatives $\partial/\partial x_{ij}$ are taken in the symmetrized directions $\tfrac12(E^{ij}+E^{ji})$.
• The matrix measure $\mu$ is encoded as $H\,d\nu$ with a finite measure $\nu$ and a positive semidefinite density $H$. This encoding is equivalent; take $\nu=\sum_i\mu_{ii}$.
• The test space $\mathcal S_+$ is represented by Schwartz functions on $M_d$, restricted to the cone. The generator is the uniform limit of $(P_tf-f)/t$.
• Transition families are indexed by $t\in\mathbb R$, and only $t\ge0$ enters. Uniqueness is equality for $t\ge0$, never ∃!.
• Analyticity on $S_d^{++}$ is analyticity of $y\mapsto G((y+y^\top)/2)$ on an open subset of $M_d$.
• Martingale problems carry an existentially quantified probability space, the natural filtration and càdlàg paths (the platform predicate EthierKurtz.HasCadlagPaths).
• The cut-offs $\phi_n$ and $\eta_\varepsilon$ of §5.2 are arbitrary functions with the properties the paper lists. The paper fixes some and uses only those properties.
• The case condition of (5.7) is tested on $\phi_n(x)x$, the argument of $\eta_\varepsilon$, rather than on $x$ as printed. The printed reading makes $s_{\varepsilon,n}$ discontinuous off $S_d^+$, which contradicts the paper's claim $s_{\varepsilon,n}\in C_b^\infty(S_d,S_d)$. The two readings agree on $S_d^+$.
• In Theorem 4.8, "locally Lipschitz" is read as Lipschitz in the state variable, locally uniformly in time. This is weaker than joint local Lipschitz continuity in $(t,x)$.
• Every statement that contains one of the integrals of (2.12), (2.16), (2.17) or (5.10) also asserts that its integrand is integrable.
• Hypotheses not present on the page: none. Lemmas 5.1 and 5.2 assume less than the section's standing assumptions (not the drift condition (2.4)).

Trivializing formalizations are excluded:

• Lean's value $0$ for a non-integrable integral is ruled out by the integrability conclusions.
• A pointwise generator would be weaker than the paper's notion, so the generator is the uniform limit.
• An ∃! over transition families would be false at negative times, so uniqueness is stated for $t\ge0$.
• A martingale problem is not posed for a fixed probability space, and $X_0=x$ is required almost surely.

Needed infrastructure, reusable beyond this mission: matrix calculus on $S_d$ (square roots, spectral derivatives), comparison theorems for quasi-monotone ODEs, analytic dependence of ODE solutions, tightness in Skorokhod space, and martingale problems on locally compact spaces. Contributions are welcome at any of these levels, as are alternative proofs of the milestones.

Selected references

• C. Cuchiero, D. Filipović, E. Mayerhofer, J. Teichmann, Affine processes on positive semidefinite matrices, Ann. Appl. Probab. 21 (2011) 397–463; cited from arXiv:0910.0137v3. https://arxiv.org/abs/0910.0137v3
• D. Duffie, D. Filipović, W. Schachermayer, Affine processes and applications in finance, Ann. Appl. Probab. 13 (2003) 984–1053. https://mathscinet.ams.org/mathscinet-getitem?mr=1994043
• M.-F. Bru, Wishart processes, J. Theoret. Probab. 4 (1991) 725–751. https://mathscinet.ams.org/mathscinet-getitem?mr=1132135
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, New York, 1986. https://mathscinet.ams.org/mathscinet-getitem?mr=0838085
• P. Volkmann, Über die Invarianz konvexer Mengen und Differentialungleichungen in einem normierten Raume, Math. Ann. 203 (1973) 201–210. https://mathscinet.ams.org/mathscinet-getitem?mr=0322305

Motivation

The Lasso is the standard estimator for high-dimensional linear regression: from $n$ noisy linear measurements of an unknown vector $\beta^*\in\mathbb R^p$, with $p$ possibly much larger than $n$, it minimizes the empirical squared error plus an $\ell_1$ penalty. Its theoretical guarantees are usually stated as sparsity oracle inequalities: the prediction error of the Lasso is bounded by the best trade-off, over all candidate vectors $\beta$, between the approximation error of $\beta$ and a term proportional to the number of nonzero components of $\beta$.

Before this paper, such inequalities for the Lasso carried a leading constant strictly larger than $1$ in front of the approximation error. The inequalities of Bunea, Tsybakov and Wegkamp (EJS 2007) and of Bickel, Ritov and Tsybakov (Ann. Statist. 2009, Theorem 6.1) have this form, and the paper notes that sharpness "was not achieved in the previous work on the Lasso" (p. 24). A leading constant larger than $1$ means the bound is not informative when the true regression function is far from every sparse linear combination: the inequality then only says that the Lasso is within a constant factor of the best approximation.

Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study nuclear-norm penalized estimation of low-rank matrices in the trace regression model. Their general oracle inequality for a linear subspace of matrices (Theorem 2) has leading constant $1$. Restricted to diagonal matrices with a fixed design, the trace regression model becomes ordinary linear regression and the estimator becomes the Lasso. Section 5.4 of the paper draws the consequence: a sharp (leading constant $1$) sparsity oracle inequality for the Lasso with Gaussian noise, Theorem 14. This mission formalizes that theorem. The source is the arXiv preprint arXiv:1011.6256v4.

Setting

Fix integers $n\ge1$ and $p\ge2$ and fixed vectors $x_1,\dots,x_n\in\mathbb R^p$, the rows of the design matrix $\mathbb X=(x_1,\dots,x_n)^\top\in\mathbb R^{n\times p}$. The diagonal elements of the Gram matrix $\frac1n\mathbb X^\top\mathbb X$ are assumed not larger than $1$. The observations are

$$Y_i = x_i^\top\beta^*+\xi_i,\qquad i=1,\dots,n,$$

with $\xi_1,\dots,\xi_n$ independent $\mathcal N(0,\sigma^2)$ random variables, $\sigma>0$.

For $z\in\mathbb R^d$, $|z|_1=\sum_j|z(j)|$, $|z|_2=(\sum_jz(j)^2)^{1/2}$ and $|z|_\infty=\max_j|z(j)|$. For $J\subseteq\{1,\dots,p\}$, $u_J$ agrees with $u$ on $J$ and vanishes on $J^c$. The support of $\beta$ is $J(\beta)=\{j:\beta(j)\neq0\}$ and the sparsity $M(\beta)$ is its cardinality.

Given $\lambda>0$, a Lasso estimator is any minimizer

$$\hat\beta^\lambda\in\arg\min_{\beta\in\mathbb R^p}\Big\{\frac1n\sum_{i=1}^n(Y_i-x_i^\top\beta)^2+\lambda|\beta|_1\Big\}.$$

The restricted constant at $\beta$, with $J=J(\beta)$ and $c_0\ge0$, is

$$\mu_{c_0}(\beta)=\inf\Big\{\mu'>0:\ |u_J|_2\le\mu'\,n^{-1/2}|\mathbb Xu|_2\ \text{ for all } u\in\mathbb R^p \text{ with } |u_{J^c}|_1\le c_0|u_J|_1\Big\},$$

equal to $+\infty$ when the set is empty, and $\mu(\beta)=\mu_5(\beta)$. It is the inverse of a restricted eigenvalue computed at the single support $J(\beta)$; the paper obtains it from its matrix quantity $\mu_{c_0}(A)$ for $A=\operatorname{diag}\beta$. Finally $\mathbf M=\frac1n\sum_i\xi_ix_i$ is the noise vector.

Formalization targets

Goal: Theorem 14 (p. 25)

Let $\lambda=C\sigma\sqrt{\log p/n}$ with $C=3b\sqrt2$, $b\ge1$. With probability at least $1-\frac{1}{p^{b^2-1}\sqrt{\pi\log p}}$,

$$\frac1n|\mathbb X(\hat\beta^\lambda-\beta^*)|_2^2\le\inf_{\beta\in\mathbb R^p}\Big\{\frac1n|\mathbb X(\beta-\beta^*)|_2^2+C^2\sigma^2\frac{\mu^2(\beta)M(\beta)\log p}{n}\Big\}.$$

The event is uniform over all $\beta$, and the statement holds for every Lasso minimizer.

Milestones

1. The cone step ((2.20)–(2.22), p. 11, diagonal case): if $\lambda\ge3\|\mathbf M\|_\infty$ and $\langle\hat\beta-\beta^*,\hat\beta-\beta\rangle_{L_2(\Pi)}>0$, then $|(\hat\beta-\beta)_{J^c}|_1\le5|(\hat\beta-\beta)_J|_1$ for $J=J(\beta)$.
2. Theorem 2 for the Lasso (p. 11 with pp. 11–12, 24–26): deterministically, if $\lambda\ge3\|\mathbf M\|_\infty$,

$$\frac1n|\mathbb X(\hat\beta^\lambda-\beta^*)|_2^2\le\inf_{\beta}\Big[\frac1n|\mathbb X(\beta-\beta^*)|_2^2+\lambda^2\mu^2(\beta)M(\beta)\Big].$$

3. The Gaussian tail bound (proof of Theorem 14, p. 25): $P(|N|>z)\le\sqrt{2/\pi}\,e^{-z^2/2}/z$ for $N\sim\mathcal N(0,1)$, $z>0$.
4. The noise bound (proof of Theorem 14, p. 25): with probability at least $1-\frac{1}{p^{b^2-1}\sqrt{\pi\log p}}$, $\|\mathbf M\|_\infty\le b\sigma\sqrt{2\log p/n}$.

Significance

Theorem 14 gives an oracle inequality for the Lasso whose leading constant is exactly $1$. As a consequence (Corollary 4 of the paper), under the restricted eigenvalue condition RE$(s,5)$ of Bickel, Ritov and Tsybakov the Lasso's prediction error is at most the best $s$-sparse approximation error plus $C^2\sigma^2M(\beta)\log p/(n\kappa^2(s,5))$, which improves the non-sharp inequality of that paper. The bound also shows that the matrix-valued argument of the paper, written for nuclear-norm penalization, specializes cleanly to the vector case; the same argument underlies the matrix completion results of the other missions of this series.

The result is proved in the paper. As far as a search of the platform shows, no formal proof of a sharp oracle inequality for the Lasso exists; the platform has the non-sharp Bickel–Ritov–Tsybakov inequality as an open statement (LassoDantzig.Oracle.theorem_6_1). This mission produces a machine-checked version of the deterministic inequality, of the Gaussian concentration step, and of their combination, with the restricted constant defined exactly as in the paper.

Difficulty

The deterministic part is where the obvious argument fails. The usual Lasso analysis compares the objective at $\hat\beta$ and at a candidate $\beta$, controls the noise cross term, and rearranges; every version of that argument in the earlier literature loses a multiplicative factor in front of the approximation error $\frac1n|\mathbb X(\beta-\beta^*)|_2^2$, and the factor cannot be pushed to $1$ by tuning constants. The sharp bound has to come from a finer use of the optimality of $\hat\beta$, and the cone constant $5$ in $\mu(\beta)=\mu_5(\beta)$ is tied to the threshold $\lambda\ge3\|\mathbf M\|_\infty$. Formally, optimality conditions for a nonsmooth convex function on $\mathbb R^p$ (the subdifferential of $|\cdot|_1$) are infrastructure that has to be in place.

The probabilistic part needs the distribution of a linear combination of independent Gaussians, a Mills-ratio tail bound that is not in Mathlib, and a union bound over $p$ coordinates, with the exact constants of the paper.

Formalization scope

Vectors are functions Fin p → ℝ, and the design is given by its rows x i : Fin p → ℝ. All statements are in vector form, as the paper itself writes Section 5.4; no matrix library is needed. The Lasso is an argmin predicate, and statements hold for every minimizer; in the goal, $\hat\beta$ is a function of the outcome that is a minimizer at every outcome, and no measurability of $\hat\beta$ is assumed (the bad event is bounded in outer measure).

The restricted constant is formalized through its witnesses: the theorems hold for every $\mu'$ in the set whose infimum is $\mu(\beta)$. This is equivalent to the infimum, because the bounds are continuous and increasing in $\mu'$. A real-valued infimum would be $0$ on an empty set and would make the oracle inequality false, so it is deliberately not used. The infimum over $\beta$ is stated as "for every $\beta$", inside the event.

Hypotheses added relative to the page, each disclosed in the item's Formalization Note: $p\ge2$ (for $p=1$, $\log p=0$ and the printed probability divides by zero), $n\ge1$, $\sigma>0$, and measurability of the noise variables. $\lambda>0$ is the paper's standing assumption. The condition $\lambda\ge3\|\mathbf M\|_\infty$ is written coordinatewise. In the deterministic milestones the noise is a fixed vector and $\mathbf M=\frac1n\sum_i\xi_ix_i$, which is the paper's $\mathbf M$ for a fixed design and centred noise. No printed slip affects these statements. The constant $C=3b\sqrt2$ is kept as printed.

A trivializing formalization would assume the event $\|\mathbf M\|_\infty\le b\sigma\sqrt{2\log p/n}$ in the goal, or use a real infimum for $\mu(\beta)$; both are ruled out. Contributions of reusable infrastructure are welcome: the Gaussian tail bound, the law of a weighted sum of independent Gaussians, and the subdifferential of the $\ell_1$ norm.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4 (2016); Ann. Statist. 39(5), 2011. https://arxiv.org/abs/1011.6256
• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 2009. https://doi.org/10.1214/08-AOS620
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 2007. https://doi.org/10.1214/07-EJS008
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Statist. Soc. B 58(1), 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x