Probability

Motivation

Reflected Brownian motion on the orthant is the diffusion that arises as the heavy-traffic limit of open networks of queues. In a $K$-station network the scaled queue-length vector lives in the nonnegative orthant $\mathbb R^K_+$; in the interior it moves like a Brownian motion, and when a station empties the process is pushed back into the orthant in a direction determined by the routing of customers between stations. Harrison (1978) obtained such a limit for two queues in tandem, and Reiman (Open Queueing Networks in Heavy Traffic, Math. Oper. Res. 9 (1984)) showed that general $K$-station open networks lead exactly to the class of processes studied here.

Classical constructions of reflected diffusions (Stroock and Varadhan 1971, Watanabe 1971) require a smooth boundary and a reflection direction varying continuously on it. The orthant has corners and the reflection direction jumps between faces, so those results do not apply. Harrison and Reiman (Reflected Brownian Motion on an Orthant, Ann. Probab. 9 (1981)) construct the process pathwise, following Skorokhod's one-dimensional approach, and derive its Markov property from the construction. The process has since become the standard object in the diffusion approximation of queueing networks.

Setting

Fix a positive integer $K$. Vectors in $\mathbb R^K$ are row vectors, indexed by $j=1,\dots,K$. Let $A$ be a $K\times K$ covariance matrix (symmetric, nonnegative definite), $b\in\mathbb R^K$ a drift vector, and $Q=(q_{ij})$ a nonnegative $K\times K$ matrix with zeros on the diagonal and spectral radius strictly less than one. $S=\mathbb R^K_+$ is the nonnegative orthant.

Let $C$ be the space of continuous paths $x:[0,\infty)\to\mathbb R^K$ with the topology of uniform convergence on compact intervals, and $C_S$ the paths with $x(0)\in S$. For $x\in C_S$, the Skorokhod problem asks for $y,z\in C$ with, for every $j$,

$$z_j(t)=x_j(t)+y_j(t)-\sum_{i=1}^K q_{ij}\,y_i(t),\qquad z_j(t)\ge 0,\qquad t\ge0, \tag{5–6}$$

$y_j$ nondecreasing with $y_j(0)=0$ (7), and $y_j$ increasing only at times $t$ where $z_j(t)=0$ (8). In matrix form, $z=x+y(I-Q)$. Theorem 1 of the paper shows there is exactly one such pair, written $y=\psi(x)$, $z=\phi(x)$.

The process is obtained by feeding a Brownian path into this map. On a probability space $(\Omega,\mathcal F,P)$ let $X$ be a $K$-dimensional Brownian motion with covariance matrix $A$, drift $b$ and $X(0)\in S$ almost surely, with $X(0)$ independent of the increments of $X$. Let $\mathcal F_t=\mathcal F(X(s);0\le s\le t)$. Set $Y=\psi(X)$ and $Z=\phi(X)$ where $X\in C_S$, and $Y=Z=0$ on the exceptional null set. $Z$ is reflected Brownian motion on $S$ with reflection matrix $I-Q$.

Formalization targets

Goal: Corollary 1

There is a family $(\kappa_t)$ of Markov transition kernels on $\mathbb R^K$, depending only on $(Q,A,b)$, such that for every such $X$, $Y$, $Z$:

$$\text{(a)}\quad Y(t),\ Z(t)\ \text{are } \mathcal F_t\text{-measurable},\ t\ge0;$$ $$\text{(b)}\quad (Y,Z)\ \text{satisfies (1)–(4) a.s., and any pair satisfying (1)–(4) a.s. equals } (Y,Z) \text{ a.s.};$$ $$\text{(c)}\quad P\big[Z(s+t)\in B \mid \mathcal F_s\big]=\kappa_t\big(Z(s),B\big)\ \text{a.s.},\qquad s,t\ge0,\ B \text{ Borel}.$$

Here (1)–(4) are (5)–(8) for the paths of $X$, $Y$, $Z$. The kernel is chosen before the probability space and the initial law, which is what "stationary transition probabilities" means.

Milestones

The milestones follow the proof of Theorem 1 on pp. 304–305:

