Why the average value-at-risk

Banks, insurers and planners who optimize under uncertainty need a single number that measures how bad the bad outcomes of an uncertain profit are. The value-at-risk, a quantile of the profit distribution, is the regulatory standard but ignores how far the worst outcomes fall below it and is not concave. The average value-at-risk (also called conditional value-at-risk, tail value-at-risk or expected shortfall) averages the worst $\alpha$-fraction of outcomes instead. It is concave, isotonic with respect to second-order stochastic dominance, and, through the minimization formula of Rockafellar and Uryasev (2000), it turns risk-averse stochastic programs into linear or convex programs. It is also the building block of most other version-independent risk functionals: distortion and Kusuoka representations write them as mixtures of average values-at-risk.

The axiomatic view goes back to Artzner, Delbaen, Eber and Heath (1999); the treatment of distributions with atoms, where several plausible definitions disagree, is due to Acerbi and Tasche (2002) and Rockafellar and Uryasev (2002). This mission follows Section 2.2.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), pp. 48–58, together with Proposition 2.74 on p. 109.

Setting

All outcomes are profit variables: larger values are better. Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $Y$ an integrable real random variable with distribution function $G(u)=\mathbb P\{Y\le u\}$ and left-continuous quantile function

$$G^{-1}(p)=\inf\{u : G(u)\ge p\},\qquad 0<p\le1 .$$

For $0<\alpha\le1$ the average value-at-risk is the lower-tail average

$$\mathbb{AV@R}_\alpha(Y)=\frac1\alpha\int_0^\alpha G^{-1}(u)\,du ,$$

so that $\mathbb{AV@R}_1(Y)=\mathbb EY$, and the average value-at-risk deviation is $\mathbb{AV@R}\mathbb D_\alpha(Y)=\mathbb EY-\mathbb{AV@R}_\alpha(Y)$. When $G$ jumps at $G^{-1}(\alpha)$, the two levels

$$\alpha^+_G=\inf\{G(u):G(u)\ge\alpha\},\qquad \alpha^-_G=\sup\{G(u):G(u)<\alpha\}$$

satisfy $\alpha^-_G\le\alpha\le\alpha^+_G$. Write $[y]^-=-\min(y,0)$ and $[y]^+=\max(y,0)$. Second-order stochastic dominance $Y^{(1)}\prec_{SSD}Y^{(2)}$ means $\mathbb E\,U(Y^{(1)})\le\mathbb E\,U(Y^{(2)})$ for every nondecreasing concave $U$ for which both expectations exist; $Y^{(1)}$, $Y^{(2)}$ are comonotone if $\mathbb P\{Y^{(1)}\le u, Y^{(2)}\le v\}=\min(G_1(u),G_2(v))$ for all $u,v$.

In the Lean development, in the namespace RiskFunctionals.AVaR, these objects are distributionFunction, quantileFunction (both of the law P.map Y), averageValueAtRisk P Y α, avarDeviation P Y α, alphaPlus, alphaMinus, SSD and Comonotone.

Formalization targets

Goal: Theorem 2.34

For integrable $Y$ and $0<\alpha\le1$:

1. $\displaystyle\mathbb{AV@R}_\alpha(Y)=\max\Big\{x-\frac1\alpha\mathbb E([Y-x]^-) : x\in\mathbb R\Big\}$, the maximum attained;
2. $\displaystyle\mathbb{AV@R}_\alpha(Y)=\min\Big\{\mathbb E(YZ) : \mathbb EZ=1,\ 0\le Z\le\frac1\alpha\Big\}$, the minimum attained;

and, if $G^{-1}(\alpha)$ is finite,

3. $\displaystyle\mathbb{AV@R}_\alpha(Y)=G^{-1}(\alpha)-\frac1\alpha\mathbb E([Y-G^{-1}(\alpha)]^-)=G^{-1}(\alpha)-\frac1\alpha\int_{-\infty}^{G^{-1}(\alpha)}(G^{-1}(\alpha)-u)\,dG(u)$;
4. $\displaystyle\mathbb{AV@R}_\alpha(Y)=\frac{\alpha^-_G}{\alpha}\mathbb E[Y\mid Y<G^{-1}(\alpha)]+\frac{\alpha-\alpha^-_G}{\alpha}G^{-1}(\alpha)$;
5. $\displaystyle\mathbb{AV@R}_\alpha(Y)=\frac{\alpha^+_G}{\alpha}\mathbb E[Y\mid Y\le G^{-1}(\alpha)]-\frac{\alpha^+_G-\alpha}{\alpha}G^{-1}(\alpha)$.

The goal is the conjunction of the five parts, stated as printed. $G^{-1}(\alpha)$ is finite for every $\alpha<1$, and for $\alpha=1$ exactly when $Y$ is essentially bounded above; parts 3–5 presuppose it. At $\alpha=1$ with $Y$ not essentially bounded above, the attainment claim of part 1 is false (see Beyond the paper), so the goal as printed is expected to be disprovable there.

Milestones

• p. 49 and (2.18): $\alpha^+_G=G(G^{-1}(\alpha))$, $\alpha^-_G=G(G^{-1}(\alpha)-)$, $\alpha^-_G\le\alpha\le\alpha^+_G$, $\mathbb P\{Y\le G^{-1}(\alpha)\}=\alpha^+_G$, $\mathbb P\{Y<G^{-1}(\alpha)\}=\alpha^-_G$.
• (2.24): $G^{-1}(\alpha)$ maximizes $x\mapsto x-\frac1\alpha\mathbb E([Y-x]^-)$.
• (2.17): $\mathbb EY=\alpha\,\mathbb{AV@R}_\alpha(Y)-(1-\alpha)\,\mathbb{AV@R}_{1-\alpha}(-Y)$ for $0<\alpha<1$.
• Proposition 2.35 (i)–(vii): translation equivariance, concavity, isotonicity with respect to $\prec_{SSD}$ and $\mathbb{AV@R}_\alpha(Y)\le\mathbb{AV@R}_\alpha(\mathbb E(Y\mid\mathcal F_1))$, positive homogeneity, $\mathbb{AV@R}\mathbb D_\alpha\ge0$, Lipschitz continuity on $L_1$, comonotone additivity.
• Proposition 2.36: $Y^{(1)}\prec_{SSD}Y^{(2)}$ iff $\mathbb{AV@R}_\alpha(Y^{(1)})\le\mathbb{AV@R}_\alpha(Y^{(2)})$ for all $0<\alpha\le1$.
• Proposition 2.37: for nonconstant integrable $Y$, $\alpha\mapsto\mathbb{AV@R}_\alpha(Y)$ is continuous and nondecreasing on $(0,1]$ and tends to $\operatorname{ess\,inf}Y$ as $\alpha\downarrow0$.
• Example 2.40 (newsboy problem): with purchase price $b$, selling price $s>b$ and refund $r<b$, the maximal expected profit is $(s-b)\,\mathbb{AV@R}_\alpha(Y)$ with $\alpha=\frac{s-b}{s-r}$, attained at the order size $G^{-1}(\alpha)$.
• Proposition 2.74: $\min_a\{\mathbb E([Y-a]^+)+\frac{1-\alpha}{\alpha}\mathbb E([Y-a]^-)\}=\mathbb{AV@R}\mathbb D_\alpha(Y)$, the minimum attained, for $0<\alpha\le1$ as printed.

Beyond the paper

A strengthened variant of Proposition 2.37 drops the hypothesis that $Y$ is nonconstant: for $Y\equiv c$ every average value-at-risk equals $c=\operatorname{ess\,inf}Y$, and the book's argument never uses the hypothesis.

Two corrected variants address the endpoint $\alpha=1$. For $Y$ integrable but not essentially bounded above (for instance exponential), $x-\mathbb E([Y-x]^-)=\mathbb E\min(Y,x)<\mathbb EY=\mathbb{AV@R}_1(Y)$ for every $x$, so the maximum in (2.19) is not attained; likewise $\mathbb E([Y-a]^+)>0=\mathbb{AV@R}\mathbb D_1(Y)$ for every $a$, so the minimum in (2.112) is not attained. The corrected Theorem 2.34 asserts part 1 only when $G^{-1}(\alpha)$ is finite, and the corrected Proposition 2.74 adds the same hypothesis; both leave everything else unchanged.

Significance

Theorem 2.34 is the toolkit through which the average value-at-risk is used. Representation 1 makes it the optimal value of a one-dimensional concave maximization, which is how it enters stochastic programs and the newsboy-type models of Examples 2.39–2.40. Representation 2 exhibits it as an infimum of linear functionals over an explicit dual set, which yields concavity, $L_1$-Lipschitz continuity and the link to the general dual representation of acceptability functionals. Representations 3–5 are the computational formulas for discrete distributions, where the naive "average of the outcomes below the quantile" is wrong. Proposition 2.36 shows that the family $(\mathbb{AV@R}_\alpha)_\alpha$ characterizes second-order dominance, and Proposition 2.74 identifies the deviation as a minimal-loss functional.

