Probability

Motivation

Every packet-switched network — an internet router, a data-center fabric, a wireless base station — must decide, timeslot by timeslot, which of many competing transfers to schedule under shared physical constraints (link capacities, interference between simultaneous transmissions). Walton (2015) introduced the random proportional scheduler (RPS): rather than solving a combinatorial scheduling problem exactly, RPS picks a randomized link configuration whose mean matches the proportionally-fair allocation of Kelly (1997) applied at the link level, then disaggregates the resulting transfer budget across competing packet classes by independent random selection. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Sections 12.6-12.7 to this policy, and closes the book with Theorem 12.28: under an explicit load condition, RPS is stable. This mission formalizes that closing result and the machinery beneath it. It is the fourteenth and final mission of a series covering the book chapter by chapter; the series as a whole runs from the equivalence of stochastic-processing-network stability and fluid-model stability (mission I, Theorem 3.5/6.2) through discrete-time, slotted packet networks (missions XII-XIV), and this mission's own goal theorem is the last numbered result the book proves.

Setting

A packet network with fixed routing (Section 12.6) has I packet classes; each class i routes, after one hop of processing, deterministically to a single successor class or exits the network — encoded here as a function $\mathrm{route} : I \to I \cup \{\text{exit}\}$. The K links are indexed by $\mathcal K$, and a matrix $A$ assigns each class to the single link its next transfer uses; $\mathcal I(k)$ denotes the classes belonging to link $k$. At the start of a timeslot, $z\in\mathbb Z^I_+$ is the vector of class-level packet counts and $y := Az$ the corresponding link-level counts. The RPS algorithm (four steps, page 245 of the printed book): (a) solve the concave program $\psi(y) := \operatorname{argmax}\{\sum_k y_k\log(\hat c_k) : \hat c \in \langle C\rangle\}$ (Eq. 12.57), where $C$ is the finite set of feasible link configurations and $\langle C\rangle$ its convex hull; (b) randomize a link configuration $c$ with mean $\psi(y)$; (c) transfer $\min(c_k,y_k)$ packets over link $k$; (d) select which packets to transfer uniformly at random from each link's queue. This makes $Z=\{Z(\tau):\tau\in\mathbb Z_+\}$ a discrete-time Markov chain. The function $\psi$ is exactly the proportionally fair (PF) allocation function of Section 10.1, applied here with the link-level demand vector $y$ in place of the PF model's job-class demand vector.

Formalization targets

Goal: Theorem 12.28 — the load condition implies RPS stability

$$\rho < \hat c \text{ for some } \hat c \in \langle C\rangle, \quad \rho := A\alpha, \quad \alpha := R^{-1}\lambda \quad\Longrightarrow\quad \text{(a) the RPS fluid model is stable, and hence}$$ $$\text{(b) the discrete-time Markov chain } Z \text{ under RPS control is positive recurrent.}$$

Here $\lambda$ is the vector of external arrival rates, $\alpha$ the resulting vector of total (external plus internally routed) arrival rates into each class, and $R$ the input-output matrix determined by $\mathrm{route}$. The load condition (12.50) is the natural feasibility requirement — average link traffic strictly below some feasible mean capacity — and the theorem asserts it is also sufficient for stability.

Supporting milestones