1. a positive diagonal $\Lambda$ with $\|\Lambda^{-1}Q\Lambda\|<1$ (Veinott scaling);
2. (5)–(8) are invariant under $(Q,x,y,z)\mapsto(\Lambda^{-1}Q\Lambda,x\Lambda,y\Lambda,z\Lambda)$;
3. the key observation that (5)–(8) are equivalent to $y\in C_0$, the fixed-point equation $y=\pi(y)$ with $\pi(y)(t)=\sup_{0\le s\le t}[y(s)Q-x(s)]^+$, and $z=x+y(I-Q)$;
4. the contraction $\|\pi(y)-\pi(y')\|\le\alpha\|y-y'\|$ on $[0,T]$;
5. convergence of the Picard iterates $y^{n+1}=\pi(y^n)$, $y^0\equiv0$;
6. the Lipschitz bound $\|\psi(x)-\psi(x')\|\le\|x-x'\|/(1-\alpha)$;
7. Theorem 1 itself: existence and uniqueness, non-anticipation (9), continuity (10);
8. the regeneration property (11): with $x^*(t)=z(T)+x(T+t)-x(T)$, $y^*(t)=y(T+t)-y(T)$, $z^*(t)=z(T+t)$, one has $y^*=\psi(x^*)$, $z^*=\phi(x^*)$.

Milestone 7 is the platform theorem Reiman84.QueueLength.lemma_1, posed as an open target by an earlier mission (Reiman 1984 cites it as its Lemma 1). It is referenced here and not posed again.

Significance

Corollary 1 is what makes $Z$ a usable stochastic process: adaptedness and almost-sure uniqueness say $Z$ is determined by the driving Brownian motion in a non-anticipating way, and the Markov property with time-homogeneous kernels is the starting point for the change-of-variable formula of §3, for generators, for stationary distributions, and for the heavy-traffic limit theorems in which $Z$ appears as the limit. The pathwise map $\phi$ and its Lipschitz continuity are reused throughout queueing theory: the continuous-mapping argument for heavy-traffic limits rests on exactly the continuity (10) established here.

The results are classical, with complete published proofs. None of them has a machine-checked proof. Mathlib has the measure-theoretic layer (kernels, conditional expectation, independence) but no reflection maps, no construction of multidimensional Brownian motion with drift, and no Markov-process theory in continuous time. This mission provides a formal statement of the pathwise reflection theory and its probabilistic consequence on which such a development can build.

Difficulty

The pathwise part is a contraction argument, but the contraction is not in the original norm: the map $y\mapsto yQ$ need not be a contraction for any standard norm when only the spectral radius of $Q$ is below one. The proof first changes coordinates by a positive diagonal matrix, and the right norm must be matched to the row-vector convention. The fixed-point characterization also has to be shown equivalent to the complementarity condition (8), which is where the zero diagonal of $Q$ enters.

For Corollary 1, the difficulty is measure-theoretic. Adaptedness requires measurability of a path functional with respect to the uncompleted natural filtration, which uses (9) and (10) and the fact that continuous paths are determined by countably many coordinates. The Markov property requires the regeneration identity (11) together with independence of the post-$s$ increments of $X$ from $\mathcal F_s$, and a kernel that is jointly measurable and independent of the initial law. Conditioning on $\mathcal F_s$ alone, without identifying the future as a fixed functional of $Z(s)$ and an independent Brownian motion, does not give a kernel that is the same for all $s$.

Formalization scope

• $\mathbb R^K$ is Fin K → ℝ (paper index $j$ = Lean index $j-1$), with $K\ge1$; row vector times matrix is Matrix.vecMul. Paths are functions ℝ → Fin K → ℝ; only times $t\ge0$ are constrained.
• Spectral radius $<1$ is rendered as $Q^m\to0$, the rendering of Reiman84.QueueLength.lemma_1. $A$ is PosSemidef.
• (5)–(8) are the published Reiman84.QueueLength.IsReflectionPair; (8) reads "$y_j$ is constant on every interval $[s,t]\subseteq[0,\infty)$ on which $z_j>0$". $C_S$ is IsCPlus; uniform convergence on compacts is UocTendsto; Brownian motion from $0$ with drift and covariance is IsDriftedBM.
• The norm on $C[0,T]$ is $\sup_{0\le t\le T}\|y(t)\|_\infty$. The suprema in $\pi$ and in the norm are real suprema, honest only for continuous paths, and every statement using them assumes continuity.
• The paper's $\|P\|$ is printed as the maximal row sum. Under the row-vector convention the contraction, Picard and Lipschitz steps need the maximal column sum; with the printed reading the contraction inequality is false (a nilpotent $3\times3$ counterexample is recorded in those items). Veinott scaling is stated as printed; applying it to $Q^\top$ gives the column version.
• The Brownian motion is $X=X_0+\xi$ with $\xi$ a drifted Brownian motion from $0$ and $X_0\ge0$ a.s. independent of the whole process $\xi$. $\mathcal F_t$ is the uncompleted σ-algebra generated by $X(s)$, $0\le s\le t$.
• $Y$ and $Z$ enter Corollary 1 as hypotheses: a solution of (5)–(8) on $\{X\in C_S\}$, zero elsewhere. That such processes exist is the existence part of Theorem 1, the referenced open item.
• The kernel family is quantified before the probability space, so it cannot depend on $s$, on $\Omega$ or on the law of $X(0)$. A version of (c) with a kernel depending on these, with the completed or full σ-algebra in place of $\mathcal F_s$, or with one-dimensional marginals only, is a different and weaker statement and is ruled out.

Out of scope: Theorem 2 (the change-of-variable formula, which needs stochastic integration), the necessity of spectral radius $<1$, and §§3–4. Useful contributions beyond the milestones include a construction of multidimensional Brownian motion with drift in Mathlib, the Skorokhod map as a function on $C_S$, and general lemmas on measurability of continuous path functionals.

Selected references

• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9(2), 302–308, 1981. https://doi.org/10.1214/aop/1176994471
• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3), 441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• A. F. Veinott, Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Annals of Mathematical Statistics 40(5), 1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• A. V. Skorokhod, Stochastic Equations for Diffusion Processes in a Bounded Region, Theory of Probability and Its Applications 6(3), 264–274, 1961. https://doi.org/10.1137/1106035
• D. W. Stroock and S. R. S. Varadhan, Diffusion Processes with Boundary Conditions, Communications on Pure and Applied Mathematics 24, 147–225, 1971. https://doi.org/10.1002/cpa.3160240206

Motivation

A firm that will receive or deliver a quantity of a commodity, currency or security at a future date carries price risk until that date. When the asset itself cannot be traded in the meantime, the standard instrument for reducing that risk is a futures contract on a correlated asset: the firm takes a position in futures and adjusts it over time, and the gains or losses of the futures position offset part of the movement of its commitment. Choosing that position is the hedging problem. The classical answer, the minimum-variance hedge ratio, is a static one-period rule. Duffie and Richardson (Ann. Appl. Probab. 1991) solved the dynamic version in continuous time with a quadratic criterion: minimize the expected squared deviation of terminal wealth from a target. Their explicit feedback solution became a reference point for the later literature on mean-variance hedging in incomplete markets (Schweizer, Gouriéroux–Laurent–Pham, and others), where the same quadratic criterion is studied under general semimartingale prices.

Setting

Fix a horizon $T>0$ and a probability space $(\Omega,\mathcal F,P)$ carrying a two-dimensional standard Brownian motion $(B,\varepsilon)$ with its filtration $\mathbb F$. Let $\mu,\sigma,m,v,\rho$ be bounded measurable functions on $[0,T]$, with $|v|$ bounded away from zero and $\rho_t\in[-1,1]$. The Brownian motion $\xi_t=\int_0^t\rho_s\,dB_s+\int_0^t\sqrt{1-\rho_s^2}\,d\varepsilon_s$ has instantaneous correlation $\rho$ with $B$. The committed asset $S$ and the futures price $F$ follow

$$dS_t=\mu_tS_t\,dt+\sigma_tS_t\,dB_t,\qquad dF_t=m_tF_t\,dt+v_tF_t\,d\xi_t,\qquad S_0,F_0>0.$$

The hedger is committed to $k$ units of $S$ at time $T$. A trading strategy is a progressively measurable process $\theta$ (the futures position) with $E\int_0^T\theta_t^2F_t^2\,dt<\infty$; $\Theta$ denotes the set of them. Its futures gain is the stochastic integral $G(\theta)_t=\int_0^t\theta_s\,dF_s$, and the terminal wealth is $W(\theta)=kS_T+G(\theta)_T$. Given a target level $L\in\mathbb R$, problem (3) is

$$\min_{\theta\in\Theta}E\big[(W(\theta)-L)^2\big].$$

With $\gamma_t=m_t\sigma_t\rho_t/v_t-\mu_t$, the tracking process is $Z_t=k\exp(-\int_t^T\gamma_s\,ds)S_t$, so that $Z_T=kS_T$, and the feedback map is

$$\Phi(G^*_t)=\frac1{F_t}\Big[\frac{m_t}{v_t^2}(L-Z_t-G^*_t)-\frac{\sigma_t\rho_t}{v_t}Z_t\Big],$$

where $G^*$ solves $dG^*_t=\Phi(G^*_t)\,dF_t$, $G^*_0=0$. The strategy $\varphi=\Phi(G^*)$ depends only on the gains realized so far and the current price $S_t$.

Formalization targets

Goal: Proposition 1

$$\varphi_t=\Phi(G^*_t)\ \text{ solves }\ \min_{\theta\in\Theta}E\big[(kS_T+G(\theta)_T-L)^2\big]$$

for every commitment $k$, every target $L$ and every solution $G^*$ of (10). No constant is hard-coded: the statement is the paper's for arbitrary coefficients satisfying the standing hypotheses.

Milestones

1. Lemma 1: $\varphi\in\Theta$ is optimal iff $E[(L-kS_T-G(\varphi)_T)\,G(\theta)_T]=0$ for every $\theta\in\Theta$.
2. Existence (§3.3): equation (10) has a solution with $G^*_t\in L^2(P)$.
3. Itô dynamics of $Z$: $dZ_t=(\gamma_t+\mu_t)Z_t\,dt+\sigma_tZ_t\,dB_t$.
4. Moment equations for $E(Z_tG_t)$, $E(G^*_tG_t)$ and $E(G_t)$, with $G=G(\theta)$.
5. Lemma 2: $H_t=E[(L-Z_t-G^*_t)G(\theta)_t]$ satisfies $\dot H_t=-(m_t^2/v_t^2)H_t$.
6. The solution of (13): $H_t=H_0\exp(-\int_0^tm_s^2/v_s^2\,ds)$.

Two further items, not milestones, formalize §4: Lemma 3 (a solution of (3) is mean-variance efficient) and §4.1 (maximizing the quadratic utility $E[W-cW^2]$, $c>0$, is problem (3) with $L=1/(2c)$).

Significance

Proposition 1 gives the optimal dynamic hedge in closed feedback form for every target level at once. Varying $L$ traces out the whole mean-variance frontier of terminal wealth (Lemma 3), and the choice $L=1/(2c)$ solves the quadratic-utility problem (§4.1); the minimum-variance hedge of §4.3 of the paper is obtained by optimizing over $L$. The result is also an instance of a general pattern: a quadratic hedging problem in an incomplete market reduces to an $L^2$ projection onto the space of attainable gains, and the projection is computed by a linear SDE.

The result is proved in the paper, in six pages. No machine-checked version of it, or of any continuous-time hedging result, exists on the platform. A formalization requires Itô's formula for products of Itô processes, the zero-mean property of square-integrable stochastic integrals, Fubini's theorem for moments, and existence for a linear SDE with an Itô-process forcing term; each of these is reusable well beyond this paper.

Difficulty

The projection step (Lemma 1) is Hilbert-space geometry and the final ODE step is Grönwall. The difficulty lies in between: the orthogonality $E[(L-kS_T-G^*_T)G(\theta)_T]=0$ must be verified against every trading strategy $\theta$, about which only $E\int_0^T\theta_t^2F_t^2\,dt<\infty$ is known. A computation that treats $\theta$ as bounded, continuous or simple does not suffice. Making the paper's moment computations rigorous requires controlling the integrability of products such as $Z_t\theta_tF_t$ and $G^*_tG(\theta)_t$, proving that the stochastic-integral parts of Itô's product rule are true martingales rather than local martingales, and differentiating expectations in time when the coefficients are only measurable, so that derivatives exist only almost everywhere.

Formalization scope

The stochastic layer is the published definition file Peng1990_SMP_Stochastic (the $L^2$ Itô integral and Itô processes on $\mathbb R_{\ge0}$ time), imported, not redefined. The mission commits to the following conventions.

• $(B,\varepsilon)$ is one $\mathbb R^2$-valued standard Brownian motion; $B$ is coordinate 0, $\varepsilon$ coordinate 1, and $d\xi$ is expanded as $\rho\,dB+\sqrt{1-\rho^2}\,d\varepsilon$.
• The filtration is the natural filtration of $(B,\varepsilon)$, not its augmentation, and trading strategies are progressively measurable instead of predictable. Neither change alters the space of terminal gains.
• Gains are relations: a gain process is any version of the Itô integral, and every statement quantifies over all versions.
• The objective $E[(W-L)^2]$ and variances take values in $[0,\infty]$, so a non-square-integrable wealth cannot be optimal through a junk value $0$; inner products carry explicit integrability.
• $\rho_t\in[-1,1]$ (§3.1), not $[0,1]$ (§2). The sign of $v$ is free; only $|v|\ge\delta>0$ is assumed.
• "$\Phi(G^*)$ defined by (9)–(11)" means: for every solution of (10), where a solution includes that $\Phi(G^*)$ is a trading strategy. The paper takes this membership for granted.
• Lemma 2 and the moment equations are stated in integral form ($H_t=H_0-\int_0^t(m^2/v^2)H\,ds$), which is the paper's "for almost every $t$" derivative together with absolute continuity; continuity of the coefficients is not assumed.
• The display for $dZ$ in the proof of Lemma 2 omits $dt$; the drift is $(\gamma_t+\mu_t)Z_t\,dt$.
• In §4.1, $c>0$ is assumed explicitly.

Proposition 1 would hold vacuously if equation (10) had no solution; the existence milestone rules this out and must be proved, not assumed. Contributions are welcome on Itô's product formula and the martingale property of Itô integrals in the Peng framework, on the existence of solutions of linear SDEs, and on the Grönwall-type uniqueness for (13).

Selected references

• D. Duffie, H. R. Richardson, Mean-Variance Hedging in Continuous Time, The Annals of Applied Probability 1(1) (1991) 1–15. https://doi.org/10.1214/aoap/1177005978
• S. Peng, A General Stochastic Maximum Principle for Optimal Control Problems, SIAM J. Control Optim. 28(4) (1990) 966–979. https://doi.org/10.1137/0328054
• P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. https://doi.org/10.1007/978-3-662-02619-9
• D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969.
• M. Schweizer, Mean-Variance Hedging for General Claims, The Annals of Applied Probability 2(1) (1992) 171–179. https://doi.org/10.1214/aoap/1177005776

Motivation

Stochastic optimization asks for a decision $x$ in a set $\mathcal X\subset\mathbb R^d$ that minimises an expected loss $E_{P_0}[\ell(x;\xi)]$ when the distribution $P_0$ of the data $\xi$ is known only through a sample $\xi_1,\dots,\xi_n$. The classical estimator, sample average approximation, replaces $P_0$ by the empirical distribution $\widehat P_n$. Distributionally robust optimization instead minimises the worst-case expected loss over all distributions close to $\widehat P_n$. Duchi, Glynn and Namkoong (arXiv:1610.03425v3; Math. Oper. Res. 46(3), 2021) take the neighbourhood to be an $f$-divergence ball of radius $\rho/n$ and show that the robust optimal value is a calibrated upper confidence bound for the population optimum, in the spirit of Owen's empirical likelihood.

A confidence bound is useful only if the robust problem still estimates the right thing. Section 5 of the paper answers this: under essentially the conditions that make sample average approximation consistent, the robust optimal value converges to the population optimal value, and the robust minimisers approach the population minimisers. This mission formalizes that consistency result (contribution (iv), p. 3, and §5.1).

Setting

Let $\xi_1,\xi_2,\dots$ be i.i.d. random elements of a separable metric space $\Xi$ with law $P_0$, and let $\widehat P_n$ be the empirical distribution of $\xi_1,\dots,\xi_n$. Let $\ell:\mathbb R^d\times\Xi\to\mathbb R$ be lower semicontinuous on $\mathcal X\times\Xi$, with $\ell(x;\cdot)$ measurable for $x\in\mathcal X$, and let $\mathcal X\subset\mathbb R^d$ be a nonempty closed feasible set, as in the paper's opening setup (p. 1).

The divergence generator $f:[0,\infty)\to\mathbb R\cup\{+\infty\}$ is convex with $f(1)=0$; Assumption A asks moreover that $f$ be three times differentiable near $1$ with $f'(1)=0$ and $f''(1)=2$. For a distribution $P\ll\widehat P_n$ with weights $p_i$ on the sample points, $D_f(P\|\widehat P_n)=\frac1n\sum_i f(np_i)$. The robust objective and the population objective are

$$\widehat F_n(x)=\sup_{P\ll\widehat P_n}\Big\{E_P[\ell(x;\xi)] : D_f(P\|\widehat P_n)\le\frac{\rho}{n}\Big\},\qquad F(x)=E_{P_0}[\ell(x;\xi)],$$

with radius parameter $\rho\ge0$. Their solution sets are $S^\star_{\widehat P_n}=\operatorname{argmin}_{x\in\mathcal X}\widehat F_n(x)$ and $S^\star_{P_0}=\operatorname{argmin}_{x\in\mathcal X}F(x)$ (display (23)). The inclusion distance from a set $A$ to a set $B$ is $d_\subset(A,B)=\sup_{x\in A}\operatorname{dist}(x,B)$ (display (6)).

Assumption E asks for a measurable envelope $Z\ge0$ with $|\ell(x;\xi)|\le Z(\xi)$ for all $x\in\mathcal X$ and $E_{P_0}[Z^{1+\epsilon}]<\infty$ for some $\epsilon>0$. A class $\mathcal H$ of functions on $\Xi$ is Glivenko–Cantelli (Definition 2) if $\sup_{h\in\mathcal H}|E_{\widehat P_n}[h]-E_{P_0}[h]|\to0$ almost surely.

Formalization targets

Goal: Corollary 1 (p. 17)

Let Assumptions A and E hold, let $\mathcal X$ be nonempty and compact, and let $\ell(\cdot;\xi)$ be continuous on $\mathcal X$ for every $\xi$. Then, in outer probability,

$$\inf_{x\in\mathcal X}\widehat F_n(x)-\inf_{x\in\mathcal X}F(x)\xrightarrow{P^*}0 \qquad\text{and}\qquad d_\subset\big(S^\star_{\widehat P_n},S^\star_{P_0}\big)\xrightarrow{P^*}0 .$$

Both conclusions belong to the goal. No rate is asserted; the statement survives any later sharpening.

Milestones

1. Lemma 13 (p. 34): the likelihood-ratio vectors of the ball satisfy $\|np-\mathbb 1\|_2\le\sqrt{\rho C_f}$ uniformly in $n$, and the bound is of the right order ($\ge\sqrt{\rho c_f}$ for some $n,p$).
2. (47) (App. E.1, p. 46): $|E_P[\ell]-E_{P_0}[\ell]|\le E_{\widehat P_n}[|L-1|^p]^{1/p}E_{\widehat P_n}[|\ell|^q]^{1/q}+|E_{\widehat P_n}[\ell]-E_{P_0}[\ell]|$ with $q=\min\{2,1+\epsilon\}$, $p=\max\{2,1+1/\epsilon\}$.
3. The display after (47) (p. 46): $E_{\widehat P_n}[|L-1|^p]^{1/p}\le n^{-1/p}\sqrt{\rho C_f}$.
4. Theorem 7 (p. 16): if $\{\ell(x;\cdot):x\in\mathcal X\}$ is Glivenko–Cantelli, then

$$\sup_{x\in\mathcal X}\sup_{P\ll\widehat P_n}\Big\{|E_P[\ell(x;\xi)]-E_{P_0}[\ell(x;\xi)]| : D_f(P\|\widehat P_n)\le\tfrac{\rho}{n}\Big\}\xrightarrow{\text{a.s.}^*}0.$$

5. Example 5 (p. 16, from van der Vaart, Asymptotic Statistics, Example 19.8): a class of losses continuous on a compact $\mathcal X$ for almost every $\xi$, with an integrable envelope, is Glivenko–Cantelli.

Significance

The result. Corollary 1 shows that robustness against a $\rho/n$-divergence perturbation of the data costs nothing asymptotically: the robust optimal value and its minimisers are consistent for the population problem. Together with the paper's coverage theorem, this justifies using the robust value both as a point estimate and as an upper confidence bound. Theorem 7 is stronger than what the corollary needs: it controls every reweighting in the ball uniformly over $\mathcal X$, which is the uniform law of large numbers for distributionally robust objectives, and it needs only slightly more than the first moment that sample average approximation needs.

Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would supply a Glivenko–Cantelli notion for parametric loss classes, the bracketing argument behind Example 5 (a uniform strong law over a compact parameter set, not in Mathlib), and the passage from uniform convergence of objectives to convergence of optimal values and of argmin sets in the inclusion distance. The last two are standard steps of M-estimation and sample average approximation theory that are reusable well beyond this paper.

Difficulty

The obvious argument writes $E_P[\ell]-E_{P_0}[\ell]$ as a reweighting term plus the ordinary empirical deviation and handles the second by the Glivenko–Cantelli property. The reweighting term $\frac1n\sum_i(np_i-1)\ell(x;\xi_i)$ is the obstacle: the weights $np_i$ are not bounded uniformly in $n$ for every divergence, and a Cauchy–Schwarz bound would need a second moment of the envelope, which Assumption E does not provide. The exponent pair $(p,q)$ and the uniform $\ell_2$ control of Lemma 13 are what make $1+\epsilon$ moments enough.

For the solution sets, uniform convergence of $\widehat F_n$ to $F$ does not by itself place the minimisers of $\widehat F_n$ near those of $F$; compactness of $\mathcal X$ and continuity of $F$ are needed to separate $F$ on the complement of an $\epsilon$-enlargement of $S^\star_{P_0}$ from its minimum. Measurability is a further obstacle: suprema over uncountable $\mathcal X$ and over the divergence ball need not be measurable, which is why the paper works with outer probability and outer almost-sure convergence.

Formalization scope

• Samples are ξ : ℕ → Ω → Ξ on a probability space, measurable, mutually independent (iIndepFun) and identically distributed with ξ 0; $P_0$ is the law of ξ 0, and $\widehat P_n$ uses ξ 0, …, ξ (n-1) (0-based indices). The separable metric sample domain and lower semicontinuous loss from p. 1 are explicit in Theorem 7 and Corollary 1. Decisions live in EuclideanSpace ℝ (Fin d); ℓ x is measurable for each $x\in\mathcal X$.
• $f$ is ℝ → EReal satisfying the published IsPhiDivergenceFunction (never $-\infty$, finite on $(0,\infty)$, $f(1)=0$, convex on $[0,\infty)$) plus the smoothness of Assumption A, stated on $t\mapsto(f\,t).\mathrm{toReal}$ on an open interval around $1$.
• A distribution $P\ll\widehat P_n$ in the ball is a weight vector in the published probUncertaintySet f (1/n,…,1/n) (ρ/n), i.e. $\{p\ge0:\sum p_i=1,\ \sum_i f(np_i)\le\rho\}$. Every supremum "over $P$ with $D_f(P\|\widehat P_n)\le\rho/n$" is read over $P\ll\widehat P_n$, as in (4a).
• Suprema of absolute deviations (Definition 2, Theorem 7) are taken in $[0,\infty]$, and $d_\subset$ is $[0,\infty]$-valued; an unbounded family therefore cannot satisfy them through a junk real supremum of $0$. Almost-sure statements use Mathlib's ∀ᵐ, which requires the exceptional set to have outer measure zero; convergence in outer probability is $\mu\{\omega:\delta<|X_n(\omega)|\}\to0$ for every $\delta>0$ with Mathlib's outer measure and no measurability hypothesis.
• Readings recorded in the items: in (47) the middle term is $E_{\widehat P_n}[|L-1|\,|\ell|]$ (the page omits the absolute value on $\ell$); in the display after (47), $\sqrt{\rho/\gamma_f}$ is $\sqrt{\rho C_f}$ with $C_f$ from Lemma 13; in Lemma 13 the constants may depend on $\rho$ as well as $f$, as in its proof.
• A trivializing formalization would take the suprema in $\mathbb R$ (where an unbounded set has supremum $0$), or allow the argmin sets to be empty by construction; neither is possible here, and nonemptiness of the solution sets is not assumed.
• Contributions welcome: a Glivenko–Cantelli library for parametric classes (Example 5), the deterministic inequalities (47) and Lemma 13, and the argmin-consistency argument of Corollary 1.

Selected references

• J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3, 2018; Math. Oper. Res. 46(3), 2021. https://arxiv.org/abs/1610.03425 , https://doi.org/10.1287/moor.2020.1085
• A. W. van der Vaart, Asymptotic Statistics, Cambridge University Press, 1998 (Example 19.8). https://doi.org/10.1017/CBO9780511802256
• A. W. van der Vaart, J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2
• A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641

Motivation

Chance-constrained programming replaces a linear program $\max c'x$ subject to $Ax\le b$ by a problem in which some data are random and each constraint only has to hold with a prescribed probability. Charnes and Cooper introduced the idea in 1959 for scheduling heating-oil production against weather-dependent demand, and the formulation is now a standard modelling tool in operations research, finance, energy systems and engineering design (Charnes and Cooper 1959; Prékopa 1995).

A chance-constrained problem is not directly solvable: its constraints are probabilities of events that depend on the decision. The 1963 paper of Charnes and Cooper (doi:10.1287/opre.11.1.18) asks when such a problem has a deterministic equivalent, an ordinary mathematical program with the same feasible decisions and corresponding objective values, and when that equivalent is a convex program. Its first answer, for the expected-value ('E') model under linear decision rules and normality, is the subject of this mission. The resulting constraint form, a mean slack dominating $K_\alpha$ standard deviations, is an early instance of the second-order-cone reformulation of individual normal chance constraints used throughout modern stochastic and robust optimization.

Timeline. 1959: Charnes and Cooper, chance-constrained programming with the heating-oil model. 1963: this paper, deterministic equivalents for the E, V and P models under linear decision rules $x=Db$. 1965: Miller and Wagner treat joint chance constraints with independent rows (doi:10.1287/opre.13.6.930). 1971: Prékopa's logarithmically concave measures give convexity of joint chance constraints under log-concave laws.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. The data are a constant $m\times n$ matrix $A$ with rows $a_1',\dots,a_m'$, a random right-hand side $b:\Omega\to\mathbb R^m$ and random objective coefficients $c:\Omega\to\mathbb R^n$. A linear decision rule is an $n\times m$ real matrix $D$; it chooses $x=Db$ after $b$ is observed. Write $\mu_b=Eb$, $\mu_c=Ec$ and $\hat b=b-\mu_b$.

The E-model (18) is

$$\max\ E(c'Db)\quad\text{subject to}\quad P(a_i'Db\le b_i)\ge\alpha_i\qquad(i=1,\dots,m),$$

with one probability level $\alpha_i$ per row: the constraints are row-wise, as in (3) of the paper, not a single joint constraint.

For $\tfrac12<\alpha<1$ let $K_\alpha=\Phi^{-1}(\alpha)>0$ be the standard normal $\alpha$-quantile. With the moment functions (30),

$$\sigma_i^2(D)=E(a_i'Db-b_i)^2,\qquad \mu_i(D)=\mu_{b_i}-a_i'D\mu_b,$$

the paper's deterministic program (29) in the variables $(D,v)$, $v\in\mathbb R^m$, is

$$\min\ -\mu_c'D\mu_b\quad\text{s.t.}\quad \mu_i(D)-v_i\ge0,\quad -K_{\alpha_i}^2\sigma_i^2(D)+K_{\alpha_i}^2\mu_i^2(D)+v_i^2\ge0,\quad v_i\ge0 .$$

Formalization targets

Goal: (18) is equivalent to the convex program (29)

Assume every $b_k$ is square integrable, every $c_j$ and $c_jb_k$ integrable, $b$ and $c$ uncorrelated ($E(c_jb_k)=E c_j\,E b_k$), every variate $a_i'Db-b_i$ normal (for every $D$ and $i$, zero variance allowed), and $\tfrac12<\alpha_i<1$. Then

$$\Big(\forall D:\ D\text{ feasible for (18)}\iff\exists v,\ (D,v)\text{ feasible for (29)}\Big)\ \wedge\ \Big(\forall D:\ E(c'Db)=\mu_c'D\mu_b\Big)\ \wedge\ \{(D,v)\ \text{feasible for (29)}\}\ \text{is convex}.$$

Milestones, in the order of the paper

1. (19a): $E(c'Db)=(Ec)'D(Eb)$ for uncorrelated $b$, $c$.
2. (22)–(27): with positive variance, $P(a_i'Db\le b_i)\ge\alpha_i\iff(-\mu_{b_i}+a_i'D\mu_b)/\sqrt{E[\hat b_i-a_i'D\hat b]^2}\le-K_{\alpha_i}$.
3. (28a)–(28b): (27) holds iff some $v_i$ satisfies $\mu_{b_i}-a_i'D\mu_b\ge v_i\ge K_{\alpha_i}\sqrt{E[\hat b_i-a_i'D\hat b]^2}\ge0$.
4. (28c)–(28d): for $v_i\ge0$, that pair is equivalent to its squared form.
5. Footnote ‡ to (30): $\sigma_i^2(D)-\mu_i^2(D)=E[\hat b_i-a_i'D\hat b]^2$.
6. The convexity paragraph after (30): the feasible set of (29) is convex in $(D,v)$.
7. 'V Model' (32)–(34): under the same normal chance assumptions and square integrability of each $c_jb_k$, the chance constraints of (32) are equivalent to (33) for some $v$; the pair feasible set and $V(D)=E(c'Db-z^0)^2$ are convex.

Significance

The result. The theorem turns a problem whose constraints are probabilities into a finite-dimensional convex program whose data are the first two moments of $b$ and the means of $c$. The optimal rules of (18) minimize (29), whose optimal value is the negative of the maximum in (18). The slack variables $v_i$ separate each constraint into a "quality" part (the mean slack $\mu_i(D)$) and a "risk" part ($K_{\alpha_i}$ standard deviations), which is the interpretation the paper develops in (31) and its Appendix. The same constraint set serves the V-model (33), so only the objective changes between the two models.

Formalizing it. The result is classical and its proof is elementary, but the paper's argument is informal in ways that matter for a machine-checked version: it divides by a standard deviation it then allows to vanish, writes $F_i$ for what must be an upper-tail function, and labels a variance as $\sigma_i^2(D)$ while defining $\sigma_i^2(D)$ as a raw second moment. This mission produces a statement in which each of these points is settled, with every hypothesis explicit. No machine-checked version of the result is known to exist.

Difficulty

The chance-constraint step itself is a one-dimensional fact about the normal law, but three points need care. The variance of $a_i'Db-b_i$ may be zero for some $D$ and $i$; then the law is a point mass, the quotient in (27) is undefined, and the equivalence must be argued separately, as footnote † of p. 28 indicates. The quadratic constraint of (29) alone, $v_i^2\ge K_{\alpha_i}^2(\sigma_i^2(D)-\mu_i^2(D))$, describes both nappes of a hyperboloid and is not convex; convexity needs $v_i\ge0$ and the positive semidefiniteness of $D\mapsto\operatorname{Var}(a_i'Db-b_i)$, which comes from square integrability of $b$ and not from normality. Finally, the identity relating $\sigma_i^2$, $\mu_i^2$ and the variance requires the integrals to be genuine, so the integrability hypotheses cannot be dropped.

Formalization scope

Everything is in the namespace ChanceDetEquiv.EModel. The probability space is (Ω, P) with [IsProbabilityMeasure P]; A : Matrix (Fin m) (Fin n) ℝ, b : Ω → Fin m → ℝ, c : Ω → Fin n → ℝ, D : Matrix (Fin n) (Fin m) ℝ; $a_i'Db$ is (A *ᵥ (D *ᵥ b ω)) i. Expectations are Bochner integrals and probabilities are P.real. Explicit readings of the paper's phrases:

• "deterministic equivalent for (18)" is the conjunction of an iff between feasible sets (with the auxiliary $v$ existentially quantified) and $E(c'Db)=\mu_c'D\mu_b$ for every $D$; (29) minimizes the negative of this mean;
• "is a convex programming problem" is Convex ℝ of the feasible set of (29) in $(D,v)$, $v_i\ge0$ included; for the V model it also asserts ConvexOn ℝ of $V$;
• "normally distributed" is: for every $D$ and $i$, the law of $a_i'Db-b_i$ is gaussianReal μ s for some $\mu$ and $s\ge0$; joint normality of $b$ is not assumed, since it would be a stronger hypothesis;
• "$b$ and $c$ are uncorrelated" is $E(c_jb_k)=E c_j\,E b_k$ for all $j,k$;
• $K_\alpha=\Phi^{-1}(\alpha)$, using the published definition Cohen2019_Robust_Phi; $F_i$ in (26)–(27) is read as the upper-tail function of $z_i$, and $\alpha_i<1$ is added so that $K_{\alpha_i}$ is finite;
• $\sigma_i^2(D)$ is the raw second moment exactly as printed in (30).

Positive variance is a hypothesis of milestones 2 and 3, where (27) has a denominator. The goal and later milestones admit zero variance. The statements admit no trivializing reading: the normality hypothesis is satisfied by constant and by Gaussian $b$, the integrability hypotheses rule out the junk value $0$ of non-integrable expectations, and $\alpha_i<1$ rules out the junk value of $\Phi^{-1}(1)$.

A complete development needs: the normal CDF and quantile, the law of an affine image of a random variable, variance as $E X^2-(EX)^2$ in $L^2$, and convexity of the epigraph of a seminorm composed with an affine map. The convexity milestones need no probability beyond $L^2$ and are reusable for any second-order-cone representation of individual chance constraints. Proofs of any milestone, and of the goal from the milestones, are welcome.

The related open platform item KallMayer.Chance.chapter2_theorem2_5 (convexity of a single normal chance-feasible set in $x$) is credited here and not restated: no item of this mission states the convexity of the set of $D$ feasible for (18). Related published items that are about other models: DRCVRP.RCI.prob_le_iff_valueAtRisk_le (chance constraints and value-at-risk for a general law) and the log-concavity results of NumStochOpt.LogConcave.

Selected references

• A. Charnes and W. W. Cooper, Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints, Operations Research 11(1), 1963, 18–39. https://doi.org/10.1287/opre.11.1.18
• A. Charnes and W. W. Cooper, Chance-Constrained Programming, Management Science 6(1), 1959, 73–79. https://doi.org/10.1287/mnsc.6.1.73
• A. Prékopa, Stochastic Programming, Kluwer, 1995. https://doi.org/10.1007/978-94-017-3087-7
• P. Kall and J. Mayer, Stochastic Linear Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4419-7729-8

Motivation

A chance constraint limits the probability of violating a requirement rather than requiring that requirement to hold for every realization of uncertain data. Charnes and Cooper developed deterministic optimization problems for several ways of judging decisions under such constraints. Their P model gives a satisficing objective: increase the probability of reaching a specified aspiration level while meeting prescribed reliability levels for the resource constraints. The paper's concrete decision rule makes the decision vector depend linearly on the random right-hand side, and its P-model section moves from a fractional deterministic program to a convex one. The result explains how a risk-adjusted ratio can be optimized without retaining a fractional objective. The source is Charnes and Cooper, 1963, pp. 30–33, especially equations (35) and (38)–(39b).

The related linear-fractional change of variables was already being used for linear programs Charnes and Cooper, 1962; the present section applies it to constraints built from second moments rather than linear equations. That distinction matters because the normalized feasible set contains a boundary at zero scale, and because second-moment inequalities require their own convexity claim. The paper cites fractional programming results for its local-to-global assertion about (38); the mission focuses on its explicit transformed program (39). Charnes and Cooper, 1963, p. 32.

Setting

Let $m,n$ be positive integers and $(\Omega,P)$ a probability space. A fixed real $m\times n$ matrix $A$ has rows $a_i'$. Random vectors $b:\Omega\to\mathbb R^m$ and $c:\Omega\to\mathbb R^n$ give the right-hand side and objective coefficients. The paper restricts decisions to the linear decision rule $x=Db$, where the real $n\times m$ matrix $D$ is chosen before $b$ is realized. Write $\mu_b=E[b]$ and $\mu_c=E[c]$. A number $z_0$ is the given aspiration value. For each row $i$, its reliability level $\alpha_i$ is strictly between $1/2$ and $1$, and $K_i=\Phi^{-1}(\alpha_i)>0$ is the corresponding standard-normal quantile. These are the objects of equations (5), (19b), (21), and (27) in Charnes and Cooper, 1963.

The residual $a_i'Db-b_i$ has raw second moment $\sigma_i^2(D)=E[(a_i'Db-b_i)^2]$ and negative mean $\mu_i(D)=\mu_{b_i}-a_i'D\mu_b$. The aspiration error has raw second moment $V(D)=E[(c'Db-z_0)^2]$. These definitions come from equations (30) and (34). The expected linear objective appearing in the deterministic programs is $\mu_c'D\mu_b$; the model records the paper's assumption that the components of $b$ and $c$ are uncorrelated. Charnes and Cooper, 1963, pp. 26, 28, 30.

Program (38) chooses $(D,v,v_0,w_0)$ and maximizes $v_0/w_0$. Its inequalities bound the mean objective below by $z_0+v_0$, bound $w_0$ below by the root-mean-square aspiration error, and bound each nonnegative $v_i$ between the row's risk term and $\mu_i(D)$. The denominator satisfies $w_0>0$. Program (39) introduces a nonnegative scale $t$ and barred variables. It fixes $\bar w_0=1$ and maximizes the linear objective $\bar v_0$. The barred moments are calculated from $\bar D$ and $t$ by equation (39b), rather than declared to be scaled copies of the unbarred moments. Charnes and Cooper, 1963, pp. 32–33.

Formalization targets

Convex transformed program

Let $F_{39}$ contain every point satisfying all of (39), including $t=0$. The paper's convex-programming claim becomes

$$F_{39}\text{ is convex}.$$

The source states the claim after displaying the barred moments, in the paragraph following (39b). Charnes and Cooper, 1963, p. 33.

Equal optimal values

Let $F_{38}$ be the feasible set of (38). Provided $F_{38}$ is nonempty, the mission goal states that the normalized substitution sends each point of $F_{38}$ to a point of $F_{39}$ with the same objective, and that

$$\sup_{(D,v,v_0,w_0)\in F_{38}}\frac{v_0}{w_0} =\sup_{(\bar D,\bar v,\bar v_0,\bar w_0,t)\in F_{39}}\bar v_0.$$

The suprema may be infinite. The equality concerns the complete program (39), including $t=0$. Positive-scale points have an inverse substitution; zero-scale points are retained in the comparison. This is the precise optimal-value reading of the paper's statement that (38) can be replaced by one convex program. Charnes and Cooper, 1963, pp. 32–33.

Significance

The result places the P model alongside the paper's E and V models as an optimization problem with convex feasible constraints and a nonfractional objective. A solver of (39) can compare aspiration and resource reliability within the same matrix decision rule. Equality of suprema says the transformed model has the same best attainable value even when the best value is only approached, and even when points at $t=0$ occur in the transformed feasible set. The forward and inverse substitution statements identify how positive-scale solutions correspond. Charnes and Cooper, 1963, pp. 30–33.

The paper result is a published mathematical claim. The present formalization states its definitions and assertions in Lean; its theorem proofs are still open. The standard Gaussian CDF and its inverse are available as a separately published Prove2Me definition, while the model-specific second moments and feasible sets must be formalized for this mission. The previously published Derman linear-fractional lemma concerns a polyhedral linear program and does not assert this P-model result. Completing the mission would add reusable formal machinery for expected-square constraints, a normalized perspective program, and equality of optimal values at a scale boundary.

Difficulty

The pointwise substitution $t=1/w_0$ only reaches points of (39) with $t>0$, while (39) explicitly permits $t=0$. Therefore a bijection of feasible points at positive scale alone does not establish equality of the displayed suprema. The proof also has to reconcile the squared form of the row constraints with convexity: $\bar\sigma_i^2$ is a raw second moment and $\bar\mu_i^2$ is the square of its mean, so their difference is the variance term relevant to the risk bound. Taking the fourth inequality as a generic difference of quadratics would obscure that claim. The paper prints a conflicting square and sign in (38), which must be resolved against its earlier (29) and later (39). Charnes and Cooper, 1963, pp. 28, 32–33.

Formalization scope

Lean uses finite index types Fin m and Fin n, real matrices and scalars, a probability measure $P$, and Bochner integrals for the moments. Square integrability is stated for every component of $b$ and $c$ and every product $c_jb_k$; this keeps the expected squares meaningful. The paper assumes $b$ and $c$ are uncorrelated, so the same componentwise equalities are recorded. It also assumes that each row residual has a Gaussian law under a decision matrix; the Lean theorem retains this standing assumption even though the substitution from (38) to (39) is algebraic. The quantile $K_i$ is imported from the published Cohen2019.Robust.PhiInvReal, with $1/2<\alpha_i<1$ excluding its junk endpoint values. The theorem concerns (38) onward; it does not assert the paper's analogous reduction from the original probability model (35), because the text does not establish a distributional theorem for its random objective. Charnes and Cooper, 1963, pp. 26–27, 31–33.

The source phrase “replace ... by one convex programming problem” is made explicit as convexity of the (39) feasible set, feasibility and value preservation of the forward scaling, and equality of extended-real suprema. The normalization $\bar w_0=1$, strict $w_0>0$, and weak $t\ge0$ are separate conditions. The $t=0$ slice is included, and the main theorem assumes $F_{38}$ nonempty. The barred functions are genuine expectations of the homogenized expressions of (39b). The square-and-sign discrepancy in printed (38) is resolved in favor of the form printed in (29) and (39), consistent with the nearby statement that the row constraints are the same as before. These choices exclude a vacuous denominator, an artificially smaller transformed set, and a trivially defined scaling identity. Reusable contributions include moment lemmas, convexity results for expected-square constraints, and supremum comparison for normalized programs.

Selected references

• A. Charnes and W. W. Cooper, Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints, Operations Research 11(1), 1963, pp. 18–39. DOI.
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4), 1962, pp. 181–186. DOI.
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 1962, pp. 16–24. DOI.
• J. Cohen, E. Rosenfeld, and Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML, 2019. arXiv.

Motivation

Network revenue management is the problem of selling several limited, perishable resources (seats on flight legs, hotel room-nights, machine hours) to customers who arrive over time and each want a fixed bundle of them. A seller who accepts every request early may run out of the resources that the most valuable later customers need, and a seller who is too cautious leaves capacity unsold at the end of the horizon. Airlines, hotels and car-rental firms solve instances of this problem daily (Talluri and van Ryzin, 2004).

The exact optimal policy is a dynamic program over the vector of remaining capacities, which is intractable for realistic networks. The standard remedy replaces the random demand by its mean, which gives a linear program, the deterministic LP (DLP), and turns its solution into an admission rule. Its value is an upper bound on what any policy can earn (Gallego and van Ryzin, 1997). Solving the LP once, at time zero, loses $O(\sqrt{T})$ against that bound over a horizon of length $T$. A natural improvement is to re-solve the LP as capacity is consumed.

Timeline of the re-solving question, as the source surveys it (Sec. 1, pp. 3–4):

• 1997: Gallego and van Ryzin: static policies built from the DLP lose $\Theta(\sqrt{T})$.
• 2002: Cooper gives an example in which re-solving the DLP makes booking-limit control worse.
• 2008: Reiman and Wang re-solve exactly once, at an endogenous random time, with probabilistic allocation, and obtain $o(\sqrt{T})$ loss.
• 2012: Jasin and Kumar prove that re-solving after every unit of time with probabilistic allocation (the policy FR below) loses $O(1)$, provided the DLP solution is nondegenerate. Wu et al. (2015) obtain $O(1)$ for one resource, with a constant that blows up as the solution approaches degeneracy.
• 2018: Bumpensanti and Wang (arXiv:1802.06192) show that FR can lose $\Omega(\sqrt{T})$ against the hindsight optimum on a degenerate instance, propose a modified policy with $O(1)$ loss in all cases, and prove that FR never loses more than $O(\sqrt{T})$ against the DLP. This mission formalizes the last of these results.

Setting

There are $n$ customer classes $j \in [n]$ and $m$ resources $l \in [m]$. Over the horizon $[0, T]$, class-$j$ customers arrive according to independent Poisson processes with rates $\lambda_j > 0$. Accepting a class-$j$ customer earns $r_j \ge 0$ and consumes $a_{lj} \ge 0$ units of each resource $l$; $A = (a_{lj})$ is the bill-of-materials matrix and $A_j$ its $j$-th column. The initial capacity vector is $C \ge 0$. A customer can be accepted only if $A_j \le C'$ componentwise, where $C'$ is the capacity remaining at its arrival.

For a capacity-per-unit-time vector $b \ge 0$, let

$$v(b) = \max\Big\{ \sum_{j=1}^n r_j x_j \ :\ \sum_{j=1}^n A_j x_j \le b,\ 0 \le x_j \le \lambda_j \Big\}.$$

The DLP value is $v^{\mathrm{DLP}}(T, C) = T\, v(C/T)$.

The Frequent Re-solving policy (FR) divides the horizon into $T$ unit periods $[t, t+1)$. At the start of period $t$, with remaining capacity $C(t)$, it sets $b(t) = C(t)/(T - t)$, computes an optimal solution $x(t)$ of the LP with right-hand side $b(t)$, and during the period accepts each class-$j$ arrival with probability $x_j(t)/\lambda_j$, subject to the capacity check. Its expected revenue is $v^{\mathrm{FR}}(T, C)$. The LP may have several optimal solutions; the results hold for every rule choosing among them.

Formalization targets

Goal: Proposition 3

There is a constant $M$, depending only on $\lambda$, $r$ and $A$, such that for every integer $T \ge 1$, every capacity $C \ge 0$ and every choice of optimal LP solutions,

$$v^{\mathrm{DLP}}(T, C) - v^{\mathrm{FR}}(T, C) \le M \sqrt{T}.$$

The content is the uniformity: $M$ does not depend on $C$, so the bound holds whether capacity is scarce, abundant, or degenerate for the LP.

Milestones, in the order the proof uses them

1. Eq. (32), p. 35. The capacity check costs FR at most $\sum_j r_j(\log T + 1) + \sum_j r_j \lambda_j$ relative to the LP revenue it targets:

$$v^{\mathrm{FR}} \ge \mathbb{E}\Big[\sum_{t=0}^{T-1} \sum_{j=1}^n r_j x_j(t)\Big] - \sum_{j=1}^n r_j (\log T + 1) - \sum_{j=1}^n r_j \lambda_j .$$

2. Eq. (33), p. 35. LP sensitivity in the right-hand side: $v(b) - v(b') \le \sum_l r^l_{\max} (b_l - b'_l)^+$ with $r^l_{\max} = \max_j r_j \mathbb{I}(a_{lj} > 0)/a_{lj}$.
3. Lemma 8, p. 43 (corrected). $\mathbb{E}[(b_l - b_l(t))^+] \le K_l \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}}$ with $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$.
4. p. 36. $\sum_{t=0}^{T-1} \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}} \le 2\sqrt{T} + \sqrt{2}$.
5. p. 36, explicit bound.

