All missions

Motivation

A scheduler in a computing system may know how to allocate a fixed collection of jobs efficiently while having no reliable forecast of future arrivals. A guarantee for jobs available at the outset does not immediately answer whether decisions remain effective when new work appears during execution. Unknown release dates capture this distinction: a job becomes available and visible only at its release time. Shmoys, Wein and Williamson separate this information restriction from uncertainty about processing requirements and give a general conversion between the two arrival models. The present target is their Theorem 2.1, rather than the independent unknown-size conversion later in the paper. Source, §2.

The question concerns both efficient computation and execution on physical resources. A short schedule selected with knowledge of future jobs is not an online algorithm. Conversely, an online rule can make legitimate decisions yet produce schedules much longer than the best off-line schedule. The target retains both requirements and asks how much a scheduler's makespan guarantee deteriorates when advance knowledge of arrivals is removed.

Setting

A job is a finite processing task using some of a fixed finite collection of exclusive resources. An instance has a finite set $J$ of job identities, job data $d_j$, and real release dates $r_j\ge0$. Jobs cannot receive processing before release. Each execution specifies resource allocations over time and must satisfy the job's processing rules. Two jobs cannot occupy the same resource simultaneously. The completion time $C_j$ is the time at which job $j$ has finished, and the makespan is

$$C_{\max}=\max(\{0\}\cup\{C_j:j\in J\}).$$

The empty instance therefore has makespan zero. The off-line optimum $C_{\max}^{*}(I)$ is the least makespan among feasible schedules for the original released instance $I$, with the same resources and processing rules as the online scheduler.

For parallel machines, a job of size $p_j>0$ runs at speed $s_{ij}>0$ on machine $i$. Identical machines have all speeds equal to one; uniformly related machines have $s_{ij}=s_i$; unrelated machines allow job-dependent speeds. Nonpreemptive execution completes a job in one uninterrupted interval. A restart discards a canceled attempt's work. Preemption permits work to accumulate across interruptions and migration. These are separate choices of the environment, not extra powers granted to the transformed scheduler. Source, §1, p. 1314.

The base scheduler $\mathcal A$ receives a finite admitted batch whose local release dates are all zero. Its admission information may include job sizes, or sizes may remain hidden until processing reveals completion. The transformation preserves that choice. In particular, removing advance knowledge of release dates does not remove information about sizes that the base scheduler needs.

Formalization targets

The goal is the complete algorithm transformation of Theorem 2.1. Let $\rho\ge1$ and suppose one uniform polynomial-time scheduler $\mathcal A$ always produces feasible zero-release schedules satisfying

$$C_{\max}^{\mathcal A}(B)\le\rho C_{\max}^{*}(B).$$

Then the paper's batching controller supplies one causal polynomial-time scheduler $\mathcal A'$ for unknown release dates such that, for every finite valid released instance,

