Operations Research

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ by the requirement that it hold for every $\mathbf u$ in an uncertainty set $\mathcal U\subseteq\mathbb R^d$. The resulting problems are tractable for many sets, but the choice of $\mathcal U$ decides whether the solution means anything probabilistically. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167:235–292, 2018) propose to build $\mathcal U$ from data so that, with high probability over the sample, every robust-feasible decision is also feasible with probability at least $1-\epsilon$ under the unknown distribution $\mathbb P^*$.

This mission covers §6 of that paper, the case where the data are samples of the marginals of $\mathbb P^*$, observed separately, with no assumption that the marginals are independent. This is the situation of asynchronous measurements or records with many missing entries: the joint law cannot be learned, yet a valid uncertainty set can still be built. The set is a box whose sides are order statistics, and its guarantee rests on an elementary binomial test (David and Nagaraja, Order Statistics, §7.1) and a Value-at-Risk bound of Embrechts, Höing and Juri (Finance Stoch. 7, 2003).

Setting

Let $\mathbb P^*$ be a probability measure on $\mathbb R^d$ whose support lies in a known box $[\hat{\mathbf u}^{(0)},\hat{\mathbf u}^{(N+1)}]=\{\mathbf u:\hat u^{(0)}_i\le u_i\le\hat u^{(N+1)}_i\}$. Fix a violation level $0<\epsilon<1$ and a significance level $0<\alpha<1$.

The Value at Risk of $\tilde{\mathbf u}^T\mathbf v$ under a probability measure $\mathbb P$ is

$$\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge1-\epsilon\},$$

and the support function of a set $\mathcal U$ is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u$. A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ if for every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ and every $\mathbf x^*$, $f(\mathbf u,\mathbf x^*)\le0$ for all $\mathbf u\in\mathcal U$ implies $\mathbb P^*(f(\tilde{\mathbf u},\mathbf x^*)\le0)\ge1-\epsilon$.

From a sample $\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N$ let $\hat u^{(j)}_i$, $1\le j\le N$, be the $j$-th order statistic (the $j$-th smallest value) of coordinate $i$, and let $\hat u^{(0)}_i,\hat u^{(N+1)}_i$ be the box ends. The index $s$ is

$$s=\min\Big\{k\in\mathbb N:\sum_{j=k}^N\binom Nj(\epsilon/d)^{N-j}(1-\epsilon/d)^j\le\frac{\alpha}{2d}\Big\},\qquad s=N+1\text{ if the set is empty}, \tag{26}$$

and the uncertainty set is the box

$$\mathcal U^M_\epsilon=\{\mathbf u\in\mathbb R^d:\hat u^{(N-s+1)}_i\le u_i\le\hat u^{(s)}_i,\ i=1,\dots,d\}. \tag{28}$$

The confidence region $\mathcal P^M$ is the set of probability measures on the box with $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(\mathbf e_i)\le\hat u^{(s)}_i$ and $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ for every $i$.

Formalization targets

Goal: Theorem 7

If $N-s+1<s$, then with probability at least $1-\alpha$ over the sample ($N$ samples of each marginal of $\mathbb P^*$, each marginal's samples i.i.d., arbitrary dependence across marginals),

$$\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)\qquad\text{for all }\mathbf v\in\mathbb R^d,$$

and, for every sample, $\mathcal U^M_\epsilon$ is nonempty, convex and compact with

$$\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)=\sum_{i=1}^d\max\big(v_i\hat u^{(N-s+1)}_i,\,v_i\hat u^{(s)}_i\big). \tag{29}$$

Milestones

1. Positive homogeneity: $\mathrm{VaR}^{\mathbb P}_\delta(c\mathbf w)=c\,\mathrm{VaR}^{\mathbb P}_\delta(\mathbf w)$ for $c>0$ (p. 10).
2. Each one-sided order-statistic test is valid at level $\alpha/(2d)$: $\mathbb P^*_{\mathcal S}(\hat u^{(s)}_i<\mathrm{VaR}^{\mathbb P^*}_{\epsilon/d}(\mathbf e_i))\le\alpha/(2d)$, and the mirror bound for $-\mathbf e_i$ with $\hat u^{(N-s+1)}_i$ (pp. 20–21).
3. Union bound: $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P^M)\ge1-\alpha$ (p. 21).
4. The weak Embrechts bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_i\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(v_i\mathbf e_i)$ for every probability measure $\mathbb P$ (p. 21).
5. If $N-s+1<s$ then $\hat u^{(N-s+1)}_i\le\hat u^{(s)}_i$ (p. 21).
6. (EC.8): for $\mathbb P\in\mathcal P^M$, $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_{v_i>0}v_i\hat u^{(s)}_i+\sum_{v_i\le0}v_i\hat u^{(N-s+1)}_i$ (p. ec5).
7. (29) as a standalone statement (p. 21).

Significance

Theorem 7 gives an uncertainty set with a finite-sample guarantee from data that carry no information on the dependence between coordinates. The set is a box, so the robust counterpart of a linear constraint is again linear, and Remark 12 of the paper notes that separation over $\{(\mathbf v,t):\delta^*(\mathbf v\mid\mathcal U^M)\le t\}$ is in closed form. Unlike the other confidence regions of the paper (χ², G-test, Kolmogorov–Smirnov, bootstrap), whose coverage is asymptotic, tabulated or approximate, the test here is exact and distribution-free, so the probability statement itself is in scope.

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a complete formal statement of Theorem 7 including the sampling probability, the binomial order-statistic test for a quantile, and the marginal Value-at-Risk bound, all of which are standard tools in nonparametric statistics and risk management that are absent from Mathlib.