$$v^{\mathrm{DLP}} - v^{\mathrm{FR}} \le \sum_{l=1}^m r^l_{\max} K_l (2\sqrt{T} + \sqrt{2}) + n\, r_{\max} (\log T + 1) + n\, r_{\max} \lambda_{\max} .$$

Significance

The result. Because $v^{\mathrm{DLP}}$ bounds the expected revenue of every admissible policy, Proposition 3 says that FR loses at most $O(\sqrt{T})$ against the optimal policy in every instance, degenerate or not. Re-solving therefore never does worse, in order, than solving once. Together with the $\Omega(\sqrt{T})$ lower bound on a degenerate instance (Proposition 2 of the same paper), it shows that the order $\sqrt{T}$ is exact for FR. The nondegeneracy assumption of the earlier $O(1)$ analysis cannot be dropped. The explicit form (milestone 5) bounds the loss by constants computable from $(\lambda, r, A)$.

Formalizing it. The result is proved in the source; no part of it is machine-checked. A formalization adds three things. It gives a precise model of an adaptive, randomized admission policy in a Poisson network, which other results on re-solving and bid-price policies can reuse. It gives a checked LP sensitivity bound. And it checks the paper's constants: the printed constant of Lemma 8 is wrong (see Formalization scope), and the mission states the corrected one.

