Probability

Motivation

Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.

Timeline

• 1963. Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show any norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
• 1981. Beck and Fiala (Discrete Appl. Math.) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
• 1980s. Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's Ten Lectures (1987) as the central open problem of the area.
• 1985. Spencer (Trans. AMS) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
• 1998. Banaszczyk (Random Struct. Algorithms) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
• 2010–2016. The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg (STOC 2016) give a polynomial-time algorithm matching Banaszczyk's bound.
• 2023. Kunisky (SIAM J. Discrete Math.) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
• 2025. Bansal and Jiang (arXiv:2508.03961) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.

Setting

Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A sign vector is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the discrepancy of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The Komlós property at constant $K$ — KomlosBound K — says that every such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.

Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.

Formalization targets

Goal — the Komlós conjecture

$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$

The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.

Milestones — the known ladder

Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.

Significance

The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.

None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.

Difficulty

Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.

Formalization scope

The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads ‖v i‖ ≤ 1); the $\ell^\infty$ conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise $0/1$ hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In beck_fiala the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.

Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.

Selected references

• J. Beck, T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981). doi:10.1016/0166-218X(81)90022-6
• J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985). doi:10.1090/S0002-9947-1985-0784009-0
• W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998). doi link
• N. Bansal, D. Dadush, S. Garg, An algorithm for Komlós conjecture matching Banaszczyk's bound, FOCS 2016 / SIAM J. Comput. arXiv:1605.02882
• N. Bansal, H. Jiang, Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk, 2025. arXiv:2508.03961
• D. Kunisky, The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant, SIAM J. Discrete Math. 37 (2023). arXiv:2111.02974
• B. Chazelle, The Discrepancy Method, Cambridge University Press, 2000. author's page

Why variance-regularized risk bounds

In statistical learning, one picks a function $f$ from a class $\mathcal F$ to make the population risk $\mathbb E[f]$ small, with access only to an i.i.d. sample $x_1,\dots,x_n$ from an unknown distribution $P$. Empirical risk minimization replaces $\mathbb E[f]$ by the empirical mean $\mathbb E_{\widehat P_n}[f]$, and its classical guarantees decay like $1/\sqrt n$ regardless of how concentrated $f$ is. Bernstein-type inequalities show that the deviation of $\mathbb E_{\widehat P_n}[f]$ from $\mathbb E[f]$ scales with the standard deviation of $f$, so a procedure that minimizes "empirical risk plus a standard-deviation penalty" can, in principle, achieve faster rates when the variance at the optimum is small (Maurer and Pontil, 2009). The penalized objective is non-convex even when every $f$ is convex in its parameters, which makes it hard to optimize.

J. C. Duchi and H. Namkoong (arXiv:1610.02581v3, 2017) replace the penalty by a distributionally robust objective: the worst-case risk over all reweightings of the sample within a $\chi^2$-divergence ball. This objective is convex whenever the losses are, and (Theorem 1 of the paper) it equals the empirical mean plus a standard-deviation penalty up to an error of order $1/n$. This mission formalizes the paper's guarantee for the minimizer of that robust objective in terms of localized Rademacher complexities (Section 3.2, Theorem 4), the sharpest of the paper's three generalization analyses. It is the third of four missions on the paper.

Setting

Let $P$ be a probability measure on a measurable space $\mathcal X$ and $x_1,\dots,x_n$, $n\ge1$, an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$. Let $M\ge1$ and let $\mathcal F$ be a collection of measurable functions $f:\mathcal X\to[0,M]$ (losses).

• The $\chi^2$ ball of radius $\rho\ge0$ is the set $\mathcal P_n$ of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$, $\sum_ip_i=1$ and $\frac12\sum_i(np_i-1)^2\le\rho$; equivalently, the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$.
• The robust risk of $f$ is $\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]=\sup_{p\in\mathcal P_n}\sum_ip_if(x_i)$, and a robust minimizer $\widehat f$ minimizes it over $\mathcal F$.
• The empirical Rademacher complexity is $\mathfrak R_n(\mathcal F)=\mathbb E_\varepsilon\big[\sup_{f\in\mathcal F}\frac1n\sum_i\varepsilon_if(x_i)\big]$ with i.i.d. uniform signs $\varepsilon_i\in\{-1,1\}$, and $\mathbb E[\mathfrak R_n(\mathcal F)]$ averages it over the sample.
• A function $\psi:\mathbb R_+\to\mathbb R_+$ is sub-root if it is nonnegative, nondecreasing, and $r\mapsto\psi(r)/\sqrt r$ is nonincreasing on $r>0$.
• The localization inequality (20) asks that, for all $r\ge0$,

$$\psi_n(r)\ \ge\ \mathbb E\big[\mathfrak R_n(\{cf : f\in\mathcal F,\ c\in[0,1],\ \mathbb E[c^2f^2]\le r\})\big],$$

with $\psi_n$ sub-root, and $r_n^\star>0$ is a point with $r_n^\star\ge\psi_n(r_n^\star)$.

Formalization targets

Goal: Theorem 4, inequality (23), as its proof establishes it