Difficulty

The deterministic half, (EC.8) and (29), is short once the weak Embrechts bound is available. The work is in the probabilistic half, which the paper delegates to a textbook citation. Validity of the order-statistic test ties together facts that no library currently connects: the combinatorics of sorted tuples, the binomial law of the number of i.i.d. sample points below a threshold, the behaviour of a quantile at its left limit (the distribution function at the quantile can exceed $1-\epsilon/d$, so the obvious bound uses the wrong probability), and the comparison of binomial tails across success probabilities. The lower-tail test must be handled with the index $N-s+1$ and the quantile of $-\tilde u_i$, where a sign or off-by-one slip produces a false statement that still looks plausible. The boundary regime $s=N+1$, where $\mathcal U^M_\epsilon$ is the a priori box, is valid only because $\mathbb P^*$ lives in that box and needs separate treatment.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with 0-based coordinates; vectors pair by ⬝ᵥ. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ applied to $\mathbf u\mapsto\mathbf u^T\mathbf v$, and the support function is the published RobustMDP.Shared.supportFunction; both are real infima/suprema, genuine under $0<\epsilon<1$, a probability measure, and a nonempty bounded set (the goal proves the latter). The order statistics use Mathlib's Tuple.sort; the index $N-s+1$ is N + 1 - s in natural numbers, which is the paper's value since $1\le s\le N+1$.

The data are an array S : Fin N → Fin d → ℝ, S k i the $k$-th sample of marginal $i$, under any probability law Q such that, for each $i$, the samples S 0 i, …, S (N-1) i are i.i.d. from the $i$-th marginal of $\mathbb P^*$ (IsMarginalSampleLaw). The dependence between samples of different marginals is left arbitrary, as the paper's asynchronous setting requires; i.i.d. draws of whole vectors are one admissible law. Probabilities of possibly non-measurable events are outer measures. The level $\epsilon$ is fixed: by Remark 11 the family $\{\mathcal U^M_\epsilon\}$ need not work for all $\epsilon$ simultaneously.

The guarantee is stated in the criterion form of Theorem 1(a) of the paper: $\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)$ for all $\mathbf v$, together with nonemptiness, convexity and compactness of $\mathcal U^M_\epsilon$. Theorem 1 (mission I of this series) shows that for such sets this criterion is equivalent to implying a probabilistic guarantee. The coverage of the test is proved, not assumed: there is no hypothesis that $\mathbb P^*\in\mathcal P^M$. A formalization in which the support function is evaluated on an empty or unbounded set, where the library value is 0, would make the criterion trivial; the nonemptiness and compactness conjunct of the goal rules it out.

Standing assumptions: $d\ge1$, $0<\epsilon<1$, $0<\alpha<1$, $\hat{\mathbf u}^{(0)}\le\hat{\mathbf u}^{(N+1)}$, $\mathbb P^*$ a probability measure with $\mathbb P^*$-null complement of the box, and Theorem 7's hypothesis $N-s+1<s$. The page prints the second condition of $\mathcal P^M$ as "$\mathrm{VaR}^{\mathbb P_i}_{\epsilon/d}\ge\hat u^{(N-s+1)}_i$"; the formal region uses the lower-tail condition $\mathrm{VaR}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ that the hypothesis, its rejection rule and the proof use. (EC.8) is stated with "$\le$" for each $\mathbb P\in\mathcal P^M$; the page's middle equality is not claimed.

Reusable infrastructure welcome beyond this mission: order statistics of tuples and the binomial law of threshold counts for i.i.d. samples; monotonicity of binomial tails in the success probability; the left-limit property of quantiles; the Embrechts-type subadditivity bound for Value at Risk.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• H. A. David, H. N. Nagaraja, Order Statistics, Wiley (cited by the paper as 1970; third edition 2003), §7.1, distribution-free confidence intervals for quantiles. https://doi.org/10.1002/0471722162
• P. Embrechts, A. Höing, A. Juri, Using copulae to bound the Value-at-Risk for functions of dependent risks, Finance and Stochastics 7:145–167, 2003. https://doi.org/10.1007/s007800200085

Motivation

A robust linear constraint $u^\top v \le t$ with $u$ ranging over an uncertainty set $\mathcal U\subseteq\mathbb R^d$ is tractable whenever the support function $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ is. Robust optimization gains a probabilistic meaning when $\mathcal U$ is chosen so that every robustly feasible decision also satisfies the constraint with probability at least $1-\varepsilon$ under the true distribution $\mathbb P^*$ of the uncertain parameter $\tilde u$. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region $\mathcal P$ of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over $\mathcal P$.

Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set $\mathcal U^{FB}_\varepsilon$ of Theorem 6, whose support function has a closed form.

Setting

The uncertain parameter $\tilde u$ takes values in $\mathbb R^d$ and $\mathbb P$ is its law. For $\varepsilon\in(0,1)$ and $v\in\mathbb R^d$, the Value at Risk is

$$\mathrm{VaR}^{\mathbb P}_\varepsilon(v)=\inf\{t:\mathbb P(\tilde u^\top v\le t)\ge1-\varepsilon\}.$$

For a probability measure $\mathbb P_i$ on $\mathbb R$ with mean $\mu_i$, the forward deviation and the backward deviation are

$$\sigma_f(\mathbb P_i)=\sup_{x>0}\sqrt{-\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{x\tilde u_i}]},\qquad\sigma_b(\mathbb P_i)=\sup_{x>0}\sqrt{\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{-x\tilde u_i}]}.$$

