Operations Research

Motivation

A variational inequality asks for a point $x$ of a set $K\subseteq\mathbb R^n$ at which a vector field $f$ makes a non-obtuse angle with every feasible direction: $(x'-x)^T f(x)\ge 0$ for all $x'\in K$. It is the common form of the first-order optimality condition of a constrained optimization problem, of complementarity problems in mathematical programming, and of equilibrium conditions in traffic networks and economics. Two generalizations are standard in operations research. In a quasi-variational inequality the constraint set depends on the unknown, $K=K(x)$, as in generalized Nash games where each player's feasible set depends on the other players' choices. In a generalized variational inequality the vector field is set-valued, $y\in f(x)$, as when $f$ is the subdifferential of a nonsmooth convex function.

D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the problem that combines both, the generalized quasi-variational inequality (GQVI), and proved existence theorems for it. Their §5 gives a second route to existence, independent of the set-valued fixed point theory of their §3: a solution is a fixed point of a map built from Euclidean projections, and for single-valued continuous $f$ the Brouwer fixed point theorem produces one. The characterization of solutions as projection fixed points, for the generalized variational inequality, is due to Fang and Peterson (reference [11] of the paper, a 1979 University of Maryland Baltimore County research report). This mission formalizes that projection route.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^Ty$ and norm $\|x\|$. A point-to-set mapping $K$ assigns to each $x\in\mathbb R^n$ a subset $K(x)\subseteq\mathbb R^n$; a point-to-point mapping $f$ assigns a vector $f(x)$.

The GQVI. Given point-to-set mappings $K$ and $f$, $\mathrm{GQVI}(K,f)$ asks for vectors $x$ and $y$ with

$$x\in K(x),\qquad y\in f(x),\qquad (x'-x)^Ty\ge 0\ \text{ for all } x'\in K(x).$$

Such a pair is a solution. For a point-to-point $f$ one takes $y=f(x)$: find $x\in K(x)$ with $(x'-x)^Tf(x)\ge0$ for all $x'\in K(x)$.

Projection. For a set $S$ and a point $z$, the projection $P_S(z)=\operatorname{sol}\min_{x\in S}\|x-z\|$ is the nearest point of $S$ to $z$. For nonempty closed convex $S$ it exists and is unique.

Semicontinuity of point-to-set mappings (Berge). $K$ is upper semicontinuous at $x$ if for every open $G\supseteq K(x)$ there is a neighbourhood $N$ of $x$ with $K(x')\subseteq G$ for $x'\in N$; lower semicontinuous at $x$ if for every open $G$ meeting $K(x)$ there is a neighbourhood $N$ of $x$ with $K(x')\cap G\ne\emptyset$ for $x'\in N$; continuous if both. "On a set $C$" means at every point of $C$, with neighbourhoods relative to $C$.

Formalization targets

Goal: Theorem 5.2 (p. 220)

Let $f$ be continuous on a nonempty compact convex set $C$, and let $K$ be a continuous mapping on $C$ whose values $K(x)$, $x\in C$, are nonempty, closed, convex and contained in $C$. Then there is $x$ with

$$x\in K(x),\qquad (x'-x)^Tf(x)\ge 0\quad\text{for all }x'\in K(x).$$

Milestone: Lemma 5.1 (p. 220)

If $K$ is continuous at $x_0$ and every $K(x)$ is nonempty, closed and convex, then for every $y_0$ the map

$$(x,y)\longmapsto p(x,y)=P_{K(x)}(y)$$

is continuous at $(x_0,y_0)$.

Milestone: Theorem 5.1 (p. 220)

If every $K(x)$ is closed and convex, then for every pair $(x^*,y^*)$

$$(x^*,y^*)\ \text{solves}\ \mathrm{GQVI}(K,f)\iff x^*=P_{K(x^*)}(x^*-y^*)\ \text{and}\ y^*\in f(x^*).$$

The Brouwer fixed point theorem is already on the platform (AGT.brouwer_fixed_point) and is included as a reference item, as is the Hilbert-space nearest-point theorem VectorSpaceOpt.min_distance_convex_set.

Significance

Theorem 5.2 is the existence theorem for quasi-variational inequalities with a moving convex constraint set and a continuous single-valued field, under compactness. With $K$ constant it is the Hartman–Stampacchia theorem (Acta Math. 115 (1966) 271–310), the basic existence result for finite-dimensional variational inequalities, and so it also covers existence of equilibria of generalized Nash games whose shared constraints satisfy the continuity hypotheses. The paper notes that Theorem 5.2 also follows from its Corollary 3.1, which rests on the Eilenberg–Montgomery fixed point theorem; the projection route needs only Brouwer.

Theorem 5.1 matters beyond this existence result: it turns the GQVI into a fixed-point equation, which is the basis of projection algorithms for variational inequalities and of the contraction argument of the paper's Theorem 5.3. Lemma 5.1, continuity of the projection onto a continuously moving closed convex set, is a stability result used throughout parametric optimization.

All three statements were proved in 1982. None has a machine-checked proof on the platform or in Mathlib, which has neither a projection onto a general closed convex set as a function of the set nor any variational inequality. The work of this mission is to formalize the known proofs.

Difficulty

Theorem 5.1 is a direct consequence of the variational characterization of the nearest point of a convex set. The substance lies in Lemma 5.1 and in adapting it to the goal. The projection depends on the set $K(x)$, not only on the point, and continuity of $K$ is a statement about sets, given by two separate semicontinuity conditions that each control only one side of the convergence. Neither alone suffices: upper semicontinuity without lower lets $K(x)$ shrink abruptly and the nearest point jump; lower without upper lets limits of nearest points fall outside $K(x_0)$. The limit points of the projections must also be kept bounded, which needs the nonemptiness near $x_0$.

A second difficulty is that the goal assumes continuity of $K$ only on $C$, with neighbourhoods relative to $C$, while Lemma 5.1 is stated for continuity at a point of $\mathbb R^n$. Applying the lemma to the composite map $x\mapsto P_{K(x)}(x-f(x))$ on $C$ therefore requires either a relative version of the lemma or a reduction; the lemma cannot be quoted verbatim.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) with its Euclidean norm, never the sup-norm space Fin n → ℝ. Point-to-set mappings are functions into Set. The solution predicate is IsGQVISolution K f x y; a point-to-point $f$ enters as fun z => {f z}. Upper and lower semicontinuity are Mathlib's UpperHemicontinuousAt/On and LowerHemicontinuousAt/On; "continuous on $C$" is both, relative to $C$.

The projection is IsProj S z p (nearest-point predicate) and proj S z, which returns a nearest point when one exists and the junk value $z$ otherwise. Theorem 5.1 uses the relational form, so no junk value enters when $K(x^*)=\emptyset$. Lemma 5.1 assumes every $K(x)$ nonempty, closed and convex, so proj is always the true projection there.

Two hypotheses implicit in the paper are explicit:

1. Closed values in Theorem 5.2. The paper uses Berge's definitions, under which upper semicontinuous mappings have compact values, and its proof uses that each $K(x)$ is closed. The Lean statement assumes $K(x)$ closed for $x\in C$; without it the theorem is false ($C=[0,1]$, $K(x)\equiv(0,1)$, $f\equiv1$).
2. Nonempty values in Lemma 5.1. The projection function $p(x,y)=P_{K(x)}(y)$ is defined only for nonempty $K(x)$; the Lean statement assumes $K(x)\ne\emptyset$ for all $x$.

A formalization in which the projection is merely "some point of $K(x)$", or ignores the distance, would make the reverse direction of Theorem 5.1 false and Lemma 5.1 meaningless; a GQVI whose test points range over $C$ instead of $K(x)$ would turn Theorem 5.2 into a plain variational inequality on $C$. Both are excluded by the definitions above.

A complete development needs the nearest-point characterization on closed convex sets (available in Mathlib and on the platform), sequential characterizations of upper and lower hemicontinuity for closed-valued mappings in $\mathbb R^n$, continuity of the projection onto a moving convex set, and Brouwer's theorem (a platform reference). The hemicontinuity lemmas and the projection-continuity lemma are reusable for the other missions of this series and for parametric optimization in general. Proofs of Lemma 5.1 and Theorem 5.1, a relative-to-$C$ version of Lemma 5.1, and a proof of Brouwer's theorem are all welcome.

Selected references

• D. Chan and J. S. Pang, The generalized quasi-variational inequality problem, Mathematics of Operations Research 7(2) (1982) 211–222. https://doi.org/10.1287/moor.7.2.211
• S. C. Fang and E. L. Peterson, Generalized variational inequalities, Mathematics Research Report No. 79-10, Department of Mathematics, University of Maryland Baltimore County, October 1979 (cited by Chan and Pang as [11]; no online copy).
• P. Hartman and G. Stampacchia, On some non-linear elliptic differential-functional equations, Acta Mathematica 115 (1966) 271–310. https://doi.org/10.1007/BF02392210
• C. Berge, Topological Spaces, The Macmillan Company, New York, 1963 (definitions of upper and lower semicontinuity of point-to-set mappings).

Motivation

Infinite-horizon optimal control problems with nonnegative costs (Strauch's negative dynamic programming, the positive-cost counterpart of Blackwell's positive model) are among the settings where the standard tools of discounted dynamic programming fail: there is no contraction, costs may be infinite, and the value-iteration algorithm started from zero may converge to the wrong limit. Strauch showed in 1966 that under these assumptions the limit of value iteration can lie strictly below the optimal cost (Strauch 1966). Bertsekas (1977) recast the deterministic, stochastic and minimax versions of these problems as one abstract problem about a monotone mapping $H$, and proved Bellman's equation, optimality criteria for stationary policies, and conditions for convergence of the dynamic programming algorithm at that level of generality (Bertsekas 1977). This framework became the basis of the "abstract dynamic programming" theory developed later in Bertsekas and Shreve (1978) and Bertsekas (2013, 2022).

This mission formalizes the part of the paper that works under the uniform increase assumption, culminating in the paper's compactness condition for convergence of value iteration.

Setting

A model consists of a nonempty state space $S$, a control space $C$, for each $x\in S$ a nonempty constraint set $U(x)\subseteq C$, a mapping $H:S\times C\times F\to[-\infty,+\infty]$, where $F$ is the set of functions $J:S\to[-\infty,\infty]$ ordered pointwise, and a terminal function $\bar J\in F$ with $\bar J(x)>-\infty$. $H$ is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for $u\in U(x)$.

A selector is $\mu:S\to C$ with $\mu(x)\in U(x)$; a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors, and $\{\mu,\mu,\dots\}$ is stationary. Define

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$ $$J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J)(x),\qquad J^*(x)=\inf_\pi J_\pi(x),\qquad J_\infty(x)=\lim_{N\to\infty}T^N(\bar J)(x).$$

$J^*$ is the optimal value function and $J_\infty$ the limit of the dynamic programming algorithm. A policy is optimal if $J_\pi=J^*$.

Assumption I is $\bar J(x)\le H(x,u,\bar J)$ for all $x$ and $u\in U(x)$. Assumption I.1 says that $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $\bar J$. Assumption I.2 says there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+re)\le H(x,u,J)+\alpha r$ for $r>0$ and $J\ge\bar J$, where $e\equiv1$. For the convergence analysis the paper introduces, for $k\ge1$, the sets $C_k=\{(x,u,\lambda)\mid u\in U(x),\ H[x,u,T^{k-1}(\bar J)]\le\lambda\}$ with $\lambda$ real, their projections $P(C_k)$ on $(x,\lambda)$ through admissible $u$, and the closure $\overline{P(C_k)}$ obtained by adding limits of real sequences $\lambda_n$ at fixed $x$.

Formalization targets

Goal: Proposition 12

Let I, I.1, I.2 hold, let $C$ be a Hausdorff topological space, and suppose there is $\bar k$ such that $U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(\bar J)]\le\lambda\}$ is compact for every $x$, real $\lambda$ and $k\ge\bar k$. Then

$$P\Bigl(\bigcap_{k\ge1}C_k\Bigr)=\bigcap_{k\ge1}\overline{P(C_k)},\qquad J_\infty=T(J_\infty)=T(J^*)=J^*,$$

and there exists an optimal stationary policy.

Milestones

In attack order: Proposition 2 ($J_N=T^N(\bar J)$ for the $N$-stage problem); Proposition 4 ($\varepsilon$-optimal policies, stationary when $\alpha<1$); Proposition 5 (Bellman's equation $J^*=T(J^*)$ and minimality of $J^*$ among $T$-excessive functions above $\bar J$); Corollary 5.1 (the same for $J_\mu$); Proposition 7 ($\{\mu^*,\mu^*,\dots\}$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$); Proposition 10 ($J_\infty\le T(J_\infty)\le T(J^*)=J^*$, with equality throughout iff $J_\infty=T(J_\infty)$); Lemma 2 ($\overline{P(C_k)}=E[T^k(\bar J)]$, the epigraph); Proposition 11 (convergence of value iteration is equivalent to interchanging projection and intersection); Lemma 3 (a function with compact real sublevel sets attains its minimum).

Significance

The result. Proposition 12 gives a checkable condition, compactness of sublevel sets of the one-stage costs, under which value iteration started at $\bar J$ converges to the optimal cost and an optimal stationary policy exists, in any model covered by the abstract framework: deterministic and stochastic control with nonnegative costs, minimax control, and problems with state constraints encoded by infinite costs. Without such a condition the algorithm can stall below $J^*$ even in one-dimensional deterministic problems. Propositions 5 and 7 are the abstract form of the classical Bellman equation and optimality criterion for positive-cost problems.

Formalizing it. The results are proved in the paper. The platform's existing dynamic programming results are finite-state, real-valued and contraction-based; none covers extended-real costs, general state spaces, or the uniform increase regime. This mission would produce a machine-checked abstract DP layer over EReal in which the Bellman equation, the stationary-policy criterion and the convergence conditions are proved once for every model satisfying the assumptions. No machine-checked proof of these results is known.

Difficulty

The obvious argument for $J_\infty=J^*$ interchanges a limit in $N$ with an infimum over policies. Under Assumption I the iterates increase, and a limit of infima of an increasing family can be strictly smaller than the infimum of the limits; the paper's own example in Section 1 shows it. Monotone convergence arguments therefore do not apply. The paper converts the interchange into a statement about projections of the sets $C_k$ and closes the gap with a compactness argument, which requires handling infinite values carefully: epigraphs are taken over real $\lambda$ only, and states where the value is $+\infty$ are treated separately. Proposition 4, on which Bellman's equation rests, needs a selection of nearly optimal policies state by state and a geometric control of the errors through I.2.

Formalization scope

Functions in $F$ are S → EReal. Policies are sequences ℕ → Selector, where a selector is a function with $\mu(x)\in U(x)$ for all $x$. The composition $T_{\mu_0}\cdots T_{\mu_{N-1}}$ applies $T_{\mu_{N-1}}$ first. $J_\pi$ and $J_\infty$ are limUnder atTop of their defining sequences. Every statement assumes Assumption I, under which these sequences are nondecreasing and the limits exist. $T$ takes the infimum over $U(x)$ only and $J^*$ over admissible policies only. Both $S$ and each $U(x)$ are nonempty. $\lambda$ ranges over $\mathbb R$, and the closure $\overline{\,\cdot\,}$ is the sequential closure in $\lambda$ at fixed $x$, not a topological closure on $S\times\mathbb R$. The sets $C_k$ are used only for $k\ge1$. I.2 is parameterized by its scalar $\alpha$. Proposition 4's second part refers to the $\alpha$ for which I.2 is assumed.

Repairs of the page. Lemma 3 is false as printed. On $\mathbb N$ with the cofinite topology every subset is compact, yet $f(n)=-n$ has no minimum. It also fails for $U=\emptyset$. The mission states Lemma 3 for a Hausdorff space $C$ and nonempty $U$, and Proposition 12 for a Hausdorff control space. Proposition 12 is also false as printed: with $S=\{0\}$, $C=U(0)=\mathbb N$ cofinite, $\bar J(0)=0$ and $H(0,u,J)=J(0)+1/(u+1)$, all hypotheses hold but no stationary policy is optimal and (70) fails. Proposition 11(b)'s parenthetical "(equivalently there exists an optimal stationary policy)" holds only together with $J_\infty=J^*$ (the paper cites an example with an optimal stationary policy and $J_\infty\neq J^*$). It is stated in that joint form, never as an equivalence between condition (68) and the bare existence of an optimal stationary policy.

Trivializing readings ruled out. An empty constraint set would make $T\equiv+\infty$ and the policy set empty, so every Bellman identity would hold trivially. The model therefore requires $U(x)\neq\emptyset$. The goal's three conclusions, (70), the chain of equalities and the optimal stationary policy, are all required, so a formalization that states only one of them is not the goal.

Needed infrastructure: monotone limits in EReal, infima over sets, and compactness in Hausdorff spaces (Mathlib's Cantor intersection theorem). The definitions (model, assumptions, epigraph sets) can be reused for the companion mission under Assumption D and for later abstract DP developments. Proofs of any milestone are welcome, as are reusable lemmas on monotone EReal sequences.

Selected references

• D. P. Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15(3), 438–464, 1977. https://doi.org/10.1137/0315031
• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699369
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. http://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. http://web.mit.edu/dimitrib/www/abstractdp.html

Motivation

Conic quadratic programs (second-order cone programs) minimize a linear objective subject to linear constraints and constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$. They model robust linear programs with ellipsoidal uncertainty, truss topology design, contact problems with Coulomb friction, and convex quadratically constrained quadratic programs. In theory they are no harder than linear programs of the same size; in practice, linear programming software handles far larger instances than conic quadratic solvers did at the time of writing (Ben-Tal & Nemirovski 2001, pp. 193–195). This raises a question about geometry rather than algorithms: can a second-order cone be replaced by a polyhedral cone of moderate size without losing much accuracy?

The obvious answer — circumscribe the cone by a polyhedral cone with many facets — fails: the number of facets must grow exponentially in the dimension, even for constant accuracy. Ben-Tal and Nemirovski showed that auxiliary variables change the picture completely: a projection of a polyhedral cone can approximate the Lorentz cone with size only $O(k\ln(1/\varepsilon))$. The construction is now standard; it underlies, for instance, the lifted linear-programming branch-and-bound algorithm for mixed-integer conic quadratic programs of Vielma, Ahmed & Nemhauser 2008.

Setting

For $y\in\mathbb R^k$ let $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$. The $(k+1)$-dimensional Lorentz cone is

$$L^k=\{(y,t)\in\mathbb R^k\times\mathbb R\mid t\ge\|y\|_2\}.$$

Fix $\varepsilon>0$. A polyhedral $\varepsilon$-approximation of $L^k$ is a linear map

$$\Pi(y,t,u):\mathbb R^k\times\mathbb R\times\mathbb R^{p}\to\mathbb R^{q}$$

such that

1. if $(y,t)\in L^k$, there is $u\in\mathbb R^p$ with $\Pi(y,t,u)\ge0$ (componentwise);
2. if $\Pi(y,t,u)\ge0$ for some $u$, then $\|y\|_2\le(1+\varepsilon)t$.

Equivalently, the polyhedral cone $\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone lying between $L^k$ and its $(1+\varepsilon)$-extension. The size of the approximation is $p+q$: the number of auxiliary variables plus the number of linear inequalities (an equation counts as two).

The construction in the paper uses a tower of variables: for $k=2^\theta$, the coordinates $y_1,\dots,y_k$ form generation $0$, each consecutive pair of generation $\ell-1$ has a successor in generation $\ell$ ($y_i^\ell$ has parents $y_{2i-1}^{\ell-1},y_{2i}^{\ell-1}$), and the single variable of generation $\theta$ is $t$. It also uses an explicit linear system (8) in variables $\xi^j,\eta^j$, $j=0,\dots,\nu$, with trigonometric coefficients $\cos(\pi/2^{j+1})$, $\sin(\pi/2^{j+1})$, $\tan(\pi/2^{\nu+1})$, whose accuracy is $\delta(\nu)=1/\cos(\pi/2^{\nu+1})-1$.

Formalization targets

Goal: Theorem 1.1

There is an absolute constant $C$ such that for every positive integer $k$ and every $\varepsilon\in(0,1]$, $L^k$ admits a polyhedral $\varepsilon$-approximation with

$$p_k+q_k\le C\,k\ln\frac{2}{\varepsilon}.$$

The constant is not fixed; the goal asserts only the order of growth, which is what the paper claims.

Milestones

1. §2, Eq. (5). For $k=2^\theta$, $\theta\ge1$: $(y,t)$ extends to a tower solving $\sqrt{[y_{2i-1}^{\ell-1}]^2+[y_{2i}^{\ell-1}]^2}\le y_i^\ell$ for all $i,\ell$ if and only if $\|y\|_2\le t$.
2. §2, Eqs. (6)–(7). Placing polyhedral $\varepsilon_\ell$-approximations of $L^2$ on every level of the tower yields a polyhedral approximation of $L^k$ with $1+\varepsilon=\prod_{\ell=1}^\theta(1+\varepsilon_\ell)$.
3. Proposition 2.1 (i), (ii) and Eq. (9). System (8) is a polyhedral $\delta(\nu)$-approximation of $L^2$, and $\delta(\nu)=O(4^{-\nu})$.
4. Proof of Theorem 1.1, system (10), property 3. System (8) with parameter $\nu_\ell$ on level $\ell$ of the tower approximates $L^{2^\theta}$ with quality $\beta=\prod_{\ell=1}^\theta 1/\cos(\pi/2^{\nu_\ell+1})-1$.
5. Proof of Theorem 1.1, choice of $\nu_\ell$. With $\nu_\ell=\lfloor c\,\ell\ln(2/\varepsilon)\rfloor$: $\beta\le\varepsilon$ and $\sum_\ell 2^{\theta-\ell}\nu_\ell\le C\,2^\theta\ln(2/\varepsilon)$.

Significance

The theorem shows that conic quadratic constraints are, up to a factor logarithmic in the accuracy, no more expensive to express as linear constraints than they are in their native form. Consequences listed in the paper include approximating convex quadratically constrained quadratic programs, robust counterparts of linear programs with ellipsoidal uncertainty, and problems with low-dimensional cones (Coulomb friction, $k\le3$; truss design, $k\le2$) by linear programs of comparable size. Together with the matching lower bound of §3 of the same paper (a separate mission of this series), it pins down the size of the best polyhedral approximation up to constants. The recursive halving of dimensions through the tower of 3-dimensional cones is a reusable device for other rotation-invariant cones.

The result is proved in the paper; as far as is known it has not been machine-checked. This mission produces a formal proof of the construction, including the trigonometric estimate $\delta(\nu)=O(4^{-\nu})$ and the explicit linear encoding with its size count. Explicit values of the absolute constants are welcome as additional results.

Difficulty

The planar estimate is the core. Part (ii) of Proposition 2.1 must hold for every solution of the inequality system (8), not only for the solution one would write down for a given point of $L^2$; an argument that tracks only the intended solution proves part (i) and nothing about part (ii). The accuracy must also come out as $1/\cos(\pi/2^{\nu+1})-1$, geometric in $\nu$; a bound that decays only polynomially in $\nu$ would give size $\mathrm{poly}(1/\varepsilon)$ instead of $\ln(1/\varepsilon)$. The naive idea of approximating $L^k$ directly by tangent hyperplanes is ruled out by the exponential facet count mentioned above; the auxiliary variables are indispensable. The second difficulty is bookkeeping: packaging $k-1$ copies of system (8) on a tower of depth $\theta=\log_2 k$ into a single linear map, counting its variables and inequalities exactly, handling $k$ that is not a power of two, and summing the accuracies so that the total size is $O(k\ln(2/\varepsilon))$ rather than $O(k\ln k\ln(1/\varepsilon))$.

Formalization scope

• Vectors of $\mathbb R^k$ are Fin k → ℝ. The norm $\|y\|_2$ is written out as eucNorm y = Real.sqrt (∑ i, y i ^ 2); the norm Mathlib attaches to Fin k → ℝ is the sup norm, under which the cone would be polyhedral and the theorem trivial.
• A polyhedral approximation is an $\mathbb R$-linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ) and $\ge0$ is the componentwise order. Linearity is essential: with an arbitrary map, $\Pi(y,t)=t-\|y\|_2$ would be an exact approximation with $p=0$, $q=1$. Affine maps are not allowed either; the paper's approximations are homogeneous.
• The paper's absolute constants $O(1)$ are existential constants quantified before $k$, $\varepsilon$ and $\theta$. The goal requires $k\ge1$ and $\varepsilon\in(0,1]$, as in the paper; $\ln$ is Real.log.
• System (8) and system (10) are stated as propositions with the absolute values written out; their parameters $\nu$, $\nu_\ell$ are required to be positive integers, as in the paper (at $\nu=0$ the coefficient $\tan(\pi/2)$ would be evaluated as $0$ by Lean).
• Tower variables are indexed Y ℓ i with 0-based i, so the parents of Y ℓ i are Y (ℓ-1) (2i) and Y (ℓ-1) (2i+1); the milestones on (6)–(7) and (10) are stated on solution sets rather than on an explicit linear map. The size counts of (10) (properties 1–2) are not separate milestones; the arithmetic milestone on $\nu_\ell$ records the bound on $\sum_\ell 2^{\theta-\ell}\nu_\ell$ to which they reduce.
• $\delta(\nu)=O(1/4^\nu)$ is stated as $\exists C>0,\ \forall\nu\ge1,\ \delta(\nu)\le C/4^\nu$.

A complete development needs: elementary trigonometry of $\pi/2^{j}$ (available in Mathlib), rotations in the plane, finite products and sums over $\{1,\dots,\theta\}$, and a way to assemble many small linear systems into one linear map with an exact count of rows and columns. The last piece, and the tower of variables with the reduction from arbitrary $k$ to a power of two, are reusable for other lifted polyhedral approximations. Contributions of any milestone, of explicit linear encodings of (8) and (10), and of the extension from $k=2^\theta$ to all $k$ are welcome.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• J. P. Vielma, S. Ahmed and G. L. Nemhauser, A lifted linear programming branch-and-bound algorithm for mixed-integer conic quadratic programs, INFORMS Journal on Computing 20(3):438–450, 2008. https://doi.org/10.1287/ijoc.1070.0256
• A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

Motivation

Quadratic programming, the minimization of a convex quadratic function subject to linear constraints, is the simplest nonlinear extension of linear programming. It arises in least-squares estimation with sign constraints, in portfolio selection, and as the subproblem solved at each iteration of Newton-type methods for general smooth convex programs. E. M. L. Beale's 1955 paper (DOI 10.1111/j.2517-6161.1955.tb00191.x) gave one of the first finite algorithms for it by extending Dantzig's simplex method: the method keeps the simplex tableau and adds free variables, linear functions of the original variables with no sign restriction, along which the quadratic stops decreasing.

Timeline:

• 1951: Dantzig publishes the simplex method for linear programming.
• 1952: Charnes introduces ε-perturbations to resolve degeneracy in the simplex method.
• 1955: Beale extends the simplex method to convex quadratic objectives and proves that the iteration terminates (§3 of the paper; the result formalized here).
• 1959: Beale's "On quadratic programming" (Naval Research Logistics Quarterly 6) develops the method further; Wolfe's simplex method for quadratic programming (Econometrica 27) appears the same year.

Setting

There are $n$ restricted variables $x_j \ge 0$ satisfying $m$ linearly independent linear equations, and a convex quadratic objective $C$. The iteration keeps $N = n - m$ nonbasic variables $z_1, \dots, z_N$, each either a restricted variable or a free variable, and writes every restricted variable as an affine function of them:

$$x_h = a_{h0} + \sum_{l=1}^{N} a_{hl} z_l. \qquad (2.3)$$

A restricted variable that is not nonbasic is basic. The associated solution sets every $z_l = 0$, so $x_h = a_{h0}$. The objective is written as

$$C = \sum_{k=0}^{N} \sum_{l=0}^{N} c_{kl} z_k z_l, \qquad z_0 = 1, \qquad (3.1)$$

with $(c_{kl})$ symmetric. Thus $c_{00}$ is the value of $C$ at the associated solution and $2c_{k0}$ is its linear coefficient in $z_k$. The number of nonbasic free variables is $s$.

One step chooses a nonbasic $z_p$ that can profitably be altered: a free one with $c_{p0} \ne 0$ if there is one, otherwise a restricted one with $c_{p0} < 0$. It orients $z_p$ so that it is to be increased, and increases it from $0$. It stops at the first of two events. Either a basic variable $x_q$ reaches $0$ (the ratio test (2.4)), and then $x_q$ becomes nonbasic in place of $z_p$. Or $C$ stops decreasing where the free variable $u_r = c_{p0} + \sum_l c_{pl} z_l$ vanishes (3.2), and then $u_r$ becomes nonbasic in place of $z_p$. The coefficients are then transformed by substituting for $z_p$ (eqs. (3.4)–(3.6)). $C$ is in standard form when it has no linear term in any free variable.

Formalization targets

Goal: the iteration terminates

From a tableau with symmetric $(c_{kl})$, positive semidefinite quadratic block $(c_{kl})_{k,l \ge 1}$ and consistent labels, there is no infinite run

$$T_0 \to T_1 \to T_2 \to \cdots$$

of steps along which every basic variable stays strictly positive in the associated solution. No bound on the number of steps is claimed, as in the paper.

Milestones

1. Eq. (3.7): the closed form of the transformed matrix, its symmetry, and the invariance $\sum c_{kl} z_k z_l = \sum c''_{kl} z'_k z'_l$.
2. Lemma 1: when a free variable enters, its row and column vanish off the diagonal, the index $0$ included.
3. Lemma 2: a slot whose row and column vanish off the diagonal keeps this property when another free variable enters.
4. The optimality criterion (p. 175): if no nonbasic variable can profitably be altered and $C$ is convex, then $c_{00}$ is the minimum over the feasible region.
5. In standard form, $c_{00} \le C(z)$ for every $z$ with the restricted nonbasic variables at $0$.
6. $C$ decreases at every step: $c'_{00} < c_{00}$.
7. A finite run never returns to a standard form with the same set of restricted nonbasic variables.
8. If $C$ is not in standard form and $s = s_0$, then within $s_0$ steps either standard form is reached or $s$ drops, and $s$ never exceeds $s_0$ on the way.

Significance

The theorem makes Beale's method an algorithm: a finite procedure that ends either at an optimal tableau (milestone 4) or with a ray along which $C$ decreases without bound. This finiteness is what later active-set methods for quadratic programming inherit.

The result was proved in 1955. What remains is to formalize it: a machine-checked account of a simplex-type method whose state includes variables that are created during the run and later discarded. Mathlib has no simplex-type algorithm for quadratic programming, and no machine-checked proof of this theorem is known. The pivot algebra (3.4)–(3.7) and the tableau model are reusable for other pivoting methods for quadratic programs.

Difficulty

The argument for linear programming does not carry over. There, the objective strictly decreases and a basis is a subset of a finite set of columns, so no basis repeats. Here each step may create a new free variable, and nothing bounds the number of distinct free variables that can occur. Tableaux are therefore not drawn from a finite set, and a strictly decreasing objective alone does not give termination. The paper states this itself: "there is no obvious limit to the number of free variables that may be involved". The difficulty is to bound the number of steps between returns to a well-behaved tableau, and this depends both on the rule that free variables are chosen first and on how the coefficient matrix evolves under repeated pivots.

Formalization scope

• Representation. The nonbasic variables occupy fixed slots Fin (N+1). Slot 0 is $z_0 = 1$; the nonbasic slot k : Fin N is index k.succ. A pivot stores the new nonbasic variable in the slot of the variable it replaces, so the paper's index $q$ in (3.4)–(3.7) is that slot. The tableau holds the labels (restricted $x_j$ or free), the rows of all $n$ restricted variables (a nonbasic one has the unit row), and $(c_{kl})$. Free variables carry no row, as in the paper.
• The pivot. pivotC is computed literally from (3.5) and then (3.6). Rows are transformed by the same substitution, as the paper states.
• The step. The step is a relation. It allows any profitable choice of $z_p$ subject to the free-first rule, and at a tie either outcome. No pricing rule is fixed, since the paper fixes none.
• Convexity. Convexity of $C$ is the symmetry of $(c_{kl})$ plus positive semidefiniteness of the block $(c_{kl})_{k,l \ge 1}$, assumed on the initial tableau.
• Added hypothesis. The one hypothesis not on the page is that every basic restricted variable is strictly positive in the associated solution of every tableau of the run. It replaces Charnes's ε-perturbations, by which the paper ensures "the $a_{h0}$ are always positive, and not zero". Positivity is required of basic variables only; nonbasic variables are $0$ in the associated solution.
• Out of scope. The link to the original equations (2.1) and phase 1 (artificial variables, the M-method) are not formalized: the iteration starts from a tableau already in the form (2.3).
• Ruling out a trivial goal. A step relation that never fires, or a positivity hypothesis that no tableau can meet after a step, would make the goal trivially true. A sorry-free check exhibits a convex instance with consistent labels, a step, and positive basic variables before and after it.

Contributions are welcome on every milestone. The algebraic milestones 1–3 are self-contained.

Selected references

• E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2):173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
• A. Charnes, Optimality and Degeneracy in Linear Programming, Econometrica 20(2):160–170, 1952. https://doi.org/10.2307/1907845
• G. B. Dantzig, Maximization of a Linear Function of Variables Subject to Linear Inequalities, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, pp. 339–347.
• E. M. L. Beale, On Quadratic Programming, Naval Research Logistics Quarterly 6(3):227–243, 1959. https://doi.org/10.1002/nav.3800060305
• P. Wolfe, The Simplex Method for Quadratic Programming, Econometrica 27(3):382–398, 1959. https://doi.org/10.2307/1909468

Motivation

Classical non-cooperative game theory randomizes with objective, independent devices: each player spins a private wheel whose odds everyone agrees on. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) asks what changes when the randomizing events are ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. The paper introduced correlated equilibrium, and it also separates two effects that the classical model fuses: subjectivity (players disagree about probabilities) and correlation (players peg their choices on common or dependent events).