Lemma 12.23 is an almost-sure convergence result for a residual process $\xi^z_i(\tau) := \sum_{m=1}^\tau (s_i(m) - \hat s_i(m))$ tracking the gap between RPS's actual per-class transfers and their conditional means — a bounded martingale-difference sum, hence governed by the strong law of large numbers. Theorem 12.24 is the RPS fluid equation: along any fluid limit on the event where both Lemma 12.12's arrival-process SLLN and Lemma 12.23's residual-process SLLN hold, every occupied class's departure rate is pinned to $(\hat Z_i(t)/\hat Y_k(t))\,\psi_k(\hat Y(t))$. Proposition 12.26 identifies the resulting RPS fluid model as literally a special case of the PF fluid model of Section 10.4 (one demand group per link, $\langle C\rangle$ playing the role of the PF model's reduced allocation set), and Theorem 12.27 is this chapter's own version of the fluid-to-stochastic transfer theorem (Theorem 6.2's slotted-time analogue, restricted to RPS): fluid stability of the RPS model implies positive recurrence of $Z$.

Significance

The result itself. Theorem 12.28 closes the loop the book opens with proportional fairness in Chapter 10: PF was introduced there as a static resource-allocation rule with no queueing content; Theorem 12.28 shows that layering PF onto a genuinely dynamic, multi-hop, discrete-time packet network — RPS — inherits stability under exactly the load condition one would hope for, with no loss from the randomized disaggregation step (d) of the algorithm. Combined with Theorem 12.8 (packet-network stability implies subcriticality, mission XII) and Eq. (12.50)'s equivalence to that subcritical region under fixed routing, this makes RPS maximally stable: it is stable whenever any Markovian policy could be.

Formalizing it. A live prior-art check (GET /theorems?q=proportional+scheduling) finds no relevant hits on the platform. This mission's genuine content is Proposition 12.26's reduction: rather than re-deriving an entropy-Lyapunov stability argument specific to RPS, it identifies the RPS fluid model precisely with mission IX's PF fluid model under an explicit correspondence, so that Theorem 12.28(a) is a direct instance of mission IX's own Theorem 10.5 and Theorem 12.28(b) a direct instance of this mission's own Theorem 12.27. This is the payoff the whole proportional-fairness apparatus (missions IX-X) was built for.

Difficulty

The central subtlety is that Theorem 12.24's departure-rate equation is stated in terms of a class-indexed process $\hat D_i(t)$, while the chapter's own general fluid-equation machinery (Theorem 12.13, mission XII) is built around an activity-indexed process — a distinction that matters when a packet network has more service types than classes. Under Sections 12.6-12.7's own fixed-routing model, however, the book's remark that "$s(\tau)$ ... is an I-vector of actual packet transfers by class" (page 245) collapses this distinction: each class has a single associated activity, so the activity-indexed and class-indexed views coincide, and the RPS fluid model can be built directly on the same class-indexed apparatus the PF fluid model (Section 10.4) already uses. Missing this identification is the natural way to get stuck restating Proposition 12.26 as a mere analogy rather than the literal equivalence the book states. A second difficulty is Lemma 12.23 itself: its proof cites Feller's strong law for bounded martingale-difference sequences as an external fact rather than deriving it, so a faithful statement must commit to an explicit representation of "martingale difference sequence" (a filtration and Mathlib's Martingale predicate) even though no full measure-theoretic construction of the underlying probability space is attempted.

Formalization scope

Classes and links are Fin-indexed; route : Fin I → Option (Fin I) records each class's deterministic routing successor (none meaning exit), and the resulting input-output matrix $R$ and routing matrix $P$ are derived from it rather than taken as independent data (this chunk verifies $R = I - P^\top$, the identity Proposition 12.26's reduction to the PF model relies on). The RPS optimization apparatus (psi, groupAggregate, the PF fluid-model predicate) is restated verbatim from mission IX, and the general packet-network fluid equations restated from mission XII, since concurrently-drafted chunks in this series never import one another's Lean files even within a shared sub-namespace. The formalization does not admit a trivializing reading: the load condition in Theorem 12.28 is a genuine strict inequality against the convex hull of feasible configurations (not weakened to $\le$ or to a single configuration), RPSFluidStable quantifies over every solution of the RPS fluid model (not a hand-picked one), and Proposition 12.26 is stated as a two-sided equivalence, not a one-directional inclusion that would understate "special case." Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.23's martingale strong law (Feller 1971, Theorem 3, Section VII.8) and Theorem 12.24's fluid-limit argument (mirroring mission XII's own Theorem 12.13 proof).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• N. S. Walton, "Concave switching in single and multihop networks," Queueing Systems 81 (2015), 265-299.
• F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33-37.
• W. Feller, An Introduction to Probability Theory and Its Applications, Volume II, 2nd edition, Wiley, 1971.

Motivation

Retailers of fashion and seasonal goods sell a fixed stock over a short season and routinely cut the price part-way through it. The markdown trades off two effects: a late discount keeps early, high-valuation customers paying the full price, while an early discount reaches customers whose interest in the product fades as the season goes on. Aviv and Pazgal (MSOM 2008) build a two-price model of this trade-off with Poisson arrivals and valuations that decline exponentially over the season, and compare sellers facing myopic customers, who buy as soon as the current price is acceptable, with sellers facing strategic customers, who may wait for the discount.

This mission formalizes the benchmark of that comparison in which the problem can be solved in closed form: myopic customers who all share the same base valuation, so that the only source of price discrimination is the decline of valuations over time. Proposition 4 of the paper identifies the optimal premium price, discount price and discount time, and the paper's Proposition 5 and Example 1 then measure how much strategic behaviour costs the seller against it.

Setting

The season is $[0, 1]$. Customers arrive as a Poisson process with rate $\lambda > 0$, so $\lambda$ is the expected number of arrivals in the season. Every customer has base valuation $1$, and a customer's valuation at time $t$ is $\rho^t$ for a fixed decline parameter $0 < \rho < 1$ (equivalently $e^{-\alpha t}$ with $\alpha = -\ln\rho$; $\rho$ is the fraction of the valuation left at the end of the season). In the paper's notation this is the case $c = 0$, $\mu = 1$, $H = 1$ of a family of Gamma-distributed base valuations with mean $\mu$ and coefficient of variation $c$; the tail of the base valuation is $\bar F(x) = 1$ for $x \le 1$ and $0$ otherwise.

The seller posts a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from the discount time $T \in [0, 1]$ on, and has unlimited inventory. A myopic customer arriving at $t < T$ buys at once iff $\rho^t \ge p_1$; otherwise the customer waits and buys at $T$ iff $\rho^T \ge p_2$. A customer arriving after $T$ buys iff the current valuation is at least $p_2$. The expected numbers of buyers in the three groups are the segment rates $\Lambda_I(p_1) = \lambda\int_0^T \bar F(p_1e^{\alpha t})\,dt$, $\Lambda_W(p_1, p_2) = \lambda\int_0^T[\bar F(\min\{p_1e^{\alpha t}, p_2e^{\alpha T}\}) - \bar F(p_1 e^{\alpha t})]\,dt$ and $\Lambda_L(p_2) = \lambda\int_T^1 \bar F(p_2 e^{\alpha t})\,dt$, and the expected revenue is

