Probability

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).

Motivation

A discrete-event simulation of a queue, an inventory system or a communication network produces an output process $Y = \{Y(t) : t \ge 0\}$, and the quantity of interest is usually its steady-state mean $\mu$, the long-run average of $Y$. The natural estimator is the time average $\bar Y_n(1) = \frac1n\int_0^n Y(s)\,ds$ of a run of length $n$. A confidence interval for $\mu$ needs the scale of the fluctuations of $\bar Y_n(1)$, the variance constant $\sigma^2$ of the central limit theorem $n^{1/2}(\bar Y_n(1) - \mu) \Rightarrow \sigma N(0,1)$. For correlated simulation output, $\sigma^2$ is a sum of autocovariances at all lags and is hard to estimate consistently.

The method of standardized time series (STS), introduced by Schruben (Schruben 1983), avoids estimating $\sigma$: it divides the centred time average by a functional of the whole observed path that scales like $\sigma$, so that $\sigma$ cancels. Batch means, the standardized sum, and the standardized maximum are all of this form.

Glynn and Iglehart (Glynn & Iglehart 1990) put the method on a general footing. They require only a functional central limit theorem (FCLT) for $Y$, and they identify an abstract class $\mathcal M$ of standardizing functionals for which the cancellation works. This mission formalizes their basic limit theorem, Theorem 2.4, and the four claims of its proof. Two companion results of §2, display (2.2) and the weak law $\bar Y_n(1) \Rightarrow \mu$, are included as further targets.

Setting

$C[0,1]$ is the space of continuous real functions on $[0,1]$ with the uniform norm and its Borel $\sigma$-algebra; $k \in C[0,1]$ is the identity path $k(t) = t$. For $g : C[0,1] \to \mathbb R$, $D(g)$ is the discontinuity set of $g$, the set of $x$ at which $g$ is not continuous. A standard Brownian motion $B$ on a probability space $(\Omega, \mathcal F, P)$ is a random element of $C[0,1]$ with Gaussian finite-dimensional laws, $B(0) = 0$ and $\operatorname{Cov}(B(s), B(t)) = \min(s,t)$.

The output $Y$ is a real-valued measurable process. Its scaled partial-integral process and its centred, rescaled version are

$$\bar Y_n(t) = \frac1n\int_0^{nt} Y(s)\,ds, \qquad X_n(t) = n^{1/2}\bigl(\bar Y_n(t) - \mu t\bigr), \qquad 0 \le t \le 1 .$$

Assumption (2.1) asks for finite constants $\mu$ and $\sigma > 0$ such that $X_n \Rightarrow \sigma B$ as $n \to \infty$, weak convergence of random elements of $C[0,1]$. It holds for $\phi$-mixing, strongly mixing, associated and regenerative output processes, among others.

The class $\mathcal M$ of (2.3) consists of the measurable $g : C[0,1] \to \mathbb R$ with

1. $g(\alpha x) = \alpha g(x)$ for $\alpha > 0$ (positive homogeneity);
2. $g(x - \beta k) = g(x)$ for $\beta \in \mathbb R$ (invariance under subtracting a linear drift);
3. $P\{g(B) > 0\} = 1$;
4. $P\{B \in D(g)\} = 0$.

The proof uses the auxiliary map $h(x) = x(1)/g(x)$ for $g(x) \ne 0$ and $h(x) = 0$ otherwise.

Formalization targets

Goal: Theorem 2.4

For every $g \in \mathcal M$, under Assumption (2.1),

$$\frac{\bar Y_n(1) - \mu}{g(\bar Y_n)} \Rightarrow \frac{B(1)}{g(B)} \qquad (n \to \infty). \tag{2.5}$$

Milestones: the four claims of the proof (p. 3)

1. $P\{\sigma B \in D(h)\} = 0$.
2. $h(X_n) \Rightarrow h(\sigma B)$.
3. $h(\sigma B) = B(1)/g(B)$, by (2.3i).
4. $h(X_n) = (\bar Y_n(1) - \mu)/g(\bar Y_n)$ for $n \ge 1$, by (2.3i) and (2.3ii).

Companions

$$n^{1/2}\bigl(\bar Y_n(1) - \mu\bigr) \Rightarrow \sigma B(1) \tag{2.2}$$