This mission formalizes the paper's result on subjectivity without correlation. Example 2.3 of the paper exhibits a three-person game in which strategies pegged on subjective but mutually secret events form an equilibrium that every player prefers to every classical mixed equilibrium. Proposition 5.1 shows that this cannot happen with two players.

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$. Player $i$ has a utility $u_i:X\to\mathbb R$; write $h_i(a)=u_i(g(a))$ for $a\in S$.

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$-field $\mathcal B$ of events, a sub-$\sigma$-field $\mathcal J_i\subseteq\mathcal B$ for each player (the events $i$ is informed about), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets $\{s_i=a\}$ lie in $\mathcal J_i$. For a profile $s=(s_1,\dots,s_n)$ of strategies the payoff of $i$ is

$$H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega),$$

computed under player $i$'s own beliefs. An equilibrium point is a profile $s$ with $H_i(s)\ge H_i(s_1,\dots,t_i,\dots,s_n)$ for every player $i$ and every strategy $t_i$ of $i$.

An event $A$ is $i$-secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$-field generated by the $\mathcal J_k$, $k\ne i$: $p_j(A\cap B)=p_j(A)p_j(B)$. A strategy is mixed if its level sets are $i$-secret, and objective if each level set has the same probability under every $p_j$. A measure is non-atomic on a $\sigma$-field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub-$\sigma$-field of $\mathcal B$ on which every $p_j$ is non-atomic. Throughout, Assumption II holds: every player $i$ has a $\sigma$-field $\mathcal R_i$ of $i$-secret events on which every $p_j$ is non-atomic.