From a sample, a bootstrap produces thresholds $t_i$, $\bar\sigma_{fi}$, $\bar\sigma_{bi}$. With the sample mean $\hat\mu_i$ put $m_{bi}=\hat\mu_i-t_i$ and $m_{fi}=\hat\mu_i+t_i$. The confidence region $\mathcal P^{FB}$ consists of the distributions of vectors with independent components $\tilde u_i\sim\mathbb P_i$, each $\mathbb P_i$ having bounded support, mean in $[m_{bi},m_{fi}]$, $\sigma_f(\mathbb P_i)\le\bar\sigma_{fi}$ and $\sigma_b(\mathbb P_i)\le\bar\sigma_{bi}$.

The uncertainty set is

$$\mathcal U^{FB}_\varepsilon=\Big\{y_1+y_2-y_3:\ y_2,y_3\in\mathbb R^d_+,\ \sum_{i=1}^d\Big(\frac{y_{2i}^2}{2\bar\sigma_{fi}^2}+\frac{y_{3i}^2}{2\bar\sigma_{bi}^2}\Big)\le\log(1/\varepsilon),\ m_{bi}\le y_{1i}\le m_{fi}\Big\}.$$

Formalization targets

Goal: Theorem 6

For $m_b\le m_f$, $\bar\sigma_f,\bar\sigma_b>0$ and $\varepsilon\in(0,1)$, the set $\mathcal U^{FB}_\varepsilon$ is nonempty, convex and compact,

$$\delta^*(v\mid\mathcal U^{FB}_\varepsilon)=\sum_{i:v_i\ge0}m_{fi}v_i+\sum_{i:v_i<0}m_{bi}v_i+\sqrt{2\log(1/\varepsilon)\Big(\sum_{i:v_i\ge0}\bar\sigma_{fi}^2v_i^2+\sum_{i:v_i<0}\bar\sigma_{bi}^2v_i^2\Big)}\qquad(24)$$

for every $v$, and $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)$ is at most the right-hand side of (24) for every $\mathbb P\in\mathcal P^{FB}$ and every $v$.

Milestones

1. The Chen–Sim–Sun bound (22): for independent components with known means $\mu_i$ and deviations, $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\sum_i\mu_iv_i+\sqrt{2\log(1/\varepsilon)(\sum_{v_i<0}\sigma_{bi}^2v_i^2+\sum_{v_i\ge0}\sigma_{fi}^2v_i^2)}$.
2. The right-hand side of (24) is the worst case of (22) over the parameters allowed by $\mathcal P^{FB}$.
3. Lagrangian strong duality for $\max_{u\in\mathcal U^{FB}_\varepsilon}u^\top v$.
4. The three one-dimensional sub-subproblems and their optimal values.
5. The combined formula: $\delta^*$ equals a linear term plus $\inf_{\lambda>0}\{\lambda\log(1/\varepsilon)+S/(2\lambda)\}$.
6. $\inf_{\lambda>0}\{\lambda L+S/(2\lambda)\}=\sqrt{2LS}$, attained at $\lambda^*=\sqrt{S/(2L)}$ when $S>0$.

Companions

• Remark 9: when (24) exceeds $t$, an explicit point of $\mathcal U^{FB}_\varepsilon$ gives a violated cut $u^\top v\le t$.
• Theorem 13(b): the constraint $\delta^*(v\mid\mathcal U^{FB}_\varepsilon)\le t$ is convex in $(v,t)$ and convex in $\varepsilon$ for $0<\varepsilon<1/\sqrt e$.

Significance

Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level $\varepsilon$ for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, $\mathcal U^{FB}_\varepsilon$ needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels $\varepsilon_j$ across several constraints.

The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values $v_i\bar\sigma^2/(2\lambda)$, which should be $v_i^2\bar\sigma^2/(2\lambda)$, and the bound $m_b\le y_1\le m_b$). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.

Difficulty

The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over $\mathcal P^{FB}$ is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of $v_i$. The Value at Risk bound needs independence of the components; without it (22) fails. When $v=0$ or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.

Formalization scope

Vectors are Fin d → ℝ, with 0-based coordinates; $\tilde u^\top v$ is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\varepsilon$, and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of $\mathcal U^{FB}_\varepsilon$, so the supremum is a true maximum and cannot hold through the value $0$ of an empty or unbounded set.

The statement is formalized in the criterion form: $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\delta^*(v\mid\mathcal U^{FB}_\varepsilon)$ for all $v$ and every $\mathbb P$ in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability $1-\alpha$ with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.

Conventions and added hypotheses:

• $\bar\sigma_{fi},\bar\sigma_{bi}>0$, so that the denominators of (23) are genuine; with $\bar\sigma=0$ Lean's $x/0=0$ would leave $y_2$ unconstrained instead of forcing $y_2=0$.
• $m_b\le m_f$, which holds because $t_i\ge0$.
• The region is built from a product measure (independence) of probability measures with bounded support. These are the hypotheses of Theorem 6 on $\mathbb P^*$ and the section's standing assumption; the page's set-builder for $\mathcal P^{FB}$ omits independence. Without bounded support, the Bochner integral of a non-integrable exponential is $0$ in Lean and the deviation conditions would lose their meaning.
• "$\sigma_f(\mathbb P_i)\le\bar\sigma$" is the predicate "the expression under the root is at most $\bar\sigma^2$ for every $x>0$", which is equivalent and avoids an unbounded supremum.
• Dual minimisations over $\lambda\ge0$ are infima over $\lambda>0$, stated with IsGLB.

A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about $0$.

The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

Motivation