and $\bar Y_n(1) \Rightarrow \mu$.

Significance

Theorem 2.4 is the limit theorem behind every STS confidence interval. The limit $B(1)/g(B)$ is free of $\sigma$ and of the output process, so with $z$ chosen so that $P\{-z \le B(1)/g(B) \le z\}$ equals a prescribed level, the interval $\bar Y_n(1) \pm z\,g(\bar Y_n)$ has asymptotically exact coverage for $\mu$. Each choice of $g \in \mathcal M$ gives a method: batch means with a fixed number of batches, Schruben's standardized sum, the standardized maximum. The later sections of the paper compare the lengths of these intervals with those of consistent-estimation intervals, and those comparisons start from Theorem 2.4.

The theorem is classical and its proof is short on paper. What is missing is a machine-checked version. The formal proof needs a continuous mapping theorem for maps that are continuous only almost surely at the limit, on the non-locally-compact space $C[0,1]$; Mathlib has the version for continuous maps only. A formal Theorem 2.4 also makes the class $\mathcal M$ and the C[0,1]-valued FCLT available for the other results of the paper, the expected-length lower bound and its non-attainment, which are formalized in sibling missions.

Difficulty

The algebra (milestones 3 and 4) is elementary. The difficulty is the continuous-mapping step. The map $h$ is in general not continuous: it can be discontinuous wherever $g$ is and wherever $g$ vanishes, and $g$ itself may be discontinuous on a large set (the standardized maximum is). The continuous mapping theorem for continuous maps does not apply. One needs its almost-sure form: if $X_n \Rightarrow X$ and $P\{X \in D(h)\} = 0$, then $h(X_n) \Rightarrow h(X)$. The class $\mathcal M$ controls $D(g)$ only along the law of $B$, and the hypothesis of the almost-sure theorem is about $D(h)$ at the scaled limit $\sigma B$, so the conditions (2.3iii) and (2.3iv) have to be transported from $B$ to $\sigma B$ and from $g$ to $h$.

Formalization scope

$C[0,1]$ is C(unitInterval, ℝ) with its sup-norm topology; the Borel MeasurableSpace instance is declared in the mission's definition file, since Mathlib has none at this commit. Weak convergence is Mathlib's TendstoInDistribution, for the $C[0,1]$-valued FCLT and for the real-valued conclusions. The standard Brownian motion is a measurable $C[0,1]$-valued map whose coordinates agree, for every $\omega$, with a process satisfying Mathlib's IsBrownianReal. $D(g)$ is the set of points where ContinuousAt g fails, and $P\{B \in D(g)\}$ is an outer measure, so no measurability of $D(g)$ is assumed.

$\bar Y_n$ is a $C[0,1]$-valued parameter pinned pointwise by $\bar Y_n(t) = \frac1n\int_0^{nt}Y(s)\,ds$, so it is determined by $Y$. Assumption (2.1) carries joint measurability of $Y$ and local integrability of each path; the second is implicit in the paper and makes $\bar Y_n$ defined. The index $n$ runs over $\mathbb N$, and milestone 4 assumes $n \ge 1$ because (2.3i) is applied with $\alpha = n^{1/2}$. Real division by zero returns $0$ in Lean, which agrees with the paper's convention for $h$; it matters only on events of probability zero in the limit. Condition (2.3iii) is printed "$P\{g(b) > 0\} = 1$" and is read as $P\{g(B) > 0\} = 1$.

Condition (2.3iv) is stated with the discontinuity set, not as continuity of $g$: requiring $g$ continuous everywhere would exclude the standardized maximum of Example 3.10 and would make the continuous-mapping step trivial. The goal assumes nothing about $h$, $D(h)$ or any mapping theorem; these appear only in the milestones.

Contributions welcome: the almost-sure continuous mapping theorem for TendstoInDistribution on a metric space (reusable well beyond this mission), the cone property of $D(g)$ under positive homogeneity, and evaluation at a point as a continuous map on $C[0,1]$. Mathlib does not yet construct a Brownian motion with continuous paths as a $C[0,1]$-valued random element, so the hypotheses cannot be instantiated inside Lean; this is a hypothesis on $B$, not a vacuity.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. https://doi.org/10.1287/moor.15.1.1
• L. Schruben, Confidence interval estimation using standardized time series, Operations Research 31(6):1090–1108, 1983. https://doi.org/10.1287/opre.31.6.1090
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968 (Theorem 5.1, the continuous mapping theorem).
• K. L. Chung, A Course in Probability Theory, 2nd ed., Academic Press, 1974 (p. 93, converging-together lemma).