The results are classical and proved in the literature. What the mission adds is a machine-checked version in the book's conventions: profit variables, the lower tail, the left-continuous quantile, the dual set in $L_\infty$ with bound $1/\alpha$, and general distributions with atoms. The platform holds related results in other conventions: the Rockafellar–Uryasev minimization formula for loss functions and upper tails, an open loss-side dual representation on $L_\infty$, and expected-shortfall properties on finite state spaces; none states these representations for profit variables on a general probability space.

Difficulty

Everything happens where $G$ has an atom at $G^{-1}(\alpha)$. A proof that pretends $G$ is continuous, so that $\mathbb P\{Y\le G^{-1}(\alpha)\}=\alpha$, covers none of the cases the theorem was written for: the optimal dual variable must put a fractional weight on the event $\{Y=G^{-1}(\alpha)\}$, and representations 4 and 5 differ from each other precisely by the jump. Passing between integrals over $\Omega$, integrals against the law, and Lebesgue integrals of the quantile function over $(0,\alpha]$ needs the quantile transform for arbitrary distributions. The endpoint $\alpha=1$ is genuinely different: there $G^{-1}(1)$ may be infinite and the maximum in (2.19) and the minimum in (2.112) are then not attained: the book's statements fail there, and the corrected variants carry the finiteness condition.

Formalization scope

A random variable is a measurable, integrable $Y:\Omega\to\mathbb R$ on a probability space; $\mathbb{AV@R}_\alpha(Y)$ is computed from the law of $Y$ and so depends only on its distribution. The quantile function is real-valued; wherever it is evaluated at a point $\alpha$, the statement assumes $G(u)\ge\alpha$ for some $u$. Maxima and minima are stated as attained greatest and least elements of the value sets, never as bare suprema or infima. In the dual representation $Z$ ranges over measurable functions with $\int Z\,d\mathbb P=1$ and $0\le Z\le1/\alpha$ almost surely. Conditional expectations given an event are integrals against the conditional probability measure; when the event is null its coefficient $\alpha^\pm_G$ is $0$ as well. The limit at $\alpha\downarrow0$ is taken in the extended reals, since $\operatorname{ess\,inf}Y$ may be $-\infty$.

A trivializing formalization is ruled out: writing (2.19) or (2.20) with sSup/sInf and no attainment, or using an upper-tail, loss-side conditional value-at-risk in place of the book's lower-tail functional, would change or empty the statement; neither is done.

Contributions welcome: the quantile transform for general laws, the change of variables between $\Omega$, the law and $(0,1)$, and the Rockafellar–Uryasev argument are reusable across the rest of this series (Kusuoka and distortion representations, nested average value-at-risk).

Selected references

• G. Ch. Pflug, W. Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007. https://doi.org/10.1142/6478
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3), 2000. https://doi.org/10.21314/JOR.2000.038
• R. T. Rockafellar, S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7), 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
• C. Acerbi, D. Tasche, On the coherence of expected shortfall, Journal of Banking & Finance 26(7), 2002. https://doi.org/10.1016/S0378-4266(02)00283-2
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068

Motivation

Risk measures used in portfolio optimization, insurance pricing and regulation are almost always law invariant: they assign a number to a random profit $Y$ that depends only on its distribution, not on the scenario in which each outcome occurs. Kusuoka (Kusuoka 2001) showed that on a non-atomic space every law-invariant coherent risk measure is the worst case, over a family of weightings, of mixtures of one elementary functional, the average value-at-risk (also called conditional value-at-risk or expected shortfall). This reduces the design and the computation of law-invariant risk measures to the choice of a set of probability measures on the interval of confidence levels, and it underlies the use of the average value-at-risk as the building block of spectral and distortion risk measures.

This mission formalizes the version of Kusuoka's theorem proved in G. Ch. Pflug and W. Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, §2.2.4, Theorem 2.45), stated for acceptability functionals of profit variables on $L_p$, $1\le p<\infty$, together with the coupling and realization results its proof uses and a worked example from the same section.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space. It is non-atomic if no measurable set $A$ with $\mathbb P(A)>0$ has only subsets of probability $0$ or $\mathbb P(A)$. Fix $1\le p<\infty$ and the conjugate exponent $q$, $1/p+1/q=1$; $L_p$ is the space of real random variables with finite $p$-th moment (identified when equal almost surely) and $L_q$ its dual, paired by $\mathbb E(YZ)$.

For $Y$ with distribution function $G(u)=\mathbb P\{Y\le u\}$, the quantile function is $G^{-1}(p)=\inf\{u: G(u)\ge p\}$, $0<p\le1$, and the average value-at-risk at level $0<\alpha\le1$ is the lower-tail average

$$\mathbb{AV@R}_\alpha(Y)=\frac1\alpha\int_0^\alpha G^{-1}(u)\,du .$$

The book uses profit variables, so larger values are better and $\mathbb{AV@R}_\alpha$ averages the worst $\alpha$-fraction of outcomes; $\mathbb{AV@R}_1(Y)=\mathbb EY$.

A real valued $\mathcal A:L_p\to\mathbb R$ is an acceptability functional if it is translation equivariant, $\mathcal A(Y+c)=\mathcal A(Y)+c$ (A1), concave (A2), and monotone, $Y^{(1)}\le Y^{(2)}$ a.s. $\Rightarrow\mathcal A(Y^{(1)})\le\mathcal A(Y^{(2)})$ (A3). It is version-independent if $\mathcal A(Y^{(1)})=\mathcal A(Y^{(2)})$ whenever $Y^{(1)}$ and $Y^{(2)}$ have the same distribution. A dual representation is

$$\mathcal A(Y)=\inf\{\mathbb E(YZ)-A(Z): Z\in\mathcal Z_{\mathcal A}\},\qquad \mathcal Z_{\mathcal A}\subseteq L_q,$$

and $(A,\mathcal Z_{\mathcal A})$ is version-independent if equally distributed $Z,\tilde Z$ are both or neither in $\mathcal Z_{\mathcal A}$, with $A(Z)=A(\tilde Z)$. Theorem 2.45 adds the conditions (C1) $A=0$, (C2) every $Z\in\mathcal Z_{\mathcal A}$ is non-negative, (C3) every $Z\in\mathcal Z_{\mathcal A}$ has $\mathbb E Z=1$.

Formalization targets

Goal: Theorem 2.45(i)

Under (C1), (C2) and (C3) there is a family $\mathcal G$ of probability measures on $(0,1]$, fixed independently of $Y$, such that for every $Y\in L_p$

$$\mathcal A(Y)=\inf\Big\{\int_{(0,1]}\mathbb{AV@R}_\alpha(Y)\,dm(\alpha): m\in\mathcal G\Big\}. \tag{2.37}$$

Milestones

• Theorem A.2 (p. 266): on a non-atomic probability space every probability law on a complete separable metric space is the law of some random variable.
• Proposition 1.8 (p. 11): for given marginals, the covariance is maximal under the comonotone coupling and minimal under the antimonotone coupling.
• Eq. (2.38) (p. 61): under (C1), $\mathcal A(Y)=\inf\{\int_0^1F^{-1}(u)G^{-1}(1-u)\,du: G\in\mathcal G\}$, with $F$ the law of $Y$ and $\mathcal G$ the laws of the $Z\in\mathcal Z_{\mathcal A}$.
• Theorem 2.45(ii)–(iv) (p. 60): the representations with non-negative measures under (C1)+(C2), with two families of measures under (C1),

$$\mathcal A(Y)=\inf\Big\{\int\mathbb{AV@R}_\alpha(Y)\,dm^{(1)}_G(\alpha)-\int\mathbb{AV@R}_{1-\alpha}(-Y)\,dm^{(2)}_G(\alpha)\Big\},$$

and in general with an additional penalty $-\tilde A\{G\}$ and $\mathbb{AV@R}_\alpha(-Y)$ in the second integral.

• Example 2.46, Eq. (2.41) (p. 64): $\mathbb E(Y)-\tfrac12\mathbb E|Y-\mathbb EY|=\inf\{\int_{(0,1]}\mathbb{AV@R}_\alpha(Y)\,dm(\alpha): m\in\mathcal P(0,1],\ \int_{(0,1)}v^{-1}\,dm(v)\le1\}$.

Significance

The result. The Kusuoka representation says that the average values-at-risk are the extreme points of law-invariant acceptability: any such functional is determined by a set of mixing measures on the confidence levels. Consequences used in the rest of the book and in the literature include the identification of comonotone additive functionals with single mixtures (Choquet representations), explicit representations of mean–deviation functionals such as (2.41), and the reduction of optimization problems with law-invariant risk constraints to families of average value-at-risk constraints. The statement for $L_p$, rather than for bounded variables, is what makes it applicable to models with unbounded returns.