A robust linear constraint $f(\mathbf u,\mathbf x)\le 0$ for all $\mathbf u\in\mathcal U$ replaces an uncertain parameter $\tilde{\mathbf u}$ by a deterministic uncertainty set $\mathcal U\subseteq\mathbb R^d$. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets directly from data. Their requirement is a probabilistic guarantee: every robust-feasible decision should satisfy the constraint with probability at least $1-\epsilon$ under the true distribution $\mathbb P^*$, and this should hold with probability at least $1-\alpha$ over the sample. The construction runs a statistical hypothesis test, takes its confidence region of distributions, and turns the worst-case Value at Risk over that region into a set.

This mission covers the case where $\mathbb P^*$ may be continuous but its $d$ coordinates are known to be independent and supported in a known box (§5.1 of the paper). The test is the classical Kolmogorov–Smirnov (KS) goodness-of-fit test, applied separately to each marginal. The result is a convex set $\mathcal U^I_\epsilon$ whose support function has a one-dimensional closed form, (19). The set is representable with exponential cones, and a line search over a single multiplier separates over it (Remarks 6–7).

Setting

Let $d\ge 0$ and $N\ge 1$ (the sample size). For each coordinate $i$ we are given points $\hat u^{(0)}_i<\hat u^{(1)}_i<\cdots<\hat u^{(N)}_i<\hat u^{(N+1)}_i$. The interval $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ is the known box containing the support, and $\hat u^{(1)}_i,\dots,\hat u^{(N)}_i$ are the order statistics of the $i$-th coordinates of the data. Let $\Gamma=\Gamma^{KS}\in(0,1)$ be the KS threshold and $0<\epsilon<1$.

• The Value at Risk of $\mathbb P$ in direction $\mathbf v$ is $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^{\mathsf T}\mathbf v\le t)\ge 1-\epsilon\}$.
• The support function of a set is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^{\mathsf T}\mathbf u$.
• The KS region $\mathcal P^{KS}_i$ is the set of Borel probability measures $\mathbb P_i$ on $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ with $\mathbb P_i(\tilde u_i\le\hat u^{(j)}_i)\ge j/N-\Gamma$ and $\mathbb P_i(\tilde u_i<\hat u^{(j)}_i)\le (j-1)/N+\Gamma$ for $j=1,\dots,N$.
• The independent region $\mathcal P^I$ is the set of product measures $\prod_i\mathbb P_i$ with $\mathbb P_i\in\mathcal P^{KS}_i$.
• The vectors $q^L(\Gamma),q^R(\Gamma)\in\Delta_{N+2}$ of (17) are the two boundary distributions of the KS band. With $k=\lfloor N(1-\Gamma)\rfloor$, $q^L$ puts mass $\Gamma$ at $j=0$, mass $1/N$ at $j=1,\dots,k$, and mass $1-\Gamma-k/N$ at $j=k+1$. Its mirror image is $q^R_j=q^L_{N+1-j}$.
• The relative entropy is $D(\mathbf q,\mathbf p)=\sum_jq_j\log(q_j/p_j)$.
• The uncertainty set (18) is

$$\mathcal U^I_\epsilon=\Big\{\mathbf u:\exists\,\theta_i\in[0,1],\ \mathbf q^i\in\Delta_{N+2},\ \sum_{j=0}^{N+1}\hat u^{(j)}_iq^i_j=u_i,\ \sum_{i=1}^dD\big(\mathbf q^i,\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R\big)\le\log(1/\epsilon)\Big\}.$$

Formalization targets

Goal: Theorem 5 (deterministic content)

For every $\mathbf v\in\mathbb R^d$:

$$\mathcal U^I_\epsilon\ \text{is nonempty, convex and compact},\qquad \mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)\ \ \forall\,\mathbb P\in\mathcal P^I,$$ $$\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)=\inf_{\lambda>0}\Big\{\lambda\log(1/\epsilon)+\lambda\sum_{i=1}^d\log\Big[\max\Big(\sum_{j}q^L_je^{v_i\hat u^{(j)}_i/\lambda},\sum_jq^R_je^{v_i\hat u^{(j)}_i/\lambda}\Big)\Big]\Big\}.\tag{19}$$

Milestones, in attack order

1. The Nemirovski–Shapiro bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\lambda\log(1/\epsilon)+\lambda\sum_i\log\mathbb E^{\mathbb P_i}[e^{v_i\tilde u_i/\lambda}]$ for independent, compactly supported marginals.
2. The boundary laws $q^L$, $q^R$ belong to $\mathcal P^{KS}_i$.
3. Theorem EC.2: for monotone $g$, $\sup_{\mathcal P^{KS}_i}\mathbb E[g(\tilde u_i)]=\max(\sum_jq^L_jg(\hat u^{(j)}_i),\sum_jq^R_jg(\hat u^{(j)}_i))$.
4. (16) combined with EC.2: the Value at Risk over $\mathcal P^I$ is at most the expression in (19), for every $\lambda>0$.
5. The Lagrangian dual of $\max\{\mathbf v^{\mathsf T}\mathbf u:\mathbf u\in\mathcal U^I_\epsilon\}$.
6. (EC.6): $\max_{\mathbf q\in\Delta}\{\mathbf c^{\mathsf T}\mathbf q-D(\mathbf q,\mathbf p)\}=\log\sum_jp_je^{c_j}$.
7. (EC.7): the linear optimization over $\theta_i\in[0,1]$ is solved at an endpoint.

Significance