$$R_\rho(p_1, p_2; T) = p_1\,\Lambda_I(p_1) + p_2\,\big(\Lambda_W(p_1, p_2) + \Lambda_L(p_2)\big).$$

For a price $p \in [\rho, 1]$ let $\tau(p) = \ln p/\ln\rho$, the time at which the valuation has fallen to $p$, and write $\tau_1 = \tau(p_1)$, $\tau_2 = \tau(p_2)$. The reduced objective is

$$G(p_1, p_2) = (p_1 - p_2)\,\frac{\ln p_1}{\ln\rho} + p_2\,\frac{\ln p_2}{\ln\rho}, \qquad \rho \le p_2 \le p_1 \le 1 .$$

Formalization targets

Goal: Proposition 4 (p. 351)

$$\pi^*_{C/N} = \lambda\cdot\max_{\rho \le p_2 \le p_1 \le 1} G(p_1, p_2) = \max_{0 < p_2 \le p_1,\ 0 \le T \le 1} R_\rho(p_1, p_2; T),$$

every maximizer $(p_1^*, p_2^*)$ of $G$ together with every $T$ with $p_2^* \le \rho^T \le p_1^*$ attains $\pi^*_{C/N}$, and, if $\rho \le e^{-2+e^{-1}}$, the maximizer is unique,

$$p_1^* = e^{-1+e^{-1}}, \qquad p_2^* = p_1^*/e, \qquad \pi^*_{C/N} = -\frac{\lambda\, e^{-1+e^{-1}}}{\ln\rho},$$

and every $T$ with $\rho^T \in [e^{-2+e^{-1}}, e^{-1+e^{-1}}]$ is optimal.

Milestones (Proof of Proposition 4, p. 359)

For $\rho \le p_2 \le p_1 \le 1$:

1. $R_\rho(p_1, p_2; T) \le R_\rho(p_1, p_2; \tau_1)$ for $T \in [0, \tau_1]$;
2. $R_\rho(p_1, p_2; T) \le R_\rho(p_1, p_2; \tau_2)$ for $T \in [\tau_2, 1]$;
3. $R_\rho(p_1, p_2; T) = \lambda\, G(p_1, p_2)$ for $T \in [\tau_1, \tau_2]$;
4. for $\rho \le e^{-2+e^{-1}}$, $\max G = -e^{-1+e^{-1}}/\ln\rho$, attained only at $(e^{-1+e^{-1}}, e^{-2+e^{-1}})$.

Significance

Proposition 4 gives an explicit optimal markdown policy in a model where segmentation happens purely by arrival time: it shows that the discount time is not pinned down but can be placed anywhere in the interval in which the valuation lies between the two prices, and that for strongly declining valuations the optimal prices do not depend on $\rho$ at all. The paper uses it as the benchmark $\pi^*_{C/N}$ against which the strategic-customer equilibrium of Proposition 5 and the losses of Example 1 are measured.

The result is proved in the paper by a short argument; nothing in it has been machine-checked. A formal development makes the three observations of the proof precise (in particular, that prices outside $[\rho, 1]$ are dominated, which the paper leaves implicit) and supplies the omitted calculus for the special case.

Difficulty

The revenue is defined through integrals of a step function of time, and the reduction to $G$ needs these integrals evaluated in every configuration of $p_1$, $p_2$ and $T$, including prices above $1$ (nobody buys) and below $\rho$ (everyone buys, at a needlessly low price). The paper's proof covers only $\rho \le p_2 \le p_1 \le 1$ and asserts the domination of the remaining prices without argument. The special case is a constrained two-variable maximization of a function that is not jointly concave; the unconstrained critical point must be shown to be feasible exactly when $\rho \le e^{-2+e^{-1}}$, and boundary points of the region must be excluded.

Formalization scope

Everything is over $\mathbb R$. Logarithms are Real.log, powers $\rho^T$ are real powers, the segment rates are interval integrals ∫ t in a..b of the tail $\bar F(x) = \mathbf 1\{x \le 1\}$, and $\alpha = -\ln\rho$ with $H = 1$. The model definitions ($\Lambda_I$, $\Lambda_W$, $\Lambda_L$ and the revenue) are stated for a general tail $\bar F$, decline factor, season length and discount time and then specialized.

The following readings of the paper's words are fixed:

• "$c = 0$": every base valuation equals $\mu = 1$ (the degenerate end of the paper's Gamma family, outside §3's "continuous distribution").
• "$Q/\lambda \to \infty$": unlimited inventory; the truncated Poisson mean $N(q, \Lambda)$ is replaced by $\Lambda$. With unlimited inventory, choosing the contingent discount at time $T$ and choosing both prices in advance give the same optimum.
• Myopic waiting customers buy at $T$ iff their valuation at $T$ is at least $p_2$, as in $\Lambda_W$.
• "$T$ could be optimally selected": $T \in [0, 1]$ is a decision variable together with the prices, which range over all $0 < p_2 \le p_1$, not only over $[\rho, 1]$.
• "Maximize his expected revenues": IsGreatest of the set of attainable revenues.
• "Setting $T$ to any value within the range $p_2^* \le \rho^T \le p_1^*$", and "it would be optimal to select $T$ so that $\rho^T \in [e^{-2+e^{-1}}, e^{-1+e^{-1}}]$": every such $T$ is optimal; it is not claimed that no other $T$ is.
• "The prices $p_1^*$ and $p_2^*$ that solve the problem" in the special case: the maximizer of $G$ is unique.
• "Never optimal" in the first two observations: a weak inequality between revenues.