$$C_{\max}^{\mathcal A'}(I)\le2\rho C_{\max}^{*}(I).$$

Both guarantees are pure multiplicative inequalities, without an unspecified additive constant. The constant $2\rho$ is fixed by the published theorem. Source, Theorem 2.1, pp. 1316–1317.

The formal target also requires an execution of the controller, feasibility of its assembled schedule, disjoint batches covering every job, and at most $n=|J|$ nonempty base invocations. If the base computation costs at most $c(N+1)^d$, the stated metered bound for the wrapper is

$$n c\bigl(N(I)+1\bigr)^d+10\bigl(N(I)+1\bigr)^2.$$

Here $N(I)$ counts encoded data cells, including release-date cells for analysis, and the constants $c,d$ and the base code are independent of both the instance and the resource configuration. The Lean statement indexes configurations explicitly, allowing their approximation factor $\rho(v)$ while retaining exactly $2\rho(v)$ in each configuration. The coefficient 10 is a bookkeeping allowance, not an approximation factor. There are no numbered milestone dependencies in the source proof; the only theorem target is Theorem 2.1.

Significance

The result allows zero-release scheduling guarantees to be used in settings with unpredictable arrivals while controlling their loss. Its scope is broader than one machine class. The source explicitly includes shop scheduling and allocation of submeshes, reflecting the independence of the conversion from particular speed formulas or off-line optimization methods. Source, p. 1317.

The mathematical theorem was proved in 1995. The task here is to formalize its statement and eventually its known guarantee. The local draft provides resource-use schedules, processing observations, an interpreted base program, and a controller whose execution is tied to the resulting schedule. Its theorem remains an open Lean proof obligation. These definitions also expose precisely what future formal proofs may assume about release information, processing information, and computation.

Difficulty

A makespan inequality alone cannot certify the result. A construction may accidentally inspect future job data, use an unattainable off-line value as an action, or count physical processing time as computational effort. Each produces a different statement from a polynomial-time online transformation.

Boundary events require equally careful treatment. Arrivals at a completion time must belong to the next batch; an arrival after an idle interval must not be lost; simultaneous arrivals must be collected together in a fixed job-ID order. Empty input and a single batch must remain meaningful without referring to nonexistent preceding batches. The source's compact stage notation is not itself an implementation specification for these cases. None of these concerns permits dropping the computational or information clauses from the target.

Formalization scope

The development uses nonnegative real time, natural-number job identities, finite profiles of half-open resource-use intervals, and a static job-local legality relation. It includes concrete parallel, shop, and mesh environment definitions. Whole-job restriction, time translation, release relaxation, and joining disjoint schedules preserve the intended static semantics. Time-dependent resource availability, external deadlines, and cross-job setup requirements are outside that interface.

The optimum inequality is written against every feasible off-line comparator. Valid jobs each have a finite legal execution; sequential execution after all releases supplies a finite feasible comparator, and makespans are bounded below by zero. Universal comparison is consequently equivalent to comparison with their infimum, including empty input.

The computational convention is an explicit finite-cell real RAM, with a finite program, a costed interpreter, and a processing port restricted to requested allocations and completion feedback. It permits arbitrary real times and does not assert a bit-complexity bound for arbitrary reals. Known and hidden sizes have separate admission encodings. Waiting for completion is a physical operation, whereas arithmetic, queue copying and message handling contribute to computation. No future job count or terminal-arrival notification is given to the controller.

The goal expressly rules out scalar-trace and vacuous-algorithm formalizations: it requires actual feasible resource schedules generated by the fixed controller using the interpreted base program, together with the computational bound. No variant theorem is posed. The recorded two-unit-job example demonstrates sharpness of this batching construction's factor 2, without claiming optimality among all possible online schedulers.

Selected references

• David B. Shmoys, Joel Wein and David P. Williamson, Scheduling Parallel Machines On-Line, SIAM Journal on Computing 24(6), 1313–1331, 1995. Published article. Theorem 2.1 and its proof occupy printed pp. 1316–1317, PDF pp. 4–5.

Motivation

Multi-stage stochastic optimization models a decision maker who acts at times $0,1,\dots,T-1$ while a random scenario unfolds, and who may use at each time only the information revealed so far. This nonanticipativity constraint is what separates a genuine multi-stage problem from a collection of deterministic ones. A standard way of measuring its cost, the expected value of perfect information of decision analysis and stochastic programming (Birge & Louveaux 2011, Ch. 4), is to compare the decision maker's optimal value with that of a clairvoyant who sees the whole scenario before deciding.

Pflug and Römisch (Modeling, Measuring and Managing Risk, World Scientific 2007, §5.2) carry out this comparison not only at the root of a scenario tree but at every node, with the expectation replaced by a general acceptability functional $\mathcal A$. This produces three stochastic processes on the tree: the optimality process, the clairvoyant process, and their difference, the value-of-information process. The book shows that, for functionals that behave linearly under mixing of distributions, the value of information is a supermartingale: the expected remaining value of perfect information decreases as the scenario is revealed, and vanishes at the horizon.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $T\ge0$. A tree process is a process $(\nu_t)_{t=0,\dots,T}$, $\nu_t$ taking values in a finite set $N_t$ of nodes, with $\sigma(\nu_t)=\sigma(\nu_s:\,s\le t)$ for every $t$: the current node determines the whole path that led to it. The root stage $N_0$ consists of one node. The standard filtration is $\boldsymbol{\mathcal F}=(\mathcal F_0,\dots,\mathcal F_T)$ with $\mathcal F_t=\sigma(\nu_t)$, and the clairvoyant's filtration is $\boldsymbol{\mathcal F}^T=(\mathcal F_T,\dots,\mathcal F_T)$.

Scenario variables are $\xi_t=f_t(\nu_t)$, $t=1,\dots,T$. A profit function $H(x_0,\xi_1,x_1,\dots,x_{T-1},\xi_T)$, written $H(x,\xi)$, depends on a decision sequence $x=(x_0,\dots,x_{T-1})$ lying in a decision space $\mathcal X$. A decision rule $x$ is a random sequence; it is non-anticipative, $x\lhd\boldsymbol{\mathcal F}$, if each $x_t$ is $\mathcal F_t$-measurable, and clairvoyant, $x\lhd\boldsymbol{\mathcal F}^T$, if each $x_t$ is $\mathcal F_T$-measurable.

A version-independent probability functional $\mathcal R$ assigns a real number to each distribution in its domain $\mathcal D$ of distributions on $\mathbb R$. For a Markov kernel $K(\cdot\mid v)$ on $\mathbb R$ and a distribution $G$ on $\mathbb R$, the compound distribution is $K\circ G=\int K(\cdot\mid v)\,dG(v)$. $\mathcal R$ is compound linear, compound convex or compound concave if

$$\mathcal R\{K\circ G\}\ \ =,\ \le,\ \ge\ \ \int\mathcal R\{K(\cdot\mid v)\}\,dG(v)$$

respectively, for all $K$, $G$ with $K(\cdot\mid v)\in\mathcal D$ for $G$-almost every $v$ and $K\circ G\in\mathcal D$, for which the right-hand integral exists ("compound linear on $\mathcal D$"; the book's Example 2.13 uses exactly this domain-relative form for expected utility).

Fix such a functional $\mathcal A$ (an acceptability functional; larger is better), whose domain contains the law of every feasible profit $H(x,\xi)$ under the conditional probabilities below. For a node $v$ of $\nu_t$ with $P\{\nu_t=v\}>0$ let $P^{\{\nu_t=v\}}=P(\cdot\mid\nu_t=v)$ and let $\mathcal A_{P^{\{\nu_t=v\}}}[Y]$ be $\mathcal A$ applied to the law of $Y$ under it. The conditional problems are

$$A_t(v)=\max\{\mathcal A_{P^{\{\nu_t=v\}}}[H(x,\xi)] : x\lhd\boldsymbol{\mathcal F},\ x\in\mathcal X\},\qquad C_t(v)=\max\{\mathcal A_{P^{\{\nu_t=v\}}}[H(x,\xi)] : x\lhd\boldsymbol{\mathcal F}^T,\ x\in\mathcal X\}.$$

At the root these are the multi-stage problem $A_0$ and the clairvoyant's problem $C_0$. The optimality process is $A_t=A_t(\nu_t)$, the clairvoyant process $C_t=C_t(\nu_t)$, and the value-of-information process $D_t=C_t-A_t$.

Formalization targets

Goal: Corollary 5.3

If $\mathcal A$ is compound linear on its domain, then

$$D_t=C_t(\nu_t)-A_t(\nu_t),\qquad t=0,\dots,T,$$

is a supermartingale under $P$ with respect to $(\mathcal F_t)$.

Milestones

1. Proposition 2.12. For a sub-$\sigma$-algebra $\mathcal F_1$ and $\mathcal R(Y\mid\mathcal F_1)$ the functional applied to the conditional distribution of $Y$ given $\mathcal F_1$: compound linearity gives $\mathcal R(Y)=\mathbb E[\mathcal R(Y\mid\mathcal F_1)]$, compound convexity $\le$, compound concavity $\ge$.
2. Lemma 5.1. If $\mathcal A$ is compound convex, $(C_t)$ is a submartingale; if compound linear, a martingale.
3. Lemma 5.2. If $\mathcal A$ is compound convex, $(A_t)$ is a submartingale.

The goal is the weakest statement of the chain: it fixes no constants and asserts only the direction of drift of $D_t$.

Significance

$D_0=C_0-A_0$ is the value of perfect information of the multi-stage problem, which the book interprets as a multi-period deviation-type risk functional (the multi-period average value-at-risk deviation of its Chapter 3 is an instance). The supermartingale property gives this risk a dynamic meaning: as the scenario is revealed, the remaining value of information decreases in conditional mean, and it is zero at the horizon. The two lemmas separate the effect of information into its two sources: the clairvoyant's value is a fair game for compound linear functionals, while the non-anticipative decision maker's value can only improve in conditional mean, because a decision fixed at time $t$ remains feasible after more is revealed.

The results are proved in the book. No formal version is known: the platform has no item on value-of-information processes, clairvoyant problems or compounding properties of functionals; the closest related items are a complete-information bound in partially observed Markov decision processes and a submartingale property of stable multi-period risk processes, both in other settings. A formalization adds a precise setting (finite scenario trees, conditioning on nodes, attained maxima) in which the chain from Definition 2.11 to Corollary 5.3 is checked.

Difficulty

The supermartingale inequality is a statement about conditional expectations on a tree, while compound convexity is a statement about functionals of mixtures of distributions; the work is to identify the law of the profit under $P^{\{\nu_t=v\}}$ as a compound distribution of the laws under the children's conditional probabilities, with the children encoded as a real mixing parameter. The book's proof of Lemma 5.1 interchanges the maximum and the functional, a step it justifies elsewhere only for monotone functionals, which Lemma 5.1 does not assume; its proof of Lemma 5.2 applies an inequality stated for nonrandom decisions to random ones. A solver should not rely on either step as printed. The martingale half of Lemma 5.1 needs the reverse inequality, for which the optimizers of the child problems must be combined into one feasible clairvoyant decision; the same combination is not available for non-anticipative decisions, which is why the optimality process is only a submartingale. Proposition 2.12 additionally needs regular conditional distributions.

Formalization scope

Lean 4 with Mathlib. Time is Fin (T + 1), stage $0$ being the single root node ([Unique (N 0)]), so $\mathcal F_0$ is trivial. Node types are finite with measurable singletons; this is what makes $P(\cdot\mid\nu_t=v)$ meaningful at every node of positive probability (Mathlib's ProbabilityTheory.cond) and every process integrable. The filtration is a Mathlib Filtration assumed equal to $\sigma(\nu_t)$ at each stage, and sub-, super- and martingales are Mathlib's Submartingale, Supermartingale, Martingale. Decisions take values in a measurable space with measurable singletons, $x\in\mathcal X$ holds for every $\omega$, and $H$ is jointly measurable. The functional is 𝒜 : Measure ℝ → ℝ, version-independent by construction, evaluated only at probability measures; it is real-valued (the book allows $\overline{\mathbb R}$) with a domain 𝒟 : Set (Measure ℝ), and each compounding (in)equality is required only when the mixed and the mixing distributions lie in $\mathcal D$ and $v\mapsto\mathcal R\{K(\cdot\mid v)\}$ is integrable. The tree theorems assume that $\mathcal D$ contains the law of every feasible profit under every conditional probability of a positive-probability node; Proposition 2.12 assumes $Y\in\operatorname{dom}\mathcal R$ and that the conditional distributions are in $\mathcal D$ almost surely. Mixing is over Markov kernels from $\mathbb R$ to $\mathbb R$ (K ∘ₘ G). Proposition 2.12 uses Mathlib's condExpKernel on a standard Borel space and assumes $\mathbb E[\mathcal R(Y\mid\mathcal F_1)]$ exists.

The maxima $A_t(v)$, $C_t(v)$ are not defined through sSup: the theorems take them as given numbers and assume each is the greatest element of its value set at every node of positive probability. This rules out the trivializing formalization in which a junk supremum of an empty or unbounded set makes the processes constant and the claim empty. The book's remark "in particular if $\mathcal A$ is the expectation" is covered as an instance and not stated separately: the expectation is compound linear on the distributions with a finite mean, and on a finite tree every feasible profit has finitely many values. Taking $\mathcal D$ to be all distributions instead would exclude the expectation, because Lean's Bochner integral of a non-integrable function is $0$.

Needed infrastructure: finite partitions and conditional expectation on atoms, mixtures of conditional laws, measurable selection of child optimizers on a finite tree, and the disintegration property of condExpKernel. The definitions CompoundLinear/CompoundConvex/CompoundConcave, IsTreeProcess, and the decision-problem sets are reusable for other results of the book on conditional acceptability and multi-stage problems. Proofs of any milestone, and sorry-free instances showing the hypotheses are satisfiable (e.g. a bounded expected utility on a two-stage tree), are welcome.

Selected references

• G. Ch. Pflug, W. Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007, §2.1.2 and §5.2. https://doi.org/10.1142/6478
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011 (value of perfect information and of the stochastic solution). https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Risk that unfolds over several periods is measured in two common ways. One adds up one-period measurements of each payment, each made with the information available one step earlier. The other composes one-period conditional measurements backwards in time, the way dynamic programming evaluates a policy. The second way is the one used in multistage stochastic programming with risk-averse objectives, because it is time-consistent by construction: a plan that is optimal today stays optimal when re-evaluated tomorrow. Ruszczyński and Shapiro (Conditional risk mappings, Math. Oper. Res. 2006) built the general theory of such compositions. Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) studied the matching dynamic-programming (Bellman) principle for coherent multiperiod risk-adjusted values.

The most widely used one-period building block is the average value-at-risk. When it is applied conditionally at every stage, the composition is the nested average value-at-risk. Section 3.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007), treats both constructions. It builds the nested functional, shows that it depends only on the total payoff, gives its dual representation as an infimum over bounded-growth martingale densities, and compares it with the additive (multi-period) average value-at-risk. This mission formalizes that section's statements.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with a filtration $\mathcal F_0=\{\emptyset,\Omega\}\subseteq\mathcal F_1\subseteq\dots\subseteq\mathcal F_T=\mathcal F$. Random variables that agree almost surely are identified, and all (in)equalities between them hold almost surely. The book uses profit variables, where larger is better. Fix $p\in[1,\infty)$ and put $\mathcal Y_t=L_p(\Omega,\mathcal F_t,\mathbb P)$. An income process is $Y=(Y_1,\dots,Y_T)$ with $Y_t\in\mathcal Y_t$.

A conditional acceptability mapping $\mathcal A_{t-1}:\mathcal Y_T\to\mathcal Y_{t-1}$ has three properties:

• (CA1) $\mathcal A_{t-1}(Y_T+Y_{t-1})=\mathcal A_{t-1}(Y_T)+Y_{t-1}$ for $Y_{t-1}\in\mathcal Y_{t-1}$;
• (CA2) it is concave;
• (CA3) it is monotone.

A family $\mathcal A_0,\dots,\mathcal A_{T-1}$ defines the nested functional and the compositions

$$\mathcal A(Y;\boldsymbol{\mathcal F})=\mathcal A_0\big[Y_1+\dots+\mathcal A_{T-2}[Y_{T-1}+\mathcal A_{T-1}(Y_T)]\cdots\big],\qquad \mathcal A^{(t)}=\mathcal A_0\circ\dots\circ\mathcal A_{t-1}.$$

Since $\mathcal F_0$ is trivial, both are constants.

For $\alpha\in(0,1]$ and a sub-$\sigma$-field $\mathcal G$, the conditional average value-at-risk $\mathbb{AV@R}_\alpha(Y\mid\mathcal G)\in L_1(\mathcal G)$ of $Y\in L_1(\mathcal F)$ is defined implicitly by

$$\mathbb E\big(\mathbb{AV@R}_\alpha(Y\mid\mathcal G)\,\mathbb 1_B\big)=\inf\Big\{\mathbb E(YZ):0\le Z\le\tfrac1\alpha\mathbb 1_B,\ \mathbb E(Z\mid\mathcal G)=\mathbb 1_B\Big\}\qquad(B\in\mathcal G).$$

With trivial $\mathcal G$ this is the lower-tail average $\frac1\alpha\int_0^\alpha G^{-1}(u)\,du$ of the quantile function. The nested average value-at-risk is

$$\mathrm{n}\mathbb{AV@R}_\alpha(Y;\boldsymbol{\mathcal F})=\mathbb{AV@R}_\alpha(\cdot\mid\mathcal F_0)\circ\dots\circ\mathbb{AV@R}_\alpha(\cdot\mid\mathcal F_{T-1})\Big(\sum_{t=1}^TY_t\Big).$$

The multi-period average value-at-risk is $\mathbb{AV@R}_{\alpha,c}(Y;\boldsymbol{\mathcal F})=\sum_{t=1}^Tc_t\,\mathbb E[\mathbb{AV@R}_{\alpha_t}(Y_t\mid\mathcal F_{t-1})]$. Below it is used with all $\alpha_t=\alpha$ and $c_t=1$.

Formalization targets

Goal: dual representation of the nested average value-at-risk (Proposition 3.35, (3.49))

For $Y_t\in L_1(\mathcal F_t)$ and $\alpha\in(0,1]$, the nested average value-at-risk is well defined, and

$$\mathrm{n}\mathbb{AV@R}_\alpha(Y;\boldsymbol{\mathcal F})=\inf\Big\{\mathbb E\big[(Y_1+\dots+Y_T)Z_T\big]:0\le Z_t\le\tfrac1\alpha Z_{t-1},\ \mathbb E(Z_t\mid\mathcal F_{t-1})=Z_{t-1},\ Z_0=1,\ t=1,\dots,T\Big\}.$$

Here $Z_t$ is $\mathcal F_t$-measurable. The feasible $(Z_t)$ are nonnegative martingales whose one-step growth is at most $1/\alpha$.

Milestones

1. Proposition 3.33. The nested functional of any family of conditional acceptability mappings has these properties:
   • it is weakly translation-equivariant, concave and monotone;
   • every $\mathcal A^{(t)}$ is an acceptability functional;
   • $\mathcal A(Y;\boldsymbol{\mathcal F})=\mathcal A^{(T)}(Y_1+\dots+Y_T)$ (3.47);
   • positive homogeneity is inherited from the mappings.
2. The step in the proof of Proposition 3.35 (via (2.59)). For bounded $Z_1\ge0$ that is $\mathcal F_1$-measurable, $\mathbb E(\mathbb{AV@R}_\alpha(Y\mid\mathcal F_1)Z_1)=\inf\{\mathbb E(YZ_2):0\le Z_2\le\frac1\alpha Z_1,\ \mathbb E(Z_2\mid\mathcal F_1)=Z_1\}$.
3. Proposition 3.36(ii). For a final process ($Y_1=\dots=Y_{T-1}=0$), $\mathrm{n}\mathbb{AV@R}_\alpha(Y;\boldsymbol{\mathcal F})\le\mathbb{AV@R}_\alpha(Y;\boldsymbol{\mathcal F})$.

Further items

• Proposition 3.36(i), $\mathrm{n}\mathbb{AV@R}_\alpha\le\alpha^{-(T-1)}\mathbb{AV@R}_\alpha$, stated as printed.
• The information-monotonicity clause of Proposition 3.35: if $\mathcal F_t\subseteq\mathcal F'_t$ for all $t$, then $\mathrm{n}\mathbb{AV@R}_\alpha(Y;\boldsymbol{\mathcal F})\le\mathrm{n}\mathbb{AV@R}_\alpha(Y;\boldsymbol{\mathcal F}')$. It is stated as its own item, as printed.