Theorem 5 gives a data-driven uncertainty set for continuous distributions with independent components. Its guarantee is finite-sample, not asymptotic, and its support function costs one line search over $\lambda$ to evaluate. Theorem 1 of the paper shows that $\mathrm{VaR}\le\delta^*$ for all $\mathbf v$ is equivalent to the probabilistic guarantee for nonempty convex compact sets. So the goal certifies that every robust-feasible solution of a constraint concave in $\mathbf u$ satisfies the chance constraint for every distribution the KS tests cannot reject. Theorem EC.2 is a reusable fact about KS bands: monotone expectations are extremized at the band's two boundary distributions.

The result is proved in the paper, but none of it has been formalized. A formal development would supply:

• worst-case expectations over a KS confidence band;
• the finite Gibbs variational identity with possibly vanishing reference masses;
• a Chernoff-type Value-at-Risk bound for product measures;
• a strong-duality statement for an entropy-constrained convex program.

Difficulty

The obvious route to the VaR bound is a union bound over coordinates. It loses a factor of $d$ in $\epsilon$, which is why the paper uses exponential moments and independence instead. The KS region is infinite dimensional, so the inner supremum of (16) is not a finite linear program. Reducing it to the boundary distributions needs the monotonicity of $u\mapsto e^{v_iu/\lambda}$, and a measure-level comparison of distribution functions against the band. The support-function identity needs strong duality for a jointly convex divergence constraint. The duality holds because $\theta_i\mapsto\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R$ is affine and $D$ is jointly convex. The reference vector can have zero entries (when $N(1-\Gamma)$ is an integer, or in the middle of the band), so the Gibbs step must handle vanishing masses.

Formalization scope

• Data and conventions. Coordinates are Fin d. The points are uhat : Fin d → Fin (N + 2) → ℝ with the page's indices $j=0,\dots,N+1$, and the KS constraints run over j : Fin N, which is the page's $j-1$. The order statistics are data. They are ordered, $\hat u^{(0)}_i\le\hat u^{(1)}_i\le\dots\le\hat u^{(N+1)}_i$ (Monotone (uhat i)), as order statistics of a sample in the box are; ties are allowed.
• Standing assumptions. $N\ge1$, $0<\Gamma<1$ and $0<\epsilon<1$.
• Regions. Measures in $\mathcal P^{KS}_i$ are probability measures on $\mathbb R$ carried by the box, and $\mathcal P^I$ consists of the Measure.pi products of such measures, so independence is built in.
• Relative entropy. $D$ carries an explicit finiteness predicate ($q_j>0\Rightarrow p_j>0$), so Lean's log 0 = 0 cannot make an infinite divergence finite.
• Published definitions. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$, and $\delta^*$ is the published RobustMDP.Shared.supportFunction, a real sSup. The goal proves $\mathcal U^I_\epsilon$ nonempty and compact, so $\delta^*$ is never the junk value $0$ of an empty or unbounded set.
• Infima and the multiplier. Infima over $\lambda$ are over $\lambda>0$ and stated with IsGLB. The page's $\lambda\ge0$ gives the same value.
• Criterion form of the guarantee. The guarantee is stated as $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)$ for all $\mathbb P\in\mathcal P^I$. By Theorem 1 (mission I of this series), this criterion is equivalent to the probabilistic guarantee for nonempty convex compact sets.
• Coverage of the test. The statement "with probability at least $1-\alpha$ over the sample" is the coverage of $\mathcal P^I$. It rests on the distribution-free law of the KS statistic (tables) and on combining $d$ tests at level $1-\sqrt[d]{1-\alpha}$. This part is cited, not formalized.
• Ruled out. The VaR inequality is never checked against a $\delta^*$ that sSup collapses to $0$, and the divergence budget is never relaxed by unguarded logarithms.

Contributions are welcome on any milestone. Milestones 1, 3 and 6 are independent of each other and of the rest; the goal follows from milestones 1–7 together with the convex-analytic facts about $\mathcal U^I_\epsilon$.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17(4):969–996, 2006. https://doi.org/10.1137/050622328
• M. A. Stephens, EDF statistics for goodness of fit and some comparisons, J. Amer. Statist. Assoc. 69(347):730–737, 1974. https://doi.org/10.1080/01621459.1974.10480196
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

Motivation

Hassler Whitney introduced matroids in On the Abstract Properties of Linear Dependence (Amer. J. Math. 57, 1935, doi:10.2307/2371182) to capture what linear dependence among the columns of a matrix and the circuit structure of a graph have in common. One of the central constructions of the paper is duality. For graphs, duality exists only for planar graphs (Whitney, Non-separable and planar graphs, Trans. AMS 34, 1932); for matroids Whitney showed that every matroid has a dual, and that duality has a direct linear-algebra model: the matroid of a subspace of $\mathbb R^n$ and the matroid of its orthogonal complement are duals.

Matroid duality underlies much of combinatorial optimization: the duality between cycles and cuts in graphs, the relation between a linear code and its dual code, the exchange of rank and corank in matroid intersection and partition, and the treatment of network flows as duals of potential problems. Whitney's §§11–13 are where this structure is first defined and where its linear-algebra meaning (Theorem 28) is established.

Setting

A matroid $M$ is a finite set of elements $e_1,\dots,e_n$ with a rank function $r$ on its subsets; equivalently, a family of independent sets, or of bases (maximal independent sets). For a subset $N$ write $\rho(N)$ for its number of elements and

$$n(N) = \rho(N) - r(N)$$

for its nullity; $r(M)$ and $n(M)$ are the rank and nullity of the whole set of elements.

Duality (§11). Let $M$ and $M'$ be matroids and $\sigma$ a one-to-one correspondence between their elements. $M'$ is a dual of $M$ (via $\sigma$) if, for every subset $N$ of $M$, with $N'$ the complement in $M'$ of $\sigma(N)$,

$$r(N') = r(M') - n(N). \tag{11.1}$$