The decimals $0.196$ and $0.532$ are not stated. A formalization that restricted prices to $[\rho, 1]$ in the revenue maximization, or that fixed $T$ in advance, would assume half of what the proposition proves and is ruled out. Welcome contributions include general lemmas evaluating interval integrals of indicator functions of intervals, and the domination argument for prices outside $[\rho, 1]$.

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• N. Stokey, Intertemporal Price Discrimination, Quarterly Journal of Economics 93(3):355–371, 1979. https://doi.org/10.2307/1883163
• D. Besanko and W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555

Why shrink an uncertainty set

Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision $v$ and a parameter $x \in \mathbb{R}^m$ with objective $f(v, x)$ to be maximized, the robust problem around a nominal parameter $x_0$ with a deviation set $\Delta$ is

$$\max_{v} \min_{x_\delta \in \Delta} f(v, x_0 + x_\delta).$$

When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix $\alpha \in (0,1)$ and solve the same problem over the shrunken set $\alpha\Delta = \{\alpha x : x \in \Delta\}$. The heuristic is easy to implement, but the meaning of the set $\alpha\Delta$ is unclear, and it has lacked a justification.

Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.

Setting

Let $\mathbb{R}^m$ carry the Euclidean norm $\|\cdot\|_2$ and its Borel $\sigma$-algebra, and let $\mathcal P$ be the set of Borel probability measures on $\mathbb{R}^m$. Let $V$ be any set of decisions and $f : V \times \mathbb{R}^m \to \mathbb{R}$. Fix $x_0 \in \mathbb{R}^m$, a deviation set $\Delta \subseteq \mathbb{R}^m$, and $\alpha \in (0,1)$. Write $x_0 + \Delta = \{x_0 + x : x \in \Delta\}$.

The two-scenario set is

$$\hat{\mathcal P}' = \{\mu \in \mathcal P \mid \mu(\{x_0\}) \ge 1-\alpha,\ \mu(x_0 + \Delta) = 1\}.$$

A distribution in $\hat{\mathcal P}'$ describes a system that is, with probability at least $1-\alpha$, in a normal state where the parameter equals $x_0$, and otherwise in an abnormal state where the parameter deviates by an element of $\Delta$. The DRSP value of a decision $v$ is $\inf_{\mu \in \hat{\mathcal P}'} \int f(v, x)\, d\mu(x)$.

Two further quantities enter. The radius of the deviation set is $D = \max_{x \in \Delta} \|x\|_2$. The curvature bound is a constant $h \ge 0$ with

$$-hI \preceq H_v(x) \preceq hI \quad \text{for all } v, x,$$

where $H_v(x)$ is the Hessian of $f(v, \cdot)$ at $x$ and $\preceq$ is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.

Formalization targets

Goal: Theorem 4.1 (p. 104)

If $f(v,\cdot)$ is twice differentiable with $-hI \preceq H_v(x) \preceq hI$ for all $v, x$, then for all $v$

$$\inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) - \alpha D^2 h \;\le\; \min_{x_\delta \in \alpha\Delta} f(v, x_0 + x_\delta) \;\le\; \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) + \alpha D^2 h.$$

Milestones (the displays of the proof on p. 105)

1. The mean-value step $f(v, x_0 + x_1) = f(v, x_0) + g_v(x_0 + \beta x_1)x_1$ for some $\beta \in [0,1]$, where $g_v$ is the gradient of $f(v,\cdot)$.
2. The gradient bound $\|g_v(x_0 + \beta x_1) - g_v(x_0 + \alpha\beta' x_1)\| \le h\|\beta x_1 - \alpha\beta' x_1\| \le h\|x_1\| \le hD$, stated together with the general fact that the Hessian bound makes $g_v$ $h$-Lipschitz.
3. The pointwise sandwich: for $x_1 \in \Delta$, $f(v, x_0 + \alpha x_1)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha f(v, x_0 + x_1)$.
4. The min sandwich: $\min_{\alpha\Delta} f(v, x_0 + \cdot)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha \min_{\Delta} f(v, x_0 + \cdot)$.
5. The two-scenario value: $(1-\alpha) f(v, x_0) + \alpha \min_{x_\delta\in\Delta} f(v, x_0 + x_\delta) = \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x)$, which the paper derives from its Corollary 5.2 (p. 107).

Further results

Corollary 4.2 (p. 104): if every $f(v,\cdot)$ is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if $\Delta$ is star shaped, every $f(v,\cdot)$ is convex with $f(v, x_0) - \min_{\Delta} f(v, x_0 + \cdot) \ge 1$ and has Hessian bounded by $h$, then the shrunken value lies between the DRSP values over $\hat{\mathcal P}''$ and $\hat{\mathcal P}'$, where $\hat{\mathcal P}''$ requires only $\mu(\{x_0\}) \ge \max(0, 1-\alpha-\alpha D^2 h)$.