For distributions $\sigma_i$ on $S_i$ the classical payoff is $F_i(\sigma)=\sum_{a\in S}h_i(a)\prod_j\sigma_j(a_j)$, and $\sigma$ is a Nash equilibrium point if no player gains by switching to another distribution.

Formalization targets

Goal: Proposition 5.1 (p. 78)

Let $n=2$ and assume

$$p_1(B)=0\iff p_2(B)=0\qquad\text{for every }B\in\mathcal B.\tag{5.2}$$

Then for every equilibrium point $s$ in mixed strategies there is an equilibrium point $t$ in objective mixed strategies with

$$H(s)=H(t).$$

The game need not be zero-sum.

Milestones

1. Lemma 7.1 (p. 81): in a roulette $\mathcal R$, for events $B^1,\dots,B^l$ and $\alpha\in[0,1]$, there is an objective $A\in\mathcal R$ with $p_i(A)=\alpha$ and $p_i(A\cap B^k)=p_i(A)p_i(B^k)$ for all $i,k$.
2. Lemma 4.1 (p. 77): every distribution $\sigma_i$ on $S_i$ is realised by an objective mixed strategy $s_i$ with $p\{s_i=a\}=\sigma_i(a)$.
3. Lemma 7.3 (p. 82): if every $s_j$, $j\ne i$, is mixed, then $p_i\{s=a\}=p_i\{s_i=a_i\}\,p_i\{s_j=a_j\ \forall j\ne i\}=\prod_j p_i\{s_j=a_j\}$.
4. Corollary 7.4 (p. 83): mixed strategies are independent under every $p_k$.
5. Proposition 4.3 (p. 77): $\{F(\sigma):\sigma\text{ Nash}\}=\{H(s): s\text{ an equilibrium point in objective mixed strategies}\}$.