Significance

The representation (3.49) shows that the nested average value-at-risk is a coherent functional of the total payoff. Its dual set consists of martingale densities with a multiplicative growth bound. Proposition 3.36 builds on this description to compare the nested and additive constructions. The same description underlies cutting-plane methods for risk-averse multistage programs: there the nested value is evaluated stage by stage, and each stage contributes one factor $Z_t/Z_{t-1}\in[0,1/\alpha]$. Proposition 3.33 is the general mechanism behind this: predictable translation-equivariance collapses a nested definition into a cumulative one.

All of these results are proved in the book, some only in outline. None is machine-checked. The platform has loss-side, upper-tail conditional value-at-risk results in other conventions and a nested risk-adjusted cost in an SDDP setting. It has no statement of the nested average value-at-risk or of (3.49). Formalizing this section yields a reusable treatment of conditional average values-at-risk defined by duality, together with their compositions along a filtration.

Difficulty

The conditional average value-at-risk is not given by a formula. It is defined through a family of infima indexed by the sets $B\in\mathcal G$, so composing two of them requires knowing what the first one does when paired with a general bounded weight rather than an indicator. Merging the infima of successive stages into one infimum over processes needs measurable selection of near-optimal densities, conditional on the earlier stages, and the martingale constraint must be preserved. The printed proof treats $T=2$ in a few lines and asserts that the general case "follows by induction". Its last display also carries a misprint, $\mathbb E(Z_1)=0$ for $\mathbb E(Z_1)=1$ (FINDINGS F5).