Formalizing it. The theorem is proved in the book and in the literature; it has not been machine-checked. Formalizing it requires infrastructure that is reusable beyond this mission: the quantile function and the average value-at-risk on $L_p$, the realization of a prescribed joint law on an arbitrary non-atomic probability space, and the Hardy–Littlewood-type rearrangement inequality behind the antimonotone coupling. Related platform results are in other conventions: a distortion functional of losses on $L_\infty$ as a single mixture of average values-at-risk (MultistageStochastic.distortion_avar_mixture, proved) and Schmeidler's comonotonic characterization on finite uniform spaces (RiskUncSets.Distortion.theorem_4_1, open). Neither covers the infimum over a family, profit variables, or $L_p$.

Difficulty

The obvious argument is to write each $Z\in\mathcal Z_{\mathcal A}$ as a mixing measure directly. This fails because $\mathbb E(YZ)$ depends on the joint law of $(Y,Z)$, not on the two marginals; the infimum must first be reduced to antimonotone couplings, which requires (a) that every coupling of the two marginals can be realized on the given space without leaving $\mathcal Z_{\mathcal A}$, using version-independence of both $\mathcal A$ and $(A,\mathcal Z_{\mathcal A})$ and non-atomicity, and (b) the extremal property of the antimonotone coupling for products of an $L_p$ and an $L_q$ variable, where quantile functions may be unbounded at both ends. The passage from $G^{-1}(1-u)$ to a mixing measure is a Stieltjes integration by parts on $(0,1)$ that must handle a point mass at $1$, and the integrability of $\alpha\mapsto\mathbb{AV@R}_\alpha(Y)$, which tends to the essential infimum of $Y$ (possibly $-\infty$) as $\alpha\to0$. Non-atomicity cannot be dropped: the book's Counterexample on p. 63 is a version-independent functional on a two-point space without representation (2.37).

Formalization scope

Probability spaces are (Ω, ℱ, P) with IsProbabilityMeasure P; non-atomicity is the book's notion (no atoms), which is stronger than Mathlib's NoAtoms. Random variables are elements of Lp ℝ p P with 1 ≤ p, p ≠ ⊤, and dual variables elements of Lp ℝ q P with p.HolderConjugate q. The quantile function is the left-continuous inverse of the book's (1.3), evaluated only on $(0,1)$ or inside integrals over $(0,\alpha]$; $\mathbb{AV@R}_\alpha$ is the lower-tail average (2.15), not the upper-tail loss CVaR. Version-independence is "equal laws give equal values" (IdentDistrib). Every infimum is stated as a greatest lower bound in $\mathbb R$ (IsGLB), which forces the indexing set to be nonempty and bounded below; measures on $(0,1]$ are measures on $\mathbb R$ with no mass outside $(0,1]$. The family $\mathcal G$ is quantified before $Y$: a family allowed to depend on $Y$ would reduce (2.37) to matching the single number $\mathcal A(Y)$ by some mixture, a much weaker statement, and that reading is excluded. Each representation also asserts that every integrand is integrable against every measure of the family, so that no integral can take Lean's default value $0$.

Beyond the paper. Two variant items accompany the goal. kusuoka_representation_strong ([Strengthened]) drops (C2) and (C3): for a real valued acceptability functional they follow from (A1), (A3) and the dual representation, since $\mathbb E(YZ)\ge\mathcal A(Y)$ for every $Y$ forces $\mathbb EZ=1$ (constants) and $Z\ge0$ (scaled indicators). kusuoka_representation_probe ([Sharpness probe]) drops non-atomicity; it is expected to be false by the p. 63 Counterexample, and a disproof is the sought outcome. The printed proof of Theorem 2.45(iii) has a sign gap (it derives $+\int\mathbb{AV@R}_{1-\alpha}(-Y)\,dm^{(2)}$); the statements (iii) and (iv) are kept as printed.

Contributions welcome: the quantile transform and realization of joint laws on non-atomic spaces, the rearrangement inequality on $L_p\times L_q$, and the integration-by-parts construction of the mixing measure, each of which can be submitted as a separate lemma.

Selected references

• G. Ch. Pflug, W. Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007, §2.2.4 and Appendix A. https://doi.org/10.1142/6478
• S. Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3, 83–95, 2001. https://doi.org/10.1007/978-4-431-67891-5_4
• W. Hoeffding, Masstabinvariante Korrelationstheorie, Schriften des Mathematischen Instituts der Universität Berlin 5, 179–233, 1940.
• S. T. Rachev, Probability Metrics and the Stability of Stochastic Models, Wiley, 1991 (Lemma 2.5.1, cited for Theorem A.2).

Scheduling shared service capacity

A switch or wireless network can have several queues ready for service while its hardware permits only certain combinations to be served together. A scheduler must choose a feasible combination repeatedly as new packets arrive. The question is whether this local sequence of decisions keeps the queue process stable whenever the arrival rates fit within the network's service capacity. Kelly and Yudovina formulate this question for finite service schedules and independent Poisson arrivals in §7.8 of Stochastic Networks.

MaxWeight scheduling gives larger queues greater influence over the choice of schedule. An exponent controls how strongly queue length affects priority. The chapter's target is a stability guarantee for every positive exponent, rather than a guarantee confined to the familiar linear weighting. The supplied Lecture Notes PDF states this as Theorem 7.13, printed page 180, and develops supporting analytic questions in Appendix D.

The queueing model

Let $R$ be a finite nonempty set of queues. A schedule is a vector $\sigma\in\mathbb N^R$ describing how many packets each queue can serve in one time slot. The feasible schedule family $S$ is finite and nonempty. It is downward closed: reducing any schedule coordinate leaves a feasible schedule. This includes the possibility of unused service when a selected queue has fewer packets than the schedule permits.

The admissible region is

$$\Lambda=\left\{v\in\mathbb R^R:v\ge0,\ \exists(c_\sigma)_{\sigma\in S},\ c_\sigma\ge0,\ \sum_{\sigma\in S}c_\sigma=1,\ v\le\sum_{\sigma\in S}c_\sigma\sigma\right\}.$$

It describes arrival rates dominated by an average of feasible schedules. The interior used here is the ordinary interior in $\mathbb R^R$.

Fix $\alpha>0$. At queue vector $q$, a schedule is drawn from a fixed probability distribution supported on the maximizers of $\sum_r\sigma_rq_r^\alpha$. New arrivals $A_r$ in the slot are independent Poisson variables of means $\lambda_r$, independent of the scheduling randomization and the past. The next queue vector is

$$q'_r=(q_r-\sigma_r)^++A_r.$$

These laws specify a homogeneous Markov chain on the countable state space $\mathbb N^R$. They follow the general model in §7.8 and the explicit empty-queue convention in Example D.4, printed page 213.

Formalization targets

The goal is Theorem 7.13: for $\lambda\in\operatorname{int}\Lambda$, the MaxWeight-$\alpha$ queue chain is positive recurrent. In return-time notation,

$$\forall q\in\mathbb N^R,\qquad \mathbb E_q[\tau_q^+]<\infty,\qquad \tau_q^+=\inf\{n\ge1:q(n)=q\}.$$

This retains every positive value of $\alpha$ and the full queue process.

Three supporting targets are selected from the same supplied source. Proposition D.1 states the Foster–Lyapunov criterion for an irreducible countable chain and an arbitrary finite exception set. A nonnegative function with drift at most $-\epsilon$ outside that set and at most $b-\epsilon$ inside it yields finite expected return to the set from every starting state and positive recurrence.

Exercise 7.18 concerns the weighted drift