Difficulty

The obvious argument compares FR with the DLP period by period: the LP that FR solves at time $t$ differs from the original only in its right-hand side, so the loss should be controlled by how far $b(t)$ drifts below $b = C/T$. Two things break a naive version of this. First, $b(t)$ is a ratio whose denominator $T - t$ shrinks to $1$, so fluctuations late in the horizon are amplified; a crude bound on the drift at each $t$ sums to more than $\sqrt{T}$. Second, FR's realized consumption is not the LP's target: the capacity check rejects customers, and the LP solutions $x(i)$ depend on the whole past, so the consumption in different periods is not independent.

Uniformity in $C$ is the whole point. Arguments that rely on a margin between $C/T$ and the degenerate points of the LP, as in the nondegenerate analysis, give constants that blow up as that margin vanishes.

Formalization scope

The source is arXiv:1802.06192v3, whose printed page numbers equal the PDF page numbers. Everything lives in the namespace ResolvingNRM.FRUpper.

• LP value. $v(b)$ is the published piValue A r b lam of RLPBidPrice.Unbiased.Model (a real supremum, equal to the LP maximum for $b \ge 0$).
• Optimal solutions. The "$\arg\max$" of Algorithm 2 is an arbitrary optimal-solution selector sel; every theorem quantifies over all selectors, with constants chosen before the selector.
• Randomness. Within a period the acceptance probabilities are fixed, so the period's arrivals are represented exactly as a Poisson number of customers in arrival order, with i.i.d. classes of law $\lambda_j / \sum_i \lambda_i$ and independent Bernoulli acceptance coins. Expectations are series over this law (windowExp). FR's value is a backward recursion over periods (frTail), and expectations of functions of $C(t)$ are a forward recursion (frStateExp).
• Horizon. $T$ is a positive integer; capacities are real vectors.
• Standing assumptions of p. 7, left implicit there and hypotheses here: $\lambda_j > 0$, $r_j \ge 0$, $a_{lj} \ge 0$, $C \ge 0$.
• $O(\cdot)$. "$= O(\sqrt{T})$" is $\exists M,\ \forall\, \mathrm{sel}, T \ge 1, C \ge 0$. The paper's threshold $T_1$ is dropped, which is equivalent because $0 \le v^{\mathrm{FR}}$ and $v^{\mathrm{DLP}} \le T\sum_j r_j\lambda_j$.
• Corrected slip, Lemma 8. The printed $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j^2}$ is false: the proof replaces the conditional variance $x_j(i) \le \lambda_j$ of a Poisson increment by $\lambda_j^2$. With one class, one resource, $a = 1$, $\lambda = 0.01$, $C = \lambda T$, $T = 1000$ and $t = 2$, an exact computation gives $\mathbb{E}[(b - b(2))^+] \approx 1.96 \cdot 10^{-5}$, above the printed bound $1.42 \cdot 10^{-5}$. The mission uses $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$ in Lemma 8 and in the explicit bound.
• Index slip. The paper's sums $\sum_{l=1}^L$ run over its $m$ resources and are read as $l \in [m]$.

A trivializing formalization is ruled out. The constant $M$ is chosen before $C$. FR is defined with every optimal LP solution, not only nondegenerate or vertex ones. The capacity check is kept arrival by arrival; without it, FR's expected revenue would equal the LP revenue it targets and the gap would be trivially small.

Contributions welcome on every milestone. The LP sensitivity bound (33) is a statement about linear programs alone and milestone 4 about real numbers alone; both are reusable outside this mission, as is the window model of a randomized admission policy.

Selected references

• Y. Bumpensanti, H. Wang, A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, arXiv:1802.06192v3, 2018 (the source of this mission; later in Management Science 66(7), 2020). https://arxiv.org/abs/1802.06192
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997.
• W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4), 720–727, 2002.
• M. I. Reiman, Q. Wang, An Asymptotically Optimal Policy for a Quantity-Based Network Revenue Management Problem, Mathematics of Operations Research 33(2), 257–282, 2008.
• S. Jasin, S. Kumar, A Re-Solving Heuristic with Bounded Revenue Loss for Network Revenue Management with Customer Choice, Mathematics of Operations Research 37(2), 313–345, 2012.
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004.

Bibliographic details of the non-arXiv entries are those of the source's reference list (pp. 24–25).