Significance

The result gives a physical meaning to the parameter $\alpha$ of the shrinkage heuristic: $1-\alpha$ is a lower bound on the probability that the system is in its nominal state. The error $\alpha D^2 h$ vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.

Difficulty

Two points need care. First, the step from the Hessian bound $-hI \preceq H_v \preceq hI$, a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of $x_0 + \Delta$.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m) with its Borel $\sigma$-algebra. Measures are Measures, and membership in $\hat{\mathcal P}'$ includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.

The formalization makes the following readings explicit:

1. $\Delta$ is compact. The page writes min over $\alpha\Delta$ and max over $\Delta$, which presuppose attainment. Compactness together with continuity of $f(v,\cdot)$ gives attainment, a finite $D$, finite integrals and measurability of $x_0 + \Delta$. The goal additionally states that the minimum over $\alpha\Delta$ is attained.
2. $0 \in \Delta$. Without it $\hat{\mathcal P}'$ is empty, since $\mu(\{x_0\}) \ge 1-\alpha > 0$ and $\mu(x_0+\Delta)=1$ force $x_0 \in x_0 + \Delta$. The page's two-scenario reading presupposes it. In Corollary 4.3 it follows from star-shapedness once $\Delta$ is nonempty, and nonemptiness is added there.
3. Twice differentiable with bounded Hessian means that $f(v,\cdot)$ and its derivative are differentiable everywhere and $|D^2 f(v,\cdot)(x)[y,y]| \le h\|y\|_2^2$ for all $x, y$. The constant $h$ is one constant for all $v$.
4. The minima over $\Delta$ and $\alpha\Delta$ are written as infima, which equal the minima under the hypotheses above.

The Lean functions drspValue and devRadius return $0$ on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped $0 \in \Delta$ would make the inequalities hold or fail for the wrong reason and is ruled out.

Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, S. Mannor, Percentile Optimization for Markov Decision Processes with Parameter Uncertainty, Operations Research 58(1):203–213, 2010. https://doi.org/10.1287/opre.1080.0685
• E. Delage, Y. Ye, Distributionally Robust Optimization under Moment Uncertainty with Applications to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• D. Bertsimas, D. B. Brown, C. Caramanis, Theory and Applications of Robust Optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510

Motivation

Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).

In data-driven problems the situation is different: the parameters $x_1,\dots,x_n$ are samples, and all of them lie in the same space $\mathbb R^m$. Robustifying each sample by its own uncertainty set $\mathcal Z_i$ gives the objective $\sum_i c_i\inf_{x_i\in\mathcal Z_i}f(x_i)$, and the sets $\mathcal Z_i$ typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on $\mathbb R^m$ itself rather than on $\mathbb R^{m\times n}$. This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.

Setting

Let $m,n\ge1$ and write $[1:n]=\{1,\dots,n\}$. Let $\mathcal P$ be the set of Borel probability measures on $\mathbb R^m$. The data are:

• a measurable utility $f:\mathbb R^m\to\mathbb R$ (the decision variable is suppressed);
• weights $c_1,\dots,c_n>0$ with $\sum_{i=1}^n c_i=1$;
• nonempty Borel uncertainty sets $\mathcal Z_1,\dots,\mathcal Z_n\subseteq\mathbb R^m$, which may intersect or coincide.

For $S\subseteq[1:n]$ write $\mathcal Z_S=\bigcup_{i\in S}\mathcal Z_i$ and $N=[1:n]$. The distribution set is

$$\mathcal P_n=\Big\{\mu\in\mathcal P\ \Big|\ \forall S\subseteq[1:n]:\ \mu(\mathcal Z_S)\ge\sum_{i\in S}c_i\Big\}.$$

Each $\mu\in\mathcal P_n$ must give every union of uncertainty sets at least the total weight of its indices. For $\mu\in\mathcal P$ the expectation $\int f\,d\mu$ is the extended integral $\int f^+d\mu-\int f^-d\mu\in[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 2.1 (Eq. (4), pp. 96–97)

$$\sum_{i=1}^n\Big[c_i\inf_{x_i\in\mathcal Z_i}f(x_i)\Big]=\inf_{\mu\in\mathcal P_n}\int_{\mathbb R^m}f(x)\,d\mu(x),$$

as an identity in $[-\infty,+\infty]$, with no boundedness assumption on $f$ and no disjointness assumption on the $\mathcal Z_i$.

Milestones (proof of Theorem 2.1, p. 97)

1. Every $\mu\in\mathcal P_n$ satisfies $\mu(\mathbb R^m\setminus\mathcal Z_N)=0$, hence $\int_{\mathbb R^m}f\,d\mu=\int_{\mathcal Z_N}f\,d\mu$.
2. Weak duality. With $f_i=\inf_{\mathcal Z_i}f$ finite, every $\alpha\in\mathbb R^{2^n}$ satisfying $\sum_S\alpha_S\mathbf 1(x\in\mathcal Z_S)\le f(x)$ on $\mathcal Z_N$ and $\alpha_S\ge0$ for $S\ne N$ obeys $\sum_i c_i\sum_S\alpha_S\mathbf 1(i\in S)\le\sum_i c_if_i$.
3. The nested dual solution. If $f_1\ge\dots\ge f_n$, the vector with $\alpha_{\{1,\dots,i\}}=f_i-f_{i+1}$, $\alpha_N=f_n$ and all other coordinates $0$ is feasible and has objective $\sum_i c_if_i$.

Further statements

• For pairwise disjoint $\mathcal Z_i$: $\mathcal P_n=\{\mu\in\mathcal P\mid\mu(\mathcal Z_i)=c_i,\ i=1,\dots,n\}$ (p. 97).
• Corollary 2.1 (Eq. (5)): $\inf_{x'\in\mathcal Z}f(x')=\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z)=1}\int f\,d\mu$.
• Corollary 5.2 (nested distributions, p. 107): for $\mathcal Z_1\subseteq\dots\subseteq\mathcal Z_n$ and $0=p_0<p_1<\dots<p_n=1$,