Motivation

In 1955 Charnes, Cooper and Ferguson proposed to estimate the weights of an executive compensation scheme by linear programming instead of least squares: the weights minimise a sum of absolute deviations subject to ranking, ceiling and floor constraints, which is a linear program. The coefficients of that program are not known exactly. They are averages of ratings collected from a sample of job holders, so the program actually solved is a random perturbation of a "true" program built from population means. The Appendix of the paper (§8, Consistency of Estimates) asks the basic statistical question about such an estimator: as the sample grows, does the optimal solution of the sample program converge to the optimal solution of the true program?

The question is not specific to compensation. Whenever the constraint matrix of a linear program is estimated from data, the computed optimum is an estimator, and its consistency is the first property one wants. The Appendix is one of the earliest statements of this kind for linear programming, written at a time when the simplex method itself was only a few years old (Dantzig 1951).

Setting

Fix integers $m$ (the number of constraints, indexed by $i$) and $n$ (the number of variables, indexed by $j$), a right-hand side $b\in\mathbb R^m$ and a cost vector $c\in\mathbb R^n$. For a real $m\times n$ matrix $X=(x_{ij})$ consider the linear program (8)

$$\min\ \sum_j c_ja_j\quad\text{subject to}\quad \sum_j x_{ij}a_j\ge b_i\ \ (i=1,\dots,m),\qquad a_j\ge0\ \ (j=1,\dots,n).$$

Its feasible set $F(X,b)$ is a polyhedron in $\mathbb R^n$, and a minimizing solution is a feasible point at which the objective is no larger than at any other feasible point.

The true matrix $\xi=(\xi_{ij})$ collects population means. For each sample size $N$ the observed matrix is

$$x_{ij}=\xi_{ij}+\eta_{ij}\qquad(9)$$

where the sampling errors $\eta_{ij}=\eta^{(N)}_{ij}$ are random variables on a probability space $(\Omega,\mathcal F,P)$ with $\eta_{ij}\to0$ in probability as $N\to\infty$.

The paper makes two assumptions about the true program:

• (I) the program (8) with matrix $\xi$ has a unique solution vector $\hat\alpha$;
• (II) every set of $m$ columns of $\xi$ is linearly independent.

A feasible point $a$ is nondegenerate if the number of strictly positive variables $a_j$ plus the number of constraints with strictly positive surplus $\sum_jx_{ij}a_j-b_i$ equals $m$. At an extreme point this means that the basis of the point, after adding one surplus variable per constraint, consists of $m$ strictly positive basic variables.

Formalization targets

Goal: consistency of the LP estimate

Under (I), (II) and nondegeneracy of $\hat\alpha$, for every $\varepsilon>0$,

$$P\bigl(\text{(8) with matrix }\xi+\eta^{(N)}\text{ has a unique minimizing solution }\hat a\text{ and }|\hat a-\hat\alpha|<\varepsilon\bigr)\longrightarrow1\qquad(N\to\infty).$$

The event asserts that the sample minimiser exists and is unique, as the paper's phrase "the minimizing solution of (8), $\hat a(\eta)$" presupposes, and that it is close to $\hat\alpha$.

Milestones

1. Claim A (p. 150): linear independence of a set of columns is preserved under sufficiently small entrywise perturbation.
2. Claim B (p. 150): the extreme points of $F(X,b)$ are exactly the feasible points whose positive variables and positive surpluses index linearly independent columns of $[X,-I]$.
3. Corresponding extreme points (p. 150): a nondegenerate extreme point of the true set has, for every nearby matrix, an extreme point of the sample set with the same positive support, arbitrarily close to it.
4. The Lipschitz bound (p. 151): $|c'(\alpha-a)|\le B|\alpha-a|$ for a positive constant $B$.
5. The gap argument (p. 151), deterministic form: under (I) and nondegeneracy of $\hat\alpha$, every matrix close enough to $\xi$ gives a program with a unique minimiser, close to $\hat\alpha$.