Formalization scope

Random variables are functions Ω → ℝ. The filtration is Mathlib's Filtration ℕ, and only indices $0,\dots,T$ matter. IsStandardFiltration records that $\mathcal F_0$ is trivial and $\mathcal F_T=\mathcal F$. The conditional average value-at-risk is the predicate IsConditionalAVaR, a literal transcription of the defining relation, with the infimum computed in EReal. The nested and multi-period values are predicates that are existential over versions of the conditional average values-at-risk. The goal therefore asserts existence and the identity separately. A version of the goal that only assumed some value exists, or that took a bare real infimum, would be vacuous or junk-valued, and the formal statement rules out both. The expectation of the $\mathcal F_0$-measurable output is the functional's real value. The dual set requires $Z_t$ to be $\mathcal F_t$-measurable, which the page leaves implicit.

Beyond the paper. Two corrected variants are posed beside the faithful statements:

• Information monotonicity (F1). Refining $\mathcal F_1$ in a two-period example lowers the nested value from $-5$ to $-10$. The variant asserts that a counterexample exists.
• Proposition 3.36(i) for $Y_t\ge0$ (F2). The printed inequality fails for $Y_2\equiv-1$ with $\alpha=1/2$. The variant adds the nonnegativity that the proof uses.

The faithful statements stay as printed and are expected to be disproved.