The matroid of a subspace (§12). Let $E_n$ be $n$-dimensional Euclidean space with coordinates $x_1,\dots,x_n$, and let $H$ be a hyperplane through the origin, which in Whitney's usage is a linear subspace of any dimension. For a set $S$ of coordinates, project $H$ onto the coordinate subspace $E'_S$ spanned by the axes $x_i$, $i\in S$. The matroid associated with $H$ has elements $e_1,\dots,e_n$, one per coordinate, and gives the set $\{e_i: i\in S\}$ the rank

$$r_H(S) = \dim \pi_S(H).$$

If $H$ is the row space of a matrix $\mathbf M$, then $r_H(S)$ is the rank of the columns of $\mathbf M$ indexed by $S$, so the associated matroid is the column matroid of $\mathbf M$.

In the Lean development these objects are WhitneyMatroid.Components.nullity (shared), IsDualVia M M' σ, IsDual M M', subspaceRank H S and IsAssociated M H.

Formalization targets

Goal: Theorem 28

Let $H$ be a subspace of $E_n$ and $H' = H^\perp$ its orthogonal complement. If $M$ and $M'$ are the matroids associated with $H$ and $H'$, then $M$ and $M'$ are duals under the correspondence of equal coordinates:

$$\forall N\subseteq\{e_1,\dots,e_n\}:\qquad r_{M'}(\overline N) = r(M') - n_M(N).$$

Milestones

1. Theorem 27. For every subspace $H$ there is exactly one matroid associated with $H$.
2. Theorem 6 (already proved on the platform). All bases have the same number of elements.
3. Theorem 7. $B$ is a base iff $r(B)=r(M)$ and $n(B)=0$.
4. Theorem 8. If $B$ is a base and $N$ is independent, then $N\cup N'$ is a base for some $N'\subseteq B$.
5. Theorem 20. If $M'$ is a dual of $M$, then $r(M') = n(M)$ and $n(M') = r(M)$.
6. Theorem 23. $M'$ is a dual of $M$ via $\sigma$ iff, for every $B$, $B$ is a base of $M$ exactly when the complement of $\sigma(B)$ is a base of $M'$.
7. Theorem 21. Duality is symmetric.
8. Theorem 22. Every matroid has a dual.

Significance

The result. Theorem 28 identifies abstract duality with orthogonal complementation. With Theorem 23 it says that the column matroid of a real matrix whose rows span $H$ and the column matroid of a matrix whose rows span $H^\perp$ have complementary bases. This is the basis of the standard representation of the dual of a represented matroid ($[I_r\mid A]$ and $[-A^{\mathsf T}\mid I_{n-r}]$), of the cycle/cocycle duality of graphs viewed through incidence matrices, and of the fact that a matroid representable over a field has a dual representable over the same field. Theorems 20–23 are the basic facts every later treatment of matroid duality starts from: duality exchanges rank and nullity, is symmetric, always exists, and is characterized by base complements.

Formalizing it. All of these results are classical and proved in Whitney's paper; what this mission adds is a machine-checked development of Whitney's own definition of duality, the rank identity (11.1), rather than the base-complement definition used in modern libraries. Mathlib defines the dual matroid $M^*$ by base complements and proves that it is a matroid; it does not, at the pinned revision, contain the rank formula (11.1) for $M^*$, the matroid of a real subspace, or Theorem 28. Theorem 6 is already proved on the platform and enters as a reference. Theorems 7 and 8 are close to Mathlib lemmas and are footholds rather than new content.

Difficulty

The difficulty of the goal is not in the combinatorics but in the passage between the two descriptions of a subspace. The natural first idea is to compare the ranks $r_H(S)$ and $r_{H^\perp}(\overline S)$ directly by counting dimensions of $H$ and $H^\perp$. This does not close: $r_H(S)$ is the dimension of a projection of $H$ onto coordinates, while $\dim H^\perp = n - \dim H$ only controls $H^\perp$ as a whole, and the rank of a complementary coordinate set in $M'$ is not determined by the dimensions of $H$ and $H^\perp$ alone. Some relation between coordinate projections of $H$ and the structure of $H^\perp$ on the complementary coordinates has to be established. Theorem 27 is itself nontrivial in Lean: the rank function $r_H$ has to be shown to satisfy the matroid axioms, which needs a careful treatment of coordinate projections and of submodularity of dimension. On the abstract side, Theorem 23 needs both directions of the passage between the rank identity and base complements, including the counting step $r(M) + r(M') = \rho(M)$.

Formalization scope