Significance

The result. Proposition 5.1 isolates correlation as the source of the new equilibrium payoffs of the subjective model in two-person games: disagreement about probabilities alone, with strategies pegged on secret events, reproduces only payoffs already achievable by classical mixed strategies (by Proposition 4.3, only Nash equilibrium payoffs). The paper uses it to explain Example 2.9, where two zero-sum players both expect more than the value, as an effect of subjectivity combined with correlation. Proposition 4.3 is the bridge that embeds classical Nash theory in the subjective model; with Nash's theorem it gives existence of equilibrium points in every game.

Formalizing it. The results are proved in the paper; to our knowledge none of them has been machine-checked. The mission produces a reusable measure-theoretic model of randomized strategies with private information and subjective beliefs (secret events, mixed and objective strategies, roulettes), a non-atomicity notion relative to a sub-$\sigma$-field, and the Lyapunov-type construction of Lemma 7.1, none of which exists in Mathlib at the pinned revision.

Difficulty

The equilibrium conditions quantify over all strategies of the deviator, i.e. all $\mathcal J_i$-measurable maps, and the deviator may know events on which the opponent's mixed strategy is pegged. The obvious computation of $H_1(t_1,s_2)$ as a sum of products of marginal probabilities is valid only because the opponent's strategy is pegged on secret events, which is the content of Lemma 7.3; for correlated strategies it fails, and Example 2.9 shows the proposition then fails. A second obstacle is that the replacement $t_1$ must reproduce player 2's beliefs about $s_1$, while player 1's own equilibrium condition is stated under $p_1$; condition (5.2) is what transfers "$a$ is played with positive probability" from one player's beliefs to the other's. Constructing objective strategies with prescribed probabilities (Lemmas 7.1 and 4.1) needs the convexity of the range of a non-atomic vector measure (Lyapunov's theorem), which is not in Mathlib.

Formalization scope

Players are a finite type (Fin 2 in the goal, players $1,2\mapsto 0,1$); the $S_i$ and $X$ are finite types, and $g$ is surjective. The $\sigma$-field $\mathcal B$ is an explicit parameter mΩ of the structure RandomizingStructure ι Ω mΩ, which carries the $\mathcal J_i$ and the probability measures $p_i$. Probabilities are $[0,\infty]$-valued Mathlib measures. Utilities and $p_i$ are data (Assumption I is used only to compare lotteries by expected utility; the uniqueness of $p_i$ is not encoded). $H_i$ is a Bochner integral; for strategy profiles the integrand has finitely many values and is measurable, hence integrable. Non-atomicity on a sub-$\sigma$-field is defined directly; Mathlib's NoAtoms (singletons are null) would trivialize Assumption II and is not used. "Mixed" means pegged on the family of all $i$-secret events, not on the $\sigma$-field $\mathcal R_i$ of Assumption II. Classical distributions, $F_i$ and Nash equilibrium points are AGT.IsLottery, AGT.expectedPayoff and AGT.IsMixedNash from the published definition agt_games.

A formalization that restricted deviations to mixed or objective strategies, or dropped "mixed" from the hypothesis on $s$, would state a different theorem and is ruled out.

Useful contributions: Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures (or the special case needed for Lemma 7.1), the factorization of Lemma 7.3, and the payoff identities used in the proof of Proposition 4.3. The model definitions are shared in meaning with the companion mission on two-person zero-sum games.

Selected references

• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• J. Nash, Non-Cooperative Games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529
• A. Liapounoff, Sur les fonctions-vecteurs complètement additives, Izv. Akad. Nauk SSSR Ser. Mat. 4 (1940) 465–478.
• L. J. Savage, The Foundations of Statistics, Wiley, 1954.

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