Contributions that would be reused beyond this mission:

• existence and uniqueness of the conditional average value-at-risk on $L_1$;
• its extension to bounded nonnegative weights;
• a general composition lemma for dual representations of conditional acceptability mappings.

Selected references

• G. Ch. Pflug and W. Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007, §3.3. https://doi.org/10.1142/6478
• A. Ruszczyński and A. Shapiro, Conditional risk mappings, Mathematics of Operations Research 31(3), 2006. https://doi.org/10.1287/moor.1060.0204
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath and H. Ku, Coherent multiperiod risk adjusted values and Bellman's principle, Annals of Operations Research 152, 2007. https://doi.org/10.1007/s10479-006-0132-6

Why mean-variance portfolios

An investor who splits a budget across $M$ risky assets faces a trade-off between expected return and risk. Markowitz proposed measuring risk by the variance of the portfolio return and selecting, for each required expected return, the portfolio of least variance (Markowitz 1952). Tobin added a risk-free asset (Tobin 1958), and Sharpe, Lintner and Mossin turned the resulting one-fund structure into the capital asset pricing model (CAPM), whose beta equation is still the standard first model of expected returns in finance (Sharpe 1964).

This mission formalizes the closed-form part of that theory as presented in §4.2.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), pp. 189–195: the explicit efficient portfolio without a risk-free asset (Proposition 4.8), the solution with a risk-free asset (Proposition 4.9), and the CAPM equation with its variance bound (Proposition 4.10).

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $\xi=(\xi^{(1)},\dots,\xi^{(M)})$ a random vector of returns, each coordinate with a finite second moment. Returns are profits: larger is better. The vector of expected returns is $r=\mathbb E\xi$ and the covariance matrix is the $M\times M$ matrix $C$ with $C_{ij}=\mathbb{C}\mathrm{ov}(\xi^{(i)},\xi^{(j)})$; it is symmetric and positive semidefinite. A portfolio is a weight vector $x\in\mathbb R^M$ (negative weights, i.e. short positions, are allowed) with return $Y_x=\sum_m x_m\xi^{(m)}$, so that $\mathbb E(Y_x)=r^\top x$ and $\mathbb{V}\mathrm{ar}(Y_x)=x^\top Cx$. Write $\mathbb 1$ for the all-ones vector.

The CAPM problem without a risk-free asset fixes a required return $\mu$ and asks for

$$\text{minimize } x^\top Cx\quad\text{subject to}\quad r^\top x=\mu,\ \ \mathbb 1^\top x=1. \tag{4.20}$$

With a risk-free asset of constant return $r_0$, a portfolio is a pair $(x_0,\tilde x)$, where $x_0$ is the holding of the risk-free asset and $\tilde x$ the holdings of the risky assets $\tilde\xi$, with mean $\tilde r$ and covariance $\tilde C$. Its return is $Y_x=x_0r_0+\tilde x^\top\tilde\xi$, and the problem is