$$D(q)=\sum_rq_r^\alpha\mathbb E[q'_r-q_r\mid q].$$

It asks for constants $\epsilon,K>0$ and finite $b$ such that

$$\|q\|_2>K\implies D(q)<-\epsilon\|q\|_2^\alpha,\qquad \|q\|_2\le K\implies D(q)<b.$$

Exercise D.1(3) asks for finite moments of $Y=\max(A,B)$, where $B$ is a finite service bound and $A$ is Poisson, and for the tail term

$$\mathbb E\!\left[\left(\left|(1+Y/K)^{\alpha+1}\right|+1\right)\mathbf1_{\{Y>\delta K\}}\right]$$

to tend to zero as $K\to\infty$ for fixed $\delta>0$. The source locations are printed pages 210–211, 182, and 214–215 respectively.

What the result establishes

The recurrence conclusion concerns repeated operation over an unlimited number of slots. It asserts a finite mean return time to each queue state under the specified policy. It does not require an explicit formula for the stationary distribution, nor does it prescribe a numerical delay guarantee. The result therefore identifies a capacity regime in which this queue-based scheduling rule is stable, while leaving performance within that regime as a separate question.

The formalization contribution is the connection between a concrete random scheduling transition law and recurrence on an infinite state space. Its reusable components include the capacity region of finite schedules, capped-service queue transitions, extended return expectations, and the Poisson envelope estimates. The textbook presents the theorem as an established result with a proof sketch. The theorem items here are statements awaiting proofs; compilation verifies their Lean syntax and types, not their mathematical proofs.

Where faithfulness requires care

Negative drift by itself is insufficient for the recurrence conclusion. The distinctions between negative drift, drift bounded away from zero, and control of upward increments matter in the chapter's discussion, printed pages 180–181. Arbitrary positive real exponents also require attention at empty queues and to unbounded Poisson arrivals.

The sketch's equality between actual departures and a chosen schedule fails when a positive queue is shorter than the proposed service. This is a proof gap, not a counterexample to the stability theorem. Appendix D additionally switches between conditioning on the full vector and conditioning on one coordinate in (D.5). Those conditional expectations need not agree for coupled schedules. The selected statements retain actual capped departures and avoid relying on that ambiguous display. Completing the analytic link to the goal remains part of the proof task.

Formalization scope

Queue and schedule coordinates are natural numbers, rates are nonnegative real numbers, and the exponent is an arbitrary positive real. The schedule family is a finite set of vectors. Random tie rules are stationary probability kernels supported on the maximizing schedules; the source specifies no particular distribution among ties. The norm in Exercise 7.18 is made Euclidean explicitly. Constants there are chosen before the queue vector is quantified, so they cannot depend on the current state or time.

Return times are represented by extended nonnegative sums of survival probabilities. Consequently, an event of never returning has infinite expected cost. Real drift sums have explicit absolute-integrability conditions. In the queue drift and Poisson moment items, integrability is a conclusion, not an assumed substitute for analysis. The Poisson tail term is an unconditional tail integral, including when its conditioning event would have probability zero.

No selected statement contains an unspecified $O(\cdot)$ term or a high-probability claim; there are therefore no numerical asymptotic constants to instantiate. Exercise D.1 is included only through its explicitly numbered part (3). The remaining parts, (D.5), congestion-control optimization results, and the switch-specific matching example are outside this mission's theorem list. No variants are posed.

Stability is not defined as negative drift, and the goal is not restricted to $\alpha=1$ or a finite truncation of the queue space. Mathlib supplies probability mass functions, product measures, Poisson laws, real powers, and topology. The local definitions supply the scheduling and recurrence interfaces needed to state the targets.

Selected references

• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. DOI: 10.1017/CBO9781139565363. Exact indices and quotations refer to the supplied Lecture Notes on Stochastic Networks PDF, SHA-256 ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a; correspondence with a particular published printing has not been verified.

Motivation

Stations sharing a communication channel must decide when to transmit. If nearby stations transmit together, their signals may interfere; if they all wait, capacity is wasted. A central scheduler can coordinate activity, but distributed access assigns decisions to individual stations. The mathematical question is whether simple random local decisions can supply all the service combinations that the interference constraints permit. This mission concerns the idealized continuous-time model in Section 5.4 of Kelly and Yudovina, Stochastic Networks, using the supplied Lecture Notes PDF.

The model isolates a capacity question from implementation issues. Stations sense active neighbors immediately, so collisions do not occur. Transmission durations and attempt clocks are exponential. The question concerns the equilibrium activity of this process for fixed parameters. Delayed sensing, packet queues, and parameter adaptation require additional results and are outside the theorem's claim.

Setting

An interference graph is a finite simple undirected graph whose vertices are stations. An edge means that its two endpoints cannot transmit together. Write $R$ for the station set and $S$ for the set of binary activity vectors $n=(n_r)_{r\in R}$ satisfying this restriction. The value $n_r=1$ means that station $r$ is transmitting. The all-zero vector is always feasible.

Each station has a finite real parameter $\theta_r$. An active station stops transmitting at rate $1$. An inactive station starts at rate $\exp(\theta_r)$ when all its neighbors are inactive. These transitions define a continuous-time Markov chain on $S$. Its generator is $Q$, with negative total outgoing rates on the diagonal, and its transition matrices are $P(t)=\exp(tQ)$ for $t\ge0$.

A distribution $p$ on feasible schedules offers mean activity $\sum_n p(n)n_r$ at station $r$. The capacity region includes every nonnegative arrival vector that some such distribution can dominate:

$$\Lambda=\left\{\lambda\ge0:\exists p\ge0,\quad\sum_{n\in S}p(n)=1,\quad \sum_{n\in S}p(n)n_r\ge\lambda_r\quad(r\in R)\right\}.$$

This definition permits arbitrary distributions on feasible schedules. The random-access process produces a much more specific family, indexed by one real number per station.

Formalization targets

Equation (5.8) identifies the stationary distribution of the specified chain:

$$\pi_\theta(n)=\frac{\exp(\sum_r n_r\theta_r)}{\sum_{m\in S}\exp(\sum_r m_r\theta_r)}, \qquad \pi_\theta P(t)=\pi_\theta\quad(t\ge0).$$

The goal is Theorem 5.17, printed page 126 of the supplied PDF. Every arrival vector in the ordinary interior of $\Lambda$ has strictly smaller coordinates than the equilibrium service vector for some finite parameters:

$$\lambda\in\operatorname{int}\Lambda \quad\Longrightarrow\quad \exists\theta\in\mathbb R^R,\quad \lambda_r<\sum_{n\in S}n_r\pi_\theta(n)\quad(r\in R).$$

Three Appendix C milestones supply the accompanying optimization statements. For a convex objective $f$ and componentwise convex constraint map $h$ on a convex set $X$, Theorem C.7 asserts convexity of the extended value function $\phi(b)=\inf\{f(x):x\in X,h(x)\le b\}$. Theorem C.3 supplies a nonvertical support at an interior point of its finite-value domain. Theorem C.4 states the equivalence between such support and the strong Lagrangian principle for equality constraints, with

$$L_b(x;y)=f(x)+y^T(b-h(x)),\qquad \phi(b)=\inf_{x\in X}L_b(x;y).$$

The faithful C.4 statement is retained without an unprinted finiteness hypothesis. Its infinite-value defect and the separately labelled correction are described below. The goal itself retains the source's strict service inequalities.

Significance

The capacity theorem says that the exponential random-access family does not leave a gap inside the region attainable by arbitrary mixtures of independent schedules. It provides a service margin in every coordinate at once. Its quantifiers allow the parameters to depend on the graph and arrival vector, but require every parameter to remain a finite real number. The theorem does not provide a uniform parameter bound as the arrival vector approaches the boundary.

The known mathematical result is attributed to Jiang and Walrand in the supplied source. The formalization target is a checked statement of that result and its supporting mathematical interfaces. The proposal's theorem declarations remain proof tasks. The finite exclusion process, its invariant law, and the distinction between feasible schedule mixtures and exponential-family marginals are reusable in later work on scheduling. The extended-value optimization layer can also support problems unrelated to communication networks.

Difficulty

Normalizing positive exponential weights only constructs a probability distribution. It does not establish that the distribution is invariant under the given dynamics, nor that its marginal vectors cover every strictly feasible demand. Changing one station's parameter changes the other stations' equilibrium opportunities through interference. Coordinatewise scalar tuning therefore does not settle simultaneous coverage.

The optimization statements require care at infeasible and unbounded problems. A real-valued infimum with a default value would conceal these cases. In particular, the literal C.4 equivalence fails for an empty domain: both primal and Lagrangian infima are $+\infty$, but no finite-height hyperplane touches that value. This is an issue with the unrestricted statement, not a new hypothesis for the capacity theorem.

Formalization scope

Stations are indexed by Fin d, and activity coordinates by Fin 2. Simple graphs enforce symmetry and exclude self-interference. A decidability instance is computational bookkeeping for a finite adjacency relation. The empty station set is permitted: it has one empty schedule, and the service conclusion has no coordinates. For one station the mean activity is $\exp(\theta)/(1+\exp(\theta))$. All normalizing sums are finite and strictly positive because the empty schedule contributes weight one.

Interior means ambient Euclidean interior. Arrival vectors in the closed region alone are insufficient: at the one-station boundary demand $\lambda=1$, no finite parameter supplies service greater than one. Finding F1 records this sharpness example; no extra sharpness item is posed.

The CTMC is represented by its finite generator and matrix-exponential transition semigroup. Its stationary-law theorem asserts invariance for every nonnegative time. Optimization infima use EReal, so infeasibility gives $+\infty$ and unboundedness below gives $-\infty$. Convexity is expressed through the real epigraph; supporting affine functions have real heights and slopes. Slack elimination in (C.2) preserves the inequality $h(x)\le b$. No asymptotic constants or failure probabilities require instantiation in these targets.

Beyond the paper. The single corrected variant of C.4 adds exactly that $\phi(b)$ is finite. Finding F2 gives the empty-domain counterexample to the unrestricted equivalence and the supporting argument for the correction. The original remains the milestone anchor. Findings F3 and F4 separately record the slack-multiplier sign error on printed page 209 and the word “maximized” in the minimization argument on printed page 127; neither changes the goal or creates a variant.

The definitions have concrete mathematical bodies without proof placeholders. The theorem types expose their defining formulas for independent auditing, and use Mathlib's finite sums, graph types, topology, convexity, extended reals, and matrix exponential. A formulation that assumes the desired service vector or proves only normalization would not capture this mission.

Selected references

• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. DOI. All numbered claims and page citations refer to the supplied Lecture Notes on Stochastic Networks PDF: Section 5.4, printed pages 125–128 (PDF pages 133–136), and Appendix C, printed pages 207–209 (PDF pages 215–217). Equivalence of this supplied file to a particular published printing is unverified.

Motivation

Food-borne outbreaks are traced slowly: when contaminated produce reaches shelves, the source is often unknown for weeks, and retailers recall everything. Traceability technology (for example blockchain ledgers) identifies the contaminated source at once, so only its units are discarded. Regulators and large retailers have pushed for it, and the intuitive view is that every member of the chain gains. Dong, Jiang & Xu (Management Science, 2022) show in a three-tier pricing game that this is not so: the chain's most powerful member, the retailer, can earn less in equilibrium with traceability than without it. The reversal happens for an explicit interval of retail prices, under an explicit condition on the primitives.

Setting

A retailer sells $n \ge 2$ units at an exogenous retail price $r$. She buys them at a wholesale price $w$ from one tier-1 supplier, who buys one unit at a procurement price $p$ from each of $n$ tier-2 suppliers (farms). Each farm produces at unit cost $c_p > 0$ and is contaminated independently with probability $\rho$, or $\rho_e$ if it exerts a risk-reduction effort at cost $e > 0$, where $0 \le \rho_e < \rho < 1$ and $\rho_\tau = \rho - \rho_e$. Assumption 1 of the paper is $c_p < \bar c_p = (1-\rho)e/\rho_\tau$. A farm's survival probability is $s = 1-\rho_e$ with effort and $1-\rho$ without.

• Case N (no traceability). Any contamination voids every payment. Farm $i$'s payoff under an effort profile $a$ is $\big(\prod_j s(a_j)\big)p - (e\mathbb 1\{a_i\} + c_p)$.
• Case T (traceability). Only contaminated units are lost. Farm $i$'s payoff is $s(a_i)p - (e\mathbb 1\{a_i\} + c_p)$.

Tier-1 earns (expected units sold)$\cdot(w-p)$ and the retailer (expected units sold)$\cdot(r-w)$; expected units sold are $n\prod_j s(a_j)$ in Case N and $\sum_j s(a_j)$ in Case T. The retailer chooses $w$, tier-1 then $p$, and the farms then choose effort simultaneously. The solution concept is subgame-perfect Nash equilibrium (SPNE) with the paper's selection rules: the Pareto-dominant tier-2 equilibrium is played; an indifferent farm exerts effort; an indifferent tier-1 or retailer induces effort; an agent with zero profit still trades.

The paper solves both games in closed form. With $\ell = (1-\rho_e)^n - (1-\rho)^n$, the effort thresholds of the retail price are

$$r^e_N = \max\Big\{\tfrac{(1-\rho_e)^{n+1}e-[2(1-\rho_e)^n-(1-\rho)^n]\rho_\tau c_p}{\rho_\tau\ell^2},\ \tfrac{e}{\rho_\tau(1-\rho_e)^{n-1}}\Big\},\qquad r^e_T = \tfrac{(1-\rho_e)^2e-(1+\rho-2\rho_e)\rho_\tau c_p}{\rho_\tau^3},$$

and the retailer's profit on the relevant branches (Tables EC.1–EC.2) is $\pi^e_{0N}(r) = n(1-\rho_e)^n(r - w^e_N)$, $\pi^o_{0T}(r) = n(1-\rho)r - nc_p$ and $\pi^e_{0T}(r) = n(1-\rho_e)(r - w^e_T)$, with $w^e_N = \max\{\frac{(1-\rho_e)e-\rho_\tau c_p}{\rho_\tau\ell}, \frac{e}{\rho_\tau(1-\rho_e)^{n-1}}\}$ and $w^e_T = \frac{(1-\rho_e)e-\rho_\tau c_p}{\rho_\tau^2}$. The paper's Definition 1:

DEFINITION 1 (BREAK POINT CRITERION). The Break Point Criterion (BPC) is satisfied if traceability adoption decreases the retailer's equilibrium profit when the retail price is at the effort threshold with traceability, i.e., $\pi^e_{0T}(r^e_T) < \pi^e_{0N}(r^e_T)$.

Formalization targets

Goal: Proposition 3 (p. 21)

Under the standing assumptions and BPC there exist $r_1, r_2$ with

$$r^e_N < r_1 < r^e_T < r_2,\qquad \pi^o_{0T}(r_1) = \pi^e_{0N}(r_1),\qquad \pi^e_{0T}(r_2) = \pi^e_{0N}(r_2),$$

such that both games have an SPNE at every retail price, and for all SPNE $s_N$, $s_T$ at $r$,

$$r_1 < r < r_2 \implies \Pi_T(r; s_T) < \Pi_N(r; s_N),\qquad r \notin (r_1, r_2) \implies \Pi_N(r; s_N) \le \Pi_T(r; s_T),$$

where $\Pi_N$, $\Pi_T$ are the retailer's equilibrium profits.

Milestones

In proof order: Lemma 1 (tier-2 equilibrium, Case N, p. 9); Lemma 2 (tier-1's optimal price, Case N, p. 10); Proposition 1 (SPNE, Case N, p. 11); Lemma 3, Lemma 4 (Case T, p. 13); Proposition 2 (SPNE, Case T, p. 14); Lemma 5 (BPC implies $r^e_N < r^e_T$ and $(1-\rho_e)^n > 1-\rho$, p. 21).

Stronger: the exact sign pattern

The variant proposition_3_strong adds strict increase with traceability on $(r^o_T, r_1) \cup (r_2, \infty)$, where $r^o_T = c_p/(1-\rho)$, and equality on $(-\infty, r^o_T] \cup \{r_1, r_2\}$.

Significance

Proposition 3 is the paper's headline result (Abstract, p. 1): removing the cascade threat does not make every member better off, and the losses concentrate on retail prices around the traceability effort threshold $r^e_T$. It underlies the paper's later welfare discussion (Observation 1, Proposition 4), where every member is worse off on part of the interval, and the policy point that adoption may need subsidies or contract adjustments.

The result is proved in the paper, partly in sketch form; none of it is formalized. A formal development produces the first fully specified multi-tier pricing-and-effort game on the platform: an $n$-player effort game with a selection rule, two nested best-response problems with tie rules, and subgame-perfect equilibrium as a predicate, together with a welfare comparison stated on equilibria rather than on formulas.

Difficulty

Each step is elementary, but the equilibrium has to be established, not assumed. The tier-2 stage is an $n$-player game in Case N whose equilibria above $p^e_N$ can be multiple (a stag hunt), so the selection rule matters. Tier-1 and the retailer optimize a margin whose effect on effort is a step function of the price; their maxima are attained only because the thresholds are closed and the tie rules settle the boundary, and they must be identified among all real prices. The final comparison is between two piecewise-linear functions with different breakpoints in the two cost branches. The paper prints no proof of Lemma 5, Lemma 4 or Proposition 2, and Proposition 3's printed proof is a short sketch that treats the high-cost branch as "similar".

Formalization scope

Everything lives in the namespace FoodTrace.Adoption (definition module Def_FoodTrace_Adoption_Model). Conventions:

• Parameters Params = (n, ρ, ρe, e, cp); Standing collects $n \ge 2$, $0 \le \rho_e$, $\rho_e < \rho$, $\rho < 1$, $e > 0$, $c_p > 0$ and Assumption 1. The implicit hypotheses $0 \le \rho_e$, $\rho < 1$, $e > 0$, $c_p > 0$ are made explicit.
• Effort is a Bool per farm; profiles are Fin n → Bool, with no symmetry built in.
• A viable tier-2 equilibrium follows (EC.9) of p. ec22: nonnegative payoffs; effort weakly preferred by farms exerting it; no effort strictly preferred by the others. The selected outcome weakly Pareto-dominates every viable equilibrium; "no sale" is selected exactly when none exists.
• "No trade" is none with profit 0; prices range over all of $\mathbb R$.
• Best responses and retailer optimality are maximizers over all prices and no trade, with the tie rules as explicit clauses (induce effort, then trade, whenever some maximizer does).
• Case T revenue for asymmetric profiles is $\sum_j s(a_j)$ times the margin; the paper prints only the symmetric case.
• $w^e_N$ and $r^e_N$ carry the max, so $\pi^e_{0N}$ is one formula in both cost branches. $\underline c_p$ is cpLow, $\bar c_p$ is cpBar.
• Proposition 3's "Otherwise, traceability adoption increases the retailer's profit" is stated as $\Pi_N \le \Pi_T$: the profits are equal at $r_1$, $r_2$ and for $r \le r^o_T$.

The retailer's profit in the goal is her payoff at an SPNE of the game, not the closed forms of Tables EC.1–EC.2; the goal asserts the existence of SPNE in both games at every retail price, so the comparison over all equilibria is not vacuous; and BPC is satisfiable (the Figure 4 instance $n = 2$, $\rho = 0.4$, $\rho_e = 0.1$, $c_p = e = 0.4$ gives $\pi^e_{0T}(r^e_T) = 36/5 < 198/25 = \pi^e_{0N}(r^e_T)$).

Beyond the paper. One variant is posed beside the faithful goal: proposition_3_strong (strengthened, finding F2), the exact sign pattern above. Evidence: a four-region comparison of the equilibrium profits, confirmed at 1.87 million sampled retail prices on 18,820 random BPC instances in both cost branches.

Needed infrastructure: finite products and sums over Fin n, real inequalities with powers, and case analysis on Option. The equilibrium layer (selection, best responses with tie rules, SPNE as a predicate) is reusable for other sequential supply-chain games. Proofs of the stage results (Lemmas 1–4, Propositions 1–2) and of Lemma 5 are welcome as independent contributions.

Selected references

• Y. Dong, B. Jiang, M. Xu, Impact of Traceability Technology Adoption in Food Supply Chain Networks, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4440 (accepted manuscript: SSRN 3484664, https://ssrn.com/abstract=3484664)

Decisions made with partial information

An adjustable decision is a rule that responds to information revealed after an optimization problem is specified. In production planning, for example, a later quantity may depend on observed demand, while an earlier commitment must remain constant. A robust counterpart requires the resulting decisions to satisfy the constraints for every realization in a prescribed uncertainty set. The information available to each decision is part of the model: observing one linear combination of uncertain data does not permit a policy to use all the data coordinates.

Quadratic rules provide a finite family of responses with more flexibility than affine rules. The resulting robust constraints still quantify over infinitely many uncertain realizations. This mission concerns the case in which that infinite family has an exact finite semidefinite representation: fixed recourse and ellipsoidal uncertainty, as stated in Corollary 14.3.8 of Ben-Tal, El Ghaoui and Nemirovski. The result is about optimization over the selected quadratic rules; it makes no claim that these rules attain the best value among all possible responses.

The model and the information available to a policy

Let $z\in\mathbb R^L$ denote the uncertain data and let

$$Z=\{z:\|Qz\|_2\le1\},\qquad Q\in\mathbb R^{r\times L},\quad\ker Q=\{0\}.$$

The uncertain linear problem has $n$ decision variables and $m$ constraint rows:

$$\min_x\{c(z)^Tx+d(z):A(z)x\ge b(z)\}.$$

All four data functions are affine in $z$. For variable $j$, a specified matrix $P_j\in\mathbb R^{k_j\times L}$ determines its observations. A quadratic decision rule has the form

$$X_j(z)=p_j+q_j^TP_jz+(P_jz)^TR_j(P_jz).$$

The optimization variables are the coefficients $p_j,q_j,R_j$ and an objective threshold $t$. The matrices $P_j$ are fixed data. The coefficient matrices $R_j$ are unrestricted: using full arrays retains every quadratic polynomial, with harmless redundancy in their skew-symmetric parts. If $P_j=0$, the policy is constant.

Fixed recourse means that whenever $P_j\ne0$, both $c_j(z)$ and column $A_j(z)$ are independent of $z$. Coefficients of nonadjustable variables may still be uncertain. This is Definition 14.3.1, printed p. 371, including the condition on the objective. Robust epigraph feasibility means that $A(z)X(z)\ge b(z)$ and $c(z)^TX(z)+d(z)\le t$ hold for every $z\in Z$.

Formalization targets

The supporting geometric target is Lemma 14.3.7, printed p. 384. The quadratic lift of $z$ is the symmetric matrix with top-left entry zero, first column $[0;z]$, and lower-right block $zz^T$. Its ordinary convex hull is compact and satisfies

$$\operatorname{conv}\left\{\begin{bmatrix}0&z^T\\z&zz^T\end{bmatrix}:z\in Z\right\} =\left\{\begin{bmatrix}0&v^T\\v&W\end{bmatrix}:\begin{bmatrix}1&v^T\\v&W\end{bmatrix}\succeq0,\ \operatorname{Tr}(QWQ^T)\le1\right\}.$$

The goal is Corollary 14.3.8. For every policy coefficient vector and threshold, robust epigraph feasibility is equivalent to feasibility of the explicit SDP after adding one nonnegative multiplier for each constraint row and one for the objective row. If the signed slack in row $i$ is written $\alpha_i+\beta_i^Tz+z^T\Gamma_i z$, its matrix constraint is

$$\begin{bmatrix}\alpha_i-\lambda_i&\beta_i^T/2\\\beta_i/2&\Gamma_i+\lambda_iQ^TQ\end{bmatrix}\succeq0,\qquad\lambda_i\ge0.$$

The model defines these coefficients directly from the original data and the observation matrices. The theorem also asserts that the matrices depend affinely on the SDP decision vector. There are $m+1$ matrix constraints of order $L+1$, and

$$N=1+\sum_j(1+k_j+k_j^2)+(m+1)$$

scalar decision variables. With $K=\sum_jk_j$, the bound $N\le1+n(1+K+K^2)+(m+1)$ and the corresponding dense matrix coefficient bound make the polynomial-size conclusion explicit.

What the exact representation provides

The equivalence retains every original policy coefficient and objective threshold. It therefore preserves the entire robust feasible epigraph, including instances with no feasible policy and optimization problems whose values are unbounded. The goal also states equality of attainable thresholds and preservation of minimizers for the same linear objective $t$ in the finite SDP. It does not assume that either problem has a minimizer. Equality of a pair of real-valued infima would express less information and could conceal degenerate cases.

The mathematical results are established in the textbook. This mission supplies open Lean theorem statements for their formal verification and concrete definitions for their objects. The homogeneous S-lemma and the inhomogeneous S-procedure are already Proved on Prove2Me and are retained as references. The moment-hull identity and the complete quadratic-policy representation are the new targets. Their definition layer can also support work on polynomial policies and other lifted uncertainty sets.

Difficulty

Checking a quadratic constraint on an ellipsoid is a global requirement. Evaluating it at a finite collection of sample points does not establish the required universal inequality. Likewise, the image of a convex uncertainty set under the quadratic lift is generally not convex. The target must identify its whole convex hull, including compactness and boundary points.

The formalization must also preserve information restrictions through every matrix coefficient. Full observation cannot replace $P_jz$, even if the resulting semidefinite program is easier to describe. The objective has uncertain affine data and participates in the same robust requirement as the constraints. These issues distinguish the complete statement from a single quadratic inequality or a result that assumes all coefficient columns are certain.

Formalization scope

All spaces and matrices are finite dimensional over the reals. The code uses finite functions for coordinates, but defines the uncertainty set through a sum of squares, so the norm is Euclidean. Matrix indices have a distinguished first coordinate. The unshifted lift has zero there; the positive-semidefinite moment block has one. Positive semidefiniteness also enforces symmetry of the moment matrix.

The model, uncertainty set, policy evaluation, original robust epigraph, and proposed SDP constraints are separate concrete definitions. Neither feasibility equivalence nor the moment-hull identity is assumed in the definitions. The theorem quantifies over every finite dimension, including zero; an empty observation list produces a constant policy. No division by a dimension or a policy-dependent denominator occurs.

The polynomial-size statement concerns the explicit real SDP representation, as in the book. It does not add a machine model or a bit-complexity theorem for an SDP solver. The formalization uses full quadratic coefficient arrays, so its stated counts need not be minimal. The bound includes all these redundant coefficients. There are no optional variants in this mission. The recorded sharpness observation about $Q$ explains why its injectivity is retained in the compactness theorem.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. DOI: 10.1515/9781400831050. Definition 14.3.1, printed p. 371; equation (14.3.6), printed p. 375; Lemma 14.3.7 and Corollary 14.3.8, printed pp. 384–385. The pinned PDF pages are respectively 397, 401, and 410–411.

Inventory decisions under uncertain demand

An inventory manager chooses replenishment orders before knowing all future demand. Orders made today affect both the stock available tomorrow and the cost of later decisions. A flexible commitment contract adds another consideration: deviations from previously announced orders can incur penalties. The uncertainty therefore concerns a sequence of observations, and the object being optimized is a sequence of decision rules. Chapter 15 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization uses this setting to compare the cost of unrestricted adaptive policies with the cost of affine policies.

For such a comparison, an exact benchmark matters. Evaluating a policy against every trajectory in a continuous uncertainty set can require infinitely many constraints. The chapter's Lemma 15.2.1 identifies a class of problems whose optimal value is preserved by restricting uncertainty to finitely many extreme scenarios. This mission formalizes that general lemma, which the book applies to inventory management, rather than the numerical experiments or a particular contract data set.

A multistage convex model

A history at stage $t$ is the tuple $d^{t-1}=(d_0,\ldots,d_{t-1})$, where each observation $d_j$ is a real vector of dimension $n_j$. A policy specifies a real decision vector $S_t(d^{t-1})$ of dimension $m_t$ for every possible history. Dependence only on observations already available is called nonanticipativity. Two full trajectories with identical observed prefixes necessarily produce the same decision at that stage.

There are $T+1$ decision stages and uncertainty sets $F_0,\ldots,F_T$. All data except the observations are fixed. Linear maps $A_t,B_{t+1},C_{t+1}$ and vectors $b_t$ impose the initial and linking inequalities

$$A_1S_1(d^0)\ge b_1,$$ $$A_{t+1}S_{t+1}(d^t)\ge B_{t+1}d^t+C_{t+1}S_t(d^{t-1})+b_{t+1},\qquad 1\le t\le T.$$

Vector inequalities hold coordinatewise. The term $B_{t+1}d^t$ uses the whole observed prefix. A fixed real bound $R$ restricts the infinity norm of each decision at stages $1,\ldots,T$. The terminal decision $S_{T+1}$ still appears in the last linking constraint, but the printed norm restriction does not cover it.

Each decision incurs a stage cost $f_t$. The costs are lower semicontinuous convex functions with polyhedral effective domains. A cost may be $+\infty$ outside its domain; within the domain it is finite. Polyhedrality of the domain does not require the cost itself to be piecewise linear. The total cost includes all $T+1$ stages.

Formalization target

Write $\operatorname{Opt}(F_0,\ldots,F_T)$ for the infimum of all real bounds $E$ for which some policy satisfies the preceding constraints and

$$\sum_{t=1}^{T+1}f_t(S_t(d^{t-1}))\le E \qquad\text{for every }d^T\in F_0\times\cdots\times F_T.$$

For nonempty polytopes $D_t\subset\mathbb R^{n_t}$, the target is the complete value equality in Lemma 15.2.1, printed p. 430:

$$\operatorname{Opt}(D_0,\ldots,D_T) =\operatorname{Opt}(\operatorname{Ext}D_0,\ldots,\operatorname{Ext}D_T).$$

Here $\operatorname{Ext}D$ denotes the set of extreme points of $D$. Both sides optimize over unrestricted nonanticipative policies. The target does not restrict those policies to affine rules, assert that every fixed policy has its worst cost at an extreme trajectory, or assert attainment of the optimum. The source states this lemma without a local numbered proof sequence, so the mission has one goal and its concrete model definitions, with no additional milestone chain.

What the result makes possible

For interval uncertainty, the extreme observations are interval endpoints. The book uses this consequence to replace a box of demand trajectories by a finite scenario set. It then describes a finite optimization problem whose decisions must agree whenever their available information agrees. These are exact comparisons of optimal values for the specified models, not estimates of sampling error. The number of scenarios can still grow exponentially with the horizon, as the chapter discusses on printed pp. 430–432 of the source.

The formalization makes the policy information pattern, terminal-stage treatment, and extended-value convention explicit. These details are useful beyond the inventory application because the lemma permits arbitrary compatible linear constraints and convex stage costs. The current artifacts state the known textbook result in Lean; a successful statement build is not a proof of the lemma. The reusable definitions are concrete and contain no unproved mathematical assertions.

Why the statement requires care

The uncertainty set is a product, but decisions at different stages are connected by constraints. A decision chosen for one trajectory cannot be chosen independently of another trajectory sharing the same history. Consequently, a statement about a single convex function on a polytope does not by itself express the multistage result. The target must retain the order of policy choice and universal quantification over trajectories, the complete cost sum, and the information available at each decision.

The final stage introduces a separate boundary issue: its cost and feasibility constraints remain present even though the printed bound stops one stage earlier. Omitting the final cost or extending the bound would change the problem. Degenerate and infeasible instances also require a value convention that does not assign them an arbitrary real number.

Formalization scope

Lean represents observations and decisions by finite real coordinate spaces, with dimensions allowed to vary by stage. Histories are finite dependent tuples; a policy's argument type contains exactly the observed prefix. Linear maps represent the book's matrices, including maps from stacked histories. Nonempty polytopes are convex hulls of nonempty finite sets, allowing singletons and lower-dimensional polytopes. The cost-domain predicate uses finitely many nonstrict matrix inequalities.

The extended optimal value is an EReal infimum of achievable real objective bounds. An empty set of bounds gives $+\infty$, while bounds unbounded below give $-\infty$. No subtraction of infinities occurs. Regular costs exclude $-\infty$, so the finite sum in the objective has no mixed-infinity ambiguity. The definition does not assume feasibility, boundedness below, or attainment. Zero horizon and zero-dimensional coordinate spaces follow the same displayed formulas.

Formalization Note No singleton assumption is placed on $D_0$, and no measurability, continuity, or affine restriction is imposed on policies. The theorem expands its concrete model for independent auditing. A Lean type check verifies agreement with the separately named reusable definitions. The required mathematical infrastructure includes convex hulls, extreme points, lower semicontinuity, finite linear algebra, and extended-real order. Completion requires a proof of the stated value equality with precisely these hypotheses.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009, Chapter 15, §15.2.4.1, Lemma 15.2.1, printed p. 430 (PDF p. 456). DOI: 10.1515/9781400831050.

Robust fitting with uncertain measurements

Regression and classification fit a parameter vector to observed data. When measurements can vary within a prescribed set, a fit judged only at the nominal observations need not control its loss on the possible data. A worst-case loss constraint requires the loss bound to hold for every admissible matrix of measurements. Such a requirement can contain infinitely many inequalities even when the parameter vector has finitely many coordinates. Chapter 12 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (2009) identifies structural assumptions under which this requirement has an exact finite convex representation.

This mission concerns the representation in Theorem 12.2.5. Its application is to robust fitting problems whose uncertainty support function separates into a feature-dependent factor and the infinity norm of a residual-space vector. The result applies to both symmetric losses, such as norms of regression residuals, and asymmetric losses formed from positive residual parts.

Data, residuals, and loss

Let $n,\ell,m$ be positive integers. The nominal data matrix $Z^n\in\mathbb R^{n\times m}$ has one column per measurement and one row per feature. For a parameter vector $\theta\in\mathbb R^n$, its residual vector is $r=(Z^n)^T\theta\in\mathbb R^m$. A fixed matrix $U\in\mathbb R^{n\times\ell}$ describes the structure of permitted perturbations, and a nonnegative scalar $\rho$ controls their size. The uncertain data matrices are

$$\mathcal Z=\{Z^n+\rho U\Delta:\Delta\in D\},$$

where $D\subset\mathbb R^{\ell\times m}$ is convex, compact, and contains zero. No independence of its columns is imposed.

The loss function $L:\mathbb R^m\to\mathbb R$ is finite and convex. Assumption L requires one of two forms: $L(r)=\pi(|r|)$ for every $r$, or $L(r)=\pi(r_+)$ for every $r$. Absolute value and positive part act coordinatewise. The function $\pi$ is convex and nondecreasing in every coordinate on the nonnegative orthant. The choice of form is global, rather than chosen separately at each residual.

Assumption A specifies the support of $D$ in every rank-one direction:

$$\max_{\Delta\in D}u^T\Delta v=\phi(u)\psi(v).$$

Here $\phi$ is finite, nonnegative, convex, and positively homogeneous, and $\psi$ is a norm. The goal uses $\psi(v)=\|v\|_\infty$. These are the standing objects and assumptions of Section 12.2, printed pages 311–319 of the source.

Formalization targets

For any real threshold $\tau$, the goal is the exact equivalence

$$\forall Z\in\mathcal Z:\ L(Z^T\theta)\le\tau$$

if and only if there exists a real $\kappa$ satisfying

$$\rho\phi(U^T\theta)\le\kappa,\qquad L((Z^n)^T\theta+\kappa e_i)\le\tau,\qquad L((Z^n)^T\theta-\kappa e_i)\le\tau\quad(1\le i\le m).$$

The goal also states convexity in $(\theta,\kappa)$ of the scalar functions on the left of these constraints. There are $2m$ shifted-loss inequalities and one amplitude inequality.

The numbered supporting targets preserve the source's identities. Equation 12.2.11 gives the Fenchel biconjugate representation of a finite convex loss. Equation 12.2.12 equates the worst-case realized loss with its conjugate expression involving the support of $D$. Equation 12.2.15 replaces that support by its factorization under Assumption A. Equation 12.2.18 equates the resulting worst-case loss with a maximum over the dual unit ball:

$$L_{\rm wc}(r,\kappa)=\max_{\psi^*(\xi)\le1}L(r+\kappa\xi),\qquad \kappa\ge0.$$

The maxima in these identities are required to be attained. The Fenchel representation itself uses the source's supremum notation.

What the representation provides

Theorem 12.2.5 replaces a constraint over a continuum of data matrices with finitely many evaluations of the original loss and the uncertainty gauge. It retains the dependence of uncertainty on the fitted parameter through $\phi(U^T\theta)$. Consequently, the representation describes exactly the robust feasible parameters, including zero uncertainty, rather than merely giving a sufficient condition. Evaluation efficiency remains relative to the supplied loss and gauge, as in the book's tractability discussion.

The mathematical result is established in the textbook. The contribution sought here is a machine-checked formalization of its statement and supporting identities. The general finite-dimensional Fenchel biconjugacy theorem already has a proved platform item and is reused as the first milestone; the other three identities and the capstone are open theorem statements in this draft.

Mathematical difficulty

The central issue is relating uncertainty in a matrix to uncertainty in the residual vector while preserving exactness. A uniform bound on individual matrix entries does not by itself express Assumption A. Conjugate functions also need extended values: replacing an infinite conjugate by a real default would change the optimization problem. Establishing equality of optimal values alone is insufficient for identities written with maxima; their attainment is part of the targets. The zero-amplitude case must agree with the nominal loss throughout.

Formalization scope

Vectors use finite-dimensional real Euclidean spaces and matrices have explicitly ordered feature and measurement indices. Coordinates use Fin m, so the first coordinate is indexed by zero. The infinity norm in the goal is taken on the plain coordinate function; it is not the Euclidean norm of the residual vector. The statements include both signs for every coordinate.

The published fenchelConjugate and fenchelBiconjugate definitions are reused. Conjugate objectives take values in EReal. Every claimed maximum is expressed using IsGreatest at a common finite real value, so existence, boundedness, equality, and attainment remain visible. The inner support supremum in Equation 12.2.12 is real-valued and ranges over a nonempty compact image. The dual unit ball in Equation 12.2.18 is represented directly by $\xi^Tv\le\psi(v)$ for all $v$.

All hypotheses about the loss, gauge, norm, and uncertainty set are explicit in each new theorem. None assumes the desired finite reformulation. Assumption L is retained despite the recorded observation that a weaker loss hypothesis suffices for the mathematical equivalence. There are no variant targets. A computational cost model and an optimization algorithm are outside this formalization; the explicit finite formulas and their convexity are the representation being formalized. Reusable work includes finite-dimensional conjugacy, compact support maximization, and dual-norm geometry.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. DOI: 10.1515/9781400831050. Section 12.2, printed pp. 311–319; Equations 12.2.11, 12.2.12, 12.2.15, 12.2.18 and Theorem 12.2.5.

Motivation: reliability under random data

A linear constraint can fail when its coefficients vary. In an engineering or planning model, requiring it to hold for every imaginable realization may exclude useful decisions, while checking it only at an average realization may give little control over failure. A chance constraint specifies an acceptable probability of violation. Chapter 2 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization studies deterministic convex conditions that guarantee this probabilistic requirement for a single uncertain linear inequality.

The chapter distinguishes a guarantee from an exact description of chance feasibility. Its robust constraints are safe approximations: satisfying them guarantees reliability, but a reliable decision need not satisfy them. The goal here concerns how known bounds on the perturbations can be incorporated into such an approximation without losing an explicit convex representation.

Setting: an uncertain scalar inequality

A decision is a vector $x\in\mathbb R^n$. The deterministic data are vectors $a^0,a^1,\ldots,a^L$ and scalars $b^0,b^1,\ldots,b^L$. Define the residual coordinates by $z_i(x)=(a^i)^Tx-b^i$, including the nominal coordinate $i=0$. A realized perturbation $\zeta\in\mathbb R^L$ satisfies the constraint exactly when

$$z_0(x)+\sum_{i=1}^L\zeta_i z_i(x)\le0.$$

For a probability law $P$ and a tolerance $0<\varepsilon<1$, chance feasibility means that the strict reverse inequality has probability at most $\varepsilon$. Robust feasibility over a deterministic set $Z$ means that the displayed inequality holds for every $\eta\in Z$.

The perturbation coordinates are independent measurable real random variables. Their moment-generating functions obey the two-sided bound

$$\mathbb E_P e^{t\zeta_i}\le\exp\left(\max\{\mu_i^-t,\mu_i^+t\}+\frac12\sigma_i^2t^2\right)\qquad(t\in\mathbb R),$$

where $\mu_i^-\le\mu_i^+$ and $\sigma_i\ge0$. These are the book's assumptions P.1–2. The goal additionally assumes almost-sure support bounds $a_i^-\le\zeta_i\le a_i^+$, with finite endpoints satisfying $a_i^-\le\mu_i^-\le\mu_i^+\le a_i^+$. No positive lower bound on $\sigma_i$ is imposed.

Formalization targets

Write $B(y)=\sum_i\max\{\mu_i^-y_i,\mu_i^+y_i\}$, $D(y)=\sqrt{\sum_i\sigma_i^2y_i^2}$, and $r_\varepsilon=\sqrt{2\log(1/\varepsilon)}$. The general safety statement, Proposition 2.4.1, asserts that

$$z_0+B(z)+r_\varepsilon D(z)\le0\quad\Longrightarrow\quad P\{z_0+\sum_i z_i\zeta_i>0\}\le\varepsilon.$$

Its feasible set is convex. Proposition 2.4.2 states the tail bound at every nonnegative safety level $r$:

$$P\{\sum_i z_i\zeta_i>B(z)+rD(z)\}\le e^{-r^2/2}.$$

Theorem 2.4.3 identifies the first deterministic inequality with robust feasibility over the moment uncertainty set

$$Z_{\rm mom}=\{\eta:\exists w,\ \mu_i^-\le\eta_i-\sigma_iw_i\le\mu_i^+\ (1\le i\le L),\ \sqrt{\sum_iw_i^2}\le r_\varepsilon\}.$$

The capstone is Theorem 2.4.4. Let $Z$ be the intersection of $Z_{\rm mom}$ with the support box $[a^-,a^+]$. Then $x$ is robust feasible over $Z$ if and only if there exist extended residual vectors $u,v\in\mathbb R^{L+1}$ satisfying

$$z_i(x)=u_i+v_i\quad(0\le i\le L),$$ $$u_0+\sum_i\max\{a_i^-u_i,a_i^+u_i\}\le0,\qquad v_0+B(v)+r_\varepsilon D(v)\le0.$$

This system is convex in its decision and auxiliary variables. Every feasible triple has violation probability at most $\varepsilon$. The theorem includes both the deterministic equivalence and the probabilistic guarantee, as on printed page 48.

Two supporting targets retain the chapter's bounded mean-zero specialization. Proposition 2.3.1 gives the tail estimate $P\{\sum_i z_i\zeta_i>r\sqrt{\sum_i z_i^2}\}\le e^{-r^2/2}$ for independent mean-zero perturbations in $[-1,1]$. Proposition 2.3.3 identifies robustness over the intersection of the unit box and a Euclidean ball with its lifted conic system and establishes the corresponding chance guarantee. These are supporting statements from the source, not replacements for the general capstone.

Significance: explicit conditions with a probability guarantee

The capstone connects a deterministic set of allowed perturbations with a stochastic model specified through moment bounds and support information. It gives a finite convex system whose feasible decisions satisfy the requested reliability level for every law meeting those assumptions. The statement does not require choosing a particular parametric distribution or estimating a probability separately for every decision.

These are known textbook results. The formalization targets are their Lean statements and eventual machine-checked proofs, including zero scales and boundary feasibility. The reusable content comprises finite-dimensional uncertainty sets, explicit exponential-moment hypotheses, and the relationship between lifted convex constraints and strict-event probabilities. The present authoring pass leaves the six theorem proofs open; compilation checks their types, not their truth.

Difficulty: boundary cases carry mathematical content

The exact robust representation includes equality cases in the endpoint order and permits degenerate ellipsoids. A formulation restricted to positive scales or strict interior intersections would omit cases of the stated theorem. The chance guarantee must also include the boundary of the explicit safe set; it cannot be replaced by a condition requiring an additional strict margin.

The printed proofs have local discrepancies recorded in the mission findings: the proof of Proposition 2.4.2 omits a sum and invokes an open-interval risk bound at its excluded endpoint when the safety level is zero, the first line of the goal's proof uses a different radius, and the limiting argument on page 50 asserts a zero limit that fails for strictly feasible residuals. These findings concern the proofs, not counterexamples to the theorem statements. The goal retains the printed constants and hypotheses.

Formalization scope

The namespace is RobustOpt2009.ScalarChance. Vectors use real-valued functions on Fin L; the nominal coordinate is a separate real component. All Euclidean lengths are explicit square roots of sums of squares, avoiding the default function-space sup norm. Probability is evaluated under a probability measure, and all random coordinates are measurable. The exponential-moment definition includes integrability, preventing nonintegrable Bochner integrals from supplying default zero values.

Scaled coordinates $\sigma_iw_i$ implement the book's zero-denominator convention: a zero scale forces zero displacement. Robust feasibility is a universal inequality, so no empty or unbounded real supremum is used. The exponential-certificate set, its topological closure, and the perturbation uncertainty set remain separate concrete objects. No definition assumes the desired equivalence or tail bound. Finite sums include the zero-dimensional case, where the statements reduce to their deterministic or empty-event versions.

Further work consists of proving the stated concentration, convexity, and exact representation claims using these definitions and Mathlib's probability and finite-dimensional analysis. No variants are posed in this chapter.

Selected references

• Aharon Ben-Tal, Laurent El Ghaoui and Arkadi Nemirovski, Robust Optimization, Princeton University Press, 2009, Chapter 2, especially printed pp. 29–33 and 45–50. DOI: 10.1515/9781400831050. Published citation basis; PDF pages are printed pages plus 26.