$$\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z_i)\ge p_i\ \forall i}\int f\,d\mu=\sum_{i=1}^n(p_i-p_{i-1})\inf_{x_i\in\mathcal Z_i}f(x_i).$$

Significance

The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space $\mathbb R^m$. This is what allows distributions in $\mathcal P_n$ to be compared with the true data-generating distribution as $n$ grows: in §3 of the paper a kernel density estimator is shown to lie in $\mathcal P_n$ for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.

Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.

Difficulty

The inequality $\ge$ from the left side is the easy half: point masses $\sum_ic_i\delta_{x_i}$ with $x_i\in\mathcal Z_i$ belong to $\mathcal P_n$. The substance is the reverse bound, that no $\mu\in\mathcal P_n$ can do better than $\sum_ic_if_i$. For disjoint sets this is immediate, since $\mu(\mathcal Z_i)=c_i$. For overlapping sets a measure may place mass in intersections, and a single point of $\mathcal Z_i\cap\mathcal Z_j$ can serve several indices at once; the constraint family over all $2^n$ subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded $\mathcal Z_i$, infinite integrals, infima equal to $-\infty$) must also be handled rather than assumed away.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ with its Borel $\sigma$-algebra; no norm is used. Indices $1,\dots,n$ are Fin n, subsets are Finset (Fin n), and $\{1,\dots,i\}$ is Finset.Iic i.
• $\mathcal P_n$ is a Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, $\emptyset$ and $[1:n]$ included.
• $\int f\,d\mu$ is expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, $\int f^+-\int f^-$. The Bochner integral is not used, because its value $0$ on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set $\mathcal Z_i$.
• Readings of the printed statements. (i) The paper allows $f$ to take the value $-\infty$; here $f$ is real-valued. The excluded case is the one the proof disposes of in its first sentence, where both sides are $-\infty$. (ii) No boundedness hypothesis is added: when some $\inf_{\mathcal Z_i}f=-\infty$ both sides are $-\infty$, and otherwise every $\mu\in\mathcal P_n$ has a finite negative part. (iii) Corollary 2.1 prints "$f:\mathbb R\cup\{-\infty\}$" without a domain; it is read as $f:\mathbb R^m\to\mathbb R$. (iv) Corollary 5.2 is corrected: the paper prints the coefficient $(p_n-p_{n-1})$, while its proof sets $c_i=p_i-p_{i-1}$; the printed version is false (for $\mathcal Z_1=\{a\}\subseteq\mathcal Z_2=\{a,b\}$, $f(a)=1$, $f(b)=0$, $p_1=1/4$, the left side is $1/4$ and the printed right side $3/4$). The mission states $(p_i-p_{i-1})$. (v) The standing hypotheses of Theorem 2.1 ($f$ measurable, $\mathcal Z_i$ nonempty Borel) are made explicit in Corollary 5.2.
• The ordering $f_1\ge\dots\ge f_n$ is a hypothesis of the nested-dual milestone only, as the proof's "without loss of generality"; the goal does not assume it. Milestones 2 and 3 assume $f$ bounded below on each $\mathcal Z_i$ (the proof's first reduction), so that $f_i$ is a real number.
• Ruled out. A Bochner-integral formulation, a restriction to disjoint sets, a distribution set containing non-probability measures, or a set $\mathcal P_n$ defined by the singleton constraints $\mu(\mathcal Z_i)\ge c_i$ alone would each change or trivialise the theorem; none is used.
• Definitions (file Model): the set $\mathcal P_n$, the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

Motivation

Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.

Setting