$$\text{minimize } \tfrac12\tilde x^\top\tilde C\tilde x\quad\text{subject to}\quad \tilde r^\top\tilde x+r_0x_0=\mu,\ \ \mathbb 1_M^\top\tilde x+x_0=1. \tag{4.23}$$

A portfolio is efficient if it solves the respective problem for some $\mu$. The market portfolio $x_+$ holds nothing in the risk-free asset and $\tilde C^{-1}(\tilde r-r_0\mathbb 1)/\mathbb 1^\top\tilde C^{-1}(\tilde r-r_0\mathbb 1)$ in the risky ones; $Y_+$ is its return, $\mu_+=\mathbb E(Y_+)$ and $\sigma_+^2=\mathbb{V}\mathrm{ar}(Y_+)$.

Formalization targets

Goal: Proposition 4.8, the efficient portfolio in closed form

Assume $C$ is invertible and $r$ is not a multiple of $\mathbb 1$. With

$$a=r^\top C^{-1}r,\quad b=r^\top C^{-1}\mathbb 1,\quad c=\mathbb 1^\top C^{-1}\mathbb 1,\quad d=ac-b^2, \tag{4.22}$$

the unique solution of (4.20) is

$$x^*(\mu)=\mu\Big[\frac cd C^{-1}r-\frac bd C^{-1}\mathbb 1\Big]+\Big[\frac ad C^{-1}\mathbb 1-\frac bd C^{-1}r\Big], \tag{4.21}$$

any two efficient portfolios for different returns span all efficient portfolios by affine combinations (the Two Fund Theorem in this model), and

$$\mathbb E(Y_\mu)=\mu,\qquad \mathbb{V}\mathrm{ar}(Y_\mu)=\frac{\mu^2c-2\mu b+a}{d}.$$

The efficient frontier is therefore a parabola in the (variance, mean) plane.

Milestones and further results

Propositions 4.10 (i) and (ii) are milestones; Proposition 4.9 is a further item of the mission on which they stand.

1. Proposition 4.9. If $\tilde C$ is invertible and $\tilde r\ne r_0\mathbb 1$, then with $q=(\tilde r-r_0\mathbb 1)^\top\tilde C^{-1}(\tilde r-r_0\mathbb 1)$ the unique solution of (4.23) is

$$x^*(\mu)=\frac1q\begin{pmatrix}(\tilde r-\mu\mathbb 1)^\top\tilde C^{-1}(\tilde r-r_0\mathbb 1)\\(\mu-r_0)\tilde C^{-1}(\tilde r-r_0\mathbb 1)\end{pmatrix},$$

and, when $\mathbb 1^\top\tilde C^{-1}(\tilde r-r_0\mathbb 1)\ne0$, every efficient portfolio is an affine combination of $(1,0,\dots,0)$ and $x_+$. 2. Proposition 4.10 (i), the CAPM equation (4.25). For every portfolio with $x_0+\mathbb 1^\top\tilde x=1$,

$$\mathbb E(Y_x)=r_0+\beta(x)(\mu_+-r_0),\qquad \beta(x)=\frac{\mathbb{C}\mathrm{ov}(Y_x,Y_+)}{\mathbb{V}\mathrm{ar}(Y_+)}.$$

3. Proposition 4.10 (ii). For every such portfolio

$$\mathbb{V}\mathrm{ar}(Y_x)\ge\Big(\frac{\mathbb E(Y_x)-r_0}{\mu_+-r_0}\Big)^2\sigma_+^2,$$

with equality if and only if the portfolio is efficient, and, as printed, if and only if $\mathbb{C}\mathrm{orr}(Y_x,Y_+)=1$.

Significance

Proposition 4.8 is the explicit description of the mean-variance efficient set: the efficient portfolios form a line in weight space, and the minimal variance is a quadratic function of the required return. Proposition 4.9 shows that a risk-free asset turns this line into one through the risk-free portfolio (the one-fund, or separation, property), and Proposition 4.10 derives from it the CAPM relation between a portfolio's expected excess return and its beta, together with the capital-market-line bound. These are the statements on which the later sections of the chapter, and most textbook treatments of portfolio theory, build: risk-return diagrams, the market portfolio, beta as a risk measure.

The results are classical and their proofs are elementary, but they are not in Mathlib, and no Prove2Me item states them; the closest platform item is the multi-period mean-variance mutual fund theorem of Bäuerle and Rieder (MDPFinance.MeanVariance.mutual_fund_theorem), a different, dynamic statement. A formalization makes the hypotheses explicit that the printed proofs leave implicit (invertibility and nondegeneracy conditions, the budget constraint behind "any portfolio") and checks the printed equality conditions, one of which is false as stated.

Difficulty

The Lagrange conditions of the printed proof are necessary conditions only. Turning them into the statement requires showing that the stationary point is the global minimizer and the only one, which uses positive definiteness of $C$; the hypothesis gives only invertibility, and positive definiteness has to come from $C$ being a covariance matrix. Dividing by $d$ needs $d>0$, which is not among the hypotheses and must be derived from "$r$ is not a multiple of $\mathbb 1$" together with the structure of $C$. The variance identities require computing variances and covariances of linear combinations of square-integrable random variables. In Proposition 4.10 (ii) the equality case is where the printed statement goes wrong: a portfolio short in the market portfolio attains equality with correlation $-1$.

Formalization scope