A companion item records that the claim as printed, under (I) and (II) alone, is false.

Significance

The theorem says that the linear programming estimator of the paper is consistent: with enough data, the computed weights are, with high probability, the unique optimum of the sample program and close to the true weights. More generally it is a stability statement for linear programs with a unique nondegenerate optimum under perturbation of the constraint matrix, which is the setting of sensitivity analysis and of sample-average approximation for linear programs.

The paper gives a sketch, not a complete proof. Its argument transfers extreme points of the true polyhedron to the sample polyhedron and compares objective values. That transfer is valid at nondegenerate extreme points only, and the claim as printed fails without such a condition: for $\xi=\begin{pmatrix}1&1\\-1&-2\end{pmatrix}$ and $b=(1,-1)$ the true feasible set is the single point $(1,0)$, so (I) holds, the two columns are independent, so (II) holds, yet replacing $\xi_{11}$ by any value in $(\tfrac12,1)$ makes the program infeasible. The mission therefore adds one disclosed hypothesis, nondegeneracy of the true optimum $\hat\alpha$, and keeps everything else as on the page. To the best of the curators' knowledge, neither the paper's statement nor the repaired one has been machine-checked; this mission formalizes the repaired theorem, the steps of the paper's argument, and the counterexample to the printed statement.

Difficulty

The natural first idea is that the feasible set and the optimum move continuously with the data. That is false in general: a polyhedron defined by perturbed inequalities can lose extreme points, gain new ones, or become empty, and the optimum of a linear program is not a continuous function of the constraint matrix. The paper's claim that the sample polyhedron has "precisely the same number of extreme points as the true convex set" and that the parenthetical of claim B is preserved under small modifications both fail at degenerate extreme points. The difficulty is to control, near a unique nondegenerate optimum $\hat\alpha$, both the feasibility of the sample program and the identity of its optimal extreme point, and to turn this into a probability statement without any measurability assumption on the estimator.

Formalization scope

All objects live in the namespace ExecCompLP.Consistency. Matrices are Matrix (Fin m) (Fin n) ℝ with X i j the entry $x_{ij}$; column $j$ is fun i => X i j. Indices are 0-based. Vectors are Fin n → ℝ, and distances between them use the maximum norm (dist on Fin n → ℝ); closeness of matrices is entrywise. Every norm gives the same statements.

• The optimal value of (8) is never defined as an infimum; a minimizer is a feasible point no worse than every feasible point. Assumption (I) includes existence.
• Assumption (II) is about $m$-element sets of columns, with $m$ the number of rows; it is vacuous when $n<m$, as on the page. It is a hypothesis of the goal, as printed, although the repaired argument does not need it; milestone 5 drops it.
• Nondegeneracy of $\hat\alpha$ is the only added hypothesis. It is not replaced by anything stronger (nondegeneracy of all extreme points, a Slater point, boundedness).
• Randomness enters only through $\eta^{(N)}_{ij}\to0$ in probability (TendstoInMeasure), which is the conclusion of (9) on p. 149 taken as a hypothesis; sample means and variances are not modelled. The probability of the goal's event is an outer measure, so no measurability of $\eta$ or of the estimator is assumed.
• Ruled out as trivializations: a conclusion that only bounds every minimizer "if any" (vacuous on infeasible samples), and a conclusion conditioned on feasibility. The goal's event asserts existence and uniqueness of the sample minimizer.

A complete development needs: openness of linear independence, the inequality-form characterization of extreme points by linearly independent positive columns, continuity of basic solutions in the data, and positivity of reduced costs at a unique nondegenerate optimum. The first three are reusable for any perturbation analysis of linear programs. Proofs of any item, and alternative arguments for the goal, are welcome.

Selected references

• A. Charnes, W. W. Cooper and R. O. Ferguson, Optimal estimation of executive compensation by linear programming, Management Science 1(2):138–151, 1955. https://doi.org/10.1287/mnsc.1.2.138
• G. B. Dantzig, Maximization of a linear function of variables subject to linear inequalities, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951.
• L. S. Pontryagin, Foundations of Combinatorial Topology, Graylock Press, 1952 (cited for claim A).
• W. Feller, An Introduction to Probability Theory and Its Applications, Wiley, 1950 (cited for (9)).