A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator $W(z) := AM(I-P')^{-1}z$ (Eq. 8.24) gives, for any buffer-contents vector $z$, the total service effort each pool would need to drain $z$ to emptiness with no further arrivals; the load vector of the standard load condition is $\rho = W(\lambda)$ (Eq. 8.25), and the total arrival rate vector $\alpha$ (including internally routed traffic) is the unique solution of the traffic equations $\alpha = \lambda + P'\alpha$. A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions $\gamma_i := \alpha_i m_i/\rho_{p(i)}$ (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.

Formalization targets

Goal: Theorem 8.18 — HLSPS control is stable under the standard load condition

For any queueing network under HLSPS control with proportion vector $\gamma$, if

$$\rho < b \qquad (\text{the standard load condition, Eq. 5.1}),$$

the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.

Supporting milestones

Lemma 8.15 isolates the workload derivative identity $\dot W_k(Z(t)) = \rho_k - b_k$ at a busy station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma 8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct structural engine behind the goal theorem: a uniform excess departure rate over the total arrival rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.

Significance

The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.

Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network, q=workload) return no relevant results (per triage.json); this mission is a from-scratch formalization of feedforward networks, the workload operator, HLSPS control, and their stability theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.

Difficulty

Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights $\delta_k$, chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function $H(z) = \max_k \delta_k W_k(z)$ is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.

Formalization scope

Mission IV's queueing-network model data and fluid-equation specialization are restated locally (drafts in this series do not import one another). The workload operator's matrix inverse $(I-P')^{-1}$ is supplied as external data with its defining two-sided-inverse property, rather than derived from substochasticity/transience hypotheses on $P$ (Chapter 2 material, out of series scope) — the same convention mission III used for its process-family apparatus. The non-idling and HLSPS fluid models are each packaged as their own predicate plus a Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the non-idling stability object (not a separately restated "FCFS fluid model") since the book's own remark identifies the two exactly for generalized Jackson networks. A formalization that stated Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's actual proof architecture (see Difficulty); this mission keeps them as independent milestones/ goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range but absent from the planning brief's disposition table, is added as a milestone rather than silently dropped, since it is the structural step the goal theorem's own proof cites by name. QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model predicates are the primary reusable contributions; contributions completing the five by sorry proofs are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
• M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.

Motivation

Comparing uncertain outcomes is the basic problem of decision making under risk. Second-degree stochastic dominance (SSD) is the comparison that every risk-averse decision maker who prefers larger outcomes agrees with: $X$ dominates $Y$ in this sense exactly when $\mathbb E\,U(X)\ge\mathbb E\,U(Y)$ for every nondecreasing concave utility $U$ for which the expectations are finite. The relation grew out of majorization theory for finite distributions (Hardy, Littlewood and Pólya) and was extended to general distributions by Rothschild and Stiglitz and by Hadar and Russell around 1970; it is the standard consistency requirement for portfolio models and for risk measures in operations research and finance.

SSD is defined through the distribution function, which is awkward in optimization: portfolio returns are linear in the decision variables, but their distribution functions are not. Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) showed that SSD has an equivalent dual description through the integrated quantile function, the absolute Lorenz curve, and that the two descriptions are related by Fenchel conjugation. That dual description underlies the later theory of SSD-constrained optimization (Dentcheva and Ruszczyński, SIAM J. Optim. 14 (2003)) and the use of conditional value-at-risk as an SSD-consistent risk measure.

Setting

Fix a probability space $(\Omega,\mathcal B,\mathbb P)$ and real random variables $X,Y:\Omega\to\mathbb R$ with $\mathbb E|X|<\infty$, $\mathbb E|Y|<\infty$.

• The distribution function is $F_X(\eta)=\mathbb P\{X\le\eta\}$ (Lean: distFun P X).
• The second performance function is the area below it, $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi$ (secondPerformance P X, eq. (2.1)).
• SSD: $X\succeq_{SSD}Y$ iff $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for every $\eta\in\mathbb R$ (SSD P X Y, eq. (2.2)). The dominating variable has the smaller curve.
• The first quantile function is the left-continuous inverse $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$, $0<p\le1$ (leftQuantile P X). A number $q$ is a $p$-quantile if $\mathbb P\{X<q\}\le p\le\mathbb P\{X\le q\}$ (IsPQuantile P X p q).
• The second quantile function (absolute Lorenz curve) $F_X^{(-2)}:\mathbb R\to\overline{\mathbb R}$ is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ for $0\le p\le1$ and $+\infty$ otherwise (secondQuantile P X, eq. (3.2)).
• The convex conjugate of $F:\mathbb R\to\overline{\mathbb R}$ is $F^*(p)=\sup_\xi\{p\xi-F(\xi)\}$ (conj F), and $\partial f(\eta)$ is the subdifferential of a real function $f$ at $\eta$ (subdiff f η).

Formalization targets

Goal: Theorem 3.2

$$X\succeq_{SSD}Y\iff F_X^{(-2)}(p)\ge F_Y^{(-2)}(p)\quad\text{for all }0\le p\le1.$$

Both directions are required, and the range of $p$ includes both endpoints (at $p=1$ the right-hand side contains $\mathbb EX\ge\mathbb EY$).

Milestones, in the order the argument uses them

1. (2.4): $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}(\eta-\xi)\,P_X(d\xi)=\mathbb E\max(\eta-X,0)$.
2. §2, p. 62: $F_X^{(2)}$ is continuous, convex, nonnegative and nondecreasing.
3. §3, p. 64: for $p\in(0,1)$ the $p$-quantiles form a closed interval with left end $F_X^{(-1)}(p)$.
4. (3.3): $\partial F_X^{(2)}(\eta)=[\mathbb P\{X<\eta\},\mathbb P\{X\le\eta\}]$ for every $\eta$.
5. Theorem 3.1(i): $F_X^{(-2)}=[F_X^{(2)}]^*$ on all of $\mathbb R$.
6. Theorem 3.1(ii): $F_X^{(2)}=[F_X^{(-2)}]^*$ on all of $\mathbb R$.