Let $0<t<n$ and let $\rho$ satisfy (21): $\frac\rho n\ge8\big(\frac{45M}n\big(t+\log\lceil\log\frac nt\rceil\big)+18r_n^\star\big)$. With probability at least $1-4e^{-t}$, every robust minimizer $\widehat f$ satisfies

$$\mathbb E[\widehat f]\ \le\ \Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\inf_{f\in\mathcal F}\Big(\mathbb E[f]+\sqrt{\tfrac{182\rho}{45n}\mathrm{Var}(f)}\Big)+\Big(14+6\sqrt{\tfrac{2\rho}n}\Big)\frac{M(3\rho+t)}n .$$

Milestones

In attack order: Bousquet's form of Talagrand's inequality (Lemma B.2); the elementary root bound (Lemma D.4); the contraction principle (Lemma D.5, a published theorem); the uniform Bernstein inequality with Rademacher complexity (Lemma D.1); its localized version in terms of $r_n^\star$ (Lemma D.2); localized second-moment bounds (Lemma D.3); the deterministic expansion (10) of Theorem 1,

$$\Big(\sqrt{\tfrac{2\rho}n s_n^2}-\tfrac{2M\rho}n\Big)_+\le\sup_{P}\mathbb E_P[Z]-\mathbb E_{\widehat P_n}[Z]\le\sqrt{\tfrac{2\rho}ns_n^2};$$

and the uniform bound (22): with probability at least $1-2e^{-t}$, for all $f\in\mathcal F$,

$$\mathbb E[f]\le\Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]+\Big(13+4\sqrt{\tfrac{2\rho}n}\Big)\frac{M\rho}n .$$

Significance

The bound (23) says that the robust minimizer competes with the best trade-off between risk and standard deviation in the class, and that the complexity of the class enters only through the fixed point $r_n^\star$ of a localized complexity bound. For bounded VC classes $r_n^\star$ is of order $\frac{d\log(n/d)}n$ (Bartlett, Bousquet and Mendelson, 2005, Corollary 3.7), so when the optimal function has small variance the excess risk is of order $\rho/n$, faster than the $1/\sqrt n$ of uniform covering arguments; and localized complexities apply to classes, such as balls of reproducing kernel Hilbert spaces, whose covering numbers are too large for the covering-number analysis of the paper's Theorem 3 (mission II of this series).

The paper's result is proved, not open. No part of it, and none of the localized-complexity machinery of Bartlett, Bousquet and Mendelson, is formalized in Lean or Mathlib to our knowledge. The mission produces a checked version of the theorem with every constant explicit and, along the way, the localization lemmas D.1–D.3, which are reusable for any localized-complexity analysis. Reading the proof also exposed three arithmetic slips in the printed statements; the mission states what the proof establishes (see Formalization scope).

Difficulty

The obvious route applies a uniform concentration inequality to $\mathcal F$ and then a Bernstein bound to each $f$. Talagrand's inequality applied to the whole class gives a deviation governed by the largest variance in the class and by the global complexity $\mathbb E[\mathfrak R_n(\mathcal F)]$, which yields only $1/\sqrt n$ rates. Obtaining a deviation that scales with each function's own second moment requires peeling the class into shells of comparable second moment and a fixed-point argument on the sub-root bound, with a union bound whose cost appears as $\log\lceil\log\frac nt\rceil$. The two directions of the localized inequalities (population to sample, and sample to population for second moments) must then be combined with the deterministic expansion (10) while keeping the constants explicit. A further subtlety is the self-normalized rescaling $f\mapsto\sqrt{r/(\mathbb E[f^2]\vee r)}\,f$, which differs from the variance normalization of Bartlett et al. and is what makes the bound compatible with the robust objective.

Formalization scope

Lean conventions. The sample is the coordinate map of the product measure $P^n$ on Fin n → X. Distributions on the sample are weight vectors in the $\chi^2$ ball; the robust risk is the real supremum over that ball (attained, since the ball is nonempty and compact for $n\ge1$, $\rho\ge0$). Population means and variances are ∫ x, f x ∂P and ProbabilityTheory.variance f P for measurable bounded $f$; empirical means and variances are normalized by $1/n$. The empirical Rademacher complexity is the published UnderstandingML_Rademacher definition evaluated on $\{(f(x_1),\dots,f(x_n))\}$. Its expectation is a Bochner integral, and every hypothesis that bounds it also asserts that the integrand is integrable: otherwise the integral is $0$, (20) would hold for free, and the theorem would be false. Probability bounds are stated for the failure event under $P^n$ (an outer measure when the event is not measurable). The goal speaks about every minimizer of the robust risk, so it is not vacuous when the set of minimizers is empty. The condition $r_n^\star>0$ is part of the page's "root" (and the proof divides by $\sqrt{r_n^\star}$); with $r_n^\star=0$ allowed, $\psi(r)=\sqrt r$ would remove the complexity term from (21). The condition $t<n$ makes $\log\lceil\log\frac nt\rceil$ defined.

Corrections of printed statements, each recorded in the item's docstring and Formalization Note (the milestone texts stay verbatim):