All statements live in the namespace RiskFunctionals.Frontier. Assets are indexed by Fin M; vectors are Fin M → ℝ, matrices Matrix (Fin M) (Fin M) ℝ, and $C^{-1}$ is Mathlib's matrix inverse. The mean vector and covariance matrix are computed from a random vector with MemLp 2 coordinates on a probability space using Mathlib's covariance and variance, so "$C$ invertible" is the printed hypothesis and positive definiteness is a consequence, not an assumption. "The solution" is stated as existence and uniqueness of a global minimizer on the feasible set (IsSolution420, IsSolution423). The divisions by $q$, by $\mathbb 1^\top\tilde C^{-1}(\tilde r-r_0\mathbb 1)$ and by $d$ are guarded by the printed or implicit nondegeneracy hypotheses; a statement in which $d=0$ or $q=0$ were allowed would make the closed forms the zero vector, so these guards are part of the statement rather than conveniences. The correlation is used only where the portfolio variance is positive, since it is undefined otherwise.

Beyond the paper. One variant item is posed beside the faithful statements: capm_variance_bound_corrected (corrected, finding F4) replaces the equality condition $\mathbb{C}\mathrm{orr}(Y_x,Y_+)=1$ of Proposition 4.10 (ii) by $|\mathbb{C}\mathrm{orr}(Y_x,Y_+)|=1$; with one risky asset of mean 2 and variance 1, $r_0=1$ and $x=(2,-1)$, equality holds while the correlation is $-1$. The faithful Proposition 4.10 (ii) is therefore expected to be disproved.

A complete development needs the variance and covariance of finite linear combinations of $L^2$ random variables, positive semidefiniteness of covariance matrices, and the minimization of a positive definite quadratic form under linear equality constraints. These are reusable well beyond this mission; proofs of them as separate lemmas are welcome.

Selected references

• G. Ch. Pflug and W. Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007, §4.2.3, pp. 189–195. https://doi.org/10.1142/6478
• H. Markowitz, Portfolio Selection, Journal of Finance 7(1), 77–91, 1952. https://doi.org/10.2307/2975974
• J. Tobin, Liquidity Preference as Behavior Towards Risk, Review of Economic Studies 25(2), 65–86, 1958. https://doi.org/10.2307/2296205
• W. F. Sharpe, Capital Asset Prices: A Theory of Market Equilibrium under Conditions of Risk, Journal of Finance 19(3), 425–442, 1964. https://doi.org/10.1111/j.1540-6261.1964.tb02865.x
• R. C. Merton, An Analytic Derivation of the Efficient Portfolio Frontier, Journal of Financial and Quantitative Analysis 7(4), 1851–1872, 1972. https://doi.org/10.2307/2329621

Motivation