• Matroids are Mathlib Matroid α on a finite type α whose ground set is all of α (Whitney's matroid is its finite set of elements). This finiteness and the ground set convention are part of the definitions; all theorems are stated under them.
• Ranks and nullities. Ranks are Mathlib's eRk, finite on a finite type and converted to integers; the nullity $n(N)=\rho(N)-r(N)$ and the identity (11.1) are computed in $\mathbb Z$. No truncated subtraction appears.
• Duality is Whitney's rank identity (11.1) for every subset, for a fixed bijection σ : α ≃ β (IsDualVia) or some bijection (IsDual). It is deliberately not defined as Mathlib's M✶: with that definition Theorem 23 would be nearly definitional and Theorem 28 would lose the rank identity. A formalization that replaces (11.1) by the base-complement condition, or states Theorem 28 only for bases, is not this mission's goal.
• Euclidean space is EuclideanSpace ℝ (Fin n) with its standard inner product; the orthogonal hyperplane is Hᗮ. The field is $\mathbb R$, as in the paper; the analogous statement over other fields with the dot-product annihilator is a generalization and not part of this mission.
• The associated matroid is a predicate (IsAssociated M H): ground set Fin n, and the rank of every set $S$ of coordinates equals the finrank of the image of $H$ under the coordinate projection onto $S$ (not of $H\cap E'_S$, a different set function). Existence and uniqueness is Theorem 27.
• Implicit hypotheses made explicit: the ground sets are finite and equal to the whole element type; Whitney's "dimension $r$" and "dimension $n-r$" in Theorem 28 are consequences of $H'=H^\perp$ and are not hypotheses. The goal covers $n=0$, $H=\{0\}$ and $H=E_n$.
• Infrastructure needed and reusable: the matroid of a real subspace (equivalently the column matroid of a real matrix), with its rank function in terms of coordinate projections; the rank formula of the dual matroid; the dimension identity relating projections of $H$ and sections of $H^\perp$. All are reusable for the other missions of this series (the Fano matroid and binary matroids) and for any later work on represented matroids. Proofs of the milestones, alternative proofs of Theorem 28 through Mathlib's M✶, and supporting lemmas on coordinate projections are welcome.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011, Chapter 2 (duality). https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• Mathlib, Mathlib.Combinatorics.Matroid (Dual, Rank). https://github.com/leanprover-community/mathlib4

Motivation

Multiechelon inventory theory studies supply systems in which stock is held at several levels: here, a depot that orders from an outside supplier and a retail outlet that is replenished from the depot and faces random customer demand. The question is how much to order and ship in each period so as to minimize expected holding, shortage and ordering costs over an infinite horizon. Clark and Scarf (Management Science, 1960) showed that the finite-horizon problem of a serial system decomposes into single-location problems linked by an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) extended the decomposition to the infinite horizon under discounted and average costs, and then asked what it costs to compute an optimal policy.

In the reduced single-location problem the only nonlinear part of the one-period cost is the expected induced penalty $P^L$. Any algorithm for the reduced problem (Veinott–Wagner type policy computations, for instance) evaluates $P^L$ many times. In general each evaluation is a numerical integral. Section 4 of the paper shows that when demand is normal, $P^L$ has a closed form in the univariate and bivariate standard normal distribution functions. This mission formalizes that closed form, eq. (13) on p. 830.

Setting

Time is discrete. One-period demand is $u\sim N(\mu,\sigma^2)$ with $\sigma>0$, independent across periods. For $i\ge1$, $u^{(i)}$ is the total demand over $i$ periods. It is normal with mean $\mu^{(i)}=i\mu$ and standard deviation $\sigma^{(i)}=i^{1/2}\sigma$, density $f^{(i)}$ and cdf $F^{(i)}$. The shipment lead time from depot to outlet is $l\ge0$ and the order lead time from the supplier is $L\ge1$. The cost factors are a system-wide holding cost $h^d>0$, a retailer holding cost $h^r>0$ and a retailer shortage penalty $p^r>0$. Write $p^s=h^d+p^r$. Costs are average costs, so the discount factor is $\alpha=1$ throughout.

The retailer's one-period cost (p. 822) is

$$R(x)=-h^d(x-\mu^{(l)})+p^rE[u^{(l+1)}-x]^++(h^d+h^r)E[x-u^{(l+1)}]^+ .$$

The critical number $x^{r*}$ is a global minimizer of $R$ (property (b), p. 824). The induced penalty cost is $P(x)=0$ for $x\ge x^{r*}$ and $P(x)=R(x)-R(x^{r*})$ for $x<x^{r*}$. Its expectation over the order lead time is

$$P^L(x)=E\,P[x-u^{(L)}]\qquad\text{(eq. (10))}.$$

Let $\Phi$ and $\phi$ be the standard normal cdf and density, $\Theta(z)=z\Phi(z)+\phi(z)$, and $\Phi(\xi_1,\xi_2;\rho)$ the cdf of a bivariate normal pair with standard normal marginals and correlation $\rho$. The paper defines (p. 830)

$$\tau_1(x)=-\frac{x-(x^{r*}+\mu^{(L)})}{\sigma^{(L)}},\quad \tau_2(x)=\frac{x-\mu^{(L+l+1)}}{\sigma^{(L+l+1)}},\quad \nu^{r*}=\frac{x^{r*}-\mu^{(l+1)}}{\sigma^{(l+1)}},$$ $$\tau_3(x)=-\frac{x-(x^{r*}+\mu^{(L)})-[\sigma^{(L)}/\sigma^{(l+1)}]^2[x^{r*}-\mu^{(l+1)}]}{\sigma^{(L)}\sigma^{(L+l+1)}/\sigma^{(l+1)}},$$ $$\epsilon_1(x)=\frac{\Phi[\tau_3(x)]\phi[\tau_2(x)]}{\sigma^{(L+l+1)}},\qquad \epsilon_2(x)=\frac{\Phi(\nu^{r*})\phi[\tau_1(x)]}{\sigma^{(L)}},\qquad \iota(x)=\sigma^{(L)}\Theta[\tau_1(x)],$$ $$\kappa(x)=\sigma^{(l+1)}\Theta(\nu^{r*})\Phi[\tau_1(x)]-\{[\sigma^{(L+l+1)}]^2\epsilon_1(x)-[\sigma^{(L)}]^2\epsilon_2(x)\}-[x-\mu^{(L+l+1)}]\,\Phi[\tau_1(x),\tau_2(x);\rho],$$

with $\rho=-\sigma^{(L)}/\sigma^{(L+l+1)}$.

Formalization targets

Goal: eq. (13)

For every real $x$,

$$P^L(x)=p^s\,\iota(x)-(p^s+h^r)\,\kappa(x).$$

This is an exact identity for every admissible parameter value. It holds with no constants left free.

Milestones

The milestones follow the paper's outline of the derivation on pp. 829–831:

1. eq. (11), $R(x)=p^s[\mu^{(l+1)}-x]+(p^s+h^r)\int_{-\infty}^xF^{(l+1)}(t)\,dt-h^d\mu$;
2. eq. (12), $P^L(x)=\int_{x-x^{r*}}^\infty[R(x-t)-R(x^{r*})]f^{(L)}(t)\,dt$;
3. eq. (14), $P^{L\prime}(x)=-p^s\Phi[\tau_1(x)]+(p^s+h^r)\int_{x-x^{r*}}^\infty F^{(l+1)}(x-t)f^{(L)}(t)\,dt$;
4. eq. (15), the same derivative with the integral replaced by $\Phi[\tau_1(x),\tau_2(x);\rho]$;
5. $P^L(x)\to0$ as $x\to\infty$, hence $P^L(x)=-\int_x^\infty P^{L\prime}(t)\,dt$;
6. $\iota'(x)=-\Phi[\tau_1(x)]$ and $\iota(x)\to0$;
7. the two conditional-normal identities, which give $\Phi[\tau_3(x)]$ and $\Phi(\nu^{r*})$;
8. $\frac{d}{dx}\Phi[\tau_1(x),\tau_2(x);\rho]=\epsilon_1(x)-\epsilon_2(x)$;
9. and 10. the formulas for $\epsilon_1'$ and $\epsilon_2'$;
10. $\kappa'(x)=-\Phi[\tau_1(x),\tau_2(x);\rho]$ and $\kappa(x)\to0$.

Two side remarks of p. 830 are also included: $\Theta'=\Phi$, and the simplified form of $\tau_3$.

Significance

The result. Under normal demand, (13) replaces the numerical integral (12) with a few evaluations of $\Phi$, $\phi$ and the bivariate normal cdf, all available in standard numerical libraries. Together with the decomposition results of Sections 1–3 of the paper, it makes the policy computation for the two-echelon system with normal demand no harder than a single-location computation with an explicit cost function. The same functions reappear in the paper's Section 5 for several retail outlets, after a reinterpretation of $\sigma^{(l+1)}$.

Formalizing it. The paper proves (13) only in outline: it calls the derivation "an elementary integration problem, but … sufficiently involved to warrant an outline" and leaves "tedious algebra" and "more algebra" to the reader. A machine-checked proof turns that outline into a complete argument, including the analytic steps the outline passes over: differentiation under the integral sign, the limits at $+\infty$, and the identification of an integral of normal densities with a bivariate normal probability. To our knowledge no formal proof of (13) exists, and no bivariate normal distribution function is on the platform yet.

Difficulty

The obvious approach is to substitute (11) into (12) and integrate. The result is a double integral of normal densities over a region bounded by a line, and it does not reduce to univariate functions. The paper's route is to differentiate first, identify the derivative (14) as a probability for the correlated pair $(u^{(L)},u^{(L)}+u^{(l+1)})$, and then recover $P^L$ by integrating from $+\infty$. That route needs three things: justification for differentiating under the integral in (12), whose integrand has a kink at $t=x-x^{r*}$; control of the limits at $+\infty$; and the conditional-normal identities, which involve conditioning on a null event and so must be handled through densities. The verification of $\kappa'$ is a long computation with $\Theta$, $\epsilon_1$ and $\epsilon_2$, in which every constant matters.

Formalization scope

Everything lives in the namespace FZEchelon.NormalDemand. The model data form the structure Data (fields $\mu,\sigma,h^d,h^r,p^r,l,L,x^{r*}$). The law of $u^{(i)}$ is the platform's normal demand law InventoryControl.newsboyDemand with mean $i\mu$ and standard deviation $\sqrt i\,\sigma$. Expectations are Bochner integrals, and improper integrals are set integrals over Set.Ioi/Set.Iic. $\Phi$ is cdf (gaussianReal 0 1). The bivariate cdf is the iterated integral of the explicit bivariate density over a lower-left quadrant (meaningful for $|\rho|<1$; here $\rho\in(-1,0)$). Derivatives are HasDerivAt and limits are Tendsto … atTop (𝓝 0).

Standing hypotheses of every theorem: $\sigma>0$; $h^d,h^r,p^r>0$ (p. 821); $L\ge1$; and $x^{r*}$ minimizes $R$. Two of these are added to the page and disclosed. $\sigma>0$ is needed because every $\tau$ divides by some $\sigma^{(i)}$. $L\ge1$ is needed because $\sigma^{(0)}=0$, and the paper treats zero order lead time separately (p. 819). Demand is exactly normal, as in §4, which acknowledges that this violates $u\ge0$ and ignores the objection. No nonnegativity, truncation or approximation enters. The goal fixes $\alpha=1$, the average-cost case the section restricts to. The discounted analogue is not part of this mission.

A trivializing formalization is ruled out: every Bochner integral in the statements has an integrable integrand, since integrands grow at most linearly and the normal law has all moments. No division by a zero standard deviation can occur under the hypotheses. A sorry-free check in the workspace shows that all hypotheses hold together, with a minimizer $x^{r*}$ of $R$ proved to exist.

Needed infrastructure: properties of gaussianReal (moments, convolution of independent normals), differentiation of parametric integrals, and a bivariate normal distribution function with its partial derivatives. A reusable treatment of the bivariate normal cdf, linking the density form used here to Mathlib's multivariateGaussian, would be a contribution of independent value. Proofs of individual milestones are welcome in any order.

Selected references

• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525