• (22) is stated with probability $1-2e^{-t}$; the paper prints $1-e^{-t}$, and its proof (p. 41) concludes $1-2e^{-t}$.
• (23) is stated with probability $1-4e^{-t}$ (printed $1-3e^{-t}$; the proof adds two fixed-$f$ events to the two of (22)) and with $\frac{182\rho}{45n}$ (printed $\frac{91\rho}{45n}$; the proof's step $\sqrt\rho+\sqrt t\le\sqrt{91\rho/45}$ multiplies $\sqrt{2\mathrm{Var}(f)/n}$).
• Lemma D.3 is stated with the additive term $72M^2(1+\eta)r_n^\star+(4(1+\eta)+\frac{14}3)\frac{M^2t}n$ and, in the reversed direction, the coefficient $1+\frac1{1+\eta}$, as its proof yields (printed: $\frac{Mt}n(4+\frac73M)$ and $1+\frac\eta{1+\eta}$), under Theorem 4's standing hypothesis $M\ge1$.
• Lemma D.5 is linked to the published contraction lemma UnderstandingML.contraction_lemma, which states it at a fixed sample for nonempty bounded classes and allows a different Lipschitz map per coordinate.

Contributions welcome: proofs of the milestones in any order; Lemma B.2 (Bousquet's inequality) is the deepest single ingredient and is reusable well beyond this mission, as are the peeling Lemma D.1 and the sub-root fixed-point Lemma D.2.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• M. Ledoux and M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

Motivation

Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least $0.95$, a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least $p$.

The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.

Timeline:

• 1959: Charnes and Cooper, individual chance constraints.
• 1971: Prékopa, logarithmic concave measures with application to stochastic programming (Acta Sci. Math. Szeged 32).
• 1973: Prékopa, logarithmic concave measures and functions (Acta Sci. Math. Szeged 34), containing the marginal theorem: marginals of log-concave functions are log-concave.
• 1970s–1980s: nonlinear programming methods for (5.1) (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) combined with Monte Carlo evaluation of $h_0$; the chapter surveys them.

Setting

Let $\xi$ be a random vector in $\mathbb R^q$ on a probability space $(\Omega, \mathcal F, P)$ and let $g_1, \dots, g_r : \mathbb R^n \times \mathbb R^q \to \mathbb R$. The chapter studies problem (5.1):

$$\min h(x) \quad \text{s.t.} \quad h_0(x) = P\bigl(g_1(x,\xi) \ge 0, \dots, g_r(x,\xi) \ge 0\bigr) \ge p, \quad h_1(x) \ge p_1, \dots, h_m(x) \ge p_m .$$

The function $h_0$ is the probability function (chanceProb in Lean). In the special case $g_i(x,y) = T_i x - y_i$ it equals $F(Tx)$, where $F$ is the joint distribution function of $\xi$.

A function $f \ge 0$ is logarithmically concave on a convex set $S$ if

$$f(\lambda u + (1-\lambda) v) \ge f(u)^{\lambda} f(v)^{1-\lambda}, \qquad u, v \in S,\ 0 < \lambda < 1 .$$

Where $f > 0$ this is concavity of $\log f$; the power form also makes sense where $f = 0$. Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.

Section 5.7 introduces the polynomial distribution (5.19) on the cube $0 < z_j \le 1$:

$$F(z_1, \dots, z_n) = \frac{1}{\sum_{i=1}^{N} c_i z_1^{\alpha_{i1}} \cdots z_n^{\alpha_{in}}}, \qquad c_i > 0,\ \alpha_{ij} \le 0,\ \textstyle\sum_j \alpha_{ij} < 0$$

(polyDistF in Lean).

Formalization targets

Goal: Theorem 5.1

If $g_1, \dots, g_r$ are jointly concave on $\mathbb R^{n+q}$ and $\xi$ has a log-concave density $f$ on $\mathbb R^q$, then

$$h_0 \text{ is logarithmically concave on } \mathbb R^n .$$

Its immediate consequence is that the feasible set $\{x : h_0(x) \ge p\}$ is convex for every $p$.

Milestones

1. Theorem 5.2.1: if $h$ is log-concave on the convex set $H = \{h \ge p\}$, $0 < p < 1$, then $h - p$ is log-concave on $H$. This makes the logarithmic penalty function (5.5) of the SUMT method convex.
2. Theorem 5.2.2: under the standing assumptions of §5.2, every interior point $z$ of the feasible set of (5.1) satisfies $h_i(z) > p_i$, $i = 0, \dots, m$.
3. Theorem 5.7.1 (proved content, (5.21)): for $n = 2$ and oppositely ordered exponents, $\partial^2 F / \partial z_1 \partial z_2 \ge 0$ on $(0,1)^2$.
4. Theorem 5.7.2: the polynomial distribution function is log-concave on $(0,1]^n$.

The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.

Significance

Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.

On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.

Difficulty

The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each $g_i$ separately in $x$ and in $y$ is not enough; joint concavity in $(x, y)$ is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.

For Theorem 5.2.2 the naive argument fails at the index $i = 0$: nothing about $h_0$ is assumed directly, and log-concavity of $h_0$ is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.

Formalization scope

$\mathbb R^n$ and $\mathbb R^q$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs $(x, y)$ in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density $f$" is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with $\xi$ and $f$ measurable and $P$ a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint $i = 0$ of Theorem 5.2.2 is stated separately from $h_1, \dots, h_m$. The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.

No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.

Corrections of the printed text, recorded in each item's Formalization Note:

• Theorem 5.1 states the density condition "for every $x_1, x_2 \in \mathbb R^n$"; the density lives on $\mathbb R^q$ and the condition is imposed there.
• (5.19) prints the first factor as $z_i^{\alpha_{i1}}$ and the domain index as $i = 1, \dots, N$; they are read as $z_1^{\alpha_{i1}}$ and $j = 1, \dots, n$.
• Theorem 5.7.1 prints its ordering hypothesis with transposed indices ($\alpha_{11} \le \alpha_{12} \le \dots \le \alpha_{1n}$); following the proof, it is read as: across the $N$ terms the $z_1$-exponents increase and the $z_2$-exponents decrease.
• Theorem 5.7.1 claims "is a probability distribution function"; the book proves only (5.21), and normalization would need $\sum_i c_i = 1$, which is not assumed. The formal statement is (5.21), the mixed derivative as an iterated deriv.

Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of $h_0$, which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.

Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are welcome.

Selected references

• A. Prékopa, "Numerical Solution of Probabilistic Constrained Programming Problems", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 5, pp. 123–139. https://doi.org/10.1007/978-3-642-61370-8
• A. Prékopa, "Logarithmic concave measures with application to stochastic programming", Acta Sci. Math. (Szeged) 32 (1971), 301–316.
• A. Prékopa, "On logarithmic concave measures and functions", Acta Sci. Math. (Szeged) 34 (1973), 335–343.
• A. Charnes and W. W. Cooper, "Chance-constrained programming", Management Science 6 (1959), 73–79. https://doi.org/10.1287/mnsc.6.1.73
• B. L. Miller and H. M. Wagner, "Chance constrained programming with joint constraints", Operations Research 13 (1965), 930–945. https://doi.org/10.1287/opre.13.6.930
• A. Prékopa, Stochastic Programming, Kluwer 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision $\theta$ must satisfy $\theta\in\Theta_\delta$ for a parameter $\delta$ that is not known in advance. Enforcing the constraint for every possible $\delta$ (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of $\delta$, which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of $N$ observed samples $\delta_1,\dots,\delta_N$ and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.

The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction $\varepsilon$ of the uncertainty is bounded by a binomial tail that depends only on $N$ and on the number $d$ of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.

Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.

Setting

Fix a cost vector $c\in\mathbb R^d$, a domain $\Theta\subseteq\mathbb R^d$, a measurable space $\Delta$ of uncertainty instances with a probability $\mathbb P$, and a constraint set $\Theta_\delta\subseteq\mathbb R^d$ for each $\delta\in\Delta$.

• The violation of a decision $\theta$ (Definition 3.1) is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$, the probability that $\theta$ fails the constraint of a fresh instance.
• For a sample $(\delta_1,\dots,\delta_m)$, the scenario program is

$$\min_{\theta\in\Theta}c^T\theta\quad\text{subject to}\quad\theta\in\bigcap_{i=1}^{m}\Theta_{\delta_i}.$$

A solution is a feasible point of least cost. With $m=N$ i.i.d. samples its solution is denoted $\theta^*$; it is a random vector, a function of the sample, and $V(\theta^*)$ is a random variable in $[0,1]$.

• Assumption 3.4 (convexity): $\Theta$ and every $\Theta_\delta$ are convex and closed. Assumption 3.6 (existence and uniqueness): for every $m$ and every sample, the program with $m$ constraints has exactly one solution.
• A constraint is a support constraint (Definition 5.1) if its removal improves the solution. A problem is fully supported (Definition 5.4) if for every $m\ge d$ the program with $m$ constraints has, with probability 1, exactly $d$ support constraints.

Formalization targets

Goal: Theorem 3.7

For $1\le d\le N$ and every $\varepsilon\in[0,1]$, under Assumptions 3.4 and 3.6,

$$\mathbb P^N\{V(\theta^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.$$

The right-hand side is the upper tail of a Beta$(d,N-d+1)$ distribution. The statement leaves $\mathbb P$, $\Theta$ and the constraint family completely unspecified beyond the two assumptions.

Milestones

1. Helly's lemma (Lemma 5.3), referenced from the platform in its $d$-dimensional form.
2. Theorem 5.2: for every $m$ and every sample, a convex scenario program has at most $d$ support constraints.
3. Eq. (5.3): for a fully supported problem with $d=N=2$, $\mathbb P^2\{V(\theta^*)>\varepsilon\}=1-\varepsilon^2$.
4. Eq. (5.2): for fully supported problems, Theorem 3.7 holds with equality.
5. Eqs. (3.5)–(3.6): the bound is the Beta$(d,N-d+1)$ distribution function (a published incomplete-beta identity).
6. Eq. (3.9): $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}\le 2^{d-1}(1-\varepsilon/2)^N\le2^{d-1}e^{-\varepsilon N/2}$.
7. Theorem 3.8: $\mathbb E[V(\theta^*)]\le d/(N+1)$.
8. Theorem 1.3: if $N\ge\frac2\varepsilon(\ln\frac1\beta+d-1)$, then $V(\theta^*)\le\varepsilon$ with probability at least $1-\beta$.

Significance

Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any $d$ and $N$.

The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).

Difficulty

The deterministic part, at most $d$ support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all $\theta$ (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of $V(\theta^*)$, not a union bound, and problems with fewer than $d$ support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general $d$. Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.

Formalization scope

• Decisions live in EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.
• The violation is the real number (P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in $[0,\infty]$ through ENNReal.ofReal.
• The solution $\theta^*$ is a function θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.
• Assumption 3.6 is stated for every $m$ including $m=0$ (a unique minimizer on $\Theta$ itself) and for every sample, as on the page.
• Hypotheses the page leaves implicit are explicit: the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is jointly measurable and θstar is measurable (the book's p. 33 convention); $\varepsilon\in[0,1]$; $d\ge1$.
• A support constraint is one whose removal leaves a feasible point of strictly smaller cost than the solution; the count is a Finset.card over Fin m.
• Theorem 3.8 asserts integrability of $V(\theta^*)$ together with the bound, so it cannot hold through the convention that a non-integrable function integrates to $0$. Theorem 1.3's own sentence omits the assumptions; they are added as in §3.2.1, where it is derived from Theorem 3.7.

A statement in which $\theta^*$ is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 2008. https://doi.org/10.1137/07069821X
• G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102, 2005. https://doi.org/10.1007/s10107-003-0499-y
• G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 2006. https://doi.org/10.1109/TAC.2006.875041
• E. Helly, Über Mengen konvexer Körper mit gemeinschaftlichen Punkten, Jahresbericht der DMV 32, 1923.

Motivation

The random walk Metropolis algorithm is one of the most widely used Markov chain Monte Carlo methods for sampling from a density known up to a constant. Its one tuning parameter is the variance of the Gaussian proposal. If the variance is too small, the chain accepts almost every move but barely moves. If it is too large, it proposes long jumps that are almost always rejected. Practitioners need a rule for choosing it, and the rule has to work in high dimension, where both failure modes are severe.

Roberts, Gelman and Gilks (Ann. Appl. Probab. 7(1), 1997) gave the first rigorous answer for product targets. As the dimension grows, one coordinate of the suitably speeded-up chain converges to a Langevin diffusion. The speed of that diffusion is an explicit function of the proposal scale, and maximising it gives the rule "tune the proposal so that about 23% of proposals are accepted". This rule, and the 2.38/√I scaling behind it, is now standard advice in applied Bayesian statistics.

Setting

Let $f:\mathbb R\to\mathbb R$ be a target density: positive, $C^2$, integrating to one, with $f'/f$ Lipschitz, and satisfying the moment conditions (A1) $\mathbb E_f[(f'/f)^8]<\infty$ and (A2) $\mathbb E_f[(f''/f)^4]<\infty$. Here $\mathbb E_f[g(X)]=\int g(x)f(x)\,dx$. In dimension $n\ge2$ the target is the product density $\pi_n(x)=\prod_{i=1}^n f(x_i)$ on $\mathbb R^n$.

Fix a scale $l>0$ and set $\sigma_n^2=l^2/(n-1)$. The random walk Metropolis chain $X^n=(X^n_0,X^n_1,\dots)$ moves as follows. From $X^n_{m-1}$ it proposes $Y\sim N(X^n_{m-1},\sigma_n^2I_n)$. It sets $X^n_m=Y$ with probability $\alpha(X^n_{m-1},Y)=1\wedge\pi_n(Y)/\pi_n(X^n_{m-1})$, and $X^n_m=X^n_{m-1}$ otherwise. The chain starts from $\pi_n$, which is stationary for it. The speeded-up first coordinate is $U^n_t=X^n_{\lfloor nt\rfloor,1}$ for $t\ge0$.

Let $\Phi$ be the standard normal distribution function, and define the roughness $I=\mathbb E_f[(f'(X)/f(X))^2]$. The speed and the limiting acceptance rate are

$$h(l)=2l^2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big),\qquad a(l)=2\,\Phi\!\Big(-\frac{l\sqrt I}{2}\Big).$$

The Langevin generator is $GV(x)=h(l)\big[\tfrac12V''(x)+\tfrac12(\log f)'(x)V'(x)\big]$. It generates the Langevin diffusion $dU_t=h(l)^{1/2}dB_t+h(l)\frac{f'(U_t)}{2f(U_t)}dt$.

Formalization targets

Goal: Theorem 1.1

As $n\to\infty$,

$$U^n\Rightarrow U,$$

where $\Rightarrow$ denotes weak convergence in the Skorokhod topology, $U_0$ has density $f$, and $U$ is the Langevin diffusion with speed $h(l)$. The limit is asserted to exist. No constants appear in the statement beyond those the model defines.

Milestones: the proof

1. Lemma 2.1. The stationary chain stays in the sets $F_n=\{|R_n-I|<n^{-1/8}\}\cap\{|S_n-I|<n^{-1/8}\}$ up to time $t$ with probability tending to one. Here $R_n$ and $S_n$ are the empirical averages of $((\log f)')^2$ and $-(\log f)''$ over coordinates $2,\dots,n$.
2. Proposition 2.2. $|1\wedge e^x-1\wedge e^y|\le|x-y|$.
3. Lemma 2.3. $\sup_{x\in F_n}\mathbb E|W_n|\to0$, where $W_n$ is the second-order part of the log acceptance ratio.
4. Proposition 2.4. $\mathbb E[1\wedge e^A]=\Phi(\mu/\sigma)+e^{\mu+\sigma^2/2}\Phi(-\sigma-\mu/\sigma)$ for $A\sim N(\mu,\sigma^2)$.
5. Lemma 2.5. $\limsup_n\sup_{x_1}n|\mathbb E[V(Y_1)-V(x_1)]|<\infty$ for $V\in C_c^\infty$.
6. Lemma 2.6. The discrete generator $G_nV(x)=n\,\mathbb E[(V(Y)-V(x))\alpha(x,Y)]$ converges to $GV$ uniformly on $F_n$, for $V\in C_c^\infty$ a function of the first coordinate (stated with bounded $(\log f)'''$, the assumption its proof uses).

Milestones: the optimal-scaling corollary

7. Corollary 1.2 (i). $a_n(l)=\iint\pi_n(x)\alpha(x,y)q_n(x,y)\,dx\,dy\to a(l)$.
8. Corollary 1.2 (ii). $h$ is maximised at $\hat l=2.38/\sqrt I$, with $a(\hat l)=0.23$ and $h(\hat l)=1.3/I$, to the printed precision.

Significance

Theorem 1.1 shows that, run for $n$ times as many steps, the chain in dimension $n$ looks like a fixed one-dimensional diffusion. The algorithm's cost therefore grows linearly in dimension, and its efficiency is measured by the single number $h(l)$. Corollary 1.2 turns this into the 0.234 acceptance-rate heuristic and the $2.38/\sqrt I$ scaling. The same diffusion-limit method has since been applied to the Metropolis-adjusted Langevin algorithm, to Hamiltonian Monte Carlo and to non-product targets.

The theorem is proved on paper; it has no machine-checked proof. A formal development would give the first verified diffusion limit of an MCMC algorithm. It would also yield reusable components: the Metropolis chain on $\mathbb R^n$ as a measurable random mapping, a martingale-problem characterisation of one-dimensional diffusions, and a Gaussian computation (Proposition 2.4) that recurs throughout the optimal-scaling literature.

Difficulty

The obvious approach, a Taylor expansion of the log acceptance ratio, gives a sum of $n-1$ terms of size $1/n$. That sum does not concentrate uniformly over the state space, since the coordinates $2,\dots,n$ are arbitrary. The expansion is controlled only on the sets $F_n$, where the empirical averages $R_n$ and $S_n$ are close to $I$. The limit therefore holds only after showing that the chain rarely leaves $F_n$ over a time horizon of $nt$ steps. A pointwise law of large numbers is not enough for that, because the bound has to survive a union over $nt$ steps. Passing from generator convergence on a set of high probability to weak convergence of processes requires the Ethier–Kurtz convergence theory: a core for the limit generator, and convergence of processes that are not themselves Markov. None of this theory is in Mathlib.

Formalization scope

All declarations live in the namespace Roberts1997.RWM. The following conventions are fixed.

• Vectors are Fin n → ℝ, and the paper's first coordinate $x_1$ is index 0. Its coordinates $2,\dots,n$ are the indices i ≠ 0.
• $\sigma_n^2=l^2/(n-1)$ is computed in $\mathbb R$. All statements concern $n\ge2$ or large $n$.
• $l>0$ is assumed. The paper leaves it implicit, but $h(-l)\ne h(l)$.
• "$f$ is a density" is read as $\int f=1$. The moment conditions are read as integrability of $(f'/f)^8f$ and $(f''/f)^4f$. The standing assumption "$f'/f$ is Lipschitz" (p. 111) is carried by every statement.
• The chain is built as a random mapping on an explicit probability space: $x_0\sim\pi_n$, with i.i.d. standard normal innovations and uniform acceptance variables. Theorem 1.1's initial condition (components i.i.d. $f$, shared across dimensions) is read as "the $n$-th chain starts from $\pi_n$", since weak convergence depends only on the law of each $U^n$.
• "$U$ satisfies the Langevin SDE" is read as "the law of $U$ solves the martingale problem for $G$ on $C_c^\infty$, with continuous paths and initial law $f(x)\,dx$". This is equivalent by Ethier–Kurtz (1986), Ch. 5, Prop. 3.1 and Thm 3.3, and follows the platform definition EthierKurtz_IsContinuousDiffusionLaw.
• "$U^n\Rightarrow U$" is read as the existence of an almost-sure coupling in which càdlàg copies of the $U^n$ converge to a continuous Langevin path uniformly on compact time intervals. For a continuous limit this is equivalent to weak convergence in $D_{\mathbb R}[0,\infty)$, by Skorokhod's representation theorem and Ethier–Kurtz Ch. 3, Thm 1.8, Prop. 5.3 and Prop. 7.1. It follows the platform encoding of Ethier–Kurtz Theorem 7.4.1.
• "$\sup\to0$" and "$\limsup\sup<\infty$" are stated as eventual uniform bounds. This avoids real suprema, whose value on an unbounded set is a default.
• In Lemma 2.6, "as $d\to\infty$" is a misprint for $n\to\infty$, and "$2f(Ut)$" in (1.2) is read as $2f(U_t)$.
• Corollary 1.2 (ii) is stated for an arbitrary constant $I>0$. "To two decimal places" is read as explicit rounding intervals: $1.3$ is read to one decimal, and all maximisers over $l>0$ are covered.

The goal cannot be satisfied trivially. The limit law $Q$ must exist, and it must be a probability measure whose initial marginal is $f(x)\,dx$, so the zero measure is excluded. The coupled copies must carry exactly the laws of the paths $U^n$, not an arbitrary process with the same one-time marginals.

The statements carry the paper's hypotheses, with one exception. The printed proof of Lemma 2.6 bounds $\sup_z|(\log f)'''(z)|$, which Theorem 1.1 does not assume, and under $C^2$ alone the uniform convergence over $F_n$ claimed by Lemma 2.6 fails (narrow spikes of $(\log f)''$ far out let a positive fraction of the coordinates shift the log acceptance ratio by a constant while $R_n$ and $S_n$ stay close to $I$). Lemma 2.6 is therefore stated with the proof's own assumption, $f\in C^3$ with $(\log f)'''$ bounded, named as an addition. Theorem 1.1 and the other results keep the paper's hypotheses.

A complete development needs several pieces not yet available: path spaces and the Skorokhod topology (or the coupling reading), the martingale problem and its well-posedness for Lipschitz drift, and the Ethier–Kurtz theorem on convergence of generators on sets of high probability. Proofs of the Gaussian milestones (Propositions 2.2 and 2.4, Lemma 2.5) and of Corollary 1.2 (ii) are independent of this infrastructure and are welcome contributions.

Selected references

• G. O. Roberts, A. Gelman, W. R. Gilks, Weak convergence and optimal scaling of random walk Metropolis algorithms, Ann. Appl. Probab. 7(1), 110–120, 1997. https://doi.org/10.1214/aoap/1034625254
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658
• A. Gelman, G. O. Roberts, W. R. Gilks, Efficient Metropolis jumping rules, Bayesian Statistics 5, Oxford University Press, 599–607, 1996.
• G. O. Roberts, J. S. Rosenthal, Optimal scaling for various Metropolis–Hastings algorithms, Statistical Science 16(4), 351–367, 2001. https://doi.org/10.1214/ss/1015346320

Motivation

The continuous-review $(Q, r)$ policy — order a fixed quantity $Q$ whenever the inventory position falls to the reorder point $r$ — is the textbook policy for a single item with random demand and a positive replenishment leadtime (Hadley and Whitin 1963). Its optimal parameters have no closed form, so practice routinely falls back on the deterministic economic order quantity (EOQ) model with backorders, whose optimum is explicit. How much the deterministic model misjudges the stochastic system's cost is therefore a practical question, and before Zheng (1992) it had been studied only numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978).

Zheng's paper answers it analytically. This mission targets its Theorem 3, which brackets the optimal cost of the stochastic model by the optimal cost of the EOQ model with the same parameters.

Setting

Demands arrive at rate $\lambda>0$ and orders arrive after a fixed leadtime $L>0$. Each order costs $K>0$; holding and backorder costs accrue at rates $h>0$ and $p>0$ per unit per unit time. The leadtime demand $D$ is a nonnegative random variable with $E(D)=\lambda L$. The inventory cost rate at inventory position $y$ is the newsvendor cost

$$G(y)=E\big[h(y-D)^+ + p(D-y)^+\big],$$

assumed to attain its minimum at a unique point $y^0$.

For order quantity $Q>0$ and reorder point $r$, the long-run average cost is

$$c(Q,r)=\frac{\lambda K+\int_r^{r+Q}G(y)\,dy}{Q}.$$

Let $r(Q)$ be a reorder point minimizing $c(Q,\cdot)$, and define $H(Q)=G(r(Q))$ for $Q>0$, $H(0)=G(y^0)$, and $C(Q)=c(Q,r(Q))$. The optimal order quantity $Q^*$ minimizes $C$ over $Q>0$, and $C^*=C(Q^*)$. Write $H_0(Q)=H(Q)-G(y^0)$ and

$$C_0(Q)=\frac{\lambda K+\int_0^Q H_0(y)\,dy}{Q},$$

the controllable cost, so that $C(Q)=G(y^0)+C_0(Q)$; $C^*_0=C_0(Q^*)$. The constant $G(y^0)$ is the newsboy cost.

The EOQ model is the same construction with demand constant at $\lambda L$: $G_d(y)=h(y-\lambda L)^+ + p(\lambda L-y)^+$, with functions $H_d$, $C_d$, optimal quantity $Q^*_d=\sqrt{2\lambda K(h+p)/(hp)}$ and optimal cost $C^*_d=C_d(Q^*_d)$.

Formalization targets

Goal: Theorem 3 (p. 97)

$$C^*_0\le\frac{Q^*_d}{Q^*}\,C^*_d,\qquad C^*_d\le C^*\le G(y^0)+\frac{Q^*_d}{Q^*}\,C^*_d.$$

All three inequalities are part of the goal. The weaker remark after the proof, $C^*_d\le C^*\le C^*_d+G(y^0)$, drops the factor $Q^*_d/Q^*$ and is not the goal.

Milestones

1. Eq. (7): $C(Q)=\big(\lambda K+\int_0^Q H(y)\,dy\big)/Q$ for $Q>0$.
2. Eq. (8): $Q>0$ is optimal iff $H(Q)=C(Q)$.
3. Eqs. (13)–(15): $C(Q)=G(y^0)+C_0(Q)$, and $H_0(Q^*)=C_0(Q^*)$.
4. Lemma 6: $A(Q)=QH(Q)-\int_0^QH$ is increasing and convex; $Q=Q^*$ iff $A(Q)=\lambda K$; $Q^*$ increases and $r^*$ decreases in $K$.
5. Eqs. (18), (20): $H_d(Q)=\frac{hp}{h+p}Q$, and $Q^*_d$ is the EOQ optimum.
6. Lemma 8: $\int_0^QH\ge\tfrac12QH(Q)\ge A(Q)\ge\tfrac12QH_0(Q)\ge\int_0^QH_0$, with equalities for deterministic demand.
7. Eq. (22): $G_d(y)\le G(y)$ for all $y$.

Significance

Theorem 3 says that randomness of leadtime demand raises the total optimal cost above the EOQ's, yet the controllable part of that cost — the part the order quantity actually trades off — is smaller than the EOQ's cost, scaled by $Q^*_d/Q^*$. Combined with $Q^*_d\le Q^*$ (Theorem 2 of the paper), the gap $C^*-C^*_d$ is at most the newsboy cost $G(y^0)$, independent of $K$, so the EOQ cost is a good proxy when $K$ is large relative to $G(y^0)$. The same machinery yields the paper's Theorem 5, that using $Q^*_d$ in the stochastic model costs at most $1/8$ more than the optimum.

The result was proved in 1992; no machine-checked proof is known to exist. Formalizing it requires the continuous $(Q,r)$ model as a whole — optimal reorder points, the one-variable reduction through $H$, and the area function $A$ — none of which is in Mathlib. The companion missions of this series formalize Theorems 2, 4 and 5 of the same paper on the same model.

Difficulty

The middle inequality compares minima of two different functions: $C_d\le C$ pointwise follows from Jensen's inequality, but only after the reorder point of each model is chosen optimally, so the comparison has to pass through the definition of $C$ as a minimum over $r$. The outer inequalities depend on Lemma 8, whose proof uses convexity of $H$ and a slope comparison $H'\le H_d'$ (Lemmas 4 and 7). The paper argues these through first and second derivatives of $r(Q)$ and $G$, which exist only when the leadtime demand has a smooth distribution; the formal statements assume no density, so a proof must either avoid derivatives or handle one-sided ones. Existence of optimal reorder points and of $Q^*$ is asserted in the paper without a separate argument.

Formalization scope

Everything lives in the namespace ZhengQR.CostBounds. The machinery (qrCost, reorderPt, idealPt, Hfun, Cfun, Afun, H0fun, C0fun, IsOptQty) is defined for an arbitrary $G:\mathbb R\to\mathbb R$ and instantiated at the stochastic $G$ and at $G_d$. A structure QRModel holds the parameters, the demand distribution $\mu$ (a probability measure on $\mathbb R$) and the standing assumptions.

Conventions committed to:

• Positivity of $\lambda,L,K,h,p$; $D\ge0$ almost surely; $D$ integrable with $E(D)=\lambda L$; $G$ has a unique minimizer (p. 90). No density is assumed.
• $r(Q)$ is a chosen minimizer of $c(Q,\cdot)$ over $\mathbb R$, not a solution of $G(r)=G(r+Q)$; $y^0$ is a chosen minimizer of $G$. Both use junk value $0$ when no minimizer exists, which never happens under the assumptions.
• $H(0)=G(y^0)$; statements about $H$ and $A$ are on $[0,\infty)$, about $c$, $C$, $C_0$ for $Q>0$.
• "Optimal order quantity" means $Q>0$ and $C(Q)\le C(Q')$ for all $Q'>0$; the goal takes any such $Q^*$ and Lemma 6 states that exactly one exists, so the goal is not vacuous.
• $C^*_d$ is $C_d(Q^*_d)$, with $Q^*_d$ the explicit formula (20); milestone 5 proves it is the EOQ optimum. $C^*_0$ is $C_0(Q^*)$, which equals $\min_{Q>0}C_0$ by (13).
• "Increasing" in Lemma 6 is read strictly, as the proof gives. Lemma 8 is stated for $Q\ge0$; "deterministic" means $\mu$ is the Dirac mass at $\lambda L$.

A formalization in which $C^*_d$ were an arbitrary number, or $Q^*$ an arbitrary positive real, would make the goal false or empty; both are tied to the model above.

Needed infrastructure: existence of minimizers of convex coercive functions on $\mathbb R$, differentiation of parametric integrals $\int_{r(Q)}^{r(Q)+Q}G$, and properties of the newsvendor cost (convexity, coercivity, Jensen). Most of it is reusable for any continuous-review inventory model. Proofs of any milestone, and of lemmas the paper uses but this mission does not list (Lemmas 2–5, 7), are welcome.

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• P. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808