A distortion functional values an uncertain profit $Y$ by integrating its quantiles against a reweighting of the probability scale: small (bad) quantiles receive more weight, large ones less. The construction appears in actuarial pricing (the distortion premium principles of Denneberg and Wang), in decision theory (Yaari's dual theory of choice), and in finance as spectral risk measures (Acerbi) or weighted values-at-risk (Cherny). Its central structural fact is that every concave distortion is a mixture of average values-at-risk, the lower-tail averages $\mathbb{AV@R}_\alpha$: this Choquet representation reduces properties of the whole class (concavity, monotonicity with respect to second-order dominance, comonotone additivity) to those of one family. The representation was proved by Acerbi (2002), Jones and Zitikis (2003) and Pflug (2006). This mission formalizes it as Proposition 2.64 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, §2.4.2), together with the lemmas of that section.

Setting

All random variables are profit variables (larger is better) on a probability space $(\Omega,\mathcal F,\mathbb P)$. For a random variable $Y$ with distribution function $G(u)=\mathbb P\{Y\le u\}$ and left limit $G(u-)=\mathbb P\{Y<u\}$, the quantile function is the left-continuous inverse

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

and the average value-at-risk at level $0<\alpha\le1$ is

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

A distortion function $H$ is a bounded, right continuous, increasing function on $[0,1]$, the distribution function of a non-negative measure $dH$ on $[0,1]$ (not necessarily a probability measure). Writing $\mathcal G_H$ for the distributions $G$ for which $G^{-1}$ is $dH$ integrable, the distortion acceptability functional is

$$\mathcal A_H\{G\}=\int_0^1 G^{-1}(p)\,dH(p),\qquad G\in\mathcal G_H,$$

also written $\mathcal A_H(Y)$. $H(p)=p$ gives the expectation, $H=\mathbb 1_{[\alpha,1]}$ the value-at-risk $G^{-1}(\alpha)$, and $H(p)=\min(p/\alpha,1)$ the average value-at-risk. $H$ is concave when $H(p)=\int_0^p h(\alpha)\,d\alpha$ with a nonincreasing density $h$, which may be unbounded near $0$.

Two orders on random variables enter: $Z\prec_{CXD}Z^*$ (convex order) when $\mathbb E\,U(Z)\le\mathbb E\,U(Z^*)$ for every convex $U$ for which both expectations exist; and $Y_1,Y_2$ are comonotone when their joint distribution function is $\min(G_1(u),G_2(v))$. A functional is comonotone additive when it is additive on comonotone pairs.

Formalization targets

Goal: the Choquet representation (Proposition 2.64)

If $H$ is concave, there is an increasing function $M$ on $[0,1]$ with $M(0)=0$ and $M(1)=H(1)$ such that, for every $G\in\mathcal G_H$,

$$\mathcal A_H\{G\}=\int_0^1\mathbb{AV@R}_\alpha\{G\}\,dM(\alpha).$$

Conversely, every comonotone additive functional having such a Choquet representation is a distortion functional. The goal leaves $M$ otherwise unspecified; one $M$ serves every $G$.

Milestones

1. Examples 2.63: the three distortions $H(p)=p$, $\mathbb 1_{[\alpha,1]}(p)$ and $\min(p/\alpha,1)$ give $\mathbb E(Y)=-\int_{-\infty}^0G+\int_0^\infty(1-G)$, $G^{-1}(\alpha)$ and $\mathbb{AV@R}_\alpha$.
2. Lemma 2.62: for $G\in\mathcal G_H$, with $\bar H(u)=H(1)-H(1-u)$,

$$\int_0^1 G^{-1}(p)\,dH(p)=-\int_{-\infty}^0H(G(u))\,du+\int_0^\infty\bar H(1-G(u))\,du .$$

3. Eq. (2.68): for $U$ uniform on $[0,1]$ and independent of $Y$, the generalized quantile transform $(1-U)G(Y-)+UG(Y)$ is uniform on $[0,1]$.
4. Eq. (2.69): for differentiable $H$ with $H(p)=\int_0^ph$, $\mathcal A_H(Y)=\mathbb E\big[Y\,h\big((1-U)G(Y-)+UG(Y)\big)\big]$.
5. Proposition 2.65, as printed: for differentiable $H$, $\mathcal A_H(Y)=\inf\{\mathbb E(YZ): Z=h(U),\ U\text{ uniform}\}=\inf\{\mathbb E(YZ):Z\prec_{CXD}h(U)\}$, attained at $Z=h\big((1-U)G(Y-)+UG(Y)\big)$.

Significance

The Choquet representation identifies the concave distortion functionals with the closed convex cone generated by the average values-at-risk. Downstream, this gives the coherence properties of spectral risk measures, their consistency with second-order stochastic dominance, and, through Proposition 2.65, a dual description by rearrangements of the distortion density that is used to optimize portfolios under such criteria. It also separates the class from the larger family of law-invariant coherent functionals, which are infima of such mixtures over a family of mixing measures (Kusuoka) rather than single mixtures.

The results are classical and proved in the literature; none is machine-checked in this form. A related loss-side layer exists on the platform (MultistageStochastic.distortion_avar_mixture, proved, for a spectrum $\sigma$ on $L_\infty$ with the upper-tail AV@R), but its sign, tail and integrability conventions differ, so it does not state this book's theorem. The formalization adds a quantile calculus with atoms (the left-continuous $G^{-1}$, $G(u-)$, the generalized quantile transform) and Lebesgue–Stieltjes integration against distortion measures, both reusable for the rest of the series.

Difficulty

The forward direction is not a finite-dimensional extreme-point argument: $h$ may be unbounded at $0$, so the mixing measure $dM$ must be obtained as a limit and the exchange of integrals justified for quantile functions that are only $dH$-integrable, with $G^{-1}$ unbounded at both ends. Distributions with atoms make $G^{-1}(G(u))<u$ on flat stretches, which is exactly where Lemma 2.62 and (2.69) need care.

Proposition 2.65 is false as printed (finding F1): for the differentiable convex $H(p)=p^2$ and $Y$ uniform on $[0,1]$, $\mathcal A_H(Y)=2/3$, while $Z=2(1-Y)=h(1-Y)$ gives $\mathbb E(YZ)=1/3$. Its printed proof uses that $h$ is nonincreasing. The faithful milestone is therefore expected to be disproved; a corrected variant is posed beside it.

Formalization scope

Distributions are probability measures $\mu$ on $\mathbb R$; for a random variable, $\mu$ is the image measure of $\mathbb P$ under $Y$. $G^{-1}$ is computed by sInf; its junk value $0$ (at $p=1$ when $G<1$ everywhere, and at $p\le0$) is never charged. $H$ and $M$ are Mathlib StieltjesFunctions; $\mathcal A_H$ integrates over $(0,1]$ against $dH$. Membership in $\mathcal G_H$ contains $dH$-integrability of $G^{-1}$, $H(0)=0$ (the mass $dH$ puts on $p=0$, where $G^{-1}=-\infty$), and finiteness of $G^{-1}(1)$ when $dH$ charges $p=1$. $M$ vanishes on $(-\infty,0]$, so $dM$ has no atom at $0$, and the representation integrates over $[0,1]$; $dM$-integrability of $\alpha\mapsto\mathbb{AV@R}_\alpha$ is part of the conclusion, and the converse is stated on integrable $Y$ for which that integrability holds. Infima in Proposition 2.65 are greatest lower bounds of value sets restricted to integrable products, with attainment stated separately. Uniform variables are measurable with law Lebesgue measure on $[0,1]$, and $U$ is independent of $Y$ in (2.68)–(2.69), as Proposition 1.3 requires. The book's $V_Y=(1-U)[G(Y-)-G(Y)]$ has a sign typo and is used as $(1-U)[G(Y)-G(Y-)]$.

A trivializing formalization would integrate a quantile function that is not $dH$- or $dM$-integrable, where Lean's integral returns $0$, or take an infimum of an empty set; every such integral is guarded by an integrability hypothesis or an asserted integrability, and every infimum is an IsGLB of a set shown nonempty by the attainment clause.

Beyond the paper. One variant: [Corrected] Proposition 2.65 adds the hypothesis "$H$ concave" and changes nothing else (finding F1, the counterexample above). A further finding (F2) records that the converse half of Proposition 2.64 does not use comonotone additivity; no variant is posed for it.

Contributions welcome: proofs of the milestones, a disproof of the printed Proposition 2.65, and reusable lemmas on quantile functions with atoms and on Stieltjes integration on $[0,1]$.

Selected references

• G. Ch. Pflug, W. Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007. https://doi.org/10.1142/6478
• C. Acerbi, Spectral measures of risk: a coherent representation of subjective risk aversion, Journal of Banking & Finance 26 (2002). https://doi.org/10.1016/S0378-4266(02)00281-9
• B. L. Jones, R. Zitikis, Empirical estimation of risk measures and related quantities, North American Actuarial Journal 7 (2003). https://doi.org/10.1080/10920277.2003.10596118
• G. Ch. Pflug, On distortion functionals, Statistics & Decisions 24 (2006). https://doi.org/10.1524/stnd.2006.24.1.45
• M. E. Yaari, The dual theory of choice under risk, Econometrica 55 (1987). https://doi.org/10.2307/1911158
• S. S. Wang, A class of distortion operators for pricing financial and insurance risks, Journal of Risk and Insurance 67 (2000). https://doi.org/10.2307/253675

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.