A companion item, Corollary 3.3, states the four equivalent characterizations of a $p$-quantile (quantile condition, attainment in either conjugate, and the Fenchel–Young equality $F_X^{(-2)}(p)+F_X^{(2)}(\eta)=p\eta$).

Significance

Theorem 3.2 converts a condition on distribution functions into a condition on integrated quantiles. Its consequences in the paper include the SSD consistency of the mean–risk models built on tail means (conditional value-at-risk), on the Gini mean difference and on the mean absolute deviation from a quantile, and the linear-programming representations of those models for finitely many scenarios; the companion mission Dual Stochastic Dominance and Related Mean-Risk Models 2 builds on the same objects. Theorem 3.1 is the precise statement that $F_X^{(2)}$ and $F_X^{(-2)}$ form a conjugate pair; Corollary 3.3 identifies the subgradients of each with the quantiles of $X$.

All results here are proved in the paper, and the quantile characterization of the increasing concave order also appears in the stochastic-orders literature. None of them is formalized: Mathlib at the pinned revision has ProbabilityTheory.cdf but no convex conjugate on the extended reals, no subdifferential of a real function, no quantile function and no stochastic dominance. The mission produces a machine-checked account of the quantile side of SSD, with the conjugacy stated exactly, including the value $+\infty$ off $[0,1]$.

Difficulty

The naive route to Theorem 3.2 compares $F_X^{(2)}$ and $F_Y^{(2)}$ through the quantile functions directly, but the first quantiles $F^{(-1)}$ need not be ordered when $X\succeq_{SSD}Y$ (the paper notes this on p. 65), so no pointwise argument on quantiles works. The equivalence rests on Theorem 3.1, and there the hard part is computing the conjugate of $F_X^{(2)}$ for a general distribution: atoms of $X$ make $F_X^{(2)}$ nondifferentiable and flat pieces of $F_X$ make the maximizer non-unique, so the subdifferential (3.3) and the interval of $p$-quantiles must be handled as sets, and the endpoints $p=0,1$ (where the supremum need not be attained) and $p\notin[0,1]$ (where it is $+\infty$) must be treated separately. Part (ii) is a biconjugation statement for a closed convex function, whose general form is not in Mathlib.

Formalization scope

• One probability space (Ω, P) with [IsProbabilityMeasure P] carries both $X$ and $Y$; nothing depends on anything but the laws, and no independence is assumed.
• $F_X(\eta)$ is P.real {ω | X ω ≤ η}; $F_X^{(2)}$ is a Bochner integral over Set.Iic η; $F_X^{(-2)}$ is an interval integral over $(0,p]$, placed in EReal, with ⊤ off $[0,1]$.
• The conjugate is ⨆ ξ, ((p * ξ : ℝ) : EReal) - F ξ in the complete lattice EReal, so terms where $F=+\infty$ contribute $-\infty$, exactly the paper's convention.
• Standing assumption. Every item using $F^{(2)}$ or $F^{(-2)}$ assumes Integrable X P (and Integrable Y P in the goal). This is the paper's own hypothesis $\mathbb E|X|<\infty$ (p. 65, and the hypothesis of Theorem 3.1), not a repair. The $p$-quantile milestone assumes only AEMeasurable X P.
• Quantile at $p=1$. $F_X^{(-1)}$ is a real sInf. It is the true infimum for $0<p<1$; at $p=1$ the paper's value can be $+\infty$ while sInf ∅ = 0. This one point does not affect (3.2), and no item states anything about $F_X^{(-1)}(1)$.
• Omitted. The conditional-expectation form $\mathbb P\{X\le\eta\}\,\mathbb E\{\eta-X\mid X\le\eta\}$ in (2.4) is not stated, since it is undefined when $\mathbb P\{X\le\eta\}=0$.
• Trivializing encodings are ruled out. $F^{(2)}$ is defined by (2.1), not as $\mathbb E\max(\eta-X,0)$, and $F^{(-2)}$ by (3.2), not as a conjugate; either shortcut would make a milestone or Theorem 3.1 true by definition.
• Infrastructure and reuse. Welcome contributions: the extended-real conjugate and Fenchel–Young inequality on $\mathbb R$, biconjugation of closed convex functions of one variable, subdifferentials of integrals of monotone functions, and the basic theory of left quantiles (the quantile transform $F_X^{(-1)}(U)\sim X$). These are reusable beyond this mission, in particular by mission 2 of this series and by any formalization of conditional value-at-risk. The platform's VectorSpaceOpt.fenchel_biconjugate_on and ConvexOptimization.fenchelConjugate concern real-valued conjugates on other spaces and are related but not reused.

Selected references

• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 12.2 and 23.5 are used in the paper's proofs). https://doi.org/10.1515/9781400873173
• M. Rothschild, J. E. Stiglitz, Increasing risk: I. A definition, J. Econom. Theory 2 (1970) 225–243. https://doi.org/10.1016/0022-0531(70)90038-4
• J. Hadar, W. R. Russell, Rules for ordering uncertain prospects, Amer. Econom. Rev. 59 (1969) 25–34. https://www.jstor.org/stable/1811090
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14(2) (2003) 548–566. https://doi.org/10.1137/S1052623402420528
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5